diff --git a/examples/multi-objective/mdp/dpm/dpm100_numerical.pctl b/examples/multi-objective/mdp/dpm/dpm100_numerical.pctl index f081396c7..97de9f0e1 100644 --- a/examples/multi-objective/mdp/dpm/dpm100_numerical.pctl +++ b/examples/multi-objective/mdp/dpm/dpm100_numerical.pctl @@ -1,3 +1,3 @@ - multi(R{"power"}min=? [ C<=100 ], R{"queue"}<=70 [ C<=100 ]); + multi(R{"power"}min=? [ C<=100 ], R{"queue"}<=70 [ C<=100 ]) // Note: The property file from http://www.prismmodelchecker.org/files/atva12mo/ does not provide a threshold for the second objective. // We pick a threshold that intersects the pareto curve. \ No newline at end of file diff --git a/src/logic/CloneVisitor.cpp b/src/logic/CloneVisitor.cpp index 3ed09346c..d6161f324 100644 --- a/src/logic/CloneVisitor.cpp +++ b/src/logic/CloneVisitor.cpp @@ -99,6 +99,10 @@ namespace storm { return std::static_pointer_cast(std::make_shared(subformula, f.getOptionalRewardModelName(), f.getOperatorInformation())); } + boost::any CloneVisitor::visit(TotalRewardFormula const& f, boost::any const& data) const { + return std::static_pointer_cast(std::make_shared()); + } + boost::any CloneVisitor::visit(UnaryBooleanStateFormula const& f, boost::any const& data) const { std::shared_ptr subformula = boost::any_cast>(f.getSubformula().accept(*this, data)); return std::static_pointer_cast(std::make_shared(f.getOperator(), subformula)); diff --git a/src/logic/CloneVisitor.h b/src/logic/CloneVisitor.h index 55c0d89c4..437278e97 100644 --- a/src/logic/CloneVisitor.h +++ b/src/logic/CloneVisitor.h @@ -29,6 +29,7 @@ namespace storm { virtual boost::any visit(NextFormula const& f, boost::any const& data) const override; virtual boost::any visit(ProbabilityOperatorFormula const& f, boost::any const& data) const override; virtual boost::any visit(RewardOperatorFormula const& f, boost::any const& data) const override; + virtual boost::any visit(TotalRewardFormula const& f, boost::any const& data) const override; virtual boost::any visit(UnaryBooleanStateFormula const& f, boost::any const& data) const override; virtual boost::any visit(UntilFormula const& f, boost::any const& data) const override; }; @@ -37,4 +38,4 @@ namespace storm { } -#endif /* STORM_LOGIC_CLONEVISITOR_H_ */ \ No newline at end of file +#endif /* STORM_LOGIC_CLONEVISITOR_H_ */ diff --git a/src/logic/ComparisonType.h b/src/logic/ComparisonType.h index b91b2432b..bf932fc2b 100644 --- a/src/logic/ComparisonType.h +++ b/src/logic/ComparisonType.h @@ -14,7 +14,20 @@ namespace storm { inline bool isLowerBound(ComparisonType t) { return (t == ComparisonType::Greater || t == ComparisonType::GreaterEqual); } - + + inline ComparisonType invert(ComparisonType t) { + switch(t) { + case ComparisonType::Less: + return ComparisonType::GreaterEqual; + case ComparisonType::LessEqual: + return ComparisonType::Greater; + case ComparisonType::Greater: + return ComparisonType::LessEqual; + case ComparisonType::GreaterEqual: + return ComparisonType::Less; + } + } + std::ostream& operator<<(std::ostream& out, ComparisonType const& comparisonType); } } diff --git a/src/logic/Formula.cpp b/src/logic/Formula.cpp index cdd259063..12a3a7212 100644 --- a/src/logic/Formula.cpp +++ b/src/logic/Formula.cpp @@ -133,6 +133,10 @@ namespace storm { return false; } + bool Formula::isTotalRewardFormula() const { + return false; + } + bool Formula::isReachabilityTimeFormula() const { return false; } @@ -363,6 +367,14 @@ namespace storm { return dynamic_cast(*this); } + TotalRewardFormula& Formula::asTotalRewardFormula() { + return dynamic_cast(*this); + } + + TotalRewardFormula const& Formula::asTotalRewardFormula() const { + return dynamic_cast(*this); + } + InstantaneousRewardFormula& Formula::asInstantaneousRewardFormula() { return dynamic_cast(*this); } @@ -470,4 +482,4 @@ namespace storm { return formula.writeToStream(out); } } -} \ No newline at end of file +} diff --git a/src/logic/Formula.h b/src/logic/Formula.h index c2d763f46..9c7a62009 100644 --- a/src/logic/Formula.h +++ b/src/logic/Formula.h @@ -76,6 +76,7 @@ namespace storm { virtual bool isInstantaneousRewardFormula() const; virtual bool isReachabilityRewardFormula() const; virtual bool isLongRunAverageRewardFormula() const; + virtual bool isTotalRewardFormula() const; // Expected time formulas. virtual bool isReachabilityTimeFormula() const; @@ -169,6 +170,9 @@ namespace storm { CumulativeRewardFormula& asCumulativeRewardFormula(); CumulativeRewardFormula const& asCumulativeRewardFormula() const; + TotalRewardFormula& asTotalRewardFormula(); + TotalRewardFormula const& asTotalRewardFormula() const; + InstantaneousRewardFormula& asInstantaneousRewardFormula(); InstantaneousRewardFormula const& asInstantaneousRewardFormula() const; @@ -220,4 +224,4 @@ namespace storm { } } -#endif /* STORM_LOGIC_FORMULA_H_ */ \ No newline at end of file +#endif /* STORM_LOGIC_FORMULA_H_ */ diff --git a/src/logic/FormulaInformationVisitor.cpp b/src/logic/FormulaInformationVisitor.cpp index f7371abb7..a23124031 100644 --- a/src/logic/FormulaInformationVisitor.cpp +++ b/src/logic/FormulaInformationVisitor.cpp @@ -81,6 +81,10 @@ namespace storm { return boost::any_cast(f.getSubformula().accept(*this)).setContainsRewardOperator(); } + boost::any FormulaInformationVisitor::visit(TotalRewardFormula const& f, boost::any const& data) const { + return FormulaInformation(); + } + boost::any FormulaInformationVisitor::visit(UnaryBooleanStateFormula const& f, boost::any const& data) const { return f.getSubformula().accept(*this); } @@ -90,4 +94,4 @@ namespace storm { } } -} \ No newline at end of file +} diff --git a/src/logic/FormulaInformationVisitor.h b/src/logic/FormulaInformationVisitor.h index 444b34b1f..5ce306c47 100644 --- a/src/logic/FormulaInformationVisitor.h +++ b/src/logic/FormulaInformationVisitor.h @@ -28,6 +28,7 @@ namespace storm { virtual boost::any visit(NextFormula const& f, boost::any const& data) const override; virtual boost::any visit(ProbabilityOperatorFormula const& f, boost::any const& data) const override; virtual boost::any visit(RewardOperatorFormula const& f, boost::any const& data) const override; + virtual boost::any visit(TotalRewardFormula const& f, boost::any const& data) const override; virtual boost::any visit(UnaryBooleanStateFormula const& f, boost::any const& data) const override; virtual boost::any visit(UntilFormula const& f, boost::any const& data) const override; }; @@ -36,4 +37,4 @@ namespace storm { } -#endif /* STORM_LOGIC_FORMULAINFORMATIONVISITOR_H_ */ \ No newline at end of file +#endif /* STORM_LOGIC_FORMULAINFORMATIONVISITOR_H_ */ diff --git a/src/logic/FormulaVisitor.h b/src/logic/FormulaVisitor.h index b0b920e53..8909a5427 100644 --- a/src/logic/FormulaVisitor.h +++ b/src/logic/FormulaVisitor.h @@ -27,6 +27,7 @@ namespace storm { virtual boost::any visit(NextFormula const& f, boost::any const& data) const = 0; virtual boost::any visit(ProbabilityOperatorFormula const& f, boost::any const& data) const = 0; virtual boost::any visit(RewardOperatorFormula const& f, boost::any const& data) const = 0; + virtual boost::any visit(TotalRewardFormula const& f, boost::any const& data) const = 0; virtual boost::any visit(UnaryBooleanStateFormula const& f, boost::any const& data) const = 0; virtual boost::any visit(UntilFormula const& f, boost::any const& data) const = 0; }; @@ -34,4 +35,4 @@ namespace storm { } } -#endif /* STORM_LOGIC_FORMULAVISITOR_H_ */ \ No newline at end of file +#endif /* STORM_LOGIC_FORMULAVISITOR_H_ */ diff --git a/src/logic/Formulas.h b/src/logic/Formulas.h index 50b51ebb2..0a39b0788 100644 --- a/src/logic/Formulas.h +++ b/src/logic/Formulas.h @@ -20,6 +20,7 @@ #include "src/logic/LongRunAverageOperatorFormula.h" #include "src/logic/MultiObjectiveFormula.h" #include "src/logic/TimeOperatorFormula.h" +#include "src/logic/TotalRewardFormula.h" #include "src/logic/UnaryBooleanStateFormula.h" #include "src/logic/UnaryPathFormula.h" #include "src/logic/UnaryStateFormula.h" @@ -27,4 +28,4 @@ #include "src/logic/ConditionalFormula.h" #include "src/logic/ProbabilityOperatorFormula.h" #include "src/logic/RewardOperatorFormula.h" -#include "src/logic/ComparisonType.h" \ No newline at end of file +#include "src/logic/ComparisonType.h" diff --git a/src/logic/FormulasForwardDeclarations.h b/src/logic/FormulasForwardDeclarations.h index d8da094eb..fcd24d1ed 100644 --- a/src/logic/FormulasForwardDeclarations.h +++ b/src/logic/FormulasForwardDeclarations.h @@ -27,6 +27,7 @@ namespace storm { class ProbabilityOperatorFormula; class RewardOperatorFormula; class StateFormula; + class TotalRewardFormula; class UnaryBooleanStateFormula; class UnaryPathFormula; class UnaryStateFormula; @@ -34,4 +35,4 @@ namespace storm { } } -#endif /* STORM_LOGIC_FORMULASFORWARDDECLARATIONS_H_ */ \ No newline at end of file +#endif /* STORM_LOGIC_FORMULASFORWARDDECLARATIONS_H_ */ diff --git a/src/logic/FragmentChecker.cpp b/src/logic/FragmentChecker.cpp index b4bda1f8f..1a1bc0087 100644 --- a/src/logic/FragmentChecker.cpp +++ b/src/logic/FragmentChecker.cpp @@ -216,6 +216,11 @@ namespace storm { return result; } + boost::any FragmentChecker::visit(TotalRewardFormula const& f, boost::any const& data) const { + InheritedInformation const& inherited = boost::any_cast(data); + return inherited.getSpecification().areTotalRewardFormulasAllowed(); + } + boost::any FragmentChecker::visit(UnaryBooleanStateFormula const& f, boost::any const& data) const { InheritedInformation const& inherited = boost::any_cast(data); bool result = inherited.getSpecification().areUnaryBooleanStateFormulasAllowed(); @@ -235,4 +240,4 @@ namespace storm { return result; } } -} \ No newline at end of file +} diff --git a/src/logic/FragmentChecker.h b/src/logic/FragmentChecker.h index 41846c37f..8410e4ee7 100644 --- a/src/logic/FragmentChecker.h +++ b/src/logic/FragmentChecker.h @@ -29,6 +29,7 @@ namespace storm { virtual boost::any visit(NextFormula const& f, boost::any const& data) const override; virtual boost::any visit(ProbabilityOperatorFormula const& f, boost::any const& data) const override; virtual boost::any visit(RewardOperatorFormula const& f, boost::any const& data) const override; + virtual boost::any visit(TotalRewardFormula const& f, boost::any const& data) const override; virtual boost::any visit(UnaryBooleanStateFormula const& f, boost::any const& data) const override; virtual boost::any visit(UntilFormula const& f, boost::any const& data) const override; }; @@ -37,4 +38,4 @@ namespace storm { } -#endif /* STORM_LOGIC_FRAGMENTCHECKER_H_ */ \ No newline at end of file +#endif /* STORM_LOGIC_FRAGMENTCHECKER_H_ */ diff --git a/src/logic/FragmentSpecification.cpp b/src/logic/FragmentSpecification.cpp index bf63e5019..851cc8741 100644 --- a/src/logic/FragmentSpecification.cpp +++ b/src/logic/FragmentSpecification.cpp @@ -94,9 +94,9 @@ namespace storm { multiObjective.setRewardOperatorsAllowed(true); multiObjective.setReachabilityRewardFormulasAllowed(true); multiObjective.setCumulativeRewardFormulasAllowed(true); + multiObjective.setTotalRewardFormulasAllowed(true); multiObjective.setBoundedUntilFormulasAllowed(true); - multiObjective.setStepBoundedUntilFormulasAllowed(true); - // multiObjective.setTimeBoundedUntilFormulasAllowed(true); //probably better to activate this only when an MA is given... + return multiObjective; } @@ -125,6 +125,7 @@ namespace storm { instantaneousRewardFormula = false; reachabilityRewardFormula = false; longRunAverageRewardFormula = false; + totalRewardFormula = false; conditionalProbabilityFormula = false; conditionalRewardFormula = false; @@ -321,6 +322,16 @@ namespace storm { return *this; } + + bool FragmentSpecification::areTotalRewardFormulasAllowed() const { + return totalRewardFormula; + } + + FragmentSpecification& FragmentSpecification::setTotalRewardFormulasAllowed(bool newValue) { + this->totalRewardFormula = newValue; + return *this; + } + bool FragmentSpecification::areConditionalProbabilityFormulasAllowed() const { return conditionalProbabilityFormula; } diff --git a/src/logic/FragmentSpecification.h b/src/logic/FragmentSpecification.h index 88910988d..d19f7da11 100644 --- a/src/logic/FragmentSpecification.h +++ b/src/logic/FragmentSpecification.h @@ -69,6 +69,9 @@ namespace storm { bool areLongRunAverageRewardFormulasAllowed() const; FragmentSpecification& setLongRunAverageRewardFormulasAllowed(bool newValue); + + bool areTotalRewardFormulasAllowed() const; + FragmentSpecification& setTotalRewardFormulasAllowed(bool newValue); bool areConditionalProbabilityFormulasAllowed() const; FragmentSpecification& setConditionalProbabilityFormulasAllowed(bool newValue); @@ -141,6 +144,7 @@ namespace storm { bool instantaneousRewardFormula; bool reachabilityRewardFormula; bool longRunAverageRewardFormula; + bool totalRewardFormula; bool conditionalProbabilityFormula; bool conditionalRewardFormula; @@ -188,4 +192,4 @@ namespace storm { } } -#endif /* STORM_LOGIC_FRAGMENTSPECIFICATION_H_ */ \ No newline at end of file +#endif /* STORM_LOGIC_FRAGMENTSPECIFICATION_H_ */ diff --git a/src/logic/ToExpressionVisitor.cpp b/src/logic/ToExpressionVisitor.cpp index 534cc008b..928275047 100644 --- a/src/logic/ToExpressionVisitor.cpp +++ b/src/logic/ToExpressionVisitor.cpp @@ -98,6 +98,10 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements."); } + boost::any ToExpressionVisitor::visit(TotalRewardFormula const& f, boost::any const& data) const { + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements."); + } + boost::any ToExpressionVisitor::visit(UnaryBooleanStateFormula const& f, boost::any const& data) const { storm::expressions::Expression subexpression = boost::any_cast(f.getSubformula().accept(*this, data)); switch (f.getOperator()) { diff --git a/src/logic/ToExpressionVisitor.h b/src/logic/ToExpressionVisitor.h index ed325d38f..ee816b6a6 100644 --- a/src/logic/ToExpressionVisitor.h +++ b/src/logic/ToExpressionVisitor.h @@ -29,6 +29,7 @@ namespace storm { virtual boost::any visit(NextFormula const& f, boost::any const& data) const override; virtual boost::any visit(ProbabilityOperatorFormula const& f, boost::any const& data) const override; virtual boost::any visit(RewardOperatorFormula const& f, boost::any const& data) const override; + virtual boost::any visit(TotalRewardFormula const& f, boost::any const& data) const override; virtual boost::any visit(UnaryBooleanStateFormula const& f, boost::any const& data) const override; virtual boost::any visit(UntilFormula const& f, boost::any const& data) const override; }; @@ -37,4 +38,4 @@ namespace storm { } -#endif /* STORM_LOGIC_TOEXPRESSIONVISITOR_H_ */ \ No newline at end of file +#endif /* STORM_LOGIC_TOEXPRESSIONVISITOR_H_ */ diff --git a/src/logic/TotalRewardFormula.cpp b/src/logic/TotalRewardFormula.cpp new file mode 100644 index 000000000..10f669f64 --- /dev/null +++ b/src/logic/TotalRewardFormula.cpp @@ -0,0 +1,28 @@ +#include "src/logic/TotalRewardFormula.h" + +#include "src/logic/FormulaVisitor.h" + +namespace storm { + namespace logic { + TotalRewardFormula::TotalRewardFormula() { + // Intentionally left empty. + } + + bool TotalRewardFormula::isTotalRewardFormula() const { + return true; + } + + bool TotalRewardFormula::isRewardPathFormula() const { + return true; + } + + boost::any TotalRewardFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const { + return visitor.visit(*this, data); + } + + std::ostream& TotalRewardFormula::writeToStream(std::ostream& out) const { + out << "C"; + return out; + } + } +} diff --git a/src/logic/TotalRewardFormula.h b/src/logic/TotalRewardFormula.h new file mode 100644 index 000000000..cc5f6b1a2 --- /dev/null +++ b/src/logic/TotalRewardFormula.h @@ -0,0 +1,29 @@ +#ifndef STORM_LOGIC_TOTALREWARDFORMULA_H_ +#define STORM_LOGIC_TOTALREWARDFORMULA_H_ + +#include + +#include "src/logic/PathFormula.h" + +namespace storm { + namespace logic { + class TotalRewardFormula : public PathFormula { + public: + TotalRewardFormula(); + + virtual ~TotalRewardFormula() { + // Intentionally left empty. + } + + virtual bool isTotalRewardFormula() const override; + virtual bool isRewardPathFormula() const override; + + virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override; + + virtual std::ostream& writeToStream(std::ostream& out) const override; + + }; + } +} + +#endif /* STORM_LOGIC_TOTALREWARDFORMULA_H_ */ diff --git a/src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.cpp b/src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.cpp index 97bac76ec..6cc793fc4 100644 --- a/src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.cpp +++ b/src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.cpp @@ -29,7 +29,7 @@ namespace storm { //In general, each initial state requires an individual scheduler (in contrast to single objective model checking). Let's exclude this. if(this->getModel().getInitialStates().getNumberOfSetBits() > 1) return false; if(!checkTask.isOnlyInitialStatesRelevantSet()) return false; - return checkTask.getFormula().isInFragment(storm::logic::multiObjective()); + return checkTask.getFormula().isInFragment(storm::logic::multiObjective().setStepBoundedUntilFormulasAllowed(true)); } template diff --git a/src/parser/FormulaParser.cpp b/src/parser/FormulaParser.cpp index 206d08b13..932553f7c 100644 --- a/src/parser/FormulaParser.cpp +++ b/src/parser/FormulaParser.cpp @@ -142,6 +142,7 @@ namespace storm { qi::rule(), Skipper> rewardPathFormula; qi::rule(), Skipper> cumulativeRewardFormula; + qi::rule(), Skipper> totalRewardFormula; qi::rule(), Skipper> instantaneousRewardFormula; qi::rule(), Skipper> longRunAverageRewardFormula; @@ -153,6 +154,7 @@ namespace storm { // Methods that actually create the expression objects. std::shared_ptr createInstantaneousRewardFormula(boost::variant const& timeBound) const; std::shared_ptr createCumulativeRewardFormula(boost::variant const& timeBound) const; + std::shared_ptr createTotalRewardFormula() const; std::shared_ptr createLongRunAverageRewardFormula() const; std::shared_ptr createAtomicExpressionFormula(storm::expressions::Expression const& expression) const; std::shared_ptr createBooleanLiteralFormula(bool literal) const; @@ -269,7 +271,10 @@ namespace storm { cumulativeRewardFormula = (qi::lit("C<=") >> strict_double)[qi::_val = phoenix::bind(&FormulaParserGrammar::createCumulativeRewardFormula, phoenix::ref(*this), qi::_1)] | (qi::lit("C<=") > qi::uint_)[qi::_val = phoenix::bind(&FormulaParserGrammar::createCumulativeRewardFormula, phoenix::ref(*this), qi::_1)]; cumulativeRewardFormula.name("cumulative reward formula"); - rewardPathFormula = conditionalFormula(storm::logic::FormulaContext::Reward) | eventuallyFormula(storm::logic::FormulaContext::Reward) | cumulativeRewardFormula | instantaneousRewardFormula | longRunAverageRewardFormula; + totalRewardFormula = (qi::lit("C"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createTotalRewardFormula, phoenix::ref(*this))]; + totalRewardFormula.name("total reward formula"); + + rewardPathFormula = conditionalFormula(storm::logic::FormulaContext::Reward) | eventuallyFormula(storm::logic::FormulaContext::Reward) | cumulativeRewardFormula | instantaneousRewardFormula | longRunAverageRewardFormula | totalRewardFormula; rewardPathFormula.name("reward path formula"); expressionFormula = expressionParser[qi::_val = phoenix::bind(&FormulaParserGrammar::createAtomicExpressionFormula, phoenix::ref(*this), qi::_1)]; @@ -375,6 +380,7 @@ namespace storm { debug(expressionFormula); debug(rewardPathFormula); debug(cumulativeRewardFormula); + debug(totalRewardFormula); debug(instantaneousRewardFormula); debug(multiObjectiveFormula); */ @@ -402,6 +408,7 @@ namespace storm { qi::on_error(expressionFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); qi::on_error(rewardPathFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); qi::on_error(cumulativeRewardFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(totalRewardFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); qi::on_error(instantaneousRewardFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); qi::on_error(multiObjectiveFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); } @@ -430,6 +437,10 @@ namespace storm { } } + std::shared_ptr FormulaParserGrammar::createTotalRewardFormula() const { + return std::shared_ptr(new storm::logic::TotalRewardFormula()); + } + std::shared_ptr FormulaParserGrammar::createLongRunAverageRewardFormula() const { return std::shared_ptr(new storm::logic::LongRunAverageRewardFormula()); }