From d62539165e028328e4d58aabca76c5a8f3c08398 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 3 Aug 2015 15:36:45 +0200 Subject: [PATCH] 'Identity updates' can now be described as applying 'true' in PRISM programs. Former-commit-id: b2f70eb465618290b2bd9467bd8254ef2a49c273 --- src/parser/PrismParser.cpp | 2 +- test/functional/parser/PrismParserTest.cpp | 1 + 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp index a7e1f522d..bff8c71b8 100644 --- a/src/parser/PrismParser.cpp +++ b/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>()]; 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)]; diff --git a/test/functional/parser/PrismParserTest.cpp b/test/functional/parser/PrismParserTest.cpp index a3fbc7526..e386b7682 100644 --- a/test/functional/parser/PrismParserTest.cpp +++ b/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());