codebase:liveness

This page is read only. You can view the source, but not change it. Ask your administrator if you think this is wrong.
====== Liveness Checking Algorithm in TLC======
The algorithm is described in the book: "temporal verification of reactive systems: safety"
===== 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 algorithm works by:
  - Converting temporal formulas to a specific normal form
  - Building a behavior graph that combines the state space with a tableau
  - Searching for strongly connected components (cycles) in this graph
  - Checking if any cycle violates the liveness properties

If a violation is found, the algorithm constructs a counterexample to show the problematic behavior. ''LiveWorker.java:33-41''

===== Formula Conversion and Preprocessing =====

==== Step 1: Processing Liveness Properties ====
The algorithm starts by parsing the liveness properties defined in the specification and converting them to a workable form:

  - Temporal formulas are parsed and converted to ''LiveExprNode'' objects through the ''astToLive'' method
  - The formulas are tagged, simplified, and converted to Disjunctive Normal Form (DNF)
  - The DNF is then classified into different types of expressions:
    * ''AEAction'': Eventually Always Actions ( []<>A )
    * ''EAAction'': Always Eventually Actions ( <>[]A )
    * ''AEState'': Eventually Always States ( []<>S )
    * ''tfs'': Temporal formulas with no actions

''Liveness.java:498-533''

==== Step 2: Creation of Tableau and Order of Solution ====
For each temporal formula, the algorithm creates:

  - A tableau graph representation
  - An "Order of Solution" that contains the tableaux and checks to perform

The Order of Solution organizes how the algorithm will verify the different components of liveness properties.

''Liveness.java:682-777''

===== Behavior Graph Construction =====

==== Step 3: Building the Behavior Graph ====
The algorithm constructs a behavior graph that combines:

  - The state space graph from model checking
  - The tableau representation of the liveness properties

This combined graph is stored using a disk-based representation (''DiskGraph'' or ''TableauDiskGraph'').

''LiveCheck.java:522-615''

When the behavior graph has tableaux, a more complex graph construction is used:
''LiveCheck.java:617-709''

===== Strongly Connected Component Detection =====

==== Step 4: Checking for Cycles Using Tarjan's Algorithm ====
The core of the liveness checking is performed by the ''LiveWorker'' class, which searches for strongly connected components (SCCs) in the behavior graph:

  - The algorithm uses an iterative version of Tarjan's algorithm to find SCCs
  - It focuses on finding cycles that might violate liveness properties
  - For each SCC found, it immediately checks if it violates the liveness properties

''LiveWorker.java:117-147''

The main SCC search algorithm:
''LiveWorker.java:229-319''

==== Step 5: Checking Components for Violations ====
For each SCC found, the algorithm checks if it violates the liveness properties by examining:

  - AEState conditions: Eventually Always State predicates
  - AEAction conditions: Eventually Always Action predicates
  - Promises: Special temporal conditions that must be fulfilled

''LiveWorker.java:530-546''

The core violation check:
''LiveWorker.java:736-766''

===== Counterexample Generation =====

==== Step 6: Building Error Traces ====
If a violation is found, the algorithm constructs a counterexample by:

  - Creating a prefix path from an initial state to the SCC
  - Identifying the cycle within the SCC that demonstrates the violation
  - Combining these into a full trace that shows the liveness violation

''LiveWorker.java:822-853''
''LiveWorker.java:887-896''

===== Optimization and Scheduling =====
The liveness checking is not performed after every state exploration step, as that would be too expensive. Instead, the algorithm:

  - Runs liveness checking periodically based on how much the behavior graph has grown
  - Uses a threshold to determine when to run the check
  - Always performs a final check on the complete graph

''LiveCheck.java:171-200''
''LiveCheck.java:225-242''

===== Parallel Execution =====
The algorithm can leverage multiple cores by:

  - Creating multiple ''LiveWorker'' threads to check different parts of the behavior graph
  - Using a queue to distribute the work among the workers
  - Synchronizing the results and error reporting

''LiveCheck.java:262-276''
''LiveCheck.java:289-300''

===== Notes =====
  * Liveness checking in TLA+ is based on the theory of temporal logic described in Manna & Pnueli's work, but with adaptations to handle TLA's action formulas.
  * The algorithm uses an on-disk representation of the behavior graph to handle large state spaces.
  * Compared to safety checking, liveness checking is more computationally expensive, which is why it runs periodically rather than after every state generation.
  * 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.
  * The content of this page was generated by deepwiki.com.