storm::gbar::modelchecker Namespace Reference

Namespaces
namespace	detail

Classes
class	AbstractAbstractionRefinementModelChecker
class	BisimulationAbstractionRefinementModelChecker
class	ExplicitGameExporter
class	GameBasedMdpModelChecker
struct	PreviousExplicitResult
class	ExplicitQuantitativeResult
class	ExplicitQuantitativeResultMinMax
class	SymbolicQuantitativeGameResult
class	SymbolicQuantitativeGameResultMinMax
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 (Environment const &env, 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 210 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 163 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 229 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 276 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 295 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 340 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 1598 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 1614 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 392 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 462 of file GameBasedMdpModelChecker.cpp.

postProcessStrategies() [1/2]

template<typename ValueType>

void storm::gbar::modelchecker::postProcessStrategies	(	Environment const &	env,
		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 1174 of file GameBasedMdpModelChecker.cpp.

postProcessStrategies() [2/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 863 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 354 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.