#include <JaniMenuGameAbstractor.h>

Inheritance diagram for storm::gbar::abstraction::jani::JaniMenuGameAbstractor< DdType, ValueType >:

Collaboration diagram for storm::gbar::abstraction::jani::JaniMenuGameAbstractor< DdType, ValueType >:

Public Member Functions
	JaniMenuGameAbstractor (storm::jani::Model const &model, std::shared_ptr< storm::utility::solver::SmtSolverFactory > const &smtSolverFactory, MenuGameAbstractorOptions const &options=MenuGameAbstractorOptions())
	Constructs an abstractor for the given model.

	JaniMenuGameAbstractor (JaniMenuGameAbstractor const &)=default

JaniMenuGameAbstractor &	operator= (JaniMenuGameAbstractor const &)=default

	JaniMenuGameAbstractor (JaniMenuGameAbstractor &&)=default

JaniMenuGameAbstractor &	operator= (JaniMenuGameAbstractor &&)=default

storm::dd::DdManager< DdType > const &	getDdManager () const override

MenuGame< DdType, ValueType >	abstract () override
	Uses the current set of predicates to derive the abstract menu game in the form of an ADD.

AbstractionInformation< DdType > const &	getAbstractionInformation () const override
	Retrieves information about the abstraction.

storm::expressions::Expression const &	getGuard (uint64_t player1Choice) const override
	Retrieves the guard predicate of the given player 1 choice.

virtual uint64_t	getNumberOfUpdates (uint64_t player1Choice) const override
	Retrieves the number of updates of the specified player 1 choice.

std::map< storm::expressions::Variable, storm::expressions::Expression >	getVariableUpdates (uint64_t player1Choice, uint64_t auxiliaryChoice) const override
	Retrieves a mapping from variables to expressions that define their updates wrt.

virtual std::set< storm::expressions::Variable > const &	getAssignedVariables (uint64_t player1Choice) const override
	Retrieves the variables assigned by the given player 1 choice.

std::pair< uint64_t, uint64_t >	getPlayer1ChoiceRange () const override
	Retrieves the range of player 1 choices.

storm::expressions::Expression	getInitialExpression () const override
	Retrieves the expression that characterizes the initial states.

storm::dd::Bdd< DdType >	getStates (storm::expressions::Expression const &expression) override
	Retrieves a BDD that characterizes the states corresponding to the given expression.

virtual void	refine (RefinementCommand const &command) override
	Performs the given refinement command.

virtual void	exportToDot (std::string const &filename, storm::dd::Bdd< DdType > const &highlightStates, storm::dd::Bdd< DdType > const &filter) const override
	Exports the current state of the abstraction in the dot format to the given file.

virtual uint64_t	getNumberOfPredicates () const override
	Retrieves the number of predicates currently in use.

virtual void	addTerminalStates (storm::expressions::Expression const &expression) override
	Adds the expression to the ones characterizing terminal states, i.e.

virtual void	notifyGuardsArePredicates () override
	Notifies the abstractor that the guards are predicates, which may be used to improve the bottom state computation.

Public Member Functions inherited from storm::gbar::abstraction::MenuGameAbstractor< DdType, ValueType >
	MenuGameAbstractor ()

virtual	~MenuGameAbstractor ()=default

std::vector< std::map< storm::expressions::Variable, storm::expressions::Expression > >	getVariableUpdates (uint64_t player1Choice) const

void	setTargetStates (storm::expressions::Expression const &targetStateExpression)
	Sets the expression characterizing the target states.

storm::expressions::Expression const &	getTargetStateExpression () const

bool	hasTargetStateExpression () const

Additional Inherited Members
Protected Member Functions inherited from storm::gbar::abstraction::MenuGameAbstractor< DdType, ValueType >
bool	isRestrictToRelevantStatesSet () const

void	exportToDot (storm::gbar::abstraction::MenuGame< DdType, ValueType > const &currentGame, std::string const &filename, storm::dd::Bdd< DdType > const &highlightStatesBdd, storm::dd::Bdd< DdType > const &filter) const

Detailed Description

template<storm::dd::DdType DdType, typename ValueType>
class storm::gbar::abstraction::jani::JaniMenuGameAbstractor< DdType, ValueType >

Definition at line 43 of file JaniMenuGameAbstractor.h.

Constructor & Destructor Documentation

◆ JaniMenuGameAbstractor() [1/3]

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

storm::gbar::abstraction::jani::JaniMenuGameAbstractor< DdType, ValueType >::JaniMenuGameAbstractor	(	storm::jani::Model const &	model,
		std::shared_ptr< storm::utility::solver::SmtSolverFactory > const &	smtSolverFactory,
		MenuGameAbstractorOptions const &	options = `MenuGameAbstractorOptions()`
	)

Constructs an abstractor for the given model.

Parameters

