From f6b341168d83f521d8d85bbeb46a0e4a7ff044c0 Mon Sep 17 00:00:00 2001 From: Stefan Pranger Date: Tue, 16 Feb 2021 17:17:14 +0100 Subject: [PATCH] added formula parser grammar for shields --- .../parser/FormulaParserGrammar.cpp | 34 ++++++++++++++++++- .../parser/FormulaParserGrammar.h | 8 +++++ 2 files changed, 41 insertions(+), 1 deletion(-) diff --git a/src/storm-parsers/parser/FormulaParserGrammar.cpp b/src/storm-parsers/parser/FormulaParserGrammar.cpp index 9d5f0283e..d5bb59ee2 100644 --- a/src/storm-parsers/parser/FormulaParserGrammar.cpp +++ b/src/storm-parsers/parser/FormulaParserGrammar.cpp @@ -140,19 +140,34 @@ namespace storm { 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("<") > shieldingType > qi::lit(",") > shieldComparison > qi::lit(">"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createShieldExpression, phoenix::ref(*this), qi::_1, qi::_2)]; + + 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]); + shieldingType.name("shielding type"); + + shieldComparison = ((qi::lit("lambda")[qi::_a = storm::logic::ShieldComparison::Relative] | + qi::lit("gamma")[qi::_a = storm::logic::ShieldComparison::Absolute]) > qi::lit("=") > qi::double_)[qi::_val = phoenix::bind(&FormulaParserGrammar::createShieldComparisonStruct, phoenix::ref(*this), qi::_a, qi::_1)]; + shieldComparison.name("shield comparison type"); + stateFormula = (orStateFormula | multiFormula | quantileFormula | 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 = (-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)] | (-formulaName >> shieldExpression >> stateFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createShieldingProperty, phoenix::ref(*this), qi::_1, qi::_3, qi::_2)]; filterProperty.name("filter property"); #pragma clang diagnostic pop @@ -490,6 +505,23 @@ namespace storm { } } + std::pair FormulaParserGrammar::createShieldComparisonStruct(storm::logic::ShieldComparison comparisonType, double value) { + return std::make_pair(comparisonType, value); + } + + storm::logic::ShieldExpression FormulaParserGrammar::createShieldExpression(storm::logic::ShieldingType type, std::pair comparisonStruct) { + return storm::logic::ShieldExpression(type, comparisonStruct.first, comparisonStruct.second); + } + + storm::jani::Property FormulaParserGrammar::createShieldingProperty(boost::optional const& propertyName, std::shared_ptr const& formula, storm::logic::ShieldExpression 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); } diff --git a/src/storm-parsers/parser/FormulaParserGrammar.h b/src/storm-parsers/parser/FormulaParserGrammar.h index 75903d04a..3c7551123 100644 --- a/src/storm-parsers/parser/FormulaParserGrammar.h +++ b/src/storm-parsers/parser/FormulaParserGrammar.h @@ -205,12 +205,19 @@ namespace storm { qi::rule(), Skipper> quantileFormula; qi::rule(), Skipper> gameFormula; + qi::rule shieldExpression; + qi::rule shieldingType; + qi::rule, qi::locals, Skipper> shieldComparison; + // Parser that is used to recognize doubles only (as opposed to Spirit's double_ parser). boost::spirit::qi::real_parser> strict_double; storm::logic::PlayerCoalition createPlayerCoalition(std::vector> const& playerIds) const; std::shared_ptr createGameFormula(storm::logic::PlayerCoalition const& coalition, std::shared_ptr const& subformula) const; + std::pair createShieldComparisonStruct(storm::logic::ShieldComparison comparisonType, double value); + storm::logic::ShieldExpression createShieldExpression(storm::logic::ShieldingType type, std::pair comparisonStruct); + bool areConstantDefinitionsAllowed() const; void addConstant(std::string const& name, ConstantDataType type, boost::optional const& expression); void addProperty(std::vector& properties, boost::optional const& name, std::shared_ptr const& formula); @@ -246,6 +253,7 @@ namespace storm { 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, storm::logic::ShieldExpression); // An error handler function. phoenix::function handler;