Environment.java

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

import java.io.PrintWriter;
import java.util.Stack;

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.ModelCellIF;
import edu.udel.cis.vsl.tass.dynamic.IF.cell.CellIF.DynamicScope;
import edu.udel.cis.vsl.tass.dynamic.IF.simplify.DynamicSimplifierIF;
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.CollectiveAssertionIF;
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.location.LocationIF;
import edu.udel.cis.vsl.tass.morph.MorphicArray;
import edu.udel.cis.vsl.tass.morph.MorphicVector;
import edu.udel.cis.vsl.tass.morph.MorphicVectorFactory;
import edu.udel.cis.vsl.tass.semantics.IF.ExecutionProblem;
import edu.udel.cis.vsl.tass.semantics.IF.LogIF;
import edu.udel.cis.vsl.tass.semantics.IF.ExecutionProblem.Certainty;
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.ModelEnvironmentIF;
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.util.Sourceable;

public class Environment implements SystemEnvironmentIF {

	private ModelSequence modelSequence;

	private StateFactory stateFactory;

	private State state;

	/**
	 * Index in queue to where modifications to pc should go. The
	 * partialPathCondition in that queue entry will be modified in the same way
	 * the regular path condition is modified during calls to setAssumption and
	 * addAssumption. This is used in the loop technique. This field is updated
	 * by invoking setCurrentProcess().
	 */
	private int loopQueueIndex = -1;

	/**
	 * The stack of indices into the collective queue representing the loops in
	 * which the current process is "in" in the current state. These could be
	 * complete or incomplete queue entries. (Complete means every process has
	 * reached that point.) Each entry will represent a "true" branch. This
	 * field is updated by invoking setCurrentProcess().
	 */
	private Stack<Integer> loopIndexStack = null;

	/**
	 * The current process that is executing. This is used in loop technique at
	 * certain points. This field is updated by invoking setCurrentProcess().
	 */
	private ProcessIF currentProcess = null;

	private ModelEnvironmentIF[] modelEnvironments;

	private DynamicFactoryIF dynamicFactory;

	private ModelStateFactory modelStateFactory;

	private MorphicVectorFactory<CollectiveRecordIF> queueFactory;

	// private MorphicArrayFactory<MorphicSet<VariableReferenceValueIF>>
	// variableSetArrayFactory;

	private int numModels;

	private StateSimplifier stateSimplifier;

	public Environment(ModelSequence modelSequence,
			StateFactoryIF stateFactory, LogIF log) {
		this.numModels = modelSequence.numModels();
		this.modelSequence = modelSequence;
		this.stateFactory = (StateFactory) stateFactory;
		this.dynamicFactory = this.stateFactory.dynamicFactory();
		this.modelStateFactory = this.stateFactory.modelStateFactory();
		this.modelEnvironments = new ModelEnvironmentIF[numModels];
		for (int i = 0; i < numModels; i++) {
			modelEnvironments[i] = new ModelEnvironment(
					modelSequence.modelWithIndex(i), modelStateFactory, log);
		}
		queueFactory = this.stateFactory.queueFactory();
		// variableSetArrayFactory =
		// this.stateFactory.variableSetArrayFactory();
		this.stateSimplifier = (StateSimplifier) stateFactory.simplifier(false);
	}

	@Override
	public void printStateLong(PrintWriter out, String prefix) {
		out.println(prefix + "begin State " + state.instanceId() + " "
				+ state.descriptor());
		out.println(prefix + "  onStack       : " + state.onStack());
		out.println(prefix + "  seen          : " + state.seen());
		out.println(prefix + "  pathCondition : " + state.pathCondition());
		if (state.collectiveQueue() != null) {
			out.println(prefix + "  begin collective queue "
					+ state.collectiveQueue().descriptor());
			for (int i = state.collectiveQueue().size() - 1; i >= 0; i--) {
				state.collectiveQueue().get(i).print(out, prefix + "    ");
			}
			out.println(prefix + "  end collective queue");
		}
		for (int i = 0; i < numModels; i++) {
			modelEnvironments[i].printStateLong(out, prefix + "  ");
		}
		out.println(prefix + "end State " + state.instanceId() + ".");
		out.flush();
	}

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

