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 321 topics
tlapm Error 4/21/17
TLA+ model of OneThirdRule algorithm from "A Reduction Theorem" paper Evgeniy Shishkin 4/21/17
tuples in function constructors using tlapm ? Ioannis Filippidis 4/20/17
TLA+ Toolbox 1.5.3 release Markus Alexander Kuppe 4/18/17
Differences between TLA+ Specification and Property Based Testing Andrew Gwozdziewycz 4/14/17
Hourly clock spec: why it needs the temporal-logic operator box [] 4/14/17
TLA+ Video Course Leslie Lamport 4/8/17
TLC: NoSuchElementException on checkpoint restore Jaak Ristioja 4/5/17
3 Random Questions Eric Lee 4/5/17
ProcSet unavailable in PlusCal define statement Jaak Ristioja 4/3/17
Unfolding macro definitions 4/1/17
I've been working on a TLA+ guide Hillel Wayne 3/29/17
Next release? Jaak Ristioja 3/28/17
About Finite Set of records 3/27/17
Fatal error starting 1.5.2 on macOS Sierra, and a solution. sriram srinivasan 3/27/17
Limiting lengths of all sequences for TLC model checking Serdar Tasiran 3/22/17
seeking programmer to work on TLC Leslie Lamport 3/20/17
TLAPM from command line Amira Methni 3/15/17
Announcing Sbuilder - a tool to generate TLA+ model for business IT systems jarjuk 3/15/17
Can't prove it 3/15/17
More topics »