This class represents the settings for the abstraction procedures. More...

#include <AbstractionSettings.h>

Inheritance diagram for storm::settings::modules::AbstractionSettings:

Collaboration diagram for storm::settings::modules::AbstractionSettings:

Public Types
enum class	Method { Games , Bisimulation }
using	PivotSelectionHeuristic = storm::gbar::abstraction::PivotSelectionHeuristic
using	SplitMode = storm::gbar::abstraction::SplitMode
using	ReuseMode = storm::gbar::abstraction::ReuseMode
using	SolveMode = storm::gbar::abstraction::SolveMode
using	ValidBlockMode = storm::gbar::abstraction::ValidBlockMode

Public Member Functions
	AbstractionSettings ()
	Creates a new set of abstraction settings.
Method	getAbstractionRefinementMethod () const
	Retrieves the selected abstraction refinement method.
bool	isUseDecompositionSet () const
	Retrieves whether the option to use the decomposition was set.
SplitMode	getSplitMode () const
	Retrieves the selected split mode.
bool	isAddAllGuardsSet () const
	Retrieves whether the option to add all guards was set.
bool	isAddAllInitialExpressionsSet () const
	Retrieves whether the option to add all initial expressions was set.
void	setAddAllGuards (bool value)
	Sets the option to add all guards to the specified value.
void	setAddAllInitialExpressions (bool value)
	Sets the option to add all initial expressions to the specified value.
bool	isUseInterpolationSet () const
	Retrieves whether the option to use interpolation was set.
double	getPrecision () const
	Retrieves the precision that is used for detecting convergence.
bool	getRelativeTerminationCriterion () const
	Retrieves whether to use a relative termination criterion for detecting convergence.
PivotSelectionHeuristic	getPivotSelectionHeuristic () const
	Retrieves the selected heuristic to select pivot blocks.
ReuseMode	getReuseMode () const
	Retrieves the selected reuse mode.
bool	isRestrictToRelevantStatesSet () const
	Retrieves whether only relevant states are to be considered.
SolveMode	getSolveMode () const
	Retrieves the mode with which to solve the games.
uint_fast64_t	getMaximalAbstractionCount () const
	Retrieves the maximal number of abstractions to perform until giving up on converging.
bool	isRankRefinementPredicatesSet () const
bool	isConstraintsSet () const
	Retrieves whether the constraints option was set.
std::string	getConstraintString () const
	Retrieves the string that specifies additional constraints.
bool	isUseEagerRefinementSet () const
	Retrieves whether to refine eagerly.
bool	isDebugSet () const
	Retrieves whether the debug option was set.
bool	isInjectRefinementPredicatesSet () const
	Retrieves whether the option to inject the refinement predicates is set.
std::string	getInjectedRefinementPredicates () const
	Retrieves a string containing refinement predicates to inject (if there are any).
bool	isFixPlayer1StrategySet () const
	Retrieves whether player 1 strategies are to be fixed.
bool	isFixPlayer2StrategySet () const
	Retrieves whether player 2 strategies are to be fixed.
ValidBlockMode	getValidBlockMode () const
	Retrieves the selected mode to guarantee valid blocks.
Public Member Functions inherited from storm::settings::modules::ModuleSettings
	ModuleSettings (std::string const &moduleName)
	Constructs a new settings object.
virtual	~ModuleSettings ()
virtual bool	check () const
	Checks whether the settings are consistent.
virtual void	finalize ()
	Prepares the modules for further usage, should be called at the end of the initialization, before checks are executed.
std::string const &	getModuleName () const
	Retrieves the name of the module to which these settings belong.
std::vector< std::shared_ptr< Option > > const &	getOptions () const
	Retrieves the options of this module.
uint_fast64_t	getPrintLengthOfLongestOption (bool includeAdvanced) const
	Retrieves the (print) length of the longest option.
void	restoreDefaults ()
	Restores the default values for all arguments of all options and marks all options as not set.

Static Public Attributes
static const std::string	moduleName = "abstraction"

Additional Inherited Members
Protected Member Functions inherited from storm::settings::modules::ModuleSettings
Option &	getOption (std::string const &longName)
	Retrieves the option with the given long name.
Option const &	getOption (std::string const &longName) const
	Retrieves the option with the given long name.
