Read the arrays of a shared function or record only of a snapshot.

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;

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);

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()) });

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<String, String> getEnv(final RecordValue environment) {
+	private static Map<String, String> getEnv(final RecordValue env) {
 		// Convert record of environment variables to what ProcessBuilder works with.
+		final RecordValue environment = env.snapshot();
 		final Map<String, String> penv = new HashMap<>();
 		for (int i = 0; i < environment.size(); i++) {
 			final UniqueString name = environment.names[i];

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;
   }

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());
 		}

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()) });
 		}