sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Refactored FDEPConflictFinder

main
Matthias Volk 6 years ago
parent
fb81571da5
commit
1767c40f2d
4 changed files with 34 additions and 56 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 4
      src/storm-dft-cli/storm-dft.cpp
  2. 58
      src/storm-dft/utility/FDEPConflictFinder.cpp
  3. 22
      src/storm-dft/utility/FDEPConflictFinder.h
  4. 6
      src/test/storm-dft/api/DftSmtTest.cpp

4
src/storm-dft-cli/storm-dft.cpp
View File

@ -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<ValueType>::getDependencyConflicts(*dft, useSMT, solverTimeout);
if (preResults.fdepConflicts.empty()) {
STORM_LOG_DEBUG("No FDEP conflicts found" << std::endl);

58
src/storm-dft/utility/FDEPConflictFinder.cpp
View File

@ -4,10 +4,9 @@ namespace storm {
namespace dft {
namespace utility {
std::vector<std::pair<uint64_t, uint64_t>>
FDEPConflictFinder::getDependencyConflicts(storm::storage::DFT<double> const &dft,
bool useSMT,
uint_fast64_t timeout) {
template<>
std::vector<std::pair<uint64_t, uint64_t>> FDEPConflictFinder<double>::getDependencyConflicts(storm::storage::DFT<double> const& dft, bool useSMT,
uint_fast64_t timeout) {
std::shared_ptr<storm::modelchecker::DFTASFChecker> 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<uint64_t, uint64_t>(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<uint64_t, uint64_t>(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<uint64_t, uint64_t>(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<uint64_t, uint64_t>(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<std::pair<uint64_t, uint64_t>>
FDEPConflictFinder::getDependencyConflicts(storm::storage::DFT<storm::RationalFunction> const &dft,
bool useSMT,
uint_fast64_t timeout) {
template<>
std::vector<std::pair<uint64_t, uint64_t>> FDEPConflictFinder<storm::RationalFunction>::getDependencyConflicts(storm::storage::DFT<storm::RationalFunction> 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<uint64_t, uint64_t>(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<double>;
template
class FDEPConflictFinder<storm::RationalFunction>;
}
}
}

22
src/storm-dft/utility/FDEPConflictFinder.h
View File

@ -5,24 +5,22 @@
namespace storm {
namespace dft {
namespace utility {
template<typename ValueType>
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<std::pair<uint64_t, uint64_t>>
getDependencyConflicts(storm::storage::DFT<double> const &dft,
bool useSMT = false, uint_fast64_t timeout = 10);
static std::vector<std::pair<uint64_t, uint64_t>>
getDependencyConflicts(storm::storage::DFT<storm::RationalFunction> const &dft,
bool useSMT = false, uint_fast64_t timeout = 10);
static std::vector<std::pair<uint64_t, uint64_t>> getDependencyConflicts(storm::storage::DFT<ValueType> const& dft, bool useSMT = false,
uint_fast64_t timeout = 10);
};
}
}

6
src/test/storm-dft/api/DftSmtTest.cpp
View File

@ -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<double>::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<double>::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<double>::getDependencyConflicts(*dft, true).size(), uint64_t(3));
}
}
Write Preview
Loading…
Cancel
Save