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

Re: [tlaplus] liveness, fairness, and the style of writing TLA+



To add to this answer, requiring fairness conditions to be formulated only over non-stuttering actions ensures that TLA formulas are insensitive to finite stuttering.

As an extreme example, suppose we were allowed to write WF(x’ = x). A behavior where x successively takes the values

0, 1, 2, 3, ...

does not satisfy the formula but repeatedly inserting stuttering steps, say,

0, 0, 1, 1, 2, 2, 3, 3, …

would make WF(x’ = x) true, although the two behaviors are stuttering-equivalent. In contrast, the formula WF_x(x’ = x) holds for any behavior because ENABLED << x’ = x >>_x is equivalent to false.

Stephan

On 3 Aug 2024, at 19:10, divyanshu ranjan <idivyanshu.ranjan@xxxxxxxxx> wrote:

> BTW, why the SF & WF rules have to be annotated with _vars?

WF_v(A)  is defined to []([] ENABLED <A>_v ⇒ <><A>_v) where <A>_v is A /\ (v' /= v). Let's suppose
TLA+ allows WF(A) which is []([] ENABLED A ⇒ <>A).  In general, action A can contain stuttering steps.

For example in the following spec if minutes are less or equal to 0 NEXT action stutters.

EXTENDS Naturals
VARIABLE minutes
CHECK == minutes \in (0..5)

INIT == minutes = 5
NEXT == IF minutes > 0 
           THEN minutes' = minutes - 1
           ELSE minutes' = minutes
SPEC == INIT /\ [][NEXT]_<<minutes>
In this case what does WF(NEXT) will mean, ENABLED NEXT is always true and <> NEXT can be satisfied by
stuttering step. This is not what we want by NEXT is weakly fair. What we want to say is that if
minutes can decrease always, it will eventually decrease. This is case with WF_minutes(NEXT). As
now ENABLED NEXT is ENABLED <NEXT>_minutes hence it is enabled only when minutes is greater than 0
and
<> NEXT is now <> <NEXT>_minutes which means step decreasing minutes will eventually happen
as it will not be satisfied by stuttering step. Hence it is better default.

Regards
Divyanshu Ranjan



On Sat, Aug 3, 2024 at 7:45 PM 'Michal Jaszczyk' via tlaplus <tlaplus@xxxxxxxxxxxxxxxx> wrote:
Thanks Stephan,

BTW, why the SF & WF rules have to be annotated with _vars?

M.

On Thu, Aug 1, 2024 at 2:53 AM Stephan Merz <stephan.merz@xxxxxxxxx> wrote:
Hi Michal,

thanks for sharing the example. The style in which your final spec is written is perfectly legitimate TLA+. In particular,

\A x \in S : SF_v(A(x))

is accepted by TLC when S is a constant. TLC will expand that formula into a finite conjunction, analogous to what you wrote in the first specification.

Stephan

On 31 Jul 2024, at 22:35, 'Michal Jaszczyk' via tlaplus <tlaplus@xxxxxxxxxxxxxxxx> wrote:

Hi all,

I ran into an interesting problem when trying to write a liveness property.

Below is a contrived model of something like a persistent message queue:

VARIABLES x_new, x_busy, x_done, x_active
VARIABLES y_new, y_busy, y_done, y_active

vars_x == << x_new, x_busy, x_done, x_active >>
vars_y == << y_new, y_busy, y_done, y_active >>

vars == << vars_x, vars_y >>

Init ==
  /\ x_new = TRUE
  /\ x_busy = FALSE
  /\ x_done = FALSE
  /\ x_active = FALSE
  /\ y_new = TRUE
  /\ y_busy = FALSE
  /\ y_done = FALSE
  /\ y_active = FALSE

StartX ==
  /\ x_active = FALSE
  /\ x_active' = TRUE
  /\ x_new = TRUE
  /\ x_new' = FALSE
  /\ x_busy' = TRUE
  /\ UNCHANGED << x_done, vars_y >>

FinishX ==
  /\ x_active = TRUE
  /\ x_active' = FALSE
  /\ x_busy' = FALSE
  /\ x_done' = TRUE
  /\ UNCHANGED << x_new, vars_y >>

TimeoutX ==
  /\ x_busy = TRUE
  /\ x_busy' = FALSE
  /\ x_new' = TRUE
  /\ UNCHANGED << x_done, x_active, vars_y >>

StartY ==
  /\ y_active = FALSE
  /\ y_active' = TRUE
  /\ y_new = TRUE
  /\ y_new' = FALSE
  /\ y_busy' = TRUE
  /\ UNCHANGED << y_done, vars_x >>

FinishY ==
  /\ y_active = TRUE
  /\ y_active' = FALSE
  /\ y_busy' = FALSE
  /\ y_done' = TRUE
  /\ UNCHANGED << y_new, vars_x >>

TimeoutY ==
  /\ y_busy = TRUE
  /\ y_busy' = FALSE
  /\ y_new' = TRUE
  /\ UNCHANGED << y_done, y_active, vars_x >>

Done ==
  /\ x_done = TRUE
  /\ y_done = TRUE

Next ==
  \/ StartX
  \/ FinishX
  \/ TimeoutX
  \/ StartY
  \/ FinishY
  \/ TimeoutY
  \/ (Done /\ UNCHANGED vars)

Spec ==
  /\ Init
  /\ [][Next]_vars
  /\ WF_vars(Next)
  /\ SF_vars(StartX)
  /\ SF_vars(StartY)
  /\ SF_vars(FinishX)
  /\ SF_vars(FinishY)

Liveness == <>[]Done

Roughly, it models a queue with two elements x & y, where a worker process can take out an element out of the queue (new -> busy) and report completion (busy -> done). queue can timeout, to capture the possibility of worker failing without reporting completion (busy -> new), but the worker can still come back after timeout.

it is beside the point if this is a good way for a persistent queue to behave ;) the point is, it's a model, there is a liveness property, and thanks to the strong fairness rules, everything checks out. the stong fairness is needed to prevent infinite loop of StartX and TimeoutX, or StartY and TimeoutY.

