Browse Source

parser test for nary predicates

tempestpy_adaptions
Sebastian Junges 4 years ago
parent
commit
b9bd9e2fd4
  1. 19
      src/test/storm/parser/PrismParserTest.cpp

19
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 =

Loading…
Cancel
Save