storm::gbar::modelchecker::GameBasedMdpModelChecker< Type, ModelType > Class Template Reference

#include <GameBasedMdpModelChecker.h>

Inheritance diagram for storm::gbar::modelchecker::GameBasedMdpModelChecker< Type, ModelType >:

Collaboration diagram for storm::gbar::modelchecker::GameBasedMdpModelChecker< Type, ModelType >:

Public Types
typedef ModelType::ValueType	ValueType
Public Types inherited from storm::modelchecker::AbstractModelChecker< ModelType >
typedef ModelType::ValueType	ValueType
using	SolutionType = typename std::conditional< std::is_same_v< ValueType, storm::Interval >, double, ValueType >::type

Public Member Functions
	GameBasedMdpModelChecker (storm::storage::SymbolicModelDescription const &model, GameBasedMdpModelCheckerOptions const &options=GameBasedMdpModelCheckerOptions(), std::shared_ptr< storm::utility::solver::SmtSolverFactory > const &smtSolverFactory=std::make_shared< storm::utility::solver::MathsatSmtSolverFactory >())
	Constructs a model checker whose underlying model is implicitly given by the provided program.
virtual bool	canHandle (storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &checkTask) const override
	Overridden methods from super class.
virtual std::unique_ptr< storm::modelchecker::CheckResult >	computeUntilProbabilities (Environment const &env, storm::modelchecker::CheckTask< storm::logic::UntilFormula, ValueType > const &checkTask) override
virtual std::unique_ptr< storm::modelchecker::CheckResult >	computeReachabilityProbabilities (Environment const &env, storm::modelchecker::CheckTask< storm::logic::EventuallyFormula, ValueType > const &checkTask) override
Public Member Functions inherited from storm::modelchecker::AbstractModelChecker< ModelType >
virtual	~AbstractModelChecker ()
virtual std::string	getClassName () const
	Returns the name of the model checker class (e.g., for display in error messages).
virtual bool	canHandle (CheckTask< storm::logic::Formula, SolutionType > const &checkTask) const =0
	Determines whether the model checker can handle the given verification task.
virtual std::unique_ptr< CheckResult >	check (Environment const &env, CheckTask< storm::logic::Formula, SolutionType > const &checkTask)
	Checks the provided formula.
std::unique_ptr< CheckResult >	check (CheckTask< storm::logic::Formula, SolutionType > const &checkTask)
	Checks the provided formula with the default environment.
virtual std::unique_ptr< CheckResult >	computeProbabilities (Environment const &env, CheckTask< storm::logic::Formula, SolutionType > const &checkTask)
virtual std::unique_ptr< CheckResult >	computeConditionalProbabilities (Environment const &env, CheckTask< storm::logic::ConditionalFormula, SolutionType > const &checkTask)
virtual std::unique_ptr< CheckResult >	computeBoundedUntilProbabilities (Environment const &env, CheckTask< storm::logic::BoundedUntilFormula, SolutionType > const &checkTask)
virtual std::unique_ptr< CheckResult >	computeReachabilityProbabilities (Environment const &env, CheckTask< storm::logic::EventuallyFormula, SolutionType > const &checkTask)
virtual std::unique_ptr< CheckResult >	computeGloballyProbabilities (Environment const &env, CheckTask< storm::logic::GloballyFormula, SolutionType > const &checkTask)
virtual std::unique_ptr< CheckResult >	computeNextProbabilities (Environment const &env, CheckTask< storm::logic::NextFormula, SolutionType > const &checkTask)
virtual std::unique_ptr< CheckResult >	computeUntilProbabilities (Environment const &env, CheckTask< storm::logic::UntilFormula, SolutionType > const &checkTask)
virtual std::unique_ptr< CheckResult >	computeHOAPathProbabilities (Environment const &env, CheckTask< storm::logic::HOAPathFormula, SolutionType > const &checkTask)
virtual std::unique_ptr< CheckResult >	computeLTLProbabilities (Environment const &env, CheckTask< storm::logic::PathFormula, SolutionType > const &checkTask)
std::unique_ptr< CheckResult >	computeStateFormulaProbabilities (Environment const &env, CheckTask< storm::logic::Formula, SolutionType > const &checkTask)
virtual std::unique_ptr< CheckResult >	computeRewards (Environment const &env, CheckTask< storm::logic::Formula, SolutionType > const &checkTask)
virtual std::unique_ptr< CheckResult >	computeConditionalRewards (Environment const &env, CheckTask< storm::logic::ConditionalFormula, SolutionType > const &checkTask)
virtual std::unique_ptr< CheckResult >	computeCumulativeRewards (Environment const &env, CheckTask< storm::logic::CumulativeRewardFormula, SolutionType > const &checkTask)
virtual std::unique_ptr< CheckResult >	computeInstantaneousRewards (Environment const &env, CheckTask< storm::logic::InstantaneousRewardFormula, SolutionType > const &checkTask)
virtual std::unique_ptr< CheckResult >	computeReachabilityRewards (Environment const &env, CheckTask< storm::logic::EventuallyFormula, SolutionType > const &checkTask)
virtual std::unique_ptr< CheckResult >	computeTotalRewards (Environment const &env, CheckTask< storm::logic::TotalRewardFormula, SolutionType > const &checkTask)
virtual std::unique_ptr< CheckResult >	computeLongRunAverageRewards (Environment const &env, CheckTask< storm::logic::LongRunAverageRewardFormula, SolutionType > const &checkTask)
virtual std::unique_ptr< CheckResult >	computeLongRunAverageProbabilities (Environment const &env, CheckTask< storm::logic::StateFormula, SolutionType > const &checkTask)
virtual std::unique_ptr< CheckResult >	computeTimes (Environment const &env, CheckTask< storm::logic::Formula, SolutionType > const &checkTask)
virtual std::unique_ptr< CheckResult >	computeReachabilityTimes (Environment const &env, CheckTask< storm::logic::EventuallyFormula, SolutionType > const &checkTask)
virtual std::unique_ptr< CheckResult >	checkStateFormula (Environment const &env, CheckTask< storm::logic::StateFormula, SolutionType > const &checkTask)
virtual std::unique_ptr< CheckResult >	checkAtomicExpressionFormula (Environment const &env, CheckTask< storm::logic::AtomicExpressionFormula, SolutionType > const &checkTask)
virtual std::unique_ptr< CheckResult >	checkAtomicLabelFormula (Environment const &env, CheckTask< storm::logic::AtomicLabelFormula, SolutionType > const &checkTask)
virtual std::unique_ptr< CheckResult >	checkBinaryBooleanStateFormula (Environment const &env, CheckTask< storm::logic::BinaryBooleanStateFormula, SolutionType > const &checkTask)
virtual std::unique_ptr< CheckResult >	checkBooleanLiteralFormula (Environment const &env, CheckTask< storm::logic::BooleanLiteralFormula, SolutionType > const &checkTask)
virtual std::unique_ptr< CheckResult >	checkProbabilityOperatorFormula (Environment const &env, CheckTask< storm::logic::ProbabilityOperatorFormula, SolutionType > const &checkTask)
virtual std::unique_ptr< CheckResult >	checkRewardOperatorFormula (Environment const &env, CheckTask< storm::logic::RewardOperatorFormula, SolutionType > const &checkTask)
virtual std::unique_ptr< CheckResult >	checkTimeOperatorFormula (Environment const &env, CheckTask< storm::logic::TimeOperatorFormula, SolutionType > const &checkTask)
virtual std::unique_ptr< CheckResult >	checkLongRunAverageOperatorFormula (Environment const &env, CheckTask< storm::logic::LongRunAverageOperatorFormula, SolutionType > const &checkTask)
virtual std::unique_ptr< CheckResult >	checkUnaryBooleanStateFormula (Environment const &env, CheckTask< storm::logic::UnaryBooleanStateFormula, SolutionType > const &checkTask)
virtual std::unique_ptr< CheckResult >	checkMultiObjectiveFormula (Environment const &env, CheckTask< storm::logic::MultiObjectiveFormula, SolutionType > const &checkTask)
virtual std::unique_ptr< CheckResult >	checkQuantileFormula (Environment const &env, CheckTask< storm::logic::QuantileFormula, SolutionType > const &checkTask)
virtual std::unique_ptr< CheckResult >	checkLexObjectiveFormula (Environment const &env, CheckTask< storm::logic::MultiObjectiveFormula, SolutionType > const &checkTask)
virtual std::unique_ptr< CheckResult >	checkGameFormula (Environment const &env, CheckTask< storm::logic::GameFormula, SolutionType > const &checkTask)

