StatementIF.java

package edu.udel.cis.vsl.tass.model.IF.statement;

import java.io.PrintWriter;

import edu.udel.cis.vsl.tass.model.IF.FunctionIF;
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.expression.ExpressionIF;
import edu.udel.cis.vsl.tass.model.IF.location.LocationIF;
import edu.udel.cis.vsl.tass.util.Sourceable;

public interface StatementIF extends Sourceable {

	public enum StatementKind {
		ALLOCATE,
		ASSERTION,
		ASSIGNMENT,
		ASSUME,
		INVOCATION,
		NOOP,
		RECEIVE,
		RETURN,
		SEND
	};

	StatementKind kind();

	FunctionIF function();

	ProcessIF process();

	ModelIF model();

	LocationIF sourceLocation();

	LocationIF targetLocation();

	ExpressionIF guard();

	/**
	 * Statements emanating from a location are ordered in a linked list. This
	 * method gives next outgoing statement from same source location:
	 */
	StatementIF next();

	/**
	 * Tells whether or not this is a "local" statement.
	 * 
	 * Let T be the set of all variables other than proper shared variables.
	 * 
	 * This is a local statement if:
	 * <ul>
	 * <li>this is an assertion or assume statement and all variables in the
	 * expression are in T,
	 * <li>this is an assignment statement and all variables on lhs and rhs are
	 * in T,
	 * <li>this is an invocation statement and all variables in the actual
	 * arguments and on lhs are in T,
	 * <li>this is a noop statement and all variables in the guard are in T, or
	 * <li>this is a return statement and all variables in the returned
	 * expression are in T,
	 * </ul>
	 * 
	 */
	boolean isLocal();

	void print(PrintWriter out);
}