Lra Tests: Added a test case for sound model checking

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,);

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