Ability to export TLC state graph #639
Comments
|
On the command line, this could be made available as another sub-parameter of Who is going to finish and create a PR? |
|
Great, @will62794! Are you working on this? I have created a state writer to output a Transit file (EDN on Json) at https://github.com/pfeodrippe/recife/blob/dfs/src/recife/core.clj#L788, it would indeed help a lot with scripts and tooling (I'm driving implementation code from it, it's awesome!), I'm just skeptical about outputting JSON as it does not retain some types (like sets). Do you have some preferred idea about the structure of the generated file? Want to see if it matches mine and if I'm missing something. |
|
@pfeodrippe nodes: {
0: "/\ a = 1 /\ b = 1",
1: "/\ a = 2 /\ b = 1",
2: "/\ a = 1 /\ b = 2",
3: "/\ a = 2 /\ b = 2"
},
edges: {
"IncreaseOne": [ (0, 1), (0, 2) ],
"IncreaseBoth": [ (0, 3) ]
}``` |
|
What is missing from https://graphviz.org/docs/outputs/json/ that converting TLC's dot output to json is not feasible? |
|
My argument would be for simplicity. The closest generated JSON format I had in mind when converting from dot was I tested
Including line breaks, my suggestion would bring this value down to: In my previous example: 4 nodes, 3 actions gave a 2 + 4 + 2 + 4 + 3 = 15 line file. nodes: {
0: "/\ a = 1 /\ b = 1",
1: "/\ a = 2 /\ b = 1",
2: "/\ a = 1 /\ b = 2",
3: "/\ a = 2 /\ b = 2"
},
edges: {
"IncreaseOne": [
(0, 1),
(0, 2)
],
"IncreaseBoth": [
(0, 3)
]
}Pros:
Cons:
Maybe other people have better suggestions? |
|
When I added dot support, I didn't bother to remove redundant nodes and edges assuming the overhead doesn't matter for small graphs that can reasonably be rendered. If the file size is an issue, I'd suggest first improving the current implementation. Anyway, it shouldn't be difficult to also add a json printer given that a json lib is already part of TLC, and state graphing amounts to implementing one or two interfaces. |
|
In case anyone else comes across this issue and prefers a quick workaround over recompiling with the patch linked above, here is a small Python script to transform the output of |
Uh oh!
There was an error while loading. Please reload this page.
In some cases it would be helpful to have the ability to export the state graph generated by TLC in an easily parseable format (e.g. JSON) for use by other tools, scripts, applications, etc. This could presumably be built as a straightforward implementation of the StateWriter interface. I have implemented a minimal prototype of this, using the previously developed functionality from the Json community module.
The text was updated successfully, but these errors were encountered: