Storm
A Modern Probabilistic Model Checker
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
SymbolicPropositionalModelChecker.h
Go to the documentation of this file.
1#ifndef STORM_MODELCHECKER_SYMBOLICPROPOSITIONALMODELCHECKER_H_
2#define STORM_MODELCHECKER_SYMBOLICPROPOSITIONALMODELCHECKER_H_
3
5
7
8namespace storm {
9namespace models {
10namespace symbolic {
11template<storm::dd::DdType Type, typename ValueType>
12class Model;
13}
14} // namespace models
15
16namespace modelchecker {
17
18template<typename ModelType>
20 public:
21 typedef typename ModelType::ValueType ValueType;
22 static const storm::dd::DdType DdType = ModelType::DdType;
23
24 explicit SymbolicPropositionalModelChecker(ModelType const& model);
25
26 // The implemented methods of the AbstractModelChecker interface.
27 virtual bool canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const override;
28 virtual std::unique_ptr<CheckResult> checkBooleanLiteralFormula(Environment const& env,
30 virtual std::unique_ptr<CheckResult> checkAtomicLabelFormula(Environment const& env,
32 virtual std::unique_ptr<CheckResult> checkAtomicExpressionFormula(Environment const& env,
34
35 protected:
41 virtual ModelType const& getModel() const;
42
43 private:
44 // The model that is to be analyzed by the model checker.
45 ModelType const& model;
46};
47
48} // namespace modelchecker
49} // namespace storm
50
51#endif /* STORM_MODELCHECKER_SYMBOLICPROPOSITIONALMODELCHECKER_H_ */
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 ModelType const & getModel() const
Retrieves the model associated with this model checker instance.
virtual std::unique_ptr< CheckResult > checkAtomicExpressionFormula(Environment const &env, CheckTask< storm::logic::AtomicExpressionFormula, ValueType > const &checkTask) override
LabParser.cpp.
Definition cli.cpp:18