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