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

Extended FDEP conflict search by not considering pairs of FDEPs with static behavior

tempestpy_adaptions
Alexander Bork 6 years ago
parent
bec75813b1
commit
aa150fc2e3
1 changed files with 31 additions and 21 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. 52
      src/storm-dft/modelchecker/dft/DFTASFChecker.cpp

52
src/storm-dft/modelchecker/dft/DFTASFChecker.cpp
View File

@ -948,28 +948,38 @@ namespace storm {
dep1Index = dft.getDependencies().at(i);
for (size_t j = i + 1; j < dft.getDependencies().size(); ++j) {
dep2Index = dft.getDependencies().at(j);
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 (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<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());
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());
break;
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<uint64_t, uint64_t>(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<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());
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());
break;
}
}
} else {
STORM_LOG_DEBUG(
"Static behavior: No conflict between " << dft.getElement(dep1Index)->name() << " and "
<< dft.getElement(dep2Index)->name());
break;
}
}
}

Write Preview
Loading…
Cancel
Save