storm::gbar::modelchecker Namespace Reference

Namespaces
namespace	detail

Classes
class	AbstractAbstractionRefinementModelChecker
class	BisimulationAbstractionRefinementModelChecker
class	ExplicitGameExporter
struct	GameBasedMdpModelCheckerOptions
class	GameBasedMdpModelChecker
struct	PreviousExplicitResult
class	ExplicitQuantitativeResult
class	ExplicitQuantitativeResultMinMax
class	SymbolicQuantitativeGameResult
class	SymbolicQuantitativeGameResultMinMax
class	ExplicitGameStrategyPair
class	ExplicitQualitativeGameResult
class	ExplicitQualitativeGameResultMinMax
class	SymbolicQualitativeGameResult
class	SymbolicQualitativeGameResultMinMax

Functions
template<storm::dd::DdType Type, typename ValueType>
std::unique_ptr< storm::modelchecker::CheckResult >	checkForResultAfterQualitativeCheck (storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &checkTask, storm::OptimizationDirection player2Direction, storm::dd::Bdd< Type > const &initialStates, storm::dd::Bdd< Type > const &prob0, storm::dd::Bdd< Type > const &prob1)
template<storm::dd::DdType Type, typename ValueType>
std::unique_ptr< storm::modelchecker::CheckResult >	checkForResultAfterQualitativeCheck (storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &checkTask, storm::dd::Bdd< Type > const &initialStates, SymbolicQualitativeGameResultMinMax< Type > const &qualitativeResult)
template<typename ValueType>
std::unique_ptr< storm::modelchecker::CheckResult >	checkForResultAfterQualitativeCheck (storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &checkTask, storm::OptimizationDirection player2Direction, storm::storage::BitVector const &initialStates, storm::storage::BitVector const &prob0, storm::storage::BitVector const &prob1)
template<typename ValueType>
std::unique_ptr< storm::modelchecker::CheckResult >	checkForResultAfterQualitativeCheck (storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &checkTask, storm::storage::BitVector const &initialStates, ExplicitQualitativeGameResultMinMax const &qualitativeResult)
template<typename ValueType>
std::unique_ptr< storm::modelchecker::CheckResult >	checkForResultAfterQuantitativeCheck (storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &checkTask, storm::OptimizationDirection const &player2Direction, std::pair< ValueType, ValueType > const &initialValueRange)
template<typename ValueType>
std::unique_ptr< storm::modelchecker::CheckResult >	checkForResultAfterQuantitativeCheck (ValueType const &minValue, ValueType const &maxValue, storm::utility::ConstantsComparator< ValueType > const &comparator)
template<storm::dd::DdType Type, typename ValueType>
SymbolicQuantitativeGameResult< Type, ValueType >	solveMaybeStates (Environment const &env, storm::OptimizationDirection const &player1Direction, storm::OptimizationDirection const &player2Direction, storm::gbar::abstraction::MenuGame< Type, ValueType > const &game, storm::dd::Bdd< Type > const &maybeStates, storm::dd::Bdd< Type > const &prob1States, boost::optional< SymbolicQuantitativeGameResult< Type, ValueType > > const &startInfo=boost::none)
template<storm::dd::DdType Type, typename ValueType>
SymbolicQuantitativeGameResult< Type, ValueType >	computeQuantitativeResult (Environment const &env, storm::OptimizationDirection player1Direction, storm::OptimizationDirection player2Direction, storm::gbar::abstraction::MenuGame< Type, ValueType > const &game, SymbolicQualitativeGameResultMinMax< Type > const &qualitativeResult, storm::dd::Add< Type, ValueType > const &initialStatesAdd, storm::dd::Bdd< Type > const &maybeStates, boost::optional< SymbolicQuantitativeGameResult< Type, ValueType > > const &startInfo=boost::none)
template<typename ValueType>
ExplicitQuantitativeResult< ValueType >	computeQuantitativeResult (Environment const &env, storm::OptimizationDirection player1Direction, storm::OptimizationDirection player2Direction, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, std::vector< uint64_t > const &player1Groups, ExplicitQualitativeGameResultMinMax const &qualitativeResult, storm::storage::BitVector const &maybeStates, storage::ExplicitGameStrategyPair &strategyPair, storm::dd::Odd const &odd, ExplicitQuantitativeResult< ValueType > const *startingQuantitativeResult=nullptr, storage::ExplicitGameStrategyPair const *startingStrategyPair=nullptr, boost::optional< PreviousExplicitResult< ValueType > > const &previousResult=boost::none)
template<typename ValueType>
void	postProcessStrategies (storm::OptimizationDirection const &player1Direction, storage::ExplicitGameStrategyPair &minStrategyPair, storage::ExplicitGameStrategyPair &maxStrategyPair, std::vector< uint64_t > const &player1Groups, std::vector< uint64_t > const &player2Groups, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::BitVector const &constraintStates, storm::storage::BitVector const &targetStates, ExplicitQualitativeGameResultMinMax const &qualitativeResult, bool redirectPlayer1, bool redirectPlayer2, bool sanityCheck)
template<typename ValueType>
void	postProcessStrategies (uint64_t iteration, storm::OptimizationDirection const &player1Direction, storage::ExplicitGameStrategyPair &minStrategyPair, storage::ExplicitGameStrategyPair &maxStrategyPair, std::vector< uint64_t > const &player1Groups, std::vector< uint64_t > const &player2Groups, storm::storage::SparseMatrix< ValueType > const &transitionMatrix, storm::storage::BitVector const &initialStates, storm::storage::BitVector const &constraintStates, storm::storage::BitVector const &targetStates, ExplicitQuantitativeResultMinMax< ValueType > const &quantitativeResult, bool redirectPlayer1, bool redirectPlayer2, bool sanityCheck)
template<storm::dd::DdType Type>
bool	checkQualitativeStrategies (bool prob0, SymbolicQualitativeGameResult< Type > const &result, storm::dd::Bdd< Type > const &targetStates)
template<storm::dd::DdType Type>
bool	checkQualitativeStrategies (SymbolicQualitativeGameResultMinMax< Type > const &qualitativeResult, storm::dd::Bdd< Type > const &targetStates)

