{-# LANGUAGE FlexibleContexts    #-}
{-# LANGUAGE NamedFieldPuns      #-}
{-# LANGUAGE Rank2Types          #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections       #-}

-----------------------------------------------------------------------------
-- |
-- 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.
--
-- Note that:
--
-- - the @.*NParallelCommands@ functions and the 'NParallelCommands' datatype
--   are expected to be used when you want to run @N@ concurrent threads running
--   at the same time and repeat each test 10 (by default) times to get
--   sufficient randomness on the RTS scheduling of concurrent actions.
--
-- - the @.*ParallelCommandsNTimes@ functions and the 'ParallelCommands'
--   datatype are expected to be used when you want to run the test with 2
--   concurrent threads and repeat each test @N@ times to get sufficient
--   randomness on the RTS scheduling of concurrent actions.
--
-- - the @.*NParallelCommandsNTime@ functions do both of the above points at the
--   same time, in particular they take an 'NParallelCommands' value generated
--   to be run by some number of threads concurrently, and they take as input
--   how many times each test should be repeated.
--
-- - the @run.*WithSetup@ functions receive a monadic action that must
--   initialize the StateMachine which will be used at the beginning of each
--   repetition of each sequence of commands. See the section in the
--   [README](https://github.com/stevana/quickcheck-state-machine#sut-initialization)
--   for more context.
--
-----------------------------------------------------------------------------

module Test.StateMachine.Parallel
  ( forAllNParallelCommands
  , forAllParallelCommands
  , generateNParallelCommands
  , generateParallelCommands
  , shrinkNParallelCommands
  , shrinkParallelCommands
  , shrinkAndValidateNParallel
  , shrinkAndValidateParallel
  , shrinkCommands'
  , runNParallelCommands
  , runNParallelCommandsWithSetup
  , runParallelCommands
  , runParallelCommandsWithSetup
  , runParallelCommands'
  , runNParallelCommandsNTimes
  , runNParallelCommandsNTimesWithSetup
  , runParallelCommandsNTimes
  , runParallelCommandsNTimesWithSetup
  , runNParallelCommandsNTimes'
  , runParallelCommandsNTimes'
  , executeParallelCommands
  , linearise
  , toBoxDrawings
  , prettyNParallelCommands
  , prettyParallelCommands
  , prettyParallelCommandsWithOpts
  , prettyNParallelCommandsWithOpts
  , advanceModel
  , checkCommandNamesParallel
  , coverCommandNamesParallel
  , commandNamesParallel
  ) where

import           Control.Monad
                   (replicateM, when)
import           Control.Monad.Catch
                   (MonadMask(..), ExitCase(..))
import           Control.Monad.State.Strict
                   (runStateT)
import           Data.Bifunctor
                   (bimap)
import           Data.Foldable
                   (toList)
import           Data.List
                   (find, partition, permutations, foldl')
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 qualified UnliftIO as UIO

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
import qualified Text.PrettyPrint.ANSI.Leijen as PP

------------------------------------------------------------------------

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 :: forall prop (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *)
       (model :: (* -> *) -> *) (m :: * -> *).
(Testable prop, Show (cmd Symbolic), Show (resp Symbolic),
 Show (model Symbolic), Traversable cmd, Foldable resp) =>
StateMachine model cmd m resp
-> Maybe Int -> (ParallelCommands cmd resp -> prop) -> Property
forAllParallelCommands StateMachine model cmd m resp
sm Maybe Int
mminSize =
  Gen (ParallelCommands cmd resp)
-> (ParallelCommands cmd resp -> [ParallelCommands cmd resp])
-> (ParallelCommands cmd resp -> String)
-> (ParallelCommands cmd resp -> prop)
-> Property
forall prop a.
Testable prop =>
Gen a -> (a -> [a]) -> (a -> String) -> (a -> prop) -> Property
forAllShrinkShow (StateMachine model cmd m resp
-> Maybe Int -> Gen (ParallelCommands cmd resp)
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
(Foldable resp, Show (model Symbolic), Show (cmd Symbolic),
 Show (resp Symbolic)) =>
StateMachine model cmd m resp
-> Maybe Int -> Gen (ParallelCommands cmd resp)
generateParallelCommands StateMachine model cmd m resp
sm Maybe Int
mminSize) (StateMachine model cmd m resp
-> ParallelCommands cmd resp -> [ParallelCommands cmd resp]
forall (cmd :: (* -> *) -> *) (model :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
(Traversable cmd, Foldable resp) =>
StateMachine model cmd m resp
-> ParallelCommands cmd resp -> [ParallelCommands cmd resp]
shrinkParallelCommands StateMachine model cmd m resp
sm) ParallelCommands cmd resp -> String
forall a. Show a => a -> String
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 :: forall prop (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *)
       (model :: (* -> *) -> *) (m :: * -> *).
(Testable prop, Show (cmd Symbolic), Show (resp Symbolic),
 Show (model Symbolic), Traversable cmd, Foldable resp) =>
StateMachine model cmd m resp
-> Int -> (NParallelCommands cmd resp -> prop) -> Property
forAllNParallelCommands StateMachine model cmd m resp
sm Int
np =
  Gen (NParallelCommands cmd resp)
-> (NParallelCommands cmd resp -> [NParallelCommands cmd resp])
-> (NParallelCommands cmd resp -> String)
-> (NParallelCommands cmd resp -> prop)
-> Property
forall prop a.
Testable prop =>
Gen a -> (a -> [a]) -> (a -> String) -> (a -> prop) -> Property
forAllShrinkShow (StateMachine model cmd m resp
-> Int -> Gen (NParallelCommands cmd resp)
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
(Foldable resp, Show (model Symbolic), Show (cmd Symbolic),
 Show (resp Symbolic)) =>
StateMachine model cmd m resp
-> Int -> Gen (NParallelCommands cmd resp)
generateNParallelCommands StateMachine model cmd m resp
sm Int
np) (StateMachine model cmd m resp
-> NParallelCommands cmd resp -> [NParallelCommands cmd resp]
forall (cmd :: (* -> *) -> *) (model :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
(Traversable cmd, Foldable resp) =>
StateMachine model cmd m resp
-> NParallelCommands cmd resp -> [NParallelCommands cmd resp]
shrinkNParallelCommands StateMachine model cmd m resp
sm) NParallelCommands cmd resp -> String
forall a. Show a => a -> String
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 :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
(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 model cmd m resp
sm@StateMachine { forall (r :: * -> *). model r
initModel :: forall (r :: * -> *). model r
initModel :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> forall (r :: * -> *). model r
initModel } Maybe Int
mminSize  = do
  Commands [Command cmd resp]
cmds      <- StateMachine model cmd m resp
-> Maybe Int -> Gen (Commands cmd resp)
forall (resp :: (* -> *) -> *) (model :: (* -> *) -> *)
       (cmd :: (* -> *) -> *) (m :: * -> *).
(Foldable resp, Show (model Symbolic), Show (cmd Symbolic),
 Show (resp Symbolic)) =>
StateMachine model cmd m resp
-> Maybe Int -> Gen (Commands cmd resp)
generateCommands StateMachine model cmd m resp
sm Maybe Int
mminSize
  Int
prefixLength       <- (Int -> Gen Int) -> Gen Int
forall a. (Int -> Gen a) -> Gen a
sized (\Int
k -> (Int, Int) -> Gen Int
forall a. Random a => (a, a) -> Gen a
choose (Int
0, Int
k Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
3))
  let (Commands cmd resp
prefix, Commands cmd resp
rest) =  ([Command cmd resp] -> Commands cmd resp)
-> ([Command cmd resp] -> Commands cmd resp)
-> ([Command cmd resp], [Command cmd resp])
-> (Commands cmd resp, Commands cmd resp)
forall a b c d. (a -> b) -> (c -> d) -> (a, c) -> (b, d)
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap [Command cmd resp] -> Commands cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
[Command cmd resp] -> Commands cmd resp
Commands [Command cmd resp] -> Commands cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
[Command cmd resp] -> Commands cmd resp
Commands (Int
-> [Command cmd resp] -> ([Command cmd resp], [Command cmd resp])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
prefixLength [Command cmd resp]
cmds)
  ParallelCommands cmd resp -> Gen (ParallelCommands cmd resp)
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (Commands cmd resp
-> [Pair (Commands cmd resp)] -> ParallelCommands cmd resp
forall (t :: * -> *) (cmd :: (* -> *) -> *)
       (resp :: (* -> *) -> *).
Commands cmd resp
-> [t (Commands cmd resp)] -> ParallelCommandsF t cmd resp
ParallelCommands Commands cmd resp
prefix
            (model Symbolic -> Commands cmd resp -> [Pair (Commands cmd resp)]
makeSuffixes (StateMachine model cmd m resp
-> model Symbolic -> Commands cmd resp -> model Symbolic
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> model Symbolic -> Commands cmd resp -> model Symbolic
advanceModel StateMachine model cmd m resp
sm model Symbolic
forall (r :: * -> *). model r
initModel Commands cmd resp
prefix) Commands cmd resp
rest))
  where
    makeSuffixes :: model Symbolic -> Commands cmd resp -> [Pair (Commands cmd resp)]
    makeSuffixes :: model Symbolic -> Commands cmd resp -> [Pair (Commands cmd resp)]
makeSuffixes model Symbolic
model0 = model Symbolic
-> [Pair (Commands cmd resp)]
-> [Command cmd resp]
-> [Pair (Commands cmd resp)]
go model Symbolic
model0 [] ([Command cmd resp] -> [Pair (Commands cmd resp)])
-> (Commands cmd resp -> [Command cmd resp])
-> Commands cmd resp
-> [Pair (Commands cmd resp)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Commands cmd resp -> [Command cmd resp]
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
Commands cmd resp -> [Command cmd resp]
unCommands
      where
        go :: model Symbolic
-> [Pair (Commands cmd resp)]
-> [Command cmd resp]
-> [Pair (Commands cmd resp)]
go model Symbolic
_     [Pair (Commands cmd resp)]
acc []   = [Pair (Commands cmd resp)] -> [Pair (Commands cmd resp)]
forall a. [a] -> [a]
reverse [Pair (Commands cmd resp)]
acc
        go model Symbolic
model [Pair (Commands cmd resp)]
acc [Command cmd resp]
cmds = model Symbolic
-> [Pair (Commands cmd resp)]
-> [Command cmd resp]
-> [Pair (Commands cmd resp)]
go (StateMachine model cmd m resp
-> model Symbolic -> Commands cmd resp -> model Symbolic
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> model Symbolic -> Commands cmd resp -> model Symbolic
advanceModel StateMachine model cmd m resp
sm model Symbolic
model ([Command cmd resp] -> Commands cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
[Command cmd resp] -> Commands cmd resp
Commands [Command cmd resp]
safe))
                               (Commands cmd resp -> Commands cmd resp -> Pair (Commands cmd resp)
forall a. a -> a -> Pair a
Pair ([Command cmd resp] -> Commands cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
[Command cmd resp] -> Commands cmd resp
Commands [Command cmd resp]
safe1) ([Command cmd resp] -> Commands cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
[Command cmd resp] -> Commands cmd resp
Commands [Command cmd resp]
safe2) Pair (Commands cmd resp)
-> [Pair (Commands cmd resp)] -> [Pair (Commands cmd resp)]
forall a. a -> [a] -> [a]
: [Pair (Commands cmd resp)]
acc)
                               [Command cmd resp]
rest
          where
            ([Command cmd resp]
safe, [Command cmd resp]
rest)   = StateMachine model cmd m resp
-> model Symbolic
-> [Command cmd resp]
-> [Command cmd resp]
-> ([Command cmd resp], [Command cmd resp])
forall (resp :: (* -> *) -> *) (model :: (* -> *) -> *)
       (cmd :: (* -> *) -> *) (m :: * -> *).
Foldable resp =>
StateMachine model cmd m resp
-> model Symbolic
-> [Command cmd resp]
-> [Command cmd resp]
-> ([Command cmd resp], [Command cmd resp])
spanSafe StateMachine model cmd m resp
sm model Symbolic
model [] [Command cmd resp]
cmds
            ([Command cmd resp]
safe1, [Command cmd resp]
safe2) = Int
-> [Command cmd resp] -> ([Command cmd resp], [Command cmd resp])
forall a. Int -> [a] -> ([a], [a])
splitAt ([Command cmd resp] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Command cmd resp]
safe Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
2) [Command cmd resp]
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 :: forall (resp :: (* -> *) -> *) (model :: (* -> *) -> *)
       (cmd :: (* -> *) -> *) (m :: * -> *).
Foldable resp =>
StateMachine model cmd m resp
-> model Symbolic
-> [Command cmd resp]
-> [Command cmd resp]
-> ([Command cmd resp], [Command cmd resp])
spanSafe StateMachine model cmd m resp
_ model Symbolic
_     [Command cmd resp]
safe []           = ([Command cmd resp] -> [Command cmd resp]
forall a. [a] -> [a]
reverse [Command cmd resp]
safe, [])
spanSafe StateMachine model cmd m resp
sm model Symbolic
model [Command cmd resp]
safe (Command cmd resp
cmd : [Command cmd resp]
cmds)
    | [Command cmd resp] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Command cmd resp]
safe Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
5
  , StateMachine model cmd m resp
-> model Symbolic -> Commands cmd resp -> Bool
forall (resp :: (* -> *) -> *) (model :: (* -> *) -> *)
       (cmd :: (* -> *) -> *) (m :: * -> *).
Foldable resp =>
StateMachine model cmd m resp
-> model Symbolic -> Commands cmd resp -> Bool
parallelSafe StateMachine model cmd m resp
sm model Symbolic
model ([Command cmd resp] -> Commands cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
[Command cmd resp] -> Commands cmd resp
Commands (Command cmd resp
cmd Command cmd resp -> [Command cmd resp] -> [Command cmd resp]
forall a. a -> [a] -> [a]
: [Command cmd resp]
safe))
  = StateMachine model cmd m resp
-> model Symbolic
-> [Command cmd resp]
-> [Command cmd resp]
-> ([Command cmd resp], [Command cmd resp])
forall (resp :: (* -> *) -> *) (model :: (* -> *) -> *)
       (cmd :: (* -> *) -> *) (m :: * -> *).
Foldable resp =>
StateMachine model cmd m resp
-> model Symbolic
-> [Command cmd resp]
-> [Command cmd resp]
-> ([Command cmd resp], [Command cmd resp])
spanSafe StateMachine model cmd m resp
sm model Symbolic
model (Command cmd resp
cmd Command cmd resp -> [Command cmd resp] -> [Command cmd resp]
forall a. a -> [a] -> [a]
: [Command cmd resp]
safe) [Command cmd resp]
cmds
  | Bool
otherwise
  = ([Command cmd resp] -> [Command cmd resp]
forall a. [a] -> [a]
reverse [Command cmd resp]
safe, Command cmd resp
cmd Command cmd resp -> [Command cmd resp] -> [Command cmd resp]
forall a. a -> [a] -> [a]
: [Command cmd resp]
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 :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
(Foldable resp, Show (model Symbolic), Show (cmd Symbolic),
 Show (resp Symbolic)) =>
StateMachine model cmd m resp
-> Int -> Gen (NParallelCommands cmd resp)
generateNParallelCommands sm :: StateMachine model cmd m resp
sm@StateMachine { forall (r :: * -> *). model r
initModel :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> forall (r :: * -> *). model r
initModel :: forall (r :: * -> *). model r
initModel } Int
np =
  if Int
np Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0 then String -> Gen (NParallelCommands cmd resp)
forall a. HasCallStack => String -> a
error String
"number of threads must be positive" else do
  Commands [Command cmd resp]
cmds      <- StateMachine model cmd m resp
-> Maybe Int -> Gen (Commands cmd resp)
forall (resp :: (* -> *) -> *) (model :: (* -> *) -> *)
       (cmd :: (* -> *) -> *) (m :: * -> *).
(Foldable resp, Show (model Symbolic), Show (cmd Symbolic),
 Show (resp Symbolic)) =>
StateMachine model cmd m resp
-> Maybe Int -> Gen (Commands cmd resp)
generateCommands StateMachine model cmd m resp
sm Maybe Int
forall a. Maybe a
Nothing
  Int
prefixLength       <- (Int -> Gen Int) -> Gen Int
forall a. (Int -> Gen a) -> Gen a
sized (\Int
k -> (Int, Int) -> Gen Int
forall a. Random a => (a, a) -> Gen a
choose (Int
0, Int
k Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
3))
  let (Commands cmd resp
prefix, Commands cmd resp
rest) =  ([Command cmd resp] -> Commands cmd resp)
-> ([Command cmd resp] -> Commands cmd resp)
-> ([Command cmd resp], [Command cmd resp])
-> (Commands cmd resp, Commands cmd resp)
forall a b c d. (a -> b) -> (c -> d) -> (a, c) -> (b, d)
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap [Command cmd resp] -> Commands cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
[Command cmd resp] -> Commands cmd resp
Commands [Command cmd resp] -> Commands cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
[Command cmd resp] -> Commands cmd resp
Commands (Int
-> [Command cmd resp] -> ([Command cmd resp], [Command cmd resp])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
prefixLength [Command cmd resp]
cmds)
  NParallelCommands cmd resp -> Gen (NParallelCommands cmd resp)
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (Commands cmd resp
-> [[Commands cmd resp]] -> NParallelCommands cmd resp
forall (t :: * -> *) (cmd :: (* -> *) -> *)
       (resp :: (* -> *) -> *).
Commands cmd resp
-> [t (Commands cmd resp)] -> ParallelCommandsF t cmd resp
ParallelCommands Commands cmd resp
prefix
            (model Symbolic -> Commands cmd resp -> [[Commands cmd resp]]
makeSuffixes (StateMachine model cmd m resp
-> model Symbolic -> Commands cmd resp -> model Symbolic
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> model Symbolic -> Commands cmd resp -> model Symbolic
advanceModel StateMachine model cmd m resp
sm model Symbolic
forall (r :: * -> *). model r
initModel Commands cmd resp
prefix) Commands cmd resp
rest))
  where
    makeSuffixes :: model Symbolic -> Commands cmd resp -> [[Commands cmd resp]]
    makeSuffixes :: model Symbolic -> Commands cmd resp -> [[Commands cmd resp]]
makeSuffixes model Symbolic
model0 = model Symbolic
-> [[Commands cmd resp]]
-> [Command cmd resp]
-> [[Commands cmd resp]]
go model Symbolic
model0 [] ([Command cmd resp] -> [[Commands cmd resp]])
-> (Commands cmd resp -> [Command cmd resp])
-> Commands cmd resp
-> [[Commands cmd resp]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Commands cmd resp -> [Command cmd resp]
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
Commands cmd resp -> [Command cmd resp]
unCommands
      where
        go :: model Symbolic
           -> [[Commands cmd resp]]
           -> [Command cmd resp]
           -> [[Commands cmd resp]]
        go :: model Symbolic
-> [[Commands cmd resp]]
-> [Command cmd resp]
-> [[Commands cmd resp]]
go model Symbolic
_     [[Commands cmd resp]]
acc []   = [[Commands cmd resp]] -> [[Commands cmd resp]]
forall a. [a] -> [a]
reverse [[Commands cmd resp]]
acc
        go model Symbolic
model [[Commands cmd resp]]
acc [Command cmd resp]
cmds = model Symbolic
-> [[Commands cmd resp]]
-> [Command cmd resp]
-> [[Commands cmd resp]]
go (StateMachine model cmd m resp
-> model Symbolic -> Commands cmd resp -> model Symbolic
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> model Symbolic -> Commands cmd resp -> model Symbolic
advanceModel StateMachine model cmd m resp
sm model Symbolic
model ([Command cmd resp] -> Commands cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
[Command cmd resp] -> Commands cmd resp
Commands [Command cmd resp]
safe))
                               ([Commands cmd resp]
safes [Commands cmd resp]
-> [[Commands cmd resp]] -> [[Commands cmd resp]]
forall a. a -> [a] -> [a]
: [[Commands cmd resp]]
acc)
                               [Command cmd resp]
rest
          where
            ([Command cmd resp]
safe, [Command cmd resp]
rest)   = StateMachine model cmd m resp
-> model Symbolic
-> [Command cmd resp]
-> [Command cmd resp]
-> ([Command cmd resp], [Command cmd resp])
forall (resp :: (* -> *) -> *) (model :: (* -> *) -> *)
       (cmd :: (* -> *) -> *) (m :: * -> *).
Foldable resp =>
StateMachine model cmd m resp
-> model Symbolic
-> [Command cmd resp]
-> [Command cmd resp]
-> ([Command cmd resp], [Command cmd resp])
spanSafe StateMachine model cmd m resp
sm model Symbolic
model [] [Command cmd resp]
cmds
            safes :: [Commands cmd resp]
safes = [Command cmd resp] -> Commands cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
[Command cmd resp] -> Commands cmd resp
Commands ([Command cmd resp] -> Commands cmd resp)
-> [[Command cmd resp]] -> [Commands cmd resp]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Int -> [Command cmd resp] -> [[Command cmd resp]]
forall a. Int -> Int -> [a] -> [[a]]
chunksOf Int
np ([Command cmd resp] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Command cmd resp]
safe Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
np) [Command cmd resp]
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 :: forall a. Int -> Int -> [a] -> [[a]]
chunksOf Int
1 Int
_ [a]
xs = [[a]
xs]
        chunksOf Int
n Int
len [a]
xs = [a]
as [a] -> [[a]] -> [[a]]
forall a. a -> [a] -> [a]
: Int -> Int -> [a] -> [[a]]
forall a. Int -> Int -> [a] -> [[a]]
chunksOf (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) Int
len [a]
bs
            where ([a]
as, [a]
bs) = Int -> [a] -> ([a], [a])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
len [a]
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 :: forall (resp :: (* -> *) -> *) (model :: (* -> *) -> *)
       (cmd :: (* -> *) -> *) (m :: * -> *).
Foldable resp =>
StateMachine model cmd m resp
-> model Symbolic -> Commands cmd resp -> Bool
parallelSafe StateMachine { model Symbolic -> cmd Symbolic -> Logic
precondition :: model Symbolic -> cmd Symbolic -> Logic
precondition :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> model Symbolic -> cmd Symbolic -> Logic
precondition, forall (r :: * -> *).
(Show1 r, Ord1 r) =>
model r -> cmd r -> resp r -> model r
transition :: forall (r :: * -> *).
(Show1 r, Ord1 r) =>
model r -> cmd r -> resp r -> model r
transition :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> forall (r :: * -> *).
   (Show1 r, Ord1 r) =>
   model r -> cmd r -> resp r -> model r
transition, model Symbolic -> cmd Symbolic -> GenSym (resp Symbolic)
mock :: model Symbolic -> cmd Symbolic -> GenSym (resp Symbolic)
mock :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> model Symbolic -> cmd Symbolic -> GenSym (resp Symbolic)
mock } model Symbolic
model0
  = ([Command cmd resp] -> Bool) -> [[Command cmd resp]] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (model Symbolic -> [Command cmd resp] -> Bool
preconditionsHold model Symbolic
model0)
  ([[Command cmd resp]] -> Bool)
-> (Commands cmd resp -> [[Command cmd resp]])
-> Commands cmd resp
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Command cmd resp] -> [[Command cmd resp]]
forall a. [a] -> [[a]]
permutations
  ([Command cmd resp] -> [[Command cmd resp]])
-> (Commands cmd resp -> [Command cmd resp])
-> Commands cmd resp
-> [[Command cmd resp]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Commands cmd resp -> [Command cmd resp]
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
Commands cmd resp -> [Command cmd resp]
unCommands
  where
    preconditionsHold :: model Symbolic -> [Command cmd resp] -> Bool
preconditionsHold model Symbolic
_     []                             = Bool
True
    preconditionsHold model Symbolic
model (Command cmd Symbolic
cmd resp Symbolic
resp [Var]
vars : [Command cmd resp]
cmds) =
        Logic -> Bool
boolean (model Symbolic -> cmd Symbolic -> Logic
precondition model Symbolic
model cmd Symbolic
cmd) Bool -> Bool -> Bool
&&
          model Symbolic -> [Command cmd resp] -> Bool
preconditionsHold (model Symbolic -> cmd Symbolic -> resp Symbolic -> model Symbolic
forall (r :: * -> *).
(Show1 r, Ord1 r) =>
model r -> cmd r -> resp r -> model r
transition model Symbolic
model cmd Symbolic
cmd resp Symbolic
resp) [Command cmd resp]
cmds Bool -> Bool -> Bool
&&
          -- 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
          [Var] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Var]
vars Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Var] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (resp Symbolic -> [Var]
forall (f :: (* -> *) -> *). Foldable f => f Symbolic -> [Var]
getUsedVars (resp Symbolic -> [Var]) -> resp Symbolic -> [Var]
forall a b. (a -> b) -> a -> b
$ (resp Symbolic, Counter) -> resp Symbolic
forall a b. (a, b) -> a
fst ((resp Symbolic, Counter) -> resp Symbolic)
-> (resp Symbolic, Counter) -> resp Symbolic
forall a b. (a -> b) -> a -> b
$ GenSym (resp Symbolic) -> Counter -> (resp Symbolic, Counter)
forall a. GenSym a -> Counter -> (a, Counter)
runGenSym (model Symbolic -> cmd Symbolic -> GenSym (resp Symbolic)
mock model Symbolic
model cmd Symbolic
cmd) Counter
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 :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> model Symbolic -> Commands cmd resp -> model Symbolic
advanceModel StateMachine { forall (r :: * -> *).
(Show1 r, Ord1 r) =>
model r -> cmd r -> resp r -> model r
transition :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> forall (r :: * -> *).
   (Show1 r, Ord1 r) =>
   model r -> cmd r -> resp r -> model r
transition :: forall (r :: * -> *).
(Show1 r, Ord1 r) =>
model r -> cmd r -> resp r -> model r
transition } model Symbolic
model0 =
  model Symbolic -> [Command cmd resp] -> model Symbolic
go model Symbolic
model0 ([Command cmd resp] -> model Symbolic)
-> (Commands cmd resp -> [Command cmd resp])
-> Commands cmd resp
-> model Symbolic
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Commands cmd resp -> [Command cmd resp]
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
Commands cmd resp -> [Command cmd resp]
unCommands
  where
    go :: model Symbolic -> [Command cmd resp] -> model Symbolic
go model Symbolic
model []                              = model Symbolic
model
    go model Symbolic
model (Command cmd Symbolic
cmd resp Symbolic
resp [Var]
_vars : [Command cmd resp]
cmds) =
        model Symbolic -> [Command cmd resp] -> model Symbolic
go (model Symbolic -> cmd Symbolic -> resp Symbolic -> model Symbolic
forall (r :: * -> *).
(Show1 r, Ord1 r) =>
model r -> cmd r -> resp r -> model r
transition model Symbolic
model cmd Symbolic
cmd resp Symbolic
resp) [Command 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 :: forall (cmd :: (* -> *) -> *) (model :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
(Traversable cmd, Foldable resp) =>
StateMachine model cmd m resp
-> ParallelCommands cmd resp -> [ParallelCommands cmd resp]
shrinkParallelCommands StateMachine model cmd m resp
sm (ParallelCommands Commands cmd resp
prefix [Pair (Commands cmd resp)]
suffixes)
  = (Shrunk (ParallelCommandsF Pair cmd resp)
 -> [ParallelCommandsF Pair cmd resp])
-> [Shrunk (ParallelCommandsF Pair cmd resp)]
-> [ParallelCommandsF Pair cmd resp]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Shrunk (ParallelCommandsF Pair cmd resp)
-> [ParallelCommandsF Pair cmd resp]
go
      [ Bool
-> ParallelCommandsF Pair cmd resp
-> Shrunk (ParallelCommandsF Pair cmd resp)
forall a. Bool -> a -> Shrunk a
Shrunk Bool
s (Commands cmd resp
-> [Pair (Commands cmd resp)] -> ParallelCommandsF Pair cmd resp
forall (t :: * -> *) (cmd :: (* -> *) -> *)
       (resp :: (* -> *) -> *).
Commands cmd resp
-> [t (Commands cmd resp)] -> ParallelCommandsF t cmd resp
ParallelCommands Commands cmd resp
prefix' (((Commands cmd resp, Commands cmd resp)
 -> Pair (Commands cmd resp))
-> [(Commands cmd resp, Commands cmd resp)]
-> [Pair (Commands cmd resp)]
forall a b. (a -> b) -> [a] -> [b]
map (Commands cmd resp, Commands cmd resp) -> Pair (Commands cmd resp)
forall a. (a, a) -> Pair a
toPair [(Commands cmd resp, Commands cmd resp)]
suffixes'))
      | Shrunk Bool
s (Commands cmd resp
prefix', [(Commands cmd resp, Commands cmd resp)]
suffixes') <- (Commands cmd resp -> [Shrunk (Commands cmd resp)])
-> ([(Commands cmd resp, Commands cmd resp)]
    -> [Shrunk [(Commands cmd resp, Commands cmd resp)]])
-> (Commands cmd resp, [(Commands cmd resp, Commands cmd resp)])
-> [Shrunk
      (Commands cmd resp, [(Commands cmd resp, Commands cmd resp)])]
forall a b.
(a -> [Shrunk a]) -> (b -> [Shrunk b]) -> (a, b) -> [Shrunk (a, b)]
shrinkPairS Commands cmd resp -> [Shrunk (Commands cmd resp)]
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
Commands cmd resp -> [Shrunk (Commands cmd resp)]
shrinkCommands' [(Commands cmd resp, Commands cmd resp)]
-> [Shrunk [(Commands cmd resp, Commands cmd resp)]]
shrinkSuffixes
                                                     (Commands cmd resp
prefix, (Pair (Commands cmd resp)
 -> (Commands cmd resp, Commands cmd resp))
-> [Pair (Commands cmd resp)]
-> [(Commands cmd resp, Commands cmd resp)]
forall a b. (a -> b) -> [a] -> [b]
map Pair (Commands cmd resp) -> (Commands cmd resp, Commands cmd resp)
forall a. Pair a -> (a, a)
fromPair [Pair (Commands cmd resp)]
suffixes)
      ]
      [ParallelCommandsF Pair cmd resp]
-> [ParallelCommandsF Pair cmd resp]
-> [ParallelCommandsF Pair cmd resp]
forall a. [a] -> [a] -> [a]
++
      [ParallelCommandsF Pair cmd resp]
shrinkMoveSuffixToPrefix
  where
    go :: Shrunk (ParallelCommands cmd resp) -> [ParallelCommands cmd resp]
    go :: Shrunk (ParallelCommandsF Pair cmd resp)
-> [ParallelCommandsF Pair cmd resp]
go (Shrunk Bool
shrunk ParallelCommandsF Pair cmd resp
cmds) =
        StateMachine model cmd m resp
-> ShouldShrink
-> ParallelCommandsF Pair cmd resp
-> [ParallelCommandsF Pair cmd resp]
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
(Traversable cmd, Foldable resp) =>
StateMachine model cmd m resp
-> ShouldShrink
-> ParallelCommands cmd resp
-> [ParallelCommands cmd resp]
shrinkAndValidateParallel StateMachine model cmd m resp
sm
                                  (if Bool
shrunk then ShouldShrink
DontShrink else ShouldShrink
MustShrink)
                                  ParallelCommandsF Pair cmd resp
cmds

    shrinkSuffixes :: [(Commands cmd resp, Commands cmd resp)]
                   -> [Shrunk [(Commands cmd resp, Commands cmd resp)]]
    shrinkSuffixes :: [(Commands cmd resp, Commands cmd resp)]
-> [Shrunk [(Commands cmd resp, Commands cmd resp)]]
shrinkSuffixes = ((Commands cmd resp, Commands cmd resp)
 -> [Shrunk (Commands cmd resp, Commands cmd resp)])
-> [(Commands cmd resp, Commands cmd resp)]
-> [Shrunk [(Commands cmd resp, Commands cmd resp)]]
forall a. (a -> [Shrunk a]) -> [a] -> [Shrunk [a]]
shrinkListS ((Commands cmd resp -> [Shrunk (Commands cmd resp)])
-> (Commands cmd resp, Commands cmd resp)
-> [Shrunk (Commands cmd resp, Commands cmd resp)]
forall a. (a -> [Shrunk a]) -> (a, a) -> [Shrunk (a, a)]
shrinkPairS' Commands cmd resp -> [Shrunk (Commands cmd resp)]
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
Commands cmd resp -> [Shrunk (Commands cmd resp)]
shrinkCommands')

    -- Moving a command from a suffix to the prefix preserves validity
    shrinkMoveSuffixToPrefix :: [ParallelCommands cmd resp]
    shrinkMoveSuffixToPrefix :: [ParallelCommandsF Pair cmd resp]
shrinkMoveSuffixToPrefix = case [Pair (Commands cmd resp)]
suffixes of
      []                   -> []
      (Pair (Commands cmd resp)
suffix : [Pair (Commands cmd resp)]
suffixes') ->
        [ Commands cmd resp
-> [Pair (Commands cmd resp)] -> ParallelCommandsF Pair cmd resp
forall (t :: * -> *) (cmd :: (* -> *) -> *)
       (resp :: (* -> *) -> *).
Commands cmd resp
-> [t (Commands cmd resp)] -> ParallelCommandsF t cmd resp
ParallelCommands (Commands cmd resp
prefix Commands cmd resp -> Commands cmd resp -> Commands cmd resp
forall a. Semigroup a => a -> a -> a
<> [Command cmd resp] -> Commands cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
[Command cmd resp] -> Commands cmd resp
Commands [Command cmd resp
prefix'])
                           (([Command cmd resp] -> Commands cmd resp)
-> Pair [Command cmd resp] -> Pair (Commands cmd resp)
forall a b. (a -> b) -> Pair a -> Pair b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Command cmd resp] -> Commands cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
[Command cmd resp] -> Commands cmd resp
Commands (([Command cmd resp], [Command cmd resp]) -> Pair [Command cmd resp]
forall a. (a, a) -> Pair a
toPair ([Command cmd resp], [Command cmd resp])
suffix') Pair (Commands cmd resp)
-> [Pair (Commands cmd resp)] -> [Pair (Commands cmd resp)]
forall a. a -> [a] -> [a]
: [Pair (Commands cmd resp)]
suffixes')
        | (Command cmd resp
prefix', ([Command cmd resp], [Command cmd resp])
suffix') <- ([Command cmd resp], [Command cmd resp])
-> [(Command cmd resp, ([Command cmd resp], [Command cmd resp]))]
forall a. ([a], [a]) -> [(a, ([a], [a]))]
pickOneReturnRest2 (Commands cmd resp -> [Command cmd resp]
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
Commands cmd resp -> [Command cmd resp]
unCommands (Pair (Commands cmd resp) -> Commands cmd resp
forall a. Pair a -> a
proj1 Pair (Commands cmd resp)
suffix),
                                                    Commands cmd resp -> [Command cmd resp]
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
Commands cmd resp -> [Command cmd resp]
unCommands (Pair (Commands cmd resp) -> Commands cmd resp
forall a. Pair a -> a
proj2 Pair (Commands cmd resp)
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 :: forall (cmd :: (* -> *) -> *) (model :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
(Traversable cmd, Foldable resp) =>
StateMachine model cmd m resp
-> NParallelCommands cmd resp -> [NParallelCommands cmd resp]
shrinkNParallelCommands StateMachine model cmd m resp
sm (ParallelCommands Commands cmd resp
prefix [[Commands cmd resp]]
suffixes)
  = (Shrunk (ParallelCommandsF [] cmd resp)
 -> [ParallelCommandsF [] cmd resp])
-> [Shrunk (ParallelCommandsF [] cmd resp)]
-> [ParallelCommandsF [] cmd resp]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap Shrunk (ParallelCommandsF [] cmd resp)
-> [ParallelCommandsF [] cmd resp]
go
      [ Bool
-> ParallelCommandsF [] cmd resp
-> Shrunk (ParallelCommandsF [] cmd resp)
forall a. Bool -> a -> Shrunk a
Shrunk Bool
s (Commands cmd resp
-> [[Commands cmd resp]] -> ParallelCommandsF [] cmd resp
forall (t :: * -> *) (cmd :: (* -> *) -> *)
       (resp :: (* -> *) -> *).
Commands cmd resp
-> [t (Commands cmd resp)] -> ParallelCommandsF t cmd resp
ParallelCommands Commands cmd resp
prefix' [[Commands cmd resp]]
suffixes')
      | Shrunk Bool
s (Commands cmd resp
prefix', [[Commands cmd resp]]
suffixes') <- (Commands cmd resp -> [Shrunk (Commands cmd resp)])
-> ([[Commands cmd resp]] -> [Shrunk [[Commands cmd resp]]])
-> (Commands cmd resp, [[Commands cmd resp]])
-> [Shrunk (Commands cmd resp, [[Commands cmd resp]])]
forall a b.
(a -> [Shrunk a]) -> (b -> [Shrunk b]) -> (a, b) -> [Shrunk (a, b)]
shrinkPairS Commands cmd resp -> [Shrunk (Commands cmd resp)]
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
Commands cmd resp -> [Shrunk (Commands cmd resp)]
shrinkCommands' [[Commands cmd resp]] -> [Shrunk [[Commands cmd resp]]]
shrinkSuffixes
                                                     (Commands cmd resp
prefix, [[Commands cmd resp]]
suffixes)
      ]
      [ParallelCommandsF [] cmd resp]
-> [ParallelCommandsF [] cmd resp]
-> [ParallelCommandsF [] cmd resp]
forall a. [a] -> [a] -> [a]
++
      [ParallelCommandsF [] cmd resp]
shrinkMoveSuffixToPrefix
  where
    go :: Shrunk (NParallelCommands cmd resp) -> [NParallelCommands cmd resp]
    go :: Shrunk (ParallelCommandsF [] cmd resp)
-> [ParallelCommandsF [] cmd resp]
go (Shrunk Bool
shrunk ParallelCommandsF [] cmd resp
cmds) =
      StateMachine model cmd m resp
-> ShouldShrink
-> ParallelCommandsF [] cmd resp
-> [ParallelCommandsF [] cmd resp]
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
(Traversable cmd, Foldable resp) =>
StateMachine model cmd m resp
-> ShouldShrink
-> NParallelCommands cmd resp
-> [NParallelCommands cmd resp]
shrinkAndValidateNParallel StateMachine model cmd m resp
sm
                                       (if Bool
shrunk then ShouldShrink
DontShrink else ShouldShrink
MustShrink)
                                       ParallelCommandsF [] cmd resp
cmds

    shrinkSuffixes :: [[Commands cmd resp]]
                   -> [Shrunk [[Commands cmd resp]]]
    shrinkSuffixes :: [[Commands cmd resp]] -> [Shrunk [[Commands cmd resp]]]
shrinkSuffixes = ([Commands cmd resp] -> [Shrunk [Commands cmd resp]])
-> [[Commands cmd resp]] -> [Shrunk [[Commands cmd resp]]]
forall a. (a -> [Shrunk a]) -> [a] -> [Shrunk [a]]
shrinkListS ((Commands cmd resp -> [Shrunk (Commands cmd resp)])
-> [Commands cmd resp] -> [Shrunk [Commands cmd resp]]
forall a. (a -> [Shrunk a]) -> [a] -> [Shrunk [a]]
shrinkListS'' Commands cmd resp -> [Shrunk (Commands cmd resp)]
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
Commands cmd resp -> [Shrunk (Commands cmd resp)]
shrinkCommands')

    -- Moving a command from a suffix to the prefix preserves validity
    shrinkMoveSuffixToPrefix :: [NParallelCommands cmd resp]
    shrinkMoveSuffixToPrefix :: [ParallelCommandsF [] cmd resp]
shrinkMoveSuffixToPrefix = case [[Commands cmd resp]]
suffixes of
      []                   -> []
      ([Commands cmd resp]
suffix : [[Commands cmd resp]]
suffixes') ->
        [ Commands cmd resp
-> [[Commands cmd resp]] -> ParallelCommandsF [] cmd resp
forall (t :: * -> *) (cmd :: (* -> *) -> *)
       (resp :: (* -> *) -> *).
Commands cmd resp
-> [t (Commands cmd resp)] -> ParallelCommandsF t cmd resp
ParallelCommands (Commands cmd resp
prefix Commands cmd resp -> Commands cmd resp -> Commands cmd resp
forall a. Semigroup a => a -> a -> a
<> [Command cmd resp] -> Commands cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
[Command cmd resp] -> Commands cmd resp
Commands [Command cmd resp
prefix'])
                           (([Command cmd resp] -> Commands cmd resp)
-> [[Command cmd resp]] -> [Commands cmd resp]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Command cmd resp] -> Commands cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
[Command cmd resp] -> Commands cmd resp
Commands [[Command cmd resp]]
suffix' [Commands cmd resp]
-> [[Commands cmd resp]] -> [[Commands cmd resp]]
forall a. a -> [a] -> [a]
: [[Commands cmd resp]]
suffixes')
        | (Command cmd resp
prefix', [[Command cmd resp]]
suffix') <- [[Command cmd resp]] -> [(Command cmd resp, [[Command cmd resp]])]
forall a. [[a]] -> [(a, [[a]])]
pickOneReturnRestL (Commands cmd resp -> [Command cmd resp]
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
Commands cmd resp -> [Command cmd resp]
unCommands (Commands cmd resp -> [Command cmd resp])
-> [Commands cmd resp] -> [[Command cmd resp]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Commands cmd resp]
suffix)
        ]

-- | Shrinks Commands in a way that it has strictly less number of commands.
shrinkCommands' :: Commands cmd resp -> [Shrunk (Commands cmd resp)]
shrinkCommands' :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
Commands cmd resp -> [Shrunk (Commands cmd resp)]
shrinkCommands' = (Shrunk [Command cmd resp] -> Shrunk (Commands cmd resp))
-> [Shrunk [Command cmd resp]] -> [Shrunk (Commands cmd resp)]
forall a b. (a -> b) -> [a] -> [b]
map (([Command cmd resp] -> Commands cmd resp)
-> Shrunk [Command cmd resp] -> Shrunk (Commands cmd resp)
forall a b. (a -> b) -> Shrunk a -> Shrunk b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Command cmd resp] -> Commands cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
[Command cmd resp] -> Commands cmd resp
Commands) ([Shrunk [Command cmd resp]] -> [Shrunk (Commands cmd resp)])
-> (Commands cmd resp -> [Shrunk [Command cmd resp]])
-> Commands cmd resp
-> [Shrunk (Commands cmd resp)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Command cmd resp] -> [Shrunk [Command cmd resp]]
forall a. [a] -> [Shrunk [a]]
shrinkListS' ([Command cmd resp] -> [Shrunk [Command cmd resp]])
-> (Commands cmd resp -> [Command cmd resp])
-> Commands cmd resp
-> [Shrunk [Command cmd resp]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Commands cmd resp -> [Command cmd resp]
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
Commands cmd resp -> [Command cmd resp]
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 :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
(Traversable cmd, Foldable resp) =>
StateMachine model cmd m resp
-> ShouldShrink
-> ParallelCommands cmd resp
-> [ParallelCommands cmd resp]
shrinkAndValidateParallel sm :: StateMachine model cmd m resp
sm@StateMachine { forall (r :: * -> *). model r
initModel :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> forall (r :: * -> *). model r
initModel :: forall (r :: * -> *). model r
initModel } = \ShouldShrink
shouldShrink (ParallelCommands Commands cmd resp
prefix [Pair (Commands cmd resp)]
suffixes) ->
    let env :: ValidateEnv model
env = model Symbolic -> ValidateEnv model
forall (model :: (* -> *) -> *).
model Symbolic -> ValidateEnv model
initValidateEnv model Symbolic
forall (r :: * -> *). model r
initModel
        curryGo :: ShouldShrink
-> (ValidateEnv model, Commands cmd resp)
-> [ParallelCommands cmd resp]
curryGo ShouldShrink
shouldShrink' (ValidateEnv model
env', Commands cmd resp
prefix') = Commands cmd resp
-> ValidateEnv model
-> ShouldShrink
-> [Pair (Commands cmd resp)]
-> [ParallelCommands cmd resp]
go Commands cmd resp
prefix' ValidateEnv model
env' ShouldShrink
shouldShrink' [Pair (Commands cmd resp)]
suffixes in
    case ShouldShrink
shouldShrink of
      ShouldShrink
DontShrink -> ((ValidateEnv model, Commands cmd resp)
 -> [ParallelCommands cmd resp])
-> [(ValidateEnv model, Commands cmd resp)]
-> [ParallelCommands cmd resp]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (ShouldShrink
-> (ValidateEnv model, Commands cmd resp)
-> [ParallelCommands cmd resp]
curryGo ShouldShrink
DontShrink) (StateMachine model cmd m resp
-> ShouldShrink
-> ValidateEnv model
-> Commands cmd resp
-> [(ValidateEnv model, Commands cmd resp)]
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
(Traversable cmd, Foldable resp) =>
StateMachine model cmd m resp
-> ShouldShrink
-> ValidateEnv model
-> Commands cmd resp
-> [(ValidateEnv model, Commands cmd resp)]
shrinkAndValidate StateMachine model cmd m resp
sm ShouldShrink
DontShrink ValidateEnv model
env Commands cmd resp
prefix)
      ShouldShrink
MustShrink -> ((ValidateEnv model, Commands cmd resp)
 -> [ParallelCommands cmd resp])
-> [(ValidateEnv model, Commands cmd resp)]
-> [ParallelCommands cmd resp]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (ShouldShrink
-> (ValidateEnv model, Commands cmd resp)
-> [ParallelCommands cmd resp]
curryGo ShouldShrink
DontShrink) (StateMachine model cmd m resp
-> ShouldShrink
-> ValidateEnv model
-> Commands cmd resp
-> [(ValidateEnv model, Commands cmd resp)]
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
(Traversable cmd, Foldable resp) =>
StateMachine model cmd m resp
-> ShouldShrink
-> ValidateEnv model
-> Commands cmd resp
-> [(ValidateEnv model, Commands cmd resp)]
shrinkAndValidate StateMachine model cmd m resp
sm ShouldShrink
MustShrink ValidateEnv model
env Commands cmd resp
prefix)
                 [ParallelCommands cmd resp]
-> [ParallelCommands cmd resp] -> [ParallelCommands cmd resp]
forall a. [a] -> [a] -> [a]
++ ((ValidateEnv model, Commands cmd resp)
 -> [ParallelCommands cmd resp])
-> [(ValidateEnv model, Commands cmd resp)]
-> [ParallelCommands cmd resp]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (ShouldShrink
-> (ValidateEnv model, Commands cmd resp)
-> [ParallelCommands cmd resp]
curryGo ShouldShrink
MustShrink) (StateMachine model cmd m resp
-> ShouldShrink
-> ValidateEnv model
-> Commands cmd resp
-> [(ValidateEnv model, Commands cmd resp)]
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
(Traversable cmd, Foldable resp) =>
StateMachine model cmd m resp
-> ShouldShrink
-> ValidateEnv model
-> Commands cmd resp
-> [(ValidateEnv model, Commands cmd resp)]
shrinkAndValidate StateMachine model cmd m resp
sm ShouldShrink
DontShrink ValidateEnv model
env Commands cmd resp
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 :: Commands cmd resp
-> ValidateEnv model
-> ShouldShrink
-> [Pair (Commands cmd resp)]
-> [ParallelCommands cmd resp]
go Commands cmd resp
prefix' = [Pair (Commands cmd resp)]
-> ValidateEnv model
-> ShouldShrink
-> [Pair (Commands cmd resp)]
-> [ParallelCommands cmd resp]
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' :: [Pair (Commands cmd resp)]
-> ValidateEnv model
-> ShouldShrink
-> [Pair (Commands cmd resp)]
-> [ParallelCommands cmd resp]
go' [Pair (Commands cmd resp)]
_   ValidateEnv model
_   ShouldShrink
MustShrink [] = [] -- Failed to shrink something
        go' [Pair (Commands cmd resp)]
acc ValidateEnv model
_   ShouldShrink
DontShrink [] = [Commands cmd resp
-> [Pair (Commands cmd resp)] -> ParallelCommands cmd resp
forall (t :: * -> *) (cmd :: (* -> *) -> *)
       (resp :: (* -> *) -> *).
Commands cmd resp
-> [t (Commands cmd resp)] -> ParallelCommandsF t cmd resp
ParallelCommands Commands cmd resp
prefix' ([Pair (Commands cmd resp)] -> [Pair (Commands cmd resp)]
forall a. [a] -> [a]
reverse [Pair (Commands cmd resp)]
acc)]
        go' [Pair (Commands cmd resp)]
acc ValidateEnv model
env ShouldShrink
shouldShrink (Pair Commands cmd resp
l Commands cmd resp
r : [Pair (Commands cmd resp)]
suffixes) = do
            ((ShouldShrink
shrinkL, ShouldShrink
shrinkR), ShouldShrink
shrinkRest) <- [((ShouldShrink, ShouldShrink), ShouldShrink)]
shrinkOpts
            (ValidateEnv model
envL, Commands cmd resp
l') <- StateMachine model cmd m resp
-> ShouldShrink
-> ValidateEnv model
-> Commands cmd resp
-> [(ValidateEnv model, Commands cmd resp)]
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
(Traversable cmd, Foldable resp) =>
StateMachine model cmd m resp
-> ShouldShrink
-> ValidateEnv model
-> Commands cmd resp
-> [(ValidateEnv model, Commands cmd resp)]
shrinkAndValidate StateMachine model cmd m resp
sm ShouldShrink
shrinkL  ValidateEnv model
env                         Commands cmd resp
l
            (ValidateEnv model
envR, Commands cmd resp
r') <- StateMachine model cmd m resp
-> ShouldShrink
-> ValidateEnv model
-> Commands cmd resp
-> [(ValidateEnv model, Commands cmd resp)]
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
(Traversable cmd, Foldable resp) =>
StateMachine model cmd m resp
-> ShouldShrink
-> ValidateEnv model
-> Commands cmd resp
-> [(ValidateEnv model, Commands cmd resp)]
shrinkAndValidate StateMachine model cmd m resp
sm ShouldShrink
shrinkR (ValidateEnv model
env ValidateEnv model -> ValidateEnv model -> ValidateEnv model
forall (model :: (* -> *) -> *).
ValidateEnv model -> ValidateEnv model -> ValidateEnv model
`withCounterFrom` ValidateEnv model
envL) Commands cmd resp
r
            [Pair (Commands cmd resp)]
-> ValidateEnv model
-> ShouldShrink
-> [Pair (Commands cmd resp)]
-> [ParallelCommands cmd resp]
go' (Commands cmd resp -> Commands cmd resp -> Pair (Commands cmd resp)
forall a. a -> a -> Pair a
Pair Commands cmd resp
l' Commands cmd resp
r' Pair (Commands cmd resp)
-> [Pair (Commands cmd resp)] -> [Pair (Commands cmd resp)]
forall a. a -> [a] -> [a]
: [Pair (Commands cmd resp)]
acc) (StateMachine model cmd m resp
-> ValidateEnv model
-> ValidateEnv model
-> Commands cmd resp
-> ValidateEnv model
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> ValidateEnv model
-> ValidateEnv model
-> Commands cmd resp
-> ValidateEnv model
combineEnv StateMachine model cmd m resp
sm ValidateEnv model
envL ValidateEnv model
envR Commands cmd resp
r') ShouldShrink
shrinkRest [Pair (Commands cmd resp)]
suffixes
          where

            shrinkOpts :: [((ShouldShrink, ShouldShrink), ShouldShrink)]
            shrinkOpts :: [((ShouldShrink, ShouldShrink), ShouldShrink)]
shrinkOpts =
                case ShouldShrink
shouldShrink of
                  ShouldShrink
DontShrink -> [ ((ShouldShrink
DontShrink, ShouldShrink
DontShrink), ShouldShrink
DontShrink) ]
                  ShouldShrink
MustShrink -> [ ((ShouldShrink
MustShrink, ShouldShrink
DontShrink), ShouldShrink
DontShrink)
                                , ((ShouldShrink
DontShrink, ShouldShrink
MustShrink), ShouldShrink
DontShrink)
                                , ((ShouldShrink
DontShrink, ShouldShrink
DontShrink), ShouldShrink
MustShrink) ]

combineEnv :: StateMachine model cmd m resp
           -> ValidateEnv model
           -> ValidateEnv model
           -> Commands cmd resp
           -> ValidateEnv model
combineEnv :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> ValidateEnv model
-> ValidateEnv model
-> Commands cmd resp
-> ValidateEnv model
combineEnv StateMachine model cmd m resp
sm ValidateEnv model
envL ValidateEnv model
envR Commands cmd resp
cmds = ValidateEnv {
      veModel :: model Symbolic
veModel   = StateMachine model cmd m resp
-> model Symbolic -> Commands cmd resp -> model Symbolic
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> model Symbolic -> Commands cmd resp -> model Symbolic
advanceModel StateMachine model cmd m resp
sm (ValidateEnv model -> model Symbolic
forall (model :: (* -> *) -> *).
ValidateEnv model -> model Symbolic
veModel ValidateEnv model
envL) Commands cmd resp
cmds
    , veScope :: Map Var Var
veScope   = Map Var Var -> Map Var Var -> Map Var Var
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union (ValidateEnv model -> Map Var Var
forall (model :: (* -> *) -> *). ValidateEnv model -> Map Var Var
veScope ValidateEnv model
envL) (ValidateEnv model -> Map Var Var
forall (model :: (* -> *) -> *). ValidateEnv model -> Map Var Var
veScope ValidateEnv model
envR)
    , veCounter :: Counter
veCounter = ValidateEnv model -> Counter
forall (model :: (* -> *) -> *). ValidateEnv model -> Counter
veCounter ValidateEnv model
envR
    }

withCounterFrom :: ValidateEnv model -> ValidateEnv model -> ValidateEnv model
withCounterFrom :: forall (model :: (* -> *) -> *).
ValidateEnv model -> ValidateEnv model -> ValidateEnv model
withCounterFrom ValidateEnv model
e ValidateEnv model
e' = ValidateEnv model
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 :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
(Traversable cmd, Foldable resp) =>
StateMachine model cmd m resp
-> ShouldShrink
-> NParallelCommands cmd resp
-> [NParallelCommands cmd resp]
shrinkAndValidateNParallel StateMachine model cmd m resp
sm = \ShouldShrink
shouldShrink  (ParallelCommands Commands cmd resp
prefix [[Commands cmd resp]]
suffixes) ->
    let env :: ValidateEnv model
env = model Symbolic -> ValidateEnv model
forall (model :: (* -> *) -> *).
model Symbolic -> ValidateEnv model
initValidateEnv (model Symbolic -> ValidateEnv model)
-> model Symbolic -> ValidateEnv model
forall a b. (a -> b) -> a -> b
$ StateMachine model cmd m resp -> forall (r :: * -> *). model r
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> forall (r :: * -> *). model r
initModel StateMachine model cmd m resp
sm
        curryGo :: ShouldShrink
-> (ValidateEnv model, Commands cmd resp)
-> [NParallelCommands cmd resp]
curryGo ShouldShrink
shouldShrink' (ValidateEnv model
env', Commands cmd resp
prefix') = Commands cmd resp
-> ValidateEnv model
-> ShouldShrink
-> [[Commands cmd resp]]
-> [NParallelCommands cmd resp]
go Commands cmd resp
prefix' ValidateEnv model
env' ShouldShrink
shouldShrink' [[Commands cmd resp]]
suffixes in
    case ShouldShrink
shouldShrink of
      ShouldShrink
DontShrink -> ((ValidateEnv model, Commands cmd resp)
 -> [NParallelCommands cmd resp])
-> [(ValidateEnv model, Commands cmd resp)]
-> [NParallelCommands cmd resp]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (ShouldShrink
-> (ValidateEnv model, Commands cmd resp)
-> [NParallelCommands cmd resp]
curryGo ShouldShrink
DontShrink) (StateMachine model cmd m resp
-> ShouldShrink
-> ValidateEnv model
-> Commands cmd resp
-> [(ValidateEnv model, Commands cmd resp)]
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
(Traversable cmd, Foldable resp) =>
StateMachine model cmd m resp
-> ShouldShrink
-> ValidateEnv model
-> Commands cmd resp
-> [(ValidateEnv model, Commands cmd resp)]
shrinkAndValidate StateMachine model cmd m resp
sm ShouldShrink
DontShrink ValidateEnv model
env Commands cmd resp
prefix)
      ShouldShrink
MustShrink -> ((ValidateEnv model, Commands cmd resp)
 -> [NParallelCommands cmd resp])
-> [(ValidateEnv model, Commands cmd resp)]
-> [NParallelCommands cmd resp]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (ShouldShrink
-> (ValidateEnv model, Commands cmd resp)
-> [NParallelCommands cmd resp]
curryGo ShouldShrink
DontShrink) (StateMachine model cmd m resp
-> ShouldShrink
-> ValidateEnv model
-> Commands cmd resp
-> [(ValidateEnv model, Commands cmd resp)]
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
(Traversable cmd, Foldable resp) =>
StateMachine model cmd m resp
-> ShouldShrink
-> ValidateEnv model
-> Commands cmd resp
-> [(ValidateEnv model, Commands cmd resp)]
shrinkAndValidate StateMachine model cmd m resp
sm ShouldShrink
MustShrink ValidateEnv model
env Commands cmd resp
prefix)
                 [NParallelCommands cmd resp]
-> [NParallelCommands cmd resp] -> [NParallelCommands cmd resp]
forall a. [a] -> [a] -> [a]
++ ((ValidateEnv model, Commands cmd resp)
 -> [NParallelCommands cmd resp])
-> [(ValidateEnv model, Commands cmd resp)]
-> [NParallelCommands cmd resp]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (ShouldShrink
-> (ValidateEnv model, Commands cmd resp)
-> [NParallelCommands cmd resp]
curryGo ShouldShrink
MustShrink) (StateMachine model cmd m resp
-> ShouldShrink
-> ValidateEnv model
-> Commands cmd resp
-> [(ValidateEnv model, Commands cmd resp)]
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
(Traversable cmd, Foldable resp) =>
StateMachine model cmd m resp
-> ShouldShrink
-> ValidateEnv model
-> Commands cmd resp
-> [(ValidateEnv model, Commands cmd resp)]
shrinkAndValidate StateMachine model cmd m resp
sm ShouldShrink
DontShrink ValidateEnv model
env Commands cmd resp
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 :: Commands cmd resp
-> ValidateEnv model
-> ShouldShrink
-> [[Commands cmd resp]]
-> [NParallelCommands cmd resp]
go Commands cmd resp
prefix' = [[Commands cmd resp]]
-> ValidateEnv model
-> ShouldShrink
-> [[Commands cmd resp]]
-> [NParallelCommands cmd resp]
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' :: [[Commands cmd resp]]
-> ValidateEnv model
-> ShouldShrink
-> [[Commands cmd resp]]
-> [NParallelCommands cmd resp]
go' [[Commands cmd resp]]
_   ValidateEnv model
_   ShouldShrink
MustShrink [] = [] -- Failed to shrink something
        go' [[Commands cmd resp]]
acc ValidateEnv model
_   ShouldShrink
DontShrink [] = [Commands cmd resp
-> [[Commands cmd resp]] -> NParallelCommands cmd resp
forall (t :: * -> *) (cmd :: (* -> *) -> *)
       (resp :: (* -> *) -> *).
Commands cmd resp
-> [t (Commands cmd resp)] -> ParallelCommandsF t cmd resp
ParallelCommands Commands cmd resp
prefix' ([[Commands cmd resp]] -> [[Commands cmd resp]]
forall a. [a] -> [a]
reverse [[Commands cmd resp]]
acc)]
        go' [[Commands cmd resp]]
acc ValidateEnv model
env ShouldShrink
shouldShrink ([Commands cmd resp]
suffix : [[Commands cmd resp]]
suffixes) = do
            ([(ShouldShrink, Commands cmd resp)]
suffixWithShrinks, ShouldShrink
shrinkRest) <- [Commands cmd resp]
-> [([(ShouldShrink, Commands cmd resp)], ShouldShrink)]
forall a. [a] -> [([(ShouldShrink, a)], ShouldShrink)]
shrinkOpts [Commands cmd resp]
suffix
            (ValidateEnv model
envFinal, [Commands cmd resp]
suffix') <- (Bool, [(ValidateEnv model, [Commands cmd resp])])
-> [(ValidateEnv model, [Commands cmd resp])]
forall a b. (a, b) -> b
snd ((Bool, [(ValidateEnv model, [Commands cmd resp])])
 -> [(ValidateEnv model, [Commands cmd resp])])
-> (Bool, [(ValidateEnv model, [Commands cmd resp])])
-> [(ValidateEnv model, [Commands cmd resp])]
forall a b. (a -> b) -> a -> b
$ ((Bool, [(ValidateEnv model, [Commands cmd resp])])
 -> (ShouldShrink, Commands cmd resp)
 -> (Bool, [(ValidateEnv model, [Commands cmd resp])]))
-> (Bool, [(ValidateEnv model, [Commands cmd resp])])
-> [(ShouldShrink, Commands cmd resp)]
-> (Bool, [(ValidateEnv model, [Commands cmd resp])])
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (Bool, [(ValidateEnv model, [Commands cmd resp])])
-> (ShouldShrink, Commands cmd resp)
-> (Bool, [(ValidateEnv model, [Commands cmd resp])])
f (Bool
True, [(ValidateEnv model
env,[])]) [(ShouldShrink, Commands cmd resp)]
suffixWithShrinks
            [[Commands cmd resp]]
-> ValidateEnv model
-> ShouldShrink
-> [[Commands cmd resp]]
-> [NParallelCommands cmd resp]
go' ([Commands cmd resp] -> [Commands cmd resp]
forall a. [a] -> [a]
reverse [Commands cmd resp]
suffix' [Commands cmd resp]
-> [[Commands cmd resp]] -> [[Commands cmd resp]]
forall a. a -> [a] -> [a]
: [[Commands cmd resp]]
acc) ValidateEnv model
envFinal ShouldShrink
shrinkRest [[Commands cmd resp]]
suffixes
          where

            f :: (Bool, [(ValidateEnv model, [Commands cmd resp])])
              -> (ShouldShrink, Commands cmd resp)
              -> (Bool, [(ValidateEnv model, [Commands cmd resp])])
            f :: (Bool, [(ValidateEnv model, [Commands cmd resp])])
-> (ShouldShrink, Commands cmd resp)
-> (Bool, [(ValidateEnv model, [Commands cmd resp])])
f (Bool
firstCall, [(ValidateEnv model, [Commands cmd resp])]
acc') (ShouldShrink
shrink, Commands cmd resp
cmds) = (Bool
False, [(ValidateEnv model, [Commands cmd resp])]
acc'')
              where
                    acc'' :: [(ValidateEnv model, [Commands cmd resp])]
acc'' = do
                      (ValidateEnv model
envPrev, [Commands cmd resp]
cmdsPrev) <- [(ValidateEnv model, [Commands cmd resp])]
acc'
                      let envUsed :: ValidateEnv model
envUsed = if Bool
firstCall then ValidateEnv model
env else ValidateEnv model
env ValidateEnv model -> ValidateEnv model -> ValidateEnv model
forall (model :: (* -> *) -> *).
ValidateEnv model -> ValidateEnv model -> ValidateEnv model
`withCounterFrom` ValidateEnv model
envPrev
                      (ValidateEnv model
env', Commands cmd resp
cmd') <- StateMachine model cmd m resp
-> ShouldShrink
-> ValidateEnv model
-> Commands cmd resp
-> [(ValidateEnv model, Commands cmd resp)]
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
(Traversable cmd, Foldable resp) =>
StateMachine model cmd m resp
-> ShouldShrink
-> ValidateEnv model
-> Commands cmd resp
-> [(ValidateEnv model, Commands cmd resp)]
shrinkAndValidate StateMachine model cmd m resp
sm ShouldShrink
shrink ValidateEnv model
envUsed Commands cmd resp
cmds
                      let env'' :: ValidateEnv model
env'' = if Bool
firstCall then ValidateEnv model
env' else
                            StateMachine model cmd m resp
-> ValidateEnv model
-> ValidateEnv model
-> Commands cmd resp
-> ValidateEnv model
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> ValidateEnv model
-> ValidateEnv model
-> Commands cmd resp
-> ValidateEnv model
combineEnv StateMachine model cmd m resp
sm ValidateEnv model
envPrev ValidateEnv model
env' Commands cmd resp
cmd'
                      (ValidateEnv model, [Commands cmd resp])
-> [(ValidateEnv model, [Commands cmd resp])]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (ValidateEnv model
env'', Commands cmd resp
cmd' Commands cmd resp -> [Commands cmd resp] -> [Commands cmd resp]
forall a. a -> [a] -> [a]
: [Commands cmd resp]
cmdsPrev)

            shrinkOpts :: [a] -> [([(ShouldShrink, a)], ShouldShrink)]
            shrinkOpts :: forall a. [a] -> [([(ShouldShrink, a)], ShouldShrink)]
shrinkOpts [a]
ls =
              let len :: Int
len = [a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
ls
                  dontShrink :: [ShouldShrink]
dontShrink = Int -> ShouldShrink -> [ShouldShrink]
forall a. Int -> a -> [a]
replicate Int
len ShouldShrink
DontShrink
                  shrinks :: [[ShouldShrink]]
shrinks = if Int
len Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0
                    then String -> [[ShouldShrink]]
forall a. HasCallStack => String -> a
error String
"Invariant violation! A suffix should never be an empty list"
                    else ((Int -> [ShouldShrink]) -> [Int] -> [[ShouldShrink]])
-> [Int] -> (Int -> [ShouldShrink]) -> [[ShouldShrink]]
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Int -> [ShouldShrink]) -> [Int] -> [[ShouldShrink]]
forall a b. (a -> b) -> [a] -> [b]
map [Int
1..Int
len] ((Int -> [ShouldShrink]) -> [[ShouldShrink]])
-> (Int -> [ShouldShrink]) -> [[ShouldShrink]]
forall a b. (a -> b) -> a -> b
$ \Int
n ->
                        Int -> ShouldShrink -> [ShouldShrink]
forall a. Int -> a -> [a]
replicate (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) ShouldShrink
DontShrink [ShouldShrink] -> [ShouldShrink] -> [ShouldShrink]
forall a. [a] -> [a] -> [a]
++ [ShouldShrink
MustShrink] [ShouldShrink] -> [ShouldShrink] -> [ShouldShrink]
forall a. [a] -> [a] -> [a]
++ Int -> ShouldShrink -> [ShouldShrink]
forall a. Int -> a -> [a]
replicate (Int
len Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
n) ShouldShrink
DontShrink
              in case ShouldShrink
shouldShrink of
                  ShouldShrink
DontShrink -> [([ShouldShrink] -> [a] -> [(ShouldShrink, a)]
forall a b. [a] -> [b] -> [(a, b)]
zip [ShouldShrink]
dontShrink [a]
ls, ShouldShrink
DontShrink)]
                  ShouldShrink
MustShrink -> ([ShouldShrink] -> ([(ShouldShrink, a)], ShouldShrink))
-> [[ShouldShrink]] -> [([(ShouldShrink, a)], ShouldShrink)]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\[ShouldShrink]
shrinkLs -> ([ShouldShrink] -> [a] -> [(ShouldShrink, a)]
forall a b. [a] -> [b] -> [(a, b)]
zip [ShouldShrink]
shrinkLs [a]
ls, ShouldShrink
DontShrink)) [[ShouldShrink]]
shrinks
                             [([(ShouldShrink, a)], ShouldShrink)]
-> [([(ShouldShrink, a)], ShouldShrink)]
-> [([(ShouldShrink, a)], ShouldShrink)]
forall a. [a] -> [a] -> [a]
++ [([ShouldShrink] -> [a] -> [(ShouldShrink, a)]
forall a b. [a] -> [b] -> [(a, b)]
zip [ShouldShrink]
dontShrink [a]
ls, ShouldShrink
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, model Concrete, Logic)]
runParallelCommands :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
       (model :: (* -> *) -> *).
(Show (cmd Concrete), Show (resp Concrete), Traversable cmd,
 Foldable resp, MonadMask m, MonadUnliftIO m) =>
StateMachine model cmd m resp
-> ParallelCommands cmd resp
-> PropertyM m [(History cmd resp, model Concrete, Logic)]
runParallelCommands = Int
-> StateMachine model cmd m resp
-> ParallelCommands cmd resp
-> PropertyM m [(History cmd resp, model Concrete, Logic)]
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
       (model :: (* -> *) -> *).
(Show (cmd Concrete), Show (resp Concrete), Traversable cmd,
 Foldable resp, MonadMask m, MonadUnliftIO m) =>
Int
-> StateMachine model cmd m resp
-> ParallelCommands cmd resp
-> PropertyM m [(History cmd resp, model Concrete, Logic)]
runParallelCommandsNTimes Int
10

runParallelCommandsWithSetup :: (Show (cmd Concrete), Show (resp Concrete))
                    => (Rank2.Traversable cmd, Rank2.Foldable resp)
                    => (MonadMask m, MonadUnliftIO m)
                    => m (StateMachine model cmd m resp)
                    -> ParallelCommands cmd resp
                    -> PropertyM m [(History cmd resp, model Concrete, Logic)]
runParallelCommandsWithSetup :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
       (model :: (* -> *) -> *).
(Show (cmd Concrete), Show (resp Concrete), Traversable cmd,
 Foldable resp, MonadMask m, MonadUnliftIO m) =>
m (StateMachine model cmd m resp)
-> ParallelCommands cmd resp
-> PropertyM m [(History cmd resp, model Concrete, Logic)]
runParallelCommandsWithSetup = Int
-> m (StateMachine model cmd m resp)
-> ParallelCommands cmd resp
-> PropertyM m [(History cmd resp, model Concrete, Logic)]
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
       (model :: (* -> *) -> *).
(Show (cmd Concrete), Show (resp Concrete), Traversable cmd,
 Foldable resp, MonadMask m, MonadUnliftIO m) =>
Int
-> m (StateMachine model cmd m resp)
-> ParallelCommands cmd resp
-> PropertyM m [(History cmd resp, model Concrete, Logic)]
runParallelCommandsNTimesWithSetup Int
10

runParallelCommands' :: (Show (cmd Concrete), Show (resp Concrete))
                     => (Rank2.Traversable cmd, Rank2.Foldable resp)
                     => (MonadMask m, MonadUnliftIO m)
                     => m (StateMachine model cmd m resp)
                     -> (cmd Concrete -> resp Concrete)
                     -> ParallelCommands cmd resp
                     -> PropertyM m [(History cmd resp, model Concrete,  Logic)]
runParallelCommands' :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
       (model :: (* -> *) -> *).
(Show (cmd Concrete), Show (resp Concrete), Traversable cmd,
 Foldable resp, MonadMask m, MonadUnliftIO m) =>
m (StateMachine model cmd m resp)
-> (cmd Concrete -> resp Concrete)
-> ParallelCommands cmd resp
-> PropertyM m [(History cmd resp, model Concrete, Logic)]
runParallelCommands' = Int
-> m (StateMachine model cmd m resp)
-> (cmd Concrete -> resp Concrete)
-> ParallelCommands cmd resp
-> PropertyM m [(History cmd resp, model Concrete, Logic)]
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
       (model :: (* -> *) -> *).
(Show (cmd Concrete), Show (resp Concrete), Traversable cmd,
 Foldable resp, MonadMask m, MonadUnliftIO m) =>
Int
-> m (StateMachine model cmd m resp)
-> (cmd Concrete -> resp Concrete)
-> ParallelCommands cmd resp
-> PropertyM m [(History cmd resp, model Concrete, Logic)]
runParallelCommandsNTimes' Int
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, model Concrete, Logic)]
runNParallelCommands :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
       (model :: (* -> *) -> *).
(Show (cmd Concrete), Show (resp Concrete), Traversable cmd,
 Foldable resp, MonadMask m, MonadUnliftIO m) =>
StateMachine model cmd m resp
-> NParallelCommands cmd resp
-> PropertyM m [(History cmd resp, model Concrete, Logic)]
runNParallelCommands = Int
-> StateMachine model cmd m resp
-> NParallelCommands cmd resp
-> PropertyM m [(History cmd resp, model Concrete, Logic)]
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
       (model :: (* -> *) -> *).
(Show (cmd Concrete), Show (resp Concrete), Traversable cmd,
 Foldable resp, MonadMask m, MonadUnliftIO m) =>
Int
-> StateMachine model cmd m resp
-> NParallelCommands cmd resp
-> PropertyM m [(History cmd resp, model Concrete, Logic)]
runNParallelCommandsNTimes Int
10

runNParallelCommandsWithSetup :: (Show (cmd Concrete), Show (resp Concrete))
                     => (Rank2.Traversable cmd, Rank2.Foldable resp)
                     => (MonadMask m, MonadUnliftIO m)
                     => m (StateMachine model cmd m resp)
                     -> NParallelCommands cmd resp
                     -> PropertyM m [(History cmd resp, model Concrete, Logic)]
runNParallelCommandsWithSetup :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
       (model :: (* -> *) -> *).
(Show (cmd Concrete), Show (resp Concrete), Traversable cmd,
 Foldable resp, MonadMask m, MonadUnliftIO m) =>
m (StateMachine model cmd m resp)
-> NParallelCommands cmd resp
-> PropertyM m [(History cmd resp, model Concrete, Logic)]
runNParallelCommandsWithSetup = Int
-> m (StateMachine model cmd m resp)
-> NParallelCommands cmd resp
-> PropertyM m [(History cmd resp, model Concrete, Logic)]
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
       (model :: (* -> *) -> *).
(Show (cmd Concrete), Show (resp Concrete), Traversable cmd,
 Foldable resp, MonadMask m, MonadUnliftIO m) =>
Int
-> m (StateMachine model cmd m resp)
-> NParallelCommands cmd resp
-> PropertyM m [(History cmd resp, model Concrete, Logic)]
runNParallelCommandsNTimesWithSetup Int
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, model Concrete, Logic)]
runParallelCommandsNTimes :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
       (model :: (* -> *) -> *).
(Show (cmd Concrete), Show (resp Concrete), Traversable cmd,
 Foldable resp, MonadMask m, MonadUnliftIO m) =>
Int
-> StateMachine model cmd m resp
-> ParallelCommands cmd resp
-> PropertyM m [(History cmd resp, model Concrete, Logic)]
runParallelCommandsNTimes Int
n StateMachine model cmd m resp
sm = Int
-> m (StateMachine model cmd m resp)
-> ParallelCommands cmd resp
-> PropertyM m [(History cmd resp, model Concrete, Logic)]
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
       (model :: (* -> *) -> *).
(Show (cmd Concrete), Show (resp Concrete), Traversable cmd,
 Foldable resp, MonadMask m, MonadUnliftIO m) =>
Int
-> m (StateMachine model cmd m resp)
-> ParallelCommands cmd resp
-> PropertyM m [(History cmd resp, model Concrete, Logic)]
runParallelCommandsNTimesWithSetup Int
n (StateMachine model cmd m resp -> m (StateMachine model cmd m resp)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure StateMachine model cmd m resp
sm)

runParallelCommandsNTimesWithSetup :: (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.
                          -> m (StateMachine model cmd m resp)
                          -> ParallelCommands cmd resp
                          -> PropertyM m [(History cmd resp, model Concrete, Logic)]
runParallelCommandsNTimesWithSetup :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
       (model :: (* -> *) -> *).
(Show (cmd Concrete), Show (resp Concrete), Traversable cmd,
 Foldable resp, MonadMask m, MonadUnliftIO m) =>
Int
-> m (StateMachine model cmd m resp)
-> ParallelCommands cmd resp
-> PropertyM m [(History cmd resp, model Concrete, Logic)]
runParallelCommandsNTimesWithSetup Int
n m (StateMachine model cmd m resp)
msm ParallelCommands cmd resp
cmds =
  Int
-> PropertyM m (History cmd resp, model Concrete, Logic)
-> PropertyM m [(History cmd resp, model Concrete, Logic)]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
n (PropertyM m (History cmd resp, model Concrete, Logic)
 -> PropertyM m [(History cmd resp, model Concrete, Logic)])
-> PropertyM m (History cmd resp, model Concrete, Logic)
-> PropertyM m [(History cmd resp, model Concrete, Logic)]
forall a b. (a -> b) -> a -> b
$ do
    TChan (Pid, HistoryEvent cmd resp)
hchan <- PropertyM m (TChan (Pid, HistoryEvent cmd resp))
forall (m :: * -> *) a. MonadIO m => m (TChan a)
newTChanIO
    ((History cmd resp
hist, model Concrete
model, Reason
reason1, Reason
reason2), StateMachine model cmd m resp
sm') <- m ((History cmd resp, model Concrete, Reason, Reason),
   StateMachine model cmd m resp)
-> PropertyM
     m
     ((History cmd resp, model Concrete, Reason, Reason),
      StateMachine model cmd m resp)
forall (m :: * -> *) a. Monad m => m a -> PropertyM m a
run (m ((History cmd resp, model Concrete, Reason, Reason),
    StateMachine model cmd m resp)
 -> PropertyM
      m
      ((History cmd resp, model Concrete, Reason, Reason),
       StateMachine model cmd m resp))
-> m ((History cmd resp, model Concrete, Reason, Reason),
      StateMachine model cmd m resp)
-> PropertyM
     m
     ((History cmd resp, model Concrete, Reason, Reason),
      StateMachine model cmd m resp)
forall a b. (a -> b) -> a -> b
$
      (((History cmd resp, model Concrete, Reason, Reason),
  StateMachine model cmd m resp),
 ())
-> ((History cmd resp, model Concrete, Reason, Reason),
    StateMachine model cmd m resp)
forall a b. (a, b) -> a
fst ((((History cmd resp, model Concrete, Reason, Reason),
   StateMachine model cmd m resp),
  ())
 -> ((History cmd resp, model Concrete, Reason, Reason),
     StateMachine model cmd m resp))
-> m (((History cmd resp, model Concrete, Reason, Reason),
       StateMachine model cmd m resp),
      ())
-> m ((History cmd resp, model Concrete, Reason, Reason),
      StateMachine model cmd m resp)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (StateMachine model cmd m resp)
-> (StateMachine model cmd m resp
    -> ExitCase
         ((History cmd resp, model Concrete, Reason, Reason),
          StateMachine model cmd m resp)
    -> m ())
-> (StateMachine model cmd m resp
    -> m ((History cmd resp, model Concrete, Reason, Reason),
          StateMachine model cmd m resp))
-> m (((History cmd resp, model Concrete, Reason, Reason),
       StateMachine model cmd m resp),
      ())
forall a b c.
HasCallStack =>
m a -> (a -> ExitCase b -> m c) -> (a -> m b) -> m (b, c)
forall (m :: * -> *) a b c.
(MonadMask m, HasCallStack) =>
m a -> (a -> ExitCase b -> m c) -> (a -> m b) -> m (b, c)
generalBracket
              m (StateMachine model cmd m resp)
msm
              (\StateMachine model cmd m resp
sm' ExitCase
  ((History cmd resp, model Concrete, Reason, Reason),
   StateMachine model cmd m resp)
ec -> case ExitCase
  ((History cmd resp, model Concrete, Reason, Reason),
   StateMachine model cmd m resp)
ec of
                            ExitCaseSuccess ((History cmd resp
_, model Concrete
model, Reason
_, Reason
_), StateMachine model cmd m resp
_) -> StateMachine model cmd m resp -> model Concrete -> m ()
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> model Concrete -> m ()
cleanup StateMachine model cmd m resp
sm' model Concrete
model
                            ExitCase
  ((History cmd resp, model Concrete, Reason, Reason),
   StateMachine model cmd m resp)
_ -> TChan (Pid, HistoryEvent cmd resp)
-> m [(Pid, HistoryEvent cmd resp)]
forall (m :: * -> *) a. MonadIO m => TChan a -> m [a]
getChanContents TChan (Pid, HistoryEvent cmd resp)
hchan m [(Pid, HistoryEvent cmd resp)]
-> ([(Pid, HistoryEvent cmd resp)] -> m ()) -> m ()
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= StateMachine model cmd m resp -> model Concrete -> m ()
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> model Concrete -> m ()
cleanup StateMachine model cmd m resp
sm' (model Concrete -> m ())
-> ([(Pid, HistoryEvent cmd resp)] -> model Concrete)
-> [(Pid, HistoryEvent cmd resp)]
-> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StateMachine model cmd m resp -> History cmd resp -> model Concrete
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> History cmd resp -> model Concrete
mkModel StateMachine model cmd m resp
sm' (History cmd resp -> model Concrete)
-> ([(Pid, HistoryEvent cmd resp)] -> History cmd resp)
-> [(Pid, HistoryEvent cmd resp)]
-> model Concrete
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Pid, HistoryEvent cmd resp)] -> History cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
History' cmd resp -> History cmd resp
History
              )
              (\StateMachine model cmd m resp
sm' -> (,StateMachine model cmd m resp
sm') ((History cmd resp, model Concrete, Reason, Reason)
 -> ((History cmd resp, model Concrete, Reason, Reason),
     StateMachine model cmd m resp))
-> m (History cmd resp, model Concrete, Reason, Reason)
-> m ((History cmd resp, model Concrete, Reason, Reason),
      StateMachine model cmd m resp)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateMachine model cmd m resp
-> ParallelCommands cmd resp
-> TChan (Pid, HistoryEvent cmd resp)
-> Bool
-> m (History cmd resp, model Concrete, Reason, Reason)
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
       (model :: (* -> *) -> *).
(Show (cmd Concrete), Show (resp Concrete), Traversable cmd,
 Foldable resp, MonadMask m, MonadUnliftIO m) =>
StateMachine model cmd m resp
-> ParallelCommands cmd resp
-> TChan (Pid, HistoryEvent cmd resp)
-> Bool
-> m (History cmd resp, model Concrete, Reason, Reason)
executeParallelCommands StateMachine model cmd m resp
sm' ParallelCommands cmd resp
cmds TChan (Pid, HistoryEvent cmd resp)
hchan Bool
True)
    (History cmd resp, model Concrete, Logic)
-> PropertyM m (History cmd resp, model Concrete, Logic)
forall a. a -> PropertyM m a
forall (m :: * -> *) a. Monad m => a -> m a
return (History cmd resp
hist, model Concrete
model, Reason -> Logic
logicReason ([Reason] -> Reason
combineReasons [Reason
reason1, Reason
reason2]) Logic -> Logic -> Logic
.&& StateMachine model cmd m resp -> History cmd resp -> Logic
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
(Show (cmd Concrete), Show (resp Concrete)) =>
StateMachine model cmd m resp -> History cmd resp -> Logic
linearise StateMachine model cmd m resp
sm' History cmd resp
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.
                           -> m (StateMachine model cmd m resp)
                           -> (cmd Concrete -> resp Concrete)
                           -> ParallelCommands cmd resp
                           -> PropertyM m [(History cmd resp, model Concrete, Logic)]
runParallelCommandsNTimes' :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
       (model :: (* -> *) -> *).
(Show (cmd Concrete), Show (resp Concrete), Traversable cmd,
 Foldable resp, MonadMask m, MonadUnliftIO m) =>
Int
-> m (StateMachine model cmd m resp)
-> (cmd Concrete -> resp Concrete)
-> ParallelCommands cmd resp
-> PropertyM m [(History cmd resp, model Concrete, Logic)]
runParallelCommandsNTimes' Int
n m (StateMachine model cmd m resp)
msm cmd Concrete -> resp Concrete
complete ParallelCommands cmd resp
cmds =
  Int
-> PropertyM m (History cmd resp, model Concrete, Logic)
-> PropertyM m [(History cmd resp, model Concrete, Logic)]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
n (PropertyM m (History cmd resp, model Concrete, Logic)
 -> PropertyM m [(History cmd resp, model Concrete, Logic)])
-> PropertyM m (History cmd resp, model Concrete, Logic)
-> PropertyM m [(History cmd resp, model Concrete, Logic)]
forall a b. (a -> b) -> a -> b
$ do
    TChan (Pid, HistoryEvent cmd resp)
hchan <- PropertyM m (TChan (Pid, HistoryEvent cmd resp))
forall (m :: * -> *) a. MonadIO m => m (TChan a)
newTChanIO
    ((History cmd resp
hist, model Concrete
model, Reason
_, Reason
_), StateMachine model cmd m resp
sm') <- m ((History cmd resp, model Concrete, Reason, Reason),
   StateMachine model cmd m resp)
-> PropertyM
     m
     ((History cmd resp, model Concrete, Reason, Reason),
      StateMachine model cmd m resp)
forall (m :: * -> *) a. Monad m => m a -> PropertyM m a
run (m ((History cmd resp, model Concrete, Reason, Reason),
    StateMachine model cmd m resp)
 -> PropertyM
      m
      ((History cmd resp, model Concrete, Reason, Reason),
       StateMachine model cmd m resp))
-> m ((History cmd resp, model Concrete, Reason, Reason),
      StateMachine model cmd m resp)
-> PropertyM
     m
     ((History cmd resp, model Concrete, Reason, Reason),
      StateMachine model cmd m resp)
forall a b. (a -> b) -> a -> b
$
      (((History cmd resp, model Concrete, Reason, Reason),
  StateMachine model cmd m resp),
 ())
-> ((History cmd resp, model Concrete, Reason, Reason),
    StateMachine model cmd m resp)
forall a b. (a, b) -> a
fst ((((History cmd resp, model Concrete, Reason, Reason),
   StateMachine model cmd m resp),
  ())
 -> ((History cmd resp, model Concrete, Reason, Reason),
     StateMachine model cmd m resp))
-> m (((History cmd resp, model Concrete, Reason, Reason),
       StateMachine model cmd m resp),
      ())
-> m ((History cmd resp, model Concrete, Reason, Reason),
      StateMachine model cmd m resp)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (StateMachine model cmd m resp)
-> (StateMachine model cmd m resp
    -> ExitCase
         ((History cmd resp, model Concrete, Reason, Reason),
          StateMachine model cmd m resp)
    -> m ())
-> (StateMachine model cmd m resp
    -> m ((History cmd resp, model Concrete, Reason, Reason),
          StateMachine model cmd m resp))
-> m (((History cmd resp, model Concrete, Reason, Reason),
       StateMachine model cmd m resp),
      ())
forall a b c.
HasCallStack =>
m a -> (a -> ExitCase b -> m c) -> (a -> m b) -> m (b, c)
forall (m :: * -> *) a b c.
(MonadMask m, HasCallStack) =>
m a -> (a -> ExitCase b -> m c) -> (a -> m b) -> m (b, c)
generalBracket
              m (StateMachine model cmd m resp)
msm
              (\StateMachine model cmd m resp
sm' ExitCase
  ((History cmd resp, model Concrete, Reason, Reason),
   StateMachine model cmd m resp)
ec -> case ExitCase
  ((History cmd resp, model Concrete, Reason, Reason),
   StateMachine model cmd m resp)
ec of
                            ExitCaseSuccess ((History cmd resp
_, model Concrete
model, Reason
_, Reason
_), StateMachine model cmd m resp
_) -> StateMachine model cmd m resp -> model Concrete -> m ()
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> model Concrete -> m ()
cleanup StateMachine model cmd m resp
sm' model Concrete
model
                            ExitCase
  ((History cmd resp, model Concrete, Reason, Reason),
   StateMachine model cmd m resp)
_ -> TChan (Pid, HistoryEvent cmd resp)
-> m [(Pid, HistoryEvent cmd resp)]
forall (m :: * -> *) a. MonadIO m => TChan a -> m [a]
getChanContents TChan (Pid, HistoryEvent cmd resp)
hchan m [(Pid, HistoryEvent cmd resp)]
-> ([(Pid, HistoryEvent cmd resp)] -> m ()) -> m ()
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= StateMachine model cmd m resp -> model Concrete -> m ()
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> model Concrete -> m ()
cleanup StateMachine model cmd m resp
sm' (model Concrete -> m ())
-> ([(Pid, HistoryEvent cmd resp)] -> model Concrete)
-> [(Pid, HistoryEvent cmd resp)]
-> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StateMachine model cmd m resp -> History cmd resp -> model Concrete
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> History cmd resp -> model Concrete
mkModel StateMachine model cmd m resp
sm' (History cmd resp -> model Concrete)
-> ([(Pid, HistoryEvent cmd resp)] -> History cmd resp)
-> [(Pid, HistoryEvent cmd resp)]
-> model Concrete
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Pid, HistoryEvent cmd resp)] -> History cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
History' cmd resp -> History cmd resp
History
              )
              (\StateMachine model cmd m resp
sm' -> (,StateMachine model cmd m resp
sm') ((History cmd resp, model Concrete, Reason, Reason)
 -> ((History cmd resp, model Concrete, Reason, Reason),
     StateMachine model cmd m resp))
-> m (History cmd resp, model Concrete, Reason, Reason)
-> m ((History cmd resp, model Concrete, Reason, Reason),
      StateMachine model cmd m resp)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateMachine model cmd m resp
-> ParallelCommands cmd resp
-> TChan (Pid, HistoryEvent cmd resp)
-> Bool
-> m (History cmd resp, model Concrete, Reason, Reason)
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
       (model :: (* -> *) -> *).
(Show (cmd Concrete), Show (resp Concrete), Traversable cmd,
 Foldable resp, MonadMask m, MonadUnliftIO m) =>
StateMachine model cmd m resp
-> ParallelCommands cmd resp
-> TChan (Pid, HistoryEvent cmd resp)
-> Bool
-> m (History cmd resp, model Concrete, Reason, Reason)
executeParallelCommands StateMachine model cmd m resp
sm' ParallelCommands cmd resp
cmds TChan (Pid, HistoryEvent cmd resp)
hchan Bool
True)
    let hist' :: History cmd resp
hist' = (cmd Concrete -> resp Concrete)
-> History cmd resp -> History cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
(cmd Concrete -> resp Concrete)
-> History cmd resp -> History cmd resp
completeHistory cmd Concrete -> resp Concrete
complete History cmd resp
hist
    (History cmd resp, model Concrete, Logic)
-> PropertyM m (History cmd resp, model Concrete, Logic)
forall a. a -> PropertyM m a
forall (m :: * -> *) a. Monad m => a -> m a
return (History cmd resp
hist', model Concrete
model, StateMachine model cmd m resp -> History cmd resp -> Logic
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
(Show (cmd Concrete), Show (resp Concrete)) =>
StateMachine model cmd m resp -> History cmd resp -> Logic
linearise StateMachine model cmd m resp
sm' History cmd resp
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, model Concrete, Logic)]
runNParallelCommandsNTimes :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
       (model :: (* -> *) -> *).
(Show (cmd Concrete), Show (resp Concrete), Traversable cmd,
 Foldable resp, MonadMask m, MonadUnliftIO m) =>
Int
-> StateMachine model cmd m resp
-> NParallelCommands cmd resp
-> PropertyM m [(History cmd resp, model Concrete, Logic)]
runNParallelCommandsNTimes Int
n StateMachine model cmd m resp
sm = Int
-> m (StateMachine model cmd m resp)
-> NParallelCommands cmd resp
-> PropertyM m [(History cmd resp, model Concrete, Logic)]
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
       (model :: (* -> *) -> *).
(Show (cmd Concrete), Show (resp Concrete), Traversable cmd,
 Foldable resp, MonadMask m, MonadUnliftIO m) =>
Int
-> m (StateMachine model cmd m resp)
-> NParallelCommands cmd resp
-> PropertyM m [(History cmd resp, model Concrete, Logic)]
runNParallelCommandsNTimesWithSetup Int
n (StateMachine model cmd m resp -> m (StateMachine model cmd m resp)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure StateMachine model cmd m resp
sm)

runNParallelCommandsNTimesWithSetup :: (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.
                           -> m (StateMachine model cmd m resp)
                           -> NParallelCommands cmd resp
                           -> PropertyM m [(History cmd resp, model Concrete, Logic)]
runNParallelCommandsNTimesWithSetup :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
       (model :: (* -> *) -> *).
(Show (cmd Concrete), Show (resp Concrete), Traversable cmd,
 Foldable resp, MonadMask m, MonadUnliftIO m) =>
Int
-> m (StateMachine model cmd m resp)
-> NParallelCommands cmd resp
-> PropertyM m [(History cmd resp, model Concrete, Logic)]
runNParallelCommandsNTimesWithSetup Int
n m (StateMachine model cmd m resp)
msm NParallelCommands cmd resp
cmds =
  Int
-> PropertyM m (History cmd resp, model Concrete, Logic)
-> PropertyM m [(History cmd resp, model Concrete, Logic)]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
n (PropertyM m (History cmd resp, model Concrete, Logic)
 -> PropertyM m [(History cmd resp, model Concrete, Logic)])
-> PropertyM m (History cmd resp, model Concrete, Logic)
-> PropertyM m [(History cmd resp, model Concrete, Logic)]
forall a b. (a -> b) -> a -> b
$ do
    TChan (Pid, HistoryEvent cmd resp)
hchan <- PropertyM m (TChan (Pid, HistoryEvent cmd resp))
forall (m :: * -> *) a. MonadIO m => m (TChan a)
newTChanIO
    ((History cmd resp
hist, model Concrete
model, Reason
reason), StateMachine model cmd m resp
sm') <- m ((History cmd resp, model Concrete, Reason),
   StateMachine model cmd m resp)
-> PropertyM
     m
     ((History cmd resp, model Concrete, Reason),
      StateMachine model cmd m resp)
forall (m :: * -> *) a. Monad m => m a -> PropertyM m a
run (m ((History cmd resp, model Concrete, Reason),
    StateMachine model cmd m resp)
 -> PropertyM
      m
      ((History cmd resp, model Concrete, Reason),
       StateMachine model cmd m resp))
-> m ((History cmd resp, model Concrete, Reason),
      StateMachine model cmd m resp)
-> PropertyM
     m
     ((History cmd resp, model Concrete, Reason),
      StateMachine model cmd m resp)
forall a b. (a -> b) -> a -> b
$
      (((History cmd resp, model Concrete, Reason),
  StateMachine model cmd m resp),
 ())
-> ((History cmd resp, model Concrete, Reason),
    StateMachine model cmd m resp)
forall a b. (a, b) -> a
fst ((((History cmd resp, model Concrete, Reason),
   StateMachine model cmd m resp),
  ())
 -> ((History cmd resp, model Concrete, Reason),
     StateMachine model cmd m resp))
-> m (((History cmd resp, model Concrete, Reason),
       StateMachine model cmd m resp),
      ())
-> m ((History cmd resp, model Concrete, Reason),
      StateMachine model cmd m resp)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (StateMachine model cmd m resp)
-> (StateMachine model cmd m resp
    -> ExitCase
         ((History cmd resp, model Concrete, Reason),
          StateMachine model cmd m resp)
    -> m ())
-> (StateMachine model cmd m resp
    -> m ((History cmd resp, model Concrete, Reason),
          StateMachine model cmd m resp))
-> m (((History cmd resp, model Concrete, Reason),
       StateMachine model cmd m resp),
      ())
forall a b c.
HasCallStack =>
m a -> (a -> ExitCase b -> m c) -> (a -> m b) -> m (b, c)
forall (m :: * -> *) a b c.
(MonadMask m, HasCallStack) =>
m a -> (a -> ExitCase b -> m c) -> (a -> m b) -> m (b, c)
generalBracket
              m (StateMachine model cmd m resp)
msm
              (\StateMachine model cmd m resp
sm' ExitCase
  ((History cmd resp, model Concrete, Reason),
   StateMachine model cmd m resp)
ec -> case ExitCase
  ((History cmd resp, model Concrete, Reason),
   StateMachine model cmd m resp)
ec of
                            ExitCaseSuccess ((History cmd resp
_, model Concrete
model, Reason
_), StateMachine model cmd m resp
_) -> StateMachine model cmd m resp -> model Concrete -> m ()
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> model Concrete -> m ()
cleanup StateMachine model cmd m resp
sm' model Concrete
model
                            ExitCase
  ((History cmd resp, model Concrete, Reason),
   StateMachine model cmd m resp)
_ -> TChan (Pid, HistoryEvent cmd resp)
-> m [(Pid, HistoryEvent cmd resp)]
forall (m :: * -> *) a. MonadIO m => TChan a -> m [a]
getChanContents TChan (Pid, HistoryEvent cmd resp)
hchan m [(Pid, HistoryEvent cmd resp)]
-> ([(Pid, HistoryEvent cmd resp)] -> m ()) -> m ()
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= StateMachine model cmd m resp -> model Concrete -> m ()
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> model Concrete -> m ()
cleanup StateMachine model cmd m resp
sm' (model Concrete -> m ())
-> ([(Pid, HistoryEvent cmd resp)] -> model Concrete)
-> [(Pid, HistoryEvent cmd resp)]
-> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StateMachine model cmd m resp -> History cmd resp -> model Concrete
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> History cmd resp -> model Concrete
mkModel StateMachine model cmd m resp
sm' (History cmd resp -> model Concrete)
-> ([(Pid, HistoryEvent cmd resp)] -> History cmd resp)
-> [(Pid, HistoryEvent cmd resp)]
-> model Concrete
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Pid, HistoryEvent cmd resp)] -> History cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
History' cmd resp -> History cmd resp
History
              )
              (\StateMachine model cmd m resp
sm' -> (,StateMachine model cmd m resp
sm') ((History cmd resp, model Concrete, Reason)
 -> ((History cmd resp, model Concrete, Reason),
     StateMachine model cmd m resp))
-> m (History cmd resp, model Concrete, Reason)
-> m ((History cmd resp, model Concrete, Reason),
      StateMachine model cmd m resp)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateMachine model cmd m resp
-> NParallelCommands cmd resp
-> TChan (Pid, HistoryEvent cmd resp)
-> Bool
-> m (History cmd resp, model Concrete, Reason)
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
       (model :: (* -> *) -> *).
(Traversable cmd, Show (cmd Concrete), Foldable resp,
 Show (resp Concrete), MonadMask m, MonadUnliftIO m) =>
StateMachine model cmd m resp
-> NParallelCommands cmd resp
-> TChan (Pid, HistoryEvent cmd resp)
-> Bool
-> m (History cmd resp, model Concrete, Reason)
executeNParallelCommands StateMachine model cmd m resp
sm' NParallelCommands cmd resp
cmds TChan (Pid, HistoryEvent cmd resp)
hchan Bool
True)
    (History cmd resp, model Concrete, Logic)
-> PropertyM m (History cmd resp, model Concrete, Logic)
forall a. a -> PropertyM m a
forall (m :: * -> *) a. Monad m => a -> m a
return (History cmd resp
hist, model Concrete
model, Reason -> Logic
logicReason Reason
reason Logic -> Logic -> Logic
.&& StateMachine model cmd m resp -> History cmd resp -> Logic
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
(Show (cmd Concrete), Show (resp Concrete)) =>
StateMachine model cmd m resp -> History cmd resp -> Logic
linearise StateMachine model cmd m resp
sm' History cmd resp
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.
                            -> m (StateMachine model cmd m resp)
                            -> (cmd Concrete -> resp Concrete)
                            -> NParallelCommands cmd resp
                            -> PropertyM m [(History cmd resp, model Concrete, Logic)]
runNParallelCommandsNTimes' :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
       (model :: (* -> *) -> *).
(Show (cmd Concrete), Show (resp Concrete), Traversable cmd,
 Foldable resp, MonadMask m, MonadUnliftIO m) =>
Int
-> m (StateMachine model cmd m resp)
-> (cmd Concrete -> resp Concrete)
-> NParallelCommands cmd resp
-> PropertyM m [(History cmd resp, model Concrete, Logic)]
runNParallelCommandsNTimes' Int
n m (StateMachine model cmd m resp)
msm cmd Concrete -> resp Concrete
complete NParallelCommands cmd resp
cmds =
  Int
-> PropertyM m (History cmd resp, model Concrete, Logic)
-> PropertyM m [(History cmd resp, model Concrete, Logic)]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
n (PropertyM m (History cmd resp, model Concrete, Logic)
 -> PropertyM m [(History cmd resp, model Concrete, Logic)])
-> PropertyM m (History cmd resp, model Concrete, Logic)
-> PropertyM m [(History cmd resp, model Concrete, Logic)]
forall a b. (a -> b) -> a -> b
$ do
    TChan (Pid, HistoryEvent cmd resp)
hchan <- PropertyM m (TChan (Pid, HistoryEvent cmd resp))
forall (m :: * -> *) a. MonadIO m => m (TChan a)
newTChanIO
    ((History cmd resp
hist, model Concrete
model, Reason
_reason), StateMachine model cmd m resp
sm') <- m ((History cmd resp, model Concrete, Reason),
   StateMachine model cmd m resp)
-> PropertyM
     m
     ((History cmd resp, model Concrete, Reason),
      StateMachine model cmd m resp)
forall (m :: * -> *) a. Monad m => m a -> PropertyM m a
run (m ((History cmd resp, model Concrete, Reason),
    StateMachine model cmd m resp)
 -> PropertyM
      m
      ((History cmd resp, model Concrete, Reason),
       StateMachine model cmd m resp))
-> m ((History cmd resp, model Concrete, Reason),
      StateMachine model cmd m resp)
-> PropertyM
     m
     ((History cmd resp, model Concrete, Reason),
      StateMachine model cmd m resp)
forall a b. (a -> b) -> a -> b
$
      (((History cmd resp, model Concrete, Reason),
  StateMachine model cmd m resp),
 ())
-> ((History cmd resp, model Concrete, Reason),
    StateMachine model cmd m resp)
forall a b. (a, b) -> a
fst ((((History cmd resp, model Concrete, Reason),
   StateMachine model cmd m resp),
  ())
 -> ((History cmd resp, model Concrete, Reason),
     StateMachine model cmd m resp))
-> m (((History cmd resp, model Concrete, Reason),
       StateMachine model cmd m resp),
      ())
-> m ((History cmd resp, model Concrete, Reason),
      StateMachine model cmd m resp)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (StateMachine model cmd m resp)
-> (StateMachine model cmd m resp
    -> ExitCase
         ((History cmd resp, model Concrete, Reason),
          StateMachine model cmd m resp)
    -> m ())
-> (StateMachine model cmd m resp
    -> m ((History cmd resp, model Concrete, Reason),
          StateMachine model cmd m resp))
-> m (((History cmd resp, model Concrete, Reason),
       StateMachine model cmd m resp),
      ())
forall a b c.
HasCallStack =>
m a -> (a -> ExitCase b -> m c) -> (a -> m b) -> m (b, c)
forall (m :: * -> *) a b c.
(MonadMask m, HasCallStack) =>
m a -> (a -> ExitCase b -> m c) -> (a -> m b) -> m (b, c)
generalBracket
              m (StateMachine model cmd m resp)
msm
              (\StateMachine model cmd m resp
sm' ExitCase
  ((History cmd resp, model Concrete, Reason),
   StateMachine model cmd m resp)
ec -> case ExitCase
  ((History cmd resp, model Concrete, Reason),
   StateMachine model cmd m resp)
ec of
                            ExitCaseSuccess ((History cmd resp
_, model Concrete
model, Reason
_), StateMachine model cmd m resp
_) -> StateMachine model cmd m resp -> model Concrete -> m ()
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> model Concrete -> m ()
cleanup StateMachine model cmd m resp
sm' model Concrete
model
                            ExitCase
  ((History cmd resp, model Concrete, Reason),
   StateMachine model cmd m resp)
_ -> TChan (Pid, HistoryEvent cmd resp)
-> m [(Pid, HistoryEvent cmd resp)]
forall (m :: * -> *) a. MonadIO m => TChan a -> m [a]
getChanContents TChan (Pid, HistoryEvent cmd resp)
hchan m [(Pid, HistoryEvent cmd resp)]
-> ([(Pid, HistoryEvent cmd resp)] -> m ()) -> m ()
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= StateMachine model cmd m resp -> model Concrete -> m ()
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> model Concrete -> m ()
cleanup StateMachine model cmd m resp
sm' (model Concrete -> m ())
-> ([(Pid, HistoryEvent cmd resp)] -> model Concrete)
-> [(Pid, HistoryEvent cmd resp)]
-> m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StateMachine model cmd m resp -> History cmd resp -> model Concrete
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> History cmd resp -> model Concrete
mkModel StateMachine model cmd m resp
sm' (History cmd resp -> model Concrete)
-> ([(Pid, HistoryEvent cmd resp)] -> History cmd resp)
-> [(Pid, HistoryEvent cmd resp)]
-> model Concrete
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Pid, HistoryEvent cmd resp)] -> History cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
History' cmd resp -> History cmd resp
History
              )
              (\StateMachine model cmd m resp
sm' -> (,StateMachine model cmd m resp
sm') ((History cmd resp, model Concrete, Reason)
 -> ((History cmd resp, model Concrete, Reason),
     StateMachine model cmd m resp))
-> m (History cmd resp, model Concrete, Reason)
-> m ((History cmd resp, model Concrete, Reason),
      StateMachine model cmd m resp)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StateMachine model cmd m resp
-> NParallelCommands cmd resp
-> TChan (Pid, HistoryEvent cmd resp)
-> Bool
-> m (History cmd resp, model Concrete, Reason)
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
       (model :: (* -> *) -> *).
(Traversable cmd, Show (cmd Concrete), Foldable resp,
 Show (resp Concrete), MonadMask m, MonadUnliftIO m) =>
StateMachine model cmd m resp
-> NParallelCommands cmd resp
-> TChan (Pid, HistoryEvent cmd resp)
-> Bool
-> m (History cmd resp, model Concrete, Reason)
executeNParallelCommands StateMachine model cmd m resp
sm' NParallelCommands cmd resp
cmds TChan (Pid, HistoryEvent cmd resp)
hchan Bool
True)
    let hist' :: History cmd resp
hist' = (cmd Concrete -> resp Concrete)
-> History cmd resp -> History cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
(cmd Concrete -> resp Concrete)
-> History cmd resp -> History cmd resp
completeHistory cmd Concrete -> resp Concrete
complete History cmd resp
hist
    (History cmd resp, model Concrete, Logic)
-> PropertyM m (History cmd resp, model Concrete, Logic)
forall a. a -> PropertyM m a
forall (m :: * -> *) a. Monad m => a -> m a
return (History cmd resp
hist, model Concrete
model, StateMachine model cmd m resp -> History cmd resp -> Logic
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
(Show (cmd Concrete), Show (resp Concrete)) =>
StateMachine model cmd m resp -> History cmd resp -> Logic
linearise StateMachine model cmd m resp
sm' History cmd resp
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
                        -> UIO.TChan (Pid, HistoryEvent cmd resp)
                        -> Bool
                        -> m (History cmd resp, model Concrete, Reason, Reason)
executeParallelCommands :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
       (model :: (* -> *) -> *).
(Show (cmd Concrete), Show (resp Concrete), Traversable cmd,
 Foldable resp, MonadMask m, MonadUnliftIO m) =>
StateMachine model cmd m resp
-> ParallelCommands cmd resp
-> TChan (Pid, HistoryEvent cmd resp)
-> Bool
-> m (History cmd resp, model Concrete, Reason, Reason)
executeParallelCommands sm :: StateMachine model cmd m resp
sm@StateMachine{ forall (r :: * -> *). model r
initModel :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> forall (r :: * -> *). model r
initModel :: forall (r :: * -> *). model r
initModel } (ParallelCommands Commands cmd resp
prefix [Pair (Commands cmd resp)]
suffixes) TChan (Pid, HistoryEvent cmd resp)
hchan Bool
stopOnError = do

  (Reason
reason0, (Environment
env0, model Symbolic
_smodel, Counter
_counter, model Concrete
cmodel)) <- StateT
  (Environment, model Symbolic, Counter, model Concrete) m Reason
-> (Environment, model Symbolic, Counter, model Concrete)
-> m (Reason,
      (Environment, model Symbolic, Counter, model Concrete))
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT
      (StateMachine model cmd m resp
-> TChan (Pid, HistoryEvent cmd resp)
-> Pid
-> Check
-> Commands cmd resp
-> StateT
     (Environment, model Symbolic, Counter, model Concrete) m Reason
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
       (model :: (* -> *) -> *).
(Show (cmd Concrete), Show (resp Concrete), Traversable cmd,
 Foldable resp, MonadCatch m, MonadIO m) =>
StateMachine model cmd m resp
-> TChan (Pid, HistoryEvent cmd resp)
-> Pid
-> Check
-> Commands cmd resp
-> StateT
     (Environment, model Symbolic, Counter, model Concrete) m Reason
executeCommands StateMachine model cmd m resp
sm TChan (Pid, HistoryEvent cmd resp)
hchan (Int -> Pid
Pid Int
0) Check
CheckEverything Commands cmd resp
prefix)
      (Environment
emptyEnvironment, model Symbolic
forall (r :: * -> *). model r
initModel, Counter
newCounter, model Concrete
forall (r :: * -> *). model r
initModel)
  if Reason
reason0 Reason -> Reason -> Bool
forall a. Eq a => a -> a -> Bool
/= Reason
Ok
  then do
    [(Pid, HistoryEvent cmd resp)]
hist <- TChan (Pid, HistoryEvent cmd resp)
-> m [(Pid, HistoryEvent cmd resp)]
forall (m :: * -> *) a. MonadIO m => TChan a -> m [a]
getChanContents TChan (Pid, HistoryEvent cmd resp)
hchan
    (History cmd resp, model Concrete, Reason, Reason)
-> m (History cmd resp, model Concrete, Reason, Reason)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Pid, HistoryEvent cmd resp)] -> History cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
History' cmd resp -> History cmd resp
History [(Pid, HistoryEvent cmd resp)]
hist, model Concrete
cmodel, Reason
reason0, Reason
reason0)
  else do
    (Reason
reason1, Reason
reason2, Environment
_) <- (Reason, Reason, Environment)
-> [Pair (Commands cmd resp)] -> m (Reason, Reason, Environment)
go (Reason
Ok, Reason
Ok, Environment
env0) [Pair (Commands cmd resp)]
suffixes
    [(Pid, HistoryEvent cmd resp)]
hist <- TChan (Pid, HistoryEvent cmd resp)
-> m [(Pid, HistoryEvent cmd resp)]
forall (m :: * -> *) a. MonadIO m => TChan a -> m [a]
getChanContents TChan (Pid, HistoryEvent cmd resp)
hchan
    (History cmd resp, model Concrete, Reason, Reason)
-> m (History cmd resp, model Concrete, Reason, Reason)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Pid, HistoryEvent cmd resp)] -> History cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
History' cmd resp -> History cmd resp
History [(Pid, HistoryEvent cmd resp)]
hist, model Concrete
cmodel, Reason
reason1, Reason
reason2)
  where
    go :: (Reason, Reason, Environment)
-> [Pair (Commands cmd resp)] -> m (Reason, Reason, Environment)
go (Reason
res1, Reason
res2, Environment
env) []                         = (Reason, Reason, Environment) -> m (Reason, Reason, Environment)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Reason
res1, Reason
res2, Environment
env)
    go (Reason
Ok,   Reason
Ok,   Environment
env) (Pair Commands cmd resp
cmds1 Commands cmd resp
cmds2 : [Pair (Commands cmd resp)]
pairs) = do

      ((Reason
reason1, (Environment
env1, model Symbolic
_, Counter
_, model Concrete
_)), (Reason
reason2, (Environment
env2, model Symbolic
_, Counter
_, model Concrete
_))) <- m (Reason, (Environment, model Symbolic, Counter, model Concrete))
-> m (Reason,
      (Environment, model Symbolic, Counter, model Concrete))
-> m ((Reason,
       (Environment, model Symbolic, Counter, model Concrete)),
      (Reason, (Environment, model Symbolic, Counter, model Concrete)))
forall (m :: * -> *) a b. MonadUnliftIO m => m a -> m b -> m (a, b)
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...

        (StateT
  (Environment, model Symbolic, Counter, model Concrete) m Reason
-> (Environment, model Symbolic, Counter, model Concrete)
-> m (Reason,
      (Environment, model Symbolic, Counter, model Concrete))
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (StateMachine model cmd m resp
-> TChan (Pid, HistoryEvent cmd resp)
-> Pid
-> Check
-> Commands cmd resp
-> StateT
     (Environment, model Symbolic, Counter, model Concrete) m Reason
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
       (model :: (* -> *) -> *).
(Show (cmd Concrete), Show (resp Concrete), Traversable cmd,
 Foldable resp, MonadCatch m, MonadIO m) =>
StateMachine model cmd m resp
-> TChan (Pid, HistoryEvent cmd resp)
-> Pid
-> Check
-> Commands cmd resp
-> StateT
     (Environment, model Symbolic, Counter, model Concrete) m Reason
executeCommands StateMachine model cmd m resp
sm TChan (Pid, HistoryEvent cmd resp)
hchan (Int -> Pid
Pid Int
1) Check
CheckNothing Commands cmd resp
cmds1) (Environment
env, model Symbolic
forall (r :: * -> *). model r
initModel, Counter
newCounter, model Concrete
forall (r :: * -> *). model r
initModel))
        (StateT
  (Environment, model Symbolic, Counter, model Concrete) m Reason
-> (Environment, model Symbolic, Counter, model Concrete)
-> m (Reason,
      (Environment, model Symbolic, Counter, model Concrete))
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (StateMachine model cmd m resp
-> TChan (Pid, HistoryEvent cmd resp)
-> Pid
-> Check
-> Commands cmd resp
-> StateT
     (Environment, model Symbolic, Counter, model Concrete) m Reason
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
       (model :: (* -> *) -> *).
(Show (cmd Concrete), Show (resp Concrete), Traversable cmd,
 Foldable resp, MonadCatch m, MonadIO m) =>
StateMachine model cmd m resp
-> TChan (Pid, HistoryEvent cmd resp)
-> Pid
-> Check
-> Commands cmd resp
-> StateT
     (Environment, model Symbolic, Counter, model Concrete) m Reason
executeCommands StateMachine model cmd m resp
sm TChan (Pid, HistoryEvent cmd resp)
hchan (Int -> Pid
Pid Int
2) Check
CheckNothing Commands cmd resp
cmds2) (Environment
env, model Symbolic
forall (r :: * -> *). model r
initModel, Counter
newCounter, model Concrete
forall (r :: * -> *). model r
initModel))
      case (Reason -> Bool
isOK (Reason -> Bool) -> Reason -> Bool
forall a b. (a -> b) -> a -> b
$ [Reason] -> Reason
combineReasons [Reason
reason1, Reason
reason2], Bool
stopOnError) of
        (Bool
False, Bool
True) -> (Reason, Reason, Environment) -> m (Reason, Reason, Environment)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Reason
reason1, Reason
reason2, Environment
env1 Environment -> Environment -> Environment
forall a. Semigroup a => a -> a -> a
<> Environment
env2)
        (Bool, Bool)
_ -> (Reason, Reason, Environment)
-> [Pair (Commands cmd resp)] -> m (Reason, Reason, Environment)
go ( Reason
reason1
                , Reason
reason2
                , Environment
env1 Environment -> Environment -> Environment
forall a. Semigroup a => a -> a -> a
<> Environment
env2
                ) [Pair (Commands cmd resp)]
pairs
    go (Reason
Ok, ExceptionThrown String
e, Environment
env) (Pair Commands cmd resp
cmds1 Commands cmd resp
_cmds2 : [Pair (Commands cmd resp)]
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?
      --
      (Reason
reason1, (Environment
env1, model Symbolic
_, Counter
_, model Concrete
_)) <- StateT
  (Environment, model Symbolic, Counter, model Concrete) m Reason
-> (Environment, model Symbolic, Counter, model Concrete)
-> m (Reason,
      (Environment, model Symbolic, Counter, model Concrete))
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (StateMachine model cmd m resp
-> TChan (Pid, HistoryEvent cmd resp)
-> Pid
-> Check
-> Commands cmd resp
-> StateT
     (Environment, model Symbolic, Counter, model Concrete) m Reason
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
       (model :: (* -> *) -> *).
(Show (cmd Concrete), Show (resp Concrete), Traversable cmd,
 Foldable resp, MonadCatch m, MonadIO m) =>
StateMachine model cmd m resp
-> TChan (Pid, HistoryEvent cmd resp)
-> Pid
-> Check
-> Commands cmd resp
-> StateT
     (Environment, model Symbolic, Counter, model Concrete) m Reason
executeCommands StateMachine model cmd m resp
sm TChan (Pid, HistoryEvent cmd resp)
hchan (Int -> Pid
Pid Int
1) Check
CheckPrecondition Commands cmd resp
cmds1)
                                              (Environment
env, model Symbolic
forall (r :: * -> *). model r
initModel, Counter
newCounter, model Concrete
forall (r :: * -> *). model r
initModel)
      (Reason, Reason, Environment)
-> [Pair (Commands cmd resp)] -> m (Reason, Reason, Environment)
go ( Reason
reason1
         , String -> Reason
ExceptionThrown String
e
         , Environment
env1
         ) [Pair (Commands cmd resp)]
pairs
    go (ExceptionThrown String
e, Reason
Ok, Environment
env) (Pair Commands cmd resp
_cmds1 Commands cmd resp
cmds2 : [Pair (Commands cmd resp)]
pairs) = do

      (Reason
reason2, (Environment
env2, model Symbolic
_, Counter
_, model Concrete
_)) <- StateT
  (Environment, model Symbolic, Counter, model Concrete) m Reason
-> (Environment, model Symbolic, Counter, model Concrete)
-> m (Reason,
      (Environment, model Symbolic, Counter, model Concrete))
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (StateMachine model cmd m resp
-> TChan (Pid, HistoryEvent cmd resp)
-> Pid
-> Check
-> Commands cmd resp
-> StateT
     (Environment, model Symbolic, Counter, model Concrete) m Reason
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
       (model :: (* -> *) -> *).
(Show (cmd Concrete), Show (resp Concrete), Traversable cmd,
 Foldable resp, MonadCatch m, MonadIO m) =>
StateMachine model cmd m resp
-> TChan (Pid, HistoryEvent cmd resp)
-> Pid
-> Check
-> Commands cmd resp
-> StateT
     (Environment, model Symbolic, Counter, model Concrete) m Reason
executeCommands StateMachine model cmd m resp
sm TChan (Pid, HistoryEvent cmd resp)
hchan (Int -> Pid
Pid Int
2) Check
CheckPrecondition Commands cmd resp
cmds2)
                                              (Environment
env, model Symbolic
forall (r :: * -> *). model r
initModel, Counter
newCounter, model Concrete
forall (r :: * -> *). model r
initModel)
      (Reason, Reason, Environment)
-> [Pair (Commands cmd resp)] -> m (Reason, Reason, Environment)
go ( String -> Reason
ExceptionThrown String
e
         , Reason
reason2
         , Environment
env2
         ) [Pair (Commands cmd resp)]
pairs
    go out :: (Reason, Reason, Environment)
out@(ExceptionThrown String
_,     ExceptionThrown String
_,     Environment
_env) (Pair (Commands cmd resp)
_ : [Pair (Commands cmd resp)]
_) = (Reason, Reason, Environment) -> m (Reason, Reason, Environment)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Reason, Reason, Environment)
out
    go out :: (Reason, Reason, Environment)
out@(PreconditionFailed {}, ExceptionThrown String
_,     Environment
_env) (Pair (Commands cmd resp)
_ : [Pair (Commands cmd resp)]
_) = (Reason, Reason, Environment) -> m (Reason, Reason, Environment)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Reason, Reason, Environment)
out
    go out :: (Reason, Reason, Environment)
out@(ExceptionThrown String
_,     PreconditionFailed {}, Environment
_env) (Pair (Commands cmd resp)
_ : [Pair (Commands cmd resp)]
_) = (Reason, Reason, Environment) -> m (Reason, Reason, Environment)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Reason, Reason, Environment)
out
    go (Reason
res1, Reason
res2, Environment
_env) (Pair Commands cmd resp
_cmds1 Commands cmd resp
_cmds2 : [Pair (Commands cmd resp)]
_pairs) =
      String -> m (Reason, Reason, Environment)
forall a. HasCallStack => String -> a
error (String
"executeParallelCommands, unexpected result: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ (Reason, Reason) -> String
forall a. Show a => a -> String
show (Reason
res1, Reason
res2))

logicReason :: Reason -> Logic
logicReason :: Reason -> Logic
logicReason Reason
Ok = Logic
Top
logicReason Reason
r  = String -> Logic -> Logic
Annotate (Reason -> String
forall a. Show a => a -> String
show Reason
r) Logic
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
                         -> UIO.TChan (Pid, HistoryEvent cmd resp)
                         -> Bool
                         -> m (History cmd resp, model Concrete, Reason)
executeNParallelCommands :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
       (model :: (* -> *) -> *).
(Traversable cmd, Show (cmd Concrete), Foldable resp,
 Show (resp Concrete), MonadMask m, MonadUnliftIO m) =>
StateMachine model cmd m resp
-> NParallelCommands cmd resp
-> TChan (Pid, HistoryEvent cmd resp)
-> Bool
-> m (History cmd resp, model Concrete, Reason)
executeNParallelCommands sm :: StateMachine model cmd m resp
sm@StateMachine{ forall (r :: * -> *). model r
initModel :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> forall (r :: * -> *). model r
initModel :: forall (r :: * -> *). model r
initModel } (ParallelCommands Commands cmd resp
prefix [[Commands cmd resp]]
suffixes) TChan (Pid, HistoryEvent cmd resp)
hchan Bool
stopOnError = do
  (Reason
reason0, (Environment
env0, model Symbolic
_smodel, Counter
_counter, model Concrete
cmodel)) <- StateT
  (Environment, model Symbolic, Counter, model Concrete) m Reason
-> (Environment, model Symbolic, Counter, model Concrete)
-> m (Reason,
      (Environment, model Symbolic, Counter, model Concrete))
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT
      (StateMachine model cmd m resp
-> TChan (Pid, HistoryEvent cmd resp)
-> Pid
-> Check
-> Commands cmd resp
-> StateT
     (Environment, model Symbolic, Counter, model Concrete) m Reason
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
       (model :: (* -> *) -> *).
(Show (cmd Concrete), Show (resp Concrete), Traversable cmd,
 Foldable resp, MonadCatch m, MonadIO m) =>
StateMachine model cmd m resp
-> TChan (Pid, HistoryEvent cmd resp)
-> Pid
-> Check
-> Commands cmd resp
-> StateT
     (Environment, model Symbolic, Counter, model Concrete) m Reason
executeCommands StateMachine model cmd m resp
sm TChan (Pid, HistoryEvent cmd resp)
hchan (Int -> Pid
Pid Int
0) Check
CheckEverything Commands cmd resp
prefix)
      (Environment
emptyEnvironment, model Symbolic
forall (r :: * -> *). model r
initModel, Counter
newCounter, model Concrete
forall (r :: * -> *). model r
initModel)
  if Reason
reason0 Reason -> Reason -> Bool
forall a. Eq a => a -> a -> Bool
/= Reason
Ok
  then do
    [(Pid, HistoryEvent cmd resp)]
hist <- TChan (Pid, HistoryEvent cmd resp)
-> m [(Pid, HistoryEvent cmd resp)]
forall (m :: * -> *) a. MonadIO m => TChan a -> m [a]
getChanContents TChan (Pid, HistoryEvent cmd resp)
hchan
    (History cmd resp, model Concrete, Reason)
-> m (History cmd resp, model Concrete, Reason)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Pid, HistoryEvent cmd resp)] -> History cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
History' cmd resp -> History cmd resp
History [(Pid, HistoryEvent cmd resp)]
hist, model Concrete
cmodel, Reason
reason0)
  else do
    (Map Int Reason
errors, Environment
_) <- (Map Int Reason, Environment)
-> [[Commands cmd resp]] -> m (Map Int Reason, Environment)
go (Map Int Reason
forall k a. Map k a
Map.empty, Environment
env0) [[Commands cmd resp]]
suffixes
    [(Pid, HistoryEvent cmd resp)]
hist <- TChan (Pid, HistoryEvent cmd resp)
-> m [(Pid, HistoryEvent cmd resp)]
forall (m :: * -> *) a. MonadIO m => TChan a -> m [a]
getChanContents TChan (Pid, HistoryEvent cmd resp)
hchan
    (History cmd resp, model Concrete, Reason)
-> m (History cmd resp, model Concrete, Reason)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Pid, HistoryEvent cmd resp)] -> History cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
History' cmd resp -> History cmd resp
History [(Pid, HistoryEvent cmd resp)]
hist, model Concrete
cmodel, [Reason] -> Reason
combineReasons ([Reason] -> Reason) -> [Reason] -> Reason
forall a b. (a -> b) -> a -> b
$ Map Int Reason -> [Reason]
forall k a. Map k a -> [a]
Map.elems Map Int Reason
errors)
  where
    go :: (Map Int Reason, Environment)
-> [[Commands cmd resp]] -> m (Map Int Reason, Environment)
go (Map Int Reason, Environment)
res [] = (Map Int Reason, Environment) -> m (Map Int Reason, Environment)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Map Int Reason, Environment)
res
    go (Map Int Reason
previousErrors, Environment
env) ([Commands cmd resp]
suffix : [[Commands cmd resp]]
rest) = do
      Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([Reason] -> Bool
isInvalid ([Reason] -> Bool) -> [Reason] -> Bool
forall a b. (a -> b) -> a -> b
$ Map Int Reason -> [Reason]
forall k a. Map k a -> [a]
Map.elems Map Int Reason
previousErrors) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
        String -> m ()
