From cc7d44dd157ea3c59d2b3831dee72e1813e81d2a Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Thu, 29 Jan 2015 21:19:49 +0100
Subject: [PATCH] Added proper canHandle method to propositional model checker.
Former-commit-id: 4af714e31a33e6c967823915f6d00027f1005537
---
.../propositional/SparsePropositionalModelChecker.cpp | 5 +++++
.../propositional/SparsePropositionalModelChecker.h | 1 +
2 files changed, 6 insertions(+)
diff --git a/src/modelchecker/propositional/SparsePropositionalModelChecker.cpp b/src/modelchecker/propositional/SparsePropositionalModelChecker.cpp
index 565546adf..aa8c4e058 100644
--- a/src/modelchecker/propositional/SparsePropositionalModelChecker.cpp
+++ b/src/modelchecker/propositional/SparsePropositionalModelChecker.cpp
@@ -15,6 +15,11 @@ namespace storm {
// Intentionally left empty.
}
+ template<typename ValueType>
+ bool SparsePropositionalModelChecker<ValueType>::canHandle(storm::logic::Formula const& formula) const {
+ return formula.isPropositionalFormula();
+ }
+
template<typename ValueType>
std::unique_ptr<CheckResult> SparsePropositionalModelChecker<ValueType>::checkBooleanLiteralFormula(storm::logic::BooleanLiteralFormula const& stateFormula) {
if (stateFormula.isTrueFormula()) {
diff --git a/src/modelchecker/propositional/SparsePropositionalModelChecker.h b/src/modelchecker/propositional/SparsePropositionalModelChecker.h
index c6309e4f0..d3a9011ce 100644
--- a/src/modelchecker/propositional/SparsePropositionalModelChecker.h
+++ b/src/modelchecker/propositional/SparsePropositionalModelChecker.h
@@ -14,6 +14,7 @@ namespace storm {
explicit SparsePropositionalModelChecker(storm::models::AbstractModel<ValueType> const& model);
// The implemented methods of the AbstractModelChecker interface.
+ virtual bool canHandle(storm::logic::Formula const& formula) const override;
virtual std::unique_ptr<CheckResult> checkBooleanLiteralFormula(storm::logic::BooleanLiteralFormula const& stateFormula) override;
virtual std::unique_ptr<CheckResult> checkAtomicLabelFormula(storm::logic::AtomicLabelFormula const& stateFormula) override;