Variables
template<typename ModelType>
const std::string	BisimulationAbstractionRefinementModelChecker< ModelType >::name = "bisimulation-based astraction refinement"

Function Documentation

checkForResultAfterQualitativeCheck() [1/4]

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

std::unique_ptr< storm::modelchecker::CheckResult > storm::gbar::modelchecker::checkForResultAfterQualitativeCheck	(	storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &	checkTask,
		storm::dd::Bdd< Type > const &	initialStates,
		SymbolicQualitativeGameResultMinMax< Type > const &	qualitativeResult )

Definition at line 218 of file GameBasedMdpModelChecker.cpp.

checkForResultAfterQualitativeCheck() [2/4]

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

std::unique_ptr< storm::modelchecker::CheckResult > storm::gbar::modelchecker::checkForResultAfterQualitativeCheck	(	storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &	checkTask,
		storm::OptimizationDirection	player2Direction,
		storm::dd::Bdd< Type > const &	initialStates,
		storm::dd::Bdd< Type > const &	prob0,
		storm::dd::Bdd< Type > const &	prob1 )

Definition at line 171 of file GameBasedMdpModelChecker.cpp.

checkForResultAfterQualitativeCheck() [3/4]

template<typename ValueType>

std::unique_ptr< storm::modelchecker::CheckResult > storm::gbar::modelchecker::checkForResultAfterQualitativeCheck	(	storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &	checkTask,
		storm::OptimizationDirection	player2Direction,
		storm::storage::BitVector const &	initialStates,
		storm::storage::BitVector const &	prob0,
		storm::storage::BitVector const &	prob1 )

Definition at line 237 of file GameBasedMdpModelChecker.cpp.

checkForResultAfterQualitativeCheck() [4/4]

template<typename ValueType>

std::unique_ptr< storm::modelchecker::CheckResult > storm::gbar::modelchecker::checkForResultAfterQualitativeCheck	(	storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &	checkTask,
		storm::storage::BitVector const &	initialStates,
		ExplicitQualitativeGameResultMinMax const &	qualitativeResult )

Definition at line 284 of file GameBasedMdpModelChecker.cpp.

checkForResultAfterQuantitativeCheck() [1/2]

template<typename ValueType>

std::unique_ptr< storm::modelchecker::CheckResult > storm::gbar::modelchecker::checkForResultAfterQuantitativeCheck	(	storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &	checkTask,
		storm::OptimizationDirection const &	player2Direction,
		std::pair< ValueType, ValueType > const &	initialValueRange )

Definition at line 303 of file GameBasedMdpModelChecker.cpp.

checkForResultAfterQuantitativeCheck() [2/2]

template<typename ValueType>

std::unique_ptr< storm::modelchecker::CheckResult > storm::gbar::modelchecker::checkForResultAfterQuantitativeCheck	(	ValueType const &	minValue,
		ValueType const &	maxValue,
		storm::utility::ConstantsComparator< ValueType > const &	comparator )

Definition at line 348 of file GameBasedMdpModelChecker.cpp.

checkQualitativeStrategies() [1/2]

template<storm::dd::DdType Type>

bool storm::gbar::modelchecker::checkQualitativeStrategies	(	bool	prob0,
		SymbolicQualitativeGameResult< Type > const &	result,
		storm::dd::Bdd< Type > const &	targetStates )

Definition at line 1605 of file GameBasedMdpModelChecker.cpp.

checkQualitativeStrategies() [2/2]

template<storm::dd::DdType Type>