model	The concrete model for which to build the abstraction.
smtSolverFactory	A factory that is to be used for creating new SMT solvers.

Definition at line 38 of file JaniMenuGameAbstractor.cpp.

◆ JaniMenuGameAbstractor() [2/3]

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

storm::gbar::abstraction::jani::JaniMenuGameAbstractor< DdType, ValueType >::JaniMenuGameAbstractor ( JaniMenuGameAbstractor< DdType, ValueType > const & )

default

◆ JaniMenuGameAbstractor() [3/3]

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

storm::gbar::abstraction::jani::JaniMenuGameAbstractor< DdType, ValueType >::JaniMenuGameAbstractor ( JaniMenuGameAbstractor< DdType, ValueType > && )

default

Member Function Documentation

◆ abstract()

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

MenuGame< DdType, ValueType > storm::gbar::abstraction::jani::JaniMenuGameAbstractor< DdType, ValueType >::abstract ( )

overridevirtual

Uses the current set of predicates to derive the abstract menu game in the form of an ADD.

Returns: The abstract stochastic two player game.

Implements storm::gbar::abstraction::MenuGameAbstractor< DdType, ValueType >.

Definition at line 129 of file JaniMenuGameAbstractor.cpp.

◆ addTerminalStates()

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

void storm::gbar::abstraction::jani::JaniMenuGameAbstractor< DdType, ValueType >::addTerminalStates ( storm::expressions::Expression const & expression )

overridevirtual

Adds the expression to the ones characterizing terminal states, i.e.

states whose transitions are not explored. For this to work, appropriate predicates must have been used to refine the abstraction, otherwise this will fail.

Implements storm::gbar::abstraction::MenuGameAbstractor< DdType, ValueType >.

Definition at line 324 of file JaniMenuGameAbstractor.cpp.

◆ exportToDot()

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

void storm::gbar::abstraction::jani::JaniMenuGameAbstractor< DdType, ValueType >::exportToDot	(	std::string const &	filename,
		storm::dd::Bdd< DdType > const &	highlightStates,
		storm::dd::Bdd< DdType > const &	filter
	)		const

overridevirtual

Exports the current state of the abstraction in the dot format to the given file.

Parameters

filename	The name of the file to which to write the dot output.
highlightStates	A BDD characterizing states that will be highlighted.
filter	A filter that is applied to select which part of the game to export.

Implements storm::gbar::abstraction::MenuGameAbstractor< DdType, ValueType >.

Definition at line 313 of file JaniMenuGameAbstractor.cpp.

◆ getAbstractionInformation()

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

AbstractionInformation< DdType > const & storm::gbar::abstraction::jani::JaniMenuGameAbstractor< DdType, ValueType >::getAbstractionInformation ( ) const

overridevirtual

Retrieves information about the abstraction.

Returns: The abstraction information object.

Implements storm::gbar::abstraction::MenuGameAbstractor< DdType, ValueType >.

Definition at line 138 of file JaniMenuGameAbstractor.cpp.

◆ getAssignedVariables()

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

std::set< storm::expressions::Variable > const & storm::gbar::abstraction::jani::JaniMenuGameAbstractor< DdType, ValueType >::getAssignedVariables ( uint64_t player1Choice ) const

overridevirtual

Retrieves the variables assigned by the given player 1 choice.

Implements storm::gbar::abstraction::MenuGameAbstractor< DdType, ValueType >.

Definition at line 159 of file JaniMenuGameAbstractor.cpp.

◆ getDdManager()

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

storm::dd::DdManager< DdType > const & storm::gbar::abstraction::jani::JaniMenuGameAbstractor< DdType, ValueType >::getDdManager ( ) const

overridevirtual

Implements storm::gbar::abstraction::MenuGameAbstractor< DdType, ValueType >.

Definition at line 99 of file JaniMenuGameAbstractor.cpp.

◆ getGuard()

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

storm::expressions::Expression const & storm::gbar::abstraction::jani::JaniMenuGameAbstractor< DdType, ValueType >::getGuard ( uint64_t player1Choice ) const

overridevirtual

Retrieves the guard predicate of the given player 1 choice.

Parameters

player1Choice The choice for which to retrieve the guard.

Returns: The guard of the player 1 choice.

Implements storm::gbar::abstraction::MenuGameAbstractor< DdType, ValueType >.

Definition at line 143 of file JaniMenuGameAbstractor.cpp.

◆ getInitialExpression()

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

storm::expressions::Expression storm::gbar::abstraction::jani::JaniMenuGameAbstractor< DdType, ValueType >::getInitialExpression ( ) const

overridevirtual

Retrieves the expression that characterizes the initial states.

Implements storm::gbar::abstraction::MenuGameAbstractor< DdType, ValueType >.

Definition at line 169 of file JaniMenuGameAbstractor.cpp.

