# Re: [tlaplus] Question about "Temporal formula is a tautology" in fairness

• Date: Thu, 14 Jul 2022 20:53:43 -0700
• Ironport-data: A9a23:9IbDvaKv2cKX4AW4FE+RXJAlxSXFcZb7ZxGr2PjKsXjdYENShDBWm GIaUTqPb62JM2L3KI8lbIuy8EtU7JCGnNE3QQAd+CA2RRqmi+KVXIXDdh+Y0wC6d5CYEho/t 63yTvGacajYm1eF/k/F3oDJ9CU6jefSLlbFILas1hpZHGeIcw98z0M58wIFqtQw24LhXFrR4 YiaT/D3YTdJ5RYkagr41IrY8HuDjNyq0N/PlgFWiVhj5TcyplFNZH4tDfnZw0jQHuG4KtWHq 9Prl9lVyI92EyAFUbtJmp6jGqEDryW70QKm0hK6UID66vROS7BbPqsTbJIhhUlrZzqhvMprm fxtlb2JEV13AJfTisAzWjhcHHQrVUFG0OevzXmXtMWSywjHdyKpzaw+Ugc5OooX/usxCmZLn RAaAGpVP1bT2qTvnuz9E7ky7iggBJGD0Ic3pnVp1TXEFrUsR5vpaIX43fBo8AcZr/pkIcn8V u09QB9AVTmaSUZoGQomIJ05m+isi3bldCBAsxSeoq9fD237lV0qj+Cyboe9ltqiYZkJl0+Vn 2T84U/HLxIWEue8+2vG/Sf57gPItXqjBNh6+KeD3vJrm1aO3Xc7FBkfE16gu7y4jFS/UpReL VYV82wgt8APGFeDS9D8W1i5pCfBsEdMBZxfFOo17AzLwa3Ri+qEOoQaZh1bco0PlO8XfGRwi GGzgMHNKzVOtLLAHBpx6YyohT+1PCEUK0oLaikFURYJ7rHfTGcb3kKnojFLQP7dszHlJd3j6 2vV83Vm1t3/meZOhvrrpwmW6965jsGRFlZd2+nBYo6yAupEiGONYoWp7R3a6a8FIt/JEB+Ou 38Ln8XY5+cLZX1sqMBvaLpXdF1Kz6zeWNE5vbKJN8V/n9hK0yL9Fb28GBkkeC9U3j8sIFcFm nP7twJL/4N0N3C3d6JxaI/ZI510kPewT4+5Da+IN4Qmjn1NmOmvrHEGiam4jzCFraTQufxX1 WqzKpvzUSxLUcyLMhLvH7pCgNfHORzSNUuKHcyhp/hW+bWZY3GRRN843KimP4gEAFe/iFyNq b53bpPUoz0GCbGWSnSJrOY7cA9SRVBmVcGeg5EGLYarf1s2cEl/UaO56e16IORNwf8K/tokC 1nmBie0PnKk2CWbQehLA1g/AI7SsWFX9iJibXZ0YQbyghDOo++Htc8iSnf+RpF/nMQL8BK+Z 6BtlxyoDqsdRzLZ1S4aaJWh/oVueA7y21CBOC2qZDUwZZl9XxeP8djhJ1O9+C4LByuxlM0/v 7zxhliAGMFcGVtvXJTMdfai71KtpnxByuh8aE3Ff4tIc0L2/Yk2diH816dlI8wFJRjZ6CGd0 gKaXUURqeXX+tZn9NTMgLuYop3vH+YnRhhWGGzS7LCXMyjG/zP/kNEaD7vSJWjQDTqm9r+ja ONZy+DHHMcGxFsa4ZBhF7tLzL4l44e9rbFtyAk5Tm7AaE6mC+89L3SLhJIdtqBEyrJDgwauX lOT/d1WZeeANM//SQBDKw0iYeCO2usThyHJq/8yJRyitiNw+bOGV2RUPgWN2XwGd+Iub916z LdzotMS5iy+lgEuboSMgBdS+jneNXcHSagm6swXDYK32AomzlZOPc7VBiPsus3dbtxNNgwrJ mbRivOS2fJTwU3Nd3d1Hn/IhLIPiZMLsRFM7VkDO1XZxYaf16FvhEVcoWYtUwBY7hRbyOYva GJlAEt4ePeV9DByickfAm2hSlNFBQaFx0rq1lENmDGLRkWkTDKdfmg0OOKR+xIW9GVTejVU5 raF0H2gVD/sdc78nXBtCR859qKzEoUoqE7fntu6Fd+OBZgwbBLqhaihYWcHsRz6Gdh3j0rC/ LE48OF1YKz9FCgRv6xqW9LBjO9PFk+JdD5YXPVs3KIVBmWAKju87j6DdhKqccRXKv2WrEK1B 5A8L85DTUjvhiaSsigAV+lLLKVzgeYyotUFfbzvKCgNtL7YoSBurYqX6iz3nGs2WJJ1jMwmI ZnQfT+PHzDCn3dSgGOR/sBINnDiPYsBbQz4meGxqaAHTsJd9u5rdk423/2/uHDMaFlr+Bedv QXiYa7Kzrw9ld49wdO0SqgTVR+pLd7TVfiT9Fzhudp5a96SY9zFsBkYqwW6MglbVVfLtw+bS VhQXB/LMEL5UHIeVmnYn9yAE/AM65ziAqxYNcX4KHQcliyHMCMpD93v5EjgQaGlUvsEjiVke +d8QMS3ctERVthHw2BNcG5VFBN152HfcPL7vS3kxxiTIkF17OEERe9LMVfmamZUciIHIZrjE hSysPGrjjydQEKgGzdcb8xb71REzJMPlEfomxAdddVVM4Vwvm6/hw==
• Ironport-hdrordr: A9a23:jSehdqyPMnztUdgLY/tRKrPxY+skLtp133Aq2lEZdPULSKDo7/ xGzc53pGbJYWgqMgBHpTnmAtj/fZq8z+8L3WB1B9iftWbdyRiVxe1ZnPffKnjbalnDHgA079 YiT0BRYOeATWSSzvyKrDVRKr4bsZi6GdmT9KXjJ8IHd3AmV0gf1XYPNu/rKDwGeOAcP+tyKH P03KMuzEvFCA9nE/hXHkN1JdQr5ee75q4OByR2TCLPxzPusdrC0s+LL/H35GZqb9uPqY1SlF QtUDaY2kxgiZ+GIq+27R6c032boqqD9jNPb/b8wvT82l7X+0+VjU1aKt/y2wwdkaWV8k8jlN SJmwstI8g2y365RBDCnTLdnzP42DJrwX7vw12VjD/CpojWXzQnEqN69M1kTic=
• Ironport-sdr: fRLfc4KUlLRywiics+HAVqnWQ0Tb2kkA/kfVfP8YYtMOYVQutZDS1lE+IlmCQf6/2ME+rAskii GrjBtIQlctUTKCKXzFSXa4GMyHoPoUycKu2CY//7EvMqQnAtEuazYD6SlWJBZjgn0I+nOtXPS6 x42cq0yJptAx/Mbb1VhYFwSOfwdCuQBBs98Yb4w63e3F5RtzjS4eM5/VcF98fKUwgYSLUpe3ZR NPjvG1ehZeaqSE56Dq775v8dmUus1TwvtYER5ax+zfJIvSQp4C6E8U9gOYgPRm/u3hMaiVedv2 97QwZr3pTW3Jy9u9my820q3v