bool storm::gbar::modelchecker::checkQualitativeStrategies	(	SymbolicQualitativeGameResultMinMax< Type > const &	qualitativeResult,
		storm::dd::Bdd< Type > const &	targetStates )

Definition at line 1621 of file GameBasedMdpModelChecker.cpp.

computeQuantitativeResult() [1/2]

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

SymbolicQuantitativeGameResult< Type, ValueType > storm::gbar::modelchecker::computeQuantitativeResult	(	Environment const &	env,
		storm::OptimizationDirection	player1Direction,
		storm::OptimizationDirection	player2Direction,
		storm::gbar::abstraction::MenuGame< Type, ValueType > const &	game,
		SymbolicQualitativeGameResultMinMax< Type > const &	qualitativeResult,
		storm::dd::Add< Type, ValueType > const &	initialStatesAdd,
		storm::dd::Bdd< Type > const &	maybeStates,
		boost::optional< SymbolicQuantitativeGameResult< Type, ValueType > > const &	startInfo = boost::none )

Definition at line 400 of file GameBasedMdpModelChecker.cpp.

computeQuantitativeResult() [2/2]

template<typename ValueType>

ExplicitQuantitativeResult< ValueType > storm::gbar::modelchecker::computeQuantitativeResult	(	Environment const &	env,
		storm::OptimizationDirection	player1Direction,
		storm::OptimizationDirection	player2Direction,
		storm::storage::SparseMatrix< ValueType > const &	transitionMatrix,
		std::vector< uint64_t > const &	player1Groups,
		ExplicitQualitativeGameResultMinMax const &	qualitativeResult,
		storm::storage::BitVector const &	maybeStates,
		storage::ExplicitGameStrategyPair &	strategyPair,
		storm::dd::Odd const &	odd,
		ExplicitQuantitativeResult< ValueType > const *	startingQuantitativeResult = nullptr,
		storage::ExplicitGameStrategyPair const *	startingStrategyPair = nullptr,
		boost::optional< PreviousExplicitResult< ValueType > > const &	previousResult = boost::none )

Definition at line 470 of file GameBasedMdpModelChecker.cpp.

postProcessStrategies() [1/2]

template<typename ValueType>

void storm::gbar::modelchecker::postProcessStrategies	(	storm::OptimizationDirection const &	player1Direction,
		storage::ExplicitGameStrategyPair &	minStrategyPair,
		storage::ExplicitGameStrategyPair &	maxStrategyPair,
		std::vector< uint64_t > const &	player1Groups,
		std::vector< uint64_t > const &	player2Groups,
		storm::storage::SparseMatrix< ValueType > const &	transitionMatrix,
		storm::storage::BitVector const &	constraintStates,
		storm::storage::BitVector const &	targetStates,
		ExplicitQualitativeGameResultMinMax const &	qualitativeResult,
		bool	redirectPlayer1,
		bool	redirectPlayer2,
		bool	sanityCheck )

Definition at line 874 of file GameBasedMdpModelChecker.cpp.

postProcessStrategies() [2/2]

template<typename ValueType>

void storm::gbar::modelchecker::postProcessStrategies	(	uint64_t	iteration,
		storm::OptimizationDirection const &	player1Direction,
		storage::ExplicitGameStrategyPair &	minStrategyPair,
		storage::ExplicitGameStrategyPair &	maxStrategyPair,
		std::vector< uint64_t > const &	player1Groups,
		std::vector< uint64_t > const &	player2Groups,
		storm::storage::SparseMatrix< ValueType > const &	transitionMatrix,
		storm::storage::BitVector const &	initialStates,
		storm::storage::BitVector const &	constraintStates,
		storm::storage::BitVector const &	targetStates,
		ExplicitQuantitativeResultMinMax< ValueType > const &	quantitativeResult,
		bool	redirectPlayer1,
		bool	redirectPlayer2,
		bool	sanityCheck )

Definition at line 1185 of file GameBasedMdpModelChecker.cpp.

solveMaybeStates()

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

SymbolicQuantitativeGameResult< Type, ValueType > storm::gbar::modelchecker::solveMaybeStates	(	Environment const &	env,
		storm::OptimizationDirection const &	player1Direction,
		storm::OptimizationDirection const &	player2Direction,
		storm::gbar::abstraction::MenuGame< Type, ValueType > const &	game,
		storm::dd::Bdd< Type > const &	maybeStates,
		storm::dd::Bdd< Type > const &	prob1States,
		boost::optional< SymbolicQuantitativeGameResult< Type, ValueType > > const &	startInfo = boost::none )

Definition at line 362 of file GameBasedMdpModelChecker.cpp.

Variable Documentation

BisimulationAbstractionRefinementModelChecker< ModelType >::name

template<typename ModelType>

const std::string storm::gbar::modelchecker::BisimulationAbstractionRefinementModelChecker< ModelType >::name = "bisimulation-based astraction refinement"

Definition at line 22 of file BisimulationAbstractionRefinementModelChecker.cpp.