Primitive (and composite) processes may be parameterised. Parameters must always be specified with a default value. This means that LTSA can always generate an LTS. Actual parameters can be substituted in composite process definitions.


//Single slot Buffer process which stores a value in the range 0..Max
BUF(Max=3) = (in[x:0..Max]->out[Max]->BUF).

//Program variable with range L to U and initial value L
VAR(L=1,U=5) = VAR[L],
VAR[v:L..U]  = (write[x:L..U] -> VAR[x] | read[v] -> VAR[v]).

Parameter names must always start with an uppercase letter.