CollectiveAssertion.java

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

import java.util.Collection;
import java.util.LinkedHashSet;

import edu.udel.cis.vsl.tass.model.IF.CollectiveAssertionIF;
import edu.udel.cis.vsl.tass.model.IF.ProcessIF;
import edu.udel.cis.vsl.tass.model.IF.location.LocationIF;
import edu.udel.cis.vsl.tass.util.Source;

public class CollectiveAssertion implements CollectiveAssertionIF {

	private Source source;
	private Collection<ProcessIF> processes;
	private ProcessIF[] processArray;
	private Collection<LocationIF> locations;
	private boolean isLoopInvariant = false;
	private boolean isJointAssertion = false;
	private String identifier;

	public CollectiveAssertion(Collection<ProcessIF> processes,
			Collection<LocationIF> locations, String identifier,
			boolean isLoopInvariant, boolean isJointAssertion) {
		this.processes = processes;
		this.locations = locations;
		this.identifier = identifier;
		this.isLoopInvariant = isLoopInvariant;
		this.isJointAssertion = isJointAssertion;
		this.processArray = new ProcessIF[processes.size()];

		int count = 0;

		for (ProcessIF process : processes) {
			processArray[count] = process;
			count++;
		}
	}

	public void addProcesses(Collection<ProcessIF> newProcesses) {
		processes.addAll(newProcesses);
		ProcessIF[] newProcessArray = new ProcessIF[processes.size()];
		int i;
		for (i = 0; i < processArray.length; i++) {
			newProcessArray[i] = processArray[i];
		}
		for (ProcessIF process : newProcesses) {
			newProcessArray[i] = process;
			i++;
		}
		processArray = newProcessArray;
	}

	// public void setExpression(ExpressionIF expression) {
	// this.expression = expression;
	// }

	@Override
	public String identifier() {
		return identifier;
	}

	public String toString() {
		return "Collective Assertion of " + source + " (" + numProcs()
				+ " processes)";
	}

	@Override
	public Source getSource() {
		return source;
	}

	@Override
	public void setSource(Source source) {
		this.source = source;
	}

	@Override
	public int numProcs() {
		return processes.size();
	}

	@Override
	public Collection<ProcessIF> processSet() {
		return processes;
	}

	@Override
	public ProcessIF process(int index) {
		return (ProcessIF) processes.toArray()[index];
	}

	// TODO: replace with constant-time algorithm instead of this linear time
	// one:

	@Override
	public int indexOf(ProcessIF process) {
		int index = -1;
		for (int i = 0; i < processes.size(); i++) {
			if (process.equals(processes.toArray()[i])) {
				index = i;
				break;
			}
		}
		return index;
	}

	// @Override
	// public ExpressionIF expression() {
	// return expression;
	// }

	@Override
	public Collection<LocationIF> locationsInProcess(ProcessIF process) {
		Collection<LocationIF> processLocations = new LinkedHashSet<LocationIF>();
		for (LocationIF loc : locations) {
			if (loc.process().equals(process)) {
				processLocations.add(loc);
			}
		}
		return processLocations;
	}

	@Override
	public Collection<LocationIF> locations() {
		return locations;
	}

	@Override
	public ProcessIF[] processArray() {
		return processArray;
	}

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

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

}