You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
176 lines
9.9 KiB
176 lines
9.9 KiB
#ifndef STORM_MODELCHECKER_GAMEBASEDMDPMODELCHECKER_H_
|
|
#define STORM_MODELCHECKER_GAMEBASEDMDPMODELCHECKER_H_
|
|
|
|
#include "storm/modelchecker/AbstractModelChecker.h"
|
|
|
|
#include "storm/storage/prism/Program.h"
|
|
|
|
#include "storm/storage/dd/DdType.h"
|
|
#include "storm/storage/dd/Odd.h"
|
|
|
|
#include "storm/storage/SymbolicModelDescription.h"
|
|
|
|
#include "storm/abstraction/SymbolicQualitativeGameResult.h"
|
|
#include "storm/abstraction/SymbolicQualitativeGameResultMinMax.h"
|
|
#include "storm/abstraction/ExplicitQuantitativeResult.h"
|
|
|
|
#include "storm/logic/Bound.h"
|
|
|
|
#include "storm/settings/modules/AbstractionSettings.h"
|
|
|
|
#include "storm/utility/ConstantsComparator.h"
|
|
#include "storm/utility/solver.h"
|
|
#include "storm/utility/graph.h"
|
|
#include "storm/utility/Stopwatch.h"
|
|
|
|
namespace storm {
|
|
namespace abstraction {
|
|
template<storm::dd::DdType Type, typename ValueType>
|
|
class MenuGame;
|
|
|
|
template<storm::dd::DdType Type, typename ValueType>
|
|
class MenuGameAbstractor;
|
|
|
|
template<storm::dd::DdType Type, typename ValueType>
|
|
class MenuGameRefiner;
|
|
|
|
template<storm::dd::DdType Type>
|
|
class SymbolicQualitativeGameResultMinMax;
|
|
|
|
template<storm::dd::DdType Type, typename ValueType>
|
|
class SymbolicQuantitativeGameResult;
|
|
|
|
class ExplicitQualitativeGameResult;
|
|
class ExplicitQualitativeGameResultMinMax;
|
|
|
|
template<typename ValueType>
|
|
class ExplicitQuantitativeResultMinMax;
|
|
|
|
class ExplicitGameStrategy;
|
|
class ExplicitGameStrategyPair;
|
|
}
|
|
|
|
namespace modelchecker {
|
|
|
|
using storm::abstraction::SymbolicQualitativeGameResult;
|
|
using storm::abstraction::SymbolicQualitativeGameResultMinMax;
|
|
using storm::abstraction::ExplicitQualitativeGameResult;
|
|
using storm::abstraction::ExplicitQualitativeGameResultMinMax;
|
|
using storm::abstraction::ExplicitQuantitativeResult;
|
|
using storm::abstraction::ExplicitQuantitativeResultMinMax;
|
|
|
|
namespace detail {
|
|
template<typename ValueType>
|
|
struct PreviousExplicitResult {
|
|
ExplicitQuantitativeResult<ValueType> values;
|
|
storm::dd::Odd odd;
|
|
|
|
void clear() {
|
|
odd = storm::dd::Odd();
|
|
values = ExplicitQuantitativeResult<ValueType>();
|
|
}
|
|
};
|
|
}
|
|
|
|
template<storm::dd::DdType Type, typename ModelType>
|
|
class GameBasedMdpModelChecker : public AbstractModelChecker<ModelType> {
|
|
public:
|
|
typedef typename ModelType::ValueType ValueType;
|
|
|
|
/*!
|
|
* Constructs a model checker whose underlying model is implicitly given by the provided program. All
|
|
* verification calls will be answererd with respect to this model.
|
|
*
|
|
* @param model The model description that (symbolically) specifies the model to check.
|
|
* @param smtSolverFactory A factory used to create SMT solver when necessary.
|
|
*/
|
|
explicit GameBasedMdpModelChecker(storm::storage::SymbolicModelDescription const& model, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>());
|
|
|
|
/// Overridden methods from super class.
|
|
virtual bool canHandle(CheckTask<storm::logic::Formula> const& checkTask) const override;
|
|
virtual std::unique_ptr<CheckResult> computeUntilProbabilities(Environment const& env, CheckTask<storm::logic::UntilFormula> const& checkTask) override;
|
|
virtual std::unique_ptr<CheckResult> computeReachabilityProbabilities(Environment const& env, CheckTask<storm::logic::EventuallyFormula> const& checkTask) override;
|
|
|
|
private:
|
|
/*!
|
|
* Performs the core part of the abstraction-refinement loop.
|
|
*/
|
|
std::unique_ptr<CheckResult> performGameBasedAbstractionRefinement(Environment const& env, CheckTask<storm::logic::Formula> const& checkTask, storm::expressions::Expression const& constraintExpression, storm::expressions::Expression const& targetStateExpression);
|
|
|
|
std::unique_ptr<CheckResult> performSymbolicAbstractionSolutionStep(Environment const& env, CheckTask<storm::logic::Formula> const& checkTask, storm::abstraction::MenuGame<Type, ValueType> const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd<Type> const& initialStates, storm::dd::Bdd<Type> const& constraintStates, storm::dd::Bdd<Type> const& targetStates, storm::abstraction::MenuGameRefiner<Type, ValueType> const& refiner, boost::optional<SymbolicQualitativeGameResultMinMax<Type>>& previousQualitativeResult, boost::optional<abstraction::SymbolicQuantitativeGameResult<Type, ValueType>>& previousMinQuantitativeResult);
|
|
std::unique_ptr<CheckResult> performExplicitAbstractionSolutionStep(Environment const& env, CheckTask<storm::logic::Formula> const& checkTask, storm::abstraction::MenuGame<Type, ValueType> const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd<Type> const& initialStates, storm::dd::Bdd<Type> const& constraintStates, storm::dd::Bdd<Type> const& targetStates, storm::abstraction::MenuGameRefiner<Type, ValueType> const& refiner, boost::optional<detail::PreviousExplicitResult<ValueType>>& previousResult);
|
|
|
|
/*!
|
|
* Retrieves the initial predicates for the abstraction.
|
|
*/
|
|
std::vector<storm::expressions::Expression> getInitialPredicates(storm::expressions::Expression const& constraintExpression, storm::expressions::Expression const& targetStateExpression);
|
|
|
|
/*!
|
|
* Derives the optimization direction of player 1.
|
|
*/
|
|
storm::OptimizationDirection getPlayer1Direction(CheckTask<storm::logic::Formula> const& checkTask);
|
|
|
|
/*!
|
|
* Performs a qualitative check on the the given game to compute the (player 1) states that have probability
|
|
* 0 or 1, respectively, to reach a target state and only visiting constraint states before.
|
|
*/
|
|
SymbolicQualitativeGameResultMinMax<Type> computeProb01States(boost::optional<SymbolicQualitativeGameResultMinMax<Type>> const& previousQualitativeResult, storm::abstraction::MenuGame<Type, ValueType> const& game, storm::OptimizationDirection player1Direction, storm::dd::Bdd<Type> const& transitionMatrixBdd, storm::dd::Bdd<Type> const& constraintStates, storm::dd::Bdd<Type> const& targetStates);
|
|
|
|
ExplicitQualitativeGameResultMinMax computeProb01States(boost::optional<detail::PreviousExplicitResult<ValueType>> const& previousResult, storm::dd::Odd const& odd, storm::OptimizationDirection player1Direction, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<uint64_t> const& player1RowGrouping, storm::storage::SparseMatrix<ValueType> const& player1BackwardTransitions, std::vector<uint64_t> const& player2BackwardTransitions, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, abstraction::ExplicitGameStrategyPair& minStrategyPair, abstraction::ExplicitGameStrategyPair& maxStrategyPair);
|
|
|
|
void printStatistics(storm::abstraction::MenuGameAbstractor<Type, ValueType> const& abstractor, storm::abstraction::MenuGame<Type, ValueType> const& game, uint64_t refinements, uint64_t peakPlayer1States, uint64_t peakTransitions) const;
|
|
|
|
/*
|
|
* Retrieves the expression characterized by the formula. The formula needs to be propositional.
|
|
*/
|
|
storm::expressions::Expression getExpression(storm::logic::Formula const& formula);
|
|
|
|
/// The preprocessed model that contains only one module/automaton and otherwhise corresponds to the semantics
|
|
/// of the original model description.
|
|
storm::storage::SymbolicModelDescription preprocessedModel;
|
|
|
|
/// A factory that is used for creating SMT solvers when needed.
|
|
std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory;
|
|
|
|
/// A comparator that can be used for detecting convergence.
|
|
storm::utility::ConstantsComparator<ValueType> comparator;
|
|
|
|
/// A flag indicating whether to reuse the qualitative results.
|
|
bool reuseQualitativeResults;
|
|
|
|
/// A flag indicating whether to reuse the quantitative results.
|
|
bool reuseQuantitativeResults;
|
|
|
|
/// The maximal number of abstractions to perform.
|
|
uint64_t maximalNumberOfAbstractions;
|
|
|
|
/// The mode selected for solving the abstraction.
|
|
storm::settings::modules::AbstractionSettings::SolveMode solveMode;
|
|
|
|
/// The currently used abstractor.
|
|
std::shared_ptr<storm::abstraction::MenuGameAbstractor<Type, ValueType>> abstractor;
|
|
|
|
/// The performed number of refinement iterations.
|
|
uint64_t iteration;
|
|
|
|
/// A flag indicating whether to fix player 1 strategies.
|
|
bool fixPlayer1Strategy;
|
|
|
|
/// A flag indicating whether to fix player 2 strategies.
|
|
bool fixPlayer2Strategy;
|
|
|
|
/// A flag that indicates whether debug mode is enabled.
|
|
bool debug;
|
|
|
|
/// Data stored for statistics.
|
|
storm::utility::Stopwatch totalAbstractionWatch;
|
|
storm::utility::Stopwatch totalSolutionWatch;
|
|
storm::utility::Stopwatch totalRefinementWatch;
|
|
storm::utility::Stopwatch totalTranslationWatch;
|
|
storm::utility::Stopwatch totalStrategyProcessingWatch;
|
|
storm::utility::Stopwatch totalWatch;
|
|
};
|
|
}
|
|
}
|
|
|
|
#endif /* STORM_MODELCHECKER_GAMEBASEDMDPMODELCHECKER_H_ */
|