shrinking optimizations

[kderme]

I'm working on a pr which tries to capture information from the execution of a list of Commands, in order to make shrinking faster. Note that QuickCheck does not support this very well, so it is a bit experimental. It is based on 2 ideas:

• if the execution failed on the n-th command of the list, we should first try to shrink the prefix up to the nth command.
• if the execution failed on the n-th command of the list, there is no reason to test a prefix smaller than n.

Using these ideas the shrink list can be pruned. I have implemented the first part for the non-monadic case and I think the second is also easy to implement. However implementing the monadic case seems tricky.

For some examples which support this idea: Say we have a list of commands [1..20] and execution fails on the 8th command. The shrinker should try to shrink [1..8]. Also shrinkListS' [1,2,3,4,5,6,7,8] returns

[Shrunk {wasShrunk = True, shrunk = []},Shrunk {wasShrunk = True, shrunk = [5,6,7,8]},Shrunk
 {wasShrunk = True, shrunk = [1,2,3,4]},Shrunk {wasShrunk = True, shrunk = 
[3,4,5,6,7,8]},Shrunk {wasShrunk = True, shrunk = [1,2,5,6,7,8]},Shrunk {wasShrunk = True, 
shrunk = [1,2,3,4,7,8]},Shrunk {wasShrunk = True, shrunk = [1,2,3,4,5,6]},Shrunk {wasShrunk = 
True, shrunk = [2,3,4,5,6,7,8]},Shrunk {wasShrunk = True, shrunk = [1,3,4,5,6,7,8]},Shrunk 
{wasShrunk = True, shrunk = [1,2,4,5,6,7,8]},Shrunk {wasShrunk = True, shrunk = 
[1,2,3,5,6,7,8]},Shrunk {wasShrunk = True, shrunk = [1,2,3,4,6,7,8]},Shrunk {wasShrunk = True, 
shrunk = [1,2,3,4,5,7,8]},Shrunk {wasShrunk = True, shrunk = [1,2,3,4,5,6,8]},Shrunk {wasShrunk 
= True, shrunk = [1,2,3,4,5,6,7]},Shrunk {wasShrunk = False, shrunk = [1,2,3,4,5,6,7,8]}]

All prefixes, like [1,2,3,4], [1,2,3,4,5,6], [1,2,3,4,5,6,7] can be safely pruned.

Thoughts on this?

[stevana]

if the execution failed on the n-th command of the list, there is no reason to test a prefix smaller than n.

You mean greater than n?

However implementing the monadic case seems tricky.

What do you mean by the monadic case here?

Thoughts on this?

I think these are good ideas!

What's your opinion on always keeping the n-th command, so that we don't trigger other bugs while shrinking?

[kderme]

You mean greater than n?

No smaller. If the command failed on the n-th comman, this means it hasn't failed up to the (n-1)th command, so there is no reason to test these cases.

What do you mean by the monadic case here?

I mean using Test.QuickCheck.Monadic. The type of monadic monadic :: (Testable a, Monad m) => (m Property -> Property) -> PropertyM m a -> Property does not allow to extract information (like the preffix that failed) from the ProperyM m a in order to pass it to the shrinker.

[kderme]

What's your opinion on always keeping the n-th command, so that we don't trigger other bugs while shrinking?

By always trying to keep n-th command we may miss smaller counter examples which don't contain it. Maybe we can keep shrinked elements which contain the n-th command first on the shrink list.

[kderme]

I finally managed to make this work (https://github.com/advancedtelematic/quickcheck-state-machine/tree/quick-shrink-monadic) and the results seem good. This is sequential memory referece with a Logic bug (verbose execution):

Failed:   
Commands
  { unCommands =
      [ Command Create (Created (Reference (Symbolic (Var 0)))) [ Var 0 ]
      , Command (Read (Reference (Symbolic (Var 0)))) (ReadValue 0) []
      , Command (Read (Reference (Symbolic (Var 0)))) (ReadValue 0) []
      , Command (Write (Reference (Symbolic (Var 0))) 7) Written []
      , Command (Read (Reference (Symbolic (Var 0)))) (ReadValue 7) []
      , Command (Increment (Reference (Symbolic (Var 0)))) Incremented []
      , Command (Increment (Reference (Symbolic (Var 0)))) Incremented []
      , Command (Increment (Reference (Symbolic (Var 0)))) Incremented []
      , Command (Write (Reference (Symbolic (Var 0))) (-75)) Written []
      , Command (Write (Reference (Symbolic (Var 0))) (-36)) Written []
      , Command
          (Read (Reference (Symbolic (Var 0)))) (ReadValue (-36)) []
      , Command
          (Read (Reference (Symbolic (Var 0)))) (ReadValue (-36)) []
      , Command Create (Created (Reference (Symbolic (Var 1)))) [ Var 1 ]
      , Command (Increment (Reference (Symbolic (Var 0)))) Incremented []
      , Command (Increment (Reference (Symbolic (Var 0)))) Incremented []
      , Command (Increment (Reference (Symbolic (Var 0)))) Incremented []
      , Command (Increment (Reference (Symbolic (Var 1)))) Incremented []
      , Command (Read (Reference (Symbolic (Var 1)))) (ReadValue 1) []
      , Command (Read (Reference (Symbolic (Var 1)))) (ReadValue 1) []
      , Command (Write (Reference (Symbolic (Var 1))) (-84)) Written []
      , Command (Write (Reference (Symbolic (Var 0))) (-94)) Written []
      , Command
          (Read (Reference (Symbolic (Var 0)))) (ReadValue (-94)) []
      ]
  }
PostconditionFailed "AnnotateC \"Read\" (PredicateC (8 :/= 7))" /= Ok

Passed:                                                  
Commands { unCommands = [] }
Ok == Ok

Passed:                                                                  
Commands
  { unCommands =
      [ Command Create (Created (Reference (Symbolic (Var 0)))) [ Var 0 ]
      , Command (Read (Reference (Symbolic (Var 0)))) (ReadValue 0) []
      , Command (Read (Reference (Symbolic (Var 0)))) (ReadValue 0) []
      ]
  }
Ok == Ok

Failed:                                                                  
Commands
  { unCommands =
      [ Command Create (Created (Reference (Symbolic (Var 0)))) [ Var 0 ]
      , Command (Read (Reference (Symbolic (Var 0)))) (ReadValue 0) []
      , Command (Write (Reference (Symbolic (Var 0))) 7) Written []
      , Command (Read (Reference (Symbolic (Var 0)))) (ReadValue 7) []
      ]
  }
PostconditionFailed "AnnotateC \"Read\" (PredicateC (8 :/= 7))" /= Ok

The execution fails on the 5th command and it quickly shrinks down to this prefix.

[kderme]

I opened an issue at QuickCheck https://github.com/nick8325/quickcheck/issues/263