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

How does TLC check liveness properties?

Presumably it can check any "liveness" property that that can be formulated in LTL. A "liveness" property is typically described as a property stating that "something good eventually happens". This is ...
Derek Elkins left SE's user avatar
2 votes

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

The standard reference for the topological characterisation is Bowen Alpern and Fred B. Schneider. Defining liveness. Information Processing Letters, 21(4): 181–185, October 1985. One notable ...
Kai's user avatar
  • 908
1 vote

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

An answer from Stephan Merz at tlaplus-googlegroup: In a linear-time framework such as TLA+, a system satisfies a property if the property holds of all system behaviors, and from your description it ...
hengxin's user avatar
  • 9,561

Only top scored, non community-wiki answers of a minimum length are eligible