#include <MenuGameAbstractor.h>
Public Member Functions | |
| MenuGameAbstractor () | |
| virtual | ~MenuGameAbstractor ()=default |
| virtual storm::dd::DdManager< DdType > const & | getDdManager () const =0 |
| virtual MenuGame< DdType, ValueType > | abstract ()=0 |
| Retrieves the abstraction. | |
| virtual AbstractionInformation< DdType > const & | getAbstractionInformation () const =0 |
| Retrieves information about the abstraction. | |
| virtual storm::expressions::Expression const & | getGuard (uint64_t player1Choice) const =0 |
| virtual std::pair< uint64_t, uint64_t > | getPlayer1ChoiceRange () const =0 |
| virtual uint64_t | getNumberOfUpdates (uint64_t player1Choice) const =0 |
| std::vector< std::map< storm::expressions::Variable, storm::expressions::Expression > > | getVariableUpdates (uint64_t player1Choice) const |
| virtual std::map< storm::expressions::Variable, storm::expressions::Expression > | getVariableUpdates (uint64_t player1Choice, uint64_t auxiliaryChoice) const =0 |
| virtual std::set< storm::expressions::Variable > const & | getAssignedVariables (uint64_t player1Choice) const =0 |
| virtual storm::expressions::Expression | getInitialExpression () const =0 |
| virtual storm::dd::Bdd< DdType > | getStates (storm::expressions::Expression const &expression)=0 |
| Retrieves a BDD that characterizes the states corresponding to the given expression. | |
| virtual void | refine (RefinementCommand const &command)=0 |
| Methods to refine the abstraction. | |
| virtual void | exportToDot (std::string const &filename, storm::dd::Bdd< DdType > const &highlightStatesBdd, storm::dd::Bdd< DdType > const &filter) const =0 |
| Exports a representation of the current abstraction state in the dot format. | |
| virtual uint64_t | getNumberOfPredicates () const =0 |
| Retrieves the number of predicates currently in use. | |
| virtual void | addTerminalStates (storm::expressions::Expression const &expression)=0 |
| Adds the expression to the ones characterizing terminal states, i.e. | |
| void | setTargetStates (storm::expressions::Expression const &targetStateExpression) |
| Sets the expression characterizing the target states. | |
| storm::expressions::Expression const & | getTargetStateExpression () const |
| bool | hasTargetStateExpression () const |
| virtual void | notifyGuardsArePredicates ()=0 |
| Notifies the abstractor that the guards are predicates, which may be used to improve the bottom state computation. | |
Protected Member Functions | |
| bool | isRestrictToRelevantStatesSet () const |
| void | exportToDot (storm::gbar::abstraction::MenuGame< DdType, ValueType > const ¤tGame, std::string const &filename, storm::dd::Bdd< DdType > const &highlightStatesBdd, storm::dd::Bdd< DdType > const &filter) const |
Detailed Description
class storm::gbar::abstraction::MenuGameAbstractor< DdType, ValueType >
Definition at line 36 of file MenuGameAbstractor.h.
Constructor & Destructor Documentation
◆ MenuGameAbstractor()
| storm::gbar::abstraction::MenuGameAbstractor< DdType, ValueType >::MenuGameAbstractor | ( | ) |
Definition at line 22 of file MenuGameAbstractor.cpp.
◆ ~MenuGameAbstractor()
|
virtualdefault |
Member Function Documentation
◆ abstract()
|
pure virtual |
Retrieves the abstraction.
Implemented in storm::gbar::abstraction::jani::JaniMenuGameAbstractor< DdType, ValueType >, and storm::gbar::abstraction::prism::PrismMenuGameAbstractor< DdType, ValueType >.
◆ addTerminalStates()
|
pure virtual |
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.
Implemented in storm::gbar::abstraction::jani::JaniMenuGameAbstractor< DdType, ValueType >, and storm::gbar::abstraction::prism::PrismMenuGameAbstractor< DdType, ValueType >.
◆ exportToDot() [1/2]
|
pure virtual |
Exports a representation of the current abstraction state in the dot format.
Implemented in storm::gbar::abstraction::jani::JaniMenuGameAbstractor< DdType, ValueType >, and storm::gbar::abstraction::prism::PrismMenuGameAbstractor< DdType, ValueType >.
◆ exportToDot() [2/2]
|
protected |
Definition at line 75 of file MenuGameAbstractor.cpp.
◆ getAbstractionInformation()
|
pure virtual |
Retrieves information about the abstraction.
Implemented in storm::gbar::abstraction::jani::JaniMenuGameAbstractor< DdType, ValueType >, and storm::gbar::abstraction::prism::PrismMenuGameAbstractor< DdType, ValueType >.
◆ getAssignedVariables()
|
pure virtual |
◆ getDdManager()
|
pure virtual |
◆ getGuard()
|
pure virtual |
◆ getInitialExpression()
|
pure virtual |
◆ getNumberOfPredicates()
|
pure virtual |
Retrieves the number of predicates currently in use.
Implemented in storm::gbar::abstraction::jani::JaniMenuGameAbstractor< DdType, ValueType >, and storm::gbar::abstraction::prism::PrismMenuGameAbstractor< DdType, ValueType >.
◆ getNumberOfUpdates()
|
pure virtual |
◆ getPlayer1ChoiceRange()
|
pure virtual |
◆ getStates()
|
pure virtual |
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.
Implemented in storm::gbar::abstraction::jani::JaniMenuGameAbstractor< DdType, ValueType >, and storm::gbar::abstraction::prism::PrismMenuGameAbstractor< DdType, ValueType >.
◆ getTargetStateExpression()
| storm::expressions::Expression const & storm::gbar::abstraction::MenuGameAbstractor< DdType, ValueType >::getTargetStateExpression | ( | ) | const |
Definition at line 184 of file MenuGameAbstractor.cpp.
◆ getVariableUpdates() [1/2]
| std::vector< std::map< storm::expressions::Variable, storm::expressions::Expression > > storm::gbar::abstraction::MenuGameAbstractor< DdType, ValueType >::getVariableUpdates | ( | uint64_t | player1Choice | ) | const |
Definition at line 28 of file MenuGameAbstractor.cpp.
◆ getVariableUpdates() [2/2]
|
pure virtual |
◆ hasTargetStateExpression()
| bool storm::gbar::abstraction::MenuGameAbstractor< DdType, ValueType >::hasTargetStateExpression | ( | ) | const |
Definition at line 189 of file MenuGameAbstractor.cpp.
◆ isRestrictToRelevantStatesSet()
|
protected |
Definition at line 70 of file MenuGameAbstractor.cpp.
◆ notifyGuardsArePredicates()
|
pure virtual |
Notifies the abstractor that the guards are predicates, which may be used to improve the bottom state computation.
Implemented in storm::gbar::abstraction::jani::JaniMenuGameAbstractor< DdType, ValueType >, and storm::gbar::abstraction::prism::PrismMenuGameAbstractor< DdType, ValueType >.
◆ refine()
|
pure virtual |
Methods to refine the abstraction.
Implemented in storm::gbar::abstraction::jani::JaniMenuGameAbstractor< DdType, ValueType >, and storm::gbar::abstraction::prism::PrismMenuGameAbstractor< DdType, ValueType >.
◆ setTargetStates()
| void storm::gbar::abstraction::MenuGameAbstractor< DdType, ValueType >::setTargetStates | ( | storm::expressions::Expression const & | targetStateExpression | ) |
Sets the expression characterizing the target states.
For this to work, appropriate predicates must have been used to refine the abstraction, otherwise this will fail.
Definition at line 179 of file MenuGameAbstractor.cpp.
The documentation for this class was generated from the following files:
- src/storm-gamebased-ar/abstraction/MenuGameAbstractor.h
- src/storm-gamebased-ar/abstraction/MenuGameAbstractor.cpp
