content: {-# LANGUAGE FlexibleContexts    #-}
  {-# LANGUAGE NamedFieldPuns      #-}
  {-# LANGUAGE Rank2Types          #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  
  -----------------------------------------------------------------------------
  -- |
  -- Module      :  Test.StateMachine.Parallel
  -- Copyright   :  (C) 2017, ATS Advanced Telematic Systems GmbH
  -- License     :  BSD-style (see the file LICENSE)
  --
  -- Maintainer  :  Stevan Andjelkovic <stevan.andjelkovic@strath.ac.uk>
  -- Stability   :  provisional
  -- Portability :  non-portable (GHC extensions)
  --
  -- This module contains helpers for generating, shrinking, and checking
  -- parallel programs.
  --
  -----------------------------------------------------------------------------
  
  module Test.StateMachine.Parallel
    ( forAllNParallelCommands
    , forAllParallelCommands
    , generateNParallelCommands
    , generateParallelCommands
    , shrinkNParallelCommands
    , shrinkParallelCommands
    , shrinkAndValidateNParallel
    , shrinkAndValidateParallel
    , shrinkCommands'
    , runNParallelCommands
    , runParallelCommands
    , runParallelCommands'
    , runNParallelCommandsNTimes
    , runParallelCommandsNTimes
    , runNParallelCommandsNTimes'
    , runParallelCommandsNTimes'
    , executeParallelCommands
    , linearise
    , toBoxDrawings
    , prettyNParallelCommands
    , prettyParallelCommands
    , prettyParallelCommandsWithOpts
    , prettyNParallelCommandsWithOpts
    , advanceModel
    , checkCommandNamesParallel
    , coverCommandNamesParallel
    , commandNamesParallel
    ) where
  
  import           Control.Monad
                     (replicateM, when)
  import           Control.Monad.Catch
                     (MonadMask, mask, onException)
  import           Control.Monad.State.Strict
                     (runStateT)
  import           Data.Bifunctor
                     (bimap)
  import           Data.Foldable
                     (toList)
  import           Data.List
                     (find, partition, permutations)
  import qualified Data.Map.Strict                   as Map
  import           Data.Maybe
                     (fromMaybe, mapMaybe)
  import           Data.Monoid
  import           Data.Set
                     (Set)
  import qualified Data.Set                          as S
  import           Data.Tree
                     (Tree(Node))
  import           Prelude
  import           Test.QuickCheck
                     (Gen, Property, Testable, choose, forAllShrinkShow,
                     property, sized)
  import           Test.QuickCheck.Monadic
                     (PropertyM, run)
  import           Text.PrettyPrint.ANSI.Leijen
                     (Doc)
  import           Text.Show.Pretty
                     (ppShow)
  import           UnliftIO
                     (MonadIO, MonadUnliftIO, concurrently,
                     forConcurrently, newTChanIO)
  
  import           Test.StateMachine.BoxDrawer
  import           Test.StateMachine.ConstructorName
  import           Test.StateMachine.DotDrawing
  import           Test.StateMachine.Logic
  import           Test.StateMachine.Sequential
  import           Test.StateMachine.Types
  import qualified Test.StateMachine.Types.Rank2     as Rank2
  import           Test.StateMachine.Utils
  
  ------------------------------------------------------------------------
  
  forAllParallelCommands :: Testable prop
                         => (Show (cmd Symbolic), Show (resp Symbolic), Show (model Symbolic))
                         => (Rank2.Traversable cmd, Rank2.Foldable resp)
                         => StateMachine model cmd m resp
                         -> Maybe Int
                         -> (ParallelCommands cmd resp -> prop)     -- ^ Predicate.
                         -> Property
  forAllParallelCommands sm mminSize =
    forAllShrinkShow (generateParallelCommands sm mminSize) (shrinkParallelCommands sm) ppShow
  
  
  forAllNParallelCommands :: Testable prop
                          => (Show (cmd Symbolic), Show (resp Symbolic), Show (model Symbolic))
                          => (Rank2.Traversable cmd, Rank2.Foldable resp)
                          => StateMachine model cmd m resp
                          -> Int                                      -- ^ Number of threads
                          -> (NParallelCommands cmd resp -> prop)     -- ^ Predicate.
                          -> Property
  forAllNParallelCommands sm np =
    forAllShrinkShow (generateNParallelCommands sm np) (shrinkNParallelCommands 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)
                           => (Show (cmd Symbolic), Show (resp Symbolic))
                           => StateMachine model cmd m resp
                           -> Maybe Int
                           -> Gen (ParallelCommands cmd resp)
  generateParallelCommands sm@StateMachine { initModel } mminSize  = do
    Commands cmds      <- generateCommands sm mminSize
    prefixLength       <- sized (\k -> choose (0, k `div` 3))
    let (prefix, rest) =  bimap Commands Commands (splitAt prefixLength cmds)
    return (ParallelCommands prefix
              (makeSuffixes (advanceModel sm initModel prefix) rest))
    where
      makeSuffixes :: model Symbolic -> Commands cmd resp -> [Pair (Commands cmd resp)]
      makeSuffixes model0 = go model0 [] . unCommands
        where
          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 sm model [] cmds
              (safe1, safe2) = splitAt (length safe `div` 2) safe
  
  -- 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 :: Rank2.Foldable resp
           => StateMachine model cmd m resp
           -> model Symbolic -> [Command cmd resp] -> [Command cmd resp]
           -> ([Command cmd resp], [Command cmd resp])
  spanSafe _ _     safe []           = (reverse safe, [])
  spanSafe sm model safe (cmd : cmds)
      | length safe <= 5
    , parallelSafe sm model (Commands (cmd : safe))
    = spanSafe sm model (cmd : safe) cmds
    | otherwise
    = (reverse safe, cmd : cmds)
  
  -- Generate Parallel commands. The length of each suffix, indicates how many thread can
  -- concurrently execute the commands safely.
  generateNParallelCommands :: forall model cmd m resp. Rank2.Foldable resp
                            => Show (model Symbolic)
                            => (Show (cmd Symbolic), Show (resp Symbolic))
                            => StateMachine model cmd m resp
                            -> Int
                            -> Gen (NParallelCommands cmd resp)
  generateNParallelCommands sm@StateMachine { initModel } np =
    if np <= 0 then error "number of threads must be positive" else 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 prefix) rest))
    where
      makeSuffixes :: model Symbolic -> Commands cmd resp -> [[(Commands cmd resp)]]
      makeSuffixes model0 = go model0 [] . unCommands
        where
          go :: model Symbolic
             -> [[(Commands cmd resp)]]
             -> [(Command cmd resp)]
             -> [[(Commands cmd resp)]]
          go _     acc []   = reverse acc
          go model acc cmds = go (advanceModel sm model (Commands safe))
                                 (safes : acc)
                                 rest
            where
              (safe, rest)   = spanSafe sm model [] cmds
              safes = Commands <$> chunksOf np (length safe `div` np) safe
  
          -- Split the list in n sublists, whose concat is the initial list.
          -- We try to keep the length of each sublist len.
          --
          -- It is important that we miss no elements here or else executeCommands may fail, because
          -- of missing references. It is also important that the final list has the correct length
          -- n, or else there will be different number of threads than the user specified.
          chunksOf :: Int -> Int -> [a] -> [[a]]
          chunksOf 1 _ xs = [xs]
          chunksOf n len xs = as : chunksOf (n-1) len bs
              where (as, bs) = splitAt len xs
  
  
  -- | A list of commands is parallel safe if the pre-conditions for all commands
  --   hold in all permutations of the list.
  parallelSafe :: Rank2.Foldable resp
               => StateMachine model cmd m resp -> model Symbolic
               -> Commands cmd resp -> Bool
  parallelSafe StateMachine { precondition, transition, mock } model0
    = all (preconditionsHold model0)
    . permutations
    . unCommands
    where
      preconditionsHold _     []                             = True
      preconditionsHold model (Command cmd resp vars : cmds) =
          boolean (precondition model cmd) &&
            preconditionsHold (transition model cmd resp) cmds &&
            -- This makes sure that in all permutations the length of variables created is the same.
            -- By doing so, we try to avoid MockSemanticsMismatch errors.
            -- More https://github.com/advancedtelematic/quickcheck-state-machine/pull/348
            length vars == length (getUsedVars $ fst $ runGenSym (mock model cmd) newCounter)
  
  -- | Apply the transition of some commands to a model.
  advanceModel :: StateMachine model cmd m resp
               -> model Symbolic      -- ^ The model.
               -> Commands cmd resp   -- ^ The commands.
               -> model Symbolic
  advanceModel StateMachine { transition } model0 =
    go model0 . unCommands
    where
      go model []                              = model
      go model (Command cmd resp _vars : cmds) =
          go (transition model cmd resp) cmds
  
  ------------------------------------------------------------------------
  
  -- | Shrink a parallel program in a pre-condition and scope respecting
  --   way.
  shrinkParallelCommands
    :: forall cmd model m resp. Rank2.Traversable cmd
    => Rank2.Foldable resp
    => StateMachine model cmd m resp
    -> (ParallelCommands cmd resp -> [ParallelCommands cmd resp])
  shrinkParallelCommands sm (ParallelCommands prefix suffixes)
    = concatMap go
        [ Shrunk s (ParallelCommands prefix' (map toPair suffixes'))
        | Shrunk s (prefix', suffixes') <- shrinkPairS shrinkCommands' shrinkSuffixes
                                                       (prefix, map fromPair suffixes)
        ]
        ++
        shrinkMoveSuffixToPrefix
    where
      go :: Shrunk (ParallelCommands cmd resp) -> [ParallelCommands cmd resp]
      go (Shrunk shrunk cmds) =
          shrinkAndValidateParallel sm
                                    (if shrunk then DontShrink else MustShrink)
                                    cmds
  
      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') ->
          [ ParallelCommands (prefix <> Commands [prefix'])
                             (fmap Commands (toPair suffix') : suffixes')
          | (prefix', suffix') <- pickOneReturnRest2 (unCommands (proj1 suffix),
                                                      unCommands (proj2 suffix))
          ]
  
  -- | Shrink a parallel program in a pre-condition and scope respecting
  --   way.
  shrinkNParallelCommands
    :: forall cmd model m resp. Rank2.Traversable cmd
    => Rank2.Foldable resp
    => StateMachine model cmd m resp
    -> (NParallelCommands cmd resp -> [NParallelCommands cmd resp])
  shrinkNParallelCommands sm (ParallelCommands prefix suffixes)
    = concatMap go
        [ Shrunk s (ParallelCommands prefix' suffixes')
        | Shrunk s (prefix', suffixes') <- shrinkPairS shrinkCommands' shrinkSuffixes
                                                       (prefix, suffixes)
        ]
        ++
        shrinkMoveSuffixToPrefix
    where
      go :: Shrunk (NParallelCommands cmd resp) -> [NParallelCommands cmd resp]
      go (Shrunk shrunk cmds) =
        shrinkAndValidateNParallel sm
                                         (if shrunk then DontShrink else MustShrink)
                                         cmds
  
      shrinkSuffixes :: [[Commands cmd resp]]
                     -> [Shrunk [[Commands cmd resp]]]
      shrinkSuffixes = shrinkListS (shrinkListS'' shrinkCommands')
  
      -- Moving a command from a suffix to the prefix preserves validity
      shrinkMoveSuffixToPrefix :: [NParallelCommands cmd resp]
      shrinkMoveSuffixToPrefix = case suffixes of
        []                   -> []
        (suffix : suffixes') ->
          [ ParallelCommands (prefix <> Commands [prefix'])
                             (fmap Commands suffix' : suffixes')
          | (prefix', suffix') <- pickOneReturnRestL (unCommands <$> suffix)
          ]
  
  -- | Shrinks Commands in a way that it has strictly less number of commands.
  shrinkCommands' :: Commands cmd resp -> [Shrunk (Commands cmd resp)]
  shrinkCommands' = map (fmap Commands) . shrinkListS' . unCommands
  
  shrinkAndValidateParallel :: forall model cmd m resp. (Rank2.Traversable cmd, Rank2.Foldable resp)
                            => StateMachine model cmd m resp
                            -> ShouldShrink
                            -> ParallelCommands cmd resp
                            -> [ParallelCommands cmd resp]
  shrinkAndValidateParallel sm@StateMachine { initModel } = \shouldShrink (ParallelCommands prefix suffixes) ->
      let env = initValidateEnv initModel
          curryGo shouldShrink' (env', prefix') = go prefix' env' shouldShrink' suffixes in
      case shouldShrink of
        DontShrink -> concatMap (curryGo DontShrink) (shrinkAndValidate sm DontShrink env prefix)
        MustShrink -> concatMap (curryGo DontShrink) (shrinkAndValidate sm MustShrink env prefix)
                   ++ concatMap (curryGo MustShrink) (shrinkAndValidate sm DontShrink env prefix)
    where
      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' = go' []
        where
          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) = do
              ((shrinkL, shrinkR), shrinkRest) <- shrinkOpts
              (envL, l') <- shrinkAndValidate sm shrinkL  env                         l
              (envR, r') <- shrinkAndValidate sm shrinkR (env `withCounterFrom` envL) r
              go' (Pair l' r' : acc) (combineEnv sm envL envR r') shrinkRest suffixes
            where
  
              shrinkOpts :: [((ShouldShrink, ShouldShrink), ShouldShrink)]
              shrinkOpts =
                  case shouldShrink of
                    DontShrink -> [ ((DontShrink, DontShrink), DontShrink) ]
                    MustShrink -> [ ((MustShrink, DontShrink), DontShrink)
                                  , ((DontShrink, MustShrink), DontShrink)
                                  , ((DontShrink, DontShrink), MustShrink) ]
  
  combineEnv :: StateMachine model cmd m resp
             -> ValidateEnv model
             -> ValidateEnv model
             -> Commands cmd resp
             -> ValidateEnv model
  combineEnv sm envL envR cmds = ValidateEnv {
        veModel   = advanceModel sm (veModel envL) cmds
      , veScope   = Map.union (veScope envL) (veScope envR)
      , veCounter = veCounter envR
      }
  
  withCounterFrom :: ValidateEnv model -> ValidateEnv model -> ValidateEnv model
  withCounterFrom e e' = e { veCounter = veCounter e' }
  
  shrinkAndValidateNParallel :: forall model cmd m resp. (Rank2.Traversable cmd, Rank2.Foldable resp)
                             => StateMachine model cmd m resp
                             -> ShouldShrink
                             -> NParallelCommands cmd resp
                             -> [NParallelCommands cmd resp]
  shrinkAndValidateNParallel sm = \shouldShrink  (ParallelCommands prefix suffixes) ->
      let env = initValidateEnv $ initModel sm
          curryGo shouldShrink' (env', prefix') = go prefix' env' shouldShrink' suffixes in
      case shouldShrink of
        DontShrink -> concatMap (curryGo DontShrink) (shrinkAndValidate sm DontShrink env prefix)
        MustShrink -> concatMap (curryGo DontShrink) (shrinkAndValidate sm MustShrink env prefix)
                   ++ concatMap (curryGo MustShrink) (shrinkAndValidate sm DontShrink env prefix)
    where
  
      go :: Commands cmd resp         -- validated prefix
         -> ValidateEnv model         -- environment after the prefix
         -> ShouldShrink              -- should we /still/ shrink something?
         -> [[Commands cmd resp]]     -- suffixes to validate
         -> [NParallelCommands cmd resp]
      go prefix' = go' []
        where
          go' :: [[Commands cmd resp]] -- accumulated validated suffixes (in reverse order)
              -> ValidateEnv model     -- environment after the validated suffixes
              -> ShouldShrink          -- should we /still/ shrink something?
              -> [[Commands cmd resp]] -- suffixes to validate
              -> [NParallelCommands cmd resp]
          go' _   _   MustShrink [] = [] -- Failed to shrink something
          go' acc _   DontShrink [] = [ParallelCommands prefix' (reverse acc)]
          go' acc env shouldShrink (suffix : suffixes) = do
              (suffixWithShrinks, shrinkRest) <- shrinkOpts suffix
              (envFinal, suffix') <- snd $ foldl f (True, [(env,[])]) suffixWithShrinks
              go' ((reverse suffix') : acc) envFinal shrinkRest suffixes
            where
  
              f :: (Bool, [(ValidateEnv model, [Commands cmd resp])])
                -> (ShouldShrink, Commands cmd resp)
                -> (Bool, [(ValidateEnv model, [Commands cmd resp])])
              f (firstCall, acc') (shrink, cmds) = (False, acc'')
                where
                      acc'' = do
                        (envPrev, cmdsPrev) <- acc'
                        let envUsed = if firstCall then env else env `withCounterFrom` envPrev
                        (env', cmd') <- shrinkAndValidate sm shrink envUsed cmds
                        let env'' = if firstCall then env' else
                              combineEnv sm envPrev env' cmd'
                        return (env'', cmd' : cmdsPrev)
  
              shrinkOpts :: [a] -> [([(ShouldShrink, a)], ShouldShrink)]
              shrinkOpts ls =
                let len = length ls
                    dontShrink = replicate len DontShrink
                    shrinks = if len == 0
                      then error "Invariant violation! A suffix should never be an empty list"
                      else flip map [1..len] $ \n ->
                          (replicate (n - 1) DontShrink) ++ [MustShrink] ++ (replicate (len - n) DontShrink)
                in case shouldShrink of
                    DontShrink -> [(zip dontShrink ls, DontShrink)]
                    MustShrink -> fmap (\shrinkLs -> (zip shrinkLs ls, DontShrink)) shrinks
                               ++ [(zip dontShrink ls, MustShrink)]
  
  ------------------------------------------------------------------------
  
  runParallelCommands :: (Show (cmd Concrete), Show (resp Concrete))
                      => (Rank2.Traversable cmd, Rank2.Foldable resp)
                      => (MonadMask m, MonadUnliftIO m)
                      => StateMachine model cmd m resp
                      -> ParallelCommands cmd resp
                      -> PropertyM m [(History cmd resp, Logic)]
  runParallelCommands = runParallelCommandsNTimes 10
  
  runParallelCommands' :: (Show (cmd Concrete), Show (resp Concrete))
                       => (Rank2.Traversable cmd, Rank2.Foldable resp)
                       => (MonadMask m, MonadUnliftIO m)
                       => StateMachine model cmd m resp
                       -> (cmd Concrete -> resp Concrete)
                       -> ParallelCommands cmd resp
                       -> PropertyM m [(History cmd resp, Logic)]
  runParallelCommands' = runParallelCommandsNTimes' 10
  
  runNParallelCommands :: (Show (cmd Concrete), Show (resp Concrete))
                       => (Rank2.Traversable cmd, Rank2.Foldable resp)
                       => (MonadMask m, MonadUnliftIO m)
                       => StateMachine model cmd m resp
                       -> NParallelCommands cmd resp
                       -> PropertyM m [(History cmd resp, Logic)]
  runNParallelCommands = runNParallelCommandsNTimes 10
  
  runParallelCommandsNTimes :: (Show (cmd Concrete), Show (resp Concrete))
                            => (Rank2.Traversable cmd, Rank2.Foldable resp)
                            => (MonadMask m, MonadUnliftIO m)
                            => Int -- ^ How many times to execute the parallel program.
                            -> StateMachine model cmd m resp
                            -> ParallelCommands cmd resp
                            -> PropertyM m [(History cmd resp, Logic)]
  runParallelCommandsNTimes n sm cmds =
    replicateM n $ do
      (hist, reason1, reason2) <- run (executeParallelCommands sm cmds True)
      return (hist, logicReason (combineReasons [reason1, reason2]) .&& linearise sm hist)
  
  runParallelCommandsNTimes' :: (Show (cmd Concrete), Show (resp Concrete))
                             => (Rank2.Traversable cmd, Rank2.Foldable resp)
                             => (MonadMask m, MonadUnliftIO m)
                             => Int -- ^ How many times to execute the parallel program.
                             -> StateMachine model cmd m resp
                             -> (cmd Concrete -> resp Concrete)
                             -> ParallelCommands cmd resp
                             -> PropertyM m [(History cmd resp, Logic)]
  runParallelCommandsNTimes' n sm complete cmds =
    replicateM n $ do
      (hist, _reason1, _reason2) <- run (executeParallelCommands sm cmds False)
      let hist' = completeHistory complete hist
      return (hist', linearise sm hist')
  
  runNParallelCommandsNTimes :: (Show (cmd Concrete), Show (resp Concrete))
                             => (Rank2.Traversable cmd, Rank2.Foldable resp)
                             => (MonadMask m, MonadUnliftIO m)
                             => Int -- ^ How many times to execute the parallel program.
                             -> StateMachine model cmd m resp
                             -> NParallelCommands cmd resp
                             -> PropertyM m [(History cmd resp, Logic)]
  runNParallelCommandsNTimes n sm cmds =
    replicateM n $ do
      (hist, reason) <- run (executeNParallelCommands sm cmds True)
      return (hist, logicReason reason .&& linearise sm hist)
  
  runNParallelCommandsNTimes' :: (Show (cmd Concrete), Show (resp Concrete))
                              => (Rank2.Traversable cmd, Rank2.Foldable resp)
                              => (MonadMask m, MonadUnliftIO m)
                              => Int -- ^ How many times to execute the parallel program.
                              -> StateMachine model cmd m resp
                              -> (cmd Concrete -> resp Concrete)
                              -> NParallelCommands cmd resp
                              -> PropertyM m [(History cmd resp, Logic)]
  runNParallelCommandsNTimes' n sm complete cmds =
    replicateM n $ do
      (hist, _reason) <- run (executeNParallelCommands sm cmds True)
      let hist' = completeHistory complete hist
      return (hist, linearise sm hist')
  
  executeParallelCommands :: (Show (cmd Concrete), Show (resp Concrete))
                          => (Rank2.Traversable cmd, Rank2.Foldable resp)
                          => (MonadMask m, MonadUnliftIO m)
                          => StateMachine model cmd m resp
                          -> ParallelCommands cmd resp
                          -> Bool
                          -> m (History cmd resp, Reason, Reason)
  executeParallelCommands sm@StateMachine{ initModel, cleanup } (ParallelCommands prefix suffixes) stopOnError =
    mask $ \restore -> do
      hchan <- restore newTChanIO
      (reason0, (env0, _smodel, _counter, _cmodel)) <- restore (runStateT
        (executeCommands sm hchan (Pid 0) CheckEverything prefix)
        (emptyEnvironment, initModel, newCounter, initModel))
          `onException` (getChanContents hchan >>= cleanup . mkModel sm . History)
      if reason0 /= Ok
      then do
        hist <- getChanContents hchan
        cleanup $ mkModel sm $ History hist
        return (History hist, reason0, reason0)
      else do
        (reason1, reason2, _) <- restore (go hchan (Ok, Ok, env0) suffixes)
          `onException` (getChanContents hchan >>= cleanup . mkModel sm . History)
        hist <- getChanContents hchan
        cleanup $ mkModel sm $ History hist
        return (History hist, reason1, reason2)
    where
      go _hchan (res1, res2, env) []                         = return (res1, res2, env)
      go hchan  (Ok,   Ok,   env) (Pair cmds1 cmds2 : pairs) = do
  
        ((reason1, (env1, _, _, _)), (reason2, (env2, _, _, _))) <- concurrently
  
          -- XXX: Post-conditions not checked, so we can pass in initModel here...
          -- It would be better if we made executeCommands take a Maybe Environment
          -- instead of the Check...
  
          (runStateT (executeCommands sm hchan (Pid 1) CheckNothing cmds1) (env, initModel, newCounter, initModel))
          (runStateT (executeCommands sm hchan (Pid 2) CheckNothing cmds2) (env, initModel, newCounter, initModel))
        case (isOK $ combineReasons [reason1, reason2], stopOnError) of
          (False, True) -> return (reason1, reason2, env1 <> env2)
          _ -> go hchan ( reason1
                        , reason2
                        , env1 <> env2
                        ) pairs
      go hchan (Ok, ExceptionThrown e, env) (Pair cmds1 _cmds2 : pairs) = do
  
        -- XXX: It's possible that pre-conditions fail at this point, because
        -- commands may depend on references that never got created in the crashed
        -- process. For example, consider:
        --
        --          x <- Create
        --    ------------+----------
        --    Write 1 x   | Write 2 x
        --    y <- Create |
        --    ------------+----------
        --    Write 3 x   | Write 4 y
        --                | Read x
        --
        -- If the @Write 1 x@ fails, @y@ will never be created and the
        -- pre-condition for @Write 4 y@ will fail. This also means that @Read x@
        -- will never get executed, and so there could be a bug in @Write@ that
        -- never gets discovered. Not sure if we can do something better here?
        --
        (reason1, (env1, _, _, _)) <- runStateT (executeCommands sm hchan (Pid 1) CheckPrecondition cmds1)
                                                (env, initModel, newCounter, initModel)
        go hchan ( reason1
                 , ExceptionThrown e
                 , env1
                 ) pairs
      go hchan (ExceptionThrown e, Ok, env) (Pair _cmds1 cmds2 : pairs) = do
  
        (reason2, (env2, _, _, _)) <- runStateT (executeCommands sm hchan (Pid 2) CheckPrecondition cmds2)
                                                (env, initModel, newCounter, initModel)
        go hchan ( ExceptionThrown e
                 , reason2
                 , env2
                 ) pairs
      go _hchan out@(ExceptionThrown _,     ExceptionThrown _,     _env) (_ : _) = return out
      go _hchan out@(PreconditionFailed {}, ExceptionThrown _,     _env) (_ : _) = return out
      go _hchan out@(ExceptionThrown _,     PreconditionFailed {}, _env) (_ : _) = return out
      go _hchan (res1, res2, _env) (Pair _cmds1 _cmds2 : _pairs) =
        error ("executeParallelCommands, unexpected result: " ++ show (res1, res2))
  
  logicReason :: Reason -> Logic
  logicReason Ok = Top
  logicReason r  = Annotate (show r) Bot
  
  executeNParallelCommands :: (Rank2.Traversable cmd, Show (cmd Concrete), Rank2.Foldable resp)
                           => Show (resp Concrete)
                           => (MonadMask m, MonadUnliftIO m)
                           => StateMachine model cmd m resp
                           -> NParallelCommands cmd resp
                           -> Bool
                           -> m (History cmd resp, Reason)
  executeNParallelCommands sm@StateMachine{ initModel, cleanup } (ParallelCommands prefix suffixes) stopOnError =
    mask $ \restore -> do
      hchan <- restore newTChanIO
      (reason0, (env0, _smodel, _counter, _cmodel)) <- restore (runStateT
        (executeCommands sm hchan (Pid 0) CheckEverything prefix)
        (emptyEnvironment, initModel, newCounter, initModel))
          `onException` (getChanContents hchan >>= cleanup . mkModel sm . History)
      if reason0 /= Ok
      then do
        hist <- getChanContents hchan
        cleanup $ mkModel sm $ History hist
        return (History hist, reason0)
      else do
        (errors, _) <- restore (go hchan (Map.empty, env0) suffixes)
          `onException` (getChanContents hchan >>= cleanup . mkModel sm . History)
        hist <- getChanContents hchan
        cleanup $ mkModel sm $ History hist
        return (History hist, combineReasons $ Map.elems errors)
    where
      go _ res [] = return res
      go hchan (previousErrors, env) (suffix : rest) = do
        when (isInvalid $ Map.elems previousErrors) $
          error ("executeNParallelCommands, unexpected result: " ++ show previousErrors)
  
        let noError = Map.null previousErrors
            check = if noError then CheckNothing else CheckPrecondition
        res <- forConcurrently (zip [1..] suffix) $ \(i, cmds) ->
          case Map.lookup i previousErrors of
            Nothing -> do
                (reason, (env', _, _, _)) <- runStateT (executeCommands sm hchan (Pid i) check cmds) (env, initModel, newCounter, initModel)
                return (if isOK reason then Nothing else Just (i, reason), env')
            Just _  -> return (Nothing, env)
        let newErrors = Map.fromList $ mapMaybe fst res
            errors = Map.union previousErrors newErrors
            newEnv = mconcat $ snd <$> res
        case (stopOnError, Map.null errors) of
          (True, False) -> return (errors, newEnv)
          _             -> go hchan (errors, newEnv) rest
  
  combineReasons :: [Reason] -> Reason
  combineReasons ls = fromMaybe Ok (find (/= Ok) ls)
  
  isInvalid :: [Reason] -> Bool
  isInvalid ls = any isPreconditionFailed ls &&
                 all notException ls
      where
        notException (ExceptionThrown _) = False
        notException _                   = True
  
  isPreconditionFailed :: Reason -> Bool
  isPreconditionFailed PreconditionFailed {} = True
  isPreconditionFailed _                     = False
  
  ------------------------------------------------------------------------
  
  -- | Try to linearise a history of a parallel program execution using a
  --   sequential model. See the *Linearizability: a correctness condition for
  --   concurrent objects* paper linked to from the README for more info.
  linearise :: forall model cmd m resp. (Show (cmd Concrete), Show (resp Concrete))
            => StateMachine model cmd m resp -> History cmd resp -> Logic
  linearise StateMachine { transition,  postcondition, initModel } = go . unHistory
    where
      go :: [(Pid, HistoryEvent cmd resp)] -> Logic
      go [] = Top
      go es = exists (interleavings es) (step initModel)
  
      step :: model Concrete -> Tree (Operation cmd resp) -> Logic
      step _model (Node (Crash _cmd _err _pid) _roses) =
        error "Not implemented yet, see issue #162 for more details."
      step model (Node (Operation cmd resp _) roses)   =
        postcondition model cmd resp .&&
          exists' roses (step (transition model cmd resp))
  
  exists' :: Show a => [a] -> (a -> Logic) -> Logic
  exists' [] _ = Top
  exists' xs p = exists xs p
  
  ------------------------------------------------------------------------
  
  -- | Takes the output of parallel program runs and pretty prints a
  --   counterexample if any of the runs fail.
  prettyParallelCommandsWithOpts :: (MonadIO m, Rank2.Foldable cmd)
                                => (Show (cmd Concrete), Show (resp Concrete))
                                => ParallelCommands cmd resp
                                -> Maybe GraphOptions
                                -> [(History cmd resp, Logic)] -- ^ Output of 'runParallelCommands'.
                                -> PropertyM m ()
  prettyParallelCommandsWithOpts cmds mGraphOptions =
    mapM_ (\(h, l) -> printCounterexample h (logic l) `whenFailM` property (boolean l))
      where
        printCounterexample hist' (VFalse ce) = do
          putStrLn ""
          print (toBoxDrawings cmds hist')
          putStrLn ""
          print (simplify ce)
          putStrLn ""
          case mGraphOptions of
            Nothing       -> return ()
            Just gOptions -> createAndPrintDot cmds gOptions hist'
        printCounterexample _hist _
          = error "prettyParallelCommands: impossible, because `boolean l` was False."
  
  simplify :: Counterexample -> Counterexample
  simplify (Fst ce@(AnnotateC _ BotC)) = ce
  simplify (Snd ce)                    = simplify ce
  simplify (ExistsC [] [])             = BotC
  simplify (ExistsC _ [Fst ce])        = ce
  simplify (ExistsC x (Fst ce : ces))  = ce `EitherC` simplify (ExistsC x ces)
  simplify (ExistsC _ (Snd ce : _))    = simplify ce
  simplify _                           = error "simplify: impossible,\
                                              \ because of the structure of linearise."
  
  prettyParallelCommands :: (Show (cmd Concrete), Show (resp Concrete))
                         => MonadIO m
                         => Rank2.Foldable cmd
                         => ParallelCommands cmd resp
                         -> [(History cmd resp, Logic)] -- ^ Output of 'runNParallelCommands'.
                         -> PropertyM m ()
  prettyParallelCommands cmds = prettyParallelCommandsWithOpts cmds Nothing
  
  -- | Takes the output of parallel program runs and pretty prints a
  --   counterexample if any of the runs fail.
  prettyNParallelCommandsWithOpts :: (Show (cmd Concrete), Show (resp Concrete))
                                  => MonadIO m
                                  => Rank2.Foldable cmd
                                  => NParallelCommands cmd resp
                                  -> Maybe GraphOptions
                                  -> [(History cmd resp, Logic)] -- ^ Output of 'runNParallelCommands'.
                                  -> PropertyM m ()
  prettyNParallelCommandsWithOpts cmds mGraphOptions =
     mapM_ (\(h, l) -> printCounterexample h (logic l) `whenFailM` property (boolean l))
      where
        printCounterexample hist' (VFalse ce) = do
          putStrLn ""
          print (simplify ce)
          putStrLn ""
          case mGraphOptions of
            Nothing       -> return ()
            Just gOptions -> createAndPrintDot cmds gOptions hist'
        printCounterexample _hist _
          = error "prettyNParallelCommands: impossible, because `boolean l` was False."
  
  prettyNParallelCommands :: (Show (cmd Concrete), Show (resp Concrete))
                          => MonadIO m
                          => Rank2.Foldable cmd
                          => NParallelCommands cmd resp
                          -> [(History cmd resp, Logic)] -- ^ Output of 'runNParallelCommands'.
                          -> PropertyM m ()
  prettyNParallelCommands cmds = prettyNParallelCommandsWithOpts cmds Nothing
  
  -- | Draw an ASCII diagram of the history of a parallel program. Useful for
  --   seeing how a race condition might have occured.
  toBoxDrawings :: forall cmd resp. Rank2.Foldable cmd
                => (Show (cmd Concrete), Show (resp Concrete))
                => ParallelCommands cmd resp -> History cmd resp -> Doc
  toBoxDrawings (ParallelCommands prefix suffixes) = toBoxDrawings'' allVars
    where
      allVars = getAllUsedVars prefix `S.union`
                  foldMap (foldMap getAllUsedVars) suffixes
  
      toBoxDrawings'' :: Set Var -> History cmd resp -> Doc
      toBoxDrawings'' knownVars (History h) = exec evT (fmap (out . snd) <$> Fork l p r)
        where
          (p, h') = partition (\e -> fst e == Pid 0) h
          (l, r)  = partition (\e -> fst e == Pid 1) h'
  
          out :: HistoryEvent cmd resp -> String
          out (Invocation cmd vars)
            | vars `S.isSubsetOf` knownVars = show (S.toList vars) ++ " ← " ++ show cmd
            | otherwise                     = show cmd
          out (Response resp) = show resp
          out (Exception err) = err
  
          toEventType :: History' cmd resp -> [(EventType, Pid)]
          toEventType = map go
            where
              go e = case e of
                (pid, Invocation _ _) -> (Open,  pid)
                (pid, Response   _)   -> (Close, pid)
                (pid, Exception  _)   -> (Close, pid)
  
          evT :: [(EventType, Pid)]
          evT = toEventType (filter (\e -> fst e `Prelude.elem` map Pid [1, 2]) h)
  
  createAndPrintDot :: forall cmd resp t. Foldable t => Rank2.Foldable cmd
                    => (Show (cmd Concrete), Show (resp Concrete))
                    => ParallelCommandsF t cmd resp
                    -> GraphOptions
                    -> History cmd resp
                    -> IO ()
  createAndPrintDot (ParallelCommands prefix suffixes) gOptions = toDotGraph allVars
    where
      allVars = getAllUsedVars prefix `S.union`
                  foldMap (foldMap getAllUsedVars) suffixes
  
      toDotGraph :: Set Var -> History cmd resp -> IO ()
      toDotGraph knownVars (History h) = printDotGraph gOptions $ (fmap out) <$> (Rose (snd <$> prefixMessages) groupByPid)
        where
          (prefixMessages, h') = partition (\e -> fst e == Pid 0) h
          alterF a Nothing   = Just [a]
          alterF a (Just ls) = Just $ a : ls
          groupByPid = foldr (\(p,e) m -> Map.alter (alterF e) p m) Map.empty h'
  
          out :: HistoryEvent cmd resp -> String
          out (Invocation cmd vars)
            | vars `S.isSubsetOf` knownVars = show (S.toList vars) ++ " ← " ++ show cmd
            | otherwise                     = show cmd
          out (Response resp) = " → " ++ show resp
          out (Exception err) = " → " ++ err
  
  
  getAllUsedVars :: Rank2.Foldable cmd => Commands cmd resp -> Set Var
  getAllUsedVars = S.fromList . foldMap (\(Command cmd _ _) -> getUsedVars cmd) . unCommands
  
  -- | Print the percentage of each command used. The prefix check is
  --   an unfortunate remaining for backwards compatibility.
  checkCommandNamesParallel :: forall cmd resp t. Foldable t => CommandNames cmd
                            => ParallelCommandsF t cmd resp -> Property -> Property
  checkCommandNamesParallel cmds = checkCommandNames $ toSequential cmds
  
  -- | Fail if some commands have not been executed.
  coverCommandNamesParallel :: forall cmd resp t. Foldable t => CommandNames cmd
                            => ParallelCommandsF t cmd resp -> Property -> Property
  coverCommandNamesParallel cmds = coverCommandNames $ toSequential cmds
  
  commandNamesParallel :: forall cmd resp t. Foldable t => CommandNames cmd
                       => ParallelCommandsF t cmd resp -> [(String, Int)]
  commandNamesParallel = commandNames . toSequential
  
  toSequential :: Foldable t => ParallelCommandsF t cmd resp -> Commands cmd resp
  toSequential cmds = prefix cmds <> mconcat (concatMap toList (suffixes cmds))
  