Constructors

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 protocol construction.

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), by 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.