From 65bb496bb9fea63840c3746d753b103153b7f203 Mon Sep 17 00:00:00 2001
From: Mavo <matthias.volk@rwth-aachen.de>
Date: Tue, 26 Jan 2016 10:40:49 +0100
Subject: [PATCH] Activate expected time in FormulaParser

Former-commit-id: 6fff9e826958ed53ae6eb03516b87cd1dfbcfbb3
---
 src/parser/FormulaParser.cpp | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

diff --git a/src/parser/FormulaParser.cpp b/src/parser/FormulaParser.cpp
index 082474187..d6de95ace 100644
--- a/src/parser/FormulaParser.cpp
+++ b/src/parser/FormulaParser.cpp
@@ -270,8 +270,8 @@ namespace storm {
             
             booleanLiteralFormula = (qi::lit("true")[qi::_a = true] | qi::lit("false")[qi::_a = false])[qi::_val = phoenix::bind(&FormulaParserGrammar::createBooleanLiteralFormula, phoenix::ref(*this), qi::_a)];
             booleanLiteralFormula.name("boolean literal formula");
-            
-            operatorFormula = probabilityOperator | rewardOperator | steadyStateOperator;
+
+            operatorFormula = probabilityOperator | rewardOperator | steadyStateOperator | expectedTimeOperator;
             operatorFormula.name("operator formulas");
             
             atomicStateFormula = booleanLiteralFormula | labelFormula | expressionFormula | (qi::lit("(") > stateFormula > qi::lit(")")) | operatorFormula;
@@ -334,8 +334,8 @@ namespace storm {
             start = qi::eps > (stateFormula % +(qi::char_("\n;"))) >> qi::skip(boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - (qi::eol | qi::eoi)))[qi::eps] >> qi::eoi;
             start.name("start");
             
-            /*!
-             * Enable the following lines to print debug output for most the rules.
+            //Enable the following lines to print debug output for most the rules.
+            /*
             debug(start);
             debug(stateFormula);
             debug(orStateFormula);
@@ -343,6 +343,7 @@ namespace storm {
             debug(probabilityOperator);
             debug(rewardOperator);
             debug(steadyStateOperator);
+            debug(expectedTimeOperator);
             debug(pathFormulaWithoutUntil);
             debug(pathFormula);
             debug(conditionalFormula);
@@ -357,7 +358,7 @@ namespace storm {
             debug(reachabilityRewardFormula);
             debug(cumulativeRewardFormula);
             debug(instantaneousRewardFormula);
-             */
+            */
 
             // Enable error reporting.
             qi::on_error<qi::fail>(start, handler(qi::_1, qi::_2, qi::_3, qi::_4));
@@ -366,6 +367,7 @@ namespace storm {
             qi::on_error<qi::fail>(andStateFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
             qi::on_error<qi::fail>(probabilityOperator, handler(qi::_1, qi::_2, qi::_3, qi::_4));
             qi::on_error<qi::fail>(rewardOperator, handler(qi::_1, qi::_2, qi::_3, qi::_4));
+            qi::on_error<qi::fail>(expectedTimeOperator, handler(qi::_1, qi::_2, qi::_3, qi::_4));
             qi::on_error<qi::fail>(steadyStateOperator, handler(qi::_1, qi::_2, qi::_3, qi::_4));
             qi::on_error<qi::fail>(operatorInformation, handler(qi::_1, qi::_2, qi::_3, qi::_4));
             qi::on_error<qi::fail>(pathFormulaWithoutUntil, handler(qi::_1, qi::_2, qi::_3, qi::_4));