Added SMT function to calculate lower bound for number of DFT failures needed for failure of TLE

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

@@ -51,11 +51,11 @@ namespace storm {
             std::vector<storm::solver::SmtSolver::CheckResult> results;
 
             results.push_back(smtChecker.checkTleNeverFailedQuery());
-
+            uint64_t lower_bound = smtChecker.getLeastFailureBound();
             if (printOutput) {
-                // TODO add suitable output function, maybe add query descriptions for better readability
+                //TODO add suitable output function, maybe add query descriptions for better readability
                 for (size_t i = 0; i < results.size(); ++i) {
-                    std::string tmp = "unknonwn";
+                    std::string tmp = "unknown";
                     if (results.at(i) == storm::solver::SmtSolver::CheckResult::Sat) {
                         tmp = "SAT";
                     } else if (results.at(i) == storm::solver::SmtSolver::CheckResult::Unsat) {
@@ -63,6 +63,7 @@ namespace storm {
                     }
                     std::cout << "Query " << std::to_string(i) << " : " << tmp << std::endl;
                 }
+                std::cout << "Lower bound: " << std::to_string(lower_bound) << std::endl;
             }
             return results;
         }

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

@@ -459,19 +459,66 @@ namespace storm {
         }
 
         storm::solver::SmtSolver::CheckResult DFTASFChecker::checkTleNeverFailedQuery() {
-            STORM_LOG_ERROR_COND(!solver, "SMT Solver was not initialized, call toSolver() before checking queries");
+            // STORM_LOG_ERROR_COND(!solver, "SMT Solver was not initialized, call toSolver() before checking queries");
 
             // Set backtracking marker to check several properties without reconstructing DFT encoding
             solver->push();
             // Constraint that toplevel element will not fail (part of constraint 13)
             std::shared_ptr<SmtConstraint> tleNeverFailedConstr = std::make_shared<IsConstantValue>(
                     timePointVariables.at(dft.getTopLevelIndex()), notFailed);
-            solver->add(tleNeverFailedConstr->toExpression(varNames,
-                                                           std::make_shared<storm::expressions::ExpressionManager>(
-                                                                   solver->getManager())));
+            std::shared_ptr<storm::expressions::ExpressionManager> manager = solver->getManager().getSharedPointer();
+            solver->add(tleNeverFailedConstr->toExpression(varNames, manager));
             storm::solver::SmtSolver::CheckResult res = solver->check();
             solver->pop();
             return res;
         }
+
+        storm::solver::SmtSolver::CheckResult DFTASFChecker::checkTleFailsWithLeq(uint64_t bound) {
+            //STORM_LOG_ERROR_COND(!solver, "SMT Solver was not initialized, call toSolver() before checking queries");
+
+            // Set backtracking marker to check several properties without reconstructing DFT encoding
+            solver->push();
+            // Constraint that toplevel element can fail with less or equal 'bound' failures
+            std::shared_ptr<SmtConstraint> tleNeverFailedConstr = std::make_shared<IsLessEqualConstant>(
+                    timePointVariables.at(dft.getTopLevelIndex()), bound);
+            std::shared_ptr<storm::expressions::ExpressionManager> manager = solver->getManager().getSharedPointer();
+            solver->add(tleNeverFailedConstr->toExpression(varNames, manager));
+            storm::solver::SmtSolver::CheckResult res = solver->check();
+            solver->pop();
+            return res;
+        }
+
+        void DFTASFChecker::setSolverTimeout(uint_fast64_t milliseconds) {
+            if (!solver) {
+                STORM_LOG_WARN("SMT Solver was not initialized, timeout setting ignored");
+            } else {
+                solver->setTimeout(milliseconds);
+            }
+        }
+
+        void DFTASFChecker::unsetSolverTimeout() {
+            if (!solver) {
+                STORM_LOG_WARN("SMT Solver was not initialized, timeout unsetting ignored");
+            } else {
+                solver->unsetTimeout();
+            }
+        }
+
+        uint64_t DFTASFChecker::getLeastFailureBound() {
+            //STORM_LOG_ERROR_COND(!solver, "SMT Solver was not initialized, call toSolver() before checking queries");
+
+            uint64_t bound = 0;
+            while (bound < notFailed) {
+                setSolverTimeout(10000);
+                storm::solver::SmtSolver::CheckResult tmp_res = checkTleFailsWithLeq(bound);
+                unsetSolverTimeout();
+                if (tmp_res == storm::solver::SmtSolver::CheckResult::Sat ||
+                    tmp_res == storm::solver::SmtSolver::CheckResult::Unknown) {
+                    return bound;
+                }
+                ++bound;
+            }
+            return bound;
+        }
     }
 }

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