forall a. HasCallStack => String -> a
error (String
"executeNParallelCommands, unexpected result: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Map Int Reason -> String
forall a. Show a => a -> String
show Map Int Reason
previousErrors)

      let noError :: Bool
noError = Map Int Reason -> Bool
forall k a. Map k a -> Bool
Map.null Map Int Reason
previousErrors
          check :: Check
check = if Bool
noError then Check
CheckNothing else Check
CheckPrecondition
      [(Maybe (Int, Reason), Environment)]
res <- [(Int, Commands cmd resp)]
-> ((Int, Commands cmd resp)
    -> m (Maybe (Int, Reason), Environment))
-> m [(Maybe (Int, Reason), Environment)]
forall (m :: * -> *) (t :: * -> *) a b.
(MonadUnliftIO m, Traversable t) =>
t a -> (a -> m b) -> m (t b)
forConcurrently ([Int] -> [Commands cmd resp] -> [(Int, Commands cmd resp)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
1..] [Commands cmd resp]
suffix) (((Int, Commands cmd resp) -> m (Maybe (Int, Reason), Environment))
 -> m [(Maybe (Int, Reason), Environment)])
-> ((Int, Commands cmd resp)
    -> m (Maybe (Int, Reason), Environment))
-> m [(Maybe (Int, Reason), Environment)]
forall a b. (a -> b) -> a -> b
$ \(Int
i, Commands cmd resp
cmds) ->
        case Int -> Map Int Reason -> Maybe Reason
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Int
i Map Int Reason
previousErrors of
          Maybe Reason