bool	isSet (std::string const &optionName) const
	Retrieves whether the option with the given name was set.
void	addOption (std::shared_ptr< Option > const &option)
	Adds and registers the given option.

Detailed Description

This class represents the settings for the abstraction procedures.

Definition at line 13 of file AbstractionSettings.h.

Member Typedef Documentation

◆ PivotSelectionHeuristic

using storm::settings::modules::AbstractionSettings::PivotSelectionHeuristic = storm::gbar::abstraction::PivotSelectionHeuristic

Definition at line 19 of file AbstractionSettings.h.

◆ ReuseMode

using storm::settings::modules::AbstractionSettings::ReuseMode = storm::gbar::abstraction::ReuseMode

Definition at line 23 of file AbstractionSettings.h.

◆ SolveMode

using storm::settings::modules::AbstractionSettings::SolveMode = storm::gbar::abstraction::SolveMode

Definition at line 25 of file AbstractionSettings.h.

◆ SplitMode

using storm::settings::modules::AbstractionSettings::SplitMode = storm::gbar::abstraction::SplitMode

Definition at line 21 of file AbstractionSettings.h.

◆ ValidBlockMode

using storm::settings::modules::AbstractionSettings::ValidBlockMode = storm::gbar::abstraction::ValidBlockMode

Definition at line 27 of file AbstractionSettings.h.

Member Enumeration Documentation

◆ Method

enum class storm::settings::modules::AbstractionSettings::Method

strong

Enumerator
Games
Bisimulation

Definition at line 15 of file AbstractionSettings.h.

Constructor & Destructor Documentation

◆ AbstractionSettings()

storm::settings::modules::AbstractionSettings::AbstractionSettings ( )

Creates a new set of abstraction settings.

Definition at line 99 of file AbstractionSettings.cpp.

Member Function Documentation

◆ getAbstractionRefinementMethod()

AbstractionSettings::Method storm::settings::modules::AbstractionSettings::getAbstractionRefinementMethod ( ) const

Retrieves the selected abstraction refinement method.

Definition at line 280 of file AbstractionSettings.cpp.

◆ getConstraintString()

std::string storm::settings::modules::AbstractionSettings::getConstraintString ( ) const

Retrieves the string that specifies additional constraints.

Returns: The string that defines the constraints.

Definition at line 384 of file AbstractionSettings.cpp.

◆ getInjectedRefinementPredicates()

std::string storm::settings::modules::AbstractionSettings::getInjectedRefinementPredicates ( ) const

Retrieves a string containing refinement predicates to inject (if there are any).

Definition at line 400 of file AbstractionSettings.cpp.

◆ getMaximalAbstractionCount()

uint_fast64_t storm::settings::modules::AbstractionSettings::getMaximalAbstractionCount ( ) const

Retrieves the maximal number of abstractions to perform until giving up on converging.

Returns: The maximal abstraction count.

Definition at line 372 of file AbstractionSettings.cpp.

◆ getPivotSelectionHeuristic()

AbstractionSettings::PivotSelectionHeuristic storm::settings::modules::AbstractionSettings::getPivotSelectionHeuristic ( ) const

Retrieves the selected heuristic to select pivot blocks.

Returns: The selected heuristic.

Definition at line 346 of file AbstractionSettings.cpp.

◆ getPrecision()

double storm::settings::modules::AbstractionSettings::getPrecision ( ) const

Retrieves the precision that is used for detecting convergence.

Returns: The precision to use for detecting convergence.

Definition at line 338 of file AbstractionSettings.cpp.

◆ getRelativeTerminationCriterion()

bool storm::settings::modules::AbstractionSettings::getRelativeTerminationCriterion ( ) const

Retrieves whether to use a relative termination criterion for detecting convergence.

Definition at line 342 of file AbstractionSettings.cpp.

◆ getReuseMode()

AbstractionSettings::ReuseMode storm::settings::modules::AbstractionSettings::getReuseMode ( ) const

Retrieves the selected reuse mode.

Returns: The selected reuse mode.

Definition at line 358 of file AbstractionSettings.cpp.

◆ getSolveMode()

AbstractionSettings::SolveMode storm::settings::modules::AbstractionSettings::getSolveMode ( ) const

