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

• From: 钱晨 <allenhandora@xxxxxxxxx>
• Date: Tue, 28 Jun 2022 19:52:29 -0700 (PDT)
• Ironport-data: A9a23:Pfb5/KzrZVLjeNDkM+V6t+eTwyrEfRIJ4+MujC+fZmUNrF6WrkUCy 2AcCmjQOamLMWHyKIx+Pt7g8EJUu5/WzNA1TgM+qVhgHilAwSbnLYTAfx2oZ0t+DeWaERk5t 51GAjXkBJppJpMJjk71atANlVEliefQAOCU5NfsYkidfyc9IMsaoU8lyrRRbrJA24DjWVvT4 4Oq+KUzBXf8s9JKGjJMg068gEg31BjCkGtwUosWOJinFHeH/5UkJMp3yZOZdxMUcaEIdgKOf Nsv+Znilo/vE7jBPfv++lrzWhVirrc/pmFigFIOM0SpqkAqSiDfTs/XOdJEAXq7hQllkPhK1 PdK7IC+Sj0vFYrrw7hDVx9ETCNHaPguFL/veRBTsOSWxkzCNmLvmrBgVRBse4If/elzDCdF8 vlwxDIlNEjSwbLrhujhEK81155LwMrDZOvzvll8yTjBCes9AprFSI/hw+d6+QcIt+1sJ9yFV 5ZEMxlWSTv5TiBvBHRKU6MWk+CviX3yfCdftUqO46Ew5gA/ySQti+O3aYqMJrRmQ+0Ou1+Gu EPU317hGy9FLIOl4zul4EOz07qncSTTAdpOTtVU7MVCjFyIzXEIEzUKUVL9pOKjz0+4QdNWb U0S4Csn66YonHFHVfH4Vhy85WeH51sSAosKVeI97w6Jx+zf5APx6nU4oiBpU8AEs5YqSz8Q0 HSuuIi1WzhprOKXcCfInluLlg+aNS8QJG4EQCYLSwoZ/tXuyL3faDqfHr6P94bl3rXI9SHML yOi93dh2u1C5SIf/+DqogCd2mPESo3hF1Ztvm3qsnSZAhSVjbNJiqSt4FnfqO9DdcOXFwjb+ ncDnMea4aYFCpTleM2xrAclQuDBCxWtamW0bbtT838Jqm7FF5mLINg43d2GDB01WvvogBewC KMphStf5YVIIFyhZrJtboS6BqwClPa9S4i5D6iPMoQTO/CdkTNrGgk+NSZ8OEi9wCARfV0XZ P93jO73UClGUf87pNZIb75NieF1rszB+Y8jbcmjk07PPUu2a3mSRrMIWGZinchohJ5oVD79q o4HX+PTk0s3eLSnPkH/rNBORXhXcylTLc2m+qR/K7/eSiI7STFJI6GLndsJJdc/94wLzbegw 51IcgoGoLYJrSOXc1zih7EKQOiHYKuTWlpnZ3NzYQ31hCJ/CWtthY9GH6YKkXAc3LQL5ZZJo zMtIa1s29xDFWbK/Sozd574oNAwfRinn1vQbSWiZzc7cpF6QBHR4ZnveQ62rHsCCS++tM0fp by811KLGsFaHFs8U8uGOuiyy16RvGQGnL4gVUX/JNQOKl7n95JnKnCsg/Jue5MMJBzPyyG0z QGTBRtE9+DBr5VkotbMjKGA6YyuFrImTEZdGmDa65ewNDXbrjLzm98eDL7QcGmEBm3u+aika eFE9N3GMaUKzARQro5xM7d31qZhtdbiorltyA47TnjGalKcDKw5fiuL0MxJga16xrFDvDywV E/SqMJRPq+EOZ+8HVMcfVF3bumK2fwOoDTK6eUpJ0H2uH1+8LadCBsAMB6LhyhQI6FyLZs+h +wmvZdOuQC4jxMrNPeAjzxVpjTXdSVbDPt4u8FIGpLvhyoq1kpGPc7WBBjw7czdcN5LKEQrf mKZiaee1bRRwk3OLyg6GXTXh7YPgJ0PvFVTzwZHKQ3YwJzKgfg42BAX+jMyF1wHwhJC2uN1G 25qK0wlevnUrmkw3JBODzK2BgVMJByF4UitmVEHo2vUEhuzXWvXIWxhZOuArRId8nlAQz5A4 bucxDq3WDrmZp+hjC47WEp5rK7sStt+8gDNgse6B9/AGpA8aDXowfTxNTtU9kW3Xppo2g7ao /J39v17c6zxOAYfpKo0D4SVz7MNUAvCL2tHGKkz8KQMFGDaWTezxTnfexvqI5gSeaPHoR2iF shjBsNTTBDihiyAmTYWWPwXKLhukf91udcPdu+5LGIKqefO/Dp1rIrLpG+5i3UsXs1118k6L YzVenSJFWnXimFThneKsM1NIm6lep4feQfn1/q0+ugEGs5Rqu1qak1ugLK4s2/PbFli9hOQ+ RrAPurYlr04j4trmIToH+NIAADtcYH/U+GB8QaStdVSbIOQbZ2f6VtN8lS3bR5LObYxWshsk ejfutDA2k6Y7q09VHrUmsXcGqREjSlosDG77i4qwLhmcSq+tAvE5hIC/yWhKsUMnooMvI+oQ Ay3bMb2ftkQMzuYKLu5dAAGeyvxyYyuBksjmc95h/uLDRcZ3APdK86/7jniamQzmuogJcjlE gGt0xqxzokwkWmPbSPow9lpBJh3JFLsQ6w7b8a3vj6dZoVtbpVupZO6/ScdBfr35rVo3So0D V8phvQzSfhqhJz18Q==
• Ironport-hdrordr: A9a23:7u4AJK2ghCUKFe5KUo6s0gqjBDkkLtp133Aq2lEZdPU1SL3lqy nKpp536faaskd0ZJhNo6HmBEDEewKlyXaaibNhS4tLcmHdyRyVxcJZnPjfKwSJIVyLygcl79 YoT0EcMqyMMbDO5vyKkDVQbexQueVvq5rY9Ns2pk0FJWoaCZ2IrT0JcTpzdHcGOjWuKqBXKH P23Ls8m9PPQwVwUix7bkN1PNQrZOekqHslW3I7765N0nj6sdpl0t/H++jy5GZgb9qH+9dSlF TtokjC/62m99u7xhXf22KWz5MTtsDm1sIrPr3/tvQo
• Ironport-sdr: ANd8b9j3k1zACCktYem8iJi7yv65isUIe9thr9LNq+mlmhMukSOxviljjyVTdbWhsqFCbTd5SO hXP5b9NtGi+CWfgjqgmOF7/wiqrt6ck/xsKMsK7a4BeNUw5bVW1Nj0lWpdIiVmklZuxMnjNoVj 5tFweCBT+abeYQVLX1mjaYLHzk9AqSM4/kbW5UOJpm9hOi3vK3dmh3GPa44d4jwthTJvT0lIGL mWED9M8wI7ZZcgzxnqQiLj2aeT6f+3Uz7VuEXnPpcaOPzpKdExGVqiyzT28r9vIoWW0xJoO+I6 deECHHnjizdBWhFLulabt5JH

I add the following condition into the fairness formulas, while it still reports the error for the liveness problem.


/\ \A rm \in RM:

SF_vars(TMRcvAborted(rm) /\ tmConfirmed' = RM)



It still appears that tmReboot occurred repeatedly before tmConfirmed is fully collected, so it loops infinitely and violates the liveness property.

I do not understand what will happen if I declare a formula in liveness except formulas that already occurred in Next.

Will it be evaluated as an action or it will do something else?

Stephan Merz 在 2022年6月29日 星期三凌晨12:37:45 [UTC+8] 的信中寫道：
It seems to me that you can express this condition by writing

SF_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 than

WF/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.

Stephan

On 28 Jun 2022, at 18:28, 钱晨 <allenh...@xxxxxxxxx> wrote:

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 below
1. We have [a, b, c] as RM
2. ....
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 problem

I 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 <<rmState, tmState, tmParticipants, tmPrepared, msgs>>

)



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+u...@xxxxxxxxxxxxxxxx.