ModelEnvironment.java

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

import java.io.PrintWriter;
import java.util.Collection;
import java.util.HashMap;
import java.util.HashSet;
import java.util.LinkedHashSet;
import java.util.Map;
import java.util.Set;

import edu.udel.cis.vsl.tass.config.RunConfiguration;
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.cell.CellIF;
import edu.udel.cis.vsl.tass.dynamic.IF.cell.HeapCellIF;
import edu.udel.cis.vsl.tass.dynamic.IF.cell.LocalCellIF;
import edu.udel.cis.vsl.tass.dynamic.IF.cell.ModelCellIF;
import edu.udel.cis.vsl.tass.dynamic.IF.cell.ProcessCellIF;
import edu.udel.cis.vsl.tass.dynamic.IF.cell.SharedCellIF;
import edu.udel.cis.vsl.tass.dynamic.IF.simplify.DynamicSimplifierIF;
import edu.udel.cis.vsl.tass.dynamic.IF.type.ReferenceValueTypeIF;
import edu.udel.cis.vsl.tass.dynamic.IF.value.MessageIF;
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.model.IF.FunctionIF;
import edu.udel.cis.vsl.tass.model.IF.ModelIF;
import edu.udel.cis.vsl.tass.model.IF.ProcessIF;
import edu.udel.cis.vsl.tass.model.IF.location.LocationIF;
import edu.udel.cis.vsl.tass.model.IF.scope.LocalScopeIF;
import edu.udel.cis.vsl.tass.model.IF.variable.LocalVariableIF;
import edu.udel.cis.vsl.tass.model.IF.variable.ProcessVariableIF;
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.MorphicVector;
import edu.udel.cis.vsl.tass.morph.MorphicVectorFactory;
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.LogIF;
import edu.udel.cis.vsl.tass.state.IF.FrameIF;
import edu.udel.cis.vsl.tass.state.IF.ModelEnvironmentIF;
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.ScopeStateIF;
import edu.udel.cis.vsl.tass.util.Sourceable;
import edu.udel.cis.vsl.tass.util.TASSInternalException;

/**
 * An implementation of EnvironmentIF using the ModelState class. A State object
 * encodes the state of one MPI model. Wrapping the state in this environment
 * class allows the information encoded in the State object to be interpreted.
 * The modification methods actually produce new ModelStates, changing the state
 * field of the environment, as the ModelStates are immutable.
 * 
 * The path condition is not part of the model state. Hence the methods that
 * involve setting/getting the assumption throw exceptions.
 * 
 * Message queues: insert on left (lower index), remove on right (higher index).
 * 
 * @author siegel
 * 
 */
public class ModelEnvironment implements ModelEnvironmentIF {

	private ModelIF model;
	private int numProcs;
	private DynamicFactoryIF dynamicFactory;
	private ModelStateFactory modelStateFactory;
	private ModelState state;
	private LogIF log;
	private ProcessStateSimplifier heapSimplifier;
	private ValueIF trueValue;
	private ValueIF zero; // integer zero

	// experimental
	private boolean canonicalizeHeap = true;

	public ModelEnvironment(ModelIF model, ModelStateFactoryIF stateFactory,
			LogIF log) {
		this.model = model;
		this.log = log;
		numProcs = model.numProcs();
		this.dynamicFactory = stateFactory.dynamicFactory();
		this.trueValue = dynamicFactory.trueValue();
		this.zero = dynamicFactory.zero();
		this.modelStateFactory = (ModelStateFactory) stateFactory;
		this.heapSimplifier = modelStateFactory.processStateFactory()
				.simplifier();
	}

	@Override
	public ModelIF model() {
		return model;
	}

	public RunConfiguration configuration() {
		return dynamicFactory.configuration();
	}

	@Override
	public void setState(ModelStateIF state) {
		this.state = (ModelState) state;
	}

	@Override
	public ModelStateIF state() {
		return state;
	}

	public MorphicArrayFactory<ValueIF> valueArrayFactory() {
		return dynamicFactory.valueArrayFactory();
	}

	public MorphicVectorFactory<ValueIF> valueVectorFactory() {
		return dynamicFactory.valueVectorFactory();
	}

	public MorphicArrayFactory<ProcessStateIF> processStateArrayFactory() {
		return modelStateFactory.processStateArrayFactory();
	}

	public MorphicVectorFactory<FrameIF> stackFactory() {
		return modelStateFactory.processStateFactory().stackFactory();
	}

	public MorphicVectorFactory<ScopeStateIF> scopeStateVectorFactory() {
		return modelStateFactory.frameFactory().scopeStateVectorFactory();
	}

	public MorphicVectorFactory<MessageIF> bufferFactory() {
		return dynamicFactory.messageVectorFactory();
	}

	/* Variables */

