diff --git a/src/storm-parsers/parser/FormulaParserGrammar.cpp b/src/storm-parsers/parser/FormulaParserGrammar.cpp index b6dde5a95..63de57930 100644 --- a/src/storm-parsers/parser/FormulaParserGrammar.cpp +++ b/src/storm-parsers/parser/FormulaParserGrammar.cpp @@ -134,14 +134,10 @@ namespace storm { quantileFormula = (qi::lit("quantile") > qi::lit("(") >> *(quantileBoundVariable) >> stateFormula > qi::lit(")"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createQuantileFormula, phoenix::ref(*this), qi::_1, qi::_2)]; quantileFormula.name("Quantile formula"); - coalitionOperator = (qi::lit("<<") - > *( (identifier[phoenix::push_back(qi::_a, qi::_1)] - | qi::int_[phoenix::push_back(qi::_a, qi::_1)]) % ',' - ) - > qi::lit(">>"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createCoalition, phoenix::ref(*this), qi::_a)]; - coalitionOperator.name("coalition operator"); + coalition = (-((identifier[phoenix::push_back(qi::_a, qi::_1)] | qi::uint_[phoenix::push_back(qi::_a, qi::_1)]) % ','))[qi::_val = phoenix::bind(&FormulaParserGrammar::createCoalition, phoenix::ref(*this), qi::_a)]; + coalition.name("coalition"); - gameFormula = (coalitionOperator > operatorFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createGameFormula, phoenix::ref(*this), qi::_1, qi::_2)]; + gameFormula = (qi::lit("<<") > coalition > qi::lit(">>") > operatorFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createGameFormula, phoenix::ref(*this), qi::_1, qi::_2)]; gameFormula.name("game formula"); stateFormula = (orStateFormula | multiFormula | quantileFormula | gameFormula); @@ -482,11 +478,11 @@ namespace storm { } } - storm::logic::Coalition FormulaParserGrammar::createCoalition(std::vector> const& playerIds) const { + storm::logic::Coalition FormulaParserGrammar::createCoalition(std::vector> const& playerIds) const { return storm::logic::Coalition(playerIds); } - std::shared_ptr FormulaParserGrammar::createGameFormula(storm::logic::Coalition coalition, std::shared_ptr const& subformula) const { + std::shared_ptr FormulaParserGrammar::createGameFormula(storm::logic::Coalition const& coalition, std::shared_ptr const& subformula) const { return std::shared_ptr(new storm::logic::GameFormula(coalition, subformula)); } } diff --git a/src/storm-parsers/parser/FormulaParserGrammar.h b/src/storm-parsers/parser/FormulaParserGrammar.h index 7693019d3..4e3ea1646 100644 --- a/src/storm-parsers/parser/FormulaParserGrammar.h +++ b/src/storm-parsers/parser/FormulaParserGrammar.h @@ -163,7 +163,7 @@ namespace storm { qi::rule(), Skipper> timeOperator; qi::rule(), Skipper> longRunAverageOperator; - qi::rule>>, Skipper> coalitionOperator; + qi::rule>>, Skipper> coalition; qi::rule filterProperty; qi::rule(), Skipper> simpleFormula; @@ -208,8 +208,8 @@ namespace storm { // Parser that is used to recognize doubles only (as opposed to Spirit's double_ parser). boost::spirit::qi::real_parser> strict_double; - storm::logic::Coalition createCoalition(std::vector> const& playerIds) const; - std::shared_ptr createGameFormula(storm::logic::Coalition coalition, std::shared_ptr const& subformula) const; + storm::logic::Coalition createCoalition(std::vector> const& playerIds) const; + std::shared_ptr createGameFormula(storm::logic::Coalition const& coalition, std::shared_ptr const& subformula) const; bool areConstantDefinitionsAllowed() const; void addConstant(std::string const& name, ConstantDataType type, boost::optional const& expression); diff --git a/src/storm/logic/FragmentChecker.cpp b/src/storm/logic/FragmentChecker.cpp index fb95572f9..94da18e87 100644 --- a/src/storm/logic/FragmentChecker.cpp +++ b/src/storm/logic/FragmentChecker.cpp @@ -191,7 +191,7 @@ namespace storm { boost::any FragmentChecker::visit(GameFormula const& f, boost::any const& data) const { InheritedInformation const& inherited = boost::any_cast(data); - bool result = inherited.getSpecification().areCoalitionOperatorsAllowed(); + bool result = inherited.getSpecification().areGameFormulasAllowed(); return result && boost::any_cast(f.getSubformula().accept(*this, data)); } diff --git a/src/storm/logic/FragmentSpecification.cpp b/src/storm/logic/FragmentSpecification.cpp index 6aa73cd5b..48b3ac14c 100644 --- a/src/storm/logic/FragmentSpecification.cpp +++ b/src/storm/logic/FragmentSpecification.cpp @@ -56,9 +56,11 @@ namespace storm { FragmentSpecification rpatl() { FragmentSpecification rpatl = prctl(); - // TODO disallow operator we currently do not support - rpatl.setCoalitionOperatorsAllowed(true); - + // TODO: disallow formulas we currently do not support + // TODO: Only allow OperatorFormulas when they are inside of a GameFormula? + // TODO: Require that operator formulas are required at the top level of a GameFormula? + rpatl.setGameFormulasAllowed(true); + return rpatl; } @@ -175,6 +177,8 @@ namespace storm { reachabilityTimeFormula = false; + gameFormula = false; + nestedOperators = true; nestedPathFormulas = false; nestedMultiObjectiveFormulas = false; @@ -629,15 +633,14 @@ namespace storm { return *this; } - bool FragmentSpecification::areCoalitionOperatorsAllowed() const { - return coalitionOperator; + bool FragmentSpecification::areGameFormulasAllowed() const { + return gameFormula; } - FragmentSpecification& FragmentSpecification::setCoalitionOperatorsAllowed(bool newValue) { - coalitionOperator = newValue; + FragmentSpecification& FragmentSpecification::setGameFormulasAllowed(bool newValue) { + gameFormula = newValue; return *this; } - } } diff --git a/src/storm/logic/FragmentSpecification.h b/src/storm/logic/FragmentSpecification.h index 830c2a9a0..19cf232ed 100644 --- a/src/storm/logic/FragmentSpecification.h +++ b/src/storm/logic/FragmentSpecification.h @@ -154,10 +154,9 @@ namespace storm { bool isRewardAccumulationAllowed() const; FragmentSpecification& setRewardAccumulationAllowed(bool newValue); - bool areCoalitionOperatorsAllowed() const; - FragmentSpecification& setCoalitionOperatorsAllowed(bool newValue); - - + bool areGameFormulasAllowed() const; + FragmentSpecification& setGameFormulasAllowed(bool newValue); + FragmentSpecification& setOperatorsAllowed(bool newValue); FragmentSpecification& setTimeAllowed(bool newValue); FragmentSpecification& setLongRunAverageProbabilitiesAllowed(bool newValue); @@ -195,7 +194,7 @@ namespace storm { bool reachabilityTimeFormula; - bool coalitionOperator; + bool gameFormula; // Members that indicate certain restrictions. bool nestedOperators; diff --git a/src/storm/logic/LiftableTransitionRewardsVisitor.cpp b/src/storm/logic/LiftableTransitionRewardsVisitor.cpp index bdb8ba58e..22ff54cdd 100644 --- a/src/storm/logic/LiftableTransitionRewardsVisitor.cpp +++ b/src/storm/logic/LiftableTransitionRewardsVisitor.cpp @@ -76,7 +76,9 @@ namespace storm { } boost::any LiftableTransitionRewardsVisitor::visit(GameFormula const& f, boost::any const& data) const { - return true; + STORM_LOG_WARN("Transitionbranch-based rewards might be reduced to action-based rewards. Be sure that this is correct for your property."); + // TODO: Check if this is correct + return f.getSubformula().accept(*this, data); } boost::any LiftableTransitionRewardsVisitor::visit(InstantaneousRewardFormula const&, boost::any const&) const { diff --git a/src/storm/storage/jani/JSONExporter.cpp b/src/storm/storage/jani/JSONExporter.cpp index 4236f4c6f..ee2487002 100644 --- a/src/storm/storage/jani/JSONExporter.cpp +++ b/src/storm/storage/jani/JSONExporter.cpp @@ -333,7 +333,7 @@ namespace storm { } boost::any FormulaToJaniJson::visit(storm::logic::GameFormula const& f, boost::any const& data) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "We currently do not support conversion of game formulas to Jani. (Does jani support games?)"); + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Conversion of game formulas to Jani is not supported."); } boost::any FormulaToJaniJson::visit(storm::logic::InstantaneousRewardFormula const&, boost::any const&) const {