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-20 of 395 topics
Need help to update the state with EXCEPT. shirish gajera 2:10 PM
A revolution fl 12/11/17
Check that both branches are executed 12/11/17
Visualize state graphs in TLA toolbox shirish gajera 11/29/17
NFM 2018 - Call for Papers Jasmin Blanchette 11/22/17
Why Amazon Chose TLA+ Chris Newcombe 11/17/17
Login required for TLA toolbox? Alex Stangl 11/17/17
How to run TLA+ ToolBox model checking from command line? 11/14/17
Apparent bug in operators using \E Michael Collins 11/10/17
What does f[x] mean when f is not a function? Greg Wiley 11/6/17
Analysis: Runway, a new formal specification system Andrew Helwer 11/5/17
Specifying Systems fig 3.2 : is my understanding correct? lthibault 11/4/17
New to TLA+: Questions about content in video courses 5 & 6 Janice D'Sa 10/31/17
non-atomic assignments (noob question) Michael Slominski 10/22/17
How to terminate or explicitly set a pc to "done" in pluscal Jose Ayerdis 10/19/17
TLA+ Toolbox 1.5.4 release Markus Alexander Kuppe 10/19/17
Using TLA+ for data modeling Chris Newcombe 10/13/17
Exclusive-Or operator? Andrew Helwer 10/11/17
Trouble Running Toolbox on macOS Sierra Daniel Gregoire 10/6/17
Very Newbie question - thanks in advance for pointing out my error Pete Mastin 10/4/17
More topics »