Base class for all symbolic models. More...

#include <Model.h>

Inheritance diagram for storm::models::symbolic::Model< Type, CValueType >:

[legend]

Collaboration diagram for storm::models::symbolic::Model< Type, CValueType >:

[legend]

Public Types
typedef CValueType	ValueType

typedef StandardRewardModel< Type, ValueType >	RewardModelType

Public Member Functions
	Model (Model< Type, ValueType > const &other)=default

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

	Model (Model< Type, ValueType > &&other)=default

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

	Model (storm::models::ModelType const &modelType, 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.

	Model (storm::models::ModelType const &modelType, 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.

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 storm::dd::Bdd< Type >	getStates (storm::expressions::Expression const &expression) const
	Returns the set of states labeled satisfying the given expression (that must be of boolean type).

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.

storm::dd::Add< Type, ValueType > &	getTransitionMatrix ()
	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.

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.

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

std::unordered_map< std::string, RewardModelType > &	getRewardModels ()

std::unordered_map< std::string, RewardModelType > const &	getRewardModels () const

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

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 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

void	addParameters (std::set< storm::RationalFunctionVariable > const &parameters)

std::set< storm::RationalFunctionVariable > const &	getParameters () const

template<typename NewValueType >
std::enable_if<!std::is_same< ValueType, NewValueType >::value, std::shared_ptr< Model< Type, NewValueType > > >::type	toValueType () const

template<typename NewValueType >
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

void	addParameters (std::set< storm::RationalFunctionVariable > const &parameters)

std::set< storm::RationalFunctionVariable > const &	getParameters () const

Public Member Functions inherited from storm::models::Model< ValueType >
	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.

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	isExact () const
	Checks whether the model is exact.

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::dd::DdType	DdType = Type

static const storm::models::ModelRepresentation	Representation = GetModelRepresentation<DdType>::representation

Protected Member Functions
void	setTransitionMatrix (storm::dd::Add< Type, ValueType > const &transitionMatrix)
	Sets the transition matrix of the model.

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
storm::dd::Add< Type, ValueType >	transitionMatrix

Detailed Description

template<storm::dd::DdType Type, typename CValueType = double>
class storm::models::symbolic::Model< Type, CValueType >

Base class for all symbolic models.

Definition at line 46 of file Model.h.

Member Typedef Documentation

◆ RewardModelType

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

typedef StandardRewardModel<Type, ValueType> storm::models::symbolic::Model< Type, CValueType >::RewardModelType

Definition at line 51 of file Model.h.

◆ ValueType

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

typedef CValueType storm::models::symbolic::Model< Type, CValueType >::ValueType

Definition at line 48 of file Model.h.

Constructor & Destructor Documentation

◆ Model() [1/4]

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

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

default

◆ Model() [2/4]

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

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

default

◆ Model() [3/4]

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

storm::models::symbolic::Model< Type, ValueType >::Model	(	storm::models::ModelType const &	modelType,
		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

modelType	The type of the model.
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 30 of file Model.cpp.

◆ Model() [4/4]

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

storm::models::symbolic::Model< Type, ValueType >::Model	(	storm::models::ModelType const &	modelType,
		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

modelType	The type of the model.
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 53 of file Model.cpp.

Member Function Documentation

◆ addParameters() [1/2]

void storm::models::symbolic::Model< storm::dd::DdType::Sylvan, storm::RationalFunction >::addParameters ( std::set< storm::RationalFunctionVariable > const & parameters )

Definition at line 432 of file Model.cpp.

◆ addParameters() [2/2]

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

void storm::models::symbolic::Model< Type, ValueType >::addParameters ( std::set< storm::RationalFunctionVariable > const & parameters )

Definition at line 422 of file Model.cpp.

◆ getColumnAndNondeterminismVariables()

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

std::set< storm::expressions::Variable > storm::models::symbolic::Model< Type, ValueType >::getColumnAndNondeterminismVariables ( ) const

Retrieves all meta variables used to encode columns and nondetermism.

Returns: All meta variables used to encode columns and nondetermism.

Definition at line 210 of file Model.cpp.

◆ getColumnVariables()

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

std::set< storm::expressions::Variable > const & storm::models::symbolic::Model< Type, ValueType >::getColumnVariables ( ) const

Retrieves the meta variables used to encode the columns of the transition matrix and the vector indices.

Returns: The meta variables used to encode the columns of the transition matrix and the vector indices.

Definition at line 197 of file Model.cpp.

◆ getDeadlockStates()

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

storm::dd::Bdd< Type > const & storm::models::symbolic::Model< Type, ValueType >::getDeadlockStates ( ) const

Definition at line 112 of file Model.cpp.

◆ getExpression()

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

storm::expressions::Expression storm::models::symbolic::Model< Type, ValueType >::getExpression ( std::string const & label ) const

virtual

Returns the expression for the given label.

Parameters

label The label for which to get the expression.

Returns: The expression characterizing the requested label.

Definition at line 132 of file Model.cpp.

◆ getInitialStates()

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

storm::dd::Bdd< Type > const & storm::models::symbolic::Model< Type, ValueType >::getInitialStates ( ) const

Retrieves the initial states of the model.

Returns: The initial states of the model.

Definition at line 107 of file Model.cpp.

◆ getLabels()

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

std::vector< std::string > storm::models::symbolic::Model< Type, ValueType >::getLabels ( ) const

Definition at line 319 of file Model.cpp.

◆ getLabelToBddMap()

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

std::map< std::string, storm::dd::Bdd< Type > > const & storm::models::symbolic::Model< Type, ValueType >::getLabelToBddMap ( ) const

protected

Retrieves the mapping of labels to their defining expressions.

Returns: The mapping of labels to their defining expressions.

Definition at line 238 of file Model.cpp.

◆ getLabelToExpressionMap()

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

std::map< std::string, storm::expressions::Expression > const & storm::models::symbolic::Model< Type, ValueType >::getLabelToExpressionMap ( ) const

protected

Retrieves the mapping of labels to their defining expressions.

Returns: The mapping of labels to their defining expressions.

Definition at line 233 of file Model.cpp.

◆ getManager()

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

storm::dd::DdManager< Type > & storm::models::symbolic::Model< Type, ValueType >::getManager ( ) const

Retrieves the manager responsible for the DDs that represent this model.

Returns: The manager responsible for the DDs that represent this model.

Definition at line 92 of file Model.cpp.

◆ getManagerAsSharedPointer()

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

std::shared_ptr< storm::dd::DdManager< Type > > const & storm::models::symbolic::Model< Type, ValueType >::getManagerAsSharedPointer ( ) const

Retrieves the manager responsible for the DDs that represent this model.

Returns: The manager responsible for the DDs that represent this model.

Definition at line 97 of file Model.cpp.

◆ getNondeterminismVariables()

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

std::set< storm::expressions::Variable > const & storm::models::symbolic::Model< Type, ValueType >::getNondeterminismVariables ( ) const

virtual

Retrieves all meta variables used to encode the nondeterminism.

Returns: All meta variables used to encode the nondeterminism.

Reimplemented in storm::models::symbolic::NondeterministicModel< Type, ValueType >, storm::models::symbolic::NondeterministicModel< DdType, ValueType >, storm::models::symbolic::NondeterministicModel< Type, double >, and storm::models::symbolic::NondeterministicModel< Type, ValueType >.

Definition at line 218 of file Model.cpp.

◆ getNumberOfChoices()

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

uint_fast64_t storm::models::symbolic::Model< Type, ValueType >::getNumberOfChoices ( ) const

overridevirtual

Returns the number of choices ine the model.

Returns: The number of choices in of the model.

Implements storm::models::ModelBase.

Reimplemented in storm::models::symbolic::NondeterministicModel< Type, ValueType >, storm::models::symbolic::NondeterministicModel< DdType, ValueType >, storm::models::symbolic::NondeterministicModel< Type, double >, and storm::models::symbolic::NondeterministicModel< Type, ValueType >.

Definition at line 87 of file Model.cpp.

◆ getNumberOfRewardModels()

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

uint_fast64_t storm::models::symbolic::Model< Type, CValueType >::getNumberOfRewardModels ( ) const

Retrieves the number of reward models associated with this model.

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

◆ getNumberOfStates()

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

uint_fast64_t storm::models::symbolic::Model< Type, ValueType >::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 77 of file Model.cpp.

◆ getNumberOfTransitions()

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

uint_fast64_t storm::models::symbolic::Model< Type, ValueType >::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 82 of file Model.cpp.

◆ getParameters() [1/2]

std::set< storm::RationalFunctionVariable > const & storm::models::symbolic::Model< storm::dd::DdType::Sylvan, storm::RationalFunction >::getParameters ( ) const

Definition at line 437 of file Model.cpp.

◆ getParameters() [2/2]

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

std::set< storm::RationalFunctionVariable > const & storm::models::symbolic::Model< Type, ValueType >::getParameters ( ) const

Definition at line 427 of file Model.cpp.

◆ getQualitativeTransitionMatrix()

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

storm::dd::Bdd< Type > storm::models::symbolic::Model< Type, ValueType >::getQualitativeTransitionMatrix ( bool keepNondeterminism = true ) const

virtual

Retrieves the matrix qualitatively (i.e.

without probabilities) representing the transitions of the model.

Parameters

keepNondeterminism If false, the matrix will abstract from the nondeterminism variables.

Returns: A matrix representing the qualitative transitions of the model.

Reimplemented in storm::models::symbolic::NondeterministicModel< Type, ValueType >, storm::models::symbolic::NondeterministicModel< DdType, ValueType >, storm::models::symbolic::NondeterministicModel< Type, double >, and storm::models::symbolic::NondeterministicModel< Type, ValueType >.

Definition at line 187 of file Model.cpp.

◆ getReachableStates()

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

storm::dd::Bdd< Type > const & storm::models::symbolic::Model< Type, ValueType >::getReachableStates ( ) const

Retrieves the reachable states of the model.

Returns: The reachble states of the model.

Definition at line 102 of file Model.cpp.

◆ getRewardModel()

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

Model< Type, ValueType >::RewardModelType const & storm::models::symbolic::Model< Type, ValueType >::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 254 of file Model.cpp.

◆ getRewardModels() [1/2]

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

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

Definition at line 303 of file Model.cpp.

◆ getRewardModels() [2/2]

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

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

Definition at line 308 of file Model.cpp.

◆ getRowAndNondeterminismVariables()

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

std::set< storm::expressions::Variable > storm::models::symbolic::Model< Type, ValueType >::getRowAndNondeterminismVariables ( ) const

Retrieves all meta variables used to encode rows and nondetermism.

Returns: All meta variables used to encode rows and nondetermism.

Definition at line 202 of file Model.cpp.

◆ getRowColumnIdentity()

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

storm::dd::Add< Type, ValueType > storm::models::symbolic::Model< Type, ValueType >::getRowColumnIdentity ( ) const

Retrieves an ADD that represents the diagonal of the transition matrix.

Returns: An ADD that represents the diagonal of the transition matrix.

Definition at line 243 of file Model.cpp.

◆ getRowColumnMetaVariablePairs()

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

std::vector< std::pair< storm::expressions::Variable, storm::expressions::Variable > > const & storm::models::symbolic::Model< Type, ValueType >::getRowColumnMetaVariablePairs ( ) const

Retrieves the pairs of row and column meta variables.

Returns: The pairs of row and column meta variables.

Definition at line 223 of file Model.cpp.

◆ getRowExpressionAdapter()

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

std::shared_ptr< storm::adapters::AddExpressionAdapter< Type, ValueType > > const & storm::models::symbolic::Model< Type, ValueType >::getRowExpressionAdapter ( ) const

protected

Retrieves the expression adapter of this model.

Returns: The expression adapter.

Definition at line 383 of file Model.cpp.

◆ getRowVariables()

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

std::set< storm::expressions::Variable > const & storm::models::symbolic::Model< Type, ValueType >::getRowVariables ( ) const

Retrieves the meta variables used to encode the rows of the transition matrix and the vector indices.

Returns: The meta variables used to encode the rows of the transition matrix and the vector indices.

Definition at line 192 of file Model.cpp.

◆ getStates() [1/2]

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

storm::dd::Bdd< Type > storm::models::symbolic::Model< Type, ValueType >::getStates ( std::string const & label ) const

virtual

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.

Reimplemented in storm::gbar::abstraction::MenuGame< Type, ValueType >.

Definition at line 117 of file Model.cpp.

◆ getStates() [2/2]

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

storm::dd::Bdd< Type > storm::models::symbolic::Model< Type, ValueType >::getStates ( storm::expressions::Expression const & expression ) const

virtual

Returns the set of states labeled satisfying the given expression (that must be of boolean type).

Parameters

expression The expression that needs to hold in the states.

Returns: The set of states satisfying the given expression.

Reimplemented in storm::gbar::abstraction::MenuGame< Type, ValueType >.

Definition at line 140 of file Model.cpp.

◆ getTransitionMatrix() [1/2]

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

storm::dd::Add< Type, ValueType > & storm::models::symbolic::Model< Type, ValueType >::getTransitionMatrix ( )

Retrieves the matrix representing the transitions of the model.

Returns: A matrix representing the transitions of the model.

Definition at line 182 of file Model.cpp.

◆ getTransitionMatrix() [2/2]

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

storm::dd::Add< Type, ValueType > const & storm::models::symbolic::Model< Type, ValueType >::getTransitionMatrix ( ) const

Retrieves the matrix representing the transitions of the model.

Returns: A matrix representing the transitions of the model.

Definition at line 177 of file Model.cpp.

◆ getUniqueRewardModel() [1/2]

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

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

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

Otherwise, an exception is thrown.

Returns: The requested reward model.

Definition at line 286 of file Model.cpp.

◆ getUniqueRewardModel() [2/2]

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

Model< Type, ValueType >::RewardModelType const & storm::models::symbolic::Model< Type, ValueType >::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 272 of file Model.cpp.

◆ getUniqueRewardModelName()

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

std::string const & storm::models::symbolic::Model< Type, ValueType >::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 279 of file Model.cpp.

◆ hasLabel()

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

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

virtual

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.

Reimplemented in storm::gbar::abstraction::MenuGame< Type, ValueType >.

Definition at line 162 of file Model.cpp.

◆ hasParameters()

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

bool storm::models::symbolic::Model< Type, ValueType >::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 407 of file Model.cpp.

◆ hasRewardModel() [1/2]

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

bool storm::models::symbolic::Model< Type, ValueType >::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<storm::dd::DdType Type, typename ValueType >

bool storm::models::symbolic::Model< Type, ValueType >::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 249 of file Model.cpp.

◆ hasUniqueRewardModel()

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

bool storm::models::symbolic::Model< Type, ValueType >::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 293 of file Model.cpp.

◆ isSymbolicModel()

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

bool storm::models::symbolic::Model< Type, ValueType >::isSymbolicModel ( ) const

overridevirtual

Checks whether the model is a symbolic model.

Returns: True iff the model is a symbolic model.

Reimplemented from storm::models::ModelBase.

Definition at line 388 of file Model.cpp.

◆ operator=() [1/2]

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

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

default

◆ operator=() [2/2]

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

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

default

◆ printDdVariableInformationToStream()

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

void storm::models::symbolic::Model< Type, ValueType >::printDdVariableInformationToStream ( std::ostream & out ) const

protectedvirtual

Prints information about the DD variables to the specified stream.

Parameters

out	The stream the information is to be printed to.

Reimplemented in storm::models::symbolic::NondeterministicModel< Type, ValueType >, storm::models::symbolic::NondeterministicModel< DdType, ValueType >, storm::models::symbolic::NondeterministicModel< Type, double >, and storm::models::symbolic::NondeterministicModel< Type, ValueType >.

Definition at line 368 of file Model.cpp.

◆ printModelInformationFooterToStream()

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

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

protected

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

Parameters

out	The stream the information is to be printed to.

Definition at line 336 of file Model.cpp.

◆ printModelInformationHeaderToStream()

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

void storm::models::symbolic::Model< Type, ValueType >::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 328 of file Model.cpp.

◆ printModelInformationToStream()

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

void storm::models::symbolic::Model< Type, ValueType >::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.

Reimplemented in storm::models::symbolic::NondeterministicModel< Type, ValueType >, storm::models::symbolic::NondeterministicModel< DdType, ValueType >, storm::models::symbolic::NondeterministicModel< Type, double >, and storm::models::symbolic::NondeterministicModel< Type, ValueType >.

Definition at line 313 of file Model.cpp.

◆ printRewardModelsInformationToStream()

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

void storm::models::symbolic::Model< Type, ValueType >::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 350 of file Model.cpp.

◆ setTransitionMatrix()

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

void storm::models::symbolic::Model< Type, ValueType >::setTransitionMatrix ( storm::dd::Add< Type, ValueType > const & transitionMatrix )

protected

Sets the transition matrix of the model.

Parameters

transitionMatrix The new transition matrix of the model.

Definition at line 228 of file Model.cpp.

◆ supportsParameters()

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

bool storm::models::symbolic::Model< Type, ValueType >::supportsParameters ( ) const

overridevirtual

Checks whether the model supports parameters.

Returns: True iff the model supports parameters.

Reimplemented from storm::models::ModelBase.

Definition at line 393 of file Model.cpp.

◆ toValueType() [1/2]

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

template<typename NewValueType >

std::enable_if< std::is_same< ValueType, NewValueType >::value, std::shared_ptr< Model< Type, NewValueType > > >::type storm::models::symbolic::Model< Type, ValueType >::toValueType ( ) const

Definition at line 443 of file Model.cpp.

◆ toValueType() [2/2]

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

template<typename NewValueType >

template std::enable_if<!std::is_same< storm::RationalNumber, double >::value, std::shared_ptr< Model< storm::dd::DdType::Sylvan, double > > >::type storm::models::symbolic::Model< Type, CValueType >::toValueType< double > ( ) const

◆ writeDotToFile()

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

void storm::models::symbolic::Model< Type, ValueType >::writeDotToFile ( std::string const & filename ) const

Definition at line 398 of file Model.cpp.

Member Data Documentation

◆ DdType

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

const storm::dd::DdType storm::models::symbolic::Model< Type, CValueType >::DdType = Type

static

Definition at line 50 of file Model.h.

◆ Representation

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

const storm::models::ModelRepresentation storm::models::symbolic::Model< Type, CValueType >::Representation = GetModelRepresentation<DdType>::representation

static

Definition at line 53 of file Model.h.

◆ transitionMatrix

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

storm::dd::Add<Type, ValueType> storm::models::symbolic::Model< Type, CValueType >::transitionMatrix

protected

Definition at line 409 of file Model.h.

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

src/storm-gamebased-ar/modelchecker/abstraction/AbstractAbstractionRefinementModelChecker.h
src/storm/models/symbolic/Model.h
src/storm/models/symbolic/Model.cpp

Public Types

Public Member Functions

Static Public Attributes

Protected Member Functions

Protected Attributes

Detailed Description

Member Typedef Documentation

◆ RewardModelType

◆ ValueType

Constructor & Destructor Documentation

◆ Model() [1/4]

◆ Model() [2/4]

◆ Model() [3/4]

◆ Model() [4/4]

Member Function Documentation

◆ addParameters() [1/2]

◆ addParameters() [2/2]

◆ getColumnAndNondeterminismVariables()

◆ getColumnVariables()

◆ getDeadlockStates()

◆ getExpression()

◆ getInitialStates()

◆ getLabels()

◆ getLabelToBddMap()

◆ getLabelToExpressionMap()

◆ getManager()

◆ getManagerAsSharedPointer()

◆ getNondeterminismVariables()

◆ getNumberOfChoices()

◆ getNumberOfRewardModels()

◆ getNumberOfStates()

◆ getNumberOfTransitions()

◆ getParameters() [1/2]

◆ getParameters() [2/2]

◆ getQualitativeTransitionMatrix()

◆ getReachableStates()

◆ getRewardModel()

◆ getRewardModels() [1/2]

◆ getRewardModels() [2/2]

◆ getRowAndNondeterminismVariables()

◆ getRowColumnIdentity()

◆ getRowColumnMetaVariablePairs()

◆ getRowExpressionAdapter()

◆ getRowVariables()

◆ getStates() [1/2]

◆ getStates() [2/2]

◆ getTransitionMatrix() [1/2]

◆ getTransitionMatrix() [2/2]

◆ getUniqueRewardModel() [1/2]

◆ getUniqueRewardModel() [2/2]

◆ getUniqueRewardModelName()

◆ hasLabel()

◆ hasParameters()

◆ hasRewardModel() [1/2]

◆ hasRewardModel() [2/2]

◆ hasUniqueRewardModel()

◆ isSymbolicModel()

◆ operator=() [1/2]

◆ operator=() [2/2]

◆ printDdVariableInformationToStream()

◆ printModelInformationFooterToStream()

◆ printModelInformationHeaderToStream()

◆ printModelInformationToStream()

◆ printRewardModelsInformationToStream()

◆ setTransitionMatrix()

◆ supportsParameters()

◆ toValueType() [1/2]

◆ toValueType() [2/2]

◆ writeDotToFile()

Member Data Documentation

◆ DdType

◆ Representation

◆ transitionMatrix