Reworked lower bound computation

src/storm-dft/modelchecker/dft/DFTASFChecker.cpp

@@ -558,21 +558,24 @@ namespace storm {
         }
 
         storm::solver::SmtSolver::CheckResult
-        DFTASFChecker::checkFailsWithLessThanMarkovianState(uint64_t checkNumber) {
+        DFTASFChecker::checkFailsLeqWithEqNonMarkovianState(uint64_t checkbound, uint64_t nrNonMarkovian) {
             STORM_LOG_ASSERT(solver, "SMT Solver was not initialized, call toSolver() before checking queries");
-            uint64_t nrMarkovian = dft.nrBasicElements();
             std::vector<uint64_t> markovianIndices;
             // Get Markovian variable indices
-            for (uint64_t i = 0; i < nrMarkovian; ++i) {
+            for (uint64_t i = 0; i < checkbound; ++i) {
                 markovianIndices.push_back(markovianVariables.at(i));
             }
             // Set backtracking marker to check several properties without reconstructing DFT encoding
             solver->push();
-            // Constraint that toplevel element can fail with less than 'checkNumber' Markovian states visited
-            std::shared_ptr<SmtConstraint> countConstr = std::make_shared<BoolCountIsLessConstant>(
-                    markovianIndices, checkNumber);
+
+            std::shared_ptr<SmtConstraint> tleFailedConstr = std::make_shared<IsLessEqualConstant>(
+                    timePointVariables.at(dft.getTopLevelIndex()), checkbound);
             std::shared_ptr<storm::expressions::ExpressionManager> manager = solver->getManager().getSharedPointer();
-            solver->add(countConstr->toExpression(varNames, manager));
+            solver->add(tleFailedConstr->toExpression(varNames, manager));
+            // TODO comment
+            std::shared_ptr<SmtConstraint> nonMarkovianConstr = std::make_shared<FalseCountIsEqualConstant>(
+                    markovianIndices, nrNonMarkovian);
+            solver->add(nonMarkovianConstr->toExpression(varNames, manager));
             storm::solver::SmtSolver::CheckResult res = solver->check();
             solver->pop();
             return res;
@@ -589,7 +592,7 @@ namespace storm {
             // Set backtracking marker to check several properties without reconstructing DFT encoding
             solver->push();
             // Constraint that toplevel element can fail with less than 'checkNumber' Markovian states visited
-            std::shared_ptr<SmtConstraint> countConstr = std::make_shared<BoolCountIsConstantValue>(
+            std::shared_ptr<SmtConstraint> countConstr = std::make_shared<TrueCountIsConstantValue>(
                     markovianIndices, timepoint);
             // Constraint that TLE fails at timepoint
             std::shared_ptr<SmtConstraint> timepointConstr = std::make_shared<IsConstantValue>(
@@ -605,24 +608,50 @@ namespace storm {
         uint64_t DFTASFChecker::correctLowerBound(uint64_t bound, uint_fast64_t timeout) {
             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));
-            while (bound >= 0) {
+            uint64_t boundCandidate = bound;
+            uint64_t nrDepEvents = 0;
+            uint64_t nrNonMarkovian = 0;
+            // Count dependent events
+            for (size_t i = 0; i < dft.nrElements(); ++i) {
+                std::shared_ptr<storm::storage::DFTElement<ValueType> const> element = dft.getElement(i);
+                if (element->type() == storm::storage::DFTElementType::BE) {
+                    auto be = std::static_pointer_cast<storm::storage::DFTBE<double> const>(element);
+                    if (be->hasIngoingDependencies()) {
+                        ++nrDepEvents;
+                    }
+                }
+            }
+            // Only need to check as long as bound candidate + nr of non-Markovians to check is smaller than number of dependent events
+            while (nrNonMarkovian <= nrDepEvents && boundCandidate > 0) {
+                STORM_LOG_TRACE(
+                        "Lower bound correction - check possible bound " << std::to_string(boundCandidate) << " with "
+                                                                         << std::to_string(nrNonMarkovian)
+                                                                         << " non-Markovian states");
                 setSolverTimeout(timeout * 1000);
-                storm::solver::SmtSolver::CheckResult tmp_res = checkFailsWithLessThanMarkovianState(bound);
+                storm::solver::SmtSolver::CheckResult tmp_res =
+                        checkFailsLeqWithEqNonMarkovianState(boundCandidate + nrNonMarkovian, nrNonMarkovian);
                 unsetSolverTimeout();
                 switch (tmp_res) {
-                    case storm::solver::SmtSolver::CheckResult::Unsat:
-                        STORM_LOG_DEBUG("Lower bound correction - corrected bound to " << std::to_string(bound));
-                        return bound;
+                    case storm::solver::SmtSolver::CheckResult::Sat:
+                        /* If SAT, there is a sequence where only boundCandidate-many BEs fail directly and rest is nonMarkovian.
+                         * Bound candidate is vaild, therefore check the next one */
+                        STORM_LOG_TRACE("Lower bound correction - SAT");
+                        --boundCandidate;
+                        break;
                     case storm::solver::SmtSolver::CheckResult::Unknown:
-                        STORM_LOG_DEBUG("Lower bound correction - Solver returned 'Unknown', corrected to "
-                                                << std::to_string(bound));
-                        return bound;
+                        // If any query returns unknown, we cannot be sure about the bound and fall back to the naive one
+                        STORM_LOG_DEBUG("Lower bound correction - Solver returned 'Unknown', corrected to 1");
+                        return 1;
                     default:
-                        --bound;
+                        // if query is UNSAT, increase number of non-Markovian states and try again
+                        STORM_LOG_TRACE("Lower bound correction - UNSAT");
+                        ++nrNonMarkovian;
                         break;
                 }
             }
-            return bound;
+            // if for one candidate all queries are UNSAT, it is not valid. Return last valid candidate
+            STORM_LOG_DEBUG("Lower bound correction - corrected bound to " << std::to_string(boundCandidate + 1));
+            return boundCandidate + 1;
         }
 
         uint64_t DFTASFChecker::correctUpperBound(uint64_t bound, uint_fast64_t timeout) {

src/storm-dft/modelchecker/dft/DFTASFChecker.h

@@ -110,13 +110,16 @@ namespace storm {
             
         private:
             /**
-             * Helper function that checks if the DFT can fail while visiting less than a given number of Markovian states
+             * Helper function to check if the TLE fails before or at a given timepoint while visiting exactly
+             * a given number of non-Markovian states
              *
-             * @param checkNumber the number to check against
-             * @return "Sat" if a sequence of BE failures exists such that less than checkNumber Markovian states are visited,
+             * @param checkbound timepoint to check against
+             * @param nrNonMarkovian the number of non-Markovian states to check against
+             * @return "Sat" if a sequence of BE failures exists such that the constraints are satisfied,
              * "Unsat" if it does not, otherwise "Unknown"
              */
-            storm::solver::SmtSolver::CheckResult checkFailsWithLessThanMarkovianState(uint64_t checkNumber);
+            storm::solver::SmtSolver::CheckResult
+            checkFailsLeqWithEqNonMarkovianState(uint64_t checkbound, uint64_t nrNonMarkovian);
 
             /**
              * Helper function that checks if the DFT can fail at a timepoint while visiting less than a given number of Markovian states
@@ -128,7 +131,10 @@ namespace storm {
             storm::solver::SmtSolver::CheckResult checkFailsAtTimepointWithOnlyMarkovianState(uint64_t timepoint);
 
             /**
-             * Helper function for correction of least failure bound when dependencies are present
+             * Helper function for correction of least failure bound when dependencies are present.
+             * The main idea is to check if a later point of failure for the TLE than the pre-computed bound exists, but
+             * up until that point the number of non-Markovian states visited is so large, that less than the pre-computed bound BEs fail by themselves.
+             * The corrected bound is then (newTLEFailureTimepoint)-(nrNonMarkovianStatesVisited). This term is minimized.
              *
              * @param bound known lower bound to be corrected
              * @param timeout timeout timeout for each query in seconds

src/storm-dft/modelchecker/dft/SmtConstraint.cpp

@@ -598,9 +598,9 @@ namespace storm {
             std::shared_ptr<SmtConstraint> elseConstraint;
         };
 
-        class BoolCountIsLessConstant : public SmtConstraint {
+        class TrueCountIsLessConstant : public SmtConstraint {
         public:
-            BoolCountIsLessConstant(std::vector<uint64_t> varIndices, uint64_t val) : varIndices(varIndices),
+            TrueCountIsLessConstant(std::vector<uint64_t> varIndices, uint64_t val) : varIndices(varIndices),
                                                                                       value(val) {
             }
 
@@ -631,9 +631,42 @@ namespace storm {
             uint64_t value;
         };
 
-        class BoolCountIsConstantValue : public SmtConstraint {
+        class FalseCountIsEqualConstant : public SmtConstraint {
         public:
-            BoolCountIsConstantValue(std::vector<uint64_t> varIndices, uint64_t val) : varIndices(varIndices),
+            FalseCountIsEqualConstant(std::vector<uint64_t> varIndices, uint64_t val) : varIndices(varIndices),
+                                                                                        value(val) {
+            }
+
+            std::string toSmtlib2(std::vector<std::string> const &varNames) const override {
+                std::stringstream sstr;
+                sstr << "(= (+ ";
+                for (uint64_t i = 0; i < varIndices.size(); ++i) {
+                    sstr << "(ite " << varNames.at(varIndices.at(i)) << " 0 1 )";
+                }
+                sstr << ") " << value << " )";
+                return sstr.str();
+            }
+
+            storm::expressions::Expression toExpression(std::vector<std::string> const &varNames,
+                                                        std::shared_ptr<storm::expressions::ExpressionManager> manager) const override {
+                std::vector<storm::expressions::Expression> boolToInt;
+                for (uint64_t i = 0; i < varIndices.size(); ++i) {
+                    boolToInt.push_back(
+                            ite(manager->getVariableExpression(varNames.at(varIndices.at(i))), // If variable is true
+                                manager->integer(0), // set 0
+                                manager->integer(1))); // else 1
+                }
+                return sum(boolToInt) == manager->integer(value);
+            }
+
+        private:
+            std::vector<uint64_t> varIndices;
+            uint64_t value;
+        };
+
+        class TrueCountIsConstantValue : public SmtConstraint {
+        public:
+            TrueCountIsConstantValue(std::vector<uint64_t> varIndices, uint64_t val) : varIndices(varIndices),
                                                                                        value(val) {
             }