Re: [tlaplus] Action name in error trace

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

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.