I have written a Fizzbee spec that is the equivalent of the TLA+ spec.
Let’s dive into the decisions I had to make with this initial Fizzbee spec.
I have written a Fizzbee spec that is the equivalent of the TLA+ spec.
Let’s dive into the decisions I had to make with this initial Fizzbee spec.
One thing I forgot to write about yesterday was how I get confidence that the TLA+ specification is doing what I expect. The thing about model checking a spec is that because there are usually millions or billions of states to explore, you can’t always see that certain states that should be reachable do get reached. It’s common to have a specification bug that causes your spec to have valid areas of the state space be unreachable, without you knowing it. This is why TLA+ practitioners learn to be a skeptical bunch and treat early success with great cynicism.
This is what I did to get confidence in this initial specification.
Strap in and fire up your nerd engines—this one's gonna be intense!
In my previous diary entry, I explained I would begin the formal modelling of Kafka transactions by implementing a tiny initial piece of the protocol - how a producer obtains a producer id. In this post I will discuss some aspects of the TLA+ specification I have written of this initial model.