@@ -37,8 +37,45 @@ namespace storm {
             void convert();
             void toFile(std::string const&);
 
+            /**
+             * Generates a new solver instance and prepares it for SMT checking of the DFT. Needs to be called before all queries to the solver
+             */
             void toSolver();
 
+            /**
+             * Check if the TLE of the DFT never fails
+             *
+             * @return  "Sat" if TLE never fails, "Unsat" if it does, otherwise "Unknown"
+             */
+            storm::solver::SmtSolver::CheckResult checkTleNeverFailedQuery();
+
+            /**
+             * Check if there exists a sequence of BE failures of given length such that the TLE of the DFT fails
+             *
+             * @param bound the length of the sequene
+             * @return "Sat" if such a sequence exists, "Unsat" if it does not, otherwise "Unknown"
+             */
+            storm::solver::SmtSolver::CheckResult checkTleFailsWithLeq(uint64_t bound);
+
+            /**
+             * Get the minimal number of BEs necessary for the TLE to fail
+             *
+             * @return the minimal number
+             */
+            uint64_t getLeastFailureBound();
+
+            /**
+             * Set the timeout of the solver
+             *
+             * @param milliseconds the timeout in milliseconds
+             */
+            void setSolverTimeout(uint_fast64_t milliseconds);
+
+            /**
+             * Unset the timeout for the solver
+             */
+            void unsetSolverTimeout();
+            
         private:
             uint64_t getClaimVariableIndex(uint64_t spareIndex, uint64_t childIndex) const;
 
@@ -72,7 +109,6 @@ namespace storm {
 
             /**
              * Add constraints encoding VOT gates.
-
              */
             void generateVotConstraint(size_t i, std::vector<uint64_t> childVarIndices,
                                        std::shared_ptr<storm::storage::DFTElement<ValueType> const> element);
@@ -107,7 +143,7 @@ namespace storm {
             /**
             * Add constraints encoding claiming rules.
             * This corresponds to constraint (8) and addition
-               */
+            */
             void addClaimingConstraints();
 
             /**
@@ -116,15 +152,8 @@ namespace storm {
              */
             void addMarkovianConstraints();
             
-            /**
-             * Check if the TLE of the DFT never fails
-             *
-             * @return  "Sat" if TLE never fails, "Unsat" if it does, otherwise "Unknown"
-             */
-            storm::solver::SmtSolver::CheckResult checkTleNeverFailedQuery();
-            
             storm::storage::DFT<ValueType> const& dft;
-            std::shared_ptr<storm::solver::SmtSolver> solver = 0;
+            std::shared_ptr<storm::solver::SmtSolver> solver = NULL;
             std::vector<std::string> varNames;
             std::unordered_map<uint64_t, uint64_t> timePointVariables;
             std::vector<std::shared_ptr<SmtConstraint>> constraints;

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

@@ -2,6 +2,7 @@
 #include "storm-config.h"
 
 #include "storm-dft/api/storm-dft.h"
+#include "storm-dft/modelchecker/dft/DFTASFChecker.h"
 #include "storm-parsers/api/storm-parsers.h"
 
 namespace {
@@ -71,6 +72,17 @@ namespace {
             return boost::get<double>(results[0]);
         }
 
+        storm::solver::SmtSolver::CheckResult analyzeSMT(std::string const &file) {
+            std::shared_ptr<storm::storage::DFT<double>> dft = storm::api::loadDFTGalileoFile<double>(file);
+            EXPECT_TRUE(storm::api::isWellFormed(*dft));
+            storm::modelchecker::DFTASFChecker smtChecker(*dft);
+            smtChecker.convert();
+            smtChecker.toSolver();
+            std::vector<storm::solver::SmtSolver::CheckResult> results;
+
+            return smtChecker.checkTleNeverFailedQuery();
+        }
+
         double analyzeReliability(std::string const &file, double bound) {
             std::shared_ptr<storm::storage::DFT<double>> dft = storm::api::loadDFTGalileoFile<double>(file);
             EXPECT_TRUE(storm::api::isWellFormed(*dft));
@@ -199,4 +211,11 @@ namespace {
         double result = this->analyzeReliability(STORM_TEST_RESOURCES_DIR "/dft/hecs_2_2.dft", 1.0);
         EXPECT_FLOAT_EQ(result, 0.00021997582);
     }
+
+    TYPED_TEST(DftModelCheckerTest, SmtTest) {
+        storm::solver::SmtSolver::CheckResult result = this->analyzeSMT(STORM_TEST_RESOURCES_DIR "/dft/and.dft");
+        EXPECT_EQ(result, storm::solver::SmtSolver::CheckResult::Unsat);
+        result = this->analyzeSMT(STORM_TEST_RESOURCES_DIR "/dft/pand.dft");
+        EXPECT_EQ(result, storm::solver::SmtSolver::CheckResult::Sat);
+    }
 }