Hi Jones,--TLA+ formulas describe behaviors in terms of properties of states, which are assignments of values to variables. TLA+ is "extensional" in the sense that nothing but those values (including their changes during state transitions) are observable. Your state machine whereI == v \in {0,1}N == v' \in {0,1}Spec == I /\ [][N]_vallows runs in which v changes value only finitely often, in other words, v has some fixed value forever after a finite prefix. From what you write, it looks like you have an "intensional" view of your specification where you record when action N takes place even if its occurrence is not visible in the value of v, and you want to require N to happen infinitely often. This leads you to suggest writingLiveSpec == Spec /\ []<>N [1]TLA+ doesn't adopt this view: you would have to make occurrences of N visible, perhaps by introducing another variable such asI == v \in {0,1} /\ tick = FALSEN == v' \in {0,1} /\ tick' = ~ tickSpec == I /\ [][N]_<<v,tick>>LiveSpec == Spec /\ []<><<N>>_<<v, tick>>A core design principle of TLA+ is to ensure that all temporal formulas are insensitive to finite stuttering, and requiring actions to be "guarded" in the forms [][A]_v and <><<A>>_v is a sufficient (but not necessary) condition to ensure this. For example, consider the (non-TLA+) formula <>(x' ~= x+1): this formula is false for a behavior where x = 0, 1, 2, 3, ... but true for a behavior where x = 0, 0, 1, 2, 3, ..., so inserting a stuttering step affects the meaning of the formula.Best,Stephan[1] Incidentally, note that in this example, Spec and LiveSpec would actually be equivalent, assuming LiveSpec were a legal TLA+ formula.On 4 Oct 2023, at 00:21, Jones Martins <jonesmvc@xxxxxxxxx> wrote:Hi Stephan, thanks for the reply!I made the silly mistake of calling all liveness properties fairness properties in my previous message. And I also realize I didn't write my question clearly.I understand that the pair of formulas (Init /\ [][Next]_v, Liveness) is guaranteed to be machine closed if we define Liveness as the conjunction of weak and strong fairness properties for subactions of Next. I'm “investigating” when Liveness is anything but fairness, and the consequences of writing such formulas.That's when I came up with the example in my previous message, and why I wonder whether the following reasoning is mistaken:Specs S1b and S2b in my previous message do not allow behaviors where the value of variable v doesn't change.Let's take specs S2a and S2b. Both describe a system where either number 0 or number 1 is repeatedly picked as a value for v.S2a's liveness condition says that action N is infinitely often true, which means it's possible to pick the same number infinitely many times.S2b's liveness condition would be the correct way of expressing this same property. Weak (or strong) fairness of action N is equivalent to []<><<N>>_v.Yet, due to a correctly written liveness property, S2b doesn't allow behaviors where the same number is picked infinitely often, and I find that a little strange.That's why I think there must be a mistake in my reasoning.Best,JonesOn Tue, 3 Oct 2023 at 04:24, Stephan Merz <stephan.merz@xxxxxxxxx> wrote:Hi Jones,the effect of a state-machine specification I /\ [][N]_v becoming inconsistent after conjoining it with a liveness property L is an extreme case of violation of machine closure [1].When the liveness property is defined as a conjunction of (countably many) weak or strong fairness conditions WF(A) or SF(A) where A is a sub-action (in first approximation, a disjunct) of the next-state relation, you can be sure that every finite behavior satisfying the state machine specification can be extended to a behavior that satisfies the complete specification.Hope this helps,StephanOn 2 Oct 2023, at 21:54, Jones Martins <jonesmvc@xxxxxxxxx> wrote:Hi everyone,
Given some specification formula S:
I == ...
N == M1 \/ M2
F == []<>M1 /\ []<>M2
S == I /\ [][N]_v /\ F
Writing []<>M1 and []<>M2 as fairness conditions is said to be wrong.
In the TLA paper [1], Lamport writes:
> An action A can appear in a TLA formula only in the form [][A]_f (unless A is a predicate), so []<>M1 and []<>M2 are not TLA formulas.
In Specifying Systems, Lamport writes:
> We can require that the clock never stops by asserting that there must be infinitely many HCnxt steps. The obvious way to write this assertion is []<>HCnxt, but that's not a legal TLA formula because HCnxt is an action, not a temporal formula. However, an HCnxt step advances the value hr of the clock, so it changes hr. Therefore, an HCnxt step is also an HCnxt step that changes hr---that is, it's an <<HCnxt>>_hr step. We can thus write the liveness property that the clock never stops as []<><<HCnxt>>_hr.
When explaining the need for stuttering steps, Lamport says, “an hour and minute clock is still an hour clock if we hide the minute display”. I was looking for some example to justify the <<A>>_v operator.
Meanwhile, I had some difficulties…
Let's say specs S1a and S1b:
I == v = 0
N == v' = 0
S1a == I /\ [][N]_v /\ []<>N
S1b == I /\ [][N]_v /\ []<><<N>>_v
When the fairness condition is defined as []<>N, spec S1a only allows behaviors where v is zero and stays zero forever.
When the fairness condition is defined as []<><<N>>_v, wouldn't spec S1b be false, since v never changes? By S1b being false, I mean that there's no sequence of assignments of v that satisfies S1b. When model checking this specification, TLC accepts S1b, so I suppose there's some mistake in my reasoning.
Changing the example so that variable v is repeatedly selected to be either 0 or 1:
I == v \in {0, 1}
N == v' \in {0, 1}
S2a == I /\ [][N]_v /\ []<>N
S2b == I /\ [][N]_v /\ []<><<N>>_v
When the fairness condition is defined as []<>N, spec S2a allows behaviors where v is always 0 or always 1, which is possible although extremely (infinitesimally?) improbable.When the fairness condition is defined as []<><<N>>_v, spec S2b doesn't allow behaviors where v never changes.Does this mean <<A>>_v exists to eliminate ambiguity? Is not allowing infinite unchanging sequences a trade-off? Are there mistakes in my reasoning?
I'd appreciate your comments!Best,
Jones--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/81a73f7d-ab60-4d68-8dd1-dbe1620816fcn%40googlegroups.com.
--
You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/NnWsXf3sNRU/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/89CE3139-C47F-4421-BF15-4D078251545E%40gmail.com.
--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CABW84Kwrcahcx7UVQMVcfE-eOSZmznpmo00ejFxnZvX%3D_Ct60w%40mail.gmail.com.
You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/NnWsXf3sNRU/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/8E9DE382-49C2-4F34-8467-F3461B3BE487%40gmail.com.