TLA+ | The way to specify

PlusCal

PlusCal (formerly called +CAL) is an algorithm language based on TLA+. An algorithm language is for writing algorithms, just as a programming language is for writing programs. (The introduction to the PlusCal manual explains how algorithms differ from programs and how PlusCal differs from programming languages.) The PlusCal Translator compiles a PlusCal algorithm into a TLA+ specification, that can be checked with the TLA+ tools–the most import of those tools being the TLC model checker.