diff --git a/src/storm-dft-cli/storm-dft.cpp b/src/storm-dft-cli/storm-dft.cpp index 619754ba1..9a2546eae 100644 --- a/src/storm-dft-cli/storm-dft.cpp +++ b/src/storm-dft-cli/storm-dft.cpp @@ -90,46 +90,25 @@ void processOptions() { dft = storm::api::applyTransformations(*dft, faultTreeSettings.isUniqueFailedBE(), true); STORM_LOG_DEBUG(dft->getElementsString()); - - dft->setDynamicBehaviorInfo(); - - storm::api::PreprocessingResult preResults; + // Compute minimal number of BE failures leading to system failure and + // maximal number of BE failures not leading to system failure yet. // TODO: always needed? - preResults.lowerBEBound = storm::dft::utility::FailureBoundFinder::getLeastFailureBound(*dft, useSMT, solverTimeout); - preResults.upperBEBound = storm::dft::utility::FailureBoundFinder::getAlwaysFailedBound(*dft, useSMT, solverTimeout); - STORM_LOG_DEBUG("BE failure bounds" << std::endl << "========================================" << std::endl << - "Lower bound: " << std::to_string(preResults.lowerBEBound) << std::endl << - "Upper bound: " << std::to_string(preResults.upperBEBound)); + auto bounds = storm::api::computeBEFailureBounds(*dft, useSMT, solverTimeout); + STORM_LOG_DEBUG("BE failure bounds: lower bound: " << bounds.first << ", upper bound: " << bounds.second << "."); - // TODO: move into API call? - preResults.fdepConflicts = storm::dft::utility::FDEPConflictFinder::getDependencyConflicts(*dft, useSMT, solverTimeout); - - if (preResults.fdepConflicts.empty()) { - STORM_LOG_DEBUG("No FDEP conflicts found"); + // Check which FDEPs actually introduce conflicts which need non-deterministic resolution + bool hasConflicts = storm::api::computeDependencyConflicts(*dft, useSMT, solverTimeout); + if (hasConflicts) { + STORM_LOG_DEBUG("FDEP conflicts found."); } else { - STORM_LOG_DEBUG("========================================" << std::endl << "FDEP CONFLICTS" << std::endl << "========================================"); - } - for (auto pair: preResults.fdepConflicts) { - STORM_LOG_DEBUG("Conflict between " << dft->getElement(pair.first)->name() << " and " << dft->getElement(pair.second)->name()); - } - - // Set the conflict map of the dft - std::set conflict_set; - for (auto conflict : preResults.fdepConflicts) { - conflict_set.insert(size_t(conflict.first)); - conflict_set.insert(size_t(conflict.second)); - } - for (size_t depId : dft->getDependencies()) { - if (!conflict_set.count(depId)) { - dft->setDependencyNotInConflict(depId); - } + STORM_LOG_DEBUG("No FDEP conflicts found."); } #ifdef STORM_HAVE_Z3 if (useSMT) { // Solve with SMT - STORM_LOG_DEBUG("Running DFT analysis with use of SMT"); + STORM_LOG_DEBUG("Running DFT analysis with use of SMT."); // Set dynamic behavior vector storm::api::analyzeDFTSMT(*dft, true); } diff --git a/src/storm-dft/api/storm-dft.h b/src/storm-dft/api/storm-dft.h index bfe90f37a..a14d7d2c7 100644 --- a/src/storm-dft/api/storm-dft.h +++ b/src/storm-dft/api/storm-dft.h @@ -18,12 +18,6 @@ namespace storm { namespace api { - struct PreprocessingResult { - uint64_t lowerBEBound; - uint64_t upperBEBound; - std::vector> fdepConflicts; - }; - /*! * Load DFT from Galileo file. @@ -93,29 +87,36 @@ namespace storm { return transformedDFT; } - template - bool computeDependencyConflicts(storm::storage::DFT const& dft, bool useSMT, double solverTimeout) { - std::vector> fdepConflicts = storm::dft::utility::FDEPConflictFinder::getDependencyConflicts(*dft, useSMT, solverTimeout); + template + std::pair computeBEFailureBounds(storm::storage::DFT const& dft, bool useSMT, double solverTimeout) { + uint64_t lowerBEBound = storm::dft::utility::FailureBoundFinder::getLeastFailureBound(dft, useSMT, solverTimeout); + uint64_t upperBEBound = storm::dft::utility::FailureBoundFinder::getAlwaysFailedBound(dft, useSMT, solverTimeout); + return std::make_pair(lowerBEBound, upperBEBound); + } - if (fdepConflicts.empty()) { - return false; - } - for (auto pair: fdepConflicts) { + template + bool computeDependencyConflicts(storm::storage::DFT& dft, bool useSMT, double solverTimeout) { + // Initialize which DFT elements have dynamic behavior + dft.setDynamicBehaviorInfo(); + + std::vector> fdepConflicts = storm::dft::utility::FDEPConflictFinder::getDependencyConflicts(dft, useSMT, solverTimeout); + + for (auto const& pair: fdepConflicts) { STORM_LOG_DEBUG("Conflict between " << dft.getElement(pair.first)->name() << " and " << dft.getElement(pair.second)->name()); } // Set the conflict map of the dft std::set conflict_set; - for (auto conflict : fdepConflicts) { + for (auto const& conflict : fdepConflicts) { conflict_set.insert(size_t(conflict.first)); conflict_set.insert(size_t(conflict.second)); } - for (size_t depId : dft->getDependencies()) { + for (size_t depId : dft.getDependencies()) { if (!conflict_set.count(depId)) { - dft->setDependencyNotInConflict(depId); + dft.setDependencyNotInConflict(depId); } } - return true; + return !fdepConflicts.empty(); } /*! diff --git a/src/storm-dft/utility/FDEPConflictFinder.cpp b/src/storm-dft/utility/FDEPConflictFinder.cpp index eb4447ffb..3b29c0976 100644 --- a/src/storm-dft/utility/FDEPConflictFinder.cpp +++ b/src/storm-dft/utility/FDEPConflictFinder.cpp @@ -25,29 +25,29 @@ namespace storm { if (dft.getDynamicBehavior()[dep1Index] && dft.getDynamicBehavior()[dep2Index]) { if (useSMT) { // if an SMT solver is to be used 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"); + STORM_LOG_TRACE("Conflict between " << dft.getElement(dep1Index)->name() << " and " << dft.getElement(dep2Index)->name() << ": Same trigger"); res.emplace_back(std::pair(dep1Index, dep2Index)); } else { switch (smtChecker->checkDependencyConflict(dep1Index, dep2Index, timeout)) { case storm::solver::SmtSolver::CheckResult::Sat: - STORM_LOG_DEBUG("Conflict between " << dft.getElement(dep1Index)->name() << " and " << dft.getElement(dep2Index)->name()); + STORM_LOG_TRACE("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()); + STORM_LOG_TRACE("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()); + STORM_LOG_TRACE("No conflict between " << dft.getElement(dep1Index)->name() << " and " << dft.getElement(dep2Index)->name()); break; } } } else { - STORM_LOG_DEBUG("Conflict between " << dft.getElement(dep1Index)->name() << " and " << dft.getElement(dep2Index)->name()); + STORM_LOG_TRACE("Conflict between " << dft.getElement(dep1Index)->name() << " and " << dft.getElement(dep2Index)->name()); res.emplace_back(std::pair(dep1Index, dep2Index)); } } else { - STORM_LOG_DEBUG("Static behavior: No conflict between " << dft.getElement(dep1Index)->name() << " and " << dft.getElement(dep2Index)->name()); + STORM_LOG_TRACE("Static behavior: No conflict between " << dft.getElement(dep1Index)->name() << " and " << dft.getElement(dep2Index)->name()); break; } } @@ -70,10 +70,10 @@ namespace storm { for (size_t j = i + 1; j < dft.getDependencies().size(); ++j) { dep2Index = dft.getDependencies().at(j); if (dft.getDynamicBehavior()[dep1Index] && dft.getDynamicBehavior()[dep2Index]) { - STORM_LOG_DEBUG("Conflict between " << dft.getElement(dep1Index)->name() << " and " << dft.getElement(dep2Index)->name()); + STORM_LOG_TRACE("Conflict between " << dft.getElement(dep1Index)->name() << " and " << dft.getElement(dep2Index)->name()); res.emplace_back(std::pair(dep1Index, dep2Index)); } else { - STORM_LOG_DEBUG("Static behavior: No conflict between " << dft.getElement(dep1Index)->name() << " and " << dft.getElement(dep2Index)->name()); + STORM_LOG_TRACE("Static behavior: No conflict between " << dft.getElement(dep1Index)->name() << " and " << dft.getElement(dep2Index)->name()); break; } } @@ -88,4 +88,4 @@ namespace storm { class FDEPConflictFinder; } } -} \ No newline at end of file +}