= 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 ==
 * !BoundVariable
 * !FormalVariable
 * !LocalVariable
 * !ProcessVariable
 * !SharedVariable
== Types ==
 * !ArrayType
 * !FunctionType
 * !PointerType
 * !RecordType
== Expressions ==
 * !PlusExpression
 * !TimesExpression
 * !DivideExpression
 * !AddressOfExpression
 * LHSExpression
   * !DereferenceExpression
   * !RecordNavigationExpression
 * !ExistsExpression
 * !ForallExpression
 * !IfThenElseExpression
 * !LiteralExpression
 * !NotEmptyExpression
 * !NotFullExpression
 * !QuantifierExpression
 * !VariableExpression
== Statements ==
 * !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.