	@Override
	public void setState(StateIF state) {
		this.state = (State) state;
		if (state != null) {
			for (int i = 0; i < numModels; i++)
				modelEnvironments[i].setState(this.state.modelState(i));
		}
	}

	/**
	 * Creates and returns a new array of model states from the current model
	 * environments.
	 */
	private ModelStateIF[] getModelStates() {
		ModelStateIF[] newModelStates = new ModelStateIF[numModels];

		for (int i = 0; i < numModels; i++)
			newModelStates[i] = modelEnvironments[i].state();
		return newModelStates;
	}

	@Override
	public ModelStateIF modelState(int modelIndex) {
		return modelEnvironments[modelIndex].state();
	}

	/**
	 * Constructs and returns new state, using the model states extracted from
	 * the current model environments, and the given path condition and
	 * collective queue. This is the only method that should be used to create a
	 * new State object in this class, to ensure that there is no sharing of
	 * modelState arrays between states.
	 */
	private State newState(ValueIF pathCondition,
			MorphicVector<CollectiveRecordIF> collectiveQueue) {
		return stateFactory.state(getModelStates(), pathCondition,
				collectiveQueue);
	}

	/**
	 * If using loop technique, in addition to modifying pc, need to modify the
	 * appropriate entry in the collective queue.
	 */
	@Override
	public void addAssumption(ValueIF predicate) throws ExecutionProblem {
		MorphicVector<CollectiveRecordIF> queue = collectiveQueue();
		ValueIF pathCondition = dynamicFactory.and(dynamicFactory.trueValue(),
				state.pathCondition(), predicate);

		if (loopQueueIndex >= 0) {
			CollectiveLoopRecord loopRecord = (CollectiveLoopRecord) queue
					.get(loopQueueIndex);
			ValueIF oldPartialPC = loopRecord.partialPathCondition();
			ValueIF newPartialPC = (oldPartialPC == null ? predicate
					: dynamicFactory.and(dynamicFactory.trueValue(),
							oldPartialPC, predicate));

			if (oldPartialPC != newPartialPC) {
				if (!loopRecord.isCommitted()) {
					loopRecord.setPartialPathCondition(newPartialPC);
				} else {
					loopRecord = stateFactory.collectiveLoopRecord(
							loopRecord.assertion(), loopRecord.snapshots(),
							newPartialPC, loopRecord.relationalPredicate(),
							loopRecord.writevarSets(), loopRecord.trueBranch());
					if (!queue.isCommitted()) {
						queue.set(loopQueueIndex, loopRecord);
					} else {
						queue = queueFactory.newVector(queue);
						queue.set(loopQueueIndex, loopRecord);
						if (!state.isCommitted()) {
							state.setCollectiveQueue(queue);
						}
					}
				}
			}
		}
		if (!state.isCommitted()) {
			state.setPathCondition(pathCondition);
		} else {
			state = newState(pathCondition, queue);
		}
	}

	@Override
	public MessageIF dequeue(ProcessIF source, ProcessIF destination,
			ValueIF tag) throws ExecutionProblem {
		int modelIndex = modelSequence.indexOf(destination.model());
		ModelEnvironmentIF modelEnvironment = modelEnvironments[modelIndex];
		MessageIF message = modelEnvironment.dequeue(source, destination, tag);

		if (!state.isCommitted()) {
			state.setModelState(modelIndex, modelEnvironment.state());
		} else {
			state = newState(state.pathCondition(), state.collectiveQueue());
		}
		return message;
	}

	@Override
	public boolean emptyStack(ProcessIF process) {
		int modelIndex = modelSequence.indexOf(process.model());

		return modelEnvironments[modelIndex].emptyStack(process);
	}

