This class represents a continuous-time Markov chain. More...

#include <Ctmc.h>

Inheritance diagram for storm::models::symbolic::Ctmc< Type, ValueType >:

[legend]

Collaboration diagram for storm::models::symbolic::Ctmc< Type, ValueType >:

[legend]

Public Types
typedef DeterministicModel< Type, ValueType >::RewardModelType	RewardModelType
Public Types inherited from storm::models::symbolic::DeterministicModel< Type, double >
typedef Model< Type, double >::RewardModelType	RewardModelType
Public Types inherited from storm::models::symbolic::Model< Type, double >
typedef double	ValueType
typedef StandardRewardModel< Type, ValueType >	RewardModelType

Public Member Functions
	Ctmc (Ctmc< Type, ValueType > const &other)=default
Ctmc &	operator= (Ctmc< Type, ValueType > const &other)=default
	Ctmc (Ctmc< Type, ValueType > &&other)=default
Ctmc &	operator= (Ctmc< Type, ValueType > &&other)=default
	Ctmc (std::shared_ptr< storm::dd::DdManager< Type > > manager, storm::dd::Bdd< Type > reachableStates, storm::dd::Bdd< Type > initialStates, storm::dd::Bdd< Type > deadlockStates, storm::dd::Add< Type, ValueType > transitionMatrix, std::set< storm::expressions::Variable > const &rowVariables, std::shared_ptr< storm::adapters::AddExpressionAdapter< Type, ValueType > > rowExpressionAdapter, std::set< storm::expressions::Variable > const &columnVariables, std::vector< std::pair< storm::expressions::Variable, storm::expressions::Variable > > const &rowColumnMetaVariablePairs, std::map< std::string, storm::expressions::Expression > labelToExpressionMap=std::map< std::string, storm::expressions::Expression >(), std::unordered_map< std::string, RewardModelType > const &rewardModels=std::unordered_map< std::string, RewardModelType >())
	Constructs a model from the given data.
	Ctmc (std::shared_ptr< storm::dd::DdManager< Type > > manager, storm::dd::Bdd< Type > reachableStates, storm::dd::Bdd< Type > initialStates, storm::dd::Bdd< Type > deadlockStates, storm::dd::Add< Type, ValueType > transitionMatrix, boost::optional< storm::dd::Add< Type, ValueType > > exitRateVector, std::set< storm::expressions::Variable > const &rowVariables, std::shared_ptr< storm::adapters::AddExpressionAdapter< Type, ValueType > > rowExpressionAdapter, std::set< storm::expressions::Variable > const &columnVariables, std::vector< std::pair< storm::expressions::Variable, storm::expressions::Variable > > const &rowColumnMetaVariablePairs, std::map< std::string, storm::expressions::Expression > labelToExpressionMap=std::map< std::string, storm::expressions::Expression >(), std::unordered_map< std::string, RewardModelType > const &rewardModels=std::unordered_map< std::string, RewardModelType >())
	Constructs a model from the given data.
	Ctmc (std::shared_ptr< storm::dd::DdManager< Type > > manager, storm::dd::Bdd< Type > reachableStates, storm::dd::Bdd< Type > initialStates, storm::dd::Bdd< Type > deadlockStates, storm::dd::Add< Type, ValueType > transitionMatrix, std::set< storm::expressions::Variable > const &rowVariables, std::set< storm::expressions::Variable > const &columnVariables, std::vector< std::pair< storm::expressions::Variable, storm::expressions::Variable > > const &rowColumnMetaVariablePairs, std::map< std::string, storm::dd::Bdd< Type > > labelToBddMap=std::map< std::string, storm::dd::Bdd< Type > >(), std::unordered_map< std::string, RewardModelType > const &rewardModels=std::unordered_map< std::string, RewardModelType >())
	Constructs a model from the given data.
	Ctmc (std::shared_ptr< storm::dd::DdManager< Type > > manager, storm::dd::Bdd< Type > reachableStates, storm::dd::Bdd< Type > initialStates, storm::dd::Bdd< Type > deadlockStates, storm::dd::Add< Type, ValueType > transitionMatrix, boost::optional< storm::dd::Add< Type, ValueType > > exitRateVector, std::set< storm::expressions::Variable > const &rowVariables, std::set< storm::expressions::Variable > const &columnVariables, std::vector< std::pair< storm::expressions::Variable, storm::expressions::Variable > > const &rowColumnMetaVariablePairs, std::map< std::string, storm::dd::Bdd< Type > > labelToBddMap=std::map< std::string, storm::dd::Bdd< Type > >(), std::unordered_map< std::string, RewardModelType > const &rewardModels=std::unordered_map< std::string, RewardModelType >())
	Constructs a model from the given data.
