TLA+ | The way to specify

The TLA+ and PlusCal Resource

Skip to content

Search for:

Operations on a sequence of records February 23, 2021
Reader Writer Problem specs : Liveness & TLC February 23, 2021
How do I get TLC to check invariants with primed variables (action predicates)? February 21, 2021
Latex Margin February 20, 2021
UNCHANGED ModuleInstance!Variables February 19, 2021

TLC prints bogus mismatch warning for TLCExt!getTrace module override. February 24, 2021 lemmy
Unify trace lookup in TLCExt#Trace by adding delegate methods February 22, 2021 lemmy
Unify trace lookup in TLCExt#Trace by adding Simualtor#getTraceInfo(), February 22, 2021 lemmy
Include TLCState#workerId and TLCState#uid in TLCState#deepCopy(). February 22, 2021 lemmy
Clearly, we need a better type system. %-) February 20, 2021 lemmy

API: change default aux dir to `.tlacache` (#20) February 16, 2021 johnyf
update version number and remove old svn-based commit numbers (#18) February 16, 2021 damiendoligez
ENH: add module `Dekker` to `examples/Dekker/` January 28, 2021 johnyf
modifications to standard TLAPS library (#27) December 30, 2020 muenchnerkindl
Switch to newer version of Github action to fix cache issues on macOS. December 17, 2020 lemmy

RT @vanlightly: I have open sourced my TLA+ specification for Apache BookKeeper here: https://t.co/5OPTLUOY0x It detected a data l… https://t.co/7EC7kO6RkS

2 hours ago
#tlaplus https://t.co/Hla5m1oDG1

7 days ago
RT @pressron: A question for TLA+ bloggers: Both mathematicians and TLA+ spec authors type x \in S when they want to write x ∈ S,… https://t.co/gxwI1BvmZ8

1 month ago
RT @ApalacheTLA: Apalache is not a baby anymore. It has a Twitter account of its own! #tlaplus #apalache

1 month ago
RT @informalinc: v0.8.0 of Apalache — the symbolic model checker for TLA+ — is released! Changes include: - A spiffy new assignment… https://t.co/Yw3MdwQTaZ

2 months ago