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 a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/MB78lt4R4U0/unsubscribe.
To unsubscribe from this group and all its topics, 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.