	@Override
	public ValueIF valueOf(ModelCellIF cell) {
		switch (cell.scope()) {
		case SHARED:
			return valueOfShared((SharedCellIF) cell);
		case PROCESS:
			return valueOfProcessCell((ProcessCellIF) cell);
		case LOCAL:
			return valueOfLocal((LocalCellIF) cell);
		case HEAP:
			return valueOfHeap((HeapCellIF) cell);
		default:
			throw new IllegalArgumentException(
					"Unknown dynamic variable kind:\n" + cell);
		}
	}

	private ValueIF valueOfShared(SharedCellIF cell) {
		return state.sharedValue(cell.sharedVariableId());
	}

	private ValueIF valueOfProcessCell(ProcessCellIF cell) {
		return state.processState(cell.process().pid()).globalValue(
				cell.processVariableId());
	}

	// check that variable is in scope...
	// do you want to allow references to variables deep in stack?
	// get variableScope
	// get current location in process, get locationScope
	// check locationScope is descendant of variableScope
	// need to find index of variableScope in frame.scopeStates
	// need method int function.depth(scope). outermost function scope has depth
	// 0.

	private ValueIF valueOfLocal(LocalCellIF cell) {
		LocalVariableIF variable = cell.variable();
		LocalScopeIF variableScope = variable.scope();
		int id = variable.idInScope();
		int stackPosition = cell.stackIndex();
		FunctionIF function = variable.scope().function();
		ProcessIF process = function.process();
		ProcessStateIF processState = state.processState(process.pid());
		FrameIF frame = processState.frame(stackPosition);
		LocationIF location = frame.location();
		LocalScopeIF locationScope = location.scope();
		int scopeIndex = variableScope.depth();
		ScopeStateIF scopeState;
		ValueIF value;

		// the following checks that the function associated to the frame
		// at position in stack recorded in cell is the same as the function
		// containing the variable. If this fails, something is inconsistent
		// in the state, and there is an internal TASS error...
		if (!frame.function().equals(function))
			throw new RuntimeException("Evaluating local variable " + variable
					+ ": expected function " + function + " but got "
					+ frame.function() + " in stack position " + stackPosition);
		// check the variable is in scope. this should probably be
		// an ExecutionException...
		if (!model.modelFactory().isDescendantOf(locationScope, variableScope))
			throw new RuntimeException(
					"Attempt to read variable out of scope: variable "
							+ variable + ", location " + location.getSource());
		scopeState = frame.scopeStates().get(scopeIndex);
		value = scopeState.values().get(id);
		return value;
	}

	private ValueIF valueOfHeap(HeapCellIF cell) {
		return state.processState(cell.process().pid()).heapValue(
				cell.heapIndex());
	}

	@Override
	public void setValue(ModelCellIF cell, ValueIF value) {
		switch (cell.scope()) {
		case SHARED:
			setValueShared((SharedCellIF) cell, value);
			break;
		case PROCESS:
			setValueProcess((ProcessCellIF) cell, value);
			break;
		case LOCAL:
			setValueLocal((LocalCellIF) cell, value);
			break;
		case HEAP:
			setValueHeap((HeapCellIF) cell, value);
			break;
		default:
			throw new IllegalArgumentException(
					"Unknown dynamic variable kind:\n" + cell);
		}

	}

	private void setValueShared(SharedCellIF cell, ValueIF value) {
		int id = cell.sharedVariableId();
		MorphicArray<ValueIF> sharedValues = state.sharedValues();

		if (!sharedValues.isCommitted()) {
			sharedValues.set(id, value);
		} else {
			sharedValues = valueArrayFactory().newArray(sharedValues);
			sharedValues.set(id, value);
			if (!state.isCommitted()) {
				state.setSharedValues(sharedValues);
			} else {
				state = modelStateFactory.newState(state.processStates(),
						sharedValues, state.buffer());
			}
		}
	}

	private void setValueProcess(ProcessCellIF cell, ValueIF value) {
		int pid = cell.process().pid();
		int vid = cell.processVariableId();
		MorphicArray<ProcessStateIF> processStates = state.processStates();
		ProcessState processState = (ProcessState) processStates.get(pid);
		MorphicArray<ValueIF> globalValues = processState.globalValues();

		if (!globalValues.isCommitted()) {
			globalValues.set(vid, value);
		} else {
			globalValues = valueArrayFactory().newArray(globalValues);
			globalValues.set(vid, value);
			if (!processState.isCommitted()) {
				processState.setGlobalValues(globalValues);
			} else {
				processState = modelStateFactory.newProcessState(globalValues,
						processState.heap(), processState.stack());
				if (!processStates.isCommitted()) {
					processStates.set(pid, processState);
				} else {
					processStates = processStateArrayFactory().newArray(
							processStates);
					processStates.set(pid, processState);
					if (!state.isCommitted()) {
						state.setProcessStates(processStates);
					} else {
						state = modelStateFactory.newState(processStates,
								state.sharedValues(), state.buffer());
					}
				}
			}
		}
	}

