Base class for all sparse models. More...

#include <Model.h>

Inheritance diagram for storm::models::sparse::Model< CValueType, CRewardModelType >:

[legend]

Collaboration diagram for storm::models::sparse::Model< CValueType, CRewardModelType >:

[legend]

Public Types
typedef CValueType	ValueType

typedef CRewardModelType	RewardModelType

Public Member Functions
	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
	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.

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

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

Static Public Attributes
static const storm::models::ModelRepresentation	Representation = ModelRepresentation::Sparse

Protected Member Functions
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 CValueType, class CRewardModelType = StandardRewardModel<CValueType>>
class storm::models::sparse::Model< CValueType, CRewardModelType >

Base class for all sparse models.

Definition at line 33 of file Model.h.

Member Typedef Documentation

◆ RewardModelType

template<class CValueType , class CRewardModelType = StandardRewardModel<CValueType>>

typedef CRewardModelType storm::models::sparse::Model< CValueType, CRewardModelType >::RewardModelType

Definition at line 36 of file Model.h.

◆ ValueType

template<class CValueType , class CRewardModelType = StandardRewardModel<CValueType>>

typedef CValueType storm::models::sparse::Model< CValueType, CRewardModelType >::ValueType

Definition at line 35 of file Model.h.

Constructor & Destructor Documentation

◆ Model() [1/3]

template<class CValueType , class CRewardModelType = StandardRewardModel<CValueType>>

storm::models::sparse::Model< CValueType, CRewardModelType >::Model ( Model< ValueType, RewardModelType > const & other )

default

◆ Model() [2/3]

template<typename ValueType , typename RewardModelType >

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

Constructs a model from the given data.

Parameters

modelType	the type of this model
components	The components for this model.

Definition at line 26 of file Model.cpp.

◆ Model() [3/3]

template<typename ValueType , typename RewardModelType >

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

Definition at line 38 of file Model.cpp.

◆ ~Model()

template<class CValueType , class CRewardModelType = StandardRewardModel<CValueType>>

virtual storm::models::sparse::Model< CValueType, CRewardModelType >::~Model ( )

virtualdefault

Reimplemented from storm::models::Model< CValueType >.

Member Function Documentation

◆ additionalDotStateInfo()

template<typename ValueType , typename RewardModelType >

std::string storm::models::sparse::Model< ValueType, RewardModelType >::additionalDotStateInfo ( uint64_t state ) const

protectedvirtual

Return a string that is additonally added to the state information in the dot stream.

Parameters

state

Returns

Reimplemented in storm::models::sparse::Pomdp< ValueType, RewardModelType >.

Definition at line 611 of file Model.cpp.

◆ addRewardModel()

template<typename ValueType , typename RewardModelType >

void storm::models::sparse::Model< ValueType, RewardModelType >::addRewardModel	(	std::string const &	rewardModelName,
		RewardModelType const &	rewModel
	)

Adds a reward model to the model.

Notice that this operation is only valid if the reward model matches the number of states and/or choices of the model. Moreover, it is required that no reward model with the same name exists in the model.

Definition at line 254 of file Model.cpp.

◆ getBackwardTransitions()

template<typename ValueType , typename RewardModelType >

storm::storage::SparseMatrix< ValueType > storm::models::sparse::Model< ValueType, RewardModelType >::getBackwardTransitions ( ) const

Retrieves the backward transition relation of the model, i.e.

a set of transitions between states that correspond to the reversed transition relation of this model.

Returns: A sparse matrix that represents the backward transitions of this model.

Definition at line 152 of file Model.cpp.

◆ getChoiceLabeling()

template<typename ValueType , typename RewardModelType >

storm::models::sparse::ChoiceLabeling const & storm::models::sparse::Model< ValueType, RewardModelType >::getChoiceLabeling ( ) const

Retrieves the labels for the choices of the model.

Note that calling this method is only valid if the model has a choice labeling.

Returns: The labels for the choices of the model.

Definition at line 334 of file Model.cpp.

◆ getChoiceOrigins()

template<typename ValueType , typename RewardModelType >

