{-# LANGUAGE ExplicitNamespaces    #-}
{-# LANGUAGE NamedFieldPuns        #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE ScopedTypeVariables   #-}
{-# LANGUAGE TupleSections         #-}

{-# OPTIONS_GHC -Wno-name-shadowing #-}
{-# LANGUAGE QuantifiedConstraints #-}
module Control.Monad.IOSim
  ( -- * Simulation monad
    IOSim
  , STMSim
    -- ** Run simulation
  , runSim
  , runSimOrThrow
  , runSimStrictShutdown
  , Failure (..)
  , runSimTrace
  , runSimTraceST
    -- *** QuickCheck Monadic combinators
  , monadicIOSim_
  , monadicIOSim
  , runIOSimGen
    -- ** Explore races using /IOSimPOR/
    -- $iosimpor
  , exploreSimTrace
  , controlSimTrace
  , ScheduleMod (..)
  , ScheduleControl (..)
    -- *** Exploration options
  , ExplorationSpec
  , ExplorationOptions (..)
  , stdExplorationOptions
  , withScheduleBound
  , withBranching
  , withStepTimelimit
  , withReplay
    -- * Lift ST computations
  , liftST
    -- * Simulation time
  , setCurrentTime
  , unshareClock
    -- * Simulation trace
  , type SimTrace
  , Trace (Cons, Nil, SimTrace, SimPORTrace, TraceDeadlock, TraceLoop, TraceMainReturn, TraceMainException, TraceRacesFound, TraceInternalError)
  , SimResult (..)
  , SimEvent (..)
  , SimEventType (..)
  , ThreadLabel
  , IOSimThreadId (..)
  , Labelled (..)
    -- ** Dynamic Tracing
  , traceM
  , traceSTM
    -- ** Pretty printers
  , ppTrace
  , ppTrace_
  , ppEvents
  , ppSimEvent
  , ppDebug
    -- ** Selectors
  , traceEvents
  , traceResult
    -- *** list selectors
  , selectTraceEvents
  , selectTraceEvents'
  , selectTraceEventsDynamic
  , selectTraceEventsDynamicWithTime
  , selectTraceEventsDynamic'
  , selectTraceEventsDynamicWithTime'
  , selectTraceEventsSay
  , selectTraceEventsSayWithTime
  , selectTraceEventsSay'
  , selectTraceEventsSayWithTime'
  , selectTraceRaces
    -- *** trace selectors
  , traceSelectTraceEvents
  , traceSelectTraceEventsDynamic
  , traceSelectTraceEventsSay
    -- ** IO printer
  , printTraceEventsSay
    -- * Eventlog
  , EventlogEvent (..)
  , EventlogMarker (..)
    -- * Low-level API
  , Timeout
  , newTimeout
  , readTimeout
  , cancelTimeout
  , awaitTimeout
  ) where

import Prelude

import Data.Bifoldable
import Data.Dynamic (fromDynamic)
import Data.List (intercalate)
import Data.Set (Set)
import Data.Set qualified as Set
import Data.Typeable (Typeable)

import Data.List.Trace (Trace (..))

import Control.Exception (throw)

import Control.Monad.ST.Lazy

import Control.Monad.Class.MonadThrow as MonadThrow

import Control.Monad.IOSim.Internal (runSimTraceST)
import Control.Monad.IOSim.Types
import Control.Monad.IOSimPOR.Internal qualified as IOSimPOR (controlSimTraceST)
import Control.Monad.IOSimPOR.QuickCheckUtils

import Test.QuickCheck
import Test.QuickCheck.Gen.Unsafe (Capture (..), capture)
import Test.QuickCheck.Monadic (PropertyM, monadic')

import System.IO.Unsafe

import Data.Functor (void)
import Data.IORef
import Debug.Trace qualified as Debug


-- | Select events according to the predicate function.  It throws an error if
-- the simulation ends with 'Failure'.
--
selectTraceEvents
    :: (Time -> SimEventType -> Maybe b)
    -> SimTrace a
    -> [b]
selectTraceEvents :: forall b a. (Time -> SimEventType -> Maybe b) -> SimTrace a -> [b]
selectTraceEvents Time -> SimEventType -> Maybe b
fn =
      (SimResult a -> [b] -> [b])
-> (b -> [b] -> [b]) -> [b] -> Trace (SimResult a) b -> [b]
forall a c b. (a -> c -> c) -> (b -> c -> c) -> c -> Trace a b -> c
forall (p :: * -> * -> *) a c b.
Bifoldable p =>
(a -> c -> c) -> (b -> c -> c) -> c -> p a b -> c
bifoldr ( \ SimResult a
v [b]
_
               -> case SimResult a
v of
                    MainException Time
_ Labelled IOSimThreadId
_ SomeException
e [Labelled IOSimThreadId]
_     -> Failure -> [b]
forall a e. Exception e => e -> a
throw (SomeException -> Failure
FailureException SomeException
e)
                    Deadlock      Time
_   [Labelled IOSimThreadId]
threads -> Failure -> [b]
forall a e. Exception e => e -> a
throw ([Labelled IOSimThreadId] -> Failure
FailureDeadlock [Labelled IOSimThreadId]
threads)
                    MainReturn    Time
_ Labelled IOSimThreadId
_ a
_ [Labelled IOSimThreadId]
_     -> []
                    SimResult a
Loop                      -> [Char] -> [b]
forall a. HasCallStack => [Char] -> a
error [Char]
"Impossible: selectTraceEvents _ TraceLoop{}"
                    InternalError [Char]
msg         -> Failure -> [b]
forall a e. Exception e => e -> a
throw ([Char] -> Failure
FailureInternal [Char]
msg)
              )
              ( \ b
b [b]
acc -> b
b b -> [b] -> [b]
forall a. a -> [a] -> [a]
: [b]
acc )
              []
    (Trace (SimResult a) b -> [b])
-> (SimTrace a -> Trace (SimResult a) b) -> SimTrace a -> [b]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Time -> SimEventType -> Maybe b)
-> SimTrace a -> Trace (SimResult a) b
forall b a.
(Time -> SimEventType -> Maybe b) -> Trace a SimEvent -> Trace a b
traceSelectTraceEvents Time -> SimEventType -> Maybe b
fn

-- | Like 'selectTraceEvents', but it returns even if the simulation trace ends
-- with 'Failure'.
--
selectTraceEvents'
    :: (Time ->  SimEventType -> Maybe b)
    -> SimTrace a
    -> [b]
selectTraceEvents' :: forall b a. (Time -> SimEventType -> Maybe b) -> SimTrace a -> [b]
selectTraceEvents' Time -> SimEventType -> Maybe b
fn =
      (SimResult a -> [b] -> [b])
-> (b -> [b] -> [b]) -> [b] -> Trace (SimResult a) b -> [b]
forall a c b. (a -> c -> c) -> (b -> c -> c) -> c -> Trace a b -> c
forall (p :: * -> * -> *) a c b.
Bifoldable p =>
(a -> c -> c) -> (b -> c -> c) -> c -> p a b -> c
bifoldr ( \ SimResult a
_ [b]
_   -> []  )
              ( \ b
b [b]
acc -> b
b b -> [b] -> [b]
forall a. a -> [a] -> [a]
: [b]
acc )
              []
    (Trace (SimResult a) b -> [b])
-> (SimTrace a -> Trace (SimResult a) b) -> SimTrace a -> [b]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Time -> SimEventType -> Maybe b)
-> SimTrace a -> Trace (SimResult a) b
forall b a.
(Time -> SimEventType -> Maybe b) -> Trace a SimEvent -> Trace a b
traceSelectTraceEvents Time -> SimEventType -> Maybe b
fn

selectTraceRaces :: SimTrace a -> [ScheduleControl]
selectTraceRaces :: forall a. SimTrace a -> [ScheduleControl]
selectTraceRaces = SimTrace a -> [ScheduleControl]
forall a. SimTrace a -> [ScheduleControl]
go
  where
    go :: SimTrace a -> [ScheduleControl]
go (SimTrace Time
_ IOSimThreadId
_ Maybe [Char]
_ SimEventType
_ SimTrace a
trace)      = SimTrace a -> [ScheduleControl]
go SimTrace a
trace
    go (SimPORTrace Time
_ IOSimThreadId
_ Int
_ Maybe [Char]
_ SimEventType
_ SimTrace a
trace) = SimTrace a -> [ScheduleControl]
go SimTrace a
trace
    go (TraceRacesFound [ScheduleControl]
races SimTrace a
trace) =
      [ScheduleControl]
races [ScheduleControl] -> [ScheduleControl] -> [ScheduleControl]
forall a. [a] -> [a] -> [a]
++ SimTrace a -> [ScheduleControl]
go SimTrace a
trace
    go SimTrace a
_                             = []

-- Extracting races from a trace.  There is a subtlety in doing so: we
-- must return a defined list of races even in the case where the
-- trace is infinite, and there are no races occurring in it! For
-- example, if the system falls into a deterministic infinite loop,
-- then there will be no races to find.

-- In reality we only want to extract races from *the part of the
-- trace used in a test*. We can only observe that by tracking lazy
-- evaluation: only races that were found in the evaluated prefix of
-- an infinite trace should contribute to the "races found". Hence we
-- return a function that returns the races found "so far". This is
-- unsafe, of course, since that function may return different results
-- at different times.

detachTraceRaces :: forall a. Int -> SimTrace a -> (() -> [ScheduleControl], SimTrace a)
detachTraceRaces :: forall a.
Int -> SimTrace a -> (() -> [ScheduleControl], SimTrace a)
detachTraceRaces Int
debugLevel SimTrace a
trace = IO (() -> [ScheduleControl], SimTrace a)
-> (() -> [ScheduleControl], SimTrace a)
forall a. IO a -> a
unsafePerformIO (IO (() -> [ScheduleControl], SimTrace a)
 -> (() -> [ScheduleControl], SimTrace a))
-> IO (() -> [ScheduleControl], SimTrace a)
-> (() -> [ScheduleControl], SimTrace a)
forall a b. (a -> b) -> a -> b
$ do
  IORef [[ScheduleControl]]
races <- [[ScheduleControl]] -> IO (IORef [[ScheduleControl]])
forall a. a -> IO (IORef a)
newIORef []
  let readRaces :: () -> [ScheduleControl]
      readRaces :: () -> [ScheduleControl]
readRaces () = [[ScheduleControl]] -> [ScheduleControl]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[ScheduleControl]] -> [ScheduleControl])
-> (IO [[ScheduleControl]] -> [[ScheduleControl]])
-> IO [[ScheduleControl]]
-> [ScheduleControl]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[ScheduleControl]] -> [[ScheduleControl]]
forall a. [a] -> [a]
reverse ([[ScheduleControl]] -> [[ScheduleControl]])
-> (IO [[ScheduleControl]] -> [[ScheduleControl]])
-> IO [[ScheduleControl]]
-> [[ScheduleControl]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IO [[ScheduleControl]] -> [[ScheduleControl]]
forall a. IO a -> a
unsafePerformIO (IO [[ScheduleControl]] -> [ScheduleControl])
-> IO [[ScheduleControl]] -> [ScheduleControl]
forall a b. (a -> b) -> a -> b
$ IORef [[ScheduleControl]] -> IO [[ScheduleControl]]
forall a. IORef a -> IO a
readIORef IORef [[ScheduleControl]]
races

      saveRaces :: [ScheduleControl] -> x -> x
      saveRaces :: forall x. [ScheduleControl] -> x -> x
saveRaces [ScheduleControl]
rs x
t = IO x -> x
forall a. IO a -> a
unsafePerformIO (IO x -> x) -> IO x -> x
forall a b. (a -> b) -> a -> b
$ IORef [[ScheduleControl]]
-> ([[ScheduleControl]] -> [[ScheduleControl]]) -> IO ()
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef IORef [[ScheduleControl]]
races ([ScheduleControl]
rs[ScheduleControl] -> [[ScheduleControl]] -> [[ScheduleControl]]
forall a. a -> [a] -> [a]
:)
                                      IO () -> IO x -> IO x
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> x -> IO x
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return x
t

      go :: SimTrace a -> SimTrace a
      go :: SimTrace a -> SimTrace a
go (SimTrace Time
a IOSimThreadId
b Maybe [Char]
c SimEventType
d SimTrace a
trace)      = Int -> Either SimEvent (SimResult a) -> SimTrace a -> SimTrace a
forall a.
Int -> Either SimEvent (SimResult a) -> SimTrace a -> SimTrace a
traceDebugLog Int
debugLevel (SimEvent -> Either SimEvent (SimResult a)
forall a b. a -> Either a b
Left (Time -> IOSimThreadId -> Maybe [Char] -> SimEventType -> SimEvent
SimEvent Time
a IOSimThreadId
b Maybe [Char]
c SimEventType
d))
                                       (SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall a b. (a -> b) -> a -> b
$ Time
-> IOSimThreadId
-> Maybe [Char]
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> IOSimThreadId
-> Maybe [Char]
-> SimEventType
-> SimTrace a
-> SimTrace a
SimTrace Time
a IOSimThreadId
b Maybe [Char]
c SimEventType
d (SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall a b. (a -> b) -> a -> b
$ SimTrace a -> SimTrace a
go SimTrace a
trace
      go (SimPORTrace Time
a IOSimThreadId
b Int
c Maybe [Char]
d SimEventType
e SimTrace a
trace) = Int -> Either SimEvent (SimResult a) -> SimTrace a -> SimTrace a
forall a.
Int -> Either SimEvent (SimResult a) -> SimTrace a -> SimTrace a
traceDebugLog Int
debugLevel (SimEvent -> Either SimEvent (SimResult a)
forall a b. a -> Either a b
Left (Time
-> IOSimThreadId -> Int -> Maybe [Char] -> SimEventType -> SimEvent
SimPOREvent Time
a IOSimThreadId
b Int
c Maybe [Char]
d SimEventType
e))
                                       (SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall a b. (a -> b) -> a -> b
$ Time
-> IOSimThreadId
-> Int
-> Maybe [Char]
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> IOSimThreadId
-> Int
-> Maybe [Char]
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
a IOSimThreadId
b Int
c Maybe [Char]
d SimEventType
e (SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall a b. (a -> b) -> a -> b
$ SimTrace a -> SimTrace a
go SimTrace a
trace
      go (TraceRacesFound [ScheduleControl]
rs SimTrace a
trace)    = Int -> Either SimEvent (SimResult a) -> SimTrace a -> SimTrace a
forall a.
Int -> Either SimEvent (SimResult a) -> SimTrace a -> SimTrace a
traceDebugLog Int
debugLevel (SimEvent -> Either SimEvent (SimResult a)
forall a b. a -> Either a b
Left ([ScheduleControl] -> SimEvent
SimRacesFound [ScheduleControl]
rs))
                                       (SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall a b. (a -> b) -> a -> b
$ [ScheduleControl] -> SimTrace a -> SimTrace a
forall x. [ScheduleControl] -> x -> x
saveRaces [ScheduleControl]
rs (SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall a b. (a -> b) -> a -> b
$ SimTrace a -> SimTrace a
go SimTrace a
trace
      go (Cons SimEvent
a SimTrace a
as)                   = Int -> Either SimEvent (SimResult a) -> SimTrace a -> SimTrace a
forall a.
Int -> Either SimEvent (SimResult a) -> SimTrace a -> SimTrace a
traceDebugLog Int
debugLevel (SimEvent -> Either SimEvent (SimResult a)
forall a b. a -> Either a b
Left SimEvent
a)
                                       (SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall a b. (a -> b) -> a -> b
$ SimEvent -> SimTrace a -> SimTrace a
forall a b. b -> Trace a b -> Trace a b
Cons SimEvent
a (SimTrace a -> SimTrace a
go SimTrace a
as)
      go (Nil SimResult a
a)                       = Int -> Either SimEvent (SimResult a) -> SimTrace a -> SimTrace a
forall a.
Int -> Either SimEvent (SimResult a) -> SimTrace a -> SimTrace a
traceDebugLog Int
debugLevel (SimResult a -> Either SimEvent (SimResult a)
forall a b. b -> Either a b
Right SimResult a
a)
                                       (SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall a b. (a -> b) -> a -> b
$ SimResult a -> SimTrace a
forall a b. a -> Trace a b
Nil SimResult a
a

  (() -> [ScheduleControl], SimTrace a)
-> IO (() -> [ScheduleControl], SimTrace a)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (() -> [ScheduleControl]
readRaces, SimTrace a -> SimTrace a
go SimTrace a
trace)

-- | Select all the traced values matching the expected type.  It relies on the
-- sim's dynamic trace facility.
--
-- For convenience, it throws exceptions for abnormal sim termination.
--
selectTraceEventsDynamic :: forall a b. Typeable b => SimTrace a -> [b]
selectTraceEventsDynamic :: forall a b. Typeable b => SimTrace a -> [b]
selectTraceEventsDynamic = (Time -> SimEventType -> Maybe b) -> SimTrace a -> [b]
forall b a. (Time -> SimEventType -> Maybe b) -> SimTrace a -> [b]
selectTraceEvents Time -> SimEventType -> Maybe b
fn
  where
    fn :: Time -> SimEventType -> Maybe b
    fn :: Time -> SimEventType -> Maybe b
fn Time
_ (EventLog Dynamic
dyn) = Dynamic -> Maybe b
forall a. Typeable a => Dynamic -> Maybe a
fromDynamic Dynamic
dyn
    fn Time
_ SimEventType
_              = Maybe b
forall a. Maybe a
Nothing

-- | Like 'selectTraceEventsDynamic' but it also captures time of the trace
-- event.
--
selectTraceEventsDynamicWithTime :: forall a b. Typeable b => SimTrace a -> [(Time, b)]
selectTraceEventsDynamicWithTime :: forall a b. Typeable b => SimTrace a -> [(Time, b)]
selectTraceEventsDynamicWithTime = (Time -> SimEventType -> Maybe (Time, b))
-> SimTrace a -> [(Time, b)]
forall b a. (Time -> SimEventType -> Maybe b) -> SimTrace a -> [b]
selectTraceEvents Time -> SimEventType -> Maybe (Time, b)
fn
  where
    fn :: Time -> SimEventType -> Maybe (Time, b)
    fn :: Time -> SimEventType -> Maybe (Time, b)
fn Time
t (EventLog Dynamic
dyn) = (Time
t,) (b -> (Time, b)) -> Maybe b -> Maybe (Time, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dynamic -> Maybe b
forall a. Typeable a => Dynamic -> Maybe a
fromDynamic Dynamic
dyn
    fn Time
_ SimEventType
_              = Maybe (Time, b)
forall a. Maybe a
Nothing

-- | Like 'selectTraceEventsDynamic' but it returns even if the simulation trace
-- ends with 'Failure'.
--
selectTraceEventsDynamic' :: forall a b. Typeable b => SimTrace a -> [b]
selectTraceEventsDynamic' :: forall a b. Typeable b => SimTrace a -> [b]
selectTraceEventsDynamic' = (Time -> SimEventType -> Maybe b) -> SimTrace a -> [b]
forall b a. (Time -> SimEventType -> Maybe b) -> SimTrace a -> [b]
selectTraceEvents' Time -> SimEventType -> Maybe b
fn
  where
    fn :: Time -> SimEventType -> Maybe b
    fn :: Time -> SimEventType -> Maybe b
fn Time
_ (EventLog Dynamic
dyn) = Dynamic -> Maybe b
forall a. Typeable a => Dynamic -> Maybe a
fromDynamic Dynamic
dyn
    fn Time
_ SimEventType
_              = Maybe b
forall a. Maybe a
Nothing

-- | Like `selectTraceEventsDynamic'` but it also captures time of the trace
-- event.
--
selectTraceEventsDynamicWithTime' :: forall a b. Typeable b => SimTrace a -> [(Time, b)]
selectTraceEventsDynamicWithTime' :: forall a b. Typeable b => SimTrace a -> [(Time, b)]
selectTraceEventsDynamicWithTime' = (Time -> SimEventType -> Maybe (Time, b))
-> SimTrace a -> [(Time, b)]
forall b a. (Time -> SimEventType -> Maybe b) -> SimTrace a -> [b]
selectTraceEvents' Time -> SimEventType -> Maybe (Time, b)
fn
  where
    fn :: Time -> SimEventType -> Maybe (Time, b)
    fn :: Time -> SimEventType -> Maybe (Time, b)
fn Time
t (EventLog Dynamic
dyn) = (Time
t,) (b -> (Time, b)) -> Maybe b -> Maybe (Time, b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Dynamic -> Maybe b
forall a. Typeable a => Dynamic -> Maybe a
fromDynamic Dynamic
dyn
    fn Time
_ SimEventType
_              = Maybe (Time, b)
forall a. Maybe a
Nothing

-- | Get a trace of 'EventSay'.
--
-- For convenience, it throws exceptions for abnormal sim termination.
--
selectTraceEventsSay :: SimTrace a -> [String]
selectTraceEventsSay :: forall a. SimTrace a -> [[Char]]
selectTraceEventsSay = (Time -> SimEventType -> Maybe [Char]) -> SimTrace a -> [[Char]]
forall b a. (Time -> SimEventType -> Maybe b) -> SimTrace a -> [b]
selectTraceEvents Time -> SimEventType -> Maybe [Char]
fn
  where
    fn :: Time -> SimEventType -> Maybe String
    fn :: Time -> SimEventType -> Maybe [Char]
fn Time
_ (EventSay [Char]
s) = [Char] -> Maybe [Char]
forall a. a -> Maybe a
Just [Char]
s
    fn Time
_ SimEventType
_            = Maybe [Char]
forall a. Maybe a
Nothing

-- | Like 'selectTraceEventsSay' but it also captures time of the trace event.
--
selectTraceEventsSayWithTime :: SimTrace a -> [(Time, String)]
selectTraceEventsSayWithTime :: forall a. SimTrace a -> [(Time, [Char])]
selectTraceEventsSayWithTime = (Time -> SimEventType -> Maybe (Time, [Char]))
-> SimTrace a -> [(Time, [Char])]
forall b a. (Time -> SimEventType -> Maybe b) -> SimTrace a -> [b]
selectTraceEvents Time -> SimEventType -> Maybe (Time, [Char])
fn
  where
    fn :: Time -> SimEventType -> Maybe (Time, String)
    fn :: Time -> SimEventType -> Maybe (Time, [Char])
fn Time
t (EventSay [Char]
s) = (Time, [Char]) -> Maybe (Time, [Char])
forall a. a -> Maybe a
Just (Time
t, [Char]
s)
    fn Time
_ SimEventType
_            = Maybe (Time, [Char])
forall a. Maybe a
Nothing

-- | Like 'selectTraceEventsSay' but it returns even if the simulation trace
-- ends with 'Failure'.
--
selectTraceEventsSay' :: SimTrace a -> [String]
selectTraceEventsSay' :: forall a. SimTrace a -> [[Char]]
selectTraceEventsSay' = (Time -> SimEventType -> Maybe [Char]) -> SimTrace a -> [[Char]]
forall b a. (Time -> SimEventType -> Maybe b) -> SimTrace a -> [b]
selectTraceEvents' Time -> SimEventType -> Maybe [Char]
fn
  where
    fn :: Time -> SimEventType -> Maybe String
    fn :: Time -> SimEventType -> Maybe [Char]
fn Time
_ (EventSay [Char]
s) = [Char] -> Maybe [Char]
forall a. a -> Maybe a
Just [Char]
s
    fn Time
_ SimEventType
_            = Maybe [Char]
forall a. Maybe a
Nothing

-- | Like `selectTraceEventsSay'` but it also captures time of the trace event.
--
selectTraceEventsSayWithTime' :: SimTrace a -> [(Time, String)]
selectTraceEventsSayWithTime' :: forall a. SimTrace a -> [(Time, [Char])]
selectTraceEventsSayWithTime' = (Time -> SimEventType -> Maybe (Time, [Char]))
-> SimTrace a -> [(Time, [Char])]
forall b a. (Time -> SimEventType -> Maybe b) -> SimTrace a -> [b]
selectTraceEvents' Time -> SimEventType -> Maybe (Time, [Char])
fn
  where
    fn :: Time -> SimEventType -> Maybe (Time, String)
    fn :: Time -> SimEventType -> Maybe (Time, [Char])
fn Time
t (EventSay [Char]
s) = (Time, [Char]) -> Maybe (Time, [Char])
forall a. a -> Maybe a
Just (Time
t, [Char]
s)
    fn Time
_ SimEventType
_            = Maybe (Time, [Char])
forall a. Maybe a
Nothing

-- | Print all 'EventSay' to the console.
--
-- For convenience, it throws exceptions for abnormal sim termination.
--
printTraceEventsSay :: SimTrace a -> IO ()
printTraceEventsSay :: forall a. SimTrace a -> IO ()
printTraceEventsSay = ([Char] -> IO ()) -> [[Char]] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ [Char] -> IO ()
forall a. Show a => a -> IO ()
print ([[Char]] -> IO ())
-> (SimTrace a -> [[Char]]) -> SimTrace a -> IO ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SimTrace a -> [[Char]]
forall a. SimTrace a -> [[Char]]
selectTraceEventsSay


-- | The most general select function.  It is a /total function/.
--
traceSelectTraceEvents
    :: (Time -> SimEventType -> Maybe b)
    -> Trace a SimEvent
    -> Trace a b
traceSelectTraceEvents :: forall b a.
(Time -> SimEventType -> Maybe b) -> Trace a SimEvent -> Trace a b
traceSelectTraceEvents Time -> SimEventType -> Maybe b
fn = (a -> Trace a b -> Trace a b)
-> (SimEvent -> Trace a b -> Trace a b)
-> Trace a b
-> Trace a SimEvent
-> Trace a b
forall a c b. (a -> c -> c) -> (b -> c -> c) -> c -> Trace a b -> c
forall (p :: * -> * -> *) a c b.
Bifoldable p =>
(a -> c -> c) -> (b -> c -> c) -> c -> p a b -> c
bifoldr ( \ a
v Trace a b
_acc -> a -> Trace a b
forall a b. a -> Trace a b
Nil a
v )
                                    ( \ SimEvent
eventCtx Trace a b
acc
                                     -> case SimEvent
eventCtx of
                                          SimRacesFound [ScheduleControl]
_ -> Trace a b
acc
                                          SimEvent{} ->
                                            case Time -> SimEventType -> Maybe b
fn (SimEvent -> Time
seTime SimEvent
eventCtx) (SimEvent -> SimEventType
seType SimEvent
eventCtx) of
                                              Maybe b
Nothing -> Trace a b
acc
                                              Just b
b  -> b -> Trace a b -> Trace a b
forall a b. b -> Trace a b -> Trace a b
Cons b
b Trace a b
acc
                                          SimPOREvent{} ->
                                            case Time -> SimEventType -> Maybe b
fn (SimEvent -> Time
seTime SimEvent
eventCtx) (SimEvent -> SimEventType
seType SimEvent
eventCtx) of
                                              Maybe b
Nothing -> Trace a b
acc
                                              Just b
b  -> b -> Trace a b -> Trace a b
forall a b. b -> Trace a b -> Trace a b
Cons b
b Trace a b
acc
                                    )
                                    Trace a b
forall a. HasCallStack => a
undefined -- it is ignored

-- | Select dynamic events.  It is a /total function/.
--
traceSelectTraceEventsDynamic :: forall a b. Typeable b
                              => Trace a SimEvent
                              -> Trace a b
traceSelectTraceEventsDynamic :: forall a b. Typeable b => Trace a SimEvent -> Trace a b
traceSelectTraceEventsDynamic = (Time -> SimEventType -> Maybe b) -> Trace a SimEvent -> Trace a b
forall b a.
(Time -> SimEventType -> Maybe b) -> Trace a SimEvent -> Trace a b
traceSelectTraceEvents Time -> SimEventType -> Maybe b
fn
  where
    fn :: Time -> SimEventType -> Maybe b
    fn :: Time -> SimEventType -> Maybe b
fn Time
_ (EventLog Dynamic
dyn) = Dynamic -> Maybe b
forall a. Typeable a => Dynamic -> Maybe a
fromDynamic Dynamic
dyn
    fn Time
_ SimEventType
_              = Maybe b
forall a. Maybe a
Nothing


-- | Select say events.  It is a /total function/.
--
traceSelectTraceEventsSay :: forall a. Trace a SimEvent -> Trace a String
traceSelectTraceEventsSay :: forall a. Trace a SimEvent -> Trace a [Char]
traceSelectTraceEventsSay = (Time -> SimEventType -> Maybe [Char])
-> Trace a SimEvent -> Trace a [Char]
forall b a.
(Time -> SimEventType -> Maybe b) -> Trace a SimEvent -> Trace a b
traceSelectTraceEvents Time -> SimEventType -> Maybe [Char]
fn
  where
    fn :: Time -> SimEventType -> Maybe String
    fn :: Time -> SimEventType -> Maybe [Char]
fn Time
_ (EventSay [Char]
s) = [Char] -> Maybe [Char]
forall a. a -> Maybe a
Just [Char]
s
    fn Time
_ SimEventType
_            = Maybe [Char]
forall a. Maybe a
Nothing

-- | Simulation terminated a failure.
--
data Failure =
       -- | The main thread terminated with an exception.
       FailureException SomeException

       -- | The threads all deadlocked.
     | FailureDeadlock ![Labelled IOSimThreadId]

       -- | The main thread terminated normally but other threads were still
       -- alive, and strict shutdown checking was requested.
       -- See 'runSimStrictShutdown'.
     | FailureSloppyShutdown [Labelled IOSimThreadId]

       -- | An exception was thrown while evaluation the trace.
       -- This could be an internal assertion failure of `io-sim` or an
       -- unhandled exception in the simulation.
     | FailureEvaluation SomeException

       -- | An internal failure of the simulator.
       --
       -- Please open an issue at
       -- <https://github.com/input-output-hk/io-sim/issues>.
     | FailureInternal String
  deriving Int -> Failure -> ShowS
[Failure] -> ShowS
Failure -> [Char]
(Int -> Failure -> ShowS)
-> (Failure -> [Char]) -> ([Failure] -> ShowS) -> Show Failure
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Failure -> ShowS
showsPrec :: Int -> Failure -> ShowS
$cshow :: Failure -> [Char]
show :: Failure -> [Char]
$cshowList :: [Failure] -> ShowS
showList :: [Failure] -> ShowS
Show

instance Exception Failure where
    displayException :: Failure -> [Char]
displayException (FailureException SomeException
err) = SomeException -> [Char]
forall e. Exception e => e -> [Char]
displayException  SomeException
err
    displayException (FailureDeadlock [Labelled IOSimThreadId]
threads) =
      [[Char]] -> [Char]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ [Char]
"<<io-sim deadlock: "
             , [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
", " (Labelled IOSimThreadId -> [Char]
forall a. Show a => a -> [Char]
show (Labelled IOSimThreadId -> [Char])
-> [Labelled IOSimThreadId] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
`map` [Labelled IOSimThreadId]
threads)
             , [Char]
">>"
             ]
    displayException (FailureSloppyShutdown [Labelled IOSimThreadId]
threads) =
      [[Char]] -> [Char]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ [Char]
"<<io-sim sloppy shutdown: "
             , [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
", " (Labelled IOSimThreadId -> [Char]
forall a. Show a => a -> [Char]
show (Labelled IOSimThreadId -> [Char])
-> [Labelled IOSimThreadId] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
`map` [Labelled IOSimThreadId]
threads)
             , [Char]
">>"
             ]
    displayException (FailureEvaluation SomeException
err) =
      [[Char]] -> [Char]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ [Char]
"<<evaluation error: "
             , SomeException -> [Char]
forall e. Exception e => e -> [Char]
displayException  SomeException
err
             , [Char]
">>"
             ]
    displayException (FailureInternal [Char]
msg) =
      [[Char]] -> [Char]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [ [Char]
"<<internal failure: "
             , [Char]
msg
             , [Char]
">>\n"
             , [Char]
"please report the issue at\n"
             , [Char]
"https://github.com/input-output-hk/io-sim/issues"
             ]


-- | 'IOSim' is a pure monad.
--
runSim :: forall a. (forall s. IOSim s a) -> Either Failure a
runSim :: forall a. (forall s. IOSim s a) -> Either Failure a
runSim forall s. IOSim s a
mainAction = Bool -> SimTrace a -> Either Failure a
forall a. Bool -> SimTrace a -> Either Failure a
traceResult Bool
False ((forall s. IOSim s a) -> SimTrace a
forall a. (forall s. IOSim s a) -> SimTrace a
runSimTrace IOSim s a
forall s. IOSim s a
mainAction)

-- | For quick experiments and tests it is often appropriate and convenient to
-- simply throw failures as exceptions.
--
runSimOrThrow :: forall a. (forall s. IOSim s a) -> a
runSimOrThrow :: forall a. (forall s. IOSim s a) -> a
runSimOrThrow forall s. IOSim s a
mainAction =
    case (forall s. IOSim s a) -> Either Failure a
forall a. (forall s. IOSim s a) -> Either Failure a
runSim IOSim s a
forall s. IOSim s a
mainAction of
      Left  Failure
e -> Failure -> a
forall a e. Exception e => e -> a
throw Failure
e
      Right a
x -> a
x

-- | Like 'runSim' but fail when the main thread terminates if there are other
-- threads still running or blocked. If one is trying to follow a strict thread
-- clean-up policy then this helps testing for that.
--
runSimStrictShutdown :: forall a. (forall s. IOSim s a) -> Either Failure a
runSimStrictShutdown :: forall a. (forall s. IOSim s a) -> Either Failure a
runSimStrictShutdown forall s. IOSim s a
mainAction = Bool -> SimTrace a -> Either Failure a
forall a. Bool -> SimTrace a -> Either Failure a
traceResult Bool
True ((forall s. IOSim s a) -> SimTrace a
forall a. (forall s. IOSim s a) -> SimTrace a
runSimTrace IOSim s a
forall s. IOSim s a
mainAction)

-- | Fold through the trace and return either 'Failure' or a simulation
-- result, i.e. the return value of the main thread.
--
traceResult :: Bool
            -- ^ if True the simulation will fail if there are any threads which
            -- didn't terminated when the main thread terminated.
            -> SimTrace a
            -- ^ simulation trace
            -> Either Failure a
traceResult :: forall a. Bool -> SimTrace a -> Either Failure a
traceResult Bool
strict = IO (Either Failure a) -> Either Failure a
forall a. IO a -> a
unsafePerformIO (IO (Either Failure a) -> Either Failure a)
-> (SimTrace a -> IO (Either Failure a))
-> SimTrace a
-> Either Failure a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SimTrace a -> IO (Either Failure a)
forall a. SimTrace a -> IO (Either Failure a)
eval
  where
    eval :: SimTrace a -> IO (Either Failure a)
    eval :: forall a. SimTrace a -> IO (Either Failure a)
eval SimTrace a
a = do
      Either SomeException (SimTrace a)
r <- IO (SimTrace a) -> IO (Either SomeException (SimTrace a))
forall e a. Exception e => IO a -> IO (Either e a)
forall (m :: * -> *) e a.
(MonadCatch m, Exception e) =>
m a -> m (Either e a)
try (SimTrace a -> IO (SimTrace a)
forall a. a -> IO a
forall (m :: * -> *) a. MonadEvaluate m => a -> m a
evaluate SimTrace a
a)
      case Either SomeException (SimTrace a)
r of
        Left SomeException
e  -> Either Failure a -> IO (Either Failure a)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Failure -> Either Failure a
forall a b. a -> Either a b
Left (SomeException -> Failure
FailureEvaluation SomeException
e))
        Right SimTrace a
_ -> SimTrace a -> IO (Either Failure a)
forall a. SimTrace a -> IO (Either Failure a)
go SimTrace a
a

    go :: SimTrace a -> IO (Either Failure a)
    go :: forall a. SimTrace a -> IO (Either Failure a)
go (SimTrace Time
_ IOSimThreadId
_ Maybe [Char]
_ SimEventType
_ SimTrace a
t)             = SimTrace a -> IO (Either Failure a)
forall a. SimTrace a -> IO (Either Failure a)
eval SimTrace a
t
    go (SimPORTrace Time
_ IOSimThreadId
_ Int
_ Maybe [Char]
_ SimEventType
_ SimTrace a
t)        = SimTrace a -> IO (Either Failure a)
forall a. SimTrace a -> IO (Either Failure a)
eval SimTrace a
t
    go (TraceRacesFound [ScheduleControl]
_ SimTrace a
t)            = SimTrace a -> IO (Either Failure a)
forall a. SimTrace a -> IO (Either Failure a)
eval SimTrace a
t
    go (TraceMainReturn Time
_ Labelled IOSimThreadId
_ a
_ tids :: [Labelled IOSimThreadId]
tids@(Labelled IOSimThreadId
_:[Labelled IOSimThreadId]
_))
                               | Bool
strict = Either Failure a -> IO (Either Failure a)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either Failure a -> IO (Either Failure a))
-> Either Failure a -> IO (Either Failure a)
forall a b. (a -> b) -> a -> b
$ Failure -> Either Failure a
forall a b. a -> Either a b
Left ([Labelled IOSimThreadId] -> Failure
FailureSloppyShutdown [Labelled IOSimThreadId]
tids)
    go (TraceMainReturn Time
_ Labelled IOSimThreadId
_ a
x [Labelled IOSimThreadId]
_)        = Either Failure a -> IO (Either Failure a)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either Failure a -> IO (Either Failure a))
-> Either Failure a -> IO (Either Failure a)
forall a b. (a -> b) -> a -> b
$ a -> Either Failure a
forall a b. b -> Either a b
Right a
x
    go (TraceMainException Time
_ Labelled IOSimThreadId
_ SomeException
e [Labelled IOSimThreadId]
_)     = Either Failure a -> IO (Either Failure a)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either Failure a -> IO (Either Failure a))
-> Either Failure a -> IO (Either Failure a)
forall a b. (a -> b) -> a -> b
$ Failure -> Either Failure a
forall a b. a -> Either a b
Left (SomeException -> Failure
FailureException SomeException
e)
    go (TraceDeadlock   Time
_   [Labelled IOSimThreadId]
threads)    = Either Failure a -> IO (Either Failure a)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either Failure a -> IO (Either Failure a))
-> Either Failure a -> IO (Either Failure a)
forall a b. (a -> b) -> a -> b
$ Failure -> Either Failure a
forall a b. a -> Either a b
Left ([Labelled IOSimThreadId] -> Failure
FailureDeadlock [Labelled IOSimThreadId]
threads)
    go TraceLoop{}                      = [Char] -> IO (Either Failure a)
forall a. HasCallStack => [Char] -> a
error [Char]
"Impossible: traceResult TraceLoop{}"
    go (TraceInternalError [Char]
msg)         = Either Failure a -> IO (Either Failure a)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either Failure a -> IO (Either Failure a))
-> Either Failure a -> IO (Either Failure a)
forall a b. (a -> b) -> a -> b
$ Failure -> Either Failure a
forall a b. a -> Either a b
Left ([Char] -> Failure
FailureInternal [Char]
msg)

-- | Turn 'SimTrace' into a list of timestamped events.
--
traceEvents :: SimTrace a -> [(Time, IOSimThreadId, Maybe ThreadLabel, SimEventType)]
traceEvents :: forall a.
SimTrace a -> [(Time, IOSimThreadId, Maybe [Char], SimEventType)]
traceEvents (SimTrace Time
time IOSimThreadId
tid Maybe [Char]
tlbl SimEventType
event SimTrace a
t)      = (Time
time, IOSimThreadId
tid, Maybe [Char]
tlbl, SimEventType
event)
                                                  (Time, IOSimThreadId, Maybe [Char], SimEventType)
-> [(Time, IOSimThreadId, Maybe [Char], SimEventType)]
-> [(Time, IOSimThreadId, Maybe [Char], SimEventType)]
forall a. a -> [a] -> [a]
: SimTrace a -> [(Time, IOSimThreadId, Maybe [Char], SimEventType)]
forall a.
SimTrace a -> [(Time, IOSimThreadId, Maybe [Char], SimEventType)]
traceEvents SimTrace a
t
traceEvents (SimPORTrace Time
time IOSimThreadId
tid Int
_ Maybe [Char]
tlbl SimEventType
event SimTrace a
t) = (Time
time, IOSimThreadId
tid, Maybe [Char]
tlbl, SimEventType
event)
                                                  (Time, IOSimThreadId, Maybe [Char], SimEventType)
-> [(Time, IOSimThreadId, Maybe [Char], SimEventType)]
-> [(Time, IOSimThreadId, Maybe [Char], SimEventType)]
forall a. a -> [a] -> [a]
: SimTrace a -> [(Time, IOSimThreadId, Maybe [Char], SimEventType)]
forall a.
SimTrace a -> [(Time, IOSimThreadId, Maybe [Char], SimEventType)]
traceEvents SimTrace a
t
traceEvents SimTrace a
_                                     = []


-- | Pretty print a timestamped event.
--
ppEvents :: [(Time, IOSimThreadId, Maybe ThreadLabel, SimEventType)]
         -> String
ppEvents :: [(Time, IOSimThreadId, Maybe [Char], SimEventType)] -> [Char]
ppEvents [(Time, IOSimThreadId, Maybe [Char], SimEventType)]
events =
    [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"\n"
      [ Int -> Int -> Int -> SimEvent -> [Char]
ppSimEvent Int
timeWidth Int
tidWidth Int
width
                   SimEvent {Time
seTime :: Time
seTime :: Time
seTime, IOSimThreadId
seThreadId :: IOSimThreadId
seThreadId :: IOSimThreadId
seThreadId, Maybe [Char]
seThreadLabel :: Maybe [Char]
seThreadLabel :: Maybe [Char]
seThreadLabel, SimEventType
seType :: SimEventType
seType :: SimEventType
seType }
      | (Time
seTime, IOSimThreadId
seThreadId, Maybe [Char]
seThreadLabel, SimEventType
seType) <- [(Time, IOSimThreadId, Maybe [Char], SimEventType)]
events
      ]
  where
    timeWidth :: Int
timeWidth = [Int] -> Int
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum
                [ [Char] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Time -> [Char]
forall a. Show a => a -> [Char]
show Time
t)
                | (Time
t, IOSimThreadId
_, Maybe [Char]
_, SimEventType
_) <- [(Time, IOSimThreadId, Maybe [Char], SimEventType)]
events
                ]
    tidWidth :: Int
tidWidth  = [Int] -> Int
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum
                [ [Char] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (IOSimThreadId -> [Char]
forall a. Show a => a -> [Char]
show IOSimThreadId
tid)
                | (Time
_, IOSimThreadId
tid, Maybe [Char]
_, SimEventType
_) <- [(Time, IOSimThreadId, Maybe [Char], SimEventType)]
events
                ]
    width :: Int
width     = [Int] -> Int
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum
                [ Int -> ([Char] -> Int) -> Maybe [Char] -> Int
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Int
0 [Char] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Maybe [Char]
threadLabel
                | (Time
_, IOSimThreadId
_, Maybe [Char]
threadLabel, SimEventType
_) <- [(Time, IOSimThreadId, Maybe [Char], SimEventType)]
events
                ]


-- | See 'runSimTraceST' below.
--
runSimTrace :: forall a. (forall s. IOSim s a) -> SimTrace a
runSimTrace :: forall a. (forall s. IOSim s a) -> SimTrace a
runSimTrace forall s. IOSim s a
mainAction = (forall s. ST s (SimTrace a)) -> SimTrace a
forall a. (forall s. ST s a) -> a
runST (IOSim s a -> ST s (SimTrace a)
forall s a. IOSim s a -> ST s (SimTrace a)
runSimTraceST IOSim s a
forall s. IOSim s a
mainAction)

--
-- IOSimPOR
--
--
-- $iosimpor
--
-- /IOSimPOR/ is a different interpreter of 'IOSim' which has the ability to
-- discover race conditions and replay the simulation using a schedule which
-- reverts them.  For extended documentation how to use it see
-- [here](https://github.com/input-output-hk/io-sim/blob/main/io-sim/how-to-use-IOSimPOR.md).
--
-- /IOSimPOR/ only discovers races between events which happen in the same time
-- slot.  In /IOSim/ and /IOSimPOR/ time only moves explicitly through timer
-- events, e.g. things like `Control.Monad.Class.MonadTimer.SI.threadDelay`,
-- `Control.Monad.Class.MonadTimer.SI.registerDelay` or the
-- `Control.Monad.Class.MonadTimer.MonadTimeout.NonStandard` API.  The usual
-- QuickCheck techniques can help explore different schedules of
-- threads too.

-- | Execute a simulation, discover & revert races.  Note that this will execute
-- the simulation multiple times with different schedules, and thus it's much
-- more costly than a simple `runSimTrace` (also the simulation environments has
-- much more state to track and hence it is slower).
--
-- On property failure it will show the failing schedule (`ScheduleControl`)
-- which can be passed to `controlSimTrace` to reproduce the failure without
-- discovering the schedule.
--
exploreSimTrace
  :: forall a test. Testable test
  => (ExplorationOptions -> ExplorationOptions)
  -- ^ modify default exploration options
  -> (forall s. IOSim s a)
  -- ^ a simulation to run
  -> (Maybe (SimTrace a) -> SimTrace a -> test)
  -- ^ a callback which receives the previous trace (e.g. before reverting
  -- a race condition) and current trace
  -> Property
exploreSimTrace :: forall a test.
Testable test =>
(ExplorationOptions -> ExplorationOptions)
-> (forall s. IOSim s a)
-> (Maybe (SimTrace a) -> SimTrace a -> test)
-> Property
exploreSimTrace ExplorationOptions -> ExplorationOptions
optsf forall s. IOSim s a
mainAction Maybe (SimTrace a) -> SimTrace a -> test
k =
  case ExplorationOptions -> Maybe ScheduleControl
explorationReplay ExplorationOptions
opts of
    Maybe ScheduleControl
Nothing ->
      Int -> Int -> ScheduleControl -> Maybe (SimTrace a) -> Property
explore (ExplorationOptions -> Int
explorationScheduleBound ExplorationOptions
opts) (ExplorationOptions -> Int
explorationBranching ExplorationOptions
opts) ScheduleControl
ControlDefault Maybe (SimTrace a)
forall a. Maybe a
Nothing Property -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.&&.
      let size :: Int
size = () -> Int
cacheSize() in Int
size Int -> Property -> Property
forall a b. a -> b -> b
`seq`
      [Char] -> [[Char]] -> Bool -> Property
forall prop.
Testable prop =>
[Char] -> [[Char]] -> prop -> Property
tabulate [Char]
"Modified schedules explored" [Int -> [Char]
bucket Int
size] Bool
True
    Just ScheduleControl
control ->
      ExplorationOptions
-> (forall s. IOSim s a)
-> ScheduleControl
-> (SimTrace a -> test)
-> Property
forall a test.
Testable test =>
ExplorationOptions
-> (forall s. IOSim s a)
-> ScheduleControl
-> (SimTrace a -> test)
-> Property
replaySimTrace ExplorationOptions
opts IOSim s a
forall s. IOSim s a
mainAction ScheduleControl
control (Maybe (SimTrace a) -> SimTrace a -> test
k Maybe (SimTrace a)
forall a. Maybe a
Nothing)
  where
    opts :: ExplorationOptions
opts = ExplorationOptions -> ExplorationOptions
optsf ExplorationOptions
stdExplorationOptions

    explore :: Int -- schedule bound
            -> Int -- branching factor
            -> ScheduleControl -> Maybe (SimTrace a) -> Property
    explore :: Int -> Int -> ScheduleControl -> Maybe (SimTrace a) -> Property
explore Int
n Int
m ScheduleControl
control Maybe (SimTrace a)
passingTrace =

      -- ALERT!!! Impure code: readRaces must be called *after* we have
      -- finished with trace.
      let (() -> [ScheduleControl]
readRaces, SimTrace a
trace0) = Int -> SimTrace a -> (() -> [ScheduleControl], SimTrace a)
forall a.
Int -> SimTrace a -> (() -> [ScheduleControl], SimTrace a)
detachTraceRaces (ExplorationOptions -> Int
explorationDebugLevel ExplorationOptions
opts)
                              (SimTrace a -> (() -> [ScheduleControl], SimTrace a))
-> SimTrace a -> (() -> [ScheduleControl], SimTrace a)
forall a b. (a -> b) -> a -> b
$ Maybe Int -> ScheduleControl -> (forall s. IOSim s a) -> SimTrace a
forall a.
Maybe Int -> ScheduleControl -> (forall s. IOSim s a) -> SimTrace a
controlSimTrace
                                  (ExplorationOptions -> Maybe Int
explorationStepTimelimit ExplorationOptions
opts) ScheduleControl
control IOSim s a
forall s. IOSim s a
mainAction
          (Maybe
  ((Time, IOSimThreadId, Maybe [Char]),
   Set (IOSimThreadId, Maybe [Char]))
sleeper,SimTrace a
trace) = Maybe (SimTrace a)
-> SimTrace a
-> (Maybe
      ((Time, IOSimThreadId, Maybe [Char]),
       Set (IOSimThreadId, Maybe [Char])),
    SimTrace a)
forall a1 a2.
Maybe (SimTrace a1)
-> SimTrace a2
-> (Maybe
      ((Time, IOSimThreadId, Maybe [Char]),
       Set (IOSimThreadId, Maybe [Char])),
    SimTrace a2)
compareTraces Maybe (SimTrace a)
passingTrace SimTrace a
trace0
      in ( [Char] -> Property -> Property
forall prop. Testable prop => [Char] -> prop -> Property
counterexample ([Char]
"Schedule control: " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ ScheduleControl -> [Char]
forall a. Show a => a -> [Char]
show ScheduleControl
control)
         (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ [Char] -> test -> Property
forall prop. Testable prop => [Char] -> prop -> Property
counterexample
            (case Maybe
  ((Time, IOSimThreadId, Maybe [Char]),
   Set (IOSimThreadId, Maybe [Char]))
sleeper of
              Maybe
  ((Time, IOSimThreadId, Maybe [Char]),
   Set (IOSimThreadId, Maybe [Char]))
Nothing -> [Char]
"No thread delayed"
              Just ((Time
t,IOSimThreadId
tid,Maybe [Char]
lab),Set (IOSimThreadId, Maybe [Char])
racing) ->
                (IOSimThreadId, Maybe [Char]) -> [Char]
showThread (IOSimThreadId
tid,Maybe [Char]
lab) [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++
                [Char]
" delayed at time "[Char] -> ShowS
forall a. [a] -> [a] -> [a]
++
                Time -> [Char]
forall a. Show a => a -> [Char]
show Time
t [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++
                [Char]
"\n  until after:\n" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++
                [[Char]] -> [Char]
unlines (((IOSimThreadId, Maybe [Char]) -> [Char])
-> [(IOSimThreadId, Maybe [Char])] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map (([Char]
"    "[Char] -> ShowS
forall a. [a] -> [a] -> [a]
++)ShowS
-> ((IOSimThreadId, Maybe [Char]) -> [Char])
-> (IOSimThreadId, Maybe [Char])
-> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(IOSimThreadId, Maybe [Char]) -> [Char]
showThread) ([(IOSimThreadId, Maybe [Char])] -> [[Char]])
-> [(IOSimThreadId, Maybe [Char])] -> [[Char]]
forall a b. (a -> b) -> a -> b
$ Set (IOSimThreadId, Maybe [Char])
-> [(IOSimThreadId, Maybe [Char])]
forall a. Set a -> [a]
Set.toList Set (IOSimThreadId, Maybe [Char])
racing)
             )
         (test -> Property) -> test -> Property
forall a b. (a -> b) -> a -> b
$ Maybe (SimTrace a) -> SimTrace a -> test
k Maybe (SimTrace a)
passingTrace SimTrace a
trace
         )
      Property -> Property -> Property
forall prop. TestableNoCatch prop => prop -> prop -> Property
.&&| let limit :: Int
limit     = (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
mInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
m
               -- To ensure the set of schedules explored is deterministic, we
               -- filter out cached ones *after* selecting the children of this
               -- node.
               races :: [ScheduleControl]
races     = (ScheduleControl -> Bool) -> [ScheduleControl] -> [ScheduleControl]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool)
-> (ScheduleControl -> Bool) -> ScheduleControl -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ScheduleControl -> Bool
cached) ([ScheduleControl] -> [ScheduleControl])
-> ([ScheduleControl] -> [ScheduleControl])
-> [ScheduleControl]
-> [ScheduleControl]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> [ScheduleControl] -> [ScheduleControl]
forall a. Int -> [a] -> [a]
take Int
limit ([ScheduleControl] -> [ScheduleControl])
-> [ScheduleControl] -> [ScheduleControl]
forall a b. (a -> b) -> a -> b
$ () -> [ScheduleControl]
readRaces ()
               branching :: Int
branching = [ScheduleControl] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [ScheduleControl]
races
           in -- tabulate "Races explored" (map show races) $
              [Char] -> [[Char]] -> Property -> Property
forall prop.
Testable prop =>
[Char] -> [[Char]] -> prop -> Property
tabulate [Char]
"Branching factor" [Int -> [Char]
bucket Int
branching] (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
              [Char] -> [[Char]] -> Property -> Property
forall prop.
Testable prop =>
[Char] -> [[Char]] -> prop -> Property
tabulate [Char]
"Race reversals per schedule" [Int -> [Char]
bucket (ScheduleControl -> Int
raceReversals ScheduleControl
control)] (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
              [Property] -> Property
forall prop. TestableNoCatch prop => [prop] -> Property
conjoinPar
                [ --Debug.trace "New schedule:" $
                  --Debug.trace ("  "++show r) $
                  --counterexample ("Schedule control: " ++ show r) $
                  Int -> Int -> ScheduleControl -> Maybe (SimTrace a) -> Property
explore Int
n' ((Int
mInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) Int -> Int -> Int
forall a. Ord a => a -> a -> a
`max` Int
1) ScheduleControl
r (SimTrace a -> Maybe (SimTrace a)
forall a. a -> Maybe a
Just SimTrace a
trace0)
                | (ScheduleControl
r,Int
n') <- [ScheduleControl] -> [Int] -> [(ScheduleControl, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [ScheduleControl]
races (Int -> Int -> [Int]
divide (Int
nInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
branching) Int
branching) ]

    bucket :: Int -> String
    bucket :: Int -> [Char]
bucket Int
n | Int
nInt -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<Int
10      = Int -> [Char]
forall a. Show a => a -> [Char]
show Int
n
             | Bool
otherwise = Int -> Int -> [Char]
forall {t}. (Show t, Integral t) => t -> t -> [Char]
buck Int
n Int
1
    buck :: t -> t -> [Char]
buck t
n t
t | t
nt -> t -> Bool
forall a. Ord a => a -> a -> Bool
<t
10      = t -> [Char]
forall a. Show a => a -> [Char]
show (t
nt -> t -> t
forall a. Num a => a -> a -> a
*t
t) [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
"-" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ t -> [Char]
forall a. Show a => a -> [Char]
show ((t
nt -> t -> t
forall a. Num a => a -> a -> a
+t
1)t -> t -> t
forall a. Num a => a -> a -> a
*t
tt -> t -> t
forall a. Num a => a -> a -> a
-t
1)
             | Bool
otherwise = t -> t -> [Char]
buck (t
n t -> t -> t
forall a. Integral a => a -> a -> a
`div` t
10) (t
tt -> t -> t
forall a. Num a => a -> a -> a
*t
10)

    -- divide n into k factors which sums up to n
    divide :: Int -> Int -> [Int]
    divide :: Int -> Int -> [Int]
divide Int
n Int
k =
      [ Int
n Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
k Int -> Int -> Int
forall a. Num a => a -> a -> a
+ if Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
n Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` Int
k then Int
1 else Int
0
      | Int
i <- [Int
0..Int
kInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1] ]

    showThread :: (IOSimThreadId,Maybe ThreadLabel) -> String
    showThread :: (IOSimThreadId, Maybe [Char]) -> [Char]
showThread (IOSimThreadId
tid,Maybe [Char]
lab) =
      IOSimThreadId -> [Char]
ppIOSimThreadId IOSimThreadId
tid [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ (case Maybe [Char]
lab of Maybe [Char]
Nothing -> [Char]
""
                                          Just [Char]
l  -> [Char]
" ("[Char] -> ShowS
forall a. [a] -> [a] -> [a]
++[Char]
l[Char] -> ShowS
forall a. [a] -> [a] -> [a]
++[Char]
")")

    -- cache of explored schedules
    cache :: IORef (Set ScheduleControl)
    cache :: IORef (Set ScheduleControl)
cache = IO (IORef (Set ScheduleControl)) -> IORef (Set ScheduleControl)
forall a. IO a -> a
unsafePerformIO IO (IORef (Set ScheduleControl))
cacheIO

    -- insert a schedule into the cache
    cached :: ScheduleControl -> Bool
    cached :: ScheduleControl -> Bool
cached = IO Bool -> Bool
forall a. IO a -> a
unsafePerformIO (IO Bool -> Bool)
-> (ScheduleControl -> IO Bool) -> ScheduleControl -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ScheduleControl -> IO Bool
cachedIO

    -- compute cache size; it's a function to make sure that `GHC` does not
    -- inline it (and share the same thunk).
    cacheSize :: () -> Int
    cacheSize :: () -> Int
cacheSize = IO Int -> Int
forall a. IO a -> a
unsafePerformIO (IO Int -> Int) -> (() -> IO Int) -> () -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. () -> IO Int
cacheSizeIO

    --
    -- Caching in IO monad
    --

    -- It is possible for the same control to be generated several times.
    -- To avoid exploring them twice, we keep a cache of explored schedules.
    cacheIO :: IO (IORef (Set ScheduleControl))
    cacheIO :: IO (IORef (Set ScheduleControl))
cacheIO = Set ScheduleControl -> IO (IORef (Set ScheduleControl))
forall a. a -> IO (IORef a)
newIORef (Set ScheduleControl -> IO (IORef (Set ScheduleControl)))
-> Set ScheduleControl -> IO (IORef (Set ScheduleControl))
forall a b. (a -> b) -> a -> b
$
              -- we use opts here just to be sure the reference cannot be
              -- lifted out of exploreSimTrace
              if ExplorationOptions -> Int
explorationScheduleBound ExplorationOptions
opts Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>=Int
0
                then Set ScheduleControl
forall a. Set a
Set.empty
                else [Char] -> Set ScheduleControl
forall a. HasCallStack => [Char] -> a
error [Char]
"exploreSimTrace: negative schedule bound"

    cachedIO :: ScheduleControl -> IO Bool
    cachedIO :: ScheduleControl -> IO Bool
cachedIO ScheduleControl
m = IORef (Set ScheduleControl)
-> (Set ScheduleControl -> (Set ScheduleControl, Bool)) -> IO Bool
forall a b. IORef a -> (a -> (a, b)) -> IO b
atomicModifyIORef' IORef (Set ScheduleControl)
cache ((Set ScheduleControl -> (Set ScheduleControl, Bool)) -> IO Bool)
-> (Set ScheduleControl -> (Set ScheduleControl, Bool)) -> IO Bool
forall a b. (a -> b) -> a -> b
$ \Set ScheduleControl
set ->
      (ScheduleControl -> Set ScheduleControl -> Set ScheduleControl
forall a. Ord a => a -> Set a -> Set a
Set.insert ScheduleControl
m Set ScheduleControl
set, ScheduleControl -> Set ScheduleControl -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member ScheduleControl
m Set ScheduleControl
set)

    cacheSizeIO :: () -> IO Int
    cacheSizeIO :: () -> IO Int
cacheSizeIO () = Set ScheduleControl -> Int
forall a. Set a -> Int
Set.size (Set ScheduleControl -> Int) -> IO (Set ScheduleControl) -> IO Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IORef (Set ScheduleControl) -> IO (Set ScheduleControl)
forall a. IORef a -> IO a
readIORef IORef (Set ScheduleControl)
cache


-- |  Trace `SimTrace` to `stderr`.
--
-- An internal function.
--
traceDebugLog :: Int -> Either SimEvent (SimResult a) -> SimTrace a -> SimTrace a
traceDebugLog :: forall a.
Int -> Either SimEvent (SimResult a) -> SimTrace a -> SimTrace a
traceDebugLog Int
logLevel Either SimEvent (SimResult a)
_event SimTrace a
trace | Int
logLevel Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0 = SimTrace a
trace
-- Discard races if log level is 1
traceDebugLog Int
1 (Left SimPOREvent { seType :: SimEvent -> SimEventType
seType = EventRaces {} }) SimTrace a
trace = SimTrace a
trace
traceDebugLog Int
1 (Left SimEvent
event) SimTrace a
trace  = [Char] -> SimTrace a -> SimTrace a
forall a. [Char] -> a -> a
Debug.trace (Int -> Int -> Int -> SimEvent -> [Char]
ppSimEvent Int
0 Int
0 Int
0 SimEvent
event) SimTrace a
trace
traceDebugLog Int
1 (Right SimResult a
event) SimTrace a
trace = [Char] -> SimTrace a -> SimTrace a
forall a. [Char] -> a -> a
Debug.trace (Int -> Int -> Int -> SimResult () -> [Char]
forall a. Show a => Int -> Int -> Int -> SimResult a -> [Char]
ppSimResult Int
0 Int
0 Int
0 (SimResult a -> SimResult ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void SimResult a
event)) SimTrace a
trace
-- Otherwise, show races
traceDebugLog Int
_ (Left SimEvent
event) SimTrace a
trace  = [Char] -> SimTrace a -> SimTrace a
forall a. [Char] -> a -> a
Debug.trace (Int -> Int -> Int -> SimEvent -> [Char]
ppSimEvent Int
0 Int
0 Int
0 SimEvent
event) SimTrace a
trace
traceDebugLog Int
_ (Right SimResult a
event) SimTrace a
trace = [Char] -> SimTrace a -> SimTrace a
forall a. [Char] -> a -> a
Debug.trace (Int -> Int -> Int -> SimResult () -> [Char]
forall a. Show a => Int -> Int -> Int -> SimResult a -> [Char]
ppSimResult Int
0 Int
0 Int
0 (SimResult a -> SimResult ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void SimResult a
event)) SimTrace a
trace

replaySimTrace :: forall a test. (Testable test)
               => ExplorationOptions
               -- ^ race exploration options
               -> (forall s. IOSim s a)
               -> ScheduleControl
               -- ^ a schedule control to reproduce
               -> (SimTrace a -> test)
               -- ^ a callback which receives the simulation trace. The trace
               -- will not contain any race events
               -> Property
replaySimTrace :: forall a test.
Testable test =>
ExplorationOptions
-> (forall s. IOSim s a)
-> ScheduleControl
-> (SimTrace a -> test)
-> Property
replaySimTrace ExplorationOptions
opts forall s. IOSim s a
mainAction ScheduleControl
control SimTrace a -> test
k =
  let (() -> [ScheduleControl]
_,SimTrace a
trace) = Int -> SimTrace a -> (() -> [ScheduleControl], SimTrace a)
forall a.
Int -> SimTrace a -> (() -> [ScheduleControl], SimTrace a)
detachTraceRaces (ExplorationOptions -> Int
explorationDebugLevel ExplorationOptions
opts) (SimTrace a -> (() -> [ScheduleControl], SimTrace a))
-> SimTrace a -> (() -> [ScheduleControl], SimTrace a)
forall a b. (a -> b) -> a -> b
$
                  Maybe Int -> ScheduleControl -> (forall s. IOSim s a) -> SimTrace a
forall a.
Maybe Int -> ScheduleControl -> (forall s. IOSim s a) -> SimTrace a
controlSimTrace (ExplorationOptions -> Maybe Int
explorationStepTimelimit ExplorationOptions
opts) ScheduleControl
control IOSim s a
forall s. IOSim s a
mainAction
  in test -> Property
forall prop. Testable prop => prop -> Property
property (SimTrace a -> test
k SimTrace a
trace)

-- | Run a simulation using a given schedule.  This is useful to reproduce
-- failing cases without exploring the races.
--
controlSimTrace :: forall a.
                   Maybe Int
                -- ^ limit on the computation time allowed per scheduling step, for
                -- catching infinite loops etc.
                -> ScheduleControl
                -- ^ a schedule to replay
                --
                -- /note/: must be either `ControlDefault` or `ControlAwait`.
                -> (forall s. IOSim s a)
                -- ^ a simulation to run
                -> SimTrace a
controlSimTrace :: forall a.
Maybe Int -> ScheduleControl -> (forall s. IOSim s a) -> SimTrace a
controlSimTrace Maybe Int
limit ScheduleControl
control forall s. IOSim s a
main =
    (forall s. ST s (SimTrace a)) -> SimTrace a
forall a. (forall s. ST s a) -> a
runST (Maybe Int -> ScheduleControl -> IOSim s a -> ST s (SimTrace a)
forall s a.
Maybe Int -> ScheduleControl -> IOSim s a -> ST s (SimTrace a)
IOSimPOR.controlSimTraceST Maybe Int
limit ScheduleControl
control IOSim s a
forall s. IOSim s a
main)

--
-- Utils
--

raceReversals :: ScheduleControl -> Int
raceReversals :: ScheduleControl -> Int
raceReversals ScheduleControl
ControlDefault      = Int
0
raceReversals (ControlAwait [ScheduleMod]
mods) = [ScheduleMod] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [ScheduleMod]
mods
raceReversals ControlFollow{}     = [Char] -> Int
forall a. HasCallStack => [Char] -> a
error [Char]
"Impossible: raceReversals ControlFollow{}"

-- `compareTracesST` is given (maybe) a passing trace and a failing trace,
-- and identifies the point at which they diverge, where it inserts a
-- "sleep" event for the thread that is delayed in the failing case,
-- and a "wake" event before its next action. It also returns the
-- identity and time of the sleeping thread. Since we expect the trace
-- to be consumed lazily (and perhaps only partially), and since the
-- sleeping thread is not of interest unless the trace is consumed
-- this far, then we collect its identity only if it is reached using
-- `unsafePerformIO`.

compareTraces :: Maybe (SimTrace a1)
              -> SimTrace a2
              -> (Maybe ((Time, IOSimThreadId, Maybe ThreadLabel),
                         Set.Set (IOSimThreadId, Maybe ThreadLabel)),
                  SimTrace a2)
compareTraces :: forall a1 a2.
Maybe (SimTrace a1)
-> SimTrace a2
-> (Maybe
      ((Time, IOSimThreadId, Maybe [Char]),
       Set (IOSimThreadId, Maybe [Char])),
    SimTrace a2)
compareTraces Maybe (SimTrace a1)
Nothing SimTrace a2
trace = (Maybe
  ((Time, IOSimThreadId, Maybe [Char]),
   Set (IOSimThreadId, Maybe [Char]))
forall a. Maybe a
Nothing, SimTrace a2
trace)
compareTraces (Just SimTrace a1
passing) SimTrace a2
trace = IO
  (Maybe
     ((Time, IOSimThreadId, Maybe [Char]),
      Set (IOSimThreadId, Maybe [Char])),
   SimTrace a2)
-> (Maybe
      ((Time, IOSimThreadId, Maybe [Char]),
       Set (IOSimThreadId, Maybe [Char])),
    SimTrace a2)
forall a. IO a -> a
unsafePerformIO (IO
   (Maybe
      ((Time, IOSimThreadId, Maybe [Char]),
       Set (IOSimThreadId, Maybe [Char])),
    SimTrace a2)
 -> (Maybe
       ((Time, IOSimThreadId, Maybe [Char]),
        Set (IOSimThreadId, Maybe [Char])),
     SimTrace a2))
-> IO
     (Maybe
        ((Time, IOSimThreadId, Maybe [Char]),
         Set (IOSimThreadId, Maybe [Char])),
      SimTrace a2)
-> (Maybe
      ((Time, IOSimThreadId, Maybe [Char]),
       Set (IOSimThreadId, Maybe [Char])),
    SimTrace a2)
forall a b. (a -> b) -> a -> b
$ do
  IORef
  (Maybe
     ((Time, IOSimThreadId, Maybe [Char]),
      Set (IOSimThreadId, Maybe [Char])))
sleeper <- Maybe
  ((Time, IOSimThreadId, Maybe [Char]),
   Set (IOSimThreadId, Maybe [Char]))
-> IO
     (IORef
        (Maybe
           ((Time, IOSimThreadId, Maybe [Char]),
            Set (IOSimThreadId, Maybe [Char]))))
forall a. a -> IO (IORef a)
newIORef Maybe
  ((Time, IOSimThreadId, Maybe [Char]),
   Set (IOSimThreadId, Maybe [Char]))
forall a. Maybe a
Nothing
  (Maybe
   ((Time, IOSimThreadId, Maybe [Char]),
    Set (IOSimThreadId, Maybe [Char])),
 SimTrace a2)
-> IO
     (Maybe
        ((Time, IOSimThreadId, Maybe [Char]),
         Set (IOSimThreadId, Maybe [Char])),
      SimTrace a2)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (IO
  (Maybe
     ((Time, IOSimThreadId, Maybe [Char]),
      Set (IOSimThreadId, Maybe [Char])))
-> Maybe
     ((Time, IOSimThreadId, Maybe [Char]),
      Set (IOSimThreadId, Maybe [Char]))
forall a. IO a -> a
unsafePerformIO (IO
   (Maybe
      ((Time, IOSimThreadId, Maybe [Char]),
       Set (IOSimThreadId, Maybe [Char])))
 -> Maybe
      ((Time, IOSimThreadId, Maybe [Char]),
       Set (IOSimThreadId, Maybe [Char])))
-> IO
     (Maybe
        ((Time, IOSimThreadId, Maybe [Char]),
         Set (IOSimThreadId, Maybe [Char])))
-> Maybe
     ((Time, IOSimThreadId, Maybe [Char]),
      Set (IOSimThreadId, Maybe [Char]))
forall a b. (a -> b) -> a -> b
$ IORef
  (Maybe
     ((Time, IOSimThreadId, Maybe [Char]),
      Set (IOSimThreadId, Maybe [Char])))
-> IO
     (Maybe
        ((Time, IOSimThreadId, Maybe [Char]),
         Set (IOSimThreadId, Maybe [Char])))
forall a. IORef a -> IO a
readIORef IORef
  (Maybe
     ((Time, IOSimThreadId, Maybe [Char]),
      Set (IOSimThreadId, Maybe [Char])))
sleeper,
          IORef
  (Maybe
     ((Time, IOSimThreadId, Maybe [Char]),
      Set (IOSimThreadId, Maybe [Char])))
-> SimTrace a1 -> SimTrace a2 -> SimTrace a2
forall {a} {a}.
IORef
  (Maybe
     ((Time, IOSimThreadId, Maybe [Char]),
      Set (IOSimThreadId, Maybe [Char])))
-> SimTrace a -> SimTrace a -> SimTrace a
go IORef
  (Maybe
     ((Time, IOSimThreadId, Maybe [Char]),
      Set (IOSimThreadId, Maybe [Char])))
sleeper SimTrace a1
passing SimTrace a2
trace)
  where go :: IORef
  (Maybe
     ((Time, IOSimThreadId, Maybe [Char]),
      Set (IOSimThreadId, Maybe [Char])))
-> SimTrace a -> SimTrace a -> SimTrace a
go IORef
  (Maybe
     ((Time, IOSimThreadId, Maybe [Char]),
      Set (IOSimThreadId, Maybe [Char])))
sleeper (SimPORTrace Time
tpass IOSimThreadId
tidpass Int
_ Maybe [Char]
_ SimEventType
_ SimTrace a
pass')
                   (SimPORTrace Time
tfail IOSimThreadId
tidfail Int
tstepfail Maybe [Char]
tlfail SimEventType
evfail SimTrace a
fail')
          | (Time
tpass,IOSimThreadId
tidpass) (Time, IOSimThreadId) -> (Time, IOSimThreadId) -> Bool
forall a. Eq a => a -> a -> Bool
== (Time
tfail,IOSimThreadId
tidfail) =
              Time
-> IOSimThreadId
-> Int
-> Maybe [Char]
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> IOSimThreadId
-> Int
-> Maybe [Char]
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
tfail IOSimThreadId
tidfail Int
tstepfail Maybe [Char]
tlfail SimEventType
evfail
                (SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall a b. (a -> b) -> a -> b
$ IORef
  (Maybe
     ((Time, IOSimThreadId, Maybe [Char]),
      Set (IOSimThreadId, Maybe [Char])))
-> SimTrace a -> SimTrace a -> SimTrace a
go IORef
  (Maybe
     ((Time, IOSimThreadId, Maybe [Char]),
      Set (IOSimThreadId, Maybe [Char])))
sleeper SimTrace a
pass' SimTrace a
fail'
        go IORef
  (Maybe
     ((Time, IOSimThreadId, Maybe [Char]),
      Set (IOSimThreadId, Maybe [Char])))
sleeper (SimPORTrace Time
tpass IOSimThreadId
tidpass Int
tsteppass Maybe [Char]
tlpass SimEventType
_ SimTrace a
_) SimTrace a
fail =
          IO (SimTrace a) -> SimTrace a
forall a. IO a -> a
unsafePerformIO (IO (SimTrace a) -> SimTrace a) -> IO (SimTrace a) -> SimTrace a
forall a b. (a -> b) -> a -> b
$ do
            IORef
  (Maybe
     ((Time, IOSimThreadId, Maybe [Char]),
      Set (IOSimThreadId, Maybe [Char])))
-> Maybe
     ((Time, IOSimThreadId, Maybe [Char]),
      Set (IOSimThreadId, Maybe [Char]))
-> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef
  (Maybe
     ((Time, IOSimThreadId, Maybe [Char]),
      Set (IOSimThreadId, Maybe [Char])))
sleeper (Maybe
   ((Time, IOSimThreadId, Maybe [Char]),
    Set (IOSimThreadId, Maybe [Char]))
 -> IO ())
-> Maybe
     ((Time, IOSimThreadId, Maybe [Char]),
      Set (IOSimThreadId, Maybe [Char]))
-> IO ()
forall a b. (a -> b) -> a -> b
$ ((Time, IOSimThreadId, Maybe [Char]),
 Set (IOSimThreadId, Maybe [Char]))
-> Maybe
     ((Time, IOSimThreadId, Maybe [Char]),
      Set (IOSimThreadId, Maybe [Char]))
forall a. a -> Maybe a
Just ((Time
tpass, IOSimThreadId
tidpass, Maybe [Char]
tlpass),Set (IOSimThreadId, Maybe [Char])
forall a. Set a
Set.empty)
            SimTrace a -> IO (SimTrace a)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (SimTrace a -> IO (SimTrace a)) -> SimTrace a -> IO (SimTrace a)
forall a b. (a -> b) -> a -> b
$ Time
-> IOSimThreadId
-> Int
-> Maybe [Char]
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> IOSimThreadId
-> Int
-> Maybe [Char]
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
tpass IOSimThreadId
tidpass Int
tsteppass Maybe [Char]
tlpass SimEventType
EventThreadSleep
                   (SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall a b. (a -> b) -> a -> b
$ IORef
  (Maybe
     ((Time, IOSimThreadId, Maybe [Char]),
      Set (IOSimThreadId, Maybe [Char])))
-> IOSimThreadId -> SimTrace a -> SimTrace a
forall {a} {a}.
IORef (Maybe (a, Set (IOSimThreadId, Maybe [Char])))
-> IOSimThreadId -> SimTrace a -> SimTrace a
wakeup IORef
  (Maybe
     ((Time, IOSimThreadId, Maybe [Char]),
      Set (IOSimThreadId, Maybe [Char])))
sleeper IOSimThreadId
tidpass SimTrace a
fail
        go IORef
  (Maybe
     ((Time, IOSimThreadId, Maybe [Char]),
      Set (IOSimThreadId, Maybe [Char])))
_ SimTrace {} SimTrace a
_ = [Char] -> SimTrace a
forall a. HasCallStack => [Char] -> a
error [Char]
"compareTraces: invariant violation"
        go IORef
  (Maybe
     ((Time, IOSimThreadId, Maybe [Char]),
      Set (IOSimThreadId, Maybe [Char])))
_ SimTrace a
_ SimTrace {} = [Char] -> SimTrace a
forall a. HasCallStack => [Char] -> a
error [Char]
"compareTraces: invariant violation"
        go IORef
  (Maybe
     ((Time, IOSimThreadId, Maybe [Char]),
      Set (IOSimThreadId, Maybe [Char])))
_ SimTrace a
_ SimTrace a
fail = SimTrace a
fail

        wakeup :: IORef (Maybe (a, Set (IOSimThreadId, Maybe [Char])))
-> IOSimThreadId -> SimTrace a -> SimTrace a
wakeup IORef (Maybe (a, Set (IOSimThreadId, Maybe [Char])))
sleeper IOSimThreadId
tidpass
               fail :: SimTrace a
fail@(SimPORTrace Time
tfail IOSimThreadId
tidfail Int
tstepfail Maybe [Char]
tlfail SimEventType
evfail SimTrace a
fail')
          | IOSimThreadId
tidpass IOSimThreadId -> IOSimThreadId -> Bool
forall a. Eq a => a -> a -> Bool
== IOSimThreadId
tidfail =
              Time
-> IOSimThreadId
-> Int
-> Maybe [Char]
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> IOSimThreadId
-> Int
-> Maybe [Char]
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
tfail IOSimThreadId
tidfail Int
tstepfail Maybe [Char]
tlfail SimEventType
EventThreadWake SimTrace a
fail
          | Bool
otherwise = IO (SimTrace a) -> SimTrace a
forall a. IO a -> a
unsafePerformIO (IO (SimTrace a) -> SimTrace a) -> IO (SimTrace a) -> SimTrace a
forall a b. (a -> b) -> a -> b
$ do
              Just (a
slp,Set (IOSimThreadId, Maybe [Char])
racing) <- IORef (Maybe (a, Set (IOSimThreadId, Maybe [Char])))
-> IO (Maybe (a, Set (IOSimThreadId, Maybe [Char])))
forall a. IORef a -> IO a
readIORef IORef (Maybe (a, Set (IOSimThreadId, Maybe [Char])))
sleeper
              IORef (Maybe (a, Set (IOSimThreadId, Maybe [Char])))
-> Maybe (a, Set (IOSimThreadId, Maybe [Char])) -> IO ()
forall a. IORef a -> a -> IO ()
writeIORef IORef (Maybe (a, Set (IOSimThreadId, Maybe [Char])))
sleeper (Maybe (a, Set (IOSimThreadId, Maybe [Char])) -> IO ())
-> Maybe (a, Set (IOSimThreadId, Maybe [Char])) -> IO ()
forall a b. (a -> b) -> a -> b
$ (a, Set (IOSimThreadId, Maybe [Char]))
-> Maybe (a, Set (IOSimThreadId, Maybe [Char]))
forall a. a -> Maybe a
Just (a
slp,(IOSimThreadId, Maybe [Char])
-> Set (IOSimThreadId, Maybe [Char])
-> Set (IOSimThreadId, Maybe [Char])
forall a. Ord a => a -> Set a -> Set a
Set.insert (IOSimThreadId
tidfail,Maybe [Char]
tlfail) Set (IOSimThreadId, Maybe [Char])
racing)
              SimTrace a -> IO (SimTrace a)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (SimTrace a -> IO (SimTrace a)) -> SimTrace a -> IO (SimTrace a)
forall a b. (a -> b) -> a -> b
$ Time
-> IOSimThreadId
-> Int
-> Maybe [Char]
-> SimEventType
-> SimTrace a
-> SimTrace a
forall a.
Time
-> IOSimThreadId
-> Int
-> Maybe [Char]
-> SimEventType
-> SimTrace a
-> SimTrace a
SimPORTrace Time
tfail IOSimThreadId
tidfail Int
tstepfail Maybe [Char]
tlfail SimEventType
evfail
                     (SimTrace a -> SimTrace a) -> SimTrace a -> SimTrace a
forall a b. (a -> b) -> a -> b
$ IORef (Maybe (a, Set (IOSimThreadId, Maybe [Char])))
-> IOSimThreadId -> SimTrace a -> SimTrace a
wakeup IORef (Maybe (a, Set (IOSimThreadId, Maybe [Char])))
sleeper IOSimThreadId
tidpass SimTrace a
fail'
        wakeup IORef (Maybe (a, Set (IOSimThreadId, Maybe [Char])))
_ IOSimThreadId
_ SimTrace {} = [Char] -> SimTrace a
forall a. HasCallStack => [Char] -> a
error [Char]
"compareTraces: invariant violation"
        wakeup IORef (Maybe (a, Set (IOSimThreadId, Maybe [Char])))
_ IOSimThreadId
_ SimTrace a
fail = SimTrace a
fail

--
-- QuickCheck monadic combinators
--



-- | Like <monadicST https://hackage.haskell.org/package/QuickCheck-2.14.3/docs/Test-QuickCheck-Monadic.html#v:monadicST>.
--
-- Note: it calls `traceResult` in non-strict mode, e.g. leaked threads do not
-- cause failures.
--
-- @since 1.4.1.0
--
monadicIOSim_ :: Testable a
              => (forall s. PropertyM (IOSim s) a)
              -> Property
monadicIOSim_ :: forall a.
Testable a =>
(forall s. PropertyM (IOSim s) a) -> Property
monadicIOSim_ forall s. PropertyM (IOSim s) a
sim =
    (SimTrace Property -> Property)
-> (forall s a. IOSim s a -> IOSim s a)
-> (forall s. PropertyM (IOSim s) a)
-> Property
forall a (m :: * -> * -> *).
(Testable a, forall s. Monad (m s)) =>
(SimTrace Property -> Property)
-> (forall s a. m s a -> IOSim s a)
-> (forall s. PropertyM (m s) a)
-> Property
monadicIOSim
      (\SimTrace Property
e -> case Bool -> SimTrace Property -> Either Failure Property
forall a. Bool -> SimTrace a -> Either Failure a
traceResult Bool
False SimTrace Property
e of
          Left Failure
e  -> [Char] -> Bool -> Property
forall prop. Testable prop => [Char] -> prop -> Property
counterexample (Failure -> [Char]
forall a. Show a => a -> [Char]
show Failure
e) Bool
False
          Right Property
p -> Property
p)
      IOSim s a -> IOSim s a
forall a. a -> a
forall s a. IOSim s a -> IOSim s a
id
      PropertyM (IOSim s) a
forall s. PropertyM (IOSim s) a
sim

-- | A more general version of `monadicIOSim_`, which:
--
-- * allows to run in monad stacks build on top of `IOSim`;
-- * gives more control how to attach debugging information to failed
--   tests.
--
-- Note, to use this combinator your monad needs to be defined as:
--
-- > newtype M s a = M s { runM :: ReaderT State (IOSim s) a }
--
-- It's important that `M s` is a monad.  For such a monad one you'll need provide
-- a natural transformation:
-- @
--   -- the state could also be created as an `IOSim` computation.
--   nat :: forall s a. State -> M s a -> 'IOSim' s a
--   nat state m = runStateT (runM m) state
-- @
--
-- @since 1.4.1.0
--
monadicIOSim :: (Testable a, forall s. Monad (m s))
             => (SimTrace Property -> Property)
             -- ^ Allows to trace `SimTrace` in counterexamples.  The simplest
             -- use case is to pass:
             --
             -- > either (\e -> counterexample (show e) False) id . traceResult False
             --
             -- as `monadicIOSim_` does.
             --
             -> (forall s a. m s a -> IOSim s a)
             -- ^ natural transformation from `m` to @IOSim` s@
             -> (forall s. PropertyM (m s) a)
             -> Property
monadicIOSim :: forall a (m :: * -> * -> *).
(Testable a, forall s. Monad (m s)) =>
(SimTrace Property -> Property)
-> (forall s a. m s a -> IOSim s a)
-> (forall s. PropertyM (m s) a)
-> Property
monadicIOSim SimTrace Property -> Property
f forall s a. m s a -> IOSim s a
tr forall s. PropertyM (m s) a
sim = Gen Property -> Property
forall prop. Testable prop => prop -> Property
property ((SimTrace Property -> Property)
-> (forall s. Gen (IOSim s Property)) -> Gen Property
forall a.
(SimTrace a -> Property)
-> (forall s. Gen (IOSim s a)) -> Gen Property
runIOSimGen SimTrace Property -> Property
f (m s Property -> IOSim s Property
forall s a. m s a -> IOSim s a
tr (m s Property -> IOSim s Property)
-> Gen (m s Property) -> Gen (IOSim s Property)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PropertyM (m s) a -> Gen (m s Property)
forall a (m :: * -> *).
(Testable a, Monad m) =>
PropertyM m a -> Gen (m Property)
monadic' PropertyM (m s) a
forall s. PropertyM (m s) a
sim))

-- | Like <runSTGen
-- https://hackage.haskell.org/package/QuickCheck-2.14.3/docs/Test-QuickCheck-Monadic.html#v:runSTGen>.
--
-- @since 1.4.1.0
--
runIOSimGen :: (SimTrace a -> Property)
            -> (forall s. Gen (IOSim s a))
            -> Gen Property
runIOSimGen :: forall a.
(SimTrace a -> Property)
-> (forall s. Gen (IOSim s a)) -> Gen Property
runIOSimGen SimTrace a -> Property
f forall s. Gen (IOSim s a)
sim = do
    Capture forall a. Gen a -> a
eval <- Gen Capture
capture
    let trace :: SimTrace a
trace = (forall s. IOSim s a) -> SimTrace a
forall a. (forall s. IOSim s a) -> SimTrace a
runSimTrace (Gen (IOSim s a) -> IOSim s a
forall a. Gen a -> a
eval Gen (IOSim s a)
forall s. Gen (IOSim s a)
sim)
    Property -> Gen Property
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (SimTrace a -> Property
f SimTrace a
trace)