Nothing -> do
              (Reason
reason, (Environment
env', model Symbolic
_, Counter
_, model Concrete
_)) <- StateT
  (Environment, model Symbolic, Counter, model Concrete) m Reason
-> (Environment, model Symbolic, Counter, model Concrete)
-> m (Reason,
      (Environment, model Symbolic, Counter, model Concrete))
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (StateMachine model cmd m resp
-> TChan (Pid, HistoryEvent cmd resp)
-> Pid
-> Check
-> Commands cmd resp
-> StateT
     (Environment, model Symbolic, Counter, model Concrete) m Reason
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
       (model :: (* -> *) -> *).
(Show (cmd Concrete), Show (resp Concrete), Traversable cmd,
 Foldable resp, MonadCatch m, MonadIO m) =>
StateMachine model cmd m resp
-> TChan (Pid, HistoryEvent cmd resp)
-> Pid
-> Check
-> Commands cmd resp
-> StateT
     (Environment, model Symbolic, Counter, model Concrete) m Reason
executeCommands StateMachine model cmd m resp
sm TChan (Pid, HistoryEvent cmd resp)
hchan (Int -> Pid
Pid Int
i) Check
check Commands cmd resp
cmds) (Environment
env, model Symbolic
forall (r :: * -> *). model r
initModel, Counter
newCounter, model Concrete
forall (r :: * -> *). model r
initModel)
              (Maybe (Int, Reason), Environment)
