CollectiveRecordFactory.java

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

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.state.IF.CollectiveLoopRecordIF;
import edu.udel.cis.vsl.tass.state.IF.CollectiveRecordIF;
import edu.udel.cis.vsl.tass.state.IF.ProcessStateIF;

public class CollectiveRecordFactory extends MorphicFactory<CollectiveRecordIF> {

	private DynamicFactoryIF dynamicFactory;

	private MorphicSetFactory<VariableReferenceValueIF> variableSetFactory;

	private ProcessStateFactory processStateFactory;

	private MorphicArrayFactory<ProcessStateIF> processStateArrayFactory;

	private MorphicArrayFactory<MorphicSet<VariableReferenceValueIF>> variableSetArrayFactory;

	public CollectiveRecordFactory(DynamicFactoryIF dynamicFactory,
			ModelSequence modelSequence,
			MorphicSetFactory<VariableReferenceValueIF> variableSetFactory,
			ProcessStateFactory processStateFactory,
			MorphicArrayFactory<ProcessStateIF> processStateArrayFactory) {
		this.dynamicFactory = dynamicFactory;
		this.variableSetFactory = variableSetFactory;
		this.processStateFactory = processStateFactory;
		this.processStateArrayFactory = processStateArrayFactory;
		this.variableSetArrayFactory = new MorphicArrayFactory<MorphicSet<VariableReferenceValueIF>>(
				variableSetFactory);
	}

	public DynamicFactoryIF dynamicFactory() {
		return dynamicFactory;
	}

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

	public ProcessStateFactory processStateFactory() {
		return processStateFactory;
	}

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

	public MorphicArrayFactory<MorphicSet<VariableReferenceValueIF>> variableSetArrayFactory() {
		return variableSetArrayFactory;
	}

	public CollectiveRecord collectiveRecord(CollectiveAssertionIF assertion,
			MorphicArray<ProcessStateIF> snapshots) {
		return new CollectiveRecord(assertion, snapshots);
	}

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

	@Override
	public void canonicalizeChildren(CollectiveRecordIF record) {
		((CollectiveRecord) record)
				.canonicalizeChildren(processStateArrayFactory);
	}

	public CollectiveRecordSimplifier simplifier(boolean simplifySnapshots) {
		return new CollectiveRecordSimplifier(this, simplifySnapshots);
	}

	public CollectiveLoopRecordIF addToWritevars(int index,
			VariableReferenceValueIF element, CollectiveLoopRecordIF record) {
		MorphicArray<MorphicSet<VariableReferenceValueIF>> writevarSets = record
				.writevarSets();
		MorphicSet<VariableReferenceValueIF> oldSet = writevarSets.get(index);
		MorphicSet<VariableReferenceValueIF> newSet;

		if (oldSet == null)
			newSet = variableSetFactory.newSet();
		else
			newSet = oldSet;
		newSet = variableSetFactory.add(newSet, element);
		if (newSet == oldSet) {
			return record;
		}
		if (!writevarSets.isCommitted()) {
			writevarSets.set(index, newSet);
			return record;
		}
		writevarSets = variableSetArrayFactory.newArray(writevarSets);
		writevarSets.set(index, newSet);
		if (!record.isCommitted()) {
			record.setWritevarSets(writevarSets);
			return record;
		}
		record = collectiveLoopRecord(record.assertion(), record.snapshots(),
				record.partialPathCondition(), record.relationalPredicate(),
				writevarSets, record.trueBranch());
		return record;
	}
}