From fa0da0bc7fd000848ac59fe014c51be34e3e825d Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Tue, 15 May 2018 22:16:51 +0200
Subject: [PATCH] fixes to parser

---
 .../abstraction/GameBasedMdpModelChecker.cpp  |  4 ++--
 src/storm/parser/ExpressionParser.cpp         | 22 ++++++++++++++-----
 2 files changed, 19 insertions(+), 7 deletions(-)

diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
index a1900236c..7657c0ceb 100644
--- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
+++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
@@ -522,13 +522,13 @@ namespace storm {
             STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(), storm::exceptions::InvalidPropertyException, "The game-based abstraction refinement model checker can only compute the result for the initial states.");
 
             // Optimization: do not compute both bounds if not necessary (e.g. if bound given and exceeded, etc.)
-            
+
             // Set up initial predicates.
             std::vector<storm::expressions::Expression> initialPredicates = getInitialPredicates(constraintExpression, targetStateExpression);
             
             // Derive the optimization direction for player 1 (assuming menu-game abstraction).
             storm::OptimizationDirection player1Direction = getPlayer1Direction(checkTask);
-            
+
             // Create the abstractor.
             std::shared_ptr<storm::abstraction::MenuGameAbstractor<Type, ValueType>> abstractor;
             if (preprocessedModel.isPrismProgram()) {
diff --git a/src/storm/parser/ExpressionParser.cpp b/src/storm/parser/ExpressionParser.cpp
index 64e185b54..5d824d82d 100644
--- a/src/storm/parser/ExpressionParser.cpp
+++ b/src/storm/parser/ExpressionParser.cpp
@@ -95,7 +95,11 @@ namespace storm {
             }
             multiplicationExpression.name("multiplication expression");
             
-            plusExpression = multiplicationExpression[qi::_val = qi::_1] > *(plusOperator_ >> multiplicationExpression)[qi::_val = phoenix::bind(&ExpressionCreator::createPlusExpression, phoenix::ref(*expressionCreator), qi::_val, qi::_1, qi::_2, qi::_pass)];
+            if (allowBacktracking) {
+                plusExpression = multiplicationExpression[qi::_val = qi::_1] >> *(plusOperator_ >> multiplicationExpression)[qi::_val = phoenix::bind(&ExpressionCreator::createPlusExpression, phoenix::ref(*expressionCreator), qi::_val, qi::_1, qi::_2, qi::_pass)];
+            } else {
+                plusExpression = multiplicationExpression[qi::_val = qi::_1] > *(plusOperator_ >> multiplicationExpression)[qi::_val = phoenix::bind(&ExpressionCreator::createPlusExpression, phoenix::ref(*expressionCreator), qi::_val, qi::_1, qi::_2, qi::_pass)];
+            }
             plusExpression.name("plus expression");
             
             if (allowBacktracking) {
@@ -105,7 +109,11 @@ namespace storm {
             }
             relativeExpression.name("relative expression");
                         
-            equalityExpression = relativeExpression[qi::_val = qi::_1] >> *(equalityOperator_ >> relativeExpression)[qi::_val = phoenix::bind(&ExpressionCreator::createEqualsExpression, phoenix::ref(*expressionCreator), qi::_val, qi::_1, qi::_2, qi::_pass)];
+            if (allowBacktracking) {
+                equalityExpression = relativeExpression[qi::_val = qi::_1] >> *(equalityOperator_ >> relativeExpression)[qi::_val = phoenix::bind(&ExpressionCreator::createEqualsExpression, phoenix::ref(*expressionCreator), qi::_val, qi::_1, qi::_2, qi::_pass)];
+            } else {
+                equalityExpression = relativeExpression[qi::_val = qi::_1] >> *(equalityOperator_ >> relativeExpression)[qi::_val = phoenix::bind(&ExpressionCreator::createEqualsExpression, phoenix::ref(*expressionCreator), qi::_val, qi::_1, qi::_2, qi::_pass)];
+            }
             equalityExpression.name("equality expression");
             
             if (allowBacktracking) {
@@ -122,7 +130,11 @@ namespace storm {
             }
             orExpression.name("or expression");
             
-            iteExpression = orExpression[qi::_val = qi::_1] > -(qi::lit("?") > iteExpression > qi::lit(":") > iteExpression)[qi::_val = phoenix::bind(&ExpressionCreator::createIteExpression, phoenix::ref(*expressionCreator), qi::_val, qi::_1, qi::_2, qi::_pass)];
+            if (allowBacktracking) {
+                iteExpression = orExpression[qi::_val = qi::_1] >> -(qi::lit("?") >> iteExpression >> qi::lit(":") >> iteExpression)[qi::_val = phoenix::bind(&ExpressionCreator::createIteExpression, phoenix::ref(*expressionCreator), qi::_val, qi::_1, qi::_2, qi::_pass)];
+            } else {
+                iteExpression = orExpression[qi::_val = qi::_1] > -(qi::lit("?") > iteExpression > qi::lit(":") > iteExpression)[qi::_val = phoenix::bind(&ExpressionCreator::createIteExpression, phoenix::ref(*expressionCreator), qi::_val, qi::_1, qi::_2, qi::_pass)];
+            }
             iteExpression.name("if-then-else expression");
             
             expression %= iteExpression;
@@ -138,12 +150,12 @@ namespace storm {
             debug(relativeExpression);
             debug(plusExpression);
             debug(multiplicationExpression);
-            debug(infixPowerExpression);
+            debug(infixPowerModuloExpression);
             debug(unaryExpression);
             debug(atomicExpression);
             debug(literalExpression);
             debug(identifierExpression);
-             */
+            */
             
             if (enableErrorHandling) {
                 // Enable error reporting.