On May 30rd, I started the #100DaysOfCode challenge to learn more about formal methods and see how much we could use them in our daily software tasks. 100 days of code: Day 0 of learning TLA+ for regular software development will give you the introduction into this journey.
As with my regular notes, I’ll share the surprising or thought-provoking discoveries I make.
Today’s mind twisting moment came from this part of the expression explorations
CASE TRUE -> FALSE  TRUE -> TRUE
If more than one match, though, TLC will pick one for you and not branch. In other words, the following code May or may not be true. Be careful
This took me a few seconds to digest.
Then it start to make sense. I already got that the model checker explores the various state spaces, and so that we need to think in states and not in steps.
Form this, yes it makes sense, since the
case do not explore all the states like a
in would do, then any state would match.
l =  x in ["a", "b", "c"] l = append(l, x) print l
["a"] ["b"] ["c"]
3 different state paths, no 3 sequential steps.
It starts to sink in.
Wish me luck, it’s only the beginning of the journey ;)
If you liked this, you can find the other posts of my #100 days of code: formal methods
If you’re interested in this, keep an eye on my notes in the next weeks. If you follow me on Twitter, I’ll also share the updates there.