LocationIF.java

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

import java.util.Collection;

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.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.scope.LocalScopeIF;
import edu.udel.cis.vsl.tass.model.IF.statement.StatementIF;
import edu.udel.cis.vsl.tass.util.Sourceable;

public interface LocationIF extends Sourceable {

	public enum LocationKind {
		ALLOCATE,
		ASSERTION,
		ASSUME,
		ASSIGNMENT,
		CHOICE,
		INVOCATION,
		RECEIVE,
		RETURN,
		SEND,
		TERMINAL
	};

	/** The scope associated to this location. */
	LocalScopeIF scope();

	/**
	 * One may associate any number of objects to the location. These objects
	 * are known as "annotations". Each annotation has a key (a string unique to
	 * this location). This method returns the current set of all annotation
	 * keys.
	 * <p>
	 * Annotations can be used to store (co-)invariant expressions, loop
	 * unrolling ratios, a list of corresponding locations, and so on.
	 */
	Collection<String> annotationKeys();

	/**
	 * Returns the annotation with the given key, or null if there is no
	 * annotation with that key.
	 */
	Object getAnnotation(String key);

	/**
	 * Adds an annotation with given key to this location. Will replace an old
	 * one if same key was used.
	 */
	void putAnnotation(String key, Object annotation);

	/**
	 * Each location falls into one of the categories enumerated in
	 * LocationKind. Each category has a corresponding Java type (an interface).
	 * Note that branch locations and loop locations are special cases of the
	 * CHOICE kind.
	 */
	LocationKind kind();

	/**
	 * A loop location is a special kind of choice location. It represents the
	 * head of a while loop. If this method returns true, then this location is
	 * an instance of LoopLocationIF.
	 */
	boolean isLoop();

	/**
	 * A branch location is a special kind of CHOICE location. It represents an
	 * if..then or if..then..else statement. If this method returns true, then
	 * this location is an instance of BranchLocationIF.
	 */
	boolean isBranch();

	/**
	 * The unique ID number for this location. It is unique within the
	 * containing function.
	 */
	int id();

	/** Label associated to this location. May be null. */
	String label();

	/** The function to which this location belongs */
	FunctionIF function();

	ProcessIF process();

	ModelIF model();

	/** The collection of statements departing from this location. */
	Collection<StatementIF> statements();

	/** The collection of statements whose target location is this location. */
	Collection<StatementIF> incomingStatements();

	/**
	 * The outgoing statements are ordered in a linked list: this gives first
	 * element:
	 */
	StatementIF firstStatement();

	/** Last outgoing statement. */
	StatementIF lastStatement();

	/**
	 * Is this a local location? A local location is a location for which all
	 * outgoing statements are local statements. See StatementIF for a
	 * definition of local statement. This can only be called after model is
	 * complete.
	 */
	boolean isLocal();

	/**
	 * Returns the corresponding location for this location.
	 * 
	 */
	LocationIF correspondingLocation();

	/**
	 * Returns the collective assertion associated to this location, if there is
	 * one. Otherwise returns null.
	 */
	CollectiveAssertionIF collectiveAssertion();

	/**
	 * If there is a collective assertion associated to this location, this
	 * returns the assertion expression associated to this location. Otherwise,
	 * returns null.
	 * */
	ExpressionIF collectiveExpression();

	/**
	 * If this location is the closing location for a compound statement block
	 * (e.g., "if..then", "if..then..else", "while", "select"), then this method
	 * returns the location that opened that compound block. Otherwise, it
	 * returns null.
	 */
	LocationIF openLocation();

	/** Sets the open location for this location. Initially, this is null. */
	void setOpenLocation(LocationIF openLocation);

}