Petri net is a very popular formalism to model distributed systems. It is a directed bipartite graph whose nodes represent either transitions, representing events in the modeled system, or places, representing the state of the system. It has a formal syntax, a graphical notation and of course a well-defined semantics. I’ll spare you the details in this post, as there are countless scientific papers describing them. But just so we are on the same page, here’s a quick and super informal description:

The places of a Petri net are marked with a given number of tokens, describing the state of the system. A transition is enabled when there enough tokens in all its input places (i.e. places for which there’s an arc to the transition). A enabled transition can be fired, consuming the tokens from its input places and producing new tokens in its output places.

We teach the Petri net formalism at University of Geneva, in the context of our Bachelor and Master degrees. But if after years of exposure the formalism became second language for us, students often struggle with it. The first obstacle is the semantics, and in particular the way tokens are consumed and produced. Unexperienced students often get the idea that tokens move from one place to another, rather than one being consumed and another new one being produced. The second obstacle is the formalization the formalism, and the interesting properties of the models that are written with it (e.g. state reachability). Here, the problem is often that students have difficulties connecting abstract concepts to even more abstract notations.

In an effort to improve the whole learning experience, we tried to explore other ways to teach our science. And after a few after work beers, we thought about making a mobile game … And since a day after idea seemed as brilliant as it was when we talked about it, we decided to go through.

The idea of our game is to create a collection of Petri net models with various interesting features (colored tokens, bounded places, inhibitor arcs, …), so as to introduce all important notions of the formalism. The game then consists of solving a puzzle by finding the particular sequence of transition that unlocks the puzzle objective(s), hence requiring to understand the semantics of the notions it features.

The game is still a work in progress, so stay tuned as its development progresses. Who knows, maybe it’ll make you love Petri nets almost as much as we do.