StateManager.java

package edu.udel.cis.vsl.tass.kripke.impl;

import java.io.File;
import java.io.PrintWriter;
import java.util.Collection;
import java.util.HashMap;
import java.util.LinkedHashMap;
import java.util.Map;
import java.util.Map.Entry;
import java.util.Set;
import java.util.Vector;

import edu.udel.cis.vsl.tass.config.RunConfiguration;
import edu.udel.cis.vsl.tass.config.RunConfiguration.DeadlockStrategy;
import edu.udel.cis.vsl.tass.dynamic.IF.DynamicException;
import edu.udel.cis.vsl.tass.dynamic.IF.DynamicFactoryIF;
import edu.udel.cis.vsl.tass.dynamic.IF.ValueSubstituterIF;
import edu.udel.cis.vsl.tass.dynamic.IF.cell.ModelCellIF;
import edu.udel.cis.vsl.tass.dynamic.IF.simplify.DynamicSimplifierIF;
import edu.udel.cis.vsl.tass.dynamic.IF.simplify.MorphicSimplifierCacheIF;
import edu.udel.cis.vsl.tass.dynamic.IF.simplify.MorphicSimplifierIF;
import edu.udel.cis.vsl.tass.dynamic.IF.value.ValueIF;
import edu.udel.cis.vsl.tass.dynamic.IF.value.VariableReferenceValueIF;
import edu.udel.cis.vsl.tass.kripke.IF.TASSEnablerIF;
import edu.udel.cis.vsl.tass.kripke.IF.TASSStateManagerIF;
import edu.udel.cis.vsl.tass.kripke.IF.VerificationUtility;
import edu.udel.cis.vsl.tass.model.IF.CollectiveAssertionIF;
import edu.udel.cis.vsl.tass.model.IF.ModelFactoryIF;
import edu.udel.cis.vsl.tass.model.IF.ModelIF;
import edu.udel.cis.vsl.tass.model.IF.ModelSequence;
import edu.udel.cis.vsl.tass.model.IF.ProcessIF;
import edu.udel.cis.vsl.tass.model.IF.expression.ExpressionIF;
import edu.udel.cis.vsl.tass.model.IF.location.ForLoopLocationIF;
import edu.udel.cis.vsl.tass.model.IF.location.LocationIF;
import edu.udel.cis.vsl.tass.model.IF.location.LoopLocationIF;
import edu.udel.cis.vsl.tass.model.IF.statement.NoopStatementIF;
import edu.udel.cis.vsl.tass.model.IF.statement.ReceiveStatementIF;
import edu.udel.cis.vsl.tass.model.IF.statement.SendStatementIF;
import edu.udel.cis.vsl.tass.model.IF.statement.StatementIF;
import edu.udel.cis.vsl.tass.model.IF.variable.SharedVariableIF;
import edu.udel.cis.vsl.tass.model.IF.variable.VariableIF;
import edu.udel.cis.vsl.tass.morph.MorphicArray;
import edu.udel.cis.vsl.tass.morph.MorphicArrayFactory;
import edu.udel.cis.vsl.tass.morph.MorphicSet;
import edu.udel.cis.vsl.tass.morph.MorphicVector;
import edu.udel.cis.vsl.tass.morph.MorphicVectorFactory;
import edu.udel.cis.vsl.tass.predicate.IF.TASSPredicateIF;
import edu.udel.cis.vsl.tass.semantics.Semantics;
import edu.udel.cis.vsl.tass.semantics.IF.EvaluatorIF;
import edu.udel.cis.vsl.tass.semantics.IF.ExecutionException;
import edu.udel.cis.vsl.tass.semantics.IF.ExecutionProblem;
import edu.udel.cis.vsl.tass.semantics.IF.ExecutionProblem.Certainty;
import edu.udel.cis.vsl.tass.semantics.IF.ExecutionProblem.ErrorKind;
import edu.udel.cis.vsl.tass.semantics.IF.ExecutionStateException;
import edu.udel.cis.vsl.tass.semantics.IF.ExecutorIF;
import edu.udel.cis.vsl.tass.semantics.IF.LibraryExecutorLoaderIF;
import edu.udel.cis.vsl.tass.semantics.IF.LogIF;
import edu.udel.cis.vsl.tass.state.States;
import edu.udel.cis.vsl.tass.state.IF.CollectiveLoopRecordIF;
import edu.udel.cis.vsl.tass.state.IF.CollectiveRecordIF;
import edu.udel.cis.vsl.tass.state.IF.ModelStateFactoryIF;
import edu.udel.cis.vsl.tass.state.IF.ModelStateIF;
import edu.udel.cis.vsl.tass.state.IF.ProcessStateIF;
import edu.udel.cis.vsl.tass.state.IF.StateFactoryIF;
import edu.udel.cis.vsl.tass.state.IF.StateIF;
import edu.udel.cis.vsl.tass.state.IF.SystemEnvironmentIF;
import edu.udel.cis.vsl.tass.symbolic.IF.SymbolicConstantIF;
import edu.udel.cis.vsl.tass.symbolic.IF.SymbolicUniverseIF;
import edu.udel.cis.vsl.tass.transition.IF.SimpleTransitionIF;
import edu.udel.cis.vsl.tass.transition.IF.SynchronousTransitionIF;
import edu.udel.cis.vsl.tass.transition.IF.TransitionIF;
import edu.udel.cis.vsl.tass.transition.IF.TransitionSequenceIF;
import edu.udel.cis.vsl.tass.util.Source;
import edu.udel.cis.vsl.tass.util.TernaryResult.ResultType;

public class StateManager implements TASSStateManagerIF {

	// experimental: remember only last guard.
	private boolean forgetAssumptions = false;

	private boolean saveStackStates = true; // experimental optimization

	private static int updatePeriod = 100000;

	private int updateThreshold = updatePeriod;

	private TASSEnablerIF enabler;

	private ModelFactoryIF modelFactory;

	private ModelSequence modelSequence;

	private int numModels;

	private DynamicFactoryIF dynamicFactory;

	private SymbolicUniverseIF universe;

	private ModelStateFactoryIF modelStateFactory;

	private StateFactoryIF stateFactory;

	private MorphicArrayFactory<ProcessStateIF> processStateArrayFactory;

	private MorphicArrayFactory<MorphicArray<ProcessStateIF>> processStateArrayArrayFactory;

	private MorphicArrayFactory<MorphicSet<VariableReferenceValueIF>> variableSetArrayFactory;

	private MorphicVectorFactory<CollectiveRecordIF> queueFactory;

	/** A state simplifier which does not simplify process state snapshots. */
	private MorphicSimplifierIF<StateIF> stateSimplifier;

