advancedtelematic / quickcheck-state-machine

Test monadic programs using state machine based models
Other
203 stars 25 forks source link

Fix parallel shrinking #315

Closed kderme closed 5 years ago

kderme commented 5 years ago

This pr fixes a bug related to parallel shrinking. It resolves https://github.com/advancedtelematic/quickcheck-state-machine/issues/302 and helps https://github.com/advancedtelematic/quickcheck-state-machine/pull/294 The current issue is caused because in shrinkAndValidateParallel the model is advanced by the commands which are not remmaped. Take a look at the following example: We have a valid MemoryReference command:

ParallelCommands
  { prefix =
      Commands
        { unCommands =
            [
             Command Create (Created (Reference (Symbolic (Var 0)))) [ Var 0 ]
             Command Create (Created (Reference (Symbolic (Var 1)))) [ Var 1 ]
            ]
        }
  , suffixes =
      [  Pair
          { proj1 =
              Commands
                { unCommands =
                    [ ]
                }
          , proj2 =
              Commands
                { unCommands =
                    [ Command (Increment (Reference (Symbolic (Var 1)))) Incremented []
                    ]
                }
          }
      , Pair
          { proj1 = Commands { unCommands = [] }
          , proj2 =
              Commands
                { unCommands =
                    [ Command (Read (Reference (Symbolic (Var 1)))) (ReadValue 1) [] ]
                }
          }
      ]
  }

First the suffix is shrunk, so this command appears

ParallelCommands
  { prefix =
      Commands
        { unCommands =
            [
             Command Create (Created (Reference (Symbolic (Var 1)))) [ Var 1 ]
            ]
        }
  , suffixes =
      [  Pair
          { proj1 =
              Commands
                { unCommands =
                    [ ]
                }
          , proj2 =
              Commands
                { unCommands =
                    [ Command (Increment (Reference (Symbolic (Var 1)))) Incremented []
                    ]
                }
          }
      , Pair
          { proj1 = Commands { unCommands = [] }
          , proj2 =
              Commands
                { unCommands =
                    [ Command (Read (Reference (Symbolic (Var 1)))) (ReadValue 1) [] ]
                }
          }
      ]
  }

For me this looks like a valid program so shrinkAndValidateParallel sm DontShrink cmd should actually return a list with a single element. shrinkAndValidate for the preffix will return an environment with a mapping (1->0). Then shrinkAndValidate for proj2 of the first suffix will succeed, because the commands are used remmaped. However combineEnv uses the commands not remmaped, so the increment will use Var 1, which will throw the exception. I think just changing combineEnv to use the commands remmaped, as returned from shrinkAndValidate, fixes the problem.

Note that the last suffix, with Read, is the one which actually forces the evaluation and throws the exception. Reducing the last command makes it realy hard to spot the problem. I actually think this failure appears many times, but most of the times the exception is not thrown because fo laziness.

I also tried to improve a bit readability (using do notation for list manipulation, which I find cleaner) and make these commands easier to use from ghci.

Another note, this increases shrink candidates, so run time of shrinking is also expected to increase.