storm::models::sparse::NondeterministicModel< ValueType, RewardModelType > Class Template Reference

The base class of sparse nondeterministic models. More...

#include <NondeterministicModel.h>

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

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

Public Member Functions
	NondeterministicModel (ModelType modelType, storm::storage::sparse::ModelComponents< ValueType, RewardModelType > const &components)
	Constructs a model from the given data.
	NondeterministicModel (ModelType modelType, storm::storage::sparse::ModelComponents< ValueType, RewardModelType > &&components)
virtual	~NondeterministicModel ()=default
std::vector< uint_fast64_t > const &	getNondeterministicChoiceIndices () const
	Retrieves the vector indicating which matrix rows represent non-deterministic choices of a certain state.
uint_fast64_t	getNumberOfChoices (uint_fast64_t state) const
virtual void	reduceToStateBasedRewards () override
	Converts the transition rewards of all reward models to state-based rewards.
uint_fast64_t	getChoiceIndex (storm::storage::StateActionPair const &stateactPair) const
	For a state/action pair, get the choice index referring to the state-action pair.
std::shared_ptr< storm::models::sparse::Model< ValueType, RewardModelType > >	applyScheduler (storm::storage::Scheduler< ValueType > const &scheduler, bool dropUnreachableStates=true, bool preserveModelType=false) const
	Applies the given scheduler to this model.
virtual void	printModelInformationToStream (std::ostream &out) const override
	Prints information about the model to the specified stream.
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.
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

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::NondeterministicModel< ValueType, RewardModelType >

The base class of sparse nondeterministic models.

Definition at line 22 of file NondeterministicModel.h.

Constructor & Destructor Documentation

NondeterministicModel() [1/2]

template<typename ValueType , typename RewardModelType >

storm::models::sparse::NondeterministicModel< ValueType, RewardModelType >::NondeterministicModel	(	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 18 of file NondeterministicModel.cpp.

NondeterministicModel() [2/2]

template<typename ValueType , typename RewardModelType >

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

Definition at line 25 of file NondeterministicModel.cpp.

~NondeterministicModel()

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

virtual storm::models::sparse::NondeterministicModel< ValueType, RewardModelType >::~NondeterministicModel ( )

virtualdefault

Member Function Documentation

applyScheduler()

template<typename ValueType , typename RewardModelType >

std::shared_ptr< storm::models::sparse::Model< ValueType, RewardModelType > > storm::models::sparse::NondeterministicModel< ValueType, RewardModelType >::applyScheduler	(	storm::storage::Scheduler< ValueType > const &	scheduler,
		bool	dropUnreachableStates = true,
		bool	preserveModelType = false
	)		const

Applies the given scheduler to this model.

Parameters

scheduler	the considered scheduler.
dropUnreachableStates	if set, the resulting model only considers the states that are reachable from an initial state
preserveModelType	if set, the resulting model has the same type as the original (this) model, even when all nondeterminism is resolved and independent of the scheduler. Otherwise, the model type may differ.

Definition at line 50 of file NondeterministicModel.cpp.

getChoiceIndex()

template<typename ValueType , typename RewardModelType >

uint_least64_t storm::models::sparse::NondeterministicModel< ValueType, RewardModelType >::getChoiceIndex

(

storm::storage::StateActionPair const &

stateactPair

)

const

For a state/action pair, get the choice index referring to the state-action pair.

Definition at line 186 of file NondeterministicModel.cpp.

getNondeterministicChoiceIndices()

template<typename ValueType , typename RewardModelType >

std::vector< uint_fast64_t > const & storm::models::sparse::NondeterministicModel< ValueType, RewardModelType >::getNondeterministicChoiceIndices

(

)

const

Retrieves the vector indicating which matrix rows represent non-deterministic choices of a certain state.

Returns

The vector indicating which matrix rows represent non-deterministic choices of a certain state.

Definition at line 32 of file NondeterministicModel.cpp.

getNumberOfChoices()

template<typename ValueType , typename RewardModelType >

uint_fast64_t storm::models::sparse::NondeterministicModel< ValueType, RewardModelType >::getNumberOfChoices

(

uint_fast64_t

state

)

const

Parameters

state

State for which we want to know how many choices it has

Returns

The number of non-deterministic choices for the given state

Definition at line 37 of file NondeterministicModel.cpp.

printModelInformationToStream()

template<typename ValueType , typename RewardModelType >

void storm::models::sparse::NondeterministicModel< 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.

Reimplemented from storm::models::sparse::Model< CValueType, CRewardModelType >.

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

Definition at line 70 of file NondeterministicModel.cpp.

reduceToStateBasedRewards()

template<typename ValueType , typename RewardModelType >

void storm::models::sparse::NondeterministicModel< 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 43 of file NondeterministicModel.cpp.

writeDotToStream()

template<typename ValueType , typename RewardModelType >

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

overridevirtual

Definition at line 77 of file NondeterministicModel.cpp.

---

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

• src/storm/models/sparse/NondeterministicModel.h
• src/storm/models/sparse/NondeterministicModel.cpp