State.java

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

import java.util.Arrays;

import edu.udel.cis.vsl.tass.dynamic.IF.DynamicFactoryIF;
import edu.udel.cis.vsl.tass.dynamic.IF.value.ValueIF;
import edu.udel.cis.vsl.tass.model.IF.location.LocationIF;
import edu.udel.cis.vsl.tass.morph.Morphic;
import edu.udel.cis.vsl.tass.morph.MorphicObject;
import edu.udel.cis.vsl.tass.morph.MorphicVector;
import edu.udel.cis.vsl.tass.morph.MorphicVectorFactory;
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.StateIF;

public class State extends MorphicObject implements StateIF {

	private int instanceId;

	private int canonicalId = -1;

	/** Is this state currently on the DFS stack? */
	private boolean onStack = false;

	/** Has this state been seen before? */
	private boolean seen = false;

	/** Conservatively, assume it is nondeterministic, unless told otherwise */
	private boolean isNonDeterministic = true;

	/**
	 * For each model, the state of that model. We are using a concrete array in
	 * place of a Morphic Array now. Because of this, you can never share this
	 * array between two states. If you did so, and one state was committed, and
	 * the other was not committed, when working with the second state you might
	 * modify this array. So every time you create a new state, you must also
	 * create a new array.
	 */
	private ModelStateIF[] modelStates;

	/**
	 * The official path condition. It is the conjunction of the
	 * partialPathCondition and the partial path conditions in the
	 * collectiveQueue and loopStack.
	 */
	private ValueIF pathCondition;

	/**
	 * The collective queue, used for checking collective assertions, using
	 * joint loop invariants, etc. This may contain a mixture of ordinary
	 * collective assertions and collective loop records. It incorporates the
	 * collective loop stack as well as the permanent path condition. If using
	 * the loop technique, element 0 will be for the permanent pc, element 1
	 * will be the bottom of the stack, and so on, followed by the oldest queue
	 * element, and so on, ending in the newest queue element. A new record will
	 * be enqueued after that, at the very end of the array.
	 */
	private MorphicVector<CollectiveRecordIF> collectiveQueue;

	public State(int instanceId, ModelStateIF[] modelStates,
			ValueIF pathCondition, MorphicVector<CollectiveRecordIF> queue) {
		this.instanceId = instanceId;
		this.modelStates = modelStates;
		this.pathCondition = pathCondition;
		this.collectiveQueue = queue;
	}

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

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

	void setCanonicalId(int id) {
		canonicalId = id;
	}

	/**
	 * The array of model states. For each model, the state of that model. The
	 * models are ordered by model index.
	 */
	public ModelStateIF[] modelStates() {
		return modelStates;
	}

	/** The model state for the model of the given model index. */
	@Override
	public ModelStateIF modelState(int modelIndex) {
		return modelStates[modelIndex];
	}

	void setModelState(int modelIndex, ModelStateIF modelState) {
		assert !isCommitted();
		modelStates[modelIndex] = modelState;
	}

	/**
	 * The official path condition. It is the conjunction of the
	 * partialPathCondition and the partial path conditions in the
	 * collectiveQueue and loopStack.
	 */
	@Override
	public ValueIF pathCondition() {
		return pathCondition;
	}

	void setPathCondition(ValueIF predicate) {
		assert !isCommitted();
		pathCondition = predicate;
	}

	/**
	 * 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 ((CollectiveLoopRecord) collectiveQueue.get(0))
				.partialPathCondition();
	}

	/**
	 * The collective queue, used for checking collective assertions. The oldest
	 * entry is at position 0. This is the one that will be dequeued by the next
	 * dequeue operation. An enqueue operation will place a new element at
	 * position collectiveQueue.length.
	 */
	@Override
	public MorphicVector<CollectiveRecordIF> collectiveQueue() {
		return collectiveQueue;
	}

	void setCollectiveQueue(MorphicVector<CollectiveRecordIF> queue) {
		assert !isCommitted();
		collectiveQueue = queue;
	}

	@Override
	public String toString() {
		return "State " + instanceId();
	}

	/** Splice all locations together in one big array. */
	@Override
	public LocationIF[] locations() {
		int numModels = modelStates.length;
		LocationIF[][] locationsForModel = new LocationIF[numModels][];
		int numLocations = 0;
		LocationIF[] locations;
		int counter = 0;

		for (int i = 0; i < numModels; i++) {
			locationsForModel[i] = modelStates[i].locations();
			numLocations += locationsForModel[i].length;
		}
		locations = new LocationIF[numLocations];
		for (int i = 0; i < numModels; i++) {
			int numLocationsForModel = locationsForModel[i].length;

			for (int j = 0; j < numLocationsForModel; j++) {
				locations[counter] = locationsForModel[i][j];
				counter++;
			}
		}
		return locations;
	}

	@Override
	protected boolean computeEquals(Morphic component) {
		if (component instanceof State) {
			State that = (State) component;

			if (!Arrays.equals(modelStates, that.modelStates))
				return false;
			if (!pathCondition.equals(that.pathCondition))
				return false;
			if (collectiveQueue == null) {
				if (that.collectiveQueue != null)
					return false;
			} else {
				if (!collectiveQueue.equals(that.collectiveQueue))
					return false;
			}
			return true;
		}
		return false;
	}

	@Override
	protected int computeHashCode() {
		int result = pathCondition.hashCode() + Arrays.hashCode(modelStates);

		if (collectiveQueue != null)
			result += collectiveQueue.hashCode();
		return result;
	}

	void canonicalizeChildren(DynamicFactoryIF dynamicFactory,
			ModelStateFactoryIF modelStateFactory,
			CollectiveRecordFactory recordFactory,
			MorphicVectorFactory<CollectiveRecordIF> queueFactory) {
		int numModelStates = modelStates.length;

		if (pathCondition != null)
			pathCondition = dynamicFactory.canonic(pathCondition);
		for (int i = 0; i < numModelStates; i++) {
			ModelStateIF modelState = modelStates[i];

			if (modelState != null)
				modelStates[i] = modelStateFactory.canonic(modelState);
		}
		if (collectiveQueue != null)
			collectiveQueue = queueFactory.canonic(collectiveQueue);
	}

	@Override
	protected void commitChildren() {
		if (collectiveQueue != null)
			collectiveQueue.commit();
		if (pathCondition != null)
			pathCondition.commit();
		for (ModelStateIF modelState : modelStates)
			modelState.commit();
	}

	@Override
	public boolean seen() {
		return seen;
	}

	@Override
	public void setSeen(boolean value) {
		seen = value;
	}

	@Override
	public boolean onStack() {
		return onStack;
	}

	@Override
	public void setOnStack(boolean value) {
		onStack = value;
	}

	@Override
	public String descriptor() {
		if (!isCommitted())
			return "";
		if (!isCanonic()) {
			return "(committed)";
		}
		return "(canonicID = " + canonicalId() + ")";
	}

	@Override
	public boolean isNonDeterministic() {
		return isNonDeterministic;
	}

	@Override
	public void setIsNonDeterministic(boolean value) {
		this.isNonDeterministic = value;
	}
}