Implement a proper interface for stateful fuzzing

[Seelengrab]

Currently, the way to do stateful fuzzing is very ad-hoc and relies on good problem modeling skills to generate good sequences of operations.

This feature should:

• Manage the state required for the fuzzing automatically (e.g. by grouping them all into a mutable struct which is modified by the various operations one can do)
• Allow the specification of transition rules from one state to the next, allowing (almost) arbitrary modifications to the declared state.
• Allow specifying preconditions on a per-rule basis, so that these are checked before any given transition is attempted.
• Allow specifying additional invariants/postconditions on the state that must be upheld after every (or perhaps even just some?) operation.
• Provide good printing of the ensuing result, clearly showing the sequence of actions taken to find the minimal counterexample.
• Ideally, this would also have a configuration option to allow operations to run in parallel, which would allow users to fuzz their datastructures for race conditions (if they violate an invariant in parallel fuzzing mode, they have a race condition).
  • This is quite a bit more tricky than it may seem at first, since shrinking may rely on very precise scheduling decisions of the Julia scheduler. An initial implementation can either omit this point entirely or just abort completely and report the found stream of (task, action_taken, time) in some form.