Detailed Description

template<storm::dd::DdType Type, typename ModelType>
class storm::gbar::modelchecker::GameBasedMdpModelChecker< Type, ModelType >

Definition at line 94 of file GameBasedMdpModelChecker.h.

Member Typedef Documentation

ValueType

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

typedef ModelType::ValueType storm::gbar::modelchecker::GameBasedMdpModelChecker< Type, ModelType >::ValueType

Definition at line 96 of file GameBasedMdpModelChecker.h.

Constructor & Destructor Documentation

GameBasedMdpModelChecker()

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

storm::gbar::modelchecker::GameBasedMdpModelChecker< Type, ModelType >::GameBasedMdpModelChecker ( storm::storage::SymbolicModelDescription const &  model, GameBasedMdpModelCheckerOptions const &  options = GameBasedMdpModelCheckerOptions(), std::shared_ptr< storm::utility::solver::SmtSolverFactory > const &  smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>()  )

explicit

Constructs a model checker whose underlying model is implicitly given by the provided program.

All verification calls will be answererd with respect to this model.

Parameters

model	The model description that (symbolically) specifies the model to check.
options	Additional options for the abstraction-refinement process.
smtSolverFactory	A factory used to create SMT solver when necessary.

Definition at line 53 of file GameBasedMdpModelChecker.cpp.

Member Function Documentation

canHandle()

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

bool storm::gbar::modelchecker::GameBasedMdpModelChecker< Type, ModelType >::canHandle ( storm::modelchecker::CheckTask< storm::logic::Formula, ValueType > const &  checkTask ) const

overridevirtual

Overridden methods from super class.

Definition at line 116 of file GameBasedMdpModelChecker.cpp.

computeReachabilityProbabilities()

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

std::unique_ptr< storm::modelchecker::CheckResult > storm::gbar::modelchecker::GameBasedMdpModelChecker< Type, ModelType >::computeReachabilityProbabilities ( Environment const &  env, storm::modelchecker::CheckTask< storm::logic::EventuallyFormula, ValueType > const &  checkTask  )

overridevirtual

Definition at line 148 of file GameBasedMdpModelChecker.cpp.

computeUntilProbabilities()

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

std::unique_ptr< storm::modelchecker::CheckResult > storm::gbar::modelchecker::GameBasedMdpModelChecker< Type, ModelType >::computeUntilProbabilities ( Environment const &  env, storm::modelchecker::CheckTask< storm::logic::UntilFormula, ValueType > const &  checkTask  )

overridevirtual

Definition at line 123 of file GameBasedMdpModelChecker.cpp.

---

The documentation for this class was generated from the following files:

• src/storm-gamebased-ar/modelchecker/abstraction/GameBasedMdpModelChecker.h
• src/storm-gamebased-ar/modelchecker/abstraction/GameBasedMdpModelChecker.cpp