Storm 1.11.1.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
StochasticTwoPlayerGame.cpp
Go to the documentation of this file.
2
7
8namespace storm {
9namespace models {
10namespace sparse {
11
12template<typename ValueType, typename RewardModelType>
15 storm::models::sparse::StateLabeling const& stateLabeling, std::unordered_map<std::string, RewardModelType> const& rewardModels)
17 storm::storage::sparse::ModelComponents<ValueType, RewardModelType>(player2Matrix, stateLabeling, rewardModels, false, boost::none, player1Matrix)) {
18 // Intentionally left empty.
19}
20
21template<typename ValueType, typename RewardModelType>
25 std::unordered_map<std::string, RewardModelType>&& rewardModels)
27 std::move(player2Matrix), std::move(stateLabeling), std::move(rewardModels), false, boost::none, std::move(player1Matrix))) {
28 // Intentionally left empty.
29}
30
31template<typename ValueType, typename RewardModelType>
37
38template<typename ValueType, typename RewardModelType>
40 : NondeterministicModel<ValueType, RewardModelType>(ModelType::S2pg, std::move(components)), player1Matrix(std::move(components.player1Matrix.get())) {
41 // Intentionally left empty
42}
43
44template<typename ValueType, typename RewardModelType>
48
49template<typename ValueType, typename RewardModelType>
53
54template<typename ValueType, typename RewardModelType>
56 return this->hasChoiceLabeling();
57}
58
59template<typename ValueType, typename RewardModelType>
63
69
70} // namespace sparse
71} // namespace models
72} // namespace storm
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.
storm::storage::SparseMatrix< ValueType > const & getPlayer2Matrix() const
Retrieves the matrix representing the choices in player 2 states and the associated probability distr...
StochasticTwoPlayerGame(storm::storage::SparseMatrix< storm::storage::sparse::state_type > const &player1Matrix, storm::storage::SparseMatrix< ValueType > const &player2Matrix, storm::models::sparse::StateLabeling const &stateLabeling, std::unordered_map< std::string, RewardModelType > const &rewardModels=std::unordered_map< std::string, RewardModelType >())
Constructs a model from the given data.
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.