Storm
A Modern Probabilistic Model Checker
|
Classes | |
class | ChoiceLabeling |
This class manages the labeling of the choice space with a number of (atomic) labels. More... | |
class | Ctmc |
This class represents a continuous-time Markov chain. More... | |
class | DeterministicModel |
The base class of all sparse deterministic models. More... | |
class | Dtmc |
This class represents a discrete-time Markov chain. More... | |
class | ItemLabeling |
A base class managing the labeling of items with a number of (atomic) labels. More... | |
class | MarkovAutomaton |
This class represents a Markov automaton. More... | |
class | Mdp |
This class represents a (discrete-time) Markov decision process. More... | |
class | Model |
Base class for all sparse models. More... | |
class | NondeterministicModel |
The base class of sparse nondeterministic models. More... | |
class | Pomdp |
This class represents a partially observable Markov decision process. More... | |
class | Smg |
This class represents a stochastic multiplayer game. More... | |
class | StandardRewardModel |
class | StateAnnotation |
class | StateLabeling |
This class manages the labeling of the state space with a number of (atomic) labels. More... | |
class | StochasticTwoPlayerGame |
This class represents a (discrete-time) stochastic two-player game. More... | |
Functions | |
std::ostream & | operator<< (std::ostream &out, ChoiceLabeling const &labeling) |
std::ostream & | operator<< (std::ostream &out, ItemLabeling const &labeling) |
std::set< storm::RationalFunctionVariable > | getProbabilityParameters (Model< storm::RationalFunction > const &model) |
Get all probability parameters occurring on transitions. | |
std::set< storm::RationalFunctionVariable > | getRewardParameters (Model< storm::RationalFunction > const &model) |
Get all parameters occurring in rewards. | |
std::set< storm::RationalFunctionVariable > | getRateParameters (Model< storm::RationalFunction > const &model) |
Get all parameters occurring in rates. | |
std::set< storm::RationalFunctionVariable > | getAllParameters (Model< storm::RationalFunction > const &model) |
Get all parameters (probability, rewards, and rates) occurring in the model. | |
template<typename ValueType > | |
std::ostream & | operator<< (std::ostream &out, StandardRewardModel< ValueType > const &rewardModel) |
std::set< storm::RationalFunctionVariable > | getRewardModelParameters (StandardRewardModel< storm::RationalFunction > const &rewModel) |
template std::ostream & | operator<<< double > (std::ostream &out, StandardRewardModel< double > const &rewardModel) |
std::ostream & | operator<< (std::ostream &out, StateLabeling const &labeling) |
std::set< storm::RationalFunctionVariable > storm::models::sparse::getAllParameters | ( | Model< storm::RationalFunction > const & | model | ) |
std::set< storm::RationalFunctionVariable > storm::models::sparse::getProbabilityParameters | ( | Model< storm::RationalFunction > const & | model | ) |
std::set< storm::RationalFunctionVariable > storm::models::sparse::getRateParameters | ( | Model< storm::RationalFunction > const & | model | ) |
std::set< storm::RationalFunctionVariable > storm::models::sparse::getRewardModelParameters | ( | StandardRewardModel< storm::RationalFunction > const & | rewModel | ) |
Definition at line 485 of file StandardRewardModel.cpp.
std::set< storm::RationalFunctionVariable > storm::models::sparse::getRewardParameters | ( | Model< storm::RationalFunction > const & | model | ) |
std::ostream & storm::models::sparse::operator<< | ( | std::ostream & | out, |
ChoiceLabeling const & | labeling | ||
) |
Definition at line 71 of file ChoiceLabeling.cpp.
std::ostream & storm::models::sparse::operator<< | ( | std::ostream & | out, |
ItemLabeling const & | labeling | ||
) |
Definition at line 227 of file ItemLabeling.cpp.
std::ostream & storm::models::sparse::operator<< | ( | std::ostream & | out, |
StandardRewardModel< ValueType > const & | rewardModel | ||
) |
Definition at line 478 of file StandardRewardModel.cpp.
std::ostream & storm::models::sparse::operator<< | ( | std::ostream & | out, |
StateLabeling const & | labeling | ||
) |
Definition at line 75 of file StateLabeling.cpp.
template std::ostream & storm::models::sparse::operator<<< double > | ( | std::ostream & | out, |
StandardRewardModel< double > const & | rewardModel | ||
) |