user:fponzi:liveness

Differences

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

Link to this comparison view

Next revision
Previous revision
user:fponzi:liveness [2024/11/13 20:30] – created fponziuser: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> 
  
  • user/fponzi/liveness.1731529811.txt.gz
  • Last modified: 2024/11/13 20:30
  • by fponzi