From 1944b947d36e1e39338de3ca8534371ef2ee8022 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 3 Aug 2016 21:14:36 +0200 Subject: [PATCH] modified formula parser to parse expressions as operator bounds and then convert them to rationals Former-commit-id: ebf441c40697fcaa56a5c1f17c0db9453d15e0c5 --- src/parser/FormulaParser.cpp | 18 ++++++++++++------ 1 file changed, 12 insertions(+), 6 deletions(-) diff --git a/src/parser/FormulaParser.cpp b/src/parser/FormulaParser.cpp index c709b061a..74dbf31cf 100644 --- a/src/parser/FormulaParser.cpp +++ b/src/parser/FormulaParser.cpp @@ -7,6 +7,8 @@ // If the parser fails due to ill-formed data, this exception is thrown. #include "src/exceptions/WrongFormatException.h" +#include "src/storage/expressions/ExpressionEvaluator.h" + namespace storm { namespace parser { @@ -99,6 +101,9 @@ namespace storm { // A parser used for recognizing the reward measure types. rewardMeasureTypeStruct rewardMeasureType_; + // The manager used to parse expressions. + std::shared_ptr manager; + // Parser and manager used for recognizing expressions. storm::parser::ExpressionParser expressionParser; @@ -108,7 +113,7 @@ namespace storm { qi::rule>(), Skipper> start; - qi::rule, boost::optional, boost::optional>, Skipper> operatorInformation; + qi::rule, boost::optional, boost::optional>, Skipper> operatorInformation; qi::rule rewardMeasureType; qi::rule(), Skipper> probabilityOperator; qi::rule(), Skipper> rewardOperator; @@ -159,7 +164,7 @@ namespace storm { std::shared_ptr createNextFormula(std::shared_ptr const& subformula) const; std::shared_ptr createUntilFormula(std::shared_ptr const& leftSubformula, boost::optional, uint_fast64_t>> 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; + 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; std::shared_ptr createRewardOperatorFormula(boost::optional const& rewardMeasureType, boost::optional const& rewardModelName, storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr const& subformula) const; std::shared_ptr createTimeOperatorFormula(boost::optional const& rewardMeasureType, storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr const& subformula) const; @@ -248,7 +253,7 @@ namespace storm { grammar->addIdentifierExpression(identifier, expression); } - FormulaParserGrammar::FormulaParserGrammar(std::shared_ptr const& manager) : FormulaParserGrammar::base_type(start), expressionParser(*manager, keywords_, true, true) { + FormulaParserGrammar::FormulaParserGrammar(std::shared_ptr const& manager) : FormulaParserGrammar::base_type(start), manager(manager), expressionParser(*manager, keywords_, true, true) { // Register all variables so we can parse them in the expressions. for (auto variableTypePair : *manager) { identifiers_.add(variableTypePair.first.getName(), variableTypePair.first); @@ -316,7 +321,7 @@ namespace storm { rewardMeasureType = qi::lit("[") >> rewardMeasureType_ >> qi::lit("]"); rewardMeasureType.name("reward measure type"); - operatorInformation = (-optimalityOperator_[qi::_a = qi::_1] >> ((relationalOperator_[qi::_b = qi::_1] > qi::double_[qi::_c = qi::_1]) | (qi::lit("=") > qi::lit("?"))))[qi::_val = phoenix::bind(&FormulaParserGrammar::createOperatorInformation, phoenix::ref(*this), qi::_a, qi::_b, qi::_c)]; + 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)]; @@ -476,9 +481,10 @@ namespace storm { 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 { + storm::logic::OperatorInformation FormulaParserGrammar::createOperatorInformation(boost::optional const& optimizationDirection, boost::optional const& comparisonType, boost::optional const& threshold) const { if (comparisonType && threshold) { - return storm::logic::OperatorInformation(optimizationDirection, storm::logic::Bound(comparisonType.get(), storm::utility::convertNumber(threshold.get()))); + storm::expressions::ExpressionEvaluator evaluator(*manager); + return storm::logic::OperatorInformation(optimizationDirection, storm::logic::Bound(comparisonType.get(), evaluator.asRational(threshold.get()))); } else { return storm::logic::OperatorInformation(optimizationDirection, boost::none); }