From e7de8cb7f4c008c08959ed0e72df89364612bb7d Mon Sep 17 00:00:00 2001 From: Dmitry Ivanov Date: Mon, 19 Aug 2024 08:30:24 +0200 Subject: [PATCH] Compute left closure --- .../wmm/analysis/NativeRelationAnalysis.java | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/NativeRelationAnalysis.java b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/NativeRelationAnalysis.java index 4e22ad1de9..048e03d4d1 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/NativeRelationAnalysis.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/wmm/analysis/NativeRelationAnalysis.java @@ -1622,15 +1622,15 @@ public Delta visitTransitiveClosure(TransitiveClosure trans) { } private EventGraph computeTransitiveClosure(EventGraph oldOuter, EventGraph inner, boolean isMay) { - EventGraph next; EventGraph outer = new EventGraph(oldOuter); - outer.addAll(inner); - for (EventGraph current = EventGraph.difference(inner, oldOuter); !current.isEmpty(); current = next) { - next = new EventGraph(); - computeComposition(next, current, outer, isMay); - computeComposition(next, outer, current, isMay); - next.removeAll(outer); - outer.addAll(next); + EventGraph update = inner.filter(outer::add); + EventGraph updateComposition = new EventGraph(); + computeComposition(updateComposition, update, oldOuter, isMay); + update.addAll(updateComposition.filter(outer::add)); + while (!update.isEmpty()) { + EventGraph t = new EventGraph(); + computeComposition(t, inner, update, isMay); + update = t.filter(outer::add); } return outer; }