From 8a102888c73f21b99de03bd3297630e154615937 Mon Sep 17 00:00:00 2001 From: Tianrui Zheng Date: Thu, 5 Dec 2024 09:28:20 +0100 Subject: [PATCH] Add support to show original version of relation using name#0 Signed-off-by: Tianrui Zheng --- .../dartagnan/verification/model/ExecutionModelManager.java | 6 ++++++ .../witness/graphviz/ExecutionGraphVisualizer.java | 3 ++- 2 files changed, 8 insertions(+), 1 deletion(-) diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/ExecutionModelManager.java b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/ExecutionModelManager.java index 7f34fa342b..b064fd3fb3 100644 --- a/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/ExecutionModelManager.java +++ b/dartagnan/src/main/java/com/dat3m/dartagnan/verification/model/ExecutionModelManager.java @@ -201,6 +201,12 @@ private void extractMemoryLayout() { // In the case of redefinition, we have to find the latest defined one which we care about only. // If there is no redefinition the original one will be returned simply. private Relation getRelationWithName(String name) { + // First check if the original definition is asked. + if (name.endsWith("#0")) { + String originalName = name.substring(0, name.lastIndexOf("#")); + return wmm.getRelation(originalName); + } + int maxId = -1; for (Relation r : wmm.getRelations()) { final int defIndex = r.getNames().stream().filter(s -> s.startsWith(name + "#")) 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 6667e004b0..02935456ed 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 @@ -114,7 +114,8 @@ private RelationModel getRelationModelByName(ExecutionModelNext model, String na for (RelationModel rm : model.getRelationModels()) { Relation r = rm.getRelation(); if (r.hasName(name) - || r.getNames().stream().anyMatch(n -> n.startsWith(name + "#"))) + || r.getNames().stream().anyMatch(n -> n.startsWith(name + "#")) + || (name.endsWith("#0") && r.hasName(name.substring(0, name.lastIndexOf("#"))))) { return rm; } } return null;