	/**
	 * A state simplifier which does simplify process state snapshots. Used in
	 * loop technique when loop symbolic constants (Y_i) are canonicalized.
	 */
	private MorphicSimplifierIF<StateIF> loopStateSimplifier;

	private ExecutorIF executor;

	private EvaluatorIF evaluator;

	private boolean simplifyState;

	private ValueIF trueValue, falseValue;

	private boolean useLoopTechnique;

	private boolean useCollectiveAssertions;

	private boolean showStates;

	private boolean showSavedStates;

	private boolean showTransitions;

	private LogIF log;

	private boolean verbose;

	private PrintWriter out;

	private int bottom = 0;

	/** The total number of transitions executed through calls to nextState. */
	private int numTransitionsExecuted = 0;

	/**
	 * The total number of states seen in the transition system. Intermediate
	 * states (those generated within the process of executing a single
	 * transition) do not count. These are only states seen after completing the
	 * execution of a transition. If the state was known to have been seen
	 * before, it is only counted once.
	 */
	private int numStatesSeen = 1;

	/**
	 * The first non-deterministic state on the stack, or null if there are no
	 * such states on the stack.
	 */
	private StateIF firstNDStateOnStack = null;

	/**
	 * If you really want to find cycles in the state space, you need to push on
	 * stack any state that is saved.
	 */
	private boolean cycleDetection = false;

	/**
	 * Does the predicate need to be checked at even the intermediate states?
	 */
	private boolean checkAllStates;

	/**
	 * The property that is being checked.
	 */
	private TASSPredicateIF predicate;

	private Map<Map<SymbolicConstantIF, SymbolicConstantIF>, DynamicSimplifierIF> loopConstantCacheMap = new HashMap<Map<SymbolicConstantIF, SymbolicConstantIF>, DynamicSimplifierIF>();

	public StateManager(LibraryExecutorLoaderIF loader,
			ModelSequence modelSequence, DynamicFactoryIF dynamicFactory,
			StateFactoryIF stateFactory, int bufferSize, LogIF log) {
		RunConfiguration configuration = dynamicFactory.configuration();

		this.verbose = configuration.verbose();
		this.out = configuration.out();
		this.cycleDetection = configuration.detectCycles();
		this.useLoopTechnique = configuration.useLoopTechnique();
		if (useLoopTechnique)
			bottom = 1;
		this.useCollectiveAssertions = configuration.useCollectiveAssertions();
		this.showStates = configuration.showStates();
		this.showSavedStates = configuration.showSavedStates();
		this.showTransitions = configuration.showTransitions();
		this.modelSequence = modelSequence;
		this.numModels = modelSequence.numModels();
		assert numModels >= 1;
		this.dynamicFactory = dynamicFactory;
		this.universe = dynamicFactory.universe();
		this.falseValue = dynamicFactory.falseValue();
		this.trueValue = dynamicFactory.trueValue();
		this.log = log;
		this.modelStateFactory = stateFactory.modelStateFactory();
		this.modelFactory = modelSequence.modelWithIndex(0).modelFactory();
		this.simplifyState = configuration.simplify();
		this.stateFactory = stateFactory;
		this.executor = Semantics.newExecutor(loader, dynamicFactory,
				bufferSize, log);
		this.evaluator = Semantics
				.newEvaluator(dynamicFactory, bufferSize, log);
		this.stateSimplifier = stateFactory.simplifier(true); // simplify
		// snapshots
		this.processStateArrayFactory = stateFactory.processStateArrayFactory();
		this.processStateArrayArrayFactory = new MorphicArrayFactory<MorphicArray<ProcessStateIF>>(
				processStateArrayFactory);
		this.variableSetArrayFactory = stateFactory.variableSetArrayFactory();
		this.queueFactory = stateFactory.queueFactory();
		this.loopStateSimplifier = stateFactory.simplifier(true);
		this.predicate = null;
		this.checkAllStates = false;
	}

	public StateManager(LibraryExecutorLoaderIF loader,
			ModelSequence modelSequence, DynamicFactoryIF dynamicFactory,
			StateFactoryIF stateFactory, int bufferSize, LogIF log,
			TASSPredicateIF predicate) {
		this(loader, modelSequence, dynamicFactory, stateFactory, bufferSize,
				log);
		this.predicate = predicate;
		this.checkAllStates = dynamicFactory.configuration().deadlockStrategy() == DeadlockStrategy.POTENTIAL;
	}

	public int numTransitionsExecuted() {
		return numTransitionsExecuted;
	}

	public int numStatesSeen() {
		return numStatesSeen;
	}

	public int numStatesSaved() {
		return stateFactory.numStates();
	}

	@Override
	public void setEnabler(TASSEnablerIF enabler) {
		this.enabler = enabler;
	}

	private StateIF save(StateIF state) throws ExecutionStateException {
		state = stateFactory.canonic(state);
		if (simplifyState)
			state = simplify(state);
		if (showSavedStates) {
			out.println();
			printStateLong(out, state);
		}
		return state;
	}

	private void save(SystemEnvironmentIF environment)
			throws ExecutionStateException {
		environment.setState(save(environment.state()));
	}

	/**
	 * If the location has the property that on any execution ...
	 * 
	 * l0 -t0-> l1 --> l2
	 * 
	 * If l1 has the property:
	 * 
	 * (1) there is exactly one incoming edge (statement), call it t0 (2) after
	 * executing t0, in whatever POR scheme is used in the search, a transition
	 * departing from l1 must necessarily get scheduled next
	 * 
	 * then it is not necessary to save the state s that arises from executing
	 * t0. Because the only way to arrive at s is by going through a state which
	 * includes l0.
	 * 
	 * 
	 * Note if there are no "ND" states on the stack then the only path to this
	 * state in the reduced state space is the single path represented by the
	 * stack, since any other path would have to branch off from that one
	 * 
	 * or go through this state and return to it....
	 * 
	 * */
	// TODO: pre-compute this statically and set field in every location!
	private boolean requiresSaving(LocationIF location) {
		if (location.isLocal() || this.firstNDStateOnStack == null) {
			int numIncoming = location.incomingStatements().size();

			if (location == location.function().startLocation())
				numIncoming++;
			if (numIncoming == 1) {
				return false;
			} else {
				LocationIF openLocation = location.openLocation();

				if (openLocation != null && openLocation.isBranch())
					return false;
			}
		}
		if (location instanceof ForLoopLocationIF) {
			if (useLoopTechnique) {
				CollectiveAssertionIF assertion = location
						.collectiveAssertion();

				if (assertion == null || !assertion.isLoopInvariant())
					return false;
			} else {
				return false;
			}
		}
		return true;
	}

	private StateIF saveIfNecessary(StateIF state, LocationIF location)
			throws ExecutionStateException {
		if (requiresSaving(location))
			return save(state);
		else
			return state;
	}

