From 98f3cdbfaf83d4c9b2115b200edcc0af6377f603 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Wed, 17 Apr 2019 19:19:08 +0200
Subject: [PATCH] Adapted tests to changes

---
 .../storm-dft/api/DftModelBuildingTest.cpp    | 44 ++++++++++++++++---
 .../storm-dft/api/DftModelCheckerTest.cpp     |  8 +---
 2 files changed, 39 insertions(+), 13 deletions(-)

diff --git a/src/test/storm-dft/api/DftModelBuildingTest.cpp b/src/test/storm-dft/api/DftModelBuildingTest.cpp
index cd71be290..46cab4f61 100644
--- a/src/test/storm-dft/api/DftModelBuildingTest.cpp
+++ b/src/test/storm-dft/api/DftModelBuildingTest.cpp
@@ -32,9 +32,8 @@ namespace {
         storm::builder::ExplicitDFTModelBuilder<double> builder2(*dft, symmetries, relevantEvents, false);
         builder2.buildModel(0, 0.0);
         model = builder2.getModel();
-        EXPECT_EQ(170ul, model->getNumberOfStates());
-        EXPECT_EQ(688ul, model->getNumberOfTransitions());
-
+        EXPECT_EQ(448ul, model->getNumberOfStates());
+        EXPECT_EQ(1260ul, model->getNumberOfTransitions());
 
         // Set relevant events (H)
         relevantEvents.clear();
@@ -43,8 +42,8 @@ namespace {
         storm::builder::ExplicitDFTModelBuilder<double> builder3(*dft, symmetries, relevantEvents, false);
         builder3.buildModel(0, 0.0);
         model = builder3.getModel();
-        EXPECT_EQ(11ul, model->getNumberOfStates());
-        EXPECT_EQ(23ul, model->getNumberOfTransitions());
+        EXPECT_EQ(12ul, model->getNumberOfStates());
+        EXPECT_EQ(25ul, model->getNumberOfTransitions());
 
 
         // Set relevant events (H, I)
@@ -55,8 +54,39 @@ namespace {
         storm::builder::ExplicitDFTModelBuilder<double> builder4(*dft, symmetries, relevantEvents, false);
         builder4.buildModel(0, 0.0);
         model = builder4.getModel();
-        EXPECT_EQ(14ul, model->getNumberOfStates());
-        EXPECT_EQ(30ul, model->getNumberOfTransitions());
+        EXPECT_EQ(16ul, model->getNumberOfStates());
+        EXPECT_EQ(33ul, model->getNumberOfTransitions());
+
+        // Set relevant events (none)
+        relevantEvents.clear();
+        // Build model
+        storm::builder::ExplicitDFTModelBuilder<double> builder5(*dft, symmetries, relevantEvents, true);
+        builder5.buildModel(0, 0.0);
+        model = builder5.getModel();
+        EXPECT_EQ(8ul, model->getNumberOfStates());
+        EXPECT_EQ(13ul, model->getNumberOfTransitions());
+
+        // Set relevant events (all)
+        relevantEvents = dft->getAllIds();
+        // Build model
+        storm::builder::ExplicitDFTModelBuilder<double> builder6(*dft, symmetries, relevantEvents, true);
+        builder6.buildModel(0, 0.0);
+        model = builder6.getModel();
+        EXPECT_EQ(8ul, model->getNumberOfStates());
+        EXPECT_EQ(13ul, model->getNumberOfTransitions());
+
+
+        // Set relevant events (H, I)
+        relevantEvents.clear();
+        relevantEvents.insert(dft->getIndex("H"));
+        relevantEvents.insert(dft->getIndex("I"));
+        // Build model
+        storm::builder::ExplicitDFTModelBuilder<double> builder7(*dft, symmetries, relevantEvents, true);
+        builder7.buildModel(0, 0.0);
+        model = builder7.getModel();
+        EXPECT_EQ(8ul, model->getNumberOfStates());
+        EXPECT_EQ(13ul, model->getNumberOfTransitions());
+
     }
 
 }
diff --git a/src/test/storm-dft/api/DftModelCheckerTest.cpp b/src/test/storm-dft/api/DftModelCheckerTest.cpp
index f49639ba3..73550a3af 100644
--- a/src/test/storm-dft/api/DftModelCheckerTest.cpp
+++ b/src/test/storm-dft/api/DftModelCheckerTest.cpp
@@ -155,12 +155,8 @@ namespace {
         result = this->analyzeMTTF(STORM_TEST_RESOURCES_DIR "/dft/pdep3.dft");
         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);
-            }
+            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");