GameBasedMdpModelChecker.cpp File Reference

#include "storm-gamebased-ar/modelchecker/abstraction/GameBasedMdpModelChecker.h"
#include "storm-gamebased-ar/abstraction/ExplicitQualitativeGameResultMinMax.h"
#include "storm-gamebased-ar/abstraction/ExplicitQuantitativeResultMinMax.h"
#include "storm-gamebased-ar/abstraction/MenuGameRefiner.h"
#include "storm-gamebased-ar/abstraction/jani/JaniMenuGameAbstractor.h"
#include "storm-gamebased-ar/abstraction/prism/PrismMenuGameAbstractor.h"
#include "storm/environment/Environment.h"
#include "storm/exceptions/InvalidModelException.h"
#include "storm/exceptions/InvalidPropertyException.h"
#include "storm/exceptions/NotSupportedException.h"
#include "storm/io/file.h"
#include "storm/logic/FragmentSpecification.h"
#include "storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h"
#include "storm/modelchecker/results/CheckResult.h"
#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
#include "storm/models/symbolic/Dtmc.h"
#include "storm/models/symbolic/Mdp.h"
#include "storm/models/symbolic/StandardRewardModel.h"
#include "storm/settings/SettingsManager.h"
#include "storm/settings/modules/CoreSettings.h"
#include "storm/settings/modules/GeneralSettings.h"
#include "storm/solver/StandardGameSolver.h"
#include "storm/solver/SymbolicGameSolver.h"
#include "storm/storage/ExplicitGameStrategyPair.h"
#include "storm/storage/dd/DdManager.h"
#include "storm/storage/expressions/ExpressionManager.h"
#include "storm/storage/expressions/VariableSetPredicateSplitter.h"
#include "storm/storage/jani/Automaton.h"
#include "storm/storage/jani/AutomatonComposition.h"
#include "storm/storage/jani/Edge.h"
#include "storm/storage/jani/EdgeDestination.h"
#include "storm/storage/jani/Location.h"
#include "storm/storage/jani/Model.h"
#include "storm/storage/jani/ParallelComposition.h"
#include "storm/storage/jani/visitor/CompositionInformationVisitor.h"
#include "storm/utility/macros.h"
#include "storm/utility/prism.h"
#include "storm/utility/vector.h"

Include dependency graph for GameBasedMdpModelChecker.cpp:

Go to the source code of this file.

Classes
class	storm::gbar::modelchecker::ExplicitGameExporter< ValueType >
struct	storm::gbar::modelchecker::PreviousExplicitResult< ValueType >
class	storm::gbar::modelchecker::ExplicitQuantitativeResult< ValueType >
class	storm::gbar::modelchecker::ExplicitQuantitativeResultMinMax< ValueType >
class	storm::gbar::modelchecker::SymbolicQuantitativeGameResult< Type, ValueType >
class	storm::gbar::modelchecker::SymbolicQuantitativeGameResultMinMax< Type, ValueType >
class	storm::gbar::modelchecker::ExplicitGameStrategyPair

Namespaces
namespace	storm
namespace	storm::gbar
namespace	storm::gbar::modelchecker

Functions
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)
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)
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)
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)
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)
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)
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)
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)
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)
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)
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)
template<storm::dd::DdType Type>
bool	storm::gbar::modelchecker::checkQualitativeStrategies (bool prob0, SymbolicQualitativeGameResult< Type > const &result, storm::dd::Bdd< Type > const &targetStates)
template<storm::dd::DdType Type>
bool	storm::gbar::modelchecker::checkQualitativeStrategies (SymbolicQualitativeGameResultMinMax< Type > const &qualitativeResult, storm::dd::Bdd< Type > const &targetStates)