From d9db3f84b6b020c33a4c67fc6a4f15bcb5b3b890 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Wed, 21 Mar 2018 13:43:35 +0100
Subject: [PATCH] Fixed dft tests

---
 .../storm-dft/api/DftModelCheckerTest.cpp     | 62 ++++++++++++-------
 1 file changed, 38 insertions(+), 24 deletions(-)

diff --git a/src/test/storm-dft/api/DftModelCheckerTest.cpp b/src/test/storm-dft/api/DftModelCheckerTest.cpp
index 8c57795d6..902108018 100644
--- a/src/test/storm-dft/api/DftModelCheckerTest.cpp
+++ b/src/test/storm-dft/api/DftModelCheckerTest.cpp
@@ -95,13 +95,13 @@ namespace {
 
     TYPED_TEST(DftModelCheckerTest, VotingMTTF) {
         double result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/voting.dft");
-        EXPECT_FLOAT_EQ(result, 5/3);
+        EXPECT_FLOAT_EQ(result, 5/3.0);
         result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/voting2.dft");
-        EXPECT_FLOAT_EQ(result, 10/17);
+        EXPECT_FLOAT_EQ(result, 10/17.0);
         result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/voting3.dft");
-        EXPECT_FLOAT_EQ(result, 1.73562);
+        EXPECT_FLOAT_EQ(result, 1.7356173);
         result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/voting4.dft");
-        EXPECT_FLOAT_EQ(result, 5/6);
+        EXPECT_FLOAT_EQ(result, 5/6.0);
     }
 
     TYPED_TEST(DftModelCheckerTest, PandMTTF) {
@@ -115,45 +115,59 @@ namespace {
     }
 
     TYPED_TEST(DftModelCheckerTest, FdepMTTF) {
-        double result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/fdep.dft");
-        EXPECT_FLOAT_EQ(result, 2/3);
-        result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/fdep2.dft");
+        double result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/fdep2.dft");
         EXPECT_FLOAT_EQ(result, 2);
         result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/fdep3.dft");
         EXPECT_FLOAT_EQ(result, 2.5);
-        result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/fdep4.dft");
-        EXPECT_FLOAT_EQ(result, 1);
-        result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/fdep5.dft");
-        EXPECT_FLOAT_EQ(result, 3);
+        if (this->getConfig().useMod) {
+            EXPECT_THROW(this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/fdep.dft"), storm::exceptions::NotSupportedException);
+            EXPECT_THROW(this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/fdep4.dft"), storm::exceptions::NotSupportedException);
+            EXPECT_THROW(this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/fdep5.dft"), storm::exceptions::NotSupportedException);
+        } else {
+            result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/fdep.dft");
+            EXPECT_FLOAT_EQ(result, 2/3.0);
+            result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/fdep4.dft");
+            EXPECT_FLOAT_EQ(result, 1);
+            result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/fdep5.dft");
+            EXPECT_FLOAT_EQ(result, 3);
+        }
     }
 
     TYPED_TEST(DftModelCheckerTest, PdepMTTF) {
         double result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/pdep.dft");
-        EXPECT_FLOAT_EQ(result, 8/3);
-        result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/pdep2.dft");
-        EXPECT_FLOAT_EQ(result, 38/15);
+        EXPECT_FLOAT_EQ(result, 8/3.0);
         result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/pdep3.dft");
-        EXPECT_FLOAT_EQ(result, 2.79167);
-        result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/pdep4.dft");
-        EXPECT_EQ(result, storm::utility::infinity<double>());
+        EXPECT_FLOAT_EQ(result, 67/24.0);
+        if (this->getConfig().useMod) {
+            if (!this->getConfig().useDC) {
+                EXPECT_THROW(this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/pdep2.dft"), storm::exceptions::NotSupportedException);
+            } else {
+                result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/pdep2.dft");
+                EXPECT_FLOAT_EQ(result, 38/15.0);
+            }
+            EXPECT_THROW(this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/pdep4.dft"), storm::exceptions::NotSupportedException);
+        } else {
+            result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/pdep4.dft");
+            EXPECT_EQ(result, storm::utility::infinity<double>());
+        }
     }
     TYPED_TEST(DftModelCheckerTest, SpareMTTF) {
         double result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/spare.dft");
-        EXPECT_FLOAT_EQ(result, 3.53846);
+        EXPECT_FLOAT_EQ(result, 46/13.0);
         result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/spare2.dft");
-        EXPECT_FLOAT_EQ(result, 1.86957);
+        EXPECT_FLOAT_EQ(result, 43/23.0);
         result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/spare3.dft");
-        EXPECT_FLOAT_EQ(result, 1.27273);
+        EXPECT_FLOAT_EQ(result, 14/11.0);
         result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/spare4.dft");
-        EXPECT_FLOAT_EQ(result, 4.8459);
+        EXPECT_FLOAT_EQ(result, 4.8458967);
         result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/spare5.dft");
-        EXPECT_FLOAT_EQ(result, 8/3);
+        EXPECT_FLOAT_EQ(result, 8/3.0);
         result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/spare6.dft");
         EXPECT_FLOAT_EQ(result, 1.4);
         result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/spare7.dft");
-        EXPECT_FLOAT_EQ(result, 3.67333);
+        EXPECT_FLOAT_EQ(result, 3.6733334);
         result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/spare8.dft");
-        EXPECT_FLOAT_EQ(result, 4.78846); // DFTCalc says 4.33779
+        EXPECT_FLOAT_EQ(result, 4.78846); // DFTCalc has result of 4.33779 due to different semantics of nested spares
     }
     TYPED_TEST(DftModelCheckerTest, SeqMTTF) {
         double result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/seq.dft");