diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp index 437ae326f..0aaeb0a71 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp +++ b/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 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 countConstr = std::make_shared( - markovianIndices, checkNumber); + + std::shared_ptr tleFailedConstr = std::make_shared( + timePointVariables.at(dft.getTopLevelIndex()), checkbound); std::shared_ptr manager = solver->getManager().getSharedPointer(); - solver->add(countConstr->toExpression(varNames, manager)); + solver->add(tleFailedConstr->toExpression(varNames, manager)); + // TODO comment + std::shared_ptr nonMarkovianConstr = std::make_shared( + 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 countConstr = std::make_shared( + std::shared_ptr countConstr = std::make_shared( markovianIndices, timepoint); // Constraint that TLE fails at timepoint std::shared_ptr timepointConstr = std::make_shared( @@ -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 const> element = dft.getElement(i); + if (element->type() == storm::storage::DFTElementType::BE) { + auto be = std::static_pointer_cast 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) { diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.h b/src/storm-dft/modelchecker/dft/DFTASFChecker.h index 36a71dff5..84310b775 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.h +++ b/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 diff --git a/src/storm-dft/modelchecker/dft/SmtConstraint.cpp b/src/storm-dft/modelchecker/dft/SmtConstraint.cpp index 760146f13..78e963d05 100644 --- a/src/storm-dft/modelchecker/dft/SmtConstraint.cpp +++ b/src/storm-dft/modelchecker/dft/SmtConstraint.cpp @@ -598,9 +598,9 @@ namespace storm { std::shared_ptr elseConstraint; }; - class BoolCountIsLessConstant : public SmtConstraint { + class TrueCountIsLessConstant : public SmtConstraint { public: - BoolCountIsLessConstant(std::vector varIndices, uint64_t val) : varIndices(varIndices), + TrueCountIsLessConstant(std::vector 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 varIndices, uint64_t val) : varIndices(varIndices), + FalseCountIsEqualConstant(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)) << " 0 1 )"; + } + 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(0), // set 0 + manager->integer(1))); // else 1 + } + return sum(boolToInt) == manager->integer(value); + } + + private: + std::vector varIndices; + uint64_t value; + }; + + class TrueCountIsConstantValue : public SmtConstraint { + public: + TrueCountIsConstantValue(std::vector varIndices, uint64_t val) : varIndices(varIndices), value(val) { }