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 336 topics
TLC not handling disjunction correctly in special case? Andrew Helwer 5/23/17
Confusion about the model of the specification of InternalMemory in Chapter 5 "A Caching Memory" of the book "Specifying Systems" Hengfeng Wei 5/23/17
TLA+ community meeting at FLOC 2018? Stephan Merz 5/22/17
Paramaterized Instantiation and Universal Quantification Adam Shimi 5/19/17
TLA+ Video Course Leslie Lamport 5/15/17
Protocol specification liveness Wan Azlan 5/14/17
Arity of NEW operator in `tlapm` Ioannis Filippidis 5/11/17
Ability to use Vim keystrokes with TLA+ Toolbox? Thomas Gebert 5/6/17
seeking a model/spec that can reproduce a "null" error trace Ian Morris Nieves 5/5/17
TLA+ Toolbox 1.5.3 not displaying error trace Andrew Helwer 5/4/17
ENABLED Operator Theorems kacem belout 5/3/17
Leibniz and ToBoolean Operators and Proof Fragment 5/2/17
Quest. Cont. About Theorem And Inference Rule 4/30/17
About a Theorem in the Raw TLA 4/30/17
theorems from instantiated modules in `tlapm` version 2 Ioannis Filippidis 4/30/17
Non reactive HMI Asterion Daedalus 4/26/17
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
More topics »