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 >(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_>(qi::_2, qi::_1)]; - boundedEventually.name("path formula"); + boundedEventually.name("path formula (for probablistic operator)"); eventually = (qi::lit("F") > stateFormula)[qi::_val = phoenix::new_ >(qi::_1)]; - eventually.name("path formula"); + eventually.name("path formula (for probablistic operator)"); globally = (qi::lit("G") > stateFormula)[qi::_val = phoenix::new_ >(qi::_1)]; - globally.name("path formula"); + globally.name("path formula (for probablistic operator)"); boundedUntil = (stateFormula[qi::_a = phoenix::construct>>(qi::_1)] >> qi::lit("U") >> qi::lit("<=") > qi::int_ > stateFormula) [qi::_val = phoenix::new_>(phoenix::bind(&storm::formula::AbstractStateFormula::clone, phoenix::bind(&std::shared_ptr>::get, qi::_a)), qi::_3, qi::_2)]; - boundedUntil.name("path formula"); + boundedUntil.name("path formula (for probablistic operator)"); until = (stateFormula[qi::_a = phoenix::construct>>(qi::_1)] >> qi::lit("U") > stateFormula)[qi::_val = phoenix::new_>(phoenix::bind(&storm::formula::AbstractStateFormula::clone, phoenix::bind(&std::shared_ptr>::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_)