	private void saveIfNecessary(SystemEnvironmentIF environment,
			LocationIF location) throws ExecutionStateException {
		environment.setState(saveIfNecessary(environment.state(), location));
	}

	public StateIF initialState() {
		SystemEnvironmentIF environment = States.newEnvironment(modelSequence,
				stateFactory, log);
		ModelStateIF modelStates[] = new ModelStateIF[numModels];
		for (int i = 0; i < numModels; i++)
			modelStates[i] = modelStateFactory.emptyState(modelSequence
					.modelWithIndex(i));
		ValueIF pathCondition = dynamicFactory.symbolicValue(true);
		ModelIF model1 = modelSequence.modelWithIndex(0);
		Map<VariableIF, ValueIF> inputs = VerificationUtility.inputMap(model1,
				dynamicFactory);
		MorphicVector<CollectiveRecordIF> collectiveQueue;
		StateIF state, result;

		if (useLoopTechnique) {
			CollectiveLoopRecordIF initialRecord = stateFactory
					.collectiveLoopRecord(null, null, pathCondition, trueValue,
							null, false);

			collectiveQueue = stateFactory.queueFactory().newVector(1);
			collectiveQueue.set(0, initialRecord);
		} else {
			collectiveQueue = stateFactory.queueFactory().newVector(0);
		}
		state = stateFactory.state(modelStates, pathCondition, collectiveQueue);
		environment.setState(state);
		if (useLoopTechnique)
			environment.setLoopQueueIndex(0);
		executor.initialize(environment, model1, environment.getAssumption(),
				inputs, true, true);
		if (numModels >= 1) {
			for (int i = 1; i < numModels; i++) {
				ModelIF model2 = modelSequence.modelWithIndex(i);

				for (SharedVariableIF variable2 : model2.scope()
						.inputVariables()) {
					SharedVariableIF variable1 = variable2
							.correspondingVariable();

					if (variable1 != null) {
						try {
							ValueIF value = evaluator.evaluate(environment,
									modelFactory.variableExpression(variable1));

							inputs.put(variable2, value);
						} catch (ExecutionException e) {
							log.report(e);
							environment.setAssumption(falseValue);
							return environment.state();
						}
					}
				}
				executor.initialize(environment, model2,
						environment.getAssumption(), inputs, false, true);
			}
		}
		if (useCollectiveAssertions)
			executeAllCollectives(environment);
		result = environment.state();
		try {
			result = save(result);
		} catch (ExecutionStateException error) {
			log.report(error);
			environment.setState(result);
			environment.setAssumption(falseValue);
		}
		TransitionSequenceIF sequence = (TransitionSequenceIF) enabler
				.enabledTransitions(result);

		enabler.setCache(result, sequence);
		result.setIsNonDeterministic(enabler.isNonDeterministic(sequence));
		return result;
	}

	public StateIF initialState(ValueIF initialPathCondition,
			Map<VariableIF, ValueIF> inputs, boolean useKeyAssumptions,
			boolean useNonKeyAssumptions) {
		SystemEnvironmentIF environment = States.newEnvironment(modelSequence,
				stateFactory, log);
		ModelStateIF modelStates[] = new ModelStateIF[numModels];
		for (int i = 0; i < numModels; i++)
			modelStates[i] = modelStateFactory.emptyState(modelSequence
					.modelWithIndex(i));
		ValueIF pathCondition = dynamicFactory.symbolicValue(true);
		StateIF state, result;
		MorphicVector<CollectiveRecordIF> collectiveQueue;

		if (useLoopTechnique) {
			CollectiveLoopRecordIF initialRecord = stateFactory
					.collectiveLoopRecord(null, null, pathCondition, trueValue,
							null, false);

			collectiveQueue = stateFactory.queueFactory().newVector(1);
			collectiveQueue.set(0, initialRecord);
		} else {
			collectiveQueue = stateFactory.queueFactory().newVector(0);
		}
		state = stateFactory.state(modelStates, pathCondition, collectiveQueue);
		environment.setState(state);
		if (useLoopTechnique)
			environment.setLoopQueueIndex(0);
		for (int i = 0; i < numModels; i++) {
			executor.initialize(environment, modelSequence.modelWithIndex(i),
					initialPathCondition, inputs, useKeyAssumptions,
					useNonKeyAssumptions);
		}
		if (useCollectiveAssertions)
			executeAllCollectives(environment);
		result = environment.state();
		try {
			result = save(result);
		} catch (ExecutionStateException error) {
			log.report(error);
			environment.setState(result);
			environment.setAssumption(falseValue);
		}
		TransitionSequenceIF sequence = (TransitionSequenceIF) enabler
				.enabledTransitions(result);

		enabler.setCache(result, sequence);
		result.setIsNonDeterministic(enabler.isNonDeterministic(sequence));
		return result;
	}

	/** Only set up initial values of vars */
	public StateIF preInitialState(ValueIF initialPathCondition,
			Map<VariableIF, ValueIF> inputs, boolean useKeyAssumptions,
			boolean useNonKeyAssumptions) {
		SystemEnvironmentIF environment = States.newEnvironment(modelSequence,
				stateFactory, log);
		ModelStateIF modelStates[] = new ModelStateIF[numModels];
		for (int i = 0; i < numModels; i++)
			modelStates[i] = modelStateFactory.emptyState(modelSequence
					.modelWithIndex(i));
		ValueIF pathCondition = dynamicFactory.symbolicValue(true);
		StateIF state, result;
		MorphicVector<CollectiveRecordIF> collectiveQueue;

		if (useLoopTechnique) {
			CollectiveLoopRecordIF initialRecord = stateFactory
					.collectiveLoopRecord(null, null, pathCondition, trueValue,
							null, false);

			collectiveQueue = stateFactory.queueFactory().newVector(1);
			collectiveQueue.set(0, initialRecord);
		} else {
			collectiveQueue = stateFactory.queueFactory().newVector(0);
		}
		state = stateFactory.state(modelStates, pathCondition, collectiveQueue);
		environment.setState(state);
		if (useLoopTechnique)
			environment.setLoopQueueIndex(0);
		for (int i = 0; i < numModels; i++) {
			executor.initialize(environment, modelSequence.modelWithIndex(i),
					initialPathCondition, inputs, useKeyAssumptions,
					useNonKeyAssumptions);
		}
		result = environment.state();
		try {
			result = save(result);
		} catch (ExecutionStateException error) {
			log.report(error);
			environment.setState(result);
			environment.setAssumption(falseValue);
		}
		return result;
	}

