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.
Last updated: July 17, 2006
Send comments and questions to ma@kestrel.edu, dusko@kestrel.edu. For more information, see also Dusko's homepage
