This section describes Constructors through one example. However,
at this point, Constructors are being rethought, and subsequent Pda
versions will most likely implement them in a different fashion. You
are not advised at this point to use them.
Constructors capture a wide space of protocol transformations.
They work like macro recorders. To define a new constructor, you have
to specify its parameters by dragging the desired protocols into the
constructor window. After that you generate the resulting protocol out
of the constructor parameters using the same tools available for
For example, we will define a constructor binding that will replace
the second and the third message in protocol
Two_CR[I, R](c, r, c0, r0),
b(I, R, m0, m1) obtaining protocol
CR2[I, R](c, b, r0).
The structure of the final derivation can be explored in the workspace or
with the derivation browser.