[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] Action name in error trace
- From: Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>
- Date: Mon, 30 May 2022 20:04:57 -0700
- Ironport-data: A9a23:lw1NYKq5xdb1IIiwV6sW9C9Z+hVeBmLiYBIvgKrLsJaIsI4StFCzt garIBmFPfiDYjP9LYgkb9i+8EhSu5+BzoM3SwY4qCtjFy0U8uPIVI+TRqvSF3PLf5ebFCqLz O1HN4KedJhsJpP4jk3wWlQ0hSAkjclkfpKlVKicfHoZqTZMEE/Nszo68wICqtMu0IHR7z+l4 4uo+ZWCYwf9gVaYD0pNg069gEM31BjNkGhA1rAOTagjUIj2yhH5pLpGTU2AByOQrrt8RoZWd M6fpF2NxV41yj92Yj+TfhkXRWVRKlLaFVDmZnO7wMFOiDAazsA5+v5T2Pbx9S67hh3R9+2dx umhurSecQQuZrXuiNgUShwbQhA5Iqlk+OXYdC3XXcy7lyUqclPpyvRqSV4sZMgWp7gxDmZJ+ vgVbjsKa3hvhcrsmOP9GrQq3J56apS1VG8ckikIITXxEfIvWZTeWObA49Ry9xcCvu9+Mcb3T vAzWWZLNk7jSjhgA3otJbwHrrmJrnb4dDJcpV2Porcv+C7YywkZPL3FaYeJJ4XSHZk9ckCw+ iHd83rbDwojDPu/7GCg3E2Kr+T9knauMG4VPOTgqqQCbEeo7mASExYLTkCTvf2wzEulQZdeL VYV82wvq7Iz/QqlVLHAswaQpXeFulsDQYMVHbBkrg6KzaXQ7kCSAW1soiN9hMIOmvc1QmQy9 E+1lsrsRm1e96KRa3LH6eLBxd+tAhQ9IWgHbC4CaAIK5dj/vY0+5i4jqP4zQMZZafWlSVnNL yC2QDsW3OpM0JZav0mv1RWW3GL2/8mhohsdv12PBgqYAhVFiJlJjrFEBHDe5PdEaZmDFxyP4 SZClM+Z4+QDS5qKkURhodnh/pn2vJ5p0xWG2TaD+qXNERzxpRZPmqgMsFlDyL9BaJpsRNMQS Ba7VfltzJFSJmC2SqR8fpi8Dc8npYC5S4m+B6uJMoAROMMuHONiwM2ITR7At4wKuBh8+ZzTx b/GGSpRJS1HU/Q4lmDeqxk1gOJymEjSOl8/tbiil0j9uVZvTHGSTrgBPTOzghMRvcu5TPHu2 4cPX+PTk0s3eLSnMkH/rNBORXhXcylTLc2m+qR/K7/fSiI7ST5JI6GLndsJJdc/94wLzbegw 51IchYGoLYJrSGac1Xih7EKQO+HYKuTWlpgYn1zZwv0hiB+CWtthY9GH6YKkXAc3LQL5ZZJo zMtIa1s29xDFWbK/Sozd574oNAwfRinn1vQbSWiZzc7cpF6QBHR4ZnveQ62rHsCCS++tM0fp by811KLGsFaHFs8U8uGOuiyy16RvGQGnL4gVUX/JNQOKl7n95JnKnCsg/Jue5MMJBzPyyG0z QGTBRtE9+DBr5VsqYvNiKWBtJukCa1yExMCTWXc6L+3Mwjc/3aimNMRDrzXIGqFDG6tofesf +RYyf34IcYrplcSvtouCatvwII/+8Dr++1QwDNiESiZdF+sEL5hfiSL0MQW7f9Ny7ZVtBGMV 1qL68VdPbnVasrpHERIelgqaeOM0fwbgD7P9e9zK0L/vXcl8L2CWERUHh+NlC0MfOAuadh6n 7gs6JwM9giyqhs2KdLa3CpawGKBcy4bWKI9u5BGXYLmh1Z5ylxGZpCAWCb67IvVMIdJO0guZ yCO3e/M2uoayU3FfH4+U3PK2LMF15gJvRlLyn4EJkiIyoWZ3K5phEUJ/GRlVBlRwzVGz/l3Z jphOXpzKPjc5DxvnsVCAz2hFlATAByC5nH30EYDkGGFHUCkWnaTfD84MOeJ4EdL/GVbcTxW8 6uf1X7+FDPjesj+02hpBh4096G9HYMor1OBhca8As6eFIM7azfNjaipam4FpAHgHNsqwkbAo LAyrup3bKT6Mw8WorE6WtnBju1LF07bKTwQW+xl8YMIAXrYJGO41w+IJh3jYchKPfHLrRK1B sAydMtDWw7ihXSOsiwDHvxLZLBum+Mx/5wNfbTkIWNAuLya6TVzt4/IsTT6jXcvXs4pits3M YjLdjiPH2HM12FYnXTB8JtNNmaiO4JWYQT92KWq6rxMGc9d9u5rdk423/2/uHDMaFlr+Bedv QXiYa7Kzrw9ld49wdO0SqgTVR+pLd7TVfiT9Fzhudp5a96SY9zFsBkYqwW6MglbVVfLtw+bS VhQXB/LMEL5UHIeVmnYn9yeDfAM65jsGuVQNc3zIT9Rmi7qtAoAJfcc0zjQFHCLuIo1Cgqbq 8+QZ8y3etoYVM1a2WVOLSNZFn7xzozpO7z4q3rVQ+ukU3AgPM+uED9j3XDuam5feyASPIDmE Un/vPPGChW0amhTLEdsOsyKyKOU7LMutWXKujExWfSl4rGUv26/
- Ironport-hdrordr: A9a23:ByZOEKmJgMZcjCdM+tUD0Ac3A7DpDfIW3DAbv31ZSRFFG/Fw8P rDoB1773DJYVMqM03I9urvBEDtexLhHPxOkOos1MaZPDUO0VHAROsO0WKI+UyDJ8SRzJ876Y 5QN4R4Fd3sHRxboK/BkW+F+g8bsby6GXaT9IPj80s=
- Ironport-sdr: X6tXVRH8IJdsKuCJbgU0lzJHtY3KXNHT8Jag4He7tXyBR2mfyhMeiflORigXzvDp/aE443035L ZnBhs+JcCuR7vZefCrfON/sCmuWMhzjz+O4/vPv0ilrg30RVOpYgfBkJd9GtRZXEryeL30NCF4 GjVjlOGwnReZy/YBXzOTLkoLRrgFUG1aubfvCprIAuZwlTOyhWkaDj8j7ivX4hgxh3sdKS59Ai 4ZQcDTrvnJFGLK/6zJ+mz5e9R3Fs1tEV83ByL7u/82ixEcB9CuZzJxc2HYP6tYb9bEpuD0sN3d 3S07GTM7gSSlmHP2jS3X26nh
- References: <333ef0a2-215c-4fc9-8711-3e6f39c0bf54@googlegroups.com> <de83307f-3a1c-a39f-db27-265460a25474@lemmster.de> <57efbd10-867e-4f4a-8b8b-a84697243793n@googlegroups.com>
Hi,
as far as I know, there is no documentation about what actions are retained. You will have to read and debug the source [1].
Markus
[1] https://github.com/tlaplus/tlaplus/blob/6ee6e9f1fe4b6879b7e9cdc4b3e6db687e03a03c/tlatools/org.lamport.tlatools/src/tlc2/tool/impl/Tool.java#L246-L394
> On May 30, 2022, at 6:30 PM, Haruki Okada <ocadaruma@xxxxxxxxx> wrote:
>
> Hi.
>
> Related to the original question, I'd like to know the rule when action names are retained.
>
> Let's take DieHard.tla as an example (https://github.com/tlaplus/Examples/blob/master/specifications/DieHard/DieHard.tla#L105-L110).
>
> I found that when we re-write Next as like below, the action names are not retained. (\E \in {FALSE}... is used just to transform the formula without affecting resulting truth value)
> Next ==
> \E i \in {FALSE}:
> \/ i
> \/ FillSmallJug
> \/ FillBigJug
> \/ EmptySmallJug
> \/ EmptyBigJug
> \/ SmallToBig
> \/ BigToSmall
>
> However, when we re-write like below, I found that the action names are retained.
> Next ==
> \E i \in {FALSE}:
> \/ FALSE
> \/ FillSmallJug
> \/ FillBigJug
> \/ EmptySmallJug
> \/ EmptyBigJug
> \/ SmallToBig
> \/ BigToSmall
>
> So I'm curious retaining action name or not is determined in which rule. Is that explained in some resources?
>
> 2019年12月19日木曜日 3:58:10 UTC+9 Markus Alexander Kuppe:
> On 17.12.19 06:10, Michel Charpentier wrote:
> > TLC is often able to display an action name in a trace, instead of a
> > line number. This is very useful. However, it seems to be failing the
> > moment Next is not expressed as a disjunction. I sometimes like to
> > "factorize" ghost variables when defining Next, as in:
> >
> > A == ...
> > B == ...
> >
> > Next ==
> > /\ A \/ B
> > /\ ghost variables stuff
> >
> > but then I lose the action names. I'd rather not have to write:
> >
> > A ==
> > /\ ...
> > /\ ghost variable stuff
> >
> > B ==
> > /\ ...
> > /\ ghost variable stuff
> >
> > Is there a way to avoid this duplication while retaining the action
> > names in traces?
>
> Hi Michel,
>
> I can't think of a trick to retain action names, but can't you
> reconstruct (logical) action names with trace expressions after model
> checking?
>
> Hope this helps,
> Markus
>
> --
> 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/57efbd10-867e-4f4a-8b8b-a84697243793n%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/19B24DE5-926E-4858-B01A-1150DB1A838F%40lemmster.de.