#include <SparsePropositionalModelChecker.h>

Inheritance diagram for storm::modelchecker::SparsePropositionalModelChecker< SparseModelType >:

[legend]

Collaboration diagram for storm::modelchecker::SparsePropositionalModelChecker< SparseModelType >:

Public Types
typedef SparseModelType::ValueType	ValueType
typedef SparseModelType::RewardModelType	RewardModelType
using	SolutionType = IntervalBaseType<ValueType>
Public Types inherited from storm::modelchecker::AbstractModelChecker< SparseModelType >
typedef SparseModelType::ValueType	ValueType
using	SolutionType

Public Member Functions
	SparsePropositionalModelChecker (SparseModelType const &model)
virtual bool	canHandle (CheckTask< storm::logic::Formula, SolutionType > const &checkTask) const override
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 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.
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)

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 11 of file SparsePropositionalModelChecker.h.