-> m (Maybe (Int, Reason), Environment)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (if Reason -> Bool
isOK Reason
reason then Maybe (Int, Reason)
forall a. Maybe a
Nothing else (Int, Reason) -> Maybe (Int, Reason)
forall a. a -> Maybe a
Just (Int
i, Reason
reason), Environment
env')
          Just Reason
_  -> (Maybe (Int, Reason), Environment)
-> m (Maybe (Int, Reason), Environment)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Int, Reason)
forall a. Maybe a
Nothing, Environment
env)
      let newErrors :: Map Int Reason
newErrors = [(Int, Reason)] -> Map Int Reason
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Int, Reason)] -> Map Int Reason)
-> [(Int, Reason)] -> Map Int Reason
forall a b. (a -> b) -> a -> b
$ ((Maybe (Int, Reason), Environment) -> Maybe (Int, Reason))
-> [(Maybe (Int, Reason), Environment)] -> [(Int, Reason)]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (Maybe (Int, Reason), Environment) -> Maybe (Int, Reason)
forall a b. (a, b) -> a
fst [(Maybe (Int, Reason), Environment)]
res
          errors :: Map Int Reason
errors = Map Int Reason -> Map Int Reason -> Map Int Reason
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map Int Reason
previousErrors Map Int Reason
newErrors
          newEnv :: Environment
