CollectiveLoopRecord.java

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

import java.io.PrintWriter;

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

public class CollectiveLoopRecord extends CollectiveRecord implements
		CollectiveLoopRecordIF {

	private ValueIF partialPathCondition;

	private ValueIF relationalPredicate;

	/**
	 * Variables which are modified during execution of the loop body. Index is
	 * process index, exactly like the snapshots. The value at that index is a
	 * set of variable references for that process.
	 */
	private MorphicArray<MorphicSet<VariableReferenceValueIF>> writevarSets;

	private boolean trueBranch;

	public CollectiveLoopRecord(CollectiveAssertionIF assertion,
			MorphicArray<ProcessStateIF> snapshots,
			ValueIF partialPathCondition, ValueIF relationalPredicate,
			MorphicArray<MorphicSet<VariableReferenceValueIF>> writevarSets,
			boolean trueBranch) {
		super(assertion, snapshots);
		assert partialPathCondition != null;
		assert relationalPredicate != null;
		this.partialPathCondition = partialPathCondition;
		this.relationalPredicate = relationalPredicate;
		this.writevarSets = writevarSets;
		this.trueBranch = trueBranch;
	}

	@Override
	public void print(PrintWriter out, String prefix) {
		out.println(prefix + "begin collective loop record ");
		out.println(prefix + "  assertion: " + assertion());
		out.println(prefix + "  writevarSets: " + writevarSets);
		out.println(prefix + "  partialPathCondition: " + partialPathCondition);
		out.println(prefix + "  relationalPredicate: " + relationalPredicate);
		out.println(prefix + "  branch: " + trueBranch);

		MorphicArray<ProcessStateIF> snapshots = snapshots();

		if (snapshots != null) {
			for (int i = 0; i < snapshots.length(); i++) {
				out.println(prefix + "  snapshot " + i + ": "
						+ snapshots.get(i));
				out.println(prefix + "  writevars " + i + ": "
						+ writevarSets().get(i));
			}
		}
		out.println(prefix + "end collective loop record ");
		out.flush();
	}

	@Override
	public ValueIF partialPathCondition() {
		return partialPathCondition;
	}

	@Override
	public ValueIF relationalPredicate() {
		return relationalPredicate;
	}

	@Override
	public boolean trueBranch() {
		return trueBranch;
	}

	@Override
	public void setPartialPathCondition(ValueIF predicate) {
		assert !isCommitted();
		partialPathCondition = predicate;
	}

	@Override
	public void setRelationalPredicate(ValueIF predicate) {
		assert !isCommitted();
		relationalPredicate = predicate;
	}

	@Override
	public void setTrueBranch(boolean value) {
		assert !isCommitted();
		trueBranch = value;
	}

	@Override
	public MorphicArray<MorphicSet<VariableReferenceValueIF>> writevarSets() {
		return writevarSets;
	}

	// add to writevar set, remove, ...?

	@Override
	public void setWritevarSets(
			MorphicArray<MorphicSet<VariableReferenceValueIF>> writevarSets) {
		assert !isCommitted();
		this.writevarSets = writevarSets;
	}

	public void setWritevarSet(int index,
			MorphicSet<VariableReferenceValueIF> set) {
		writevarSets.set(index, set);
	}

	@Override
	public MorphicSet<VariableReferenceValueIF> getWritevarSet(int index) {
		return writevarSets.get(index);
	}

	@Override
	public MorphicSet<VariableReferenceValueIF> getWritevarSet(ProcessIF process) {
		return getWritevarSet(assertion().indexOf(process));
	}

	public void setWritevarSet(ProcessIF process,
			MorphicSet<VariableReferenceValueIF> set) {
		setWritevarSet(assertion().indexOf(process), set);
	}

	@Override
	public boolean isInitial() {
		return assertion() == null && snapshots() == null
				&& relationalPredicate == null && !trueBranch();
	}

	@Override
	protected boolean computeEquals(Morphic component) {
		if (component instanceof CollectiveLoopRecord) {
			CollectiveLoopRecord that = (CollectiveLoopRecord) component;

			if (!super.computeEquals(component))
				return false;
			if (partialPathCondition == null) {
				if (that.partialPathCondition != null)
					return false;
			} else {
				if (!partialPathCondition.equals(that.partialPathCondition))
					return false;
			}
			if (relationalPredicate == null) {
				if (that.relationalPredicate != null)
					return false;
			} else {
				if (!relationalPredicate.equals(that.relationalPredicate))
					return false;
			}
			if (writevarSets == null) {
				if (that.writevarSets != null)
					return false;
			} else {
				if (!writevarSets.equals(that.writevarSets))
					return false;
			}
			return trueBranch == that.trueBranch;
		}
		return false;
	}

	@Override
	protected int computeHashCode() {
		int result = super.computeHashCode();

		if (partialPathCondition != null)
			result += partialPathCondition.hashCode();
		if (relationalPredicate != null)
			result += relationalPredicate.hashCode();
		if (writevarSets != null)
			result += writevarSets.hashCode();
		if (trueBranch)
			result += 4096;
		return result;
	}

	@Override
	protected void commitChildren() {
		if (partialPathCondition != null)
			partialPathCondition.commit();
		if (relationalPredicate != null)
			relationalPredicate.commit();
		if (writevarSets != null)
			writevarSets.commit();
	}

	void canonicalizeChildren(CollectiveRecordFactory recordFactory) {
		DynamicFactoryIF dynamicFactory = recordFactory.dynamicFactory();
		MorphicArrayFactory<MorphicSet<VariableReferenceValueIF>> variableSetArrayFactory = recordFactory
				.variableSetArrayFactory();

		if (partialPathCondition != null)
			partialPathCondition = dynamicFactory.canonic(partialPathCondition);
		if (relationalPredicate != null)
			relationalPredicate = dynamicFactory.canonic(relationalPredicate);
		if (writevarSets != null)
			writevarSets = variableSetArrayFactory.canonic(writevarSets);
	}
}