the Alias feature is only evaluated when TLC prints traces. The state graph visualization indeed ignores an Alias. It wouldn't be impossible to add this feature, but I'm not convinced it's worth the effort.
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/FE47BEC4-D2B2-4A82-BBB3-305A21914373%40lemmster.de.