diff --git a/src/storm-parsers/parser/FormulaParserGrammar.cpp b/src/storm-parsers/parser/FormulaParserGrammar.cpp index 87fe8edc9..ed355dcc4 100644 --- a/src/storm-parsers/parser/FormulaParserGrammar.cpp +++ b/src/storm-parsers/parser/FormulaParserGrammar.cpp @@ -3,7 +3,7 @@ namespace storm { namespace parser { - + FormulaParserGrammar::FormulaParserGrammar(std::shared_ptr const& manager) : FormulaParserGrammar::base_type(start), constManager(manager), manager(nullptr), expressionParser(*manager, keywords_, true, true), propertyCount(0) { initialize(); } @@ -16,72 +16,72 @@ namespace storm { // Register all variables so we can parse them in the expressions. for (auto variableTypePair : *constManager) { identifiers_.add(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_('_')))]]]; label.name("label"); - + 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("(") > stateFormula > qi::lit(")")) | operatorFormula; atomicStateFormula.name("atomic state formula"); - + atomicStateFormulaWithoutExpression = booleanLiteralFormula | labelFormula | (qi::lit("(") > stateFormula > qi::lit(")")) | operatorFormula; atomicStateFormula.name("atomic state formula without expression"); - + notStateFormula = (unaryBooleanOperator_ >> atomicStateFormulaWithoutExpression)[qi::_val = phoenix::bind(&FormulaParserGrammar::createUnaryBooleanStateFormula, phoenix::ref(*this), qi::_2, qi::_1)] | atomicStateFormula[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") >> pathFormulaWithoutUntil(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createGloballyFormula, phoenix::ref(*this), qi::_1)]; 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; 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"); - + conditionalFormula = untilFormula(qi::_r1)[qi::_val = qi::_1] >> *(qi::lit("||") >> untilFormula(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)] | (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) @@ -89,46 +89,46 @@ 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); 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 > 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::_val = qi::_1] >> *(qi::lit("&") >> notStateFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createBinaryBooleanStateFormula, phoenix::ref(*this), qi::_val, qi::_1, storm::logic::BinaryBooleanStateFormula::OperatorType::And)]; andStateFormula.name("and state formula"); - + 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"); - + multiFormula = (qi::lit("multi") > qi::lit("(") >> ((pathFormula(storm::logic::FormulaContext::Probability) | stateFormula) % 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 > qi::lit(")"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createQuantileFormula, phoenix::ref(*this), qi::_1, qi::_2)]; @@ -141,17 +141,31 @@ namespace storm { gameFormula.name("game formula"); stateFormula = (orStateFormula | multiFormula | quantileFormula | gameFormula); + + coalitionOperator = (qi::lit("<<") + > *( (identifier[phoenix::push_back(qi::_a, qi::_1)] + | qi::int_[phoenix::push_back(qi::_b, qi::_1)]) % ',' + ) + > qi::lit(">>"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createCoalition, phoenix::ref(*this), qi::_a, qi::_b)]; + coalitionOperator.name("coalition operator"); + + // only LRA for now, need to adapt this (beware of cyclic gameFormula pass!) + gameFormula = (coalitionOperator > longRunAverageOperator)[qi::_val = phoenix::bind(&FormulaParserGrammar::createGameFormula, phoenix::ref(*this), storm::logic::Coalition({}, {1}), qi::_1)]; + gameFormula.name("game formula"); + + stateFormula = (orStateFormula | multiFormula | quantileFormula | gameFormula); +>>>>>>> f106b8332... WIP added grammar rules for gameFormula stateFormula.name("state formula"); - + formulaName = qi::lit("\"") >> identifier >> qi::lit("\"") >> qi::lit(":"); formulaName.name("formula name"); - + constantDefinition = (qi::lit("const") > -(qi::lit("int")[qi::_a = ConstantDataType::Integer] | qi::lit("bool")[qi::_a = ConstantDataType::Bool] | qi::lit("double")[qi::_a = ConstantDataType::Rational]) >> identifier >> -(qi::lit("=") > expressionParser))[phoenix::bind(&FormulaParserGrammar::addConstant, phoenix::ref(*this), qi::_1, qi::_a, qi::_2)]; constantDefinition.name("constant definition"); - + #pragma clang diagnostic push #pragma clang diagnostic ignored "-Woverloaded-shift-op-parentheses" - + filterProperty = (-formulaName >> qi::lit("filter") > qi::lit("(") > filterType_ > qi::lit(",") > stateFormula > qi::lit(",") > stateFormula > qi::lit(")"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createProperty, phoenix::ref(*this), qi::_1, qi::_2, qi::_3, qi::_4)] | (-formulaName >> stateFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createPropertyWithDefaultFilterTypeAndStates, phoenix::ref(*this), qi::_1, qi::_2)]; filterProperty.name("filter property"); @@ -162,7 +176,7 @@ namespace storm { | qi::eps) % +(qi::char_("\n;")) >> qi::skip(storm::spirit_encoding::space_type() | qi::lit("//") >> *(qi::char_ - (qi::eol | qi::eoi)))[qi::eps] >> qi::eoi; start.name("start"); - + // Enable the following lines to print debug output for most the rules. // debug(start); // debug(constantDefinition); @@ -188,7 +202,7 @@ namespace storm { // debug(totalRewardFormula); // debug(instantaneousRewardFormula); // debug(multiFormula); - + // 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)); @@ -216,16 +230,16 @@ namespace storm { 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)); } - + void FormulaParserGrammar::addIdentifierExpression(std::string const& identifier, storm::expressions::Expression const& expression) { this->identifiers_.add(identifier, expression); } - + void FormulaParserGrammar::addConstant(std::string const& name, ConstantDataType type, boost::optional const& expression) { STORM_LOG_ASSERT(manager, "Mutable expression manager required to define new constants."); storm::expressions::Variable newVariable; STORM_LOG_THROW(!manager->hasVariable(name), storm::exceptions::WrongFormatException, "Invalid constant definition '" << name << "' in property: variable already exists."); - + if (type == ConstantDataType::Bool) { newVariable = manager->declareBooleanVariable(name); } else if (type == ConstantDataType::Integer) { @@ -233,7 +247,7 @@ namespace storm { } else { newVariable = manager->declareRationalVariable(name); } - + if (expression) { addIdentifierExpression(name, expression.get()); } else { @@ -241,11 +255,11 @@ namespace storm { addIdentifierExpression(name, newVariable); } } - + bool FormulaParserGrammar::areConstantDefinitionsAllowed() const { return static_cast(manager); } - + std::shared_ptr FormulaParserGrammar::createTimeBoundReference(storm::logic::TimeBoundType const& type, boost::optional const& rewardModelName) const { if (type == storm::logic::TimeBoundType::Reward) { STORM_LOG_THROW(rewardModelName, storm::exceptions::WrongFormatException, "Reward bound does not specify a reward model name."); @@ -254,7 +268,7 @@ namespace storm { return std::make_shared(type); } } - + std::tuple, boost::optional, std::shared_ptr> FormulaParserGrammar::createTimeBoundFromInterval(storm::expressions::Expression const& lowerBound, storm::expressions::Expression const& upperBound, std::shared_ptr const& timeBoundReference) const { // As soon as it somehow does not break everything anymore, I will change return types here. @@ -262,7 +276,7 @@ namespace storm { storm::logic::TimeBound upper(false, upperBound); return std::make_tuple(lower, upper, timeBoundReference); } - + std::tuple, boost::optional, std::shared_ptr> FormulaParserGrammar::createTimeBoundFromSingleBound(storm::expressions::Expression const& bound, bool upperBound, bool strict, std::shared_ptr const& timeBoundReference) const { // As soon as it somehow does not break everything anymore, I will change return types here. if (upperBound) { @@ -271,11 +285,11 @@ namespace storm { return std::make_tuple(storm::logic::TimeBound(strict, bound), boost::none, timeBoundReference); } } - + std::shared_ptr FormulaParserGrammar::createInstantaneousRewardFormula(storm::expressions::Expression const& timeBound) const { return std::shared_ptr(new storm::logic::InstantaneousRewardFormula(timeBound)); } - + std::shared_ptr FormulaParserGrammar::createCumulativeRewardFormula(std::vector, boost::optional, std::shared_ptr>> const& timeBounds) const { std::vector bounds; std::vector timeBoundReferences; @@ -287,28 +301,28 @@ namespace storm { } return std::shared_ptr(new storm::logic::CumulativeRewardFormula(bounds, timeBoundReferences)); } - + std::shared_ptr FormulaParserGrammar::createTotalRewardFormula() const { return std::shared_ptr(new storm::logic::TotalRewardFormula()); } - + std::shared_ptr FormulaParserGrammar::createLongRunAverageRewardFormula() const { return std::shared_ptr(new storm::logic::LongRunAverageRewardFormula()); } - + std::shared_ptr FormulaParserGrammar::createAtomicExpressionFormula(storm::expressions::Expression const& expression) const { STORM_LOG_THROW(expression.hasBooleanType(), storm::exceptions::WrongFormatException, "Expected expression of boolean type."); return std::shared_ptr(new storm::logic::AtomicExpressionFormula(expression)); } - + std::shared_ptr FormulaParserGrammar::createBooleanLiteralFormula(bool literal) const { return std::shared_ptr(new storm::logic::BooleanLiteralFormula(literal)); } - + std::shared_ptr FormulaParserGrammar::createAtomicLabelFormula(std::string const& label) const { return std::shared_ptr(new storm::logic::AtomicLabelFormula(label)); } - + std::shared_ptr FormulaParserGrammar::createEventuallyFormula(boost::optional, boost::optional, std::shared_ptr>>> const& timeBounds, storm::logic::FormulaContext context, std::shared_ptr const& subformula) const { if (timeBounds && !timeBounds.get().empty()) { std::vector> lowerBounds, upperBounds; @@ -323,15 +337,15 @@ namespace storm { return std::shared_ptr(new storm::logic::EventuallyFormula(subformula, context)); } } - + std::shared_ptr FormulaParserGrammar::createGloballyFormula(std::shared_ptr const& subformula) const { return std::shared_ptr(new storm::logic::GloballyFormula(subformula)); } - + std::shared_ptr FormulaParserGrammar::createNextFormula(std::shared_ptr const& subformula) const { return std::shared_ptr(new storm::logic::NextFormula(subformula)); } - + std::shared_ptr FormulaParserGrammar::createUntilFormula(std::shared_ptr const& leftSubformula, boost::optional, boost::optional, std::shared_ptr>>> const& timeBounds, std::shared_ptr const& rightSubformula) { if (timeBounds && !timeBounds.get().empty()) { std::vector> lowerBounds, upperBounds; @@ -346,11 +360,11 @@ namespace storm { return std::shared_ptr(new storm::logic::UntilFormula(leftSubformula, rightSubformula)); } } - + 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)); } - + storm::logic::OperatorInformation FormulaParserGrammar::createOperatorInformation(boost::optional const& optimizationDirection, boost::optional const& comparisonType, boost::optional const& threshold) const { if (comparisonType && threshold) { storm::expressions::ExpressionEvaluator evaluator(*constManager); @@ -359,11 +373,11 @@ namespace storm { return storm::logic::OperatorInformation(optimizationDirection, boost::none); } } - + 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)); } - + std::shared_ptr FormulaParserGrammar::createRewardOperatorFormula(boost::optional const& rewardMeasureType, boost::optional const& rewardModelName, storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr const& subformula) const { storm::logic::RewardMeasureType measureType = storm::logic::RewardMeasureType::Expectation; if (rewardMeasureType) { @@ -371,7 +385,7 @@ namespace storm { } return std::shared_ptr(new storm::logic::RewardOperatorFormula(subformula, rewardModelName, operatorInformation, measureType)); } - + std::shared_ptr FormulaParserGrammar::createTimeOperatorFormula(boost::optional const& rewardMeasureType, storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr const& subformula) const { storm::logic::RewardMeasureType measureType = storm::logic::RewardMeasureType::Expectation; if (rewardMeasureType) { @@ -379,15 +393,15 @@ namespace storm { } return std::shared_ptr(new storm::logic::TimeOperatorFormula(subformula, operatorInformation, measureType)); } - + std::shared_ptr FormulaParserGrammar::createProbabilityOperatorFormula(storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr const& subformula) { return std::shared_ptr(new storm::logic::ProbabilityOperatorFormula(subformula, operatorInformation)); } - + std::shared_ptr FormulaParserGrammar::createBinaryBooleanStateFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, storm::logic::BinaryBooleanStateFormula::OperatorType operatorType) { return std::shared_ptr(new storm::logic::BinaryBooleanStateFormula(operatorType, leftSubformula, rightSubformula)); } - + std::shared_ptr FormulaParserGrammar::createUnaryBooleanStateFormula(std::shared_ptr const& subformula, boost::optional const& operatorType) { if (operatorType) { return std::shared_ptr(new storm::logic::UnaryBooleanStateFormula(operatorType.get(), subformula)); @@ -395,7 +409,7 @@ namespace storm { return subformula; } } - + std::shared_ptr FormulaParserGrammar::createMultiFormula(std::vector> const& subformulas) { bool isMultiDimensionalBoundedUntilFormula = !subformulas.empty(); for (auto const& subformula : subformulas) { @@ -404,7 +418,7 @@ namespace storm { break; } } - + if (isMultiDimensionalBoundedUntilFormula) { std::vector> leftSubformulas, rightSubformulas; std::vector> lowerBounds, upperBounds; @@ -431,7 +445,7 @@ namespace storm { return std::shared_ptr(new storm::logic::MultiObjectiveFormula(subformulas)); } } - + storm::expressions::Variable FormulaParserGrammar::createQuantileBoundVariables(boost::optional const& dir, std::string const& variableName) { STORM_LOG_ASSERT(manager, "Mutable expression manager required to define quantile bound variable."); storm::expressions::Variable var; @@ -450,17 +464,17 @@ namespace storm { std::shared_ptr FormulaParserGrammar::createQuantileFormula(std::vector const& boundVariables, std::shared_ptr const& subformula) { return std::shared_ptr(new storm::logic::QuantileFormula(boundVariables, subformula)); } - + std::set FormulaParserGrammar::getUndefinedConstants(std::shared_ptr const& formula) const { std::set result; std::set usedVariables = formula->getUsedVariables(); std::set_intersection(usedVariables.begin(), usedVariables.end(), undefinedConstants.begin(), undefinedConstants.end(), std::inserter(result, result.begin())); return result; } - + storm::jani::Property FormulaParserGrammar::createProperty(boost::optional const& propertyName, storm::modelchecker::FilterType const& filterType, std::shared_ptr const& formula, std::shared_ptr const& states) { storm::jani::FilterExpression filterExpression(formula, filterType, states); - + ++propertyCount; if (propertyName) { return storm::jani::Property(propertyName.get(), filterExpression, this->getUndefinedConstants(formula)); @@ -468,7 +482,7 @@ namespace storm { return storm::jani::Property(std::to_string(propertyCount - 1), filterExpression, this->getUndefinedConstants(formula)); } } - + storm::jani::Property FormulaParserGrammar::createPropertyWithDefaultFilterTypeAndStates(boost::optional const& propertyName, std::shared_ptr const& formula) { ++propertyCount; if (propertyName) { diff --git a/src/storm-parsers/parser/FormulaParserGrammar.h b/src/storm-parsers/parser/FormulaParserGrammar.h index e709366cd..ad76aa87f 100644 --- a/src/storm-parsers/parser/FormulaParserGrammar.h +++ b/src/storm-parsers/parser/FormulaParserGrammar.h @@ -19,17 +19,17 @@ namespace storm { namespace logic { class Formula; } - + namespace parser { - + class FormulaParserGrammar : public qi::grammar(), Skipper> { public: FormulaParserGrammar(std::shared_ptr const& manager); FormulaParserGrammar(std::shared_ptr const& manager); - + FormulaParserGrammar(FormulaParserGrammar const& other) = delete; FormulaParserGrammar& operator=(FormulaParserGrammar const& other) = delete; - + /*! * Adds an identifier and the expression it is supposed to be replaced with. This can, for example be used * to substitute special identifiers in the formula by expressions. @@ -38,10 +38,10 @@ namespace storm { * @param expression The expression it is to be substituted with. */ void addIdentifierExpression(std::string const& identifier, storm::expressions::Expression const& expression); - + private: void initialize(); - + struct keywordsStruct : qi::symbols { keywordsStruct() { add @@ -56,10 +56,10 @@ namespace storm { ("quantile", 9); } }; - + // A parser used for recognizing the keywords. keywordsStruct keywords_; - + struct relationalOperatorStruct : qi::symbols { relationalOperatorStruct() { add @@ -69,10 +69,10 @@ namespace storm { ("<", storm::logic::ComparisonType::Less); } }; - + // A parser used for recognizing the operators at the "relational" precedence level. relationalOperatorStruct relationalOperator_; - + struct binaryBooleanOperatorStruct : qi::symbols { binaryBooleanOperatorStruct() { add @@ -80,20 +80,20 @@ namespace storm { ("|", 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 @@ -101,10 +101,10 @@ namespace storm { ("max", storm::OptimizationDirection::Maximize); } }; - + // A parser used for recognizing the optimality operators. optimalityOperatorStruct optimalityOperator_; - + struct rewardMeasureTypeStruct : qi::symbols { rewardMeasureTypeStruct() { add @@ -112,10 +112,10 @@ namespace storm { ("var", storm::logic::RewardMeasureType::Variance); } }; - + // A parser used for recognizing the reward measure types. rewardMeasureTypeStruct rewardMeasureType_; - + struct filterTypeStruct : qi::symbols { filterTypeStruct() { add @@ -134,28 +134,28 @@ namespace storm { // A parser used for recognizing the filter type. filterTypeStruct filterType_; - + // The manager used to parse expressions. std::shared_ptr constManager; std::shared_ptr manager; - + // Parser and manager used for recognizing expressions. storm::parser::ExpressionParser expressionParser; - + // 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; - + enum class ConstantDataType { Bool, Integer, Rational }; - + qi::rule, Skipper> constantDefinition; qi::rule identifier; qi::rule formulaName; - + qi::rule, boost::optional, boost::optional>, Skipper> operatorInformation; qi::rule rewardMeasureType; qi::rule(), Skipper> probabilityOperator; @@ -176,30 +176,30 @@ namespace storm { qi::rule(), Skipper> operatorFormula; qi::rule label; qi::rule rewardModelName; - + qi::rule(), Skipper> andStateFormula; qi::rule(), Skipper> orStateFormula; qi::rule(), Skipper> notStateFormula; qi::rule(), Skipper> labelFormula; qi::rule(), Skipper> expressionFormula; qi::rule(), qi::locals, Skipper> booleanLiteralFormula; - + qi::rule(storm::logic::FormulaContext), Skipper> conditionalFormula; 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, 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(), Skipper> longRunAverageRewardFormula; - + qi::rule(), Skipper> multiFormula; qi::rule>, Skipper> quantileBoundVariable; qi::rule(), Skipper> quantileFormula; @@ -242,16 +242,16 @@ namespace storm { std::shared_ptr createMultiFormula(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); - + // An error handler function. phoenix::function handler; - + uint64_t propertyCount; - + std::set undefinedConstants; std::set quantileFormulaVariables; };