Re: [tlaplus] Enhancing state transition information in TLC’s DOT output

Best regards,

Ana Catarina Ribeiro

PhD student - Computer Science @ NOVA FCT

On 18 Feb 2025, at 12:21, Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx> wrote:

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

On Feb 18, 2025, at 11:47 AM, 'Ana Ribeiro' via tlaplus <tlaplus@xxxxxxxxxxxxxxxx> wrote:

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

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

--
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 visit https://groups.google.com/d/msgid/tlaplus/D0FEA21A-D695-4614-92D4-207D44937F78%40lemmster.de.