[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[tlaplus] Questions about TLA+ formula.
- From: 宏黄 <wpkzxp@xxxxxxxxx>
- Date: Sun, 24 Apr 2022 19:26:21 -0700 (PDT)
- Ironport-data: A9a23:AA/R068nIcSNlrPnack5DrUDHHuTJUtcMsCJ2f8bNWPcYEJGY0x3m GYWXT2DMqqJYmfwftx/Po239E1V6p7Qx9RrQFdvq39EQiMRo6IpJ/zJdxaqZ3v6wu7rFR88s Z1GMrEsCOhuExcwcz/0auCJQUFUjP3OHvymYAL9EngZqTVMEU/Nsjo+3b9h6mJUqYLhWVnV5 Ymu+5e31GKNglaYDEpEs8pvlzs05JweiBtA1rDpTa0jUPf2zhH5PbpHTU2DByOQrrp8QoZWc 93+IISRpQs1yfuC5uSNyd4XemVSKlLb0JPnZnB+A8BOiTAazsA+PzpS2Pc0MS9qZzu1c99Z6 oRm7M2CCgMTfYLFob4lDjhRHnAiFPgTkFPHCSDXXc27ykTHdz713awrAh9ve4If/elzDCdF8 vlwxDIlNEjSwbLrhujiG68y36zPL+GzVG8bkm1kxCndEO1lS5bIaYmVuu0D+hUK2ut0N8rjQ fYySwNKQy3tSD1+Ang5Mboxm+CngnTwaTpFsEnTrq0yi4TW5FUrium2a4GNEjCMbYIEkWGTp jLiwyPCMzcRZdnYzCWf7Fv504cjmguiAN5IfFGizdZmgUaY23cIIAESXB2+uuP8i0ikWtsZK koO+yNoo7JayaCwZtz0Xhn9uWDd+xBCApxfFOo17AzLwa3Ri+qEOoQaZhwQQ4V3howyf38F3 2bTp47IDDE+7JTAHBpx6YyohT+1PCEUK0oLaikFURYJ7rHfTGcb3kKnojFLQP7dszHlJd3j6 2vV83Vm1t3/meZOhvrrpwmW6965jsGRFlZd2+nBYo6yAupEiGONYoWp7R3C868FItjACFaGu 3cAlo6V6+Vm4XCxeM6lH7pl8FKBva7t3NjgbbhHQ8hJG9OFpifLQGyoyGsiTHqFy+5dEdMTX GfduBlK+LhYN2awYKl8buqZUpp3lfe8RIS6D6iKMrKih6SdkifXrEmCgmbAjwjQfLQEzMnTx L/AIZ38Ui1KYUiZ5GPuHLdFj9fHORzSNUuKHcyhp/hW+bWZY3GRRN843KimP4gEAFe/iFyNq 753bpPUoz0GCb2WSnSJrOY7cA9SRVBmVcGeg5EGKoarf1s2cEl/UaO56e16IORNwf8F/tokC 1nmMqOu4Aej3iKvxMTjQisLVY4Dqr4i8yJmZXB8YQfANrpKSd/H0ZrzvqAfJdEPnNGPB9YtJ xXcU8nfUPlJVBrd/DERMcv0oIB4LUr5igWJMC6obyI4YoZ7AQfO/4a8LAfo8SAPCAuxtNc/8 u37jVqAHsRcSlQwFtvSZdKu00i14SoXltV0UhaaOdJUYkjtrNVnJnWp3P86Ks0BMzvZwT6e2 1rECBsUv7ifrIo88d2PjqeB9t/7H+x7F0tcPm/a8bfmbXmArjT/mddNCb/acyrcWWX4/LSZS d9Ul/ysYucamFtqspZnF+k5wK874ezpreAIwwlhGkLNcA33WL5tJ3+x3f5PuLdI8blXtFbkQ UmI4NRbZeyENc68SwwRKQMpY/652OkQiyXV6fhpckz26DUuouiIVkJdOxSDkitANKAzO4Qgm L9ztMkT4g25qxwrLtfX3nsPrj/TcCMNA/c9q5UXII73kQ53mFtMVprRV33t65aVZtQQb0QnL 2PGhKfGgLgAlEPOf2BpTirI1OtZwI0Q4VVEkgZEKFOOld7IwPQw2UQJozgwSw1UyDRB0v5ya jc3bRwrff3W8mc6ntVHUkCtBxpFWE+T9Hv3xgZbj2beVUSpCjHAITxvPeeW4H0f6H9WejQHr riUxHy7AWTvdcD1wixgVklipPjuQsZ26xXZ3cWuGc2KEtphPmq03vLwNTVR8kWkHMUqmUfcr vNr9utYZqr8OiodrLc8FpGBk78XTUncdmBFRPhg+oIPHH3dKWHpgmHVdB7ud5MfPeHO/G+5F 9dqepBFWSO42XvctTscH6MNf+J5kfJ1ttMOdqm3dDwGr6eHtWgu953K8TXmnykkRNJhlct7I YTUMD2YFXGIwmdQknfJsdIDIXeyetIeZQfx0e3pov8FEYkP7LNlfU0oiODmunyUNE5+4UvRs l2aIaDRyONmxMJnmI61SvdPAAC9KNXSUuWU8VDs744fM4uXacqe5RkIrlTHPhhNOedDUdpAk 7nQ4sX821nIveprXm3U83Vb+3KlOSlvsCtr3sPLwL1ymCKDXIr1/UJG9T7hb5NOl9xZ64+sQ A7QhA5cszIKc481+ZGXQ3E2/9Uh52DfYaDnqiewoO6LFwAGlwfAKbtLMFf3OHpDeHZg14LWU 2fJVjXH2jychItLAxAACv58BIJgOxnoXq5Omxgdc9WHJjHAv25ucYcOWfbtBf8nx5VE/AvHD Ur5eyXD
- Ironport-hdrordr: A9a23:AiR/Q6CUAk8st/TlHekz55DYdb4zR+YMi2TDtnoBMyC9F/bz+v xG885rsSMc5AxhP03Jd7i7Sd29qV21z+8B3WBTB8bSYOHe0FHYXr2KlLGStAEIeBeOjdK0YM xbAtZD4aPLfCFHZJ3BkXaF+r8bqbHtgcKVbIHlvgtQpC5RBJ2IhD0JcjpzfHcGIjWvxPICZf mhDwl8yQZIu056UiwKbUN1LNQra+erqHoXCiR2eiLPITPv/FaVwY+/KQGR2lM1Uj9Ew7sutU jD1yLj4Lm72svLuiPh6w==
- Ironport-sdr: apdVowGic5iPWcJRcVXRkTHnlAh1TzNvzaRjUfpXv7wjRdP3A1DUmv1tNA8AqMTFjb3t7VDDpQ pjnLzaIFHI82JOVB+xXiFczq8ywdy0/Ef3GFet5qNfJfD+X6yPlCOC5MXNqi5MbLXkbAOpfodF v08bgp4d3RcKBfWVNf6kAIKIW1n+lQXuQgjBZcT4PA3oducfUh1qswKrHaNbaeiL78470TJd9s JvO9hkqN3ZPo6koGPlzkLsc+cVifSTZNEE839sZSm4O91pK4vhiIq4pBsbS57q3VVngzc+WIaC CNBXa9UruvKWYURWGTvQNrAy
Hi all.
I'm reading the TLA+ hyperbook ,And I met some questions.
In Chapter 17 Temporal Logic Question 17.5
How to prove []p=>p' is not equivalent to any legal TLA+ formula.
and in Chapter 17.4.1 lead to
How to understand F~>false,i think it is nerver true,when F is true,false do not become true
--
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/f53159ac-2f7c-4c02-9f61-64a2b11e1fean%40googlegroups.com.