From 449c513db246b22915e0329d5be2cd5fa79c6dff Mon Sep 17 00:00:00 2001 From: Alexander Bork Date: Wed, 10 Jul 2019 17:03:03 +0200 Subject: [PATCH] Cleanup DFTASFChecker --- src/storm-dft-cli/storm-dft.cpp | 6 ++++-- src/storm-dft/api/storm-dft.cpp | 16 ++++------------ src/storm-dft/api/storm-dft.h | 4 ++-- src/storm-dft/modelchecker/dft/DFTASFChecker.cpp | 9 +-------- src/storm-dft/modelchecker/dft/DFTASFChecker.h | 7 ------- src/storm-dft/utility/FDEPConflictFinder.cpp | 1 - src/storm-dft/utility/FailureBoundFinder.cpp | 2 -- src/test/storm-dft/api/DftSmtTest.cpp | 2 -- 8 files changed, 11 insertions(+), 36 deletions(-) diff --git a/src/storm-dft-cli/storm-dft.cpp b/src/storm-dft-cli/storm-dft.cpp index 01271e2c5..7349e0704 100644 --- a/src/storm-dft-cli/storm-dft.cpp +++ b/src/storm-dft-cli/storm-dft.cpp @@ -86,7 +86,7 @@ void processOptions() { dft = dftTransformator.transformBinaryFDEPs(*dft); } // Export to smtlib2 - storm::api::exportDFTToSMT(*dft, dftIOSettings.getExportSmtFilename(), debug.isTestSet()); + storm::api::exportDFTToSMT(*dft, dftIOSettings.getExportSmtFilename()); return; } @@ -101,7 +101,7 @@ void processOptions() { STORM_LOG_DEBUG("Running DFT analysis with use of SMT"); // Set dynamic behavior vector dft->setDynamicBehaviorInfo(); - auto smtResults = storm::api::analyzeDFTSMT(*dft, true, debug.isTestSet()); + auto smtResults = storm::api::analyzeDFTSMT(*dft, true); // Set the conflict map of the dft std::set conflict_set; for (auto conflict : smtResults.fdepConflicts) { @@ -116,6 +116,8 @@ void processOptions() { } #endif + //Proprocessing + // From now on we analyse DFT via model checking // Set min or max diff --git a/src/storm-dft/api/storm-dft.cpp b/src/storm-dft/api/storm-dft.cpp index 8d2c3ce2a..dd9bd9dcd 100644 --- a/src/storm-dft/api/storm-dft.cpp +++ b/src/storm-dft/api/storm-dft.cpp @@ -31,30 +31,23 @@ namespace storm { } template<> - void exportDFTToSMT(storm::storage::DFT const &dft, std::string const &file, bool experimentalMode) { + void exportDFTToSMT(storm::storage::DFT const &dft, std::string const &file) { storm::modelchecker::DFTASFChecker asfChecker(dft); - if (experimentalMode) { - asfChecker.activateExperimentalMode(); - } asfChecker.convert(); asfChecker.toFile(file); } template<> - void exportDFTToSMT(storm::storage::DFT const &dft, std::string const &file, - bool experimentalMode) { + void exportDFTToSMT(storm::storage::DFT const &dft, std::string const &file) { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Export to SMT does not support this data type."); } template<> storm::api::PreprocessingResult - analyzeDFTSMT(storm::storage::DFT const &dft, bool printOutput, bool experimentalMode) { + analyzeDFTSMT(storm::storage::DFT const &dft, bool printOutput) { uint64_t solverTimeout = 10; storm::modelchecker::DFTASFChecker smtChecker(dft); - if (experimentalMode) { - smtChecker.activateExperimentalMode(); - } smtChecker.toSolver(); storm::api::PreprocessingResult results; @@ -87,8 +80,7 @@ namespace storm { template<> storm::api::PreprocessingResult - analyzeDFTSMT(storm::storage::DFT const &dft, bool printOutput, - bool experimentalMode) { + 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 70d21f854..a3cb5a865 100644 --- a/src/storm-dft/api/storm-dft.h +++ b/src/storm-dft/api/storm-dft.h @@ -109,7 +109,7 @@ namespace storm { */ template storm::api::PreprocessingResult - analyzeDFTSMT(storm::storage::DFT const &dft, bool printOutput, bool experimentalMode); + analyzeDFTSMT(storm::storage::DFT const &dft, bool printOutput); /*! * Export DFT to JSON file. @@ -136,7 +136,7 @@ namespace storm { * @param file File. */ template - void exportDFTToSMT(storm::storage::DFT const &dft, std::string const &file, bool experimentalMode); + void exportDFTToSMT(storm::storage::DFT const &dft, std::string const &file); /*! * Transform DFT to GSPN. diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp index ff9e4f53c..558e2a45c 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp @@ -18,11 +18,6 @@ namespace storm { // Intentionally left empty. } - void DFTASFChecker::activateExperimentalMode() { - STORM_LOG_WARN("DFT-SMT-Checker now runs in experimental mode, no guarantee for correct results is given!"); - experimentalMode = true; - } - uint64_t DFTASFChecker::getClaimVariableIndex(uint64_t spare, uint64_t child) const { return claimVariables.at(SpareAndChildPair(spare, child)); } @@ -44,9 +39,7 @@ namespace storm { beVariables.push_back(varNames.size() - 1); break; case storm::storage::DFTElementType::BE_CONST: { - STORM_LOG_THROW(experimentalMode, storm::exceptions::NotSupportedException, - "Constant BEs are not supported in SMT translation."); - STORM_LOG_WARN("Constant BEs are only experimentally supported"); + STORM_LOG_WARN("Constant BEs are only experimentally supported in the SMT encoding"); // Constant BEs are initially either failed or failsafe, treat them differently auto be = std::static_pointer_cast const>(element); if (be->failed()) { diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.h b/src/storm-dft/modelchecker/dft/DFTASFChecker.h index 61da80af9..8a6e3fda2 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.h +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.h @@ -45,12 +45,6 @@ namespace storm { public: DFTASFChecker(storm::storage::DFT const&); - /** - * Activates the experimental support for constant BEs and possibly other not thoroughly tested features - * - */ - void activateExperimentalMode(); - /** * Generate general variables and constraints for the DFT and store them in the corresponding maps and vectors * @@ -235,7 +229,6 @@ namespace storm { std::unordered_map markovianVariables; std::vector tmpTimePointVariables; uint64_t notFailed; - bool experimentalMode = false; }; } } diff --git a/src/storm-dft/utility/FDEPConflictFinder.cpp b/src/storm-dft/utility/FDEPConflictFinder.cpp index fb214bcce..53f63ae4b 100644 --- a/src/storm-dft/utility/FDEPConflictFinder.cpp +++ b/src/storm-dft/utility/FDEPConflictFinder.cpp @@ -13,7 +13,6 @@ namespace storm { if (useSMT) { storm::modelchecker::DFTASFChecker checker(dft); smtChecker = std::make_shared(checker); - smtChecker->activateExperimentalMode(); smtChecker->toSolver(); } diff --git a/src/storm-dft/utility/FailureBoundFinder.cpp b/src/storm-dft/utility/FailureBoundFinder.cpp index 59243ad54..d09caae83 100644 --- a/src/storm-dft/utility/FailureBoundFinder.cpp +++ b/src/storm-dft/utility/FailureBoundFinder.cpp @@ -143,7 +143,6 @@ namespace storm { STORM_LOG_TRACE("Compute lower bound for number of BE failures necessary for the DFT to fail"); storm::modelchecker::DFTASFChecker smtchecker(dft); - smtchecker.activateExperimentalMode(); smtchecker.toSolver(); uint64_t bound = 0; @@ -191,7 +190,6 @@ namespace storm { if (useSMT) { storm::modelchecker::DFTASFChecker smtchecker(dft); - smtchecker.activateExperimentalMode(); smtchecker.toSolver(); if (smtchecker.checkTleNeverFailed() == storm::solver::SmtSolver::CheckResult::Sat) { diff --git a/src/test/storm-dft/api/DftSmtTest.cpp b/src/test/storm-dft/api/DftSmtTest.cpp index a572c2b23..f23a433c9 100644 --- a/src/test/storm-dft/api/DftSmtTest.cpp +++ b/src/test/storm-dft/api/DftSmtTest.cpp @@ -1,5 +1,3 @@ -#include "storm-dft/utility/FDEPConflictFinder.h" -#include "storm-dft/utility/FailureBoundFinder.h" #include "gtest/gtest.h" #include "storm-config.h"