Differences

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

--- user:fponzi:liveness [2024/11/13 20:30] – created fponzi
+++ user:fponzi:liveness [2024/12/17 01:01] (current) – removed fponzi
@@ Line 1: / Line 1: @@
-==== Goals: ====
-  - understanding how the liveness checking algorithm works
-  - understand how the code for the liveness checking works
-  - Produce documentation or else to help other people understand it.
-----
-TODOS:
-  * this naturals has unused code copied from 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 bash>
----- 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 by using some new tests.
-unit tests are completely lacking apparently
-TLC:
-<HTML><ul></HTML>
-<HTML><li></HTML>Initializes Model checker
-<HTML><ul></HTML>
-<HTML><li></HTML>Calls Abstract Checker
-<HTML><ul></HTML>
-<HTML><li></HTML>Initializes CostModelCreator<HTML></li></HTML>
-<HTML><li></HTML>Initializes LiveCheck if liveness is requested. ''%%if (this.checkLiveness) {%%''
-<HTML><ul></HTML>
-<HTML><li></HTML><HTML><p></HTML>LiveCheck constructor will call ''%%Liveness.processLiveness(tool)%%'' to generate the OrderOfSolution.<HTML></p></HTML>
-<HTML><ul></HTML>
-<HTML><li></HTML>''%%*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.*%%''<HTML></li></HTML>
-<HTML><li></HTML>First, this method calls parseLiveness.
-<HTML><ul></HTML>
-<HTML><li></HTML>ParseLiveness returns a LiveExprNode in the form of liveness(fairness) / ~livecheck
-<HTML><ul></HTML>
-<HTML><li></HTML>where liveness(fairness) is basically the WF_vars(Next)<HTML></li></HTML>
-<HTML><li></HTML>livecheck are the actions used to check for liveness, as defined for config file.<HTML></li></HTML><HTML></ul></HTML>
-<HTML></li></HTML><HTML></ul></HTML>
-<HTML></li></HTML>
-<HTML><li></HTML>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.*%%''<HTML></li></HTML>
-<HTML><li></HTML>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).%%''*<HTML></li></HTML>
-<HTML><li></HTML>Then:<HTML></li></HTML><HTML></ul></HTML>
-<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>
-<HTML><ul></HTML>
-<HTML><li></HTML>Then:<HTML></li></HTML><HTML></ul></HTML>
-<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>
-<HTML><ul></HTML>
-<HTML><li></HTML><HTML><p></HTML>Tfbin is an array of Tableau Particle. This is the doc:<HTML></p></HTML>
-<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 loose generality.
- * <p>
- * The formulas are in positive form, meaning negation
- * is only applied to state formulas. The state formulas are not keep 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>
-<HTML></li></HTML>
-<HTML><li></HTML><HTML><p></HTML>Then: VI: We then create an OrderOfSolution for each tf in tfbin.<HTML></p></HTML><HTML></li></HTML>
-<HTML><li></HTML><HTML><p></HTML>There is also an option to write the Tableau graph to disk:''%%*// Uncomment to write the tableau in dot format to disk.*%%''<HTML></p></HTML><HTML></li></HTML>
-<HTML><li></HTML><HTML><p></HTML>Then:<HTML></p></HTML>
-<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>
-<HTML></li></HTML><HTML></ul></HTML>
-<HTML></li></HTML>
-<HTML><li></HTML><HTML><p></HTML>Because this solution has no Tableau, a livechecker is created<HTML></p></HTML>
-<HTML><p></HTML>''%%checker[soln] = new LiveChecker(solutions[soln], soln, bucketStatistics, writer);%%''<HTML></p></HTML>
-<HTML><ul></HTML>
-<HTML><li></HTML>but this is an array, so depending on the OrderOfSolution, different formulas might need a TableauLiveChecker or a LiveChecker.<HTML></li></HTML><HTML></ul></HTML>
-<HTML></li></HTML>
-<HTML><li></HTML><HTML></li></HTML><HTML></ul></HTML>
-<HTML></li></HTML><HTML></ul></HTML>
-<HTML></li></HTML><HTML></ul></HTML>
-<HTML></li></HTML><HTML></ul></HTML>