TLA+ | The way to specify

The TLA+ and PlusCal Resource

Skip to content

Search for:

Support launching TLC from a relative path. October 18, 2019 lemmy
Correctly handle function definitions with nested LETIN statements October 18, 2019 lemmy
Performance bottleneck creating the profiler tree (CostModel) with large October 18, 2019 lemmy
Deleting a spec that has unsaved changes - #375 October 17, 2019 quaeler
See d784869296cb503692d5269bc6aeea0412e330f1 October 17, 2019 lemmy

RT @dahlia_malkhi: Proudly announcing the publication of my book ``Concurrency: the Works of Leslie Lamport'' https://t.co/lY6Dabt2mN

3 days ago
RT @alygin: TLA+ for Visual Studio Code v1.1 released with the Constant Expression Evaluation feature #tlaplus, #pluscal,… https://t.co/otKKFmAaMu

2 weeks ago
RT @lemmster: Follow-up question: On a scale from 1 to 3; how much effort do you put into minimizing the state space of models (3 is significant effort)?

3 weeks ago
RT @lemmster: What is the avg size of your #tlaplus models (number of distinct states)?

4 weeks ago
RT @lemmster: #tlaplus conf 2019: "Keynote: TLA+ at Microsoft: 16 Years in Production" by David Langworthy… https://t.co/QAi4PPhMZK

4 weeks ago