Differences

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

--- user:fponzi:liveness [2024/11/13 20:34] – fponzi
+++ user:fponzi:liveness [2024/12/17 01:01] (current) – removed fponzi
@@ Line 1: / Line 1: @@
-====== TLA+ Liveness Checking Algorithm ======
-=== Goals: ===
-  - Understanding how the liveness checking algorithm works
-  - Understand how the code for the liveness checking works
-  - Produce documentation or other materials to help others understand it
----
-=== TODOS: ===
-  * This Naturals module has unused code copied from the Integers module: /home/fponzi/dev/tlaplus/tlatools/org.lamport.tlatools/src/tlc2/module/Naturals.java
-  *
-<code bash>
-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
-</code>
-<code>
----- 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
-======
-</code>
-**TODO:** Explore the implementation using some new tests.
-Unit tests are completely lacking, apparently.
-=== TLC: ===
-  - Initializes Model Checker
-      - Calls Abstract Checker
-          - Initializes CostModelCreator
-          - Initializes LiveCheck if liveness is requested. ''if (this.checkLiveness) {''\\
-              - LiveCheck constructor will call ''Liveness.processLiveness(tool)'' to generate the OrderOfSolution.
-                  - ''*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.*''
-                  - First, this method calls parseLiveness.
-                      - ParseLiveness returns a LiveExprNode in the form of liveness(fairness) \/ ~livecheck\\
-                          - Where liveness(fairness) is basically the WF_vars(Next)\\
-                          - Livecheck contains the actions used to check for liveness, as defined in the config file.
-                  - 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).*''
-                  - Then:
-<code bash>
-                      // 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
-                      //
-</code>
-                  - Then:
-<code bash>
-                      // 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.
-</code>
-                  - Tfbin is an array of Tableau Particles. This is the doc:
-<code bash>
-                      /**
-                       * 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.
-                       */
-</code>
-                  - Then: VI: We then create an OrderOfSolution for each tf in tfbin.
-                  - There is also an option to write the Tableau graph to disk: ''Uncomment to write the tableau in dot format to disk.*''
-                  - Then:
-<code bash>
-                      // 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.
-</code>
-                  - Because this solution has no Tableau, a livechecker is created:\\
-                  ''checker[soln] = new LiveChecker(solutions[soln], soln, bucketStatistics, writer);''\\
-                  - But this is an array, so depending on the OrderOfSolution, different formulas might need a TableauLiveChecker or a LiveChecker.