Re: [tlaplus] Action name in error trace

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

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