	private void executeAllCollectives(SystemEnvironmentIF environment) {
		for (int i = 0; i < numModels; i++) {
			ModelIF model = modelSequence.modelWithIndex(i);
			int numProcs = model.numProcs();

			for (int j = 0; j < numProcs; j++) {
				ProcessIF process = model.process(j);

				executeCollective(environment, process);
			}
		}
	}

	public StateIF nextState(StateIF state, TransitionIF transition) {
		// loop. if you've seen the state before (check seen field),
		// return it. get the enabled sequence from the enabler.
		// if it has exactly one transition, repeat. Else return it.

		// TODO: it seems like you have to check the predicate on the
		// intermediate states.
		SystemEnvironmentIF environment = States.newEnvironment(modelSequence,
				stateFactory, log);

		while (true) {
			boolean printTransition = verbose;

			if (!printTransition) {
				if (showTransitions && transition instanceof SimpleTransitionIF) {
					SimpleTransitionIF simpleTransition = (SimpleTransitionIF) transition;
					StatementIF statement = simpleTransition.statement();

					if (statement != null) {
						Source source = statement.getSource();

						if (source != null) {
							File file = source.file();

							if (file != null) {
								String filename = file.getName();

								if (filename != null
										&& !filename.startsWith("lib")) {
									printTransition = true;
								}
							}
						}
					}
				}
			}
			if (printTransition) {
				out.print("\nExecuting ");
				transition.print(out);
				out.println();
				out.flush();
			}
			state = immediateNextState(state, transition);
			if (showStates) {
				printStateLong(out, state);
			}
			if (seen(state)) {
				return state;
			}
			numStatesSeen++;
			if (cycleDetection && state.isCanonic()) {
				TransitionSequenceIF sequence = (TransitionSequenceIF) enabler
						.enabledTransitions(state);

				enabler.setCache(state, sequence);
				state.setIsNonDeterministic(enabler
						.isNonDeterministic(sequence));
				return state;
			} else {
				TransitionSequenceIF sequence = (TransitionSequenceIF) enabler
						.enabledTransitions(state);

				if (enabler.hasOneTransition(sequence)) {
					if (verbose) {
						out.println();
						printStateLong(out, state);
					}
					if (state.isCommitted())
						setSeen(state, true);

					// TODO: here you are about to pass through this state.
					// Before you do this, shouldn't you check the predicate?

					if (checkAllStates) {
						if (predicate.holdsAt(state))
							return state;
					}

					transition = enabler.next(sequence);
				} else {
					enabler.setCache(state, sequence);
					state.commit();
					if (saveStackStates) {
						environment.setState(state);
						try {
							save(environment);
						} catch (ExecutionStateException e) {
							log.report(e);
							environment.setAssumption(falseValue);
						}
						state = environment.state();
					}
					state.setIsNonDeterministic(enabler
							.isNonDeterministic(sequence));

					return state;
				}
			}
		}
	}

	private StateIF immediateNextState(StateIF state, TransitionIF transition) {
		numTransitionsExecuted++;

		if (numTransitionsExecuted == updateThreshold) {
			if (numTransitionsExecuted == updatePeriod)
				out.println();
			out.println("    transitionsExecuted: " + numTransitionsExecuted
					+ "    statesSeen: " + numStatesSeen + "    statesSaved: "
					+ numStatesSaved());
			out.flush();
			updateThreshold += updatePeriod;
		}
		if (transition instanceof SimpleTransitionIF) {
			SimpleTransitionIF simple = (SimpleTransitionIF) transition;

			if (useLoopTechnique) {
				StatementIF statement = simple.statement();
				LocationIF location = statement.sourceLocation();

				if (location instanceof LoopLocationIF) {
					CollectiveAssertionIF assertion = location
							.collectiveAssertion();

					if (assertion != null && assertion.isLoopInvariant()) {
						return nextStateLoop(state, (NoopStatementIF) statement);
					}
				}
			}
			return nextStateSimple(state, simple);
		} else
			return nextStateSynchronous(state,
					(SynchronousTransitionIF) transition);
	}

	private boolean isComplete(CollectiveRecordIF record) {
		MorphicArray<ProcessStateIF> snapshots = record.snapshots();

		for (ProcessStateIF snapshot : snapshots) {
			if (snapshot == null)
				return false;
		}
		return true;
	}

	/**
	 * Execute actions dealing with collective assertion. Given a process which
	 * may have just moved to a new location, and the current environment.
	 * Modifies the environment by dealing with the collective assertion queue,
	 * checking assertion holds, etc.
	 * 
	 * @param oldState
	 * @param process
	 * @return
	 * @throws DynamicException
	 * @throws ExecutionProblem
	 */
	private void executeCollective(SystemEnvironmentIF environment,
			ProcessIF process) {
		LocationIF location = environment.location(process);

		if (location == null)
			return;

		CollectiveAssertionIF assertion = location.collectiveAssertion();

		if (assertion == null)
			return;

		int processIndex = assertion.indexOf(process);
		ProcessStateIF newSnapshot = environment.processState(process);
		int queueLength = environment.collectiveQueueSize();
		CollectiveRecordIF record;
		int position;

		try {
			position = getPositionInQueue(environment, assertion, process);
		} catch (ExecutionStateException e) {
			log.report(e);
			environment.setAssumption(falseValue);
			return;
		}
		if (position >= queueLength)
			environment.collectiveEnqueue(stateFactory
					.collectiveRecord(assertion));
		environment.setSnapshot(position, processIndex, newSnapshot);
		record = environment.getCollectiveRecord(position);
		if (isComplete(record)) {
			try {
				checkCollectiveAssertion(assertion, record.snapshots(),
						environment);
			} catch (DynamicException e) {
				log.report(new ExecutionStateException(environment.locations(),
						e, Certainty.NONE));
				environment.setAssumption(falseValue);
			} catch (ExecutionProblem problem) {
				log.report(new ExecutionStateException(environment.locations(),
						problem));
				environment.setAssumption(falseValue);
			}
			if (environment.getAssumption().equals(falseValue))
				return;
			environment.removeCollectiveRecord(position);
		}
	}

	private int getPositionInQueue(SystemEnvironmentIF environment,
			CollectiveAssertionIF assertion, ProcessIF process)
			throws ExecutionStateException {
		MorphicVector<CollectiveRecordIF> queue = environment.collectiveQueue();
		int queueLength = queue.size();
		int position = -1;

		// if useLoopTechnique, position 0 has special use: permanentPC, so
		// don't look at it...
		for (int i = queueLength - 1; i >= bottom; i--) {
			if (queue.get(i).reachedBy(process)) {
				position = i + 1;
				break;
			}
		}
		if (position < 0) {
			// there are no non-null entries:
			position = bottom;
		}
		if (position < queueLength) {
			// record already exists
			CollectiveRecordIF oldRecord = queue.get(position);

			if (!assertion.equals(oldRecord.assertion()))
				throw new ExecutionStateException(environment.locations(),
						ErrorKind.ASSERTION_VIOLATION, Certainty.PROVEABLE,
						"Out of order collective assertion: " + process
								+ " arrived at assertion:\n" + assertion
								+ "\nExpected to see assertion:\n"
								+ oldRecord.assertion());
		}
		return position;
	}

