From 9c74bbed248305c96f795bd7cce488fef070020f Mon Sep 17 00:00:00 2001 From: Alexander Bork Date: Wed, 10 Jul 2019 14:34:53 +0200 Subject: [PATCH] Decoupled FDEP conflict search and SMT solver --- src/storm-dft/api/storm-dft.cpp | 4 +- src/storm-dft/api/storm-dft.h | 2 +- .../modelchecker/dft/DFTASFChecker.cpp | 46 ------- .../modelchecker/dft/DFTASFChecker.h | 7 -- src/storm-dft/utility/FDEPConflictFinder.cpp | 112 ++++++++++++++++++ src/storm-dft/utility/FDEPConflictFinder.h | 29 +++++ src/test/storm-dft/api/DftSmtTest.cpp | 16 +-- 7 files changed, 149 insertions(+), 67 deletions(-) create mode 100644 src/storm-dft/utility/FDEPConflictFinder.cpp create mode 100644 src/storm-dft/utility/FDEPConflictFinder.h diff --git a/src/storm-dft/api/storm-dft.cpp b/src/storm-dft/api/storm-dft.cpp index 2cb36853f..d74120402 100644 --- a/src/storm-dft/api/storm-dft.cpp +++ b/src/storm-dft/api/storm-dft.cpp @@ -4,6 +4,7 @@ #include "storm-dft/settings/modules/DftGspnSettings.h" #include "storm-conv/settings/modules/JaniExportSettings.h" #include "storm-conv/api/storm-conv.h" +#include "storm-dft/utility/FDEPConflictFinder.h" namespace storm { namespace api { @@ -67,7 +68,8 @@ namespace storm { "Upper bound: " << std::to_string(results.upperBEBound) << std::endl) } - results.fdepConflicts = smtChecker.getDependencyConflicts(solverTimeout); + results.fdepConflicts = storm::dft::utility::FDEPConflictFinder::getDependencyConflicts(dft, true, + solverTimeout); if (printOutput) { STORM_PRINT("========================================" << std::endl << diff --git a/src/storm-dft/api/storm-dft.h b/src/storm-dft/api/storm-dft.h index 2af6a43e1..17bc94a15 100644 --- a/src/storm-dft/api/storm-dft.h +++ b/src/storm-dft/api/storm-dft.h @@ -13,7 +13,7 @@ namespace storm { namespace api { - struct SMTResult { + struct PreprocessingResult { uint64_t lowerBEBound; uint64_t upperBEBound; std::vector> fdepConflicts; diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp index c30b365a1..6fc9ef1ae 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp @@ -939,51 +939,5 @@ namespace storm { return bound; } - std::vector> DFTASFChecker::getDependencyConflicts(uint_fast64_t timeout) { - STORM_LOG_ASSERT(solver, "SMT Solver was not initialized, call toSolver() before checking queries"); - std::vector> res; - uint64_t dep1Index; - uint64_t dep2Index; - for (size_t i = 0; i < dft.getDependencies().size(); ++i) { - dep1Index = dft.getDependencies().at(i); - for (size_t j = i + 1; j < dft.getDependencies().size(); ++j) { - dep2Index = dft.getDependencies().at(j); - if (dft.getDynamicBehavior()[dep1Index] && dft.getDynamicBehavior()[dep2Index]) { - 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; - } - } - } else { - STORM_LOG_DEBUG( - "Static behavior: No conflict between " << dft.getElement(dep1Index)->name() << " and " - << dft.getElement(dep2Index)->name()); - break; - } - } - } - return res; - } } } diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.h b/src/storm-dft/modelchecker/dft/DFTASFChecker.h index 73f15a530..3cff2a6a5 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.h +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.h @@ -116,13 +116,6 @@ namespace storm { */ uint64_t getAlwaysFailedBound(uint_fast64_t timeout = 10); - /** - * Get a vector of index pairs of FDEPs which are conflicting according to a conservative definition - * - * @param timeout timeout for each query in seconds, defaults to 10 seconds - * @return a vector of pairs of FDEP indices which are conflicting - */ - std::vector> getDependencyConflicts(uint_fast64_t timeout = 10); /** * Set the timeout of the solver diff --git a/src/storm-dft/utility/FDEPConflictFinder.cpp b/src/storm-dft/utility/FDEPConflictFinder.cpp new file mode 100644 index 000000000..fb214bcce --- /dev/null +++ b/src/storm-dft/utility/FDEPConflictFinder.cpp @@ -0,0 +1,112 @@ +#include "FDEPConflictFinder.h" + +namespace storm { + namespace dft { + namespace utility { + + std::vector> + FDEPConflictFinder::getDependencyConflicts(storm::storage::DFT const &dft, + bool useSMT, + uint_fast64_t timeout) { + + std::shared_ptr smtChecker = nullptr; + if (useSMT) { + storm::modelchecker::DFTASFChecker checker(dft); + smtChecker = std::make_shared(checker); + smtChecker->activateExperimentalMode(); + smtChecker->toSolver(); + } + + std::vector> res; + uint64_t dep1Index; + uint64_t dep2Index; + for (size_t i = 0; i < dft.getDependencies().size(); ++i) { + dep1Index = dft.getDependencies().at(i); + for (size_t j = i + 1; j < dft.getDependencies().size(); ++j) { + dep2Index = dft.getDependencies().at(j); + 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"); + 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()); + 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; + } + } + } else { + STORM_LOG_DEBUG( + "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()); + break; + } + } + } + return res; + } + + std::vector> + FDEPConflictFinder::getDependencyConflicts(storm::storage::DFT const &dft, + bool useSMT, + uint_fast64_t timeout) { + if (useSMT) { + STORM_LOG_WARN("SMT encoding for rational functions is not supported"); + } + + std::vector> res; + uint64_t dep1Index; + uint64_t dep2Index; + for (size_t i = 0; i < dft.getDependencies().size(); ++i) { + dep1Index = dft.getDependencies().at(i); + 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()); + 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()); + break; + } + } + } + return res; + } + + class FDEPConflictFinder; + + } + } +} \ No newline at end of file diff --git a/src/storm-dft/utility/FDEPConflictFinder.h b/src/storm-dft/utility/FDEPConflictFinder.h new file mode 100644 index 000000000..831bfd248 --- /dev/null +++ b/src/storm-dft/utility/FDEPConflictFinder.h @@ -0,0 +1,29 @@ +#include +#include "storm-dft/storage/dft/DFT.h" +#include "storm-dft/modelchecker/dft/DFTASFChecker.h" + +namespace storm { + namespace dft { + namespace utility { + class FDEPConflictFinder { + public: + /** + * Get a vector of index pairs of FDEPs in the DFT which are conflicting. Two FDEPs are conflicting if + * their simultaneous triggering may cause unresolvable non-deterministic behavior. + * + * @param dft the DFT + * @param useSMT if set, an SMT solver is used to refine the conflict set + * @param timeout timeout for each query in seconds, defaults to 10 seconds + * @return a vector of pairs of indices. The indices in a pair refer to FDEPs which are conflicting + */ + static std::vector> + getDependencyConflicts(storm::storage::DFT const &dft, + bool useSMT = false, uint_fast64_t timeout = 10); + + static std::vector> + getDependencyConflicts(storm::storage::DFT const &dft, + bool useSMT = false, uint_fast64_t timeout = 10); + }; + } + } +} diff --git a/src/test/storm-dft/api/DftSmtTest.cpp b/src/test/storm-dft/api/DftSmtTest.cpp index a7d5f0993..5a7b31095 100644 --- a/src/test/storm-dft/api/DftSmtTest.cpp +++ b/src/test/storm-dft/api/DftSmtTest.cpp @@ -1,3 +1,4 @@ +#include #include "gtest/gtest.h" #include "storm-config.h" @@ -65,11 +66,8 @@ namespace { dft->setDynamicBehaviorInfo(); EXPECT_EQ(dft->getDynamicBehavior(), true_vector); - storm::modelchecker::DFTASFChecker smtChecker(*dft); - smtChecker.convert(); - smtChecker.toSolver(); - EXPECT_TRUE(smtChecker.getDependencyConflicts().empty()); + EXPECT_TRUE(storm::dft::utility::FDEPConflictFinder::getDependencyConflicts(*dft, true).empty()); } TEST(DftSmtTest, FDEPConflictSPARETest) { @@ -80,11 +78,8 @@ namespace { dft->setDynamicBehaviorInfo(); EXPECT_EQ(dft->getDynamicBehavior(), true_vector); - storm::modelchecker::DFTASFChecker smtChecker(*dft); - smtChecker.convert(); - smtChecker.toSolver(); - EXPECT_TRUE(smtChecker.getDependencyConflicts().empty()); + EXPECT_TRUE(storm::dft::utility::FDEPConflictFinder::getDependencyConflicts(*dft, true).empty()); } TEST(DftSmtTest, FDEPConflictSEQTest) { @@ -96,10 +91,7 @@ namespace { dft->setDynamicBehaviorInfo(); EXPECT_EQ(dft->getDynamicBehavior(), expected_dynamic_vector); - storm::modelchecker::DFTASFChecker smtChecker(*dft); - smtChecker.convert(); - smtChecker.toSolver(); - EXPECT_EQ(smtChecker.getDependencyConflicts().size(), uint64_t(3)); + EXPECT_EQ(storm::dft::utility::FDEPConflictFinder::getDependencyConflicts(*dft, true).size(), uint64_t(3)); } } \ No newline at end of file