std::shared_ptr< storm::storage::sparse::ChoiceOrigins > const & storm::models::sparse::Model< ValueType, RewardModelType >::getChoiceOrigins ( ) const

Retrieves the origins of the choices of the model.

Note that calling this method is only valid if the model has choice origins.

Returns: The origins of the choices of the model.

Definition at line 374 of file Model.cpp.

◆ getInitialStates()

template<typename ValueType , typename RewardModelType >

storm::storage::BitVector const & storm::models::sparse::Model< ValueType, RewardModelType >::getInitialStates ( ) const

Retrieves the initial states of the model.

Returns: The initial states of the model represented by a bit vector.

Definition at line 177 of file Model.cpp.

◆ getLabelsOfState()

template<typename ValueType , typename RewardModelType >

std::set< std::string > storm::models::sparse::Model< ValueType, RewardModelType >::getLabelsOfState ( storm::storage::sparse::state_type state ) const

Retrieves the set of labels attached to the given state.

Parameters

state The state whose labels to retrieve.

Returns: The set of labels attach to the given state.

Definition at line 616 of file Model.cpp.

◆ getNumberOfChoices()

template<typename ValueType , typename RewardModelType >

uint_fast64_t storm::models::sparse::Model< ValueType, RewardModelType >::getNumberOfChoices ( ) const

overridevirtual

Returns the number of choices ine the model.

Returns: The number of choices in of the model.

Implements storm::models::ModelBase.

Definition at line 172 of file Model.cpp.

◆ getNumberOfRewardModels()

template<typename ValueType , typename RewardModelType >

uint_fast64_t storm::models::sparse::Model< ValueType, RewardModelType >::getNumberOfRewardModels ( ) const

Retrieves the number of reward models associated with this model.

Returns: The number of reward models associated with this model.

Definition at line 315 of file Model.cpp.

◆ getNumberOfStates()

template<typename ValueType , typename RewardModelType >

uint_fast64_t storm::models::sparse::Model< ValueType, RewardModelType >::getNumberOfStates ( ) const

overridevirtual

Returns the number of states of the model.

Returns: The number of states of the model.

Implements storm::models::ModelBase.

Definition at line 162 of file Model.cpp.

◆ getNumberOfTransitions()

template<typename ValueType , typename RewardModelType >

uint_fast64_t storm::models::sparse::Model< ValueType, RewardModelType >::getNumberOfTransitions ( ) const

overridevirtual

Returns the number of (non-zero) transitions of the model.

Returns: The number of (non-zero) transitions of the model.

Implements storm::models::ModelBase.

Definition at line 167 of file Model.cpp.

◆ getOptionalChoiceLabeling() [1/2]

template<typename ValueType , typename RewardModelType >

std::optional< storm::models::sparse::ChoiceLabeling > & storm::models::sparse::Model< ValueType, RewardModelType >::getOptionalChoiceLabeling ( )

Retrieves an optional value that contains the choice labeling if there is one.

Returns: The labels for the choices, if they're saved.

Definition at line 344 of file Model.cpp.

◆ getOptionalChoiceLabeling() [2/2]

template<typename ValueType , typename RewardModelType >

std::optional< storm::models::sparse::ChoiceLabeling > const & storm::models::sparse::Model< ValueType, RewardModelType >::getOptionalChoiceLabeling ( ) const

Retrieves an optional value that contains the choice labeling if there is one.

Returns: The labels for the choices, if they're saved.

Definition at line 339 of file Model.cpp.

◆ getOptionalChoiceOrigins() [1/2]

template<typename ValueType , typename RewardModelType >

std::optional< std::shared_ptr< storm::storage::sparse::ChoiceOrigins > > & storm::models::sparse::Model< ValueType, RewardModelType >::getOptionalChoiceOrigins ( )

Retrieves an optional value that contains the choice origins if there are some.

Returns: The choice origins, if they're saved.

Definition at line 384 of file Model.cpp.

◆ getOptionalChoiceOrigins() [2/2]

template<typename ValueType , typename RewardModelType >