newEnv = [Environment] -> Environment
forall a. Monoid a => [a] -> a
mconcat ([Environment] -> Environment) -> [Environment] -> Environment
forall a b. (a -> b) -> a -> b
$ (Maybe (Int, Reason), Environment) -> Environment
forall a b. (a, b) -> b
snd ((Maybe (Int, Reason), Environment) -> Environment)
-> [(Maybe (Int, Reason), Environment)] -> [Environment]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Maybe (Int, Reason), Environment)]
res
      case (Bool
stopOnError, Map Int Reason -> Bool
forall k a. Map k a -> Bool
Map.null Map Int Reason
errors) of
        (Bool
True, Bool
False) -> (Map Int Reason, Environment) -> m (Map Int Reason, Environment)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Map Int Reason
errors, Environment
newEnv)
        (Bool, Bool)
_             -> (Map Int Reason, Environment)
-> [[Commands cmd resp]] -> m (Map Int Reason, Environment)
go (Map Int Reason
errors, Environment
newEnv) [[Commands cmd resp]]
rest

combineReasons :: [Reason] -> Reason
combineReasons :: [Reason] -> Reason
combineReasons [Reason]
ls = Reason -> Maybe Reason -> Reason
forall a. a -> Maybe a -> a
fromMaybe Reason
Ok ((Reason -> Bool) -> [Reason] -> Maybe Reason
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find (Reason -> Reason -> Bool
forall a. Eq a => a -> a -> Bool
/= Reason
Ok) [Reason]
ls)

