codebase:liveness

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Next revision		 Previous revision
codebase:liveness [2025/05/05 10:42] – created fponzicodebase:liveness [2025/05/06 21:23] (current) – fponzi
Line 1: Line 1:
 ====== Liveness Checking Algorithm in TLC====== ====== Liveness Checking Algorithm in TLC======
 +The algorithm is described in the book: "temporal verification of reactive systems: safety"
 ===== High-Level Overview ===== ===== High-Level Overview =====
 The liveness checking algorithm in TLA+ verifies temporal properties in specifications - properties that describe how a system should behave over time. Unlike safety properties (which check that bad things never happen), liveness properties assert that something good eventually happens. The liveness checking algorithm in TLA+ verifies temporal properties in specifications - properties that describe how a system should behave over time. Unlike safety properties (which check that bad things never happen), liveness properties assert that something good eventually happens.
Line 116: Line 116:
   * The tableau construction is a key theoretical component that allows the algorithm to check arbitrary temporal formulas.   * The tableau construction is a key theoretical component that allows the algorithm to check arbitrary temporal formulas.
   * Tarjan's algorithm for finding strongly connected components is at the core of the liveness checking mechanism.   * Tarjan's algorithm for finding strongly connected components is at the core of the liveness checking mechanism.
 +  * The content of this page was generated by deepwiki.com.
  • codebase/liveness.1746441762.txt.gz
  • Last modified: 2025/05/05 10:42
  • by fponzi