Forgot to mention earlier that “Pre-init” and “Init 0” are not actions. Init 0 is an initial state. Generally speaking a nondeterministic model can have multiple different init states, so Pre-init serves as a launch point from which to choose one. The actor system model uses a deterministic initial state, and I would be open to eliminating initial state nondeterminism as it does clutter the UI and adds some complexity to the library with relatively little offsetting value.

https://discord.com/channels/781357978652901386/781357978652901389/809987561874784307