TLA+ | The way to specify

The TLA+ and PlusCal Resource

Skip to content

Search for:

Proving refinement for specs with fairness properties April 11, 2021
meaning of the lead to (~>) operator April 10, 2021
How to solve this error ? April 7, 2021
TLA+ Graph Explorer April 7, 2021
How to generate all possible linear extensions (i.e., topological sortings) of a partial order? April 6, 2021

Replace unpublished `TLCGet("mode")` with `TLCGet("config")` that equals April 10, 2021 lemmy
In simulation mode, evaluate (implied) invariants and (state- & action-) April 9, 2021 lemmy
Add ITool#getNextStates(INextStateFunctor, TLCState, Action) to evaluate April 9, 2021 lemmy
Eagerly filter initial states that do not satisfy the state-constraints April 9, 2021 lemmy
Do *not* unset the predecessor if running simulation. Simulation April 9, 2021 lemmy

CI: bump to `create-release@v1.1.4` March 18, 2021 johnyf
Merge pull request #25 March 4, 2021 johnyf
Apply suggestions from code review February 16, 2021 johnyf
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

RT @sadraskol: I'll present an introduction to TLA+ and first order logic tomorrow. Join us to leverage the power of an awesome sp… https://t.co/acrnk1nkzQ

1 month ago
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 months ago
#tlaplus https://t.co/Hla5m1oDG1

2 months 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

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

3 months ago