Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
StochasticTwoPlayerGame.h
Go to the documentation of this file.
1#ifndef STORM_MODELS_SPARSE_STOCHASTICTWOPLAYERGAME_H_
2#define STORM_MODELS_SPARSE_STOCHASTICTWOPLAYERGAME_H_
3
6
7namespace storm {
8namespace models {
9namespace sparse {
10
14template<class ValueType, typename RewardModelType = StandardRewardModel<ValueType>>
15class StochasticTwoPlayerGame : public NondeterministicModel<ValueType, RewardModelType> {
16 public:
27 std::unordered_map<std::string, RewardModelType> const& rewardModels = std::unordered_map<std::string, RewardModelType>()),
28
39 std::unordered_map<std::string, RewardModelType>&& rewardModels = std::unordered_map<std::string, RewardModelType>()),
40
48
51
54
61
69
75 bool hasPlayer2ChoiceLabeling() const;
76
83
84 private:
85 // A matrix that stores the player 1 choices. This matrix contains a row group for each player 1 node. Every
86 // row group contains a row for each choice in that player 1 node. Each such row contains exactly one
87 // (non-zero) entry at a column that indicates the player 2 node this choice leads to (which is essentially
88 // the index of a row group in the matrix for player 2).
90
91 // The matrix for player 2 are stored in the superclass.
92};
93
94} // namespace sparse
95} // namespace models
96} // namespace storm
97
98#endif /* STORM_MODELS_SPARSE_STOCHASTICTWOPLAYERGAME_H_ */
This class manages the labeling of the choice space with a number of (atomic) labels.
The base class of sparse nondeterministic models.
This class manages the labeling of the state space with a number of (atomic) labels.
This class represents a (discrete-time) stochastic two-player game.
bool hasPlayer2ChoiceLabeling() const
Retrieves whether the game has labels attached to player 2 states.
storm::storage::SparseMatrix< storm::storage::sparse::state_type > const & getPlayer1Matrix() const
Retrieves the matrix representing the choices in player 1 states.
StochasticTwoPlayerGame & operator=(StochasticTwoPlayerGame &&other)=default
StochasticTwoPlayerGame & operator=(StochasticTwoPlayerGame const &other)=default
StochasticTwoPlayerGame(StochasticTwoPlayerGame &&other)=default
storm::storage::SparseMatrix< ValueType > const & getPlayer2Matrix() const
Retrieves the matrix representing the choices in player 2 states and the associated probability distr...
StochasticTwoPlayerGame(StochasticTwoPlayerGame const &other)=default
storm::models::sparse::ChoiceLabeling const & getPlayer2ChoiceLabeling() const
Retrieves the labels attached to the choices of player 2 states.
A class that holds a possibly non-square matrix in the compressed row storage format.
LabParser.cpp.
Definition cli.cpp:18