From 8f9ff95531b30d121087c30d4ba1f2119f91ae4c Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Mon, 19 Apr 2021 12:25:18 +0200
Subject: [PATCH] Added Test cases for parsing/processing prism programs that
 use unbounded integer variables

---
 src/test/storm/parser/PrismParserTest.cpp   | 17 +++++++++++++++++
 src/test/storm/storage/PrismProgramTest.cpp |  5 ++++-
 2 files changed, 21 insertions(+), 1 deletion(-)

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());
 }