It also allows you to implement your own "logger" through which you can emit enough information to construct some cool visualizations. I had a lot of fun working on visualizing an implementation of Paxos using Coyote (then P#) (screenshot at https://ibb.co/TTk2hYb)
> TLA+ is a formal specification language developed by Leslie Lamport. It is used to design, model, document, and verify programs, especially concurrent systems and distributed systems. TLA+ has been described as exhaustively-testable pseudocode, and its use likened to drawing blueprints for software systems; TLA is an acronym for Temporal Logic of Actions.
I was puzzling over, trying to find a meaning for TLA.
In the 1980s I learned that TLA meant "Three Letter Acronyms". That made it easier to complain about the use of TLAs that were not explained. A TLA becomes a form of jargon that those not "on the inside" don't get.
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?
> 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...), 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?