From f16b4885900e0b66890618ab9399f0223ed5fd63 Mon Sep 17 00:00:00 2001
From: Alexander Bork <alexander.bork@rwth-aachen.de>
Date: Thu, 25 Apr 2019 17:06:47 +0200
Subject: [PATCH] Added conservative lower bound correction

---
 ...{spareTwoModules.dft => spare_two_modules.dft} |  0
 src/storm-dft/modelchecker/dft/DFTASFChecker.cpp  | 15 ++++++++++++++-
 src/storm-dft/modelchecker/dft/DFTASFChecker.h    | 12 +++++++++++-
 src/test/storm-dft/api/DftSmtTest.cpp             |  2 +-
 4 files changed, 26 insertions(+), 3 deletions(-)
 rename resources/examples/testfiles/dft/{spareTwoModules.dft => spare_two_modules.dft} (100%)

diff --git a/resources/examples/testfiles/dft/spareTwoModules.dft b/resources/examples/testfiles/dft/spare_two_modules.dft
similarity index 100%
rename from resources/examples/testfiles/dft/spareTwoModules.dft
rename to resources/examples/testfiles/dft/spare_two_modules.dft
diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp
index 59b736c68..051b2a555 100644
--- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp
+++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp
@@ -504,6 +504,15 @@ namespace storm {
             return checkTleFailsWithEq(notFailed);
         }
 
+        uint64_t DFTASFChecker::correctLowerBound(uint64_t bound) {
+            STORM_LOG_ASSERT(solver, "SMT Solver was not initialized, call toSolver() before checking queries");
+            STORM_LOG_DEBUG("Lower bound correction - try to correct bound " << std::to_string(bound));
+            // placeholder, set lower bound to 1 to prevent loss of precision
+            return 1;
+            // TODO correction mechanism
+            // easy method ("climb down" all direct predecessor states of bound) does not work
+        }
+
         uint64_t DFTASFChecker::getLeastFailureBound(uint_fast64_t timeout) {
             STORM_LOG_TRACE("Compute lower bound for number of BE failures necessary for the DFT to fail");
             STORM_LOG_ASSERT(solver, "SMT Solver was not initialized, call toSolver() before checking queries");
@@ -514,7 +523,11 @@ namespace storm {
                 unsetSolverTimeout();
                 switch (tmp_res) {
                     case storm::solver::SmtSolver::CheckResult::Sat:
-                        return bound;
+                        if (dft.getDependencies().size() > 0) {
+                            return correctLowerBound(bound);
+                        } else {
+                            return bound;
+                        }
                     case storm::solver::SmtSolver::CheckResult::Unknown:
                         STORM_LOG_DEBUG("Lower bound: Solver returned 'Unknown'");
                         return bound;
diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.h b/src/storm-dft/modelchecker/dft/DFTASFChecker.h
index d8da63dce..4ebe91f0b 100644
--- a/src/storm-dft/modelchecker/dft/DFTASFChecker.h
+++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.h
@@ -74,7 +74,8 @@ namespace storm {
             uint64_t getLeastFailureBound(uint_fast64_t timeout = 10);
 
             /**
-             * Get the number of BE failures for which the TLE always fails (upper bound for number of failures to check)
+             * Get the number of BE failures for which the TLE always fails (upper bound for number of failures to check).
+             * Note that the returned value may be higher than the real one when dependencies are present.
              *
              * @param timeout timeout for each query in seconds, defaults to 10 seconds
              * @return the number
@@ -94,6 +95,15 @@ namespace storm {
             void unsetSolverTimeout();
             
         private:
+            /**
+             * Helper function for correction of least failure bound when dependencies are present
+             *
+             * @param state number of the state in the sequence to check
+             * @param bound known lower bound to be corrected
+             * @return the corrected bound, 1 if correction cannot be completed
+             */
+            uint64_t correctLowerBound(uint64_t bound);
+
             uint64_t getClaimVariableIndex(uint64_t spareIndex, uint64_t childIndex) const;
 
             /**
diff --git a/src/test/storm-dft/api/DftSmtTest.cpp b/src/test/storm-dft/api/DftSmtTest.cpp
index bc83caa3b..9404c5f5e 100644
--- a/src/test/storm-dft/api/DftSmtTest.cpp
+++ b/src/test/storm-dft/api/DftSmtTest.cpp
@@ -26,7 +26,7 @@ namespace {
 
     TEST(DftSmtTest, SpareTest) {
         std::shared_ptr<storm::storage::DFT<double>> dft =
-                storm::api::loadDFTGalileoFile<double>(STORM_TEST_RESOURCES_DIR "/dft/spareTwoModules.dft");
+                storm::api::loadDFTGalileoFile<double>(STORM_TEST_RESOURCES_DIR "/dft/spare_two_modules.dft");
         EXPECT_TRUE(storm::api::isWellFormed(*dft));
         storm::modelchecker::DFTASFChecker smtChecker(*dft);
         smtChecker.convert();