TLA+ Exercises Some experiments in making exercises for teaching TLA+: Passfail: Exercises in finding useful properties. Typeset: Exercises in generating useful sets.