This class represents a discrete-time stochastic two-player game. More...

#include <MenuGame.h>

Inheritance diagram for storm::gbar::abstraction::MenuGame< Type, ValueType >:

[legend]

Collaboration diagram for storm::gbar::abstraction::MenuGame< Type, ValueType >:

[legend]

Public Types
typedef storm::models::symbolic::StochasticTwoPlayerGame< Type, ValueType >::RewardModelType	RewardModelType

Public Types inherited from storm::models::symbolic::StochasticTwoPlayerGame< Type, ValueType >
typedef NondeterministicModel< Type, ValueType >::RewardModelType	RewardModelType

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

Public Types inherited from storm::models::symbolic::Model< Type, ValueType >
typedef ValueType	ValueType

typedef StandardRewardModel< Type, ValueType >	RewardModelType

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

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

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

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

	MenuGame (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, storm::dd::Bdd< Type > bottomStates, 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::set< storm::expressions::Variable > const &player1Variables, std::set< storm::expressions::Variable > const &player2Variables, std::set< storm::expressions::Variable > const &allNondeterminismVariables, std::set< storm::expressions::Variable > const &probabilisticBranchingVariables, std::map< storm::expressions::Expression, storm::dd::Bdd< Type > > const &expressionToBddMap)
	Constructs a model from the given data.

virtual storm::dd::Bdd< Type >	getStates (std::string const &label) const override
	Returns the sets of states labeled with the given label.

virtual storm::dd::Bdd< Type >	getStates (storm::expressions::Expression const &expression) const override
	Returns the set of states satisfying the given expression (that must be of boolean type).

storm::dd::Bdd< Type >	getStates (storm::expressions::Expression const &expression, bool negated) const
	Returns the set of states satisfying the given expression (that must be of boolean type).

storm::dd::Bdd< Type >	getBottomStates () const
	Retrieves the bottom states of the model.

storm::dd::Add< Type, ValueType > const &	getExtendedTransitionMatrix () const
	Retrieves the transition matrix extended by variables that encode additional information for the probabilistic branching.

std::set< storm::expressions::Variable > const &	getProbabilisticBranchingVariables () const
	Retrieves the variables used to encode additional information for the probabilistic branching in the extended transition matrix.

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

