storm::gbar::abstraction Namespace Reference

Namespaces
namespace	jani
namespace	prism

Classes
class	AbstractionInformation
struct	AbstractionInformationOptions
struct	BottomStateResult
struct	ExplicitDijkstraQueueElement
struct	ExplicitDijkstraQueueElementLess
struct	ExplicitPivotStateResult
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	MenuGameAbstractorOptions
class	MenuGameRefiner
struct	MenuGameRefinerOptions
struct	PivotStateCandidatesResult
class	QualitativeResult
class	QualitativeResultMinMax
class	RefinementCommand
class	RefinementPredicates
class	StateSet
class	StateSetAbstractor
struct	SymbolicMostProbablePathsResult
struct	SymbolicPivotStateResult
class	SymbolicQualitativeGameResult
class	SymbolicQualitativeGameResultMinMax
class	SymbolicQualitativeMdpResult
class	SymbolicQualitativeMdpResultMinMax
class	SymbolicQualitativeResult
class	SymbolicQualitativeResultMinMax
class	SymbolicQuantitativeGameResult
class	SymbolicQuantitativeGameResultMinMax
class	SymbolicStateSet
class	ValidBlockAbstractor
struct	VariableSetHash

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 (AbstractionSettings::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, AbstractionSettings::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)

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 532 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 122 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 38 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 1146 of file MenuGameRefiner.cpp.

pickPivotState() [1/2]

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

SymbolicPivotStateResult< Type, ValueType > storm::gbar::abstraction::pickPivotState	(	AbstractionSettings::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 162 of file MenuGameRefiner.cpp.

pickPivotState() [2/2]

template<typename ValueType >

boost::optional< ExplicitPivotStateResult< ValueType > > storm::gbar::abstraction::pickPivotState	(	bool	generatePredecessors,
		AbstractionSettings::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 1188 of file MenuGameRefiner.cpp.