David Jimenez

When modeling a system we have to determine how we are going to represent its state.  In this post we explore how to do that for a traffic light.

Modeling a traffic light - Part 1: State

TLA+ is a specification language that can used to model software. Importantly, TLA+ comes with a set of tools to test those models.
Though TLA+ is based on math and logic, the specifications written with it are not proofs. Instead, the specifications serve as testable blue prints.
If you are coding in a language like Python or Java, what advantage is there to writing a TLA+ specification? After all, even if the model is perfect, there is a chance that you can introduce bugs when performing the translation from TLA+ to your programming language of choice.
The advantage comes in that TLA+ forces you to clearly specify what you are trying to accomplish. Then, when checking your models, you may realize that you were not thinking of certain edge cases. Or perhaps you come to find out that you were making assumptions that are not valid.
To make the case for TLA+, I plan to write a series of post describing the key elements of the language as I develop a simple specification for a traffic light.

This post explores what TLA+ is and why it may be worth using.

What is TLA+?

How do you know that your code works? Traditionally, there have been two options: you can prove it using mathematics; or you can write tests to show that despite your best effort you cannot break it.