std::optional< std::shared_ptr< storm::storage::sparse::ChoiceOrigins > > const & storm::models::sparse::Model< ValueType, RewardModelType >::getOptionalChoiceOrigins ( ) const

Retrieves an optional value that contains the choice origins if there are some.

Returns: The choice origins, if they're saved.

Definition at line 379 of file Model.cpp.

◆ getOptionalStateValuations() [1/2]

template<typename ValueType , typename RewardModelType >

std::optional< storm::storage::sparse::StateValuations > & storm::models::sparse::Model< ValueType, RewardModelType >::getOptionalStateValuations ( )

Retrieves an optional value that contains the state valuations if there are some.

Returns: The state valuations, if they're saved.

Definition at line 364 of file Model.cpp.

◆ getOptionalStateValuations() [2/2]

template<typename ValueType , typename RewardModelType >

std::optional< storm::storage::sparse::StateValuations > const & storm::models::sparse::Model< ValueType, RewardModelType >::getOptionalStateValuations ( ) const

Retrieves an optional value that contains the state valuations if there are some.

Returns: The state valuations, if they're saved.

Definition at line 359 of file Model.cpp.

◆ getRewardModel() [1/2]

template<typename ValueType , typename RewardModelType >

RewardModelType & storm::models::sparse::Model< ValueType, RewardModelType >::getRewardModel ( std::string const & rewardModelName )

Retrieves the reward model with the given name, if one exists.

Otherwise, an exception is thrown.

Returns: The reward model with the given name, if it exists.

Definition at line 236 of file Model.cpp.

◆ getRewardModel() [2/2]

template<typename ValueType , typename RewardModelType >

RewardModelType const & storm::models::sparse::Model< ValueType, RewardModelType >::getRewardModel ( std::string const & rewardModelName ) const

Retrieves the reward model with the given name, if one exists.

Otherwise, an exception is thrown.

Returns: The reward model with the given name, if it exists.

Definition at line 218 of file Model.cpp.

◆ getRewardModels() [1/2]

template<typename ValueType , typename RewardModelType >

std::unordered_map< std::string, RewardModelType > & storm::models::sparse::Model< ValueType, RewardModelType >::getRewardModels ( )

Retrieves the reward models.

Returns: A mapping from reward model names to the reward models.

Definition at line 694 of file Model.cpp.

◆ getRewardModels() [2/2]

template<typename ValueType , typename RewardModelType >

std::unordered_map< std::string, RewardModelType > const & storm::models::sparse::Model< ValueType, RewardModelType >::getRewardModels ( ) const

Retrieves the reward models.

Returns: A mapping from reward model names to the reward models.

Definition at line 699 of file Model.cpp.

◆ getRows()

template<typename ValueType , typename RewardModelType >

storm::storage::SparseMatrix< ValueType >::const_rows storm::models::sparse::Model< ValueType, RewardModelType >::getRows ( storm::storage::sparse::state_type state ) const

virtual

Returns an object representing the matrix rows associated with the given state.

Parameters

state The state for which to retrieve the rows.

Returns: An object representing the matrix rows associated with the given state.

Definition at line 157 of file Model.cpp.

◆ getStateLabeling() [1/2]

template<typename ValueType , typename RewardModelType >

storm::models::sparse::StateLabeling & storm::models::sparse::Model< ValueType, RewardModelType >::getStateLabeling ( )

Returns the state labeling associated with this model.

Returns: The state labeling associated with this model.

Definition at line 324 of file Model.cpp.

◆ getStateLabeling() [2/2]

template<typename ValueType , typename RewardModelType >

storm::models::sparse::StateLabeling const & storm::models::sparse::Model< ValueType, RewardModelType >::getStateLabeling ( ) const

Returns the state labeling associated with this model.

Returns: The state labeling associated with this model.

Definition at line 319 of file Model.cpp.

◆ getStates()

template<typename ValueType , typename RewardModelType >

storm::storage::BitVector const & storm::models::sparse::Model< ValueType, RewardModelType >::getStates ( std::string const & label ) const

Returns the sets of states labeled with the given label.

