TLA+ | The way to specify

The TLA+ and PlusCal Resource

Skip to content

Search for:

Safety Liveness Decomposition and Machine Closure August 9, 2020
New user: question about 'with' August 9, 2020
TLA+ Community Modules August 7, 2020
Is it possible to create two separate channels so that they can run separately according to their respective heartbeat timing August 7, 2020
In TLC, what are "generated" vs "distinct" states? July 30, 2020

pcalTLAGenerator.translate() mutates the PCal AST for some inputs August 8, 2020 lemmy
Do not create redundant "nightly" git tag. August 5, 2020 lemmy
Hey Markus, this is why you run tests locally first! August 5, 2020 lemmy
* Shorten checksum (from md5 to CRC32) August 4, 2020 lemmy
Warn before overwriting a modified TLA+ translation of a PlusCal August 3, 2020 lemmy

RT @lemmster: @dharmashukla will give the keynote at this year's #tlaplus community event and share how TLA+ has been useful with… https://t.co/fM1Dg4Dxsz

22 hours ago
RT @lemmster: awesome-tlaplus: https://t.co/sZxLIlkQgx (PRs welcome)

1 month ago
RT @lemmster: @MarcJBrooker Who uses refinement when writing #tlaplus specs?

1 month ago
RT @hillelogram: I'm offering a new online workshop, this time a 3 day TLA+ training! Learn how to find bugs in complex systems BEFO… https://t.co/qTSMCWNrVH

2 months ago
eXtreme Modelling in Practice, by @jessejiryudavis @visemet @judahschvimer On testing an implementation against a… https://t.co/haFduVkXOA

2 months ago