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