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_SPARSE_STOCHASTICTWOPLAYERGAME_H_
2#define STORM_MODELS_SPARSE_STOCHASTICTWOPLAYERGAME_H_
3
5
6namespace storm {
7namespace models {
8namespace sparse {
9
13template<class ValueType, typename RewardModelType = StandardRewardModel<ValueType>>
14class StochasticTwoPlayerGame : public NondeterministicModel<ValueType, RewardModelType> {
15 public:
26 std::unordered_map<std::string, RewardModelType> const& rewardModels = std::unordered_map<std::string, RewardModelType>()),
27
38 std::unordered_map<std::string, RewardModelType>&& rewardModels = std::unordered_map<std::string, RewardModelType>()),
39
47
50
53
60
68
74 bool hasPlayer2ChoiceLabeling() const;
75
82
83 private:
84 // A matrix that stores the player 1 choices. This matrix contains a row group for each player 1 node. Every
85 // row group contains a row for each choice in that player 1 node. Each such row contains exactly one
86 // (non-zero) entry at a column that indicates the player 2 node this choice leads to (which is essentially
87 // the index of a row group in the matrix for player 2).
89
90 // The matrix for player 2 are stored in the superclass.
91};
92
93} // namespace sparse
94} // namespace models
95} // namespace storm
96
97#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.