Added conservative lower bound correction

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;

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;
 
             /**

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();