This repository contains TLA model examples for use with the accompanying document 'tla.pdf'. Links are provided therein to directories in this repository.
Straightforward: see 'tla.pdf' section 4 for instructions
Tested on Ubuntu 13.3.0 with the 25.0.1 JAVA compiler, and OpenJDK 25.0.1+8-Ubuntu-124.04 runtime
Every example comes with a Makefile. Execute make to run verification
The RPC example (section 13 of 'tla.pdf') is in development. ETA March 2026.