[tlaplus] Best current way of visualizing a state trace?

["J.D. Meadows" <tr1pl3.d3v@xxxxxxxxx>]

I'm using the Toolbox, which has a trace explorer sidebar that can be maximized, but the font is too large and some of the sequences are too long to be read comfortably.

I've found a slightly better way by manually converting the TLA+ error trace (exported from the Toolbox to the clipboard) to JSON, using just the replacement function of a text editor. That JSON can then be reviewed in VSCode, which can also format it. That way every field shows in a different line. I think I could craft a spec-specific python converter in a reasonable time. I hope the tools would have this functionality built in, as JSON is a more universal format, and better visualization tools could then be created by the community.

I'm aware thanks to his google group that JSON converting alternatives have already been created in the past, but they require installing some TLA modules and decorating the Spec formula. That is undesirable for me. I want the code unaltered, and the project portable so that other devs don't have to manually install additional TLA+ modules.

With the JSON approach however I lose the highlighting of the changing fields that the toolbox provides. Some trace visualizers exist in github but they seem outdated and I have no clue on how to use them. Are there any recent advances in visualization/animation? What is considered the best current approach?

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/9f3078aa-35c3-4247-9711-8bea48e79facn%40googlegroups.com.