Tla

PlusCal is a language for writing algorithms that translates into TLA+. It is an invaluable tool for reasoning about concurrency.

What must be true of every state in all behaviors of a functioning traffic light?

What does a TLA+ specification look like?

This post introduces the concept of behavior in TLA+.

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.

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

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.