Added test for bound correction

resources/examples/testfiles/dft/fdep_bound.dft

@@ -0,0 +1,15 @@
+toplevel "A";
+"A" or "B" "C";
+"B" and "D" "L";
+"C" and "M" "N";
+"D" and "I" "J" "K";
+"DEP1" fdep "T" "I" "J" "K";
+"DEP2" fdep "D" "L";
+
+"I" lambda=0.5 dorm=0;
+"J" lambda=0.5 dorm=0.5;
+"K" lambda=0.5 dorm=0.5;
+"L" lambda=0.5 dorm=0.5;
+"M" lambda=0.5 dorm=0.5;
+"N" lambda=0.5 dorm=0.5;
+"T" lambda=0.5 dorm=0.5;

src/test/storm-dft/api/DftSmtTest.cpp

@@ -45,4 +45,15 @@ namespace {
         EXPECT_EQ(smtChecker.getLeastFailureBound(30), uint64_t(2));
         EXPECT_EQ(smtChecker.getAlwaysFailedBound(30), uint64_t(4));
     }
+
+    TEST(DftSmtTest, FDEPBoundTest) {
+        std::shared_ptr<storm::storage::DFT<double>> dft =
+                storm::api::loadDFTGalileoFile<double>(STORM_TEST_RESOURCES_DIR "/dft/fdep_bound.dft");
+        EXPECT_TRUE(storm::api::isWellFormed(*dft));
+        storm::modelchecker::DFTASFChecker smtChecker(*dft);
+        smtChecker.convert();
+        smtChecker.toSolver();
+        EXPECT_EQ(smtChecker.getLeastFailureBound(30), uint64_t(1));
+        EXPECT_EQ(smtChecker.getAlwaysFailedBound(30), uint64_t(5));
+    }
 }