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 values0, 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.StephanOn 3 Aug 2024, at 19:10, divyanshu ranjan wrote:> BTW, why the SF & WF rules have to be annotated with _vars?WF_v(A)  is defined to []([] ENABLED _v ⇒ <>_v) where _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]_<In this case what does WF(NEXT) will mean, ENABLED NEXT is always true and <> NEXT can be satisfied bystuttering step. This is not what we want by NEXT is weakly fair. What we want to say is that ifminutes can decrease always, it will eventually decrease. This is case with WF_minutes(NEXT). As now ENABLED NEXT is ENABLED _minutes hence it is enabled only when minutes is greater than 0and <> NEXT is now <> _minutes which means step decreasing minutes will eventually happenas it will not be satisfied by stuttering step. Hence it is better default. RegardsDivyanshu Ranjan On Sat, Aug 3, 2024 at 7:45 PM 'Michal Jaszczyk' via tlaplus 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 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.StephanOn 31 Jul 2024, at 22:35, 'Michal Jaszczyk' via tlaplus 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_activeVARIABLES y_new, y_busy, y_done, y_activevars_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 = FALSEStartX ==  /\ 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 = TRUENext ==  \/ 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 == <>[]DoneRoughly, 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, activevars == << 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 == <>[]DoneWhile 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, activevars == << 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 == <>[]DoneNow 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.