Re: [tlaplus] Division in action expression

[tlaplus-google-group@xxxxxxxxxxx]

Hi Abhishek,

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.

Markus 

On Jan 28, 2022, at 6:25 PM, Abhishek Verma <vermaabhishekp@xxxxxxxxx> wrote:

[…]

I am trying to use the ALIAS feature in the generated State Graph visualization, but it doesn't seem to pretty-print it in the TLA+ toolbox UI.

I tried the command-line option to dump a dot file: 

$ java -jar tla2tools.jar Huang -deadlock -dump dot h.dot

But it does not contain the pretty-printed text either. 

Is this a missing feature?

Thanks!

-Abhishek.

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