From 965c54b76d01af4f37ac694af78581d5dca6ac15 Mon Sep 17 00:00:00 2001 From: Alexander Bork Date: Fri, 17 May 2019 15:21:15 +0200 Subject: [PATCH] Fixed error that only one FDEP was required to be active for a possible conflict to be detected --- src/storm-dft/modelchecker/dft/DFTASFChecker.cpp | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp index 1583f3867..beecbc805 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp @@ -341,7 +341,7 @@ namespace storm { auto const &trigger = dependency->triggerEvent(); std::vector dependentIndices; for (size_t j = 0; j < dependentEvents.size(); ++j) { - dependentIndices.push_back(dependentEvents[j]->id()); + dependentIndices.push_back(timePointVariables.at(dependentEvents[j]->id())); } constraints.push_back(std::make_shared(dependencyVariables.at(i), dependentIndices)); @@ -617,7 +617,9 @@ namespace storm { STORM_LOG_DEBUG( "Check " << dft.getElement(dep1Index)->name() << " and " << dft.getElement(dep2Index)->name()); andConstr.clear(); - // FDEP2 was triggered before dependent elements have failed + // Both FDEPs were triggered before dependent elements have failed + andConstr.push_back(std::make_shared( + timePointVariables.at(dep1Index), dependencyVariables.at(dep1Index))); andConstr.push_back(std::make_shared( timePointVariables.at(dep2Index), dependencyVariables.at(dep2Index))); // AND FDEP1 is triggered before FDEP2 is resolved @@ -628,9 +630,11 @@ namespace storm { std::shared_ptr betweenConstr1 = std::make_shared(andConstr); andConstr.clear(); - // FDEP1 was triggered before dependent elements have failed + // Both FDEPs were triggered before dependent elements have failed andConstr.push_back(std::make_shared( timePointVariables.at(dep1Index), dependencyVariables.at(dep1Index))); + andConstr.push_back(std::make_shared( + timePointVariables.at(dep2Index), dependencyVariables.at(dep2Index))); // AND FDEP2 is triggered before FDEP1 is resolved andConstr.push_back(std::make_shared( timePointVariables.at(dep2Index), timePointVariables.at(dep1Index)));