Parameters
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.
Examples:
//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.