Model.java

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

import java.io.PrintWriter;
import java.util.Collection;
import java.util.LinkedHashSet;
import java.util.List;
import java.util.Vector;

import edu.udel.cis.vsl.tass.model.IF.CollectiveAssertionIF;
import edu.udel.cis.vsl.tass.model.IF.FunctionIF;
import edu.udel.cis.vsl.tass.model.IF.ModelFactoryIF;
import edu.udel.cis.vsl.tass.model.IF.ModelIF;
import edu.udel.cis.vsl.tass.model.IF.ProcessIF;
import edu.udel.cis.vsl.tass.model.IF.SyntaxException;
import edu.udel.cis.vsl.tass.model.IF.SystemFunctionIF;
import edu.udel.cis.vsl.tass.model.IF.expression.ExpressionIF;
import edu.udel.cis.vsl.tass.model.IF.expression.LHSExpressionIF;
import edu.udel.cis.vsl.tass.model.IF.location.AllocateLocationIF;
import edu.udel.cis.vsl.tass.model.IF.location.AnySourceReceiveLocationIF;
import edu.udel.cis.vsl.tass.model.IF.location.AssertionLocationIF;
import edu.udel.cis.vsl.tass.model.IF.location.AssignmentLocationIF;
import edu.udel.cis.vsl.tass.model.IF.location.AssumeLocationIF;
import edu.udel.cis.vsl.tass.model.IF.location.BranchLocationIF;
import edu.udel.cis.vsl.tass.model.IF.location.ChoiceLocationIF;
import edu.udel.cis.vsl.tass.model.IF.location.ForLoopLocationIF;
import edu.udel.cis.vsl.tass.model.IF.location.InvocationLocationIF;
import edu.udel.cis.vsl.tass.model.IF.location.LocationIF;
import edu.udel.cis.vsl.tass.model.IF.location.LoopLocationIF;
import edu.udel.cis.vsl.tass.model.IF.location.ReceiveLocationIF;
import edu.udel.cis.vsl.tass.model.IF.location.ReturnLocationIF;
import edu.udel.cis.vsl.tass.model.IF.location.SendLocationIF;
import edu.udel.cis.vsl.tass.model.IF.location.StandardReceiveLocationIF;
import edu.udel.cis.vsl.tass.model.IF.location.TerminalLocationIF;
import edu.udel.cis.vsl.tass.model.IF.scope.BoundScopeIF;
import edu.udel.cis.vsl.tass.model.IF.scope.LocalScopeIF;
import edu.udel.cis.vsl.tass.model.IF.scope.ScopeIF;
import edu.udel.cis.vsl.tass.model.IF.statement.AllocateStatementIF;
import edu.udel.cis.vsl.tass.model.IF.statement.AssertionStatementIF;
import edu.udel.cis.vsl.tass.model.IF.statement.AssignmentStatementIF;
import edu.udel.cis.vsl.tass.model.IF.statement.AssumeStatementIF;
import edu.udel.cis.vsl.tass.model.IF.statement.InvocationStatementIF;
import edu.udel.cis.vsl.tass.model.IF.statement.NoopStatementIF;
import edu.udel.cis.vsl.tass.model.IF.statement.ReceiveStatementIF;
import edu.udel.cis.vsl.tass.model.IF.statement.ReturnStatementIF;
import edu.udel.cis.vsl.tass.model.IF.statement.SendStatementIF;
import edu.udel.cis.vsl.tass.model.IF.statement.StatementIF;
import edu.udel.cis.vsl.tass.model.IF.type.TypeIF;
import edu.udel.cis.vsl.tass.model.IF.type.TypeIF.TypeKind;
import edu.udel.cis.vsl.tass.model.IF.variable.BoundVariableIF;
import edu.udel.cis.vsl.tass.model.IF.variable.FormalVariableIF;
import edu.udel.cis.vsl.tass.model.IF.variable.ProcessVariableIF;
import edu.udel.cis.vsl.tass.model.IF.variable.SharedVariableIF;
import edu.udel.cis.vsl.tass.model.IF.variable.VariableIF;
import edu.udel.cis.vsl.tass.model.impl.location.AllocateLocation;
import edu.udel.cis.vsl.tass.model.impl.location.AnySourceReceiveLocation;
import edu.udel.cis.vsl.tass.model.impl.location.AssertionLocation;
import edu.udel.cis.vsl.tass.model.impl.location.AssignmentLocation;
import edu.udel.cis.vsl.tass.model.impl.location.AssumeLocation;
import edu.udel.cis.vsl.tass.model.impl.location.BranchLocation;
import edu.udel.cis.vsl.tass.model.impl.location.ChoiceLocation;
import edu.udel.cis.vsl.tass.model.impl.location.ForLoopLocation;
import edu.udel.cis.vsl.tass.model.impl.location.InvocationLocation;
import edu.udel.cis.vsl.tass.model.impl.location.Location;
import edu.udel.cis.vsl.tass.model.impl.location.LoopLocation;
import edu.udel.cis.vsl.tass.model.impl.location.ReturnLocation;
import edu.udel.cis.vsl.tass.model.impl.location.SendLocation;
import edu.udel.cis.vsl.tass.model.impl.location.StandardReceiveLocation;
import edu.udel.cis.vsl.tass.model.impl.location.TerminalLocation;
import edu.udel.cis.vsl.tass.model.impl.scope.LocalScope;
import edu.udel.cis.vsl.tass.model.impl.scope.ModelScope;
import edu.udel.cis.vsl.tass.model.impl.scope.ProcessScope;
import edu.udel.cis.vsl.tass.model.impl.statement.AllocateStatement;
import edu.udel.cis.vsl.tass.model.impl.statement.AssertionStatement;
import edu.udel.cis.vsl.tass.model.impl.statement.AssignmentStatement;
import edu.udel.cis.vsl.tass.model.impl.statement.AssumeStatement;
import edu.udel.cis.vsl.tass.model.impl.statement.InvocationStatement;
import edu.udel.cis.vsl.tass.model.impl.statement.NoopStatement;
import edu.udel.cis.vsl.tass.model.impl.statement.ReceiveStatement;
import edu.udel.cis.vsl.tass.model.impl.statement.ReturnStatement;
import edu.udel.cis.vsl.tass.model.impl.statement.SendStatement;
import edu.udel.cis.vsl.tass.model.impl.statement.Statement;
import edu.udel.cis.vsl.tass.model.impl.variable.FormalVariable;
import edu.udel.cis.vsl.tass.model.impl.variable.LocalVariable;
import edu.udel.cis.vsl.tass.model.impl.variable.ProcessVariable;
import edu.udel.cis.vsl.tass.model.impl.variable.SharedVariable;
import edu.udel.cis.vsl.tass.model.impl.variable.Variable;
import edu.udel.cis.vsl.tass.util.Sourceable;

