Behavioral Programming with Petri Nets
À la functional way, through examples
The Statebox language has come a long way in the past year, and so it’s time to illustrate how programming using Statebox works. Sure, the monograph details the mathematics behind Statebox but how do you actually use it?
Our codebase will soon be made public for everyone to read, but this is very different from making developers understand how Statebox can be useful in their everyday life. We felt we needed a series of tutorials worked out by means of examples, not only to document the use of Statebox per sé but also to teach the ways of what we call behavioral programming.
…And so we did! Lately we filmed a series of short videos explaining how to use Petri nets to design software. This series of blogposts will serve as a (not too verbose) addendum to better understand what’s going on in the videos.
What is behavioral programming?
Let’s start by clarifying what behavioral programming means using comparisons. In imperative programming, you think in terms of instructions, by literally giving to the computer a list of things to do. In functional programming you think functions, which then you pipe together to get the job done. In event-driven programming, you think in terms of things that can happen (events) and how to react to them. In behavioral programming, as the name suggests, you must think in terms of which properties (behavior) you want your software to have. In this sense, programming becomes goal-oriented, and starts with a high-level sketch of the software structure.
Throughout this tutorial, we will borrow the mantra of type-driven development with Idris, a great and very inspiring book by Edwin Brady: The mantra is type, define, refine. In our context, this means that we will start sketching the code structure, we will test for its behavior and then we will refine it so that it meets our goals.
We will start with a computer science classic originally proposed by Dijkstra in 1965, namely the dining philosophers problem. Our related video is this one.
It goes like this: You have four philosophers at a table which can either think or eat. The catch is that they have to share cutlery, and coordinate between them about this. Translating this to a real-world scenario, we can think about philosophers and cutlery in terms of processes and resources to be shared, respectively. The point about this example is that one has to be clever about refining access to resources to avoid a total mess. Indeed, in the video we give some resource-access rules that will turn out to be a recipe for disaster. The rules are as follows:
- In the beginning, all philosophers are thinking.
- A philosopher wanting to eat will have to first take the cutlery piece on their left and then the cutlery piece on their right. Eating is not possible without having both cutlery pieces.
- After a philosopher finishes eating, the cutlery pieces must be put back on the table.
- There are no other rules.
Forgetting for a second about the fact that these people are sharing cutlery while eating (groooooss!!!), you can see what the problem is here: It is possible that all philosophers try to eat at the same time and that all of them end up having only one cutlery piece. Since we defined no rules for this circumstance, the process will inevitably jam: Each philosopher cannot put the cutlery down, since this can be done only when finished eating. On the other hand, a philosopher needs two cutlery pieces to eat which is not possible since they are all taken. Boom!
We start by showing how this problem can be modelled using Petri nets, the fundamental ingredient in the Statebox secret sauce. This is done in this video.
Ok, so we started with a very simple and understandable problem, and we in turn defined an ugly and complicated net to model it. It doesn’t seem like we gained much, right? Wrong! We did! In fact:
- We modelled philosophers and cutlery using places and transitions in our net, which can now be whatever we want them to be: In the Statebox environment places are datatypes, tokens are data of the type of the place they live in, and transitions are functions. Of course, we are free to specify datatypes and functions at a later stage, while for now we are allowed to care only about the code structure. If you think along these lines, we abstracted a very specific problem into a very general one, which can then be tailored to our needs.
- By modelling the problem with Petri nets, we automatically get access to a lot of analysis tools which can automatically spot how nice the behavior of the net is. In fact, the problem highlighted above of all philosophers having only one cutlery piece corresponds to a property of Petri nets called deadlock, to which we can test our net against! Indeed, if we run formal analysis on our net we will find out that it can deadlock. Not nice, right? Right! …But the good thing is that having an automated way to spot a mess in our code structure gives us the opportunity to fix it before putting a real work case into it.
So, starting with a bad-behaved problem, we defined a bad-behaved net. At least, we now happily realize that we were able to spot a deadlock before writing a single line of code. We want now to refine the net and fix it. This is done in the next video.
This star shaped net is deadlock-free, a condition which we can again check formally. The way we fixed the problem is by modifying the rules so that philosophers wanting to eat first need to reserve both pieces of cutlery at their side, then pick them up. This is not the only way to solve the problem, but it’s probably the simplest one. You can check the dining philosophers problem’s Wikipedia page if you are looking for a different solution. In fact, why don’t you try to model one of the alternative solutions using Petri nets yourself?
The crux of our solution lies in limiting the amount of concurrency allowed in the system. Sure, now things are a bit less independent and a bit less concurrent, but at least now they are guaranteed to work.
Hopefully, you now got the general idea behind Statebox programming: First, starting with a goal (modelling philosophers at a table), defining a net to capture the problem mechanics and refining it so that it follows a prescribed behavior. Then, mapping places and transitions to datatypes and functions to obtain code in its final form. Between each of these steps, a ton of formal tools can help us find the right path to the next one.
In the next post, we will leave the realm of theoretical computer science examples to turn at more practical ones, where we will use Petri nets to model the behavior of a smart contract. Stay tuned!
