1#ifndef STORM_MODELCHECKER_SYMBOLICPROPOSITIONALMODELCHECKER_H_
2#define STORM_MODELCHECKER_SYMBOLICPROPOSITIONALMODELCHECKER_H_
11template<storm::dd::DdType Type,
typename ValueType>
16namespace modelchecker {
18template<
typename ModelType>
41 virtual ModelType
const&
getModel()
const;
45 ModelType
const& model;
virtual bool canHandle(CheckTask< storm::logic::Formula, ValueType > const &checkTask) const override
ModelType::ValueType ValueType
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 ModelType const & getModel() const
Retrieves the model associated with this model checker instance.
static const storm::dd::DdType DdType
virtual std::unique_ptr< CheckResult > checkAtomicExpressionFormula(Environment const &env, CheckTask< storm::logic::AtomicExpressionFormula, ValueType > const &checkTask) override