From 1767c40f2d0d0a0b0123c806159bfe269bd87025 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 22 Oct 2019 18:13:08 +0200 Subject: [PATCH] Refactored FDEPConflictFinder --- src/storm-dft-cli/storm-dft.cpp | 4 +- src/storm-dft/utility/FDEPConflictFinder.cpp | 58 +++++++------------- src/storm-dft/utility/FDEPConflictFinder.h | 22 ++++---- src/test/storm-dft/api/DftSmtTest.cpp | 6 +- 4 files changed, 34 insertions(+), 56 deletions(-) diff --git a/src/storm-dft-cli/storm-dft.cpp b/src/storm-dft-cli/storm-dft.cpp index f14d3e6ca..185908d61 100644 --- a/src/storm-dft-cli/storm-dft.cpp +++ b/src/storm-dft-cli/storm-dft.cpp @@ -112,8 +112,8 @@ void processOptions() { "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, useSMT, - solverTimeout); + // 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" << std::endl); diff --git a/src/storm-dft/utility/FDEPConflictFinder.cpp b/src/storm-dft/utility/FDEPConflictFinder.cpp index 53f63ae4b..eb4447ffb 100644 --- a/src/storm-dft/utility/FDEPConflictFinder.cpp +++ b/src/storm-dft/utility/FDEPConflictFinder.cpp @@ -4,10 +4,9 @@ namespace storm { namespace dft { namespace utility { - std::vector> - FDEPConflictFinder::getDependencyConflicts(storm::storage::DFT const &dft, - bool useSMT, - uint_fast64_t timeout) { + template<> + std::vector> FDEPConflictFinder::getDependencyConflicts(storm::storage::DFT const& dft, bool useSMT, + uint_fast64_t timeout) { std::shared_ptr smtChecker = nullptr; if (useSMT) { @@ -25,46 +24,30 @@ namespace storm { 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"); + 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()); + 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()); + 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()); + 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()); + 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()); + STORM_LOG_DEBUG("Static behavior: No conflict between " << dft.getElement(dep1Index)->name() << " and " << dft.getElement(dep2Index)->name()); break; } } @@ -72,10 +55,9 @@ namespace storm { return res; } - std::vector> - FDEPConflictFinder::getDependencyConflicts(storm::storage::DFT const &dft, - bool useSMT, - uint_fast64_t timeout) { + template<> + 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"); } @@ -88,15 +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_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()); + STORM_LOG_DEBUG("Static behavior: No conflict between " << dft.getElement(dep1Index)->name() << " and " << dft.getElement(dep2Index)->name()); break; } } @@ -104,8 +81,11 @@ namespace storm { return res; } - class FDEPConflictFinder; + template + class FDEPConflictFinder; + template + class FDEPConflictFinder; } } } \ No newline at end of file diff --git a/src/storm-dft/utility/FDEPConflictFinder.h b/src/storm-dft/utility/FDEPConflictFinder.h index 831bfd248..e783f9000 100644 --- a/src/storm-dft/utility/FDEPConflictFinder.h +++ b/src/storm-dft/utility/FDEPConflictFinder.h @@ -5,24 +5,22 @@ namespace storm { namespace dft { namespace utility { + + template 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 + * @param dft The DFT. + * @param useSMT If set, an SMT solver is used to refine the conflict set. + * @param timeout Timeout for each SMT 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); + 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 f23a433c9..c367a8c52 100644 --- a/src/test/storm-dft/api/DftSmtTest.cpp +++ b/src/test/storm-dft/api/DftSmtTest.cpp @@ -66,7 +66,7 @@ namespace { dft->setDynamicBehaviorInfo(); EXPECT_EQ(dft->getDynamicBehavior(), true_vector); - EXPECT_TRUE(storm::dft::utility::FDEPConflictFinder::getDependencyConflicts(*dft, true).empty()); + EXPECT_TRUE(storm::dft::utility::FDEPConflictFinder::getDependencyConflicts(*dft, true).empty()); } TEST(DftSmtTest, FDEPConflictSPARETest) { @@ -78,7 +78,7 @@ namespace { dft->setDynamicBehaviorInfo(); EXPECT_EQ(dft->getDynamicBehavior(), true_vector); - EXPECT_TRUE(storm::dft::utility::FDEPConflictFinder::getDependencyConflicts(*dft, true).empty()); + EXPECT_TRUE(storm::dft::utility::FDEPConflictFinder::getDependencyConflicts(*dft, true).empty()); } TEST(DftSmtTest, FDEPConflictSEQTest) { @@ -91,6 +91,6 @@ namespace { dft->setDynamicBehaviorInfo(); EXPECT_EQ(dft->getDynamicBehavior(), expected_dynamic_vector); - EXPECT_EQ(storm::dft::utility::FDEPConflictFinder::getDependencyConflicts(*dft, true).size(), uint64_t(3)); + EXPECT_EQ(storm::dft::utility::FDEPConflictFinder::getDependencyConflicts(*dft, true).size(), uint64_t(3)); } } \ No newline at end of file