This is a discussion group for users of the TLA+ specification language, the PlusCal algorithm language, and their associated tools.
To find out about the languages and tools, see The TLA Home Page 
Posts by non-members are moderated.
We encourage you to join the group.

Showing 1-21 of 451 topics
TLA+ Community Meeting Stephan Merz 3/20/18
TLATeX Pedro Paiva 6:04 AM
How to run models on different modules in the same Spec Tony Zhang 4/22/18
How to define Hexa decimal sets/Vectors in TLA+ 4/20/18
Best way to test a library? Hillel Wayne 4/15/18
Multi-threaded TLC Simulation Mode William Schultz 4/12/18
Possible new language constructs for TLA+3? Andrew Helwer 4/9/18
Is tla+.jj up to date on github? Raghav Boorgapally 4/8/18
Fairness condition for messages Pedro Paiva 4/4/18
TLA+ Video Course Leslie Lamport 4/3/18
The level of the expression or operator substituted for 'Def' must be at most 0 Andrew Helwer 4/1/18
TLC model checking RealTime module: problem with variable now Lorenzo Rodriguez 4/1/18
How do I create a TLC model for a specific module in a spec with the toolbox? Andrew Helwer 3/31/18
How to give a refinement mapping from one subactions to many subactions Changgeng Zhao 3/27/18
relevant conferences? Sara Hamouda 3/27/18
Cannot open toolbox after update Laura Santamaria 3/26/18
Google Summer of Code Stephan Merz 3/25/18
Toolbox beta release with Unicode support Markus Alexander Kuppe 3/20/18
TLA+ REPL William Schultz 3/19/18
Pluscal able to translate my spec. However, after translation, the spec status becomes error Charly Abraham 3/18/18
Google Summer of Code 2018 Parv Mor 3/17/18
More topics »