TLA+ | The way to specify

The TLA+ and PlusCal Resource

Skip to content

Search for:

Toolbox trace exploration broken because generated (trace) spec lacks April 28, 2021 lemmy
Support KSubsetValue appearing as variable values. April 27, 2021 lemmy
Remove one off index check for -simulate argument. April 26, 2021 pfeodrippe
When opting in or out of execution statistics, create ~/.tlaplus/ parent April 26, 2021 lemmy
Restrict users from typing the number of workers on the "TLC Options" April 26, 2021 lemmy

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

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

3 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

4 months ago