Browse Source

Fixed error that SMT solver was always used in the FDEP conflict search

tempestpy_adaptions
Alexander Bork 5 years ago
parent
commit
628331fda3
  1. 6
      src/storm-dft-cli/storm-dft.cpp

6
src/storm-dft-cli/storm-dft.cpp

@ -117,13 +117,17 @@ void processOptions() {
"Lower bound: " << std::to_string(preResults.lowerBEBound) << std::endl << "Lower bound: " << std::to_string(preResults.lowerBEBound) << std::endl <<
"Upper bound: " << std::to_string(preResults.upperBEBound) << std::endl); "Upper bound: " << std::to_string(preResults.upperBEBound) << std::endl);
preResults.fdepConflicts = storm::dft::utility::FDEPConflictFinder::getDependencyConflicts(*dft, true,
preResults.fdepConflicts = storm::dft::utility::FDEPConflictFinder::getDependencyConflicts(*dft, useSMT,
solverTimeout); solverTimeout);
if (preResults.fdepConflicts.empty()) {
STORM_LOG_DEBUG("No FDEP conflicts found" << std::endl);
} else {
STORM_LOG_DEBUG("========================================" << std::endl << STORM_LOG_DEBUG("========================================" << std::endl <<
"FDEP CONFLICTS" << std::endl << "FDEP CONFLICTS" << std::endl <<
"========================================" "========================================"
<< std::endl); << std::endl);
}
for (auto pair: preResults.fdepConflicts) { for (auto pair: preResults.fdepConflicts) {
STORM_LOG_DEBUG("Conflict between " << dft->getElement(pair.first)->name() << " and " STORM_LOG_DEBUG("Conflict between " << dft->getElement(pair.first)->name() << " and "
<< dft->getElement(pair.second)->name() << std::endl); << dft->getElement(pair.second)->name() << std::endl);

Loading…
Cancel
Save