diff --git a/src/test/storm/parser/PrismParserTest.cpp b/src/test/storm/parser/PrismParserTest.cpp index 73c53347c..9caba734f 100644 --- a/src/test/storm/parser/PrismParserTest.cpp +++ b/src/test/storm/parser/PrismParserTest.cpp @@ -99,6 +99,49 @@ TEST(PrismParser, ComplexTest) { EXPECT_EQ(1ul, result.getNumberOfLabels()); } + +TEST(PrismParser, POMDPInputTest) { + std::string testInput = + R"(pomdp + + observables + i + endobservables + + 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 + + )"; + + storm::prism::Program result; + EXPECT_NO_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile")); + + std::string testInput2 = + R"(pomdp + + observable intermediate = s=1 | s=2; + + module example + s : [0..4] init 0; + [] s=0 -> 0.5: (s'=1) + 0.5: (s'=2); + [l] s=1 -> 1: (s'=3); + [l] s=2 -> 1: (s'=4); + [r] s=1 -> 1: (s'=4); + [r] s=2 -> 1: (s'=3); + endmodule + + )"; + + EXPECT_NO_THROW(result = storm::parser::PrismParser::parseFromString(testInput2, "testfile")); +} + + TEST(PrismParser, IllegalInputTest) { std::string testInput = R"(ctmc @@ -224,4 +267,3 @@ TEST(PrismParser, IllegalInputTest) { TEST(PrismParser, IllegalSynchronizedWriteTest) { STORM_SILENT_EXPECT_THROW(storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/coin2-2-illegalSynchronizingWrite.nm"), storm::exceptions::WrongFormatException); } -