	/**
	 * Constructs the composite state by "gluing together" the snapshot states,
	 * using empty states for the processes not involved in the assertion, and
	 * using the path condition from the given environment. Shared values
	 * (input/output variables) in each model are taken from the corresponding
	 * shared values in the environment.
	 */
	private StateIF compositeState(CollectiveAssertionIF assertion,
			MorphicArray<ProcessStateIF> snapshots,
			SystemEnvironmentIF environment) throws DynamicException,
			ExecutionProblem {
		StateIF currentState = environment.state();
		int numAssertionProcs = assertion.numProcs();
		MorphicArray<MorphicArray<ProcessStateIF>> allNewProcessStates = processStateArrayArrayFactory
				.newArray(numModels);
		ModelStateIF[] newModelStates = new ModelStateIF[numModels];

		for (int i = 0; i < numModels; i++) {
			allNewProcessStates.set(i, processStateArrayFactory
					.newArray(modelSequence.modelWithIndex(i).numProcs()));
		}
		for (int j = 0; j < numAssertionProcs; j++) {
			ProcessIF process = assertion.process(j);
			int modelIndex = modelSequence.indexOf(process.model());

			allNewProcessStates.get(modelIndex).set(process.pid(),
					snapshots.get(j));
		}
		for (int i = 0; i < numModels; i++) {
			ModelIF model = modelSequence.modelWithIndex(i);
			int numProcs = model.numProcs();
			ModelStateIF currentModelState = environment.modelState(i);
			MorphicArray<ProcessStateIF> newProcessStates = allNewProcessStates
					.get(i);

			for (int j = 0; j < numProcs; j++) {
				if (newProcessStates.get(j) == null)
					newProcessStates.set(j, modelStateFactory
							.emptyProcessState(model.process(j)));
			}
			newModelStates[i] = modelStateFactory.newState(newProcessStates,
					currentModelState.sharedValues(),
					currentModelState.buffer());
		}
		return stateFactory.state(newModelStates, currentState.pathCondition(),
				currentState.collectiveQueue());
	}

	/**
	 * Evaluates the conjunction of the collective assertion expressions in the
	 * processes involved in a collective assertions. The assumption used in
	 * evaluating the expressions is the path condition in the composite state.
	 */
	private ValueIF collectiveClaim(CollectiveAssertionIF assertion,
			StateIF compositeState) throws ExecutionException, DynamicException {
		int numAssertionProcs = assertion.numProcs();
		SystemEnvironmentIF environment = States.newEnvironment(modelSequence,
				stateFactory, log);
		ValueIF claim = null;

		environment.setState(compositeState);
		for (int i = 0; i < numAssertionProcs; i++) {
			ProcessIF process = assertion.process(i);
			ExpressionIF collectiveExpression = environment.location(process)
					.collectiveExpression();
			ValueIF localClaim = evaluator.evaluate(environment,
					collectiveExpression);

			if (claim == null)
				claim = localClaim;
			else
				claim = dynamicFactory.and(trueValue, claim, localClaim);
			if (verbose) {
				out.println("Collective assertion " + assertion.identifier()
						+ " expression from " + process + ":\n"
						+ collectiveExpression + "\nEvaluates to:\n"
						+ localClaim);
				out.flush();
			}
		}
		return claim;
	}

	/**
	 * Checks that the collective assertion holds in the given composite state.
	 * To extract the collective claim, the path condition in the composite
	 * state is used. To check the claim is valid, the path condition in the
	 * given environment is used. The environment is modified if the claim
	 * cannot be proved valid.
	 */
	private void checkCollectiveAssertion(SystemEnvironmentIF environment,
			CollectiveAssertionIF assertion, StateIF compositeState)
			throws DynamicException, ExecutionProblem {
		ValueIF claim = null;
		ResultType truth;

		if (verbose) {
			out.println("Checking collective assertion "
					+ assertion.identifier() + "...");
			out.flush();
		}
		claim = collectiveClaim(assertion, compositeState);
		truth = dynamicFactory.valid(environment.getAssumption(), claim);
		if (truth != ResultType.YES) {
			String message;
			Certainty certainty;

			if (truth == ResultType.MAYBE) {
				message = "Cannot prove that collective assertion "
						+ assertion.identifier() + " holds.";
				certainty = Certainty.MAYBE;
			} else {
				message = "Collective assertion " + assertion.identifier()
						+ " can be violated.";
				certainty = Certainty.PROVEABLE;
			}
			message += "\n    path condition : "
					+ compositeState.pathCondition()
					+ "\n         assertion : " + claim;
			log.report(new ExecutionException(assertion,
					ErrorKind.ASSERTION_VIOLATION, certainty, message));
			environment.addAssumption(claim);
		} else {
			if (verbose) {
				out.println("...Collective assertion " + assertion.identifier()
						+ " holds.");
				out.flush();
			}
		}
	}

	/**
	 * Checks the collective assertion holds in the process snapshots, using the
	 * assumption in the given environment. Modifies the path condition in the
	 * environment if necessary to force assertion to be valid (after logging
	 * error).
	 */
	private void checkCollectiveAssertion(CollectiveAssertionIF assertion,
			MorphicArray<ProcessStateIF> snapshots,
			SystemEnvironmentIF environment) throws DynamicException,
			ExecutionProblem {
		StateIF compositeState = compositeState(assertion, snapshots,
				environment);

		checkCollectiveAssertion(environment, assertion, compositeState);
	}

	private StateIF nextStateLoop(StateIF state, NoopStatementIF statement) {
		SystemEnvironmentIF environment = States.newEnvironment(modelSequence,
				stateFactory, log);
		environment.setState(state);
		try {
			executeLoopTransition(environment, statement);
		} catch (ExecutionProblem problem) {
			log.report(new ExecutionException(statement, problem));
			environment.setAssumption(falseValue);
		} catch (DynamicException exception) {
			log.report(new ExecutionException(statement, exception,
					Certainty.NONE));
			environment.setAssumption(falseValue);
		}
		if (useCollectiveAssertions)
			executeCollective(environment, statement.process());
		try {
			// saveIfNecessary(environment, statement.targetLocation());
			save(environment);
		} catch (ExecutionStateException e) {
			log.report(e);
			environment.setAssumption(falseValue);
		}
		return environment.state();
	}

