Namespaces
namespace	jani
namespace	prism

Classes
struct	AbstractionInformationOptions
class	AbstractionInformation
struct	AbstractionOptions
	Options that configure the game-based abstraction-refinement procedure. More...
struct	BottomStateResult
class	ExplicitQualitativeGameResult
class	ExplicitQualitativeGameResultMinMax
class	ExplicitQualitativeResult
class	ExplicitQualitativeResultMinMax
class	ExplicitQuantitativeResult
class	ExplicitQuantitativeResultMinMax
class	ExpressionTranslator
struct	GameBddResult
class	LocalExpressionInformation
class	MenuGame
	This class represents a discrete-time stochastic two-player game. More...
class	MenuGameAbstractor
struct	PivotStateCandidatesResult
struct	ExplicitDijkstraQueueElement
struct	ExplicitDijkstraQueueElementLess
struct	VariableSetHash
class	RefinementPredicates
struct	SymbolicMostProbablePathsResult
struct	SymbolicPivotStateResult
struct	ExplicitPivotStateResult
class	MenuGameRefiner
class	SymbolicQualitativeResult
class	QualitativeResult
class	SymbolicQualitativeResultMinMax
class	QualitativeResultMinMax
class	RefinementCommand
class	SymbolicStateSet
class	StateSet
class	StateSetAbstractor
class	SymbolicQualitativeGameResult
class	SymbolicQualitativeGameResultMinMax
class	SymbolicQualitativeMdpResult
class	SymbolicQualitativeMdpResultMinMax
class	SymbolicQuantitativeGameResult
class	SymbolicQuantitativeGameResultMinMax
class	ValidBlockAbstractor

Enumerations
enum class	PivotSelectionHeuristic { NearestMaximalDeviation , MostProbablePath , MaxWeightedDeviation }
enum class	SplitMode { All , None , NonGuard }
enum class	ReuseMode { All , None , Qualitative , Quantitative }
enum class	SolveMode { Dd , Sparse }
enum class	ValidBlockMode { MorePredicates , BlockEnumeration }

Functions
template<storm::dd::DdType DdType>
std::ostream &	operator<< (std::ostream &out, LocalExpressionInformation< DdType > const &partition)
template std::ostream &	operator<< (std::ostream &out, LocalExpressionInformation< storm::dd::DdType::CUDD > const &partition)
template std::ostream &	operator<< (std::ostream &out, LocalExpressionInformation< storm::dd::DdType::Sylvan > const &partition)
template<typename ValueType>
std::string	getStateName (std::pair< storm::expressions::SimpleValuation, ValueType > const &stateValue, std::set< storm::expressions::Variable > const &locationVariables, std::set< storm::expressions::Variable > const &predicateVariables, storm::expressions::Variable const &bottomVariable)
template<storm::dd::DdType Type, typename ValueType>
SymbolicMostProbablePathsResult< Type, ValueType >	getMostProbablePathSpanningTree (storm::gbar::abstraction::MenuGame< Type, ValueType > const &game, storm::dd::Bdd< Type > const &transitionFilter)
template<storm::dd::DdType Type, typename ValueType>
SymbolicPivotStateResult< Type, ValueType >	pickPivotState (PivotSelectionHeuristic const &heuristic, storm::gbar::abstraction::MenuGame< Type, ValueType > const &game, PivotStateCandidatesResult< Type > const &pivotStateCandidateResult, boost::optional< SymbolicQualitativeGameResultMinMax< Type > > const &qualitativeResult, boost::optional< SymbolicQuantitativeGameResultMinMax< Type, ValueType > > const &quantitativeResult)
template<storm::dd::DdType Type, typename ValueType>
PivotStateCandidatesResult< Type >	computePivotStates (storm::gbar::abstraction::MenuGame< Type, ValueType > const &game, storm::dd::Bdd< Type > const &transitionMatrixBdd, storm::dd::Bdd< Type > const &minPlayer1Strategy, storm::dd::Bdd< Type > const &minPlayer2Strategy, storm::dd::Bdd< Type > const &maxPlayer1Strategy, storm::dd::Bdd< Type > const &maxPlayer2Strategy)
template<typename ValueType>
void	performDijkstraStep (std::set< ExplicitDijkstraQueueElement< ValueType >, ExplicitDijkstraQueueElementLess< ValueType > > &dijkstraQueue, bool probabilityDistances, std::vector< ValueType > &distances, std::vector< std::pair< uint64_t, uint64_t > > &predecessors, bool generatePredecessors, bool lower, uint64_t currentState, ValueType const &currentDistance, bool isPivotState, storm::storage::ExplicitGameStrategyPair const &strategyPair, storm::storage::ExplicitGameStrategyPair const &otherStrategyPair, std::vector< uint64_t > const &player1Labeling, std::vector< uint64_t > const &player2Grouping, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::BitVector const &targetStates, storm::storage::BitVector const &relevantStates)
template<typename ValueType>
boost::optional< ExplicitPivotStateResult< ValueType > >	pickPivotState (bool generatePredecessors, PivotSelectionHeuristic pivotSelectionHeuristic, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, std::vector< uint64_t > const &player1Labeling, storm::storage::BitVector const &initialStates, storm::storage::BitVector const &relevantStates, storm::storage::BitVector const &targetStates, storage::ExplicitGameStrategyPair const &minStrategyPair, storage::ExplicitGameStrategyPair const &maxStrategyPair, std::vector< ValueType > const lowerValues=nullptr, std::vector< ValueType > const upperValues=nullptr)

