Options that configure the game-based abstraction-refinement procedure. More...

#include <AbstractionOptions.h>

Public Member Functions
	AbstractionOptions ()=default
	AbstractionOptions (std::vector< storm::expressions::Expression > &&constraints, std::vector< std::vector< storm::expressions::Expression > > &&injectedRefinementPredicates)

Public Attributes
bool	restrictToRelevantStates = true
	A flag indicating whether the abstractor restricts the abstraction to relevant states.
bool	restrictToValidBlocks = false
	A flag indicating whether the abstractor restricts the initial states to valid blocks.
bool	useDecomposition = true
	A flag indicating whether decomposition is to be used during the abstraction.
bool	useInterpolation = true
	A flag indicating whether interpolation is to be used to eliminate spurious pivot blocks.
SplitMode	splitMode = SplitMode::All
	The mode that determines which predicates are split into atoms for the refinement.
PivotSelectionHeuristic	pivotSelectionHeuristic = PivotSelectionHeuristic::NearestMaximalDeviation
	The heuristic to use for pivot block selection.
bool	rankRefinementPredicates = false
	A flag indicating whether refinement predicates are to be ranked.
bool	useEagerRefinement = false
	A flag indicating whether to refine eagerly.
bool	addAllGuards = true
	A flag indicating whether all guards are added as initial predicates.
bool	addAllInitialExpressions = true
	A flag indicating whether all initial expressions are added as initial predicates.
double	precision = 1e-03
	The precision used for detecting convergence.
bool	relativeTerminationCriterion = false
	A flag indicating whether to use a relative termination criterion.
SolveMode	solveMode = SolveMode::Sparse
	The mode with which to solve the abstractions.
ReuseMode	reuseMode = ReuseMode::All
	The mode determining which results are reused.
uint_fast64_t	maximalNumberOfAbstractions = 20000
	The maximal number of abstractions to perform until giving up on converging.
bool	fixPlayer1Strategy = true
	A flag indicating whether player 1 strategies are to be fixed.
bool	fixPlayer2Strategy = true
	A flag indicating whether player 2 strategies are to be fixed.
bool	debug = false
	A flag indicating whether debug mode is enabled.
std::vector< storm::expressions::Expression >	constraints
	Additional constraints used by the abstraction.
std::vector< std::vector< storm::expressions::Expression > >	injectedRefinementPredicates
	Predicates that are injected (starting with the last one in this list) instead of the derived ones.

Detailed Description

Options that configure the game-based abstraction-refinement procedure.

The default values correspond to the defaults of the (formerly used) abstraction settings.

Definition at line 25 of file AbstractionOptions.h.

Constructor & Destructor Documentation

◆ AbstractionOptions() [1/2]

storm::gbar::abstraction::AbstractionOptions::AbstractionOptions ( )

default

◆ AbstractionOptions() [2/2]

storm::gbar::abstraction::AbstractionOptions::AbstractionOptions	(	std::vector< storm::expressions::Expression > &&	constraints,
		std::vector< std::vector< storm::expressions::Expression > > &&	injectedRefinementPredicates )

inline

Definition at line 28 of file AbstractionOptions.h.

Member Data Documentation

◆ addAllGuards

bool storm::gbar::abstraction::AbstractionOptions::addAllGuards = true

A flag indicating whether all guards are added as initial predicates.

Definition at line 61 of file AbstractionOptions.h.

◆ addAllInitialExpressions

bool storm::gbar::abstraction::AbstractionOptions::addAllInitialExpressions = true

A flag indicating whether all initial expressions are added as initial predicates.

Definition at line 64 of file AbstractionOptions.h.

◆ constraints

std::vector<storm::expressions::Expression> storm::gbar::abstraction::AbstractionOptions::constraints

Additional constraints used by the abstraction.

Definition at line 93 of file AbstractionOptions.h.

◆ debug

bool storm::gbar::abstraction::AbstractionOptions::debug = false

A flag indicating whether debug mode is enabled.

Definition at line 89 of file AbstractionOptions.h.