storm::dd::Add< Type, ValueType > const &	getExitRateVector () const
	Retrieves the exit rate vector of the CTMC.
virtual void	reduceToStateBasedRewards () override
	Converts the transition rewards of all reward models to state-based rewards.
storm::dd::Add< Type, ValueType >	computeProbabilityMatrix () const
template<typename NewValueType>
std::shared_ptr< Ctmc< Type, NewValueType > >	toValueType () const
Public Member Functions inherited from storm::models::symbolic::DeterministicModel< Type, double >
	DeterministicModel (DeterministicModel< Type, double > const &other)=default
DeterministicModel &	operator= (DeterministicModel< Type, double > const &other)=default
Public Member Functions inherited from storm::models::symbolic::Model< Type, double >
void	addParameters (std::set< storm::RationalFunctionVariable > const &parameters)
std::set< storm::RationalFunctionVariable > const &	getParameters () const
	Model (Model< Type, ValueType > const &other)=default
Model &	operator= (Model< Type, ValueType > const &other)=default
virtual uint_fast64_t	getNumberOfStates () const override
	Returns the number of states of the model.
virtual uint_fast64_t	getNumberOfTransitions () const override
	Returns the number of (non-zero) transitions of the model.
virtual uint_fast64_t	getNumberOfChoices () const override
	Returns the number of choices ine the model.
storm::dd::DdManager< Type > &	getManager () const
	Retrieves the manager responsible for the DDs that represent this model.
std::shared_ptr< storm::dd::DdManager< Type > > const &	getManagerAsSharedPointer () const
	Retrieves the manager responsible for the DDs that represent this model.
storm::dd::Bdd< Type > const &	getReachableStates () const
	Retrieves the reachable states of the model.
storm::dd::Bdd< Type > const &	getInitialStates () const
	Retrieves the initial states of the model.
storm::dd::Bdd< Type > const &	getDeadlockStates () const
virtual storm::dd::Bdd< Type >	getStates (std::string const &label) const
	Returns the sets of states labeled with the given label.
virtual storm::expressions::Expression	getExpression (std::string const &label) const
	Returns the expression for the given label.
virtual bool	hasLabel (std::string const &label) const
	Retrieves whether the given label is a valid label in this model.
storm::dd::Add< Type, ValueType > const &	getTransitionMatrix () const
	Retrieves the matrix representing the transitions of the model.
