From 4cf2fd7d61521fbc7101bcff54445341f0878fa7 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Tue, 13 Apr 2021 15:56:32 +0200 Subject: [PATCH] Heavily refactored FormulaParser as it had become quite messy. LTL-Operator precedence should now correctly mimic the behavior of PRISM. --- .../parser/FormulaParserGrammar.cpp | 520 ++++++++++-------- .../parser/FormulaParserGrammar.h | 201 ++++--- 2 files changed, 400 insertions(+), 321 deletions(-) diff --git a/src/storm-parsers/parser/FormulaParserGrammar.cpp b/src/storm-parsers/parser/FormulaParserGrammar.cpp index d768fab9b..0b1ce85ab 100644 --- a/src/storm-parsers/parser/FormulaParserGrammar.cpp +++ b/src/storm-parsers/parser/FormulaParserGrammar.cpp @@ -17,81 +17,98 @@ namespace storm { void FormulaParserGrammar::initialize() { // Register all variables so we can parse them in the expressions. for (auto variableTypePair : *constManager) { - identifiers_.add(variableTypePair.first.getName(), variableTypePair.first); + addIdentifierExpression(variableTypePair.first.getName(), variableTypePair.first); } // Set the identifier mapping to actually generate expressions. expressionParser.setIdentifierMapping(&identifiers_); - longRunAverageRewardFormula = (qi::lit("LRA") | qi::lit("S") | qi::lit("MP"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createLongRunAverageRewardFormula, phoenix::ref(*this))]; - longRunAverageRewardFormula.name("long run average reward formula"); - - instantaneousRewardFormula = (qi::lit("I=") > expressionParser)[qi::_val = phoenix::bind(&FormulaParserGrammar::createInstantaneousRewardFormula, phoenix::ref(*this), qi::_1)]; - instantaneousRewardFormula.name("instantaneous reward formula"); - - cumulativeRewardFormula = (qi::lit("C") >> timeBounds)[qi::_val = phoenix::bind(&FormulaParserGrammar::createCumulativeRewardFormula, phoenix::ref(*this), qi::_1)]; - cumulativeRewardFormula.name("cumulative reward formula"); - - totalRewardFormula = (qi::lit("C"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createTotalRewardFormula, phoenix::ref(*this))]; - totalRewardFormula.name("total reward formula"); - - rewardPathFormula = longRunAverageRewardFormula | conditionalFormula(storm::logic::FormulaContext::Reward) | eventuallyFormula(storm::logic::FormulaContext::Reward) | cumulativeRewardFormula | instantaneousRewardFormula | totalRewardFormula; - rewardPathFormula.name("reward path formula"); - - expressionFormula = expressionParser[qi::_val = phoenix::bind(&FormulaParserGrammar::createAtomicExpressionFormula, phoenix::ref(*this), qi::_1)]; - expressionFormula.name("expression formula"); - - label = qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_')))]]]; + keywords_.name("keyword"); + nonStandardKeywords_.name("non-standard Storm-specific keyword"); + relationalOperator_.name("relational operator"); + optimalityOperator_.name("optimality operator"); + rewardMeasureType_.name("reward measure"); + operatorKeyword_.name("Operator keyword"); + filterType_.name("filter type"); + + // Auxiliary helpers + isPathFormula = qi::eps(qi::_r1 == FormulaKind::Path); + noAmbiguousNonAssociativeOperator = !(qi::lit(qi::_r2)[qi::_pass = phoenix::bind(&FormulaParserGrammar::raiseAmbiguousNonAssociativeOperatorError, phoenix::ref(*this), qi::_r1, qi::_r2)]); + noAmbiguousNonAssociativeOperator.name("no ambiguous non-associative operator"); + identifier %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_') | qi::char_('.')) >> *(qi::alnum | qi::char_('_')))]]]; + identifier.name("identifier"); + label %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_')))]]]; label.name("label"); + quotedString %= qi::as_string[qi::lexeme[qi::omit[qi::char_('"')] > qi::raw[*(!qi::char_('"') >> qi::char_)] > qi::omit[qi::lit('"')]]]; + quotedString.name("quoted string"); + + // PCTL-like Operator Formulas + operatorInformation = (-optimalityOperator_)[qi::_a = qi::_1] >> + ((qi::lit("=") > qi::lit("?"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createOperatorInformation, phoenix::ref(*this), qi::_a, boost::none, boost::none)] + | (relationalOperator_ > expressionParser)[qi::_val = phoenix::bind(&FormulaParserGrammar::createOperatorInformation, phoenix::ref(*this), qi::_a, qi::_1, qi::_2)] + ); + operatorInformation.name("operator information"); + operatorSubFormula = (( (qi::eps(qi::_r1 == storm::logic::FormulaContext::Probability) > formula(FormulaKind::Path, qi::_r1)) + | (qi::eps(qi::_r1 == storm::logic::FormulaContext::Reward) > (longRunAverageRewardFormula | eventuallyFormula( qi::_r1) | cumulativeRewardFormula | instantaneousRewardFormula | totalRewardFormula)) + | (qi::eps(qi::_r1 == storm::logic::FormulaContext::Time) > eventuallyFormula(qi::_r1)) + | (qi::eps(qi::_r1 == storm::logic::FormulaContext::LongRunAverage) > formula(FormulaKind::State, storm::logic::FormulaContext::LongRunAverage)) + ) >> -(qi::lit("||") > formula(FormulaKind::Path, storm::logic::FormulaContext::Probability)) + )[qi::_val = phoenix::bind(&FormulaParserGrammar::createConditionalFormula, phoenix::ref(*this), qi::_1, qi::_2, qi::_r1)]; + operatorSubFormula.name("operator subformula"); + rewardModelName = qi::eps(qi::_r1 == storm::logic::FormulaContext::Reward) >> (qi::lit("{\"") > label > qi::lit("\"}")); + rewardModelName.name("reward model name"); + rewardMeasureType = qi::eps(qi::_r1 == storm::logic::FormulaContext::Reward || qi::_r1 == storm::logic::FormulaContext::Time) >> qi::lit("[") >> rewardMeasureType_ >> qi::lit("]"); + rewardMeasureType.name("reward measure type"); + operatorFormula = (operatorKeyword_[qi::_a = qi::_1] > -rewardMeasureType(qi::_a) > -rewardModelName(qi::_a) > operatorInformation > qi::lit("[") > operatorSubFormula(qi::_a) > qi::lit("]")) + [qi::_val = phoenix::bind(&FormulaParserGrammar::createOperatorFormula, phoenix::ref(*this), qi::_a, qi::_2, qi::_3, qi::_4, qi::_5)]; + operatorFormula.name("operator formula"); + + // Atomic propositions labelFormula = (qi::lit("\"") >> label >> qi::lit("\""))[qi::_val = phoenix::bind(&FormulaParserGrammar::createAtomicLabelFormula, phoenix::ref(*this), qi::_1)]; labelFormula.name("label formula"); - booleanLiteralFormula = (qi::lit("true")[qi::_a = true] | qi::lit("false")[qi::_a = false])[qi::_val = phoenix::bind(&FormulaParserGrammar::createBooleanLiteralFormula, phoenix::ref(*this), qi::_a)]; booleanLiteralFormula.name("boolean literal formula"); - - operatorFormula = probabilityOperator | rewardOperator | longRunAverageOperator | timeOperator; - operatorFormula.name("operator formulas"); - - atomicStateFormula = booleanLiteralFormula | labelFormula | expressionFormula | (qi::lit("(") > untilFormula(qi::_r1) > qi::lit(")")) | operatorFormula; - atomicStateFormula.name("atomic state formula"); - - atomicStateFormulaWithoutExpression = booleanLiteralFormula | labelFormula | (qi::lit("(") > untilFormula(qi::_r1) > qi::lit(")")) | operatorFormula; - atomicStateFormula.name("atomic state formula without expression"); - - notStateFormula = (unaryBooleanOperator_ >> atomicStateFormulaWithoutExpression(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createUnaryBooleanStateOrPathFormula, phoenix::ref(*this), qi::_2, qi::_1)] | atomicStateFormula(qi::_r1)[qi::_val = qi::_1]; - notStateFormula.name("negation formula"); - - eventuallyFormula = (qi::lit("F") >> (-timeBounds) >> pathFormulaWithoutUntil(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createEventuallyFormula, phoenix::ref(*this), qi::_1, qi::_r1, qi::_2)]; - eventuallyFormula.name("eventually formula"); - - globallyFormula = (qi::lit("G") >> (-timeBounds) >> pathFormulaWithoutUntil(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createGloballyFormula, phoenix::ref(*this), qi::_1, qi::_2)]; - globallyFormula.name("globally formula"); - - nextFormula = (qi::lit("X") >> pathFormulaWithoutUntil(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createNextFormula, phoenix::ref(*this), qi::_1)]; - nextFormula.name("next formula"); - - pathFormulaWithoutUntil = eventuallyFormula(qi::_r1) | globallyFormula(qi::_r1) | nextFormula(qi::_r1) | stateFormula(qi::_r1); - pathFormulaWithoutUntil.name("path formula"); - - untilFormula = pathFormulaWithoutUntil(qi::_r1)[qi::_val = qi::_1] >> *(qi::lit("U") >> (-timeBounds) >> pathFormulaWithoutUntil(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createUntilFormula, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)]; - untilFormula.name("until formula"); - - hoaPathFormula = qi::lit("HOA:") > qi::lit("{") - > quotedString[qi::_val = phoenix::bind(&FormulaParserGrammar::createHOAPathFormula, phoenix::ref(*this), qi::_1)] - >> *(qi::lit(",") > quotedString > qi::lit("->") > stateFormula(qi::_r1) )[phoenix::bind(&FormulaParserGrammar::addHoaAPMapping, phoenix::ref(*this), *qi::_val, qi::_1, qi::_2)] - > qi::lit("}"); - - basicPathFormula = (hoaPathFormula(qi::_r1)[qi::_val = qi::_1]) | untilFormula(qi::_r1)[qi::_val = qi::_1]; + expressionFormula = expressionParser[qi::_val = phoenix::bind(&FormulaParserGrammar::createAtomicExpressionFormula, phoenix::ref(*this), qi::_1)]; + expressionFormula.name("expression formula"); + atomicPropositionFormula = (booleanLiteralFormula | labelFormula | expressionFormula); + atomicPropositionFormula.name("atomic proposition"); + + // Propositional Logic operators + // To correctly parse the operator precedences (! binds stronger than & binds stronger than |), we run through different "precedence levels" starting with the weakest binding operator. + basicPropositionalFormula = (qi::lit("(") >> (formula(qi::_r1, qi::_r2) > qi::lit(")"))) + | atomicPropositionFormula // Should be checked before operator formulas and others. Otherwise, e.g. variable "Random" would be parsed as reward operator 'R' (followed by andom) + | negationPropositionalFormula(qi::_r1, qi::_r2) + | operatorFormula + | multiOperatorFormula + | quantileFormula + | gameFormula + | (isPathFormula(qi::_r1) >> prefixOperatorPathFormula(qi::_r2)); // Needed for e.g. F "a" & X "a" = F ("a" & (X "a")) + negationPropositionalFormula = (qi::lit("!") > basicPropositionalFormula(qi::_r1, qi::_r2))[qi::_val = phoenix::bind(&FormulaParserGrammar::createUnaryBooleanStateOrPathFormula, phoenix::ref(*this), qi::_1, storm::logic::UnaryBooleanOperatorType::Not)]; + basicPropositionalFormula.name("basic propositional formula"); + andLevelPropositionalFormula = basicPropositionalFormula(qi::_r1, qi::_r2)[qi::_val = qi::_1] + >> *( qi::lit("&") + > basicPropositionalFormula(qi::_r1, qi::_r2)[qi::_val = phoenix::bind(&FormulaParserGrammar::createBinaryBooleanStateOrPathFormula, phoenix::ref(*this), qi::_val, qi::_1, storm::logic::BinaryBooleanStateFormula::OperatorType::And)]); + andLevelPropositionalFormula.name("and precedence level propositional formula"); + orLevelPropositionalFormula = andLevelPropositionalFormula(qi::_r1, qi::_r2)[qi::_val = qi::_1] + >> *( (!qi::lit("||") >> qi::lit("|")) // Make sure to not confuse with conditional operator "||" + > andLevelPropositionalFormula(qi::_r1, qi::_r2)[qi::_val = phoenix::bind(&FormulaParserGrammar::createBinaryBooleanStateOrPathFormula, phoenix::ref(*this), qi::_val, qi::_1, storm::logic::BinaryBooleanStateFormula::OperatorType::Or)]); + orLevelPropositionalFormula.name("or precedence level propositional formula"); + propositionalFormula = orLevelPropositionalFormula(qi::_r1, qi::_r2); + + // Path operators + // Again need to parse precedences correctly. Propositional formulae bind stronger than temporal operators. + basicPathFormula = propositionalFormula(FormulaKind::Path, qi::_r1) // Bracketed case is handled here as well + | prefixOperatorPathFormula(qi::_r1); // Needs to be checked *after* atomic expression formulas. Otherwise e.g. variable Fail would be parsed as "F (ail)" + prefixOperatorPathFormula = eventuallyFormula(qi::_r1) + | nextFormula(qi::_r1) + | globallyFormula(qi::_r1) + | hoaPathFormula(qi::_r1) + | multiBoundedPathFormula(qi::_r1); basicPathFormula.name("basic path formula"); - - conditionalFormula = basicPathFormula(qi::_r1)[qi::_val = qi::_1] >> *(qi::lit("||") >> basicPathFormula(storm::logic::FormulaContext::Probability))[qi::_val = phoenix::bind(&FormulaParserGrammar::createConditionalFormula, phoenix::ref(*this), qi::_val, qi::_1, qi::_r1)]; - conditionalFormula.name("conditional formula"); - - timeBoundReference = (-qi::lit("rew") >> rewardModelName)[qi::_val = phoenix::bind(&FormulaParserGrammar::createTimeBoundReference, phoenix::ref(*this), storm::logic::TimeBoundType::Reward, qi::_1)] + timeBoundReference = (-qi::lit("rew") >> rewardModelName(storm::logic::FormulaContext::Reward))[qi::_val = phoenix::bind(&FormulaParserGrammar::createTimeBoundReference, phoenix::ref(*this), storm::logic::TimeBoundType::Reward, qi::_1)] | (qi::lit("steps"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createTimeBoundReference, phoenix::ref(*this), storm::logic::TimeBoundType::Steps, boost::none)] | (-qi::lit("time"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createTimeBoundReference, phoenix::ref(*this), storm::logic::TimeBoundType::Time, boost::none)]; timeBoundReference.name("time bound reference"); - timeBound = ((timeBoundReference >> qi::lit("[")) > expressionParser > qi::lit(",") > expressionParser > qi::lit("]")) [qi::_val = phoenix::bind(&FormulaParserGrammar::createTimeBoundFromInterval, phoenix::ref(*this), qi::_2, qi::_3, qi::_1)] | ( timeBoundReference >> (qi::lit("<=")[qi::_a = true, qi::_b = false] | qi::lit("<")[qi::_a = true, qi::_b = true] | qi::lit(">=")[qi::_a = false, qi::_b = false] | qi::lit(">")[qi::_a = false, qi::_b = true]) >> expressionParser) @@ -99,79 +116,63 @@ namespace storm { | ( timeBoundReference >> qi::lit("=") >> expressionParser) [qi::_val = phoenix::bind(&FormulaParserGrammar::createTimeBoundFromInterval, phoenix::ref(*this), qi::_2, qi::_2, qi::_1)]; timeBound.name("time bound"); - timeBounds = (timeBound % qi::lit(",")) | (((-qi::lit("^") >> qi::lit("{")) >> (timeBound % qi::lit(","))) >> qi::lit("}")); timeBounds.name("time bounds"); - - pathFormula = conditionalFormula(qi::_r1); + eventuallyFormula = (qi::lit("F") > (-timeBounds) > basicPathFormula(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createEventuallyFormula, phoenix::ref(*this), qi::_1, qi::_r1, qi::_2)]; + eventuallyFormula.name("eventually formula"); + nextFormula = (qi::lit("X") > basicPathFormula(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createNextFormula, phoenix::ref(*this), qi::_1)]; + nextFormula.name("next formula"); + globallyFormula = (qi::lit("G") > basicPathFormula(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createGloballyFormula, phoenix::ref(*this), qi::_1)]; + globallyFormula.name("globally formula"); + hoaPathFormula = qi::lit("HOA:") > qi::lit("{") + > quotedString[qi::_val = phoenix::bind(&FormulaParserGrammar::createHOAPathFormula, phoenix::ref(*this), qi::_1)] + >> *(qi::lit(",") > quotedString > qi::lit("->") > formula(FormulaKind::Path, qi::_r1) )[phoenix::bind(&FormulaParserGrammar::addHoaAPMapping, phoenix::ref(*this), *qi::_val, qi::_1, qi::_2)] + > qi::lit("}"); + multiBoundedPathFormulaOperand = pathFormula(qi::_r1)[qi::_pass = phoenix::bind(&FormulaParserGrammar::isValidMultiBoundedPathFormulaOperand, phoenix::ref(*this), qi::_val)]; + multiBoundedPathFormulaOperand.name("multi bounded path formula operand"); + multiBoundedPathFormula = (qi::lit("multi") > qi::lit("(") >> (multiBoundedPathFormulaOperand(qi::_r1) % qi::lit(",")) >> qi::lit(")"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createMultiBoundedPathFormula, phoenix::ref(*this), qi::_1)]; + multiBoundedPathFormula.name("multi bounded path formula"); + untilLevelPathFormula = basicPathFormula(qi::_r1)[qi::_val = qi::_1] + >> -( (qi::lit("U") + > (-timeBounds) > basicPathFormula(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createUntilFormula, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)]) + >> (qi::eps > noAmbiguousNonAssociativeOperator(qi::_val,std::string("U"))); // Do not parse a U b U c + untilLevelPathFormula.name("until precedence level path formula"); + pathFormula = untilLevelPathFormula(qi::_r1); pathFormula.name("path formula"); - - rewardMeasureType = qi::lit("[") >> rewardMeasureType_ >> qi::lit("]"); - rewardMeasureType.name("reward measure type"); - - operatorInformation = (-optimalityOperator_[qi::_a = qi::_1] >> ((relationalOperator_[qi::_b = qi::_1] > expressionParser[qi::_c = qi::_1]) | (qi::lit("=") > qi::lit("?"))))[qi::_val = phoenix::bind(&FormulaParserGrammar::createOperatorInformation, phoenix::ref(*this), qi::_a, qi::_b, qi::_c)]; - operatorInformation.name("operator information"); - - longRunAverageOperator = ((qi::lit("LRA") | qi::lit("S")) > operatorInformation > qi::lit("[") > stateFormula(storm::logic::FormulaContext::LongRunAverage) > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createLongRunAverageOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)]; - longRunAverageOperator.name("long-run average operator"); - - rewardModelName = qi::lit("{\"") > label > qi::lit("\"}"); - rewardModelName.name("reward model name"); - - rewardOperator = (qi::lit("R") > -rewardMeasureType > -rewardModelName > operatorInformation > qi::lit("[") > rewardPathFormula > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createRewardOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2, qi::_3, qi::_4)]; - rewardOperator.name("reward operator"); - - timeOperator = (qi::lit("T") > -rewardMeasureType > operatorInformation > qi::lit("[") > eventuallyFormula(storm::logic::FormulaContext::Time) > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createTimeOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2, qi::_3)]; - timeOperator.name("time operator"); - - probabilityOperator = (qi::lit("P") > operatorInformation > qi::lit("[") > pathFormula(storm::logic::FormulaContext::Probability) > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createProbabilityOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)]; - probabilityOperator.name("probability operator"); - - andStateFormula = notStateFormula(qi::_r1)[qi::_val = qi::_1] >> *(qi::lit("&") >> notStateFormula(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createBinaryBooleanStateOrPathFormula, phoenix::ref(*this), qi::_val, qi::_1, storm::logic::BinaryBooleanStateFormula::OperatorType::And)]; - andStateFormula.name("and state formula"); - - orStateFormula = andStateFormula(qi::_r1)[qi::_val = qi::_1] >> *(qi::lit("|") >> andStateFormula(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createBinaryBooleanStateOrPathFormula, phoenix::ref(*this), qi::_val, qi::_1, storm::logic::BinaryBooleanStateFormula::OperatorType::Or)]; - orStateFormula.name("or state formula"); - - multiFormula = (qi::lit("multi") > qi::lit("(") >> ((pathFormula(storm::logic::FormulaContext::Probability) | stateFormula(storm::logic::FormulaContext::Probability)) % qi::lit(",")) >> qi::lit(")"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createMultiFormula, phoenix::ref(*this), qi::_1)]; - multiFormula.name("Multi formula"); - - identifier %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_') | qi::char_('.')) >> *(qi::alnum | qi::char_('_')))]]]; - identifier.name("identifier"); - - quantileBoundVariable = (-(qi::lit("min")[qi::_a = storm::solver::OptimizationDirection::Minimize] | qi::lit("max")[qi::_a = storm::solver::OptimizationDirection::Maximize]) >> identifier >> qi::lit(","))[qi::_val = phoenix::bind(&FormulaParserGrammar::createQuantileBoundVariables, phoenix::ref(*this), qi::_a, qi::_1)]; - quantileBoundVariable.name("quantile bound variable"); - quantileFormula = (qi::lit("quantile") > qi::lit("(") >> *(quantileBoundVariable) >> stateFormula(storm::logic::FormulaContext::Undefined) > qi::lit(")"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createQuantileFormula, phoenix::ref(*this), qi::_1, qi::_2)]; - quantileFormula.name("Quantile formula"); - + + // Quantitative path formulae (reward) + longRunAverageRewardFormula = (qi::lit("LRA") | qi::lit("S") | qi::lit("MP"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createLongRunAverageRewardFormula, phoenix::ref(*this))]; + longRunAverageRewardFormula.name("long run average reward formula"); + instantaneousRewardFormula = (qi::lit("I=") > expressionParser)[qi::_val = phoenix::bind(&FormulaParserGrammar::createInstantaneousRewardFormula, phoenix::ref(*this), qi::_1)]; + instantaneousRewardFormula.name("instantaneous reward formula"); + cumulativeRewardFormula = (qi::lit("C") >> timeBounds)[qi::_val = phoenix::bind(&FormulaParserGrammar::createCumulativeRewardFormula, phoenix::ref(*this), qi::_1)]; + cumulativeRewardFormula.name("cumulative reward formula"); + totalRewardFormula = (qi::lit("C"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createTotalRewardFormula, phoenix::ref(*this))]; + totalRewardFormula.name("total reward formula"); + + // Game Formulae playerCoalition = (-((identifier[phoenix::push_back(qi::_a, qi::_1)] | qi::uint_[phoenix::push_back(qi::_a, qi::_1)]) % ','))[qi::_val = phoenix::bind(&FormulaParserGrammar::createPlayerCoalition, phoenix::ref(*this), qi::_a)]; playerCoalition.name("player coalition"); - gameFormula = (qi::lit("<<") > playerCoalition > qi::lit(">>") > operatorFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createGameFormula, phoenix::ref(*this), qi::_1, qi::_2)]; gameFormula.name("game formula"); - - shieldExpression = (qi::lit("<") > label > qi::lit(",") > shieldingType > -(qi::lit(",") > shieldComparison) > qi::lit(">"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createShieldExpression, phoenix::ref(*this), qi::_2, qi::_1, qi::_3)]; - - shieldExpression.name("shield expression"); - - shieldingType = (qi::lit("PreSafety")[qi::_val = storm::logic::ShieldingType::PreSafety] | - qi::lit("PostSafety")[qi::_val = storm::logic::ShieldingType::PostSafety] | - qi::lit("Optimal")[qi::_val = storm::logic::ShieldingType::Optimal]) > -qi::lit("Shield"); - shieldingType.name("shielding type"); - - probability = qi::double_[qi::_pass = (qi::_1 >= 0) & (qi::_1 <= 1.0), qi::_val = qi::_1 ]; - probability.name("double between 0 and 1"); - - shieldComparison = ((qi::lit("lambda")[qi::_a = storm::logic::ShieldComparison::Relative] | - qi::lit("gamma")[qi::_a = storm::logic::ShieldComparison::Absolute]) > qi::lit("=") > probability)[qi::_val = phoenix::bind(&FormulaParserGrammar::createShieldComparisonStruct, phoenix::ref(*this), qi::_a, qi::_1)]; - shieldComparison.name("shield comparison type"); - - stateFormula = (orStateFormula(qi::_r1) | multiFormula | quantileFormula); - stateFormula.name("state formula"); - - quotedString %= qi::as_string[qi::lexeme[qi::omit[qi::char_('"')] > qi::raw[*(!qi::char_('"') >> qi::char_)] > qi::omit[qi::lit('"')]]]; - quotedString.name("quoted string"); - + + // Multi-objective, quantiles + multiOperatorFormula = (qi::lit("multi") > qi::lit("(") + > (operatorFormula % qi::lit(",")) + > qi::lit(")"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createMultiOperatorFormula, phoenix::ref(*this), qi::_1)]; + multiOperatorFormula.name("multi-objective operator formula"); + quantileBoundVariable = (-optimalityOperator_ > identifier > qi::lit(","))[qi::_val = phoenix::bind(&FormulaParserGrammar::createQuantileBoundVariables, phoenix::ref(*this), qi::_1, qi::_2)]; + quantileBoundVariable.name("quantile bound variable"); + quantileFormula = (qi::lit("quantile") > qi::lit("(") > *(quantileBoundVariable) > operatorFormula[qi::_pass = phoenix::bind(&FormulaParserGrammar::isBooleanReturnType, phoenix::ref(*this), qi::_1, true)] > qi::lit(")"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createQuantileFormula, phoenix::ref(*this), qi::_1, qi::_2)]; + quantileFormula.name("Quantile formula"); + + // General formulae + formula = (isPathFormula(qi::_r1) >> pathFormula(qi::_r2) | propositionalFormula(qi::_r1, qi::_r2)); + formula.name("formula"); + + topLevelFormula = formula(FormulaKind::State, storm::logic::FormulaContext::Undefined); + topLevelFormula.name("top-level formula"); + formulaName = qi::lit("\"") >> identifier >> qi::lit("\"") >> qi::lit(":"); formulaName.name("formula name"); @@ -182,8 +183,9 @@ namespace storm { #pragma clang diagnostic push #pragma clang diagnostic ignored "-Woverloaded-shift-op-parentheses" - - filterProperty = (-formulaName >> qi::lit("filter") > qi::lit("(") > filterType_ > qi::lit(",") > stateFormula(storm::logic::FormulaContext::Undefined) > qi::lit(",") > stateFormula(storm::logic::FormulaContext::Undefined) > qi::lit(")"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createProperty, phoenix::ref(*this), qi::_1, qi::_2, qi::_3, qi::_4)] | (-formulaName >> stateFormula(storm::logic::FormulaContext::Undefined))[qi::_val = phoenix::bind(&FormulaParserGrammar::createPropertyWithDefaultFilterTypeAndStates, phoenix::ref(*this), qi::_1, qi::_2)] | (-formulaName >> shieldExpression >> stateFormula(storm::logic::FormulaContext::Undefined))[qi::_val = phoenix::bind(&FormulaParserGrammar::createShieldingProperty, phoenix::ref(*this), qi::_1, qi::_3, qi::_2)]; + + filterProperty = (-formulaName >> qi::lit("filter") > qi::lit("(") > filterType_ > qi::lit(",") > topLevelFormula > qi::lit(",") > formula(FormulaKind::State, storm::logic::FormulaContext::Undefined)> qi::lit(")"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createProperty, phoenix::ref(*this), qi::_1, qi::_2, qi::_3, qi::_4)] | + (-formulaName >> topLevelFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createPropertyWithDefaultFilterTypeAndStates, phoenix::ref(*this), qi::_1, qi::_2)]; filterProperty.name("filter property"); #pragma clang diagnostic pop @@ -195,62 +197,91 @@ namespace storm { start.name("start"); // Enable the following lines to print debug output for most the rules. - //debug(start); - //debug(constantDefinition); - //debug(stateFormula); - //debug(orStateFormula); - //debug(andStateFormula); - //debug(probabilityOperator); - //debug(rewardOperator); - //debug(longRunAverageOperator); - //debug(timeOperator); - //debug(pathFormulaWithoutUntil); - //debug(pathFormula); - //debug(conditionalFormula); - //debug(nextFormula); - //debug(globallyFormula); - //debug(eventuallyFormula); - //debug(atomicStateFormula); - //debug(booleanLiteralFormula); - //debug(labelFormula); - //debug(expressionFormula); - //debug(rewardPathFormula); - //debug(cumulativeRewardFormula); - //debug(totalRewardFormula); - //debug(instantaneousRewardFormula); - //debug(multiFormula); - +// debug(rewardModelName) +// debug(rewardMeasureType) +// debug(operatorFormula) +// debug(labelFormula) +// debug(expressionFormula) +// debug(booleanLiteralFormula) +// debug(atomicPropositionFormula) +// debug(basicPropositionalFormula) +// debug(negationPropositionalFormula) +// debug(andLevelPropositionalFormula) +// debug(orLevelPropositionalFormula) +// debug(propositionalFormula) +// debug(timeBoundReference) +// debug(timeBound) +// debug(timeBounds) +// debug(eventuallyFormula) +// debug(nextFormula) +// debug(globallyFormula) +// debug(hoaPathFormula) +// debug(multiBoundedPathFormula) +// debug(prefixOperatorPathFormula) +// debug(basicPathFormula) +// debug(untilLevelPathFormula) +// debug(pathFormula) +// debug(longRunAverageRewardFormula) +// debug(instantaneousRewardFormula) +// debug(cumulativeRewardFormula) +// debug(totalRewardFormula) +// debug(playerCoalition) +// debug(gameFormula) +// debug(multiOperatorFormula) +// debug(quantileBoundVariable) +// debug(quantileFormula) +// debug(formula) +// debug(topLevelFormula) +// debug(formulaName) +// debug(filterProperty) +// debug(constantDefinition ) +// debug(start) + // Enable error reporting. - qi::on_error(start, handler(qi::_1, qi::_2, qi::_3, qi::_4)); - qi::on_error(stateFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); - qi::on_error(orStateFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); - qi::on_error(andStateFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); - qi::on_error(probabilityOperator, handler(qi::_1, qi::_2, qi::_3, qi::_4)); - qi::on_error(rewardOperator, handler(qi::_1, qi::_2, qi::_3, qi::_4)); - qi::on_error(longRunAverageOperator, handler(qi::_1, qi::_2, qi::_3, qi::_4)); - qi::on_error(timeOperator, handler(qi::_1, qi::_2, qi::_3, qi::_4)); - qi::on_error(operatorInformation, handler(qi::_1, qi::_2, qi::_3, qi::_4)); - qi::on_error(pathFormulaWithoutUntil, handler(qi::_1, qi::_2, qi::_3, qi::_4)); - qi::on_error(pathFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); - qi::on_error(conditionalFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); - qi::on_error(untilFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); - qi::on_error(hoaPathFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); - qi::on_error(basicPathFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); - qi::on_error(nextFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); - qi::on_error(globallyFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); - qi::on_error(eventuallyFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); - qi::on_error(atomicStateFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); - qi::on_error(booleanLiteralFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(rewardModelName, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(rewardMeasureType, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(operatorFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); qi::on_error(labelFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); 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(booleanLiteralFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(atomicPropositionFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(basicPropositionalFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(negationPropositionalFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(andLevelPropositionalFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(orLevelPropositionalFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(propositionalFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(timeBoundReference, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(timeBound, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(timeBounds, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(eventuallyFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(nextFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(globallyFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(hoaPathFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(multiBoundedPathFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(prefixOperatorPathFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(basicPathFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(untilLevelPathFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(pathFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(longRunAverageRewardFormula, 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(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(multiFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(playerCoalition, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(gameFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(multiOperatorFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(quantileBoundVariable, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(quantileFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(formula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(topLevelFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(formulaName, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(filterProperty, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(constantDefinition , handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(start, handler(qi::_1, qi::_2, qi::_3, qi::_4)); } void FormulaParserGrammar::addIdentifierExpression(std::string const& identifier, storm::expressions::Expression const& expression) { + STORM_LOG_WARN_COND(keywords_.find(identifier) == nullptr, "Identifier `" << identifier << "' coincides with a reserved keyword or operator. Property expressions using the variable or constant '" << identifier << "' will not be parsed correctly."); + STORM_LOG_WARN_COND(nonStandardKeywords_.find(identifier) == nullptr, "Identifier `" << identifier << "' coincides with a reserved keyword or operator. Property expressions using the variable or constant '" << identifier << "' might not be parsed correctly."); this->identifiers_.add(identifier, expression); } @@ -403,8 +434,13 @@ namespace storm { hoaFormula_.addAPMapping(ap, expression); } - std::shared_ptr FormulaParserGrammar::createConditionalFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, storm::logic::FormulaContext context) const { - return std::shared_ptr(new storm::logic::ConditionalFormula(leftSubformula, rightSubformula, context)); + std::shared_ptr FormulaParserGrammar::createConditionalFormula(std::shared_ptr const& leftSubformula, boost::optional> const& rightSubformula, storm::logic::FormulaContext context) const { + if (rightSubformula) { + return std::shared_ptr(new storm::logic::ConditionalFormula(leftSubformula, rightSubformula.get(), context)); + } else { + // If there is no rhs, just return the lhs + return leftSubformula; + } } storm::logic::OperatorInformation FormulaParserGrammar::createOperatorInformation(boost::optional const& optimizationDirection, boost::optional const& comparisonType, boost::optional const& threshold) const { @@ -415,7 +451,25 @@ namespace storm { return storm::logic::OperatorInformation(optimizationDirection, boost::none); } } - + + std::shared_ptr FormulaParserGrammar::createOperatorFormula(storm::logic::FormulaContext const& context, boost::optional const& rewardMeasureType, boost::optional const& rewardModelName, storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr const& subformula) { + switch(context) { + case storm::logic::FormulaContext::Probability: + STORM_LOG_ASSERT(!rewardMeasureType && !rewardModelName, "Probability operator with reward information parsed"); + return createProbabilityOperatorFormula(operatorInformation, subformula); + case storm::logic::FormulaContext::Reward: + return createRewardOperatorFormula(rewardMeasureType, rewardModelName, operatorInformation, subformula); + case storm::logic::FormulaContext::LongRunAverage: + STORM_LOG_ASSERT(!rewardMeasureType && !rewardModelName, "LRA operator with reward information parsed"); + return createLongRunAverageOperatorFormula(operatorInformation, subformula); + case storm::logic::FormulaContext::Time: + STORM_LOG_ASSERT(!rewardModelName, "Time operator with reward model name parsed"); + return createTimeOperatorFormula(rewardMeasureType, operatorInformation, subformula); + default: + STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Unexpected formula context."); + } + } + std::shared_ptr FormulaParserGrammar::createLongRunAverageOperatorFormula(storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr const& subformula) const { return std::shared_ptr(new storm::logic::LongRunAverageOperatorFormula(subformula, operatorInformation)); } @@ -467,53 +521,58 @@ namespace storm { std::shared_ptr FormulaParserGrammar::createBinaryBooleanStateOrPathFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, storm::logic::BinaryBooleanOperatorType operatorType) { if (leftSubformula->isStateFormula() && rightSubformula->isStateFormula()) { return createBinaryBooleanStateFormula(leftSubformula, rightSubformula, operatorType); - } else { + } else if (leftSubformula->isPathFormula() || rightSubformula->isPathFormula()) { return createBinaryBooleanPathFormula(leftSubformula, rightSubformula, operatorType); } + STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Subformulas have unexpected type."); } std::shared_ptr FormulaParserGrammar::createUnaryBooleanStateOrPathFormula(std::shared_ptr const& subformula, boost::optional const& operatorType) { if (subformula->isStateFormula()) { return createUnaryBooleanStateFormula(subformula, operatorType); - } else { + } else if (subformula->isPathFormula()) { return createUnaryBooleanPathFormula(subformula, operatorType); } + STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Subformulas have unexpected type."); } - std::shared_ptr FormulaParserGrammar::createMultiFormula(std::vector> const& subformulas) { - bool isMultiDimensionalBoundedUntilFormula = !subformulas.empty(); - for (auto const& subformula : subformulas) { - if (!subformula->isBoundedUntilFormula()) { - isMultiDimensionalBoundedUntilFormula = false; - break; + bool FormulaParserGrammar::isValidMultiBoundedPathFormulaOperand(std::shared_ptr const& operand) { + if (operand->isBoundedUntilFormula()) { + if (!operand->asBoundedUntilFormula().isMultiDimensional()) { + return true; } + STORM_LOG_ERROR("Composition of multidimensional bounded until formula must consist of single dimension subformulas. Got '" << *operand << "' instead."); } + return false; + } - if (isMultiDimensionalBoundedUntilFormula) { - std::vector> leftSubformulas, rightSubformulas; - std::vector> lowerBounds, upperBounds; - std::vector timeBoundReferences; - for (auto const& subformula : subformulas) { - auto const& f = subformula->asBoundedUntilFormula(); - STORM_LOG_THROW(!f.isMultiDimensional(), storm::exceptions::WrongFormatException, "Composition of multidimensional bounded until formula must consist of single dimension subformulas. Got '" << f << "' instead."); - leftSubformulas.push_back(f.getLeftSubformula().asSharedPointer()); - rightSubformulas.push_back(f.getRightSubformula().asSharedPointer()); - if (f.hasLowerBound()) { - lowerBounds.emplace_back(storm::logic::TimeBound(f.isLowerBoundStrict(), f.getLowerBound())); - } else { - lowerBounds.emplace_back(); - } - if (f.hasUpperBound()) { - upperBounds.emplace_back(storm::logic::TimeBound(f.isUpperBoundStrict(), f.getUpperBound())); - } else { - upperBounds.emplace_back(); - } - timeBoundReferences.push_back(f.getTimeBoundReference()); + std::shared_ptr FormulaParserGrammar::createMultiBoundedPathFormula(std::vector> const& subformulas) { + std::vector> leftSubformulas, rightSubformulas; + std::vector> lowerBounds, upperBounds; + std::vector timeBoundReferences; + for (auto const& subformula : subformulas) { + STORM_LOG_THROW(subformula->isBoundedUntilFormula(), storm::exceptions::WrongFormatException, "multi-path formulas require bounded until (or eventually) subformulae. Got '" << *subformula << "' instead."); + auto const& f = subformula->asBoundedUntilFormula(); + STORM_LOG_THROW(!f.isMultiDimensional(), storm::exceptions::WrongFormatException, "Composition of multidimensional bounded until formula must consist of single dimension subformulas. Got '" << f << "' instead."); + leftSubformulas.push_back(f.getLeftSubformula().asSharedPointer()); + rightSubformulas.push_back(f.getRightSubformula().asSharedPointer()); + if (f.hasLowerBound()) { + lowerBounds.emplace_back(storm::logic::TimeBound(f.isLowerBoundStrict(), f.getLowerBound())); + } else { + lowerBounds.emplace_back(); } - return std::shared_ptr(new storm::logic::BoundedUntilFormula(leftSubformulas, rightSubformulas, lowerBounds, upperBounds, timeBoundReferences)); - } else { - return std::shared_ptr(new storm::logic::MultiObjectiveFormula(subformulas)); + if (f.hasUpperBound()) { + upperBounds.emplace_back(storm::logic::TimeBound(f.isUpperBoundStrict(), f.getUpperBound())); + } else { + upperBounds.emplace_back(); + } + timeBoundReferences.push_back(f.getTimeBoundReference()); } + return std::shared_ptr(new storm::logic::BoundedUntilFormula(leftSubformulas, rightSubformulas, lowerBounds, upperBounds, timeBoundReferences)); + } + + std::shared_ptr FormulaParserGrammar::createMultiOperatorFormula(std::vector> const& subformulas) { + return std::shared_ptr(new storm::logic::MultiObjectiveFormula(subformulas)); } storm::expressions::Variable FormulaParserGrammar::createQuantileBoundVariables(boost::optional const& dir, std::string const& variableName) { @@ -561,30 +620,7 @@ namespace storm { return storm::jani::Property(std::to_string(propertyCount), formula, this->getUndefinedConstants(formula)); } } - - std::pair FormulaParserGrammar::createShieldComparisonStruct(storm::logic::ShieldComparison comparisonType, double value) { - return std::make_pair(comparisonType, value); - } - - std::shared_ptr FormulaParserGrammar::createShieldExpression(storm::logic::ShieldingType type, std::string name, boost::optional> comparisonStruct) { - if(comparisonStruct.is_initialized()) { - STORM_LOG_WARN_COND(type != storm::logic::ShieldingType::Optimal , "Comparison for optimal shield will be ignored."); - return std::shared_ptr(new storm::logic::ShieldExpression(type, name, comparisonStruct.get().first, comparisonStruct.get().second)); - } else { - STORM_LOG_THROW(type == storm::logic::ShieldingType::Optimal , storm::exceptions::WrongFormatException, "Construction of safety shield needs a comparison parameter (lambda or gamma)"); - return std::shared_ptr(new storm::logic::ShieldExpression(type, name)); - } - } - - storm::jani::Property FormulaParserGrammar::createShieldingProperty(boost::optional const& propertyName, std::shared_ptr const& formula, std::shared_ptr const& shieldExpression) { - ++propertyCount; - if (propertyName) { - return storm::jani::Property(propertyName.get(), formula, this->getUndefinedConstants(formula), shieldExpression); - } else { - return storm::jani::Property(std::to_string(propertyCount), formula, this->getUndefinedConstants(formula), shieldExpression); - } - } - + storm::logic::PlayerCoalition FormulaParserGrammar::createPlayerCoalition(std::vector> const& playerIds) const { return storm::logic::PlayerCoalition(playerIds); } @@ -592,5 +628,19 @@ namespace storm { std::shared_ptr FormulaParserGrammar::createGameFormula(storm::logic::PlayerCoalition const& coalition, std::shared_ptr const& subformula) const { return std::shared_ptr(new storm::logic::GameFormula(coalition, subformula)); } + + bool FormulaParserGrammar::isBooleanReturnType(std::shared_ptr const& formula, bool raiseErrorMessage) { + if (formula->hasQualitativeResult()) { + return true; + } + STORM_LOG_ERROR_COND(!raiseErrorMessage, "Formula " << *formula << " does not have a Boolean return type."); + return false; + } + + bool FormulaParserGrammar::raiseAmbiguousNonAssociativeOperatorError(std::shared_ptr const& formula, std::string const& op) { + STORM_LOG_ERROR( "Ambiguous use of non-associative operator '" << op << "' in formula '" << *formula << " U ... '"); + return true; + } + } } diff --git a/src/storm-parsers/parser/FormulaParserGrammar.h b/src/storm-parsers/parser/FormulaParserGrammar.h index 2bba99c73..33d9e7935 100644 --- a/src/storm-parsers/parser/FormulaParserGrammar.h +++ b/src/storm-parsers/parser/FormulaParserGrammar.h @@ -53,14 +53,32 @@ namespace storm { ("F", 5) ("G", 6) ("X", 7) - ("multi", 8) - ("quantile", 9); + ("U", 8) + ("C", 9) + ("I", 10) + ("P", 11) + ("R", 12) + ("S", 13); } }; - - // A parser used for recognizing the keywords. + // A parser used for recognizing the standard keywords (that also apply to e.g. PRISM). These shall not coincide with expression variables keywordsStruct keywords_; - + + struct nonStandardKeywordsStruct : qi::symbols { + nonStandardKeywordsStruct() { + add + ("T", 1) + ("LRA", 2) + ("MP", 3) + ("multi", 4) + ("quantile", 5) + ("HOA", 6); + } + }; + // A parser used for recognizing non-standard Storm-specific keywords. + // For compatibility, we still try to parse expression variables whose identifier is such a keyword and just issue a warning. + nonStandardKeywordsStruct nonStandardKeywords_; + struct relationalOperatorStruct : qi::symbols { relationalOperatorStruct() { add @@ -73,28 +91,7 @@ namespace storm { // A parser used for recognizing the operators at the "relational" precedence level. relationalOperatorStruct relationalOperator_; - - struct binaryBooleanOperatorStruct : qi::symbols { - binaryBooleanOperatorStruct() { - add - ("&", storm::logic::BinaryBooleanStateFormula::OperatorType::And) - ("|", storm::logic::BinaryBooleanStateFormula::OperatorType::Or); - } - }; - - // A parser used for recognizing the operators at the "binary" precedence level. - binaryBooleanOperatorStruct binaryBooleanOperator_; - - struct unaryBooleanOperatorStruct : qi::symbols { - unaryBooleanOperatorStruct() { - add - ("!", storm::logic::UnaryBooleanStateFormula::OperatorType::Not); - } - }; - - // A parser used for recognizing the operators at the "unary" precedence level. - unaryBooleanOperatorStruct unaryBooleanOperator_; - + struct optimalityOperatorStruct : qi::symbols { optimalityOperatorStruct() { add @@ -135,6 +132,24 @@ namespace storm { // A parser used for recognizing the filter type. filterTypeStruct filterType_; + + struct operatorKeyword : qi::symbols { + operatorKeyword() { + add + ("P", storm::logic::FormulaContext::Probability) + ("R", storm::logic::FormulaContext::Reward) + ("T", storm::logic::FormulaContext::Time) + ("LRA", storm::logic::FormulaContext::LongRunAverage) + ("S", storm::logic::FormulaContext::LongRunAverage); + } + }; + operatorKeyword operatorKeyword_; + + enum class FormulaKind { + State, /// PCTL*-like (boolean) state formula + Path, /// PCTL*-like (boolean) path formula (include state formulae) + }; + qi::rule isPathFormula; // The manager used to parse expressions. std::shared_ptr constManager; @@ -146,75 +161,84 @@ namespace storm { // A symbol table that is a mapping from identifiers that can be used in expressions to the expressions // they are to be replaced with. qi::symbols identifiers_; - - qi::rule(), Skipper> start; - - qi::rule, Skipper> constantDefinition; + + + // Rules + + // Auxiliary helpers + qi::rule, std::string), Skipper> noAmbiguousNonAssociativeOperator; qi::rule identifier; - qi::rule formulaName; - qi::rule quotedString; - - qi::rule, boost::optional, boost::optional>, Skipper> operatorInformation; - qi::rule rewardMeasureType; - qi::rule(), Skipper> probabilityOperator; - qi::rule(), Skipper> rewardOperator; - qi::rule(), Skipper> timeOperator; - qi::rule(), Skipper> longRunAverageOperator; - - qi::rule>>, Skipper> playerCoalition; - - qi::rule filterProperty; - qi::rule(), Skipper> simpleFormula; - qi::rule(storm::logic::FormulaContext), Skipper> stateFormula; - qi::rule(storm::logic::FormulaContext), Skipper> pathFormula; - qi::rule(storm::logic::FormulaContext), Skipper> pathFormulaWithoutUntil; - qi::rule(), Skipper> simplePathFormula; - qi::rule(storm::logic::FormulaContext), Skipper> atomicStateFormula; - qi::rule(storm::logic::FormulaContext), Skipper> atomicStateFormulaWithoutExpression; - qi::rule(), Skipper> operatorFormula; qi::rule label; - qi::rule rewardModelName; - - qi::rule(storm::logic::FormulaContext), Skipper> andStateFormula; - qi::rule(storm::logic::FormulaContext), Skipper> orStateFormula; - qi::rule(storm::logic::FormulaContext), Skipper> notStateFormula; + qi::rule quotedString; + + // PCTL-like Operator Formulas + qi::rule>, Skipper> operatorInformation; + qi::rule(storm::logic::FormulaContext), Skipper> operatorSubFormula; + qi::rule rewardModelName; + qi::rule rewardMeasureType; + qi::rule(), qi::locals, Skipper> operatorFormula; + + // Atomic propositions qi::rule(), Skipper> labelFormula; qi::rule(), Skipper> expressionFormula; qi::rule(), qi::locals, Skipper> booleanLiteralFormula; - - qi::rule(storm::logic::FormulaContext), Skipper> conditionalFormula; + qi::rule(), Skipper> atomicPropositionFormula; + + // Propositional logic operators + qi::rule(FormulaKind, storm::logic::FormulaContext), Skipper> basicPropositionalFormula; + qi::rule(FormulaKind, storm::logic::FormulaContext), Skipper> negationPropositionalFormula; + qi::rule(FormulaKind, storm::logic::FormulaContext), Skipper> andLevelPropositionalFormula; + qi::rule(FormulaKind, storm::logic::FormulaContext), Skipper> orLevelPropositionalFormula; + qi::rule(FormulaKind, storm::logic::FormulaContext), Skipper> propositionalFormula; + + // Path operators + qi::rule, Skipper> timeBoundReference; + qi::rule, boost::optional, std::shared_ptr>(), qi::locals, Skipper> timeBound; + qi::rule, boost::optional, std::shared_ptr>>(), qi::locals, Skipper> timeBounds; qi::rule(storm::logic::FormulaContext), Skipper> eventuallyFormula; qi::rule(storm::logic::FormulaContext), Skipper> nextFormula; qi::rule(storm::logic::FormulaContext), Skipper> globallyFormula; - qi::rule(storm::logic::FormulaContext), Skipper> untilFormula; - - qi::rule(storm::logic::FormulaContext), Skipper> basicPathFormula; qi::rule(storm::logic::FormulaContext), Skipper> hoaPathFormula; - - void addHoaAPMapping(storm::logic::Formula const& hoaFormula, const std::string& ap, std::shared_ptr& expression) const; - - qi::rule, Skipper> timeBoundReference; - qi::rule, boost::optional, std::shared_ptr>(), qi::locals, Skipper> timeBound; - qi::rule, boost::optional, std::shared_ptr>>(), qi::locals, Skipper> timeBounds; - - qi::rule(), Skipper> rewardPathFormula; - qi::rule(), qi::locals, Skipper> cumulativeRewardFormula; - qi::rule(), Skipper> totalRewardFormula; - qi::rule(), Skipper> instantaneousRewardFormula; + qi::rule(storm::logic::FormulaContext), Skipper> multiBoundedPathFormulaOperand; + qi::rule(storm::logic::FormulaContext), Skipper> multiBoundedPathFormula; + qi::rule(storm::logic::FormulaContext), Skipper> prefixOperatorPathFormula; + qi::rule(storm::logic::FormulaContext), Skipper> basicPathFormula; + qi::rule(storm::logic::FormulaContext), Skipper> untilLevelPathFormula; + qi::rule(storm::logic::FormulaContext), Skipper> pathFormula; + + // Quantitative path operators (reward) qi::rule(), Skipper> longRunAverageRewardFormula; + qi::rule(), Skipper> instantaneousRewardFormula; + qi::rule(), Skipper> cumulativeRewardFormula; + qi::rule(), Skipper> totalRewardFormula; + + // Game Formulae + qi::rule>>, Skipper> playerCoalition; + qi::rule(), Skipper> gameFormula; - qi::rule(), Skipper> multiFormula; - qi::rule>, Skipper> quantileBoundVariable; + // Multi-objective, quantiles + qi::rule(), Skipper> multiOperatorFormula; + qi::rule quantileBoundVariable; qi::rule(), Skipper> quantileFormula; - qi::rule(), Skipper> gameFormula; + + // General formulae + qi::rule(FormulaKind, storm::logic::FormulaContext), Skipper> formula; + qi::rule(), Skipper> topLevelFormula; - qi::rule(), Skipper> shieldExpression; - qi::rule shieldingType; - qi::rule probability; - qi::rule, qi::locals, Skipper> shieldComparison; + // Properties + qi::rule formulaName; + qi::rule filterProperty; + + // Constant declarations + enum class ConstantDataType { + Bool, Integer, Rational + }; + qi::rule, Skipper> constantDefinition; - // Parser that is used to recognize doubles only (as opposed to Spirit's double_ parser). - boost::spirit::qi::real_parser> strict_double; + // Start symbol + qi::rule(), Skipper> start; + + void addHoaAPMapping(storm::logic::Formula const& hoaFormula, const std::string& ap, std::shared_ptr& expression) const; storm::logic::PlayerCoalition createPlayerCoalition(std::vector> const& playerIds) const; std::shared_ptr createGameFormula(storm::logic::PlayerCoalition const& coalition, std::shared_ptr const& subformula) const; @@ -243,8 +267,9 @@ namespace storm { std::shared_ptr createNextFormula(std::shared_ptr const& subformula) const; std::shared_ptr createUntilFormula(std::shared_ptr const& leftSubformula, boost::optional, boost::optional, std::shared_ptr>>> const& timeBounds, std::shared_ptr const& rightSubformula); std::shared_ptr createHOAPathFormula(const std::string& automataFile) const; - std::shared_ptr createConditionalFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, storm::logic::FormulaContext context) const; + std::shared_ptr createConditionalFormula(std::shared_ptr const& leftSubformula, boost::optional> const& rightSubformula, storm::logic::FormulaContext context) const; storm::logic::OperatorInformation createOperatorInformation(boost::optional const& optimizationDirection, boost::optional const& comparisonType, boost::optional const& threshold) const; + std::shared_ptr createOperatorFormula(storm::logic::FormulaContext const& context, boost::optional const& rewardMeasureType, boost::optional const& rewardModelName, storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr const& subformula); std::shared_ptr createLongRunAverageOperatorFormula(storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr const& subformula) const; std::shared_ptr createRewardOperatorFormula(boost::optional const& rewardMeasureType, boost::optional const& rewardModelName, storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr const& subformula) const; std::shared_ptr createTimeOperatorFormula(boost::optional const& rewardMeasureType, storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr const& subformula) const; @@ -255,15 +280,19 @@ namespace storm { std::shared_ptr createUnaryBooleanStateFormula(std::shared_ptr const& subformula, boost::optional const& operatorType); std::shared_ptr createUnaryBooleanPathFormula(std::shared_ptr const& subformula, boost::optional const& operatorType); std::shared_ptr createUnaryBooleanStateOrPathFormula(std::shared_ptr const& subformula, boost::optional const& operatorType); - std::shared_ptr createMultiFormula(std::vector> const& subformulas); + bool isValidMultiBoundedPathFormulaOperand(std::shared_ptr const& operand); + std::shared_ptr createMultiBoundedPathFormula(std::vector> const& subformulas); + std::shared_ptr createMultiOperatorFormula(std::vector> const& subformulas); storm::expressions::Variable createQuantileBoundVariables(boost::optional const& dir, std::string const& variableName); std::shared_ptr createQuantileFormula(std::vector const& boundVariables, std::shared_ptr const& subformula); std::set getUndefinedConstants(std::shared_ptr const& formula) const; storm::jani::Property createProperty(boost::optional const& propertyName, storm::modelchecker::FilterType const& filterType, std::shared_ptr const& formula, std::shared_ptr const& states); storm::jani::Property createPropertyWithDefaultFilterTypeAndStates(boost::optional const& propertyName, std::shared_ptr const& formula); - storm::jani::Property createShieldingProperty(boost::optional const& propertyName, std::shared_ptr const& formula, std::shared_ptr const& shieldingExpression); - + + bool isBooleanReturnType(std::shared_ptr const& formula, bool raiseErrorMessage = false); + bool raiseAmbiguousNonAssociativeOperatorError(std::shared_ptr const& formula, std::string const& op); + // An error handler function. phoenix::function handler;