Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
storm::models::sparse Namespace Reference

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::RationalFunctionVariablegetProbabilityParameters (Model< storm::RationalFunction > const &model)
 Get all probability parameters occurring on transitions.
 
std::set< storm::RationalFunctionVariablegetRewardParameters (Model< storm::RationalFunction > const &model)
 Get all parameters occurring in rewards.
 
std::set< storm::RationalFunctionVariablegetRateParameters (Model< storm::RationalFunction > const &model)
 Get all parameters occurring in rates.
 
std::set< storm::RationalFunctionVariablegetAllParameters (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::RationalFunctionVariablegetRewardModelParameters (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)
 

Function Documentation

◆ getAllParameters()

std::set< storm::RationalFunctionVariable > storm::models::sparse::getAllParameters ( Model< storm::RationalFunction > const &  model)

Get all parameters (probability, rewards, and rates) occurring in the model.

Parameters
modelModel.
Returns
Set of parameters.

Definition at line 728 of file Model.cpp.

◆ getProbabilityParameters()

std::set< storm::RationalFunctionVariable > storm::models::sparse::getProbabilityParameters ( Model< storm::RationalFunction > const &  model)

Get all probability parameters occurring on transitions.

Parameters
modelModel.
Returns
Set of parameters.

Definition at line 703 of file Model.cpp.

◆ getRateParameters()

std::set< storm::RationalFunctionVariable > storm::models::sparse::getRateParameters ( Model< storm::RationalFunction > const &  model)

Get all parameters occurring in rates.

Parameters
modelModel.
Returns
Set of parameters. If model is not a continuous time model, the returned set is empty.

Definition at line 716 of file Model.cpp.

◆ getRewardModelParameters()

std::set< storm::RationalFunctionVariable > storm::models::sparse::getRewardModelParameters ( StandardRewardModel< storm::RationalFunction > const &  rewModel)

Definition at line 485 of file StandardRewardModel.cpp.

◆ getRewardParameters()

std::set< storm::RationalFunctionVariable > storm::models::sparse::getRewardParameters ( Model< storm::RationalFunction > const &  model)

Get all parameters occurring in rewards.

Parameters
modelModel.
Returns
Set of parameters.

Definition at line 707 of file Model.cpp.

◆ operator<<() [1/4]

std::ostream & storm::models::sparse::operator<< ( std::ostream &  out,
ChoiceLabeling const &  labeling 
)

Definition at line 71 of file ChoiceLabeling.cpp.

◆ operator<<() [2/4]

std::ostream & storm::models::sparse::operator<< ( std::ostream &  out,
ItemLabeling const &  labeling 
)

Definition at line 227 of file ItemLabeling.cpp.

◆ operator<<() [3/4]

template<typename ValueType >
std::ostream & storm::models::sparse::operator<< ( std::ostream &  out,
StandardRewardModel< ValueType > const &  rewardModel 
)

Definition at line 478 of file StandardRewardModel.cpp.

◆ operator<<() [4/4]

std::ostream & storm::models::sparse::operator<< ( std::ostream &  out,
StateLabeling const &  labeling 
)

Definition at line 75 of file StateLabeling.cpp.

◆ operator<<< double >()

template std::ostream & storm::models::sparse::operator<<< double > ( std::ostream &  out,
StandardRewardModel< double > const &  rewardModel 
)