Skip to main content
Share Your Experience: Take the 2024 Developer Survey

Questions tagged [tlaplus]

TLA+ (tlaplus) is a formal specification language developed by Leslie Lamport. TLA stands for "Temporal Logic of Actions."

Filter by
Sorted by
Tagged with
1 vote
1 answer
32 views

Topological/metric space formed by behaviors of distributed system: Safety and Liveness

In the book A Science of Concurrent Programs Leslie Lamport describes alternative way how to look at safety and liveness properties in distributed algorithms. A.5 Another Way to Look at Safety and ...
Andreo's user avatar
  • 113
0 votes
0 answers
22 views

Are ASM and TLA+ somehow related?

I learned about abstract state macines recently, and on first sight they seem somehow reminiscent to TLA formalism. For example both: Are used to research possible state sequence and prove safety/...
uhbif19's user avatar
  • 101
0 votes
1 answer
278 views

How to collect all states of a behavior in TLA+?

Description of the problem: I am modeling checking a distributed protocol against a global property with TLA+ developed by Leslie Lamport. The global property is defined on all states of a behavior (...
hengxin's user avatar
  • 9,561
8 votes
1 answer
703 views

How does TLC check liveness properties?

The paper "Model Checking TLA+ Specifications" published in 1999 explained how TLC (Temporal Logic Checker) checks safety properties written in TLA+ developed by Lamport. At that time, TLC did not yet ...
hengxin's user avatar
  • 9,561