public class Model implements ModelIF {

	/** The scope object for this model. */
	private ModelScope modelScope;

	/**
	 * The input variable (type int) holding the number of arguments passed to
	 * the main function on process 0. May be null. If not null, must be an
	 * integer at least 1.
	 */
	private SharedVariableIF argcInput;

	/**
	 * The input variable which is an array of int of length argcInput holding
	 * the length of each input string on process 0. May be null. If not null,
	 * each entry will have length at least 1.
	 */
	private SharedVariableIF argLengthsInput;

	/**
	 * The input variable holding the actual input strings on process 0. This is
	 * a ragged array of dimension 2 of char. The length vector is
	 * argLengthsInput; this type is written char[argLengthsInput].
	 */
	private SharedVariableIF argsInput;

	/**
	 * A process global variable on process0 which is an array of pointer to
	 * char of length argc, holding a pointer to the first character of each
	 * input string. I.e., argvGlobal[i]=&argsInput[i][0].
	 */
	private ProcessVariableIF argvGlobal;

	/**
	 * Output variable to hold the output produced by main on process 0. May be
	 * null. If not null, has integer type.
	 */
	private SharedVariableIF mainOutput;

	/** Has this model been completed? */
	private boolean complete = false;

	private ModelFactoryIF factory;

	private int id;

	private String name;

	private int numProcs;

	private Process[] processes;

	private ExpressionIF trueExpression;

	private Collection<CollectiveAssertionIF> collectiveAssertions = new LinkedHashSet<CollectiveAssertionIF>();

	public Model(int id, String name, int numProcs, ModelFactoryIF factory) {
		if (name == null)
			throw new NullPointerException("null name");
		if (factory == null)
			throw new NullPointerException("null factory");
		if (numProcs <= 0)
			throw new IllegalArgumentException(
					"numProcs must be positive, not " + numProcs);
		this.id = id;
		this.name = name;
		this.numProcs = numProcs;
		this.factory = factory;
		this.modelScope = new ModelScope(factory.systemScope(), this);
		this.processes = new Process[numProcs];
		for (int i = 0; i < numProcs; i++) {
			processes[i] = new Process(this, i);
		}
		this.trueExpression = factory.booleanLiteralExpression(true);
	}

