Lightweight double-shrinking

[MaximilianAlgehed]

This PR introduces some super lightweight double-shrinking for action sequences. In order to reduce sequences of actions it's sometimes necessary to remove actions with unused variables in order for an action to change what variable it refers to. So in addition to shrinking actions we also try deleting actions that don't bind used variables.

[github-actions[bot]]

Unit Test Results

3 tests  ±0   3 :heavy_check_mark: ±0   0s :stopwatch: ±0s 1 suites ±0   0 :zzz: ±0  1 files   ±0   0 :x: ±0 

Results for commit 637bd70f. ± Comparison against base commit 7243e632.

[abailly-iohk]

Would you have an example of when/why this would be useful? And what the result would look like?

[MaximilianAlgehed]

Yes, I'm sorry for not including it from the beginning.

Imagine you have a model that uses a symbolic variable for a thread token:

data Action Model a where
  A :: Action Model (Var Token)
  B :: Var Token -> Action Model (Var Token)
  C :: Var Token -> Action Model ()

and the minimal counterexample to your property is something like:

do v <- action A
      action $ C v

or

do v <- action A
     y <- action $ B v
     action $ C y

or more generally, an A followed by a (possibly empty) sequence of Bs followed by a C is a counterexample.

However, the following is NOT a counterexample at all:

do v <- action A
      y <- action $ B v
      action $ C v

because we re-use the thread token from A that was invalidated by B.

Now, the minimal failing counterexample is always nice to get (obviously) but quickcheck can't necessarily shrink a bigger counterexample to the minimal counterexample without this PR. For example, if the first counterexample you get is e.g.

do v0 <- action A
      v1 <- action $ B v0
      v2 <- action $ B v1
      ...
      vn <- action $ B v{n-1}
      action $ C vn

quickcheck will try to shirnk it to e.g.

do v0 <- action A
      v1 <- action $ B v0
      v2 <- action $ B v1
      ...
      vn <- action $ B v{n-1}
      action $ C v{n-1}

However, this is not a counterexample because we need to also remove the action B v{n-1} for the property to fail.

With this PR however, we now get the shrinking we are looking for because B v{n-1} is precisely the kind of action (that doesn't produce a result we will use) that we can safely remove.

We could try to refine the extra shrinking we do here to not try to remove every action that doesn't produce a useful result (removing () typed actions isn't necessarily very interesting for example) but I think this is a good start.

Now, you could (and maybe you should) write your model in a way that this threading isn't so explicit. However, I would argue that we don't want to do a poor job on shrinking just because the model isn't written in the most elegant possible way. Furthermore, writing your model this way might be the best thing to do if you want to test e.g. mixing between two simultaneous "threads" where you want to ensure that mixing up arguments doesn't break anything etc. etc.

[abailly-iohk]

Thanks a lot for the detailed example, that's probably something we want to put somewhere in the haddocks :) So does this amount to a dependency analysis in the graph induced by the sequence of actions we are trying to shrink in order to shrink more by removing some nodes in the graph?

[MaximilianAlgehed]

Yes, something like this would be nice for the docs! I'll update the CHANGELOG with a small note about this too.

In a sense this is doing a "cheap" dependency analysis yes. However, it under-approximates the dependencies because it only looks at the explicit dependencies.