siiky
2023/09/20
2023/09/20
en
As I've mentioned on my tinylog, my master's thesis will revolve around Petri nets. More specifically, about the practical application of Petri nets, not only to model but to program concurrent/distributed programs. That's an area that doesn't seem to be as well explored as modeling with, and formal verification of, Petri nets -- formalists tend to work only in theory, never in practice[*].
The things I'd been reading before, especially Statebox, were very promising (theory-wise and intent-wise), but in practice they never got to anything people can get their hands dirty with. Statebox specifically seem to have abandoned the programming idea completely (very unfortunate), and turned to a documentation-oriented product (not yet out), as I've mentioned in log #005. The fact that they never replied was also very disappointing... :/
Some time ago I found gen_pnet, an Erlang library that defines a Petri net behaviour. I didn't understand the point at first, it seemed like a waste not to take advantage of Erlang's parallel computation abilities. Until I watched a related talk: the net is used to define the behaviour of each process, but they still communicate as normal Erlang processes through message passing! From there I found the related whitepaper, and then "Understanding Petri Nets", by Wolfgang Reisig -- I'm reading this now.
"Understanding Petri Nets" is more pragmatic so far, there's less focus on the formal theory and more on getting shit done (modeling). Some of the questions I had sent to Statebox were kind of irrelevant (depending on how you implement/use Petri nets); others, after having started reading this book, seem like they didn't think about them at all. Or if they did, they didn't get to formalize mathematically (understandable, it's pretty fucking hard). Still, would have been useful to mention these details as future work.
Still haven't learned of any implementation other than gen_pnet, which limits experimentation. But before that, I'd like to have a light process/pipeline to generate Petri net graphics based on a simple textual language, so that I can model and visualize more easily (drawing by hand is fine, but editing not so much). I hacked something together using GraphViz, but without any customizations the results are really fugly -- take a look at log #003 (the end result is the same, I just created a new "front-end"). After some searching I learned there's a Petri nets library for (in?) TikZ, that'll be my next attempt. To be clear, LaTeX is NOT a simple textual language! I'll first play with it to learn how it's used, and if it works well I'll create another Scheme DSL for it.
[*]: Speaking as a Formal Methods major myself: If formal methods (i.e. theory) are not easy to use, or not usable at all, then they're basically useless.