From 9af46452bca1f8e647b3ca36ef79dd8f41e9fc13 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Tue, 4 Jul 2017 16:54:26 +0200 Subject: [PATCH] first attempt for a parser --- src/storm/parser/FormulaParserGrammar.cpp | 10 +++++++--- src/storm/parser/FormulaParserGrammar.h | 8 ++++---- 2 files changed, 11 insertions(+), 7 deletions(-) diff --git a/src/storm/parser/FormulaParserGrammar.cpp b/src/storm/parser/FormulaParserGrammar.cpp index 95cb3f860..6141cacac 100644 --- a/src/storm/parser/FormulaParserGrammar.cpp +++ b/src/storm/parser/FormulaParserGrammar.cpp @@ -77,7 +77,8 @@ namespace storm { 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"); - timeBound = (qi::lit("[") > expressionParser > qi::lit(",") > expressionParser > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createTimeBoundFromInterval, phoenix::ref(*this), qi::_1, qi::_2)] | ((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)[qi::_val = phoenix::bind(&FormulaParserGrammar::createTimeBoundFromSingleBound, phoenix::ref(*this), qi::_1, qi::_a, qi::_b)]; + timeBound = (-rewardModelName >> (qi::lit("[") > expressionParser > qi::lit(",") > expressionParser > qi::lit("]")))[qi::_val = phoenix::bind(&FormulaParserGrammar::createTimeBoundFromInterval, phoenix::ref(*this), qi::_2, qi::_3, qi::_1)] + | (-rewardModelName >> ((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))[qi::_val = phoenix::bind(&FormulaParserGrammar::createTimeBoundFromSingleBound, phoenix::ref(*this), qi::_2, qi::_a, qi::_b, qi::_1)]; timeBound.name("time bound"); pathFormula = conditionalFormula(qi::_r1); @@ -212,13 +213,16 @@ namespace storm { return static_cast(manager); } - std::pair, boost::optional> FormulaParserGrammar::createTimeBoundFromInterval(storm::expressions::Expression const& lowerBound, storm::expressions::Expression const& upperBound) const { + std::pair, boost::optional> FormulaParserGrammar::createTimeBoundFromInterval(storm::expressions::Expression const& lowerBound, storm::expressions::Expression const& upperBound, boost::optional const& rewardName) const { + // As soon as it somehow does not break everything anymore, I will change return types here. + storm::logic::TimeBound lower(false, lowerBound); storm::logic::TimeBound upper(false, upperBound); return std::make_pair(lower, upper); } - std::pair, boost::optional> FormulaParserGrammar::createTimeBoundFromSingleBound(storm::expressions::Expression const& bound, bool upperBound, bool strict) const { + std::pair, boost::optional> FormulaParserGrammar::createTimeBoundFromSingleBound(storm::expressions::Expression const& bound, bool upperBound, bool strict, boost::optional const& rewardName) const { + // As soon as it somehow does not break everything anymore, I will change return types here. if (upperBound) { return std::make_pair(boost::none, storm::logic::TimeBound(strict, bound)); } else { diff --git a/src/storm/parser/FormulaParserGrammar.h b/src/storm/parser/FormulaParserGrammar.h index 79b272246..10c124785 100644 --- a/src/storm/parser/FormulaParserGrammar.h +++ b/src/storm/parser/FormulaParserGrammar.h @@ -198,10 +198,10 @@ namespace storm { void addConstant(std::string const& name, bool integer); void addProperty(std::vector& properties, boost::optional const& name, std::shared_ptr const& formula); - std::pair, boost::optional> createTimeBoundFromInterval(storm::expressions::Expression const& lowerBound, storm::expressions::Expression const& upperBound) const; - std::pair, boost::optional> createTimeBoundFromSingleBound(storm::expressions::Expression const& bound, bool upperBound, bool strict) const; - - // Methods that actually create the expression objects. + std::pair, boost::optional> createTimeBoundFromInterval(storm::expressions::Expression const& lowerBound, storm::expressions::Expression const& upperBound, boost::optional const& rewardName) const; + std::pair, boost::optional> createTimeBoundFromSingleBound(storm::expressions::Expression const& bound, bool upperBound, bool strict, boost::optional const& rewardName) const; + + // Methods that actually create the expression objects. std::shared_ptr createInstantaneousRewardFormula(storm::expressions::Expression const& timeBound) const; std::shared_ptr createCumulativeRewardFormula(storm::expressions::Expression const& timeBound, bool strict) const; std::shared_ptr createTotalRewardFormula() const;