From f7a03673dd2da17a4f655a6579f651a64be2abb3 Mon Sep 17 00:00:00 2001
From: dgelessus <dgelessus@users.noreply.github.com>
Date: Wed, 24 Jul 2024 12:46:05 +0200
Subject: [PATCH] Weaken some collection types in our code
---
.../src/tlc2/output/OutputCollector.java | 23 ++++++++++---------
.../src/tlc2/tool/TLCTrace.java | 5 ++--
2 files changed, 15 insertions(+), 13 deletions(-)
diff --git a/tlatools/org.lamport.tlatools/src/tlc2/output/OutputCollector.java b/tlatools/org.lamport.tlatools/src/tlc2/output/OutputCollector.java
index 920504f58..55a832033 100644
--- a/tlatools/org.lamport.tlatools/src/tlc2/output/OutputCollector.java
+++ b/tlatools/org.lamport.tlatools/src/tlc2/output/OutputCollector.java
@@ -4,6 +4,7 @@ import java.util.ArrayList;
import java.util.Collections;
import java.util.Date;
import java.util.HashMap;
+import java.util.List;
import java.util.Map;
import tla2sany.semantic.ExprNode;
@@ -16,23 +17,23 @@ import tlc2.tool.TLCStateInfo;
public class OutputCollector {
private static TLCState initialState = null;
- private static ArrayList<TLCStateInfo> trace = null;
- private static ArrayList<Message> allMessages = new ArrayList<Message>();
+ private static List<TLCStateInfo> trace = null;
+ private static List<Message> allMessages = new ArrayList<>();
private static Map<Location, Long> lineCount = new HashMap<>();
private static ModuleNode moduleNode = null;
- private static ArrayList<ExprNode> violatedAssumptions = new ArrayList<>();
+ private static List<ExprNode> violatedAssumptions = new ArrayList<>();
- public static ArrayList<TLCStateInfo> getTrace() {
- return trace;
+ public static List<TLCStateInfo> getTrace() {
+ return Collections.unmodifiableList(trace);
}
- public static void setTrace(ArrayList<TLCStateInfo> trace) {
+ public static void setTrace(List<TLCStateInfo> trace) {
OutputCollector.trace = trace;
}
public static void addStateToTrace(TLCStateInfo tlcStateInfo) {
if (trace == null) {
- trace = new ArrayList<TLCStateInfo>();
+ trace = new ArrayList<>();
}
trace.add(tlcStateInfo);
}
@@ -45,16 +46,16 @@ public class OutputCollector {
return OutputCollector.initialState;
}
- public static ArrayList<Message> getAllMessages() {
- return allMessages;
+ public static List<Message> getAllMessages() {
+ return Collections.unmodifiableList(allMessages);
}
public static void addViolatedAssumption(ExprNode assumption) {
violatedAssumptions.add(assumption);
}
- public static ArrayList<ExprNode> getViolatedAssumptions() {
- return violatedAssumptions;
+ public static List<ExprNode> getViolatedAssumptions() {
+ return Collections.unmodifiableList(violatedAssumptions);
}
public synchronized static void saveMessage(int messageClass,
diff --git a/tlatools/org.lamport.tlatools/src/tlc2/tool/TLCTrace.java b/tlatools/org.lamport.tlatools/src/tlc2/tool/TLCTrace.java
index 4cd1d64e0..98d791a37 100644
--- a/tlatools/org.lamport.tlatools/src/tlc2/tool/TLCTrace.java
+++ b/tlatools/org.lamport.tlatools/src/tlc2/tool/TLCTrace.java
@@ -11,8 +11,8 @@ import java.io.DataOutputStream;
import java.io.File;
import java.io.IOException;
import java.util.ArrayList;
-import java.util.Arrays;
import java.util.HashMap;
+import java.util.List;
import java.util.Map;
import tlc2.output.EC;
@@ -22,6 +22,7 @@ import tlc2.output.StatePrinter;
import tlc2.util.BufferedRandomAccessFile;
import tlc2.util.LongVec;
import tlc2.value.RandomEnumerableValues;
+
import util.FileUtil;
public class TLCTrace {
@@ -343,7 +344,7 @@ public class TLCTrace {
protected synchronized final void printTrace(final TLCState s1, final TLCState s2, final TLCStateInfo[] prefix)
throws IOException, WorkerException {
- ArrayList<TLCStateInfo> trace = new ArrayList<TLCStateInfo>(); // collecting the whole error trace
+ List<TLCStateInfo> trace = new ArrayList<>(); // collecting the whole error trace
if (s1.isInitial()) {
// Do not recreate the potentially expensive error trace - e.g. when the set of
--
GitLab