From 3f2a5ffa62a15d9cdbfdf78c5c24c3bef2a47663 Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Thu, 27 Aug 2020 17:32:28 +0200
Subject: [PATCH] Lra Tests: Added a test case for sound model checking

---
 .../csl/LraCtmcCslModelCheckerTest.cpp          | 17 ++++++++++++++++-
 .../prctl/mdp/LraMdpPrctlModelCheckerTest.cpp   | 15 ++++++++++++++-
 2 files changed, 30 insertions(+), 2 deletions(-)

diff --git a/src/test/storm/modelchecker/csl/LraCtmcCslModelCheckerTest.cpp b/src/test/storm/modelchecker/csl/LraCtmcCslModelCheckerTest.cpp
index 75e41cdf2..f0e1dd5d8 100755
--- a/src/test/storm/modelchecker/csl/LraCtmcCslModelCheckerTest.cpp
+++ b/src/test/storm/modelchecker/csl/LraCtmcCslModelCheckerTest.cpp
@@ -209,6 +209,20 @@ namespace {
         }
     };
     
+    class SoundEnvironment {
+    public:
+        static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
+        static const CtmcEngine engine = CtmcEngine::PrismSparse;
+        static const bool isExact = false;
+        typedef double ValueType;
+        typedef storm::models::sparse::Ctmc<ValueType> ModelType;
+        static storm::Environment createEnvironment() {
+            storm::Environment env;
+            env.solver().setForceSoundness(true);
+            return env;
+        }
+    };
+    
     template<typename TestType>
     class LraCtmcCslModelCheckerTest : public ::testing::Test {
     public:
@@ -317,7 +331,8 @@ namespace {
             GBSparseNativeSorEnvironment,
             DistrSparseGmmxxGmresIluEnvironment,
             DistrSparseEigenDoubleLUEnvironment,
-            ValueIterationSparseEnvironment
+            ValueIterationSparseEnvironment,
+            SoundEnvironment
         > TestingTypes;
     
     TYPED_TEST_SUITE(LraCtmcCslModelCheckerTest, TestingTypes,);
diff --git a/src/test/storm/modelchecker/prctl/mdp/LraMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/prctl/mdp/LraMdpPrctlModelCheckerTest.cpp
index 0dc55deb9..64ce6342d 100755
--- a/src/test/storm/modelchecker/prctl/mdp/LraMdpPrctlModelCheckerTest.cpp
+++ b/src/test/storm/modelchecker/prctl/mdp/LraMdpPrctlModelCheckerTest.cpp
@@ -53,6 +53,18 @@ namespace {
         }
     };
     
+    class SparseSoundEnvironment {
+    public:
+        static const bool isExact = false;
+        typedef double ValueType;
+        typedef storm::models::sparse::Mdp<ValueType> ModelType;
+        static storm::Environment createEnvironment() {
+            storm::Environment env;
+            env.solver().setForceSoundness(true);
+            return env;
+        }
+    };
+    
     class SparseRationalLinearProgrammingEnvironment {
     public:
         static const bool isExact = true;
@@ -100,7 +112,8 @@ namespace {
   
     typedef ::testing::Types<
             SparseValueTypeValueIterationEnvironment,
-            SparseValueTypeLinearProgrammingEnvironment
+            SparseValueTypeLinearProgrammingEnvironment,
+            SparseSoundEnvironment
 #ifdef STORM_HAVE_Z3_OPTIMIZE
             , SparseRationalLinearProgrammingEnvironment
 #endif