Parameters

label The label for which to get the labeled states.

Returns: The set of states labeled with the requested label in the form of a bit vector.

Definition at line 187 of file Model.cpp.

◆ getStateValuations()

template<typename ValueType , typename RewardModelType >

storm::storage::sparse::StateValuations const & storm::models::sparse::Model< ValueType, RewardModelType >::getStateValuations ( ) const

Retrieves the valuations of the states of the model.

Note that calling this method is only valid if the model has state valuations.

Returns: The valuations of the states of the model.

Definition at line 354 of file Model.cpp.

◆ getTransitionMatrix() [1/2]

template<typename ValueType , typename RewardModelType >

storm::storage::SparseMatrix< ValueType > & storm::models::sparse::Model< ValueType, RewardModelType >::getTransitionMatrix ( )

Retrieves the matrix representing the transitions of the model.

Returns: A matrix representing the transitions of the model.

Definition at line 202 of file Model.cpp.

◆ getTransitionMatrix() [2/2]

template<typename ValueType , typename RewardModelType >

storm::storage::SparseMatrix< ValueType > const & storm::models::sparse::Model< ValueType, RewardModelType >::getTransitionMatrix ( ) const

Retrieves the matrix representing the transitions of the model.

Returns: A matrix representing the transitions of the model.

Definition at line 197 of file Model.cpp.

◆ getUniqueRewardModel() [1/2]

template<typename ValueType , typename RewardModelType >

RewardModelType & storm::models::sparse::Model< ValueType, RewardModelType >::getUniqueRewardModel ( )

Retrieves the unique reward model, if there exists exactly one.

Otherwise, an exception is thrown.

Returns: The requested reward model.

Definition at line 309 of file Model.cpp.

◆ getUniqueRewardModel() [2/2]

template<typename ValueType , typename RewardModelType >

RewardModelType const & storm::models::sparse::Model< ValueType, RewardModelType >::getUniqueRewardModel ( ) const

Retrieves the unique reward model, if there exists exactly one.

Otherwise, an exception is thrown.

Returns: The requested reward model.

Definition at line 303 of file Model.cpp.

◆ getUniqueRewardModelName()

template<typename ValueType , typename RewardModelType >

std::string const & storm::models::sparse::Model< ValueType, RewardModelType >::getUniqueRewardModelName ( ) const

overridevirtual

Retrieves the name of the unique reward model, if there exists exactly one.

Otherwise, an exception is thrown.

Returns: The name of the unique reward model.

Implements storm::models::ModelBase.

Definition at line 292 of file Model.cpp.

◆ hasChoiceLabeling()

template<typename ValueType , typename RewardModelType >

bool storm::models::sparse::Model< ValueType, RewardModelType >::hasChoiceLabeling ( ) const

Retrieves whether this model has a labeling of the choices.

Returns: True iff this model has a labeling of the choices.

Definition at line 329 of file Model.cpp.

◆ hasChoiceOrigins()

template<typename ValueType , typename RewardModelType >

bool storm::models::sparse::Model< ValueType, RewardModelType >::hasChoiceOrigins ( ) const

Retrieves whether this model was build with choice origins.

Returns: True iff this model has choice origins.

Definition at line 369 of file Model.cpp.

◆ hash()

template<typename ValueType , typename RewardModelType >

std::size_t storm::models::sparse::Model< ValueType, RewardModelType >::hash ( ) const

virtual

Reimplemented in storm::models::sparse::Pomdp< ValueType, RewardModelType >.

Definition at line 395 of file Model.cpp.

◆ hasLabel()

template<typename ValueType , typename RewardModelType >

bool storm::models::sparse::Model< ValueType, RewardModelType >::hasLabel ( std::string const & label ) const

Retrieves whether the given label is a valid label in this model.

Parameters

label The label to be checked for validity.

Returns: True if the given label is valid in this model.

Definition at line 192 of file Model.cpp.

◆ hasParameters()

template<typename ValueType , typename RewardModelType >

bool storm::models::sparse::Model< ValueType, RewardModelType >::hasParameters ( ) const

