/tlaplus

TLA+

TLA+ has been described as exhaustively-testable pseudocode, and is an initialism for Temporal Logic of Actions, per wikipedia

Getting started

  1. Grab the latest release of TLA Toolbox (for your OS)
  2. Check out the various user manuals and guides that the toolbox comes with under the Help menu.
    • user guide
    • Help > TLA+ Cheat Sheet
    • Help > PlusCal User Manual
  3. Check out the examples on learntla.com. E.g., this one

PlusCal

The given example is in PlusCal, which is a higher level pseudocode language that gets transpiled into TLA+.

examples/transfer.tla

---- MODULE transfer ----
EXTENDS Naturals, TLC

(* --algorithm transfer
variables alice_account = 10, bob_account = 10, money \in 1..11;

begin
A: alice_account := alice_account - money;
B: bob_account := bob_account + money;
C: assert alice_account >= 0;

end algorithm *)
====
  • Hitting ⌘T on mac translates this PlusCal to TLA+.
  • Create a new "model" (name it TransferModel).
  • Run TLC on the model.
  • This immediately fails, since our test case included money=11 which violates our invariant assert alic_account >= 0
  • Profit!

References