	@Override
	public void enqueue(MessageIF message) {
		int modelIndex = modelSequence.indexOf(message.destination().model());
		ModelEnvironmentIF modelEnvironment = modelEnvironments[modelIndex];

		modelEnvironment.enqueue(message);
		if (!state.isCommitted()) {
			state.setModelState(modelIndex, modelEnvironment.state());
		} else {
			state = newState(state.pathCondition(), state.collectiveQueue());
		}
	}

	@Override
	public ValueIF getAssumption() {
		return state.pathCondition();
	}

	@Override
	public boolean hasMessage(ProcessIF source, ProcessIF destination,
			ValueIF tag) throws ExecutionProblem {
		int modelIndex = modelSequence.indexOf(destination.model());

		return modelEnvironments[modelIndex].hasMessage(source, destination,
				tag);
	}

	@Override
	public LocationIF location(ProcessIF process) {
		int modelIndex = modelSequence.indexOf(process.model());

		return modelEnvironments[modelIndex].location(process);
	}

	@Override
	public int numMessages(ProcessIF source, ProcessIF destination) {
		int modelIndex = modelSequence.indexOf(destination.model());

		return modelEnvironments[modelIndex].numMessages(source, destination);
	}

	@Override
	public int numMessages(ModelIF model) {
		int modelIndex = modelSequence.indexOf(model);

		return modelEnvironments[modelIndex].numMessages();
	}

	@Override
	public void pop(ProcessIF process) {
		int modelIndex = modelSequence.indexOf(process.model());
		ModelEnvironmentIF modelEnvironment = modelEnvironments[modelIndex];

		modelEnvironment.pop(process);
		if (!state.isCommitted()) {
			state.setModelState(modelIndex, modelEnvironment.state());
		} else {
			state = newState(state.pathCondition(), state.collectiveQueue());
		}
	}

	@Override
	public MessageIF probe(ProcessIF source, ProcessIF destination, ValueIF tag)
			throws ExecutionProblem {
		int modelIndex = modelSequence.indexOf(destination.model());

		return modelEnvironments[modelIndex].probe(source, destination, tag);
	}

	@Override
	public void push(ProcessIF process, LocationIF location) {
		int modelIndex = modelSequence.indexOf(process.model());
		ModelEnvironmentIF modelEnvironment = modelEnvironments[modelIndex];

		modelEnvironment.push(process, location);
		if (!state.isCommitted()) {
			state.setModelState(modelIndex, modelEnvironment.state());
		} else {
			state = newState(state.pathCondition(), state.collectiveQueue());
		}
	}

	@Override
	public void setAssumption(ValueIF predicate) {
		MorphicVector<CollectiveRecordIF> queue = collectiveQueue();

		if (loopQueueIndex >= 0) {
			CollectiveLoopRecord loopRecord = (CollectiveLoopRecord) queue
					.get(loopQueueIndex);
			ValueIF oldPartialPC = loopRecord.partialPathCondition();

			if (oldPartialPC != predicate) {
				if (!loopRecord.isCommitted()) {
					loopRecord.setPartialPathCondition(predicate);
				} else {
					loopRecord = stateFactory.collectiveLoopRecord(
							loopRecord.assertion(), loopRecord.snapshots(),
							predicate, loopRecord.relationalPredicate(),
							loopRecord.writevarSets(), loopRecord.trueBranch());
					if (!queue.isCommitted()) {
						queue.set(loopQueueIndex, loopRecord);
					} else {
						queue = queueFactory.newVector(queue);
						queue.set(loopQueueIndex, loopRecord);
						if (!state.isCommitted()) {
							state.setCollectiveQueue(queue);
						}
					}
				}
			}
		}
		if (!state.isCommitted())
			state.setPathCondition(predicate);
		else
			state = newState(predicate, queue);
	}

	@Override
	public int setLocation(ProcessIF process, LocationIF location) {
		int modelIndex = modelSequence.indexOf(process.model());
		ModelEnvironmentIF modelEnvironment = modelEnvironments[modelIndex];
		int result = modelEnvironment.setLocation(process, location);

		if (!state.isCommitted()) {
			state.setModelState(modelIndex, modelEnvironment.state());
		} else {
			state = newState(state.pathCondition(), state.collectiveQueue());
		}
		return result;
	}

