Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
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: / | ||
- | * | ||
- | |||
- | <code bash> | ||
- | java -agentlib: | ||
- | -jar ./ | ||
- | -lncheck final -fpmem 0.65 -fp 120 \ | ||
- | -seed -8286054000752913025 | ||
- | -workers 1 \ | ||
- | -config / | ||
- | / | ||
- | </ | ||
- | |||
- | < | ||
- | ---- 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 == <> | ||
- | ==== | ||
- | ----- CONFIG simple ----- | ||
- | SPECIFICATION Spec | ||
- | PROPERTIES Liveness2 | ||
- | ====== | ||
- | </ | ||
- | |||
- | **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. '' | ||
- | - LiveCheck constructor will call '' | ||
- | - '' | ||
- | - 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: '' | ||
- | - And then: '' | ||
- | - 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-<> | ||
- | // | ||
- | // " | ||
- | // " | ||
- | // | ||
- | // 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) <> | ||
- | // 2) []<> | ||
- | // 3) <> | ||
- | // 4) tf: " | ||
- | // | ||
- | // For example, below is what happens for a simple spec: | ||
- | // | ||
- | // VARIABLE x | ||
- | // Spec == x = 0 /\ [][x' | ||
- | // | ||
- | // Prop1 == <> | ||
- | // Prop2 == []<> | ||
- | // Prop3 == <> | ||
- | // Prop4 == <>(x \in Nat) \* LNAll(LNNeg(LNStateAST) in OSExprPem# | ||
- | // | ||
- | </ | ||
- | - 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, | ||
- | // just syntactically. This is hopefully sufficient, because we | ||
- | // haven' | ||
- | // up \/ and /\ above them. tfbin contains the different tf's. | ||
- | // pembin is a vect of vect-of-pems collecting each tf's pems. | ||
- | </ | ||
- | - Tfbin is an array of Tableau Particles. This is the doc: | ||
- | <code bash> | ||
- | /** | ||
- | * See Section 5.5 " | ||
- | * 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, | ||
- | * 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# | ||
- | * 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. | ||
- | */ | ||
- | </ | ||
- | - Then: VI: We then create an OrderOfSolution for each tf in tfbin. | ||
- | - There is also an option to write the Tableau graph 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 `[]<> | ||
- | // are added to the OOS. The OOS holds the `[]<> | ||
- | // (OOS# | ||
- | // OOS# | ||
- | // | ||
- | // The split into OrderOfSolution (OOS) and PossibleErrorModel (PEM) appears to | ||
- | // be a code-level optimization to speed-up the check of the liveness/ | ||
- | // in LiveWorker. | ||
- | </ | ||
- | - Because this solution has no Tableau, a livechecker is created:\\ | ||
- | '' | ||
- | - But this is an array, so depending on the OrderOfSolution, | ||