Merge branch 'master' of https://sselab.de/lab9/private/git/storm into philippTopologicalRevival

Former-commit-id: af74c0e14d

examples/mdp/asynchronous_leader/leader4.nm

@@ -4,7 +4,7 @@
 
 mdp
 
-const N= 4; // number of processes
+const int N= 4; // number of processes
 
 //----------------------------------------------------------------------------------------------------------------------------
 module process1

examples/mdp/asynchronous_leader/leader5.nm

@@ -4,7 +4,7 @@
 
 mdp
 
-const N= 5; // number of processes
+const int N= 5; // number of processes
 
 //----------------------------------------------------------------------------------------------------------------------------
 module process1

examples/mdp/asynchronous_leader/leader6.nm

@@ -4,7 +4,7 @@
 
 mdp
 
-const N= 6; // number of processes
+const int N= 6; // number of processes
 
 //----------------------------------------------------------------------------------------------------------------------------
 module process1

examples/mdp/asynchronous_leader/leader7.nm

@@ -4,7 +4,7 @@
 
 mdp
 
-const N= 7; // number of processes
+const int N= 7; // number of processes
 
 //----------------------------------------------------------------------------------------------------------------------------
 module process1

src/exceptions/ExceptionMacros.h

@@ -16,8 +16,13 @@ extern log4cplus::Logger logger;
         assert(cond);                           \
     }                                           \
 } while (false)
+#define LOG_DEBUG(message)                      \
+{                                               \
+    LOG4CPLUS_DEBUG(logger, message);           \
+} while (false)
 #else
 #define LOG_ASSERT(cond, message) /* empty */
+#define LOG_DEBUG(message) /* empty */
 #endif
 
 #define LOG_THROW(cond, exception, message)     \

src/parser/PrismParser.cpp

@@ -41,6 +41,7 @@ namespace storm {
                 // Start first run.
                 bool succeeded = qi::phrase_parse(iter, last, grammar, boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol, result);
                 LOG_THROW(succeeded,  storm::exceptions::WrongFormatException, "Parsing failed in first pass.");
+                LOG_DEBUG("First pass of parsing PRISM input finished.");
                 
                 // Start second run.
                 first = PositionIteratorType(input.begin());
@@ -138,7 +139,7 @@ namespace storm {
             updateListDefinition %= +updateDefinition(qi::_r1) % "+";
             updateListDefinition.name("update list");
             
-            commandDefinition = (qi::lit("[") > -(identifier[qi::_a = qi::_1]) > qi::lit("]") > expressionParser > qi::lit("->") > updateListDefinition(qi::_r1) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createCommand, phoenix::ref(*this), qi::_a, qi::_2, qi::_3, qi::_r1)];
+            commandDefinition = qi::lit("[") > +(qi::char_ - qi::lit(";")) > qi::lit(";")[qi::_val = phoenix::construct<storm::prism::Command>()];
             commandDefinition.name("command definition");
             
             moduleDefinition = ((qi::lit("module") >> identifier >> *(variableDefinition(qi::_a, qi::_b))) > +commandDefinition(qi::_r1) > qi::lit("endmodule"))[qi::_val = phoenix::bind(&PrismParser::createModule, phoenix::ref(*this), qi::_1, qi::_a, qi::_b, qi::_2, qi::_r1)];
@@ -188,6 +189,10 @@ namespace storm {
         }
         
         void PrismParser::moveToSecondRun() {
+            // In the second run, we actually need to parse the commands instead of just skipping them,
+            // so we adapt the rule for parsing commands.
+            commandDefinition = (qi::lit("[") > -(identifier[qi::_a = qi::_1]) > qi::lit("]") > expressionParser > qi::lit("->") > updateListDefinition(qi::_r1) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createCommand, phoenix::ref(*this), qi::_a, qi::_2, qi::_3, qi::_r1)];
+            
             this->secondRun = true;
             this->expressionParser.setIdentifierMapping(&this->identifiers_);
         }