	private void setValueLocal(LocalCellIF cell, ValueIF value) {
		LocalVariableIF variable = cell.variable();
		int vid = cell.localID();
		int stackPosition = cell.stackIndex();
		FunctionIF function = variable.scope().function();
		ProcessIF process = function.process();
		int pid = process.pid();
		MorphicArray<ProcessStateIF> processStates = state.processStates();
		ProcessState processState = (ProcessState) processStates.get(pid);
		MorphicVector<FrameIF> stack = processState.stack();
		Frame frame = (Frame) stack.get(stackPosition);
		LocalScopeIF variableScope = variable.scope();
		MorphicVector<ScopeStateIF> scopeStates = frame.scopeStates();
		int scopeIndex = variableScope.depth();
		ScopeState scopeState = (ScopeState) scopeStates.get(scopeIndex);
		MorphicArray<ValueIF> values = scopeState.values();

		if (!values.isCommitted()) {
			values.set(vid, value);
		} else {
			values = valueArrayFactory().newArray(values);
			values.set(vid, value);
			if (!scopeState.isCommitted()) {
				scopeState.setValues(values);
			} else {
				scopeState = modelStateFactory.newScopeState(
						scopeState.scope(), values);
				if (!scopeStates.isCommitted()) {
					scopeStates.set(scopeIndex, scopeState);
				} else {
					scopeStates = scopeStateVectorFactory().newVector(
							scopeStates);
					scopeStates.set(scopeIndex, scopeState);
					if (!frame.isCommitted()) {
						frame.setScopeStates(scopeStates);
					} else {
						frame = modelStateFactory.newFrame(frame.location(),
								scopeStates);
						if (!stack.isCommitted()) {
							stack.set(stackPosition, frame);
						} else {
							stack = stackFactory().newVector(stack);
							stack.set(stackPosition, frame);
							if (!processState.isCommitted()) {
								processState.setStack(stack);
							} else {
								processState = modelStateFactory
										.newProcessState(
												processState.globalValues(),
												processState.heap(), stack);
								if (!processStates.isCommitted()) {
									processStates.set(pid, processState);
								} else {
									processStates = processStateArrayFactory()
											.newArray(processStates);
									processStates.set(pid, processState);
									if (!state.isCommitted()) {
										state.setProcessStates(processStates);
									} else {
										state = modelStateFactory.newState(
												processStates,
												state.sharedValues(),
												state.buffer());
									}
								}
							}
						}
					}
				}
			}
		}
	}

	private void setValueHeap(HeapCellIF heapVariable, ValueIF value) {
		int pid = heapVariable.process().pid();
		int heapIndex = heapVariable.heapIndex();
		MorphicArray<ProcessStateIF> processStates = state.processStates();
		ProcessState processState = (ProcessState) processStates.get(pid);
		MorphicVector<ValueIF> heap = processState.heap();

		if (!heap.isCommitted()) {
			heap.setExtend(heapIndex, value);
		} else {
			heap = valueVectorFactory().newVector(heap);
			heap.setExtend(heapIndex, value);
			if (!processState.isCommitted()) {
				processState.setHeap(heap);
			} else {
				processState = modelStateFactory
						.newProcessState(processState.globalValues(), heap,
								processState.stack());
				if (!processStates.isCommitted()) {
					processStates.set(pid, processState);
				} else {
					processStates = processStateArrayFactory().newArray(
							processStates);
					processStates.set(pid, processState);
					if (!state.isCommitted()) {
						state.setProcessStates(processStates);
					} else {
						state = modelStateFactory.newState(processStates,
								state.sharedValues(), state.buffer());
					}
				}
			}
		}
	}

	/* Call stacks */

	@Override
	public boolean emptyStack(ProcessIF process) {
		return state.processState(process.pid()).stackSize() == 0;
	}

	@Override
	public int stackSize(ProcessIF process) {
		return state.processState(process.pid()).stackSize();
	}

	@Override
	public void pop(ProcessIF process) {
		MorphicArray<ProcessStateIF> processStates = state.processStates();
		int pid = process.pid();
		ProcessState processState = (ProcessState) processStates.get(pid);
		MorphicVector<FrameIF> stack = processState.stack();

		if (!stack.isCommitted()) {
			stack.pop();
		} else {
			stack = stackFactory().newVector(stack);
			stack.pop();
			if (!processState.isCommitted()) {
				processState.setStack(stack);
			} else {
				processState = modelStateFactory
						.newProcessState(processState.globalValues(),
								processState.heap(), stack);
				if (!processStates.isCommitted()) {
					processStates.set(pid, processState);
				} else {
					processStates = processStateArrayFactory().newArray(
							processStates);
					processStates.set(pid, processState);
					if (!state.isCommitted()) {
						state.setProcessStates(processStates);
					} else {
						state = modelStateFactory.newState(processStates,
								state.sharedValues(), state.buffer());
					}
				}
			}
		}
	}