The bogus error message has been corrected as part of https://github.com/tlaplus/tlaplus/issues/742

Markus

> On Jun 28, 2022, at 12:07 AM, Stephan Merz <stephan.merz@xxxxxxxxx> wrote:
>
> Hello,
>
> I believe that TLC is wrong when it claims that your liveness property is a tautology. Your fairness conditions include
>
> \A rm \in RM : SF_vars(TMRcvPreparedNO(rm))
>
> where TMRcvPreparedNO is a stuttering action (as the comment above the action definition confirms). Therefore,
>
> ENABLED <<TMRcvPreparedNO(rm)>>_vars
>
> is equivalent to FALSE (for any value of rm), and the fairness condition is equivalent to TRUE – but that just means that this condition is trivial, not that the entire liveness property is a tautology.
>
> When I comment out this useless fairness condition, TLC throws an exception that appears to indicate that some internal tables become too big.
>
> Trying to reduce the size of the fairness condition, I defined formulas TMNext and RMNext(rm) corresponding to the disjunctions of all actions of the transaction manager and of the resource managers, respectively [1]. I then replaced your fairness conditions by
>
>   /\ WF_vars(TMNext)
>   /\ \A rm \in RM : WF_vars(RMNext(rm))
>
> Now TLC produces what appears to be a sensible counter-example in which the TM reboots very frequently. I therefore adjusted that condition by removing the TMReboot action from the fairness condition [2], i.e.
>
> Fairness ==
>   /\ WF_vars(TMRcv2PC \/ TMDecideToCommit \/ TMDecideToAbort \/ TMForgetCtx)
>   /\ \A rm \in RM : WF_vars(RMNext(rm))
>
> For this specification, TLC says that the liveness property is satisfied. (Note in particular that weak fairness appears to be enough for this specification.) Of course, it is up to you to decide if that corresponds to a reasonable fairness hypothesis for your algorithm.
>
> Lessons learnt:
> 1. Do not assert fairness conditions for stuttering actions – although I believe that TLC should be able to handle those.
> 2. Prefer few fairness hypotheses for disjunctions of actions (that correspond to progress of individual actors) over conjuncts of many individual fairness conditions.
>
> Hope this helps,
> Stephan
>
> [1] Probably you do not want to include all actions in these disjuncts, but I didn't have time to understand your specification in detail.
> [2] I am assuming that rebooting corresponds to an error in the execution, which the algorithm has to be prepared to handle, but which you do not request to occur.
>
>
> --
> 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/2C070E7E-A900-4476-B102-808738D0A34A%40gmail.com.
>
>
>> On 26 Jun 2022, at 10:35, 钱晨 <allenhandora@xxxxxxxxx> wrote:
>>
>> I have recently written a 2pc protocol with fairness, I first write all request/response handlers as the strong fairness(except reboot and exception events) in order to pass the liveness check:
>>
>> the liveness check is as below:
>> 2PCLivevess == \A r \in RM: 1 = 1 ~> (2pcState[r] = "aborted" \/ 2pcState[r] = "committed")
>>
>> the spec is something like below:
>> ================== start====================
>> Fairness ==
>>
>>     /\ WF_vars(TMRcv2PC)
>>
>>     /\ SF_vars(TMDecideToAbort)
>>
>>     /\ SF_vars(TMDecideToCommit)
>>
>>     /\ \A rm \in RM:
>>
>>             SF_vars(TMRcvPreparedOK(rm))
>>
>>     /\ \A rm \in RM:
>>
>>             SF_vars(TMRcvPreparedNO(rm))
>>
>>     /\ \A rm \in RM:
>>
>>             SF_vars(TMRcvCommitted(rm))
>>
>>     /\ \A rm \in RM:
>>
>>             SF_vars(TMRcvAborted(rm))
>>
>>     /\ \A rm \in RM:
>>
>>             SF_vars(RMRcvPrepareOK(rm))
>>
>>     /\ \A rm \in RM:
>>
>>             SF_vars(RMRcvPrepareNO(rm))
>>
>>     /\ \A rm \in RM:
>>
>>             SF_vars(RMRcvCommit(rm))
>>
>>     /\ \A rm \in RM:
>>
>>             SF_vars(RMRcvAbort(rm))
>>
>>     /\ \A rm \in RM:
>>
>>             SF_vars(OrphanRMRcvMsg(rm))
>>
>>     /\ \A rm \in RM:
>>
>>             SF_vars(RMForgetCtx(rm))
>>
>>     /\ SF_vars(TMForgetCtx)
>>
>> ================== end ====================
>>
>> While the model check reports "Temporal formula is a tautology (its negation is unsatisfiable).". Can any tell me why my fairness check reports the errors.
>>
>>
>> --
>> 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.
>
>
> --
> 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/2C070E7E-A900-4476-B102-808738D0A34A%40gmail.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/C2134D23-304C-4994-8970-E4E586FFF28E%40lemmster.de.



• References: