From 799510044108cea51aac1c1df9fe2fd7bb835f38 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Sun, 12 May 2019 19:21:32 +0200
Subject: [PATCH] Small fixes in DFT tests

---
 .../storm-dft/api/DftModelCheckerTest.cpp     | 25 +++++++++++--------
 1 file changed, 15 insertions(+), 10 deletions(-)

diff --git a/src/test/storm-dft/api/DftModelCheckerTest.cpp b/src/test/storm-dft/api/DftModelCheckerTest.cpp
index dc68faf0e..96f9263c6 100644
--- a/src/test/storm-dft/api/DftModelCheckerTest.cpp
+++ b/src/test/storm-dft/api/DftModelCheckerTest.cpp
@@ -11,6 +11,7 @@ namespace {
         bool useSR;
         bool useMod;
         bool useDC;
+        bool allowDCForRelevantEvents;
     };
 
     class NoOptimizationsConfig {
@@ -18,7 +19,7 @@ namespace {
         typedef double ValueType;
 
         static DftAnalysisConfig createConfig() {
-            return DftAnalysisConfig{false, false, false};
+            return DftAnalysisConfig{false, false, false, true};
         }
     };
 
@@ -27,7 +28,7 @@ namespace {
         typedef double ValueType;
 
         static DftAnalysisConfig createConfig() {
-            return DftAnalysisConfig{false, false, true};
+            return DftAnalysisConfig{false, false, true, true};
         }
     };
 
@@ -36,7 +37,7 @@ namespace {
         typedef double ValueType;
 
         static DftAnalysisConfig createConfig() {
-            return DftAnalysisConfig{false, true, false};
+            return DftAnalysisConfig{false, true, false, true};
         }
     };
 
@@ -45,7 +46,7 @@ namespace {
         typedef double ValueType;
 
         static DftAnalysisConfig createConfig() {
-            return DftAnalysisConfig{true, false, false};
+            return DftAnalysisConfig{true, false, false, true};
         }
     };
 
@@ -54,7 +55,7 @@ namespace {
         typedef double ValueType;
 
         static DftAnalysisConfig createConfig() {
-            return DftAnalysisConfig{true, true, true};
+            return DftAnalysisConfig{true, true, true, true};
         }
     };
 
@@ -77,11 +78,11 @@ namespace {
             std::string property = "Tmin=? [F \"failed\"]";
             std::vector<std::shared_ptr<storm::logic::Formula const>> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(property));
             std::set<size_t> relevantEvents;
-            if (config.useDC) {
+            if (!config.useDC) {
                 relevantEvents = dft->getAllIds();
             }
             typename storm::modelchecker::DFTModelChecker<double>::dft_results results = storm::api::analyzeDFT<double>(*dft, properties, config.useSR, config.useMod,
-                                                                                                                        relevantEvents, true);
+                                                                                                                        relevantEvents, config.allowDCForRelevantEvents);
             return boost::get<double>(results[0]);
         }
 
@@ -91,8 +92,12 @@ namespace {
             std::string property = "Pmin=? [F<=" + std::to_string(bound) + " \"failed\"]";
             std::vector<std::shared_ptr<storm::logic::Formula const>> properties = storm::api::extractFormulasFromProperties(
                     storm::api::parseProperties(property));
-            typename storm::modelchecker::DFTModelChecker<double>::dft_results results = storm::api::analyzeDFT<double>(
-                    *dft, properties, config.useSR, config.useMod, config.useDC, false);
+            std::set<size_t> relevantEvents;
+            if (!config.useDC) {
+                relevantEvents = dft->getAllIds();
+            }
+            typename storm::modelchecker::DFTModelChecker<double>::dft_results results = storm::api::analyzeDFT<double>(*dft, properties, config.useSR, config.useMod,
+                                                                                                                        relevantEvents, config.allowDCForRelevantEvents);
             return boost::get<double>(results[0]);
         }
 
@@ -216,7 +221,7 @@ namespace {
         EXPECT_FLOAT_EQ(result, storm::utility::infinity<double>());
     }
 
-    TYPED_TEST(DftModelCheckerTest, HecsMTTF) {
+    TYPED_TEST(DftModelCheckerTest, HecsReliability) {
         double result = this->analyzeReliability(STORM_TEST_RESOURCES_DIR "/dft/hecs_2_2.dft", 1.0);
         EXPECT_FLOAT_EQ(result, 0.00021997582);
     }