	/**
	 * Returns the stack of indices into the collective queue representing the
	 * loops in which the given process is "in" in the current state. These
	 * could be complete or incomplete queue entries. (Complete means every
	 * process has reached that point.) Each entry will represent a "true"
	 * branch.
	 */
	@Override
	public Stack<Integer> loopIndexStack(ProcessIF process) {
		Stack<Integer> indexStack = new Stack<Integer>();
		Stack<CollectiveLoopRecord> loopStack = new Stack<CollectiveLoopRecord>();
		MorphicVector<CollectiveRecordIF> queue = collectiveQueue();
		int queueLength = queue.size();

		for (int i = 1; i < queueLength; i++) {
			CollectiveRecordIF record = queue.get(i);

			if (!record.reachedBy(process))
				break; // no more entries for this proc

			CollectiveAssertionIF assertion = record.assertion();

			if (assertion == null || !(record instanceof CollectiveLoopRecord))
				continue;

			CollectiveLoopRecord loopRecord = (CollectiveLoopRecord) record;
			boolean trueBranch = loopRecord.trueBranch();

			if (!loopStack.isEmpty()) {
				assert loopStack.peek().trueBranch();
				if (assertion == loopStack.peek().assertion()) {
					loopStack.pop();
					indexStack.pop();
				}
			}
			if (trueBranch) {
				loopStack.push(loopRecord);
				indexStack.push(i);
			}
		}
		return indexStack;
	}

	@Override
	public void setCurrentProcess(ProcessIF process) {
		this.currentProcess = process;
		if (process == null) {
			this.loopIndexStack = null;
			this.loopQueueIndex = -1;
		} else {
			this.loopIndexStack = loopIndexStack(process);
			this.loopQueueIndex = (loopIndexStack.isEmpty() ? 0
					: loopIndexStack.peek());
		}
	}

	@Override
	public ProcessIF currentProcess() {
		return currentProcess;
	}

	// if using loop technique,
	// need to update writevars in appropriate queue positions
	// for all loops that the process owning this cell is currently in.
	// what is cell is shared? Output var. Need to know which proc
	// is writing to it. OR: do not re-write output vars?
	// how do we get stack?
	//
	// Add only those values that are defined at the top of the loop
	// if local variable deeper in stack or heap variable that was not
	// in existence at beginning of loop entry, ignore?
	// refs to heap cells that are freed will become undefined in
	// canonicalization.
	// refs to local variables will not when stack is popped (this is
	// problem--they should)
	//
	// get length of stack when entered loop: this is in snapshot. so is
	// heap. if stack length greater than it was then : ignore this.

	// heap: if loop is creating heap cells on each iteration, there is no
	// way convergence can occur (unless it also destroying heap cells).
	// If the heap cell still exists when you get back to top of loop, re-write
	// it. else, ignore.

	// note: cannot set value of a literal cell. check this.

