diff --git a/src/storm-dft/api/storm-dft.cpp b/src/storm-dft/api/storm-dft.cpp index 961b5fd5d..96c7604a4 100644 --- a/src/storm-dft/api/storm-dft.cpp +++ b/src/storm-dft/api/storm-dft.cpp @@ -51,11 +51,11 @@ namespace storm { std::vector 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; } diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp index 5c26ca08f..a8d31232d 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp +++ b/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 tleNeverFailedConstr = std::make_shared( timePointVariables.at(dft.getTopLevelIndex()), notFailed); - solver->add(tleNeverFailedConstr->toExpression(varNames, - std::make_shared( - solver->getManager()))); + std::shared_ptr 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 tleNeverFailedConstr = std::make_shared( + timePointVariables.at(dft.getTopLevelIndex()), bound); + std::shared_ptr 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; + } } } diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.h b/src/storm-dft/modelchecker/dft/DFTASFChecker.h index bf448b0ba..5f4b97498 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.h +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.h @@ -37,7 +37,44 @@ 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 childVarIndices, std::shared_ptr const> element); @@ -107,7 +143,7 @@ namespace storm { /** * Add constraints encoding claiming rules. * This corresponds to constraint (8) and addition - */ + */ void addClaimingConstraints(); /** @@ -115,16 +151,9 @@ namespace storm { * This corresponds to constraints (9), (10) and (11) */ 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 const& dft; - std::shared_ptr solver = 0; + std::shared_ptr solver = NULL; std::vector varNames; std::unordered_map timePointVariables; std::vector> constraints; diff --git a/src/test/storm-dft/api/DftModelCheckerTest.cpp b/src/test/storm-dft/api/DftModelCheckerTest.cpp index 65e1e05d2..274d5c6e5 100644 --- a/src/test/storm-dft/api/DftModelCheckerTest.cpp +++ b/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(results[0]); } + storm::solver::SmtSolver::CheckResult analyzeSMT(std::string const &file) { + std::shared_ptr> dft = storm::api::loadDFTGalileoFile(file); + EXPECT_TRUE(storm::api::isWellFormed(*dft)); + storm::modelchecker::DFTASFChecker smtChecker(*dft); + smtChecker.convert(); + smtChecker.toSolver(); + std::vector results; + + return smtChecker.checkTleNeverFailedQuery(); + } + double analyzeReliability(std::string const &file, double bound) { std::shared_ptr> dft = storm::api::loadDFTGalileoFile(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); + } }