CSP2PN

Click here for a short description of the technique...

CSP2PN is a tool able to automatically transform a CSP specification into an equivalent Petri net. The Petri net is generated by using an instrumentation of the CSP's operational semantics which generates it as a side-effect. The Petri net generated produces the same sequences of visible events as the CSP specification. In CSP terminology, these sequences are the so-called traces. In Petri nets they correspond to the transition firing sequences.

You can find a more detailed description of the tool here, including the source files..

You can either write down the initial CSP specification or choose one from the list of examples.

Once the Petri net is generated (Generate Petri net) it is possible to visualize the it (View Petri net).
After the Petri net is generated, we also show the execution log of the instrumented semantics used by the transformation technique.

CSP2PN: Translating CSP to Petri nets

CSP specification

Petri net (PNML format)

Log