CollectiveRecordSimplifier.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.IF.value.VariableReferenceValueIF;
import edu.udel.cis.vsl.tass.dynamic.impl.simplify.MorphicSimplifier;
import edu.udel.cis.vsl.tass.morph.MorphicArray;
import edu.udel.cis.vsl.tass.morph.MorphicArrayFactory;
import edu.udel.cis.vsl.tass.morph.MorphicSet;
import edu.udel.cis.vsl.tass.morph.MorphicSetFactory;
import edu.udel.cis.vsl.tass.state.IF.CollectiveRecordIF;
import edu.udel.cis.vsl.tass.state.IF.ProcessStateIF;

public class CollectiveRecordSimplifier extends
		MorphicSimplifier<CollectiveRecordIF> {

	private boolean simplifySnapshots;

	private CollectiveRecordFactory recordFactory;

	private MorphicSimplifierIF<MorphicArray<ProcessStateIF>> processStateArraySimplifier;

	private MorphicSimplifierIF<ValueIF> valueSimplifier;

	private MorphicSimplifierIF<MorphicArray<MorphicSet<VariableReferenceValueIF>>> variableSetArraySimplifier;

	public CollectiveRecordSimplifier(CollectiveRecordFactory recordFactory,
			boolean simplifySnapshots) {
		this.simplifySnapshots = simplifySnapshots;

		DynamicFactoryIF dynamicFactory = recordFactory.dynamicFactory();
		MorphicSetFactory<VariableReferenceValueIF> variableSetFactory = recordFactory
				.variableSetFactory();
		MorphicArrayFactory<MorphicSet<VariableReferenceValueIF>> variableSetArrayFactory = recordFactory
				.variableSetArrayFactory();
		MorphicArrayFactory<ProcessStateIF> processStateArrayFactory = recordFactory
				.processStateArrayFactory();

		this.recordFactory = recordFactory;
		this.valueSimplifier = dynamicFactory.valueSimplifier();

		MorphicSimplifierIF<MorphicSet<VariableReferenceValueIF>> variableSetSimplifier = dynamicFactory
				.newSetSimplifier(variableSetFactory, valueSimplifier);

		variableSetArraySimplifier = dynamicFactory.newArraySimplifier(
				variableSetArrayFactory, variableSetSimplifier);

		ProcessStateFactory processStateFactory = recordFactory
				.processStateFactory();
		ProcessStateSimplifier processStateSimplifier = processStateFactory
				.simplifier();

		processStateArraySimplifier = dynamicFactory.newArraySimplifier(
				processStateArrayFactory, processStateSimplifier);
	}

	@Override
	public CollectiveRecordIF simplify(DynamicSimplifierIF dynamicSimplifier,
			CollectiveRecordIF record) throws DynamicException {
		CollectiveRecordIF newRecord;

		record = recordFactory.canonic(record);
		newRecord = (CollectiveRecordIF) dynamicSimplifier
				.getCachedResult(record);
		if (newRecord != null)
			return newRecord;

		// sometimes you want to simplify snapshots, sometimes you don't:

		MorphicArray<ProcessStateIF> oldSnapshots = record.snapshots();
		MorphicArray<ProcessStateIF> newSnapshots;

		if (simplifySnapshots && oldSnapshots != null) {
			newSnapshots = processStateArraySimplifier.simplify(
					dynamicSimplifier, oldSnapshots);
		} else {
			newSnapshots = oldSnapshots;
		}

		boolean change = oldSnapshots != newSnapshots;

		if (record instanceof CollectiveLoopRecord) {
			CollectiveLoopRecord loopRecord = (CollectiveLoopRecord) record;
			ValueIF oldPartialPathCondition = loopRecord.partialPathCondition();
			ValueIF newPartialPathCondition = (oldPartialPathCondition != null ? valueSimplifier
					.simplify(dynamicSimplifier, oldPartialPathCondition)
					: null);
			ValueIF oldRelationalPredicate = loopRecord.relationalPredicate();
			ValueIF newRelationalPredicate = (oldRelationalPredicate != null ? valueSimplifier
					.simplify(dynamicSimplifier, oldRelationalPredicate)
					: null);
			MorphicArray<MorphicSet<VariableReferenceValueIF>> oldWritevarSets = loopRecord
					.writevarSets();
			MorphicArray<MorphicSet<VariableReferenceValueIF>> newWritevarSets = (oldWritevarSets == null ? null
					: variableSetArraySimplifier.simplify(dynamicSimplifier,
							oldWritevarSets));

			change = change
					|| oldPartialPathCondition != newPartialPathCondition
					|| oldRelationalPredicate != newRelationalPredicate
					|| oldWritevarSets != newWritevarSets;
			if (change)
				newRecord = recordFactory.collectiveLoopRecord(record
						.assertion(), newSnapshots, newPartialPathCondition,
						newRelationalPredicate, newWritevarSets, loopRecord
								.trueBranch());
			else
				newRecord = record;
		} else {
			if (change)
				newRecord = recordFactory.collectiveRecord(record.assertion(),
						newSnapshots);
			else
				newRecord = record;
		}
		newRecord = recordFactory.canonic(newRecord);
		dynamicSimplifier.cacheResult(record, newRecord);
		return newRecord;
	}
}