{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}

-- | Tests for the resource registry
--
-- The resource registry is a component throughout the consensus layer that
-- helps us keep track of resources and makes sure that all resources that we
-- allocate are eventually also deallocated in the right order.
--
-- The tests for the registry are model based. The model records which resources
-- we expect to be alive and which we expect to have been deallocated. The only
-- resources we are modelling here are threads; the commands we then execute are
--
-- * Fork a thread from some other thread
-- * Terminate a thread
-- * Have a thread crash
-- * Collect all live threads
--
-- We then verify that the resource registry behaves like the model, cleaning
-- up resources as threads terminate or crash.
--
module Test.Consensus.ResourceRegistry (tests) where

import           Control.Monad ((>=>))
import           Control.Monad.Class.MonadTimer.SI
import           Control.Monad.Except (Except, MonadError, runExcept,
                     throwError)
import           Control.Monad.IO.Class (liftIO)
import           Data.Foldable (toList)
import           Data.Function (on)
import           Data.Functor.Classes
import           Data.Kind (Type)
import           Data.List (delete, sort)
import           Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import           Data.TreeDiff
import           Data.Typeable
import qualified Generics.SOP as SOP
import           GHC.Generics (Generic, Generic1)
import           Ouroboros.Consensus.Util.IOLike
import           Ouroboros.Consensus.Util.ResourceRegistry
import           Prelude hiding (elem)
import qualified Test.QuickCheck as QC
import           Test.QuickCheck (Gen)
import qualified Test.QuickCheck.Monadic as QC
import           Test.StateMachine
import qualified Test.StateMachine.Types as QSM
import qualified Test.StateMachine.Types.Rank2 as Rank2
import           Test.Tasty hiding (after)
import           Test.Tasty.QuickCheck (testProperty)
import           Test.Util.QSM
import           Test.Util.SOP
import           Test.Util.ToExpr ()

tests :: TestTree
tests :: TestTree
tests = TestName -> [TestTree] -> TestTree
testGroup TestName
"ResourceRegistry" [
      TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"sequential" Property
prop_sequential
    ]

{-------------------------------------------------------------------------------
  Mock implementaton
-------------------------------------------------------------------------------}