	/**
	 * Note that the new local variables are not initialized in any way: the
	 * values associated to them are all null.
	 */
	@Override
	public void push(ProcessIF process, LocationIF location) {
		MorphicArray<ProcessStateIF> processStates = state.processStates();
		int pid = process.pid();
		ProcessState processState = (ProcessState) processStates.get(pid);
		MorphicVector<FrameIF> stack = processState.stack();
		LocalScopeIF newScope = location.scope();
		int numScopes = newScope.depth() + 1;
		MorphicVector<ScopeStateIF> scopeStates = scopeStateVectorFactory()
				.newVector(numScopes);
		Frame newFrame;
		LocalScopeIF scope = newScope;

		for (int i = numScopes - 1; i >= 0; i--) {
			int numVariables = scope.numVariables();
			MorphicArray<ValueIF> localValues = valueArrayFactory().newArray(
					numVariables);
			ScopeState scopeState = modelStateFactory.newScopeState(scope,
					localValues);

			scopeStates.set(i, scopeState);
			if (i > 0)
				scope = (LocalScopeIF) scope.parent();
		}
		newFrame = modelStateFactory.newFrame(location, scopeStates);
		if (!stack.isCommitted()) {
			stack.push(newFrame);
		} else {
			stack = stackFactory().newVector(stack);
			stack.push(newFrame);
			if (!processState.isCommitted()) {
				processState.setStack(stack);
			} else {
				processState = modelStateFactory
						.newProcessState(processState.globalValues(),
								processState.heap(), stack);
				if (!processStates.isCommitted()) {
					processStates.set(pid, processState);
				} else {
					processStates = processStateArrayFactory().newArray(
							processStates);
					processStates.set(pid, processState);
					if (!state.isCommitted()) {
						state.setProcessStates(processStates);
					} else {
						state = modelStateFactory.newState(processStates,
								state.sharedValues(), state.buffer());
					}
				}
			}
		}
	}

	/* Locations */

	private LocationIF location(int pid) {
		ProcessStateIF processState = state.processState(pid);
		int stackSize = processState.stackSize();

		return (stackSize == 0 ? null : processState.frame(stackSize - 1)
				.location());
	}

	@Override
	public LocationIF location(ProcessIF process) {
		return location(process.pid());
	}

	@Override
	public int setLocation(ProcessIF process, LocationIF location) {
		MorphicArray<ProcessStateIF> processStates = state.processStates();
		int pid = process.pid();
		ProcessState processState = (ProcessState) processStates.get(pid);
		MorphicVector<FrameIF> stack = processState.stack();
		int stackSize = stack.size();
		Frame frame = (Frame) processState.frame(stackSize - 1);
		LocationIF oldLocation = frame.location();
		LocalScopeIF oldScope = oldLocation.scope();
		LocalScopeIF newScope = location.scope();
		FunctionIF function = location.function();
		FunctionIF oldFunction = oldLocation.function();
		MorphicVector<ScopeStateIF> scopeStates = frame.scopeStates();
		MorphicVector<ScopeStateIF> newScopeStates;
		int result = 0;

		if (!function.equals(oldFunction))
			throw new TASSInternalException(
					"Attempt to setLocation to location in different function:\n"
							+ oldFunction + "\n" + function);
		if (oldScope.equals(newScope)) {
			newScopeStates = scopeStates;
		} else {
			LocalScopeIF joinScope = (LocalScopeIF) model.modelFactory().join(
					oldScope, newScope);
			LocalScopeIF scope = newScope;
			int joinDepth = joinScope.depth();
			int newDepth = newScope.depth();

			result = newDepth - joinDepth;
			if (scopeStates.isCommitted()) {
				MorphicVectorFactory<ScopeStateIF> scopeStateVectorFactory = modelStateFactory
						.frameFactory().scopeStateVectorFactory();

				newScopeStates = scopeStateVectorFactory.newVector(scopeStates);
			} else {
				newScopeStates = scopeStates;
			}
			newScopeStates.setSize(newDepth + 1);
			for (int i = newDepth; i > joinDepth; i--) {
				int numVariables = scope.numVariables();
				MorphicArray<ValueIF> localValues = valueArrayFactory()
						.newArray(numVariables);
				ScopeStateIF newScopeState = modelStateFactory.newScopeState(
						scope, localValues);

				newScopeStates.set(i, newScopeState);
				scope = (LocalScopeIF) scope.parent();
			}
		}
		if (!frame.isCommitted()) {
			frame.setLocation(location);
			frame.setScopeStates(newScopeStates);
		} else {
			frame = modelStateFactory.newFrame(location, newScopeStates);
			if (!stack.isCommitted()) {
				stack.set(stackSize - 1, frame);
			} else {
				stack = stackFactory().newVector(stack);
				stack.set(stackSize - 1, frame);
				if (!processState.isCommitted()) {
					processState.setStack(stack);
				} else {
					processState = modelStateFactory.newProcessState(
							processState.globalValues(), processState.heap(),
							stack);
					if (!processStates.isCommitted()) {
						processStates.set(pid, processState);
					} else {
						processStates = processStateArrayFactory().newArray(
								processStates);
						processStates.set(pid, processState);
						if (!state.isCommitted()) {
							state.setProcessStates(processStates);
						} else {
							state = modelStateFactory.newState(processStates,
									state.sharedValues(), state.buffer());
						}
					}
				}
			}
		}
		return result;
	}

