Hi everyone,
Given some specification formula
S:
I == ...
N == M1 \/ M2
F == []<>M1 /\ []<>M2
S == I /\ [][N]_v /\ FWriting
[]<>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>>_vWhen 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.