Simulator.java

// Copyright (c) 2003 Compaq Corporation.  All rights reserved.
// Portions Copyright (c) 2003 Microsoft Corporation.  All rights reserved.
// Last modified on Mon 30 Apr 2007 at 15:29:56 PST by lamport
//      modified on Thu Jan 10 11:22:26 PST 2002 by yuanyu

package tlc2.tool;

import java.io.IOException;
import java.math.BigDecimal;
import java.math.RoundingMode;
import java.util.ArrayList;
import java.util.HashMap;
import java.util.HashSet;
import java.util.List;
import java.util.Map;
import java.util.Map.Entry;
import java.util.Set;
import java.util.TimerTask;
import java.util.concurrent.BlockingQueue;
import java.util.concurrent.LinkedBlockingQueue;
import java.util.concurrent.atomic.AtomicLong;
import java.util.concurrent.atomic.LongAdder;
import java.util.stream.Collectors;

import tla2sany.semantic.ExprNode;
import tlc2.TLCGlobals;
import tlc2.output.EC;
import tlc2.output.MP;
import tlc2.output.StatePrinter;
import tlc2.tool.SimulationWorker.SimulationWorkerError;
import tlc2.tool.SimulationWorker.SimulationWorkerResult;
import tlc2.tool.coverage.CostModelCreator;
import tlc2.tool.impl.FastTool;
import tlc2.tool.impl.Tool;
import tlc2.tool.liveness.ILiveCheck;
import tlc2.tool.liveness.LiveCheck;
import tlc2.tool.liveness.LiveCheck1;
import tlc2.tool.liveness.LiveException;
import tlc2.tool.liveness.NoOpLiveCheck;
import tlc2.util.DotActionWriter;
import tlc2.util.RandomGenerator;
import tlc2.util.statistics.DummyBucketStatistics;
import tlc2.value.IValue;
import util.Assert.TLCRuntimeException;
import util.FileUtil;
import util.FilenameToStream;

public class Simulator {

	public static boolean EXPERIMENTAL_LIVENESS_SIMULATION = Boolean
			.getBoolean(Simulator.class.getName() + ".experimentalLiveness");
	public static boolean actionStats = Boolean.getBoolean(tlc2.tool.Simulator.class.getName() + ".actionStats");

	/* Constructors */

	// SZ Feb 20, 2009: added the possibility to pass the SpecObject
	public Simulator(String specFile, String configFile, String traceFile, boolean deadlock, int traceDepth,
			long traceNum, RandomGenerator rng, long seed, FilenameToStream resolver,
			int numWorkers) throws IOException {
		this(new FastTool(extracted(specFile), configFile, resolver, Tool.Mode.Simulation), "", traceFile, deadlock,
				traceDepth, traceNum, rng, seed, resolver, numWorkers);
	}

	private static String extracted(String specFile) {
		int lastSep = specFile.lastIndexOf(FileUtil.separatorChar);
		return specFile.substring(lastSep + 1);
	}

