Storm 1.10.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
StochasticTwoPlayerGame.h
Go to the documentation of this file.
1#ifndef STORM_MODELS_SYMBOLIC_STOCHASTICTWOPLAYERGAME_H_
2#define STORM_MODELS_SYMBOLIC_STOCHASTICTWOPLAYERGAME_H_
3
5
6namespace storm {
7namespace models {
8namespace symbolic {
9
13template<storm::dd::DdType Type, typename ValueType = double>
14class StochasticTwoPlayerGame : public NondeterministicModel<Type, ValueType> {
15 public:
17
20
23
44 std::shared_ptr<storm::dd::DdManager<Type>> manager, storm::dd::Bdd<Type> reachableStates, storm::dd::Bdd<Type> initialStates,
45 storm::dd::Bdd<Type> deadlockStates, storm::dd::Add<Type, ValueType> transitionMatrix, std::set<storm::expressions::Variable> const& rowVariables,
46 std::shared_ptr<storm::adapters::AddExpressionAdapter<Type, ValueType>> rowExpressionAdapter,
47 std::set<storm::expressions::Variable> const& columnVariables,
48 std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs,
49 std::set<storm::expressions::Variable> const& player1Variables, std::set<storm::expressions::Variable> const& player2Variables,
50 std::set<storm::expressions::Variable> const& allNondeterminismVariables,
51 std::map<std::string, storm::expressions::Expression> labelToExpressionMap = std::map<std::string, storm::expressions::Expression>(),
52 std::unordered_map<std::string, RewardModelType> const& rewardModels = std::unordered_map<std::string, RewardModelType>());
53
71 StochasticTwoPlayerGame(std::shared_ptr<storm::dd::DdManager<Type>> manager, storm::dd::Bdd<Type> reachableStates, storm::dd::Bdd<Type> initialStates,
73 std::set<storm::expressions::Variable> const& rowVariables, std::set<storm::expressions::Variable> const& columnVariables,
74 std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs,
75 std::set<storm::expressions::Variable> const& player1Variables, std::set<storm::expressions::Variable> const& player2Variables,
76 std::set<storm::expressions::Variable> const& allNondeterminismVariables,
77 std::map<std::string, storm::dd::Bdd<Type>> labelToBddMap = std::map<std::string, storm::dd::Bdd<Type>>(),
78 std::unordered_map<std::string, RewardModelType> const& rewardModels = std::unordered_map<std::string, RewardModelType>());
79
85 std::set<storm::expressions::Variable> const& getPlayer1Variables() const;
86
92 std::set<storm::expressions::Variable> const& getPlayer2Variables() const;
93
100
107
108 template<typename NewValueType>
109 std::shared_ptr<StochasticTwoPlayerGame<Type, NewValueType>> toValueType() const;
110
114 uint64_t getNumberOfPlayer2States() const;
115
116 private:
120 void createIllegalMasks();
121
122 // A mask that characterizes all illegal player 1 choices.
123 storm::dd::Bdd<Type> illegalPlayer1Mask;
124
125 // A mask that characterizes all illegal player 2 choices.
126 storm::dd::Bdd<Type> illegalPlayer2Mask;
127
128 // The meta variables used to encode the nondeterministic choices of player 1.
129 std::set<storm::expressions::Variable> player1Variables;
130
131 // The meta variables used to encode the nondeterministic choices of player 2.
132 std::set<storm::expressions::Variable> player2Variables;
133};
134
135} // namespace symbolic
136} // namespace models
137} // namespace storm
138
139#endif /* STORM_MODELS_SYMBOLIC_STOCHASTICTWOPLAYERGAME_H_ */
storm::dd::Add< Type, ValueType > transitionMatrix
Definition Model.h:410
Base class for all nondeterministic symbolic models.
This class represents a discrete-time stochastic two-player game.
NondeterministicModel< Type, ValueType >::RewardModelType RewardModelType
StochasticTwoPlayerGame & operator=(StochasticTwoPlayerGame< Type, ValueType > &&other)=default
std::set< storm::expressions::Variable > const & getPlayer1Variables() const
Retrieeves the set of meta variables used to encode the nondeterministic choices of player 1.
std::set< storm::expressions::Variable > const & getPlayer2Variables() const
Retrieeves the set of meta variables used to encode the nondeterministic choices of player 2.
storm::dd::Bdd< Type > getIllegalPlayer1Mask() const
Retrieves a BDD characterizing all illegal player 1 choice encodings in the model.
std::shared_ptr< StochasticTwoPlayerGame< Type, NewValueType > > toValueType() const
StochasticTwoPlayerGame & operator=(StochasticTwoPlayerGame< Type, ValueType > const &other)=default
StochasticTwoPlayerGame(StochasticTwoPlayerGame< Type, ValueType > &&other)=default
uint64_t getNumberOfPlayer2States() const
Retrieves the number of player 2 states in the game.
storm::dd::Bdd< Type > getIllegalPlayer2Mask() const
Retrieves a BDD characterizing all illegal player 2 choice encodings in the model.
StochasticTwoPlayerGame(StochasticTwoPlayerGame< Type, ValueType > const &other)=default
LabParser.cpp.