overridevirtual

Checks whether the model has parameters.

Performance warning: the worst-case complexity is linear in the number of transitions.

Returns: True iff the model has parameters.

Reimplemented from storm::models::ModelBase.

Definition at line 659 of file Model.cpp.

◆ hasRewardModel() [1/2]

template<typename ValueType , typename RewardModelType >

bool storm::models::sparse::Model< ValueType, RewardModelType >::hasRewardModel ( ) const

Retrieves whether the model has at least one reward model.

Returns: True iff the model has a reward model.

Definition at line 298 of file Model.cpp.

◆ hasRewardModel() [2/2]

template<typename ValueType , typename RewardModelType >

bool storm::models::sparse::Model< ValueType, RewardModelType >::hasRewardModel ( std::string const & rewardModelName ) const

overridevirtual

Retrieves whether the model has a reward model with the given name.

Returns: True iff the model has a reward model with the given name.

Implements storm::models::ModelBase.

Definition at line 207 of file Model.cpp.

◆ hasStateValuations()

template<typename ValueType , typename RewardModelType >

bool storm::models::sparse::Model< ValueType, RewardModelType >::hasStateValuations ( ) const

Retrieves whether this model was build with state valuations.

Returns: True iff this model has state valuations.

Definition at line 349 of file Model.cpp.

◆ hasUncertainty()

template<typename ValueType , typename RewardModelType >

bool storm::models::sparse::Model< ValueType, RewardModelType >::hasUncertainty ( ) const

virtual

Checks whether the model actually is uncertain, i.e., whether there is a non-singleton transition relation.

Performance warning: the worst-case complexity is linear in the number of transitions. Notice that while parametric Markov models may be seen as uncertain, within storm,these models are not called uncertain.

Returns: True iff the model can be instantiated in more than one way.

Definition at line 674 of file Model.cpp.

◆ hasUniqueRewardModel()

template<typename ValueType , typename RewardModelType >

bool storm::models::sparse::Model< ValueType, RewardModelType >::hasUniqueRewardModel ( ) const

overridevirtual

Retrieves whether the model has a unique reward model.

Returns: True iff the model has a unique reward model.

Implements storm::models::ModelBase.

Definition at line 287 of file Model.cpp.

◆ isExact()

template<typename ValueType , typename RewardModelType >

bool storm::models::sparse::Model< ValueType, RewardModelType >::isExact ( ) const

overridevirtual

Checks whether the model is exact.

Returns: True iff the model is exact.

Reimplemented from storm::models::ModelBase.

Definition at line 689 of file Model.cpp.

◆ isSinkState()

template<typename ValueType , typename RewardModelType >

bool storm::models::sparse::Model< ValueType, RewardModelType >::isSinkState ( uint64_t sink ) const

Definition at line 631 of file Model.cpp.

◆ isSparseModel()

template<typename ValueType , typename RewardModelType >

bool storm::models::sparse::Model< ValueType, RewardModelType >::isSparseModel ( ) const

overridevirtual

Checks whether the model is a sparse model.

Returns: True iff the model is a sparse model.

Reimplemented from storm::models::ModelBase.

Definition at line 644 of file Model.cpp.

◆ operator=()

template<class CValueType , class CRewardModelType = StandardRewardModel<CValueType>>

Model & storm::models::sparse::Model< CValueType, CRewardModelType >::operator= ( Model< ValueType, RewardModelType > const & other )

default

◆ printModelInformationFooterToStream()

template<typename ValueType , typename RewardModelType >

void storm::models::sparse::Model< ValueType, RewardModelType >::printModelInformationFooterToStream ( std::ostream & out ) const

protected

Prints the information footer (reward models, labels and size in memory) of the model to the specified stream.

Parameters

out	The stream the information is to be printed to.

Definition at line 423 of file Model.cpp.

◆ printModelInformationHeaderToStream()

template<typename ValueType , typename RewardModelType >

void storm::models::sparse::Model< ValueType, RewardModelType >::printModelInformationHeaderToStream ( std::ostream & out ) const

protected

