This page collects a non exhaustive list of tools that use SNAKES or that can be related to it. If you know a tool that should be listed here, please let me know.


Neco is a Petri net compiler: it takes a Petri net and builds a library that has all the primitives to explore the state space of the considered Petri net. This library is optimised in many ways, so that it allows to build fast state space traversal. Neco also provides a compiler for LTL formulas that produces an explicit LTL model-checker using the SPOT library. Neco-SPOT was awarded at the model-checking contest as the fastest and most reliable LTL model-checker for Petri nets. Neco is using SNAKES to handle Petri nets as well as to input them from various formats.


PNTooL is a python library for the modular construction of Petri nets transducers (PNTs) through composition operations. Constructed PNTs can be exported in an XML-format which is based on the standard PNML format developed for basic Petri net variants [5]. Moreover, PNTs can be visualised and pictures can be exported in all standard formats. PNTooL serves as a basis for the implementation and evaluation of algorithms for analysis, simulation and optimisation of PNTs.

Simulator GUI for Colored Petri Nets

A GUI to edit and simulate coloured Petri nets.


VMO-Score is a tool that allows improvisers and composers to construct an interactive musical environment directly from a musical recording. VMO-Score finds larger structures in an audio recording using the Variable Markov Oracle model and constructs an interactive score to control the improvisation. This score is modeled as a Time Petri Net (TPN) that allows artists to define transitions rules that impose logical and temporal constraints in the improvisation. VMO-Score uses the SNAKES library to specify and simulate (offline improvisation) the TPN model, and it uses the inter-media sequencer i-score to improvise in real-time.


PNEmu is an extensible python library that provides all the necessary to model Self-Adaptive Systems using High-Level Petri nets. It provides to researchers the ability to quickly model and simulate self-adaptive systems using P/T nets and High-Level Petri nets as managed and managing subsystem, respectively. The managed subsystem is encoded into the marking of a High-Level Petri net emulator that can execute, sense and alter the managed subsystem by means of library primitives implemented by using High-Level net transitions. Our modeling approach leverages the concept of subnets to specify decentralized adaptation control in terms of MAPE loops.