-- | Mock thread IDs record thread pedigree
--
-- > [t]           top-level thread t
-- > [t, t']       child t' of top-level thread t
-- > [t, t', t'']  child t'' of thread t', itself a child of t
--
-- NOTE: All thread IDs will be unique. If both threads 1 and 2 spawn a child,
-- they would be @[1,3]@ and @[2,4]@.
type MockThread = [Int]

-- | Threads and their subthreads
--
-- Once created, threads are never removed from this map. Instead, when they are
-- killed their 'alive' status is set to 'False'.
newtype MockThreads = MTs { MockThreads -> Map Int MockState
mockThreadsMap :: Map Int MockState }
  deriving (Int -> MockThreads -> ShowS
[MockThreads] -> ShowS
MockThreads -> TestName
(Int -> MockThreads -> ShowS)
-> (MockThreads -> TestName)
-> ([MockThreads] -> ShowS)
-> Show MockThreads
forall a.
(Int -> a -> ShowS) -> (a -> TestName) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> MockThreads -> ShowS
showsPrec :: Int -> MockThreads -> ShowS
$cshow :: MockThreads -> TestName
show :: MockThreads -> TestName
$cshowList :: [MockThreads] -> ShowS
showList :: [MockThreads] -> ShowS
Show, (forall x. MockThreads -> Rep MockThreads x)
-> (forall x. Rep MockThreads x -> MockThreads)
-> Generic MockThreads
forall x. Rep MockThreads x -> MockThreads
forall x. MockThreads -> Rep MockThreads x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. MockThreads -> Rep MockThreads x
from :: forall x. MockThreads -> Rep MockThreads x
$cto :: forall x. Rep MockThreads x -> MockThreads
to :: forall x. Rep MockThreads x -> MockThreads
Generic)

-- | State of a mock thread
data MockState = MS {
      MockState -> Bool
alive :: Bool
    , MockState -> MockThreads
kids  :: MockThreads
    }
  deriving (Int -> MockState -> ShowS
[MockState] -> ShowS
MockState -> TestName
(Int -> MockState -> ShowS)
-> (MockState -> TestName)
-> ([MockState] -> ShowS)
-> Show MockState
forall a.
(Int -> a -> ShowS) -> (a -> TestName) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> MockState -> ShowS
showsPrec :: Int -> MockState -> ShowS
$cshow :: MockState -> TestName
show :: MockState -> TestName
$cshowList :: [MockState] -> ShowS
showList :: [MockState] -> ShowS
Show, (forall x. MockState -> Rep MockState x)
-> (forall x. Rep MockState x -> MockState) -> Generic MockState
forall x. Rep MockState x -> MockState
forall x. MockState -> Rep MockState x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. MockState -> Rep MockState x
from :: forall x. MockState -> Rep MockState x
$cto :: forall x. Rep MockState x -> MockState
to :: forall x. Rep MockState x -> MockState
Generic)

-- | All known threads, and whether or not they are alive
--
-- TODO: Perhaps it would be better to have an invariant that in 'MockThreads'
-- threads must be recorded as dead if any of their parents are, rather than
-- computing that here.
mockThreads :: MockThreads -> [(MockThread, Bool)]
mockThreads :: MockThreads -> [(MockThread, Bool)]
mockThreads = MockThread -> Bool -> MockThreads -> [(MockThread, Bool)]
go [] Bool
True
  where
    go :: [Int] -> Bool -> MockThreads -> [(MockThread, Bool)]
    go :: MockThread -> Bool -> MockThreads -> [(MockThread, Bool)]
go MockThread
prefix Bool
parentAlive =
        ((Int, MockState) -> [(MockThread, Bool)])
-> [(Int, MockState)] -> [(MockThread, Bool)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Int, MockState) -> [(MockThread, Bool)]
aux ([(Int, MockState)] -> [(MockThread, Bool)])
-> (MockThreads -> [(Int, MockState)])
-> MockThreads
-> [(MockThread, Bool)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map Int MockState -> [(Int, MockState)]
forall k a. Map k a -> [(k, a)]
Map.toList (Map Int MockState -> [(Int, MockState)])
-> (MockThreads -> Map Int MockState)
-> MockThreads
-> [(Int, MockState)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MockThreads -> Map Int MockState
mockThreadsMap
      where
        aux :: (Int, MockState) -> [(MockThread, Bool)]
        aux :: (Int, MockState) -> [(MockThread, Bool)]
aux (Int
tid, MS{Bool
MockThreads
alive :: MockState -> Bool
kids :: MockState -> MockThreads
alive :: Bool
kids :: MockThreads
..}) =
            (MockThread
t, Bool
parentAlive Bool -> Bool -> Bool
&& Bool
alive) (MockThread, Bool) -> [(MockThread, Bool)] -> [(MockThread, Bool)]
forall a. a -> [a] -> [a]
: MockThread -> Bool -> MockThreads -> [(MockThread, Bool)]
go MockThread
t Bool
alive' MockThreads
kids
          where
            t :: [Int]
            t :: MockThread
t = MockThread
prefix MockThread -> MockThread -> MockThread
forall a. [a] -> [a] -> [a]
++ [Int
tid]

            alive' :: Bool
            alive' :: Bool
alive' = Bool
parentAlive Bool -> Bool -> Bool
&& Bool
alive

mockLiveThreads :: MockThreads -> [MockThread]
mockLiveThreads :: MockThreads -> [MockThread]
mockLiveThreads = ((MockThread, Bool) -> MockThread)
-> [(MockThread, Bool)] -> [MockThread]
forall a b. (a -> b) -> [a] -> [b]
map (MockThread, Bool) -> MockThread
forall a b. (a, b) -> a
fst ([(MockThread, Bool)] -> [MockThread])
-> (MockThreads -> [(MockThread, Bool)])
-> MockThreads
-> [MockThread]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((MockThread, Bool) -> Bool)
-> [(MockThread, Bool)] -> [(MockThread, Bool)]
forall a. (a -> Bool) -> [a] -> [a]
filter (MockThread, Bool) -> Bool
forall a b. (a, b) -> b
snd ([(MockThread, Bool)] -> [(MockThread, Bool)])
-> (MockThreads -> [(MockThread, Bool)])
-> MockThreads
-> [(MockThread, Bool)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MockThreads -> [(MockThread, Bool)]
mockThreads

alterThreadF :: forall m. MonadError Err m
             => MockThread
             -> (Maybe MockState -> m MockState)
             -> MockThreads -> m MockThreads
alterThreadF :: forall (m :: * -> *).
MonadError Err m =>
MockThread
-> (Maybe MockState -> m MockState) -> MockThreads -> m MockThreads
alterThreadF [] Maybe MockState -> m MockState
_ MockThreads
_ =
    TestName -> m MockThreads
forall a. HasCallStack => TestName -> a
error TestName
"alterThreadF: invalid thread"
alterThreadF [Int
t] Maybe MockState -> m MockState
f (MTs Map Int MockState
m) =
    Map Int MockState -> MockThreads
MTs (Map Int MockState -> MockThreads)
-> m (Map Int MockState) -> m MockThreads
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Maybe MockState -> m (Maybe MockState))
-> Int -> Map Int MockState -> m (Map Int MockState)
forall (f :: * -> *) k a.
(Functor f, Ord k) =>
(Maybe a -> f (Maybe a)) -> k -> Map k a -> f (Map k a)
Map.alterF ((MockState -> Maybe MockState)
-> m MockState -> m (Maybe MockState)
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap MockState -> Maybe MockState
forall a. a -> Maybe a
Just (m MockState -> m (Maybe MockState))
-> (Maybe MockState -> m MockState)
-> Maybe MockState
-> m (Maybe MockState)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe MockState -> m MockState
f) Int
t Map Int MockState
m
alterThreadF thread :: MockThread
thread@(Int
t:MockThread
ts) Maybe MockState -> m MockState
f (MTs Map Int MockState
m) =
    Map Int MockState -> MockThreads
MTs (Map Int MockState -> MockThreads)
-> m (Map Int MockState) -> m MockThreads
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Maybe MockState -> m (Maybe MockState))
-> Int -> Map Int MockState -> m (Map Int MockState)
forall (f :: * -> *) k a.
(Functor f, Ord k) =>
(Maybe a -> f (Maybe a)) -> k -> Map k a -> f (Map k a)
Map.alterF ((MockState -> Maybe MockState)
-> m MockState -> m (Maybe MockState)
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap MockState -> Maybe MockState
forall a. a -> Maybe a
Just (m MockState -> m (Maybe MockState))
-> (Maybe MockState -> m MockState)
-> Maybe MockState
-> m (Maybe MockState)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe MockState -> m MockState
f') Int
t Map Int MockState
m
  where
    f' :: Maybe MockState -> m MockState
    f' :: Maybe MockState -> m MockState
f' Maybe MockState
Nothing   = Err -> m MockState
forall a. Err -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Err -> m MockState) -> Err -> m MockState
forall a b. (a -> b) -> a -> b
$ TestName -> Err
ErrInvalidThread (MockThread -> TestName
forall a. Show a => a -> TestName
show MockThread
thread)
    f' (Just MockState
ms) = (\MockThreads
kids' -> MockState
ms { kids = kids' }) (MockThreads -> MockState) -> m MockThreads -> m MockState
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
                     MockThread
-> (Maybe MockState -> m MockState) -> MockThreads -> m MockThreads
forall (m :: * -> *).
MonadError Err m =>
MockThread
-> (Maybe MockState -> m MockState) -> MockThreads -> m MockThreads
alterThreadF MockThread
ts Maybe MockState -> m MockState
f (MockState -> MockThreads
kids MockState
ms)

-- Create thread with the given ID
mockFork :: MockThread -> MockThreads -> Except Err MockThreads
mockFork :: MockThread -> MockThreads -> Except Err MockThreads
mockFork MockThread
t = MockThread
-> (Maybe MockState -> ExceptT Err Identity MockState)
-> MockThreads
-> Except Err MockThreads
forall (m :: * -> *).
MonadError Err m =>
MockThread
-> (Maybe MockState -> m MockState) -> MockThreads -> m MockThreads
alterThreadF MockThread
t ((Maybe MockState -> ExceptT Err Identity MockState)
 -> MockThreads -> Except Err MockThreads)
-> (Maybe MockState -> ExceptT Err Identity MockState)
-> MockThreads
-> Except Err MockThreads
forall a b. (a -> b) -> a -> b
$ \case
    Just MockState
_  -> TestName -> ExceptT Err Identity MockState
forall a. HasCallStack => TestName -> a
error TestName
"fork: thread already exists (bug in runMock)"
    Maybe MockState
Nothing -> MockState -> ExceptT Err Identity MockState
forall a. a -> ExceptT Err Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return MockState
newState
  where
    newState :: MockState
    newState :: MockState
newState = MS {
          alive :: Bool
alive = Bool
True
        , kids :: MockThreads
kids  = Map Int MockState -> MockThreads
MTs Map Int MockState
forall k a. Map k a
Map.empty
        }

mockKill :: MockThread -> MockThreads -> Except Err MockThreads
mockKill :: MockThread -> MockThreads -> Except Err MockThreads
mockKill MockThread
t = MockThread
-> (Maybe MockState -> ExceptT Err Identity MockState)
-> MockThreads
-> Except Err MockThreads
forall (m :: * -> *).
MonadError Err m =>
MockThread
-> (Maybe MockState -> m MockState) -> MockThreads -> m MockThreads
alterThreadF MockThread
t ((Maybe MockState -> ExceptT Err Identity MockState)
 -> MockThreads -> Except Err MockThreads)
-> (Maybe MockState -> ExceptT Err Identity MockState)
-> MockThreads
-> Except Err MockThreads
forall a b. (a -> b) -> a -> b
$ \case
    Maybe MockState
Nothing -> Err -> ExceptT Err Identity MockState
forall a. Err -> ExceptT Err Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Err -> ExceptT Err Identity MockState)
-> Err -> ExceptT Err Identity MockState
forall a b. (a -> b) -> a -> b
$ TestName -> Err
ErrInvalidThread (MockThread -> TestName
forall a. Show a => a -> TestName
show MockThread
t)
    Just MockState
st -> MockState -> ExceptT Err Identity MockState
forall a. a -> ExceptT Err Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return MockState
st { alive = False }

data Mock = Mock {
      Mock -> Int
nextId  :: Int
    , Mock -> MockThreads
threads :: MockThreads
    , Mock -> Map MockThread (Link MockThread)
links   :: Map MockThread (Link MockThread)
    }
  deriving (Int -> Mock -> ShowS
[Mock] -> ShowS
Mock -> TestName
(Int -> Mock -> ShowS)
-> (Mock -> TestName) -> ([Mock] -> ShowS) -> Show Mock
forall a.
(Int -> a -> ShowS) -> (a -> TestName) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Mock -> ShowS
showsPrec :: Int -> Mock -> ShowS
$cshow :: Mock -> TestName
show :: Mock -> TestName
$cshowList :: [Mock] -> ShowS
showList :: [Mock] -> ShowS
Show, (forall x. Mock -> Rep Mock x)
-> (forall x. Rep Mock x -> Mock) -> Generic Mock
forall x. Rep Mock x -> Mock
forall x. Mock -> Rep Mock x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Mock -> Rep Mock x
from :: forall x. Mock -> Rep Mock x
$cto :: forall x. Rep Mock x -> Mock
to :: forall x. Rep Mock x -> Mock
Generic)

emptyMock :: Mock
emptyMock :: Mock
emptyMock = Mock {
      nextId :: Int
nextId  = Int
1
    , threads :: MockThreads
threads = Map Int MockState -> MockThreads
MTs Map Int MockState
forall k a. Map k a
Map.empty
    , links :: Map MockThread (Link MockThread)
links   = Map MockThread (Link MockThread)
forall k a. Map k a
Map.empty
    }

{-------------------------------------------------------------------------------
  Commands
-------------------------------------------------------------------------------}

-- | Should we link a new thread to its parent?
--
-- If yes, we need some information about that parent.
data Link a = LinkFromParent a | DontLink
  deriving (Int -> Link a -> ShowS
[Link a] -> ShowS
Link a -> TestName
(Int -> Link a -> ShowS)
-> (Link a -> TestName) -> ([Link a] -> ShowS) -> Show (Link a)
forall a. Show a => Int -> Link a -> ShowS
forall a. Show a => [Link a] -> ShowS
forall a. Show a => Link a -> TestName
forall a.
(Int -> a -> ShowS) -> (a -> TestName) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> Link a -> ShowS
showsPrec :: Int -> Link a -> ShowS
$cshow :: forall a. Show a => Link a -> TestName
show :: Link a -> TestName
$cshowList :: forall a. Show a => [Link a] -> ShowS
showList :: [Link a] -> ShowS
Show, (forall a b. (a -> b) -> Link a -> Link b)
-> (forall a b. a -> Link b -> Link a) -> Functor Link
forall a b. a -> Link b -> Link a
forall a b. (a -> b) -> Link a -> Link b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> Link a -> Link b
fmap :: forall a b. (a -> b) -> Link a -> Link b
$c<$ :: forall a b. a -> Link b -> Link a
<$ :: forall a b. a -> Link b -> Link a
Functor, (forall x. Link a -> Rep (Link a) x)
-> (forall x. Rep (Link a) x -> Link a) -> Generic (Link a)
forall x. Rep (Link a) x -> Link a
forall x. Link a -> Rep (Link a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Link a) x -> Link a
forall a x. Link a -> Rep (Link a) x
$cfrom :: forall a x. Link a -> Rep (Link a) x
from :: forall x. Link a -> Rep (Link a) x
$cto :: forall a x. Rep (Link a) x -> Link a
to :: forall x. Rep (Link a) x -> Link a
Generic)

data Cmd t =
    -- | Fork a new top-level thread
    --
    -- We don't allow linking here, because we don't want an exception in one
    -- of these threads to kill the thread running the tests.
    Fork

    -- | Fork a child thread
  | ForkFrom t (Link ())

    -- | Cause a thread to terminate normally
  | Terminate t

    -- | Cause a thread to terminate abnormally
  | Crash t

    -- | Get all live threads
  | LiveThreads
  deriving (Int -> Cmd t -> ShowS
[Cmd t] -> ShowS
Cmd t -> TestName
(Int -> Cmd t -> ShowS)
-> (Cmd t -> TestName) -> ([Cmd t] -> ShowS) -> Show (Cmd t)
forall t. Show t => Int -> Cmd t -> ShowS
forall t. Show t => [Cmd t] -> ShowS
forall t. Show t => Cmd t -> TestName
forall a.
(Int -> a -> ShowS) -> (a -> TestName) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall t. Show t => Int -> Cmd t -> ShowS
showsPrec :: Int -> Cmd t -> ShowS
$cshow :: forall t. Show t => Cmd t -> TestName
show :: Cmd t -> TestName
$cshowList :: forall t. Show t => [Cmd t] -> ShowS
showList :: [Cmd t] -> ShowS
Show, (forall a b. (a -> b) -> Cmd a -> Cmd b)
-> (forall a b. a -> Cmd b -> Cmd a) -> Functor Cmd
forall a b. a -> Cmd b -> Cmd a
forall a b. (a -> b) -> Cmd a -> Cmd b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> Cmd a -> Cmd b
fmap :: forall a b. (a -> b) -> Cmd a -> Cmd b
$c<$ :: forall a b. a -> Cmd b -> Cmd a
<$ :: forall a b. a -> Cmd b -> Cmd a
Functor, (forall m. Monoid m => Cmd m -> m)
-> (forall m a. Monoid m => (a -> m) -> Cmd a -> m)
-> (forall m a. Monoid m => (a -> m) -> Cmd a -> m)
-> (forall a b. (a -> b -> b) -> b -> Cmd a -> b)
-> (forall a b. (a -> b -> b) -> b -> Cmd a -> b)
-> (forall b a. (b -> a -> b) -> b -> Cmd a -> b)
-> (forall b a. (b -> a -> b) -> b -> Cmd a -> b)
-> (forall a. (a -> a -> a) -> Cmd a -> a)
-> (forall a. (a -> a -> a) -> Cmd a -> a)
-> (forall a. Cmd a -> [a])
-> (forall a. Cmd a -> Bool)
-> (forall a. Cmd a -> Int)
-> (forall a. Eq a => a -> Cmd a -> Bool)
-> (forall a. Ord a => Cmd a -> a)
-> (forall a. Ord a => Cmd a -> a)
-> (forall a. Num a => Cmd a -> a)
-> (forall a. Num a => Cmd a -> a)
-> Foldable Cmd
forall a. Eq a => a -> Cmd a -> Bool
forall a. Num a => Cmd a -> a
forall a. Ord a => Cmd a -> a
forall m. Monoid m => Cmd m -> m
forall a. Cmd a -> Bool
forall a. Cmd a -> Int
forall a. Cmd a -> [a]
forall a. (a -> a -> a) -> Cmd a -> a
forall m a. Monoid m => (a -> m) -> Cmd a -> m
forall b a. (b -> a -> b) -> b -> Cmd a -> b
forall a b. (a -> b -> b) -> b -> Cmd a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall m. Monoid m => Cmd m -> m
fold :: forall m. Monoid m => Cmd m -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Cmd a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Cmd a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Cmd a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> Cmd a -> m
$cfoldr :: forall a b. (a -> b -> b) -> b -> Cmd a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Cmd a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Cmd a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Cmd a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Cmd a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Cmd a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Cmd a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> Cmd a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> Cmd a -> a
foldr1 :: forall a. (a -> a -> a) -> Cmd a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Cmd a -> a
foldl1 :: forall a. (a -> a -> a) -> Cmd a -> a
$ctoList :: forall a. Cmd a -> [a]
toList :: forall a. Cmd a -> [a]
$cnull :: forall a. Cmd a -> Bool
null :: forall a. Cmd a -> Bool
$clength :: forall a. Cmd a -> Int
length :: forall a. Cmd a -> Int
$celem :: forall a. Eq a => a -> Cmd a -> Bool
elem :: forall a. Eq a => a -> Cmd a -> Bool
$cmaximum :: forall a. Ord a => Cmd a -> a
maximum :: forall a. Ord a => Cmd a -> a
$cminimum :: forall a. Ord a => Cmd a -> a
minimum :: forall a. Ord a => Cmd a -> a
$csum :: forall a. Num a => Cmd a -> a
sum :: forall a. Num a => Cmd a -> a
$cproduct :: forall a. Num a => Cmd a -> a
product :: forall a. Num a => Cmd a -> a
Foldable, Functor Cmd
Foldable Cmd
(Functor Cmd, Foldable Cmd) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> Cmd a -> f (Cmd b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    Cmd (f a) -> f (Cmd a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Cmd a -> m (Cmd b))
-> (forall (m :: * -> *) a. Monad m => Cmd (m a) -> m (Cmd a))
-> Traversable Cmd
forall (t :: * -> *).
(Functor t, Foldable t) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => Cmd (m a) -> m (Cmd a)
forall (f :: * -> *) a. Applicative f => Cmd (f a) -> f (Cmd a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Cmd a -> m (Cmd b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Cmd a -> f (Cmd b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Cmd a -> f (Cmd b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Cmd a -> f (Cmd b)
$csequenceA :: forall (f :: * -> *) a. Applicative f => Cmd (f a) -> f (Cmd a)
sequenceA :: forall (f :: * -> *) a. Applicative f => Cmd (f a) -> f (Cmd a)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Cmd a -> m (Cmd b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Cmd a -> m (Cmd b)
$csequence :: forall (m :: * -> *) a. Monad m => Cmd (m a) -> m (Cmd a)
sequence :: forall (m :: * -> *) a. Monad m => Cmd (m a) -> m (Cmd a)
Traversable, (forall x. Cmd t -> Rep (Cmd t) x)
-> (forall x. Rep (Cmd t) x -> Cmd t) -> Generic (Cmd t)
forall x. Rep (Cmd t) x -> Cmd t
forall x. Cmd t -> Rep (Cmd t) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall t x. Rep (Cmd t) x -> Cmd t
forall t x. Cmd t -> Rep (Cmd t) x
$cfrom :: forall t x. Cmd t -> Rep (Cmd t) x
from :: forall x. Cmd t -> Rep (Cmd t) x
$cto :: forall t x. Rep (Cmd t) x -> Cmd t
to :: forall x. Rep (Cmd t) x -> Cmd t
Generic)

data Success t =
    Unit ()
  | Spawned t
  | Threads [t]
  deriving (Int -> Success t -> ShowS
[Success t] -> ShowS
Success t -> TestName
(Int -> Success t -> ShowS)
-> (Success t -> TestName)
-> ([Success t] -> ShowS)
-> Show (Success t)
forall t. Show t => Int -> Success t -> ShowS
forall t. Show t => [Success t] -> ShowS
forall t. Show t => Success t -> TestName
forall a.
(Int -> a -> ShowS) -> (a -> TestName) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall t. Show t => Int -> Success t -> ShowS
showsPrec :: Int -> Success t -> ShowS
$cshow :: forall t. Show t => Success t -> TestName
show :: Success t -> TestName
$cshowList :: forall t. Show t => [Success t] -> ShowS
showList :: [Success t] -> ShowS
Show, Success t -> Success t -> Bool
(Success t -> Success t -> Bool)
-> (Success t -> Success t -> Bool) -> Eq (Success t)
forall t. Eq t => Success t -> Success t -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall t. Eq t => Success t -> Success t -> Bool
== :: Success t -> Success t -> Bool
$c/= :: forall t. Eq t => Success t -> Success t -> Bool
/= :: Success t -> Success t -> Bool
Eq, (forall a b. (a -> b) -> Success a -> Success b)
-> (forall a b. a -> Success b -> Success a) -> Functor Success
forall a b. a -> Success b -> Success a
forall a b. (a -> b) -> Success a -> Success b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> Success a -> Success b
fmap :: forall a b. (a -> b) -> Success a -> Success b
$c<$ :: forall a b. a -> Success b -> Success a
<$ :: forall a b. a -> Success b -> Success a
Functor, (forall m. Monoid m => Success m -> m)
-> (forall m a. Monoid m => (a -> m) -> Success a -> m)
-> (forall m a. Monoid m => (a -> m) -> Success a -> m)
-> (forall a b. (a -> b -> b) -> b -> Success a -> b)
-> (forall a b. (a -> b -> b) -> b -> Success a -> b)
-> (forall b a. (b -> a -> b) -> b -> Success a -> b)
-> (forall b a. (b -> a -> b) -> b -> Success a -> b)
-> (forall a. (a -> a -> a) -> Success a -> a)
-> (forall a. (a -> a -> a) -> Success a -> a)
-> (forall a. Success a -> [a])
-> (forall a. Success a -> Bool)
-> (forall a. Success a -> Int)
-> (forall a. Eq a => a -> Success a -> Bool)
-> (forall a. Ord a => Success a -> a)
-> (forall a. Ord a => Success a -> a)
-> (forall a. Num a => Success a -> a)
-> (forall a. Num a => Success a -> a)
-> Foldable Success
forall a. Eq a => a -> Success a -> Bool
forall a. Num a => Success a -> a
forall a. Ord a => Success a -> a
forall m. Monoid m => Success m -> m
forall a. Success a -> Bool
forall a. Success a -> Int
forall a. Success a -> [a]
forall a. (a -> a -> a) -> Success a -> a
forall m a. Monoid m => (a -> m) -> Success a -> m
forall b a. (b -> a -> b) -> b -> Success a -> b
forall a b. (a -> b -> b) -> b -> Success a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall m. Monoid m => Success m -> m
fold :: forall m. Monoid m => Success m -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Success a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Success a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Success a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> Success a -> m
$cfoldr :: forall a b. (a -> b -> b) -> b -> Success a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Success a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Success a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Success a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Success a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Success a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Success a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> Success a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> Success a -> a
foldr1 :: forall a. (a -> a -> a) -> Success a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Success a -> a
foldl1 :: forall a. (a -> a -> a) -> Success a -> a
$ctoList :: forall a. Success a -> [a]
toList :: forall a. Success a -> [a]
$cnull :: forall a. Success a -> Bool
null :: forall a. Success a -> Bool
$clength :: forall a. Success a -> Int
length :: forall a. Success a -> Int
$celem :: forall a. Eq a => a -> Success a -> Bool
elem :: forall a. Eq a => a -> Success a -> Bool
$cmaximum :: forall a. Ord a => Success a -> a
maximum :: forall a. Ord a => Success a -> a
$cminimum :: forall a. Ord a => Success a -> a
minimum :: forall a. Ord a => Success a -> a
$csum :: forall a. Num a => Success a -> a
sum :: forall a. Num a => Success a -> a
$cproduct :: forall a. Num a => Success a -> a
product :: forall a. Num a => Success a -> a
Foldable, Functor Success
Foldable Success
(Functor Success, Foldable Success) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> Success a -> f (Success b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    Success (f a) -> f (Success a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Success a -> m (Success b))
-> (forall (m :: * -> *) a.
    Monad m =>
    Success (m a) -> m (Success a))
-> Traversable Success
forall (t :: * -> *).
(Functor t, Foldable t) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => Success (m a) -> m (Success a)
forall (f :: * -> *) a.
Applicative f =>
Success (f a) -> f (Success a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Success a -> m (Success b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Success a -> f (Success b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Success a -> f (Success b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Success a -> f (Success b)
$csequenceA :: forall (f :: * -> *) a.
Applicative f =>
Success (f a) -> f (Success a)
sequenceA :: forall (f :: * -> *) a.
Applicative f =>
Success (f a) -> f (Success a)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Success a -> m (Success b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Success a -> m (Success b)
$csequence :: forall (m :: * -> *) a. Monad m => Success (m a) -> m (Success a)
sequence :: forall (m :: * -> *) a. Monad m => Success (m a) -> m (Success a)
Traversable)

data Err =
    ErrTimeout
  | ErrInvalidThread String
  deriving (Int -> Err -> ShowS
[Err] -> ShowS
Err -> TestName
(Int -> Err -> ShowS)
-> (Err -> TestName) -> ([Err] -> ShowS) -> Show Err
forall a.
(Int -> a -> ShowS) -> (a -> TestName) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Err -> ShowS
showsPrec :: Int -> Err -> ShowS
$cshow :: Err -> TestName
show :: Err -> TestName
$cshowList :: [Err] -> ShowS
showList :: [Err] -> ShowS
Show, Err -> Err -> Bool
(Err -> Err -> Bool) -> (Err -> Err -> Bool) -> Eq Err
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Err -> Err -> Bool
== :: Err -> Err -> Bool
$c/= :: Err -> Err -> Bool
/= :: Err -> Err -> Bool
Eq)

newtype Resp t = Resp (Either Err (Success t))
  deriving (Int -> Resp t -> ShowS
[Resp t] -> ShowS
Resp t -> TestName
(Int -> Resp t -> ShowS)
-> (Resp t -> TestName) -> ([Resp t] -> ShowS) -> Show (Resp t)
forall t. Show t => Int -> Resp t -> ShowS
forall t. Show t => [Resp t] -> ShowS
forall t. Show t => Resp t -> TestName
forall a.
(Int -> a -> ShowS) -> (a -> TestName) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall t. Show t => Int -> Resp t -> ShowS
showsPrec :: Int -> Resp t -> ShowS
$cshow :: forall t. Show t => Resp t -> TestName
show :: Resp t -> TestName
$cshowList :: forall t. Show t => [Resp t] -> ShowS
showList :: [Resp t] -> ShowS
Show, Resp t -> Resp t -> Bool
(Resp t -> Resp t -> Bool)
-> (Resp t -> Resp t -> Bool) -> Eq (Resp t)
forall t. Eq t => Resp t -> Resp t -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall t. Eq t => Resp t -> Resp t -> Bool
== :: Resp t -> Resp t -> Bool
$c/= :: forall t. Eq t => Resp t -> Resp t -> Bool
/= :: Resp t -> Resp t -> Bool
Eq, (forall a b. (a -> b) -> Resp a -> Resp b)
-> (forall a b. a -> Resp b -> Resp a) -> Functor Resp
forall a b. a -> Resp b -> Resp a
forall a b. (a -> b) -> Resp a -> Resp b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a b. (a -> b) -> Resp a -> Resp b
fmap :: forall a b. (a -> b) -> Resp a -> Resp b
$c<$ :: forall a b. a -> Resp b -> Resp a
<$ :: forall a b. a -> Resp b -> Resp a
Functor, (forall m. Monoid m => Resp m -> m)
-> (forall m a. Monoid m => (a -> m) -> Resp a -> m)
-> (forall m a. Monoid m => (a -> m) -> Resp a -> m)
-> (forall a b. (a -> b -> b) -> b -> Resp a -> b)
-> (forall a b. (a -> b -> b) -> b -> Resp a -> b)
-> (forall b a. (b -> a -> b) -> b -> Resp a -> b)
-> (forall b a. (b -> a -> b) -> b -> Resp a -> b)
-> (forall a. (a -> a -> a) -> Resp a -> a)
-> (forall a. (a -> a -> a) -> Resp a -> a)
-> (forall a. Resp a -> [a])
-> (forall a. Resp a -> Bool)
-> (forall a. Resp a -> Int)
-> (forall a. Eq a => a -> Resp a -> Bool)
-> (forall a. Ord a => Resp a -> a)
-> (forall a. Ord a => Resp a -> a)
-> (forall a. Num a => Resp a -> a)
-> (forall a. Num a => Resp a -> a)
-> Foldable Resp
forall a. Eq a => a -> Resp a -> Bool
forall a. Num a => Resp a -> a
forall a. Ord a => Resp a -> a
forall m. Monoid m => Resp m -> m
forall a. Resp a -> Bool
forall a. Resp a -> Int
forall a. Resp a -> [a]
forall a. (a -> a -> a) -> Resp a -> a
forall m a. Monoid m => (a -> m) -> Resp a -> m
forall b a. (b -> a -> b) -> b -> Resp a -> b
forall a b. (a -> b -> b) -> b -> Resp a -> b
forall (t :: * -> *).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall m. Monoid m => Resp m -> m
fold :: forall m. Monoid m => Resp m -> m
$cfoldMap :: forall m a. Monoid m => (a -> m) -> Resp a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> Resp a -> m
$cfoldMap' :: forall m a. Monoid m => (a -> m) -> Resp a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> Resp a -> m
$cfoldr :: forall a b. (a -> b -> b) -> b -> Resp a -> b
foldr :: forall a b. (a -> b -> b) -> b -> Resp a -> b
$cfoldr' :: forall a b. (a -> b -> b) -> b -> Resp a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> Resp a -> b
$cfoldl :: forall b a. (b -> a -> b) -> b -> Resp a -> b
foldl :: forall b a. (b -> a -> b) -> b -> Resp a -> b
$cfoldl' :: forall b a. (b -> a -> b) -> b -> Resp a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> Resp a -> b
$cfoldr1 :: forall a. (a -> a -> a) -> Resp a -> a
foldr1 :: forall a. (a -> a -> a) -> Resp a -> a
$cfoldl1 :: forall a. (a -> a -> a) -> Resp a -> a
foldl1 :: forall a. (a -> a -> a) -> Resp a -> a
$ctoList :: forall a. Resp a -> [a]
toList :: forall a. Resp a -> [a]
$cnull :: forall a. Resp a -> Bool
null :: forall a. Resp a -> Bool
$clength :: forall a. Resp a -> Int
length :: forall a. Resp a -> Int
$celem :: forall a. Eq a => a -> Resp a -> Bool
elem :: forall a. Eq a => a -> Resp a -> Bool
$cmaximum :: forall a. Ord a => Resp a -> a
maximum :: forall a. Ord a => Resp a -> a
$cminimum :: forall a. Ord a => Resp a -> a
minimum :: forall a. Ord a => Resp a -> a
$csum :: forall a. Num a => Resp a -> a
sum :: forall a. Num a => Resp a -> a
$cproduct :: forall a. Num a => Resp a -> a
product :: forall a. Num a => Resp a -> a
Foldable, Functor Resp
Foldable Resp
(Functor Resp, Foldable Resp) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> Resp a -> f (Resp b))
-> (forall (f :: * -> *) a.
    Applicative f =>
    Resp (f a) -> f (Resp a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Resp a -> m (Resp b))
-> (forall (m :: * -> *) a. Monad m => Resp (m a) -> m (Resp a))
-> Traversable Resp
forall (t :: * -> *).
(Functor t, Foldable t) =>
(forall (f :: * -> *) a b.
 Applicative f =>
 (a -> f b) -> t a -> f (t b))
-> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
-> (forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: * -> *) a. Monad m => Resp (m a) -> m (Resp a)
forall (f :: * -> *) a. Applicative f => Resp (f a) -> f (Resp a)
forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Resp a -> m (Resp b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Resp a -> f (Resp b)
$ctraverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Resp a -> f (Resp b)
traverse :: forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Resp a -> f (Resp b)
$csequenceA :: forall (f :: * -> *) a. Applicative f => Resp (f a) -> f (Resp a)
sequenceA :: forall (f :: * -> *) a. Applicative f => Resp (f a) -> f (Resp a)
$cmapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Resp a -> m (Resp b)
mapM :: forall (m :: * -> *) a b.
Monad m =>
(a -> m b) -> Resp a -> m (Resp b)
$csequence :: forall (m :: * -> *) a. Monad m => Resp (m a) -> m (Resp a)
sequence :: forall (m :: * -> *) a. Monad m => Resp (m a) -> m (Resp a)
Traversable)

{-------------------------------------------------------------------------------
  "Up-to" comparison for responses

  This is used in 'postcondition'.
-------------------------------------------------------------------------------}

normalize :: Resp MockThread -> Resp MockThread
normalize :: Resp MockThread -> Resp MockThread
normalize (Resp Either Err (Success MockThread)
r) = Either Err (Success MockThread) -> Resp MockThread
forall t. Either Err (Success t) -> Resp t
Resp (Either Err (Success MockThread) -> Resp MockThread)
-> Either Err (Success MockThread) -> Resp MockThread
forall a b. (a -> b) -> a -> b
$ Success MockThread -> Success MockThread
aux (Success MockThread -> Success MockThread)
-> Either Err (Success MockThread)
-> Either Err (Success MockThread)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Either Err (Success MockThread)
r
  where
    aux :: Success MockThread -> Success MockThread
    aux :: Success MockThread -> Success MockThread
aux (Unit ())    = () -> Success MockThread
forall t. () -> Success t
Unit ()
    aux (Spawned MockThread
t)  = MockThread -> Success MockThread
forall t. t -> Success t
Spawned MockThread
t
    aux (Threads [MockThread]
ts) = [MockThread] -> Success MockThread
forall t. [t] -> Success t
Threads ([MockThread] -> [MockThread]
forall a. Ord a => [a] -> [a]
sort [MockThread]
ts)

{-------------------------------------------------------------------------------
  Run against the mock implementation
-------------------------------------------------------------------------------}

runMock :: Cmd MockThread -> Mock -> (Resp MockThread, Mock)
runMock :: Cmd MockThread -> Mock -> (Resp MockThread, Mock)
runMock Cmd MockThread
cmd m :: Mock
m@Mock{Int
Map MockThread (Link MockThread)
MockThreads
nextId :: Mock -> Int
threads :: Mock -> MockThreads
links :: Mock -> Map MockThread (Link MockThread)
nextId :: Int
threads :: MockThreads
links :: Map MockThread (Link MockThread)
..} =
    case Except Err (Success MockThread, Mock)
-> Either Err (Success MockThread, Mock)
forall e a. Except e a -> Either e a
runExcept (Cmd MockThread -> Except Err (Success MockThread, Mock)
go Cmd MockThread
cmd) of
      Left  Err
err           -> (Either Err (Success MockThread) -> Resp MockThread
forall t. Either Err (Success t) -> Resp t
Resp (Err -> Either Err (Success MockThread)
forall a b. a -> Either a b
Left Err
err), Mock
m)
      Right (Success MockThread
success, Mock
m') -> (Either Err (Success MockThread) -> Resp MockThread
forall t. Either Err (Success t) -> Resp t
Resp (Success MockThread -> Either Err (Success MockThread)
forall a b. b -> Either a b
Right Success MockThread
success), Mock
m')
  where
    go :: Cmd MockThread -> Except Err (Success MockThread, Mock)
    go :: Cmd MockThread -> Except Err (Success MockThread, Mock)
go Cmd MockThread
Fork                = Link MockThread
-> MockThread -> Except Err (Success MockThread, Mock)
createThread Link MockThread
forall a. Link a
DontLink           [Int
nextId]
    go (ForkFrom MockThread
t Link ()
linked) = Link MockThread
-> MockThread -> Except Err (Success MockThread, Mock)
createThread (MockThread -> () -> MockThread
forall a b. a -> b -> a
const MockThread
t (() -> MockThread) -> Link () -> Link MockThread
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Link ()
linked) (MockThread
t MockThread -> MockThread -> MockThread
forall a. [a] -> [a] -> [a]
++ [Int
nextId])
    go (Terminate MockThread
t)       = (\MockThreads
x -> (() -> Success MockThread
forall t. () -> Success t
Unit (), Mock
m { threads = x })) (MockThreads -> (Success MockThread, Mock))
-> Except Err MockThreads -> Except Err (Success MockThread, Mock)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MockThread -> MockThreads -> Except Err MockThreads
mockKill MockThread
t MockThreads
threads
    go (Crash MockThread
t)           = (\MockThreads
x -> (() -> Success MockThread
forall t. () -> Success t
Unit (), Mock
m { threads = x })) (MockThreads -> (Success MockThread, Mock))
-> Except Err MockThreads -> Except Err (Success MockThread, Mock)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MockThread -> MockThreads -> Except Err MockThreads
killAll  MockThread
t MockThreads
threads
    go Cmd MockThread
LiveThreads         = (Success MockThread, Mock) -> Except Err (Success MockThread, Mock)
forall a. a -> ExceptT Err Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return ([MockThread] -> Success MockThread
forall t. [t] -> Success t
Threads ([MockThread] -> Success MockThread)
-> [MockThread] -> Success MockThread
forall a b. (a -> b) -> a -> b
$ MockThreads -> [MockThread]
mockLiveThreads MockThreads
threads, Mock
m)

    createThread :: Link MockThread -- Thread to link to (if any)
                 -> MockThread -> Except Err (Success MockThread, Mock)
    createThread :: Link MockThread
-> MockThread -> Except Err (Success MockThread, Mock)
createThread Link MockThread
shouldLink MockThread
t = do
        MockThreads
threads' <- MockThread -> MockThreads -> Except Err MockThreads
mockFork MockThread
t MockThreads
threads
        (Success MockThread, Mock) -> Except Err (Success MockThread, Mock)
forall a. a -> ExceptT Err Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (
            MockThread -> Success MockThread
forall t. t -> Success t
Spawned MockThread
t
          , Mock
m { nextId  = succ nextId
              , threads = threads'
              , links   = Map.insert t shouldLink links
              }
          )

    killAll :: MockThread -> MockThreads -> Except Err MockThreads
    killAll :: MockThread -> MockThreads -> Except Err MockThreads
killAll MockThread
t =
        MockThread -> MockThreads -> Except Err MockThreads
mockKill MockThread
t (MockThreads -> Except Err MockThreads)
-> (MockThreads -> Except Err MockThreads)
-> MockThreads
-> Except Err MockThreads
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> Link MockThread -> MockThreads -> Except Err MockThreads
killParent (Link MockThread
-> MockThread
-> Map MockThread (Link MockThread)
-> Link MockThread
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Link MockThread
forall a. Link a
DontLink MockThread
t Map MockThread (Link MockThread)
links)
      where
        killParent :: Link MockThread -> MockThreads -> Except Err MockThreads
        killParent :: Link MockThread -> MockThreads -> Except Err MockThreads
killParent Link MockThread
DontLink            = MockThreads -> Except Err MockThreads
forall a. a -> ExceptT Err Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return
        killParent (LinkFromParent MockThread
t') = MockThread -> MockThreads -> Except Err MockThreads
killAll MockThread
t'

{-------------------------------------------------------------------------------
  Run in IO (possibly simulated)
-------------------------------------------------------------------------------}

data TestThread m = TestThread {
      -- | The underlying 'Thread'
      forall (m :: * -> *). TestThread m -> Thread m ()
testThread   :: Thread m ()

      -- | Parent thread this thread is linked to (if any)
    , forall (m :: * -> *). TestThread m -> Link (TestThread m)
threadLinked :: Link (TestThread m)

      -- | Send the thread instructions (see 'ThreadInstr')
    , forall (m :: * -> *). TestThread m -> TQueue m (QueuedInstr m)
threadComms  :: TQueue m (QueuedInstr m)
    }

-- | Instructions to a thread
--
-- The type argument indicates the result of the instruction
data ThreadInstr m :: Type -> Type where
  -- | Have the thread spawn a child thread
  ThreadFork :: Link () -> ThreadInstr m (TestThread m)

  -- | Have the thread terminate normally
  ThreadTerminate :: ThreadInstr m ()

  -- | Raise an exception in the thread
  ThreadCrash :: ThreadInstr m ()

-- | Instruction along with an MVar for the result
data QueuedInstr m = forall a. QueuedInstr (ThreadInstr m a) (StrictMVar m a)

runInThread :: IOLike m => TestThread m -> ThreadInstr m a -> m a
runInThread :: forall (m :: * -> *) a.
IOLike m =>
TestThread m -> ThreadInstr m a -> m a
runInThread TestThread{TQueue m (QueuedInstr m)
Thread m ()
Link (TestThread m)
testThread :: forall (m :: * -> *). TestThread m -> Thread m ()
threadLinked :: forall (m :: * -> *). TestThread m -> Link (TestThread m)
threadComms :: forall (m :: * -> *). TestThread m -> TQueue m (QueuedInstr m)
testThread :: Thread m ()
threadLinked :: Link (TestThread m)
threadComms :: TQueue m (QueuedInstr m)
..} ThreadInstr m a
instr = do
    StrictMVar m a
result <- m (StrictMVar m a)
forall (m :: * -> *) a. MonadMVar m => m (StrictMVar m a)
uncheckedNewEmptyMVar
    STM m () -> m ()
forall a. HasCallStack => STM m a -> m a
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
STM m a -> m a
atomically (STM m () -> m ()) -> STM m () -> m ()
forall a b. (a -> b) -> a -> b
$ TQueue m (QueuedInstr m) -> QueuedInstr m -> STM m ()
forall a. TQueue m a -> a -> STM m ()
forall (m :: * -> *) a. MonadSTM m => TQueue m a -> a -> STM m ()
writeTQueue TQueue m (QueuedInstr m)
threadComms (ThreadInstr m a -> StrictMVar m a -> QueuedInstr m
forall (m :: * -> *) a.
ThreadInstr m a -> StrictMVar m a -> QueuedInstr m
QueuedInstr ThreadInstr m a
instr StrictMVar m a
result)
    StrictMVar m a -> m a
forall (m :: * -> *) a. MonadMVar m => StrictMVar m a -> m a
takeMVar StrictMVar m a
result

instance (IOLike m) => Show (TestThread m) where
  show :: TestThread m -> TestName
show TestThread{TQueue m (QueuedInstr m)
Thread m ()
Link (TestThread m)
testThread :: forall (m :: * -> *). TestThread m -> Thread m ()
threadLinked :: forall (m :: * -> *). TestThread m -> Link (TestThread m)
threadComms :: forall (m :: * -> *). TestThread m -> TQueue m (QueuedInstr m)
testThread :: Thread m ()
threadLinked :: Link (TestThread m)
threadComms :: TQueue m (QueuedInstr m)
..} = TestName
"<Thread " TestName -> ShowS
forall a. [a] -> [a] -> [a]
++ ThreadId m -> TestName
forall a. Show a => a -> TestName
show (Thread m () -> ThreadId m
forall (m :: * -> *) a. Thread m a -> ThreadId m
threadId Thread m ()
testThread) TestName -> ShowS
forall a. [a] -> [a] -> [a]
++ TestName
">"

instance (IOLike m) => Eq (TestThread m) where
  == :: TestThread m -> TestThread m -> Bool
(==) = ThreadId m -> ThreadId m -> Bool
forall a. Eq a => a -> a -> Bool
(==) (ThreadId m -> ThreadId m -> Bool)
-> (TestThread m -> ThreadId m)
-> TestThread m
-> TestThread m
-> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (Thread m () -> ThreadId m
forall (m :: * -> *) a. Thread m a -> ThreadId m
threadId (Thread m () -> ThreadId m)
-> (TestThread m -> Thread m ()) -> TestThread m -> ThreadId m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TestThread m -> Thread m ()
forall (m :: * -> *). TestThread m -> Thread m ()
testThread)

-- | Create a new thread in the given registry
--
-- In order to be able to see which threads are alive, we have threads
-- register and unregister themselves. We do not reuse the registry for this,
-- to avoid circular reasoning in the tests.
newThread :: forall m. IOLike m
          => StrictTVar m [TestThread m]
          -> ResourceRegistry m
          -> Link (TestThread m)
          -> m (TestThread m)
newThread :: forall (m :: * -> *).
IOLike m =>
StrictTVar m [TestThread m]
-> ResourceRegistry m -> Link (TestThread m) -> m (TestThread m)
newThread StrictTVar m [TestThread m]
alive ResourceRegistry m
parentReg = \Link (TestThread m)
shouldLink -> do
    TQueue m (QueuedInstr m)
comms      <- STM m (TQueue m (QueuedInstr m)) -> m (TQueue m (QueuedInstr m))
forall a. HasCallStack => STM m a -> m a
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
STM m a -> m a
atomically (STM m (TQueue m (QueuedInstr m)) -> m (TQueue m (QueuedInstr m)))
-> STM m (TQueue m (QueuedInstr m)) -> m (TQueue m (QueuedInstr m))
forall a b. (a -> b) -> a -> b
$ STM m (TQueue m (QueuedInstr m))
forall a. STM m (TQueue m a)
forall (m :: * -> *) a. MonadSTM m => STM m (TQueue m a)
newTQueue
    StrictMVar m (TestThread m)
spawned    <- m (StrictMVar m (TestThread m))
forall (m :: * -> *) a. MonadMVar m => m (StrictMVar m a)
uncheckedNewEmptyMVar

    Thread m ()
thread <- ResourceRegistry m -> TestName -> m () -> m (Thread m ())
forall (m :: * -> *) a.
(IOLike m, HasCallStack) =>
ResourceRegistry m -> TestName -> m a -> m (Thread m a)
forkThread ResourceRegistry m
parentReg TestName
"newThread" (m () -> m (Thread m ())) -> m () -> m (Thread m ())
forall a b. (a -> b) -> a -> b
$
                (ResourceRegistry m -> m ()) -> m ()
forall (m :: * -> *) a.
(IOLike m, HasCallStack) =>
(ResourceRegistry m -> m a) -> m a
withRegistry ((ResourceRegistry m -> m ()) -> m ())
-> (ResourceRegistry m -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ \ResourceRegistry m
childReg ->
                  ResourceRegistry m
-> StrictMVar m (TestThread m) -> TQueue m (QueuedInstr m) -> m ()
threadBody ResourceRegistry m
childReg StrictMVar m (TestThread m)
spawned TQueue m (QueuedInstr m)
comms
    case Link (TestThread m)
shouldLink of
      LinkFromParent TestThread m
_ -> Thread m () -> m ()
forall (m :: * -> *) a. IOLike m => Thread m a -> m ()
linkToRegistry Thread m ()
thread
      Link (TestThread m)
DontLink         -> () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

    let testThread :: TestThread m
        testThread :: TestThread m
testThread = TestThread {
                         testThread :: Thread m ()
testThread   = Thread m ()
thread
                       , threadLinked :: Link (TestThread m)
threadLinked = Link (TestThread m)
shouldLink
                       , threadComms :: TQueue m (QueuedInstr m)
threadComms  = TQueue m (QueuedInstr m)
comms
                       }

    -- Make sure to register thread before starting it
    STM m () -> m ()
forall a. HasCallStack => STM m a -> m a
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
STM m a -> m a
atomically (STM m () -> m ()) -> STM m () -> m ()
forall a b. (a -> b) -> a -> b
$ StrictTVar m [TestThread m]
-> ([TestThread m] -> [TestThread m]) -> STM m ()
forall (m :: * -> *) a.
MonadSTM m =>
StrictTVar m a -> (a -> a) -> STM m ()
modifyTVar StrictTVar m [TestThread m]
alive (TestThread m
testThreadTestThread m -> [TestThread m] -> [TestThread m]
forall a. a -> [a] -> [a]
:)
    StrictMVar m (TestThread m) -> TestThread m -> m ()
forall (m :: * -> *) a.
(HasCallStack, MonadMVar m) =>
StrictMVar m a -> a -> m ()
putMVar StrictMVar m (TestThread m)
spawned TestThread m
testThread
    TestThread m -> m (TestThread m)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return TestThread m
testThread
  where
    threadBody :: ResourceRegistry m
               -> StrictMVar m (TestThread m)
               -> TQueue m (QueuedInstr m)
               -> m ()
    threadBody :: ResourceRegistry m
-> StrictMVar m (TestThread m) -> TQueue m (QueuedInstr m) -> m ()
threadBody ResourceRegistry m
childReg StrictMVar m (TestThread m)
spawned TQueue m (QueuedInstr m)
comms = do
        TestThread m
us <- StrictMVar m (TestThread m) -> m (TestThread m)
forall (m :: * -> *) a. MonadMVar m => StrictMVar m a -> m a
readMVar StrictMVar m (TestThread m)
spawned
        TestThread m -> m ()
loop TestThread m
us m () -> m () -> m ()
forall a b. m a -> m b -> m a
forall (m :: * -> *) a b. MonadThrow m => m a -> m b -> m a
`finally` (STM m () -> m ()
forall a. HasCallStack => STM m a -> m a
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
STM m a -> m a
atomically (STM m () -> m ()) -> STM m () -> m ()
forall a b. (a -> b) -> a -> b
$ StrictTVar m [TestThread m]
-> ([TestThread m] -> [TestThread m]) -> STM m ()
forall (m :: * -> *) a.
MonadSTM m =>
StrictTVar m a -> (a -> a) -> STM m ()
modifyTVar StrictTVar m [TestThread m]
alive (TestThread m -> [TestThread m] -> [TestThread m]
forall a. Eq a => a -> [a] -> [a]
delete TestThread m
us))
      where
        loop :: TestThread m -> m ()
        loop :: TestThread m -> m ()
loop TestThread m
us = do
          QueuedInstr ThreadInstr m a
instr StrictMVar m a
result <- STM m (QueuedInstr m) -> m (QueuedInstr m)
forall a. HasCallStack => STM m a -> m a
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
STM m a -> m a
atomically (STM m (QueuedInstr m) -> m (QueuedInstr m))
-> STM m (QueuedInstr m) -> m (QueuedInstr m)
forall a b. (a -> b) -> a -> b
$ TQueue m (QueuedInstr m) -> STM m (QueuedInstr m)
forall a. TQueue m a -> STM m a
forall (m :: * -> *) a. MonadSTM m => TQueue m a -> STM m a
readTQueue TQueue m (QueuedInstr m)
comms
          case ThreadInstr m a
instr of
            ThreadFork Link ()
linked -> do
              TestThread m
child <- StrictTVar m [TestThread m]
-> ResourceRegistry m -> Link (TestThread m) -> m (TestThread m)
forall (m :: * -> *).
IOLike m =>
StrictTVar m [TestThread m]
-> ResourceRegistry m -> Link (TestThread m) -> m (TestThread m)
newThread StrictTVar m [TestThread m]
alive ResourceRegistry m
childReg (TestThread m -> () -> TestThread m
forall a b. a -> b -> a
const TestThread m
us (() -> TestThread m) -> Link () -> Link (TestThread m)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Link ()
linked)
              StrictMVar m a -> a -> m ()
forall (m :: * -> *) a.
(HasCallStack, MonadMVar m) =>
StrictMVar m a -> a -> m ()
putMVar StrictMVar m a
result a
TestThread m
child
              TestThread m -> m ()
loop TestThread m
us
            ThreadInstr m a
ThreadTerminate -> do
              StrictMVar m a -> a -> m ()
forall (m :: * -> *) a.
(HasCallStack, MonadMVar m) =>
StrictMVar m a -> a -> m ()
putMVar StrictMVar m a
result ()
            ThreadInstr m a
ThreadCrash -> do
              StrictMVar m a -> a -> m ()
forall (m :: * -> *) a.
(HasCallStack, MonadMVar m) =>
StrictMVar m a -> a -> m ()
putMVar StrictMVar m a
result ()
              TestName -> m ()
forall a. HasCallStack => TestName -> a
error TestName
"crashing"

runIO :: forall m. (IOLike m, MonadTimer m)
      => StrictTVar m [TestThread m]
      -> ResourceRegistry m
      -> Cmd (TestThread m) -> m (Resp (TestThread m))
runIO :: forall (m :: * -> *).
(IOLike m, MonadTimer m) =>
StrictTVar m [TestThread m]
-> ResourceRegistry m
-> Cmd (TestThread m)
-> m (Resp (TestThread m))
runIO StrictTVar m [TestThread m]
alive ResourceRegistry m
reg Cmd (TestThread m)
cmd = m (Maybe (Success (TestThread m))) -> m (Resp (TestThread m))
forall a. m (Maybe (Success a)) -> m (Resp a)
catchEx (m (Maybe (Success (TestThread m))) -> m (Resp (TestThread m)))
-> m (Maybe (Success (TestThread m))) -> m (Resp (TestThread m))
forall a b. (a -> b) -> a -> b
$ DiffTime
-> m (Success (TestThread m)) -> m (Maybe (Success (TestThread m)))
forall a. DiffTime -> m a -> m (Maybe a)
forall (m :: * -> *) a.
MonadTimer m =>
DiffTime -> m a -> m (Maybe a)
timeout DiffTime
1 (m (Success (TestThread m)) -> m (Maybe (Success (TestThread m))))
-> m (Success (TestThread m)) -> m (Maybe (Success (TestThread m)))
forall a b. (a -> b) -> a -> b
$
    case Cmd (TestThread m)
cmd of
      Cmd (TestThread m)
Fork ->
        TestThread m -> Success (TestThread m)
forall t. t -> Success t
Spawned (TestThread m -> Success (TestThread m))
-> m (TestThread m) -> m (Success (TestThread m))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StrictTVar m [TestThread m]
-> ResourceRegistry m -> Link (TestThread m) -> m (TestThread m)
forall (m :: * -> *).
IOLike m =>
StrictTVar m [TestThread m]
-> ResourceRegistry m -> Link (TestThread m) -> m (TestThread m)
newThread StrictTVar m [TestThread m]
alive ResourceRegistry m
reg Link (TestThread m)
forall a. Link a
DontLink
      ForkFrom TestThread m
thread Link ()
shouldLink -> do
        TestThread m -> Success (TestThread m)
forall t. t -> Success t
Spawned (TestThread m -> Success (TestThread m))
-> m (TestThread m) -> m (Success (TestThread m))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TestThread m -> ThreadInstr m (TestThread m) -> m (TestThread m)
forall (m :: * -> *) a.
IOLike m =>
TestThread m -> ThreadInstr m a -> m a
runInThread TestThread m
thread (Link () -> ThreadInstr m (TestThread m)
forall (m :: * -> *). Link () -> ThreadInstr m (TestThread m)
ThreadFork Link ()
shouldLink)
      Terminate TestThread m
thread -> do
        TestThread m -> ThreadInstr m () -> m ()
forall (m :: * -> *) a.
IOLike m =>
TestThread m -> ThreadInstr m a -> m a
runInThread TestThread m
thread ThreadInstr m ()
forall (m :: * -> *). ThreadInstr m ()
ThreadTerminate
        () -> Success (TestThread m)
forall t. () -> Success t
Unit (() -> Success (TestThread m))
-> m () -> m (Success (TestThread m))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TestThread m -> m ()
waitForTermination TestThread m
thread
      Crash TestThread m
thread -> do
        TestThread m -> ThreadInstr m () -> m ()
forall (m :: * -> *) a.
IOLike m =>
TestThread m -> ThreadInstr m a -> m a
runInThread TestThread m
thread ThreadInstr m ()
forall (m :: * -> *). ThreadInstr m ()
ThreadCrash
        () -> Success (TestThread m)
forall t. () -> Success t
Unit (() -> Success (TestThread m))
-> m () -> m (Success (TestThread m))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TestThread m -> m ()
waitForTermination TestThread m
thread
      Cmd (TestThread m)
LiveThreads ->
        STM m (Success (TestThread m)) -> m (Success (TestThread m))
forall a. HasCallStack => STM m a -> m a
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
STM m a -> m a
atomically (STM m (Success (TestThread m)) -> m (Success (TestThread m)))
-> STM m (Success (TestThread m)) -> m (Success (TestThread m))
forall a b. (a -> b) -> a -> b
$ [TestThread m] -> Success (TestThread m)
forall t. [t] -> Success t
Threads ([TestThread m] -> Success (TestThread m))
-> STM m [TestThread m] -> STM m (Success (TestThread m))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StrictTVar m [TestThread m] -> STM m [TestThread m]
forall (m :: * -> *) a. MonadSTM m => StrictTVar m a -> STM m a
readTVar StrictTVar m [TestThread m]
alive
  where
    catchEx :: m (Maybe (Success a)) -> m (Resp a)
    catchEx :: forall a. m (Maybe (Success a)) -> m (Resp a)
catchEx = (Maybe (Success a) -> Resp a)
-> m (Maybe (Success a)) -> m (Resp a)
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Either Err (Success a) -> Resp a
forall t. Either Err (Success t) -> Resp t
Resp (Either Err (Success a) -> Resp a)
-> (Maybe (Success a) -> Either Err (Success a))
-> Maybe (Success a)
-> Resp a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Either Err (Success a)
-> (Success a -> Either Err (Success a))
-> Maybe (Success a)
-> Either Err (Success a)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Err -> Either Err (Success a)
forall a b. a -> Either a b
Left Err
ErrTimeout) Success a -> Either Err (Success a)
forall a b. b -> Either a b
Right)

    -- For the thread and all of its linked parents to have terminated
    waitForTermination :: TestThread m -> m ()
    waitForTermination :: TestThread m -> m ()
waitForTermination TestThread m
t = do
        Either SomeException ()
result <- m () -> m (Either SomeException ())
forall e a. Exception e => m a -> m (Either e a)
forall (m :: * -> *) e a.
(MonadCatch m, Exception e) =>
m a -> m (Either e a)
try (m () -> m (Either SomeException ()))
-> m () -> m (Either SomeException ())
forall a b. (a -> b) -> a -> b
$ Thread m () -> m ()
forall (m :: * -> *) a. IOLike m => Thread m a -> m a
waitThread (TestThread m -> Thread m ()
forall (m :: * -> *). TestThread m -> Thread m ()
testThread TestThread m
t)
        case (Either SomeException ()
result, TestThread m -> Link (TestThread m)
forall (m :: * -> *). TestThread m -> Link (TestThread m)
threadLinked TestThread m
t) of
          (Left (SomeException
_ :: SomeException), LinkFromParent TestThread m
t') ->
            TestThread m -> m ()
waitForTermination TestThread m
t'
          (Either SomeException (), Link (TestThread m))
_otherwise ->
            () -> m ()
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ()

{-------------------------------------------------------------------------------
  QSM wrappers
-------------------------------------------------------------------------------}

newtype At m f r = At (f (Reference (TestThread m) r))

deriving instance (Show1 r, IOLike m) => Show (At m Cmd  r)
deriving instance (Show1 r, IOLike m) => Show (At m Resp r)

{-------------------------------------------------------------------------------
  Relate model to IO
-------------------------------------------------------------------------------}

-- TODO: Use RefEnv?
type Refs m r = [(Reference (TestThread m) r, MockThread)]

(!) :: (Eq k, Show k) => [(k, a)] -> k -> a
[(k, a)]
env ! :: forall k a. (Eq k, Show k) => [(k, a)] -> k -> a
! k
r = case k -> [(k, a)] -> Maybe a
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup k
r [(k, a)]
env of
            Just a
a  -> a
a
            Maybe a
Nothing -> TestName -> a
forall a. HasCallStack => TestName -> a
error (TestName -> a) -> TestName -> a
forall a b. (a -> b) -> a -> b
$ TestName
"Unknown reference: " TestName -> ShowS
forall a. [a] -> [a] -> [a]
++ k -> TestName
forall a. Show a => a -> TestName
show k
r

data Model m r = Model Mock (Refs m r)
  deriving (Int -> Model m r -> ShowS
[Model m r] -> ShowS
Model m r -> TestName
(Int -> Model m r -> ShowS)
-> (Model m r -> TestName)
-> ([Model m r] -> ShowS)
-> Show (Model m r)
forall a.
(Int -> a -> ShowS) -> (a -> TestName) -> ([a] -> ShowS) -> Show a
forall (m :: * -> *) (r :: * -> *).
(Show1 r, IOLike m) =>
Int -> Model m r -> ShowS
forall (m :: * -> *) (r :: * -> *).
(Show1 r, IOLike m) =>
[Model m r] -> ShowS
forall (m :: * -> *) (r :: * -> *).
(Show1 r, IOLike m) =>
Model m r -> TestName
$cshowsPrec :: forall (m :: * -> *) (r :: * -> *).
(Show1 r, IOLike m) =>
Int -> Model m r -> ShowS
showsPrec :: Int -> Model m r -> ShowS
$cshow :: forall (m :: * -> *) (r :: * -> *).
(Show1 r, IOLike m) =>
Model m r -> TestName
show :: Model m r -> TestName
$cshowList :: forall (m :: * -> *) (r :: * -> *).
(Show1 r, IOLike m) =>
[Model m r] -> ShowS
showList :: [Model m r] -> ShowS
Show, (forall x. Model m r -> Rep (Model m r) x)
-> (forall x. Rep (Model m r) x -> Model m r)
-> Generic (Model m r)
forall x. Rep (Model m r) x -> Model m r
forall x. Model m r -> Rep (Model m r) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (m :: * -> *) (r :: * -> *) x.
Rep (Model m r) x -> Model m r
forall (m :: * -> *) (r :: * -> *) x.
Model m r -> Rep (Model m r) x
$cfrom :: forall (m :: * -> *) (r :: * -> *) x.
Model m r -> Rep (Model m r) x
from :: forall x. Model m r -> Rep (Model m r) x
$cto :: forall (m :: * -> *) (r :: * -> *) x.
Rep (Model m r) x -> Model m r
to :: forall x. Rep (Model m r) x -> Model m r
Generic)

initModel :: Model m r
initModel :: forall (m :: * -> *) (r :: * -> *). Model m r
initModel = Mock -> Refs m r -> Model m r
forall (m :: * -> *) (r :: * -> *). Mock -> Refs m r -> Model m r
Model Mock
emptyMock []

{-------------------------------------------------------------------------------
  Events
-------------------------------------------------------------------------------}

toMock :: forall m f r. (Functor f, Eq1 r, Show1 r, IOLike m)
       => Model m r -> At m f r -> f MockThread
toMock :: forall (m :: * -> *) (f :: * -> *) (r :: * -> *).
(Functor f, Eq1 r, Show1 r, IOLike m) =>
Model m r -> At m f r -> f MockThread
toMock (Model Mock
_ Refs m r
hs) (At f (Reference (TestThread m) r)
fr) = (Refs m r
hs Refs m r -> Reference (TestThread m) r -> MockThread
forall k a. (Eq k, Show k) => [(k, a)] -> k -> a
!) (Reference (TestThread m) r -> MockThread)
-> f (Reference (TestThread m) r) -> f MockThread
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> f (Reference (TestThread m) r)
fr

step :: (Eq1 r, Show1 r, IOLike m)
     => Model m r -> At m Cmd r -> (Resp MockThread, Mock)
step :: forall (r :: * -> *) (m :: * -> *).
(Eq1 r, Show1 r, IOLike m) =>
Model m r -> At m Cmd r -> (Resp MockThread, Mock)
step m :: Model m r
m@(Model Mock
mock Refs m r
_) At m Cmd r
c = Cmd MockThread -> Mock -> (Resp MockThread, Mock)
runMock (Model m r -> At m Cmd r -> Cmd MockThread
forall (m :: * -> *) (f :: * -> *) (r :: * -> *).
(Functor f, Eq1 r, Show1 r, IOLike m) =>
Model m r -> At m f r -> f MockThread
toMock Model m r
m At m Cmd r
c) Mock
mock

data Event m r = Event {
      forall (m :: * -> *) (r :: * -> *). Event m r -> Model m r
before   :: Model  m     r
    , forall (m :: * -> *) (r :: * -> *). Event m r -> At m Cmd r
cmd      :: At     m Cmd r
    , forall (m :: * -> *) (r :: * -> *). Event m r -> Model m r
after    :: Model  m     r
    , forall (m :: * -> *) (r :: * -> *). Event m r -> Resp MockThread
mockResp :: Resp MockThread
    }

lockstep :: (Eq1 r, Show1 r, IOLike m)
         => Model m      r
         -> At    m Cmd  r
         -> At    m Resp r
         -> Event m      r
lockstep :: forall (r :: * -> *) (m :: * -> *).
(Eq1 r, Show1 r, IOLike m) =>
Model m r -> At m Cmd r -> At m Resp r -> Event m r
lockstep m :: Model m r
m@(Model Mock
_ Refs m r
hs) At m Cmd r
c (At Resp (Reference (TestThread m) r)
resp) = Event {
      before :: Model m r
before   = Model m r
m
    , cmd :: At m Cmd r
cmd      = At m Cmd r
c
    , after :: Model m r
after    = Mock -> Refs m r -> Model m r
forall (m :: * -> *) (r :: * -> *). Mock -> Refs m r -> Model m r
Model Mock
mock' (Refs m r
hs Refs m r -> Refs m r -> Refs m r
forall a. Semigroup a => a -> a -> a
<> Refs m r
hs')
    , mockResp :: Resp MockThread
mockResp = Resp MockThread
resp'
    }
  where
    (Resp MockThread
resp', Mock
mock') = Model m r -> At m Cmd r -> (Resp MockThread, Mock)
forall (r :: * -> *) (m :: * -> *).
(Eq1 r, Show1 r, IOLike m) =>
Model m r -> At m Cmd r -> (Resp MockThread, Mock)
step Model m r
m At m Cmd r
c
    hs' :: Refs m r
hs' = [Reference (TestThread m) r] -> [MockThread] -> Refs m r
forall a b. [a] -> [b] -> [(a, b)]
zip (Resp (Reference (TestThread m) r) -> [Reference (TestThread m) r]
forall a. Resp a -> [a]
newHandles Resp (Reference (TestThread m) r)
resp) (Resp MockThread -> [MockThread]
forall a. Resp a -> [a]
newHandles Resp MockThread
resp')

    newHandles :: Resp r -> [r]
    newHandles :: forall a. Resp a -> [a]
newHandles (Resp (Left Err
_))            = []
    newHandles (Resp (Right (Unit ())))   = []
    newHandles (Resp (Right (Spawned r
t))) = [r
t]
    newHandles (Resp (Right (Threads [r]
_))) = []

{-------------------------------------------------------------------------------
  Generator
-------------------------------------------------------------------------------}

generator :: forall m. Model m Symbolic -> Maybe (Gen (At m Cmd Symbolic))
generator :: forall (m :: * -> *).
Model m Symbolic -> Maybe (Gen (At m Cmd Symbolic))
generator (Model Mock
_ Refs m Symbolic
hs) = Gen (At m Cmd Symbolic) -> Maybe (Gen (At m Cmd Symbolic))
forall a. a -> Maybe a
Just (Gen (At m Cmd Symbolic) -> Maybe (Gen (At m Cmd Symbolic)))
-> Gen (At m Cmd Symbolic) -> Maybe (Gen (At m Cmd Symbolic))
forall a b. (a -> b) -> a -> b
$ [Gen (At m Cmd Symbolic)] -> Gen (At m Cmd Symbolic)
forall a. [Gen a] -> Gen a
QC.oneof ([Gen (At m Cmd Symbolic)] -> Gen (At m Cmd Symbolic))
-> [Gen (At m Cmd Symbolic)] -> Gen (At m Cmd Symbolic)
forall a b. (a -> b) -> a -> b
$ [[Gen (At m Cmd Symbolic)]] -> [Gen (At m Cmd Symbolic)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [
      [Gen (At m Cmd Symbolic)]
withoutHandle
    , if Refs m Symbolic -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null Refs m Symbolic
hs then [] else Gen (Reference (TestThread m) Symbolic)
-> [Gen (At m Cmd Symbolic)]
withHandle ([Reference (TestThread m) Symbolic]
-> Gen (Reference (TestThread m) Symbolic)
forall a. [a] -> Gen a
QC.elements (((Reference (TestThread m) Symbolic, MockThread)
 -> Reference (TestThread m) Symbolic)
-> Refs m Symbolic -> [Reference (TestThread m) Symbolic]
forall a b. (a -> b) -> [a] -> [b]
map (Reference (TestThread m) Symbolic, MockThread)
-> Reference (TestThread m) Symbolic
forall a b. (a, b) -> a
fst Refs m Symbolic
hs))
    ]
  where
    withoutHandle :: [Gen (At m Cmd Symbolic)]
    withoutHandle :: [Gen (At m Cmd Symbolic)]
withoutHandle = [
          (Cmd (Reference (TestThread m) Symbolic) -> At m Cmd Symbolic)
-> Gen (Cmd (Reference (TestThread m) Symbolic))
-> Gen (At m Cmd Symbolic)
forall a b. (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Cmd (Reference (TestThread m) Symbolic) -> At m Cmd Symbolic
forall (m :: * -> *) (f :: * -> *) (r :: * -> *).
f (Reference (TestThread m) r) -> At m f r
At (Gen (Cmd (Reference (TestThread m) Symbolic))
 -> Gen (At m Cmd Symbolic))
-> Gen (Cmd (Reference (TestThread m) Symbolic))
-> Gen (At m Cmd Symbolic)
forall a b. (a -> b) -> a -> b
$ Cmd (Reference (TestThread m) Symbolic)
-> Gen (Cmd (Reference (TestThread m) Symbolic))
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return Cmd (Reference (TestThread m) Symbolic)
forall t. Cmd t
Fork
        , (Cmd (Reference (TestThread m) Symbolic) -> At m Cmd Symbolic)
-> Gen (Cmd (Reference (TestThread m) Symbolic))
-> Gen (At m Cmd Symbolic)
forall a b. (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Cmd (Reference (TestThread m) Symbolic) -> At m Cmd Symbolic
forall (m :: * -> *) (f :: * -> *) (r :: * -> *).
f (Reference (TestThread m) r) -> At m f r
At (Gen (Cmd (Reference (TestThread m) Symbolic))
 -> Gen (At m Cmd Symbolic))
-> Gen (Cmd (Reference (TestThread m) Symbolic))
-> Gen (At m Cmd Symbolic)
forall a b. (a -> b) -> a -> b
$ Cmd (Reference (TestThread m) Symbolic)
-> Gen (Cmd (Reference (TestThread m) Symbolic))
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return Cmd (Reference (TestThread m) Symbolic)
forall t. Cmd t
LiveThreads
        ]

    withHandle :: Gen (Reference (TestThread m) Symbolic)
               -> [Gen (At m Cmd Symbolic)]
    withHandle :: Gen (Reference (TestThread m) Symbolic)
-> [Gen (At m Cmd Symbolic)]
withHandle Gen (Reference (TestThread m) Symbolic)
pickThread = [
          (Cmd (Reference (TestThread m) Symbolic) -> At m Cmd Symbolic)
-> Gen (Cmd (Reference (TestThread m) Symbolic))
-> Gen (At m Cmd Symbolic)
forall a b. (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Cmd (Reference (TestThread m) Symbolic) -> At m Cmd Symbolic
forall (m :: * -> *) (f :: * -> *) (r :: * -> *).
f (Reference (TestThread m) r) -> At m f r
At (Gen (Cmd (Reference (TestThread m) Symbolic))
 -> Gen (At m Cmd Symbolic))
-> Gen (Cmd (Reference (TestThread m) Symbolic))
-> Gen (At m Cmd Symbolic)
forall a b. (a -> b) -> a -> b
$ Reference (TestThread m) Symbolic
-> Cmd (Reference (TestThread m) Symbolic)
forall t. t -> Cmd t
Terminate (Reference (TestThread m) Symbolic
 -> Cmd (Reference (TestThread m) Symbolic))
-> Gen (Reference (TestThread m) Symbolic)
-> Gen (Cmd (Reference (TestThread m) Symbolic))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (Reference (TestThread m) Symbolic)
pickThread
        , (Cmd (Reference (TestThread m) Symbolic) -> At m Cmd Symbolic)
-> Gen (Cmd (Reference (TestThread m) Symbolic))
-> Gen (At m Cmd Symbolic)
forall a b. (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Cmd (Reference (TestThread m) Symbolic) -> At m Cmd Symbolic
forall (m :: * -> *) (f :: * -> *) (r :: * -> *).
f (Reference (TestThread m) r) -> At m f r
At (Gen (Cmd (Reference (TestThread m) Symbolic))
 -> Gen (At m Cmd Symbolic))
-> Gen (Cmd (Reference (TestThread m) Symbolic))
-> Gen (At m Cmd Symbolic)
forall a b. (a -> b) -> a -> b
$ Reference (TestThread m) Symbolic
-> Cmd (Reference (TestThread m) Symbolic)
forall t. t -> Cmd t
Crash     (Reference (TestThread m) Symbolic
 -> Cmd (Reference (TestThread m) Symbolic))
-> Gen (Reference (TestThread m) Symbolic)
-> Gen (Cmd (Reference (TestThread m) Symbolic))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (Reference (TestThread m) Symbolic)
pickThread
        , (Cmd (Reference (TestThread m) Symbolic) -> At m Cmd Symbolic)
-> Gen (Cmd (Reference (TestThread m) Symbolic))
-> Gen (At m Cmd Symbolic)
forall a b. (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Cmd (Reference (TestThread m) Symbolic) -> At m Cmd Symbolic
forall (m :: * -> *) (f :: * -> *) (r :: * -> *).
f (Reference (TestThread m) r) -> At m f r
At (Gen (Cmd (Reference (TestThread m) Symbolic))
 -> Gen (At m Cmd Symbolic))
-> Gen (Cmd (Reference (TestThread m) Symbolic))
-> Gen (At m Cmd Symbolic)
forall a b. (a -> b) -> a -> b
$ Reference (TestThread m) Symbolic
-> Link () -> Cmd (Reference (TestThread m) Symbolic)
forall t. t -> Link () -> Cmd t
ForkFrom  (Reference (TestThread m) Symbolic
 -> Link () -> Cmd (Reference (TestThread m) Symbolic))
-> Gen (Reference (TestThread m) Symbolic)
-> Gen (Link () -> Cmd (Reference (TestThread m) Symbolic))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (Reference (TestThread m) Symbolic)
pickThread Gen (Link () -> Cmd (Reference (TestThread m) Symbolic))
-> Gen (Link ()) -> Gen (Cmd (Reference (TestThread m) Symbolic))
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen (Link ())
genLink
        ]

    genLink :: Gen (Link ())
    genLink :: Gen (Link ())
genLink = Bool -> Link ()
aux (Bool -> Link ()) -> Gen Bool -> Gen (Link ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Bool
forall a. Arbitrary a => Gen a
QC.arbitrary
      where
        aux :: Bool -> Link ()
        aux :: Bool -> Link ()
aux Bool
True  = () -> Link ()
forall a. a -> Link a
LinkFromParent ()
        aux Bool
False = Link ()
forall a. Link a
DontLink

shrinker :: Model m Symbolic -> At m Cmd Symbolic -> [At m Cmd Symbolic]
shrinker :: forall (m :: * -> *).
Model m Symbolic -> At m Cmd Symbolic -> [At m Cmd Symbolic]
shrinker Model m Symbolic
_ At m Cmd Symbolic
_ = []

{-------------------------------------------------------------------------------
  QSM required instances
-------------------------------------------------------------------------------}

instance SOP.Generic         (Cmd t)
instance SOP.HasDatatypeInfo (Cmd t)

deriving instance Generic1 (At m Cmd)
deriving instance Generic1 (At m Resp)

instance CommandNames (At m Cmd) where
  cmdName :: forall (r :: * -> *). At m Cmd r -> TestName
cmdName  (At Cmd (Reference (TestThread m) r)
cmd) = Cmd (Reference (TestThread m) r) -> TestName
forall a. HasDatatypeInfo a => a -> TestName
constrName Cmd (Reference (TestThread m) r)
cmd
  cmdNames :: forall (r :: * -> *). Proxy (At m Cmd r) -> [TestName]
cmdNames Proxy (At m Cmd r)
_        = Proxy (Cmd ()) -> [TestName]
forall a (proxy :: * -> *).
HasDatatypeInfo a =>
proxy a -> [TestName]
constrNames (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @(Cmd ()))

instance Rank2.Foldable    (At m Cmd)
instance Rank2.Functor     (At m Cmd)
instance Rank2.Traversable (At m Cmd)

instance Rank2.Foldable (At m Resp)

instance ToExpr MockState
instance ToExpr MockThreads
instance ToExpr Mock
instance ToExpr (Link MockThread)
instance ToExpr (Model IO Concrete)

instance (IOLike m) => ToExpr (TestThread m) where
  toExpr :: TestThread m -> Expr
toExpr = TestThread m -> Expr
forall a. Show a => a -> Expr
defaultExprViaShow

{-------------------------------------------------------------------------------
  QSM toplevel
-------------------------------------------------------------------------------}

semantics :: (IOLike m, MonadTimer m, Typeable m)
          => StrictTVar m [TestThread m]
          -> ResourceRegistry m
          -> At m Cmd Concrete -> m (At m Resp Concrete)
semantics :: forall (m :: * -> *).
(IOLike m, MonadTimer m, Typeable m) =>
StrictTVar m [TestThread m]
-> ResourceRegistry m
-> At m Cmd Concrete
-> m (At m Resp Concrete)
semantics StrictTVar m [TestThread m]
alive ResourceRegistry m
reg (At Cmd (Reference (TestThread m) Concrete)
c) =
    (Resp (Reference (TestThread m) Concrete) -> At m Resp Concrete
forall (m :: * -> *) (f :: * -> *) (r :: * -> *).
f (Reference (TestThread m) r) -> At m f r
At (Resp (Reference (TestThread m) Concrete) -> At m Resp Concrete)
-> (Resp (TestThread m)
    -> Resp (Reference (TestThread m) Concrete))
-> Resp (TestThread m)
-> At m Resp Concrete
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TestThread m -> Reference (TestThread m) Concrete)
-> Resp (TestThread m) -> Resp (Reference (TestThread m) Concrete)
forall a b. (a -> b) -> Resp a -> Resp b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TestThread m -> Reference (TestThread m) Concrete
forall a. Typeable a => a -> Reference a Concrete
reference) (Resp (TestThread m) -> At m Resp Concrete)
-> m (Resp (TestThread m)) -> m (At m Resp Concrete)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
      StrictTVar m [TestThread m]
-> ResourceRegistry m
-> Cmd (TestThread m)
-> m (Resp (TestThread m))
forall (m :: * -> *).
(IOLike m, MonadTimer m) =>
StrictTVar m [TestThread m]
-> ResourceRegistry m
-> Cmd (TestThread m)
-> m (Resp (TestThread m))
runIO StrictTVar m [TestThread m]
alive ResourceRegistry m
reg (Reference (TestThread m) Concrete -> TestThread m
forall a. Reference a Concrete -> a
concrete (Reference (TestThread m) Concrete -> TestThread m)
-> Cmd (Reference (TestThread m) Concrete) -> Cmd (TestThread m)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Cmd (Reference (TestThread m) Concrete)
c)

transition :: (Eq1 r, Show1 r, IOLike m)
           => Model m r -> At m Cmd r -> At m Resp r -> Model m r
transition :: forall (r :: * -> *) (m :: * -> *).
(Eq1 r, Show1 r, IOLike m) =>
Model m r -> At m Cmd r -> At m Resp r -> Model m r
transition Model m r
m At m Cmd r
c = Event m r -> Model m r
forall (m :: * -> *) (r :: * -> *). Event m r -> Model m r
after (Event m r -> Model m r)
-> (At m Resp r -> Event m r) -> At m Resp r -> Model m r
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Model m r -> At m Cmd r -> At m Resp r -> Event m r
forall (r :: * -> *) (m :: * -> *).
(Eq1 r, Show1 r, IOLike m) =>
Model m r -> At m Cmd r -> At m Resp r -> Event m r
lockstep Model m r
m At m Cmd r
c

precondition :: forall m. (IOLike m)
             => Model m Symbolic -> At m Cmd Symbolic -> Logic
precondition :: forall (m :: * -> *).
IOLike m =>
Model m Symbolic -> At m Cmd Symbolic -> Logic
precondition (Model Mock
mock Refs m Symbolic
hs) (At Cmd (Reference (TestThread m) Symbolic)
c) =
    [Reference (TestThread m) Symbolic]
-> (Reference (TestThread m) Symbolic -> Logic) -> Logic
forall a. Show a => [a] -> (a -> Logic) -> Logic
forAll (Cmd (Reference (TestThread m) Symbolic)
-> [Reference (TestThread m) Symbolic]
forall a. Cmd a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Cmd (Reference (TestThread m) Symbolic)
c) Reference (TestThread m) Symbolic -> Logic
checkRef
  where
    checkRef :: Reference (TestThread m) Symbolic -> Logic
    checkRef :: Reference (TestThread m) Symbolic -> Logic
checkRef Reference (TestThread m) Symbolic
r =
        case Reference (TestThread m) Symbolic
-> Refs m Symbolic -> Maybe MockThread
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Reference (TestThread m) Symbolic
r Refs m Symbolic
hs of
          Maybe MockThread
Nothing -> Logic
Bot
          Just MockThread
r' -> MockThread
r' MockThread -> [MockThread] -> Logic
forall (t :: * -> *) a.
(Foldable t, Eq a, Show a, Show (t a)) =>
a -> t a -> Logic
`member` MockThreads -> [MockThread]
mockLiveThreads (Mock -> MockThreads
threads Mock
mock)

postcondition :: (IOLike m)
              => Model m      Concrete
              -> At    m Cmd  Concrete
              -> At    m Resp Concrete
              -> Logic
postcondition :: forall (m :: * -> *).
IOLike m =>
Model m Concrete
-> At m Cmd Concrete -> At m Resp Concrete -> Logic
postcondition Model m Concrete
m At m Cmd Concrete
c At m Resp Concrete
r =
    Resp MockThread -> Resp MockThread
normalize (Model m Concrete -> At m Resp Concrete -> Resp MockThread
forall (m :: * -> *) (f :: * -> *) (r :: * -> *).
(Functor f, Eq1 r, Show1 r, IOLike m) =>
Model m r -> At m f r -> f MockThread
toMock (Event m Concrete -> Model m Concrete
forall (m :: * -> *) (r :: * -> *). Event m r -> Model m r
after Event m Concrete
e) At m Resp Concrete
r) Resp MockThread -> Resp MockThread -> Logic
forall a. (Eq a, Show a) => a -> a -> Logic
.== Resp MockThread -> Resp MockThread
normalize (Event m Concrete -> Resp MockThread
forall (m :: * -> *) (r :: * -> *). Event m r -> Resp MockThread
mockResp Event m Concrete
e)
  where
    e :: Event m Concrete
e = Model m Concrete
-> At m Cmd Concrete -> At m Resp Concrete -> Event m Concrete
forall (r :: * -> *) (m :: * -> *).
(Eq1 r, Show1 r, IOLike m) =>
Model m r -> At m Cmd r -> At m Resp r -> Event m r
lockstep Model m Concrete
m At m Cmd Concrete
c At m Resp Concrete
r

symbolicResp :: (IOLike m, Typeable m)
             => Model m     Symbolic
             -> At    m Cmd Symbolic
             -> GenSym (At m Resp Symbolic)
symbolicResp :: forall (m :: * -> *).
(IOLike m, Typeable m) =>
Model m Symbolic
-> At m Cmd Symbolic -> GenSym (At m Resp Symbolic)
symbolicResp Model m Symbolic
m At m Cmd Symbolic
c = Resp (Reference (TestThread m) Symbolic) -> At m Resp Symbolic
forall (m :: * -> *) (f :: * -> *) (r :: * -> *).
f (Reference (TestThread m) r) -> At m f r
At (Resp (Reference (TestThread m) Symbolic) -> At m Resp Symbolic)
-> GenSym (Resp (Reference (TestThread m) Symbolic))
-> GenSym (At m Resp Symbolic)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (MockThread -> GenSym (Reference (TestThread m) Symbolic))
-> Resp MockThread
-> GenSym (Resp (Reference (TestThread m) Symbolic))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Resp a -> f (Resp b)
traverse (GenSym (Reference (TestThread m) Symbolic)
-> MockThread -> GenSym (Reference (TestThread m) Symbolic)
forall a b. a -> b -> a
const GenSym (Reference (TestThread m) Symbolic)
forall a. Typeable a => GenSym (Reference a Symbolic)
genSym) Resp MockThread
resp
  where
    (Resp MockThread
resp, Mock
_mock') = Model m Symbolic -> At m Cmd Symbolic -> (Resp MockThread, Mock)
forall (r :: * -> *) (m :: * -> *).
(Eq1 r, Show1 r, IOLike m) =>
Model m r -> At m Cmd r -> (Resp MockThread, Mock)
step Model m Symbolic
m At m Cmd Symbolic
c

sm :: (IOLike m, MonadTimer m, Typeable m)
   => StrictTVar m [TestThread m]
   -> ResourceRegistry m
   -> StateMachine (Model m) (At m Cmd) m (At m Resp)
sm :: forall (m :: * -> *).
(IOLike m, MonadTimer m, Typeable m) =>
StrictTVar m [TestThread m]
-> ResourceRegistry m
-> StateMachine (Model m) (At m Cmd) m (At m Resp)
sm StrictTVar m [TestThread m]
alive ResourceRegistry m
reg = StateMachine {
      initModel :: forall (r :: * -> *). Model m r
initModel     = Model m r
forall (r :: * -> *). Model m r
forall (m :: * -> *) (r :: * -> *). Model m r
initModel
    , transition :: forall (r :: * -> *).
(Show1 r, Ord1 r) =>
Model m r -> At m Cmd r -> At m Resp r -> Model m r
transition    = Model m r -> At m Cmd r -> At m Resp r -> Model m r
forall (r :: * -> *).
(Show1 r, Ord1 r) =>
Model m r -> At m Cmd r -> At m Resp r -> Model m r
forall (r :: * -> *) (m :: * -> *).
(Eq1 r, Show1 r, IOLike m) =>
Model m r -> At m Cmd r -> At m Resp r -> Model m r
transition
    , precondition :: Model m Symbolic -> At m Cmd Symbolic -> Logic
precondition  = Model m Symbolic -> At m Cmd Symbolic -> Logic
forall (m :: * -> *).
IOLike m =>
Model m Symbolic -> At m Cmd Symbolic -> Logic
precondition
    , postcondition :: Model m Concrete
-> At m Cmd Concrete -> At m Resp Concrete -> Logic
postcondition = Model m Concrete
-> At m Cmd Concrete -> At m Resp Concrete -> Logic
forall (m :: * -> *).
IOLike m =>
Model m Concrete
-> At m Cmd Concrete -> At m Resp Concrete -> Logic
postcondition
    , invariant :: Maybe (Model m Concrete -> Logic)
invariant     = Maybe (Model m Concrete -> Logic)
forall a. Maybe a
Nothing
    , generator :: Model m Symbolic -> Maybe (Gen (At m Cmd Symbolic))
generator     = Model m Symbolic -> Maybe (Gen (At m Cmd Symbolic))
forall (m :: * -> *).
Model m Symbolic -> Maybe (Gen (At m Cmd Symbolic))
generator
    , shrinker :: Model m Symbolic -> At m Cmd Symbolic -> [At m Cmd Symbolic]
shrinker      = Model m Symbolic -> At m Cmd Symbolic -> [At m Cmd Symbolic]
forall (m :: * -> *).
Model m Symbolic -> At m Cmd Symbolic -> [At m Cmd Symbolic]
shrinker
    , semantics :: At m Cmd Concrete -> m (At m Resp Concrete)
semantics     = StrictTVar m [TestThread m]
-> ResourceRegistry m
-> At m Cmd Concrete
-> m (At m Resp Concrete)
forall (m :: * -> *).
(IOLike m, MonadTimer m, Typeable m) =>
StrictTVar m [TestThread m]
-> ResourceRegistry m
-> At m Cmd Concrete
-> m (At m Resp Concrete)
semantics StrictTVar m [TestThread m]
alive ResourceRegistry m
reg
    , mock :: Model m Symbolic
-> At m Cmd Symbolic -> GenSym (At m Resp Symbolic)
mock          = Model m Symbolic
-> At m Cmd Symbolic -> GenSym (At m Resp Symbolic)
forall (m :: * -> *).
(IOLike m, Typeable m) =>
Model m Symbolic
-> At m Cmd Symbolic -> GenSym (At m Resp Symbolic)
symbolicResp
    , cleanup :: Model m Concrete -> m ()
cleanup       = Model m Concrete -> m ()
forall (m :: * -> *) (model :: (* -> *) -> *).
Monad m =>
model Concrete -> m ()
noCleanup
    }

prop_sequential :: QC.Property
prop_sequential :: Property
prop_sequential = StateMachine (Model IO) (At IO Cmd) IO (At IO Resp)
-> Maybe Int
-> (Commands (At IO Cmd) (At IO Resp) -> Property)
-> Property
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 -> (Commands cmd resp -> prop) -> Property
forAllCommands (StrictTVar IO [TestThread IO]
-> ResourceRegistry IO
-> StateMachine (Model IO) (At IO Cmd) IO (At IO Resp)
forall (m :: * -> *).
(IOLike m, MonadTimer m, Typeable m) =>
StrictTVar m [TestThread m]
-> ResourceRegistry m
-> StateMachine (Model m) (At m Cmd) m (At m Resp)
sm StrictTVar IO [TestThread IO]
forall a. a
unused ResourceRegistry IO
forall a. a
unused) Maybe Int
forall a. Maybe a
Nothing Commands (At IO Cmd) (At IO Resp) -> Property
prop_sequential'

prop_sequential' :: QSM.Commands (At IO Cmd) (At IO Resp) -> QC.Property
prop_sequential' :: Commands (At IO Cmd) (At IO Resp) -> Property
prop_sequential' Commands (At IO Cmd) (At IO Resp)
cmds = PropertyM IO () -> Property
forall a. Testable a => PropertyM IO a -> Property
QC.monadicIO (PropertyM IO () -> Property) -> PropertyM IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
    StrictTVar IO [TestThread IO]
alive <- IO (StrictTVar IO [TestThread IO])
-> PropertyM IO (StrictTVar IO [TestThread IO])
forall a. IO a -> PropertyM IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (StrictTVar IO [TestThread IO])
 -> PropertyM IO (StrictTVar IO [TestThread IO]))
-> IO (StrictTVar IO [TestThread IO])
-> PropertyM IO (StrictTVar IO [TestThread IO])
forall a b. (a -> b) -> a -> b
$ [TestThread IO] -> IO (StrictTVar IO [TestThread IO])
forall (m :: * -> *) a. MonadSTM m => a -> m (StrictTVar m a)
uncheckedNewTVarM []
    ResourceRegistry IO
reg   <- IO (ResourceRegistry IO) -> PropertyM IO (ResourceRegistry IO)
forall a. IO a -> PropertyM IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO (ResourceRegistry IO) -> PropertyM IO (ResourceRegistry IO))
-> IO (ResourceRegistry IO) -> PropertyM IO (ResourceRegistry IO)
forall a b. (a -> b) -> a -> b
$ IO (ResourceRegistry IO)
forall (m :: * -> *).
(IOLike m, HasCallStack) =>
m (ResourceRegistry m)
unsafeNewRegistry
    let sm' :: StateMachine (Model IO) (At IO Cmd) IO (At IO Resp)
sm' = StrictTVar IO [TestThread IO]
-> ResourceRegistry IO
-> StateMachine (Model IO) (At IO Cmd) IO (At IO Resp)
forall (m :: * -> *).
(IOLike m, MonadTimer m, Typeable m) =>
StrictTVar m [TestThread m]
-> ResourceRegistry m
-> StateMachine (Model m) (At m Cmd) m (At m Resp)
sm StrictTVar IO [TestThread IO]
alive ResourceRegistry IO
reg
    (History (At IO Cmd) (At IO Resp)
hist, Model IO Concrete
_model, Reason
res) <- StateMachine (Model IO) (At IO Cmd) IO (At IO Resp)
-> Commands (At IO Cmd) (At IO Resp)
-> PropertyM
     IO (History (At IO Cmd) (At IO Resp), Model IO Concrete, Reason)
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
       (model :: (* -> *) -> *).
(Show (cmd Concrete), Show (resp Concrete), Traversable cmd,
 Foldable resp, MonadMask m, MonadIO m) =>
StateMachine model cmd m resp
-> Commands cmd resp
-> PropertyM m (History cmd resp, model Concrete, Reason)
runCommands StateMachine (Model IO) (At IO Cmd) IO (At IO Resp)
sm' Commands (At IO Cmd) (At IO Resp)
cmds
    StateMachine (Model IO) (At IO Cmd) IO (At IO Resp)
-> History (At IO Cmd) (At IO Resp) -> Property -> PropertyM IO ()
forall (m :: * -> *) (model :: (* -> *) -> *)
       (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
(MonadIO m, CanDiff (model Concrete), Show (cmd Concrete),
 Show (resp Concrete)) =>
StateMachine model cmd m resp
-> History cmd resp -> Property -> PropertyM m ()
prettyCommands StateMachine (Model IO) (At IO Cmd) IO (At IO Resp)
sm' History (At IO Cmd) (At IO Resp)
hist
      (Property -> PropertyM IO ()) -> Property -> PropertyM IO ()
forall a b. (a -> b) -> a -> b
$ Commands (At IO Cmd) (At IO Resp) -> Property -> Property
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
CommandNames cmd =>
Commands cmd resp -> Property -> Property
checkCommandNames Commands (At IO Cmd) (At IO Resp)
cmds
      (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ Reason
res Reason -> Reason -> Property
forall a. (Eq a, Show a) => a -> a -> Property
QC.=== Reason
Ok

unused :: a
unused :: forall a. a
unused = TestName -> a
forall a. HasCallStack => TestName -> a
error TestName
"not used during command generation"

{-------------------------------------------------------------------------------
  For running things from ghci
-------------------------------------------------------------------------------}

_forkCount :: QSM.Commands (At IO Cmd) (At IO Resp)
_forkCount :: Commands (At IO Cmd) (At IO Resp)
_forkCount = StateMachine (Model IO) (At IO Cmd) IO (At IO Resp)
-> Example (At IO Cmd) () -> Commands (At IO Cmd) (At IO Resp)
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
(Foldable resp, Show (cmd Symbolic)) =>
StateMachine model cmd m resp
-> Example cmd () -> Commands cmd resp
example (StrictTVar IO [TestThread IO]
-> ResourceRegistry IO
-> StateMachine (Model IO) (At IO Cmd) IO (At IO Resp)
forall (m :: * -> *).
(IOLike m, MonadTimer m, Typeable m) =>
StrictTVar m [TestThread m]
-> ResourceRegistry m
-> StateMachine (Model m) (At m Cmd) m (At m Resp)
sm StrictTVar IO [TestThread IO]
forall a. a
unused ResourceRegistry IO
forall a. a
unused) (Example (At IO Cmd) () -> Commands (At IO Cmd) (At IO Resp))
-> Example (At IO Cmd) () -> Commands (At IO Cmd) (At IO Resp)
forall a b. (a -> b) -> a -> b
$ do
    At IO Cmd Symbolic -> Example (At IO Cmd) ()
forall (cmd :: (* -> *) -> *). cmd Symbolic -> Example cmd ()
run' (At IO Cmd Symbolic -> Example (At IO Cmd) ())
-> At IO Cmd Symbolic -> Example (At IO Cmd) ()
forall a b. (a -> b) -> a -> b
$ Cmd (Reference (TestThread IO) Symbolic) -> At IO Cmd Symbolic
forall (m :: * -> *) (f :: * -> *) (r :: * -> *).
f (Reference (TestThread m) r) -> At m f r
At (Cmd (Reference (TestThread IO) Symbolic) -> At IO Cmd Symbolic)
-> Cmd (Reference (TestThread IO) Symbolic) -> At IO Cmd Symbolic
forall a b. (a -> b) -> a -> b
$ Cmd (Reference (TestThread IO) Symbolic)
forall t. Cmd t
Fork
    At IO Cmd Symbolic -> Example (At IO Cmd) ()
forall (cmd :: (* -> *) -> *). cmd Symbolic -> Example cmd ()
run' (At IO Cmd Symbolic -> Example (At IO Cmd) ())
-> At IO Cmd Symbolic -> Example (At IO Cmd) ()
forall a b. (a -> b) -> a -> b
$ Cmd (Reference (TestThread IO) Symbolic) -> At IO Cmd Symbolic
forall (m :: * -> *) (f :: * -> *) (r :: * -> *).
f (Reference (TestThread m) r) -> At m f r
At (Cmd (Reference (TestThread IO) Symbolic) -> At IO Cmd Symbolic)
-> Cmd (Reference (TestThread IO) Symbolic) -> At IO Cmd Symbolic
forall a b. (a -> b) -> a -> b
$ Cmd (Reference (TestThread IO) Symbolic)
forall t. Cmd t
LiveThreads

_forkKillCount :: QSM.Commands (At IO Cmd) (At IO Resp)
_forkKillCount :: Commands (At IO Cmd) (At IO Resp)
_forkKillCount = StateMachine (Model IO) (At IO Cmd) IO (At IO Resp)
-> Example (At IO Cmd) () -> Commands (At IO Cmd) (At IO Resp)
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
(Foldable resp, Show (cmd Symbolic)) =>
StateMachine model cmd m resp
-> Example cmd () -> Commands cmd resp
example (StrictTVar IO [TestThread IO]
-> ResourceRegistry IO
-> StateMachine (Model IO) (At IO Cmd) IO (At IO Resp)
forall (m :: * -> *).
(IOLike m, MonadTimer m, Typeable m) =>
StrictTVar m [TestThread m]
-> ResourceRegistry m
-> StateMachine (Model m) (At m Cmd) m (At m Resp)
sm StrictTVar IO [TestThread IO]
forall a. a
unused ResourceRegistry IO
forall a. a
unused) (Example (At IO Cmd) () -> Commands (At IO Cmd) (At IO Resp))
-> Example (At IO Cmd) () -> Commands (At IO Cmd) (At IO Resp)
forall a b. (a -> b) -> a -> b
$ do
    [Reference (TestThread IO) Symbolic
t] <- At IO Cmd Symbolic
-> Example (At IO Cmd) [Reference (TestThread IO) Symbolic]
forall a (cmd :: (* -> *) -> *).
Typeable a =>
cmd Symbolic -> Example cmd [Reference a Symbolic]
run (At IO Cmd Symbolic
 -> Example (At IO Cmd) [Reference (TestThread IO) Symbolic])
-> At IO Cmd Symbolic
-> Example (At IO Cmd) [Reference (TestThread IO) Symbolic]
forall a b. (a -> b) -> a -> b
$ Cmd (Reference (TestThread IO) Symbolic) -> At IO Cmd Symbolic
forall (m :: * -> *) (f :: * -> *) (r :: * -> *).
f (Reference (TestThread m) r) -> At m f r
At (Cmd (Reference (TestThread IO) Symbolic) -> At IO Cmd Symbolic)
-> Cmd (Reference (TestThread IO) Symbolic) -> At IO Cmd Symbolic
forall a b. (a -> b) -> a -> b
$ Cmd (Reference (TestThread IO) Symbolic)
forall t. Cmd t
Fork
    At IO Cmd Symbolic -> Example (At IO Cmd) ()
forall (cmd :: (* -> *) -> *). cmd Symbolic -> Example cmd ()
run' (At IO Cmd Symbolic -> Example (At IO Cmd) ())
-> At IO Cmd Symbolic -> Example (At IO Cmd) ()
forall a b. (a -> b) -> a -> b
$ Cmd (Reference (TestThread IO) Symbolic) -> At IO Cmd Symbolic
forall (m :: * -> *) (f :: * -> *) (r :: * -> *).
f (Reference (TestThread m) r) -> At m f r
At (Cmd (Reference (TestThread IO) Symbolic) -> At IO Cmd Symbolic)
-> Cmd (Reference (TestThread IO) Symbolic) -> At IO Cmd Symbolic
forall a b. (a -> b) -> a -> b
$ Reference (TestThread IO) Symbolic
-> Cmd (Reference (TestThread IO) Symbolic)
forall t. t -> Cmd t
Terminate Reference (TestThread IO) Symbolic
t
    At IO Cmd Symbolic -> Example (At IO Cmd) ()
forall (cmd :: (* -> *) -> *). cmd Symbolic -> Example cmd ()
run' (At IO Cmd Symbolic -> Example (At IO Cmd) ())
-> At IO Cmd Symbolic -> Example (At IO Cmd) ()
forall a b. (a -> b) -> a -> b
$ Cmd (Reference (TestThread IO) Symbolic) -> At IO Cmd Symbolic
forall (m :: * -> *) (f :: * -> *) (r :: * -> *).
f (Reference (TestThread m) r) -> At m f r
At (Cmd (Reference (TestThread IO) Symbolic) -> At IO Cmd Symbolic)
-> Cmd (Reference (TestThread IO) Symbolic) -> At IO Cmd Symbolic
forall a b. (a -> b) -> a -> b
$ Cmd (Reference (TestThread IO) Symbolic)
forall t. Cmd t
LiveThreads

_forkFromKillCount :: QSM.Commands (At IO Cmd) (At IO Resp)
_forkFromKillCount :: Commands (At IO Cmd) (At IO Resp)
_forkFromKillCount = StateMachine (Model IO) (At IO Cmd) IO (At IO Resp)
-> Example (At IO Cmd) () -> Commands (At IO Cmd) (At IO Resp)
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
(Foldable resp, Show (cmd Symbolic)) =>
StateMachine model cmd m resp
-> Example cmd () -> Commands cmd resp
example (StrictTVar IO [TestThread IO]
-> ResourceRegistry IO
-> StateMachine (Model IO) (At IO Cmd) IO (At IO Resp)
forall (m :: * -> *).
(IOLike m, MonadTimer m, Typeable m) =>
StrictTVar m [TestThread m]
-> ResourceRegistry m
-> StateMachine (Model m) (At m Cmd) m (At m Resp)
sm StrictTVar IO [TestThread IO]
forall a. a
unused ResourceRegistry IO
forall a. a
unused) (Example (At IO Cmd) () -> Commands (At IO Cmd) (At IO Resp))
-> Example (At IO Cmd) () -> Commands (At IO Cmd) (At IO Resp)
forall a b. (a -> b) -> a -> b
$ do
    [Reference (TestThread IO) Symbolic
t] <- At IO Cmd Symbolic
-> Example (At IO Cmd) [Reference (TestThread IO) Symbolic]
forall a (cmd :: (* -> *) -> *).
Typeable a =>
cmd Symbolic -> Example cmd [Reference a Symbolic]
run (At IO Cmd Symbolic
 -> Example (At IO Cmd) [Reference (TestThread IO) Symbolic])
-> At IO Cmd Symbolic
-> Example (At IO Cmd) [Reference (TestThread IO) Symbolic]
forall a b. (a -> b) -> a -> b
$ Cmd (Reference (TestThread IO) Symbolic) -> At IO Cmd Symbolic
forall (m :: * -> *) (f :: * -> *) (r :: * -> *).
f (Reference (TestThread m) r) -> At m f r
At (Cmd (Reference (TestThread IO) Symbolic) -> At IO Cmd Symbolic)
-> Cmd (Reference (TestThread IO) Symbolic) -> At IO Cmd Symbolic
forall a b. (a -> b) -> a -> b
$ Cmd (Reference (TestThread IO) Symbolic)
forall t. Cmd t
Fork
    At IO Cmd Symbolic -> Example (At IO Cmd) ()
forall (cmd :: (* -> *) -> *). cmd Symbolic -> Example cmd ()
run' (At IO Cmd Symbolic -> Example (At IO Cmd) ())
-> At IO Cmd Symbolic -> Example (At IO Cmd) ()
forall a b. (a -> b) -> a -> b
$ Cmd (Reference (TestThread IO) Symbolic) -> At IO Cmd Symbolic
forall (m :: * -> *) (f :: * -> *) (r :: * -> *).
f (Reference (TestThread m) r) -> At m f r
At (Cmd (Reference (TestThread IO) Symbolic) -> At IO Cmd Symbolic)
-> Cmd (Reference (TestThread IO) Symbolic) -> At IO Cmd Symbolic
forall a b. (a -> b) -> a -> b
$ Reference (TestThread IO) Symbolic
-> Link () -> Cmd (Reference (TestThread IO) Symbolic)
forall t. t -> Link () -> Cmd t
ForkFrom Reference (TestThread IO) Symbolic
t Link ()
forall a. Link a
DontLink
    At IO Cmd Symbolic -> Example (At IO Cmd) ()
forall (cmd :: (* -> *) -> *). cmd Symbolic -> Example cmd ()
run' (At IO Cmd Symbolic -> Example (At IO Cmd) ())
-> At IO Cmd Symbolic -> Example (At IO Cmd) ()
forall a b. (a -> b) -> a -> b
$ Cmd (Reference (TestThread IO) Symbolic) -> At IO Cmd Symbolic
forall (m :: * -> *) (f :: * -> *) (r :: * -> *).
f (Reference (TestThread m) r) -> At m f r
At (Cmd (Reference (TestThread IO) Symbolic) -> At IO Cmd Symbolic)
-> Cmd (Reference (TestThread IO) Symbolic) -> At IO Cmd Symbolic
forall a b. (a -> b) -> a -> b
$ Reference (TestThread IO) Symbolic
-> Cmd (Reference (TestThread IO) Symbolic)
forall t. t -> Cmd t
Terminate Reference (TestThread IO) Symbolic
t
    At IO Cmd Symbolic -> Example (At IO Cmd) ()
forall (cmd :: (* -> *) -> *). cmd Symbolic -> Example cmd ()
run' (At IO Cmd Symbolic -> Example (At IO Cmd) ())
-> At IO Cmd Symbolic -> Example (At IO Cmd) ()
forall a b. (a -> b) -> a -> b
$ Cmd (Reference (TestThread IO) Symbolic) -> At IO Cmd Symbolic
forall (m :: * -> *) (f :: * -> *) (r :: * -> *).
f (Reference (TestThread m) r) -> At m f r
At (Cmd (Reference (TestThread IO) Symbolic) -> At IO Cmd Symbolic)
-> Cmd (Reference (TestThread IO) Symbolic) -> At IO Cmd Symbolic
forall a b. (a -> b) -> a -> b
$ Cmd (Reference (TestThread IO) Symbolic)
forall t. Cmd t
LiveThreads

_invalidForkFrom :: QSM.Commands (At IO Cmd) (At IO Resp)
_invalidForkFrom :: Commands (At IO Cmd) (At IO Resp)
_invalidForkFrom = StateMachine (Model IO) (At IO Cmd) IO (At IO Resp)
-> Example (At IO Cmd) () -> Commands (At IO Cmd) (At IO Resp)
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
       (m :: * -> *) (resp :: (* -> *) -> *).
(Foldable resp, Show (cmd Symbolic)) =>
StateMachine model cmd m resp
-> Example cmd () -> Commands cmd resp
example (StrictTVar IO [TestThread IO]
-> ResourceRegistry IO
-> StateMachine (Model IO) (At IO Cmd) IO (At IO Resp)
forall (m :: * -> *).
(IOLike m, MonadTimer m, Typeable m) =>
StrictTVar m [TestThread m]
-> ResourceRegistry m
-> StateMachine (Model m) (At m Cmd) m (At m Resp)
sm StrictTVar IO [TestThread IO]
forall a. a
unused ResourceRegistry IO
forall a. a
unused) (Example (At IO Cmd) () -> Commands (At IO Cmd) (At IO Resp))
-> Example (At IO Cmd) () -> Commands (At IO Cmd) (At IO Resp)
forall a b. (a -> b) -> a -> b
$ do
    [Reference (TestThread IO) Symbolic
t] <- At IO Cmd Symbolic
-> Example (At IO Cmd) [Reference (TestThread IO) Symbolic]
forall a (cmd :: (* -> *) -> *).
Typeable a =>
cmd Symbolic -> Example cmd [Reference a Symbolic]
run (At IO Cmd Symbolic
 -> Example (At IO Cmd) [Reference (TestThread IO) Symbolic])
-> At IO Cmd Symbolic
-> Example (At IO Cmd) [Reference (TestThread IO) Symbolic]
forall a b. (a -> b) -> a -> b
$ Cmd (Reference (TestThread IO) Symbolic) -> At IO Cmd Symbolic
forall (m :: * -> *) (f :: * -> *) (r :: * -> *).
f (Reference (TestThread m) r) -> At m f r
At (Cmd (Reference (TestThread IO) Symbolic) -> At IO Cmd Symbolic)
-> Cmd (Reference (TestThread IO) Symbolic) -> At IO Cmd Symbolic
forall a b. (a -> b) -> a -> b
$ Cmd (Reference (TestThread IO) Symbolic)
forall t. Cmd t
Fork
    At IO Cmd Symbolic -> Example (At IO Cmd) ()
forall (cmd :: (* -> *) -> *). cmd Symbolic -> Example cmd ()
run' (At IO Cmd Symbolic -> Example (At IO Cmd) ())
-> At IO Cmd Symbolic -> Example (At IO Cmd) ()
forall a b. (a -> b) -> a -> b
$ Cmd (Reference (TestThread IO) Symbolic) -> At IO Cmd Symbolic
forall (m :: * -> *) (f :: * -> *) (r :: * -> *).
f (Reference (TestThread m) r) -> At m f r
At (Cmd (Reference (TestThread IO) Symbolic) -> At IO Cmd Symbolic)
-> Cmd (Reference (TestThread IO) Symbolic) -> At IO Cmd Symbolic
forall a b. (a -> b) -> a -> b
$ Reference (TestThread IO) Symbolic
-> Cmd (Reference (TestThread IO) Symbolic)
forall t. t -> Cmd t
Terminate Reference (TestThread IO) Symbolic
t
    At IO Cmd Symbolic -> Example (At IO Cmd) ()
forall (cmd :: (* -> *) -> *). cmd Symbolic -> Example cmd ()
run' (At IO Cmd Symbolic -> Example (At IO Cmd) ())
-> At IO Cmd Symbolic -> Example (At IO Cmd) ()
forall a b. (a -> b) -> a -> b
$ Cmd (Reference (TestThread IO) Symbolic) -> At IO Cmd Symbolic
forall (m :: * -> *) (f :: * -> *) (r :: * -> *).
f (Reference (TestThread m) r) -> At m f r
At (Cmd (Reference (TestThread IO) Symbolic) -> At IO Cmd Symbolic)
-> Cmd (Reference (TestThread IO) Symbolic) -> At IO Cmd Symbolic
forall a b. (a -> b) -> a -> b
$ Reference (TestThread IO) Symbolic
-> Link () -> Cmd (Reference (TestThread IO) Symbolic)
forall t. t -> Link () -> Cmd t
ForkFrom Reference (TestThread IO) Symbolic
t Link ()
forall a. Link a
DontLink