ClassCastException due to ummuxed WorkerValue.

Follow up of Github PR #1062 #1062 [Bug][TLC] Signed-off-by: Markus Alexander Kuppe <[email protected]>
tlaplus · Nov 22, 2024 · 7d10d73 · 7d10d73
1 parent 1cf97d4
commit 7d10d73
Showing 1 changed file with 3 additions and 3 deletions.
diff --git a/tlatools/org.lamport.tlatools/src/tlc2/debug/TLCStackFrame.java b/tlatools/org.lamport.tlatools/src/tlc2/debug/TLCStackFrame.java
@@ -302,7 +302,7 @@ public Variable[] getVariables(final int vr) {
 			if (ctxtId == vr) {
 				Context c = this.ctxt;
 				while (c.hasNext()) {
-					Object val = c.getValue();
+					Object val = WorkerValue.mux(c.getValue());
 					if (val instanceof LazyValue) {
 						// unlazy/eval LazyValues
 						val = unlazy((LazyValue) c.getValue());
@@ -317,7 +317,7 @@ public Variable[] getVariables(final int vr) {
 					} else if (val instanceof RuntimeException) {
 						final Variable variable = new Variable();
 						variable.setName(c.getName().getName().toString());
-						variable.setValue(c.getValue().toString());
+						variable.setValue(WorkerValue.mux(c.getValue()).toString());
 						final RuntimeException re = (RuntimeException) val;
 						variable.setType(re.getMessage());
 						vars.add(variable);
@@ -376,7 +376,7 @@ private void getConstants(final List<Variable> vars) {
 					final Set<Entry<OpDefOrDeclNode,Object>> entrySet = e.getValue().entrySet();
 					for (Entry<OpDefOrDeclNode, Object> entry : entrySet) {
 						final OpDefOrDeclNode oddn = entry.getKey();
-						final Object value = entry.getValue();
+						final Object value = WorkerValue.mux(entry.getValue());
 						if (oddn instanceof OpDefNode) {
 							final OpDefNode odn = (OpDefNode) oddn;
 							l.add((DebugTLCVariable) ((Value) value)