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

*From*: Jones Martins <jonesmvc@xxxxxxxxx>*Date*: Mon, 2 Oct 2023 12:54:39 -0700 (PDT)

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.

I'd appreciate your comments!

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

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.

**Follow-Ups**:**Re: [tlaplus] Fairness conditions and <<A>>_v***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] Re: TLA+ job: Principal Research Engineer (Formal Methods) at Huawei Ireland** - Next by Date:
**Re: [tlaplus] Fairness conditions and <<A>>_v** - Previous by thread:
**Re: [tlaplus] Re: TLA+ job: Principal Research Engineer (Formal Methods) at Huawei Ireland** - Next by thread:
**Re: [tlaplus] Fairness conditions and <<A>>_v** - Index(es):