	@Override
	public void setValue(ModelCellIF variable, ValueIF value) {
		int modelIndex = modelSequence.indexOf(variable.model());
		ModelEnvironmentIF modelEnvironment = modelEnvironments[modelIndex];
		MorphicVector<CollectiveRecordIF> queue = collectiveQueue();

		modelEnvironment.setValue(variable, value);
		if (currentProcess != null && value != null) {
			// this is used in loop technique only.
			// go through stack and add this reference to all appropriate queues
			// if not already there...
			VariableReferenceValueIF modifiedVariable = dynamicFactory
					.referenceValue(variable, dynamicFactory
							.referenceValueType(value.valueType()));
			int currentStackLength = -1;

			assert loopIndexStack != null;
			if (variable.scope() == DynamicScope.LOCAL) {
				currentStackLength = stackSize(currentProcess);
				assert currentStackLength >= 1;
			}
			for (int index : loopIndexStack) {
				if (index == 0)
					continue;

				CollectiveLoopRecord record = (CollectiveLoopRecord) queue
						.get(index);

				assert record.trueBranch();
				if (currentStackLength >= 0
						&& currentStackLength > record.getSnapshot(
								currentProcess).stackSize())
					continue;

				CollectiveAssertionIF assertion = record.assertion();
				int processIndex = assertion.indexOf(currentProcess);
				CollectiveLoopRecordIF newRecord = stateFactory.recordFactory()
						.addToWritevars(processIndex, modifiedVariable, record);

				if (newRecord != record) {
					if (!queue.isCommitted()) {
						queue.set(index, newRecord);
					} else {
						queue = queueFactory.newVector(queue);
						queue.set(index, newRecord);
					}
				}
			}
		}
		if (!state.isCommitted()) {
			state.setModelState(modelIndex, modelEnvironment.state());
			state.setCollectiveQueue(queue);
		} else {
			state = newState(state.pathCondition(), queue);
		}
	}

	@Override
	public ProcessStateIF processState(ProcessIF process) {
		int modelIndex = modelSequence.indexOf(process.model());

		return getModelStates()[modelIndex].processState(process.pid());
	}

	@Override
	public int stackSize(ProcessIF process) {
		int modelIndex = modelSequence.indexOf(process.model());

		return modelEnvironments[modelIndex].stackSize(process);
	}

	@Override
	public ValueIF valueOf(ModelCellIF variable) {
		int modelIndex = modelSequence
				.indexOf(((ModelCellIF) variable).model());

		return modelEnvironments[modelIndex].valueOf(variable);
	}

	// cache heap canonicalization: pairs <ProcessStateIF,Morphic>->Morphic
	// two parts: new heap, and then updating references
	// oldHeap->newHeap

	// now model environment only permutes heap, does not update references.
	// that job moves to here....

	@Override
	public DynamicSimplifierIF canonicalizeHeap(ProcessIF process,
			Sourceable sourceable) throws ExecutionProblem {
		int modelIndex = modelSequence.indexOf(process.model());
		ModelEnvironmentIF modelEnvironment = modelEnvironments[modelIndex];
		ModelStateIF modelState = modelEnvironment.state();
		DynamicSimplifierIF dynamicSimplifier;
		ModelStateIF newModelState;
		MorphicVector<CollectiveRecordIF> queue = state.collectiveQueue();

		// this updates process state. Still need to update queue, which
		// contains references, possibly to heap...
		dynamicSimplifier = modelEnvironment.canonicalizeHeap(process,
				sourceable); // this might change modelState
		if (dynamicSimplifier == null) // no change
			return null;
		newModelState = modelEnvironment.state();
		if (modelState != newModelState) {
			if (!state.isCommitted()) {
				state.setModelState(modelIndex, newModelState);
			} else {
				state = newState(state.pathCondition(), queue);
			}
		}
		if (stateFactory.useLoopTechnique()) {
			MorphicVector<CollectiveRecordIF> newQueue;

			try {
				newQueue = stateSimplifier.simplifyQueue(dynamicSimplifier,
						queue);
			} catch (DynamicException e) {
				throw new ExecutionProblem(e, Certainty.NONE);
			}
			if (queue != newQueue) {
				if (!state.isCommitted()) {
					state.setCollectiveQueue(newQueue);
				} else {
					state = newState(state.pathCondition(), newQueue);
				}
			}
		}
		return dynamicSimplifier;
	}

	public int heapSize(ProcessIF process) {
		int modelIndex = modelSequence.indexOf(process.model());

		return modelEnvironments[modelIndex].heapSize(process);
	}

	@Override
	public LocationIF[] locations() {
		return state.locations();
	}

	@Override
	public MorphicVector<CollectiveRecordIF> collectiveQueue() {
		return state.collectiveQueue();
	}

	@Override
	public CollectiveRecordIF getCollectiveRecord(int position) {
		return state.collectiveQueue().get(position);
	}