	// TODO: could store the list of symbolic constants in state
	private void executeLoopTransition(SystemEnvironmentIF environment,
			NoopStatementIF statement) throws DynamicException,
			ExecutionProblem {
		ProcessIF process = statement.process();
		MorphicVector<CollectiveRecordIF> queue = environment.collectiveQueue();
		int queueLength = queue.size();
		LoopLocationIF loopLocation = (LoopLocationIF) statement
				.sourceLocation();
		CollectiveAssertionIF assertion = loopLocation.collectiveAssertion();
		int numProcs = assertion.numProcs();
		int processIndex = assertion.indexOf(process);
		assert processIndex >= 0;
		int position = getPositionInQueue(environment, assertion, process);
		boolean newEntry = position >= queueLength;
		ValueIF newPathCondition = environment.getAssumption();
		MorphicArray<ProcessStateIF> newSnapshots = processStateArrayFactory
				.newArray(numProcs);
		MorphicArray<MorphicSet<VariableReferenceValueIF>> newWritevarSets = variableSetArrayFactory
				.newArray(numProcs);
		MorphicSet<VariableReferenceValueIF> writevarSet = null;
		Collection<SymbolicConstantIF> collectibles = collectibleSymbolicConstants(environment
				.state());
		int nextIndex = 0;
		boolean isComplete = true;
		ProcessStateIF newSnapshot;
		CollectiveLoopRecordIF oldRecord = null;
		ValueIF newPartialPathCondition, newRelationalPredicate;
		CollectiveLoopRecordIF newRecord;
		boolean isTrueBranch;
		MorphicVector<CollectiveRecordIF> newQueue;

		assert useLoopTechnique;
		if (statement == loopLocation.trueBranch()) {
			isTrueBranch = true;
		} else if (statement == loopLocation.falseBranch()) {
			isTrueBranch = false;
		} else {
			throw new ExecutionProblem(
					ErrorKind.INTERNAL,
					Certainty.NONE,
					"TASS internal error:\n"
							+ "Statement from loop node is neither true nor false branch:\n"
							+ statement);
		}
		environment.setCurrentProcess(process);
		int oldLoopIndex = environment.loopQueueIndex();
		if (oldLoopIndex > 0) {
			CollectiveLoopRecordIF previousRecord = (CollectiveLoopRecordIF) queue
					.get(oldLoopIndex);

			assert previousRecord.trueBranch();
			if (assertion == previousRecord.assertion()) {
				writevarSet = previousRecord.writevarSets().get(processIndex);
			}
		}
		if (!newEntry) {
			oldRecord = (CollectiveLoopRecordIF) queue.get(position);
			if (oldRecord.trueBranch() != isTrueBranch) {
				throw new ExecutionProblem(ErrorKind.ASSERTION_VIOLATION,
						Certainty.MAYBE, "Inconsistency in collective loop:\n"
								+ "expected " + oldRecord.trueBranch()
								+ " branch but saw " + isTrueBranch
								+ " branch in " + process);
			}
			newPartialPathCondition = oldRecord.partialPathCondition();
			newRelationalPredicate = oldRecord.relationalPredicate();
			for (int i = 0; i < numProcs; i++) {
				if (i == processIndex)
					newWritevarSets.set(i, writevarSet);
				else
					newWritevarSets.set(i, oldRecord.writevarSets().get(i));
			}
		} else {
			newPartialPathCondition = trueValue;
			newRelationalPredicate = trueValue;
			newWritevarSets.set(processIndex, writevarSet);
			// remaining entries are null.
		}
		// so that all changes to path condition do not affect anything in
		// queue...
		environment.setCurrentProcess(null);
		for (SymbolicConstantIF x : collectibles) {
			int index = indexOf(x);

			if (index >= nextIndex)
				nextIndex = index + 1;
		}
		if (writevarSet != null) {
			for (VariableReferenceValueIF variableReference : writevarSet) {
				ModelCellIF cell = (ModelCellIF) variableReference.variable();
				ValueIF oldValue = environment.valueOf(cell);

				if (dynamicFactory.isUndefined(oldValue))
					continue;

				ValueIF newValue = dynamicFactory.symbolicConstant("Y"
						+ nextIndex, oldValue.valueType());
				ValueIF predicate = dynamicFactory.equals(trueValue, newValue,
						oldValue);

				nextIndex++;
				newRelationalPredicate = dynamicFactory.and(trueValue,
						newRelationalPredicate, predicate);
				environment.setValue(cell, newValue);
			}
		}
		newSnapshot = environment.processState(process);
		newSnapshot.commit();
		newSnapshots.set(processIndex, newSnapshot);
		if (!newEntry) {
			for (int i = 0; i < numProcs; i++)
				if (i != processIndex)
					newSnapshots.set(i, oldRecord.snapshots().get(i));
		}

		ValueIF guard = evaluator.evaluate(environment,
				loopLocation.condition());

		if (!isTrueBranch)
			guard = dynamicFactory.not(trueValue, guard);
		newPartialPathCondition = dynamicFactory.and(trueValue,
				newPartialPathCondition, guard);
		newPathCondition = dynamicFactory.and(trueValue, newPathCondition,
				newPartialPathCondition);
		newPathCondition = dynamicFactory.and(trueValue, newPathCondition,
				newRelationalPredicate);

		// for a false branch, the newPartialPathCondition should
		// contain only the guards, since it is never used to
		// add assumptions

		// the newPathCondition is used to evaluate the claim...

		environment.setAssumption(newPathCondition);
		for (ProcessStateIF processState : newSnapshots) {
			if (processState == null) {
				isComplete = false;
				break;
			}
		}
		if (!isComplete) {
			int newQueueLength = (newEntry ? queueLength + 1 : queueLength);

			newQueue = queueFactory.newVector(newQueueLength);
			assert newSnapshots != null;
			newRecord = stateFactory.collectiveLoopRecord(assertion,
					newSnapshots, newPartialPathCondition,
					newRelationalPredicate, newWritevarSets, isTrueBranch);
			for (int i = 0; i < position; i++)
				newQueue.set(i, queue.get(i));
			newQueue.set(position, newRecord);
			for (int i = position + 1; i < newQueueLength; i++)
				newQueue.set(i, queue.get(i));
		} else { // isComplete
			// collective assertion is checked using newPathCondition...
			StateIF compositeState = compositeState(assertion, newSnapshots,
					environment);
			ValueIF claim = null;

			checkCollectiveAssertion(environment, assertion, compositeState);

			boolean pop = false;
			int newQueueLength = queueLength;

			if (newEntry) // enqueing a new entry increases queue length by 1
				newQueueLength++;

			// look at position-1. This has to be top of stack
			// because position is complete. need to determine if
			// this is repeat entry into loop.
			if (position >= 2) {
				CollectiveLoopRecordIF top = (CollectiveLoopRecordIF) queue
						.get(position - 1);

				assert top.trueBranch();
				assert top.isComplete();
				if (top.assertion() == assertion) {
					pop = true;
					// popping old record from loop stack decreases length by 1
					newQueueLength--;
				}
			}

			// construct new record...
			{
				// extract the claim: must use the right assumption to avoid
				// exceptions such as array out of bounds...
				ValueIF claimExtractionAssumption = newPartialPathCondition;
				int newTop = (pop ? position - 1 : position);

				for (int i = 0; i < newTop; i++) {
					ValueIF ppc = ((CollectiveLoopRecordIF) queue.get(i))
							.partialPathCondition();

					if (ppc != null)
						claimExtractionAssumption = dynamicFactory.and(
								trueValue, claimExtractionAssumption, ppc);
				}

				StateIF compositeState2 = stateFactory.state(
						compositeState.modelStates(),
						claimExtractionAssumption,
						compositeState.collectiveQueue());

				claim = collectiveClaim(assertion, compositeState2);

				newRelationalPredicate = trueValue;
				newPartialPathCondition = dynamicFactory.and(trueValue,
						newPartialPathCondition, claim);
				// consider making newSnapshots null here. maybe needed?
				newRecord = stateFactory.collectiveLoopRecord(assertion,
						newSnapshots, newPartialPathCondition,
						newRelationalPredicate, newWritevarSets, isTrueBranch);
			}

			// construct new Queue....
			if (isTrueBranch) {
				// complete entry gets moved from queue to stack, no further
				// change in length
				newQueue = queueFactory.newVector(newQueueLength);
				if (newEntry) {
					for (int i = 0; i < newQueueLength - 1; i++)
						newQueue.set(i, queue.get(i));
					newQueue.set(newQueueLength - 1, newRecord);
				} else {
					if (pop) {
						// deleting entry at position-1 and replacing entry
						// at position with newRecord
						for (int i = 0; i < position - 1; i++)
							newQueue.set(i, queue.get(i));
						newQueue.set(position - 1, newRecord);
						for (int i = position; i < newQueueLength; i++)
							newQueue.set(i, queue.get(i + 1));
					} else {
						// replacing entry at position
						for (int i = 0; i < position; i++)
							newQueue.set(i, queue.get(i));
						newQueue.set(position, newRecord);
						for (int i = position + 1; i < newQueueLength; i++)
							newQueue.set(i, queue.get(i));
					}
				}
			} else {// false branch
				// need to modify the record below this one...
				int prevPosition = (pop ? position - 2 : position - 1);
				CollectiveLoopRecordIF prevRecord = (CollectiveLoopRecordIF) queue
						.get(prevPosition);

				ValueIF newPrevPartialPC = dynamicFactory.and(
						trueValue,
						prevRecord.partialPathCondition(),
						(forgetAssumptions ? dynamicFactory.and(trueValue,
								claim, guard) : newPartialPathCondition));
				CollectiveLoopRecordIF newPrevRecord = stateFactory
						.collectiveLoopRecord(prevRecord.assertion(),
								prevRecord.snapshots(), newPrevPartialPC,
								prevRecord.relationalPredicate(),
								prevRecord.writevarSets(),
								prevRecord.trueBranch());

				// complete entry is dequeued, decreasing stack length by 1:
				newQueueLength--;
				// removing old entry:
				newQueue = queueFactory.newVector(newQueueLength);
				if (newEntry) {
					// delete top 0 or 1 elements from queue
					for (int i = 0; i < newQueueLength - 1; i++)
						newQueue.set(i, queue.get(i));
					newQueue.set(newQueueLength - 1, newPrevRecord);
				} else {
					if (pop) {
						// remove elements at position and position-1;
						// replace element at position-2 with newPrevRecord
						for (int i = 0; i < position - 2; i++)
							newQueue.set(i, queue.get(i));
						newQueue.set(position - 2, newPrevRecord);
						for (int i = position - 1; i < newQueueLength; i++)
							newQueue.set(i, queue.get(i + 2));
					} else {
						// remove element at position only
						// replace element at position-1 with newPrevRecord
						for (int i = 0; i < position - 1; i++)
							newQueue.set(i, queue.get(i));
						newQueue.set(position - 1, newPrevRecord);
						for (int i = position; i < newQueueLength; i++)
							newQueue.set(i, queue.get(i + 1));
					}
				}
			}
		}
		newPathCondition = stateFactory.computePathCondition(newQueue);
		environment.setAssumption(newPathCondition);
		environment.setCollectiveQueue(newQueue);
		environment.setCurrentProcess(process);
		executor.execute(environment, statement);
	}

