Unify trace lookup in TLCExt#Trace by adding Simualtor#getTraceInfo(),

which additionally paves the road to include the action names.

[Refactor][TLC]

tlatools/org.lamport.tlatools/src/tlc2/module/TLCExt.java

@@ -185,7 +185,7 @@ public synchronized static TupleValue getTrace(final TLCState s0) throws IOExcep
 		if (TLCGlobals.simulator != null) {
 			// TODO Somehow load only this implementation in simulation mode => module
 			// overrides for a specific tool mode.
-			return new TupleValue(TLCGlobals.simulator.getTrace().toRecords(s0));
+			return getTrace0(s0, TLCGlobals.simulator.getTraceInfo());
 		}
 		final ModelChecker mc = (ModelChecker) TLCGlobals.mainChecker;
 		final ConcurrentTLCTrace traceFile = mc.trace;

tlatools/org.lamport.tlatools/src/tlc2/tool/SimulationWorker.java

@@ -472,6 +472,16 @@ public final long getTraceCnt() {
 	public final StateVec getTrace() {
 		return stateTrace;
 	}
+
+	public final TLCStateInfo[] getTraceInfo() {
+		final Action[] actions = this.tool.getActions();
+		final TLCStateInfo[] trace = new TLCStateInfo[stateTrace.size()];
+		for (int i = 0; i < stateTrace.size(); i++) {
+			final TLCStateMutSimulation s = (TLCStateMutSimulation) stateTrace.elementAt(i);
+			trace[i] = new TLCStateInfo(s, actions[s.getActionId()]);
+		}
+		return trace;
+	}
 
 	public void start(StateVec initStates) {
 		this.initStates = initStates;

tlatools/org.lamport.tlatools/src/tlc2/tool/Simulator.java

@@ -617,6 +617,16 @@ public final StateVec getTrace() {
 			return workers.get(0).getTrace();
 		}
 	}
+
+	public final TLCStateInfo[] getTraceInfo() {
+		if (Thread.currentThread() instanceof SimulationWorker) {
+			final SimulationWorker w = (SimulationWorker) Thread.currentThread();
+			return w.getTraceInfo();
+		} else {
+			assert numWorkers == 1 && workers.size() == numWorkers;
+			return workers.get(0).getTraceInfo();
+		}
+	}
 
 	public void stop() {
 		for (SimulationWorker worker : workers) {