4 ms·
This is great, and replicates a feature I really like about PRISM: the ability to step through your model's transitions to see that they do what you think they
by ahelwer 6y ago
This is great, and replicates a feature I really like about PRISM: the ability to step through your model's transitions to see that they do what you think they do (and are enabled when you think they are). I notice in the screenshots the next states are labeled Child 1-N, wonder whether there will be an update to map those children to the names of the actions taken in the spec (although that feature would probably require interpreting the spec itself instead of just the dotfile).
We also finally have a TLA+ state visualizer! One of the really neat ideas included with Runway (RIP, F in the chat, etc.). You write the visualizations in D3 I guess?
- afonsonf 6y agoHi, > wonder whether there will be an update to map those children to the names of the actions taken in the spec This can be done by, for example, adding a variable to the spec with the name of the transition, lets say a variable named label. Then in the tool you can parse the state string (variable value in function updateChilds, https://github.com/afonsonf/tlaplus-graph-explorer/blob/main/src/js/utils.js#L74 https://github.com/afonsonf/tlaplus-graph-explorer/blob/main...), and then use the label when creating the radio button. The label can be obtained from the variable value in updateChilds with something like: label = parseVars(value).get("label"). > You write the visualizations in D3 I guess? The visualization I think can be written with any javascript library, at least I tried to make it able to do so. In the second example I wrote the visualization with svg.js.