Datatypes

bit (1 bit)
bool (1 bit)
byte (8 bits unsigned)
short (16* bits signed)
int (32* bits signed)
unsigned (≤ 32* bits unsigned)
      * - for a 32-bit machine
pid
chan
mtype = { name, name, ... }
typedef typename { seq. of declarations }

Operators (descending precendence)

() [] . ! ~ ++ -- * / % + - << >>
< <= > >= == != & ^ | && ||
( .. -> .. : .. ) conditional expression

Predefined

Constants - true, false
Variables - (read-only except _):
     _ - write-only hidden scratch variable
     _nr_pr - number of processes
     _pid instance number of executing process
     timeout no exec. statements in the system?

Preprocessor

#define name (arguments) string
#undef, #if, #ifdef, #ifndef, #else, #endif
#include "file name"
inline name (arguments) { ... }

Statements

mtype var; - variable declaration
mtype var[N]; - array declaration
var = expr, var++, var--
assert(expression)

printf, printm - print to standard output
     %c (character), %d (decimal), %e (mtype),
     %o (octal), %u (unsigned), %x (hex)
scanf - read from standard input

Statements (ctd)

skip - no operation
break - exit innermost do loop
goto - jump to label
Label prefixes with special meaning:
     accept - accept cycle
     end - valid end state
     progress - non-progress cycle
atomic { ... } - execute without interleaving
d_step { ... } - execute deterministically
(no jumping in or out; deterministic choice
among true guards; only the first statement
can block)
{ ... } unless { ... }- exception handling

Guarded commands

if :: guard -> statements :: .. fi
do :: guard -> statements :: .. od
else guard - executed if all others are false

Processes

Declaration - proctype procname (parameters) { ... }
Activate with prefixes - active or active[N]
Explicit process activation - run procname (arguments)
Initial process - init { ... }
Declaration suffixes:
     priority - set simulation priority
     provided (e) - executable only if e is true

Channels

chan ch = [capacity] of { type, type, ... }

Channels (ctd)

Matching in a receive statement: constants and mtype
symbols must match; variables are assigned the
values in the message; eval(e) forces a match
with the current value of the expression.

len(ch) - number of messages in a channel
empty(ch) / nempty(ch) - is channel (not) empty?
full(ch) / nfull(ch) - is channel (not) full?

Channel use assertions:
     xr ch - channel ch is receive-only in this process
     xs ch - channel ch is send-only in this process

Temporal logic

Remote references

Test the control state or value of a variable:
     process-name @ label-name
     process-name [ expression ] @ label-name
     process-name : label-name
     process-name [ expression ] : label-name

LTL formula

Variable declaration prefixes

Comments