StateFactory.java

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

import java.util.Collection;
import java.util.LinkedHashSet;
import java.util.Vector;

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.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.ModelSequence;
import edu.udel.cis.vsl.tass.morph.MorphicArray;
import edu.udel.cis.vsl.tass.morph.MorphicArrayFactory;
import edu.udel.cis.vsl.tass.morph.MorphicFactory;
import edu.udel.cis.vsl.tass.morph.MorphicSet;
import edu.udel.cis.vsl.tass.morph.MorphicSetFactory;
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.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.symbolic.IF.SymbolicConstantIF;

public class StateFactory extends MorphicFactory<StateIF> implements
		StateFactoryIF {

	private DynamicFactoryIF dynamicFactory;

	private ScopeStateFactory scopeStateFactory;

	private FrameFactory frameFactory;

	private ProcessStateFactory processStateFactory;

	private CollectiveRecordFactory recordFactory;

	private MorphicVectorFactory<CollectiveRecordIF> queueFactory;

	private MorphicSetFactory<VariableReferenceValueIF> variableSetFactory;

	private MorphicArrayFactory<ProcessStateIF> processStateArrayFactory;

	private ValueIF trueValue;

	private int numModels;

	private ModelStateFactory modelStateFactory;

	private Vector<State> stateVector = new Vector<State>();

	private boolean useLoopTechnique;

	private int stateCounter = 0;

	public StateFactory(ModelSequence modelSequence,
			DynamicFactoryIF dynamicFactory) {
		this.dynamicFactory = dynamicFactory;
		this.trueValue = dynamicFactory.trueValue();
		this.useLoopTechnique = dynamicFactory.configuration()
				.useLoopTechnique();
		this.numModels = modelSequence.numModels();
		this.scopeStateFactory = new ScopeStateFactory(dynamicFactory);
		this.frameFactory = new FrameFactory(scopeStateFactory);
		this.processStateFactory = new ProcessStateFactory(frameFactory);
		this.modelStateFactory = new ModelStateFactory(processStateFactory);
		this.processStateArrayFactory = modelStateFactory
				.processStateArrayFactory();
		this.variableSetFactory = new MorphicSetFactory<VariableReferenceValueIF>(
				dynamicFactory.valueFactory());
		this.recordFactory = new CollectiveRecordFactory(dynamicFactory,
				modelSequence, variableSetFactory, modelStateFactory
						.processStateFactory(), processStateArrayFactory);
		this.queueFactory = new MorphicVectorFactory<CollectiveRecordIF>(
				recordFactory);
	}

	@Override
	public StateSimplifier simplifier(boolean simplifySnapshots) {
		return new StateSimplifier(this, simplifySnapshots);
	}

	public boolean useLoopTechnique() {
		return useLoopTechnique;
	}

	public DynamicFactoryIF dynamicFactory() {
		return dynamicFactory;
	}

	@Override
	public ModelStateFactory modelStateFactory() {
		return modelStateFactory;
	}

	public CollectiveRecordFactory recordFactory() {
		return recordFactory;
	}

	@Override
	public MorphicVectorFactory<CollectiveRecordIF> queueFactory() {
		return queueFactory;
	}

	@Override
	public MorphicArrayFactory<ProcessStateIF> processStateArrayFactory() {
		return processStateArrayFactory;
	}

	@Override
	public MorphicSetFactory<VariableReferenceValueIF> variableSetFactory() {
		return variableSetFactory;
	}

	/**
	 * Constructs and returns a new state.
	 */
	public State state(ModelStateIF[] modelStates, ValueIF pathCondition,
			MorphicVector<CollectiveRecordIF> queue) {
		State state = new State(stateCounter, modelStates, pathCondition, queue);

		stateCounter++;
		return state;
	}

	@Override
	protected void canonicalizeChildren(StateIF state) {
		((State) state).canonicalizeChildren(dynamicFactory, modelStateFactory,
				recordFactory, queueFactory);
	}

	@Override
	public StateIF canonic(StateIF state) {
		State result = (State) super.canonic(state);

		if (result.canonicalId() < 0) {
			result.setCanonicalId(stateVector.size());
			stateVector.add(result);
		}
		return result;
	}

	@Override
	public CollectiveRecord collectiveRecord(CollectiveAssertionIF assertion,
			MorphicArray<ProcessStateIF> snapshots) {
		return recordFactory.collectiveRecord(assertion, snapshots);
	}

	@Override
	public CollectiveRecord collectiveRecord(CollectiveAssertionIF assertion) {
		return collectiveRecord(assertion, processStateArrayFactory
				.newArray(assertion.numProcs()));
	}

	public CollectiveRecordIF canonic(CollectiveRecordIF record) {
		return recordFactory.canonic(record);
	}

	@Override
	public CollectiveLoopRecord collectiveLoopRecord(
			CollectiveAssertionIF assertion,
			MorphicArray<ProcessStateIF> snapshots,
			ValueIF partialPathCondition, ValueIF relationalPredicate,
			MorphicArray<MorphicSet<VariableReferenceValueIF>> writevarSets,
			boolean trueBranch) {
		return recordFactory.collectiveLoopRecord(assertion, snapshots,
				partialPathCondition, relationalPredicate, writevarSets,
				trueBranch);
	}

	public MorphicSet<VariableReferenceValueIF> newVariableSet(
			LinkedHashSet<VariableReferenceValueIF> references) {
		return variableSetFactory.newSet(references);
	}

	/** New variable set with empty set. */
	public MorphicSet<VariableReferenceValueIF> newVariableSet() {
		return variableSetFactory.newSet();
	}

	public MorphicSet<VariableReferenceValueIF> add(
			MorphicSet<VariableReferenceValueIF> oldSet,
			VariableReferenceValueIF reference) {
		return variableSetFactory.add(oldSet, reference);
	}

	/**
	 * To be used in loop technique: the path condition is determined by taking
	 * the conjunction of all the predicates in the queue.
	 */
	@Override
	public ValueIF computePathCondition(MorphicVector<CollectiveRecordIF> queue)
			throws DynamicException {
		ValueIF result = trueValue;

		assert useLoopTechnique;
		for (CollectiveRecordIF record : queue) {
			if (record instanceof CollectiveLoopRecord) {
				CollectiveLoopRecord loopRecord = (CollectiveLoopRecord) record;

				result = dynamicFactory.and(trueValue, result, loopRecord
						.partialPathCondition());
				result = dynamicFactory.and(trueValue, result, loopRecord
						.relationalPredicate());
			}
		}
		return result;
	}

	public Collection<ValueIF> values(StateIF state) {
		Collection<ValueIF> result = new LinkedHashSet<ValueIF>();

		for (int i = 0; i < numModels; i++) {
			ModelStateIF modelState = state.modelState(i);

			result.addAll(modelStateFactory.values(modelState));
		}
		result.add(state.pathCondition());
		for (CollectiveRecordIF record : state.collectiveQueue()) {
			CollectiveAssertionIF assertion = record.assertion();
			MorphicArray<ProcessStateIF> snapshots = record.snapshots();

			if (assertion != null && snapshots != null) {
				int numProcs = assertion.numProcs();

				for (int i = 0; i < numProcs; i++) {
					ProcessStateIF processState = snapshots.get(i);

					if (processState != null) {
						result.addAll(modelStateFactory.values(processState));
					}
				}
			}
			if (record instanceof CollectiveLoopRecord) {
				CollectiveLoopRecord loopRecord = (CollectiveLoopRecord) record;

				result.add(loopRecord.partialPathCondition());
				result.add(loopRecord.relationalPredicate());
			}
		}
		return result;
	}

	@Override
	public Collection<SymbolicConstantIF> symbolicConstants(StateIF state) {
		Collection<ValueIF> values = values(state);

		return dynamicFactory.symbolicConstants(values);
	}

	@Override
	public int numStates() {
		return stateVector.size();
	}

	@Override
	public MorphicArrayFactory<MorphicSet<VariableReferenceValueIF>> variableSetArrayFactory() {
		return recordFactory.variableSetArrayFactory();
	}
}