diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,3 +1,19 @@
+#### 0.6.0 (2019-1-15)
+
+  This is a breaking release. See mentioned PRs for how to upgrade your code,
+  and feel free to open an issue if anything isn't clear.
+
+  * Generalise shrinking so that it might depend on the model (PR #263);
+
+  * Drop support for GHC 8.0.* or older, by requiring base >= 4.10 (PR #267). If
+    you need support for older GHC versions, open a ticket;
+
+  * Use Stack resolver lts-13 as default (PR #261);
+
+  * Generalise the `GConName` type class to make it possible to use it for
+    commands that cannot have `Generic1` instances. Also rename the type class
+    to `CommandNames` (PR #259).
+
 #### 0.5.0 (2019-1-4)
 
   The first and third item in the below list might break things, have a look at
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -151,9 +151,9 @@
   , (4, Increment <$> elements (domain model))
   ]
 
-shrinker :: Command Symbolic -> [Command Symbolic]
-shrinker (Write ref i) = [ Write ref i' | i' <- shrink i ]
-shrinker _             = []
+shrinker :: Model Symbolic -> Command Symbolic -> [Command Symbolic]
+shrinker _ (Write ref i) = [ Write ref i' | i' <- shrink i ]
+shrinker _ _             = []
 ```
 
 To stop the generation of new commands, e.g., when the model has reached a
diff --git a/quickcheck-state-machine.cabal b/quickcheck-state-machine.cabal
--- a/quickcheck-state-machine.cabal
+++ b/quickcheck-state-machine.cabal
@@ -1,126 +1,118 @@
-name:                quickcheck-state-machine
-version:             0.5.0
-synopsis:            Test monadic programs using state machine based models
-description:         See README at <https://github.com/advancedtelematic/quickcheck-state-machine#readme>
-homepage:            https://github.com/advancedtelematic/quickcheck-state-machine#readme
-license:             BSD3
-license-file:        LICENSE
-author:              Stevan Andjelkovic
-maintainer:          Stevan Andjelkovic <stevan.andjelkovic@here.com>
-copyright:           Copyright (C) 2017-2018, ATS Advanced Telematic Systems GmbH;
-                                   2018-2019, HERE Europe B.V.
-category:            Testing
-build-type:          Simple
-extra-source-files:  README.md
-                   , CHANGELOG.md
-                   , CONTRIBUTING.md
-cabal-version:       >=1.10
-tested-with:         GHC == 8.2.2, GHC == 8.4.3
+cabal-version: >=1.10
+name: quickcheck-state-machine
+version: 0.6.0
+license: BSD3
+license-file: LICENSE
+copyright: Copyright (C) 2017-2018, ATS Advanced Telematic Systems GmbH;
+           2018-2019, HERE Europe B.V.
+maintainer: Stevan Andjelkovic <stevan.andjelkovic@here.com>
+author: Stevan Andjelkovic
+tested-with: ghc ==8.2.2 ghc ==8.4.3 ghc ==8.6.3
+homepage: https://github.com/advancedtelematic/quickcheck-state-machine#readme
+synopsis: Test monadic programs using state machine based models
+description:
+    See README at <https://github.com/advancedtelematic/quickcheck-state-machine#readme>
+category: Testing
+build-type: Simple
+extra-source-files:
+    README.md
+    CHANGELOG.md
+    CONTRIBUTING.md
 
+source-repository head
+    type: git
+    location: https://github.com/advancedtelematic/quickcheck-state-machine
+
 library
-  hs-source-dirs:      src
-  ghc-options:
-              -Weverything
-              -Wno-missing-exported-signatures
-              -Wno-missing-import-lists
-              -Wno-missed-specialisations
-              -Wno-all-missed-specialisations
-              -Wno-unsafe
-              -Wno-safe
-              -Wno-missing-local-signatures
-              -Wno-monomorphism-restriction
-  exposed-modules:     Test.StateMachine
-                     , Test.StateMachine.BoxDrawer
-                     , Test.StateMachine.ConstructorName
-                     , Test.StateMachine.Logic
-                     , Test.StateMachine.Parallel
-                     , Test.StateMachine.Sequential
-                     , Test.StateMachine.Types
-                     , Test.StateMachine.Types.Environment
-                     , Test.StateMachine.Types.GenSym
-                     , Test.StateMachine.Types.History
-                     , Test.StateMachine.Types.Rank2
-                     , Test.StateMachine.Types.References
-                     , Test.StateMachine.Utils
-                     , Test.StateMachine.Z
-  other-modules:
-      Paths_quickcheck_state_machine
-  build-depends:
+    exposed-modules:
+        Test.StateMachine
+        Test.StateMachine.BoxDrawer
+        Test.StateMachine.ConstructorName
+        Test.StateMachine.Logic
+        Test.StateMachine.Parallel
+        Test.StateMachine.Sequential
+        Test.StateMachine.Types
+        Test.StateMachine.Types.Environment
+        Test.StateMachine.Types.GenSym
+        Test.StateMachine.Types.History
+        Test.StateMachine.Types.Rank2
+        Test.StateMachine.Types.References
+        Test.StateMachine.Utils
+        Test.StateMachine.Z
+    hs-source-dirs: src
+    other-modules:
+        Paths_quickcheck_state_machine
+    default-language: Haskell2010
+    ghc-options: -Weverything -Wno-missing-exported-signatures
+                 -Wno-missing-import-lists -Wno-missed-specialisations
+                 -Wno-all-missed-specialisations -Wno-unsafe -Wno-safe
+                 -Wno-missing-local-signatures -Wno-monomorphism-restriction
+    build-depends:
         ansi-wl-pprint >=0.6.7.3,
-        base >=4.9 && <5,
+        base >=4.10 && <5,
         containers >=0.5.7.1,
         exceptions >=0.8.3,
         matrix >=0.3.5.0,
         mtl >=2.2.1,
-        pretty-show,
+        pretty-show >=1.9.5,
         QuickCheck >=2.9.2,
-        split >=0.2.3.3,
         tree-diff >=0.0.2,
         vector >=0.12.0.1,
         unliftio >=0.2.7.0
-  default-language:    Haskell2010
 
 test-suite quickcheck-state-machine-test
-  type:                exitcode-stdio-1.0
-  hs-source-dirs:      test
-  main-is:             Spec.hs
-  build-depends:       base,
-                       bytestring,
-                       containers,
-                       directory,
-                       doctest,
-                       filelock,
-                       filepath,
-                       http-client,
-                       matrix >=0.3.5.0,
-                       monad-logger,
-                       mtl,
-                       network,
-                       persistent,
-                       persistent-postgresql,
-                       persistent-template,
-                       process,
-                       QuickCheck >=2.9.2,
-                       quickcheck-instances,
-                       quickcheck-state-machine,
-                       random,
-                       resourcet,
-                       servant,
-                       servant-client,
-                       servant-server,
-                       strict,
-                       string-conversions,
-                       tasty,
-                       tasty-hunit,
-                       tasty-quickcheck,
-                       text,
-                       tree-diff,
-                       vector >=0.12.0.1,
-                       wai,
-                       warp,
-                       unliftio
-
-  other-modules:       CircularBuffer,
-                       CrudWebserverDb,
-                       DieHard,
-                       Echo,
-                       ErrorEncountered,
-                       MemoryReference,
-                       TicketDispenser
-
-  ghc-options:
-              -threaded -rtsopts -with-rtsopts=-N
-              -Weverything
-              -Wno-missing-exported-signatures
-              -Wno-missing-import-lists
-              -Wno-missed-specialisations
-              -Wno-all-missed-specialisations
-              -Wno-unsafe
-              -Wno-safe
-              -Wno-missing-local-signatures
-              -Wno-monomorphism-restriction
-  default-language:    Haskell2010
-
-source-repository head
-  type:     git
-  location: https://github.com/advancedtelematic/quickcheck-state-machine
+    type: exitcode-stdio-1.0
+    main-is: Spec.hs
+    hs-source-dirs: test
+    other-modules:
+        CircularBuffer
+        CrudWebserverDb
+        DieHard
+        Echo
+        ErrorEncountered
+        MemoryReference
+        TicketDispenser
+        ShrinkingProps
+    default-language: Haskell2010
+    ghc-options: -threaded -rtsopts -with-rtsopts=-N
+                 -fno-ignore-asserts -Weverything -Wno-missing-exported-signatures
+                 -Wno-missing-import-lists -Wno-missed-specialisations
+                 -Wno-all-missed-specialisations -Wno-unsafe -Wno-safe
+                 -Wno-missing-local-signatures -Wno-monomorphism-restriction
+    build-depends:
+        base >=4.12.0.0,
+        bytestring >=0.10.8.2,
+        containers >=0.6.0.1,
+        directory >=1.3.3.0,
+        doctest >=0.16.0.1,
+        filelock >=0.1.1.2,
+        filepath >=1.4.2.1,
+        http-client >=0.5.14,
+        matrix >=0.3.5.0,
+        monad-logger >=0.3.30,
+        mtl >=2.2.2,
+        network >=2.8.0.0,
+        persistent >=2.9.0,
+        persistent-postgresql >=2.9.0,
+        persistent-template >=2.5.4,
+        pretty-show >=1.9.5,
+        process >=1.6.3.0,
+        QuickCheck >=2.9.2,
+        quickcheck-instances >=0.3.19,
+        quickcheck-state-machine -any,
+        random >=1.1,
+        resourcet >=1.2.2,
+        servant >=0.15,
+        servant-client >=0.15,
+        servant-server >=0.15,
+        strict >=0.3.2,
+        string-conversions >=0.4.0.1,
+        tasty >=1.2,
+        tasty-hunit >=0.10.0.1,
+        tasty-quickcheck >=0.10,
+        text >=1.2.3.1,
+        tree-diff >=0.0.2,
+        vector >=0.12.0.1,
+        wai >=3.2.1.2,
+        warp >=3.2.25,
+        unliftio >=0.2.10
diff --git a/src/Test/StateMachine.hs b/src/Test/StateMachine.hs
--- a/src/Test/StateMachine.hs
+++ b/src/Test/StateMachine.hs
@@ -42,6 +42,7 @@
   , Reason(..)
   , GenSym
   , genSym
+  , CommandNames(..)
 
   , module Test.StateMachine.Logic
 
@@ -49,6 +50,7 @@
 
 import           Prelude
                    ()
+import           Test.StateMachine.ConstructorName
 import           Test.StateMachine.Logic
 import           Test.StateMachine.Parallel
 import           Test.StateMachine.Sequential
diff --git a/src/Test/StateMachine/ConstructorName.hs b/src/Test/StateMachine/ConstructorName.hs
--- a/src/Test/StateMachine/ConstructorName.hs
+++ b/src/Test/StateMachine/ConstructorName.hs
@@ -1,3 +1,5 @@
+{-# LANGUAGE DataKinds            #-}
+{-# LANGUAGE DefaultSignatures    #-}
 {-# LANGUAGE FlexibleContexts     #-}
 {-# LANGUAGE FlexibleInstances    #-}
 {-# LANGUAGE PolyKinds            #-}
@@ -7,15 +9,13 @@
 {-# LANGUAGE UndecidableInstances #-}
 
 module Test.StateMachine.ConstructorName
-  ( GConName
-  , gconName
-  , gconNames
-  , GConName1
-  , gconName1
-  , gconNames1
+  ( CommandNames(..)
+  , commandName
   )
   where
 
+import           Data.Kind
+                   (Type)
 import           Data.Proxy
                    (Proxy(Proxy))
 import           GHC.Generics
@@ -25,64 +25,68 @@
 import           Prelude
 
 import           Test.StateMachine.Types
-                   (Command(..), Reference, Symbolic)
+                   (Command(..))
 
 ------------------------------------------------------------------------
 
-class GConName a where
-  gconName  :: a -> String
-  gconNames :: Proxy a -> [String]
+-- | The names of all possible commands
+--
+-- This is used for things like tagging, coverage checking, etc.
+class CommandNames (cmd :: k -> Type) where
+  -- | Name of this particular command
+  cmdName  :: cmd r -> String
 
-class GConName1 f where
-  gconName1  :: f a -> String
-  gconNames1 :: Proxy (f a) -> [String]
+  -- | Name of all possible commands
+  cmdNames :: Proxy (cmd r) -> [String]
 
-instance GConName1 U1 where
-  gconName1  _ = ""
-  gconNames1 _ = []
+  default cmdName :: (Generic1 cmd, CommandNames (Rep1 cmd)) => cmd r -> String
+  cmdName = cmdName . from1
 
-instance GConName1 (K1 i c) where
-  gconName1  _ = ""
-  gconNames1 _ = []
+  default cmdNames :: forall r. CommandNames (Rep1 cmd) => Proxy (cmd r) -> [String]
+  cmdNames _ = cmdNames (Proxy @(Rep1 cmd r))
 
-instance Constructor c => GConName1 (M1 C c f) where
-  gconName1                            = conName
-  gconNames1 (_ :: Proxy (M1 C c f p)) = [ conName @c undefined ] -- Can we do
+instance CommandNames U1 where
+  cmdName  _ = ""
+  cmdNames _ = []
+
+instance CommandNames (K1 i c) where
+  cmdName  _ = ""
+  cmdNames _ = []
+
+instance Constructor c => CommandNames (M1 C c f) where
+  cmdName                            = conName
+  cmdNames (_ :: Proxy (M1 C c f p)) = [ conName @c undefined ] -- Can we do
                                                                   -- better
                                                                   -- here?
 
-instance GConName1 f => GConName1 (M1 D c f) where
-  gconName1                            = gconName1  . unM1
-  gconNames1 (_ :: Proxy (M1 D c f p)) = gconNames1 (Proxy :: Proxy (f p))
+instance CommandNames f => CommandNames (M1 D c f) where
+  cmdName                            = cmdName  . unM1
+  cmdNames (_ :: Proxy (M1 D c f p)) = cmdNames (Proxy :: Proxy (f p))
 
-instance GConName1 f => GConName1 (M1 S c f) where
-  gconName1                            = gconName1  . unM1
-  gconNames1 (_ :: Proxy (M1 S c f p)) = gconNames1 (Proxy :: Proxy (f p))
+instance CommandNames f => CommandNames (M1 S c f) where
+  cmdName                            = cmdName  . unM1
+  cmdNames (_ :: Proxy (M1 S c f p)) = cmdNames (Proxy :: Proxy (f p))
 
-instance (GConName1 f, GConName1 g) => GConName1 (f :+: g) where
-  gconName1 (L1 x) = gconName1 x
-  gconName1 (R1 y) = gconName1 y
+instance (CommandNames f, CommandNames g) => CommandNames (f :+: g) where
+  cmdName (L1 x) = cmdName x
+  cmdName (R1 y) = cmdName y
 
-  gconNames1 (_ :: Proxy ((f :+: g) a)) =
-    gconNames1 (Proxy :: Proxy (f a)) ++
-    gconNames1 (Proxy :: Proxy (g a))
+  cmdNames (_ :: Proxy ((f :+: g) a)) =
+    cmdNames (Proxy :: Proxy (f a)) ++
+    cmdNames (Proxy :: Proxy (g a))
 
-instance (GConName1 f, GConName1 g) => GConName1 (f :*: g) where
-  gconName1  (x :*: y)                  = gconName1 x ++ gconName1 y
-  gconNames1 (_ :: Proxy ((f :*: g) a)) =
-    gconNames1 (Proxy :: Proxy (f a)) ++
-    gconNames1 (Proxy :: Proxy (g a))
+instance (CommandNames f, CommandNames g) => CommandNames (f :*: g) where
+  cmdName  (x :*: y)                  = cmdName x ++ cmdName y
+  cmdNames (_ :: Proxy ((f :*: g) a)) =
+    cmdNames (Proxy :: Proxy (f a)) ++
+    cmdNames (Proxy :: Proxy (g a))
 
-instance GConName1 f => GConName1 (Rec1 f) where
-  gconName1                          = gconName1  . unRec1
-  gconNames1 (_ :: Proxy (Rec1 f p)) = gconNames1 (Proxy :: Proxy (f p))
+instance CommandNames f => CommandNames (Rec1 f) where
+  cmdName                          = cmdName  . unRec1
+  cmdNames (_ :: Proxy (Rec1 f p)) = cmdNames (Proxy :: Proxy (f p))
 
 ------------------------------------------------------------------------
 
-instance GConName1 (Reference a) where
-  gconName1  _ = ""
-  gconNames1 _ = []
-
-instance (Generic1 cmd, GConName1 (Rep1 cmd)) => GConName (Command cmd) where
-  gconName  (Command cmd _) = gconName1  (from1 cmd)
-  gconNames _               = gconNames1 (Proxy :: Proxy (Rep1 cmd Symbolic))
+-- | Convenience wrapper for 'Command'
+commandName :: CommandNames cmd => Command cmd resp -> String
+commandName (Command cmd _ _) = cmdName cmd
diff --git a/src/Test/StateMachine/Parallel.hs b/src/Test/StateMachine/Parallel.hs
--- a/src/Test/StateMachine/Parallel.hs
+++ b/src/Test/StateMachine/Parallel.hs
@@ -22,14 +22,14 @@
   ( forAllParallelCommands
   , generateParallelCommands
   , shrinkParallelCommands
-  , validParallelCommands
-  , prop_splitCombine
+  , shrinkAndValidateParallel
   , runParallelCommands
   , runParallelCommandsNTimes
   , executeParallelCommands
   , linearise
   , toBoxDrawings
   , prettyParallelCommands
+  , advanceModel
   ) where
 
 import           Control.Arrow
@@ -39,16 +39,12 @@
 import           Control.Monad.Catch
                    (MonadCatch)
 import           Control.Monad.State
-                   (State, evalState, put, runStateT)
+                   (runStateT)
 import           Data.Bifunctor
                    (bimap)
 import           Data.List
                    (partition, permutations)
-import           Data.List.Split
-                   (splitPlacesBlanks)
-import           Data.Map
-                   (Map)
-import qualified Data.Map                          as M
+import qualified Data.Map.Strict                   as Map
 import           Data.Monoid
                    ((<>))
 import           Data.Set
@@ -56,12 +52,9 @@
 import qualified Data.Set                          as S
 import           Data.Tree
                    (Tree(Node))
-import           GHC.Generics
-                   (Generic1, Rep1)
 import           Prelude
 import           Test.QuickCheck
-                   (Gen, Property, Testable, choose, property,
-                   shrinkList, sized)
+                   (Gen, Property, Testable, choose, property, sized)
 import           Test.QuickCheck.Monadic
                    (PropertyM, run)
 import           Text.PrettyPrint.ANSI.Leijen
@@ -82,82 +75,120 @@
 ------------------------------------------------------------------------
 
 forAllParallelCommands :: Testable prop
-                       => (Show (cmd Symbolic), Show (model Symbolic))
-                       => (Generic1 cmd, GConName1 (Rep1 cmd))
+                       => (Show (cmd Symbolic), Show (resp Symbolic), Show (model Symbolic))
+                       => CommandNames cmd
                        => (Rank2.Traversable cmd, Rank2.Foldable resp)
                        => StateMachine model cmd m resp
-                       -> (ParallelCommands cmd -> prop)     -- ^ Predicate.
+                       -> (ParallelCommands cmd resp -> prop)     -- ^ Predicate.
                        -> Property
 forAllParallelCommands sm =
   forAllShrinkShow (generateParallelCommands sm) (shrinkParallelCommands sm) ppShow
 
+-- | Generate parallel commands.
+--
+-- Parallel commands are generated as follows. We begin by generating
+-- sequential commands and then splitting this list in two at some index. The
+-- first half will be used as the prefix.
+--
+-- The second half will be used to build suffixes. For example, starting from
+-- the following sequential commands:
+--
+-- > [A, B, C, D, E, F, G, H, I]
+--
+-- We split it in two, giving us the prefix and the rest:
+--
+-- > prefix: [A, B]
+-- > rest:   [C, D, E, F, G, H, I]
+--
+-- We advance the model with the prefix.
+--
+-- __Make a suffix__: we take commands from @rest@ as long as these are
+-- parallel safe (see 'parallelSafe'). This means that the pre-conditions
+-- (using the \'advanced\' model) of each of those commands will hold no
+-- matter in which order they are executed.
+--
+-- Say this is true for @[C, D, E]@, but not anymore for @F@, maybe because
+-- @F@ depends on one of @[C, D, E]@. Then we divide this \'chunk\' in two by
+-- splitting it in the middle, obtaining @[C]@ and @[D, E]@. These two halves
+-- of the chunk (stored as a 'Pair') will later be executed in parallel.
+-- Together they form one suffix.
+--
+-- Then the model is advanced using the whole chunk @[C, D, E]@. Think of it
+-- as a barrier after executing the two halves of the chunk in parallel. Then
+-- this process of building a chunk/suffix repeats itself, starting from
+-- __Make a suffix__ using the \'advanced\' model.
+--
+-- In the end we might end up with something like this:
+--
+-- >         ┌─ [C] ──┐  ┌ [F, G] ┐
+-- > [A, B] ─┤        ├──┤        │
+-- >         └ [D, E] ┘  └ [H, I] ┘
+--
 generateParallelCommands :: forall model cmd m resp
                           . (Rank2.Foldable resp, Show (model Symbolic))
-                         => (Generic1 cmd, GConName1 (Rep1 cmd))
+                         => CommandNames cmd
                          => StateMachine model cmd m resp
-                         -> Gen (ParallelCommands cmd)
+                         -> Gen (ParallelCommands cmd resp)
 generateParallelCommands sm@StateMachine { initModel } = do
   Commands cmds      <- generateCommands sm Nothing
   prefixLength       <- sized (\k -> choose (0, k `div` 3))
   let (prefix, rest) =  bimap Commands Commands (splitAt prefixLength cmds)
   return (ParallelCommands prefix
-            (makeSuffixes (advanceModel sm initModel newCounter prefix) rest))
+            (makeSuffixes (advanceModel sm initModel prefix) rest))
   where
-    makeSuffixes :: (model Symbolic, Counter) -> Commands cmd -> [Pair (Commands cmd)]
-    makeSuffixes (model0, counter0) = go (model0, counter0) [] . unCommands
+    makeSuffixes :: model Symbolic -> Commands cmd resp -> [Pair (Commands cmd resp)]
+    makeSuffixes model0 = go model0 [] . unCommands
       where
-        go _                acc []   = reverse acc
-        go (model, counter) acc cmds = go (advanceModel sm model counter (Commands safe))
-                                          (Pair (Commands safe1) (Commands safe2) : acc)
-                                          rest
+        go _     acc []   = reverse acc
+        go model acc cmds = go (advanceModel sm model (Commands safe))
+                               (Pair (Commands safe1) (Commands safe2) : acc)
+                               rest
           where
-            (safe, rest)   = spanSafe model counter [] cmds
+            (safe, rest)   = spanSafe model [] cmds
             (safe1, safe2) = splitAt (length safe `div` 2) safe
 
         suffixLength = 5
 
-        spanSafe :: model Symbolic -> Counter -> [Command cmd] -> [Command cmd]
-                 -> ([Command cmd], [Command cmd])
-        spanSafe _     _       safe []                         = (reverse safe, [])
-        spanSafe model counter safe (cmd@(Command _ _) : cmds)
-          | length safe <= suffixLength &&
-              parallelSafe sm model counter (Commands (cmd : safe)) =
-                spanSafe model counter (cmd : safe) cmds
-          | otherwise = (reverse safe, cmd : cmds)
+        -- Split the list of commands in two such that the first half is a
+        -- list of commands for which the preconditions of all commands hold
+        -- for permutation of the list, i.e. it is parallel safe. The other
+        -- half is the remainder of the input list.
+        spanSafe :: model Symbolic -> [Command cmd resp] -> [Command cmd resp]
+                 -> ([Command cmd resp], [Command cmd resp])
+        spanSafe _     safe []           = (reverse safe, [])
+        spanSafe model safe (cmd : cmds)
+          | length safe <= suffixLength
+          , parallelSafe sm model (Commands (cmd : safe))
+          = spanSafe model (cmd : safe) cmds
+          | otherwise
+          = (reverse safe, cmd : cmds)
 
 -- | A list of commands is parallel safe if the pre-conditions for all commands
 --   hold in all permutations of the list.
 parallelSafe :: StateMachine model cmd m resp -> model Symbolic
-             -> Counter -> Commands cmd -> Bool
-parallelSafe StateMachine { precondition, transition, mock } model0 counter0
+             -> Commands cmd resp -> Bool
+parallelSafe StateMachine { precondition, transition } model0
   = and
-  . map (preconditionsHold model0 counter0)
+  . map (preconditionsHold model0)
   . permutations
   . unCommands
   where
-    preconditionsHold _     _       []                         = True
-    preconditionsHold model counter (Command cmd _vars : cmds) =
-      let
-        (resp, counter') = runGenSym (mock model cmd) counter
-      in
+    preconditionsHold _     []                              = True
+    preconditionsHold model (Command cmd resp _vars : cmds) =
         boolean (precondition model cmd) &&
-          preconditionsHold (transition model cmd resp) counter' cmds
+          preconditionsHold (transition model cmd resp) cmds
 
 -- | Apply the transition of some commands to a model.
 advanceModel :: StateMachine model cmd m resp
-             -> model Symbolic  -- ^ The model.
-             -> Counter
-             -> Commands cmd    -- ^ The commands.
-             -> (model Symbolic, Counter)
-advanceModel StateMachine { transition, mock } model0 counter0 =
-  go model0 counter0 . unCommands
+             -> model Symbolic      -- ^ The model.
+             -> Commands cmd resp   -- ^ The commands.
+             -> model Symbolic
+advanceModel StateMachine { transition } model0 =
+  go model0 . unCommands
   where
-    go model counter []                         = (model, counter)
-    go model counter (Command cmd _vars : cmds) =
-      let
-        (resp, counter') = runGenSym (mock model cmd) counter
-      in
-        go (transition model cmd resp) counter' cmds
+    go model []                              = model
+    go model (Command cmd resp _vars : cmds) =
+        go (transition model cmd resp) cmds
 
 ------------------------------------------------------------------------
 
@@ -167,27 +198,33 @@
   :: forall cmd model m resp. Rank2.Traversable cmd
   => Rank2.Foldable resp
   => StateMachine model cmd m resp
-  -> (ParallelCommands cmd -> [ParallelCommands cmd])
-shrinkParallelCommands sm@StateMachine { shrinker, initModel }
+  -> (ParallelCommands cmd resp -> [ParallelCommands cmd resp])
+shrinkParallelCommands sm@StateMachine { initModel }
                        (ParallelCommands prefix suffixes)
-  = filterMaybe (flip evalState (initModel, M.empty, newCounter) . validParallelCommands sm)
-      [ ParallelCommands prefix' (map toPair suffixes')
-      | (prefix', suffixes') <- shrinkPair' shrinkCommands' shrinkSuffixes
-                                            (prefix, map fromPair suffixes)
+  = concatMap go
+      [ Shrunk s (ParallelCommands prefix' (map toPair suffixes'))
+      | Shrunk s (prefix', suffixes') <- shrinkPairS shrinkCommands' shrinkSuffixes
+                                                     (prefix, map fromPair suffixes)
       ]
       ++
       shrinkMoveSuffixToPrefix
   where
-    shrinkCommands' :: Commands cmd -> [Commands cmd]
-    shrinkCommands'
-      = map Commands
-      . shrinkList (liftShrinkCommand shrinker)
-      . unCommands
+    go :: Shrunk (ParallelCommands cmd resp) -> [ParallelCommands cmd resp]
+    go (Shrunk shrunk cmds) =
+        shrinkAndValidateParallel sm
+                                  (if shrunk then DontShrink else MustShrink)
+                                  (initValidateEnv initModel)
+                                  cmds
 
-    shrinkSuffixes :: [(Commands cmd, Commands cmd)] -> [[(Commands cmd, Commands cmd)]]
-    shrinkSuffixes = shrinkList (shrinkPair shrinkCommands')
+    shrinkCommands' :: Commands cmd resp -> [Shrunk (Commands cmd resp)]
+    shrinkCommands' = map (fmap Commands) . shrinkListS' . unCommands
 
-    shrinkMoveSuffixToPrefix :: [ParallelCommands cmd]
+    shrinkSuffixes :: [(Commands cmd resp, Commands cmd resp)]
+                   -> [Shrunk [(Commands cmd resp, Commands cmd resp)]]
+    shrinkSuffixes = shrinkListS (shrinkPairS' shrinkCommands')
+
+    -- Moving a command from a suffix to the prefix preserves validity
+    shrinkMoveSuffixToPrefix :: [ParallelCommands cmd resp]
     shrinkMoveSuffixToPrefix = case suffixes of
       []                   -> []
       (suffix : suffixes') ->
@@ -197,61 +234,72 @@
                                                     unCommands (proj2 suffix))
         ]
 
+    -- >    pickOneReturnRest []     == []
+    -- >    pickOneReturnRest [1]    == [ (1,[]) ]
+    -- >    pickOneReturnRest [1..3] == [ (1,[2,3]), (2,[1,3]), (3,[1,2]) ]
     pickOneReturnRest :: [a] -> [(a, [a])]
     pickOneReturnRest []       = []
     pickOneReturnRest (x : xs) = (x, xs) : map (id *** (x :)) (pickOneReturnRest xs)
 
+    -- >    pickOneReturnRest2 ([], []) == []
+    -- >    pickOneReturnRest2 ([1,2], [3,4])
+    -- > == [ (1,([2],[3,4])), (2,([1],[3,4])), (3,([1,2],[4])), (4,([1,2],[3])) ]
     pickOneReturnRest2 :: ([a], [a]) -> [(a, ([a],[a]))]
     pickOneReturnRest2 (xs, ys) =
       map (id *** flip (,) ys) (pickOneReturnRest xs) ++
       map (id ***      (,) xs) (pickOneReturnRest ys)
 
-validParallelCommands :: forall model cmd m resp. (Rank2.Traversable cmd, Rank2.Foldable resp)
-                      => StateMachine model cmd m resp -> ParallelCommands cmd
-                      -> State (model Symbolic, Map Var Var, Counter) (Maybe (ParallelCommands cmd))
-validParallelCommands sm@StateMachine { initModel } (ParallelCommands prefix suffixes) = do
-  let prefixLength       = lengthCommands prefix
-      leftSuffixes       = map (\(Pair l _r) -> l) suffixes
-      rightSuffixes      = map (\(Pair _l r) -> r) suffixes
-      leftSuffixLengths  = map lengthCommands leftSuffixes
-      rightSuffixLengths = map lengthCommands rightSuffixes
-      leftSuffix         = mconcat leftSuffixes
-      rightSuffix        = mconcat rightSuffixes
-  mleft  <- validCommands sm (prefix <> leftSuffix)
-  put (initModel, M.empty, newCounter)
-  mright <- validCommands sm (prefix <> rightSuffix)
-  case (mleft, mright) of
-    (Nothing, Nothing)      -> return Nothing
-    (Just _,  Nothing)      -> return Nothing
-    (Nothing, Just _)       -> return Nothing
-    (Just left, Just right) ->
-      case (splitPlacesBlanks (prefixLength : leftSuffixLengths)  (unCommands left),
-            splitPlacesBlanks (prefixLength : rightSuffixLengths) (unCommands right)) of
-        ([]                     , [])                 -> error "validParallelCommands: impossible"
-        ([]                     , _ : _)              -> error "validParallelCommands: impossible"
-        (_ : _                  , [])                 -> error "validParallelCommands: impossible"
-        (prefix' : leftSuffixes', _ : rightSuffixes') -> do
-          let suffixes' = zipWith Pair (map Commands leftSuffixes')
-                                       (map Commands rightSuffixes')
-              (model', counter') = advanceModel sm initModel newCounter (Commands prefix')
-
-          if parallelSafeMany sm model' counter' suffixes'
-          then return (Just (ParallelCommands (Commands prefix') suffixes'))
-          else return Nothing
-
-parallelSafeMany :: StateMachine model cmd m resp -> model Symbolic
-                 -> Counter -> [Pair (Commands cmd)] -> Bool
-parallelSafeMany sm = go
+shrinkAndValidateParallel :: forall model cmd m resp. (Rank2.Traversable cmd, Rank2.Foldable resp)
+                          => StateMachine model cmd m resp
+                          -> ShouldShrink
+                          -> ValidateEnv model
+                          -> ParallelCommands cmd resp
+                          -> [ParallelCommands cmd resp]
+shrinkAndValidateParallel sm = \shouldShrink env (ParallelCommands prefix suffixes) ->
+    let go' shouldShrink' (env', prefix') = go prefix' env' shouldShrink' suffixes in
+    case shouldShrink of
+      DontShrink -> concatMap (go' DontShrink) (shrinkAndValidate sm DontShrink env prefix)
+      MustShrink -> concatMap (go' DontShrink) (shrinkAndValidate sm MustShrink env prefix)
+                 ++ concatMap (go' MustShrink) (shrinkAndValidate sm DontShrink env prefix)
   where
-    go _ _ []                                   = True
-    go model counter (Pair cmds1 cmds2 : cmdss) = parallelSafe sm model counter cmds
-                                                && go model' counter' cmdss
+    withCounterFrom :: ValidateEnv model -> ValidateEnv model -> ValidateEnv model
+    e `withCounterFrom` e' = e { veCounter = veCounter e' }
+
+    go :: Commands cmd resp          -- validated prefix
+       -> ValidateEnv model          -- environment after the prefix
+       -> ShouldShrink               -- should we /still/ shrink something?
+       -> [Pair (Commands cmd resp)] -- suffixes to validate
+       -> [ParallelCommands cmd resp]
+    go prefix' envAfterPrefix = go' [] envAfterPrefix
       where
-        cmds               = cmds1 <> cmds2
-        (model', counter') = advanceModel sm model counter cmds
+        go' :: [Pair (Commands cmd resp)] -- accumulated validated suffixes (in reverse order)
+            -> ValidateEnv model          -- environment after the validated suffixes
+            -> ShouldShrink               -- should we /still/ shrink something?
+            -> [Pair (Commands cmd resp)] -- suffixes to validate
+            -> [ParallelCommands cmd resp]
+        go' _   _   MustShrink [] = [] -- Failed to shrink something
+        go' acc _   DontShrink [] = [ParallelCommands prefix' (reverse acc)]
+        go' acc env shouldShrink (Pair l r : suffixes) =
+            flip concatMap shrinkOpts $ \((shrinkL, shrinkR), shrinkRest) -> concat
+              [ go' (Pair l' r' : acc) (combineEnv envL envR) shrinkRest suffixes
+              | (envL, l') <- shrinkAndValidate sm shrinkL  env                         l
+              , (envR, r') <- shrinkAndValidate sm shrinkR (env `withCounterFrom` envL) r
+              ]
+          where
+            combineEnv :: ValidateEnv model -> ValidateEnv model -> ValidateEnv model
+            combineEnv envL envR = ValidateEnv {
+                  veModel   = advanceModel sm (veModel envL) r
+                , veScope   = Map.union (veScope envL) (veScope envR)
+                , veCounter = veCounter envR
+                }
 
-prop_splitCombine :: [[Int]] -> Bool
-prop_splitCombine xs = splitPlacesBlanks (map length xs) (concat xs) == xs
+            shrinkOpts :: [((ShouldShrink, ShouldShrink), ShouldShrink)]
+            shrinkOpts =
+                case shouldShrink of
+                  DontShrink -> [ ((DontShrink, DontShrink), DontShrink) ]
+                  MustShrink -> [ ((MustShrink, DontShrink), DontShrink)
+                                , ((DontShrink, MustShrink), DontShrink)
+                                , ((DontShrink, DontShrink), MustShrink) ]
 
 ------------------------------------------------------------------------
 
@@ -259,7 +307,7 @@
                     => (Rank2.Traversable cmd, Rank2.Foldable resp)
                     => (MonadCatch m, MonadUnliftIO m)
                     => StateMachine model cmd m resp
-                    -> ParallelCommands cmd
+                    -> ParallelCommands cmd resp
                     -> PropertyM m [(History cmd resp, Logic)]
 runParallelCommands sm = runParallelCommandsNTimes 10 sm
 
@@ -268,7 +316,7 @@
                           => (MonadCatch m, MonadUnliftIO m)
                           => Int -- ^ How many times to execute the parallel program.
                           -> StateMachine model cmd m resp
-                          -> ParallelCommands cmd
+                          -> ParallelCommands cmd resp
                           -> PropertyM m [(History cmd resp, Logic)]
 runParallelCommandsNTimes n sm cmds =
   replicateM n $ do
@@ -278,7 +326,7 @@
 executeParallelCommands :: (Rank2.Traversable cmd, Rank2.Foldable resp)
                         => (MonadCatch m, MonadUnliftIO m)
                         => StateMachine model cmd m resp
-                        -> ParallelCommands cmd
+                        -> ParallelCommands cmd resp
                         -> m (History cmd resp, Reason)
 executeParallelCommands sm@StateMachine{ initModel } (ParallelCommands prefix suffixes) = do
 
@@ -344,7 +392,7 @@
 --   counterexample if any of the runs fail.
 prettyParallelCommands :: (MonadIO m, Rank2.Foldable cmd)
                        => (Show (cmd Concrete), Show (resp Concrete))
-                       => ParallelCommands cmd
+                       => ParallelCommands cmd resp
                        -> [(History cmd resp, Logic)] -- ^ Output of 'runParallelCommands'.
                        -> PropertyM m ()
 prettyParallelCommands cmds =
@@ -369,7 +417,7 @@
 --   seeing how a race condition might have occured.
 toBoxDrawings :: forall cmd resp. Rank2.Foldable cmd
               => (Show (cmd Concrete), Show (resp Concrete))
-              => ParallelCommands cmd -> History cmd resp -> Doc
+              => ParallelCommands cmd resp -> History cmd resp -> Doc
 toBoxDrawings (ParallelCommands prefix suffixes) = toBoxDrawings'' allVars
   where
     allVars = getAllUsedVars prefix `S.union`
@@ -399,5 +447,5 @@
         evT :: [(EventType, Pid)]
         evT = toEventType (filter (\e -> fst e `Prelude.elem` map Pid [1, 2]) h)
 
-getAllUsedVars :: Rank2.Foldable cmd => Commands cmd -> Set Var
-getAllUsedVars = S.fromList . foldMap (\(Command cmd _) -> getUsedVars cmd) . unCommands
+getAllUsedVars :: Rank2.Foldable cmd => Commands cmd resp -> Set Var
+getAllUsedVars = S.fromList . foldMap (\(Command cmd _ _) -> getUsedVars cmd) . unCommands
diff --git a/src/Test/StateMachine/Sequential.hs b/src/Test/StateMachine/Sequential.hs
--- a/src/Test/StateMachine/Sequential.hs
+++ b/src/Test/StateMachine/Sequential.hs
@@ -6,6 +6,7 @@
 {-# LANGUAGE PolyKinds             #-}
 {-# LANGUAGE RecordWildCards       #-}
 {-# LANGUAGE ScopedTypeVariables   #-}
+{-# LANGUAGE TupleSections         #-}
 
 -----------------------------------------------------------------------------
 -- |
@@ -30,9 +31,10 @@
   , calculateFrequency
   , getUsedVars
   , shrinkCommands
-  , liftShrinkCommand
-  , validCommands
-  , filterMaybe
+  , shrinkAndValidate
+  , ValidateEnv(..)
+  , ShouldShrink(..)
+  , initValidateEnv
   , runCommands
   , getChanContents
   , executeCommands
@@ -50,8 +52,9 @@
 import           Control.Monad.Catch
                    (MonadCatch, catch)
 import           Control.Monad.State
-                   (State, StateT, evalState, evalStateT, get, lift, put,
-                   runStateT)
+                   (StateT, evalStateT, get, lift, put, runStateT)
+import           Data.Bifunctor
+                   (second)
 import           Data.Dynamic
                    (Dynamic, toDyn)
 import           Data.Either
@@ -73,12 +76,10 @@
 import           Data.TreeDiff
                    (ToExpr, ansiWlBgEditExprCompact, ediff)
 import qualified Data.Vector                       as V
-import           GHC.Generics
-                   (Generic1, Rep1, from1)
 import           Prelude
 import           Test.QuickCheck
                    (Gen, Property, Testable, choose, collect, generate,
-                   resize, shrinkList, sized, suchThat)
+                   resize, sized, suchThat)
 import           Test.QuickCheck.Monadic
                    (PropertyM, run)
 import           Text.PrettyPrint.ANSI.Leijen
@@ -87,8 +88,8 @@
 import           Text.Show.Pretty
                    (ppShow)
 import           UnliftIO
-                   (MonadIO, TChan, newTChanIO, tryReadTChan, writeTChan,
-                   atomically)
+                   (MonadIO, TChan, atomically, newTChanIO,
+                   tryReadTChan, writeTChan)
 
 import           Test.StateMachine.ConstructorName
 import           Test.StateMachine.Logic
@@ -99,38 +100,38 @@
 ------------------------------------------------------------------------
 
 forAllCommands :: Testable prop
-               => (Show (cmd Symbolic), Show (model Symbolic))
-               => (Generic1 cmd, GConName1 (Rep1 cmd))
+               => (Show (cmd Symbolic), Show (resp Symbolic), Show (model Symbolic))
+               => CommandNames cmd
                => (Rank2.Traversable cmd, Rank2.Foldable resp)
                => StateMachine model cmd m resp
                -> Maybe Int -- ^ Minimum number of commands.
-               -> (Commands cmd -> prop)     -- ^ Predicate.
+               -> (Commands cmd resp -> prop)     -- ^ Predicate.
                -> Property
 forAllCommands sm mnum =
   forAllShrinkShow (generateCommands sm mnum) (shrinkCommands sm) ppShow
 
 generateCommands :: (Rank2.Foldable resp, Show (model Symbolic))
-                 => (Generic1 cmd, GConName1 (Rep1 cmd))
+                 => CommandNames cmd
                  => StateMachine model cmd m resp
                  -> Maybe Int -- ^ Minimum number of commands.
-                 -> Gen (Commands cmd)
+                 -> Gen (Commands cmd resp)
 generateCommands sm@StateMachine { initModel } mnum =
   evalStateT (generateCommandsState sm newCounter mnum) (initModel, Nothing)
 
 generateCommandsState :: forall model cmd m resp. Rank2.Foldable resp
                       => Show (model Symbolic)
-                      => (Generic1 cmd, GConName1 (Rep1 cmd))
+                      => CommandNames cmd
                       => StateMachine model cmd m resp
                       -> Counter
                       -> Maybe Int -- ^ Minimum number of commands.
-                      -> StateT (model Symbolic, Maybe (cmd Symbolic)) Gen (Commands cmd)
+                      -> StateT (model Symbolic, Maybe (cmd Symbolic)) Gen (Commands cmd resp)
 generateCommandsState StateMachine { precondition, generator, transition
                                    , mock, distribution } counter0 mnum = do
   size0 <- lift (sized (\k -> choose (fromMaybe 0 mnum, k)))
   Commands <$> go size0 counter0 []
   where
-    go :: Int -> Counter -> [Command cmd]
-       -> StateT (model Symbolic, Maybe (cmd Symbolic)) Gen [Command cmd]
+    go :: Int -> Counter -> [Command cmd resp]
+       -> StateT (model Symbolic, Maybe (cmd Symbolic)) Gen [Command cmd resp]
     go 0    _       cmds = return (reverse cmds)
     go size counter cmds = do
       (model, mprevious) <- get
@@ -149,30 +150,29 @@
               Just next -> do
                 let (resp, counter') = runGenSym (mock model next) counter
                 put (transition model next resp, Just next)
-                go (size - 1) counter' (Command next (getUsedVars resp) : cmds)
+                go (size - 1) counter' (Command next resp (getUsedVars resp) : cmds)
 
-commandFrequency :: forall cmd. (Generic1 cmd, GConName1 (Rep1 cmd))
+commandFrequency :: forall cmd. CommandNames cmd
                  => Gen (cmd Symbolic) -> Maybe (Matrix Int) -> Maybe (cmd Symbolic)
                  -> [(Int, Gen (cmd Symbolic))]
 commandFrequency gen Nothing             _          = [ (1, gen) ]
 commandFrequency gen (Just distribution) mprevious  =
-  [ (freq, gen `suchThat` ((== con) . gconName1 . from1)) | (freq, con) <- weights ]
+  [ (freq, gen `suchThat` ((== con) . cmdName)) | (freq, con) <- weights ]
     where
       idx = case mprevious of
               Nothing       -> 1
               Just previous ->
                 let
-                  rep = from1 previous
-                  con = gconName1 rep
+                  con = cmdName previous
                   err = "genetateCommandState: no command: " <> con
                 in
                   fromMaybe (error err) ((+ 2) <$>
-                    elemIndex con (gconNames1 (Proxy :: Proxy (Rep1 cmd Symbolic))))
+                    elemIndex con (cmdNames (Proxy :: Proxy (cmd Symbolic))))
       row     = V.toList (getRow idx distribution)
-      weights = zip row (gconNames1 (Proxy :: Proxy (Rep1 cmd Symbolic)))
+      weights = zip row (cmdNames (Proxy :: Proxy (cmd Symbolic)))
 
 measureFrequency :: (Rank2.Foldable resp, Show (model Symbolic))
-                 => (Generic1 cmd, GConName1 (Rep1 cmd))
+                 => CommandNames cmd
                  => StateMachine model cmd m resp
                  -> Maybe Int -- ^ Minimum number of commands.
                  -> Int       -- ^ Maximum number of commands.
@@ -181,76 +181,133 @@
   cmds <- generate (sequence [ resize n (generateCommands sm min0) | n <- [0, 2..size] ])
   return (M.unions (map calculateFrequency cmds))
 
-calculateFrequency :: (Generic1 cmd, GConName1 (Rep1 cmd))
-                   => Commands cmd -> Map (String, Maybe String) Int
+calculateFrequency :: CommandNames cmd
+                   => Commands cmd resp -> Map (String, Maybe String) Int
 calculateFrequency = go M.empty . unCommands
   where
     go m [] = m
     go m [cmd]
-      = M.insertWith (\_ old -> old + 1) (gconName cmd, Nothing) 1 m
+      = M.insertWith (\_ old -> old + 1) (commandName cmd, Nothing) 1 m
     go m (cmd1 : cmd2 : cmds)
-      = go (M.insertWith (\_ old -> old + 1) (gconName cmd1,
-                                              Just (gconName cmd2)) 1 m) cmds
+      = go (M.insertWith (\_ old -> old + 1) (commandName cmd1,
+                                              Just (commandName cmd2)) 1 m) cmds
 
 getUsedVars :: Rank2.Foldable f => f Symbolic -> [Var]
 getUsedVars = Rank2.foldMap (\(Symbolic v) -> [v])
 
 -- | Shrink commands in a pre-condition and scope respecting way.
-shrinkCommands :: (Rank2.Traversable cmd, Rank2.Foldable resp)
-               => StateMachine model cmd m resp -> Commands cmd
-               -> [Commands cmd]
-shrinkCommands sm@StateMachine { initModel, shrinker }
-  = filterMaybe ( flip evalState (initModel, M.empty, newCounter)
-                . validCommands sm
-                . Commands)
-  . shrinkList (liftShrinkCommand shrinker)
-  . unCommands
+shrinkCommands ::  forall model cmd m resp. (Rank2.Traversable cmd, Rank2.Foldable resp)
+               => StateMachine model cmd m resp -> Commands cmd resp
+               -> [Commands cmd resp]
+shrinkCommands sm@StateMachine { initModel } =
+    concatMap go . shrinkListS' . unCommands
+  where
+    go :: Shrunk [Command cmd resp] -> [Commands cmd resp]
+    go (Shrunk shrunk cmds) = map snd $
+        shrinkAndValidate sm
+                          (if shrunk then DontShrink else MustShrink)
+                          (initValidateEnv initModel)
+                          (Commands cmds)
 
-liftShrinkCommand :: (cmd Symbolic -> [cmd Symbolic])
-                  -> (Command cmd -> [Command cmd])
-liftShrinkCommand shrinker (Command cmd resp) =
-  [ Command cmd' resp | cmd' <- shrinker cmd ]
+-- | Environment required during 'shrinkAndValidate'
+data ValidateEnv model = ValidateEnv {
+      -- | The model we're starting validation from
+      veModel   :: model Symbolic
 
-filterMaybe :: (a -> Maybe b) -> [a] -> [b]
-filterMaybe _ []       = []
-filterMaybe f (x : xs) = case f x of
-  Nothing ->     filterMaybe f xs
-  Just y  -> y : filterMaybe f xs
+      -- | Reference renumbering
+      --
+      -- When a command
+      --
+      -- > Command .. [Var i, ..]
+      --
+      -- is changed during validation to
+      --
+      -- > Command .. [Var j, ..]
+      --
+      -- then any subsequent uses of @Var i@ should be replaced by @Var j@. This
+      -- is recorded in 'veScope'. When we /remove/ the first command
+      -- altogether (during shrinking), then @Var i@ won't appear in the
+      -- 'veScope' and shrank candidates that contain commands referring to @Var
+      -- i@ should be considered as invalid.
+    , veScope   :: Map Var Var
 
-validCommands :: forall model cmd m resp. (Rank2.Traversable cmd, Rank2.Foldable resp)
-              => StateMachine model cmd m resp -> Commands cmd
-              -> State (model Symbolic, Map Var Var, Counter) (Maybe (Commands cmd))
-validCommands StateMachine { precondition, transition, mock } =
-  fmap (fmap Commands) . go . unCommands
+      -- | Counter (for generating new references)
+    , veCounter :: Counter
+    }
+
+initValidateEnv :: model Symbolic -> ValidateEnv model
+initValidateEnv initModel = ValidateEnv {
+      veModel   = initModel
+    , veScope   = M.empty
+    , veCounter = newCounter
+    }
+
+data ShouldShrink = MustShrink | DontShrink
+
+-- | Validate list of commands, optionally shrinking one of the commands
+--
+-- The input to this function is a list of commands ('Commands'), for example
+--
+-- > [A, B, C, D, E, F, G, H]
+--
+-- The /result/ is a /list/ of 'Commands', i.e. a list of lists. The
+-- outermost list is used for all the shrinking possibilities. For example,
+-- let's assume we haven't shrunk something yet, and therefore need to shrink
+-- one of the commands. Let's further assume that only commands B and E can be
+-- shrunk, to B1, B2 and E1, E2, E3 respectively. Then the result will look
+-- something like
+--
+-- > [    -- outermost list recording all the shrink possibilities
+-- >     [A', B1', C', D', E' , F', G', H']   -- B shrunk to B1
+-- >   , [A', B1', C', D', E' , F', G', H']   -- B shrunk to B2
+-- >   , [A', B' , C', D', E1', F', G', H']   -- E shrunk to E1
+-- >   , [A', B' , C', D', E2', F', G', H']   -- E shrunk to E2
+-- >   , [A', B' , C', D', E3', F', G', H']   -- E shrunk to E3
+-- > ]
+--
+-- where one of the commands has been shrunk and all commands have been
+-- validated and renumbered (references updated). So, in this example, the
+-- result will contain at most 5 lists; it may contain fewer, since some of
+-- these lists may not be valid.
+--
+-- If we _did_ already shrink something, then no commands will be shrunk, and
+-- the resulting list will either be empty (if the list of commands was invalid)
+-- or contain a /single/ element with the validated and renumbered commands.
+shrinkAndValidate :: forall model cmd m resp. (Rank2.Traversable cmd, Rank2.Foldable resp)
+                  => StateMachine model cmd m resp
+                  -> ShouldShrink
+                  -> ValidateEnv model
+                  -> Commands cmd resp
+                  -> [(ValidateEnv model, Commands cmd resp)]
+shrinkAndValidate StateMachine { precondition, transition, mock, shrinker } =
+    \env shouldShrink cmds -> map (second Commands) $ go env shouldShrink (unCommands cmds)
   where
-    -- As we validate we keep track of the variables that are in scope, in terms
-    -- of a mapping from old variables to new variables. For example, if a
-    -- command previously returned variables @[x',y']@, and in the new model
-    -- returns @[x,y]@, we extend our scope mapping with @[(x',x),(y',y)]@.
-    -- Later commands will then be translated accordingly, replacing references
-    -- to @x'@ by references to @y'@; references for which we have no updated
-    -- variable in scope are considered invalid: this may happen if those later
-    -- commands refer to a command which shrinking deleted altogether, /or/ it
-    -- may happen when the command was not deleted but in the new model returned
-    -- fewer references.
-    go :: [Command cmd] -> State (model Symbolic, Map Var Var, Counter) (Maybe [Command cmd])
-    go []                          = return (Just [])
-    go (Command cmd' vars' : cmds) = do
-      (model, scope, counter) <- get
+    go :: ShouldShrink -> ValidateEnv model -> [Command cmd resp] -> [(ValidateEnv model, [Command cmd resp])]
+    go MustShrink   _   [] = []          -- we failed to shrink anything
+    go DontShrink   env [] = [(env, [])] -- successful termination
+    go shouldShrink (ValidateEnv model scope counter) (Command cmd' _resp vars' : cmds) =
       case Rank2.traverse (remapVars scope) cmd' of
-        Just cmd | boolean (precondition model cmd) -> do
-          let (resp, counter') = runGenSym (mock model cmd) counter
-              vars             = getUsedVars resp
-
-          put ( transition model cmd resp
-              , M.fromList (zip vars' vars) `M.union` scope
-              , counter')
-          mih <- go cmds
-          case mih of
-            Nothing -> return Nothing
-            Just ih -> return (Just (Command cmd vars : ih))
-        _otherwise ->
-          return Nothing
+        Just remapped ->
+          -- shrink at most one command
+          let candidates :: [(ShouldShrink, cmd Symbolic)]
+              candidates =
+                case shouldShrink of
+                  DontShrink -> [(DontShrink, remapped)]
+                  MustShrink -> map (DontShrink,) (shrinker model remapped)
+                             ++ [(MustShrink, remapped)]
+          in flip concatMap candidates $ \(shouldShrink', cmd) ->
+               if boolean (precondition model cmd)
+                 then let (resp, counter') = runGenSym (mock model cmd) counter
+                          vars = getUsedVars resp
+                          env' = ValidateEnv {
+                                     veModel   = transition model cmd resp
+                                   , veScope   = M.fromList (zip vars' vars) `M.union` scope
+                                   , veCounter = counter'
+                                   }
+                      in map (second (Command cmd resp vars:)) $ go shouldShrink' env' cmds
+                 else []
+        Nothing ->
+          []
 
     remapVars :: Map Var Var -> Symbolic a -> Maybe (Symbolic a)
     remapVars scope (Symbolic v) = Symbolic <$> M.lookup v scope
@@ -258,7 +315,7 @@
 runCommands :: (Rank2.Traversable cmd, Rank2.Foldable resp)
             => (MonadCatch m, MonadIO m)
             => StateMachine model cmd m resp
-            -> Commands cmd
+            -> Commands cmd resp
             -> PropertyM m (History cmd resp, model Concrete, Reason)
 runCommands sm@StateMachine { initModel } = run . go
   where
@@ -285,13 +342,13 @@
                 -> TChan (Pid, HistoryEvent cmd resp)
                 -> Pid
                 -> Bool -- ^ Check invariant and post-condition?
-                -> Commands cmd
+                -> Commands cmd resp
                 -> StateT (Environment, model Symbolic, Counter, model Concrete) m Reason
 executeCommands StateMachine {..} hchan pid check =
   go . unCommands
   where
-    go []                         = return Ok
-    go (Command scmd vars : cmds) = do
+    go []                           = return Ok
+    go (Command scmd _ vars : cmds) = do
       (env, smodel, counter, cmodel) <- get
       case (check, logic (precondition smodel scmd)) of
         (True, VFalse ce) -> return (PreconditionFailed (show ce))
@@ -386,35 +443,35 @@
 
 -- | Print distribution of commands and fail if some commands have not
 --   been executed.
-checkCommandNames :: forall cmd. (Generic1 cmd, GConName1 (Rep1 cmd))
-                  => Commands cmd -> Property -> Property
+checkCommandNames :: forall cmd resp. CommandNames cmd
+                  => Commands cmd resp -> Property -> Property
 checkCommandNames cmds
   = collect names
   . oldCover (length names == numOfConstructors) 1 "coverage"
   where
     names             = commandNames cmds
-    numOfConstructors = length (gconNames1 (Proxy :: Proxy (Rep1 cmd Symbolic)))
+    numOfConstructors = length (cmdNames (Proxy :: Proxy (cmd Symbolic)))
 
-commandNames :: forall cmd. (Generic1 cmd, GConName1 (Rep1 cmd))
-             => Commands cmd -> [(String, Int)]
+commandNames :: forall cmd resp. CommandNames cmd
+             => Commands cmd resp -> [(String, Int)]
 commandNames = M.toList . foldl go M.empty . unCommands
   where
-    go :: Map String Int -> Command cmd -> Map String Int
-    go ih cmd = M.insertWith (+) (gconName cmd) 1 ih
+    go :: Map String Int -> Command cmd resp -> Map String Int
+    go ih cmd = M.insertWith (+) (commandName cmd) 1 ih
 
-commandNamesInOrder :: forall cmd. (Generic1 cmd, GConName1 (Rep1 cmd))
-                    => Commands cmd -> [String]
+commandNamesInOrder :: forall cmd resp. CommandNames cmd
+                    => Commands cmd resp -> [String]
 commandNamesInOrder = reverse . foldl go [] . unCommands
   where
-    go :: [String] -> Command cmd -> [String]
-    go ih cmd = gconName cmd : ih
+    go :: [String] -> Command cmd resp -> [String]
+    go ih cmd = commandName cmd : ih
 
 
-transitionMatrix :: forall cmd. GConName1 (Rep1 cmd)
+transitionMatrix :: forall cmd. CommandNames cmd
                  => Proxy (cmd Symbolic)
                  -> (String -> String -> Int) -> Matrix Int
 transitionMatrix _ f =
-  let cons = gconNames1 (Proxy :: Proxy (Rep1 cmd Symbolic))
+  let cons = cmdNames (Proxy :: Proxy (cmd Symbolic))
       n    = length cons
       m    = succ n
   in matrix m n $ \case
diff --git a/src/Test/StateMachine/Types.hs b/src/Test/StateMachine/Types.hs
--- a/src/Test/StateMachine/Types.hs
+++ b/src/Test/StateMachine/Types.hs
@@ -63,22 +63,25 @@
   , invariant      :: Maybe (model Concrete -> Logic)
   , generator      :: model Symbolic -> Maybe (Gen (cmd Symbolic))
   , distribution   :: Maybe (Matrix Int)
-  , shrinker       :: cmd Symbolic -> [cmd Symbolic]
+  , shrinker       :: model Symbolic -> cmd Symbolic -> [cmd Symbolic]
   , semantics      :: cmd Concrete -> m (resp Concrete)
   , mock           :: model Symbolic -> cmd Symbolic -> GenSym (resp Symbolic)
   }
 
-data Command cmd = Command !(cmd Symbolic) ![Var]
+-- | Previously symbolically executed command
+--
+-- Invariant: the variables must be the variables in the response.
+data Command cmd resp = Command !(cmd Symbolic) !(resp Symbolic) ![Var]
 
-deriving instance Show (cmd Symbolic) => Show (Command cmd)
+deriving instance (Show (cmd Symbolic), Show (resp Symbolic)) => Show (Command cmd resp)
 
-newtype Commands cmd = Commands
-  { unCommands :: [Command cmd] }
+newtype Commands cmd resp = Commands
+  { unCommands :: [Command cmd resp] }
   deriving (Semigroup, Monoid)
 
-deriving instance Show (cmd Symbolic) => Show (Commands cmd)
+deriving instance (Show (cmd Symbolic), Show (resp Symbolic)) => Show (Commands cmd resp)
 
-lengthCommands :: Commands cmd -> Int
+lengthCommands :: Commands cmd resp -> Int
 lengthCommands = length . unCommands
 
 data Reason
@@ -89,13 +92,13 @@
   | ExceptionThrown
   deriving (Eq, Show)
 
-data ParallelCommandsF t cmd = ParallelCommands
-  { prefix   :: !(Commands cmd)
-  , suffixes :: [t (Commands cmd)]
+data ParallelCommandsF t cmd resp = ParallelCommands
+  { prefix   :: !(Commands cmd resp)
+  , suffixes :: [t (Commands cmd resp)]
   }
 
-deriving instance (Show (cmd Symbolic), Show (t (Commands cmd))) =>
-  Show (ParallelCommandsF t cmd)
+deriving instance (Show (cmd Symbolic), Show (resp Symbolic), Show (t (Commands cmd resp))) =>
+  Show (ParallelCommandsF t cmd resp)
 
 data Pair a = Pair
   { proj1 :: !a
diff --git a/src/Test/StateMachine/Utils.hs b/src/Test/StateMachine/Utils.hs
--- a/src/Test/StateMachine/Utils.hs
+++ b/src/Test/StateMachine/Utils.hs
@@ -1,6 +1,8 @@
 {-# OPTIONS_GHC -Wno-orphans #-}
 
-{-# LANGUAGE CPP #-}
+{-# LANGUAGE CPP                 #-}
+{-# LANGUAGE DeriveFunctor       #-}
+{-# LANGUAGE ScopedTypeVariables #-}
 
 -----------------------------------------------------------------------------
 -- |
@@ -26,19 +28,27 @@
   , shrinkPair'
   , suchThatOneOf
   , oldCover
+  , Shrunk(..)
+  , shrinkS
+  , shrinkListS
+  , shrinkListS'
+  , shrinkPairS
+  , shrinkPairS'
   )
   where
 
 import           Prelude
+
 import           Test.QuickCheck
-                   (Gen, Property, Testable, again, counterexample,
-                   frequency, resize, shrinking, sized, suchThatMaybe,
+                   (Arbitrary, Gen, Property, Testable, again,
+                   counterexample, frequency, resize, shrink,
+                   shrinkList, shrinking, sized, suchThatMaybe,
                    whenFail)
 import           Test.QuickCheck.Monadic
                    (PropertyM(MkPropertyM))
 import           Test.QuickCheck.Property
-                   (Property(MkProperty), property, unProperty, (.&&.),
-                   (.||.), cover)
+                   (Property(MkProperty), cover, property, unProperty,
+                   (.&&.), (.||.))
 #if !MIN_VERSION_QuickCheck(2,10,0)
 import           Test.QuickCheck.Property
                    (succeeded)
@@ -121,3 +131,63 @@
 #else
   cover (fromIntegral n) x s p
 #endif
+
+-----------------------------------------------------------------------------
+
+-- | More permissive notion of shrinking where a value can shrink to itself
+--
+-- For example
+--
+-- > shrink  3 == [0, 2] -- standard QuickCheck shrink
+-- > shrinkS 3 == [Shrunk True 0, Shrunk True 2, Shrunk False 3]
+--
+-- This is primarily useful when shrinking composite structures: the combinators
+-- here keep track of whether something was shrunk /somewhere/ in the structure.
+-- For example, we have
+--
+-- >    shrinkListS (shrinkPairS shrinkS shrinkS) [(1,3),(2,4)]
+-- > == [ Shrunk True  []             -- removed all elements of the list
+-- >    , Shrunk True  [(2,4)]        -- removed the first
+-- >    , Shrunk True  [(1,3)]        -- removed the second
+-- >    , Shrunk True  [(0,3),(2,4)]  -- shrinking the '1'
+-- >    , Shrunk True  [(1,0),(2,4)]  -- shrinking the '3'
+-- >    , Shrunk True  [(1,2),(2,4)]  -- ..
+-- >    , Shrunk True  [(1,3),(0,4)]  -- shrinking the '2'
+-- >    , Shrunk True  [(1,3),(1,4)]  -- ..
+-- >    , Shrunk True  [(1,3),(2,0)]  -- shrinking the '4'
+-- >    , Shrunk True  [(1,3),(2,2)]  -- ..
+-- >    , Shrunk True  [(1,3),(2,3)]  -- ..
+-- >    , Shrunk False [(1,3),(2,4)]  -- the original unchanged list
+-- >    ]
+data Shrunk a = Shrunk { wasShrunk :: Bool, shrunk :: a }
+  deriving (Show, Functor)
+
+shrinkS :: Arbitrary a => a -> [Shrunk a]
+shrinkS a = map (Shrunk True) (shrink a) ++ [Shrunk False a]
+
+shrinkListS :: forall a. (a -> [Shrunk a]) -> [a] -> [Shrunk [a]]
+shrinkListS f = \xs -> concat [
+      map (Shrunk True) (shrinkList (const []) xs)
+    , shrinkOne xs
+    , [Shrunk False xs]
+    ]
+  where
+    shrinkOne :: [a] -> [Shrunk [a]]
+    shrinkOne []     = []
+    shrinkOne (x:xs) = [Shrunk True (x' : xs) | Shrunk True x'  <- f x]
+                    ++ [Shrunk True (x : xs') | Shrunk True xs' <- shrinkOne xs]
+
+-- | Shrink list without shrinking elements
+shrinkListS' :: [a] -> [Shrunk [a]]
+shrinkListS' = shrinkListS (\a -> [Shrunk False a])
+
+shrinkPairS :: (a -> [Shrunk a])
+            -> (b -> [Shrunk b])
+            -> (a, b) -> [Shrunk (a, b)]
+shrinkPairS f g (a, b) =
+       [Shrunk True (a', b) | Shrunk True a' <- f a ]
+    ++ [Shrunk True (a, b') | Shrunk True b' <- g b ]
+    ++ [Shrunk False (a, b)]
+
+shrinkPairS' :: (a -> [Shrunk a]) -> (a, a) -> [Shrunk (a, a)]
+shrinkPairS' f = shrinkPairS f f
diff --git a/test/CircularBuffer.hs b/test/CircularBuffer.hs
--- a/test/CircularBuffer.hs
+++ b/test/CircularBuffer.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE DataKinds          #-}
 {-# LANGUAGE DeriveAnyClass     #-}
 {-# LANGUAGE DeriveGeneric      #-}
 {-# LANGUAGE FlexibleInstances  #-}
@@ -44,6 +45,9 @@
 import           Data.Functor.Classes
                    (Eq1)
 import           Data.IORef
+                   (IORef, newIORef, readIORef, writeIORef)
+import           Data.Kind
+                   (Type)
 import           Data.Maybe
                    (isJust)
 import           Data.TreeDiff
@@ -138,7 +142,7 @@
 ------------------------------------------------------------------------
 
 -- | Buffer actions.
-data Action (r :: * -> *)
+data Action (r :: Type -> Type)
     -- | Create a new buffer of bounded capacity.
   = New Int
 
@@ -150,9 +154,9 @@
 
     -- | Get the number of elements in the buffer.
   | Len (Reference (Opaque Buffer) r)
-  deriving (Show, Generic1, Rank2.Functor, Rank2.Foldable, Rank2.Traversable)
+  deriving (Show, Generic1, Rank2.Functor, Rank2.Foldable, Rank2.Traversable, CommandNames)
 
-data Response (r :: * -> *)
+data Response (r :: Type -> Type)
   = NewR (Reference (Opaque Buffer) r)
   | PutR
   | GetR Int
@@ -251,10 +255,10 @@
   ] ++
   [ (4, Len <$> (fst <$> elements m)) | version == YesLen ]
 
-shrinker :: Action Symbolic -> [Action Symbolic]
-shrinker (New n)        = [ New n'        | n' <- shrink n ]
-shrinker (Put x buffer) = [ Put x' buffer | x' <- shrink x ]
-shrinker _              = []
+shrinker :: Model Symbolic -> Action Symbolic -> [Action Symbolic]
+shrinker _ (New n)        = [ New n'        | n' <- shrink n ]
+shrinker _ (Put x buffer) = [ Put x' buffer | x' <- shrink x ]
+shrinker _ _              = []
 
 ------------------------------------------------------------------------
 
diff --git a/test/CrudWebserverDb.hs b/test/CrudWebserverDb.hs
--- a/test/CrudWebserverDb.hs
+++ b/test/CrudWebserverDb.hs
@@ -71,11 +71,13 @@
                    (ReaderT, ask, runReaderT)
 import           Control.Monad.Trans.Resource
                    (ResourceT)
-import qualified Data.ByteString.Char8           as BS
+import qualified Data.ByteString.Char8         as BS
 import           Data.Char
                    (isPrint)
 import           Data.Functor.Classes
                    (Eq1)
+import           Data.Kind
+                   (Type)
 import           Data.List
                    (dropWhileEnd)
 import           Data.Monoid
@@ -86,7 +88,7 @@
                    (cs)
 import           Data.Text
                    (Text)
-import qualified Data.Text                       as T
+import qualified Data.Text                     as T
 import           Data.TreeDiff
                    (Expr(App), ToExpr, toExpr)
 import           Database.Persist.Postgresql
@@ -99,12 +101,15 @@
                    sqlSettings)
 import           GHC.Generics
                    (Generic, Generic1)
-import           Network
-                   (PortID(PortNumber), connectTo)
 import           Network.HTTP.Client
                    (Manager, defaultManagerSettings, newManager)
-import qualified Network.Wai.Handler.Warp        as Warp
-import           Prelude                         hiding
+import           Network.Socket
+                   (AddrInfoFlag(AI_NUMERICSERV, AI_NUMERICHOST),
+                   Socket, SocketType(Stream), addrAddress, addrFamily,
+                   addrFlags, addrProtocol, addrSocketType, close,
+                   connect, defaultHints, getAddrInfo, socket)
+import qualified Network.Wai.Handler.Warp      as Warp
+import           Prelude                       hiding
                    (elem)
 import qualified Prelude
 import           Servant
@@ -115,8 +120,6 @@
                    client, mkClientEnv, runClientM)
 import           Servant.Server
                    (Handler)
-import           System.IO
-                   (Handle, hClose)
 import           System.Process
                    (callProcess, readProcess)
 import           Test.QuickCheck
@@ -128,10 +131,10 @@
 import           Test.QuickCheck.Monadic
                    (monadic)
 import           UnliftIO
-                   (MonadIO, Async, liftIO, async, cancel, waitEither)
+                   (Async, MonadIO, async, cancel, liftIO, waitEither)
 
 import           Test.StateMachine
-import qualified Test.StateMachine.Types.Rank2   as Rank2
+import qualified Test.StateMachine.Types.Rank2 as Rank2
 
 ------------------------------------------------------------------------
 -- * User datatype
@@ -233,7 +236,7 @@
 
 
 
-data Action (r :: * -> *)
+data Action (r :: Type -> Type)
   = PostUser   User
   | GetUser    (Reference (Key User) r)
   | IncAgeUser (Reference (Key User) r)
@@ -243,8 +246,9 @@
 instance Rank2.Functor     Action where
 instance Rank2.Foldable    Action where
 instance Rank2.Traversable Action where
+instance CommandNames      Action where
 
-data Response (r :: * -> *)
+data Response (r :: Type -> Type)
   = PostedUser (Reference (Key User) r)
   | GotUser    (Maybe User)
   | IncedAgeUser
@@ -315,10 +319,10 @@
   , (2, DeleteUser <$> elements (map fst m))
   ]
 
-shrinker :: Action Symbolic -> [Action Symbolic]
-shrinker (PostUser (User user age)) =
+shrinker :: Model Symbolic -> Action Symbolic -> [Action Symbolic]
+shrinker _ (PostUser (User user age)) =
   [ PostUser (User user' age') | (user', age') <- shrink (user, age) ]
-shrinker _                          = []
+shrinker _ _                          = []
 
 ------------------------------------------------------------------------
 -- * The semantics.
@@ -494,13 +498,19 @@
 
     healthyDb :: String -> IO ()
     healthyDb ip = do
-      handle <- go 10
-      hClose handle
+      sock <- go 10
+      close sock
       where
-        go :: Int -> IO Handle
+        go :: Int -> IO Socket
         go 0 = error "healtyDb: db isn't healthy"
         go n = do
-          connectTo ip (PortNumber 5432)
+          let hints = defaultHints
+                { addrFlags      = [AI_NUMERICHOST , AI_NUMERICSERV]
+                , addrSocketType = Stream
+                }
+          addr : _ <- getAddrInfo (Just hints) (Just ip) (Just "5432")
+          sock <- socket (addrFamily addr) (addrSocketType addr) (addrProtocol addr)
+          (connect sock (addrAddress addr) >> return sock)
             `catch` (\(_ :: IOException) -> do
                         threadDelay 1000000
                         go (n - 1))
diff --git a/test/DieHard.hs b/test/DieHard.hs
--- a/test/DieHard.hs
+++ b/test/DieHard.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE DataKinds          #-}
 {-# LANGUAGE DeriveAnyClass     #-}
 {-# LANGUAGE DeriveGeneric      #-}
 {-# LANGUAGE FlexibleInstances  #-}
@@ -30,6 +31,8 @@
   , prop_dieHard
   ) where
 
+import           Data.Kind
+                   (Type)
 import           Data.TreeDiff
                    (ToExpr)
 import           GHC.Generics
@@ -50,7 +53,7 @@
 
 -- We start of defining the different actions that are allowed:
 
-data Command (r :: * -> *)
+data Command (r :: Type -> Type)
   = FillBig      -- Fill the 5-liter jug.
   | FillSmall    -- Fill the 3-liter jug.
   | EmptyBig     -- Empty the 5-liter jug.
@@ -58,9 +61,9 @@
   | SmallIntoBig -- Pour the contents of the 3-liter jug
                  -- into 5-liter jug.
   | BigIntoSmall
-  deriving (Eq, Show, Generic1, Rank2.Functor, Rank2.Foldable, Rank2.Traversable)
+  deriving (Eq, Show, Generic1, Rank2.Functor, Rank2.Foldable, Rank2.Traversable, CommandNames)
 
-data Response (r :: * -> *) = Done
+data Response (r :: Type -> Type) = Done
   deriving (Show, Generic1, Rank2.Foldable)
 
 ------------------------------------------------------------------------
@@ -68,7 +71,7 @@
 -- The model (or state) keeps track of what amount of water is in the
 -- two jugs.
 
-data Model (r :: * -> *) = Model
+data Model (r :: Type -> Type) = Model
   { bigJug   :: Int
   , smallJug :: Int
   } deriving (Show, Eq, Generic)
@@ -131,8 +134,8 @@
 
 -- There's nothing to shrink.
 
-shrinker :: Command r -> [Command r]
-shrinker _ = []
+shrinker :: Model r -> Command r -> [Command r]
+shrinker _ _ = []
 
 ------------------------------------------------------------------------
 
diff --git a/test/Echo.hs b/test/Echo.hs
--- a/test/Echo.hs
+++ b/test/Echo.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE DataKinds          #-}
 {-# LANGUAGE DeriveAnyClass     #-}
 {-# LANGUAGE DeriveGeneric      #-}
 {-# LANGUAGE FlexibleInstances  #-}
@@ -24,6 +25,8 @@
   )
   where
 
+import           Data.Kind
+                   (Type)
 import           Data.TreeDiff
                    (ToExpr)
 import           GHC.Generics
@@ -34,7 +37,7 @@
 import           Test.QuickCheck.Monadic
                    (monadicIO)
 import           UnliftIO
-                   (TVar, newTVarIO, readTVar, writeTVar, atomically)
+                   (TVar, atomically, newTVarIO, readTVar, writeTVar)
 
 import           Test.StateMachine
 import           Test.StateMachine.Types
@@ -129,8 +132,8 @@
           ]
 
       -- | Trivial shrinker.
-      mShrinker :: Action Symbolic -> [Action Symbolic]
-      mShrinker _ = []
+      mShrinker :: Model Symbolic -> Action Symbolic -> [Action Symbolic]
+      mShrinker _ _ = []
 
       -- | Here we'd do the dispatch to the actual SUT.
       mSemantics :: Action Concrete -> IO (Response Concrete)
@@ -152,7 +155,7 @@
 
 -- | The model contains the last string that was communicated in an input
 -- action.
-data Model (r :: * -> *)
+data Model (r :: Type -> Type)
     = -- | The model hasn't been initialized.
       Empty
     | -- | Last input string (a buffer with size one).
@@ -160,16 +163,16 @@
   deriving (Eq, Show, Generic)
 
 -- | Actions supported by the system.
-data Action (r :: * -> *)
+data Action (r :: Type -> Type)
     = -- | Input a string, which should be echoed later.
       In String
       -- | Request a string output.
     | Echo
-  deriving (Show, Generic1, Rank2.Foldable, Rank2.Traversable, Rank2.Functor)
+  deriving (Show, Generic1, Rank2.Foldable, Rank2.Traversable, Rank2.Functor, CommandNames)
 
 -- | The system gives a single type of output response, containing a string
 -- with the input previously received.
-data Response (r :: * -> *)
+data Response (r :: Type -> Type)
     = -- | Input acknowledgment.
       InAck
       -- | The previous action wasn't an input, so there is no input to echo.
diff --git a/test/ErrorEncountered.hs b/test/ErrorEncountered.hs
--- a/test/ErrorEncountered.hs
+++ b/test/ErrorEncountered.hs
@@ -1,8 +1,8 @@
-{-# LANGUAGE DeriveAnyClass       #-}
-{-# LANGUAGE DeriveGeneric        #-}
-{-# LANGUAGE FlexibleInstances    #-}
-{-# LANGUAGE PolyKinds            #-}
-{-# LANGUAGE StandaloneDeriving   #-}
+{-# LANGUAGE DeriveAnyClass     #-}
+{-# LANGUAGE DeriveGeneric      #-}
+{-# LANGUAGE FlexibleInstances  #-}
+{-# LANGUAGE PolyKinds          #-}
+{-# LANGUAGE StandaloneDeriving #-}
 
 module ErrorEncountered
   ( prop_error_sequential
@@ -13,8 +13,7 @@
 import           Data.Functor.Classes
                    (Eq1)
 import           Data.IORef
-                   (IORef, newIORef, readIORef,
-                   writeIORef)
+                   (IORef, newIORef, readIORef, writeIORef)
 import           Data.TreeDiff
                    (ToExpr)
 import           GHC.Generics
@@ -49,7 +48,7 @@
   = Create
   | Read  (Reference (Opaque (IORef Int)) r)
   | Write (Reference (Opaque (IORef Int)) r) Int
-  deriving (Eq, Generic1, Rank2.Functor, Rank2.Foldable, Rank2.Traversable)
+  deriving (Eq, Generic1, Rank2.Functor, Rank2.Foldable, Rank2.Traversable, CommandNames)
 
 deriving instance Show (Command Symbolic)
 deriving instance Show (Command Concrete)
@@ -78,11 +77,11 @@
 transition :: Eq1 r => Model r -> Command r -> Response r -> Model r
 transition ErrorEncountered _  _    = ErrorEncountered
 transition m@(Model model) cmd resp = case (cmd, resp) of
-  (Create, Created ref)        -> Model ((ref, 0) : model)
-  (Read _, ReadValue _)        -> m
-  (Write ref x, Written)       -> Model (update ref x model)
-  (Write _   _, WriteFailed)   -> ErrorEncountered
-  _                            -> error "transition: impossible."
+  (Create, Created ref)      -> Model ((ref, 0) : model)
+  (Read _, ReadValue _)      -> m
+  (Write ref x, Written)     -> Model (update ref x model)
+  (Write _   _, WriteFailed) -> ErrorEncountered
+  _                          -> error "transition: impossible."
 
 update :: Eq a => a -> b -> [(a, b)] -> [(a, b)]
 update ref i m = (ref, i) : filter ((/= ref) . fst) m
@@ -90,9 +89,9 @@
 precondition :: Model Symbolic -> Command Symbolic -> Logic
 precondition ErrorEncountered _ = Bot
 precondition (Model m) cmd = case cmd of
-  Create        -> Top
-  Read  ref     -> ref `elem` domain m
-  Write ref _   -> ref `elem` domain m
+  Create      -> Top
+  Read  ref   -> ref `elem` domain m
+  Write ref _ -> ref `elem` domain m
 
 postcondition :: Model Concrete -> Command Concrete -> Response Concrete -> Logic
 postcondition (Model m) cmd resp = case (cmd, resp) of
@@ -135,9 +134,9 @@
   ]
 generator ErrorEncountered = Nothing
 
-shrinker :: Command Symbolic -> [Command Symbolic]
-shrinker (Write ref i) = [ Write ref i' | i' <- shrink i ]
-shrinker _             = []
+shrinker :: Model Symbolic -> Command Symbolic -> [Command Symbolic]
+shrinker _ (Write ref i) = [ Write ref i' | i' <- shrink i ]
+shrinker _ _             = []
 
 sm :: StateMachine Model Command IO Response
 sm = StateMachine initModel transition precondition postcondition
diff --git a/test/MemoryReference.hs b/test/MemoryReference.hs
--- a/test/MemoryReference.hs
+++ b/test/MemoryReference.hs
@@ -53,7 +53,7 @@
   | Read  (Reference (Opaque (IORef Int)) r)
   | Write (Reference (Opaque (IORef Int)) r) Int
   | Increment (Reference (Opaque (IORef Int)) r)
-  deriving (Eq, Generic1, Rank2.Functor, Rank2.Foldable, Rank2.Traversable)
+  deriving (Eq, Generic1, Rank2.Functor, Rank2.Foldable, Rank2.Traversable, CommandNames)
 
 deriving instance Show (Command Symbolic)
 deriving instance Show (Command Concrete)
@@ -150,9 +150,9 @@
   , (4, Increment <$> elements (domain model))
   ]
 
-shrinker :: Command Symbolic -> [Command Symbolic]
-shrinker (Write ref i) = [ Write ref i' | i' <- shrink i ]
-shrinker _             = []
+shrinker :: Model Symbolic -> Command Symbolic -> [Command Symbolic]
+shrinker _ (Write ref i) = [ Write ref i' | i' <- shrink i ]
+shrinker _ _             = []
 
 sm :: Bug -> StateMachine Model Command IO Response
 sm bug = StateMachine initModel transition precondition postcondition
@@ -179,4 +179,4 @@
     where
       sm'  = sm None
       cmds = Commands
-        [ Types.Command (Read (Reference (Symbolic (Var 0)))) [] ]
+        [ Types.Command (Read (Reference (Symbolic (Var 0)))) (ReadValue 0) [] ]
diff --git a/test/ShrinkingProps.hs b/test/ShrinkingProps.hs
new file mode 100644
--- /dev/null
+++ b/test/ShrinkingProps.hs
@@ -0,0 +1,602 @@
+{-# LANGUAGE BangPatterns        #-}
+{-# LANGUAGE DeriveAnyClass      #-}
+{-# LANGUAGE DeriveFoldable      #-}
+{-# LANGUAGE DeriveFunctor       #-}
+{-# LANGUAGE DeriveGeneric       #-}
+{-# LANGUAGE DeriveTraversable   #-}
+{-# LANGUAGE FlexibleContexts    #-}
+{-# LANGUAGE FlexibleInstances   #-}
+{-# LANGUAGE ImplicitParams      #-}
+{-# LANGUAGE PolyKinds           #-}
+{-# LANGUAGE RecordWildCards     #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneDeriving  #-}
+{-# LANGUAGE TypeApplications    #-}
+{-# LANGUAGE TypeOperators       #-}
+
+module ShrinkingProps (
+    tests
+    -- Just to avoid compiler warnings
+  , ShrinkSeqFailure(..)
+  , ShrinkParFailure(..)
+  ) where
+
+import           Prelude                       hiding
+                   (elem)
+
+import           Control.Monad
+                   (replicateM)
+import           Control.Monad.Except
+                   (Except, runExcept, throwError)
+import           Control.Monad.State
+                   (State, gets, modify, runState, state)
+import           Data.Bifunctor
+                   (first)
+import           Data.Foldable
+                   (toList)
+import           Data.Functor.Classes
+                   (Eq1, Show1)
+import           Data.Map.Strict
+                   (Map)
+import qualified Data.Map.Strict               as Map
+import           Data.Monoid
+                   ((<>))
+import           Data.Proxy
+import           Data.Set
+                   (Set)
+import qualified Data.Set                      as Set
+import           Data.TreeDiff
+                   (ToExpr(..), defaultExprViaShow)
+import           Data.Typeable
+                   (Typeable)
+import           GHC.Generics
+                   (Generic, Generic1)
+import           GHC.Stack
+import           Text.Show.Pretty
+                   (ppShow)
+import           UnliftIO.STM
+
+import           Test.QuickCheck.Monadic
+                   (monadicIO)
+import           Test.Tasty
+import           Test.Tasty.QuickCheck
+                   (Arbitrary(..), Gen, Property, conjoin,
+                   counterexample, elements, getNonNegative, getSmall,
+                   oneof, property, testProperty, (===))
+
+import           Test.StateMachine
+import qualified Test.StateMachine.Parallel    as QSM
+import qualified Test.StateMachine.Sequential  as QSM
+import qualified Test.StateMachine.Types       as QSM
+import qualified Test.StateMachine.Types.Rank2 as Rank2
+import           Test.StateMachine.Utils
+                   (forAllShrinkShow)
+
+tests :: TestTree
+tests = testGroup "Shrinking properties" [
+      testProperty "Sanity check: standard sequential test"        prop_sequential
+    , testProperty "Sanity check: standard parallel test"          prop_parallel
+    , testProperty "Correct references after sequential shrinking" prop_sequential_subprog
+    , testProperty "Correct references after parallel shrinking"   prop_parallel_subprog
+    , testProperty "Correct references after parallel shrinking (buggyShrinkCmds)"   (prop_parallel_subprog' buggyShrinkCmds)
+    , testProperty "Sequential shrinker provides correct model"    prop_sequential_model
+    , testProperty "Parallel shrinker provides correct model"      prop_parallel_model
+    ]
+
+{-------------------------------------------------------------------------------
+  Example set up
+
+  This language is contrived, but designed to have lots of references, including
+  commands that /use/ a variable number of references and commands that /create/
+  a variable number of references.
+-------------------------------------------------------------------------------}
+
+-- | Unique command identifier
+--
+-- This is used when testing whether shrinking messes up references (see below)
+newtype CmdID = CmdID Int
+  deriving (Show, Eq, Ord, Generic)
+
+-- | Commands
+--
+-- Commands have two somewhat unusual features that are just here for the
+-- specific purpose of testing shrinking:
+--
+-- * The 'CmdID' fields are there so that we can build the reference graph
+--   (see 'RefGraph') below to check that shrinking does not mess up references.
+-- * The 'Maybe Model' field is there to check that the shrinker gets presented
+--   with the right model.
+data Cmd var =
+    -- | Create @n@ new mutable variables
+    CreateRef CmdID (Maybe (Model Symbolic)) Int
+
+    -- | Increment the value of the specified variables
+  | Incr CmdID (Maybe (Model Symbolic)) [var]
+
+    -- | Get the value of the specified variables
+  | Read CmdID (Maybe (Model Symbolic)) [var]
+  deriving (Show, Eq, Functor, Foldable, Traversable, Generic1, CommandNames)
+
+data Resp var =
+    Refs [var]
+  | Unit ()
+  | Vals [Int]
+  deriving (Show, Eq, Functor, Foldable, Traversable)
+
+cmdID :: Cmd var -> CmdID
+cmdID (CreateRef cid _ _) = cid
+cmdID (Incr      cid _ _) = cid
+cmdID (Read      cid _ _) = cid
+
+cmdModel :: Cmd var -> Maybe (Model Symbolic)
+cmdModel (CreateRef _ m _) = m
+cmdModel (Incr      _ m _) = m
+cmdModel (Read      _ m _) = m
+
+{-------------------------------------------------------------------------------
+  Mock implementation
+-------------------------------------------------------------------------------}
+
+-- | Mock variable
+newtype MockVar = MockVar Int
+  deriving (Show, Eq, Ord, Generic)
+
+-- | Mock system state
+newtype MockState = MockState (Map MockVar Int)
+  deriving (Show, Eq, Ord, Generic)
+
+newVar :: State MockState MockVar
+newVar = state $ \(MockState m) ->
+           let x = MockVar (Map.size m)
+           in (x, MockState (Map.insert x 0 m))
+
+incrVar :: MockVar -> State MockState ()
+incrVar x = modify $ \(MockState m) ->
+              let incr Nothing  = error "incrVar: undefined variable"
+                  incr (Just v) = Just (v + 1)
+              in MockState $ Map.alter incr x m
+
+readVar :: MockVar -> State MockState Int
+readVar x = gets $ \(MockState m) ->
+              case Map.lookup x m of
+                Just n  -> n
+                Nothing -> error $ "readVar: variable " ++ show x ++ " not found"
+
+runMock :: Cmd MockVar -> MockState -> (Resp MockVar, MockState)
+runMock (CreateRef _ _ n)  = first Refs . runState (replicateM n newVar)
+runMock (Incr      _ _ xs) = first Unit . runState (mapM_ incrVar xs)
+runMock (Read      _ _ xs) = first Vals . runState (mapM  readVar xs)
+
+{-------------------------------------------------------------------------------
+  I/O implementation
+
+  We use STM variables here so guarantee atomicity of 'Incr' command
+  (we are testing the shrinker, not looking for atomicity bugs! :)
+-------------------------------------------------------------------------------}
+
+data IOVar = IOVar String (TVar Int)
+  deriving (Eq)
+
+instance Show IOVar where
+  show (IOVar l _) = "<" ++ l ++ ">"
+
+newIOVar :: CmdID -> Int -> STM IOVar
+newIOVar cid n = IOVar (show (cid, n)) <$> newTVar 0
+
+incrIOVar :: IOVar -> STM ()
+incrIOVar (IOVar _ x) = modifyTVar x (+1)
+
+readIOVar :: IOVar -> STM Int
+readIOVar (IOVar _ x) = readTVar x
+
+runIO :: Cmd IOVar -> IO (Resp IOVar)
+runIO (CreateRef cid _ n)  = atomically $ Refs <$> mapM (newIOVar cid) [0 .. n - 1]
+runIO (Incr      _   _ xs) = atomically $ Unit <$> mapM_ incrIOVar xs
+runIO (Read      _   _ xs) = atomically $ Vals <$> mapM  readIOVar xs
+
+{-------------------------------------------------------------------------------
+  Instantiate to references
+-------------------------------------------------------------------------------}
+
+newtype At f r = At (f (Reference IOVar r))
+  deriving (Generic1, Rank2.Functor, Rank2.Foldable, Rank2.Traversable)
+
+type (:@) f r = At f r
+
+{-------------------------------------------------------------------------------
+  Model
+-------------------------------------------------------------------------------}
+
+type KnownRefs r = [(Reference IOVar r, MockVar)]
+
+resolveRef :: (Eq1 r, Show1 r, HasCallStack)
+           => KnownRefs r -> Reference IOVar r -> MockVar
+resolveRef refs r =
+    case lookup r refs of
+      Just x  -> x
+      Nothing -> error $ "resolveRef: reference " ++ show r
+                      ++ "not found in environment " ++ show refs
+
+-- | Model relating the mock state with the IO state
+--
+-- We include the CmdID so that we can reference it in the generator
+data Model r = Model MockState (KnownRefs r) CmdID
+  deriving (Generic, Eq)
+
+initModel :: Model r
+initModel = Model (MockState Map.empty) [] (CmdID 0)
+
+toMock :: (Eq1 r, Show1 r, Functor f, HasCallStack)
+       => Model r -> f :@ r -> f MockVar
+toMock (Model _ knownRefs _) (At fr) = fmap (resolveRef knownRefs) fr
+
+step :: (Eq1 r, Show1 r, HasCallStack) => Model r -> Cmd :@ r -> (Resp MockVar, MockState)
+step model@(Model mockState _ _) cmd =
+    let cs = callStack
+    in let ?callStack = pushCallStack ("<stepping " ++ show cmd ++ ">", here) cs
+       in runMock (toMock model cmd) mockState
+  where
+    here = SrcLoc "quickcheck-state-machine" "ShrinkingProps" "ShrinkingProps.hs" 0 0 0 0
+
+{-------------------------------------------------------------------------------
+  Events
+-------------------------------------------------------------------------------}
+
+data Event r = Event {
+    eventBefore   :: Model  r
+  , eventCmd      :: Cmd :@ r
+  , eventAfter    :: Model  r
+  , eventMockResp :: Resp MockVar
+  }
+
+event :: forall r. (Eq1 r, Show1 r, HasCallStack)
+      => Model  r
+      -> Cmd :@ r
+      -> (Resp MockVar -> KnownRefs r)
+      -> Event  r
+event model@(Model _ knownRefs (CmdID n)) cmd newRefs = Event {
+      eventBefore   = model
+    , eventCmd      = cmd
+    , eventAfter    = Model mock' (newRefs resp' ++ knownRefs) (CmdID (n + 1))
+    , eventMockResp = resp'
+    }
+  where
+    (resp', mock') = step model cmd
+
+lockstep :: (Eq1 r, Show1 r, HasCallStack)
+         => Model r -> Cmd :@ r -> Resp :@ r -> Event r
+lockstep model cmd (At resp) = event model cmd $ \resp' ->
+    zip (toList resp) (toList resp')
+
+{-------------------------------------------------------------------------------
+  Generator
+-------------------------------------------------------------------------------}
+
+generator :: Model Symbolic -> Maybe (Gen (Cmd :@ Symbolic))
+generator (Model _ knownRefs cid) = Just $ oneof [
+      At . CreateRef cid Nothing <$> small
+    , small >>= \n -> At . Incr cid Nothing <$> replicateM n pickRef
+    , small >>= \n -> At . Read cid Nothing <$> replicateM n pickRef
+    ]
+  where
+    pickRef :: Gen (Reference IOVar Symbolic)
+    pickRef = elements (map fst knownRefs)
+
+    small :: Gen Int
+    small = getSmall . getNonNegative <$> arbitrary
+
+-- | Shrinker
+--
+-- The only thing the shrinker does is record the model we are given as part
+-- of the shrunk command, so that we can check later we got the right model.
+shrinker :: Model Symbolic -> Cmd :@ Symbolic -> [Cmd :@ Symbolic]
+shrinker m (At cmd) =
+    case cmd of
+      CreateRef cid Nothing n  -> [At $ CreateRef cid (Just m) n ]
+      Incr      cid Nothing xs -> [At $ Incr      cid (Just m) xs]
+      Read      cid Nothing xs -> [At $ Read      cid (Just m) xs]
+      _otherwise               -> []
+
+{-------------------------------------------------------------------------------
+  The state machine
+-------------------------------------------------------------------------------}
+
+transition :: (Eq1 r, Show1 r) => Model r -> Cmd :@ r -> Resp :@ r -> Model r
+transition model cmd = eventAfter . lockstep model cmd
+
+precondition :: Model Symbolic -> Cmd :@ Symbolic -> Logic
+precondition (Model _ knownRefs _) (At cmd) =
+    forall (toList cmd) (`elem` map fst knownRefs)
+
+postcondition :: HasCallStack
+              => Model Concrete -> Cmd :@ Concrete -> Resp :@ Concrete -> Logic
+postcondition model cmd resp = toMock (eventAfter ev) resp .== eventMockResp ev
+  where
+    ev = lockstep model cmd resp
+
+mock :: Model Symbolic -> Cmd :@ Symbolic -> GenSym (Resp :@ Symbolic)
+mock model cmd = At <$> traverse (const QSM.genSym) resp
+  where
+    (resp, _mock') = step model cmd
+
+semantics :: Cmd :@ Concrete -> IO (Resp :@ Concrete)
+semantics (At cmd) = (At . fmap QSM.reference) <$> runIO (QSM.concrete <$> cmd)
+
+sm :: StateMachine Model (At Cmd) IO (At Resp)
+sm = QSM.StateMachine {
+         initModel     = initModel
+       , transition    = transition
+       , precondition  = precondition
+       , postcondition = postcondition
+       , generator     = generator
+       , shrinker      = shrinker
+       , semantics     = semantics
+       , mock          = mock
+       , invariant     = Nothing
+       , distribution  = Nothing
+       }
+
+{-------------------------------------------------------------------------------
+  The type class instances required by QSM
+-------------------------------------------------------------------------------}
+
+deriving instance Show1 r => Show (Cmd  :@ r)
+deriving instance Show1 r => Show (Resp :@ r)
+deriving instance Show1 r => Show (Model   r)
+
+instance CommandNames (At Cmd) where
+  cmdName  (At cmd) = cmdName cmd
+  cmdNames _        = cmdNames (Proxy @(Cmd ()))
+
+deriving instance ToExpr (Model Concrete)
+deriving instance ToExpr MockState
+deriving instance ToExpr MockVar
+deriving instance ToExpr CmdID
+
+instance ToExpr IOVar where
+  toExpr = defaultExprViaShow
+
+{-------------------------------------------------------------------------------
+  The standard QSM tests (as a sanity check)
+-------------------------------------------------------------------------------}
+
+prop_sequential :: Property
+prop_sequential = forAllCommands sm Nothing $ \cmds -> monadicIO $ do
+    (hist, _model, res) <- runCommands sm cmds
+    prettyCommands sm hist (checkCommandNames cmds (res === Ok))
+
+prop_parallel :: Property
+prop_parallel = forAllParallelCommands sm $ \cmds -> monadicIO $
+    prettyParallelCommands cmds =<< runParallelCommands sm cmds
+
+{-------------------------------------------------------------------------------
+  Test that shrinking does not mess up references
+
+  We do this by translating the program to use references of an alternative
+  shape: they explicitly say "the nth reference returned by command with ID id".
+  Since command IDs do not change during shrinking, the translated program
+  after shrinking should be a strict sublist of the translated original program.
+-------------------------------------------------------------------------------}
+
+data ExplicitRef = ExplicitRef CmdID Int
+  deriving (Show, Eq, Ord)
+
+type RefGraph = Map CmdID (Set ExplicitRef)
+
+isSubGraphOf :: RefGraph -> RefGraph -> Bool
+g `isSubGraphOf` g' = Map.isSubmapOfBy Set.isSubsetOf g g'
+
+refGraph :: HasCallStack => QSM.Commands (At Cmd) (At Resp) -> RefGraph
+refGraph (QSM.Commands cmds) = go Map.empty Map.empty cmds
+  where
+    go :: Map QSM.Var ExplicitRef
+       -> RefGraph
+       -> [QSM.Command (At Cmd) (At Resp)]
+       -> RefGraph
+    go _    !acc []                                     = acc
+    go refs !acc (QSM.Command (At cmd) _resp vars : cs) =
+        go (refs `union` newRefs)
+           (Map.insert (cmdID cmd) (Set.fromList $ map deref (toList cmd)) acc)
+           cs
+      where
+        deref :: Reference r Symbolic -> ExplicitRef
+        deref (QSM.Reference (QSM.Symbolic x)) =
+            case Map.lookup x refs of
+              Just r  -> r
+              Nothing -> error $ "deref: reference " ++ show x ++ " not found "
+                      ++ "in environment " ++ show refs
+                      ++ " with commands " ++ show cmds
+
+        newRefs :: Map QSM.Var ExplicitRef
+        newRefs = Map.fromList $ zipWith mkRef vars [0..]
+
+        -- When adding new 'QSM.Var's, check that they are not already present
+        -- in the map, as the same 'QSM.Var' may never be created by two
+        -- different commands.
+        union :: Map QSM.Var ExplicitRef -- ^ Known references
+              -> Map QSM.Var ExplicitRef -- ^ New references
+              -> Map QSM.Var ExplicitRef
+        union known new = foldr insertUnlessKnown known (Map.toList new)
+          where
+            insertUnlessKnown (var, newRef) =
+                Map.insertWith (\_ oldRef -> error $ mkMsg var oldRef newRef)
+                var newRef
+            mkMsg var oldRef newRef =   show var    ++
+              " created by "         ++ show oldRef ++
+              " already created by " ++ show newRef ++
+              " with commands\n"     ++ ppShow cmds
+
+
+        mkRef :: QSM.Var -> Int -> (QSM.Var, ExplicitRef)
+        mkRef x i = (x, ExplicitRef (cmdID cmd) i)
+
+data ShrinkSeqFailure = SSF {
+      ssfOrig     :: QSM.Commands (At Cmd) (At Resp)
+    , ssfShrunk   :: QSM.Commands (At Cmd) (At Resp)
+    , ssfGrOrig   :: RefGraph
+    , ssfGrShrunk :: RefGraph
+    }
+  deriving (Show)
+
+-- | Test that sequential shrinking results in a program whose reference
+-- graph is a subgraph of the reference graph of the original program
+--
+-- We don't use 'forAllCommands' directly as that would be circular (if the
+-- shrinker is broken, we don't want to use it to test the shrinker!).
+prop_sequential_subprog :: Property
+prop_sequential_subprog =
+    forAllShrinkShow (QSM.generateCommands sm Nothing) (const []) ppShow $ \cmds ->
+      let cmds' = refGraph cmds in
+      conjoin [ let shrunk' = refGraph shrunk in
+                counterexample (ppShow (SSF cmds shrunk cmds' shrunk')) $
+                  shrunk' `isSubGraphOf` cmds'
+              | shrunk <- QSM.shrinkCommands sm cmds
+              ]
+
+{-------------------------------------------------------------------------------
+  For parallel shrinking we do pretty much the same thing, we just need to
+  walk over all commands in 'ParallelCommands'
+-------------------------------------------------------------------------------}
+
+data ShrinkParFailure = SPF {
+      spfOrig     :: QSM.ParallelCommands (At Cmd) (At Resp)
+    , spfShrunk   :: QSM.ParallelCommands (At Cmd) (At Resp)
+    , spfTrOrig   :: RefGraph
+    , spfTrShrunk :: RefGraph
+    }
+  deriving (Show)
+
+-- | Compute reference graph for a parallel program
+--
+-- We do this by constructing the refernce graph of the sequential program
+-- where we execute the left and right part of all suffices in interleaved
+-- fashion.
+refGraph' :: HasCallStack => QSM.ParallelCommands (At Cmd) (At Resp) -> RefGraph
+refGraph' (QSM.ParallelCommands prefix suffixes) =
+    refGraph (prefix <> mconcat (map (\(QSM.Pair l r) -> l `mappend` r) suffixes))
+
+prop_parallel_subprog :: Property
+prop_parallel_subprog =
+    forAllShrinkShow (QSM.generateParallelCommands sm) (const []) ppShow $
+      prop_parallel_subprog'
+  where
+    -- TODO add as a test (?)
+    -- genCmds = return buggyShrinkCmds
+
+prop_parallel_subprog' :: QSM.ParallelCommands (At Cmd) (At Resp) -> Property
+prop_parallel_subprog' cmds =
+    conjoin [ let shrunk' = refGraph' shrunk in
+              counterexample (ppShow (SPF cmds shrunk cmds' shrunk')) $
+                shrunk' `isSubGraphOf` cmds'
+            | shrunk <- QSM.shrinkParallelCommands sm cmds
+            ]
+  where
+    cmds' = refGraph' cmds
+
+-- A set of valid commands to resulted in an invalid shrink
+buggyShrinkCmds :: QSM.ParallelCommands (At Cmd) (At Resp)
+buggyShrinkCmds = QSM.ParallelCommands (QSM.Commands [])
+    [ QSM.Pair (QSM.Commands [mkCreateRef 0 [0]])
+               (QSM.Commands [mkCreateRef 1 [1]])
+               -- This Var 1 was shrunk to Var 0
+    , QSM.Pair (QSM.Commands [mkRead 2 [0]])
+               (QSM.Commands [mkRead 3 [1]])
+    ]
+  where
+    mkCreateRef, mkRead :: Int -> [Int] -> QSM.Command (At Cmd) (At Resp)
+    mkCreateRef cid vars =
+      QSM.Command (At (CreateRef (CmdID cid) Nothing (length vars)))
+                  (At (Refs (map mkRef vars)))
+                  (map QSM.Var vars)
+    mkRead cid vars =
+      QSM.Command (At (Read (CmdID cid) Nothing (map mkRef vars)))
+                  (At (Vals (map (const 0) vars)))
+                  []
+
+    mkRef :: Typeable a => Int -> Reference a Symbolic
+    mkRef = QSM.Reference . QSM.Symbolic . QSM.Var
+
+
+{-------------------------------------------------------------------------------
+  Check that the shrinker gets presented with the right model
+-------------------------------------------------------------------------------}
+
+execCmd :: Model Symbolic -> QSM.Command (At Cmd) (At Resp) -> Event Symbolic
+execCmd model (QSM.Command cmd resp _) = lockstep model cmd resp
+
+checkCorrectModel :: QSM.Commands (At Cmd) (At Resp) -> Property
+checkCorrectModel cmds =
+    case runExcept (checkCorrectModel' initModel cmds) of
+      Left err -> counterexample err $ property False
+      Right _  -> property True
+
+-- | Verify that all commands have been paired with the right model
+-- (if they have been paired)
+--
+-- Returns the final model if successful.
+checkCorrectModel' :: Model Symbolic
+                   -> QSM.Commands (At Cmd) (At Resp)
+                   -> Except String (Model Symbolic)
+checkCorrectModel' = \model (QSM.Commands cmds) -> go model cmds
+  where
+    go :: Model Symbolic
+       -> [QSM.Command (At Cmd) (At Resp)]
+       -> Except String (Model Symbolic)
+    go m []       = return m
+    go m (c : cs) = do verifyModel m (cmdModel' c)
+                       go (eventAfter (execCmd m c)) cs
+
+    verifyModel :: Model Symbolic -> Maybe (Model Symbolic) -> Except String ()
+    verifyModel _ Nothing   = return ()
+    verifyModel m (Just m')
+                | m == m'   = return ()
+                | otherwise = throwError (show m ++ " /= " ++ show m')
+
+
+    cmdModel' :: QSM.Command (At Cmd) (At Resp) -> Maybe (Model Symbolic)
+    cmdModel' (QSM.Command (At cmd) _ _) = cmdModel cmd
+
+
+prop_sequential_model :: Property
+prop_sequential_model =
+    forAllShrinkShow (QSM.generateCommands sm Nothing) (const []) ppShow $ \cmds ->
+      conjoin [ checkCorrectModel shrunk
+              | shrunk <- QSM.shrinkCommands sm cmds
+              ]
+
+{-------------------------------------------------------------------------------
+  For the parallel case we do the same, but traversing the left and right
+  suffix separately
+-------------------------------------------------------------------------------}
+
+checkCorrectModelParallel :: QSM.ParallelCommands (At Cmd) (At Resp) -> Property
+checkCorrectModelParallel = \(QSM.ParallelCommands prefix suffixes) ->
+    case runExcept (go prefix suffixes) of
+      Left err -> counterexample err $ property False
+      Right () -> property True
+  where
+    go :: QSM.Commands (At Cmd) (At Resp)
+       -> [QSM.Pair (QSM.Commands (At Cmd) (At Resp))]
+       -> Except String ()
+    go prefix suffixes = do
+        modelAfterPrefix <- checkCorrectModel' initModel prefix
+        go' modelAfterPrefix suffixes
+
+    go' :: Model Symbolic
+        -> [QSM.Pair (QSM.Commands (At Cmd) (At Resp))]
+        -> Except String ()
+    go' _ []                        = return ()
+    go' m (QSM.Pair l r : suffixes) = do
+        modelAfterLeft <- checkCorrectModel' m l
+        -- The starting model for the right part is the /initial/ model:
+        -- it should not be affected by the left part
+        _ <- checkCorrectModel' m r
+        -- But when we check the /next/ suffix, /both/ parts have been executed
+        go' (QSM.advanceModel sm modelAfterLeft r) suffixes
+
+prop_parallel_model :: Property
+prop_parallel_model =
+    forAllShrinkShow (QSM.generateParallelCommands sm) (const []) ppShow $ \cmds ->
+      conjoin [ checkCorrectModelParallel shrunk
+              | shrunk <- QSM.shrinkParallelCommands sm cmds
+              ]
diff --git a/test/Spec.hs b/test/Spec.hs
--- a/test/Spec.hs
+++ b/test/Spec.hs
@@ -26,6 +26,7 @@
 import           Echo
 import           ErrorEncountered
 import           MemoryReference
+import qualified ShrinkingProps
 import           TicketDispenser
 
 ------------------------------------------------------------------------
@@ -33,6 +34,7 @@
 tests :: Bool -> TestTree
 tests docker0 = testGroup "Tests"
   [ testCase "Doctest Z module" (doctest ["src/Test/StateMachine/Z.hs"])
+  , ShrinkingProps.tests
   , testProperty "Die Hard"
       (expectFailure (withMaxSuccess 2000 prop_dieHard))
   , testGroup "Memory reference"
diff --git a/test/TicketDispenser.hs b/test/TicketDispenser.hs
--- a/test/TicketDispenser.hs
+++ b/test/TicketDispenser.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE DataKinds           #-}
 {-# LANGUAGE DeriveAnyClass      #-}
 {-# LANGUAGE DeriveGeneric       #-}
 {-# LANGUAGE FlexibleInstances   #-}
@@ -36,6 +37,8 @@
 
 import           Control.Exception
                    (IOException, catch)
+import           Data.Kind
+                   (Type)
 import           Data.TreeDiff
                    (ToExpr)
 import           GHC.Generics
@@ -65,12 +68,12 @@
 
 -- The actions of the ticket dispenser are:
 
-data Action (r :: * -> *)
+data Action (r :: Type -> Type)
   = TakeTicket
   | Reset
-  deriving (Show, Generic1, Rank2.Functor, Rank2.Foldable, Rank2.Traversable)
+  deriving (Show, Generic1, Rank2.Functor, Rank2.Foldable, Rank2.Traversable, CommandNames)
 
-data Response (r :: * -> *)
+data Response (r :: Type -> Type)
   = GotTicket Int
   | ResetOk
   deriving (Show, Generic1, Rank2.Foldable)
@@ -82,7 +85,7 @@
 
 -- The dispenser has to be reset before use, hence the maybe integer.
 
-newtype Model (r :: * -> *) = Model (Maybe Int)
+newtype Model (r :: Type -> Type) = Model (Maybe Int)
   deriving (Eq, Show, Generic)
 
 deriving instance ToExpr (Model Concrete)
@@ -116,8 +119,8 @@
   , (4, pure TakeTicket)
   ]
 
-shrinker :: Action Symbolic -> [Action Symbolic]
-shrinker _ = []
+shrinker :: Model Symbolic -> Action Symbolic -> [Action Symbolic]
+shrinker _ _ = []
 
 ------------------------------------------------------------------------