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