TLA+ Graph Explorer | Hacker News Reader

TLA+ Graph Explorer

github.com

103 pointshwayne6 comments

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)

https://en.wikipedia.org/wiki/TLA%2B

Your comment is very helpful, but it would have been perfect if it included the first paragraph.

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

Thank You for that!

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.

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?

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.

Reply on news.ycombinator.com