[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] Question about "Temporal formula is a tautology" in fairness
- From: Stephan Merz <stephan.merz@xxxxxxxxx>
- Date: Tue, 28 Jun 2022 17:55:43 +0200
- Ironport-data: A9a23:AsqxeKPNPPFrW7fvrR05ksFynXyQoLVcMsEvi/4bfWQNrUoh1TUGm DMcDGCDaP2JY2XwfdFxaYqxoElX65LQndBjTXM5pCpnJ55ogZqcVI7Bdi8cHAvLc5adFBo/h yk6QoOdRCzhZiaE/n9BCpC48T8kk/vgqoPUUIYoAAgoLeNfYHpn2EgLd9IR2NYy24DnWVPV4 7senuWGULOb824sWo4rw/nbwP9flKyaVOQw4zTSzdgS1LPvvyF94KA3fcldHFOkKmVgJdNWc s6YpF2PEsw1yD92Yj+tuu6TnkTn2dc+NyDW4pZdc/DKbhSvOkXe345jXMfwZ3u7hB2bwMF80 tUcpaXvCjw2HLHSiP4AVydXRnQW0a1uoNcrIFC6uM2XiknIKj7ina0oA0YxMokVvO1wBAmi9 9RCcGFLPk3F3rzphuzjIgVvrpxLwM3DIIcWonV91nLTC/0Mar+fe5X0uO5p/A0ar/9sQM39X u82UBdGUzeaWCJ+ElgQD506keiygWTnaHtTr1f9Sa8fvzOJk1wrjuiF3Nz9SJutFd8Fp1ahh l3tvFzYXConEeLG1m/Qmp6rrraXwXmTtJgpPLG57fV3m0a72mgaThgNTx66p+O4gwi/XcheI goa4EITQbMa8UWqSpz5UUT9riDc+BEbXNVUHqsx7wTlJrfoDxixFDcVQyRBOcwf64wNWh42y E+TgtfXCmk62FGKck61+rCRpDK0HCEaK24eeCMJJTfpBfGz8OnfaTqfHr5e/L6JYs7dQm6vn mjbxMQqr/BC0p5RjvTTEUXv2mr0/vD0ohgJChI7t19JAyt8bY+hIoimsB3Vs64GI4GeQV2M+ nMDnqByDdzi77nSykRho81XR9lFAspp1hWB2jaD+LF8rlyQF4aLJ9w43d2HDB4B3jw4UTHoe lTPngha+YVeOnCnBYcuPd/vUJl2k/K+TYW8PhwxUjaoSsghHONg1HE+DXN8I0iw+KTRufpiZ svDKprE4YgyUPQ/kWveqxghPU8Dn3hinws/tLj0yBOo1bf2WZJmYeZtDbd6VchgtPnsiFyNr b53bpLaoz0CDrCWSnSIqeY7cABbRVBmVMyeg5EGJoarfFA6cEl/UKS56e16K+RYc1F9zY8kC FngBhQHoLc+7FWcQTi3hodLNu++BMsv8y9lVcHuVH7xs0UejU+UxP93X/MKkXMPrbALISdcQ 6ZXdsOeLO5ITzibqT0RYYOk8t5tcxOkgQ+BJS24eCN5dJllHlSb9tjhdwrp1S8PEivm5ZBl+ ub/iFzWEcgZWgBvLMfKc/bznVm/in4QxbBpVEzSL9gPJUjhqdA4KyH4gvItDdsLLBHPmmmT2 wqMUEUXoODMp8k+99yQ3fKIqIKgEu1fGEtGHjmDvezma3WCpmf6mN1OSueFezzZRVjYwqT6a LUH1ez4Pd0GgE1O7NhxHrNt+qQ0uIniqrpc+QJ7RSmZYlmuDIRgFXmIx8x4sKNAm+1CsgysV 0PTo9RXNOzSasPoGVIcPjAoduCSyfYQlmWA5Pg5OhyktiBw+7WDXEpIOASUk2pWK74saNEpx uIoucg37Q2ji0t6aY3f1X8KqGncfGYdV6gHt40BBNO5gAQczFwfM4fXDTX74c3SZthBbhsqL zuTiPaQjrhQ3BCZIX86FHyI2eQEwJpQ4FZFy1gNI1nPkd3A36dl0BpU+DUxbwJU0hQXjL4pa zYzbxV4dfeU4jNlpMlfRGTwSQtPMxuUpx7qwFwTmWyFEkSlBz7JLXYhBOCW4Uod/z4OdzRX5 u/ImmPsUDL2e5P+2Sw9XUNqsfv+Vcc08wTEkc+qXJ/aT8hmPGS13fb3OykVrQD6C9g6nkzNq MFl++F/baD0LykNu7Z9AI6fjOxCRBeBLW1EYPdg4KJYTTqHIWrth2eDexKrZ8dAB/3W6kvkW cZgEcRCCkal3yGUozFHWKMBL+MmlfIl/oZTKLP3OXYd4fzYoSBurYrLsCf5g2AvTpNllsN6J ZnWairFDmiZnX9JgCjWscNfMXC5a9QJaVGuxuyz6+lVRZsPvPs2KhM327qw+nGbaU5poUrSs wTEaKvbiedlzN00zYfrF6xCASSyKM/yBLvUqlHt64wWYIOdK9rKuiMUtkLjY1ZcM4wXVoklj r+KqtP2gB7Isbtev7o1QHVd+3SlJPleXda79uryJXhe2C+MAYrivUNF9Ge/JphE1tha46FLg ud+hNSYLbYotxV1nRW5qBSy1z4SDKP4aqrvvySgt+/KAR8YueACBM3y7mfnNAm3aQdRU6ATy WbIVzKG6ddfo4BBCwUDGul9RZR/JTcPnEfgm8LZ7VGlM4Vjvr9OVnYOW/btBfEnx0RoyPrH3 K8=
- Ironport-hdrordr: A9a23:m89IWKi+w6gjGuf/sjjEIxK5m3BQX4513DAbv31ZSRFFG/FwyP rD7Y8mPE7P5UdoZJh/o7rwQZVoJkmshqKdgLNhTYtKOTOI1ldAQ7sSmbcKrweQahEWs9QtnJ uJncBFeZnN5XYTt7e+3OD6Kadg/DG/mJrYx9s2tk0dCj2D3spbnklE43igYwVLrXh9dOgE/c Gnl4V6TlObEBx9H6PLfAh4Lpb+SsXw5e/biFw9dmkaAW+1/H+VAZHBcyRwtS1uJg+nr41Sh1 QsUmTCl8GeWjKAu3zhPq3ojqi/KLDau5h+7QC3+6oow03X+02VjIkLYczOgNjEy9vfomrCWe O8xmZHTrtOwkKURHi8pV/G2gXr0joir1/kjXGCh2f7yPaJBA4HNw==
- Ironport-sdr: de6BEs6cLsBH2G/wO3LVuXheAdp27yYgBywU6bSsNkEQETRtYIZk35RRw8PfX3iz7MP0IjdSBf cG0grQkbku4G8bd8QzVdf8CMXsy4QYh0cFej/oe4oLGGh0He/zSFkmW9aMhMatZM9J+fFQi03W 81u6838Gh7fkb/W8oHYd68IkiDRf1Gq9XN22F1oQ4nSZbquwdr+QcN1i6stFPzKLvoOh3xJPpg kb5p583Oycg3TzVq2dMYfavYujWNAClnLvXWrZejM3iOwUtkgAdX53rkgkhonFgK33NBWc+A2X z9A1boTQ9y0+VVsVG9qI5BSM
- References: <9e859fd3-6d18-43f6-81b0-ed329f780047n@googlegroups.com> <2C070E7E-A900-4476-B102-808738D0A34A@gmail.com> <6d08a54c-e7eb-47ed-a8d2-5e551c4cac09n@googlegroups.com>
> 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/556DE16C-105F-46E9-B580-5BC5DD4C274D%40gmail.com.