Our great sponsors
- Onboard AI - Learn any GitHub repo in 59 seconds
- InfluxDB - Collect and Analyze Billions of Data Points in Real Time
- SaaSHub - Software Alternatives and Reviews
-
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 label 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.
-
coyote
Coyote is a library and tool for testing concurrent C# code and deterministically reproducing bugs.
Visualizations do help a lot when model checkers and concurrency schedule exploration tools like Coyote find bugs. Coyote include the ability to visualize the traces if you express your concurrency using actors (see https://microsoft.github.io/coyote/#concepts/actors/state-ma...)
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)
-
Onboard AI
Learn any GitHub repo in 59 seconds. Onboard AI learns any GitHub repo in minutes and lets you chat with it to locate functionality, understand different parts, and generate new code. Use it for free at www.getonboard.dev.