	@Override
	public void addToLocation(LocationIF location,
			CollectiveAssertionIF assertion, ExpressionIF expression) {
		// It's possible this assertion is a joint assertion from the spec.
		// If so, add it to our assertions.
		if (!assertion.processSet().contains(location.process()))
			throw new RuntimeException(
					"Internal error: Collective assertion does not belong to process:\n"
							+ assertion + "\n" + location.process());
		if (!collectiveAssertions.contains(assertion)) {
			collectiveAssertions.add(assertion);
		}
		((Location) location).setCollectiveAssertion(assertion);
		((Location) location).setCollectiveExpression(expression);
	}

	/**
	 * Checks a number of syntactic properties of the model and throws an
	 * exception if any of them fail. Also computes, loop bodies, read and write
	 * sets, etc. Puts model in "complete state".
	 */
	@Override
	public void complete() throws SyntaxException {
		modelScope.complete();
		processMainFunction();
		for (VariableIF variable : modelScope.variables()) {
			if (variable.type().kind() == TypeKind.ARRAY) {
				if (variable.dimensionExpressions() == null) {
					throw new SyntaxException(variable,
							"Need to set dimensions of this array variable");
				}
			}
		}
		for (Process process : processes) {
			process.complete();
		}
		complete = true;
	}

	private void processMainFunction() throws SyntaxException {
		Process proc0 = process(0);
		FunctionIF main = proc0.mainFunction();
		int numFormals = main.numFormals();

		if (numFormals == 0)
			return;
		if (numFormals != 2)
			throw new SyntaxException(main,
					"main function does not have 2 args");

		FormalVariableIF formal0 = main.formal(0);
		FormalVariableIF formal1 = main.formal(1);
		TypeIF integerType = factory.integerType();
		TypeIF characterType = factory.characterType();
		TypeIF arrayOfInt = factory.arrayType(integerType);
		TypeIF arrayOfPointerToChar = factory.arrayType(factory
				.pointerType(characterType));
		TypeIF arrayOfArrayOfChar = factory.arrayType(characterType, 2);
		ExpressionIF zero = factory.integerLiteralExpression(0);
		ExpressionIF one = factory.integerLiteralExpression(1);

		if (!formal0.type().equals(integerType)) {
			throw new SyntaxException(formal0,
					"First argument to main does not have integer type");
		}
		if (!arrayOfPointerToChar.equals(formal1.type())) {
			throw new SyntaxException(formal1,
					"Second argument to main does not have type array-of-pointer-to-char");
		}
		// add input variable "int TASS_argc"...
		this.argcInput = this.newInputVariable(integerType, "TASS_argc");

		LHSExpressionIF argcInputExpression = factory
				.variableExpression(argcInput);

		this.setAssumption(argcInput, factory.lessThanOrEqualsExpression(one,
				argcInputExpression)); // 1<=argc

		// add input variable "int TASS_argLengths[TASS_argc]"...
		this.argLengthsInput = this.newInputVariable(arrayOfInt,
				"TASS_argLengths");

		LHSExpressionIF argLengthsExpression = factory
				.variableExpression(argLengthsInput);

		// int TASS_argLengths[argc]...
		this.setArrayDimensions(argLengthsInput,
				new ExpressionIF[] { argcInputExpression });

		// add ragged input variable "char TASS_args[TASS_argLengths]"...
		this.argsInput = this.newInputVariable(arrayOfArrayOfChar, "TASS_args");

		// make TASS_args a ragged array of dimension 2 over char...
		this.setArrayDimensions(argsInput,
				new ExpressionIF[] { argLengthsExpression });

		BoundScopeIF argIndexScope = factory.newBoundScope(modelScope);
		BoundVariableIF indexL = factory.newBoundVariable("TASS_arg_index",
				integerType, argIndexScope);
		LHSExpressionIF indexLExpression = factory.variableExpression(indexL);

		// argLengths[i]:
		ExpressionIF read = factory.subscriptExpression(argLengthsExpression,
				indexLExpression);

		// 0<=i<argc:
		ExpressionIF indexBoundExpression = factory.andExpression(factory
				.lessThanOrEqualsExpression(zero, indexLExpression), factory
				.lessThanExpression(indexLExpression, argcInputExpression));

		// forall {int i | 0<=i<argc } 1<=argLengths[i]:
		this.setAssumption(argLengthsInput, factory.forallExpression(indexL,
				indexBoundExpression, factory.lessThanOrEqualsExpression(one,
						read)));
		this.argvGlobal = this.newProcessVariable(proc0, arrayOfPointerToChar,
				"TASS_argv");
		this.setArrayDimensions(argvGlobal,
				new ExpressionIF[] { argcInputExpression });

		BoundScopeIF argInitScope = factory.newBoundScope(proc0.scope());
		BoundVariableIF indexVariable = factory.newBoundVariable(
				"TASS_arg_init", integerType, argInitScope);
		ExpressionIF indexExpression = factory
				.variableExpression(indexVariable); // i
		ExpressionIF indexVariableRestriction = factory.andExpression(factory
				.lessThanOrEqualsExpression(zero, indexExpression), factory
				.lessThanExpression(indexExpression, argcInputExpression)); // 0<=i<argc
		LHSExpressionIF argsInputExpression = factory
				.variableExpression(argsInput);
		LHSExpressionIF expr1 = (LHSExpressionIF) factory.subscriptExpression(
				argsInputExpression, indexExpression); // TASS_args[i]
		LHSExpressionIF expr2 = (LHSExpressionIF) factory.subscriptExpression(
				expr1, zero); // TASS_args[i][0]
		ExpressionIF expr3 = factory.addressOfExpression(expr2); // &TASS_args[i][0]
		ExpressionIF lambda = factory.lambdaExpression(indexVariable,
				indexVariableRestriction, expr3); // lambda(i).&TASS_args[i][0]
		ExpressionIF arrayLambda = factory.arrayLambdaExpression(
				argcInputExpression, lambda);

		this.setInitializationExpression(argvGlobal, arrayLambda);

		TypeIF mainReturnType = main.returnType();

		if (mainReturnType != null && mainReturnType.kind() == TypeKind.INTEGER) {
			this.mainOutput = this.newOutputVariable(integerType,
					"TASS_main_out");
		}

	}

