Feature request: State transition graph in JSON format

[smheidrich]

Feature request

Great project, thanks for writing and publishing it!

One thing I'd find useful is if the state transition graph which FizzBee currently outputs in GraphViz dot format could also be output as JSON, especially if the state inside each node could be represented as JSON as well. That would make it easier to process, apply custom filtering and formatting etc. as one desires.

Since the GraphViz dot file is produced unconditionally (unless the graph is too large) and I don't expect JSON to be more expensive to produce, I guess it would be fine if it was unconditional as well. But I don't think anyone would complain if it had to be enabled with a CLI switch or config option instead.

Additional context

Just to show that this is a common feature request for model checkers: People have been requesting the same feature in TLA+'s tooling for a while (tlaplus/tlaplus#639, tlaplus/tlaplus#1073) and the issues link to some examples of what people would do with it.

[jp-fizzbee]

The graph is being persisted, but as a binary proto file.
Anytime ./fizz dir_with_fizz_file/finename.fizz, there will an dir_with_fizz_file/out/run_[YYYY-MM-DD_HH-mm-ss]/
The proto is defined at https://github.com/fizzbee-io/fizzbee/blob/main/proto/graph.proto

[jp-fizzbee]

Just curious what you want to use it for?

[smheidrich]

Thanks for pointing me towards the protobuf files! That's definitely better than just the .dot graph, but I still see two problems:

1. If a run failed, e.g. due to encountering a deadlock, the output directory will only contain nodes_error.pb and adjacency_lists_error.pb files which (as far as I can tell) contain only a single trace leading to the error. Meanwhile, graph.dot contains many more nodes - not necessarily the whole graph because the error does cut state exploration short, but still more than just a trace. So IMO in order for the protobuf files to be a proper alternative to graph.dot, there should be protobuf files containing the same nodes as the latter.
2. Extracting the data from the protobuf files needs quite a lot of tooling to be installed on the user's side and even then isn't very convenient (cf. how I ended up doing it below). Of course someone could make a third party tool to make this easier, but since FizzBee already has the protobuf definitions anyway, it would probably be easiest for it to just provide JSON export functionality itself.

Just curious what you want to use it for?

Very generally making graphs easier to look at as the situation demands. For example:

• Sometimes I have unimportant variables which are distracting in the graph visualization. With the state represented as JSON, I could easily filter them out. Conversely, there may be important variables I want to highlight.
• Exploring different ways of visualizing variables that make up the state: I did some experiments on TLA+ graphs here with not very great results, but with some layout improvements this could probably make graphs easier to read.
• Simplifying graphs resulting from specs that use the any x in y: feature: The .dot graph exported by FizzBee contains a lot of "intermediate" states that represent selecting an x, even when the actions are atomic. At least for me, the graph would be easier to read if these were reduced to just arrows between the "actual" states. If there was a JSON export, it would be fairly easy to get rid of them myself.

Of course you could implement all of these in FizzBee's own GraphViz .dot export functionality, but you'll never cover the entirety of what people may want to do. So I think this is a perfect situation to apply the UNIX philosophy of doing one thing well, while outputting the result in a sufficiently commonplace format that other tools can do the same.

---

P. S. Just for the benefit of anyone else who comes across this issue, here is how I converted the data inside the protobuf files (generated by FizzBee @ aad1bb7) to JSON:

After a successful fizz run, you'll have files nodes_000000_of_000000.pb and adjacency_lists_000000_of_000000.pb in your output directory. As you can guess, the former contains the nodes (states) of the graph and the latter the transitions between them. To extract both:

1. Install ProtobufJson. We'll be using its ProtoToJson binary to turn protobuf data into JSON.
2. Extracting the transitions/links between nodes is easy: ProtoToJson -I /PATH/TO/FIZZBEE/REPO/proto/ Links < /PATH/TO/OUTPUT/DIR/adjacency_lists_000000_of_000000.pb. In the resulting JSON, the numbers in src and dest refer to the 0-indexed positions in the list of nodes we'll obtain below, and if src is not given, it refers to position 0.
3. The nodes file contains JSON at the protobuf level which ProtoToJson will turn into encoded-JSON-inside-strings of the larger JSON structure, so to turn that into normal-JSON-all-the-way-down, we'll need a bit of postprocessing, which can be done using jq: ProtoToJson -I /PATH/TO/FIZZBEE/REPO/proto/ Nodes < /PATH/TO/OUTPUT/DIR/nodes_000000_of_000000.pb | jq '[ .json[] | fromjson ]