[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[tlaplus] Fairness in multi-step protocol
- From: "'Marian Grigoras' via tlaplus" <tlaplus@xxxxxxxxxxxxxxxx>
- Date: Wed, 22 Jun 2022 00:20:49 -0700 (PDT)
- Ironport-data: A9a23:+T3RrKLlxgxyQn8KFE+RWJAlxSXFcZb7ZxGr2PjKsXjdYENSg2RRy 2sYDWCAbPqMMDSnetBwbYu+o0xT6pTTn4U3TgUd+CA2RRqmi+KVXIXDdh+Y0wC6d5CYEho/t 63yTvGacajYm1eF/k/F3oDJ9CU6jefSLlbFILas1hpZHGeIcw98z0M58wIFqtQw24LhXVnX4 YqaT/D3YTdJ5RYkagr41IrY8HuDjNyq0N/PlgFWiVhj5TcyplFNZH4tDfnZw0jQHuG4KtWHq 9Prl9lVyI92EyAFUbtJmp6jGqEDryW70QKm0hK6UID66vROS7BbPqsTbJIhhUlrZzqhhNxUl vZUh6eLdlkQHfLoqPUmbhpiKnQrVUFG0OevzXmXtMWSywjfcCKpzaw+XAc5OooX/usxCmZLn RAaAGpVP1bT2qTsmuj9E7k87iggBJGD0Ic3pnVp1TXEFrUsR5vpaJ3uwf9/9gcVofpkIMvwV e06UB9AVTmdTyURYGc+IJ05m+isi3bldCBAsxSeoq9fD237lVMtjeWwYYa9ltqid+dcxHSIp 0P/oG2mLw42LPzEyzar7Sf57gPItXqjBNh6+KeD3vJrm1aO3Xc7FBkfE16gu7y4jFS/UpReL VYV82wgt8APGFeDS9D8W1ihoyfBsEdMC5xfFOo17AzLwa3Ri+qEOoQaZiVNTYIFrf0NfgN07 3zWu+P4PgFsioTAHBpx6YyohT+1PCEUK0oLaikFURYJ7rHfTGcb3kKnojFLQP7dszHlJd3j6 2vV83Vm1t3/meZOhvrrpwmW6965jsGRFlZd2+nBYo6yAupEiGONYoWp7R3C7q8FIt/JHh+Ou 38Ln8XY5+cLZX1sqMBvaLpQdF1Kz6zdWNE5vbKJN8R4n9hK0yP7Fb28GBkkeC9U3j8sIFcFm nP7twJL/4N0N3C3d6JxaI/ZI510kPWwToq/DK6OP4smjn1NmOmvrHEGiam4jzCFraTQufxX1 WqzKpvzUS5BVcyLMhLvF7xBidfHORzSNUuKHcyhp/hW+bWZY3GRRN843KimP4gEAFe/iFyNq 753bpPUoz0GCbGWSnSJrOY7cA9SRVBmVMieg5EGK4arf1s2cEl/UaO56e16IORNwf8F/tokC 1n4BSe0PnKh1S2bQehLA1g4AI7SsWFX9C1kZ313Ywv4ixDOo++Htc8iSnf+RpF/nMQL8BK+Z 6JtlxyoDqsdRzLZ1S4aaJWh/oVueA7y21CBOC2qZDUwZZl9XxeP8djhJ1O9+C4LByuxlM0/v 7zxhliAGMFcGVtvXJTMdfai71KtpnxByuh8aE3Ff4tIc0L2/Yk2diH816dlI8wFJRjZ6CGd0 gKaXUURqeXX+tFn/97OiqSJoJ2uDvNlWEFdGjCDv7qxMCDb+EulwJNBAbbTJmmGCz2r9fz7N +tPzvz6PPkWp3pwstJxQ+Rx0KYzx9rzvLsGnA5qK3PGMgawAbR6L3jagMRCu/QWlL9UsAe7Q HiC4t1LJbKNNJ+3GVIdPlN7POuE0v4QlzbI6uktOwPx4youpOiLVkBbPh+tji1BLeola9h8m rh/58NGuRaijhcKM8qdinwG/Wq7KHFdAb4ssYsXAdO2hwcmlgNCbJjbBnOk6Z2DcY8QYEwjI zvRnambwroFlhqEfH00GnzAm+FagM1W6hxNyVYDIXWPm8bE1qBrhkwPqWxvQ1QH1AhD3sJyJ nNvax9/K5KI8mo6n8NERW2tR1xMCUzL/k3q12YPj3DTS0X0BGXBIHdjabSI9UEd72UOcT9c8 7WVx3ziTC7xOcT42CI9VA0+9KyyEYEvplKbwZ7kAsKeApMhaiDkiKKGam0PpB/qDtk2mVXc4 +Jt+b8oO6H8MCcRpYw9CpWbhORLE0nfezIdTKEz5r4NEEHdZCq2hWqEJXe3d54fPPfN60K5V 5FjK84TBR2y2DzS/2IbGbIUOO0z2/Ez48caYfXkImkJt7bZpT1s953K8TXmw3MvSs1qjN16M Z7bbDmYE2adiHYIyXXBqtJIZjixbdUePlGu2em09KAQFMtGvrg8IQc91by7u3jTOwxipkrGs ATGbq7Q7upj1YU8wNe2Q/sbX125eYHpSeCF0AGvqNASP9nBBsHD6lEOoV79MgUKYLYcVrybT 1hWXAIbAa8EgFo3b4wds5yIFq0M/MbrGeQOYpKxI35dki+PHsTr5nPvPox+xYNhyLtgCguPH mNUq/dcsfYaXNBSwHBacS9DCw1bAKPyBksljT3otOyCU3DxziSeRO5KNhbVgaVzeSgPNJnzB RXzpu61oNtfqeygwfPC6+5OW/dFHbMoZUfqmxAde9VV4qlET25uYoffqCc=
- Ironport-hdrordr: A9a23:x84Py6/DsV2hz9Xh4mtuk+BGI+orL9Y04lQ7vn2ZKCYlCvBw8v rFoB11726XtN98YgBEpThvUJPwNE812/ZOkPss1PSZLXfbUFLBFvAQ0WKa+UyVJ8SczJ8l6U /UGJIOd+EYc2IK6voSuzPIb+rIqePvmMvJuQ659QYRcegAUdAH0+4WMHf+LqW2LDMmOXP7Lv ahDwh8ygZJyR8sH7SG77U+MNQqcbbw5ejbie5sPW9d1OBGt13Yi4LSIlyjxx8bFxlPzb0h/W WAswu8yL6kr+jT8G6s61Pu
- Ironport-sdr: vU7+Qjz3kEYnCTHPg5OBvvBPwyC+Yzqu8yNhZ4zbX9gu8UbCCEePuSDWnwCN0JkmDVldAansUX YO7KT6Gey5M8VPrbY+qzekCGZyBTh2SPrJ6G9sAEY/FrKqK7JNy8DzW4Ue/F/+ajJteC/F9au3 oD0M8OJF65zOHuGSfXDU4F7s61cclL1EbZS4pjfnpQI7tZepqlivkjBcGfejcHKaqLX3Av+5SF GXWMgowmJIYSmArzBrL38pRUlYE4goA6jz4ZqJUfN12XjAiqVg4ly37SrretKiiB8wz1Ihdqc3 Ia83GYLCZ7shzh83ZWkfK+ql
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
--
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/44f1bea2-3dbc-4902-870e-5b509d7a3ef1n%40googlegroups.com.
Attachment:
cs.tla
Description: Binary data