diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp index 7b61ea655..e993ac7dc 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp @@ -241,14 +241,6 @@ namespace storm { STORM_LOG_ASSERT(children.size() >= 2, "Spare has only one child"); 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); @@ -259,28 +251,6 @@ 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 { @@ -309,7 +279,9 @@ namespace storm { // not a different spare. continue; } - claimingPossibleC.push_back(std::make_shared(getClaimVariableIndex(otherSpare->id(), child->id()), notFailed)); + claimingPossibleC.push_back(std::make_shared(timepoint, + getClaimVariableIndex(otherSpare->id(), + child->id()))); } // Claim child if available @@ -532,40 +504,51 @@ namespace storm { return checkTleFailsWithEq(notFailed); } - uint64_t DFTASFChecker::getLeastFailureBound() { + uint64_t DFTASFChecker::getLeastFailureBound(uint_fast64_t timeout) { 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); + setSolverTimeout(timeout * 1000); 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; + switch (tmp_res) { + case storm::solver::SmtSolver::CheckResult::Sat: + return bound; + case storm::solver::SmtSolver::CheckResult::Unknown: + STORM_LOG_DEBUG("Solver returned 'Unknown'"); + return bound; + default: + ++bound; + break; } - ++bound; + } return bound; } - uint64_t DFTASFChecker::getAlwaysFailedBound() { + uint64_t DFTASFChecker::getAlwaysFailedBound(uint_fast64_t timeout) { 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); + setSolverTimeout(timeout * 1000); 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; + switch (tmp_res) { + case storm::solver::SmtSolver::CheckResult::Sat: + return bound; + case storm::solver::SmtSolver::CheckResult::Unknown: + STORM_LOG_DEBUG("Solver returned 'Unknown'"); + return bound; + default: + --bound; + break; } - --bound; } return bound; } diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.h b/src/storm-dft/modelchecker/dft/DFTASFChecker.h index 2141694f5..d8da63dce 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.h +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.h @@ -68,16 +68,18 @@ namespace storm { /** * 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(); + 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) * + * @param timeout timeout for each query in seconds, defaults to 10 seconds * @return the number */ - uint64_t getAlwaysFailedBound(); + uint64_t getAlwaysFailedBound(uint_fast64_t timeout = 10); /** * Set the timeout of the solver @@ -94,19 +96,6 @@ 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. diff --git a/src/storm-dft/modelchecker/dft/SmtConstraint.cpp b/src/storm-dft/modelchecker/dft/SmtConstraint.cpp index e9bc2b220..83433989b 100644 --- a/src/storm-dft/modelchecker/dft/SmtConstraint.cpp +++ b/src/storm-dft/modelchecker/dft/SmtConstraint.cpp @@ -370,6 +370,31 @@ namespace storm { uint64_t value; }; + class IsGreaterConstant : public SmtConstraint { + public: + IsGreaterConstant(uint64_t varIndex, uint64_t val) : varIndex(varIndex), value(val) { + } + + virtual ~IsGreaterConstant() { + } + + 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 IsLessEqualConstant : public SmtConstraint { public: IsLessEqualConstant(uint64_t varIndex, uint64_t val) : varIndex(varIndex), value(val) {