From f37bcea1eaf96268a96d8bdef371a36e96b32ca1 Mon Sep 17 00:00:00 2001
From: Alexander Bork <alexander.bork@rwth-aachen.de>
Date: Fri, 10 May 2019 14:32:28 +0200
Subject: [PATCH] Added test for bound correction

---
 resources/examples/testfiles/dft/fdep_bound.dft | 15 +++++++++++++++
 src/test/storm-dft/api/DftSmtTest.cpp           | 11 +++++++++++
 2 files changed, 26 insertions(+)
 create mode 100644 resources/examples/testfiles/dft/fdep_bound.dft

diff --git a/resources/examples/testfiles/dft/fdep_bound.dft b/resources/examples/testfiles/dft/fdep_bound.dft
new file mode 100644
index 000000000..4164d52a3
--- /dev/null
+++ b/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;
\ 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 9404c5f5e..95bcad150 100644
--- a/src/test/storm-dft/api/DftSmtTest.cpp
+++ b/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));
+    }
 }
\ No newline at end of file