Hi,
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?
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.