Overview

PN2CCS is a web application built to be ran in modern web browsers. To run it, simply open the src/index.html file in a modern web browser with JavaScript enabled (see Supported Browsers).

The tool allows to input a Petri net (by drawing it using the graphical user interface or importing a P/T net PNML-file). The Petri net will then be classified in terms of the classes known by PN2CCS (see in Fig. 1 in [BBS24]) and encoded into a CCS process, if possible. For further details and how to use PN2CCS, then please click on the Help-button in the top right corner when you have the tool opened. You can also review the How to Reproduce Examples for a short introduction.

In addition, this repository also contains examples, see Examples for further details.

Publications

• [BBS24] Bogø, B., Burattin, A., & Scalas, A. (2024). Encoding Petri Nets into CCS. In Proceedings of the 26th International Conference on Coordination Models and Languages (Vol. 14676, pp. 38-55). Springer. https://doi.org/10.1007/978-3-031-62697-5_3
• [BBS??] Upcoming: Bogø, B., Burattin, A., & Scalas, A. PN2CCS: A Tool to Encode Petri Nets into Calculus of Communicating Systems.

Supported Browsers

The first version number is the minimum version that should be supported according to @mdn/browser-compat-data. The numbers in parentheses are the versions that have been tested. The tool shows a warning if it detects that the browser does not support all the needed functionality.

Desktop

• Google Chrome 79+ (129 on Windows 11)
• Microsoft Edge 79+ (129 on Windows 11)
• Mozilla Firefox 75+ (131 on Windows 11)
• Opera 66+ (113 on Windows 11)
• Safari 14.1+ (not tested!)

Android

• Google Chrome 79+ (115 on Android 10)
• Mozilla Firefox 79+ (127 on Android 10)
• Opera 57+ (83 on Android 14)
• Samsung Internet 12.0+ (not tested!)

iOS

• Safari 14.5+ (not tested!)

Petri Net Classification

The tool contains a (colored) Venn-diagram that shows the supported Petri nets and their relation. The tool can detect and encode the following classes (except general Petri nets):

• Petri net: Bipartite graph (not encodable).
• Group-choice net: For every pair of places they either have a same post set or disjointed post sets.
• 2-τ-synchronisation net: All transitions have at most 2 ingoing edges - transitions with 2 ingoing edges have label τ.
• CCS net: All transitions have 1 or 2 ingoing edges - transitions with 2 ingoing edges have label τ.
• Free-choice net: All places with multiple outgoing edges only have edges to transitions with one ingoing edge.
• Workflow net: Has one place i with no ingoing edges and one place o with no outgoing edges such that for every place/transition n, there is a path from i to o via n.
• Free-choice workflow net: Both a free-choice net and a workflow net.

Calculus of Communicating Systems (CCS) Syntax

Action: a Co-action: a Internal action: τ Inaction: 0 Prefix: μ.Q Choice: (P + P) Parallel: (Q | Q) Exponent: Qn Restriction: (νa)Q Constant: X where a is a visible action, τ is an internal (invisible) action, μ is a (co-)action or internal action, P is a sequential process (inaction, prefix or choice) and Q is a process (sequential process, parallel, exponent, restriction or constant).

Examples

The directory /examples/pnml contains PNML-files for all examples listed below. The directory /examples/images contains pdf/image-files for most of the Petri nets.

Files prefixed with a number (NN-xxx.pnml) corresponds to Petri nets shown in figures (Fig. NN) in [BBS24]. However, note that places and transitions can have different names in the tool (as these cannot be changed in the tool). Furthermore, the encoding might be different (but equivalent) in the tool because the encoding have nondeterministic choices (see line 11-12 in Algorithm 1 in [BBS24]).

Files prefixed with s (sNN-xxx.pnml) corresponds to Petri nets shown in figures (Fig. NN) in [BBS??].

Files prefixed with x (xN-xxx.pnml) are additional advanced examples not included in the papers. These examples only have PNML-files generated by other tools and might not give a good visual result for the Petri net in PN2CCS due to missing/bad positions or the fixed sized nodes in PN2CCS. In those cases (except x7-x9), please consult the images for a better visualization.

[BBS24] Encoding Petri Nets into CCS (10.1007/978-3-031-62697-5_3)

