Differences
This shows you the differences between two versions of the page.
Next revision | Previous revision | ||
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: / | ||
- | * | ||
- | |||
- | <code bash> | ||
- | |||
- | java -agentlib: | ||
- | -jar ./ | ||
- | -lncheck final -fpmem 0.65 -fp 120 \ | ||
- | -seed -8286054000752913025 | ||
- | -workers 1 \ | ||
- | -config / | ||
- | / | ||
- | </ | ||
- | |||
- | <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 == <> | ||
- | ==== | ||
- | ----- CONFIG simple ----- | ||
- | SPECIFICATION Spec | ||
- | PROPERTIES Liveness2 | ||
- | ====== | ||
- | </ | ||
- | |||
- | TODO: Explore the implementation by using some new tests. | ||
- | |||
- | unit tests are completely lacking apparently | ||
- | |||
- | TLC: | ||
- | |||
- | < | ||
- | < | ||
- | < | ||
- | < | ||
- | < | ||
- | < | ||
- | < | ||
- | < | ||
- | < | ||
- | < | ||
- | < | ||
- | < | ||
- | < | ||
- | < | ||
- | < | ||
- | < | ||
- | < | ||
- | < | ||
- | < | ||
- | < | ||
- | < | ||
- | < | ||
- | |||
- | <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# | ||
- | // | ||
- | </ | ||
- | |||
- | < | ||
- | < | ||
- | |||
- | <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. | ||
- | </ | ||
- | |||
- | < | ||
- | < | ||
- | <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 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# | ||
- | * 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 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. | ||
- | </ | ||
- | < | ||
- | < | ||
- | < | ||
- | < | ||
- | < | ||
- | < | ||
- | < | ||
- | < | ||
- | < | ||
- | < | ||
- | < | ||