From a956fc782acf82a9506331fcbb506a81f1aee7b9 Mon Sep 17 00:00:00 2001
From: Lanchid <thomas.heinemann@rwth-aachen.de>
Date: Wed, 15 May 2013 16:25:38 +0200
Subject: [PATCH] Added support for atomic propositions containing numbers.

---
 src/parser/PrctlParser.cpp | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/parser/PrctlParser.cpp b/src/parser/PrctlParser.cpp
index 07cf79b7a..18f470660 100644
--- a/src/parser/PrctlParser.cpp
+++ b/src/parser/PrctlParser.cpp
@@ -37,13 +37,13 @@ struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, storm::property::prctl:
 	PrctlGrammar() : PrctlGrammar::base_type(start) {
 
 		//This block contains helper rules that may be used several times
-		freeIdentifierName = qi::lexeme[+(qi::alpha | qi::char_('_'))];
+		freeIdentifierName = qi::lexeme[qi::alpha >> *(qi::alnum | qi::char_('_'))];
 		comparisonType = (
 				(qi::lit(">="))[qi::_val = storm::property::GREATER_EQUAL] |
 				(qi::lit(">"))[qi::_val = storm::property::GREATER] |
 				(qi::lit("<="))[qi::_val = storm::property::LESS_EQUAL] |
 				(qi::lit("<"))[qi::_val = storm::property::LESS]);
-		comment = qi::lit("//")
+		comment = (qi::lit("//") >> *(qi::char_))[qi::_val = nullptr];
 
 		//This block defines rules for parsing state formulas
 		stateFormula %= orFormula;
@@ -142,7 +142,7 @@ struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, storm::property::prctl:
 		instantaneousReward.name("path formula (for reward operator)");
 		steadyStateReward = (qi::lit("S"))[qi::_val = phoenix::new_<storm::property::prctl::SteadyStateReward<double>>()];
 
-		start = (comment | noBoundOperator | stateFormula | qi::eps[qi::error()]);
+		start = (comment | noBoundOperator | stateFormula) >> qi::eoi;
 		start.name("PRCTL formula");
 	}
 
@@ -231,7 +231,7 @@ storm::parser::PrctlParser::PrctlParser(std::string formulaString) {
 	// The syntax can be so wrong that no rule can be matched at all
 	// In that case, no expectation failure is thrown, but the parser just returns nullptr
 	// Then, of course the result is not usable, hence we throw a WrongFormatException, too.
-	if (positionIteratorBegin != formulaString.end()) {
+	if (positionIteratorBegin != positionIteratorEnd) {
 		throw storm::exceptions::WrongFormatException() << "Syntax error in formula";
 	}