diff --git a/src/storm/logic/MultiObjectiveFormula.cpp b/src/storm/logic/MultiObjectiveFormula.cpp index dec0fc6cd..edae6a1ea 100644 --- a/src/storm/logic/MultiObjectiveFormula.cpp +++ b/src/storm/logic/MultiObjectiveFormula.cpp @@ -19,10 +19,6 @@ namespace storm { return true; } - bool MultiObjectiveFormula::isStateFormula() const { - return true; - } - bool MultiObjectiveFormula::hasQualitativeResult() const { for(auto const& subformula : this->subformulas){ if(subformula->hasQuantitativeResult()){ diff --git a/src/storm/logic/MultiObjectiveFormula.h b/src/storm/logic/MultiObjectiveFormula.h index bee816a61..82e34807e 100644 --- a/src/storm/logic/MultiObjectiveFormula.h +++ b/src/storm/logic/MultiObjectiveFormula.h @@ -1,18 +1,17 @@ #ifndef STORM_LOGIC_MULTIOBJECTIVEFORMULA_H_ #define STORM_LOGIC_MULTIOBJECTIVEFORMULA_H_ -#include "storm/logic/Formula.h" +#include "storm/logic/StateFormula.h" namespace storm { namespace logic { - class MultiObjectiveFormula : public Formula { + class MultiObjectiveFormula : public StateFormula { public: MultiObjectiveFormula(std::vector> const& subformulas); virtual ~MultiObjectiveFormula(); virtual bool isMultiObjectiveFormula() const override; - virtual bool isStateFormula() const override; virtual bool hasQualitativeResult() const override; // Result is true or false virtual bool hasQuantitativeResult() const override; // Result is numerical or a pareto curve diff --git a/src/storm/logic/QuantileFormula.h b/src/storm/logic/QuantileFormula.h index 4bfe0a5a1..16fbaf408 100644 --- a/src/storm/logic/QuantileFormula.h +++ b/src/storm/logic/QuantileFormula.h @@ -1,10 +1,10 @@ #pragma once -#include "storm/logic/Formula.h" +#include "storm/logic/StateFormula.h" namespace storm { namespace logic { - class QuantileFormula : public Formula { + class QuantileFormula : public StateFormula { public: QuantileFormula(std::vector const& boundVariables, std::shared_ptr subformula); diff --git a/src/storm/modelchecker/AbstractModelChecker.cpp b/src/storm/modelchecker/AbstractModelChecker.cpp index 31b34cd72..8e40891f4 100644 --- a/src/storm/modelchecker/AbstractModelChecker.cpp +++ b/src/storm/modelchecker/AbstractModelChecker.cpp @@ -237,6 +237,10 @@ namespace storm { return this->checkBooleanLiteralFormula(env, checkTask.substituteFormula(stateFormula.asBooleanLiteralFormula())); } else if (stateFormula.isGameFormula()) { return this->checkGameFormula(env, checkTask.substituteFormula(stateFormula.asGameFormula())); + } else if (stateFormula.isMultiObjectiveFormula()){ + return this->checkMultiObjectiveFormula(env, checkTask.substituteFormula(stateFormula.asMultiObjectiveFormula())); + } else if (stateFormula.isQuantileFormula()){ + return this->checkQuantileFormula(env, checkTask.substituteFormula(stateFormula.asQuantileFormula())); } STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << stateFormula << "' is invalid."); }