Part of the Embarrassing Trainwreck release. Full notes there, main highlights:
- “Concurrency” section is slightly better
- “Temporal Properties” section is slightly better
- New “Techniques” section for how to write better specs.
As always, critique appreciated, the more vitriolic the better. Thanks for reading!
Although used up time on another thread, I’ll add at a quick glance that I like seeing addition of conditionals and infinite loops. In formal verification, a lot of things involve guarded conditionals or loop invariants. Good to have that represented in TLA+ guide.