Variables
template<typename ValueType>
const uint64_t	ExplicitPivotStateResult< ValueType >::NO_PREDECESSOR = std::numeric_limits<uint64_t>::max()

Enumeration Type Documentation

◆ PivotSelectionHeuristic

enum class storm::gbar::abstraction::PivotSelectionHeuristic

strong

Enumerator
NearestMaximalDeviation
MostProbablePath
MaxWeightedDeviation

Definition at line 11 of file AbstractionOptions.h.

◆ ReuseMode

enum class storm::gbar::abstraction::ReuseMode

strong

Enumerator
All
None
Qualitative
Quantitative

Definition at line 15 of file AbstractionOptions.h.

◆ SolveMode

enum class storm::gbar::abstraction::SolveMode

strong

Enumerator
Dd
Sparse

Definition at line 17 of file AbstractionOptions.h.

◆ SplitMode

enum class storm::gbar::abstraction::SplitMode

strong

Enumerator
All
None
NonGuard

Definition at line 13 of file AbstractionOptions.h.

◆ ValidBlockMode

enum class storm::gbar::abstraction::ValidBlockMode

strong

Enumerator
MorePredicates
BlockEnumeration

Definition at line 19 of file AbstractionOptions.h.

Function Documentation

◆ computePivotStates()

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

PivotStateCandidatesResult< Type > storm::gbar::abstraction::computePivotStates	(	storm::gbar::abstraction::MenuGame< Type, ValueType > const &	game,
		storm::dd::Bdd< Type > const &	transitionMatrixBdd,
		storm::dd::Bdd< Type > const &	minPlayer1Strategy,
		storm::dd::Bdd< Type > const &	minPlayer2Strategy,
		storm::dd::Bdd< Type > const &	maxPlayer1Strategy,
		storm::dd::Bdd< Type > const &	maxPlayer2Strategy )

Definition at line 511 of file MenuGameRefiner.cpp.

◆ getMostProbablePathSpanningTree()

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

SymbolicMostProbablePathsResult< Type, ValueType > storm::gbar::abstraction::getMostProbablePathSpanningTree	(	storm::gbar::abstraction::MenuGame< Type, ValueType > const &	game,
		storm::dd::Bdd< Type > const &	transitionFilter )

Definition at line 101 of file MenuGameRefiner.cpp.

◆ getStateName()

template<typename ValueType>

std::string storm::gbar::abstraction::getStateName	(	std::pair< storm::expressions::SimpleValuation, ValueType > const &	stateValue,
		std::set< storm::expressions::Variable > const &	locationVariables,
		std::set< storm::expressions::Variable > const &	predicateVariables,
		storm::expressions::Variable const &	bottomVariable )

Definition at line 29 of file MenuGameAbstractor.cpp.

◆ operator<<() [1/3]

template<storm::dd::DdType DdType>

std::ostream & storm::gbar::abstraction::operator<<	(	std::ostream &	out,
		LocalExpressionInformation< DdType > const &	partition )

