From 75d28060cc0c831ebfc02178f909b25c75d51241 Mon Sep 17 00:00:00 2001 From: Alexander Bork Date: Wed, 10 Jul 2019 16:34:18 +0200 Subject: [PATCH] Moved failure bound computation to decouple it from the SMT checker --- src/storm-dft/api/storm-dft.cpp | 13 +- src/storm-dft/api/storm-dft.h | 4 +- .../modelchecker/dft/DFTASFChecker.cpp | 185 -------------- .../modelchecker/dft/DFTASFChecker.h | 50 +--- src/storm-dft/utility/FailureBoundFinder.cpp | 241 ++++++++++++++++++ src/storm-dft/utility/FailureBoundFinder.h | 73 ++++++ src/test/storm-dft/api/DftSmtTest.cpp | 11 +- 7 files changed, 340 insertions(+), 237 deletions(-) create mode 100644 src/storm-dft/utility/FailureBoundFinder.cpp create mode 100644 src/storm-dft/utility/FailureBoundFinder.h diff --git a/src/storm-dft/api/storm-dft.cpp b/src/storm-dft/api/storm-dft.cpp index d74120402..8d2c3ce2a 100644 --- a/src/storm-dft/api/storm-dft.cpp +++ b/src/storm-dft/api/storm-dft.cpp @@ -4,7 +4,6 @@ #include "storm-dft/settings/modules/DftGspnSettings.h" #include "storm-conv/settings/modules/JaniExportSettings.h" #include "storm-conv/api/storm-conv.h" -#include "storm-dft/utility/FDEPConflictFinder.h" namespace storm { namespace api { @@ -48,7 +47,7 @@ namespace storm { } template<> - storm::api::SMTResult + storm::api::PreprocessingResult analyzeDFTSMT(storm::storage::DFT const &dft, bool printOutput, bool experimentalMode) { uint64_t solverTimeout = 10; @@ -57,10 +56,12 @@ namespace storm { smtChecker.activateExperimentalMode(); } smtChecker.toSolver(); - storm::api::SMTResult results; + storm::api::PreprocessingResult results; - results.lowerBEBound = smtChecker.getLeastFailureBound(solverTimeout); - results.upperBEBound = smtChecker.getAlwaysFailedBound(solverTimeout); + results.lowerBEBound = storm::dft::utility::FailureBoundFinder::getLeastFailureBound(dft, true, + solverTimeout); + results.upperBEBound = storm::dft::utility::FailureBoundFinder::getAlwaysFailedBound(dft, true, + solverTimeout); if (printOutput) { STORM_PRINT("BE FAILURE BOUNDS" << std::endl << "========================================" << std::endl << @@ -85,7 +86,7 @@ namespace storm { } template<> - storm::api::SMTResult + storm::api::PreprocessingResult analyzeDFTSMT(storm::storage::DFT const &dft, bool printOutput, bool experimentalMode) { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, diff --git a/src/storm-dft/api/storm-dft.h b/src/storm-dft/api/storm-dft.h index 17bc94a15..70d21f854 100644 --- a/src/storm-dft/api/storm-dft.h +++ b/src/storm-dft/api/storm-dft.h @@ -8,6 +8,8 @@ #include "storm-dft/modelchecker/dft/DFTModelChecker.h" #include "storm-dft/modelchecker/dft/DFTASFChecker.h" #include "storm-dft/transformations/DftToGspnTransformator.h" +#include "storm-dft/utility/FDEPConflictFinder.h" +#include "storm-dft/utility/FailureBoundFinder.h" #include "storm-gspn/api/storm-gspn.h" @@ -106,7 +108,7 @@ namespace storm { * @return Result result vector */ template - storm::api::SMTResult + storm::api::PreprocessingResult analyzeDFTSMT(storm::storage::DFT const &dft, bool printOutput, bool experimentalMode); /*! diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp index 6fc9ef1ae..ff9e4f53c 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp @@ -754,190 +754,5 @@ namespace storm { 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"); - if (experimentalMode) - STORM_LOG_WARN("DFT-SMT-Checker now runs in experimental mode, bound correction is prone to errors!"); - STORM_LOG_DEBUG("Lower bound correction - try to correct bound " << std::to_string(bound)); - 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_EXP || - element->type() == storm::storage::DFTElementType::BE_CONST) { - 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) { - if (nrNonMarkovian == 0 and boundCandidate == 0) { - nrNonMarkovian = 1; - } - STORM_LOG_TRACE( - "Lower bound correction - check possible bound " << std::to_string(boundCandidate) << " with " - << std::to_string(nrNonMarkovian) - << " non-Markovian states"); - // The uniqueness transformation for constantly failed BEs guarantees that a DFT never fails - // in step 0 without intermediate non-Markovians, thus forcibly set nrNonMarkovian - setSolverTimeout(timeout * 1000); - storm::solver::SmtSolver::CheckResult tmp_res = - checkFailsLeqWithEqNonMarkovianState(boundCandidate + nrNonMarkovian, nrNonMarkovian); - unsetSolverTimeout(); - switch (tmp_res) { - 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"); - // Prevent integer underflow - if (boundCandidate == 0) { - STORM_LOG_DEBUG("Lower bound correction - corrected bound to 0"); - return 0; - } - --boundCandidate; - break; - case storm::solver::SmtSolver::CheckResult::Unknown: - // 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: - // if query is UNSAT, increase number of non-Markovian states and try again - STORM_LOG_TRACE("Lower bound correction - UNSAT"); - ++nrNonMarkovian; - break; - } - } - // 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) { - STORM_LOG_ASSERT(solver, "SMT Solver was not initialized, call toSolver() before checking queries"); - if (experimentalMode) - STORM_LOG_WARN("DFT-SMT-Checker now runs in experimental mode, bound correction is prone to errors!"); - STORM_LOG_DEBUG("Upper bound correction - try to correct bound " << std::to_string(bound)); - uint64_t boundCandidate = bound; - uint64_t nrDepEvents = 0; - uint64_t nrNonMarkovian = 0; - uint64_t currentTimepoint = 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_EXP || - element->type() == storm::storage::DFTElementType::BE_CONST) { - auto be = std::static_pointer_cast const>(element); - if (be->hasIngoingDependencies()) { - ++nrDepEvents; - } - } - } - while (boundCandidate >= 0) { - currentTimepoint = bound + 1; - while (currentTimepoint - boundCandidate > 0) { - --currentTimepoint; - nrNonMarkovian = currentTimepoint - boundCandidate; - STORM_LOG_TRACE( - "Upper bound correction - candidate " << std::to_string(boundCandidate) << " check split " - << - std::to_string(currentTimepoint) << "|" - << std::to_string(nrNonMarkovian)); - setSolverTimeout(timeout * 1000); - storm::solver::SmtSolver::CheckResult tmp_res = - checkFailsAtTimepointWithEqNonMarkovianState(currentTimepoint, nrNonMarkovian); - unsetSolverTimeout(); - switch (tmp_res) { - case storm::solver::SmtSolver::CheckResult::Sat: - STORM_LOG_TRACE("Upper bound correction - SAT"); - STORM_LOG_DEBUG("Upper bound correction - corrected to bound " << boundCandidate << - " (TLE can fail at sequence point " - << std::to_string( - currentTimepoint) - << " with " - << std::to_string( - nrNonMarkovian) - << " non-Markovian states)"); - return boundCandidate; - case storm::solver::SmtSolver::CheckResult::Unknown: - // If any query returns unknown, we cannot be sure about the bound and fall back to the naive one - STORM_LOG_DEBUG( - "Upper bound correction - Solver returned 'Unknown', corrected to bound " << bound); - return bound; - default: - // if query is UNSAT, increase number of non-Markovian states and try again - STORM_LOG_TRACE("Lower bound correction - UNSAT"); - break; - } - } - --boundCandidate; - } - - // if for one candidate all queries are UNSAT, it is not valid. Return last valid candidate - STORM_LOG_DEBUG("Upper bound correction - corrected bound to " << std::to_string(boundCandidate)); - return boundCandidate; - } - - uint64_t DFTASFChecker::getLeastFailureBound(uint_fast64_t timeout) { - STORM_LOG_TRACE("Compute lower bound for number of BE failures necessary for the DFT to fail"); - STORM_LOG_ASSERT(solver, "SMT Solver was not initialized, call toSolver() before checking queries"); - uint64_t bound = 0; - while (bound < notFailed) { - setSolverTimeout(timeout * 1000); - storm::solver::SmtSolver::CheckResult tmp_res = checkTleFailsWithLeq(bound); - unsetSolverTimeout(); - switch (tmp_res) { - case storm::solver::SmtSolver::CheckResult::Sat: - if (!dft.getDependencies().empty()) { - return correctLowerBound(bound, timeout); - } else { - return bound; - } - case storm::solver::SmtSolver::CheckResult::Unknown: - STORM_LOG_DEBUG("Lower bound: Solver returned 'Unknown'"); - return bound; - default: - ++bound; - break; - } - - } - - return bound; - } - - uint64_t DFTASFChecker::getAlwaysFailedBound(uint_fast64_t timeout) { - STORM_LOG_TRACE("Compute bound for number of BE failures such that the DFT always fails"); - 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(timeout * 1000); - storm::solver::SmtSolver::CheckResult tmp_res = checkTleFailsWithEq(bound); - unsetSolverTimeout(); - switch (tmp_res) { - case storm::solver::SmtSolver::CheckResult::Sat: - if (!dft.getDependencies().empty()) { - return correctUpperBound(bound, timeout); - } else { - return bound; - } - case storm::solver::SmtSolver::CheckResult::Unknown: - STORM_LOG_DEBUG("Upper bound: Solver returned 'Unknown'"); - return bound; - default: - --bound; - break; - } - } - return bound; - } - } } diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.h b/src/storm-dft/modelchecker/dft/DFTASFChecker.h index 3cff2a6a5..61da80af9 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.h +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.h @@ -99,23 +99,6 @@ namespace storm { storm::solver::SmtSolver::CheckResult checkDependencyConflict(uint64_t dep1Index, uint64_t dep2Index, uint64_t timeout = 10); - /** - * Get the minimal number of BEs necessary for the TLE to fail (lower bound for number of failures to check) - * - * @param timeout timeout for each query in seconds, defaults to 10 seconds - * @return the minimal number - */ - uint64_t getLeastFailureBound(uint_fast64_t timeout = 10); - - /** - * Get the number of BE failures for which the TLE always fails (upper bound for number of failures to check). - * Note that the returned value may be higher than the real one when dependencies are present. - * - * @param timeout timeout for each query in seconds, defaults to 10 seconds - * @return the number - */ - uint64_t getAlwaysFailedBound(uint_fast64_t timeout = 10); - /** * Set the timeout of the solver @@ -128,8 +111,14 @@ namespace storm { * Unset the timeout for the solver */ void unsetSolverTimeout(); - - private: + + /** + * Get a reference to the DFT + */ + storm::storage::DFT const &getDFT() { + return dft; + } + /** * Helper function to check if the TLE fails before or at a given timepoint while visiting exactly * a given number of non-Markovian states @@ -151,27 +140,8 @@ namespace storm { */ storm::solver::SmtSolver::CheckResult checkFailsAtTimepointWithEqNonMarkovianState(uint64_t timepoint, uint64_t nrNonMarkovian); - - /** - * 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 - * @return the corrected bound - */ - uint64_t correctLowerBound(uint64_t bound, uint_fast64_t timeout); - - /** - * Helper function for correction of bound for number of BEs such that the DFT always fails when dependencies are present - * - * @param bound known bound to be corrected - * @param timeout timeout timeout for each query in seconds - * @return the corrected bound - */ - uint64_t correctUpperBound(uint64_t bound, uint_fast64_t timeout); + + private: uint64_t getClaimVariableIndex(uint64_t spareIndex, uint64_t childIndex) const; diff --git a/src/storm-dft/utility/FailureBoundFinder.cpp b/src/storm-dft/utility/FailureBoundFinder.cpp new file mode 100644 index 000000000..59243ad54 --- /dev/null +++ b/src/storm-dft/utility/FailureBoundFinder.cpp @@ -0,0 +1,241 @@ +#include "FailureBoundFinder.h" + +namespace storm { + namespace dft { + namespace utility { + uint64_t + FailureBoundFinder::correctLowerBound(std::shared_ptr smtchecker, + uint64_t bound, uint_fast64_t timeout) { + STORM_LOG_DEBUG("Lower bound correction - try to correct bound " << std::to_string(bound)); + uint64_t boundCandidate = bound; + uint64_t nrDepEvents = 0; + uint64_t nrNonMarkovian = 0; + auto dft = smtchecker->getDFT(); + + // 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_EXP || + element->type() == storm::storage::DFTElementType::BE_CONST) { + 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) { + if (nrNonMarkovian == 0 and boundCandidate == 0) { + nrNonMarkovian = 1; + } + STORM_LOG_TRACE( + "Lower bound correction - check possible bound " << std::to_string(boundCandidate) + << " with " + << std::to_string(nrNonMarkovian) + << " non-Markovian states"); + // The uniqueness transformation for constantly failed BEs guarantees that a DFT never fails + // in step 0 without intermediate non-Markovians, thus forcibly set nrNonMarkovian + smtchecker->setSolverTimeout(timeout * 1000); + storm::solver::SmtSolver::CheckResult tmp_res = + smtchecker->checkFailsLeqWithEqNonMarkovianState(boundCandidate + nrNonMarkovian, + nrNonMarkovian); + smtchecker->unsetSolverTimeout(); + switch (tmp_res) { + 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"); + // Prevent integer underflow + if (boundCandidate == 0) { + STORM_LOG_DEBUG("Lower bound correction - corrected bound to 0"); + return 0; + } + --boundCandidate; + break; + case storm::solver::SmtSolver::CheckResult::Unknown: + // 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: + // if query is UNSAT, increase number of non-Markovian states and try again + STORM_LOG_TRACE("Lower bound correction - UNSAT"); + ++nrNonMarkovian; + break; + } + } + // 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 + FailureBoundFinder::correctUpperBound(std::shared_ptr smtchecker, + uint64_t bound, uint_fast64_t timeout) { + STORM_LOG_DEBUG("Upper bound correction - try to correct bound " << std::to_string(bound)); + uint64_t boundCandidate = bound; + uint64_t nrDepEvents = 0; + uint64_t nrNonMarkovian = 0; + uint64_t currentTimepoint = 0; + auto dft = smtchecker->getDFT(); + // 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_EXP || + element->type() == storm::storage::DFTElementType::BE_CONST) { + auto be = std::static_pointer_cast const>(element); + if (be->hasIngoingDependencies()) { + ++nrDepEvents; + } + } + } + while (boundCandidate >= 0) { + currentTimepoint = bound + 1; + while (currentTimepoint - boundCandidate > 0) { + --currentTimepoint; + nrNonMarkovian = currentTimepoint - boundCandidate; + STORM_LOG_TRACE( + "Upper bound correction - candidate " << std::to_string(boundCandidate) + << " check split " + << + std::to_string(currentTimepoint) << "|" + << std::to_string(nrNonMarkovian)); + smtchecker->setSolverTimeout(timeout * 1000); + storm::solver::SmtSolver::CheckResult tmp_res = + smtchecker->checkFailsAtTimepointWithEqNonMarkovianState(currentTimepoint, + nrNonMarkovian); + smtchecker->unsetSolverTimeout(); + switch (tmp_res) { + case storm::solver::SmtSolver::CheckResult::Sat: + STORM_LOG_TRACE("Upper bound correction - SAT"); + STORM_LOG_DEBUG("Upper bound correction - corrected to bound " << boundCandidate << + " (TLE can fail at sequence point " + << std::to_string( + currentTimepoint) + << " with " + << std::to_string( + nrNonMarkovian) + << " non-Markovian states)"); + return boundCandidate; + case storm::solver::SmtSolver::CheckResult::Unknown: + // If any query returns unknown, we cannot be sure about the bound and fall back to the naive one + STORM_LOG_DEBUG( + "Upper bound correction - Solver returned 'Unknown', corrected to bound " + << bound); + return bound; + default: + // if query is UNSAT, increase number of non-Markovian states and try again + STORM_LOG_TRACE("Lower bound correction - UNSAT"); + break; + } + } + --boundCandidate; + } + + // if for one candidate all queries are UNSAT, it is not valid. Return last valid candidate + STORM_LOG_DEBUG("Upper bound correction - corrected bound to " << std::to_string(boundCandidate)); + return boundCandidate; + } + + uint64_t FailureBoundFinder::getLeastFailureBound(storm::storage::DFT const &dft, + bool useSMT, uint_fast64_t timeout) { + if (useSMT) { + STORM_LOG_TRACE("Compute lower bound for number of BE failures necessary for the DFT to fail"); + + storm::modelchecker::DFTASFChecker smtchecker(dft); + smtchecker.activateExperimentalMode(); + smtchecker.toSolver(); + + uint64_t bound = 0; + while (bound < dft.nrBasicElements() + 1) { + smtchecker.setSolverTimeout(timeout * 1000); + storm::solver::SmtSolver::CheckResult tmp_res = smtchecker.checkTleFailsWithLeq(bound); + smtchecker.unsetSolverTimeout(); + switch (tmp_res) { + case storm::solver::SmtSolver::CheckResult::Sat: + if (!dft.getDependencies().empty()) { + return correctLowerBound( + std::make_shared(smtchecker), bound, + timeout); + } else { + return bound; + } + case storm::solver::SmtSolver::CheckResult::Unknown: + STORM_LOG_DEBUG("Lower bound: Solver returned 'Unknown'"); + return bound; + default: + ++bound; + break; + } + + } + + return bound; + } else { + // naive bound + return 1; + } + } + + uint64_t FailureBoundFinder::getLeastFailureBound(storm::storage::DFT const &dft, + bool useSMT, uint_fast64_t timeout) { + if (useSMT) { + STORM_LOG_WARN("SMT encoding does not support rational functions"); + } + return 1; + } + + uint64_t FailureBoundFinder::getAlwaysFailedBound(storm::storage::DFT const &dft, bool useSMT, + uint_fast64_t timeout) { + STORM_LOG_TRACE("Compute bound for number of BE failures such that the DFT always fails"); + if (useSMT) { + + storm::modelchecker::DFTASFChecker smtchecker(dft); + smtchecker.activateExperimentalMode(); + smtchecker.toSolver(); + + if (smtchecker.checkTleNeverFailed() == storm::solver::SmtSolver::CheckResult::Sat) { + return dft.nrBasicElements() + 1; + } + uint64_t bound = dft.nrBasicElements(); + while (bound >= 0) { + smtchecker.setSolverTimeout(timeout * 1000); + storm::solver::SmtSolver::CheckResult tmp_res = smtchecker.checkTleFailsWithEq(bound); + smtchecker.unsetSolverTimeout(); + switch (tmp_res) { + case storm::solver::SmtSolver::CheckResult::Sat: + if (!dft.getDependencies().empty()) { + return correctUpperBound( + std::make_shared(smtchecker), bound, + timeout); + } else { + return bound; + } + case storm::solver::SmtSolver::CheckResult::Unknown: + STORM_LOG_DEBUG("Upper bound: Solver returned 'Unknown'"); + return bound; + default: + --bound; + break; + } + } + return bound; + } else { + // naive bound + return dft.nrBasicElements() + 1; + } + } + + uint64_t + FailureBoundFinder::getAlwaysFailedBound(storm::storage::DFT const &dft, bool useSMT, + uint_fast64_t timeout) { + if (useSMT) { + STORM_LOG_WARN("SMT encoding does not support rational functions"); + } + return dft.nrBasicElements() + 1; + } + + class FailureBoundFinder; + } + } +} \ No newline at end of file diff --git a/src/storm-dft/utility/FailureBoundFinder.h b/src/storm-dft/utility/FailureBoundFinder.h new file mode 100644 index 000000000..f4186da98 --- /dev/null +++ b/src/storm-dft/utility/FailureBoundFinder.h @@ -0,0 +1,73 @@ +#include +#include "storm-dft/storage/dft/DFT.h" +#include "storm-dft/modelchecker/dft/DFTASFChecker.h" + +namespace storm { + namespace dft { + namespace utility { + class FailureBoundFinder { + public: + /** + * Get the minimal number of BEs necessary for the TLE to fail (lower bound for number of failures to check) + * + * @param dft the DFT to check + * @param useSMT if set, an SMT solver is used to improve the bounds + * @param timeout timeout for each query in seconds, defaults to 10 seconds + * @return the minimal number + */ + static uint64_t getLeastFailureBound(storm::storage::DFT const &dft, + bool useSMT = false, + uint_fast64_t timeout = 10); + + static uint64_t getLeastFailureBound(storm::storage::DFT const &dft, + bool useSMT = false, + uint_fast64_t timeout = 10); + + /** + * Get the number of BE failures for which the TLE always fails (upper bound for number of failures to check). + * + * @param dft the DFT to check + * @param useSMT if set, an SMT solver is used to improve the bounds + * @param timeout timeout for each query in seconds, defaults to 10 seconds + * @return the number + */ + static uint64_t getAlwaysFailedBound(storm::storage::DFT const &dft, + bool useSMT = false, + uint_fast64_t timeout = 10); + + static uint64_t getAlwaysFailedBound(storm::storage::DFT const &dft, + bool useSMT = false, + uint_fast64_t timeout = 10); + + private: + /** + * 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 smtchecker the SMT checker to use + * @param bound known lower bound to be corrected + * @param timeout timeout timeout for each query in seconds + * @return the corrected bound + */ + static uint64_t + correctLowerBound(std::shared_ptr smtchecker, uint64_t bound, + uint_fast64_t timeout); + + /** + * Helper function for correction of bound for number of BEs such that the DFT always fails when dependencies are present + * + * @param smtchecker the SMT checker to use + * @param bound known bound to be corrected + * @param timeout timeout timeout for each query in seconds + * @return the corrected bound + */ + static uint64_t + correctUpperBound(std::shared_ptr smtchecker, uint64_t bound, + uint_fast64_t timeout); + }; + } + } +} + diff --git a/src/test/storm-dft/api/DftSmtTest.cpp b/src/test/storm-dft/api/DftSmtTest.cpp index 5a7b31095..a572c2b23 100644 --- a/src/test/storm-dft/api/DftSmtTest.cpp +++ b/src/test/storm-dft/api/DftSmtTest.cpp @@ -1,4 +1,5 @@ -#include +#include "storm-dft/utility/FDEPConflictFinder.h" +#include "storm-dft/utility/FailureBoundFinder.h" #include "gtest/gtest.h" #include "storm-config.h" @@ -43,8 +44,8 @@ namespace { storm::modelchecker::DFTASFChecker smtChecker(*dft); smtChecker.convert(); smtChecker.toSolver(); - EXPECT_EQ(smtChecker.getLeastFailureBound(30), uint64_t(2)); - EXPECT_EQ(smtChecker.getAlwaysFailedBound(30), uint64_t(4)); + EXPECT_EQ(storm::dft::utility::FailureBoundFinder::getLeastFailureBound(*dft, true, 30), uint64_t(2)); + EXPECT_EQ(storm::dft::utility::FailureBoundFinder::getAlwaysFailedBound(*dft, true, 30), uint64_t(4)); } TEST(DftSmtTest, FDEPBoundTest) { @@ -54,8 +55,8 @@ namespace { storm::modelchecker::DFTASFChecker smtChecker(*dft); smtChecker.convert(); smtChecker.toSolver(); - EXPECT_EQ(smtChecker.getLeastFailureBound(30), uint64_t(1)); - EXPECT_EQ(smtChecker.getAlwaysFailedBound(30), uint64_t(5)); + EXPECT_EQ(storm::dft::utility::FailureBoundFinder::getLeastFailureBound(*dft, true, 30), uint64_t(1)); + EXPECT_EQ(storm::dft::utility::FailureBoundFinder::getAlwaysFailedBound(*dft, true, 30), uint64_t(5)); } TEST(DftSmtTest, FDEPConflictTest) {