two processes, one critical section: mutual exclusion and starvation freedom both hold
the same algorithm without the await: TLC finds the interleaving that breaks mutual exclusion
two concurrent wire transfers both pass the balance check, and an account goes negative
plain TLA+: claim the puzzle is unsolvable, and the counterexample is the solution
without a fair process, TLC may stop scheduling it: the counterexample stutters forever
checks the algorithm on all 27 arrays over 1..3, using the Community Modules' Range
ABOUT
This is the TLA+ project's own tla2tools.jar — the PlusCal translator, the SANY parser and the TLC model checker — with the Community Modules, unmodified, on CheerpJ, a JVM in WebAssembly. Each run starts TLC fresh, exactly as java tlc2.TLC would. Nothing leaves your machine. It runs one worker and is slower than a native JVM — fine for the small models you'd write while thinking, not for a cluster's worth of states. How it's built.