TLA+ | The way to specify

The TLA+ and PlusCal Resource

Skip to content

Search for:

A monolith/uber spec is a single .tla file with one to N TLA+ modules June 2, 2020 lemmy
If TLC runs without -tool output it might still be useful to report June 2, 2020 lemmy
Set Tycho build repository ids where missing. June 2, 2020 lemmy
Grrr, Eclipse Tycho/p2 non-deterministically selects *broken* June 2, 2020 lemmy
Report errorCode even when workers did not preemptively terminate June 1, 2020 lemmy

added Barcan formula to FOLTL.tla April 12, 2020 muenchnerkindl
use more generic URLs for release binary files March 17, 2020 damiendoligez
Create CNAME March 17, 2020 lemmy
Build and test tlapm on every pull request March 17, 2020 lemmy
change the download links to absolute URLs pointing to the release pa… March 17, 2020 damiendoligez

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

13 hours ago
RT @lemmster: The new #tlaplus release has been published at https://t.co/VAG3w1C1GL

1 month ago
RT @lemmster: We are ramping up a new #tlaplus release. Please help by test driving https://t.co/VAG3w1C1GL

1 month ago
RT @_jesusmg: I have just created a Flatpak package containing the TLA+ toolbox! Available at https://t.co/SLVkWT3dft #flatpak #tlaplus @tlaplus

2 months ago
RT @lemmster: This reminds me that I want to thank @killdoll (https://t.co/LSBmR8akUf) for making significant contributions to TLC and the Toolbox!

2 months ago