◆ getNumberOfPredicates()

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

uint64_t storm::gbar::abstraction::jani::JaniMenuGameAbstractor< DdType, ValueType >::getNumberOfPredicates ( ) const

overridevirtual

Retrieves the number of predicates currently in use.

Implements storm::gbar::abstraction::MenuGameAbstractor< DdType, ValueType >.

Definition at line 319 of file JaniMenuGameAbstractor.cpp.

◆ getNumberOfUpdates()

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

uint64_t storm::gbar::abstraction::jani::JaniMenuGameAbstractor< DdType, ValueType >::getNumberOfUpdates ( uint64_t player1Choice ) const

overridevirtual

Retrieves the number of updates of the specified player 1 choice.

Implements storm::gbar::abstraction::MenuGameAbstractor< DdType, ValueType >.

Definition at line 148 of file JaniMenuGameAbstractor.cpp.

◆ getPlayer1ChoiceRange()

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

std::pair< uint64_t, uint64_t > storm::gbar::abstraction::jani::JaniMenuGameAbstractor< DdType, ValueType >::getPlayer1ChoiceRange ( ) const

overridevirtual

Retrieves the range of player 1 choices.

Implements storm::gbar::abstraction::MenuGameAbstractor< DdType, ValueType >.

Definition at line 164 of file JaniMenuGameAbstractor.cpp.

◆ getStates()

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

storm::dd::Bdd< DdType > storm::gbar::abstraction::jani::JaniMenuGameAbstractor< DdType, ValueType >::getStates ( storm::expressions::Expression const & expression )

overridevirtual

Retrieves a BDD that characterizes the states corresponding to the given expression.

For this to work, appropriate predicates must have been used to refine the abstraction, otherwise this will fail.

Implements storm::gbar::abstraction::MenuGameAbstractor< DdType, ValueType >.

Definition at line 174 of file JaniMenuGameAbstractor.cpp.

◆ getVariableUpdates()

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

std::map< storm::expressions::Variable, storm::expressions::Expression > storm::gbar::abstraction::jani::JaniMenuGameAbstractor< DdType, ValueType >::getVariableUpdates	(	uint64_t	player1Choice,
		uint64_t	auxiliaryChoice
	)		const

overridevirtual

Retrieves a mapping from variables to expressions that define their updates wrt.

to the given player 1 choice and auxiliary choice.

Implements storm::gbar::abstraction::MenuGameAbstractor< DdType, ValueType >.

Definition at line 153 of file JaniMenuGameAbstractor.cpp.

◆ notifyGuardsArePredicates()

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

void storm::gbar::abstraction::jani::JaniMenuGameAbstractor< DdType, ValueType >::notifyGuardsArePredicates ( )

overridevirtual

Notifies the abstractor that the guards are predicates, which may be used to improve the bottom state computation.

Implements storm::gbar::abstraction::MenuGameAbstractor< DdType, ValueType >.

Definition at line 329 of file JaniMenuGameAbstractor.cpp.

◆ operator=() [1/2]

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

JaniMenuGameAbstractor & storm::gbar::abstraction::jani::JaniMenuGameAbstractor< DdType, ValueType >::operator= ( JaniMenuGameAbstractor< DdType, ValueType > && )

default

◆ operator=() [2/2]

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

JaniMenuGameAbstractor & storm::gbar::abstraction::jani::JaniMenuGameAbstractor< DdType, ValueType >::operator= ( JaniMenuGameAbstractor< DdType, ValueType > const & )

default

◆ refine()

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

void storm::gbar::abstraction::jani::JaniMenuGameAbstractor< DdType, ValueType >::refine ( RefinementCommand const & command )

overridevirtual

Performs the given refinement command.

Parameters

command The command to perform.

Implements storm::gbar::abstraction::MenuGameAbstractor< DdType, ValueType >.

Definition at line 104 of file JaniMenuGameAbstractor.cpp.

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

src/storm-gamebased-ar/abstraction/jani/JaniMenuGameAbstractor.h
src/storm-gamebased-ar/abstraction/jani/JaniMenuGameAbstractor.cpp

Public Member Functions

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

◆ JaniMenuGameAbstractor() [1/3]

◆ JaniMenuGameAbstractor() [2/3]

◆ JaniMenuGameAbstractor() [3/3]

Member Function Documentation

◆ abstract()

◆ addTerminalStates()

◆ exportToDot()

◆ getAbstractionInformation()

◆ getAssignedVariables()

◆ getDdManager()

◆ getGuard()

◆ getInitialExpression()

◆ getNumberOfPredicates()

◆ getNumberOfUpdates()

◆ getPlayer1ChoiceRange()

◆ getStates()

◆ getVariableUpdates()

◆ notifyGuardsArePredicates()

◆ operator=() [1/2]

◆ operator=() [2/2]

◆ refine()