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()));