A graphical editor and analyzer for coloured Petri nets, built in Python with Tkinter.
Groupe 3 — Hadil Maadi, Maeva Rechak-Lambert, Rafaelle Bueno, Tiphaine Brun, Natasha Litherland ID4 — CY Cergy Paris University — Graph Theory, Semester 1, 2025–2026 Prof. Zaouche Djaouida
A Petri net is a mathematical and graphical model used to represent and analyze complex systems with discrete events — systems where state changes happen at specific moments in response to well-defined triggers. First introduced in Carl Adam Petri's 1962 doctoral thesis, they are widely used for modeling, simulation, and verification of dynamic behavior.
This project is a fully interactive Petri net editor and simulator. Users can build networks visually, fire transitions, and run formal analyses — all within a GUI. It supports both standard (anonymous token) networks and coloured Petri nets, where tokens carry a type (colour) that encodes additional information.
Editing
- Add, modify, and delete places, transitions, and arcs via a graphical canvas
- Set place capacities and initial token counts
- Configure arc weights by colour and quantity (for coloured nets)
- Named places and transitions, repositionable on the canvas
Simulation
- Fire transitions manually; the GUI validates firing conditions before executing
- Tokens displayed as coloured dots arranged in a spiral inside places
- Real-time visual refresh after every state change
- Atomic token movement: all tokens consumed and produced in a single operation
Analysis
- Reachability / state space exploration via DFS and BFS
- Boundedness check: verifies that token counts in all places stay below a defined limit across all reachable states
- Deadlock detection: identifies states where no transition is fireable
- Liveness analysis: uses Tarjan's strongly connected components algorithm to verify that all transitions remain potentially fireable (L4 liveness)
- Invariants: checks place invariants (token conservation across transitions) and transition invariants
Import / Export
- Save and load networks as JSON files
- Export canvas as PNG (requires Graphviz)
├── main.py # Entry point — launches the Tkinter window
├── reseau_de_petri.py # Core Petri net class (places, transitions, arcs, coloured tokens)
├── petri_gui.py # Graphical interface (PetriGUI class, canvas rendering, toolbar)
├── petri_propriete.py # Analysis class (boundedness, deadlock, liveness via Tarjan)
├── json_sauv_import.py # JSON save and load
├── test_petri.py # Unit tests
└── README.md # This file
The ReseauPetri class is the single source of truth for the network's state. It manages:
- Places: each defined by a name, a list of coloured tokens, and an optional capacity limit. Capacity enforcement prevents token overflow and guards against infinite cycles.
- Transitions: fire atomically once
is_enabled()confirms (1) sufficient tokens of the right colours in input places and (2) enough remaining capacity in output places. - Arcs: directed connections between places and transitions (or vice versa), each carrying a dictionary of
{colour: quantity}pairs that define what is consumed or produced on firing.
For simple (non-coloured) networks, tokens default to black and arc weights default to 1, making the model behave as a classical Petri net.
PetriGUI is a visual wrapper over ReseauPetri. It captures user clicks, dispatches them to backend methods, and redraws the canvas on every state change via a refresh() call. The GUI never maintains its own model state — it always queries the backend, which prevents desynchronization.
Key rendering choices:
- Arrow anchor points are computed mathematically so arcs connect cleanly to the edges of circles (places) and rectangles (transitions) regardless of node position
- coloured tokens are drawn as small dots in a spiral pattern inside places, giving a quick visual read of load and token distribution
- Dialog windows collect textual input (arc weights, place names) without cluttering the main canvas
The toolbar mode system works as follows: clicking a toolbar button sets an internal mode variable; the next click on the canvas is interpreted according to that mode (e.g., mode Arc means the next two clicks define source and destination).
State space exploration
Both DFS and BFS build the same output: a dictionary of known states (etats_connus) and an adjacency dictionary (structure_graphe). The difference is traversal order:
- DFS uses a LIFO stack, going as deep as possible before backtracking
- BFS uses a FIFO queue, exploring states level by level — useful for finding shortest transition sequences
Boundedness
Starting from the initial marking, all reachable states are explored. If any place ever holds more than the defined limit (default: 10 tokens), the network is flagged as potentially unbounded.
Deadlock
Simple check: for a given state, if no transition satisfies is_enabled(), the state is a deadlock (sink state).
Liveness (Tarjan's algorithm)
The state graph is analyzed for strongly connected components (SCCs). A terminal SCC — one from which you cannot exit — is a trap. Any transition that does not appear within a terminal SCC is unreachable once the system enters that loop, making it a dead transition. If any dead transition is found, the network is not live (not L4).
Each node receives a unique index on first visit. A lowlink value tracks the lowest index reachable from that node. When a node's lowlink equals its own index, it is the root of an SCC.
Requirements
- Python 3.x
tkinter(usually bundled with Python; see note for macOS below)Adafruit_NeoPixelis not required — this is a pure Python projectgraphviz(optional, only needed for PNG export):pip install graphviz
Run
python main.pyA 1200×800 window will open titled Simulateur de Réseau de Pétri.
macOS note: The default system Python on macOS often ships with an outdated version of Tkinter that causes display issues. Use a Python installation from python.org or via Homebrew instead.
Windows / Linux: No known platform-specific issues beyond the above.
| Action | How |
|---|---|
| Add a place | Click + Place, then click on the canvas |
| Add a transition | Click + Transition, then click on the canvas |
| Add an arc | Click + Arc, click source node, then destination node; a dialog will ask for arc weights |
| Fire a transition | Click Tir, then click the transition to fire |
| Modify an element | Click Modifier, then click the element |
| Delete an element | Click Supprimer, then click the element |
| Run analysis | Click Check for deadlock/boundedness/liveness, or Invariants for invariant checks |
| Export PNG | Click Export PNG (requires Graphviz) |
| Save / Load JSON | Click Sauver JSON or use the import option |
| New network | Click Nouveau to reset |
When creating or modifying a place, tokens are specified as a comma-separated list:
rouge:3, bleu:2, vert:1
Arc weights follow the same format. If no colour is specified, tokens default to black (standard mode).
Explores the state space by always following the most recently discovered state first (LIFO stack). Used to generate the full reachability graph and detect cycles.
Explores states level by level from the initial marking (FIFO queue). Finds shortest paths between states and is used as the basis for liveness analysis.
Detects strongly connected components in the state graph for liveness verification. A component is "strongly connected" if every state within it is reachable from every other. Terminal SCCs that trap the system without containing all transitions indicate dead transitions and a non-live network.
| Area | Issue |
|---|---|
| JSON re-import | Saved JSON files cannot be fully reloaded into the state-space explorer for deeper analysis — the import/export and analysis pipelines are not fully integrated |
| Cross-platform rendering | Some elements rendered differently across Windows, Linux, and macOS during development; minor visual inconsistencies may remain |
| State space size | For large or unbounded networks, state space exploration can become memory- and time-intensive |
| Boundedness threshold | The boundedness limit (default 10 tokens) is hardcoded; very large valid networks may be incorrectly flagged |
| No undo | There is no undo/redo mechanism; deletions are permanent until the session is reset |
- Separating backend logic from GUI rendering cleanly (the
refresh()pattern) prevents state desynchronization and made debugging significantly easier - Tarjan's algorithm is elegant but requires careful index/lowlink bookkeeping — working through it as a group helped clarify the logic
- coloured Petri nets dramatically increase expressiveness but also analysis complexity; the token colour dictionary approach was a practical compromise
- Working across different operating systems (Windows, Linux, macOS) revealed unexpected Tkinter rendering differences that cost significant debugging time
- Git workflow discipline — especially avoiding parallel edits to the same file — is as important as the code itself
- Agree on the full data structure before splitting into parallel workstreams — the mid-project backend refactor cost significant time
- Integrate JSON export/import with the analysis pipeline from the start
- Allocate more people to the frontend earlier; GUI work was underestimated
- Work in person more — remote collaboration without video calls made it easy to silently diverge on implementation decisions
| Name | |
|---|---|
| Hadil Maadi | maadihadil@cy-tech.fr |
| Maeva Rechak-Lambert | rechaklamb@cy-tech.fr |
| Rafaelle Bueno | buenorafae@cy-tech.fr |
| Tiphaine Brun | bruntiphai@cy-tech.fr |
| Natasha Litherland | litherland@cy-tech.fr |
A major source of inspiration for this project was petrinetsimulator.com :)
Academic project — CY Cergy Paris University, 2025–2026. Shared freely for learning and reference.