content: -- |
  -- Module      : Test.DejaFu.Conc
  -- Copyright   : (c) 2016--2019 Michael Walker
  -- License     : MIT
  -- Maintainer  : Michael Walker <mike@barrucadu.co.uk>
  -- Stability   : experimental
  -- Portability : portable
  --
  -- Deterministic traced execution of concurrent computations.
  --
  -- This works by executing the computation on a single thread, calling
  -- out to the supplied scheduler after each step to determine which
  -- thread runs next.
  module Test.DejaFu.Conc
    ( -- * Expressing concurrent programs
      Program
    , Basic
    , ConcT
    , ConcIO
  
    -- ** Setup and teardown
    , WithSetup
    , WithSetupAndTeardown
    , withSetup
    , withTeardown
    , withSetupAndTeardown
  
    -- ** Invariants
    , Invariant
    , registerInvariant
    , inspectIORef
    , inspectMVar
    , inspectTVar
  
    -- * Executing concurrent programs
    , Snapshot
    , MemType(..)
    , runConcurrent
    , recordSnapshot
    , runSnapshot
  
    -- ** Scheduling
    , module Test.DejaFu.Schedule
  
    -- * Results
    , Condition(..)
    , Trace
    , Decision(..)
    , ThreadId(..)
    , ThreadAction(..)
    , Lookahead(..)
    , MVarId
    , IORefId
    , MaskingState(..)
    , showTrace
    , showCondition
    ) where
  
  import           Control.Exception                 (MaskingState(..))
  import           Control.Monad                     (void)
  
  import           Test.DejaFu.Conc.Internal.Common
  import           Test.DejaFu.Conc.Internal.Program
  import           Test.DejaFu.Conc.Internal.STM     (ModelTVar)
  import           Test.DejaFu.Schedule
  import           Test.DejaFu.Types
  import           Test.DejaFu.Utils
  
  -------------------------------------------------------------------------------
  -- Expressing concurrent programs
  
  -- | @since 1.4.0.0
  type ConcT = Program Basic
  
  -- | A 'MonadConc' implementation using @IO@.
  --
  -- @since 0.4.0.0
  type ConcIO = ConcT IO
  
  -------------------------------------------------------------------------------
  -- Setup & teardown
  
  -- | A concurrent program with some set-up action.
  --
  -- In terms of results, this is the same as @setup >>= program@.
  -- However, the setup action will be __snapshotted__ (see
  -- 'recordSnapshot' and 'runSnapshot') by the testing functions.  This
  -- means that even if dejafu runs this program many many times, the
  -- setup action will only be run the first time, and its effects
  -- remembered for subsequent executions.
  --
  -- @since 2.0.0.0
  withSetup
    :: Program Basic n x
    -- ^ Setup action
    -> (x -> Program Basic n a)
    -- ^ Main program
    -> Program (WithSetup x) n a
  withSetup setup p = WithSetup
    { wsSetup   = setup
    , wsProgram = p
    }
  
  -- | A concurrent program with some set-up and teardown actions.
  --
  -- This is similar to
  --
  -- @
  -- do
  --   x <- setup
  --   y <- program x
  --   teardown x y
  -- @
  --
  -- But with two differences:
  --
  --   * The setup action can be __snapshotted__, as described for
  --     'withSetup'
  --
  --   * The teardown action will be executed even if the main action
  --     fails to produce a value.
  --
  -- @since 2.0.0.0
  withTeardown
    :: (x -> Either Condition y -> Program Basic n a)
    -- ^ Teardown action
    -> Program (WithSetup x) n y
    -- ^ Main program
    -> Program (WithSetupAndTeardown x y) n a
  withTeardown teardown ws = WithSetupAndTeardown
    { wstSetup    = wsSetup ws
    , wstProgram  = wsProgram ws
    , wstTeardown = teardown
    }
  
  -- | A combination of 'withSetup' and 'withTeardown' for convenience.
  --
  -- @
  -- withSetupAndTeardown setup teardown =
  --   withTeardown teardown . withSetup setup
  -- @
  --
  -- @since 2.0.0.0
  withSetupAndTeardown
    :: Program Basic n x
    -- ^ Setup action
    -> (x -> Either Condition y -> Program Basic n a)
    -- ^ Teardown action
    -> (x -> Program Basic n y)
    -- ^ Main program
    -> Program (WithSetupAndTeardown x y) n a
  withSetupAndTeardown setup teardown =
    withTeardown teardown . withSetup setup
  
  -------------------------------------------------------------------------------
  -- Invariants
  
  -- | Call this in the setup phase to register new invariant which will
  -- be checked after every scheduling point in the main phase.
  -- Invariants are atomic actions which can inspect the shared state of
  -- your computation.
  --
  -- If the invariant throws an exception, the execution will be aborted
  -- with n @InvariantFailure@.  Any teardown action will still be run.
  --
  -- @since 2.0.0.0
  registerInvariant :: Invariant n a -> Program Basic n ()
  registerInvariant inv = ModelConc (\c -> ANewInvariant (void inv) (c ()))
  
  -- | Read the content of an @IORef@.
  --
  -- This returns the globally visible value, which may not be the same
  -- as the value visible to any particular thread when using a memory
  -- model other than 'SequentialConsistency'.
  --
  -- @since 2.0.0.0
  inspectIORef :: ModelIORef n a -> Invariant n a
  inspectIORef = Invariant . IInspectIORef
  
  -- | Read the content of an @MVar@.
  --
  -- This is essentially @tryReadMVar@.
  --
  -- @since 2.0.0.0
  inspectMVar :: ModelMVar n a -> Invariant n (Maybe a)
  inspectMVar = Invariant . IInspectMVar
  
  -- | Read the content of a @TVar@.
  --
  -- This is essentially @readTVar@.
  --
  -- @since 2.0.0.0
  inspectTVar :: ModelTVar n a -> Invariant n a
  inspectTVar = Invariant . IInspectTVar
  