	/**
	 * The input variable (type int) holding the number of arguments passed to
	 * the main function on process 0. May be null. If not null, must be an
	 * integer at least 1.
	 */
	@Override
	public SharedVariableIF argcInput() {
		return argcInput;
	}

	/**
	 * The input variable which is an array of int of length argcInput holding
	 * the length of each input string on process 0. May be null. If not null,
	 * each entry will have length at least 1.
	 */
	@Override
	public SharedVariableIF argLengthsInput() {
		return argLengthsInput;
	}

	/**
	 * The input variable holding the actual input strings on process 0. This is
	 * a ragged array of dimension 2 of char. The length vector is
	 * argLengthsInput; this type is written char[argLengthsInput].
	 */
	@Override
	public SharedVariableIF argsInput() {
		return argsInput;
	}

	/**
	 * A process global variable on process0 which is an array of pointer to
	 * char of length argc, holding a pointer to the first character of each
	 * input string. I.e., argvGlobal[i]=&argsInput[i][0].
	 */
	@Override
	public ProcessVariableIF argvGlobal() {
		return argvGlobal;
	}

	/**
	 * Output variable to hold the output produced by main on process 0. May be
	 * null. If not null, has integer type.
	 */
	@Override
	public SharedVariableIF mainOutput() {
		return mainOutput;
	}

	@Override
	public boolean equals(Object object) {
		if (object instanceof Model) {
			Model that = (Model) object;

			return factory.equals(that.factory) && id == that.id;
		}
		return false;
	}

	@Override
	public int hashCode() {
		return id * 32768;
	}

	@Override
	public int id() {
		return id;
	}

	@Override
	public boolean isComplete() {
		return complete;
	}

	@Override
	public Collection<LocationIF> locationsWithLabel(String label) {
		Vector<LocationIF> result = new Vector<LocationIF>();

		for (ProcessIF process : processes) {
			result.addAll(process.locationsWithLabel(label));
		}
		return result;
	}

	@Override
	public ModelFactoryIF modelFactory() {
		return factory;
	}

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

	@Override
	public AllocateLocationIF newAllocateLocation(LocalScopeIF scope) {
		AllocateLocationIF location = new AllocateLocation(scope);

		complete = false;
		((Function) scope.function()).addLocation(location);
		return location;
	}

	@Override
	public AllocateStatementIF newAllocateStatement(
			AllocateLocationIF sourceLocation, LHSExpressionIF lhs,
			TypeIF elementType, ExpressionIF size) throws SyntaxException {
		AllocateStatement statement = new AllocateStatement(factory,
				sourceLocation, lhs, elementType, size);

		complete = false;
		((AllocateLocation) sourceLocation).setStatement(statement);
		return statement;
	}

	@Override
	public AnySourceReceiveLocationIF newAnySourceReceiveLocation(
			LocalScopeIF scope) {
		AnySourceReceiveLocationIF location = new AnySourceReceiveLocation(
				scope);

		complete = false;
		((Function) scope.function()).addLocation(location);
		return location;
	}

	@Override
	public AssertionLocationIF newAssertionLocation(LocalScopeIF scope) {
		AssertionLocationIF location = new AssertionLocation(scope);

		((Function) scope.function()).addLocation(location);
		complete = false;
		return location;
	}