Retrieves the mode with which to solve the games.

Definition at line 306 of file AbstractionSettings.cpp.

◆ getSplitMode()

AbstractionSettings::SplitMode storm::settings::modules::AbstractionSettings::getSplitMode ( ) const

Retrieves the selected split mode.

Returns: The selected split mode.

Definition at line 294 of file AbstractionSettings.cpp.

◆ getValidBlockMode()

AbstractionSettings::ValidBlockMode storm::settings::modules::AbstractionSettings::getValidBlockMode ( ) const

Retrieves the selected mode to guarantee valid blocks.

Definition at line 412 of file AbstractionSettings.cpp.

◆ isAddAllGuardsSet()

bool storm::settings::modules::AbstractionSettings::isAddAllGuardsSet ( ) const

Retrieves whether the option to add all guards was set.

Returns: True iff the option was set.

Definition at line 314 of file AbstractionSettings.cpp.

◆ isAddAllInitialExpressionsSet()

bool storm::settings::modules::AbstractionSettings::isAddAllInitialExpressionsSet ( ) const

Retrieves whether the option to add all initial expressions was set.

Returns: True iff the option was set.

Definition at line 318 of file AbstractionSettings.cpp.

◆ isConstraintsSet()

bool storm::settings::modules::AbstractionSettings::isConstraintsSet ( ) const

Retrieves whether the constraints option was set.

Returns: True if the constraints option was set.

Definition at line 380 of file AbstractionSettings.cpp.

◆ isDebugSet()

bool storm::settings::modules::AbstractionSettings::isDebugSet ( ) const

Retrieves whether the debug option was set.

Definition at line 392 of file AbstractionSettings.cpp.

◆ isFixPlayer1StrategySet()

bool storm::settings::modules::AbstractionSettings::isFixPlayer1StrategySet ( ) const

Retrieves whether player 1 strategies are to be fixed.

Definition at line 404 of file AbstractionSettings.cpp.

◆ isFixPlayer2StrategySet()

bool storm::settings::modules::AbstractionSettings::isFixPlayer2StrategySet ( ) const

Retrieves whether player 2 strategies are to be fixed.

Definition at line 408 of file AbstractionSettings.cpp.

◆ isInjectRefinementPredicatesSet()

bool storm::settings::modules::AbstractionSettings::isInjectRefinementPredicatesSet ( ) const

Retrieves whether the option to inject the refinement predicates is set.

Definition at line 396 of file AbstractionSettings.cpp.

◆ isRankRefinementPredicatesSet()

bool storm::settings::modules::AbstractionSettings::isRankRefinementPredicatesSet ( ) const

Definition at line 376 of file AbstractionSettings.cpp.

◆ isRestrictToRelevantStatesSet()

bool storm::settings::modules::AbstractionSettings::isRestrictToRelevantStatesSet ( ) const

Retrieves whether only relevant states are to be considered.

Returns: True iff the option was set.

Definition at line 334 of file AbstractionSettings.cpp.

◆ isUseDecompositionSet()

bool storm::settings::modules::AbstractionSettings::isUseDecompositionSet ( ) const

Retrieves whether the option to use the decomposition was set.

Returns: True iff the option was set.

Definition at line 290 of file AbstractionSettings.cpp.

◆ isUseEagerRefinementSet()

bool storm::settings::modules::AbstractionSettings::isUseEagerRefinementSet ( ) const

Retrieves whether to refine eagerly.

Definition at line 388 of file AbstractionSettings.cpp.

◆ isUseInterpolationSet()

bool storm::settings::modules::AbstractionSettings::isUseInterpolationSet ( ) const

Retrieves whether the option to use interpolation was set.

Returns: True iff the option was set.

Definition at line 330 of file AbstractionSettings.cpp.

◆ setAddAllGuards()

void storm::settings::modules::AbstractionSettings::setAddAllGuards ( bool value )

Sets the option to add all guards to the specified value.

Parameters

value The new value.

Definition at line 322 of file AbstractionSettings.cpp.

◆ setAddAllInitialExpressions()

void storm::settings::modules::AbstractionSettings::setAddAllInitialExpressions ( bool value )

Sets the option to add all initial expressions to the specified value.