	private StateIF nextStateSimple(StateIF state, SimpleTransitionIF transition) {
		SystemEnvironmentIF environment = States.newEnvironment(modelSequence,
				stateFactory, log);
		StatementIF statement = transition.statement();
		LocationIF newLocation = statement.targetLocation();

		environment.setState(state);
		try {
			if (useLoopTechnique) {
				ValueIF guardValue = evaluator.evaluateOverride(environment,
						statement.guard());

				environment.setCurrentProcess(statement.process());
				environment.addAssumption(guardValue);
			} else {
				environment.setAssumption(transition.pathCondition());
			}
			executor.execute(environment, transition.statement());
			if (useCollectiveAssertions)
				executeCollective(environment, statement.process());
			saveIfNecessary(environment, newLocation);
			return environment.state();
		} catch (ExecutionStateException error) {
			log.report(error);
		} catch (ExecutionException e) {
			log.report(e);
		} catch (ExecutionProblem problem) {
			log.report(new ExecutionException(statement, problem));
		}
		environment.setAssumption(falseValue);
		return environment.state();
	}

	private StateIF nextStateSynchronous(StateIF state,
			SynchronousTransitionIF transition) {
		SystemEnvironmentIF environment = States.newEnvironment(modelSequence,
				stateFactory, log);
		SendStatementIF send = transition.send();
		ReceiveStatementIF receive = transition.receive();

		environment.setState(state);
		if (useLoopTechnique) {
			environment.setCurrentProcess(send.process());
		}
		// no change to path condition in synchronous transition:
		// environment.setAssumption(transition.pathCondition());
		executor.execute(environment, send);
		if (useCollectiveAssertions)
			executeCollective(environment, send.process());
		if (useLoopTechnique) {
			environment.setCurrentProcess(receive.process());
		}
		executor.execute(environment, receive);
		if (useCollectiveAssertions)
			executeCollective(environment, receive.process());
		state = environment.state();
		try {
			if (requiresSaving(send.targetLocation())
					|| requiresSaving(receive.targetLocation()))
				save(environment);
		} catch (ExecutionStateException error) {
			log.report(error);
			environment.setAssumption(falseValue);
		}
		return environment.state();
	}

