[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Action name in error trace

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

Hope this helps,

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/de83307f-3a1c-a39f-db27-265460a25474%40lemmster.de.