	/* Messages */

	@Override
	public boolean hasMessage(ProcessIF source, ProcessIF destination,
			ValueIF tag) throws ExecutionProblem {
		for (MessageIF message : state.buffer()) {
			if (match(message.source(), message.destination(), message.tag(),
					source, destination, tag))
				return true;
		}
		return false;
	}

	@Override
	public MessageIF probe(ProcessIF source, ProcessIF destination, ValueIF tag)
			throws ExecutionProblem {
		MorphicVector<MessageIF> buffer = state.buffer();
		int length = buffer.size();

		for (int i = length - 1; i >= 0; i--) {
			MessageIF message = buffer.get(i);

			if (match(message.source(), message.destination(), message.tag(),
					source, destination, tag))
				return message;
		}
		return null;
	}

	/** Neither argument can be null */
	@Override
	public int numMessages(ProcessIF source, ProcessIF destination) {
		MorphicVector<MessageIF> buffer = state.buffer();
		int numMessages = buffer.size();

		for (int i = 0; i < numMessages; i++) {
			MessageIF message = buffer.get(i);
			int j;

			if (precedes(source, destination, message.source(),
					message.destination()))
				return 0;
			if (message.source() == source
					&& message.destination() == destination) {
				for (j = i + 1; j < numMessages; j++) {
					message = buffer.get(j);
					if (message.source() != source
							|| message.destination() != destination)
						break;
				}
				return j - i;
			}
		}
		return 0;
	}

	@Override
	public int numMessages() {
		return state.buffer().size();
	}

	@Override
	public int numMessages(ModelIF model) {
		assert model == this.model;
		return numMessages();
	}

	// TODO: this is where a linked list would be nice instead of a
	// vector...
	@Override
	public void enqueue(MessageIF message) {
		ProcessIF source = message.source();
		ProcessIF destination = message.destination();
		MorphicVector<MessageIF> buffer = state.buffer();
		int numMessages = buffer.size();
		int i;

		if (!buffer.isCommitted()) {
			for (i = 0; i < numMessages; i++) {
				MessageIF bufferedMessage = buffer.get(i);

				if (!precedes(bufferedMessage.source(),
						bufferedMessage.destination(), source, destination)) {
					break;
				}
			}
			for (int j = numMessages; j > i; j--) {
				buffer.setExtend(j, buffer.get(j - 1));
			}
			buffer.setExtend(i, message);
		} else {
			MorphicVector<MessageIF> newBuffer = bufferFactory().newVector(
					numMessages + 1);

			for (i = 0; i < numMessages; i++) {
				MessageIF bufferedMessage = buffer.get(i);

				if (!precedes(bufferedMessage.source(),
						bufferedMessage.destination(), source, destination)) {
					break;
				}
				newBuffer.set(i, bufferedMessage);
			}
			newBuffer.set(i, message);
			while (i < numMessages) {
				newBuffer.set(i + 1, buffer.get(i));
				i++;
			}
			if (!state.isCommitted()) {
				state.setBuffer(newBuffer);
			} else {
				state = modelStateFactory.newState(state.processStates(),
						state.sharedValues(), newBuffer);
			}
		}
	}

	@Override
	public MessageIF dequeue(ProcessIF source, ProcessIF destination,
			ValueIF tag) throws ExecutionProblem {
		MorphicVector<MessageIF> buffer = state.buffer();
		int newLength = buffer.size() - 1;

		if (!buffer.isCommitted()) {
			MessageIF nextMessage = null;

			for (int i = newLength; i >= 0; i--) {
				MessageIF message = buffer.get(i);

				buffer.set(i, nextMessage);
				if (match(message.source(), message.destination(),
						message.tag(), source, destination, tag)) {
					buffer.setSize(newLength);
					return message;
				}
				nextMessage = message;
			}
		} else {
			MorphicVector<MessageIF> newBuffer = bufferFactory().newVector(
					newLength);

			for (int i = newLength; i >= 0; i--) {
				MessageIF message = buffer.get(i);

				if (match(message.source(), message.destination(),
						message.tag(), source, destination, tag)) {
					for (int j = 0; j < i; j++)
						newBuffer.set(j, buffer.get(j));
					for (int j = i; j < newLength; j++)
						newBuffer.set(j, buffer.get(j + 1));
					if (!state.isCommitted()) {
						state.setBuffer(newBuffer);
					} else {
						state = modelStateFactory.newState(
								state.processStates(), state.sharedValues(),
								newBuffer);
					}
					return message;
				}
			}
		}
		throw new RuntimeException("No matching message found");
	}

