Added two test cases for the FDEP conflict search

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;

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;

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));
+    }
 }