CollectiveRecordFactory.java

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

import java.util.LinkedList;
import java.util.List;

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;

		// debugging:
		// if (dynamicFactory.isUndefined(element)) {
		// throw new RuntimeException(
		// "Attempt to add undefined reference to writevar set");
		// }

		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;
	}

	public MorphicSet<VariableReferenceValueIF> removeUndefineds(
			MorphicSet<VariableReferenceValueIF> varset) {
		List<VariableReferenceValueIF> undefs = new LinkedList<VariableReferenceValueIF>();

		for (VariableReferenceValueIF value : varset) {
			if (dynamicFactory.isUndefined(value)) {
				undefs.add(value);
			}
		}
		if (!undefs.isEmpty()) {
			if (varset.isCommitted()) {
				varset = variableSetFactory.newSet(varset);
			}
			for (VariableReferenceValueIF undef : undefs) {
				varset.remove(undef);
			}
		}
		return varset;
	}

	public CollectiveLoopRecordIF removeUndefineds(CollectiveLoopRecordIF record) {
		int numRecords = record.writevarSets().length();
		MorphicArray<MorphicSet<VariableReferenceValueIF>> writevarSets = null;

		for (int i = 0; i < numRecords; i++) {
			MorphicSet<VariableReferenceValueIF> oldset = record
					.getWritevarSet(i);
			MorphicSet<VariableReferenceValueIF> newset = removeUndefineds(oldset);

			if (oldset != newset) {
				if (writevarSets == null) {
					writevarSets = record.writevarSets();

					if (writevarSets.isCommitted()) {
						writevarSets = variableSetArrayFactory
								.newArray(writevarSets);
					}
				}
				writevarSets.set(i, newset);
			}
		}
		if (writevarSets == null) {
			return record;
		} else {
			return collectiveLoopRecord(record.assertion(), record.snapshots(),
					record.partialPathCondition(),
					record.relationalPredicate(), writevarSets,
					record.trueBranch());
		}
	}
}