	public Simulator(ITool tool, String metadir, String traceFile, boolean deadlock, int traceDepth,
				long traceNum, RandomGenerator rng, long seed, FilenameToStream resolver,
				int numWorkers) throws IOException {
		this.tool = tool;

		this.checkDeadlock = deadlock && tool.getModelConfig().getCheckDeadlock();
		this.checkLiveness = !this.tool.livenessIsTrue();
		this.invariants = this.tool.getInvariants();
		if (traceDepth != -1) {
			// this.actionTrace = new Action[traceDepth]; // SZ: never read
			// locally
			this.traceDepth = traceDepth;
		} else {
			// this.actionTrace = new Action[0]; // SZ: never read locally
			this.traceDepth = Integer.MAX_VALUE;
		}
		this.traceFile = traceFile;
		this.traceNum = traceNum;
		this.rng = rng;
		this.seed = seed;
		this.aril = 0;
		// Initialization for liveness checking
		if (this.checkLiveness) {
			if (EXPERIMENTAL_LIVENESS_SIMULATION) {
				final String tmpDir = System.getProperty("java.io.tmpdir");
				liveCheck = new LiveCheck(this.tool, tmpDir, new DummyBucketStatistics());
			} else {
				liveCheck = new LiveCheck1(this.tool);
			}
		} else {
			liveCheck = new NoOpLiveCheck(tool, metadir);
		}

		this.numWorkers = numWorkers;
		this.workers = new ArrayList<>(numWorkers);
		for (int i = 0; i < this.numWorkers; i++) {
			this.workers.add(new SimulationWorker(i, this.tool, this.workerResultQueue, this.rng.nextLong(),
					this.traceDepth, this.traceNum, this.checkDeadlock, this.traceFile, this.liveCheck,
					this.numOfGenStates, this.numOfGenTraces, this.welfordM2AndMean));
		}
		
		if (TLCGlobals.isCoverageEnabled()) {
        	CostModelCreator.create(this.tool);
        }
		
		//TODO Eventually derive Simulator from AbstractChecker.
		AbstractChecker.scheduleTermination(new TimerTask() {
			@Override
			public void run() {
				Simulator.this.stop();
			}
		});
	}

	/* Fields */
	private final ILiveCheck liveCheck;
	private final ITool tool;
	private final Action[] invariants; // the invariants to be checked
	private final boolean checkDeadlock; // check deadlock?
	private final boolean checkLiveness; // check liveness?

	// The total number of states/traces generated by all workers. May be written to
	// concurrently, so we use a LongAdder to reduce potential contention.
	private final LongAdder numOfGenStates = new LongAdder();
	private final LongAdder numOfGenTraces = new LongAdder();
	private final AtomicLong welfordM2AndMean = new AtomicLong();

	// private Action[] actionTrace; // SZ: never read locally
	private final String traceFile;

	// The maximum length of a simulated trace.
	private final int traceDepth;

	// The maximum number of total traces to generate.
	private final long traceNum;

	// The number of worker threads to use for simulation.
	private int numWorkers = 1;

	private final RandomGenerator rng;
	private final long seed;
	private long aril;

	// Each simulation worker pushes their results onto this shared queue.
	private final BlockingQueue<SimulationWorkerResult> workerResultQueue = new LinkedBlockingQueue<>();
	
    /**
     * Timestamp of when simulation started.
     */
	private final long startTime = System.currentTimeMillis();
	
	private final List<SimulationWorker> workers;
		 
	 /**
	 * Returns whether a given error code is considered "continuable". That is, if
	 * any worker returns this error, should we consider continuing to run the
	 * simulator. These errors are considered "fatal" since they most likely
	 * indicate an error in the way the spec is written.
	 */
	private boolean isNonContinuableError(int ec) {
		return ec == EC.TLC_INVARIANT_EVALUATION_FAILED || 
			   ec == EC.TLC_ACTION_PROPERTY_EVALUATION_FAILED ||
			   ec == EC.TLC_STATE_NOT_COMPLETELY_SPECIFIED_NEXT;
	}
	
	/**
	 * Shut down all of the given workers and make sure they have stopped.
	 */
	private void shutdownAndJoinWorkers(final List<SimulationWorker> workers) throws InterruptedException {
		for (SimulationWorker worker : workers) {
			worker.interrupt();
			worker.join();
		}
	}