	/** None of the parameters can be null */
	private boolean precedes(ProcessIF source1, ProcessIF dest1,
			ProcessIF source2, ProcessIF dest2) {
		return source1.pid() < source2.pid()
				|| (source1.pid() == source2.pid() && dest1.pid() < dest2.pid());
	}

	private boolean match(ProcessIF source1, ProcessIF dest1, ValueIF tag1,
			ProcessIF source2, ProcessIF dest2, ValueIF tag2)
			throws ExecutionProblem {
		try {
			if (source2 != null && source1 != source2)
				return false;
			if (dest1 != dest2)
				return false;
			if (tag2 == null) { // any tag
				// can only match nonnegative tag1 because negative
				// tags are used for collective operations
				return !dynamicFactory.isValid(trueValue,
						dynamicFactory.lessThan(trueValue, tag1, zero));
			} else {
				ValueIF equalExpression = dynamicFactory.equals(trueValue,
						tag1, tag2);
				boolean equalTags = dynamicFactory.isValid(trueValue,
						equalExpression);

				if (equalTags) {
					return true;
				} else {
					boolean nequalTags = dynamicFactory.isValid(trueValue,
							dynamicFactory.not(trueValue, equalExpression));

					// TODO: split into two cases?

					if (!nequalTags)
						throw new ExecutionProblem(ErrorKind.COMMUNICATION,
								Certainty.NONE,
								"Unable to determine whether tags match: "
										+ tag1 + " vs. " + tag2);
					return false;
				}
			}
		} catch (DynamicException error) {
			throw new ExecutionProblem(error, Certainty.NONE);
		}
	}

	private void printVariableValue(PrintWriter out, String prefix,
			ModelCellIF cell) {
		ValueIF value = null;
		String valueString;

		if (cell != null) {
			value = valueOf(cell);
			if (value != null)
				valueString = value.typedString();
			else
				valueString = "null";
			out.println(prefix + cell + " = " + valueString + ";");
			out.flush();
		}
	}

	@Override
	public void printStateLong(PrintWriter out, String prefix) {
		MorphicVector<MessageIF> buffer = state.buffer();

		out.println(prefix + "begin model state (mid=" + model.id() + ", name="
				+ model.name() + ") " + state.descriptor());
		out.println(prefix + "  begin shared variables "
				+ state.sharedValues().descriptor());
		for (VariableIF variable : model.scope().variables()) {
			printVariableValue(out, prefix + "    ",
					dynamicFactory.sharedCell((SharedVariableIF) variable));
		}
		out.println(prefix + "  end shared variables;");
		for (int i = 0; i < numProcs; i++) {
			ProcessIF process = model.process(i);
			ProcessStateIF processState = state.processState(process.pid());
			// FrameIF[] stack = processState.stack();
			int stackSize = processState.stackSize();
			int heapSize = heapSize(process);

			out.println(prefix + "  begin process " + i + " "
					+ processState.descriptor());
			out.println(prefix + "    process state id : "
					+ processState.instanceId());
			if (!process.scope().variables().isEmpty()) {
				out.println(prefix + "    begin global variables "
						+ processState.globalValues().descriptor());
				for (VariableIF variable : process.scope().variables()) {
					printVariableValue(out, prefix + "      ",
							dynamicFactory
									.processCell((ProcessVariableIF) variable));
				}
				out.println(prefix + "    end global variables;");
			}
			if (heapSize > 0) {
				out.println(prefix + "    begin heap variables "
						+ processState.heap().descriptor());
				for (int j = 0; j < heapSize; j++) {
					printVariableValue(out, prefix + "      ",
							dynamicFactory.heapCell(process, j));
				}
				out.println(prefix + "    end heap variables;");
			}
			for (int j = stackSize - 1; j >= 0; j--) {
				FrameIF frame = processState.frame(j);
				LocationIF location = frame.location();
				FunctionIF function = location.function();

				out.println(prefix + "    begin stack frame " + j + " "
						+ frame.descriptor());
				out.println(prefix + "      function : " + function + ";");
				out.println(prefix + "      location : " + location.id() + ";");

				for (ScopeStateIF scopeState : frame.scopeStates()) {
					LocalScopeIF scope = (LocalScopeIF) scopeState.scope();
					MorphicArray<ValueIF> values = scopeState.values();

					out.println(prefix + "      begin scope " + scope.localId());
					for (VariableIF variable : scope.variables()) {
						ValueIF value = values.get(variable.idInScope());

						out.println(prefix + "        " + variable + " = "
								+ value + " ("
								+ (value == null ? "null" : value.valueType())
								+ ");");
					}
					out.println(prefix + "      end scope " + scope.localId());
				}
				out.println(prefix + "    end stack frame " + j + ";");
			}
			out.println(prefix + "  end process " + i + ";");
		}
		if (buffer.size() > 0) {
			out.println(prefix + "  begin buffer " + buffer.descriptor());
			for (int i = 0; i < buffer.size(); i++) {
				MessageIF message = buffer.get(i);

				out.println(prefix + "    begin message " + i + " "
						+ message.descriptor());
				out.println(prefix + "      source      = "
						+ message.source().pid() + ";");
				out.println(prefix + "      destination = "
						+ message.destination().pid() + ";");
				out.println(prefix + "      tag         = " + message.tag()
						+ ";");
				out.println(prefix + "      data        = " + message.data()
						+ ";");
				out.println(prefix + "    end message " + i + ";");
			}
			out.println(prefix + "  end buffer;");
		}
		out.println(prefix + "end model state (mid=" + model.id() + ", name="
				+ model.name() + ")");
		out.flush();
	}

