From 3616bdbf13737af01bf6ab6e838dc3588ba195e9 Mon Sep 17 00:00:00 2001
From: Alexander Bork <alexander.bork@rwth-aachen.de>
Date: Wed, 19 Jun 2019 11:19:14 +0200
Subject: [PATCH] Added two test cases for the FDEP conflict search

---
 .../testfiles/dft/seq_conflict_test.dft       | 12 +++++
 .../testfiles/dft/spare_conflict_test.dft     | 12 +++++
 src/test/storm-dft/api/DftSmtTest.cpp         | 46 +++++++++++++++++++
 3 files changed, 70 insertions(+)
 create mode 100644 resources/examples/testfiles/dft/seq_conflict_test.dft
 create mode 100644 resources/examples/testfiles/dft/spare_conflict_test.dft

diff --git a/resources/examples/testfiles/dft/seq_conflict_test.dft b/resources/examples/testfiles/dft/seq_conflict_test.dft
new file mode 100644
index 000000000..77b22e0f2
--- /dev/null
+++ b/resources/examples/testfiles/dft/seq_conflict_test.dft
@@ -0,0 +1,12 @@
+toplevel "A";
+"A" and "I" "B";
+"SEQ_dynamic" seq "I" "B";
+"B" or "J" "K";
+"DEP1_1" fdep "T1" "I";
+"DEP1_2" fdep "T1" "J";
+"DEP1_3" fdep "T1" "K";
+
+"I" lambda=0.5 dorm=0;
+"J" lambda=0.5 dorm=0;
+"K" lambda=0.5 dorm=0;
+"T1" lambda=0.5 dorm=0;
\ No newline at end of file
diff --git a/resources/examples/testfiles/dft/spare_conflict_test.dft b/resources/examples/testfiles/dft/spare_conflict_test.dft
new file mode 100644
index 000000000..e7d076fa7
--- /dev/null
+++ b/resources/examples/testfiles/dft/spare_conflict_test.dft
@@ -0,0 +1,12 @@
+toplevel "A";
+"A" pand "SP1" "SP2";
+"SP1" wsp "I" "J";
+"SP2" wsp "J" "K";
+"DEP1" fdep "T1" "I";
+"DEP2" fdep "T2" "K";
+
+"I" lambda=0.5 dorm=0;
+"J" lambda=0.5 dorm=0;
+"K" lambda=0.5 dorm=0;
+"T1" lambda=0.5 dorm=0;
+"T2" lambda=0.5 dorm=0;
\ No newline at end of file
diff --git a/src/test/storm-dft/api/DftSmtTest.cpp b/src/test/storm-dft/api/DftSmtTest.cpp
index 95bcad150..a7d5f0993 100644
--- a/src/test/storm-dft/api/DftSmtTest.cpp
+++ b/src/test/storm-dft/api/DftSmtTest.cpp
@@ -56,4 +56,50 @@ namespace {
         EXPECT_EQ(smtChecker.getLeastFailureBound(30), uint64_t(1));
         EXPECT_EQ(smtChecker.getAlwaysFailedBound(30), uint64_t(5));
     }
+
+    TEST(DftSmtTest, FDEPConflictTest) {
+        std::shared_ptr<storm::storage::DFT<double>> dft =
+                storm::api::loadDFTGalileoFile<double>(STORM_TEST_RESOURCES_DIR "/dft/spare_conflict_test.dft");
+        EXPECT_TRUE(storm::api::isWellFormed(*dft));
+        std::vector<bool> true_vector(10, true);
+
+        dft->setDynamicBehaviorInfo();
+        EXPECT_EQ(dft->getDynamicBehavior(), true_vector);
+        storm::modelchecker::DFTASFChecker smtChecker(*dft);
+        smtChecker.convert();
+        smtChecker.toSolver();
+
+        EXPECT_TRUE(smtChecker.getDependencyConflicts().empty());
+    }
+
+    TEST(DftSmtTest, FDEPConflictSPARETest) {
+        std::shared_ptr<storm::storage::DFT<double>> dft =
+                storm::api::loadDFTGalileoFile<double>(STORM_TEST_RESOURCES_DIR "/dft/spare_conflict_test.dft");
+        EXPECT_TRUE(storm::api::isWellFormed(*dft));
+        std::vector<bool> true_vector(10, true);
+
+        dft->setDynamicBehaviorInfo();
+        EXPECT_EQ(dft->getDynamicBehavior(), true_vector);
+        storm::modelchecker::DFTASFChecker smtChecker(*dft);
+        smtChecker.convert();
+        smtChecker.toSolver();
+
+        EXPECT_TRUE(smtChecker.getDependencyConflicts().empty());
+    }
+
+    TEST(DftSmtTest, FDEPConflictSEQTest) {
+        std::shared_ptr<storm::storage::DFT<double>> dft =
+                storm::api::loadDFTGalileoFile<double>(STORM_TEST_RESOURCES_DIR "/dft/seq_conflict_test.dft");
+        EXPECT_TRUE(storm::api::isWellFormed(*dft));
+        std::vector<bool> expected_dynamic_vector(dft->nrElements(), true);
+        expected_dynamic_vector.at(dft->getTopLevelIndex()) = false;
+
+        dft->setDynamicBehaviorInfo();
+        EXPECT_EQ(dft->getDynamicBehavior(), expected_dynamic_vector);
+        storm::modelchecker::DFTASFChecker smtChecker(*dft);
+        smtChecker.convert();
+        smtChecker.toSolver();
+
+        EXPECT_EQ(smtChecker.getDependencyConflicts().size(), uint64_t(3));
+    }
 }
\ No newline at end of file