diff --git a/src/storm-dft/api/storm-dft.cpp b/src/storm-dft/api/storm-dft.cpp index 6f9943768..16b6f4d00 100644 --- a/src/storm-dft/api/storm-dft.cpp +++ b/src/storm-dft/api/storm-dft.cpp @@ -45,19 +45,23 @@ namespace storm { template<> storm::api::SMTResult analyzeDFTSMT(storm::storage::DFT 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 << diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp index beecbc805..85326c8b2 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp @@ -798,21 +798,28 @@ namespace storm { 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; + 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(dep1Index, dep2Index)); + } else { + 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; + } } } }