	/*
	 * This method does random simulation on a TLA+ spec.
	 * 
	 * It runs until en error is encountered or we have generated the maximum number of traces.
	 * 
   * @return an error code, or <code>EC.NO_ERROR</code> on success
	 */
	public int simulate() throws Exception {
		final int res = this.tool.checkAssumptions();
		if (res != EC.NO_ERROR) {
			return res;
		}
		
		TLCState curState = null;

		// The init states are calculated only ever once and never change
		// in the loops below. Ideally the variable would be final.
		StateVec initStates = this.tool.getInitStates();

		//
		// Compute the initial states.
		//
		try {


			// This counter should always be initialized at zero.
			assert (this.numOfGenStates.longValue() == 0);
			this.numOfGenStates.add(initStates.size());
			
			MP.printMessage(EC.TLC_COMPUTING_INIT_PROGRESS, this.numOfGenStates.toString());

			// Check all initial states for validity.
			for (int i = 0; i < initStates.size(); i++) {
				curState = initStates.elementAt(i);
				if (this.tool.isGoodState(curState)) {
					for (int j = 0; j < this.invariants.length; j++) {
						if (!this.tool.isValid(this.invariants[j], curState)) {
							// We get here because of invariant violation.
							return MP.printError(EC.TLC_INVARIANT_VIOLATED_INITIAL,
									new String[] { this.tool.getInvNames()[j], curState.toString() });
						}
					}
				} else {
					return MP.printError(EC.TLC_STATE_NOT_COMPLETELY_SPECIFIED_INITIAL, curState.toString());
				}
			}
		} catch (Exception e) {
			final int errorCode;
			if (curState != null) {
				errorCode = MP.printError(EC.TLC_INITIAL_STATE,
						new String[] { (e.getMessage() == null) ? e.toString() : e.getMessage(), curState.toString() });
			} else {
				errorCode = MP.printError(EC.GENERAL, e); // LL changed call 7 April 2012
			}

			this.printSummary();
			return errorCode;
		}

		if (this.numOfGenStates.longValue() == 0) {
			return MP.printError(EC.TLC_NO_STATES_SATISFYING_INIT);
		}

		// It appears deepNormalize brings the states into a canonical form to
		// speed up equality checks.
		initStates.deepNormalize();

		//
		// Start progress report thread.
		//
		final ProgressReport report = new ProgressReport();
		report.start();

		//
		// Start simulating.
		//
		this.aril = rng.getAril();
		
		// Start up multiple simulation worker threads, each with their own unique seed.
		final Set<Integer> runningWorkers = new HashSet<>();
		for (int i = 0; i < this.workers.size(); i++) {
			SimulationWorker worker = workers.get(i);
			worker.start(initStates);
			runningWorkers.add(i);
		}

		int errorCode = EC.NO_ERROR;
		
		// Continuously consume results from all worker threads.
		while (true) {
			final SimulationWorkerResult result = workerResultQueue.take();

			// If the result is an error, print it.
			if (result.isError()) {
				SimulationWorkerError error = result.error();
				
				// We assume that if a worker threw an unexpected exception, there is a bug
				// somewhere, so we print out the exception and terminate. In the case of a
				// liveness error, which is reported as an exception, we also terminate.
				if (error.exception != null) {
					if (error.exception instanceof LiveException) {
						// In case of a liveness error, there is no need to print out
						// the behavior since the liveness checker should take care of that itself.
						this.printSummary();
						errorCode = ((LiveException)error.exception).errorCode;
					} else if (error.exception instanceof TLCRuntimeException) {
						final TLCRuntimeException exception = (TLCRuntimeException)error.exception;
						printBehavior(exception, error.state, error.stateTrace);
						errorCode = exception.errorCode;
					} else {
						printBehavior(EC.GENERAL, new String[] { MP.ECGeneralMsg("", error.exception) }, error.state,
								error.stateTrace);
						errorCode = EC.GENERAL;
					}
					break;
				}
				
				// Print the trace for all other errors.
				printBehavior(error);
				
				// For certain, "fatal" errors, we shut down all workers and terminate,
				// regardless of the "continue" parameter, since these errors likely indicate a bug in the spec.
				if (isNonContinuableError(error.errorCode)) {
					errorCode = error.errorCode;
					break;
				}
				
				// If the 'continue' option is false, then we always terminate on the
				// first error, shutting down all workers. Otherwise, we continue receiving
				// results from the worker threads.
				if (!TLCGlobals.continuation) {
					errorCode = error.errorCode;
					break;
				}

				if (errorCode == EC.NO_ERROR)
				{
					errorCode = EC.GENERAL;
				}
			}
			// If the result is OK, this indicates that the worker has terminated, so we
			// make note of this. If all of the workers have terminated, there is no need to
			// continue waiting for results, so we should terminate.
			else {
				runningWorkers.remove(result.workerId());
				if(runningWorkers.isEmpty()) {
					break;
				}
			}
		}
		
		// Shut down all workers.
		this.shutdownAndJoinWorkers(workers);
		
		if (errorCode == EC.NO_ERROR) {
			// see tlc2.tool.Worker.doPostCheckAssumption()
			final ExprNode sn = (ExprNode) this.tool.getPostConditionSpec();
			try {
				if (sn != null && !this.tool.isValid(sn)) {
					MP.printError(EC.TLC_ASSUMPTION_FALSE, sn.toString());
				}
			} catch (Exception e) {
				// tool.isValid(sn) failed to evaluate...
				MP.printError(EC.TLC_ASSUMPTION_EVALUATION_ERROR, new String[] { sn.toString(), e.getMessage() });
			}
		}

		// Do a final progress report.
		report.isRunning = false;
		synchronized (report) {
			report.notify();
		}
		// Wait for the progress reporter thread to finish.
		report.join();

		return errorCode;
	}

