Added check for conflicts between dependencies in the DFT

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<std::shared_ptr<SmtConstraint>> andConstr;
+            std::vector<std::shared_ptr<SmtConstraint>> 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<IsLess>(
+                    timePointVariables.at(dep2Index), dependencyVariables.at(dep2Index)));
+            // AND FDEP1 is triggered before FDEP2 is resolved
+            andConstr.push_back(std::make_shared<IsGreaterEqual>(
+                    timePointVariables.at(dep1Index), timePointVariables.at(dep2Index)));
+            andConstr.push_back(std::make_shared<IsLess>(
+                    timePointVariables.at(dep1Index), dependencyVariables.at(dep2Index)));
+            std::shared_ptr<SmtConstraint> betweenConstr1 = std::make_shared<And>(andConstr);
+
+            andConstr.clear();
+            // FDEP1 was triggered before dependent elements have failed
+            andConstr.push_back(std::make_shared<IsLess>(
+                    timePointVariables.at(dep1Index), dependencyVariables.at(dep1Index)));
+            // AND FDEP2 is triggered before FDEP1 is resolved
+            andConstr.push_back(std::make_shared<IsGreaterEqual>(
+                    timePointVariables.at(dep2Index), timePointVariables.at(dep1Index)));
+            andConstr.push_back(std::make_shared<IsLess>(
+                    timePointVariables.at(dep2Index), dependencyVariables.at(dep1Index)));
+            std::shared_ptr<SmtConstraint> betweenConstr2 = std::make_shared<And>(andConstr);
+
+            orConstr.clear();
+            // Either one of the above constraints holds
+            orConstr.push_back(betweenConstr1);
+            orConstr.push_back(betweenConstr2);
+            std::shared_ptr<SmtConstraint> checkConstr = std::make_shared<Or>(orConstr);
+            std::shared_ptr<storm::expressions::ExpressionManager> 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<std::pair<uint64_t, uint64_t>> DFTASFChecker::getDependencyConflicts(uint_fast64_t timeout) {
+            STORM_LOG_ASSERT(solver, "SMT Solver was not initialized, call toSolver() before checking queries");
+            std::vector<std::pair<uint64_t, uint64_t>> 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<uint64_t, uint64_t>(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<uint64_t, uint64_t>(dep1Index, dep2Index));
+                            break;
+                        default:
+                            STORM_LOG_DEBUG("No conflict between " << dft.getElement(dep1Index)->name() << " and "
+                                                                   << dft.getElement(dep2Index)->name());
+                            break;
+                    }
+                }
+            }
+            return res;
+        }
     }
 }

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<std::pair<uint64_t, uint64_t>> getDependencyConflicts(uint_fast64_t timeout = 10);
+
             /**
              * Set the timeout of the solver
              *

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<std::string> const &varNames) const override {
+                return "(<= " + varNames.at(var1Index) + " " + varNames.at(var2Index) + ")";
+            }
+
+            storm::expressions::Expression toExpression(std::vector<std::string> const &varNames,
+                                                        std::shared_ptr<storm::expressions::ExpressionManager> 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<std::string> const &varNames) const override {
+                return "(>= " + varNames.at(var1Index) + " " + varNames.at(var2Index) + ")";
+            }
+
+            storm::expressions::Expression toExpression(std::vector<std::string> const &varNames,
+                                                        std::shared_ptr<storm::expressions::ExpressionManager> 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: