[PCover] Update symmetry depedency tracking

p-org · Oct 2, 2023 · f83a2cf · f83a2cf
1 parent 70296bf
commit f83a2cf
Show file tree

Hide file tree

Showing 3 changed files with 38 additions and 27 deletions.
diff --git a/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/machine/Machine.java b/Src/PRuntimes/PSymRuntime/src/main/java/psym/runtime/machine/Machine.java
@@ -25,6 +25,7 @@ public abstract class Machine implements Serializable, Comparable<Machine> {
   @Getter
   private static final int mainMachineId = 2;
   protected static int globalMachineId = mainMachineId;
+  @Getter private static final Map<String, Machine> nameToMachine = new HashMap<>();
   public final Map<
           String,
           SerializableFunction<
@@ -54,6 +55,7 @@ public Machine(String name, int id, State startState, State... states) {
     this.name = name;
     //        this.instanceId = id;
     this.instanceId = globalMachineId++;
+    nameToMachine.put(toString(), this);
 
     this.startState = startState;
     this.sendBuffer = new EventQueue(this);

diff --git a/...Runtime/src/main/java/psym/runtime/scheduler/search/explicit/ExplicitSymmetryTracker.java b/...Runtime/src/main/java/psym/runtime/scheduler/search/explicit/ExplicitSymmetryTracker.java
@@ -70,7 +70,8 @@ public void reset() {
     machineToParent = new HashMap<>();
   }
 
-  public void addMachineSymData(Machine machine, String dataName, Object data) {
+  public void addMachineSymData(Machine machine, Object data) {
+    String dataName = data.getClass().toString();
     Map<String, Object> machineSymmetricData = machineToSymData.get(machine);
     if (machineSymmetricData == null) {
       machineSymmetricData = new HashMap<>();
@@ -89,11 +90,11 @@ public void addMachineSymData(Machine machine, String dataName, Object data) {
     }
   }
 
-  public Object getMachineSymData(Machine machine, String dataName, Object curr) {
-    Object result = curr;
+  public Object getMachineSymData(Machine machine, Object curr) {
+    String dataName = curr.getClass().toString();
     Map<String, Object> machineSymmetricData = machineToSymData.get(machine);
     if (machineSymmetricData != null) {
-      result = machineSymmetricData.get(dataName);
+      Object result = machineSymmetricData.get(dataName);
       if (result != null) {
         return result;
       }

diff --git a/Src/PRuntimes/PSymRuntime/src/main/java/psym/valuesummary/NamedTupleVS.java b/Src/PRuntimes/PSymRuntime/src/main/java/psym/valuesummary/NamedTupleVS.java
@@ -23,17 +23,21 @@ public class NamedTupleVS implements ValueSummary<NamedTupleVS> {
   private void storeSymmetricTuple() {
     if (PSymGlobal.getConfiguration().getSymmetryMode() == SymmetryMode.Full) {
       if (this.names.size() == 2 && !isEmptyVS()) {
-        if (this.names.get(0).equals("symMachine")) {
+        if (this.names.get(0).equals("symtag")) {
           if (PSymGlobal.getSymmetryTracker() instanceof ExplicitSymmetryTracker) {
             ExplicitSymmetryTracker symTracker = (ExplicitSymmetryTracker) PSymGlobal.getSymmetryTracker();
-            List<GuardedValue<?>> machineGVs = ValueSummary.getGuardedValues(this.tuple.getField(0));
+
+            List<GuardedValue<?>> symtagGVs = ValueSummary.getGuardedValues(this.tuple.getField(0));
+            assert (symtagGVs.size() == 1);
             List<GuardedValue<?>> dataGVs = ValueSummary.getGuardedValues(this.tuple.getField(1));
-            assert (machineGVs.size() == 1);
             assert (dataGVs.size() == 1);
-            if (machineGVs.get(0).getValue() != null) {
-              assert (machineGVs.get(0).getValue() instanceof Machine);
-              symTracker.addMachineSymData(
-                      (Machine) machineGVs.get(0).getValue(), this.names.get(1), dataGVs.get(0).getValue());
+
+            if (symtagGVs.get(0).getValue() != null) {
+              String symTag = symtagGVs.get(0).getValue().toString();
+              Machine machineTag = Machine.getNameToMachine().get(symTag);
+              if (machineTag != null) {
+                symTracker.addMachineSymData(machineTag, dataGVs.get(0).getValue());
+              }
             }
           }
         }
@@ -89,27 +93,31 @@ public NamedTupleVS getCopy() {
 
   public NamedTupleVS swap(Map<Machine, Machine> mapping) {
     if (this.names.size() == 2 && !isEmptyVS()) {
-        if (this.names.get(0).equals("symMachine")) {
+        if (this.names.get(0).equals("symtag")) {
           if (PSymGlobal.getSymmetryTracker() instanceof ExplicitSymmetryTracker) {
             ExplicitSymmetryTracker symTracker = (ExplicitSymmetryTracker) PSymGlobal.getSymmetryTracker();
 
-            List<GuardedValue<?>> machineGVs = ValueSummary.getGuardedValues(this.tuple.getField(0));
+            List<GuardedValue<?>> symtagGVs = ValueSummary.getGuardedValues(this.tuple.getField(0));
+            assert (symtagGVs.size() == 1);
             List<GuardedValue<?>> dataGVs = ValueSummary.getGuardedValues(this.tuple.getField(1));
-            assert (machineGVs.size() == 1);
             assert (dataGVs.size() == 1);
-            if (machineGVs.get(0).getValue() != null) {
-              assert (machineGVs.get(0).getValue() instanceof Machine);
-
-              Machine origMachine = (Machine) machineGVs.get(0).getValue();
-              Machine newMachine = mapping.get(origMachine);
-              if (newMachine != null) {
-                Object origValue = dataGVs.get(0).getValue();
-                Object newValue = symTracker.getMachineSymData(newMachine, this.names.get(1), origValue);
-                Guard guard = machineGVs.get(0).getGuard();
-
-                return new NamedTupleVS(
-                        new ArrayList<>(this.names),
-                        new TupleVS(new PrimitiveVS<>(newMachine, guard), new PrimitiveVS<>(newValue, guard)));
+
+            if (symtagGVs.get(0).getValue() != null) {
+              String symTag = symtagGVs.get(0).getValue().toString();
+              Machine machineTag = Machine.getNameToMachine().get(symTag);
+              if (machineTag != null) {
+                Machine machineTagSwapped = mapping.get(machineTag);
+                if (machineTagSwapped != null) {
+                  Object origValue = dataGVs.get(0).getValue();
+                  Object newValue =
+                      symTracker.getMachineSymData(machineTagSwapped, origValue);
+                  Guard guard = symtagGVs.get(0).getGuard();
+
+                  return new NamedTupleVS(
+                      new ArrayList<>(this.names),
+                      new TupleVS(
+                          new PrimitiveVS<>(machineTagSwapped.toString(), guard), new PrimitiveVS<>(newValue, guard)));
+                }
               }
             }
             return this;