user:fponzi:liveness

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
user:fponzi:liveness [2024/11/13 20:38] fponziuser: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. 
- 
-=== 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. 
  
  • user/fponzi/liveness.1731530322.txt.gz
  • Last modified: 2024/11/13 20:38
  • by fponzi