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

#include <Ctmc.h>

Inheritance diagram for storm::models::sparse::Ctmc< ValueType, RewardModelType >:

[legend]

Collaboration diagram for storm::models::sparse::Ctmc< ValueType, RewardModelType >:

[legend]

Public Member Functions
	Ctmc (storm::storage::SparseMatrix< ValueType > const &rateMatrix, 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.

	Ctmc (storm::storage::SparseMatrix< ValueType > &&rateMatrix, storm::models::sparse::StateLabeling &&stateLabeling, std::unordered_map< std::string, RewardModelType > &&rewardModels=std::unordered_map< std::string, RewardModelType >())
	Constructs a model by moving the given data.

	Ctmc (storm::storage::sparse::ModelComponents< ValueType, RewardModelType > const &components)
	Constructs a model from the given data.

	Ctmc (storm::storage::sparse::ModelComponents< ValueType, RewardModelType > &&components)

	Ctmc (Ctmc< ValueType, RewardModelType > const &ctmc)=default

Ctmc &	operator= (Ctmc< ValueType, RewardModelType > const &ctmc)=default

	Ctmc (Ctmc< ValueType, RewardModelType > &&ctmc)=default

Ctmc &	operator= (Ctmc< ValueType, RewardModelType > &&ctmc)=default

std::vector< ValueType > const &	getExitRateVector () const
	Retrieves the vector of exit rates of the model.

std::vector< ValueType > &	getExitRateVector ()
	Retrieves the vector of exit rates of the model.

virtual void	reduceToStateBasedRewards () override
	Converts the transition rewards of all reward models to state-based rewards.

storm::storage::SparseMatrix< ValueType >	computeProbabilityMatrix () const

Public Member Functions inherited from storm::models::sparse::DeterministicModel< ValueType, RewardModelType >
	DeterministicModel (ModelType modelType, storm::storage::sparse::ModelComponents< ValueType, RewardModelType > const &components)
	Constructs a model from the given data.

	DeterministicModel (ModelType modelType, storm::storage::sparse::ModelComponents< ValueType, RewardModelType > &&components)

	DeterministicModel (DeterministicModel< ValueType, RewardModelType > const &other)=default

DeterministicModel &	operator= (DeterministicModel< ValueType, RewardModelType > const &other)=default

	DeterministicModel (DeterministicModel< ValueType, RewardModelType > &&other)=default

DeterministicModel< ValueType, RewardModelType > &	operator= (DeterministicModel< ValueType, RewardModelType > &&model)=default

virtual	~DeterministicModel ()=default

virtual void	writeDotToStream (std::ostream &outStream, size_t maxWidthLabel=30, bool includeLabeling=true, storm::storage::BitVector const subsystem=nullptr, std::vector< ValueType > const firstValue=nullptr, std::vector< ValueType > const secondValue=nullptr, std::vector< uint_fast64_t > const stateColoring=nullptr, std::vector< std::string > const colors=nullptr, std::vector< uint_fast64_t > scheduler=nullptr, bool finalizeOutput=true) const override

Public Member Functions inherited from storm::models::sparse::Model< CValueType, CRewardModelType >
	Model (Model< ValueType, RewardModelType > const &other)=default

Model &	operator= (Model< ValueType, RewardModelType > const &other)=default

	Model (ModelType modelType, storm::storage::sparse::ModelComponents< ValueType, RewardModelType > const &components)
	Constructs a model from the given data.

	Model (ModelType modelType, storm::storage::sparse::ModelComponents< ValueType, RewardModelType > &&components)

virtual	~Model ()=default

storm::storage::SparseMatrix< ValueType >	getBackwardTransitions () const
	Retrieves the backward transition relation of the model, i.e.

virtual storm::storage::SparseMatrix< ValueType >::const_rows	getRows (storm::storage::sparse::state_type state) const
	Returns an object representing the matrix rows associated with the given state.

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::storage::BitVector const &	getInitialStates () const
	Retrieves the initial states of the model.

void	setInitialStates (storm::storage::BitVector const &states)
	Overwrites the initial states of the model.

storm::storage::BitVector const &	getStates (std::string const &label) const
	Returns the sets of states labeled with the given label.

bool	hasLabel (std::string const &label) const
	Retrieves whether the given label is a valid label in this model.

storm::storage::SparseMatrix< ValueType > const &	getTransitionMatrix () const
	Retrieves the matrix representing the transitions of the model.

storm::storage::SparseMatrix< ValueType > &	getTransitionMatrix ()
	Retrieves the matrix representing the transitions of the model.

std::unordered_map< std::string, RewardModelType > const &	getRewardModels () const
	Retrieves the reward models.

std::unordered_map< std::string, RewardModelType > &	getRewardModels ()
	Retrieves the reward models.

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 &	getRewardModel (std::string const &rewardModelName)
	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.

RewardModelType &	getUniqueRewardModel ()
	Retrieves the unique reward model, if there exists exactly one.

virtual bool	hasUniqueRewardModel () const override
	Retrieves whether the model has a unique reward model.

virtual std::string const &	getUniqueRewardModelName () const override
	Retrieves the name of the unique reward model, if there exists exactly one.

bool	hasRewardModel () const
	Retrieves whether the model has at least one reward model.

uint_fast64_t	getNumberOfRewardModels () const
	Retrieves the number of reward models associated with this model.

void	addRewardModel (std::string const &rewardModelName, RewardModelType const &rewModel)
	Adds a reward model to the model.

bool	removeRewardModel (std::string const &rewardModelName)
	Removes the reward model with the given name from the model.

void	restrictRewardModels (std::set< std::string > const &keptRewardModels)
	Removes all reward models whose name is not in the given set.

storm::models::sparse::StateLabeling const &	getStateLabeling () const
	Returns the state labeling associated with this model.

storm::models::sparse::StateLabeling &	getStateLabeling ()
	Returns the state labeling associated with this model.

bool	hasChoiceLabeling () const
	Retrieves whether this model has a labeling of the choices.

storm::models::sparse::ChoiceLabeling const &	getChoiceLabeling () const
	Retrieves the labels for the choices of the model.

std::optional< storm::models::sparse::ChoiceLabeling > const &	getOptionalChoiceLabeling () const
	Retrieves an optional value that contains the choice labeling if there is one.

std::optional< storm::models::sparse::ChoiceLabeling > &	getOptionalChoiceLabeling ()
	Retrieves an optional value that contains the choice labeling if there is one.

bool	hasStateValuations () const
	Retrieves whether this model was build with state valuations.

storm::storage::sparse::StateValuations const &	getStateValuations () const
	Retrieves the valuations of the states of the model.

std::optional< storm::storage::sparse::StateValuations > const &	getOptionalStateValuations () const
	Retrieves an optional value that contains the state valuations if there are some.

std::optional< storm::storage::sparse::StateValuations > &	getOptionalStateValuations ()
	Retrieves an optional value that contains the state valuations if there are some.

bool	hasChoiceOrigins () const
	Retrieves whether this model was build with choice origins.

std::shared_ptr< storm::storage::sparse::ChoiceOrigins > const &	getChoiceOrigins () const
	Retrieves the origins of the choices of the model.

std::optional< std::shared_ptr< storm::storage::sparse::ChoiceOrigins > > const &	getOptionalChoiceOrigins () const
	Retrieves an optional value that contains the choice origins if there are some.

std::optional< std::shared_ptr< storm::storage::sparse::ChoiceOrigins > > &	getOptionalChoiceOrigins ()
	Retrieves an optional value that contains the choice origins if there are some.

virtual void	printModelInformationToStream (std::ostream &out) const override
	Prints information about the model to the specified stream.

bool	isSinkState (uint64_t sink) const

virtual void	writeDotToStream (std::ostream &outStream, size_t maxWidthLabel=30, bool includeLabeling=true, storm::storage::BitVector const subsystem=nullptr, std::vector< ValueType > const firstValue=nullptr, std::vector< ValueType > const secondValue=nullptr, std::vector< uint64_t > const stateColoring=nullptr, std::vector< std::string > const colors=nullptr, std::vector< uint_fast64_t > scheduler=nullptr, bool finalizeOutput=true) const
	Exports the model to the dot-format and prints the result to the given stream.

virtual void	writeJsonToStream (std::ostream &outStream) const
	Writes a JSON representation of the model to the given stream.

std::set< std::string >	getLabelsOfState (storm::storage::sparse::state_type state) const
	Retrieves the set of labels attached to the given state.

virtual bool	isSparseModel () const override
	Checks whether the model is a sparse model.

virtual bool	supportsParameters () const override
	Checks whether the model supports parameters.

virtual bool	hasParameters () const override
	Checks whether the model has parameters.

virtual bool	isExact () const override
	Checks whether the model is exact.

virtual bool	supportsUncertainty () const override
	Does it support uncertainty (e.g., via interval-valued entries).

virtual bool	hasUncertainty () const
	Checks whether the model actually is uncertain, i.e., whether there is a non-singleton transition relation.

virtual std::size_t	hash () const

void	writeJsonToStream (std::ostream &) const

Public Member Functions inherited from storm::models::Model< CValueType >
	Model (ModelType const &modelType)
	Constructs a model of the given type.

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	isSymbolicModel () const
	Checks whether the model is a symbolic model.

virtual std::optional< storm::dd::DdType >	getDdType () const

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
Public Types inherited from storm::models::sparse::Model< CValueType, CRewardModelType >
typedef CValueType	ValueType

typedef CRewardModelType	RewardModelType

Static Public Attributes inherited from storm::models::sparse::Model< CValueType, CRewardModelType >
static const storm::models::ModelRepresentation	Representation = ModelRepresentation::Sparse

Protected Member Functions inherited from storm::models::sparse::Model< CValueType, CRewardModelType >
RewardModelType &	rewardModel (std::string const &rewardModelName)

void	setTransitionMatrix (storm::storage::SparseMatrix< ValueType > const &transitionMatrix)
	Sets the transition matrix of the model.

void	setTransitionMatrix (storm::storage::SparseMatrix< ValueType > &&transitionMatrix)
	Sets the transition matrix of the model.

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 and size in memory) of the model to the specified stream.

