From 5d5487140fdf260f2aa32cb356d9bbe0d3a42603 Mon Sep 17 00:00:00 2001 From: Alexander Bork Date: Wed, 24 Apr 2019 12:25:04 +0200 Subject: [PATCH] Fixed bound calculation for SMT encoding --- src/storm-dft/api/storm-dft.cpp | 6 +- .../modelchecker/dft/DFTASFChecker.cpp | 83 +++++++++++++++---- .../modelchecker/dft/DFTASFChecker.h | 36 +++++++- .../modelchecker/dft/SmtConstraint.cpp | 25 ++++++ .../storm-dft/api/DftModelCheckerTest.cpp | 2 +- 5 files changed, 127 insertions(+), 25 deletions(-) diff --git a/src/storm-dft/api/storm-dft.cpp b/src/storm-dft/api/storm-dft.cpp index 96c7604a4..5c9db7040 100644 --- a/src/storm-dft/api/storm-dft.cpp +++ b/src/storm-dft/api/storm-dft.cpp @@ -46,12 +46,12 @@ namespace storm { std::vector analyzeDFTSMT(storm::storage::DFT const &dft, bool printOutput) { storm::modelchecker::DFTASFChecker smtChecker(dft); - smtChecker.convert(); smtChecker.toSolver(); std::vector results; - results.push_back(smtChecker.checkTleNeverFailedQuery()); + results.push_back(smtChecker.checkTleNeverFailed()); uint64_t lower_bound = smtChecker.getLeastFailureBound(); + uint64_t upper_bound = smtChecker.getAlwaysFailedBound(); if (printOutput) { //TODO add suitable output function, maybe add query descriptions for better readability for (size_t i = 0; i < results.size(); ++i) { @@ -61,9 +61,9 @@ namespace storm { } else if (results.at(i) == storm::solver::SmtSolver::CheckResult::Unsat) { tmp = "UNSAT"; } - std::cout << "Query " << std::to_string(i) << " : " << tmp << std::endl; } std::cout << "Lower bound: " << std::to_string(lower_bound) << std::endl; + std::cout << "Upper bound: " << std::to_string(upper_bound) << std::endl; } return results; } diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp index a8d31232d..7b61ea655 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp @@ -242,6 +242,13 @@ namespace storm { for (uint64_t currChild = 0; currChild < children.size() - 1; ++currChild) { uint64_t timeCurrChild = childVarIndices.at(currChild); // Moment when current child fails + // If trying to claim (i+1)-th child, either child claimed before or never claimed by other spare + // (additional constraint) + std::shared_ptr claimEarlyC = generateClaimEarlyConstraint(spare, currChild); + constraints.push_back(std::make_shared( + std::make_shared(getClaimVariableIndex(spare->id(), children.at(currChild)->id()), + timeCurrChild), claimEarlyC)); + constraints.back()->setDescription("Ensure earliest possible claiming"); // If i-th child fails after being claimed, then try to claim next child (constraint 6) std::shared_ptr tryClaimC = generateTryToClaimConstraint(spare, currChild + 1, timeCurrChild); @@ -252,6 +259,28 @@ namespace storm { } } + std::shared_ptr + DFTASFChecker::generateClaimEarlyConstraint(std::shared_ptr const> spare, + uint64_t childIndex) const { + auto child = spare->children().at(childIndex + 1); + std::vector> constraintAggregator; + for (auto const &otherSpare : child->parents()) { + if (otherSpare->id() == spare->id()) { + // not a different spare. + continue; + } + std::vector> OrAggregator; + // Other spare has claimed before + OrAggregator.push_back(std::make_shared( + getClaimVariableIndex(otherSpare->id(), child->id()), timePointVariables.at(childIndex))); + // Other spare will never claim + OrAggregator.push_back(std::make_shared( + getClaimVariableIndex(otherSpare->id(), child->id()), notFailed)); + constraintAggregator.push_back(std::make_shared(OrAggregator)); + } + return std::make_shared(constraintAggregator); + } + std::shared_ptr DFTASFChecker::generateTryToClaimConstraint(std::shared_ptr const> spare, uint64_t childIndex, uint64_t timepoint) const { @@ -458,14 +487,14 @@ namespace storm { } - storm::solver::SmtSolver::CheckResult DFTASFChecker::checkTleNeverFailedQuery() { - // STORM_LOG_ERROR_COND(!solver, "SMT Solver was not initialized, call toSolver() before checking queries"); + storm::solver::SmtSolver::CheckResult DFTASFChecker::checkTleFailsWithEq(uint64_t bound) { + STORM_LOG_ASSERT(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) + // Constraint that toplevel element can fail with less or equal 'bound' failures std::shared_ptr tleNeverFailedConstr = std::make_shared( - timePointVariables.at(dft.getTopLevelIndex()), notFailed); + 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(); @@ -474,7 +503,7 @@ namespace storm { } storm::solver::SmtSolver::CheckResult DFTASFChecker::checkTleFailsWithLeq(uint64_t bound) { - //STORM_LOG_ERROR_COND(!solver, "SMT Solver was not initialized, call toSolver() before checking queries"); + STORM_LOG_ASSERT(solver, "SMT Solver was not initialized, call toSolver() before checking queries"); // Set backtracking marker to check several properties without reconstructing DFT encoding solver->push(); @@ -489,24 +518,25 @@ namespace storm { } void DFTASFChecker::setSolverTimeout(uint_fast64_t milliseconds) { - if (!solver) { - STORM_LOG_WARN("SMT Solver was not initialized, timeout setting ignored"); - } else { - solver->setTimeout(milliseconds); - } + STORM_LOG_ASSERT(solver, "SMT Solver was not initialized, timeout cannot be set"); + solver->setTimeout(milliseconds); } void DFTASFChecker::unsetSolverTimeout() { - if (!solver) { - STORM_LOG_WARN("SMT Solver was not initialized, timeout unsetting ignored"); - } else { - solver->unsetTimeout(); - } + STORM_LOG_ASSERT(solver, "SMT Solver was not initialized, timeout cannot be unset"); + solver->unsetTimeout(); } - uint64_t DFTASFChecker::getLeastFailureBound() { - //STORM_LOG_ERROR_COND(!solver, "SMT Solver was not initialized, call toSolver() before checking queries"); + storm::solver::SmtSolver::CheckResult DFTASFChecker::checkTleNeverFailed() { + STORM_LOG_ASSERT(solver, "SMT Solver was not initialized, call toSolver() before checking queries"); + return checkTleFailsWithEq(notFailed); + } + uint64_t DFTASFChecker::getLeastFailureBound() { + STORM_LOG_ASSERT(solver, "SMT Solver was not initialized, call toSolver() before checking queries"); + if (checkTleNeverFailed() == storm::solver::SmtSolver::CheckResult::Sat) { + return notFailed; + } uint64_t bound = 0; while (bound < notFailed) { setSolverTimeout(10000); @@ -520,5 +550,24 @@ namespace storm { } return bound; } + + uint64_t DFTASFChecker::getAlwaysFailedBound() { + STORM_LOG_ASSERT(solver, "SMT Solver was not initialized, call toSolver() before checking queries"); + if (checkTleNeverFailed() == storm::solver::SmtSolver::CheckResult::Sat) { + return notFailed; + } + uint64_t bound = notFailed - 1; + while (bound >= 0) { + setSolverTimeout(10000); + storm::solver::SmtSolver::CheckResult tmp_res = checkTleFailsWithEq(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 5f4b97498..2141694f5 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.h +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.h @@ -47,23 +47,38 @@ namespace storm { * * @return "Sat" if TLE never fails, "Unsat" if it does, otherwise "Unknown" */ - storm::solver::SmtSolver::CheckResult checkTleNeverFailedQuery(); + storm::solver::SmtSolver::CheckResult checkTleNeverFailed(); /** - * Check if there exists a sequence of BE failures of given length such that the TLE of the DFT fails + * Check if there exists a sequence of BE failures of exactly 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 checkTleFailsWithEq(uint64_t bound); + + /** + * Check if there exists a sequence of BE failures of at least given length such that the TLE of the DFT fails + * + * @param bound the length of the sequence + * @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 + * Get the minimal number of BEs necessary for the TLE to fail (lower bound for number of failures to check) * * @return the minimal number */ uint64_t getLeastFailureBound(); + /** + * Get the number of BE failures for which the TLE always fails (upper bound for number of failures to check) + * + * @return the number + */ + uint64_t getAlwaysFailedBound(); + /** * Set the timeout of the solver * @@ -79,6 +94,19 @@ namespace storm { private: uint64_t getClaimVariableIndex(uint64_t spareIndex, uint64_t childIndex) const; + /** + * Generate constraint for spares such that when trying to claim child (i+1), other spares either claimed it + * before or will never claim it + * + * @param spare Spare. + * @param childIndex Index of child to consider in spare children + * @param timepoint Timepoint to try to claim + * @return + */ + std::shared_ptr + generateClaimEarlyConstraint(std::shared_ptr const> spare, + uint64_t childIndex) const; + /** * Generate constraint for 'spare (s) tries to claim the child (i) at the given timepoint (t)'. * This corresponds to the function \phi^s_i(t) in constraint 7. @@ -153,7 +181,7 @@ namespace storm { void addMarkovianConstraints(); storm::storage::DFT const& dft; - std::shared_ptr solver = NULL; + std::shared_ptr solver = nullptr; std::vector varNames; std::unordered_map timePointVariables; std::vector> constraints; diff --git a/src/storm-dft/modelchecker/dft/SmtConstraint.cpp b/src/storm-dft/modelchecker/dft/SmtConstraint.cpp index 34450d98f..e9bc2b220 100644 --- a/src/storm-dft/modelchecker/dft/SmtConstraint.cpp +++ b/src/storm-dft/modelchecker/dft/SmtConstraint.cpp @@ -395,6 +395,31 @@ namespace storm { uint64_t value; }; + class IsGreaterEqualConstant : public SmtConstraint { + public: + IsGreaterEqualConstant(uint64_t varIndex, uint64_t val) : varIndex(varIndex), value(val) { + } + + virtual ~IsGreaterEqualConstant() { + } + + std::string toSmtlib2(std::vector const &varNames) const override { + std::stringstream sstr; + assert(varIndex < varNames.size()); + sstr << "(<= " << value << " " << varNames.at(varIndex) << ")"; + return sstr.str(); + } + + storm::expressions::Expression toExpression(std::vector const &varNames, + std::shared_ptr manager) const override { + return manager->getVariableExpression(varNames.at(varIndex)) >= value; + } + + private: + uint64_t varIndex; + uint64_t value; + }; + class IsEqual : public SmtConstraint { public: diff --git a/src/test/storm-dft/api/DftModelCheckerTest.cpp b/src/test/storm-dft/api/DftModelCheckerTest.cpp index 274d5c6e5..454c94f36 100644 --- a/src/test/storm-dft/api/DftModelCheckerTest.cpp +++ b/src/test/storm-dft/api/DftModelCheckerTest.cpp @@ -80,7 +80,7 @@ namespace { smtChecker.toSolver(); std::vector results; - return smtChecker.checkTleNeverFailedQuery(); + return smtChecker.checkTleNeverFailed(); } double analyzeReliability(std::string const &file, double bound) {