• 02-preliminaries-none [IMG] (group-choice net + CCS net*)
• 03-preliminaries-workflow [IMG] (group-choice net + workflow net + CCS net*)
• 04-preliminaries-free-choice [IMG] (group-choice net + free-choice net + CCS net*)
• 05-preliminaries-free-choice-workflow [IMG] (free-choice workflow net + CCS net*)
• 06-ccs-net-place-0 [IMG] (free-choice workflow net + CCS net**)
• 07-ccs-net-place-1 [IMG] (free-choice net + CCS net**)
• 08-ccs-net-place-3 [IMG] (free-choice net + CCS net**)
• 09-ccs-net-transition-0 [IMG] (free-choice net + 2-τ-synchronisation net**)
• 10-ccs-net-transition-1 [IMG] (free-choice net + 2-τ-synchronisation net**)
• 11-ccs-net-transition-2 [IMG] (free-choice net + 2-τ-synchronisation net**)
• 12-ccs-net-example [IMG] (2-τ-synchronisation net***)
• 14-free-choice-before [IMG] (free-choice net)
• 15-free-choice-after [IMG] (free-choice net)
• 16-group-choice-not [IMG] (Petri net)
• 17-group-choice-before [IMG] (group-choice net)
• 18-group-choice-after [IMG] (free-choice net + 2-τ-synchronisation net)

* The Petri net in [BBS24] has no labels/actions, so all transitions are labeled with τ in the PNML-file - and is therefore a CCS net.

** The encoding in [BBS24] only shows a partial encoding of a place/transition used to help understanding Algorithm 1 in [BBS24] while the tool produces a full encoding (using Algorithm 6 + Algorithm 4 in [BBS24]).

*** The encoding is not exactly as in [BBS24] (but equivalent) since s_2.X_p1 and \overline{s_2}.0 are swapped compared to [BBS24].

[BBS??] Upcoming

• s02-vending-machine [IMG] (free-choice workflow net)
• s03-sync-patterns [IMG] (group-choice net)
• s06-order-to-cash-process [IMG] (free-choice workflow net)

Extra Petri Nets

Fairly large models generated using PLG2:

• x1-net-1 [IMG] (free-choice workflow net)
• x2-net-2 [IMG] (free-choice workflow net)
• x3-net-3 [IMG] (free-choice workflow net)

Mined Petri nets using different process mining algorithms on the road traffic fines log:

• x4-road-traffic-fines-alpha [IMG] (free-choice net)
• x5-road-traffic-fines-inductive-miner [IMG] (free-choice workflow net)
• x6-road-traffic-fines-heuristics-miner [IMG] (free-choice workflow net)

Petri nets from the official PNML website pnml.org:

• x7-philo (Petri net - no image, positions are scaled for better visualization)
• x8-piscine (Petri net - no image)
• x9-token-ring (Petri net - no image)

How to Reproduce Examples

Below are instructions to reproduce examples. All examples can be imported as a PNML-file and there are step-by-step guides for a few examples.

Important: In the following, be aware that:

• Click refers to using the primary mouse button or tapping on the touch screen.
• Right-click refers to using the secondary mouse button or making a long tap on the touch screen.

Importing a PNML-file

Click on the Import PN-button, select a file in the dialog (on your device) and press the Import Petri net-button to import the Petri net. It centers the Petri net on the first place or transition. You can drag the Petri net to get a better view of it.

Step-by-Step Instructions for 17-group-choice-before [IMG]

1. Drag-and-drop 3 places onto the empty space. If you (by mistake) create a wrong place, right-click on the place and click Delete place in the dialog.
2. Click on p1 to select it (it becomes bold). Afterwards, you can drag p1 to move it. Move the places such that they form a vertical line with p1 at the top, p2 in the middle and p3 at the bottom. (You can move the entire Petri net by dragging the background.)
3. Drag-and-drop 3 transitions onto the empty space such that t1 is to the right of p1, t2 is to the right of p2 and t3 is to the right of p3.
4. If there is a selected (bold) node, make sure to deselect it by clicking on it again.
5. Click on p1 and then on t1 to draw an edge. Continue by drawing the following edges: (p2, t1), (p2, t2) and (p3, t3). If you (by mistake) make a wrong edge, right-click on the edge and click Delete edge in the dialog.
6. Notice that the current Petri net is a CCS net. Right-click on t1, then in the dialog, change the label to a and click Update transition. Repeat for t2 and t3 such that t2 gets label b and t3 gets label c.
7. Notice that the Petri net is no longer a CCS net (or any of the other encodable classes). Add the missing edge from p1 to t2 such that it becomes a group-choice net.
8. The number of tokens in a place can be changed by right-clicking on the place similar to how transition labels are changed.

Brief Step-by-Step Instructions for s06-order-to-cash-process [IMG]

1. Drag-and-drop places and transitions onto the empty space in a pattern similar to /examples/images/s06-order-to-cash-process.pdf. You can move a place/transition by clicking on it to select it (it becomes bold) and then drag it to its new position (click on it again to deselect it). You can move the entire Petri net by dragging the background. If you (by mistake) create a wrong place/transition, right-click on the place/transition and click Delete place/Delete transition in the dialog.
2. Add edges by first clicking on a place and then on a transition, or vice versa. If you (by mistake) make a wrong edge, right-click on the edge and click Delete edge in the dialog.
3. Right-click on the left most place (likely p1) to open a dialog. Enter 1 in the text field and click on Update place to set the number of tokens in the place.
4. Right-click each transition and enter their action labels similar to how the number tokens were set.