[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

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


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.