[darioush]

the core idea is to model the state and valid state transitions formally (which may be more directly applicable to the audio driver), so they can be enumerated exhaustively up to a certain bound.

it may be that a bug only shows when hundreds of transitions are performed (like an overflow or bug due to large data), but that's more stress testing. many bugs have repros involving a few state transitions.

relational algebra is a useful tool in my opinion because much of programming involves adding/removing things from sets or testing for their membership in a set. also relations are powerful as they can express recursive ideas like which widgets are contained within others (from the GUI example).

relations also allow defining invariants at a high level which must be true at any state. (eg, there should be no state like: audio_buffer_is_empty and audio_playing)

additionally we have languages such as SQL or for example https://alloytools.org/applications.html that can help programmers specify this in a familiar way.

[DowsingSpoon]

That is fascinating. Thank you!

Is it necessary to be able to exhaustively enumerate states? I remember a project I worked on some years ago which had me sketching out a statechart for a system which was not structured as an explicit FSM. The end result was surprisingly complex. I imagine some systems might even have an unbounded number of “states.”

I’ll definitely read more about Alloy too.