diff --git a/src/logic/CloneVisitor.cpp b/src/logic/CloneVisitor.cpp
index fe7182bf7..3ed09346c 100644
--- a/src/logic/CloneVisitor.cpp
+++ b/src/logic/CloneVisitor.cpp
@@ -76,6 +76,14 @@ namespace storm {
return std::static_pointer_cast<Formula>(std::make_shared<LongRunAverageRewardFormula>(f));
}
+ boost::any CloneVisitor::visit(MultiObjectiveFormula const& f, boost::any const& data) const {
+ std::vector<std::shared_ptr<Formula const>> subformulas;
+ for(uint_fast64_t index = 0; index < f.getNumberOfSubformulas(); ++index){
+ subformulas.push_back(boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula(index).accept(*this, data)));
+ }
+ return std::static_pointer_cast<Formula>(std::make_shared<MultiObjectiveFormula>(subformulas));
+ }
+
boost::any CloneVisitor::visit(NextFormula const& f, boost::any const& data) const {
std::shared_ptr<Formula> subformula = boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula().accept(*this, data));
return std::static_pointer_cast<Formula>(std::make_shared<NextFormula>(subformula));
diff --git a/src/logic/CloneVisitor.h b/src/logic/CloneVisitor.h
index 23fc3ffdc..55c0d89c4 100644
--- a/src/logic/CloneVisitor.h
+++ b/src/logic/CloneVisitor.h
@@ -25,6 +25,7 @@ namespace storm {
virtual boost::any visit(InstantaneousRewardFormula const& f, boost::any const& data) const override;
virtual boost::any visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const override;
virtual boost::any visit(LongRunAverageRewardFormula const& f, boost::any const& data) const override;
+ virtual boost::any visit(MultiObjectiveFormula const& f, boost::any const& data) const override;
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;
diff --git a/src/logic/Formula.cpp b/src/logic/Formula.cpp
index de915eaa1..cdd259063 100644
--- a/src/logic/Formula.cpp
+++ b/src/logic/Formula.cpp
@@ -17,6 +17,10 @@ namespace storm {
return false;
}
+ bool Formula::isMultiObjectiveFormula() const {
+ return false;
+ }
+
bool Formula::isBinaryStateFormula() const {
return false;
}
@@ -183,6 +187,14 @@ namespace storm {
return dynamic_cast<StateFormula const&>(*this);
}
+ MultiObjectiveFormula& Formula::asMultiObjectiveFormula() {
+ return dynamic_cast<MultiObjectiveFormula&>(*this);
+ }
+
+ MultiObjectiveFormula const& Formula::asMultiObjectiveFormula() const {
+ return dynamic_cast<MultiObjectiveFormula const&>(*this);
+ }
+
BinaryStateFormula& Formula::asBinaryStateFormula() {
return dynamic_cast<BinaryStateFormula&>(*this);
}
diff --git a/src/logic/Formula.h b/src/logic/Formula.h
index d5625a296..c2d763f46 100644
--- a/src/logic/Formula.h
+++ b/src/logic/Formula.h
@@ -46,6 +46,8 @@ namespace storm {
virtual bool isBinaryBooleanStateFormula() const;
virtual bool isUnaryBooleanStateFormula() const;
+
+ virtual bool isMultiObjectiveFormula() const;
// Operator formulas.
virtual bool isOperatorFormula() const;
@@ -101,6 +103,9 @@ namespace storm {
StateFormula& asStateFormula();
StateFormula const& asStateFormula() const;
+ MultiObjectiveFormula& asMultiObjectiveFormula();
+ MultiObjectiveFormula const& asMultiObjectiveFormula() const;
+
BinaryStateFormula& asBinaryStateFormula();
BinaryStateFormula const& asBinaryStateFormula() const;
diff --git a/src/logic/FormulaInformationVisitor.cpp b/src/logic/FormulaInformationVisitor.cpp
index b44045766..f7371abb7 100644
--- a/src/logic/FormulaInformationVisitor.cpp
+++ b/src/logic/FormulaInformationVisitor.cpp
@@ -61,6 +61,14 @@ namespace storm {
return FormulaInformation();
}
+ boost::any FormulaInformationVisitor::visit(MultiObjectiveFormula const& f, boost::any const& data) const {
+ FormulaInformation result;
+ for(uint_fast64_t index = 0; index < f.getNumberOfSubformulas(); ++index){
+ result.join(boost::any_cast<FormulaInformation>(f.getSubformula(index).accept(*this)));
+ }
+ return result;
+ }
+
boost::any FormulaInformationVisitor::visit(NextFormula const& f, boost::any const& data) const {
return boost::any_cast<FormulaInformation>(f.getSubformula().accept(*this)).setContainsNextFormula();
}
diff --git a/src/logic/FormulaInformationVisitor.h b/src/logic/FormulaInformationVisitor.h
index 8e706cabf..444b34b1f 100644
--- a/src/logic/FormulaInformationVisitor.h
+++ b/src/logic/FormulaInformationVisitor.h
@@ -24,6 +24,7 @@ namespace storm {
virtual boost::any visit(InstantaneousRewardFormula const& f, boost::any const& data) const override;
virtual boost::any visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const override;
virtual boost::any visit(LongRunAverageRewardFormula const& f, boost::any const& data) const override;
+ virtual boost::any visit(MultiObjectiveFormula const& f, boost::any const& data) const override;
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;
diff --git a/src/logic/FormulaVisitor.h b/src/logic/FormulaVisitor.h
index 1208b63a6..b0b920e53 100644
--- a/src/logic/FormulaVisitor.h
+++ b/src/logic/FormulaVisitor.h
@@ -23,6 +23,7 @@ namespace storm {
virtual boost::any visit(InstantaneousRewardFormula const& f, boost::any const& data) const = 0;
virtual boost::any visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const = 0;
virtual boost::any visit(LongRunAverageRewardFormula const& f, boost::any const& data) const = 0;
+ virtual boost::any visit(MultiObjectiveFormula const& f, boost::any const& data) const = 0;
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;
diff --git a/src/logic/Formulas.h b/src/logic/Formulas.h
index 7183dcb01..50b51ebb2 100644
--- a/src/logic/Formulas.h
+++ b/src/logic/Formulas.h
@@ -18,6 +18,7 @@
#include "src/logic/RewardOperatorFormula.h"
#include "src/logic/StateFormula.h"
#include "src/logic/LongRunAverageOperatorFormula.h"
+#include "src/logic/MultiObjectiveFormula.h"
#include "src/logic/TimeOperatorFormula.h"
#include "src/logic/UnaryBooleanStateFormula.h"
#include "src/logic/UnaryPathFormula.h"
diff --git a/src/logic/FormulasForwardDeclarations.h b/src/logic/FormulasForwardDeclarations.h
index 43fcf0ab9..d8da094eb 100644
--- a/src/logic/FormulasForwardDeclarations.h
+++ b/src/logic/FormulasForwardDeclarations.h
@@ -20,6 +20,7 @@ namespace storm {
class InstantaneousRewardFormula;
class LongRunAverageOperatorFormula;
class LongRunAverageRewardFormula;
+ class MultiObjectiveFormula;
class NextFormula;
class OperatorFormula;
class PathFormula;
diff --git a/src/logic/FragmentChecker.cpp b/src/logic/FragmentChecker.cpp
index b86a96693..26a787455 100644
--- a/src/logic/FragmentChecker.cpp
+++ b/src/logic/FragmentChecker.cpp
@@ -159,6 +159,21 @@ namespace storm {
return inherited.getSpecification().areLongRunAverageRewardFormulasAllowed();
}
+ boost::any FragmentChecker::visit(MultiObjectiveFormula const& f, boost::any const& data) const {
+ InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
+
+ FragmentSpecification subFormulaFragment(inherited.getSpecification());
+ if(!inherited.getSpecification().areNestedMultiObjectiveFormulasAllowed()){
+ subFormulaFragment.setMultiObjectiveFormulasAllowed(false);
+ }
+
+ bool result = inherited.getSpecification().areMultiObjectiveFormulasAllowed();
+ for(uint_fast64_t index = 0; index<f.getNumberOfSubformulas(); ++index){
+ result = result && boost::any_cast<bool>(f.getSubformula(index).accept(*this, InheritedInformation(subFormulaFragment)));
+ }
+ return result;
+ }
+
boost::any FragmentChecker::visit(NextFormula const& f, boost::any const& data) const {
InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
bool result = inherited.getSpecification().areNextFormulasAllowed();
diff --git a/src/logic/FragmentChecker.h b/src/logic/FragmentChecker.h
index 9b0377aba..41846c37f 100644
--- a/src/logic/FragmentChecker.h
+++ b/src/logic/FragmentChecker.h
@@ -25,6 +25,7 @@ namespace storm {
virtual boost::any visit(InstantaneousRewardFormula const& f, boost::any const& data) const override;
virtual boost::any visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const override;
virtual boost::any visit(LongRunAverageRewardFormula const& f, boost::any const& data) const override;
+ virtual boost::any visit(MultiObjectiveFormula const& f, boost::any const& data) const override;
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;
diff --git a/src/logic/FragmentSpecification.cpp b/src/logic/FragmentSpecification.cpp
index 3dd2bf12b..9014873c0 100644
--- a/src/logic/FragmentSpecification.cpp
+++ b/src/logic/FragmentSpecification.cpp
@@ -83,12 +83,31 @@ namespace storm {
return csrl;
}
+ FragmentSpecification multiObjective() {
+ FragmentSpecification multiObjective = propositional();
+
+ multiObjective.setMultiObjectiveFormulasAllowed(true);
+ multiObjective.setProbabilityOperatorsAllowed(true);
+ multiObjective.setUntilFormulasAllowed(true);
+ multiObjective.setReachabilityProbabilityFormulasAllowed(true);
+ multiObjective.setRewardOperatorsAllowed(true);
+ multiObjective.setReachabilityRewardFormulasAllowed(true);
+ multiObjective.setBoundedUntilFormulasAllowed(true);
+ multiObjective.setStepBoundedUntilFormulasAllowed(true);
+ // multiObjective.setTimeBoundedUntilFormulasAllowed(true); //probably better to activate this only when an MA is given...
+ multiObjective.setNestedOperatorsAllowed(false);
+
+ return multiObjective;
+ }
+
FragmentSpecification::FragmentSpecification() {
probabilityOperator = false;
rewardOperator = false;
expectedTimeOperator = false;
longRunAverageOperator = false;
+ multiObjectiveFormula = false;
+
globallyFormula = false;
reachabilityProbabilityFormula = false;
nextFormula = false;
@@ -113,6 +132,7 @@ namespace storm {
nestedOperators = true;
nestedPathFormulas = false;
+ setNestedMultiObjectiveFormulasAllowed(false);
onlyEventuallyFormuluasInConditionalFormulas = true;
stepBoundedUntilFormulas = false;
timeBoundedUntilFormulas = false;
@@ -164,6 +184,15 @@ namespace storm {
return *this;
}
+ bool FragmentSpecification::areMultiObjectiveFormulasAllowed() const {
+ return multiObjectiveFormula;
+ }
+
+ FragmentSpecification& FragmentSpecification::setMultiObjectiveFormulasAllowed( bool newValue) {
+ this->multiObjectiveFormula = newValue;
+ return *this;
+ }
+
bool FragmentSpecification::areGloballyFormulasAllowed() const {
return globallyFormula;
}
@@ -334,6 +363,15 @@ namespace storm {
this->nestedPathFormulas = newValue;
return *this;
}
+
+ bool FragmentSpecification::areNestedMultiObjectiveFormulasAllowed() const {
+ return this->nestedMultiObjectiveFormulas;
+ }
+
+ FragmentSpecification& FragmentSpecification::setNestedMultiObjectiveFormulasAllowed(bool newValue) {
+ this->nestedMultiObjectiveFormulas = newValue;
+ return *this;
+ }
bool FragmentSpecification::areOnlyEventuallyFormuluasInConditionalFormulasAllowed() const {
return this->onlyEventuallyFormuluasInConditionalFormulas;
diff --git a/src/logic/FragmentSpecification.h b/src/logic/FragmentSpecification.h
index 6637d0750..c53b287d0 100644
--- a/src/logic/FragmentSpecification.h
+++ b/src/logic/FragmentSpecification.h
@@ -24,6 +24,9 @@ namespace storm {
bool areLongRunAverageOperatorsAllowed() const;
FragmentSpecification& setLongRunAverageOperatorsAllowed(bool newValue);
+
+ bool areMultiObjectiveFormulasAllowed() const;
+ FragmentSpecification& setMultiObjectiveFormulasAllowed( bool newValue);
bool areGloballyFormulasAllowed() const;
FragmentSpecification& setGloballyFormulasAllowed(bool newValue);
@@ -78,10 +81,13 @@ namespace storm {
bool areNestedOperatorsAllowed() const;
FragmentSpecification& setNestedOperatorsAllowed(bool newValue);
-
+
bool areNestedPathFormulasAllowed() const;
FragmentSpecification& setNestedPathFormulasAllowed(bool newValue);
+ bool areNestedMultiObjectiveFormulasAllowed() const;
+ FragmentSpecification& setNestedMultiObjectiveFormulasAllowed(bool newValue);
+
bool areOnlyEventuallyFormuluasInConditionalFormulasAllowed() const;
FragmentSpecification& setOnlyEventuallyFormuluasInConditionalFormulasAllowed(bool newValue);
@@ -114,6 +120,8 @@ namespace storm {
bool expectedTimeOperator;
bool longRunAverageOperator;
+ bool multiObjectiveFormula;
+
bool globallyFormula;
bool reachabilityProbabilityFormula;
bool nextFormula;
@@ -139,6 +147,7 @@ namespace storm {
// Members that indicate certain restrictions.
bool nestedOperators;
bool nestedPathFormulas;
+ bool nestedMultiObjectiveFormulas;
bool onlyEventuallyFormuluasInConditionalFormulas;
bool stepBoundedUntilFormulas;
bool timeBoundedUntilFormulas;
@@ -168,6 +177,9 @@ namespace storm {
// CSL + cumulative, instantaneous, reachability and long-run rewards.
FragmentSpecification csrl();
+
+ // Multi-Objective formulas.
+ FragmentSpecification multiObjective();
}
}
diff --git a/src/logic/MultiObjectiveFormula.cpp b/src/logic/MultiObjectiveFormula.cpp
new file mode 100644
index 000000000..22d02b40d
--- /dev/null
+++ b/src/logic/MultiObjectiveFormula.cpp
@@ -0,0 +1,78 @@
+#include "src/logic/MultiObjectiveFormula.h"
+
+#include "src/logic/FormulaVisitor.h"
+#include "src/utility/macros.h"
+#include "src/exceptions/InvalidArgumentException.h"
+
+namespace storm {
+ namespace logic {
+
+ MultiObjectiveFormula::MultiObjectiveFormula(std::vector<std::shared_ptr<Formula const>> const& subformulas) : subformulas(subformulas) {
+ //Intentionally left empty
+ }
+
+ MultiObjectiveFormula::~MultiObjectiveFormula() {
+ //Intentionally left empty
+ }
+
+ bool MultiObjectiveFormula::isMultiObjectiveFormula() const {
+ return true;
+ }
+
+ bool MultiObjectiveFormula::hasQualitativeResult() const {
+ for(auto const& subformula : this->subformulas){
+ if(subformula->hasQuantitativeResult()){
+ return false;
+ }
+ }
+ return true;
+ }
+
+ bool MultiObjectiveFormula::hasQuantitativeResult() const {
+ return !hasQualitativeResult();
+ };
+
+ Formula const& MultiObjectiveFormula::getSubformula(uint_fast64_t index) const {
+ STORM_LOG_THROW(index < getNumberOfSubformulas(), storm::exceptions::InvalidArgumentException, "Tried to access subformula with index " << index << " but there are only " << this->getNumberOfSubformulas() << " subformulas.");
+ return *this->subformulas[index];
+ }
+
+ uint_fast64_t MultiObjectiveFormula::getNumberOfSubformulas() const {
+ return this->subformulas.size();
+ }
+
+ boost::any MultiObjectiveFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const {
+ return visitor.visit(*this, data);
+ }
+
+ void MultiObjectiveFormula::gatherAtomicExpressionFormulas(std::vector<std::shared_ptr<AtomicExpressionFormula const>>& atomicExpressionFormulas) const {
+ for(auto const& subformula : this->subformulas){
+ subformula->gatherAtomicExpressionFormulas(atomicExpressionFormulas);
+ }
+ }
+
+ void MultiObjectiveFormula::gatherAtomicLabelFormulas(std::vector<std::shared_ptr<AtomicLabelFormula const>>& atomicLabelFormulas) const {
+ for(auto const& subformula : this->subformulas){
+ subformula->gatherAtomicLabelFormulas(atomicLabelFormulas);
+ }
+ }
+
+ void MultiObjectiveFormula::gatherReferencedRewardModels(std::set<std::string>& referencedRewardModels) const {
+ for(auto const& subformula : this->subformulas){
+ subformula->gatherReferencedRewardModels(referencedRewardModels);
+ }
+ }
+
+ std::ostream& MultiObjectiveFormula::writeToStream(std::ostream &out) const {
+ out << "multi(";
+ for(uint_fast64_t index = 0; index < this->getNumberOfSubformulas(); ++index){
+ if(index>0){
+ out << ", ";
+ }
+ this->getSubformula(index).writeToStream(out);
+ }
+ out << ")";
+ return out;
+ }
+ }
+}
\ No newline at end of file
diff --git a/src/logic/MultiObjectiveFormula.h b/src/logic/MultiObjectiveFormula.h
new file mode 100644
index 000000000..7647300ac
--- /dev/null
+++ b/src/logic/MultiObjectiveFormula.h
@@ -0,0 +1,35 @@
+#ifndef STORM_LOGIC_MULTIOBJECTIVEFORMULA_H_
+#define STORM_LOGIC_MULTIOBJECTIVEFORMULA_H_
+
+#include "src/logic/Formula.h"
+
+namespace storm {
+ namespace logic {
+ class MultiObjectiveFormula : public Formula {
+ public:
+ MultiObjectiveFormula(std::vector<std::shared_ptr<Formula const>> const& subformulas);
+
+ virtual ~MultiObjectiveFormula();
+
+ virtual bool isMultiObjectiveFormula() const override;
+
+ virtual bool hasQualitativeResult() const override;
+ virtual bool hasQuantitativeResult() const override;
+
+ Formula const& getSubformula(uint_fast64_t index) const;
+ uint_fast64_t getNumberOfSubformulas() const;
+
+
+ virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override;
+ virtual void gatherAtomicExpressionFormulas(std::vector<std::shared_ptr<AtomicExpressionFormula const>>& atomicExpressionFormulas) const override;
+ virtual void gatherAtomicLabelFormulas(std::vector<std::shared_ptr<AtomicLabelFormula const>>& atomicLabelFormulas) const override;
+ virtual void gatherReferencedRewardModels(std::set<std::string>& referencedRewardModels) const override;
+
+ virtual std::ostream& writeToStream(std::ostream& out) const override;
+ private:
+ std::vector<std::shared_ptr<Formula const>> subformulas;
+ };
+ }
+}
+
+#endif /* STORM_LOGIC_MULTIOBJECTIVEFORMULA_H_ */
\ No newline at end of file
diff --git a/src/logic/ToExpressionVisitor.cpp b/src/logic/ToExpressionVisitor.cpp
index 53dfedeca..534cc008b 100644
--- a/src/logic/ToExpressionVisitor.cpp
+++ b/src/logic/ToExpressionVisitor.cpp
@@ -82,6 +82,10 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements.");
}
+ boost::any ToExpressionVisitor::visit(MultiObjectiveFormula 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(NextFormula const& f, boost::any const& data) const {
STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements.");
}
diff --git a/src/logic/ToExpressionVisitor.h b/src/logic/ToExpressionVisitor.h
index ee4a81d8f..ed325d38f 100644
--- a/src/logic/ToExpressionVisitor.h
+++ b/src/logic/ToExpressionVisitor.h
@@ -25,6 +25,7 @@ namespace storm {
virtual boost::any visit(InstantaneousRewardFormula const& f, boost::any const& data) const override;
virtual boost::any visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const override;
virtual boost::any visit(LongRunAverageRewardFormula const& f, boost::any const& data) const override;
+ virtual boost::any visit(MultiObjectiveFormula const& f, boost::any const& data) const override;
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;
diff --git a/src/parser/FormulaParser.cpp b/src/parser/FormulaParser.cpp
index db6e8a1ea..206d08b13 100644
--- a/src/parser/FormulaParser.cpp
+++ b/src/parser/FormulaParser.cpp
@@ -36,7 +36,8 @@ namespace storm {
("max", 4)
("F", 5)
("G", 6)
- ("X", 7);
+ ("X", 7)
+ ("multi", 8);
}
};
@@ -144,6 +145,8 @@ namespace storm {
qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> instantaneousRewardFormula;
qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> longRunAverageRewardFormula;
+ qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> multiObjectiveFormula;
+
// Parser that is used to recognize doubles only (as opposed to Spirit's double_ parser).
boost::spirit::qi::real_parser<double, boost::spirit::qi::strict_real_policies<double>> strict_double;
@@ -166,6 +169,7 @@ namespace storm {
std::shared_ptr<storm::logic::Formula const> createProbabilityOperatorFormula(storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr<storm::logic::Formula const> const& subformula);
std::shared_ptr<storm::logic::Formula const> createBinaryBooleanStateFormula(std::shared_ptr<storm::logic::Formula const> const& leftSubformula, std::shared_ptr<storm::logic::Formula const> const& rightSubformula, storm::logic::BinaryBooleanStateFormula::OperatorType operatorType);
std::shared_ptr<storm::logic::Formula const> createUnaryBooleanStateFormula(std::shared_ptr<storm::logic::Formula const> const& subformula, boost::optional<storm::logic::UnaryBooleanStateFormula::OperatorType> const& operatorType);
+ std::shared_ptr<storm::logic::Formula const> createMultiObjectiveFormula(std::vector<std::shared_ptr<storm::logic::Formula const>> const& subformulas);
// An error handler function.
phoenix::function<SpiritErrorHandler> handler;
@@ -340,7 +344,10 @@ namespace storm {
orStateFormula = andStateFormula[qi::_val = qi::_1] >> *(qi::lit("|") >> andStateFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createBinaryBooleanStateFormula, phoenix::ref(*this), qi::_val, qi::_1, storm::logic::BinaryBooleanStateFormula::OperatorType::Or)];
orStateFormula.name("or state formula");
- stateFormula = (orStateFormula);
+ multiObjectiveFormula = (qi::lit("multi") > qi::lit("(") >> (stateFormula % qi::lit(",")) >> qi::lit(")"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createMultiObjectiveFormula, phoenix::ref(*this), qi::_1)];
+ multiObjectiveFormula.name("Multi-objective formula");
+
+ stateFormula = (orStateFormula | multiObjectiveFormula);
stateFormula.name("state formula");
start = qi::eps > (stateFormula % +(qi::char_("\n;"))) >> qi::skip(boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - (qi::eol | qi::eoi)))[qi::eps] >> qi::eoi;
@@ -369,6 +376,7 @@ namespace storm {
debug(rewardPathFormula);
debug(cumulativeRewardFormula);
debug(instantaneousRewardFormula);
+ debug(multiObjectiveFormula);
*/
// Enable error reporting.
@@ -395,6 +403,7 @@ namespace storm {
qi::on_error<qi::fail>(rewardPathFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
qi::on_error<qi::fail>(cumulativeRewardFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
qi::on_error<qi::fail>(instantaneousRewardFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+ qi::on_error<qi::fail>(multiObjectiveFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
}
void FormulaParserGrammar::addIdentifierExpression(std::string const& identifier, storm::expressions::Expression const& expression) {
@@ -519,6 +528,10 @@ namespace storm {
return subformula;
}
}
+
+ std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createMultiObjectiveFormula(std::vector<std::shared_ptr<storm::logic::Formula const>> const& subformulas) {
+ return std::shared_ptr<storm::logic::Formula const>(new storm::logic::MultiObjectiveFormula(subformulas));
+ }
} // namespace parser
} // namespace storm
diff --git a/test/functional/parser/FormulaParserTest.cpp b/test/functional/parser/FormulaParserTest.cpp
index 1435806eb..da7d02804 100644
--- a/test/functional/parser/FormulaParserTest.cpp
+++ b/test/functional/parser/FormulaParserTest.cpp
@@ -148,3 +148,34 @@ TEST(FormulaParserTest, WrongFormatTest) {
input = "P>0.5 [F y!=0)]";
EXPECT_THROW(formula = formulaParser.parseSingleFormulaFromString(input), storm::exceptions::WrongFormatException);
}
+
+TEST(FormulaParserTest, MultiObjectiveFormulaTest) {
+ storm::parser::FormulaParser formulaParser;
+
+ std::string input = "multi(P<0.9 [ F \"a\" ], R<42 [ F \"b\" ], Pmin=? [ F\"c\" ])";
+ std::vector<std::shared_ptr<storm::logic::Formula const>> formulas;
+ ASSERT_NO_THROW(formulas = formulaParser.parseFromString(input));
+ ASSERT_EQ(1, formulas.size());
+ ASSERT_TRUE(formulas[0]->isMultiObjectiveFormula());
+ storm::logic::MultiObjectiveFormula mof = formulas[0]->asMultiObjectiveFormula();
+ ASSERT_EQ(3, mof.getNumberOfSubformulas());
+
+ ASSERT_TRUE(mof.getSubformula(0).isProbabilityOperatorFormula());
+ ASSERT_TRUE(mof.getSubformula(0).asProbabilityOperatorFormula().getSubformula().isEventuallyFormula());
+ ASSERT_TRUE(mof.getSubformula(0).asProbabilityOperatorFormula().getSubformula().asEventuallyFormula().getSubformula().isAtomicLabelFormula());
+ ASSERT_TRUE(mof.getSubformula(0).asProbabilityOperatorFormula().hasBound());
+ ASSERT_EQ(0.9, mof.getSubformula(0).asProbabilityOperatorFormula().getBound().threshold);
+
+ ASSERT_TRUE(mof.getSubformula(1).isRewardOperatorFormula());
+ ASSERT_TRUE(mof.getSubformula(1).asRewardOperatorFormula().getSubformula().isEventuallyFormula());
+ ASSERT_TRUE(mof.getSubformula(1).asRewardOperatorFormula().getSubformula().asEventuallyFormula().getSubformula().isAtomicLabelFormula());
+ ASSERT_TRUE(mof.getSubformula(1).asRewardOperatorFormula().hasBound());
+ ASSERT_EQ(42, mof.getSubformula(1).asRewardOperatorFormula().getBound().threshold);
+
+ ASSERT_TRUE(mof.getSubformula(2).isProbabilityOperatorFormula());
+ ASSERT_TRUE(mof.getSubformula(2).asProbabilityOperatorFormula().getSubformula().isEventuallyFormula());
+ ASSERT_TRUE(mof.getSubformula(2).asProbabilityOperatorFormula().getSubformula().asEventuallyFormula().getSubformula().isAtomicLabelFormula());
+ ASSERT_TRUE(mof.getSubformula(2).asProbabilityOperatorFormula().hasOptimalityType());
+ ASSERT_TRUE(storm::solver::minimize(mof.getSubformula(2).asProbabilityOperatorFormula().getOptimalityType()));
+
+}