Now, instead of mentioning elements X & Y explicitly, let's parameterize:

VARIABLES new, busy, done, active

vars == << new, busy, done, active >>

Init ==
  /\ new = << TRUE, TRUE >>
  /\ busy = << FALSE, FALSE >>
  /\ done = << FALSE, FALSE >>
  /\ active = << FALSE, FALSE >>

Start ==
  \E i \in {1, 2}:
    /\ active[i] = FALSE
    /\ active' = [active EXCEPT ![i] = TRUE]
    /\ new[i] = TRUE
    /\ new' = [new EXCEPT ![i] = FALSE]
    /\ busy' = [busy EXCEPT ![i] = TRUE]
    /\ UNCHANGED << done >>

Finish ==
  \E i \in {1, 2}:
    /\ active[i] = TRUE
    /\ active' = [active EXCEPT ![i] = FALSE]
    /\ busy' = [busy EXCEPT ![i] = FALSE]
    /\ done' = [done EXCEPT ![i] = TRUE]
    /\ UNCHANGED << new >>

Timeout ==
  \E i \in {1, 2}:
    /\ busy[i] = TRUE
    /\ busy' = [busy EXCEPT ![i] = FALSE]
    /\ new' = [new EXCEPT ![i] = TRUE]
    /\ UNCHANGED << done, active >>

Done ==
  /\ done = << TRUE, TRUE >>

Next ==
  \/ Start
  \/ Finish
  \/ Timeout
  \/ (Done /\ UNCHANGED vars)

Spec ==
  /\ Init
  /\ [][Next]_vars
  /\ WF_vars(Next)
  /\ SF_vars(Start)
  /\ SF_vars(Finish)

Liveness == <>[]Done

While this is pretty much the same thing, the liveness doesn't hold now! The problem is, Start, Finish & Timeout can enter a loop where they always choose 1, never 2. SF_vars(Start) is not the same as SF_vars(StartX) /\ SF_vars(StartY).

this can be repaired as follows:

VARIABLES new, busy, done, active

vars == << new, busy, done, active >>

Init ==
  /\ new = << TRUE, TRUE >>
  /\ busy = << FALSE, FALSE >>
  /\ done = << FALSE, FALSE >>
  /\ active = << FALSE, FALSE >>

Start(i) ==
  /\ active[i] = FALSE
  /\ active' = [active EXCEPT ![i] = TRUE]
  /\ new[i] = TRUE
  /\ new' = [new EXCEPT ![i] = FALSE]
  /\ busy' = [busy EXCEPT ![i] = TRUE]
  /\ UNCHANGED << done >>

Finish(i) ==
  /\ active[i] = TRUE
  /\ active' = [active EXCEPT ![i] = FALSE]
  /\ busy' = [busy EXCEPT ![i] = FALSE]
  /\ done' = [done EXCEPT ![i] = TRUE]
  /\ UNCHANGED << new >>

Timeout(i) ==
  /\ busy[i] = TRUE
  /\ busy' = [busy EXCEPT ![i] = FALSE]
  /\ new' = [new EXCEPT ![i] = TRUE]
  /\ UNCHANGED << done, active >>

Done ==
  /\ done = << TRUE, TRUE >>

Next ==
  \/ \E i \in {1, 2}: Start(i)
  \/ \E i \in {1, 2}: Finish(i)
  \/ \E i \in {1, 2}: Timeout(i)
  \/ (Done /\ UNCHANGED vars)

Spec ==
  /\ Init
  /\ [][Next]_vars
  /\ WF_vars(Next)
  /\ \A i \in {1, 2}: SF_vars(Start(i))
  /\ \A i \in {1, 2}: SF_vars(Finish(i))

Liveness == <>[]Done

Now things work again. In some sense, this is now closer to the original than the previous attempt, in that Start(1) & Start(2) correspond directly to StartX & StartY, and we have a family of actions Start(i), instead of a single action Start making a choice internally.

This leads me to a few questions:

1. Is \A i \in {1, 2}: SF_vars(Start(i)) supported? Obviously TLC accepted it, but I want to make sure I'm not running into something unintended. What is the class of formulas allowed inside of SF_vars(...)?

2. Are there any style guides / recommendations how to write TLA+ specs? Given this example, it would seem that something like "push your existentials to the top" would be a good piece of advice.


Cheers,

MJ

--
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/41d464a8-6f04-4ebb-84e5-0a9a8913f905n%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/eJqtgiZCeu8/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/454AB6CB-4677-48E5-BF87-F60E63CBAE34%40gmail.com.


--
Michal Jaszczyk

--
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/CAJiLpFvE59fUcNQfsbBY5kpMyiYX5EfGWnrxycxJDiOhoROFWg%40mail.gmail.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/CAL9hw256btnxodp9Opr7m1FevhMnHUPuKkBH4FtL4Mbn%2BDdrpQ%40mail.gmail.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/56FCDC6A-A5BA-4BA4-BE8A-C343D0086BB0%40gmail.com.