[tlaplus] Fairness conditions and <<A>>_v

[Jones Martins <jonesmvc@xxxxxxxxx>]

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!

[1]: https://www.microsoft.com/en-us/research/uploads/prod/1991/12/The-Temporal-Logic-of-Actions-Current.pdf

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.