TLA+ - cheat sheet

TLA+ - cheat sheet TLA+ is a formal specification language to model and proof systems. You basically model your system as state machine and let the model checker find deadlocks by going through each legal state transition. The language was invented by L. Lamport, also famously known for LaTeX and Lamport clocks. Contents Unchanged Sets Special Actions Structs Constraints Invariants Constants Impressions References Unchanged Sets Variables are set to null after any satisfied action. This default is quite counter-intuitive in contrast to virtually any other programming language. The prime of a variable can be used to set its value for the next action using '. E.g. i' is the prime for the variable i VARIABLE i Increment == i' = i + 1 Init == i = 0 Next == Increment I think of a variable like a math function with step t where “‘” refers to the next t: f(t+1) = f(t) + 1 If the value shouldn’t change, the prime can be set to the original variable: i' = i. This can become quite unreadable…