	@Override
	public AssertionStatementIF newAssertionStatement(
			AssertionLocationIF sourceLocation, ExpressionIF assertion)
			throws SyntaxException {
		AssertionStatement statement = new AssertionStatement(factory,
				sourceLocation, assertion);

		((AssertionLocation) sourceLocation).setStatement(statement);
		complete = false;
		return statement;
	}

	@Override
	public AssertionStatementIF newAssertionStatement(
			AssertionLocationIF sourceLocation, ExpressionIF assertion,
			String message) throws SyntaxException {
		AssertionStatement statement = new AssertionStatement(factory,
				sourceLocation, assertion, message);

		((AssertionLocation) sourceLocation).setStatement(statement);
		complete = false;
		return statement;
	}

	@Override
	public AssignmentLocationIF newAssignmentLocation(LocalScopeIF scope) {
		AssignmentLocationIF location = new AssignmentLocation(scope);

		((Function) scope.function()).addLocation(location);
		complete = false;
		return location;
	}

	@Override
	public AssignmentStatementIF newAssignmentStatement(
			AssignmentLocationIF sourceLocation, LHSExpressionIF lhs,
			ExpressionIF rhs) throws SyntaxException {
		AssignmentStatement statement = new AssignmentStatement(factory,
				sourceLocation, lhs, rhs);

		((AssignmentLocation) sourceLocation).setStatement(statement);
		complete = false;
		return statement;
	}

	@Override
	public AssumeLocationIF newAssumeLocation(LocalScopeIF scope) {
		AssumeLocationIF location = new AssumeLocation(scope);

		complete = false;
		((Function) scope.function()).addLocation(location);
		return location;
	}

	@Override
	public AssumeStatementIF newAssumeStatement(
			AssumeLocationIF sourceLocation, ExpressionIF assumption)
			throws SyntaxException {
		AssumeStatement statement = new AssumeStatement(factory,
				sourceLocation, assumption);

		complete = false;
		((AssumeLocation) sourceLocation).setStatement(statement);
		return statement;
	}

	@Override
	public BranchLocationIF newBranchLocation(LocalScopeIF scope,
			ExpressionIF condition) {
		BranchLocationIF location = new BranchLocation(scope, condition);

		((Function) scope.function()).addLocation(location);
		complete = false;
		return location;
	}

	@Override
	public ChoiceLocationIF newChoiceLocation(LocalScopeIF scope) {
		ChoiceLocation location = new ChoiceLocation(scope);

		((Function) scope.function()).addLocation(location);
		complete = false;
		return location;
	}

	@Override
	public NoopStatementIF newChoiceStatement(ChoiceLocationIF sourceLocation,
			ExpressionIF guard) throws SyntaxException {
		NoopStatement statement = new NoopStatement(factory, sourceLocation,
				guard);

		((Location) sourceLocation).addOutgoing(statement);
		complete = false;
		return statement;
	}

	@Override
	public CollectiveAssertionIF newCollectiveAssertion(Sourceable sourceable,
			ProcessIF[] processes, String identifier, boolean isInvariant,
			boolean isJoint) {
		Collection<LocationIF> locations = new Vector<LocationIF>();
		Collection<ProcessIF> processCollection = new Vector<ProcessIF>();
		for (int i = 0; i < processes.length; i++) {
			processCollection.add(processes[i]);
		}
		CollectiveAssertionIF result = new CollectiveAssertion(
				processCollection, locations, identifier, isInvariant, isJoint);
		// Set source
		if (sourceable != null)
			result.setSource(sourceable.getSource());
		collectiveAssertions.add(result);
		return result;
	}

	@Override
	public NoopStatementIF newFalseBranchStatement(
			BranchLocationIF sourceLocation) throws SyntaxException {
		ExpressionIF guard = factory.notExpression(sourceLocation.condition());
		NoopStatement statement = new NoopStatement(factory, sourceLocation,
				guard);

		((BranchLocation) sourceLocation).setFalseBranch(statement);
		complete = false;
		return statement;
	}

	@Override
	public ForLoopLocationIF newForLoopLocation(LocalScopeIF scope,
			ExpressionIF condition) {
		Function function = (Function) scope.function();
		ForLoopLocationIF location = new ForLoopLocation(scope, condition);

		complete = false;
		function.addLocation(location);
		return location;
	}

	@Override
	public FormalVariableIF newFormalVariable(FunctionIF function, TypeIF type,
			String name, int index) throws SyntaxException {
		FormalVariable variable = new FormalVariable(name, type,
				(LocalScope) function.outermostScope(), index);

		((Function) function).setFormal(variable);
		complete = false;
		return variable;
	}

	@Override
	public FunctionIF newFunction(ProcessIF process, String name,
			TypeIF returnType, int numFormals) throws SyntaxException {
		Function function = new Function(process.scope(), name, returnType,
				numFormals);

		((Process) process).addFunction(function);
		complete = false;
		return function;
	}

