Recursion is supported in the protocol definition by defining a
'rec' keyword with a label prior to a block, that defines the scope of the recursive
behaviour, and at some point in the enclosed behaviour, the
same label is used to show where the recursion
should be performed. The label can only be used within the
scope of the recursion block to which the label has been
associated.

rec <Label> "{"
    ...
    <Label> ";"
"}"

The following example shows a recursion construct defined using the
label 'Transaction'. Within the associated block, the recursion is
triggered by the 'Transaction' clause.

rec Transaction {
    ...
	Transaction;
}