I worked at a bizarre company that followed Agile practices to the letter for a while.
One rule was that you could not check in code while any integration tests were failing. I used a Petri net simulation to demonstrate that based on the number of developers on the project, and the number of changes waiting to check in, and the length of time the tests took, and the length of time reviews/fixing took after fixing failures, and the chances of tests failing, and some other factors, you could essentially never check in code at all! Which unfortunately was pretty much what happened in practice.
It is becoming expected that every computer scientist know some basic Petri net theory.
ok, i’ll bite! completely unfamiliar with Petri Net Theory, but i’m interested to learn. this book feels a bit long to just dip my toes in, and i quickly bounced off the wikipedia page. any recommendation for getting a basic understanding of the theory before jumping in with something like this book?
Draw a bunch of circles on a piece of paper. These are your “places”. Throw some coins at random on the places.
Draw a bunch of lines. These are your “transitions”. Draw some arrows from some places to some transitions, and from transitions to places. Any configuration is ok.
A transition is “live” if every place with an arrow to the transition has a coin on it. A live transition can “fire”. Remove a coin from every inbound place, and put a coin on every outbound place. Note that if a place is both inbound and outbound, its coin number won’t change. If multiple transitions are live, any of them can fire.
There, that’s petri nets for ya. Try making a petri net that adds the tokens on two places together.
The nLab page goes from zero to state-of-the-art research, including pictures and the manufacturing metaphor. A Petri net is kind of like a fancy graph, and Petri-net theory is kind of like fancy graph theory; we are given nets, and we want to compute various properties of each net. Common places where you’ll encounter Petri nets include manufacturing, chemistry, and distributed systems.
Petri nets correspond to a fragment of linear logic, and have some nice properties (they aren’t Turing complete by default). Adding some additional connectives in by way of inhibitor arcs and other extensions can turn them into counter machines and thus make them Turing complete.
It’s interesting how similar everything looks. Linear logic, petri nets, state machines… once you’re near the bottom, everything looks the same.
Petri nets can be super useful for modeling concurrent systems, assuming you have software to help.
Many aeons ago I tutored/TA’d a course on concurrent system and we used a piece of software called LTSA, which you can still find at https://www.doc.ic.ac.uk/ltsa/. It’s not without issues being academic-ware, but it is still a very useful tool. You could actually reason about the system - from basics like “can it deadlock” to forward progress assertions, race condition assertions, etc.
The core problem - and the issue the students struggled with most - is that it’s a piece of modeling software, and for any of the proofs or assertions to hold your software must exactly match the model. It is very easy to “implement a model” where you end up with a state transition in your code that semantically matters, that the model does not have, and the moment that happens the proofs and guarantees go away.
I worked at a bizarre company that followed Agile practices to the letter for a while.
One rule was that you could not check in code while any integration tests were failing. I used a Petri net simulation to demonstrate that based on the number of developers on the project, and the number of changes waiting to check in, and the length of time the tests took, and the length of time reviews/fixing took after fixing failures, and the chances of tests failing, and some other factors, you could essentially never check in code at all! Which unfortunately was pretty much what happened in practice.
ok, i’ll bite! completely unfamiliar with Petri Net Theory, but i’m interested to learn. this book feels a bit long to just dip my toes in, and i quickly bounced off the wikipedia page. any recommendation for getting a basic understanding of the theory before jumping in with something like this book?
Draw a bunch of circles on a piece of paper. These are your “places”. Throw some coins at random on the places.
Draw a bunch of lines. These are your “transitions”. Draw some arrows from some places to some transitions, and from transitions to places. Any configuration is ok.
A transition is “live” if every place with an arrow to the transition has a coin on it. A live transition can “fire”. Remove a coin from every inbound place, and put a coin on every outbound place. Note that if a place is both inbound and outbound, its coin number won’t change. If multiple transitions are live, any of them can fire.
There, that’s petri nets for ya. Try making a petri net that adds the tokens on two places together.
The nLab page goes from zero to state-of-the-art research, including pictures and the manufacturing metaphor. A Petri net is kind of like a fancy graph, and Petri-net theory is kind of like fancy graph theory; we are given nets, and we want to compute various properties of each net. Common places where you’ll encounter Petri nets include manufacturing, chemistry, and distributed systems.
Petri nets correspond to a fragment of linear logic, and have some nice properties (they aren’t Turing complete by default). Adding some additional connectives in by way of inhibitor arcs and other extensions can turn them into counter machines and thus make them Turing complete.
It’s interesting how similar everything looks. Linear logic, petri nets, state machines… once you’re near the bottom, everything looks the same.
Petri nets can be super useful for modeling concurrent systems, assuming you have software to help.
Many aeons ago I tutored/TA’d a course on concurrent system and we used a piece of software called LTSA, which you can still find at https://www.doc.ic.ac.uk/ltsa/. It’s not without issues being academic-ware, but it is still a very useful tool. You could actually reason about the system - from basics like “can it deadlock” to forward progress assertions, race condition assertions, etc.
The core problem - and the issue the students struggled with most - is that it’s a piece of modeling software, and for any of the proofs or assertions to hold your software must exactly match the model. It is very easy to “implement a model” where you end up with a state transition in your code that semantically matters, that the model does not have, and the moment that happens the proofs and guarantees go away.