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

• From: Stephan Merz <stephan.merz@xxxxxxxxx>
• Date: Tue, 28 Jun 2022 18:37:40 +0200
• Ironport-data: A9a23:pc6l8KwIjMUZ9wDKWa16t+eqwyrEfRIJ4+MujC+fZmUNrF6WrkUGy TRLC2iBbPvfMzP8ctl/a4nloU9Q7JKGm9dmG1drr1hgHilAwSbnLYTAfx2oZ0t+DeWaERk5t 51GAjXkBJppJpMJjk71atANlVEliefQAOCU5NfsYkidfyc9IMsaoU8lyrRRbrJA24DjWVvT4 4Oq+aUzBXf8s9JKGjJMg068gEg31BjCkGtwUosWOJinFHeH/5UkJMp3yZOZdxMUcaEIdgKOf Nsv+Znilo/vE7jBPfv++lrzWhVirrc/pmFigFIOM0SpqkAqSiDfTs/XOdJEAXq7hQllkPh/5 YlEtK2bZTwON5XTqcJFUzxVAS9xaPguFL/veRBTsOSWxkzCNmTpmrBgURxwMoof9eJ6R2pJ8 JT0KhhXNkHF17/wmejrDLQx7iggBJGD0Ic3pnVp1TXEFrUsR5vpaIqW3e9mgQYBpvpkI6iCO vE6UB9AVTmbPUBuFggmIJ05m+isi3bldCBAsxSeoq9fD237kFcrgOW2b4K9ltqiRMBajmukj W780mGhXz5GHYakkWOhyyf57gPItXqjBNh6+KeD3vJrm1aO3Xc7FBkfE16gu7y4jFS/UpReL VYV82wgt8APGFeDS9D8W1inpSfBsENBHdVXFOI+5UeGza+8Dxul6nYsQBMdYd0Xn+MNYjUSy W6vx9PMCC5hv+jAIZ6CzYu8oTS3MCkTCGYNYy4YUAcIi+UPRqlj3nojqf4zQMaIYs3J9SLYm G/V8XBv71kHpYtaiPXhpAGvbyeE/8CRFmYIChPrsnVJBz6Viaagbo2srEfetLNOcdvfQV6Gs 3wJ3cOZ6Yji7K1hdgTSHY3h/5nzv55p1QEwZ3YyRfHNEBzwohaekXh4um0WGauQGp9slcXVS EHSoxhNw5RYIWGna6R6C6roVZl0lvW8S467DqGNBjarXnSXXF/XlM2JTR7At10BbGBx+U3CE czGLpr0Vipy5VpPlWruGrZ1PUAXKtAWnDuPH/gXPjyo1r2RYHP9dFv2GArmUwzN14vV8G39q o4BX+PTkkk3eLCgP0H/rNFLRXhXfSlTLc2n96R/K7/TSiI4Qj1JI6GKmtsJJdc195m5Y8+Tl p1LchIEkwWXaLyuAV7iV02Pn5u2Asgh8StiY3x2VbtqslB6CbuSAG4kX8NfVdEaGCZLkJaYl tEJJJeNBOphUDPC92hPZJXxttU8Jhusgg2KMiW/ZyUnZNhrQAmQoo3oeQ7m9S8vCCurtJpu+ Ob5jVyFHpdTFR5/CMv2ae60yw/jt3Yqnu8vDVDDJcNeeRmx/YUzc37xg/Y7LtsiMxLGwjfGh Q+aDQ1J9+bIqo4xttLOgPnc/YuuFuJ/GGtcHnXave7mb3mEojL7zNYZAuiSfD3bWGflw4mYZ L1Yn6PmLfkKvFdWqI4jQbtmyKQJ4dGw9bJXywJTGmqSMwamB7ZmFXmx3cdVs5pLyLIE6xC9X ViC+4UDNLiEYZi3EFMYKAc/VOmb0eAInT3esaY8LEngvXEl872AXkFfMAOLlTRGarByNdp9k +smvccX7S25iwYrY4bd1XkPqDrTIyxSSbgju7EbHJTv1lghxGZEbMGOESTx+pyON4hBP0R2c D+ZgK3O2+ZVykbYKSFhEHHM2a9CgM1Ltk0XilAFIFuNl5zOgfpuhE9d9jE+TwJ0yBRb0rIsZ jI6aRUtfajerS11gMVjXny3H10TDhOu/EGsmUACk3fUThX1W2Gcfmk8Ivqw+lsE+WZQImpS8 L2Clja3VD/reN32jCQ1XkFhpvP5SsFp7UjHkcauEMnGRMZqMGa43P/xPDNW6AbhGt47n0bdp ONn1Ol3bqL/OCEKpLAjEM+R0rFJEEKII2lLQPdA+qIVHDCMI2rrgmfQdE3hKNlQI/Hq8FOjD 5A8LMx4URnjhj2FqSoWBPJRLrJ4wKwg6NYYJuK5JXIaq6DN6X1mqpXN7jO4i2gsTNFj1806L 8TebTWfCiuMgXJMn3LW69JZMHGze9gOaQDxgLKv/OMSG85Rue1gaxtpgL69vnHQLw4+uhzJ4 UXMYKjZy+EkwoNpxtO+HqJGDgSyCNXySOXYr1zp4ooWNYvCYZXUqgcYilj7JAAKb7EfbNJ6y OaWu9nt0UKZ4bs7Xgg1QXVa+3WlOClzYAZWDi4zBHxTnC/HR8q1phVepia3LptGlN4b7c6iL +d9hA1cavZNM+qxBlUMA8SdL/rZI6vwaajkqCynqOmUEV4W1gmvwBaP6yrydW8CHsMXE8SWN +I30spCIvhXq4NDABILHfZ7G4Q+K1jmMUfjmxsdqhHAZlSVbpi+VncOWPbuBfwnypVJLSoi3 a/4ew==
• Ironport-hdrordr: A9a23:KkgRhqvjcMorfuKD9/rM4v0S7skCKIMji2hC6mlwRA09TyXGra ze58jzhCWY+U4ssS8b86H4BEDgewKtyXcR2+Z+AV7MZniShILFFvAS0WKm+UyXJ8URntQtkJ uJXcBFeZ/N5BtB/IjHCDDRKadi/DD/ytHtuQ9qpE0dAj2CFZsQpjuRezzrYXGeHzM2SabRfa D0jqE3wEvbCAhnEPhXHkN1ItQr5ee74K4OByR2SiLPxzPvsdrC0s+JL/H35GZob9uPqY1SlV QtUDaJhZlLccvb9vdtvFWjr6i+VOGRqOerfPb8wvT8J17X+0yVjHQLYczIgNn9mpDLmTBa7+ XkklMbJsx2r1nRcmu2rRao+w6l/i0p92aK8y7YvUfe
• Ironport-sdr: iTA0RSpqoKPMLIHbykxOmIc0Vve3iwKIB4PkoKHNTKp7fVOjJnRHuzyB1okOGC5Qzn+yO5yOId ZejmSIPKSot5xhLEKiPdIgVz9ZQQZj7s9LwDuFEs3fxToWQPzfNiiJwrY7oozovkDau2A6CHPj /iec60Pff5NjTQOR2VFGQPzwAYlTkidDBG7suXCrGsQxsVysJmkXux6k1GpKKO2Z3TtlsukL60 uQAe73/ChRs1mMSaQfkVAJg+XTRuHExyAP9mBUconWPLD6LBwPC70boXT6sExiceUnk3eZVkq6 Ys5NmMiuxdl8BXventI3gPvR
 It seems to me that you can express this condition by writingSF_vars(TMRcvAborted /\ tmConfirmed' = RM)But I don't understand your specification well enough to know if this is a reasonable fairness condition, and why you really need this variant rather thanWF/SF_vars(TMRcvAborted)which requires TMRcvAborted to occur eventually when it is enabled, eventually ensuring that tmConfirmed = RM.Given that no action appears to be in conflict with TMRcvAborted, there should be no difference between weak and strong fairness for this action.StephanOn 28 Jun 2022, at 18:28, 钱晨 wrote:Thanks for your nice explanation.I have another question I want to ask. When I run the case after solving the problem of 'tautology', it happens to be a case that violates the liveness check like below1. We have [a, b, c] as RM2. ....3. TM is in 'aborted' state and all rms are in 'TombstoneNo' (* means forget the result, and 2pc will use Presumed Abort to answer the TM)4. TM receives one of the abort responses and fills in it in tmConfirmed(* like tmConfirmed = [a] *)5. Tm occurred tmReboot(* and tmConfirmed will be empty again(* like tmConfirmed = [] *)Then 4 and 5 will loop forever and cause a liveness problemI solve the problem by adding the following formulas into the fairness(I also add another one that involves "committed" state), and it finally pass the liveness check    /\ SF_vars(        /\ tmState = "aborted"        /\ tmConfirmed /= RM        /\ \A rm \in RM:            /\ [type |-> "RMABORTED", rm |-> rm] \in msgs        /\ tmConfirmed' = RM        /\ UNCHANGED <>                  ) It seems we must collect all responses before advancing to the next stage and cannot reboot during the process. In my way, we must write a completely new formula to achieve the goal. Does it exist another better writing style that can achieve the same goal or just use the original formula like TMRcvAborted?Stephan Merz 在 2022年6月28日 星期二晚上11:55:48 [UTC+8] 的信中寫道：> One more question, you say "When I comment out this useless fairness condition, TLC throws an exception that appears to indicate that some internal tables become too big.". I also encounter the problem, and I want to know what is meant by "some internal tables become too big". Does it mean that some data structures in TLC can not support the size of the action in the Next? It's not the next-state relation that's the problem but the fairness conditions: TLC has to monitor for each fairness condition at which state the underlying action is enabled and which transitions correspond to the action being taken. I do not know how TLC represents this information, but apparently it is not meant to handle a lot of fairness conditions (remember that you have to multiply the RM actions by the number of resource managers in the model). 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+unsubscribe@xxxxxxxxxxxxxxxx. To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/09eb6219-9a8b-4f35-ad5a-e522cf160e05n%40googlegroups.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/05BAD015-F2FC-4FAD-939C-F470AF363410%40gmail.com.