From c7afcecf4ac7ffd6c172dba7431fab912bbf1385 Mon Sep 17 00:00:00 2001
From: Lanchid <thomas.heinemann@rwth-aachen.de>
Date: Mon, 8 Apr 2013 13:50:22 +0200
Subject: [PATCH] Minor changes (mainly improving comments)

---
 src/formula/SteadyStateReward.h |  4 ++--
 src/parser/PrctlParser.cpp      | 13 +++++++------
 2 files changed, 9 insertions(+), 8 deletions(-)

diff --git a/src/formula/SteadyStateReward.h b/src/formula/SteadyStateReward.h
index eae0def8b..70db11a46 100644
--- a/src/formula/SteadyStateReward.h
+++ b/src/formula/SteadyStateReward.h
@@ -2,7 +2,7 @@
  * SteadyStateReward.h
  *
  *  Created on: 08.04.2013
- *      Author: thomas
+ *      Author: Thomas Heinemann
  */
 
 #ifndef STORM_FORMULA_STEADYSTATEREWARD_H_
@@ -103,4 +103,4 @@ public:
 
 } /* namespace formula */
 } /* namespace storm */
-#endif /* STEADYSTATEREWARD_H_ */
+#endif /* STORM_FORMULA_STEADYSTATEREWARD_H_ */
diff --git a/src/parser/PrctlParser.cpp b/src/parser/PrctlParser.cpp
index 3d7db0c7c..e50facb0e 100644
--- a/src/parser/PrctlParser.cpp
+++ b/src/parser/PrctlParser.cpp
@@ -90,25 +90,26 @@ struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, storm::formula::Abstrac
 				phoenix::new_<storm::formula::RewardNoBoundOperator<double> >(qi::_1)];
 		rewardNoBoundOperator.name("no bound operator");
 
-		//This block defines rules for parsing path formulas
+		//This block defines rules for parsing probabilistic path formulas
 		pathFormula = (boundedEventually | eventually | globally | boundedUntil | 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");
+		boundedEventually.name("path formula (for probablistic operator)");
 		eventually = (qi::lit("F") > stateFormula)[qi::_val =
 				phoenix::new_<storm::formula::Eventually<double> >(qi::_1)];
-		eventually.name("path formula");
+		eventually.name("path formula (for probablistic operator)");
 		globally = (qi::lit("G") > stateFormula)[qi::_val =
 				phoenix::new_<storm::formula::Globally<double> >(qi::_1)];
-		globally.name("path formula");
+		globally.name("path formula (for probablistic 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");
+		boundedUntil.name("path formula (for probablistic 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");
+		until.name("path formula (for probablistic operator)");
 
+		//This block defines rules for parsing reward path formulas
 		rewardPathFormula = (cumulativeReward | reachabilityReward | instantaneousReward | steadyStateReward);
 		rewardPathFormula.name("path formula (for reward operator)");
 		cumulativeReward = (qi::lit("C") > qi::lit("<=") > qi::double_)