◆ fixPlayer1Strategy

bool storm::gbar::abstraction::AbstractionOptions::fixPlayer1Strategy = true

A flag indicating whether player 1 strategies are to be fixed.

Definition at line 83 of file AbstractionOptions.h.

◆ fixPlayer2Strategy

bool storm::gbar::abstraction::AbstractionOptions::fixPlayer2Strategy = true

A flag indicating whether player 2 strategies are to be fixed.

Definition at line 86 of file AbstractionOptions.h.

◆ injectedRefinementPredicates

std::vector<std::vector<storm::expressions::Expression> > storm::gbar::abstraction::AbstractionOptions::injectedRefinementPredicates

Predicates that are injected (starting with the last one in this list) instead of the derived ones.

Definition at line 96 of file AbstractionOptions.h.

◆ maximalNumberOfAbstractions

uint_fast64_t storm::gbar::abstraction::AbstractionOptions::maximalNumberOfAbstractions = 20000

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

Definition at line 80 of file AbstractionOptions.h.

◆ pivotSelectionHeuristic

PivotSelectionHeuristic storm::gbar::abstraction::AbstractionOptions::pivotSelectionHeuristic = PivotSelectionHeuristic::NearestMaximalDeviation

The heuristic to use for pivot block selection.

Definition at line 52 of file AbstractionOptions.h.

◆ precision

double storm::gbar::abstraction::AbstractionOptions::precision = 1e-03

The precision used for detecting convergence.

Definition at line 68 of file AbstractionOptions.h.

◆ rankRefinementPredicates

bool storm::gbar::abstraction::AbstractionOptions::rankRefinementPredicates = false

A flag indicating whether refinement predicates are to be ranked.

Definition at line 55 of file AbstractionOptions.h.

◆ relativeTerminationCriterion

bool storm::gbar::abstraction::AbstractionOptions::relativeTerminationCriterion = false

A flag indicating whether to use a relative termination criterion.

Definition at line 71 of file AbstractionOptions.h.

◆ restrictToRelevantStates

bool storm::gbar::abstraction::AbstractionOptions::restrictToRelevantStates = true

A flag indicating whether the abstractor restricts the abstraction to relevant states.

Definition at line 36 of file AbstractionOptions.h.

◆ restrictToValidBlocks

bool storm::gbar::abstraction::AbstractionOptions::restrictToValidBlocks = false

A flag indicating whether the abstractor restricts the initial states to valid blocks.

Definition at line 39 of file AbstractionOptions.h.

◆ reuseMode

ReuseMode storm::gbar::abstraction::AbstractionOptions::reuseMode = ReuseMode::All

The mode determining which results are reused.

Definition at line 77 of file AbstractionOptions.h.

◆ solveMode

SolveMode storm::gbar::abstraction::AbstractionOptions::solveMode = SolveMode::Sparse

The mode with which to solve the abstractions.

Definition at line 74 of file AbstractionOptions.h.

◆ splitMode

SplitMode storm::gbar::abstraction::AbstractionOptions::splitMode = SplitMode::All

The mode that determines which predicates are split into atoms for the refinement.

Definition at line 49 of file AbstractionOptions.h.

◆ useDecomposition

bool storm::gbar::abstraction::AbstractionOptions::useDecomposition = true

A flag indicating whether decomposition is to be used during the abstraction.

Definition at line 42 of file AbstractionOptions.h.

◆ useEagerRefinement

bool storm::gbar::abstraction::AbstractionOptions::useEagerRefinement = false

A flag indicating whether to refine eagerly.

Definition at line 58 of file AbstractionOptions.h.

◆ useInterpolation

bool storm::gbar::abstraction::AbstractionOptions::useInterpolation = true

A flag indicating whether interpolation is to be used to eliminate spurious pivot blocks.

Definition at line 46 of file AbstractionOptions.h.

The documentation for this struct was generated from the following file:

src/storm-gamebased-ar/abstraction/AbstractionOptions.h

Public Member Functions

Public Attributes