Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
Public Types | Public Member Functions | Static Public Attributes | Protected Member Functions | List of all members
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 std::conditional< std::is_same_v< ValueType, storm::Interval >, double, ValueType >::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 > 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 19 of file SymbolicPropositionalModelChecker.h.

Member Typedef Documentation

◆ ValueType

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

Definition at line 21 of file SymbolicPropositionalModelChecker.h.

Constructor & Destructor Documentation

◆ SymbolicPropositionalModelChecker()

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

Definition at line 24 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::HybridMarkovAutomatonCslModelChecker< ModelType >, storm::modelchecker::HybridDtmcPrctlModelChecker< ModelType >, storm::modelchecker::HybridMdpPrctlModelChecker< ModelType >, storm::modelchecker::SymbolicDtmcPrctlModelChecker< ModelType >, and storm::modelchecker::SymbolicMdpPrctlModelChecker< ModelType >.

Definition at line 29 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 55 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 46 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 35 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 62 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 22 of file SymbolicPropositionalModelChecker.h.

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