== Types ==
* boolean
* int
* double
* $proc : The process type.
* $scope : The scope type.

== Expressions ==

* +, - , * , / , %
* =
* ==, <=. >=, <, >
* ++, --
* $true, $false
* $self : The process invoking the expression (constant of type $proc).
* $spawn f(e1, ..., e_n) : Spawn a process executing f on (e1, ..., e_n), return a reference to the process.
* function calls

== Statements ==
* Expression statement : Use an expression as a statement (e.g. i++;).
* if-then-else statements : Same syntax as C.
* while, for loops
* $assert <expr> : Check that <expr> holds.
* $assume <expr> : Add <expr> to the path condition.
* $wait <expr> : For <expr> of type $proc, block until <expr> terminates.
* $when (<expr>) S; : Guarded statement.  Block until <expr> is true, then execute S.
* $choose : A $choose statement has the form 
{{{
  $choose {
  stmt1;
  stmt2;
  ...
  default: stmt
}
}}}
The "default" clause is optional.
The guards of the statements are evaluated and among those that are
true, one is chosen nondeterministically and executed.  If none are
true and the default clause is present, it is chosen.  The default
clause will only be selected if all guards are false.  If no default
clause is present and all guards are false, the statement blocks.
Hence the implicit guard of the $choose statement without a default
clause is the disjunction of the guards of its sub-statements.
The implicit guard of the $choose statement with a default clause
is "true".