From ec67166041d50c3d4127cc5cba1cf76335c77595 Mon Sep 17 00:00:00 2001 From: Alexander Bork Date: Wed, 10 Jul 2019 17:38:57 +0200 Subject: [PATCH] Decoupled preprocessing and SMT solving in commandline interface --- src/storm-dft-cli/storm-dft.cpp | 68 +++++++++++++++++++++++++-------- src/storm-dft/api/storm-dft.cpp | 35 +++-------------- src/storm-dft/api/storm-dft.h | 2 +- 3 files changed, 60 insertions(+), 45 deletions(-) diff --git a/src/storm-dft-cli/storm-dft.cpp b/src/storm-dft-cli/storm-dft.cpp index 7349e0704..7ce6eadea 100644 --- a/src/storm-dft-cli/storm-dft.cpp +++ b/src/storm-dft-cli/storm-dft.cpp @@ -28,7 +28,6 @@ void processOptions() { storm::settings::modules::FaultTreeSettings const& faultTreeSettings = storm::settings::getModule(); storm::settings::modules::IOSettings const& ioSettings = storm::settings::getModule(); storm::settings::modules::DftGspnSettings const& dftGspnSettings = storm::settings::getModule(); - auto const &debug = storm::settings::getModule(); auto dftTransformator = storm::transformations::dft::DftTransformator(); @@ -90,33 +89,72 @@ void processOptions() { return; } + // TODO introduce some flags + bool useSMT = false; + bool printOutput = false; + uint64_t solverTimeout = 10; #ifdef STORM_HAVE_Z3 if (faultTreeSettings.solveWithSMT()) { + useSMT = true; + STORM_PRINT("Use SMT for preprocessing" << std::endl) dft = dftTransformator.transformUniqueFailedBe(*dft); if (dft->getDependencies().size() > 0) { // Making the constantly failed BE unique may introduce non-binary FDEPs dft = dftTransformator.transformBinaryFDEPs(*dft); } + } +#endif + + dft->setDynamicBehaviorInfo(); + + storm::api::PreprocessingResult preResults; + preResults.lowerBEBound = storm::dft::utility::FailureBoundFinder::getLeastFailureBound(*dft, useSMT, + solverTimeout); + preResults.upperBEBound = storm::dft::utility::FailureBoundFinder::getAlwaysFailedBound(*dft, useSMT, + solverTimeout); + if (printOutput) { + STORM_PRINT("BE FAILURE BOUNDS" << std::endl << + "========================================" << std::endl << + "Lower bound: " << std::to_string(preResults.lowerBEBound) << std::endl << + "Upper bound: " << std::to_string(preResults.upperBEBound) << std::endl) + } + + preResults.fdepConflicts = storm::dft::utility::FDEPConflictFinder::getDependencyConflicts(*dft, true, + solverTimeout); + + if (printOutput) { + STORM_PRINT("========================================" << std::endl << + "FDEP CONFLICTS" << std::endl << + "========================================" + << std::endl) + for (auto pair: preResults.fdepConflicts) { + STORM_PRINT("Conflict between " << dft->getElement(pair.first)->name() << " and " + << dft->getElement(pair.second)->name() << std::endl) + } + } + + // 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); + } + } + + +#ifdef STORM_HAVE_Z3 + if (faultTreeSettings.solveWithSMT()) { // Solve with SMT STORM_LOG_DEBUG("Running DFT analysis with use of SMT"); // Set dynamic behavior vector - dft->setDynamicBehaviorInfo(); - auto smtResults = storm::api::analyzeDFTSMT(*dft, true); - // Set the conflict map of the dft - std::set conflict_set; - for (auto conflict : smtResults.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::api::analyzeDFTSMT(*dft, true); } #endif - //Proprocessing // From now on we analyse DFT via model checking diff --git a/src/storm-dft/api/storm-dft.cpp b/src/storm-dft/api/storm-dft.cpp index dd9bd9dcd..b4deb1cfa 100644 --- a/src/storm-dft/api/storm-dft.cpp +++ b/src/storm-dft/api/storm-dft.cpp @@ -43,43 +43,20 @@ namespace storm { } template<> - storm::api::PreprocessingResult + void analyzeDFTSMT(storm::storage::DFT const &dft, bool printOutput) { uint64_t solverTimeout = 10; storm::modelchecker::DFTASFChecker smtChecker(dft); smtChecker.toSolver(); - storm::api::PreprocessingResult results; - - results.lowerBEBound = storm::dft::utility::FailureBoundFinder::getLeastFailureBound(dft, true, - solverTimeout); - results.upperBEBound = storm::dft::utility::FailureBoundFinder::getAlwaysFailedBound(dft, true, - 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 = storm::dft::utility::FDEPConflictFinder::getDependencyConflicts(dft, true, - solverTimeout); - - if (printOutput) { - STORM_PRINT("========================================" << std::endl << - "FDEP CONFLICTS" << std::endl << - "========================================" - << std::endl) - for (auto pair: results.fdepConflicts) { - STORM_PRINT("Conflict between " << dft.getElement(pair.first)->name() << " and " - << dft.getElement(pair.second)->name() << std::endl) - } - } - return results; + // Removed bound computation etc. here + smtChecker.setSolverTimeout(solverTimeout); + smtChecker.checkTleNeverFailed(); + smtChecker.unsetSolverTimeout(); } template<> - storm::api::PreprocessingResult + void analyzeDFTSMT(storm::storage::DFT const &dft, bool printOutput) { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Analysis by SMT not supported for this data type."); diff --git a/src/storm-dft/api/storm-dft.h b/src/storm-dft/api/storm-dft.h index a3cb5a865..c9aa6b902 100644 --- a/src/storm-dft/api/storm-dft.h +++ b/src/storm-dft/api/storm-dft.h @@ -108,7 +108,7 @@ namespace storm { * @return Result result vector */ template - storm::api::PreprocessingResult + void analyzeDFTSMT(storm::storage::DFT const &dft, bool printOutput); /*!