From 35baa5ff02a4e87315c2778963cf048d7ce613d2 Mon Sep 17 00:00:00 2001
From: Lanchid <thomas.heinemann@rwth-aachen.de>
Date: Wed, 10 Apr 2013 14:08:48 +0200
Subject: [PATCH] Added parsing of time bounded operators

---
 src/parser/CslParser.cpp | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

diff --git a/src/parser/CslParser.cpp b/src/parser/CslParser.cpp
index 1f451e433..810788056 100644
--- a/src/parser/CslParser.cpp
+++ b/src/parser/CslParser.cpp
@@ -98,20 +98,20 @@ struct CslParser::CslGrammar : qi::grammar<Iterator, storm::formula::AbstractFor
 		steadyStateNoBoundOperator.name("no bound operator");
 
 		//This block defines rules for parsing probabilistic path formulas
-		pathFormula = (boundedEventually | eventually | globally | boundedUntil | until);
+		pathFormula = (timeBoundedEventually | eventually | globally | timeBoundedUntil | until);
 		pathFormula.name("path formula");
-		boundedEventually = (qi::lit("F") >> qi::lit("<=") > qi::int_ > stateFormula)[qi::_val =
-				phoenix::new_<storm::formula::BoundedEventually<double>>(qi::_2, qi::_1)];
-		boundedEventually.name("path formula (for probabilistic operator)");
+		timeBoundedEventually = (qi::lit("F") >> qi::lit("[") > qi::double_ > qi::lit(",") > qi::double_ > qi::lit("]") > stateFormula)[qi::_val =
+				phoenix::new_<storm::formula::TimeBoundedEventually<double>>(qi::_1, qi::_2, qi::_3)];
+		timeBoundedEventually.name("path formula (for probabilistic operator)");
 		eventually = (qi::lit("F") > stateFormula)[qi::_val =
 				phoenix::new_<storm::formula::Eventually<double> >(qi::_1)];
 		eventually.name("path formula (for probabilistic operator)");
 		globally = (qi::lit("G") > stateFormula)[qi::_val =
 				phoenix::new_<storm::formula::Globally<double> >(qi::_1)];
 		globally.name("path formula (for probabilistic operator)");
-		boundedUntil = (stateFormula[qi::_a = phoenix::construct<std::shared_ptr<storm::formula::AbstractStateFormula<double>>>(qi::_1)] >> qi::lit("U") >> qi::lit("<=") > qi::int_ > stateFormula)
-				[qi::_val = phoenix::new_<storm::formula::BoundedUntil<double>>(phoenix::bind(&storm::formula::AbstractStateFormula<double>::clone, phoenix::bind(&std::shared_ptr<storm::formula::AbstractStateFormula<double>>::get, qi::_a)), qi::_3, qi::_2)];
-		boundedUntil.name("path formula (for probabilistic operator)");
+		timeBoundedUntil = (stateFormula[qi::_a = phoenix::construct<std::shared_ptr<storm::formula::AbstractStateFormula<double>>>(qi::_1)] >> qi::lit("U") >> qi::lit("[") > qi::double_ > qi::lit(",") > qi::double_ > qi::lit("]")  > stateFormula)
+				[qi::_val = phoenix::new_<storm::formula::TimeBoundedUntil<double>>(qi::_2, qi::_3, phoenix::bind(&storm::formula::AbstractStateFormula<double>::clone, phoenix::bind(&std::shared_ptr<storm::formula::AbstractStateFormula<double>>::get, qi::_a)), qi::_4)];
+		timeBoundedUntil.name("path formula (for probabilistic operator)");
 		until = (stateFormula[qi::_a = phoenix::construct<std::shared_ptr<storm::formula::AbstractStateFormula<double>>>(qi::_1)] >> qi::lit("U") > stateFormula)[qi::_val =
 				phoenix::new_<storm::formula::Until<double>>(phoenix::bind(&storm::formula::AbstractStateFormula<double>::clone, phoenix::bind(&std::shared_ptr<storm::formula::AbstractStateFormula<double>>::get, qi::_a)), qi::_2)];
 		until.name("path formula (for probabilistic operator)");
@@ -138,10 +138,10 @@ struct CslParser::CslGrammar : qi::grammar<Iterator, storm::formula::AbstractFor
 	qi::rule<Iterator, storm::formula::StateNoBoundOperator<double>*(), Skipper> steadyStateNoBoundOperator;
 
 	qi::rule<Iterator, storm::formula::AbstractPathFormula<double>*(), Skipper> pathFormula;
-	qi::rule<Iterator, storm::formula::BoundedEventually<double>*(), Skipper> boundedEventually;
+	qi::rule<Iterator, storm::formula::TimeBoundedEventually<double>*(), Skipper> timeBoundedEventually;
 	qi::rule<Iterator, storm::formula::Eventually<double>*(), Skipper> eventually;
 	qi::rule<Iterator, storm::formula::Globally<double>*(), Skipper> globally;
-	qi::rule<Iterator, storm::formula::BoundedUntil<double>*(), qi::locals< std::shared_ptr<storm::formula::AbstractStateFormula<double>>>, Skipper> boundedUntil;
+	qi::rule<Iterator, storm::formula::TimeBoundedUntil<double>*(), qi::locals< std::shared_ptr<storm::formula::AbstractStateFormula<double>>>, Skipper> timeBoundedUntil;
 	qi::rule<Iterator, storm::formula::Until<double>*(), qi::locals< std::shared_ptr<storm::formula::AbstractStateFormula<double>>>, Skipper> until;
 
 	qi::rule<Iterator, storm::formula::AbstractPathFormula<double>*(), Skipper> rewardPathFormula;