Enhancing state transition information in TLC’s DOT output

[Ana Ribeiro]

Dear TLA+ Community,

I am currently using TLA+ and TLC to develop a testing strategy for microservice architectures, leveraging the state space graph produced by TLC. 

I am looking for ways to enrich the information available in the transition edges of the graph.

As of now, the information included on state transitions is the action responsible for the transition. However, I would like to also capture the model value used in the action. 

Let’s say I have an action A receiving as argument one element of the set of model values {a1, a2}. When action A occurs, I would like to know whether a1 or a2 was used, without having to inspect the states before and after the transition. 

In the current version, the edge definition in the generated DOT file looks like this:

s1 -> s2 [label="A"];

However, I would like to generate something like this:




s1 -> s2 [label="A (a2)"];

I have looked into the DOT generation code in the TLA+ repository as well as the DOT language grammar, and it seems that capturing the model value information should be possible. However, I would greatly appreciate any guidance on:

• Whether there is an existing way to achieve this within TLC; or
• If there is the possibility to modify the current version of TLC to include model values in the generated DOT output.

If anyone has insights or past experience with something similar, I would be truly grateful for your advice.

Thank you all for your time.

Best regards,

Ana Catarina Ribeiro

PhD student - Computer Science @ NOVA FCT

[Frederic Marand (FGM)]

Seconding that idea: I looked for that feature when I discovered the graph generator feature, and regretted no to see it.

This email, including any attachments, is confidential and may be privileged. If you are not the intended recipient please notify the sender immediately, and please delete it; you should not copy it or use it for any purpose or disclose its contents to any other person. If the email, including any attachments, is legally privileged, you should not forward it to any other person.

[Markus Kuppe]

The method `tlc2.tool.Action#getParameter` exposes an action's parameters, if any. Your proposed feature essentially involves including these parameters in `tlc2.util.DotStateWriter.writeState(TLCState, TLCState, BitVector, int, int, short, Visualization, Action, SemanticNode)`. To contribute, please submit a pull request at https://github.com/tlaplus/tlaplus/pulls.

Related:
* https://github.com/tlaplus/tlaplus/blob/master/CONTRIBUTING.md
* https://github.com/tlaplus/tlaplus/commit/0999e2c1bc65679cb8107aa225105c88581801c4

> --
> 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+u...@googlegroups.com.
> To view this discussion visit https://groups.google.com/d/msgid/tlaplus/808576B3-F9F4-4D07-87AD-31959A5DAF5F%40campus.fct.unl.pt.

[Ana Ribeiro]

Dear TLA+ community, 

I have implemented the changes to include model values in transition labels in TLC’s DOT output and opened a pull request for review. 

A big thank you to Markus Kuppe for the help and to Frederic Marand for supporting the idea! 

To view this discussion visit https://groups.google.com/d/msgid/tlaplus/D0FEA21A-D695-4614-92D4-207D44937F78%40lemmster.de.