Possible Developer Experience Improvements

[ANorwell]

Here's a grab bag of feedback on developer experience after a few days use, take from this what you will:

• A documentation page on developer experience and tricks when building a non-trivial model might be useful. I think there are some non-obvious things, e.g. writing invariants that are actually tests to debug the model. Some tips about keeping state space small might be useful.
• Debugging the situation where all correctness invariants are passing, but your expectation is that they should be failing, is difficult. I wanted to see some specific traces e.g. in the HTML view, but I had no way I knew of to do that. Once the state space is large enough, the graph vizs of all states were unwieldy or just not generated.
  • Potentially non-exhaustive state space eval would be pretty useful here? e.g. provide the HTML view of 5-10 traces that I can look through individually
• Debugging liveness invariants seems difficult. I was desiring two things here:
  • A easy way to tell which invariants were true and false for each state (e.g. on the HTML page). (I think the graph was coloring success states green, but I could hardly see that, and found the HTML page more useful than the graph.)
  • and possibly an easier way to see why an invariant was false. Especially for global conditions, e.g. one item in set A is missing from set B -- at invariant eval time, the invariant function knows why there is a failure, but I didn't have a way that I know of to annotate the state with the failure reason so that I could reason about it easily afterwards.
• The documentation is very playground-first, but I was not using the playground. It's not clear how to e.g. use the explorer locally.
• The graph visualization started to get unwieldy for me pretty quickly. The amount of state in each node was so large that it was difficult to see the state that was important. The JSON diff HTML view was super helpful here. I also found myself doing things like prefixing some fields with z_ so that they sorted to the end in the graph view, since I didn't care about them.
• It would be nice if the documentation was in github, or otherwise globally searchable. I want to ctrl-F the entire docs, ask my LLM questions about it, etc.
• Dedicated doc on func would be useful. e.g. apparently (I think?) an atomic func that calls a (non-atomic) func is not atomic, which isn't obvious
• I had several fair any select an ID to act on type statements in my model, and it was kind of annoying that these statements were granularly visible in the state space / HTML. I'm not sure if I was just doing it wrong somehow, but I felt like what I really wanted was the ability to collapse "select Action A to perform + use one or more fair any statements to initialize how the action will be performed", and that would just be one state transition node. e.g. I want the transition to show Dequeue(id=5) rather than Dequeue() -> id = 5.

Thanks for making fizzbee, it has a lot of promise!

[jp-fizzbee]

Potentially non-exhaustive state space eval would be pretty useful here? e.g. provide the HTML view of 5-10 traces that I can look through individually

At present, you can generate one trace at a time by running it in the simulation mode.
./fizz --simulation --max_runs 1 /path/to/dir/spec_file.fizz
At present, it only generates the graph.dot, you can generate

dot -Tsvg /path/to/dir/out/latest/graph.dot -o graph.svg && open graph.svg

I'll generate the full html trace like when there is an error. Filed a separate issue to track this #190

---

A easy way to tell which invariants were true and false for each state (e.g. on the HTML page).
Filed a separate issue #191 to track this

---

and possibly an easier way to see why an invariant was false.
For safety assertions, it might be easier to just add a print statement conditionally. Since the invariant would fail, the last print statement would have the info. Unfortunately, the print statements are not tied to the transitions, they are just printed as they are executed.
#192 #193

---

how to e.g. use the explorer locally.
The instructions are in this pull request #158

---

I had several fair any select an ID to act on type statements in my model, and it was kind of annoying that these statements were granularly visible in the state space / HTML.
Agreed. This has been an issue for a while. In majority of the cases, the any statements are within the first few steps in the action, so it is obviously less useful and more of a clutter. There are times it becomes useful - for example,

1. the any statement happens deep within the execution of certain steps.
2. the any statement is executed within a loop.
3. any statement after yield points. For actions that are not atomic, where there can be multiple thread interleavings, this will get more complicated.
4. for probability/performance modeling as having this is required to set the correct probability.

That said, for the error graph or at least in the HTML, I can easily hide it with a checkbox. Correct me if I am wrong, there would be two columns for the diff, one of them will show the diff of the json from the previous yield point. Can you confirm if it is sufficient?

[ANorwell]

Can you confirm if it is sufficient?

I was using the previous yield point diff and it was a good workaround. But I was mostly completely ignoring the fair any rows/nodes. Optional or collapsible/expandable sounds useful.