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.