	@Override
	public int loopQueueIndex() {
		return loopQueueIndex;
	}

	@Override
	public void setLoopQueueIndex(int value) {
		this.loopQueueIndex = value;
	}

	/**
	 * This variable is used to store path condition modifications that occur
	 * outside of any inductive loop. Modifications to the path condition that
	 * occur within some loop will be stored in the appropriate place in the
	 * collectiveQueue or loopStack.
	 */
	@Override
	public ValueIF permanentPathCondition() {
		return state.permanentPathCondition();
	}

	// add methods to modify collective queue?
	// second: setQueueEntry(int position, CollectiveRecord record);
	// third: enqueueCollectiveRecord(CollectiveRecord record);

	@Override
	public void setCollectiveQueue(MorphicVector<CollectiveRecordIF> queue) {
		if (!state.isCommitted())
			state.setCollectiveQueue(queue);
		else
			state = newState(state.pathCondition(), queue);
	}

	@Override
	public void setSnapshot(int queuePosition, int processIndex,
			ProcessStateIF snapshot) {
		MorphicVector<CollectiveRecordIF> queue = state.collectiveQueue();
		CollectiveRecordIF record = queue.get(queuePosition);
		MorphicArray<ProcessStateIF> snapshots = record.snapshots();

		snapshot.commit();
		if (!snapshots.isCommitted()) {
			snapshots.set(processIndex, snapshot);
		} else {
			snapshots = stateFactory.processStateArrayFactory().newArray(
					snapshots);
			snapshots.set(processIndex, snapshot);
			if (!record.isCommitted()) {
				record.setSnapshots(snapshots);
			} else {
				if (record instanceof CollectiveLoopRecordIF) {
					CollectiveLoopRecordIF loopRecord = (CollectiveLoopRecordIF) record;

					record = stateFactory.collectiveLoopRecord(
							record.assertion(), snapshots,
							loopRecord.partialPathCondition(),
							loopRecord.relationalPredicate(),
							loopRecord.writevarSets(), loopRecord.trueBranch());
				} else {
					record = stateFactory.collectiveRecord(record.assertion(),
							snapshots);
				}
				if (!queue.isCommitted()) {
					queue.set(queuePosition, record);
				} else {
					queue = queueFactory.newVector(queue);
					queue.set(queuePosition, record);
					if (!state.isCommitted()) {
						state.setCollectiveQueue(queue);
					} else {
						state = newState(state.pathCondition(), queue);
					}
				}
			}
		}
	}

	@Override
	public boolean terminated(ProcessIF process) {
		int modelIndex = modelSequence.indexOf(process.model());

		return modelEnvironments[modelIndex].terminated(process);
	}

	@Override
	public boolean terminated(ModelIF model) {
		return modelEnvironments[modelSequence.indexOf(model)]
				.terminated(model);
	}

	@Override
	public void collectiveEnqueue(CollectiveRecordIF record) {
		MorphicVector<CollectiveRecordIF> queue = state.collectiveQueue();

		if (!queue.isCommitted()) {
			queue.add(record);
		} else {
			queue = queueFactory.newVector(queue);
			queue.add(record);
			if (!state.isCommitted()) {
				state.setCollectiveQueue(queue);
			} else {
				state = newState(state.pathCondition(), queue);
			}
		}
	}

	@Override
	public CollectiveRecordIF removeCollectiveRecord(int position) {
		MorphicVector<CollectiveRecordIF> queue = state.collectiveQueue();
		CollectiveRecordIF result;

		if (!queue.isCommitted()) {
			result = queue.removeElementAt(position);
		} else {
			queue = queueFactory.newVector(queue);
			result = queue.removeElementAt(position);
			if (!state.isCommitted()) {
				state.setCollectiveQueue(queue);
			} else {
				state = newState(state.pathCondition(), queue);
			}
		}
		return result;
	}

	@Override
	public int collectiveQueueSize() {
		return state.collectiveQueue().size();
	}

}