virtual storm::dd::Bdd< Type >	getQualitativeTransitionMatrix (bool keepNondeterminism=true) const
	Retrieves the matrix qualitatively (i.e.
std::set< storm::expressions::Variable > const &	getRowVariables () const
	Retrieves the meta variables used to encode the rows of the transition matrix and the vector indices.
std::set< storm::expressions::Variable > const &	getColumnVariables () const
	Retrieves the meta variables used to encode the columns of the transition matrix and the vector indices.
std::set< storm::expressions::Variable >	getRowAndNondeterminismVariables () const
	Retrieves all meta variables used to encode rows and nondetermism.
std::set< storm::expressions::Variable >	getColumnAndNondeterminismVariables () const
	Retrieves all meta variables used to encode columns and nondetermism.
virtual std::set< storm::expressions::Variable > const &	getNondeterminismVariables () const
	Retrieves all meta variables used to encode the nondeterminism.
std::vector< std::pair< storm::expressions::Variable, storm::expressions::Variable > > const &	getRowColumnMetaVariablePairs () const
	Retrieves the pairs of row and column meta variables.
storm::dd::Add< Type, ValueType >	getRowColumnIdentity () const
	Retrieves an ADD that represents the diagonal of the transition matrix.
virtual bool	hasRewardModel (std::string const &rewardModelName) const override
	Retrieves whether the model has a reward model with the given name.
RewardModelType const &	getRewardModel (std::string const &rewardModelName) const
	Retrieves the reward model with the given name, if one exists.
RewardModelType const &	getUniqueRewardModel () const
	Retrieves the unique reward model, if there exists exactly one.
virtual std::string const &	getUniqueRewardModelName () const override
	Retrieves the name of the unique reward model, if there exists exactly one.
virtual bool	hasUniqueRewardModel () const override
	Retrieves whether the model has a unique reward model.
std::unordered_map< std::string, RewardModelType > &	getRewardModels ()
virtual void	printModelInformationToStream (std::ostream &out) const override
	Prints information about the model to the specified stream.
virtual bool	isSymbolicModel () const override
	Checks whether the model is a symbolic model.
virtual std::optional< storm::dd::DdType >	getDdType () const override
virtual bool	isExact () const override
	Checks whether the model is exact.
virtual bool	supportsParameters () const override
	Checks whether the model supports parameters.
virtual bool	hasParameters () const override
	Checks whether the model has parameters.
std::vector< std::string >	getLabels () const
std::enable_if<!std::is_same< ValueType, NewValueType >::value, std::shared_ptr< Model< Type, NewValueType > > >::type	toValueType () const
void	writeDotToFile (std::string const &filename) const
Public Member Functions inherited from storm::models::Model< double >
	Model (ModelType const &modelType)
	Constructs a model of the given type.
virtual	~Model ()=default
Public Member Functions inherited from storm::models::ModelBase
	ModelBase (ModelType const &modelType)
	Constructs a model of the given type.
virtual	~ModelBase ()
template<typename ModelType>
std::shared_ptr< ModelType >	as ()
	Casts the model into the model type given by the template parameter.
template<typename ModelType>
std::shared_ptr< ModelType const >	as () const
	Casts the model into the model type given by the template parameter.
virtual ModelType	getType () const
	Return the actual type of the model.
virtual bool	isSparseModel () const
	Checks whether the model is a sparse model.
virtual bool	supportsUncertainty () const
	Does it support uncertainty (e.g., via interval-valued entries).
bool	isOfType (storm::models::ModelType const &modelType) const
	Checks whether the model is of the given type.
bool	isNondeterministicModel () const
	Returns true if the model is a nondeterministic model.
bool	isDiscreteTimeModel () const
	Returns true if the model is a descrete-time model.
virtual bool	isPartiallyObservable () const

Additional Inherited Members
Static Public Attributes inherited from storm::models::symbolic::Model< Type, double >
static const storm::dd::DdType	DdType
static const storm::models::ModelRepresentation	Representation
Protected Member Functions inherited from storm::models::symbolic::Model< Type, double >
std::map< std::string, storm::expressions::Expression > const &	getLabelToExpressionMap () const
	Retrieves the mapping of labels to their defining expressions.
std::map< std::string, storm::dd::Bdd< Type > > const &	getLabelToBddMap () const
	Retrieves the mapping of labels to their defining expressions.
void	printModelInformationHeaderToStream (std::ostream &out) const
	Prints the information header (number of states and transitions) of the model to the specified stream.
void	printModelInformationFooterToStream (std::ostream &out) const
	Prints the information footer (reward models, labels) of the model to the specified stream.
void	printRewardModelsInformationToStream (std::ostream &out) const
	Prints information about the reward models to the specified stream.
virtual void	printDdVariableInformationToStream (std::ostream &out) const
	Prints information about the DD variables to the specified stream.
std::shared_ptr< storm::adapters::AddExpressionAdapter< Type, ValueType > > const &	getRowExpressionAdapter () const
	Retrieves the expression adapter of this model.
Protected Attributes inherited from storm::models::symbolic::Model< Type, double >
storm::dd::Add< Type, ValueType >	transitionMatrix

Detailed Description

template<storm::dd::DdType Type, typename ValueType = double>
class storm::models::symbolic::Ctmc< Type, ValueType >

This class represents a continuous-time Markov chain.

Definition at line 13 of file Ctmc.h.

Member Typedef Documentation

◆ RewardModelType

template<storm::dd::DdType Type, typename ValueType = double>

typedef DeterministicModel<Type,ValueType>::RewardModelType storm::models::symbolic::Ctmc< Type, ValueType >::RewardModelType

Definition at line 15 of file Ctmc.h.

Constructor & Destructor Documentation

◆ Ctmc() [1/6]

template<storm::dd::DdType Type, typename ValueType = double>

storm::models::symbolic::Ctmc< Type, ValueType >::Ctmc ( Ctmc< Type, ValueType > const & other )

default

◆ Ctmc() [2/6]

template<storm::dd::DdType Type, typename ValueType = double>

storm::models::symbolic::Ctmc< Type, ValueType >::Ctmc ( Ctmc< Type, ValueType > && other )

default

◆ Ctmc() [3/6]

template<storm::dd::DdType Type, typename ValueType>

storm::models::symbolic::Ctmc< Type, ValueType >::Ctmc	(	std::shared_ptr< storm::dd::DdManager< Type > >	manager,
		storm::dd::Bdd< Type >	reachableStates,
		storm::dd::Bdd< Type >	initialStates,
		storm::dd::Bdd< Type >	deadlockStates,
		storm::dd::Add< Type, ValueType >	transitionMatrix,
		std::set< storm::expressions::Variable > const &	rowVariables,
		std::shared_ptr< storm::adapters::AddExpressionAdapter< Type, ValueType > >	rowExpressionAdapter,
		std::set< storm::expressions::Variable > const &	columnVariables,
		std::vector< std::pair< storm::expressions::Variable, storm::expressions::Variable > > const &	rowColumnMetaVariablePairs,
		std::map< std::string, storm::expressions::Expression >	labelToExpressionMap = std::map<std::string, storm::expressions::Expression>(),
		std::unordered_map< std::string, RewardModelType > const &	rewardModels = std::unordered_map<std::string, RewardModelType>() )

Constructs a model from the given data.

Parameters

manager	The manager responsible for the decision diagrams.
reachableStates	A DD representing the reachable states.
initialStates	A DD representing the initial states of the model.
deadlockStates	A DD representing the deadlock states of the model.
transitionMatrix	The matrix representing the transitions in the model.
rowVariables	The set of row meta variables used in the DDs.
rowExpressionAdapter	An object that can be used to translate expressions in terms of the row meta variables.
columVariables	The set of column meta variables used in the DDs.
rowColumnMetaVariablePairs	All pairs of row/column meta variables.
labelToExpressionMap	A mapping from label names to their defining expressions.
rewardModels	The reward models associated with the model.

Definition at line 14 of file Ctmc.cpp.

◆ Ctmc() [4/6]

template<storm::dd::DdType Type, typename ValueType>

storm::models::symbolic::Ctmc< Type, ValueType >::Ctmc	(	std::shared_ptr< storm::dd::DdManager< Type > >	manager,
		storm::dd::Bdd< Type >	reachableStates,
		storm::dd::Bdd< Type >	initialStates,
		storm::dd::Bdd< Type >	deadlockStates,
		storm::dd::Add< Type, ValueType >	transitionMatrix,
		boost::optional< storm::dd::Add< Type, ValueType > >	exitRateVector,
		std::set< storm::expressions::Variable > const &	rowVariables,
		std::shared_ptr< storm::adapters::AddExpressionAdapter< Type, ValueType > >	rowExpressionAdapter,
		std::set< storm::expressions::Variable > const &	columnVariables,
		std::vector< std::pair< storm::expressions::Variable, storm::expressions::Variable > > const &	rowColumnMetaVariablePairs,
		std::map< std::string, storm::expressions::Expression >	labelToExpressionMap = std::map<std::string, storm::expressions::Expression>(),
		std::unordered_map< std::string, RewardModelType > const &	rewardModels = std::unordered_map<std::string, RewardModelType>() )

Constructs a model from the given data.

Parameters

manager	The manager responsible for the decision diagrams.
reachableStates	A DD representing the reachable states.
initialStates	A DD representing the initial states of the model.
deadlockStates	A DD representing the deadlock states of the model.
transitionMatrix	The matrix representing the transitions in the model.
exitRateVector	The vector specifying the exit rates for the states.
rowVariables	The set of row meta variables used in the DDs.
rowExpressionAdapter	An object that can be used to translate expressions in terms of the row meta variables.
columVariables	The set of column meta variables used in the DDs.
rowColumnMetaVariablePairs	All pairs of row/column meta variables.
labelToExpressionMap	A mapping from label names to their defining expressions.
rewardModels	The reward models associated with the model.

Definition at line 28 of file Ctmc.cpp.

◆ Ctmc() [5/6]

template<storm::dd::DdType Type, typename ValueType>

storm::models::symbolic::Ctmc< Type, ValueType >::Ctmc	(	std::shared_ptr< storm::dd::DdManager< Type > >	manager,
		storm::dd::Bdd< Type >	reachableStates,
		storm::dd::Bdd< Type >	initialStates,
		storm::dd::Bdd< Type >	deadlockStates,
		storm::dd::Add< Type, ValueType >	transitionMatrix,
		std::set< storm::expressions::Variable > const &	rowVariables,
		std::set< storm::expressions::Variable > const &	columnVariables,
		std::vector< std::pair< storm::expressions::Variable, storm::expressions::Variable > > const &	rowColumnMetaVariablePairs,
		std::map< std::string, storm::dd::Bdd< Type > >	labelToBddMap = std::map<std::string, storm::dd::Bdd<Type>>(),
		std::unordered_map< std::string, RewardModelType > const &	rewardModels = std::unordered_map<std::string, RewardModelType>() )

Constructs a model from the given data.

Parameters

manager	The manager responsible for the decision diagrams.
reachableStates	A DD representing the reachable states.
initialStates	A DD representing the initial states of the model.
deadlockStates	A DD representing the deadlock states of the model.
transitionMatrix	The matrix representing the transitions in the model.
rowVariables	The set of row meta variables used in the DDs.
columVariables	The set of column meta variables used in the DDs.
rowColumnMetaVariablePairs	All pairs of row/column meta variables.
labelToBddMap	A mapping from label names to their defining BDDs.
rewardModels	The reward models associated with the model.

Definition at line 43 of file Ctmc.cpp.

◆ Ctmc() [6/6]

template<storm::dd::DdType Type, typename ValueType>

storm::models::symbolic::Ctmc< Type, ValueType >::Ctmc	(	std::shared_ptr< storm::dd::DdManager< Type > >	manager,
		storm::dd::Bdd< Type >	reachableStates,
		storm::dd::Bdd< Type >	initialStates,
		storm::dd::Bdd< Type >	deadlockStates,
		storm::dd::Add< Type, ValueType >	transitionMatrix,
		boost::optional< storm::dd::Add< Type, ValueType > >	exitRateVector,
		std::set< storm::expressions::Variable > const &	rowVariables,
		std::set< storm::expressions::Variable > const &	columnVariables,
		std::vector< std::pair< storm::expressions::Variable, storm::expressions::Variable > > const &	rowColumnMetaVariablePairs,
		std::map< std::string, storm::dd::Bdd< Type > >	labelToBddMap = std::map<std::string, storm::dd::Bdd<Type>>(),
		std::unordered_map< std::string, RewardModelType > const &	rewardModels = std::unordered_map<std::string, RewardModelType>() )

Constructs a model from the given data.

Parameters

manager	The manager responsible for the decision diagrams.
reachableStates	A DD representing the reachable states.
initialStates	A DD representing the initial states of the model.
deadlockStates	A DD representing the deadlock states of the model.
transitionMatrix	The matrix representing the transitions in the model.
exitRateVector	The vector specifying the exit rates for the states.
rowVariables	The set of row meta variables used in the DDs.
columVariables	The set of column meta variables used in the DDs.
rowColumnMetaVariablePairs	All pairs of row/column meta variables.
labelToBddMap	A mapping from label names to their defining BDDs.
rewardModels	The reward models associated with the model.

Definition at line 54 of file Ctmc.cpp.

Member Function Documentation

◆ computeProbabilityMatrix()

template<storm::dd::DdType Type, typename ValueType>

storm::dd::Add< Type, ValueType > storm::models::symbolic::Ctmc< Type, ValueType >::computeProbabilityMatrix ( ) const

Returns: the probabilistic transition matrix P

Note: getTransitionMatrix() retrieves the exit rate matrix R, where R(s,s') = r(s) * P(s,s')

Definition at line 85 of file Ctmc.cpp.

◆ getExitRateVector()

template<storm::dd::DdType Type, typename ValueType>

storm::dd::Add< Type, ValueType > const & storm::models::symbolic::Ctmc< Type, ValueType >::getExitRateVector ( ) const

Retrieves the exit rate vector of the CTMC.

Returns: The exit rate vector.

Definition at line 67 of file Ctmc.cpp.

◆ operator=() [1/2]

template<storm::dd::DdType Type, typename ValueType = double>

Ctmc & storm::models::symbolic::Ctmc< Type, ValueType >::operator= ( Ctmc< Type, ValueType > && other )

default

◆ operator=() [2/2]

template<storm::dd::DdType Type, typename ValueType = double>

Ctmc & storm::models::symbolic::Ctmc< Type, ValueType >::operator= ( Ctmc< Type, ValueType > const & other )

default

◆ reduceToStateBasedRewards()

template<storm::dd::DdType Type, typename ValueType>

void storm::models::symbolic::Ctmc< Type, ValueType >::reduceToStateBasedRewards ( )

overridevirtual

Converts the transition rewards of all reward models to state-based rewards.

For deterministic models, this reduces the rewards to state rewards only. For nondeterminstic models, the reward models will contain state rewards and state-action rewards. Note that this transformation does not preserve all properties, but it preserves expected rewards.

Implements storm::models::ModelBase.

Definition at line 75 of file Ctmc.cpp.

◆ toValueType()

template<storm::dd::DdType Type, typename ValueType>

template<typename NewValueType>

template std::shared_ptr< Ctmc< storm::dd::DdType::Sylvan, double > > storm::models::symbolic::Ctmc< Type, ValueType >::toValueType ( ) const

Definition at line 91 of file Ctmc.cpp.

The documentation for this class was generated from the following files:

src/storm/models/symbolic/Ctmc.h
src/storm/models/symbolic/Ctmc.cpp

Public Types

Public Member Functions

Additional Inherited Members

Detailed Description

Member Typedef Documentation

◆ RewardModelType

Constructor & Destructor Documentation

◆ Ctmc() [1/6]

◆ Ctmc() [2/6]

◆ Ctmc() [3/6]

◆ Ctmc() [4/6]

◆ Ctmc() [5/6]

◆ Ctmc() [6/6]

Member Function Documentation

◆ computeProbabilityMatrix()

◆ getExitRateVector()

◆ operator=() [1/2]

◆ operator=() [2/2]

◆ reduceToStateBasedRewards()

◆ toValueType()