	public boolean onStack(StateIF state) {
		return state.onStack();
	}

	public void printAllStatesLong(PrintWriter out) {
		for (StateIF state : stateFactory.store()) {
			printStateLong(out, state);
			out.println();
		}
	}

	public void printAllStatesShort(PrintWriter out) {
		for (StateIF state : stateFactory.store()) {
			printStateShort(out, state);
			out.println();
		}
	}

	public void printStateLong(PrintWriter out, StateIF state) {
		SystemEnvironmentIF environment = States.newEnvironment(modelSequence,
				stateFactory, log);

		environment.setState(state);
		environment.printStateLong(out, "");
		environment.setState(null);
	}

	public void printStateShort(PrintWriter out, StateIF state) {
		out.print("State " + state.instanceId());
	}

	public void printTransitionLong(PrintWriter out, TransitionIF transition) {
		transition.print(out);
	}

	public void printTransitionShort(PrintWriter out, TransitionIF transition) {
		transition.print(out);
	}

	public boolean seen(StateIF state) {
		return state.seen();
	}

	public void setOnStack(StateIF state, boolean value) {
		state.setOnStack(value);
		if (value) {
			if (firstNDStateOnStack == null && state.isNonDeterministic()) {
				firstNDStateOnStack = state;
			}
		} else if (firstNDStateOnStack == state) {
			firstNDStateOnStack = null;
		}
	}

	public void setSeen(StateIF state, boolean value) {
		state.setSeen(value);
	}

	/**
	 * Simplifies state. If useLoopTechnique, also canonicalizes the "Y"
	 * symbolic constants.
	 */
	// do not simplify the permanent pc....which is now in entry 0 of queue.
	private StateIF simplify(StateIF state) throws ExecutionStateException {
		DynamicSimplifierIF dynamicSimplifier;

		try {
			if (useLoopTechnique) {
				dynamicSimplifier = dynamicFactory.simplifier(
						state.permanentPathCondition(),
						dynamicFactory.simplifyCache());
			} else {
				dynamicSimplifier = dynamicFactory.simplifier(
						state.pathCondition(), dynamicFactory.simplifyCache());
			}
			StateIF newState = stateSimplifier.simplify(dynamicSimplifier,
					state);

			if (useLoopTechnique)
				newState = canonicalizeSymbolicConstants(newState);
			return newState;
		} catch (DynamicException e) {
			throw new ExecutionStateException(state.locations(), e,
					Certainty.NONE);
		}
	}

	/**
	 * Takes a state and returns the ValueIF path condition for that state.
	 */
	public ValueIF getPathCondition(StateIF state) {
		SystemEnvironmentIF environment = States.newEnvironment(modelSequence,
				stateFactory, log);
		environment.setState(state);
		return environment.getAssumption();
	}

	/**
	 * Returns a map from SharedVariableIF variables to their ValueIF values.
	 * These values could be concrete or symbolic constants.
	 */
	@Override
	public Map<SharedVariableIF, ValueIF> getSharedVariableValues(
			Map<SharedVariableIF, ModelCellIF> map, StateIF state) {
		SystemEnvironmentIF environment = States.newEnvironment(modelSequence,
				stateFactory, log);
		environment.setState(state);

		Map<SharedVariableIF, ValueIF> valueMap = new HashMap<SharedVariableIF, ValueIF>();
		Set<Entry<SharedVariableIF, ModelCellIF>> entrySet = map.entrySet();

		for (Entry<SharedVariableIF, ModelCellIF> entry : entrySet) {
			valueMap.put((SharedVariableIF) entry.getKey(),
					environment.valueOf(entry.getValue()));
		}
		return valueMap;
	}

	private Vector<SymbolicConstantIF> collectibleSymbolicConstants(
			StateIF state) {
		Vector<SymbolicConstantIF> result = new Vector<SymbolicConstantIF>();
		Collection<SymbolicConstantIF> symbolicConstants = stateFactory
				.symbolicConstants(state);

		for (SymbolicConstantIF symbolicConstant : symbolicConstants) {
			String name = symbolicConstant.name();

			if (name.charAt(0) == 'Y') {
				result.add(symbolicConstant);
			}
		}
		return result;
	}

	public StateIF canonicalizeSymbolicConstants(StateIF state)
			throws DynamicException, ExecutionStateException {
		Vector<SymbolicConstantIF> collectionVector = collectibleSymbolicConstants(state);
		int numCollectibles = collectionVector.size();
		Map<SymbolicConstantIF, SymbolicConstantIF> symbolicConstantMap = new LinkedHashMap<SymbolicConstantIF, SymbolicConstantIF>();

		for (int i = 0; i < numCollectibles; i++) {
			SymbolicConstantIF x = collectionVector.elementAt(i);
			String name = "Y" + i;

			if (!x.name().equals(name)) {
				SymbolicConstantIF y = universe.getOrCreateSymbolicConstant(
						name, x.type());

				symbolicConstantMap.put(x, y);
				if (verbose) {
					out.println("Substituting: " + x + " -> " + y);
					out.flush();
				}
			}
		}
		if (symbolicConstantMap.isEmpty()) {
			return state;
		} else {
			DynamicSimplifierIF dynamicSimplifier = loopConstantSimplifier(symbolicConstantMap);

			state = loopStateSimplifier.simplify(dynamicSimplifier, state);
			return state;
		}
	}

	/**
	 * Returns an instance of DynamicSimplifierIF that replaces old loop
	 * symbolic constants (the Y_i) with the new ones.
	 */
	private DynamicSimplifierIF loopConstantSimplifier(
			Map<SymbolicConstantIF, SymbolicConstantIF> symbolicConstantMap) {
		DynamicSimplifierIF dynamicSimplifier = loopConstantCacheMap
				.get(symbolicConstantMap);

		if (dynamicSimplifier == null) {
			MorphicSimplifierCacheIF heapCache = dynamicFactory
					.newSimpleCache();
			ValueSubstituterIF substituter = dynamicFactory
					.valueSubstituterFromSymbolicConstantMap(symbolicConstantMap);

			dynamicSimplifier = dynamicFactory.simplifier(substituter,
					heapCache);
		}
		return dynamicSimplifier;
	}

	private int indexOf(SymbolicConstantIF x) {
		String name = x.name();
		String substring = name.substring(1);
		int result = new Integer(substring);

		return result;
	}

	@Override
	public Map<SharedVariableIF, ValueIF> getInputVariableValues(StateIF state) {
		// TODO Auto-generated method stub
		return null;
	}

	@Override
	public Map<SharedVariableIF, ValueIF> getOutputVariableValues(StateIF state) {
		// TODO Auto-generated method stub
		return null;
	}

}