= The MiniMP Intermediate Representation =
== Model ==
A model is an abstract representation of a MiniMP program.  It has a name, a set of shared variables, and a sequence of processes.
== Processes ==
Processes are numbered 0,1,...,n-1, where n is the number of processes.  The number n is fixed when the model is created and can never change.  The unique number associated to a process is known as the process's "pid."

Each process contains a number of process variables, and a number of functions.  One of the functions is designated the "main" function (though that function's name does not have to be "main").  In particular, every process must contain at least one function.
== Variables ==
There are four different scopes to which a variable may belong.
 * !SharedVariable

  Shared scope includes all input and output variables, and general shared variables; these are variables that can be accessed by any process.
 * !ProcessVariable

  Process variables have the scope of one process; they can be accessed by any function in that process.
 * !LocalVariable

  Local variables are local to a specific function in a specific process.  They can only be accessed within the function body.
  * !FormalVariable
 
      Formal variables are the formal parameters to a function.  They are a special type of local variable.
 * !BoundVariable

  Bound variables are specific to an expression;  these are variables from forall and exists statements.

== Types ==
 * !ArrayType
 * !FunctionType
 * !PointerType
 * !RecordType
== Expressions ==
 * !PlusExpression
 * !TimesExpression
 * !DivideExpression
 * !AddressOfExpression
 * LHSExpression
   * !DereferenceExpression
   * !RecordNavigationExpression
 * !ExistsExpression
 * !ForallExpression
 * !IfThenElseExpression
 * !LiteralExpression
 * !NotEmptyExpression
 * !NotFullExpression
 * !QuantifierExpression
 * !VariableExpression
== Locations ==
The locations fall into a number of categories, for the most part corresponding to the kinds of statements that can emanate from that location.  Some locations only allow one outgoing statement, while others allow several, and others none.
 * !AllocateLocation
 * !AssertionLocation
 * !AssignmentLocation
 * !AssumeLocation
 * !BranchLocation
 * !ChoiceLocation
 * !DeallocateLocation
 * !ForLoopLocation
 * !InvocationLocation
 * !ReceiveLocation
 * !ReturnLocation
 * !SendLocation
 * !TerminalLocation
== Statements ==
Each statement has a single source location and a single destination location.
 * !AllocateStatement
 * !AssertionStatement
 * !AssignmentStatement
 * !AssumeStatement
 * !DeallocateStatement
 * !InvocationStatement
 * !NoopStatement
 * !ReceiveStatement
 * !SendStatement
== Functions ==
A function specifies a number of formal parameters, or "formal variables."  In addition, it specifies a number of "proper local variables."  All of these (formal and proper locals) are referred to as "local variables."  The local variables can only be accessed within the function body.

The function body itself is a transition system.  The function contains a set of locations and a set of statements.  These define a directed graph in which the locations are nodes and the statements are edges.  A function has a designated "start location," and thus every function must have at least one location.