Prints the information header (number of states and transitions) of the model to the specified stream.

Parameters

out	The stream the information is to be printed to.

Definition at line 415 of file Model.cpp.

◆ printModelInformationToStream()

template<typename ValueType , typename RewardModelType >

void storm::models::sparse::Model< ValueType, RewardModelType >::printModelInformationToStream ( std::ostream & out ) const

overridevirtual

Prints information about the model to the specified stream.

Parameters

out	The stream the information is to be printed to.

Implements storm::models::ModelBase.

Definition at line 389 of file Model.cpp.

◆ printRewardModelsInformationToStream()

template<typename ValueType , typename RewardModelType >

void storm::models::sparse::Model< ValueType, RewardModelType >::printRewardModelsInformationToStream ( std::ostream & out ) const

protected

Prints information about the reward models to the specified stream.

Parameters

out	The stream the information is to be printed to.

Definition at line 437 of file Model.cpp.

◆ removeRewardModel()

template<typename ValueType , typename RewardModelType >

bool storm::models::sparse::Model< ValueType, RewardModelType >::removeRewardModel ( std::string const & rewardModelName )

Removes the reward model with the given name from the model.

Returns: true, iff such a reward model existed

Definition at line 264 of file Model.cpp.

◆ restrictRewardModels()

template<typename ValueType , typename RewardModelType >

void storm::models::sparse::Model< ValueType, RewardModelType >::restrictRewardModels ( std::set< std::string > const & keptRewardModels )

Removes all reward models whose name is not in the given set.

Definition at line 274 of file Model.cpp.

◆ rewardModel()

template<typename ValueType , typename RewardModelType >

RewardModelType & storm::models::sparse::Model< ValueType, RewardModelType >::rewardModel ( std::string const & rewardModelName )

protected

Definition at line 212 of file Model.cpp.

◆ setInitialStates()

template<typename ValueType , typename RewardModelType >

void storm::models::sparse::Model< ValueType, RewardModelType >::setInitialStates ( storm::storage::BitVector const & states )

Overwrites the initial states of the model.

Parameters

states the new initial states

Definition at line 182 of file Model.cpp.

◆ setTransitionMatrix() [1/2]

template<typename ValueType , typename RewardModelType >

void storm::models::sparse::Model< ValueType, RewardModelType >::setTransitionMatrix ( storm::storage::SparseMatrix< ValueType > && transitionMatrix )

protected

Sets the transition matrix of the model.

Parameters

transitionMatrix The new transition matrix of the model.

Definition at line 626 of file Model.cpp.

◆ setTransitionMatrix() [2/2]

template<typename ValueType , typename RewardModelType >

void storm::models::sparse::Model< ValueType, RewardModelType >::setTransitionMatrix ( storm::storage::SparseMatrix< ValueType > const & transitionMatrix )

protected

Sets the transition matrix of the model.

Parameters

transitionMatrix The new transition matrix of the model.

Definition at line 621 of file Model.cpp.

◆ supportsParameters()

template<typename ValueType , typename RewardModelType >

bool storm::models::sparse::Model< ValueType, RewardModelType >::supportsParameters ( ) const

overridevirtual

Checks whether the model supports parameters.

Returns: True iff the model supports parameters.

Reimplemented from storm::models::ModelBase.

Definition at line 649 of file Model.cpp.

◆ supportsUncertainty()

template<typename ValueType , typename RewardModelType >

bool storm::models::sparse::Model< ValueType, RewardModelType >::supportsUncertainty ( ) const

virtual

Does it support uncertainty (e.g., via interval-valued entries).

Notice that while parametric Markov models may be seen as uncertain, within storm,these models are not called uncertain.

Returns

Definition at line 654 of file Model.cpp.

◆ writeDotToStream()

template<class CValueType , class CRewardModelType = StandardRewardModel<CValueType>>

virtual void storm::models::sparse::Model< CValueType, CRewardModelType >::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

virtual

Exports the model to the dot-format and prints the result to the given stream.

Parameters