void	printRewardModelsInformationToStream (std::ostream &out) const
	Prints information about the reward models to the specified stream.

virtual std::string	additionalDotStateInfo (uint64_t state) const
	Return a string that is additonally added to the state information in the dot stream.

Detailed Description

template<class ValueType, typename RewardModelType = StandardRewardModel<ValueType>>
class storm::models::sparse::Ctmc< ValueType, RewardModelType >

This class represents a continuous-time Markov chain.

Definition at line 14 of file Ctmc.h.

Constructor & Destructor Documentation

◆ Ctmc() [1/6]

template<typename ValueType , typename RewardModelType >

storm::models::sparse::Ctmc< ValueType, RewardModelType >::Ctmc	(	storm::storage::SparseMatrix< ValueType > const &	rateMatrix,
		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.

Parameters

rateMatrix	The matrix representing the transitions in the model.
stateLabeling	The labeling of the states.
rewardModels	A mapping of reward model names to reward models.

Definition at line 11 of file Ctmc.cpp.

◆ Ctmc() [2/6]

template<typename ValueType , typename RewardModelType >

storm::models::sparse::Ctmc< ValueType, RewardModelType >::Ctmc	(	storm::storage::SparseMatrix< ValueType > &&	rateMatrix,
		storm::models::sparse::StateLabeling &&	stateLabeling,
		std::unordered_map< std::string, RewardModelType > &&	rewardModels = `std::unordered_map<std::string, RewardModelType>()`
	)

Constructs a model by moving the given data.

Parameters

rateMatrix	The matrix representing the transitions in the model.
stateLabeling	The labeling of the states.
rewardModels	A mapping of reward model names to reward models.

Definition at line 18 of file Ctmc.cpp.

◆ Ctmc() [3/6]

template<typename ValueType , typename RewardModelType >

storm::models::sparse::Ctmc< ValueType, RewardModelType >::Ctmc ( storm::storage::sparse::ModelComponents< ValueType, RewardModelType > const & components )

Constructs a model from the given data.

Parameters

components The components for this model.

Definition at line 26 of file Ctmc.cpp.

◆ Ctmc() [4/6]

template<typename ValueType , typename RewardModelType >

storm::models::sparse::Ctmc< ValueType, RewardModelType >::Ctmc ( storm::storage::sparse::ModelComponents< ValueType, RewardModelType > && components )

Definition at line 41 of file Ctmc.cpp.

◆ Ctmc() [5/6]

template<class ValueType , typename RewardModelType = StandardRewardModel<ValueType>>

storm::models::sparse::Ctmc< ValueType, RewardModelType >::Ctmc ( Ctmc< ValueType, RewardModelType > const & ctmc )

default

◆ Ctmc() [6/6]

template<class ValueType , typename RewardModelType = StandardRewardModel<ValueType>>

storm::models::sparse::Ctmc< ValueType, RewardModelType >::Ctmc ( Ctmc< ValueType, RewardModelType > && ctmc )

default

Member Function Documentation

◆ computeProbabilityMatrix()

template<typename ValueType , typename RewardModelType >

storm::storage::SparseMatrix< ValueType > storm::models::sparse::Ctmc< ValueType, RewardModelType >::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 82 of file Ctmc.cpp.

◆ getExitRateVector() [1/2]

template<typename ValueType , typename RewardModelType >

std::vector< ValueType > & storm::models::sparse::Ctmc< ValueType, RewardModelType >::getExitRateVector ( )

Retrieves the vector of exit rates of the model.

Returns: The exit rate vector.

Definition at line 61 of file Ctmc.cpp.

◆ getExitRateVector() [2/2]

template<typename ValueType , typename RewardModelType >

std::vector< ValueType > const & storm::models::sparse::Ctmc< ValueType, RewardModelType >::getExitRateVector ( ) const

Retrieves the vector of exit rates of the model.

Returns: The exit rate vector.

Definition at line 56 of file Ctmc.cpp.

◆ operator=() [1/2]

template<class ValueType , typename RewardModelType = StandardRewardModel<ValueType>>

Ctmc & storm::models::sparse::Ctmc< ValueType, RewardModelType >::operator= ( Ctmc< ValueType, RewardModelType > && ctmc )

default

◆ operator=() [2/2]

template<class ValueType , typename RewardModelType = StandardRewardModel<ValueType>>

Ctmc & storm::models::sparse::Ctmc< ValueType, RewardModelType >::operator= ( Ctmc< ValueType, RewardModelType > const & ctmc )

default

◆ reduceToStateBasedRewards()

template<typename ValueType , typename RewardModelType >

void storm::models::sparse::Ctmc< ValueType, RewardModelType >::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.

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

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

Public Member Functions

Additional Inherited Members

Detailed Description

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() [1/2]

◆ getExitRateVector() [2/2]

◆ operator=() [1/2]

◆ operator=() [2/2]

◆ reduceToStateBasedRewards()