Add support to show original version of relation using name#0

Signed-off-by: Tianrui Zheng <[email protected]>
hernanponcedeleon · Dec 5, 2024 · 8a10288 · 8a10288
1 parent c23fe23
commit 8a10288
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 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
@@ -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
@@ -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;