Definition at line 205 of file LocalExpressionInformation.cpp.

◆ operator<<() [2/3]

template std::ostream & storm::gbar::abstraction::operator<<	(	std::ostream &	out,
		LocalExpressionInformation< storm::dd::DdType::CUDD > const &	partition )

◆ operator<<() [3/3]

template std::ostream & storm::gbar::abstraction::operator<<	(	std::ostream &	out,
		LocalExpressionInformation< storm::dd::DdType::Sylvan > const &	partition )

◆ performDijkstraStep()

template<typename ValueType>

void storm::gbar::abstraction::performDijkstraStep	(	std::set< ExplicitDijkstraQueueElement< ValueType >, ExplicitDijkstraQueueElementLess< ValueType > > &	dijkstraQueue,
		bool	probabilityDistances,
		std::vector< ValueType > &	distances,
		std::vector< std::pair< uint64_t, uint64_t > > &	predecessors,
		bool	generatePredecessors,
		bool	lower,
		uint64_t	currentState,
		ValueType const &	currentDistance,
		bool	isPivotState,
		storm::storage::ExplicitGameStrategyPair const &	strategyPair,
		storm::storage::ExplicitGameStrategyPair const &	otherStrategyPair,
		std::vector< uint64_t > const &	player1Labeling,
		std::vector< uint64_t > const &	player2Grouping,
		storm::storage::SparseMatrix< ValueType > const &	transitionMatrix,
		storm::storage::BitVector const &	targetStates,
		storm::storage::BitVector const &	relevantStates )

Definition at line 1125 of file MenuGameRefiner.cpp.

◆ pickPivotState() [1/2]

template<typename ValueType>

boost::optional< ExplicitPivotStateResult< ValueType > > storm::gbar::abstraction::pickPivotState	(	bool	generatePredecessors,
		PivotSelectionHeuristic	pivotSelectionHeuristic,
		storm::storage::SparseMatrix< ValueType > const &	transitionMatrix,
		std::vector< uint64_t > const &	player1Labeling,
		storm::storage::BitVector const &	initialStates,
		storm::storage::BitVector const &	relevantStates,
		storm::storage::BitVector const &	targetStates,
		storage::ExplicitGameStrategyPair const &	minStrategyPair,
		storage::ExplicitGameStrategyPair const &	maxStrategyPair,
		std::vector< ValueType > const *	lowerValues = nullptr,
		std::vector< ValueType > const *	upperValues = nullptr )

Definition at line 1167 of file MenuGameRefiner.cpp.

◆ pickPivotState() [2/2]

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

SymbolicPivotStateResult< Type, ValueType > storm::gbar::abstraction::pickPivotState	(	PivotSelectionHeuristic const &	heuristic,
		storm::gbar::abstraction::MenuGame< Type, ValueType > const &	game,
		PivotStateCandidatesResult< Type > const &	pivotStateCandidateResult,
		boost::optional< SymbolicQualitativeGameResultMinMax< Type > > const &	qualitativeResult,
		boost::optional< SymbolicQuantitativeGameResultMinMax< Type, ValueType > > const &	quantitativeResult )

Definition at line 141 of file MenuGameRefiner.cpp.

Variable Documentation

◆ ExplicitPivotStateResult< ValueType >::NO_PREDECESSOR

template<typename ValueType>

const uint64_t storm::gbar::abstraction::ExplicitPivotStateResult< ValueType >::NO_PREDECESSOR = std::numeric_limits<uint64_t>::max()

Definition at line 717 of file MenuGameRefiner.cpp.

Namespaces

Classes

Enumerations

Functions

Variables

Enumeration Type Documentation

◆ PivotSelectionHeuristic

◆ ReuseMode

◆ SolveMode

◆ SplitMode

◆ ValidBlockMode

Function Documentation

◆ computePivotStates()

◆ getMostProbablePathSpanningTree()

◆ getStateName()

◆ operator<<() [1/3]

◆ operator<<() [2/3]

◆ operator<<() [3/3]

◆ performDijkstraStep()

◆ pickPivotState() [1/2]

◆ pickPivotState() [2/2]

Variable Documentation

◆ ExplicitPivotStateResult< ValueType >::NO_PREDECESSOR