From a16eee4982de32ab258ffb5ae4158ca106fb7a5e Mon Sep 17 00:00:00 2001 From: TimQu Date: Fri, 18 Aug 2017 18:24:35 +0200 Subject: [PATCH] made multi(..) path formulas pass the fragment check --- src/storm/logic/FragmentChecker.cpp | 2 +- src/storm/logic/FragmentSpecification.cpp | 3 ++- src/storm/parser/FormulaParserGrammar.cpp | 2 +- 3 files changed, 4 insertions(+), 3 deletions(-) diff --git a/src/storm/logic/FragmentChecker.cpp b/src/storm/logic/FragmentChecker.cpp index 6fc458796..63a6ffd78 100644 --- a/src/storm/logic/FragmentChecker.cpp +++ b/src/storm/logic/FragmentChecker.cpp @@ -202,7 +202,7 @@ namespace storm { bool result = inherited.getSpecification().areProbabilityOperatorsAllowed(); result = result && (!f.hasQualitativeResult() || inherited.getSpecification().areQualitativeOperatorResultsAllowed()); result = result && (!f.hasQuantitativeResult() || inherited.getSpecification().areQuantitativeOperatorResultsAllowed()); - result = result && (f.getSubformula().isProbabilityPathFormula() || f.getSubformula().isConditionalProbabilityFormula()); + result = result && (f.getSubformula().isProbabilityPathFormula() || f.getSubformula().isConditionalProbabilityFormula() || f.getSubformula().isMultiObjectiveFormula()); if (!inherited.getSpecification().areNestedOperatorsAllowed()) { result = result && boost::any_cast(f.getSubformula().accept(*this, InheritedInformation(inherited.getSpecification().copy().setOperatorsAllowed(false)))); } else { diff --git a/src/storm/logic/FragmentSpecification.cpp b/src/storm/logic/FragmentSpecification.cpp index 11a3ac2f4..eba4087e3 100644 --- a/src/storm/logic/FragmentSpecification.cpp +++ b/src/storm/logic/FragmentSpecification.cpp @@ -89,7 +89,8 @@ namespace storm { multiObjective.setMultiObjectiveFormulasAllowed(true); multiObjective.setMultiObjectiveFormulaAtTopLevelRequired(true); - multiObjective.setOperatorsAtTopLevelOfMultiObjectiveFormulasRequired(true); + multiObjective.setNestedMultiObjectiveFormulasAllowed(true); + multiObjective.setOperatorsAtTopLevelOfMultiObjectiveFormulasRequired(false); multiObjective.setProbabilityOperatorsAllowed(true); multiObjective.setUntilFormulasAllowed(true); multiObjective.setGloballyFormulasAllowed(true); diff --git a/src/storm/parser/FormulaParserGrammar.cpp b/src/storm/parser/FormulaParserGrammar.cpp index 33e27e9c8..30b4f4e38 100644 --- a/src/storm/parser/FormulaParserGrammar.cpp +++ b/src/storm/parser/FormulaParserGrammar.cpp @@ -113,7 +113,7 @@ 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"); - multiObjectiveFormula = (qi::lit("multi") > qi::lit("(") >> (stateFormula % qi::lit(",")) >> qi::lit(")"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createMultiObjectiveFormula, phoenix::ref(*this), qi::_1)]; + multiObjectiveFormula = (qi::lit("multi") > qi::lit("(") >> ((pathFormula(storm::logic::FormulaContext::Probability) | stateFormula) % qi::lit(",")) >> qi::lit(")"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createMultiObjectiveFormula, phoenix::ref(*this), qi::_1)]; multiObjectiveFormula.name("Multi-objective formula"); stateFormula = (orStateFormula | multiObjectiveFormula);