Artikel
An Introduction to TLA+ and Its Use in Parties
TLA+ is a system for modeling all possible states of a system. On this model, you can then verify certain properties of this system. Smart people can use this to check that their thread scheduling runs all threads equally, or that their work queue will never overflow. In this article, we’ll try and verify the fraught process of ordering pizza for a pizza party as a small introduction to the concepts and syntax of TLA+.
