SNAKES is mainly dedicated to construct and transform Petri nets, it is able to execute them, but this is not efficient in general because the development effort has been directed toward generality instead of efficiency. So, if you want to efficiently execute a Petri net from SNAKES for analysis purpose, the best way is to use Neco net compiler.

Neco will take your Petri net, compile it to efficient C code (even if your net embeds complex Python)¹ that is in turn compiled into a native library that can be loaded has a Python module. Neco also provides fast state space construction allowing to dump the whole states as a set of as a graph. Finally, Neco is also able to call the SPOT model checking library to perform LTL model-checking on your nets. You should check Neco homepage for a tutorial and installation instructions, we will see here only a quick introduction about how to compile a net and execute its transitions using Neco. So, let's borrow the simple Petri net from Neco tutorial and assume we save it to a file called model.py:

from snakes.nets import *
net = PetriNet('Net')
s1 = Place('s1', [dot], tBlackToken)
s2 = Place('s2', [], tBlackToken)
net.add_place(s1)
net.add_place(s2)
transition = Transition('t')
net.add_transition(transition)
net.add_input('s1', 't', Value(dot))
net.add_output('s2', 't', Value(dot))

It can be compiled by Neco as follows:

$ neco-compile -m model.py -lcython

This will produce a lot of output, mainly due to Cython and GCC running. Notice that this takes quite a lot of time, but, for models with a large state space, this time is worth spending as a initial step and will be widely compensated by the speedup during state space exploration (which is not the case of course for our toy example). The compilation process eventually ends producing a file net.so that is a Python native module. We will use this now on:

import net
ctx = net.NecoCtx()
todo = ctx.remaining
done = ctx.state_space
todo.add(net.init())
while todo :
    state = todo.pop()
    process(state)  # defined below
    done.add(state)
    todo.update(net.succs(state, ctx) - done)

Two functions are used to build the state space: net.init returns the initial marking of the compiled net, and net.succs returns the successors of a marking. We have two sets of states: todo holds those sets for which we have not yet computed the successors, and done holds all known states. Function net.succs actually needs as its second argument a context used to avoid rebuilding already known states, so we build this context at the beginning with ctx.NecoCtx() and directly take from it references to the sets corresponding to todo and done. Then, state space computation is straightforward: while there are states to process, one is picked from todo and its successors are computed, if new states are discovered, they are added to todo.

In concrete situations, we probably would like to analysis states as they are discovered. When Neco is used, states are instances of net.Marking that is a structure defined by Neco and optimised with respect to the data types used in the net. Unfortunately, there is not much we can do with this structure, indeed, providing a friendly API for it would lead to inefficient processing done by user's programs. Instead, to perform complex analysis on the markings, the preferred approach is to use LTL model-checking: this way, atomic access to the marking are compiled also by Neco and can be made efficient. More about LTL model-checking can be found in Neco tutorial. So, for our small example, let's just print the state by defining a simple function process:

def process (state) :
    print(state.__dump__())
    # use `state.__line_dump__()` instead for a 1-line output