Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
Namespaces | Classes | Functions
storm::gbar::modelchecker Namespace Reference

Namespaces

namespace  detail
 

Classes

class  AbstractAbstractionRefinementModelChecker
 
class  BisimulationAbstractionRefinementModelChecker
 
class  ExplicitGameExporter
 
class  GameBasedMdpModelChecker
 
struct  GameBasedMdpModelCheckerOptions
 

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)
 

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.