Examples

A list of examples is available in the default installation of the client. You can inspect them by loading the corresponding file, verifying all processes and compositions and viewing their graphs.

The following examples are included:

1. SimpleCopyAndSequence.json: Simple example demonstrating the copy node and 2 separate methods of serial sequential composition. Inspection of the graph and underlying π-calculus structure shows the difference between composing right-to-left (simpler structure) and left-to-right (introduces axiom buffers).

2. SimpleOptionalTreatment.json: Simple healthcare-inspired example demonstrating resource accounting when handling optional/exceptional outcomes as presented in:

   • A Pragmatic, Scalable Approach to Correct-by-construction Process Composition Using Classical Linear Logic Inference

3. BuySki.json: Example of a workflow for buying Ski equipment as presented in:

   • A theorem proving framework for the formal verification of Web Services Composition

4. HomePurchase.json: Example of a workflow for purchasing property as presented in:

   • Formal verification of Web Services composition using linear logic and the pi-calculus

5. HealthcareHandover.json: Example of 2 patient handover workflows via assignment and delegation, as presented in:

   • Formal verification of collaboration patterns in healthcare
   • Rigorous process-based modelling of patterns for collaborative work in healthcare teams