From 53254a450dc040e7e71a914ddf3a3cc559c4ee29 Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Fri, 23 Oct 2026 18:24:38 -0700 Subject: [PATCH] Read the arrays of a shared function or record only of a snapshot. TLC sorts a FcnRcdValue or RecordValue in place the first time it needs it sorted. An override that reads its arrays while another worker sorts it may miss an element or see one twice. The overrides now read the arrays of a snapshot(), as TLC's own modules do. Part of Github issue #1445 https://github.com/tlaplus/tlaplus/issues/1445 [Bug] Co-authored-by: Claude Opus 5.5 Signed-off-by: Markus Alexander Kuppe --- modules/tlc2/overrides/BagsExt.java | 1 + modules/tlc2/overrides/CBOR.java | 3 ++- modules/tlc2/overrides/Functions.java | 2 +- modules/tlc2/overrides/IOUtils.java | 3 ++- modules/tlc2/overrides/Json.java | 28 +++++++++++++----------- modules/tlc2/overrides/SVG.java | 7 +++--- modules/tlc2/overrides/SequencesExt.java | 2 +- 7 files changed, 26 insertions(+), 20 deletions(-) diff --git a/modules/tlc2/overrides/BagsExt.java b/modules/tlc2/overrides/BagsExt.java index 97d387a..98c4b65 100644 --- a/modules/tlc2/overrides/BagsExt.java +++ b/modules/tlc2/overrides/BagsExt.java @@ -51,6 +51,7 @@ public static Value foldBag(final OpValue op, final Value base, final Value bag) throw new EvalException(EC.TLC_MODULE_ARGUMENT_ERROR, new String[] { "third", "FoldBag", "bag", Values.ppr(bag.toString()) }); } + bfcn = bfcn.snapshot(); final Value[] domain = bfcn.getDomainAsValues(); final Value[] values = bfcn.values; diff --git a/modules/tlc2/overrides/CBOR.java b/modules/tlc2/overrides/CBOR.java index 8eb39c6..c3a4f68 100644 --- a/modules/tlc2/overrides/CBOR.java +++ b/modules/tlc2/overrides/CBOR.java @@ -263,7 +263,8 @@ private void value(final Value v) { } } - private void function(final FcnRcdValue f) { + private void function(final FcnRcdValue fcn) { + final FcnRcdValue f = fcn.snapshot(); final Value form = functionValue(f); if (form instanceof TupleValue) { array(((TupleValue) form).elems); diff --git a/modules/tlc2/overrides/Functions.java b/modules/tlc2/overrides/Functions.java index 7f0f4c4..1d4f5b9 100644 --- a/modules/tlc2/overrides/Functions.java +++ b/modules/tlc2/overrides/Functions.java @@ -69,7 +69,7 @@ public static BoolValue IsInjective(final Value val) { final Value fcn = val.toFcnRcd(); if (fcn instanceof FcnRcdValue) { // Input e.g. [a |-> 1, b |-> 2] or [x \in BOOLEAN |-> x] - return isInjectiveNonDestructive(((FcnRcdValue) fcn).values); + return isInjectiveNonDestructive(((FcnRcdValue) fcn).snapshot().values); } throw new EvalException(EC.TLC_MODULE_ONE_ARGUMENT_ERROR, new String[] { "IsInjective", "function", Values.ppr(val.toString()) }); diff --git a/modules/tlc2/overrides/IOUtils.java b/modules/tlc2/overrides/IOUtils.java index 7439b04..ea2df02 100644 --- a/modules/tlc2/overrides/IOUtils.java +++ b/modules/tlc2/overrides/IOUtils.java @@ -346,8 +346,9 @@ public static Value ioEnvExecTemplate(final Value env, final Value commandTempla return runProcess(getEnv(environment), command); } - private static Map getEnv(final RecordValue environment) { + private static Map getEnv(final RecordValue env) { // Convert record of environment variables to what ProcessBuilder works with. + final RecordValue environment = env.snapshot(); final Map penv = new HashMap<>(); for (int i = 0; i < environment.size(); i++) { final UniqueString name = environment.names[i]; diff --git a/modules/tlc2/overrides/Json.java b/modules/tlc2/overrides/Json.java index 2c32751..fd05492 100644 --- a/modules/tlc2/overrides/Json.java +++ b/modules/tlc2/overrides/Json.java @@ -265,18 +265,19 @@ private static JsonElement getObjectNode(IValue value) throws IOException { * @return the converted {@code JsonElement} */ private static JsonElement getObjectNode(FcnRcdValue value) throws IOException { - if (isValidSequence(value)) { - return getArrayNode(value); + final FcnRcdValue fcn = value.snapshot(); + if (isValidSequence(fcn)) { + return getArrayNode(fcn); } - final Value[] domain = value.getDomainAsValues(); + final Value[] domain = fcn.getDomainAsValues(); JsonObject jsonObject = new JsonObject(); for (int i = 0; i < domain.length; i++) { Value domainValue = domain[i]; if (domainValue instanceof StringValue) { - jsonObject.add(((StringValue) domainValue).val.toString(), getNode(value.values[i])); + jsonObject.add(((StringValue) domainValue).val.toString(), getNode(fcn.values[i])); } else { - jsonObject.add(domainValue.toString(), getNode(value.values[i])); + jsonObject.add(domainValue.toString(), getNode(fcn.values[i])); } } return jsonObject; @@ -289,9 +290,10 @@ private static JsonElement getObjectNode(FcnRcdValue value) throws IOException { * @return the converted {@code JsonElement} */ private static JsonElement getObjectNode(RecordValue value) throws IOException { + final RecordValue rcd = value.snapshot(); JsonObject jsonObject = new JsonObject(); - for (int i = 0; i < value.names.length; i++) { - jsonObject.add(value.names[i].toString(), getNode(value.values[i])); + for (int i = 0; i < rcd.names.length; i++) { + jsonObject.add(rcd.names[i].toString(), getNode(rcd.values[i])); } return jsonObject; } @@ -353,14 +355,14 @@ private static JsonElement getArrayNode(TupleValue value) throws IOException { * @return the converted {@code JsonElement} */ private static JsonElement getArrayNode(FcnRcdValue value) throws IOException { - if (!isValidSequence(value)) { - return getObjectNode(value); + final FcnRcdValue fcn = value.snapshot(); + if (!isValidSequence(fcn)) { + return getObjectNode(fcn); } - value.normalize(); - JsonArray jsonArray = new JsonArray(value.values.length); - for (int i = 0; i < value.values.length; i++) { - jsonArray.add(getNode(value.values[i])); + JsonArray jsonArray = new JsonArray(fcn.values.length); + for (int i = 0; i < fcn.values.length; i++) { + jsonArray.add(getNode(fcn.values[i])); } return jsonArray; } diff --git a/modules/tlc2/overrides/SVG.java b/modules/tlc2/overrides/SVG.java index 8fad665..3d61fe6 100644 --- a/modules/tlc2/overrides/SVG.java +++ b/modules/tlc2/overrides/SVG.java @@ -75,6 +75,7 @@ public static Value SVGElemToString(Value elem) throws Exception { if(attrs == null){ throw new Exception("Was unable to convert element to a record: " + attrsVal.toString()); } + attrs = attrs.snapshot(); String attrStr = ""; for (UniqueString us : attrs.names) { attrStr += " "; @@ -96,13 +97,13 @@ public static Value SVGElemToString(Value elem) throws Exception { children = tv.elems; } else if (childrenVal instanceof RecordValue) { RecordValue rv = (RecordValue) childrenVal.toRcd(); - children = rv.values; + children = rv.snapshot().values; } else if (childrenVal instanceof FcnRcdValue) { FcnRcdValue fcv = (FcnRcdValue) childrenVal.toFcnRcd(); - children = fcv.values; + children = fcv.snapshot().values; } else if (childrenVal instanceof FcnLambdaValue) { FcnRcdValue fcv = (FcnRcdValue) childrenVal.toFcnRcd(); - children = fcv.values; + children = fcv.snapshot().values; } else { throw new Exception("Was unable to convert element to a tuple or (function) record: " + childrenVal.toString()); } diff --git a/modules/tlc2/overrides/SequencesExt.java b/modules/tlc2/overrides/SequencesExt.java index 3ccc28a..5350497 100644 --- a/modules/tlc2/overrides/SequencesExt.java +++ b/modules/tlc2/overrides/SequencesExt.java @@ -193,7 +193,7 @@ public static Value longestCommonPrefix(final Value val) { set.normalize(); final ValueVec elems = set.elems; - if (set.elems.isEmpty()) { + if (elems.isEmpty()) { throw new EvalException(EC.TLC_MODULE_ONE_ARGUMENT_ERROR, new String[] { "LongestCommonPrefix", "non-empty set", Values.ppr(val.toString()) }); }