= 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."
== 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 ==