diff --git a/src/test/storm/parser/PrismParserTest.cpp b/src/test/storm/parser/PrismParserTest.cpp index 9caba734f..ad509af46 100644 --- a/src/test/storm/parser/PrismParserTest.cpp +++ b/src/test/storm/parser/PrismParserTest.cpp @@ -28,6 +28,7 @@ TEST(PrismParser, SimpleTest) { EXPECT_NO_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile")); EXPECT_EQ(1ul, result.getNumberOfModules()); EXPECT_EQ(storm::prism::Program::ModelType::DTMC, result.getModelType()); + EXPECT_FALSE(result.hasUnboundedVariables()); testInput = R"(mdp @@ -44,6 +45,7 @@ TEST(PrismParser, SimpleTest) { EXPECT_NO_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile")); EXPECT_EQ(1ul, result.getNumberOfModules()); EXPECT_EQ(storm::prism::Program::ModelType::MDP, result.getModelType()); + EXPECT_FALSE(result.hasUnboundedVariables()); } TEST(PrismParser, ComplexTest) { @@ -97,8 +99,23 @@ TEST(PrismParser, ComplexTest) { EXPECT_EQ(3ul, result.getNumberOfModules()); EXPECT_EQ(2ul, result.getNumberOfRewardModels()); EXPECT_EQ(1ul, result.getNumberOfLabels()); + EXPECT_FALSE(result.hasUnboundedVariables()); } +TEST(PrismParser, UnboundedTest) { + std::string testInput = + R"(mdp + module main + b : int; + [a] true -> 1: (b'=b+1); + endmodule)"; + + storm::prism::Program result; + EXPECT_NO_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile")); + EXPECT_EQ(1ul, result.getNumberOfModules()); + EXPECT_EQ(storm::prism::Program::ModelType::MDP, result.getModelType()); + EXPECT_TRUE(result.hasUnboundedVariables()); +} TEST(PrismParser, POMDPInputTest) { std::string testInput = diff --git a/src/test/storm/storage/PrismProgramTest.cpp b/src/test/storm/storage/PrismProgramTest.cpp index dc3ba04b6..73f019e30 100644 --- a/src/test/storm/storage/PrismProgramTest.cpp +++ b/src/test/storm/storage/PrismProgramTest.cpp @@ -1,5 +1,5 @@ -#include "test/storm_gtest.h" #include "storm-config.h" +#include "test/storm_gtest.h" #include "storm-parsers/parser/PrismParser.h" #include "storm/utility/solver.h" @@ -163,4 +163,7 @@ TEST(PrismProgramTest, ConvertToJani) { ASSERT_NO_THROW(prismProgram = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/nand-5-2.pm")); ASSERT_NO_THROW(janiModel = prismProgram.toJani()); + + ASSERT_NO_THROW(prismProgram = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/unbounded.nm")); + ASSERT_NO_THROW(janiModel = prismProgram.toJani()); }