From ba907a1d757fb8390da266b3d5a7a8e3662dd45a Mon Sep 17 00:00:00 2001 From: Joachim Klein Date: Mon, 24 Aug 2020 22:24:56 +0200 Subject: [PATCH] WIP (HOA-path) FormulaParser: parse HOAPathFormula Note: Syntax of HOA path formulas will change! Conflicts: src/storm-parsers/parser/FormulaParserGrammar.cpp src/storm-parsers/parser/FormulaParserGrammar.h --- .../parser/FormulaParserGrammar.cpp | 29 ++++++++++++++++++- .../parser/FormulaParserGrammar.h | 7 +++++ 2 files changed, 35 insertions(+), 1 deletion(-) diff --git a/src/storm-parsers/parser/FormulaParserGrammar.cpp b/src/storm-parsers/parser/FormulaParserGrammar.cpp index 3aba843be..57e18295e 100644 --- a/src/storm-parsers/parser/FormulaParserGrammar.cpp +++ b/src/storm-parsers/parser/FormulaParserGrammar.cpp @@ -1,6 +1,8 @@ #include "FormulaParserGrammar.h" #include "storm/storage/expressions/ExpressionManager.h" +#include + namespace storm { namespace parser { @@ -73,8 +75,17 @@ namespace storm { 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)]; + + hoaPathFormula = qi::lit("HOA:") > qi::lit("{") + > quotedString[qi::_val = phoenix::bind(&FormulaParserGrammar::createHOAPathFormula, phoenix::ref(*this), qi::_1)] + >> *(qi::lit(",") > quotedString > qi::lit("->") > stateFormula )[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]; + 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)] @@ -159,6 +170,9 @@ namespace storm { stateFormula = (orStateFormula | multiFormula | quantileFormula | gameFormula); 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"); + formulaName = qi::lit("\"") >> identifier >> qi::lit("\"") >> qi::lit(":"); formulaName.name("formula name"); @@ -221,6 +235,8 @@ namespace storm { 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)); @@ -377,6 +393,17 @@ namespace storm { } } + std::shared_ptr FormulaParserGrammar::createHOAPathFormula(std::string const& automatonFile) const { + return std::shared_ptr(new storm::logic::HOAPathFormula(automatonFile)); + } + + void FormulaParserGrammar::addHoaAPMapping(storm::logic::Formula const& hoaFormula, const std::string& ap, std::shared_ptr& expression) const { + // taking a const Formula reference and doing static_ and const_cast from Formula to allow non-const access to + // qi::_val of the hoaPathFormula rule + storm::logic::HOAPathFormula& hoaFormula_ = static_cast(const_cast(hoaFormula)); + 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)); } diff --git a/src/storm-parsers/parser/FormulaParserGrammar.h b/src/storm-parsers/parser/FormulaParserGrammar.h index 35ac56b6b..c40842532 100644 --- a/src/storm-parsers/parser/FormulaParserGrammar.h +++ b/src/storm-parsers/parser/FormulaParserGrammar.h @@ -152,6 +152,7 @@ namespace storm { qi::rule, Skipper> constantDefinition; qi::rule identifier; qi::rule formulaName; + qi::rule quotedString; qi::rule, boost::optional, boost::optional>, Skipper> operatorInformation; qi::rule rewardMeasureType; @@ -187,6 +188,11 @@ namespace storm { 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; @@ -236,6 +242,7 @@ namespace storm { std::shared_ptr createGloballyFormula(boost::optional, boost::optional, std::shared_ptr>>> const& timeBounds, std::shared_ptr const& subformula) const; 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; storm::logic::OperatorInformation createOperatorInformation(boost::optional const& optimizationDirection, boost::optional const& comparisonType, boost::optional const& threshold) const; std::shared_ptr createLongRunAverageOperatorFormula(storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr const& subformula) const;