isInvalid :: [Reason] -> Bool
isInvalid :: [Reason] -> Bool
isInvalid [Reason]
ls = (Reason -> Bool) -> [Reason] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Reason -> Bool
isPreconditionFailed [Reason]
ls Bool -> Bool -> Bool
&&
               (Reason -> Bool) -> [Reason] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Reason -> Bool
notException [Reason]
ls
    where
      notException :: Reason -> Bool
notException (ExceptionThrown String
_) = Bool
False
      notException Reason
_                   = Bool
True

isPreconditionFailed :: Reason -> Bool
isPreconditionFailed :: Reason -> Bool
isPreconditionFailed PreconditionFailed {} = Bool
True
isPreconditionFailed Reason
_                     = Bool
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 :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
(Show (cmd Concrete), Show (resp Concrete)) =>
StateMachine model cmd m resp -> History cmd resp -> Logic
linearise StateMachine { forall (r :: * -> *).
(Show1 r, Ord1 r) =>
model r -> cmd r -> resp r -> model r
transition :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> forall (r :: * -> *).
   (Show1 r, Ord1 r) =>
   model r -> cmd r -> resp r -> model r
transition :: forall (r :: * -> *).
(Show1 r, Ord1 r) =>
model r -> cmd r -> resp r -> model r
transition,  model Concrete -> cmd Concrete -> resp Concrete -> Logic
postcondition :: model Concrete -> cmd Concrete -> resp Concrete -> Logic
postcondition :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp
-> model Concrete -> cmd Concrete -> resp Concrete -> Logic
postcondition, forall (r :: * -> *). model r
initModel :: forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> forall (r :: * -> *). model r
initModel :: forall (r :: * -> *). model r
initModel } = [(Pid, HistoryEvent cmd resp)] -> Logic
go ([(Pid, HistoryEvent cmd resp)] -> Logic)
-> (History cmd resp -> [(Pid, HistoryEvent cmd resp)])
-> History cmd resp
-> Logic
forall b c a. (b -> c) -> (a -> b) -> a -> c
. History cmd resp -> [(Pid, HistoryEvent cmd resp)]
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
History cmd resp -> History' cmd resp
unHistory
  where
    go :: [(Pid, HistoryEvent cmd resp)] -> Logic
    go :: [(Pid, HistoryEvent cmd resp)] -> Logic