	private final void printBehavior(final TLCRuntimeException exception, final TLCState state, final StateVec stateTrace) {
		MP.printTLCRuntimeException(exception);
		printBehavior(state, stateTrace);
	}

	private final void printBehavior(SimulationWorkerError error) {
		printBehavior(error.errorCode, error.parameters, error.state, error.stateTrace);
	}

	/**
	 * Prints out the simulation behavior, in case of an error. (unless we're at
	 * maximum depth, in which case don't!)
	 */
	private final void printBehavior(final int errorCode, final String[] parameters, final TLCState state, final StateVec stateTrace) {
		MP.printError(errorCode, parameters);
		printBehavior(state, stateTrace);
		this.printSummary();
	}
	
	private final void printBehavior(final TLCState state, final StateVec stateTrace) {
		if (this.traceDepth == Long.MAX_VALUE) {
			MP.printMessage(EC.TLC_ERROR_STATE);
			StatePrinter.printStandaloneErrorState(state);
		} else {
			if (!stateTrace.isLastElement(state)) {
				// MAK 09/24/2019: this method is called with state being the stateTrace's
				// last element or not.
				stateTrace.addElement(state);
			}
			
			MP.printError(EC.TLC_BEHAVIOR_UP_TO_THIS_POINT);
			// MAK 09/24/2019: For space reasons, TLCState does not store the state's action.
			// This is why the loop below creates TLCStateInfo instances out of the pair cur
			// -> last to print the action's name as part of the error trace. This is
			// especially useful for Error-Trace Explorer in the Toolbox.
			TLCState lastState = null;
			TLCStateInfo sinfo;
			int omitted = 0;
			for (int i = 0; i < stateTrace.size(); i++) {
				final TLCStateMutSimulation curState = (TLCStateMutSimulation) stateTrace.elementAt(i);
				// Last state's successor is itself.
				final TLCState sucState = stateTrace.elementAt(Math.min(i + 1, stateTrace.size() - 1));
				if (lastState != null) {
					// Contrary to BFS/ModelChecker, simulation remembers the action (its id) during
					// trace exploration to print the error-trace without re-evaluating the
					// next-state relation for lastStates -> cusState (tool.getState(curState,
					// lastState)) to determine the action.  This would fail for specs whose next-state
					// relation is probabilistic (ie. TLC!RandomElement or Randomization.tla). In other
					// words, tool.getState(curState,lastState) would return for some pairs of states.
					sinfo = new TLCStateInfo(curState, tool.getActions()[curState.getActionId()].getLocation());
				} else {
					sinfo = new TLCStateInfo(curState, "<Initial predicate>");
					StatePrinter.printInvariantViolationStateTraceState(tool.evalAlias(sinfo, sucState), lastState, curState.getLevel());
					lastState = curState;
					continue;
				}
				
				// MAK 09/25/2019: It is possible for
				// tlc2.tool.SimulationWorker.simulateRandomTrace() to produce traces with
				// *non-terminal* stuttering steps, i.e. it might produce traces such
				// as s0,s1,s1,s2,s3,s3,s3,...sN* (where sN* represents an infinite suffix of
				// "terminal" stuttering steps). In other words, it produces traces s.t.
				// a trace has finite (sub-)sequence of stuttering steps.
				// The reason is that simulateRandomTrace, with non-zero probability, selects
				// a stuttering step as the current state's successor. Guarding against it
				// would require to fingerprint states (i.e. check equality) for each selected
				// successor state (which is considered too expensive).
				// A trace with finite stuttering can be reduced to a shorter - hence
				// better readable - trace with only infinite stuttering at the end. This
				// takes mostly care of the confusing Toolbox behavior where a trace with
				// finite stuttering is silently reduced by breadth-first-search when trace
				// expressions are evaluated (see https://github.com/tlaplus/tlaplus/issues/400#issuecomment-650418597).
				if (TLCGlobals.printDiffsOnly && curState.fingerPrint() == lastState.fingerPrint()) {
					omitted++;
				} else {
					// print the state's actual level and not a monotonically increasing state
					// number => Numbering will have gaps with difftrace.
					StatePrinter.printInvariantViolationStateTraceState(tool.evalAlias(sinfo, sucState), lastState, curState.getLevel());
				}
				lastState = curState;
			}
			if (omitted > 0) {
				assert TLCGlobals.printDiffsOnly;
				MP.printMessage(EC.GENERAL, String.format(
						"difftrace requested: Shortened behavior by omitting finite stuttering (%s states), which is an artifact of simulation mode.\n",
						omitted));
			}
		}
	}