outStream	The stream to which the model is to be written.
maxWidthLabel	Maximal width of the labeling before a linebreak is inserted. Value 0 represents no linebreaks.
includeLabling	If set to true, the states will be exported with their labels.
subsystem	If not null, this represents the subsystem that is to be exported.
firstValue	If not null, the values in this vector are attached to the states.
secondValue	If not null, the values in this vector are attached to the states.
stateColoring	If not null, this is a mapping from states to color codes.
colors	A mapping of color codes to color names.
finalizeOutput	A flag that sets whether or not the dot stream is closed with a curly brace.

Returns: A string containing the exported model in dot-format.

◆ writeJsonToStream() [1/2]

void storm::models::sparse::Model< double, storm::models::sparse::StandardRewardModel< storm::Interval > >::writeJsonToStream ( std::ostream & ) const

Definition at line 606 of file Model.cpp.

◆ writeJsonToStream() [2/2]

template<typename ValueType , typename RewardModelType >

void storm::models::sparse::Model< ValueType, RewardModelType >::writeJsonToStream ( std::ostream & outStream ) const

virtual

Writes a JSON representation of the model to the given stream.

Definition at line 523 of file Model.cpp.

Member Data Documentation

◆ Representation

template<class CValueType , class CRewardModelType = StandardRewardModel<CValueType>>

const storm::models::ModelRepresentation storm::models::sparse::Model< CValueType, CRewardModelType >::Representation = ModelRepresentation::Sparse

static

Definition at line 37 of file Model.h.

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

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

Public Types

Public Member Functions

Static Public Attributes

Protected Member Functions

Detailed Description

Member Typedef Documentation

◆ RewardModelType

◆ ValueType

Constructor & Destructor Documentation

◆ Model() [1/3]

◆ Model() [2/3]

◆ Model() [3/3]

◆ ~Model()

Member Function Documentation

◆ additionalDotStateInfo()

◆ addRewardModel()

◆ getBackwardTransitions()

◆ getChoiceLabeling()

◆ getChoiceOrigins()

◆ getInitialStates()

◆ getLabelsOfState()

◆ getNumberOfChoices()

◆ getNumberOfRewardModels()

◆ getNumberOfStates()

◆ getNumberOfTransitions()

◆ getOptionalChoiceLabeling() [1/2]

◆ getOptionalChoiceLabeling() [2/2]

◆ getOptionalChoiceOrigins() [1/2]

◆ getOptionalChoiceOrigins() [2/2]

◆ getOptionalStateValuations() [1/2]

◆ getOptionalStateValuations() [2/2]

◆ getRewardModel() [1/2]

◆ getRewardModel() [2/2]

◆ getRewardModels() [1/2]

◆ getRewardModels() [2/2]

◆ getRows()

◆ getStateLabeling() [1/2]

◆ getStateLabeling() [2/2]

◆ getStates()

◆ getStateValuations()

◆ getTransitionMatrix() [1/2]

◆ getTransitionMatrix() [2/2]

◆ getUniqueRewardModel() [1/2]

◆ getUniqueRewardModel() [2/2]

◆ getUniqueRewardModelName()

◆ hasChoiceLabeling()

◆ hasChoiceOrigins()

◆ hash()

◆ hasLabel()

◆ hasParameters()

◆ hasRewardModel() [1/2]

◆ hasRewardModel() [2/2]

◆ hasStateValuations()

◆ hasUncertainty()

◆ hasUniqueRewardModel()

◆ isExact()

◆ isSinkState()

◆ isSparseModel()

◆ operator=()

◆ printModelInformationFooterToStream()

◆ printModelInformationHeaderToStream()

◆ printModelInformationToStream()

◆ printRewardModelsInformationToStream()

◆ removeRewardModel()

◆ restrictRewardModels()

◆ rewardModel()

◆ setInitialStates()

◆ setTransitionMatrix() [1/2]

◆ setTransitionMatrix() [2/2]

◆ supportsParameters()

◆ supportsUncertainty()

◆ writeDotToStream()

◆ writeJsonToStream() [1/2]

◆ writeJsonToStream() [2/2]

Member Data Documentation

◆ Representation