diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp index 87cd93a17..1583f3867 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp @@ -610,6 +610,49 @@ namespace storm { return res; } + storm::solver::SmtSolver::CheckResult + DFTASFChecker::checkDependencyConflict(uint64_t dep1Index, uint64_t dep2Index, uint64_t timeout) { + std::vector> andConstr; + std::vector> orConstr; + STORM_LOG_DEBUG( + "Check " << dft.getElement(dep1Index)->name() << " and " << dft.getElement(dep2Index)->name()); + andConstr.clear(); + // FDEP2 was triggered before dependent elements have failed + andConstr.push_back(std::make_shared( + timePointVariables.at(dep2Index), dependencyVariables.at(dep2Index))); + // AND FDEP1 is triggered before FDEP2 is resolved + andConstr.push_back(std::make_shared( + timePointVariables.at(dep1Index), timePointVariables.at(dep2Index))); + andConstr.push_back(std::make_shared( + timePointVariables.at(dep1Index), dependencyVariables.at(dep2Index))); + std::shared_ptr betweenConstr1 = std::make_shared(andConstr); + + andConstr.clear(); + // FDEP1 was triggered before dependent elements have failed + andConstr.push_back(std::make_shared( + timePointVariables.at(dep1Index), dependencyVariables.at(dep1Index))); + // AND FDEP2 is triggered before FDEP1 is resolved + andConstr.push_back(std::make_shared( + timePointVariables.at(dep2Index), timePointVariables.at(dep1Index))); + andConstr.push_back(std::make_shared( + timePointVariables.at(dep2Index), dependencyVariables.at(dep1Index))); + std::shared_ptr betweenConstr2 = std::make_shared(andConstr); + + orConstr.clear(); + // Either one of the above constraints holds + orConstr.push_back(betweenConstr1); + orConstr.push_back(betweenConstr2); + std::shared_ptr checkConstr = std::make_shared(orConstr); + std::shared_ptr manager = solver->getManager().getSharedPointer(); + solver->push(); + solver->add(checkConstr->toExpression(varNames, manager)); + setSolverTimeout(timeout * 1000); + storm::solver::SmtSolver::CheckResult res = solver->check(); + unsetSolverTimeout(); + 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)); @@ -741,5 +784,35 @@ namespace storm { } return bound; } + + std::vector> DFTASFChecker::getDependencyConflicts(uint_fast64_t timeout) { + STORM_LOG_ASSERT(solver, "SMT Solver was not initialized, call toSolver() before checking queries"); + std::vector> res; + uint64_t dep1Index; + uint64_t dep2Index; + for (size_t i = 0; i < dft.getDependencies().size(); ++i) { + dep1Index = dft.getDependencies().at(i); + for (size_t j = i + 1; j < dft.getDependencies().size(); ++j) { + dep2Index = dft.getDependencies().at(j); + switch (checkDependencyConflict(dep1Index, dep2Index, timeout)) { + case storm::solver::SmtSolver::CheckResult::Sat: + STORM_LOG_DEBUG("Conflict between " << dft.getElement(dep1Index)->name() << " and " + << dft.getElement(dep2Index)->name()); + res.emplace_back(std::pair(dep1Index, dep2Index)); + break; + case storm::solver::SmtSolver::CheckResult::Unknown: + STORM_LOG_DEBUG("Unknown: Conflict between " << dft.getElement(dep1Index)->name() << " and " + << dft.getElement(dep2Index)->name()); + res.emplace_back(std::pair(dep1Index, dep2Index)); + break; + default: + STORM_LOG_DEBUG("No conflict between " << dft.getElement(dep1Index)->name() << " and " + << dft.getElement(dep2Index)->name()); + break; + } + } + } + return res; + } } } diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.h b/src/storm-dft/modelchecker/dft/DFTASFChecker.h index 84310b775..75eef8c64 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.h +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.h @@ -79,6 +79,19 @@ namespace storm { */ storm::solver::SmtSolver::CheckResult checkTleFailsWithLeq(uint64_t bound); + /** + * Check if two given dependencies are conflicting in their resolution, i.e. check if non-determinism may occur. + * Note that this is a very conservative check using SMT formulae. + * We only check if sequences exist, where one of the dependencies is triggered before the other is completely resolved + * + * @param dep1Index Index of the first dependency + * @param dep2Index Index of the second dependency + * @param timeout timeout for the solver + * @return "Sat" if the dependencies are conflicting, "Unsat" if they are not, otherwise "Unknown" + */ + 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) * @@ -96,6 +109,14 @@ namespace storm { */ uint64_t getAlwaysFailedBound(uint_fast64_t timeout = 10); + /** + * Get a vector of index pairs of FDEPs which are conflicting according to a conservative definition + * + * @param timeout timeout for each query in seconds, defaults to 10 seconds + * @return a vector of pairs of FDEP indices which are conflicting + */ + std::vector> getDependencyConflicts(uint_fast64_t timeout = 10); + /** * Set the timeout of the solver * diff --git a/src/storm-dft/modelchecker/dft/SmtConstraint.cpp b/src/storm-dft/modelchecker/dft/SmtConstraint.cpp index 78e963d05..ef16d580a 100644 --- a/src/storm-dft/modelchecker/dft/SmtConstraint.cpp +++ b/src/storm-dft/modelchecker/dft/SmtConstraint.cpp @@ -493,6 +493,52 @@ namespace storm { uint64_t var2Index; }; + class IsLessEqual : public SmtConstraint { + public: + IsLessEqual(uint64_t varIndex1, uint64_t varIndex2) : var1Index(varIndex1), var2Index(varIndex2) { + } + + virtual ~IsLessEqual() { + } + + std::string toSmtlib2(std::vector const &varNames) const override { + return "(<= " + varNames.at(var1Index) + " " + varNames.at(var2Index) + ")"; + } + + storm::expressions::Expression toExpression(std::vector const &varNames, + std::shared_ptr manager) const override { + return manager->getVariableExpression(varNames.at(var1Index)) <= + manager->getVariableExpression(varNames.at(var2Index)); + } + + private: + uint64_t var1Index; + uint64_t var2Index; + }; + + class IsGreaterEqual : public SmtConstraint { + public: + IsGreaterEqual(uint64_t varIndex1, uint64_t varIndex2) : var1Index(varIndex1), var2Index(varIndex2) { + } + + virtual ~IsGreaterEqual() { + } + + std::string toSmtlib2(std::vector const &varNames) const override { + return "(>= " + varNames.at(var1Index) + " " + varNames.at(var2Index) + ")"; + } + + storm::expressions::Expression toExpression(std::vector const &varNames, + std::shared_ptr manager) const override { + return manager->getVariableExpression(varNames.at(var1Index)) >= + manager->getVariableExpression(varNames.at(var2Index)); + } + + private: + uint64_t var1Index; + uint64_t var2Index; + }; + class PairwiseDifferent : public SmtConstraint { public: