From 6a46d0abd5f83242c7a105e3ea0994cde135667e Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Tue, 4 Jul 2017 23:34:46 +0200 Subject: [PATCH] formula parser extended with reward bounded rewards --- src/storm/parser/FormulaParserGrammar.cpp | 27 +++++++++++++++-------- src/storm/parser/FormulaParserGrammar.h | 12 +++++----- 2 files changed, 24 insertions(+), 15 deletions(-) diff --git a/src/storm/parser/FormulaParserGrammar.cpp b/src/storm/parser/FormulaParserGrammar.cpp index 45f6fc62e..45fa27c16 100644 --- a/src/storm/parser/FormulaParserGrammar.cpp +++ b/src/storm/parser/FormulaParserGrammar.cpp @@ -215,20 +215,20 @@ namespace storm { return static_cast(manager); } - std::pair, boost::optional> FormulaParserGrammar::createTimeBoundFromInterval(storm::expressions::Expression const& lowerBound, storm::expressions::Expression const& upperBound, boost::optional const& rewardName) const { + std::tuple, boost::optional, 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); + return std::make_tuple(lower, upper, rewardName); } - std::pair, boost::optional> FormulaParserGrammar::createTimeBoundFromSingleBound(storm::expressions::Expression const& bound, bool upperBound, bool strict, boost::optional const& rewardName) const { + std::tuple, boost::optional, 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)); + return std::make_tuple(boost::none, storm::logic::TimeBound(strict, bound), rewardName); } else { - return std::make_pair(storm::logic::TimeBound(strict, bound), boost::none); + return std::make_tuple(storm::logic::TimeBound(strict, bound), boost::none, rewardName); } } @@ -261,9 +261,13 @@ namespace storm { return std::shared_ptr(new storm::logic::AtomicLabelFormula(label)); } - std::shared_ptr FormulaParserGrammar::createEventuallyFormula(boost::optional, boost::optional>> const& timeBound, storm::logic::FormulaContext context, std::shared_ptr const& subformula) const { + std::shared_ptr FormulaParserGrammar::createEventuallyFormula(boost::optional, boost::optional, boost::optional>> const& timeBound, storm::logic::FormulaContext context, std::shared_ptr const& subformula) const { if (timeBound) { - return std::shared_ptr(new storm::logic::BoundedUntilFormula(createBooleanLiteralFormula(true), subformula, timeBound.get().first, timeBound.get().second, storm::logic::TimeBoundReference(storm::logic::TimeBoundType::Time))); + if (std::get<2>(timeBound.get())) { + return std::shared_ptr(new storm::logic::BoundedUntilFormula(createBooleanLiteralFormula(true), subformula, std::get<0>(timeBound.get()), std::get<1>(timeBound.get()), storm::logic::TimeBoundReference(std::get<2>(timeBound.get()).get()))); + } else { + return std::shared_ptr(new storm::logic::BoundedUntilFormula(createBooleanLiteralFormula(true), subformula, std::get<0>(timeBound.get()), std::get<1>(timeBound.get()), storm::logic::TimeBoundReference(storm::logic::TimeBoundType::Time))); + } } else { return std::shared_ptr(new storm::logic::EventuallyFormula(subformula, context)); } @@ -277,9 +281,14 @@ namespace storm { return std::shared_ptr(new storm::logic::NextFormula(subformula)); } - std::shared_ptr FormulaParserGrammar::createUntilFormula(std::shared_ptr const& leftSubformula, boost::optional, boost::optional>> const& timeBound, std::shared_ptr const& rightSubformula) { + std::shared_ptr FormulaParserGrammar::createUntilFormula(std::shared_ptr const& leftSubformula, boost::optional, boost::optional, boost::optional>> const& timeBound, std::shared_ptr const& rightSubformula) { if (timeBound) { - return std::shared_ptr(new storm::logic::BoundedUntilFormula(leftSubformula, rightSubformula, timeBound.get().first, timeBound.get().second, storm::logic::TimeBoundReference(storm::logic::TimeBoundType::Time))); + if (std::get<2>(timeBound.get())) { + return std::shared_ptr(new storm::logic::BoundedUntilFormula(leftSubformula, rightSubformula, std::get<0>(timeBound.get()), std::get<1>(timeBound.get()), storm::logic::TimeBoundReference(std::get<2>(timeBound.get()).get()))); + } else { + return std::shared_ptr(new storm::logic::BoundedUntilFormula(leftSubformula, rightSubformula, std::get<0>(timeBound.get()), std::get<1>(timeBound.get()), storm::logic::TimeBoundReference(storm::logic::TimeBoundType::Time))); + } + } else { return std::shared_ptr(new storm::logic::UntilFormula(leftSubformula, rightSubformula)); } diff --git a/src/storm/parser/FormulaParserGrammar.h b/src/storm/parser/FormulaParserGrammar.h index 10c124785..31f766789 100644 --- a/src/storm/parser/FormulaParserGrammar.h +++ b/src/storm/parser/FormulaParserGrammar.h @@ -181,7 +181,7 @@ namespace storm { qi::rule(storm::logic::FormulaContext), Skipper> globallyFormula; qi::rule(storm::logic::FormulaContext), Skipper> untilFormula; - qi::rule, boost::optional>(), qi::locals, Skipper> timeBound; + qi::rule, boost::optional, boost::optional>(), qi::locals, Skipper> timeBound; qi::rule(), Skipper> rewardPathFormula; qi::rule(), qi::locals, Skipper> cumulativeRewardFormula; @@ -197,9 +197,9 @@ namespace storm { bool areConstantDefinitionsAllowed() const; 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, boost::optional const& rewardName) const; - std::pair, boost::optional> createTimeBoundFromSingleBound(storm::expressions::Expression const& bound, bool upperBound, bool strict, boost::optional const& rewardName) const; + + std::tuple, boost::optional, boost::optional> createTimeBoundFromInterval(storm::expressions::Expression const& lowerBound, storm::expressions::Expression const& upperBound, boost::optional const& rewardName) const; + std::tuple, boost::optional, 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; @@ -209,10 +209,10 @@ namespace storm { std::shared_ptr createAtomicExpressionFormula(storm::expressions::Expression const& expression) const; std::shared_ptr createBooleanLiteralFormula(bool literal) const; std::shared_ptr createAtomicLabelFormula(std::string const& label) const; - std::shared_ptr createEventuallyFormula(boost::optional, boost::optional>> const& timeBound, storm::logic::FormulaContext context, std::shared_ptr const& subformula) const; + std::shared_ptr createEventuallyFormula(boost::optional, boost::optional, boost::optional>> const& timeBound, storm::logic::FormulaContext context, std::shared_ptr const& subformula) const; std::shared_ptr createGloballyFormula(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>> const& timeBound, std::shared_ptr const& rightSubformula); + std::shared_ptr createUntilFormula(std::shared_ptr const& leftSubformula, boost::optional, boost::optional, boost::optional>> const& timeBound, std::shared_ptr const& rightSubformula); 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;