go [] = Logic
Top
    go [(Pid, HistoryEvent cmd resp)]
es = [Tree (Operation cmd resp)]
-> (Tree (Operation cmd resp) -> Logic) -> Logic
forall a. Show a => [a] -> (a -> Logic) -> Logic
exists ([(Pid, HistoryEvent cmd resp)] -> [Tree (Operation cmd resp)]
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
History' cmd resp -> Forest (Operation cmd resp)
interleavings [(Pid, HistoryEvent cmd resp)]
es) (model Concrete -> Tree (Operation cmd resp) -> Logic
step model Concrete
forall (r :: * -> *). model r
initModel)

    step :: model Concrete -> Tree (Operation cmd resp) -> Logic
    step :: model Concrete -> Tree (Operation cmd resp) -> Logic
step model Concrete
_model (Node (Crash cmd Concrete
_cmd String
_err Pid
_pid) [Tree (Operation cmd resp)]
_roses) =
      String -> Logic
forall a. HasCallStack => String -> a
error String
"Not implemented yet, see issue #162 for more details."
    step model Concrete
model (Node (Operation cmd Concrete
cmd resp Concrete
resp Pid
_) [Tree (Operation cmd resp)]
roses)   =
      model Concrete -> cmd Concrete -> resp Concrete -> Logic
postcondition model Concrete
model cmd Concrete
cmd resp Concrete
resp Logic -> Logic -> Logic
.&&
        [Tree (Operation cmd resp)]
-> (Tree (Operation cmd resp) -> Logic) -> Logic
forall a. Show a => [a] -> (a -> Logic) -> Logic
exists' [Tree (Operation cmd resp)]
roses (model Concrete -> Tree (Operation cmd resp) -> Logic
step (model Concrete -> cmd Concrete -> resp Concrete -> model Concrete
forall (r :: * -> *).
(Show1 r, Ord1 r) =>
model r -> cmd r -> resp r -> model r
transition model Concrete
model cmd Concrete
cmd resp Concrete
resp))

exists' :: Show a => [a] -> (a -> Logic) -> Logic
exists' :: forall a. Show a => [a] -> (a -> Logic) -> Logic
exists' [] a -> Logic
_ = Logic
Top
exists' [a]
xs a -> Logic
p = [a] -> (a -> Logic) -> Logic
forall a. Show a => [a] -> (a -> Logic) -> Logic
exists [a]
xs a -> Logic
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, a, Logic)] -- ^ Output of 'runParallelCommands'.
                              -> PropertyM m ()
prettyParallelCommandsWithOpts :: forall (m :: * -> *) (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *)
       a.
(MonadIO m, Foldable cmd, Show (cmd Concrete),
 Show (resp Concrete)) =>
ParallelCommands cmd resp
-> Maybe GraphOptions
-> [(History cmd resp, a, Logic)]
-> PropertyM m ()
prettyParallelCommandsWithOpts ParallelCommands cmd resp
cmds Maybe GraphOptions
mGraphOptions [(History cmd resp, a, Logic)]
histories = do
  ((History cmd resp, a, Logic) -> PropertyM m ())
-> [(History cmd resp, a, Logic)] -> PropertyM m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\(History cmd resp
h, a
_, Logic
l) -> History cmd resp -> Value -> IO ()
printCounterexample History cmd resp
h (Logic -> Value
logic Logic
l) IO () -> Property -> PropertyM m ()
forall (m :: * -> *).
Monad m =>
IO () -> Property -> PropertyM m ()
`whenFailM` Bool -> Property
forall prop. Testable prop => prop -> Property
property (Logic -> Bool
boolean Logic
l)) [(History cmd resp, a, Logic)]
histories
    where
      printCounterexample :: History cmd resp -> Value -> IO ()
printCounterexample History cmd resp
hist' (VFalse Counterexample
ce) = do
        Doc -> IO ()
PP.putDoc (Doc -> IO ()) -> Doc -> IO ()
forall a b. (a -> b) -> a -> b
$
          [Doc] -> Doc
forall a. Monoid a => [a] -> a
mconcat
           [ Doc
PP.line
           , String -> Doc
PP.string (Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$ ParallelCommands cmd resp -> History cmd resp -> Doc
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
(Foldable cmd, Show (cmd Concrete), Show (resp Concrete)) =>
ParallelCommands cmd resp -> History cmd resp -> Doc
toBoxDrawings ParallelCommands cmd resp
cmds History cmd resp
hist')
           , String -> Doc
PP.string (Counterexample -> String
forall a. Show a => a -> String
show (Counterexample -> String) -> Counterexample -> String
forall a b. (a -> b) -> a -> b
$ Counterexample -> Counterexample
simplify Counterexample
ce)
           , Doc
PP.line
           , Doc
PP.line
           , String -> Doc
PP.string (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$
             if [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [ Logic -> Bool
boolean Logic
l | (History cmd resp
_, a
_, Logic
l) <- [(History cmd resp, a, Logic)]
histories]
             then String
"However, some repetitions of this sequence of commands passed. Maybe there is a race condition?"
             else String
"And all repetitions of this sequence of commands failed. Maybe there is a logic bug? Try with more repetitions to be sure that it happens consistently"
           , Doc
PP.line
           ]
        case Maybe GraphOptions
mGraphOptions of
          Maybe GraphOptions
Nothing       -> () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
          Just GraphOptions
gOptions -> ParallelCommands cmd resp
-> GraphOptions -> History cmd resp -> IO ()
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *)
       (t :: * -> *).
(Foldable t, Foldable cmd, Show (cmd Concrete),
 Show (resp Concrete)) =>
ParallelCommandsF t cmd resp
-> GraphOptions -> History cmd resp -> IO ()
createAndPrintDot ParallelCommands cmd resp
cmds GraphOptions
gOptions History cmd resp
hist'
      printCounterexample History cmd resp
_hist Value
_
        = String -> IO ()
forall a. HasCallStack => String -> a
error String
"prettyParallelCommands: impossible, because `boolean l` was False."

simplify :: Counterexample -> Counterexample
simplify :: Counterexample -> Counterexample
simplify (Fst ce :: Counterexample
ce@(AnnotateC String
_ Counterexample
BotC)) = Counterexample
ce
simplify (Snd Counterexample
ce)                    = Counterexample -> Counterexample
simplify Counterexample
ce
simplify (ExistsC [] [])             = Counterexample
BotC
simplify (ExistsC [a]
_ [Fst Counterexample
ce])        = Counterexample
ce
simplify (ExistsC [a]
x (Fst Counterexample
ce : [Counterexample]
ces))  = Counterexample
ce Counterexample -> Counterexample -> Counterexample
`EitherC` Counterexample -> Counterexample
simplify ([a] -> [Counterexample] -> Counterexample
forall a. Show a => [a] -> [Counterexample] -> Counterexample
ExistsC [a]
x [Counterexample]
ces)
simplify (ExistsC [a]
_ (Snd Counterexample
ce : [Counterexample]
_))    = Counterexample -> Counterexample
simplify Counterexample
ce
simplify Counterexample
_                           = String -> Counterexample
forall a. HasCallStack => String -> a
error String
"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, a, Logic)] -- ^ Output of 'runNParallelCommands'.
                       -> PropertyM m ()
prettyParallelCommands :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
       a.
(Show (cmd Concrete), Show (resp Concrete), MonadIO m,
 Foldable cmd) =>
ParallelCommands cmd resp
-> [(History cmd resp, a, Logic)] -> PropertyM m ()
prettyParallelCommands ParallelCommands cmd resp
cmds = ParallelCommands cmd resp
-> Maybe GraphOptions
-> [(History cmd resp, a, Logic)]
-> PropertyM m ()
forall (m :: * -> *) (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *)
       a.
(MonadIO m, Foldable cmd, Show (cmd Concrete),
 Show (resp Concrete)) =>
ParallelCommands cmd resp
-> Maybe GraphOptions
-> [(History cmd resp, a, Logic)]
-> PropertyM m ()
prettyParallelCommandsWithOpts ParallelCommands cmd resp
cmds Maybe GraphOptions
forall a. Maybe a
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, a, Logic)] -- ^ Output of 'runNParallelCommands'.
                                -> PropertyM m ()
prettyNParallelCommandsWithOpts :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
       a.
(Show (cmd Concrete), Show (resp Concrete), MonadIO m,
 Foldable cmd) =>
NParallelCommands cmd resp
-> Maybe GraphOptions
-> [(History cmd resp, a, Logic)]
-> PropertyM m ()
prettyNParallelCommandsWithOpts NParallelCommands cmd resp
cmds Maybe GraphOptions
mGraphOptions [(History cmd resp, a, Logic)]
histories =
   ((History cmd resp, a, Logic) -> PropertyM m ())
-> [(History cmd resp, a, Logic)] -> PropertyM m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\(History cmd resp
h, a
_, Logic
l) -> History cmd resp -> Value -> IO ()
printCounterexample History cmd resp
h (Logic -> Value
logic Logic
l) IO () -> Property -> PropertyM m ()
forall (m :: * -> *).
Monad m =>
IO () -> Property -> PropertyM m ()
`whenFailM` Bool -> Property
forall prop. Testable prop => prop -> Property
property (Logic -> Bool
boolean Logic
l)) [(History cmd resp, a, Logic)]
histories
    where
      printCounterexample :: History cmd resp -> Value -> IO ()
printCounterexample History cmd resp
hist' (VFalse Counterexample
ce) = do
        Doc -> IO ()
PP.putDoc (Doc -> IO ()) -> Doc -> IO ()
forall a b. (a -> b) -> a -> b
$
          [Doc] -> Doc