	public IValue getLocalValue(int idx) {
		for (SimulationWorker w : workers) {
			return w.getLocalValue(idx);
		}
		return null;
	}

	public void setAllValues(int idx, IValue val) {
		for (SimulationWorker w : workers) {
			w.setLocalValue(idx, val);
		}
	}

	public List<IValue> getAllValues(int idx) {
		return workers.stream().map(w -> w.getLocalValue(idx)).collect(Collectors.toList());
	}

	/**
	 * Prints the summary
	 */
	private final void printSummary() {
		this.reportCoverage();

		/*
		 * This allows the toolbox to easily display the last set of state space
		 * statistics by putting them in the same form as all other progress statistics.
		 */
		if (TLCGlobals.tool) {
			MP.printMessage(EC.TLC_PROGRESS_SIMU, String.valueOf(numOfGenStates.longValue()));
		}

		MP.printMessage(EC.TLC_STATS_SIMU, new String[] { String.valueOf(numOfGenStates.longValue()),
				String.valueOf(this.seed), String.valueOf(this.aril) });
	}

	/**
	 * Reports coverage
	 */
	public final void reportCoverage() {
		if (TLCGlobals.isCoverageEnabled()) {
            CostModelCreator.report(this.tool, this.startTime );
		}
	}

	public final ITool getTool() {
	    return this.tool;	
	}
	
	/**
	 * Reports progress information
	 */
	final class ProgressReport extends Thread {

		volatile boolean isRunning = true;