	@Override
	public SharedVariableIF newInputVariable(TypeIF type, String name)
			throws SyntaxException {
		SharedVariable variable = new SharedVariable(name, type,
				SharedVariable.SharedKind.INPUT, modelScope);

		modelScope.addSharedVariable(variable);
		complete = false;
		return variable;
	}

	@Override
	public InvocationLocationIF newInvocationLocation(LocalScopeIF scope) {
		InvocationLocationIF location = new InvocationLocation(scope);

		complete = false;
		((Function) scope.function()).addLocation(location);
		return location;
	}

	@Override
	public InvocationStatementIF newInvocationStatement(
			InvocationLocationIF sourceLocation, LHSExpressionIF lhs,
			FunctionIF callee, List<ExpressionIF> arguments)
			throws SyntaxException {
		InvocationStatement statement = null;
		if (callee instanceof SystemFunctionIF
				&& ((SystemFunctionIF) callee).guard() != null) {
			statement = new InvocationStatement(factory, sourceLocation, lhs,
					callee, arguments, ((SystemFunctionIF) callee).guard());
		} else {
			statement = new InvocationStatement(factory, sourceLocation, lhs,
					callee, arguments);
		}
		complete = false;
		((InvocationLocation) sourceLocation).setStatement(statement);
		return statement;
	}

	public LocalVariable newLocalVariable(LocalScope scope, TypeIF type,
			String name) throws SyntaxException {
		LocalVariable variable = new LocalVariable(name, type, scope);

		complete = false;
		scope.addProperLocalVariable(variable);
		return variable;
	}

	@Override
	public NoopStatementIF newLoopFalseBranchStatement(
			LoopLocationIF sourceLocation) throws SyntaxException {
		ExpressionIF guard = factory.notExpression(sourceLocation.condition());
		NoopStatement statement = new NoopStatement(factory, sourceLocation,
				guard);

		complete = false;
		((LoopLocation) sourceLocation).setFalseBranch(statement);
		return statement;
	}

	@Override
	public LoopLocationIF newLoopLocation(LocalScopeIF scope,
			ExpressionIF condition) {
		LoopLocationIF location = new LoopLocation(scope, condition);

		complete = false;
		((Function) scope.function()).addLocation(location);
		return location;
	}

	@Override
	public NoopStatementIF newLoopTrueBranchStatement(
			LoopLocationIF sourceLocation) throws SyntaxException {
		ExpressionIF guard = sourceLocation.condition();
		NoopStatement statement = new NoopStatement(factory, sourceLocation,
				guard);

		complete = false;
		((LoopLocation) sourceLocation).setTrueBranch(statement);
		return statement;
	}

	@Override
	public SharedVariableIF newOutputVariable(TypeIF type, String name)
			throws SyntaxException {
		SharedVariable variable = new SharedVariable(name, type,
				SharedVariable.SharedKind.OUTPUT, modelScope);

		complete = false;
		modelScope.addSharedVariable(variable);
		return variable;
	}

	public ProcessVariable newProcessVariable(ProcessIF process, TypeIF type,
			String name) throws SyntaxException {
		ProcessVariable variable = new ProcessVariable(name, type,
				(ProcessScope) process.scope());

		complete = false;
		((Process) process).addProcessVariable(variable);
		return variable;
	}

	@Override
	public ReceiveStatementIF newReceiveStatement(
			ReceiveLocationIF sourceLocation, LHSExpressionIF buffer,
			ExpressionIF source, ExpressionIF tag) throws SyntaxException {
		return newReceiveStatement(sourceLocation, buffer, source, tag, null);
	}

	@Override
	public ReceiveStatementIF newReceiveStatement(
			ReceiveLocationIF sourceLocation, LHSExpressionIF buffer,
			ExpressionIF source, ExpressionIF tag, LHSExpressionIF size)
			throws SyntaxException {
		ReceiveStatement statement = new ReceiveStatement(factory,
				sourceLocation, buffer, source, tag, size);

		complete = false;
		if (sourceLocation instanceof StandardReceiveLocation) {
			((StandardReceiveLocation) sourceLocation).setStatement(statement);
		} else if (sourceLocation instanceof AnySourceReceiveLocation) {
			AnySourceReceiveLocation location = (AnySourceReceiveLocation) sourceLocation;

			location.addOutgoing(statement);
			if (location.getSource() == null && statement.getSource() != null) {
				location.setSource(statement.getSource());
			}
		} else {
			throw new IllegalArgumentException(
					"Unknown receive location type: " + sourceLocation);
		}
		return statement;
	}

