Include TLCState#workerId and TLCState#uid in TLCState#deepCopy().

See related commit e1ae0b9 [Refactor][TLC]
tlaplus · Feb 22, 2021 · 45d8275 · 45d8275
1 parent 0a517b6
commit 45d8275
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/tlatools/org.lamport.tlatools/src/tlc2/tool/TLCState.java b/tlatools/org.lamport.tlatools/src/tlc2/tool/TLCState.java
@@ -86,6 +86,8 @@ public IValue lookup(String var) {
 
   protected TLCState deepCopy(TLCState copy) {
 	  copy.level = this.level;
+	  copy.workerId = this.workerId;
+	  copy.uid = this.uid;
 	  return copy;
   }