Public Member Functions inherited from storm::models::symbolic::StochasticTwoPlayerGame< Type, ValueType >
	StochasticTwoPlayerGame (StochasticTwoPlayerGame< Type, ValueType > const &other)=default

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

	StochasticTwoPlayerGame (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::set< storm::expressions::Variable > const &player1Variables, std::set< storm::expressions::Variable > const &player2Variables, std::set< storm::expressions::Variable > const &allNondeterminismVariables, 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.

	StochasticTwoPlayerGame (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::set< storm::expressions::Variable > const &player1Variables, std::set< storm::expressions::Variable > const &player2Variables, std::set< storm::expressions::Variable > const &allNondeterminismVariables, 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.

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

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

std::set< storm::expressions::Variable > const &	getPlayer1Variables () const
	Retrieeves the set of meta variables used to encode the nondeterministic choices of player 1.

std::set< storm::expressions::Variable > const &	getPlayer2Variables () const
	Retrieeves the set of meta variables used to encode the nondeterministic choices of player 2.

storm::dd::Bdd< Type >	getIllegalPlayer1Mask () const
	Retrieves a BDD characterizing all illegal player 1 choice encodings in the model.

storm::dd::Bdd< Type >	getIllegalPlayer2Mask () const
	Retrieves a BDD characterizing all illegal player 2 choice encodings in the model.

std::shared_ptr< StochasticTwoPlayerGame< Type, NewValueType > >	toValueType () const

uint64_t	getNumberOfPlayer2States () const
	Retrieves the number of player 2 states in the game.

Public Member Functions inherited from storm::models::symbolic::NondeterministicModel< Type, ValueType >
	NondeterministicModel (NondeterministicModel< Type, ValueType > const &other)=default

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

	NondeterministicModel (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::set< storm::expressions::Variable > const &nondeterminismVariables, 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.

	NondeterministicModel (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::set< storm::expressions::Variable > const &nondeterminismVariables, 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.

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

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

virtual uint_fast64_t	getNumberOfChoices () const override
	Retrieves the number of nondeterministic choices in the model.

virtual std::set< storm::expressions::Variable > const &	getNondeterminismVariables () const override
	Retrieves the meta variables used to encode the nondeterminism in the model.

storm::dd::Bdd< Type > const &	getIllegalMask () const
	Retrieves a BDD characterizing all illegal nondeterminism encodings in the model.

storm::dd::Bdd< Type >	getIllegalSuccessorMask () const
	Retrieves a BDD characterizing the illegal successors for each choice.

virtual storm::dd::Bdd< Type >	getQualitativeTransitionMatrix (bool keepNondeterminism=true) const override
	Retrieves the matrix qualitatively (i.e.

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

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

Public Member Functions inherited from storm::models::symbolic::Model< Type, ValueType >
	Model (Model< Type, ValueType > const &other)=default

	Model (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.

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

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

virtual uint_fast64_t	getNumberOfStates () const override
	Returns the number of states of the model.

virtual uint_fast64_t	getNumberOfTransitions () const override
	Returns the number of (non-zero) transitions of the model.

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::expressions::Expression	getExpression (std::string const &label) const
	Returns the expression for the given label.

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.

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.

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.

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

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.

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

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

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

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

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

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

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

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

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

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

void	writeDotToFile (std::string const &filename) const

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

Additional Inherited Members
Static Public Attributes inherited from storm::models::symbolic::Model< Type, ValueType >
static const storm::dd::DdType	DdType

static const storm::models::ModelRepresentation	Representation

Protected Member Functions inherited from storm::models::symbolic::NondeterministicModel< Type, ValueType >
virtual void	printDdVariableInformationToStream (std::ostream &out) const override
	Prints information about the DD variables to the specified stream.

Protected Member Functions inherited from storm::models::symbolic::Model< Type, ValueType >
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.

std::shared_ptr< storm::adapters::AddExpressionAdapter< Type, ValueType > > const &	getRowExpressionAdapter () const
	Retrieves the expression adapter of this model.

Protected Attributes inherited from storm::models::symbolic::NondeterministicModel< Type, ValueType >
storm::dd::Bdd< Type >	illegalMask

Protected Attributes inherited from storm::models::symbolic::Model< Type, ValueType >
storm::dd::Add< Type, ValueType >	transitionMatrix

Detailed Description

template<storm::dd::DdType Type, typename ValueType>
class storm::gbar::abstraction::MenuGame< Type, ValueType >

This class represents a discrete-time stochastic two-player game.

Definition at line 16 of file MenuGame.h.

Member Typedef Documentation

◆ RewardModelType

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

typedef storm::models::symbolic::StochasticTwoPlayerGame<Type,ValueType>::RewardModelType storm::gbar::abstraction::MenuGame< Type, ValueType >::RewardModelType

Definition at line 18 of file MenuGame.h.

Constructor & Destructor Documentation

◆ MenuGame() [1/3]

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

storm::gbar::abstraction::MenuGame< Type, ValueType >::MenuGame ( MenuGame< Type, ValueType > const & other )

default

◆ MenuGame() [2/3]

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

storm::gbar::abstraction::MenuGame< Type, ValueType >::MenuGame ( MenuGame< Type, ValueType > && other )

default

◆ MenuGame() [3/3]

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

storm::gbar::abstraction::MenuGame< Type, ValueType >::MenuGame	(	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,
		storm::dd::Bdd< Type >	bottomStates,
		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::set< storm::expressions::Variable > const &	player1Variables,
		std::set< storm::expressions::Variable > const &	player2Variables,
		std::set< storm::expressions::Variable > const &	allNondeterminismVariables,
		std::set< storm::expressions::Variable > const &	probabilisticBranchingVariables,
		std::map< storm::expressions::Expression, storm::dd::Bdd< Type > > const &	expressionToBddMap
	)

Constructs a model from the given data.

Parameters

manager	The manager responsible for the decision diagrams.
reachableStates	The reachable states of the model.
initialStates	The initial states of the model.
deadlockStates	The deadlock states of the model.
transitionMatrix	The matrix representing the transitions in the model.
bottomStates	The bottom states of 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.
player1Variables	The meta variables used to encode the nondeterministic choices of player 1.
player2Variables	The meta variables used to encode the nondeterministic choices of player 2.
allNondeterminismVariables	The meta variables used to encode the nondeterminism in the model.
probabilisticBranchingVariables	The variables used to encode probabilistic branching.
expressionToBddMap	A mapping from expressions (used) in the abstraction to the BDDs encoding them.

Definition at line 19 of file MenuGame.cpp.

Member Function Documentation

◆ getBottomStates()

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

storm::dd::Bdd< Type > storm::gbar::abstraction::MenuGame< Type, ValueType >::getBottomStates ( ) const

Retrieves the bottom states of the model.

Returns: The bottom states of the model.

Definition at line 68 of file MenuGame.cpp.

◆ getExtendedTransitionMatrix()

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

storm::dd::Add< Type, ValueType > const & storm::gbar::abstraction::MenuGame< Type, ValueType >::getExtendedTransitionMatrix ( ) const

Retrieves the transition matrix extended by variables that encode additional information for the probabilistic branching.

@reutrn Th extended transition matrix.

Definition at line 73 of file MenuGame.cpp.

◆ getProbabilisticBranchingVariables()

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

std::set< storm::expressions::Variable > const & storm::gbar::abstraction::MenuGame< Type, ValueType >::getProbabilisticBranchingVariables ( ) const

Retrieves the variables used to encode additional information for the probabilistic branching in the extended transition matrix.

Returns: The probabilistic branching variables.

Definition at line 78 of file MenuGame.cpp.

◆ getStates() [1/3]

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

storm::dd::Bdd< Type > storm::gbar::abstraction::MenuGame< Type, ValueType >::getStates ( std::string const & label ) const

overridevirtual

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

Definition at line 40 of file MenuGame.cpp.

◆ getStates() [2/3]

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

storm::dd::Bdd< Type > storm::gbar::abstraction::MenuGame< Type, ValueType >::getStates ( storm::expressions::Expression const & expression ) const

overridevirtual

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

Note that for menu games, the given expression must be a predicate that was used to build the abstract game.

Parameters

expression The expression that needs to hold in the states.

Returns: The set of states satisfying the given expression.

Reimplemented from storm::models::symbolic::Model< Type, ValueType >.

Definition at line 45 of file MenuGame.cpp.

◆ getStates() [3/3]

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

storm::dd::Bdd< Type > storm::gbar::abstraction::MenuGame< Type, ValueType >::getStates	(	storm::expressions::Expression const &	expression,
		bool	negated
	)		const

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

Note that for menu games, the given expression must be a predicate that was used to build the abstract game.

Parameters

expression	The expression that needs to hold in the states.
negated	If set to true, the result is the set of states not satisfying the expression.

Returns: The set of states labeled satisfying the given expression.

Definition at line 50 of file MenuGame.cpp.

◆ hasLabel()

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

bool storm::gbar::abstraction::MenuGame< Type, ValueType >::hasLabel ( std::string const & label ) const

overridevirtual

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

Definition at line 83 of file MenuGame.cpp.

◆ operator=() [1/2]

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

MenuGame & storm::gbar::abstraction::MenuGame< Type, ValueType >::operator= ( MenuGame< Type, ValueType > && other )

default

◆ operator=() [2/2]

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

MenuGame & storm::gbar::abstraction::MenuGame< Type, ValueType >::operator= ( MenuGame< Type, ValueType > const & other )

default

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

src/storm-gamebased-ar/abstraction/MenuGame.h
src/storm-gamebased-ar/abstraction/MenuGame.cpp

Public Types

Public Member Functions

Additional Inherited Members

Detailed Description

Member Typedef Documentation

◆ RewardModelType

Constructor & Destructor Documentation

◆ MenuGame() [1/3]

◆ MenuGame() [2/3]

◆ MenuGame() [3/3]

Member Function Documentation

◆ getBottomStates()

◆ getExtendedTransitionMatrix()

◆ getProbabilisticBranchingVariables()

◆ getStates() [1/3]

◆ getStates() [2/3]

◆ getStates() [3/3]

◆ hasLabel()

◆ operator=() [1/2]

◆ operator=() [2/2]