	@Override
	public ReturnLocationIF newReturnLocation(LocalScopeIF scope) {
		ReturnLocation location = new ReturnLocation(scope);

		complete = false;
		((Function) scope.function()).addLocation(location);
		return location;
	}

	@Override
	public ReturnStatementIF newReturnStatement(
			ReturnLocationIF sourceLocation, ExpressionIF result)
			throws SyntaxException {
		ReturnStatement statement = new ReturnStatement(factory,
				sourceLocation, result);

		complete = false;
		((ReturnLocation) sourceLocation).setStatement(statement);
		return statement;
	}

	@Override
	public SendLocationIF newSendLocation(LocalScopeIF scope) {
		SendLocation location = new SendLocation(scope);

		complete = false;
		((Function) scope.function()).addLocation(location);
		return location;
	}

	@Override
	public SendStatementIF newSendStatement(SendLocationIF sourceLocation,
			LHSExpressionIF buffer, ExpressionIF dest, ExpressionIF tag)
			throws SyntaxException {
		SendStatement statement = new SendStatement(factory, sourceLocation,
				buffer, dest, tag);

		complete = false;
		((SendLocation) sourceLocation).setStatement(statement);
		return statement;
	}

	public SharedVariableIF newSharedVariable(TypeIF type, String name)
			throws SyntaxException {
		SharedVariable variable = new SharedVariable(name, type,
				SharedVariable.SharedKind.GENERAL, modelScope);

		complete = false;
		modelScope.addSharedVariable(variable);
		return variable;
	}

	@Override
	public StandardReceiveLocationIF newStandardReceiveLocation(
			LocalScopeIF scope) {
		StandardReceiveLocationIF location = new StandardReceiveLocation(scope);

		complete = false;
		((Function) scope.function()).addLocation(location);
		return location;
	}

	@Override
	public void setGuard(SystemFunctionIF function, ExpressionIF guard)
			throws SyntaxException {
		factory.checkScope(guard, function.outermostScope());
		((SystemFunction) function).setGuard(guard);
	}

	@Override
	public SystemFunctionIF newSystemFunction(String libraryName,
			ProcessIF process, String name, TypeIF returnType, int numFormals)
			throws SyntaxException {
		SystemFunction function = new SystemFunction(process.scope(), name,
				returnType, numFormals, trueExpression);

		((ModelFactory) factory).registerSystemFunction(libraryName, function);
		((Process) process).addFunction(function);
		complete = false;
		return function;
	}

	@Override
	public TerminalLocationIF newTerminalLocation(LocalScopeIF scope) {
		TerminalLocation location = new TerminalLocation(scope);

		complete = false;
		((Function) scope.function()).addLocation(location);
		return location;
	}

	@Override
	public NoopStatementIF newTrueBranchStatement(
			BranchLocationIF sourceLocation) throws SyntaxException {
		ExpressionIF guard = sourceLocation.condition();
		NoopStatement statement = new NoopStatement(factory, sourceLocation,
				guard);

		complete = false;
		((BranchLocation) sourceLocation).setTrueBranch(statement);
		return statement;
	}

	@Override
	public int numProcs() {
		return numProcs;
	}

	@Override
	public void print(PrintWriter out) {
		print(out, false);
	}

	@Override
	public void print(PrintWriter out, boolean withSource) {
		out.println("begin model " + name);
		out.println("| begin input variables");
		for (VariableIF variable : modelScope.inputVariables()) {
			out.println("| | " + variableDeclaration(variable));
			if (withSource) {
				out.println("| | | " + variable.getSource());
			}
		}
		out.println("| end input variables;");
		out.println("| begin output variables");
		for (VariableIF variable : modelScope.outputVariables()) {
			out.println("| | " + variableDeclaration(variable));
			if (withSource) {
				out.println("| | | " + variable.getSource());
			}
		}
		out.println("| end output variables;");
		if (!modelScope.properSharedVariables().isEmpty()) {
			out.println("| begin proper shared variables");
			for (VariableIF variable : modelScope.properSharedVariables()) {
				out.println("    " + variableDeclaration(variable));
				if (withSource) {
					out.println("    | " + variable.getSource());
				}
			}
			out.println("| end proper shared variables;");
		}
		for (Process process : processes) {
			process.print("| ", out, withSource);
		}
		out.println("end model " + name + ".");
		out.flush();
	}

	@Override
	public Process process(int pid) {
		return processes[pid];
	}

