[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?

MC

--
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.