	@Override
	public void addAssumption(ValueIF predicate) {
		throw new UnsupportedOperationException(
				"ModelEnvironment does not contain path condition");
	}

	@Override
	public ValueIF getAssumption() {
		throw new UnsupportedOperationException(
				"ModelEnvironment does not contain path condition");
	}

	@Override
	public void setAssumption(ValueIF predicate) {
		throw new UnsupportedOperationException(
				"ModelEnvironment does not contain path condition");
	}

	/**
	 * Puts heap for the given process into a canonical form. Gets rid of
	 * "freed" heap cells and performs a garbage collection, updating all
	 * references to the heap. References to freed heap cells are replaced with
	 * undefined values.
	 * 
	 * The sourceable element is used for reporting memory leaks.
	 * 
	 * Improvement: this could be optimized substantially by only performing
	 * substitutions on those values that require it, only updating the part of
	 * the state that needs to be updated, etc.
	 * 
	 * TODO: in addition, the symbolic constants of the heap allocated arrays
	 * need to be changed to reflect their new positions in the heap. The name
	 * corresponds to the heap index.
	 * 
	 * Why can't we just rename all symbolic constants in a canonical way? As
	 * symbolic constants are introduced and disappear, they can be renamed.
	 * 
	 * What about other parts of state (outside of model state). Can return the
	 * substituter?
	 * 
	 * */

	// TODO : can be made much more efficient. If you don't change a process
	// state no need to create a new one

	// TODO: change entire heap representation to one heap per malloc statement

	// a return value of null means nothing to do (identify transform)

	public DynamicSimplifierIF canonicalizeHeap(ProcessIF process,
			Sourceable sourceable) throws ExecutionProblem {
		if (!canonicalizeHeap)
			return null;

		MorphicArray<ProcessStateIF> processStates = state.processStates();
		// int nprocs = process.model().numProcs();
		int pid = process.pid();
		ProcessStateIF processState = processStates.get(pid);

		// 1. find (a) all references to heap cells in this process, and (b) all
		// reachable, live heap cells in process...

		Set<VariableReferenceValueIF> references = new LinkedHashSet<VariableReferenceValueIF>();
		Set<HeapCellIF> newHeapCells = new LinkedHashSet<HeapCellIF>();

		computeReachableHeap(process, references, newHeapCells);

		// 2. construct new heap and mapping between old and new...

		MorphicVector<ValueIF> oldHeap = processState.heap();
		int oldHeapSize = oldHeap.size();
		int newHeapSize = newHeapCells.size();
		MorphicVector<ValueIF> newHeap = valueVectorFactory().newVector(
				newHeapSize);

		// at position i, gives the cell in the new heap that will contain
		// what was in the cell at position i in the old heap, or null
		// if that cell at position i in the old heap was unreachable
		HeapCellIF[] inverseMap = new HeapCellIF[oldHeapSize];
		int index = 0;
		boolean change = oldHeapSize != newHeapSize;

		for (HeapCellIF cell : newHeapCells) {
			HeapCellIF oldCell = dynamicFactory.heapCell(process, index);

			change = change || !cell.equals(oldCell);
			newHeap.set(index, valueOf(cell));
			inverseMap[cell.heapIndex()] = oldCell;
			index++;
		}

		// if no change, return now...

		if (!change)
			return null;

		// 2b. A live heap cell which is unreachable is a memory leak and
		// should be reported. Could store in the heap object the allocation
		// statement that created this object, and report that here for a more
		// useable error report.

		for (int i = 0; i < oldHeapSize; i++) {
			if (inverseMap[i] == null && oldHeap.get(i) != null) {
				log.report(new ExecutionException(sourceable,
						ErrorKind.MEMORY_LEAK, Certainty.PROVEABLE,
						"Memory leak detected in process " + pid
								+ " heap cell " + i + " value:\n"
								+ oldHeap.get(i)));
			}
		}

		// 3. prepare the map of old reference values to new...

		Map<ValueIF, ValueIF> substitutionMap = new HashMap<ValueIF, ValueIF>();
		DynamicSimplifierIF dynamicSimplifier;

		for (VariableReferenceValueIF oldReference : references) {
			ReferenceValueTypeIF valueType = oldReference.valueType();
			HeapCellIF oldCell = (HeapCellIF) oldReference.variable();
			HeapCellIF newCell = inverseMap[oldCell.heapIndex()];

			if (oldCell != null && !oldCell.equals(newCell)) {
				ValueIF newValue;

				if (newCell == null) {
					newValue = dynamicFactory.undefinedValue(valueType);
				} else {
					newValue = dynamicFactory
							.referenceValue(newCell, valueType);
				}
				substitutionMap.put(oldReference, newValue);
			}
		}
		dynamicSimplifier = modelStateFactory
				.heapReferenceSimplifier(substitutionMap);

		// 4. update heap and replace old references with new...

		if (!processState.isCommitted()) {
			((ProcessState) processState).setHeap(newHeap);
		} else {
			processState = modelStateFactory.newProcessState(
					processState.globalValues(), newHeap, processState.stack());
		}
		try {
			processState = heapSimplifier.simplify(dynamicSimplifier,
					processState);
		} catch (DynamicException e) {
			throw new ExecutionProblem(e, Certainty.NONE);
		}
		if (!processStates.isCommitted()) {
			processStates.set(pid, processState);
		} else {
			processStates = processStateArrayFactory().newArray(processStates);
			processStates.set(pid, processState);
			if (!state.isCommitted()) {
				state.setProcessStates(processStates);
			} else {
				state = modelStateFactory.newState(processStates,
						state.sharedValues(), state.buffer());
			}
		}
		return dynamicSimplifier;
	}

