Storm 1.14.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
storm::modelchecker::SymbolicPropositionalModelChecker< ModelType > Class Template Reference

#include <SymbolicPropositionalModelChecker.h>

Inheritance diagram for storm::modelchecker::SymbolicPropositionalModelChecker< ModelType >:
Inheritance graph
[legend]
Collaboration diagram for storm::modelchecker::SymbolicPropositionalModelChecker< ModelType >:
Collaboration graph
[legend]

Public Types

typedef ModelType::ValueType ValueType
Public Types inherited from storm::modelchecker::AbstractModelChecker< ModelType >
typedef ModelType::ValueType ValueType
using SolutionType = typename GetSolutionType<ValueType, void>::type

Public Member Functions

 SymbolicPropositionalModelChecker (ModelType const &model)
virtual bool canHandle (CheckTask< storm::logic::Formula, ValueType > const &checkTask) const override
virtual std::unique_ptr< CheckResult > checkBooleanLiteralFormula (Environment const &env, CheckTask< storm::logic::BooleanLiteralFormula, ValueType > const &checkTask) override
virtual std::unique_ptr< CheckResult > checkAtomicLabelFormula (Environment const &env, CheckTask< storm::logic::AtomicLabelFormula, ValueType > const &checkTask) override
virtual std::unique_ptr< CheckResult > checkAtomicExpressionFormula (Environment const &env, CheckTask< storm::logic::AtomicExpressionFormula, 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 > computeDiscountedCumulativeRewards (Environment const &env, CheckTask< storm::logic::DiscountedCumulativeRewardFormula, SolutionType > const &checkTask)
virtual std::unique_ptr< CheckResult > computeDiscountedTotalRewards (Environment const &env, CheckTask< storm::logic::DiscountedTotalRewardFormula, 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)

Static Public Attributes

static const storm::dd::DdType DdType = ModelType::DdType

Protected Member Functions

virtual ModelType const & getModel () const
 Retrieves the model associated with this model checker instance.

Detailed Description

template<typename ModelType>
class storm::modelchecker::SymbolicPropositionalModelChecker< ModelType >

Definition at line 18 of file SymbolicPropositionalModelChecker.h.

Member Typedef Documentation

◆ ValueType

template<typename ModelType>
typedef ModelType::ValueType storm::modelchecker::SymbolicPropositionalModelChecker< ModelType >::ValueType

Definition at line 20 of file SymbolicPropositionalModelChecker.h.

Constructor & Destructor Documentation

◆ SymbolicPropositionalModelChecker()

template<typename ModelType>
storm::modelchecker::SymbolicPropositionalModelChecker< ModelType >::SymbolicPropositionalModelChecker ( ModelType const & model)
explicit

Definition at line 19 of file SymbolicPropositionalModelChecker.cpp.

Member Function Documentation

◆ canHandle()

template<typename ModelType>
bool storm::modelchecker::SymbolicPropositionalModelChecker< ModelType >::canHandle ( CheckTask< storm::logic::Formula, ValueType > const & checkTask) const
overridevirtual

Reimplemented in storm::modelchecker::HybridCtmcCslModelChecker< ModelType >, storm::modelchecker::HybridDtmcPrctlModelChecker< ModelType >, storm::modelchecker::HybridMarkovAutomatonCslModelChecker< ModelType >, storm::modelchecker::HybridMdpPrctlModelChecker< ModelType >, storm::modelchecker::SymbolicDtmcPrctlModelChecker< ModelType >, and storm::modelchecker::SymbolicMdpPrctlModelChecker< ModelType >.

Definition at line 24 of file SymbolicPropositionalModelChecker.cpp.

◆ checkAtomicExpressionFormula()

template<typename ModelType>
std::unique_ptr< CheckResult > storm::modelchecker::SymbolicPropositionalModelChecker< ModelType >::checkAtomicExpressionFormula ( Environment const & env,
CheckTask< storm::logic::AtomicExpressionFormula, ValueType > const & checkTask )
overridevirtual

Definition at line 50 of file SymbolicPropositionalModelChecker.cpp.

◆ checkAtomicLabelFormula()

template<typename ModelType>
std::unique_ptr< CheckResult > storm::modelchecker::SymbolicPropositionalModelChecker< ModelType >::checkAtomicLabelFormula ( Environment const & env,
CheckTask< storm::logic::AtomicLabelFormula, ValueType > const & checkTask )
overridevirtual

Definition at line 41 of file SymbolicPropositionalModelChecker.cpp.

◆ checkBooleanLiteralFormula()

template<typename ModelType>
std::unique_ptr< CheckResult > storm::modelchecker::SymbolicPropositionalModelChecker< ModelType >::checkBooleanLiteralFormula ( Environment const & env,
CheckTask< storm::logic::BooleanLiteralFormula, ValueType > const & checkTask )
overridevirtual

Definition at line 30 of file SymbolicPropositionalModelChecker.cpp.

◆ getModel()

template<typename ModelType>
ModelType const & storm::modelchecker::SymbolicPropositionalModelChecker< ModelType >::getModel ( ) const
protectedvirtual

Retrieves the model associated with this model checker instance.

Returns
The model associated with this model checker instance.

Definition at line 57 of file SymbolicPropositionalModelChecker.cpp.

Member Data Documentation

◆ DdType

template<typename ModelType>
const storm::dd::DdType storm::modelchecker::SymbolicPropositionalModelChecker< ModelType >::DdType = ModelType::DdType
static

Definition at line 21 of file SymbolicPropositionalModelChecker.h.

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