		public void run() {
			int count = TLCGlobals.coverageInterval / TLCGlobals.progressInterval;
			try {
				while (isRunning) {
					synchronized (this) {
						this.wait(TLCGlobals.progressInterval);
					}
					final long genTrace = numOfGenTraces.longValue();
					final long m2AndMean = welfordM2AndMean.get();
					final long mean = m2AndMean & 0x00000000FFFFFFFFL; // could be int.
					final long m2 = m2AndMean >>> 32;
					MP.printMessage(EC.TLC_PROGRESS_SIMU, 
							String.valueOf(numOfGenStates.longValue()),
							String.valueOf(genTrace),
							String.valueOf(mean),
							String.valueOf(Math.round(m2 / (genTrace + 1d))), // Var(X),  +1 to prevent div-by-zero.
							String.valueOf(Math.round(Math.sqrt(m2 / (genTrace + 1d))))); // SD, +1 to prevent div-by-zero.
					if (count > 1) {
						count--;
					} else {
						reportCoverage();
						count = TLCGlobals.coverageInterval / TLCGlobals.progressInterval;
					}
					
					writeActionFlowGraph();
				}
			} catch (Exception e) {
				// SZ Jul 10, 2009: changed from error to bug
				MP.printTLCBug(EC.TLC_REPORTER_DIED, null);
			}
		}

		private void writeActionFlowGraph() throws IOException {
			if (!actionStats) {
				return;
			}
			// The number of actions is expected to be low (dozens commons and hundreds a
			// rare). This is why the code below isn't optimized for performance.
			final Action[] actions = Simulator.this.tool.getActions();
			final int len = actions.length;
			
			// Clusters of actions that have the same context:
			// CONSTANT Proc
			// ...
			// A(p) == p \in {...} /\ v' = 42...
			// Next == \E p \in Proc : A(p)
			final Map<String, Set<Integer>> clusters = new HashMap<>();
			for (int i = 0; i < len; i++) {
				final String con = actions[i].con.toString();
				if (!clusters.containsKey(con)) {
				   clusters.put(con, new HashSet<>());	
				}
				clusters.get(con).add(i);
			}
			
			// Write clusters to dot file (override previous file).
			final DotActionWriter dotActionWriter = new DotActionWriter(
					Simulator.this.tool.getRootName() + "_actions.dot", "");
			for (Entry<String, Set<Integer>> cluster : clusters.entrySet()) {
				// key is a unique set of chars accepted/valid as a graphviz cluster id.
				final String key = Integer.toString(Math.abs(cluster.getKey().hashCode()));
				dotActionWriter.writeSubGraphStart(key, cluster.getKey().toString());

				final Set<Integer> ids = cluster.getValue();
				for (Integer id : ids) {
					dotActionWriter.write(actions[id], id);
				}
				dotActionWriter.writeSubGraphEnd();
			}					

			// Element-wise sum the statistics from all workers.
			long[][] aggregateActionStats = new long[len][len];
			final List<SimulationWorker> workers = Simulator.this.workers;
			for (SimulationWorker sw : workers) {
				final long[][] s = sw.actionStats;
				for (int i = 0; i < len; i++) {
					for (int j = 0; j < len; j++) {
						aggregateActionStats[i][j] += s[i][j];
					}
				}
			}
			
			// Write stats to dot file as edges between the action vertices.
			for (int i = 0; i < len; i++) {
				for (int j = 0; j < len; j++) {
					long l = aggregateActionStats[i][j];
					if (l > 0L) {
						// LogLog l (to keep the graph readable) and round to two decimal places (to not
						// write a gazillion decimal places truncated by graphviz anyway).
						final double loglogWeight = Math.log10(Math.log10(l+1)); // +1 to prevent negative inf.
						dotActionWriter.write(actions[i], i, actions[j], j,
								BigDecimal.valueOf(loglogWeight).setScale(2, RoundingMode.HALF_UP)
										.doubleValue());
					} else {
						dotActionWriter.write(actions[i], i, actions[j], j);
					}
				}
			}
			
			// Close dot file.
			dotActionWriter.close();
		}
	}

	public final StateVec getTrace() {
		if (Thread.currentThread() instanceof SimulationWorker) {
			final SimulationWorker w = (SimulationWorker) Thread.currentThread();
			return w.getTrace();
		} else {
			assert numWorkers == 1 && workers.size() == numWorkers;
			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) {
			worker.interrupt();
		}
	}
}