From 113f17372f3088d04150027d4b555606bd4d8d68 Mon Sep 17 00:00:00 2001 From: hannah Date: Tue, 29 Jun 2021 08:19:22 +0200 Subject: [PATCH] set hasQualitativeResult to false for HOAFormulas --- src/storm/logic/HOAPathFormula.cpp | 4 ++++ src/storm/logic/HOAPathFormula.h | 1 + src/storm/modelchecker/AbstractModelChecker.cpp | 6 ------ 3 files changed, 5 insertions(+), 6 deletions(-) diff --git a/src/storm/logic/HOAPathFormula.cpp b/src/storm/logic/HOAPathFormula.cpp index cd17a6a46..b5dc17d27 100644 --- a/src/storm/logic/HOAPathFormula.cpp +++ b/src/storm/logic/HOAPathFormula.cpp @@ -43,6 +43,10 @@ namespace storm { return true; } + bool HOAPathFormula::hasQualitativeResult() const { + return false; + } + boost::any HOAPathFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const { return visitor.visit(*this, data); } diff --git a/src/storm/logic/HOAPathFormula.h b/src/storm/logic/HOAPathFormula.h index fd9ba1a93..53fcc1120 100644 --- a/src/storm/logic/HOAPathFormula.h +++ b/src/storm/logic/HOAPathFormula.h @@ -32,6 +32,7 @@ namespace storm { virtual bool isHOAPathFormula() const override; virtual bool isProbabilityPathFormula() const override; virtual bool hasQuantitativeResult() const override; + virtual bool hasQualitativeResult() const override; virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override; diff --git a/src/storm/modelchecker/AbstractModelChecker.cpp b/src/storm/modelchecker/AbstractModelChecker.cpp index f2d880db0..fc1534585 100644 --- a/src/storm/modelchecker/AbstractModelChecker.cpp +++ b/src/storm/modelchecker/AbstractModelChecker.cpp @@ -65,11 +65,6 @@ namespace storm { std::unique_ptr AbstractModelChecker::computeProbabilities(Environment const& env, CheckTask const& checkTask) { storm::logic::Formula const& formula = checkTask.getFormula(); - //TODO if this is not checked first, computeStateFormulaProbabilities(...) is called (hasQualitativeResult true) - if (formula.isHOAPathFormula()) { - return this->computeHOAPathProbabilities(env, checkTask.substituteFormula(formula.asHOAPathFormula())); - } - if (formula.isStateFormula() || formula.hasQualitativeResult()) { return this->computeStateFormulaProbabilities(env, checkTask.substituteFormula(formula)); } @@ -89,7 +84,6 @@ namespace storm { } else if (formula.isUntilFormula()) { return this->computeUntilProbabilities(env, checkTask.substituteFormula(formula.asUntilFormula())); } else if (formula.isHOAPathFormula()) { - // TODO checked earlier? return this->computeHOAPathProbabilities(env, checkTask.substituteFormula(formula.asHOAPathFormula())); } else if (formula.isNextFormula()) { return this->computeNextProbabilities(env, checkTask.substituteFormula(formula.asNextFormula()));