From b9bd9e2fd4a934c52272ef824de24916ecacdea2 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Thu, 20 May 2021 14:25:37 -0700 Subject: [PATCH] parser test for nary predicates --- src/test/storm/parser/PrismParserTest.cpp | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/src/test/storm/parser/PrismParserTest.cpp b/src/test/storm/parser/PrismParserTest.cpp index ad509af46..14a0362c2 100644 --- a/src/test/storm/parser/PrismParserTest.cpp +++ b/src/test/storm/parser/PrismParserTest.cpp @@ -158,6 +158,25 @@ TEST(PrismParser, POMDPInputTest) { EXPECT_NO_THROW(result = storm::parser::PrismParser::parseFromString(testInput2, "testfile")); } +TEST(PrismParser, NAryPredicates) { + std::string testInput = + R"(dtmc + + module example + s : [0..4] init 0; + i : bool init true; + [] s=0 -> 0.5: (s'=1) & (i'=false) + 0.5: (s'=2) & (i'=false); + [] s=1 | s=2 -> 1: (s'=3) & (i'=true); + [r] s=1 -> 1: (s'=4) & (i'=true); + [r] s=2 -> 1: (s'=3) & (i'=true); + endmodule + + label "test" = atMostOneOf(s=0, s=3, s=4); + label "test2" = exactlyOneOf(s=0, i, !i & s=3); + )"; + + EXPECT_NO_THROW(result = storm::parser::PrismParser::parseFromString(testInput2, "testfile")); +} TEST(PrismParser, IllegalInputTest) { std::string testInput =