Fairness in multi-step protocol

[Marian Grigoras]

I have a Client (C) and a Server (S) talking a simple multi-step protocol for one logical exchange:
1) C sends request1 to S
2) S answers with response1
3) C continues with request2
4) S answers with response2

Now I want to allow the server to respond with an error in step 2, in which case the client resends request1:
1) C > S: req1
2) S > C: either resp1 or error
3) C > S: if error resend req1, if resp1 send req2
4) S > C: resp2

For simplicity I'm not using queues between C and S, but just 2 variables to hold the messages between C and S: C2S and S2C (the protocol should ensure that at most one message is ever sent between the 2 parties).

I disabled the deadlock check, and added a temporal formula <>Terminated, where
Terminated == /\ pc[0] = "client"
              /\ pc[1] = "server"
              /\ S2C = NULL
              /\ C2S = NULL

I'm also using an artificial initial message S2C="bootstrap" to trigger a single client-server exchange.

What I observe:
"Temporal properties were violated." with a "Back to state 6" indication of a loop.

What I expected:
Making the server process strongly fair, I expected that the server is guaranteed to "at some point" take the "normal response" branch, which leads to termination.

Afaict TLC is telling me that the server can infinitely respond with error, but doesn't this go against strong fairness?
It feels like I'm missing something basic about how to define the termination condition with proper fairness for such a multi-step protocol.

Any pointers on how to fix (or model differently)?
Thank you

[Stephan Merz]

You may want to look at the discussion of what I believe is an analogous question: https://groups.google.com/g/tlaplus/c/99lWDQyk-wE

In short, you want to express the intended fairness assumption at the TLA+ level by writing something like

SF_vars(SOnReq1 /\ S2C' = "response1")

Regards,

Stephan

--
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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/44f1bea2-3dbc-4902-870e-5b509d7a3ef1n%40googlegroups.com.
<cs.tla>

[Marian Grigoras]

Using FairSpec == Spec /\ SF_vars(SOnReq1 /\ S2C' = "response1") solved it.

Thanks for the link!

Marian