'Identity updates' can now be described as applying 'true' in PRISM programs.

Former-commit-id: b2f70eb465

src/parser/PrismParser.cpp

@@ -133,7 +133,7 @@ namespace storm {
             assignmentDefinition = (qi::lit("(") > identifier > qi::lit("'") > qi::lit("=") > expressionParser > qi::lit(")"))[qi::_val = phoenix::bind(&PrismParser::createAssignment, phoenix::ref(*this), qi::_1, qi::_2)];
             assignmentDefinition.name("assignment");
             
-            assignmentDefinitionList %= +assignmentDefinition % "&";
+            assignmentDefinitionList = (assignmentDefinition % "&")[qi::_val = qi::_1] | (qi::lit("true"))[qi::_val = phoenix::construct<std::vector<storm::prism::Assignment>>()];
             assignmentDefinitionList.name("assignment list");
             
             updateDefinition = (((expressionParser > qi::lit(":")) | qi::attr(manager->rational(1))) >> assignmentDefinitionList)[qi::_val = phoenix::bind(&PrismParser::createUpdate, phoenix::ref(*this), qi::_1, qi::_2, qi::_r1)];

test/functional/parser/PrismParserTest.cpp

@@ -40,6 +40,7 @@ TEST(PrismParser, SimpleTest) {
         [] x=3 -> 1:(x'=1);
         [] x=3 -> 1:(x'=4);
         [] x=4 -> 1:(x'=5);
+        [] x=5 -> 1: true;
     endmodule)";
     EXPECT_NO_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile"));
     EXPECT_EQ(1, result.getNumberOfModules());