Storm 1.11.1.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
StochasticTwoPlayerGame.cpp
Go to the documentation of this file.
2
5
6namespace storm {
7namespace models {
8namespace sparse {
9
10template<typename ValueType, typename RewardModelType>
13 storm::models::sparse::StateLabeling const& stateLabeling, std::unordered_map<std::string, RewardModelType> const& rewardModels)
15 storm::storage::sparse::ModelComponents<ValueType, RewardModelType>(player2Matrix, stateLabeling, rewardModels, false, boost::none, player1Matrix)) {
16 // Intentionally left empty.
17}
18
19template<typename ValueType, typename RewardModelType>
23 std::unordered_map<std::string, RewardModelType>&& rewardModels)
25 std::move(player2Matrix), std::move(stateLabeling), std::move(rewardModels), false, boost::none, std::move(player1Matrix))) {
26 // Intentionally left empty.
27}
28
29template<typename ValueType, typename RewardModelType>
35
36template<typename ValueType, typename RewardModelType>
38 : NondeterministicModel<ValueType, RewardModelType>(ModelType::S2pg, std::move(components)), player1Matrix(std::move(components.player1Matrix.get())) {
39 // Intentionally left empty
40}
41
42template<typename ValueType, typename RewardModelType>
46
47template<typename ValueType, typename RewardModelType>
51
52template<typename ValueType, typename RewardModelType>
54 return this->hasChoiceLabeling();
55}
56
57template<typename ValueType, typename RewardModelType>
61
67
68} // namespace sparse
69} // namespace models
70} // 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.