From 0baccee440e7c5e018eb6cccdadd294b008d161d Mon Sep 17 00:00:00 2001 From: Alexander Bork Date: Thu, 2 May 2019 16:20:53 +0200 Subject: [PATCH] Added correction of constraint for non-Markovian states and better lower bound computation --- .../modelchecker/dft/DFTASFChecker.cpp | 58 ++++++++++++++++--- .../modelchecker/dft/DFTASFChecker.h | 13 ++++- .../modelchecker/dft/SmtConstraint.cpp | 33 +++++++++++ 3 files changed, 95 insertions(+), 9 deletions(-) diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp index 051b2a555..19ae50a42 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp @@ -325,6 +325,7 @@ namespace storm { void DFTASFChecker::addMarkovianConstraints() { uint64_t nrMarkovian = dft.nrBasicElements(); + std::set depElements; // Vector containing (non-)Markovian constraints for each timepoint std::vector>> markovianC(nrMarkovian); std::vector>> nonMarkovianC(nrMarkovian); @@ -352,13 +353,14 @@ namespace storm { constraints.back()->setDescription("Markovian (" + std::to_string(i) + ") iff all dependent events which trigger failed also failed."); } - // In non-Markovian steps the next failed element is a dependent BE (constraint 10) + // In non-Markovian steps the next failed element is a dependent BE (constraint 10) + additions to specification in paper for (size_t j = 0; j < dft.nrElements(); ++j) { std::shared_ptr const> element = dft.getElement(j); if (element->isBasicElement()) { auto be = std::static_pointer_cast const>(element); if (be->hasIngoingDependencies()) { + depElements.emplace(j); for (uint64_t i = 0; i < nrMarkovian -1; ++i) { std::shared_ptr nextFailure = std::make_shared( timePointVariables.at(j), i + 1); @@ -372,6 +374,14 @@ namespace storm { } } for (uint64_t i = 0; i < nrMarkovian; ++i) { + std::vector> dependentConstr; + for (auto dependentEvent: depElements) { + std::shared_ptr nextFailure = std::make_shared( + timePointVariables.at(dependentEvent), i + 1); + dependentConstr.push_back(nextFailure); + } + // Add Constraint that any DEPENDENT event has to fail next + nonMarkovianC[i].push_back(std::make_shared(dependentConstr)); constraints.push_back(std::make_shared(std::make_shared(markovianVariables.at(i), false), std::make_shared(nonMarkovianC[i]))); constraints.back()->setDescription("Non-Markovian (" + std::to_string(i) + ") -> next failure is dependent BE."); } @@ -504,13 +514,47 @@ namespace storm { return checkTleFailsWithEq(notFailed); } - uint64_t DFTASFChecker::correctLowerBound(uint64_t bound) { + storm::solver::SmtSolver::CheckResult + DFTASFChecker::checkFailsWithLessThanMarkovianState(uint64_t checkNumber) { + STORM_LOG_ASSERT(solver, "SMT Solver was not initialized, call toSolver() before checking queries"); + uint64_t nrMarkovian = dft.nrBasicElements(); + std::vector markovianIndices; + // Get Markovian variable indices + for (uint64_t i = 0; i < nrMarkovian; ++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 or equal 'bound' failures + std::shared_ptr countConstr = std::make_shared( + markovianIndices, checkNumber); + std::shared_ptr manager = solver->getManager().getSharedPointer(); + solver->add(countConstr->toExpression(varNames, manager)); + storm::solver::SmtSolver::CheckResult res = solver->check(); + solver->pop(); + return res; + } + + 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)); - // 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 + while (bound >= 0) { + setSolverTimeout(timeout * 1000); + storm::solver::SmtSolver::CheckResult tmp_res = checkFailsWithLessThanMarkovianState(bound); + 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::Unknown: + STORM_LOG_DEBUG("Lower bound correction - Solver returned 'Unknown', corrected to "); + return bound; + default: + --bound; + break; + } + } + return bound; } uint64_t DFTASFChecker::getLeastFailureBound(uint_fast64_t timeout) { @@ -524,7 +568,7 @@ namespace storm { switch (tmp_res) { case storm::solver::SmtSolver::CheckResult::Sat: if (dft.getDependencies().size() > 0) { - return correctLowerBound(bound); + return correctLowerBound(bound, timeout); } else { return bound; } diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.h b/src/storm-dft/modelchecker/dft/DFTASFChecker.h index 4ebe91f0b..5c102fb6e 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.h +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.h @@ -95,14 +95,23 @@ namespace storm { void unsetSolverTimeout(); private: + /** + * Helper function that checks if the DFT can fail while visiting less than a given number of 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, + * "Unsat" if it does not, otherwise "Unknown" + */ + storm::solver::SmtSolver::CheckResult checkFailsWithLessThanMarkovianState(uint64_t checkNumber); + /** * 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 + * @param timeout timeout timeout for each query in seconds * @return the corrected bound, 1 if correction cannot be completed */ - uint64_t correctLowerBound(uint64_t bound); + uint64_t correctLowerBound(uint64_t bound, uint_fast64_t timeout); uint64_t getClaimVariableIndex(uint64_t spareIndex, uint64_t childIndex) const; diff --git a/src/storm-dft/modelchecker/dft/SmtConstraint.cpp b/src/storm-dft/modelchecker/dft/SmtConstraint.cpp index 83433989b..0a56fe8f6 100644 --- a/src/storm-dft/modelchecker/dft/SmtConstraint.cpp +++ b/src/storm-dft/modelchecker/dft/SmtConstraint.cpp @@ -597,6 +597,39 @@ namespace storm { std::shared_ptr thenConstraint; std::shared_ptr elseConstraint; }; + + class BoolCountIsLessConstant : public SmtConstraint { + public: + BoolCountIsLessConstant(std::vector varIndices, uint64_t val) : varIndices(varIndices), + value(val) { + } + + std::string toSmtlib2(std::vector const &varNames) const override { + std::stringstream sstr; + sstr << "(< (+ "; + for (uint64_t i = 0; i < varIndices.size(); ++i) { + sstr << "(ite " << varNames.at(varIndices.at(i)) << " 1 0 )"; + } + sstr << ") " << value << " )"; + return sstr.str(); + } + + storm::expressions::Expression toExpression(std::vector const &varNames, + std::shared_ptr manager) const override { + std::vector 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(1), // set 1 + manager->integer(0))); // else 0 + } + return sum(boolToInt) < manager->integer(value); + } + + private: + std::vector varIndices; + uint64_t value; + }; } }