TLA+ Liveness Checking Algorithm

1. Understanding how the liveness checking algorithm works
2. Understand how the code for the liveness checking works
3. Produce documentation or other materials to help others understand it

---

• This Naturals module has unused code copied from the Integers module: /home/fponzi/dev/tlaplus/tlatools/org.lamport.tlatools/src/tlc2/module/Naturals.java

java -agentlib:jdwp=transport=dt_socket,server=y,suspend=y,address=*:5005 \
-jar ./dist/tla2tools.jar \
-lncheck final -fpmem 0.65 -fp 120 \
-seed -8286054000752913025  \
-workers 1 \
-config /tmp/elevator.cfg \
/tmp/simple.tla

---- MODULE simple ----
EXTENDS Naturals
VARIABLE x
Init == x = 1
Next ==
  IF x = 5 THEN UNCHANGED x
  ELSE x' = x + 1
Spec == Init ∧ □[Next]_x ∧ WF_x(Next)
\*Liveness == (x = 1) ⇒ ◇□(x = 5)
Liveness2 == <>[](x = 5)
====
----- CONFIG simple -----
SPECIFICATION Spec
PROPERTIES Liveness2
======

TODO: Explore the implementation using some new tests.

Unit tests are completely lacking, apparently.

1. Initializes Model Checker
   1. Calls Abstract Checker
      1. Initializes CostModelCreator
      2. Initializes LiveCheck if liveness is requested. if (this.checkLiveness) {
         
         1. LiveCheck constructor will call Liveness.processLiveness(tool) to generate the OrderOfSolution.
            1. *The method processLiveness normalizes the list of temporals and * impliedTemporals to check their validity, and to figure out the order and * manner in which things should ultimately be checked. This method returns * a handle, which can subsequently be passed to the other liveness things.*
            2. First, this method calls parseLiveness.
               1. ParseLiveness returns a LiveExprNode in the form of liveness(fairness) \/ ~livecheck
                  
                  1. Where liveness(fairness) is basically the WF_vars(Next)
                     
                  2. Livecheck contains the actions used to check for liveness, as defined in the config file.
            3. Then: *Give tags to all action and state predicates, for equality checking (tlc2.tool.liveness.LiveExprNode.equals(LiveExprNode)). We tag them here so that, if disjunct normal form (DNF) should happen to duplicate expressions, then they will still have the same tag.* - And then: *Converting the formula to DNF pushes negation inside (see LiveExprNode#pushNeg). This is important later when the promises are extracted (see LiveExprNode#extractPromises).*
            4. Then:

                      // IV:
                      // Now we will turn DNF into a format that can be tested by the
                      // tableau method. The first step is to collect everything into
                      // pems+lexps: listof-(listof-<>[],[]<> /\ tf).
                      //
                      // "pems":  Possible Error Models
                      // "lexps": Liveness expressions ?
                      //
                      // In other words, for each junction of the disjunct normal form, classify DNF
                      // into four Vects in OSExprPem with A an action and S a state-predicate:
                      //
                      // 1) <>[]A: "Eventually Always Actions"        OSExprPem#AEAction
                      // 2) []<>A: "Always Eventually Actions"        OSExprPem#EAAction
                      // 3) <>[]S: "Eventually Always States"         OSExprPem#AEState
                      // 4) tf:   "temporal formulae with no actions" OSExprPem#tfs
                      //
                      // For example, below is what happens for a simple spec:
                      //
                      //  VARIABLE x
                      //  Spec == x = 0 /\ [][x'=x+1]_x /\ WF_x(x'=x+1)     \* LNDisj(LNNeg(LNStateEnabled) \/ LNAction) in OSExprPem#AEAction
                      //
                      //  Prop1 == <>[][x' > x]_x                           \* LNNeg(LNAction) in OSExprPem#AEAction
                      //  Prop2 == []<>(<<x' > x>>_x)                       \* LNNeg(LNAction) in OSExprPem#EAAction
                      //  Prop3 == <>[](x \in Nat)                          \* LNNeg(LNState)  in OSExprPem#AEState
                      //  Prop4 == <>(x \in Nat)                            \* LNAll(LNNeg(LNStateAST) in OSExprPem#tfs
                      //

1. Then:

                      // V:
                      // Now, we will create our OrderOfSolutions. We lump together all
                      // disjunctions that have the same tf. This will happen often in
                      // cases such as (WF /\ SF) => (WF /\ SF /\ TF), since the WF and
                      // SF will be broken up into many cases and the TF will remain the
                      // same throughout. (Incidentally, we're checking equality on TFs
                      // just syntactically. This is hopefully sufficient, because we
                      // haven't done any real rearrangement of them, apart from munging
                      // up \/ and /\ above them. tfbin contains the different tf's.
                      // pembin is a vect of vect-of-pems collecting each tf's pems.

1. Tfbin is an array of Tableau Particles. This is the doc:

                      /**
                       * See Section 5.5 "Particle Tableaux" in Temporal Verification of Reactive
                       * Systems *Safety* by Zohar Manna and Amir Pnueli.
                       * <p>
                       * A {@link TBPar} means Tableau Particle. A particle is an incomplete atom
                       * because it only adheres to a relaxed version of atoms. Due to its
                       * incompleteness, it results in a more efficient tableau since its size is less
                       * than that with complete atoms. However, it does not lose generality.
                       * <p>
                       * The formulas are in positive form, meaning negation
                       * is only applied to state formulas. The state formulas are not kept in
                       * {@link TBPar}, but in {@link TBGraphNode#statePreds} instead. There is also where the
                       * successors of the particle are held.
                       * <p>
                       * TLA+ supports only future formulas and no past temporal operators (compare
                       * with p. 43 fig. 0.15), thus it uses the PART-TAB algorithm (p. 456) for the
                       * tableau construction.
                       */

1. Then: VI: We then create an OrderOfSolution for each tf in tfbin.
2. There is also an option to write the Tableau graph to disk: Uncomment to write the tableau in dot format to disk.*
3. Then:

                      // VII:
                      // We lump all the pems into a single checkState and checkAct,
                      // and oss[i].pems will simply be integer lookups into them.
                      //
                      // At this point, the temporal formulae are done and only the `[]<>A`, `<>[]A`, and `[]<>S`
                      // are added to the OOS.  The OOS holds the `[]<>S` and the union of `[]<>A` and `<>[]A`
                      // (OOS#checkState and OOS#checkAction). The PossibleErrorModel stores the indices into
                      // OOS#checkState and OOS#checkAction.
                      //
                      // The split into OrderOfSolution (OOS) and PossibleErrorModel (PEM) appears to
                      // be a code-level optimization to speed-up the check of the liveness/behavior-graph
                      // in LiveWorker.

1. Because this solution has no Tableau, a livechecker is created:
   

checker[soln] = new LiveChecker(solutions[soln], soln, bucketStatistics, writer);

1. But this is an array, so depending on the OrderOfSolution, different formulas might need a TableauLiveChecker or a LiveChecker.