TLA+ | The way to specify

The TLA+ and PlusCal Resource

Skip to content

Search for:

why need /\ item' = item? January 23, 2019
Error trying to run a model: The status must be "parsed" before model checking is allowed January 22, 2019
What if every action could use all the variables? Would we need to define Init? January 21, 2019
Help with running TLC in distributed mode (ad hoc) January 20, 2019
Can TLAPS check any termination proofs? January 19, 2019

RT @lemmster: The upcoming TLC profiler - on which I have been working on for much longer than intended - will help identify expe… https://t.co/yZeftYWe5i

2 weeks ago
TLA+ Conference September 12, 2019 in St. Louis, MO, USA: https://t.co/hK1y3Z5pY8 #tlaplus

3 weeks ago
RT @talex5: Experiences using @tlaplus to understand Xen's vchan protocol: https://t.co/ueNzjIX2gu @OpenMirage @QubesOS

3 weeks ago
RT @pressron: Verifying Software Traces Against a Formal Specification with TLA+ and TLC https://t.co/OS9KfgJu1o

1 month ago
RT @pressron: A TLA+ specification of Tic-Tac-Toe in the Behavioral Programming style, after https://t.co/F04UNz34wi by David Har… https://t.co/eGC1xoOj2Q

2 months ago