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

[tlaplus] Action name in error trace

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?


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/333ef0a2-215c-4fc9-8711-3e6f39c0bf54%40googlegroups.com.