Improved conflict search by directly capturing DEPs with same trigger

src/storm-dft/api/storm-dft.cpp

@@ -45,19 +45,23 @@ namespace storm {
         template<>
         storm::api::SMTResult
         analyzeDFTSMT(storm::storage::DFT<double> const &dft, bool printOutput) {
+            uint64_t solverTimeout = 10;
+
             storm::modelchecker::DFTASFChecker smtChecker(dft);
             smtChecker.toSolver();
             storm::api::SMTResult results;
 
-            results.lowerBEBound = smtChecker.getLeastFailureBound();
-            results.upperBEBound = smtChecker.getAlwaysFailedBound();
+            results.lowerBEBound = smtChecker.getLeastFailureBound(solverTimeout);
+            results.upperBEBound = smtChecker.getAlwaysFailedBound(solverTimeout);
             if (printOutput) {
                 STORM_PRINT("BE FAILURE BOUNDS" << std::endl <<
                                                 "========================================" << std::endl <<
                                                 "Lower bound: " << std::to_string(results.lowerBEBound) << std::endl <<
                                                 "Upper bound: " << std::to_string(results.upperBEBound) << std::endl)
             }
-            results.fdepConflicts = smtChecker.getDependencyConflicts();
+
+            results.fdepConflicts = smtChecker.getDependencyConflicts(solverTimeout);
+
             if (printOutput) {
                 STORM_PRINT("========================================" << std::endl <<
                                                                        "FDEP CONFLICTS" << std::endl <<

src/storm-dft/modelchecker/dft/DFTASFChecker.cpp

@@ -798,6 +798,11 @@ namespace storm {
                 dep1Index = dft.getDependencies().at(i);
                 for (size_t j = i + 1; j < dft.getDependencies().size(); ++j) {
                     dep2Index = dft.getDependencies().at(j);
+                    if (dft.getDependency(dep1Index)->triggerEvent() == dft.getDependency(dep2Index)->triggerEvent()) {
+                        STORM_LOG_DEBUG("Conflict between " << dft.getElement(dep1Index)->name() << " and "
+                                                            << dft.getElement(dep2Index)->name() << ": Same trigger");
+                        res.emplace_back(std::pair<uint64_t, uint64_t>(dep1Index, dep2Index));
+                    } else {
                         switch (checkDependencyConflict(dep1Index, dep2Index, timeout)) {
                             case storm::solver::SmtSolver::CheckResult::Sat:
                                 STORM_LOG_DEBUG("Conflict between " << dft.getElement(dep1Index)->name() << " and "
@@ -805,7 +810,8 @@ namespace storm {
                                 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 "
+                                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;
@@ -816,6 +822,7 @@ namespace storm {
                         }
                     }
                 }
+            }
             return res;
         }
     }