Construct does not allow parallel execution. It’s a deterministic simulation testing framework, so parallelism is a no-go there. Only one process is allowed to execute at a time.
I think the difference in approach here can be summarized as “breadth-first vs depth-first”, but maybe I am not fully understanding.
Either way, I see the similarities and I’ll keep your approach in mind. Hobbes probably has too large a state space to explore exhaustively this way (not computationally tractable), but maybe smaller parts of it could be exhaustively checked for bugs.
Do you see parallels between your approach and formal methods (e.g. TLA+)?
