This allows results to be naturally reported as lazy trees, rather
than as lists representing a tree traversal. This in turn means
that the actual bound can be moved outwards to the testing code, and
not used at all in the runner. Trees let us do nice things with
shrinking and short-circuiting, if we make the (fairly reasonable)
assumption that the children of a buggy result will exhibit the same
bug.
Storing results as trees does complicate the predicate helper
functions somewhat, but I think the clarity gained in the actual
SCT code is well worth it.
Shrinking attempts to find a "maximally simple" trace which
exhibits the same bug as the original. Typically, this means that
the results are equal. Shrinking is implemented in terms of
recursively trying to find the simplest variant of the original
trace, where simplest in particular means:
1. A trace with fewer pre-emptions is simpler.
2. A trace with fewer non-pre-emptive context switches is simpler.
3. A trace lexicographically smaller is simpler.
These three criteria are applied in that order in order to determine
which the simplest trace out of a collection is.
For test output, there is a final set of simplification done at the end.
Shrinking attempts to reduce individual traces to their simplest variant,
which can result in multiple test failures having the same shrunk trace.
Thus, the test runner then filters out duplicate failures by only keeping
the simplest trace for a given result.
