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

• From: 钱晨 <allenhandora@xxxxxxxxx>
• Date: Tue, 28 Jun 2022 09:28:41 -0700 (PDT)
• Ironport-data: A9a23:HC+PEau5dPx4WMwhdepCO5DYp+fnVPNbMUV32f8akzHdYApBsoF/q tZmKTzXOfbeZGr1LdwiPI2z8x8PuZfdm9ZlGgdlpC1mHitBgMeUXt7xwmXYb3rDdJWbJK5Ex 5xDMYeYdJhcolv0/ErF3m3J9CEkvU2wbuOgTraCYEidfCc8IMsboUsLd9UR38g527BVPyvX4 Ymo+5OFaAf/s9JJGjt8B5yr+EsHUMva42twUmwWPZina3eD/5W9JMt3yZCZdxMUcKEMdgKJb 7qrIIWCw4/s10xF5uVJPVrMWhZirrb6ZWBig5fNMkSoqkAqSicais7XOBeAAKtao23hojx/9 DlCnZKiFiU1BovBpOUUawFzIXpCOKlHoJaSdBBTseTLp6HHW37lwvErFUJveINBqrcxDmZJ+ vgVbjsKa3hvhcrsmOP9GrQq3J55apC7bevzuVk4pd3dJeoiSIjHXr6J79lT9hwWvuJrLc7vS ugjQx1QXUn7QCRqFW46JKpkub2Bv1HwdDpXrF+av60q+3OVxwt0uFToGIOFIoTSH5gP9qqej kbq/13ZC0wRDsLBxWGu7Viqn8HAmyyuDer+E5XhrqIw6LGJ/UQfCQYdSECgieW9gwi7QMgaK koO+yNorK4o9UXtQMOVYvGjiHuNvxpZQtkJVuNjuFDLxa3T7AKUQGMDS1atdeDKquc4V2MIy mevku/oDAR3m4/OdXeZ9++9+Gba1TcuEUcOYioNTA0g6tbloZ0ugh+ncjqFOP7l5jESMWGgq w1mvBTSlJ1I0pFWj/TTEUTvxmPz9sKQH2bZ8y2OBjr9hj6VcrJJcGBB1LQ2xfNJLYLcV1rY+ XZdy5nY4+cJApWA0ieKRY3h/Y1FBd7abVUwYnY1R/HNEghBHVb+J+i8BxkjfC9U3j4sI2OBX aMqkVo5CGVvFHWrd7RrRIm6Ft4ny6Ptffy8CK2KNYcSPMIvLF7elM2LWaJ29zC9+KTLufFvU ap3je7xZZrnIf86k2buHLt1PUEDn3BmmDK7qW/HI+SPiOLCPhZ5uJ8KN1yBau1R0U93iFS9z jqrDOPTk003eLSmPEH/qNdPRXhXcyVTLc2o+qR/K7/bSiI7STxJI6KAkdsJJdY594wLzb2g1 i/mCidlJK/XwCOvxfOiNCA5MdsCnP9X9hoGAMDbFQj0iiF+Mdjyss/ytfIfJNEayQCq9tYsJ 9FtRilKKq0npu3v92tPYJ/jgpZlcRj31wuCMzD8PmoweJlvQwHG4Nj5ZhCp/y4LV3Llucw7q rym9wXaXZtSF185VZ2JNq2inwGroHwQuONuRE+UcNNdT0PhrdpxICvrg/5rfswBcE2RxjaT2 wuMLw0foO3B/908/NXT1PKLqo6oF611GU8DRzvX6rO/NC/7+Gu/wN8YALzYI2yFDG6tofesf +RYyf34IcYrplcSvtouCatvwII/+8Dr+O1XwwFiK3PBMAamB7ZmFX+ZhJUdu6BIwIhZjgu4Q Ee4/NdXZOeSM8T/HV9NfQcoY73Yh/EZkzXf9844OEHr+Chz8ObVWEleJUDS2iNaK7RxPYw/x vo5o4gd7Anm0kgmNdOPjyZ18WWQLy1QCP5+7c5EX4K72BA2zlxiYIDHDnOk6p+4bdgRYFIhJ SWZhfafirlRmhjCfn40GSSf1OZRn85S6hVDzVtHPlfQ39Sc1q5x0xpW/jA6CA9Sy0wfge50P 2FqMWxzJLmPr2g03pkdBzj0FlETHgCd92zw10ANyD/TQX6uWzGfN2Y6I+uMoB0U/jMOejlA4 Iye03vvVTq2Lsj90jFsCRxgov3nUdsj+QrFl8SqEN6CAoEhJD/shKahaClT9Eu2XZ5v1BKe/ Lcp4eBrdKfgPjQRqaATBI6d2rAdRwqDOXRZB/pm+fpRT23bfTiz3xmIKlywK5MWfKWRrhHnB pw8PN9LWjS/yD2K8mIRC5kKLuImh/Uu/tcDJu7mKGJa4bKToiA14cDQ6jTmnz1sBNp0ltslM cXecDWNFmHWjnxR3GDXq9RcfXa8aMEAeRa7x/2/6+4TFpgOvewwI1s+1KC44yecPAd9pU7Gu QrCY+rPzLUnx908zs3jFaJMAwjyItT2Dbza/Ae2utVITNXOLcae6F9P+we/Z1xbbekLRtB6t bWRq9qrjknLi7A7DjLCkJ6bGqgVuMi/UYK76C4swKW2QMdDZCPt3/fH02WxKJgMidAEo8f+F 1r+Z8y3etoYHdxawRW5rsSY/wk1U8zKgmXI/EtRbMhgzjAS1gvIKN6o73j0dXodfSgNU3E7I hGhoO6gv7i0s6wVbCLpxJha71tQL1jkVq8reMf2qCGDSGKvhztuf1ckeQUIsVn2N5VPLCo2D V8piPQzmNRedZwkFO1kjrE=
• Ironport-sdr: VMe0+z8TEYbfzDw/spI0/6jmWL50Mxplh2UjfrFGe418KMli8SCg3JIFCdoa8VLNMTNonJYuKh hneZsyMJYyZNfYRKOWofhj5Q7MOLM13B4i112FNQ5ruDoRmru2J11rr2T7jJ5C0UBzvItoWY1B NZYwsAI8X35V8JgEad4pkoLE09p0M9YApWjTSjZGt4b7ZB8vy60jBUzzHddFgcEWLEjpv4SvQT bTPHrS/W8Z4PZ6X+71SDAZ7cm4q6enUFAGeRrIixKV08sp7j2n6ogXiLqaRA1GnjT5Hml5njSA jpSrTVWUzF2v3DNB3a6985Bh

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