Storm
A Modern Probabilistic Model Checker
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
GameBasedMdpModelChecker.h
Go to the documentation of this file.
1#ifndef STORM_MODELCHECKER_GAMEBASEDMDPMODELCHECKER_H_
2#define STORM_MODELCHECKER_GAMEBASEDMDPMODELCHECKER_H_
3
5
6#include <boost/algorithm/string.hpp>
7
9
12
14
18
19#include "storm/logic/Bound.h"
20
22
25
28#include "storm/utility/graph.h"
30
31namespace storm::gbar {
32namespace abstraction {
33
34template<storm::dd::DdType Type, typename ValueType>
35class MenuGame;
36
37template<storm::dd::DdType Type, typename ValueType>
38class MenuGameAbstractor;
39
40template<storm::dd::DdType Type, typename ValueType>
41class MenuGameRefiner;
42
43template<storm::dd::DdType Type>
44class SymbolicQualitativeGameResultMinMax;
45
46template<storm::dd::DdType Type, typename ValueType>
47class SymbolicQuantitativeGameResult;
48
49class ExplicitQualitativeGameResult;
50class ExplicitQualitativeGameResultMinMax;
51
52template<typename ValueType>
53class ExplicitQuantitativeResultMinMax;
54
55class ExplicitGameStrategy;
56class ExplicitGameStrategyPair;
57} // namespace abstraction
58
59namespace modelchecker {
60
67
68namespace detail {
69template<typename ValueType>
79} // namespace detail
80
83 GameBasedMdpModelCheckerOptions(std::vector<storm::expressions::Expression> const& constraints,
84 std::vector<std::vector<storm::expressions::Expression>> const& injectedRefinementPredicates)
86 // Intentionally left empty.
87 }
88
89 std::vector<storm::expressions::Expression> constraints;
90 std::vector<std::vector<storm::expressions::Expression>> injectedRefinementPredicates;
91};
92
93template<storm::dd::DdType Type, typename ModelType>
95 public:
96 typedef typename ModelType::ValueType ValueType;
97
108 std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory =
109 std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>());
110
112 virtual bool canHandle(storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> const& checkTask) const override;
113 virtual std::unique_ptr<storm::modelchecker::CheckResult> computeUntilProbabilities(
115 virtual std::unique_ptr<storm::modelchecker::CheckResult> computeReachabilityProbabilities(
117
118 private:
122 std::unique_ptr<storm::modelchecker::CheckResult> performGameBasedAbstractionRefinement(
124 storm::expressions::Expression const& constraintExpression, storm::expressions::Expression const& targetStateExpression);
125
126 std::unique_ptr<storm::modelchecker::CheckResult> performSymbolicAbstractionSolutionStep(
129 storm::dd::Bdd<Type> const& initialStates, storm::dd::Bdd<Type> const& constraintStates, storm::dd::Bdd<Type> const& targetStates,
131 boost::optional<SymbolicQualitativeGameResultMinMax<Type>>& previousQualitativeResult,
132 boost::optional<abstraction::SymbolicQuantitativeGameResult<Type, ValueType>>& previousMinQuantitativeResult);
133 std::unique_ptr<storm::modelchecker::CheckResult> performExplicitAbstractionSolutionStep(
136 storm::dd::Bdd<Type> const& initialStates, storm::dd::Bdd<Type> const& constraintStates, storm::dd::Bdd<Type> const& targetStates,
138
142 std::vector<storm::expressions::Expression> getInitialPredicates(storm::expressions::Expression const& constraintExpression,
143 storm::expressions::Expression const& targetStateExpression);
144
149
154 SymbolicQualitativeGameResultMinMax<Type> computeProb01States(boost::optional<SymbolicQualitativeGameResultMinMax<Type>> const& previousQualitativeResult,
156 storm::OptimizationDirection player1Direction,
157 storm::dd::Bdd<Type> const& transitionMatrixBdd, storm::dd::Bdd<Type> const& constraintStates,
158 storm::dd::Bdd<Type> const& targetStates);
159
160 ExplicitQualitativeGameResultMinMax computeProb01States(
161 boost::optional<detail::PreviousExplicitResult<ValueType>> const& previousResult, storm::dd::Odd const& odd,
162 storm::OptimizationDirection player1Direction, storm::storage::SparseMatrix<ValueType> const& transitionMatrix,
163 std::vector<uint64_t> const& player1RowGrouping, storm::storage::SparseMatrix<ValueType> const& player1BackwardTransitions,
164 std::vector<uint64_t> const& player2BackwardTransitions, storm::storage::BitVector const& constraintStates,
165 storm::storage::BitVector const& targetStates, storage::ExplicitGameStrategyPair& minStrategyPair, storage::ExplicitGameStrategyPair& maxStrategyPair);
166
167 void printStatistics(storm::gbar::abstraction::MenuGameAbstractor<Type, ValueType> const& abstractor,
168 storm::gbar::abstraction::MenuGame<Type, ValueType> const& game, uint64_t refinements, uint64_t peakPlayer1States,
169 uint64_t peakTransitions) const;
170
171 /*
172 * Retrieves the expression characterized by the formula. The formula needs to be propositional.
173 */
174 storm::expressions::Expression getExpression(storm::logic::Formula const& formula);
175
178
182
184 std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory;
185
188
190 bool reuseQualitativeResults;
191
193 bool reuseQuantitativeResults;
194
196 uint64_t maximalNumberOfAbstractions;
197
200
202 std::shared_ptr<storm::gbar::abstraction::MenuGameAbstractor<Type, ValueType>> abstractor;
203
205 uint64_t iteration;
206
208 bool fixPlayer1Strategy;
209
211 bool fixPlayer2Strategy;
212
214 bool debug;
215
217 storm::utility::Stopwatch totalAbstractionWatch;
218 storm::utility::Stopwatch totalSolutionWatch;
219 storm::utility::Stopwatch totalRefinementWatch;
220 storm::utility::Stopwatch totalTranslationWatch;
221 storm::utility::Stopwatch totalStrategyProcessingWatch;
222 storm::utility::Stopwatch setupWatch;
223 storm::utility::Stopwatch totalWatch;
224};
225} // namespace modelchecker
226} // namespace storm::gbar
227
228#endif /* STORM_MODELCHECKER_GAMEBASEDMDPMODELCHECKER_H_ */
This class represents a discrete-time stochastic two-player game.
Definition MenuGame.h:16
virtual std::unique_ptr< storm::modelchecker::CheckResult > computeReachabilityProbabilities(Environment const &env, storm::modelchecker::CheckTask< storm::logic::EventuallyFormula, ValueType > const &checkTask) override
virtual std::unique_ptr< storm::modelchecker::CheckResult > computeUntilProbabilities(Environment const &env, storm::modelchecker::CheckTask< storm::logic::UntilFormula, ValueType > const &checkTask) override
virtual bool canHandle(storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &checkTask) const override
Overridden methods from super class.
A bit vector that is internally represented as a vector of 64-bit values.
Definition BitVector.h:18
A class that holds a possibly non-square matrix in the compressed row storage format.
A class that provides convenience operations to display run times.
Definition Stopwatch.h:14
GameBasedMdpModelCheckerOptions(std::vector< storm::expressions::Expression > const &constraints, std::vector< std::vector< storm::expressions::Expression > > const &injectedRefinementPredicates)
std::vector< std::vector< storm::expressions::Expression > > injectedRefinementPredicates
std::vector< storm::expressions::Expression > constraints