	/**
	 * Computes:
	 * 
	 * 1. The set of reachable references to heap cells in the given process.
	 * Reachability starts from any global variables or stack variable in any
	 * process. Note that these references may refer to heap cells that have
	 * been freed, so the references are invalid.
	 * 
	 * 2. The set of live (have not been freed) reachable heap cells in the
	 * process.
	 * 
	 * The found items are added to the sets references and heapCells, resp.
	 * Typically this method would be called with new empty sets for those two
	 * parameters.
	 */
	private void computeReachableHeap(ProcessIF process,
			Set<VariableReferenceValueIF> references, Set<HeapCellIF> heapCells) {
		Collection<ValueIF> seenValues = new HashSet<ValueIF>();

		// if this proves too expensive, consider starting only from
		// variables in the given process since at least for now this
		// is the only way to reach the proc's heap.

		for (ValueIF value : state.sharedValues())
			if (value.valueType().containsReferences())
				dfs(value, seenValues, references, heapCells, process);
		for (int i = 0; i < numProcs; i++) {
			ProcessStateIF processState = state.processState(i);
			int stackSize = processState.stackSize();

			for (ValueIF value : processState.globalValues())
				if (value.valueType().containsReferences())
					dfs(value, seenValues, references, heapCells, process);
			for (int j = 0; j < stackSize; j++)
				for (ScopeStateIF scopeState : processState.frame(j)
						.scopeStates())
					for (ValueIF value : scopeState.values())
						if (value != null
								&& value.valueType().containsReferences())
							dfs(value, seenValues, references, heapCells,
									process);
		}
	}

	/**
	 * Performs depth-first search of value graph, looking for references to the
	 * process' heap. Also accumulates the referenced heap cells that are live.
	 */
	private void dfs(ValueIF value, Collection<ValueIF> seenValues,
			Set<VariableReferenceValueIF> references,
			Set<HeapCellIF> heapCells, ProcessIF process) {
		Set<VariableReferenceValueIF> newReferences = dynamicFactory
				.reachableVariableReferences(value, seenValues);

		for (VariableReferenceValueIF reference : newReferences) {
			CellIF cell = reference.variable();

			// ignore literal cells...
			if (cell instanceof ModelCellIF) {
				ValueIF cellValue = valueOf((ModelCellIF) cell);

				if (cell instanceof HeapCellIF
						&& process.equals(((HeapCellIF) cell).process())) {
					references.add(reference);
					if (cellValue != null)
						heapCells.add((HeapCellIF) cell);
				}
				if (cellValue != null)
					dfs(cellValue, seenValues, references, heapCells, process);
			}
		}
	}

	@Override
	public int heapSize(ProcessIF process) {
		return state.processState(process.pid()).heap().size();
	}

	@Override
	public LocationIF[] locations() {
		LocationIF[] result = new LocationIF[numProcs];

		for (int i = 0; i < numProcs; i++)
			result[i] = location(i);
		return result;
	}

	@Override
	public boolean terminated(ProcessIF process) {
		return stackSize(process) == 0;
	}

	@Override
	public boolean terminated(ModelIF model) {
		int numProcs = model.numProcs();

		for (int i = 0; i < numProcs; i++) {
			if (!terminated(model.process(i)))
				return false;
		}
		return true;
	}
}