StateSimplifier.java

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

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.simplify.DynamicSimplifierIF;
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.impl.simplify.MorphicSimplifier;
import edu.udel.cis.vsl.tass.morph.MorphicVector;
import edu.udel.cis.vsl.tass.morph.MorphicVectorFactory;
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.StateIF;

public class StateSimplifier extends MorphicSimplifier<StateIF> {

	private boolean useLoopTechnique;

	private StateFactory stateFactory;

	private ModelStateFactoryIF modelStateFactory;

	private MorphicSimplifierIF<ModelStateIF> modelStateSimplifier;

	private DynamicFactoryIF dynamicFactory;

	private CollectiveRecordFactory recordFactory;

	private MorphicVectorFactory<CollectiveRecordIF> queueFactory;

	private MorphicSimplifierIF<CollectiveRecordIF> recordSimplifier;

	private ValueIF trueValue;

	public StateSimplifier(StateFactory stateFactory, boolean simplifySnapshots) {
		this.useLoopTechnique = stateFactory.useLoopTechnique();
		this.stateFactory = stateFactory;
		this.modelStateFactory = stateFactory.modelStateFactory();
		this.modelStateSimplifier = modelStateFactory.simplifier();
		this.dynamicFactory = stateFactory.dynamicFactory();
		this.recordFactory = stateFactory.recordFactory();
		this.recordSimplifier = recordFactory.simplifier(simplifySnapshots);
		this.queueFactory = stateFactory.queueFactory();
		this.trueValue = dynamicFactory.trueValue();
	}

	/**
	 * Simplifies the collective record array. Special handling needed in
	 * position 0 of queue if using loop technique, which is why we don't use
	 * the generic vector simplifier.
	 */
	@SuppressWarnings("unchecked")
	public MorphicVector<CollectiveRecordIF> simplifyQueue(
			DynamicSimplifierIF dynamicSimplifier,
			MorphicVector<CollectiveRecordIF> queue) throws DynamicException {
		queue = queueFactory.canonic(queue);

		MorphicVector<CollectiveRecordIF> result = (MorphicVector<CollectiveRecordIF>) dynamicSimplifier
				.getCachedResult(queue);

		if (result != null)
			return result;

		int size = queue.size();
		boolean change = false;
		int bottom = 0;

		if (useLoopTechnique && dynamicSimplifier.pathConditionIsSpecial()) {
			ValueIF oldPermanentPc = ((CollectiveLoopRecord) queue.get(0))
					.partialPathCondition();
			ValueIF newPermanentPc = dynamicSimplifier.newAssumption();

			if (newPermanentPc != oldPermanentPc) {
				change = true;
				result = queueFactory.newVector(size);
				result.set(0, recordFactory.collectiveLoopRecord(null, null,
						newPermanentPc, trueValue, null, false));
			}
			bottom = 1;
		}
		for (int i = bottom; i < size; i++) {
			CollectiveRecordIF oldRecord = queue.get(i);
			CollectiveRecordIF newRecord = recordSimplifier.simplify(
					dynamicSimplifier, oldRecord);

			change = change || newRecord != oldRecord;
			if (change) {
				if (result == null) {
					result = queueFactory.newVector(size);
					for (int j = 0; j < i; j++)
						result.set(j, queue.get(j));
				}
				result.set(i, newRecord);
			}
		}
		if (change)
			result = queueFactory.canonic(result);
		else
			result = queue;
		dynamicSimplifier.cacheResult(queue, result);
		return result;
	}

	@Override
	public StateIF simplify(DynamicSimplifierIF dynamicSimplifier, StateIF state)
			throws DynamicException {
		state = stateFactory.canonic(state);

		StateIF result = (StateIF) dynamicSimplifier.getCachedResult(state);

		if (result != null)
			return result;

		MorphicVector<CollectiveRecordIF> oldQueue = state.collectiveQueue();
		MorphicVector<CollectiveRecordIF> newQueue = simplifyQueue(
				dynamicSimplifier, oldQueue);
		ModelStateIF[] oldModelStates = state.modelStates();
		int numModels = oldModelStates.length;
		ModelStateIF[] newModelStates = new ModelStateIF[numModels];
		boolean change = oldQueue != newQueue;

		for (int i = 0; i < numModels; i++) {
			ModelStateIF oldModelState = oldModelStates[i];
			ModelStateIF newModelState = modelStateSimplifier.simplify(
					dynamicSimplifier, oldModelState);

			change = change || oldModelState != newModelState;
			newModelStates[i] = newModelState;
		}

		ValueIF oldPathCondition = state.pathCondition();
		ValueIF newPathCondition;

		if (!dynamicSimplifier.pathConditionIsSpecial()) {
			newPathCondition = dynamicSimplifier.simplify(oldPathCondition);
		} else {
			if (!useLoopTechnique) {
				newPathCondition = dynamicSimplifier.newAssumption();
			} else {
				int numRecords = newQueue.size();
				CollectiveLoopRecordIF record0 = (CollectiveLoopRecordIF) newQueue
						.get(0);
				ValueIF permanentPathCondition = record0.partialPathCondition();
				ValueIF relational0 = record0.relationalPredicate();

				newPathCondition = permanentPathCondition;
				if (relational0 != null)
					newPathCondition = dynamicFactory.and(trueValue,
							newPathCondition, relational0);
				for (int i = 1; i < numRecords; i++) {
					CollectiveRecordIF record = newQueue.get(i);

					if (record != null
							&& record instanceof CollectiveLoopRecordIF) {
						ValueIF partialPathCondition = ((CollectiveLoopRecordIF) record)
								.partialPathCondition();
						ValueIF relational = ((CollectiveLoopRecordIF) record)
								.relationalPredicate();

						if (partialPathCondition != null)
							newPathCondition = dynamicFactory.and(trueValue,
									newPathCondition, partialPathCondition);
						if (relational != null)
							newPathCondition = dynamicFactory.and(trueValue,
									newPathCondition, relational);
					}
				}
			}
		}

		change = change || newPathCondition != oldPathCondition;

		if (change) {
			result = stateFactory.state(newModelStates, newPathCondition,
					newQueue);
			result = stateFactory.canonic(result);
		} else {
			result = state;
		}
		dynamicSimplifier.cacheResult(state, result);
		return result;
	}
}