Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
Public Types | Public Member Functions | Protected Member Functions | List of all members
storm::modelchecker::SparsePropositionalModelChecker< SparseModelType > Class Template Reference

#include <SparsePropositionalModelChecker.h>

Inheritance diagram for storm::modelchecker::SparsePropositionalModelChecker< SparseModelType >:
Inheritance graph
[legend]
Collaboration diagram for storm::modelchecker::SparsePropositionalModelChecker< SparseModelType >:
Collaboration graph
[legend]

Public Types

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

Public Member Functions

 SparsePropositionalModelChecker (SparseModelType const &model)
 
virtual bool canHandle (CheckTask< storm::logic::Formula, SolutionType > const &checkTask) const override
 Determines whether the model checker can handle the given verification task.
 
virtual std::unique_ptr< CheckResult > checkBooleanLiteralFormula (Environment const &env, CheckTask< storm::logic::BooleanLiteralFormula, SolutionType > const &checkTask) override
 
virtual std::unique_ptr< CheckResult > checkAtomicLabelFormula (Environment const &env, CheckTask< storm::logic::AtomicLabelFormula, SolutionType > const &checkTask) override
 
- Public Member Functions inherited from storm::modelchecker::AbstractModelChecker< SparseModelType >
virtual ~AbstractModelChecker ()
 
virtual std::string getClassName () const
 Returns the name of the model checker class (e.g., for display in error messages).
 
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 > checkBinaryBooleanStateFormula (Environment const &env, CheckTask< storm::logic::BinaryBooleanStateFormula, 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)
 

Protected Member Functions

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

Detailed Description

template<typename SparseModelType>
class storm::modelchecker::SparsePropositionalModelChecker< SparseModelType >

Definition at line 10 of file SparsePropositionalModelChecker.h.

Member Typedef Documentation

◆ RewardModelType

template<typename SparseModelType >
typedef SparseModelType::RewardModelType storm::modelchecker::SparsePropositionalModelChecker< SparseModelType >::RewardModelType

Definition at line 13 of file SparsePropositionalModelChecker.h.

◆ SolutionType

template<typename SparseModelType >
using storm::modelchecker::SparsePropositionalModelChecker< SparseModelType >::SolutionType = typename std::conditional<std::is_same_v<ValueType, storm::Interval>, double, ValueType>::type

Definition at line 14 of file SparsePropositionalModelChecker.h.

◆ ValueType

template<typename SparseModelType >
typedef SparseModelType::ValueType storm::modelchecker::SparsePropositionalModelChecker< SparseModelType >::ValueType

Definition at line 12 of file SparsePropositionalModelChecker.h.

Constructor & Destructor Documentation

◆ SparsePropositionalModelChecker()

template<typename SparseModelType >
storm::modelchecker::SparsePropositionalModelChecker< SparseModelType >::SparsePropositionalModelChecker ( SparseModelType const &  model)
explicit

Definition at line 23 of file SparsePropositionalModelChecker.cpp.

Member Function Documentation

◆ canHandle()

template<typename SparseModelType >
bool storm::modelchecker::SparsePropositionalModelChecker< SparseModelType >::canHandle ( CheckTask< storm::logic::Formula, SolutionType > const &  checkTask) const
overridevirtual

Determines whether the model checker can handle the given verification task.

If this method returns false, the task must not be checked using this model checker.

Parameters
checkTaskThe task for which to check whether the model checker can handle it.
Returns
True iff the model checker can check the given task.

Implements storm::modelchecker::AbstractModelChecker< SparseModelType >.

Reimplemented in storm::modelchecker::SparseMdpPrctlModelChecker< SparseMdpModelType >.

Definition at line 28 of file SparsePropositionalModelChecker.cpp.

◆ checkAtomicLabelFormula()

template<typename SparseModelType >
std::unique_ptr< CheckResult > storm::modelchecker::SparsePropositionalModelChecker< SparseModelType >::checkAtomicLabelFormula ( Environment const &  env,
CheckTask< storm::logic::AtomicLabelFormula, SolutionType > const &  checkTask 
)
overridevirtual

Reimplemented from storm::modelchecker::AbstractModelChecker< SparseModelType >.

Definition at line 45 of file SparsePropositionalModelChecker.cpp.

◆ checkBooleanLiteralFormula()

template<typename SparseModelType >
std::unique_ptr< CheckResult > storm::modelchecker::SparsePropositionalModelChecker< SparseModelType >::checkBooleanLiteralFormula ( Environment const &  env,
CheckTask< storm::logic::BooleanLiteralFormula, SolutionType > const &  checkTask 
)
overridevirtual

Reimplemented from storm::modelchecker::AbstractModelChecker< SparseModelType >.

Definition at line 34 of file SparsePropositionalModelChecker.cpp.

◆ getModel()

template<typename SparseModelType >
SparseModelType const & storm::modelchecker::SparsePropositionalModelChecker< SparseModelType >::getModel ( ) const
protected

Retrieves the model associated with this model checker instance.

Returns
The model associated with this model checker instance.

Definition at line 54 of file SparsePropositionalModelChecker.cpp.

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