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

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

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.