Browse Source

flagging multi-objective and quantile formulae as StateFormulae (fixing the previous commit)

Conflicts:
	src/storm/modelchecker/AbstractModelChecker.cpp
main
Tim Quatmann 4 years ago
committed by Stefan Pranger
parent
commit
aa29ad1196
  1. 4
      src/storm/logic/MultiObjectiveFormula.cpp
  2. 5
      src/storm/logic/MultiObjectiveFormula.h
  3. 4
      src/storm/logic/QuantileFormula.h
  4. 4
      src/storm/modelchecker/AbstractModelChecker.cpp

4
src/storm/logic/MultiObjectiveFormula.cpp

@ -19,10 +19,6 @@ namespace storm {
return true; return true;
} }
bool MultiObjectiveFormula::isStateFormula() const {
return true;
}
bool MultiObjectiveFormula::hasQualitativeResult() const { bool MultiObjectiveFormula::hasQualitativeResult() const {
for(auto const& subformula : this->subformulas){ for(auto const& subformula : this->subformulas){
if(subformula->hasQuantitativeResult()){ if(subformula->hasQuantitativeResult()){

5
src/storm/logic/MultiObjectiveFormula.h

@ -1,18 +1,17 @@
#ifndef STORM_LOGIC_MULTIOBJECTIVEFORMULA_H_ #ifndef STORM_LOGIC_MULTIOBJECTIVEFORMULA_H_
#define STORM_LOGIC_MULTIOBJECTIVEFORMULA_H_ #define STORM_LOGIC_MULTIOBJECTIVEFORMULA_H_
#include "storm/logic/Formula.h" #include "storm/logic/StateFormula.h"
namespace storm { namespace storm {
namespace logic { namespace logic {
class MultiObjectiveFormula : public Formula { class MultiObjectiveFormula : public StateFormula {
public: public:
MultiObjectiveFormula(std::vector<std::shared_ptr<Formula const>> const& subformulas); MultiObjectiveFormula(std::vector<std::shared_ptr<Formula const>> const& subformulas);
virtual ~MultiObjectiveFormula(); virtual ~MultiObjectiveFormula();
virtual bool isMultiObjectiveFormula() const override; virtual bool isMultiObjectiveFormula() const override;
virtual bool isStateFormula() const override;
virtual bool hasQualitativeResult() const override; // Result is true or false virtual bool hasQualitativeResult() const override; // Result is true or false
virtual bool hasQuantitativeResult() const override; // Result is numerical or a pareto curve virtual bool hasQuantitativeResult() const override; // Result is numerical or a pareto curve

4
src/storm/logic/QuantileFormula.h

@ -1,10 +1,10 @@
#pragma once #pragma once
#include "storm/logic/Formula.h" #include "storm/logic/StateFormula.h"
namespace storm { namespace storm {
namespace logic { namespace logic {
class QuantileFormula : public Formula { class QuantileFormula : public StateFormula {
public: public:
QuantileFormula(std::vector<storm::expressions::Variable> const& boundVariables, std::shared_ptr<Formula const> subformula); QuantileFormula(std::vector<storm::expressions::Variable> const& boundVariables, std::shared_ptr<Formula const> subformula);

4
src/storm/modelchecker/AbstractModelChecker.cpp

@ -237,6 +237,10 @@ namespace storm {
return this->checkBooleanLiteralFormula(env, checkTask.substituteFormula(stateFormula.asBooleanLiteralFormula())); return this->checkBooleanLiteralFormula(env, checkTask.substituteFormula(stateFormula.asBooleanLiteralFormula()));
} else if (stateFormula.isGameFormula()) { } else if (stateFormula.isGameFormula()) {
return this->checkGameFormula(env, checkTask.substituteFormula(stateFormula.asGameFormula())); 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."); STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The given formula '" << stateFormula << "' is invalid.");
} }

|||||||
100:0
Loading…
Cancel
Save