diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java b/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java index 644a4a9ecd..b1ba46f1ff 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/Dartagnan.java @@ -241,7 +241,6 @@ public static File generateExecutionGraphFile(VerificationTask task, ProverEnvir // FR edges only give ordering information which is known if the pair is also in PO // CO edges only give ordering information which is known if the pair is also in PO return generateGraphvizFile(encodingContext, prover.getModel(), 1, (x, y) -> true, - (x, y) -> !x.getThreadModel().getThread().equals(y.getThreadModel().getThread()), (x, y) -> !x.getThreadModel().getThread().equals(y.getThreadModel().getThread()), getOrCreateOutputDirectory() + "/", name, synContext, witnessType.convertToPng()); diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java index 7c2f6eeaa2..b90e5454f2 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/solving/RefinementSolver.java @@ -902,10 +902,10 @@ private static void generateGraphvizFiles(VerificationTask task, ExecutionModelM String fileNameBase = String.format("%s-%d", programName, iterationCount); final SyntacticContextAnalysis emptySynContext = getEmptyInstance(); // File with reason edges only - generateGraphvizFile(model, context, smtModel, iterationCount, edgeFilter, edgeFilter, edgeFilter, directoryName, fileNameBase, + generateGraphvizFile(model, context, smtModel, iterationCount, edgeFilter, edgeFilter, directoryName, fileNameBase, emptySynContext); // File with all edges - generateGraphvizFile(model, context, smtModel, iterationCount, (x, y) -> true, (x, y) -> true, (x, y) -> true, directoryName, + generateGraphvizFile(model, context, smtModel, iterationCount, (x, y) -> true, (x, y) -> true, directoryName, fileNameBase + "-full", emptySynContext); } } \ No newline at end of file diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphviz/ExecutionGraphVisualizer.java b/dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphviz/ExecutionGraphVisualizer.java index 02935456ed..2828480043 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphviz/ExecutionGraphVisualizer.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/witness/graphviz/ExecutionGraphVisualizer.java @@ -45,7 +45,6 @@ public class ExecutionGraphVisualizer { private SyntacticContextAnalysis synContext = getEmptyInstance(); // By default, we do not filter anything private BiPredicate rfFilter = (x, y) -> true; - private BiPredicate frFilter = (x, y) -> true; private BiPredicate coFilter = (x, y) -> true; private final List sortedMemoryObjects = new ArrayList<>(); private List relsToShow = List.of(PO, CO, RF); @@ -70,11 +69,6 @@ public ExecutionGraphVisualizer setReadFromFilter(BiPredicate filter) { - this.frFilter = filter; - return this; - } - public ExecutionGraphVisualizer setCoherenceFilter(BiPredicate filter) { this.coFilter = filter; return this; @@ -147,12 +141,8 @@ private ExecutionGraphVisualizer addRelation(RelationModel rm, String name) { String attributes = String.format("color=%s", colorMap.getColor(name)); graphviz.setEdgeAttributes(attributes); String label = String.format("label=\"%s\"", name); - BiPredicate filter; - if (rm.getRelation().getDefinition().getClass() == ReadFrom.class) { - filter = rfFilter; - } else if (name.equals("fr")) { - filter = frFilter; - } else { filter = getFilter(name); } + BiPredicate filter = rm.getRelation().getDefinition().getClass() == ReadFrom.class ? + rfFilter : getFilter(name); for (RelationModel.EdgeModel edge : rm.getEdgeModels()) { EventModel from = edge.getFrom(); EventModel to = edge.getTo(); @@ -331,7 +321,6 @@ public static File generateGraphvizFile(ExecutionModelNext model, Model smtModel, int iterationCount, BiPredicate rfFilter, - BiPredicate frFilter, BiPredicate coFilter, String directoryName, String fileNameBase, @@ -345,7 +334,6 @@ public static File generateGraphvizFile(ExecutionModelNext model, if (visualizer == null) { visualizer = new ExecutionGraphVisualizer(); } visualizer.setSyntacticContext(synContext) .setReadFromFilter(rfFilter) - .setFromReadFilter(frFilter) .setCoherenceFilter(coFilter) .generateGraphOfExecutionModel(writer, "Iteration " + iterationCount, model, context, smtModel); @@ -365,7 +353,6 @@ public static File generateGraphvizFile(EncodingContext context, Model smtModel, int iterationCount, BiPredicate rfFilter, - BiPredicate frFilter, BiPredicate coFilter, String directoryName, String fileNameBase, @@ -379,7 +366,6 @@ public static File generateGraphvizFile(EncodingContext context, smtModel, iterationCount, rfFilter, - frFilter, coFilter, directoryName, fileNameBase, @@ -393,7 +379,6 @@ public static void generateGraphvizFile(ExecutionModelNext model, Model smtModel, int iterationCount, BiPredicate rfFilter, - BiPredicate frFilter, BiPredicate coFilter, String directoryName, String fileNameBase, @@ -403,7 +388,6 @@ public static void generateGraphvizFile(ExecutionModelNext model, smtModel, iterationCount, rfFilter, - frFilter, coFilter, directoryName, fileNameBase,