From e06bb99cc46ea5637d88d9bd9cbbc8ba60118f74 Mon Sep 17 00:00:00 2001
From: Alexander Bork <alexander.bork@rwth-aachen.de>
Date: Wed, 22 May 2019 11:02:47 +0200
Subject: [PATCH] Changed DEP conflict constraint to avoid double check

---
 .../modelchecker/dft/DFTASFChecker.cpp        | 22 +++++++++----------
 1 file changed, 11 insertions(+), 11 deletions(-)

diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp
index 85326c8b2..a5633bb56 100644
--- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp
+++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp
@@ -617,11 +617,6 @@ namespace storm {
             STORM_LOG_DEBUG(
                     "Check " << dft.getElement(dep1Index)->name() << " and " << dft.getElement(dep2Index)->name());
             andConstr.clear();
-            // Both FDEPs were triggered before dependent elements have failed
-            andConstr.push_back(std::make_shared<IsLess>(
-                    timePointVariables.at(dep1Index), dependencyVariables.at(dep1Index)));
-            andConstr.push_back(std::make_shared<IsLess>(
-                    timePointVariables.at(dep2Index), dependencyVariables.at(dep2Index)));
             // AND FDEP1 is triggered before FDEP2 is resolved
             andConstr.push_back(std::make_shared<IsGreaterEqual>(
                     timePointVariables.at(dep1Index), timePointVariables.at(dep2Index)));
@@ -630,11 +625,6 @@ namespace storm {
             std::shared_ptr<SmtConstraint> betweenConstr1 = std::make_shared<And>(andConstr);
 
             andConstr.clear();
-            // Both FDEPs were triggered before dependent elements have failed
-            andConstr.push_back(std::make_shared<IsLess>(
-                    timePointVariables.at(dep1Index), dependencyVariables.at(dep1Index)));
-            andConstr.push_back(std::make_shared<IsLess>(
-                    timePointVariables.at(dep2Index), dependencyVariables.at(dep2Index)));
             // AND FDEP2 is triggered before FDEP1 is resolved
             andConstr.push_back(std::make_shared<IsGreaterEqual>(
                     timePointVariables.at(dep2Index), timePointVariables.at(dep1Index)));
@@ -646,7 +636,17 @@ namespace storm {
             // Either one of the above constraints holds
             orConstr.push_back(betweenConstr1);
             orConstr.push_back(betweenConstr2);
-            std::shared_ptr<SmtConstraint> checkConstr = std::make_shared<Or>(orConstr);
+
+            // Both FDEPs were triggered before dependent elements have failed
+            andConstr.clear();
+            andConstr.push_back(std::make_shared<IsLess>(
+                    timePointVariables.at(dep1Index), dependencyVariables.at(dep1Index)));
+            andConstr.push_back(std::make_shared<IsLess>(
+                    timePointVariables.at(dep2Index), dependencyVariables.at(dep2Index)));
+            andConstr.push_back(std::make_shared<Or>(orConstr));
+
+            std::shared_ptr<SmtConstraint> checkConstr = std::make_shared<And>(andConstr);
+
             std::shared_ptr<storm::expressions::ExpressionManager> manager = solver->getManager().getSharedPointer();
             solver->push();
             solver->add(checkConstr->toExpression(varNames, manager));