From 9ce47989ed2ec665bd5fcffd226dbdc096d97de2 Mon Sep 17 00:00:00 2001
From: masawei <manuel.sascha.weiand@rwth-aachen.de>
Date: Sat, 7 Dec 2013 15:45:33 +0100
Subject: [PATCH] The MA transition parser is now able to handle arbitrary
 labels.

Former-commit-id: 9643f41141530c4797c7bf80ed021540c1a7e463
---
 src/parser/MarkovAutomatonSparseTransitionParser.cpp | 12 ++++++------
 src/parser/Parser.cpp                                | 12 ++++++++++--
 src/parser/Parser.h                                  |  5 +++++
 3 files changed, 21 insertions(+), 8 deletions(-)

diff --git a/src/parser/MarkovAutomatonSparseTransitionParser.cpp b/src/parser/MarkovAutomatonSparseTransitionParser.cpp
index 46bc05d2f..dc4d37888 100644
--- a/src/parser/MarkovAutomatonSparseTransitionParser.cpp
+++ b/src/parser/MarkovAutomatonSparseTransitionParser.cpp
@@ -57,12 +57,12 @@ namespace storm {
                 
                 // Depending on the action name, the choice is either a probabilitic one or a markovian one.
                 bool isMarkovianChoice = false;
-                if (buf[0] == '!') {
+                if (buf[0] == '!' &&  skipWord(buf) - buf == 1) {
                     isMarkovianChoice = true;
-                } else {
+                }else {
                     isMarkovianChoice = false;
                 }
-                ++buf;
+                buf = skipWord(buf);
                 
                 if (isMarkovianChoice) {
                     if (stateHasMarkovianChoice) {
@@ -99,7 +99,7 @@ namespace storm {
                         }
                     } else if (buf[0] == '*') {
                         // As we have encountered a "*", we know that there is an additional successor state for the current choice.
-                        ++buf;
+                        buf= skipWord(buf);
                         
                         // Now we need to read the successor state and check if we already saw a higher state index.
                         target = checked_strtol(buf, &buf);
@@ -180,7 +180,7 @@ namespace storm {
                 
                 // Depending on the action name, the choice is either a probabilitic one or a markovian one.
                 bool isMarkovianChoice = false;
-                if (buf[0] == '!') {
+                if (buf[0] == '!' && skipWord(buf) - buf == 1) {
                     isMarkovianChoice = true;
                     
                     // Mark the current state as a Markovian one.
@@ -209,7 +209,7 @@ namespace storm {
                         hasSuccessorState = true;
                         
                         // As we have encountered a "*", we know that there is an additional successor state for the current choice.
-                        ++buf;
+                        buf = skipWord(buf);
                         
                         // Now we need to read the successor state and check if we already saw a higher state index.
                         target = checked_strtol(buf, &buf);
diff --git a/src/parser/Parser.cpp b/src/parser/Parser.cpp
index 5ed957c17..611afc9c6 100644
--- a/src/parser/Parser.cpp
+++ b/src/parser/Parser.cpp
@@ -60,7 +60,16 @@ bool storm::parser::fileExistsAndIsReadable(const char* fileName) {
 }
 
 /*!
- *	Skips spaces, tabs, newlines and carriage returns. Returns pointer
+ * Skips all numbers, letters and special characters.
+ * Returns a pointer to the first char that is a whitespace.
+ */
+char* storm::parser::skipWord(char* buf){
+	while((*buf != ' ') && (*buf != '\t') && (*buf != '\n') && (*buf != '\r')) buf++;
+	return buf;
+}
+
+/*!
+ *	Skips spaces, tabs, newlines and carriage returns. Returns a pointer
  *	to first char that is not a whitespace.
  *	@param buf String buffer
  *	@return	pointer to first non-whitespace character
@@ -78,7 +87,6 @@ storm::parser::SupportedLineEndingsEnum storm::parser::findUsedLineEndings(std::
 	char* buf = nullptr;
 	char* const bufferEnd = fileMap.dataend;
 
-	bool sawR = false;
 	for (buf = fileMap.data; buf != bufferEnd; ++buf) {
 		if (*buf == '\r') {
 			// check for following \n
diff --git a/src/parser/Parser.h b/src/parser/Parser.h
index f934ec50a..94e0cbb58 100644
--- a/src/parser/Parser.h
+++ b/src/parser/Parser.h
@@ -125,6 +125,11 @@ namespace parser {
 	 */
 	double checked_strtod(const char* str, char** end);
 	
+	/*!
+	 * @brief Skips all non whitespace characters until the next whitespace.
+	 */
+	char* skipWord(char* buf);
+
 	/*!
 	 *	@brief Skips common whitespaces in a string.
 	 */