	@Override
	public void setArrayDimensions(VariableIF arrayVariable,
			ExpressionIF[] dimensions) throws SyntaxException {
		if (arrayVariable.type().kind() != TypeKind.ARRAY)
			throw new IllegalArgumentException("Variable is not array: "
					+ arrayVariable);
		if (arrayVariable instanceof FormalVariableIF)
			throw new IllegalArgumentException(
					"Formal parameter variables of array type cannot have specific dimensions: "
							+ arrayVariable);
		((Variable) arrayVariable).setDimensions(dimensions);
		complete = false;
	}

	@Override
	public void setAssumption(SharedVariableIF inputVariable,
			ExpressionIF assumption) throws SyntaxException {
		if (inputVariable == null)
			throw new NullPointerException("null inputVariable");
		if (!modelScope.inputVariables().contains(inputVariable))
			throw new IllegalArgumentException(
					"Variable is not an input variable: " + inputVariable);
		if (assumption != null && assumption.type().kind() != TypeKind.BOOLEAN)
			throw new SyntaxException(assumption,
					"Assumption for input variable " + inputVariable
							+ " is not a boolean valued expression");
		((SharedVariable) inputVariable).setAssumption(assumption);
	}

	@Override
	public void setCorrespondingLocation(LocationIF location,
			LocationIF correspondingLocation) {
		((Location) location).setCorrespondingLocation(correspondingLocation);
	}

	@Override
	public void setCorrespondingVariable(SharedVariableIF variable,
			SharedVariableIF correspondingVariable) throws SyntaxException {
		if (variable == null) {
			throw new NullPointerException(
					"null variable in setCorrespondingVariable");
		}
		if (correspondingVariable == null) {
			throw new NullPointerException(
					"null correspondingVariable in setCorrespondingVariable");
		}
		if (!modelScope.variables().contains(variable)) {
			throw new SyntaxException(variable,
					"Variable not contained in model " + this);
		}
		((SharedVariable) variable)
				.setCorrespondingVariable(correspondingVariable);
	}

	@Override
	public void setExitLocation(BranchLocationIF branchLocation,
			LocationIF exitLocation) {
		complete = false;
		exitLocation.setOpenLocation(branchLocation);
		((BranchLocation) branchLocation).setExitLocation(exitLocation);
	}

	@Override
	public void setInitializationExpression(VariableIF variable,
			ExpressionIF expression) throws SyntaxException {
		((Variable) variable).setInitializationExpression(expression);
	}

	@Override
	public void setLabel(LocationIF location, String label) {
		complete = false;
		if (location == null)
			throw new NullPointerException("null location");
		((Location) location).setLabel(label);
	}

	@Override
	public void setMainFunction(ProcessIF process, FunctionIF function)
			throws SyntaxException {
		complete = false;
		if (!this.equals(process.model()))
			throw new IllegalArgumentException(
					"process belongs to different model: " + process.model());
		((Process) process).setMainFunction(function);
	}

	@Override
	public void setStartLocation(FunctionIF function, LocationIF location) {
		complete = false;
		((Function) function).setStartLocation(location);
	}

	@Override
	public void setTargetLocation(StatementIF statement,
			LocationIF targetLocation) throws SyntaxException {
		complete = false;
		if (!statement.function().equals(targetLocation.function())) {
			throw new SyntaxException(statement,
					"Target location in different function from statement: "
							+ targetLocation.function() + ", "
							+ statement.function());
		}
		((Statement) statement).setTargetLocation(targetLocation);
		((Location) targetLocation).addIncoming(statement);
	}

	@Override
	public String toString() {
		return name;
	}

	private String variableDeclaration(VariableIF variable) {
		String result = variable + " : " + variable.decl();

		if (variable.initializationExpression() != null) {
			result += " = " + variable.initializationExpression();
		}
		result += ";";
		return result;
	}

	@Override
	public Collection<CollectiveAssertionIF> collectiveAssertions() {
		return collectiveAssertions;
	}

	@Override
	public LocalScope newLocalScope(LocalScopeIF parent) {
		LocalScope newScope = ((Function) parent.function()).newScope(parent);

		return newScope;
	}

	@Override
	public VariableIF newVariable(ScopeIF scope, TypeIF type, String name)
			throws SyntaxException {
		switch (scope.kind()) {
		case SYSTEM:
			throw new IllegalArgumentException(
					"Should use ModelFactoryIF to create system-level variable");
		case MODEL:
			return newSharedVariable(type, name);
		case PROCESS:
			return newProcessVariable(((ProcessScope) scope).process(), type,
					name);
		case LOCAL:
			return newLocalVariable((LocalScope) scope, type, name);
		case BOUND:
			throw new IllegalArgumentException(
					"Should use ModelFactoryIF to create bound variables");
		default:
			throw new IllegalArgumentException("Unknown kind of scope: "
					+ scope.kind());
		}
	}

	@Override
	public ModelScope scope() {
		return modelScope;
	}
}