forall a. Monoid a => [a] -> a
mconcat
           [ Doc
PP.line
           , String -> Doc
PP.string (Counterexample -> String
forall a. Show a => a -> String
show (Counterexample -> String) -> Counterexample -> String
forall a b. (a -> b) -> a -> b
$ Counterexample -> Counterexample
simplify Counterexample
ce)
           , Doc
PP.line
           , Doc
PP.line
           , String -> Doc
PP.string (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$
             if [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or [ Logic -> Bool
boolean Logic
l | (History cmd resp
_, a
_, Logic
l) <- [(History cmd resp, a, Logic)]
histories]
             then String
"However, some repetitions of this sequence of commands passed. Maybe there is a race condition?"
             else String
"And all repetitions of this sequence of commands failed. Maybe there is a logic bug? Try with more repetitions to be sure that it happens consistently"
           , Doc
PP.line
           ]
        case Maybe GraphOptions
mGraphOptions of
          Maybe GraphOptions
Nothing       -> () -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
          Just GraphOptions
gOptions -> NParallelCommands cmd resp
-> GraphOptions -> History cmd resp -> IO ()
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *)
       (t :: * -> *).
(Foldable t, Foldable cmd, Show (cmd Concrete),
 Show (resp Concrete)) =>
ParallelCommandsF t cmd resp
-> GraphOptions -> History cmd resp -> IO ()
createAndPrintDot NParallelCommands cmd resp
cmds GraphOptions
gOptions History cmd resp
hist'
      printCounterexample History cmd resp
_hist Value
_
        = String -> IO ()
forall a. HasCallStack => String -> a
error String
"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, a, Logic)] -- ^ Output of 'runNParallelCommands'.
                        -> PropertyM m ()
prettyNParallelCommands :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
       a.
(Show (cmd Concrete), Show (resp Concrete), MonadIO m,
 Foldable cmd) =>
NParallelCommands cmd resp
-> [(History cmd resp, a, Logic)] -> PropertyM m ()
prettyNParallelCommands NParallelCommands cmd resp
cmds = NParallelCommands cmd resp
-> Maybe GraphOptions
-> [(History cmd resp, a, Logic)]
-> PropertyM m ()
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
       a.
(Show (cmd Concrete), Show (resp Concrete), MonadIO m,
 Foldable cmd) =>
NParallelCommands cmd resp
-> Maybe GraphOptions
-> [(History cmd resp, a, Logic)]
-> PropertyM m ()
prettyNParallelCommandsWithOpts NParallelCommands cmd resp
cmds Maybe GraphOptions
forall a. Maybe a
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 :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
(Foldable cmd, Show (cmd Concrete), Show (resp Concrete)) =>
ParallelCommands cmd resp -> History cmd resp -> Doc
toBoxDrawings (ParallelCommands Commands cmd resp
prefix [Pair (Commands cmd resp)]
suffixes) = Set Var -> History cmd resp -> Doc
toBoxDrawings'' Set Var
allVars
  where
    allVars :: Set Var
allVars = Commands cmd resp -> Set Var
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
Foldable cmd =>
Commands cmd resp -> Set Var
getAllUsedVars Commands cmd resp
prefix Set Var -> Set Var -> Set Var
forall a. Ord a => Set a -> Set a -> Set a
`S.union`
                (Pair (Commands cmd resp) -> Set Var)
-> [Pair (Commands cmd resp)] -> Set Var
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap ((Commands cmd resp -> Set Var)
-> Pair (Commands cmd resp) -> Set Var
forall m a. Monoid m => (a -> m) -> Pair a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Commands cmd resp -> Set Var
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
Foldable cmd =>
Commands cmd resp -> Set Var
getAllUsedVars) [Pair (Commands cmd resp)]
suffixes

    toBoxDrawings'' :: Set Var -> History cmd resp -> Doc
    toBoxDrawings'' :: Set Var -> History cmd resp -> Doc
toBoxDrawings'' Set Var
knownVars (History History' cmd resp
h) = [Doc] -> Doc
forall a. Monoid a => [a] -> a
mconcat
        ([ [(EventType, Pid)] -> Fork [String] -> Doc
exec [(EventType, Pid)]
evT (((Pid, HistoryEvent cmd resp) -> String)
-> History' cmd resp -> [String]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (HistoryEvent cmd resp -> String
out  (HistoryEvent cmd resp -> String)
-> ((Pid, HistoryEvent cmd resp) -> HistoryEvent cmd resp)
-> (Pid, HistoryEvent cmd resp)
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Pid, HistoryEvent cmd resp) -> HistoryEvent cmd resp
forall a b. (a, b) -> b
snd) (History' cmd resp -> [String])
-> Fork (History' cmd resp) -> Fork [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> History' cmd resp
-> History' cmd resp
-> History' cmd resp
-> Fork (History' cmd resp)
forall a. a -> a -> a -> Fork a
Fork History' cmd resp
l History' cmd resp
p History' cmd resp
r)
         , Doc
PP.line
         , Doc
PP.line
         ]
         [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ ((Int, String) -> Doc) -> [(Int, String)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Int, String) -> Doc
ppException [(Int, String)]
exceptions
        )
      where
        (Int
_, [(Int, String)]
exceptions, History' cmd resp
h'') = ((Int, [(Int, String)], History' cmd resp)
 -> (Pid, HistoryEvent cmd resp)
 -> (Int, [(Int, String)], History' cmd resp))
-> (Int, [(Int, String)], History' cmd resp)
-> History' cmd resp
-> (Int, [(Int, String)], History' cmd resp)
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl'
               (\(Int
i, [(Int, String)]
excs, History' cmd resp
evs) (Pid
pid, HistoryEvent cmd resp
ev) ->
                  case HistoryEvent cmd resp
ev of
                    Exception String
err -> (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1, [(Int, String)]
excs [(Int, String)] -> [(Int, String)] -> [(Int, String)]
forall a. [a] -> [a] -> [a]
++ [(Int
i, String
err)], History' cmd resp
evs History' cmd resp -> History' cmd resp -> History' cmd resp
forall a. [a] -> [a] -> [a]
++ [(Pid
pid, String -> HistoryEvent cmd resp
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
String -> HistoryEvent cmd resp
Exception (String -> HistoryEvent cmd resp)
-> String -> HistoryEvent cmd resp
forall a b. (a -> b) -> a -> b
$ String
"Exception " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show Int
i)])
                    HistoryEvent cmd resp
_ -> (Int
i, [(Int, String)]
excs, History' cmd resp
evs History' cmd resp -> History' cmd resp -> History' cmd resp
forall a. [a] -> [a] -> [a]
++ [(Pid
pid, HistoryEvent cmd resp
ev)])
               )
               (Int
0 :: Int, [], [])
               History' cmd resp
h
        (History' cmd resp
p, History' cmd resp
h') = ((Pid, HistoryEvent cmd resp) -> Bool)
-> History' cmd resp -> (History' cmd resp, History' cmd resp)
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (\(Pid, HistoryEvent cmd resp)
e -> (Pid, HistoryEvent cmd resp) -> Pid
forall a b. (a, b) -> a
fst (Pid, HistoryEvent cmd resp)
e Pid -> Pid -> Bool
forall a. Eq a => a -> a -> Bool
== Int -> Pid
Pid Int
0) History' cmd resp
h''
        (History' cmd resp
l, History' cmd resp
r)  = ((Pid, HistoryEvent cmd resp) -> Bool)
-> History' cmd resp -> (History' cmd resp, History' cmd resp)
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (\(Pid, HistoryEvent cmd resp)
e -> (Pid, HistoryEvent cmd resp) -> Pid
forall a b. (a, b) -> a
fst (Pid, HistoryEvent cmd resp)
e Pid -> Pid -> Bool
forall a. Eq a => a -> a -> Bool
== Int -> Pid
Pid Int
1) History' cmd resp
h'

        out :: HistoryEvent cmd resp -> String
        out :: HistoryEvent cmd resp -> String
out (Invocation cmd Concrete
cmd Set Var
vars)
          | Set Var
vars Set Var -> Set Var -> Bool
forall a. Ord a => Set a -> Set a -> Bool
`S.isSubsetOf` Set Var
knownVars = [Var] -> String
forall a. Show a => a -> String
show (Set Var -> [Var]
forall a. Set a -> [a]
S.toList Set Var
vars) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" ← " String -> String -> String
forall a. [a] -> [a] -> [a]
++ cmd Concrete -> String
forall a. Show a => a -> String
show cmd Concrete
cmd
          | Bool
otherwise                     = cmd Concrete -> String
forall a. Show a => a -> String
show cmd Concrete
cmd
        out (Response resp Concrete
resp) = resp Concrete -> String
forall a. Show a => a -> String
show resp Concrete
resp
        out (Exception String
err) = String
err

        toEventType :: History' cmd resp -> [(EventType, Pid)]
        toEventType :: History' cmd resp -> [(EventType, Pid)]
toEventType = ((Pid, HistoryEvent cmd resp) -> (EventType, Pid))
-> History' cmd resp -> [(EventType, Pid)]
forall a b. (a -> b) -> [a] -> [b]
map (Pid, HistoryEvent cmd resp) -> (EventType, Pid)
forall {b} {cmd :: (* -> *) -> *} {resp :: (* -> *) -> *}.
(b, HistoryEvent cmd resp) -> (EventType, b)
go
          where
            go :: (b, HistoryEvent cmd resp) -> (EventType, b)
go (b, HistoryEvent cmd resp)
e = case (b, HistoryEvent cmd resp)
e of
              (b
pid, Invocation cmd Concrete
_ Set Var
_) -> (EventType
Open,  b
pid)
              (b
pid, Response   resp Concrete
_)   -> (EventType
Close, b
pid)
              (b
pid, Exception  String
_)   -> (EventType
Close, b
pid)

        evT :: [(EventType, Pid)]
        evT :: [(EventType, Pid)]
evT = History' cmd resp -> [(EventType, Pid)]
toEventType (((Pid, HistoryEvent cmd resp) -> Bool)
-> History' cmd resp -> History' cmd resp
forall a. (a -> Bool) -> [a] -> [a]
filter (\(Pid, HistoryEvent cmd resp)
e -> (Pid, HistoryEvent cmd resp) -> Pid
forall a b. (a, b) -> a
fst (Pid, HistoryEvent cmd resp)
e Pid -> [Pid] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`Prelude.elem` (Int -> Pid) -> [Int] -> [Pid]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Pid
Pid [Int
1, Int
2]) History' cmd resp
h)

        ppException :: (Int, String) -> Doc
        ppException :: (Int, String) -> Doc
ppException (Int
idx, String
err) = [Doc] -> Doc
forall a. Monoid a => [a] -> a
mconcat
         [ String -> Doc
PP.string (String -> Doc) -> String -> Doc
forall a b. (a -> b) -> a -> b
$ String
"Exception " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Int -> String
forall a. Show a => a -> String
show Int
idx String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
":"
         , Doc
PP.line
         , Int -> Doc -> Doc
PP.indent Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
PP.string String
err
         , Doc
PP.line
         , Doc
PP.line
         ]

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 :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *)
       (t :: * -> *).
(Foldable t, Foldable cmd, Show (cmd Concrete),
 Show (resp Concrete)) =>
ParallelCommandsF t cmd resp
-> GraphOptions -> History cmd resp -> IO ()
createAndPrintDot (ParallelCommands Commands cmd resp
prefix [t (Commands cmd resp)]
suffixes) GraphOptions
gOptions = Set Var -> History cmd resp -> IO ()
toDotGraph Set Var
allVars
  where
    allVars :: Set Var
allVars = Commands cmd resp -> Set Var
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
Foldable cmd =>
Commands cmd resp -> Set Var
getAllUsedVars Commands cmd resp
prefix Set Var -> Set Var -> Set Var
forall a. Ord a => Set a -> Set a -> Set a
`S.union`
                (t (Commands cmd resp) -> Set Var)
-> [t (Commands cmd resp)] -> Set Var
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap ((Commands cmd resp -> Set Var) -> t (Commands cmd resp) -> Set Var
forall m a. Monoid m => (a -> m) -> t a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Commands cmd resp -> Set Var
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
Foldable cmd =>
Commands cmd resp -> Set Var
getAllUsedVars) [t (Commands cmd resp)]
suffixes

    toDotGraph :: Set Var -> History cmd resp -> IO ()
    toDotGraph :: Set Var -> History cmd resp -> IO ()
toDotGraph Set Var
knownVars (History History' cmd resp
h) = GraphOptions -> Rose [String] -> IO ()
printDotGraph GraphOptions
gOptions (Rose [String] -> IO ()) -> Rose [String] -> IO ()
forall a b. (a -> b) -> a -> b
$ (HistoryEvent cmd resp -> String)
-> [HistoryEvent cmd resp] -> [String]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap HistoryEvent cmd resp -> String
out ([HistoryEvent cmd resp] -> [String])
-> Rose [HistoryEvent cmd resp] -> Rose [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [HistoryEvent cmd resp]
-> Map Pid [HistoryEvent cmd resp] -> Rose [HistoryEvent cmd resp]
forall a. a -> Map Pid a -> Rose a
Rose ((Pid, HistoryEvent cmd resp) -> HistoryEvent cmd resp
forall a b. (a, b) -> b
snd ((Pid, HistoryEvent cmd resp) -> HistoryEvent cmd resp)
-> History' cmd resp -> [HistoryEvent cmd resp]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> History' cmd resp
prefixMessages) Map Pid [HistoryEvent cmd resp]
groupByPid
      where
        (History' cmd resp
prefixMessages, History' cmd resp
h') = ((Pid, HistoryEvent cmd resp) -> Bool)
-> History' cmd resp -> (History' cmd resp, History' cmd resp)
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (\(Pid, HistoryEvent cmd resp)
e -> (Pid, HistoryEvent cmd resp) -> Pid
forall a b. (a, b) -> a
fst (Pid, HistoryEvent cmd resp)
e Pid -> Pid -> Bool
forall a. Eq a => a -> a -> Bool
== Int -> Pid
Pid Int
0) History' cmd resp
h
        alterF :: a -> Maybe [a] -> Maybe [a]
alterF a
a Maybe [a]
Nothing   = [a] -> Maybe [a]
forall a. a -> Maybe a
Just [a
a]
        alterF a
a (Just [a]
ls) = [a] -> Maybe [a]
forall a. a -> Maybe a
Just ([a] -> Maybe [a]) -> [a] -> Maybe [a]
forall a b. (a -> b) -> a -> b
$ a
a a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
ls
        groupByPid :: Map Pid [HistoryEvent cmd resp]
groupByPid = ((Pid, HistoryEvent cmd resp)
 -> Map Pid [HistoryEvent cmd resp]
 -> Map Pid [HistoryEvent cmd resp])
-> Map Pid [HistoryEvent cmd resp]
-> History' cmd resp
-> Map Pid [HistoryEvent cmd resp]
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\(Pid
p,HistoryEvent cmd resp
e) Map Pid [HistoryEvent cmd resp]
m -> (Maybe [HistoryEvent cmd resp] -> Maybe [HistoryEvent cmd resp])
-> Pid
-> Map Pid [HistoryEvent cmd resp]
-> Map Pid [HistoryEvent cmd resp]
forall k a.
Ord k =>
(Maybe a -> Maybe a) -> k -> Map k a -> Map k a
Map.alter (HistoryEvent cmd resp
-> Maybe [HistoryEvent cmd resp] -> Maybe [HistoryEvent cmd resp]
forall {a}. a -> Maybe [a] -> Maybe [a]
alterF HistoryEvent cmd resp
e) Pid
p Map Pid [HistoryEvent cmd resp]
m) Map Pid [HistoryEvent cmd resp]
forall k a. Map k a
Map.empty History' cmd resp
h'

        out :: HistoryEvent cmd resp -> String
        out :: HistoryEvent cmd resp -> String
out (Invocation cmd Concrete
cmd Set Var
vars)
          | Set Var
vars Set Var -> Set Var -> Bool
forall a. Ord a => Set a -> Set a -> Bool
`S.isSubsetOf` Set Var
knownVars = [Var] -> String
forall a. Show a => a -> String
show (Set Var -> [Var]
forall a. Set a -> [a]
S.toList Set Var
vars) String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" ← " String -> String -> String
forall a. [a] -> [a] -> [a]
++ cmd Concrete -> String
forall a. Show a => a -> String
show cmd Concrete
cmd
          | Bool
otherwise                     = cmd Concrete -> String
forall a. Show a => a -> String
show cmd Concrete
cmd
        out (Response resp Concrete
resp) = String
" → " String -> String -> String
forall a. [a] -> [a] -> [a]
++ resp Concrete -> String
forall a. Show a => a -> String
show resp Concrete
resp
        out (Exception String
err) = String
" → " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
err


getAllUsedVars :: Rank2.Foldable cmd => Commands cmd resp -> Set Var
getAllUsedVars :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
Foldable cmd =>
Commands cmd resp -> Set Var
getAllUsedVars = [Var] -> Set Var
forall a. Ord a => [a] -> Set a
S.fromList ([Var] -> Set Var)
-> (Commands cmd resp -> [Var]) -> Commands cmd resp -> Set Var
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Command cmd resp -> [Var]) -> [Command cmd resp] -> [Var]
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (\(Command cmd Symbolic
cmd resp Symbolic
_ [Var]
_) -> cmd Symbolic -> [Var]
forall (f :: (* -> *) -> *). Foldable f => f Symbolic -> [Var]
getUsedVars cmd Symbolic
cmd) ([Command cmd resp] -> [Var])
-> (Commands cmd resp -> [Command cmd resp])
-> Commands cmd resp
-> [Var]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Commands cmd resp -> [Command cmd resp]
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
Commands cmd resp -> [Command cmd resp]
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 :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *)
       (t :: * -> *).
(Foldable t, CommandNames cmd) =>
ParallelCommandsF t cmd resp -> Property -> Property
checkCommandNamesParallel ParallelCommandsF t cmd resp
cmds = Commands cmd resp -> Property -> Property
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
CommandNames cmd =>
Commands cmd resp -> Property -> Property
checkCommandNames (Commands cmd resp -> Property -> Property)
-> Commands cmd resp -> Property -> Property
forall a b. (a -> b) -> a -> b
$ ParallelCommandsF t cmd resp -> Commands cmd resp
forall (t :: * -> *) (cmd :: (* -> *) -> *)
       (resp :: (* -> *) -> *).
Foldable t =>
ParallelCommandsF t cmd resp -> Commands cmd resp
toSequential ParallelCommandsF t cmd resp
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 :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *)
       (t :: * -> *).
(Foldable t, CommandNames cmd) =>
ParallelCommandsF t cmd resp -> Property -> Property
coverCommandNamesParallel ParallelCommandsF t cmd resp
cmds = Commands cmd resp -> Property -> Property
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
CommandNames cmd =>
Commands cmd resp -> Property -> Property
coverCommandNames (Commands cmd resp -> Property -> Property)
-> Commands cmd resp -> Property -> Property
forall a b. (a -> b) -> a -> b
$ ParallelCommandsF t cmd resp -> Commands cmd resp
forall (t :: * -> *) (cmd :: (* -> *) -> *)
       (resp :: (* -> *) -> *).
Foldable t =>
ParallelCommandsF t cmd resp -> Commands cmd resp
toSequential ParallelCommandsF t cmd resp
cmds

commandNamesParallel :: forall cmd resp t. Foldable t => CommandNames cmd
                     => ParallelCommandsF t cmd resp -> [(String, Int)]
commandNamesParallel :: forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *)
       (t :: * -> *).
(Foldable t, CommandNames cmd) =>
ParallelCommandsF t cmd resp -> [(String, Int)]
commandNamesParallel = Commands cmd resp -> [(String, Int)]
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
CommandNames cmd =>
Commands cmd resp -> [(String, Int)]
commandNames (Commands cmd resp -> [(String, Int)])
-> (ParallelCommandsF t cmd resp -> Commands cmd resp)
-> ParallelCommandsF t cmd resp
-> [(String, Int)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ParallelCommandsF t cmd resp -> Commands cmd resp
forall (t :: * -> *) (cmd :: (* -> *) -> *)
       (resp :: (* -> *) -> *).
Foldable t =>
ParallelCommandsF t cmd resp -> Commands cmd resp
toSequential

toSequential :: Foldable t => ParallelCommandsF t cmd resp -> Commands cmd resp
toSequential :: forall (t :: * -> *) (cmd :: (* -> *) -> *)
       (resp :: (* -> *) -> *).
Foldable t =>
ParallelCommandsF t cmd resp -> Commands cmd resp
toSequential ParallelCommandsF t cmd resp
cmds = ParallelCommandsF t cmd resp -> Commands cmd resp
forall (t :: * -> *) (cmd :: (* -> *) -> *)
       (resp :: (* -> *) -> *).
ParallelCommandsF t cmd resp -> Commands cmd resp
prefix ParallelCommandsF t cmd resp
cmds Commands cmd resp -> Commands cmd resp -> Commands cmd resp
forall a. Semigroup a => a -> a -> a
<> [Commands cmd resp] -> Commands cmd resp
forall a. Monoid a => [a] -> a
mconcat ((t (Commands cmd resp) -> [Commands cmd resp])
-> [t (Commands cmd resp)] -> [Commands cmd resp]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap t (Commands cmd resp) -> [Commands cmd resp]
forall a. t a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (ParallelCommandsF t cmd resp -> [t (Commands cmd resp)]
forall (t :: * -> *) (cmd :: (* -> *) -> *)
       (resp :: (* -> *) -> *).
ParallelCommandsF t cmd resp -> [t (Commands cmd resp)]
suffixes ParallelCommandsF t cmd resp
cmds))