{-# LANGUAGE CPP #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}

-- |
-- Module      : Test.DejaFu.Conc.Internal.Common
-- Copyright   : (c) 2016--2020 Michael Walker
-- License     : MIT
-- Maintainer  : Michael Walker <mike@barrucadu.co.uk>
-- Stability   : experimental
-- Portability : CPP, ExistentialQuantification, GADTs, RankNTypes
--
-- Common types and utility functions for deterministic execution of
-- 'MonadConc' implementations. This module is NOT considered to form
-- part of the public interface of this library.
module Test.DejaFu.Conc.Internal.Common where

import           Control.Exception             (Exception, MaskingState(..))
import           Control.Monad.Catch           (MonadCatch(..), MonadThrow(..))
import qualified Control.Monad.Fail            as Fail
import           Data.Map.Strict               (Map)

import           Test.DejaFu.Conc.Internal.STM (ModelSTM, ModelTVar)
import           Test.DejaFu.Types

--------------------------------------------------------------------------------
-- * Types for Modelling Concurrency

-- | The underlying monad is based on continuations over 'Action's.
--
-- One might wonder why the return type isn't reflected in 'Action',
-- and a free monad formulation used. This would remove the need for a
-- @AStop@ actions having their parameter. However, this makes the
-- current expression of threads and exception handlers very difficult
-- (perhaps even not possible without significant reworking), so I
-- abandoned the attempt.
type ModelConc = Program Basic

-- | A representation of a concurrent program for testing.
--
-- To construct these, use the 'C.MonadConc' instance, or see
-- 'Test.DejaFu.Conc.withSetup', 'Test.DejaFu.Conc.withTeardown', and
-- 'Test.DejaFu.Conc.withSetupAndTeardown'.
--
-- @since 2.0.0.0
data Program pty n a where
  ModelConc ::
    { Program Basic n a -> (a -> Action n) -> Action n
runModelConc :: (a -> Action n) -> Action n
    } -> Program Basic n a
  WithSetup ::
    { Program (WithSetup x) n a -> ModelConc n x
wsSetup   :: ModelConc n x
    , Program (WithSetup x) n a -> x -> ModelConc n a
wsProgram :: x -> ModelConc n a
    } -> Program (WithSetup x) n a
  WithSetupAndTeardown ::
    { Program (WithSetupAndTeardown x y) n a -> ModelConc n x
wstSetup    :: ModelConc n x
    , Program (WithSetupAndTeardown x y) n a -> x -> ModelConc n y
wstProgram  :: x -> ModelConc n y
    , Program (WithSetupAndTeardown x y) n a
-> x -> Either Condition y -> ModelConc n a
wstTeardown :: x -> Either Condition y -> ModelConc n a
    } -> Program (WithSetupAndTeardown x y) n a

-- | A type used to constrain 'Program': a @Program Basic@ is a
-- \"basic\" program with no set-up or teardown.
--
-- Construct with the 'MonadConc' instance.
--
-- @since 2.0.0.0
data Basic

-- | A type used to constrain 'Program': a @Program (WithSetup x)@ is
-- a program with some set-up action producing a value of type @x@.
--
-- Construct with 'Test.DejaFu.Conc.withSetup'.
--
-- @since 2.0.0.0
data WithSetup x

-- | A type used to constrain 'Program': a @Program
-- (WithSetupAndTeardown x y)@ is a program producing a value of type
-- @y@ with some set-up action producing a value of type @x@ and a
-- teardown action producing the final result.
--
-- Construct with 'Test.DejaFu.Conc.withTeardown' or
-- 'Test.DejaFu.Conc.withSetupAndTeardown'.
--
-- @since 2.0.0.0
data WithSetupAndTeardown x y

instance (pty ~ Basic) => Functor (Program pty n) where
  fmap :: (a -> b) -> Program pty n a -> Program pty n b
fmap a -> b
f Program pty n a
m = ((b -> Action n) -> Action n) -> Program Basic n b
forall a (n :: * -> *).
((a -> Action n) -> Action n) -> Program Basic n a
ModelConc (((b -> Action n) -> Action n) -> Program Basic n b)
-> ((b -> Action n) -> Action n) -> Program Basic n b
forall a b. (a -> b) -> a -> b
$ \b -> Action n
c -> Program Basic n a -> (a -> Action n) -> Action n
forall (n :: * -> *) a.
Program Basic n a -> (a -> Action n) -> Action n
runModelConc Program pty n a
Program Basic n a
m (b -> Action n
c (b -> Action n) -> (a -> b) -> a -> Action n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
f)

instance (pty ~ Basic) => Applicative (Program pty n) where
  -- without the @AReturn@, a thread could lock up testing by entering
  -- an infinite loop (eg: @forever (return ())@)
  pure :: a -> Program pty n a
pure a
x  = ((a -> Action n) -> Action n) -> Program Basic n a
forall a (n :: * -> *).
((a -> Action n) -> Action n) -> Program Basic n a
ModelConc (((a -> Action n) -> Action n) -> Program Basic n a)
-> ((a -> Action n) -> Action n) -> Program Basic n a
forall a b. (a -> b) -> a -> b
$ \a -> Action n
c -> Action n -> Action n
forall (n :: * -> *). Action n -> Action n
AReturn (Action n -> Action n) -> Action n -> Action n
forall a b. (a -> b) -> a -> b
$ a -> Action n
c a
x
  Program pty n (a -> b)
f <*> :: Program pty n (a -> b) -> Program pty n a -> Program pty n b
<*> Program pty n a
v = ((b -> Action n) -> Action n) -> Program Basic n b
forall a (n :: * -> *).
((a -> Action n) -> Action n) -> Program Basic n a
ModelConc (((b -> Action n) -> Action n) -> Program Basic n b)
-> ((b -> Action n) -> Action n) -> Program Basic n b
forall a b. (a -> b) -> a -> b
$ \b -> Action n
c -> Program Basic n (a -> b) -> ((a -> b) -> Action n) -> Action n
forall (n :: * -> *) a.
Program Basic n a -> (a -> Action n) -> Action n
runModelConc Program pty n (a -> b)
Program Basic n (a -> b)
f (\a -> b
g -> Program Basic n a -> (a -> Action n) -> Action n
forall (n :: * -> *) a.
Program Basic n a -> (a -> Action n) -> Action n
runModelConc Program pty n a
Program Basic n a
v (b -> Action n
c (b -> Action n) -> (a -> b) -> a -> Action n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
g))

instance (pty ~ Basic) => Monad (Program pty n) where
  return :: a -> Program pty n a
return  = a -> Program pty n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
  Program pty n a
m >>= :: Program pty n a -> (a -> Program pty n b) -> Program pty n b
>>= a -> Program pty n b
k = ((b -> Action n) -> Action n) -> Program Basic n b
forall a (n :: * -> *).
((a -> Action n) -> Action n) -> Program Basic n a
ModelConc (((b -> Action n) -> Action n) -> Program Basic n b)
-> ((b -> Action n) -> Action n) -> Program Basic n b
forall a b. (a -> b) -> a -> b
$ \b -> Action n
c -> Program Basic n a -> (a -> Action n) -> Action n
forall (n :: * -> *) a.
Program Basic n a -> (a -> Action n) -> Action n
runModelConc Program pty n a
Program Basic n a
m (\a
x -> Program Basic n b -> (b -> Action n) -> Action n
forall (n :: * -> *) a.
Program Basic n a -> (a -> Action n) -> Action n
runModelConc (a -> Program pty n b
k a
x) b -> Action n
c)

#if MIN_VERSION_base(4,13,0)
#else
  fail = Fail.fail
#endif

instance (pty ~ Basic) => Fail.MonadFail (Program pty n) where
  fail :: String -> Program pty n a
fail String
e = ((a -> Action n) -> Action n) -> Program Basic n a
forall a (n :: * -> *).
((a -> Action n) -> Action n) -> Program Basic n a
ModelConc (((a -> Action n) -> Action n) -> Program Basic n a)
-> ((a -> Action n) -> Action n) -> Program Basic n a
forall a b. (a -> b) -> a -> b
$ \a -> Action n
_ -> MonadFailException -> Action n
forall (n :: * -> *) e. Exception e => e -> Action n
AThrow (String -> MonadFailException
MonadFailException String
e)

-- | An @MVar@ is modelled as a unique ID and a reference holding a
-- @Maybe@ value.
data ModelMVar n a = ModelMVar
  { ModelMVar n a -> MVarId
mvarId  :: MVarId
  , ModelMVar n a -> Ref n (Maybe a)
mvarRef :: Ref n (Maybe a)
  }

-- | A @IORef@ is modelled as a unique ID and a reference holding
-- thread-local values, the number of commits, and the most recent
-- committed value.
data ModelIORef n a = ModelIORef
  { ModelIORef n a -> IORefId
iorefId  :: IORefId
  , ModelIORef n a -> Ref n (Map ThreadId a, Integer, a)
iorefRef :: Ref n (Map ThreadId a, Integer, a)
  }

-- | A @Ticket@ is modelled as the ID of the @ModelIORef@ it came from,
-- the commits to the @ModelIORef@ at the time it was produced, and the
-- value observed.
data ModelTicket a = ModelTicket
  { ModelTicket a -> IORefId
ticketIORef  :: IORefId
  , ModelTicket a -> Integer
ticketWrites :: Integer
  , ModelTicket a -> a
ticketVal    :: a
  }

--------------------------------------------------------------------------------
-- ** Primitive Actions

-- | Scheduling is done in terms of a trace of 'Action's. Blocking can
-- only occur as a result of an action, and they cover (most of) the
-- primitives of the concurrency. 'spawn' is absent as it is
-- implemented in terms of 'newEmptyMVar', 'fork', and 'putMVar'.
data Action n =
    AFork   String ((forall b. ModelConc n b -> ModelConc n b) -> Action n) (ThreadId -> Action n)
  | AForkOS String ((forall b. ModelConc n b -> ModelConc n b) -> Action n) (ThreadId -> Action n)

  | ASupportsBoundThreads (Bool -> Action n)
  | AIsBound (Bool -> Action n)
  | AMyTId (ThreadId -> Action n)

  | AGetNumCapabilities (Int -> Action n)
  | ASetNumCapabilities Int (Action n)

  | forall a. ANewMVar String (ModelMVar n a -> Action n)
  | forall a. APutMVar     (ModelMVar n a) a (Action n)
  | forall a. ATryPutMVar  (ModelMVar n a) a (Bool -> Action n)
  | forall a. AReadMVar    (ModelMVar n a) (a -> Action n)
  | forall a. ATryReadMVar (ModelMVar n a) (Maybe a -> Action n)
  | forall a. ATakeMVar    (ModelMVar n a) (a -> Action n)
  | forall a. ATryTakeMVar (ModelMVar n a) (Maybe a -> Action n)

  | forall a.   ANewIORef String a (ModelIORef n a -> Action n)
  | forall a.   AReadIORef    (ModelIORef n a) (a -> Action n)
  | forall a.   AReadIORefCas (ModelIORef n a) (ModelTicket a -> Action n)
  | forall a b. AModIORef     (ModelIORef n a) (a -> (a, b)) (b -> Action n)
  | forall a b. AModIORefCas  (ModelIORef n a) (a -> (a, b)) (b -> Action n)
  | forall a.   AWriteIORef   (ModelIORef n a) a (Action n)
  | forall a.   ACasIORef     (ModelIORef n a) (ModelTicket a) a ((Bool, ModelTicket a) -> Action n)

  | forall e.   Exception e => AThrow e
  | forall e.   Exception e => AThrowTo ThreadId e (Action n)
  | forall a e. Exception e => ACatching (e -> ModelConc n a) (ModelConc n a) (a -> Action n)
  | APopCatching (Action n)
  | forall a. AMasking MaskingState ((forall b. ModelConc n b -> ModelConc n b) -> ModelConc n a) (a -> Action n)
  | AResetMask Bool Bool MaskingState (Action n)
  | AGetMasking (MaskingState -> Action n)

  | forall a. AAtom (ModelSTM n a) (a -> Action n)
  | ALift (n (Action n))
  | AYield  (Action n)
  | ADelay Int (Action n)
  | AReturn (Action n)
  | ACommit ThreadId IORefId
  | AStop (n ())

  | ANewInvariant (Invariant n ()) (Action n)

--------------------------------------------------------------------------------
-- ** Scheduling & Traces

-- | Look as far ahead in the given continuation as possible.
lookahead :: Action n -> Lookahead
lookahead :: Action n -> Lookahead
lookahead (AFork String
_ (forall b. ModelConc n b -> ModelConc n b) -> Action n
_ ThreadId -> Action n
_) = Lookahead
WillFork
lookahead (AForkOS String
_ (forall b. ModelConc n b -> ModelConc n b) -> Action n
_ ThreadId -> Action n
_) = Lookahead
WillForkOS
lookahead (ASupportsBoundThreads Bool -> Action n
_) = Lookahead
WillSupportsBoundThreads
lookahead (AIsBound Bool -> Action n
_) = Lookahead
WillIsCurrentThreadBound
lookahead (AMyTId ThreadId -> Action n
_) = Lookahead
WillMyThreadId
lookahead (AGetNumCapabilities Int -> Action n
_) = Lookahead
WillGetNumCapabilities
lookahead (ASetNumCapabilities Int
i Action n
_) = Int -> Lookahead
WillSetNumCapabilities Int
i
lookahead (ANewMVar String
_ ModelMVar n a -> Action n
_) = Lookahead
WillNewMVar
lookahead (APutMVar (ModelMVar MVarId
m Ref n (Maybe a)
_) a
_ Action n
_) = MVarId -> Lookahead
WillPutMVar MVarId
m
lookahead (ATryPutMVar (ModelMVar MVarId
m Ref n (Maybe a)
_) a
_ Bool -> Action n
_) = MVarId -> Lookahead
WillTryPutMVar MVarId
m
lookahead (AReadMVar (ModelMVar MVarId
m Ref n (Maybe a)
_) a -> Action n
_) = MVarId -> Lookahead
WillReadMVar MVarId
m
lookahead (ATryReadMVar (ModelMVar MVarId
m Ref n (Maybe a)
_) Maybe a -> Action n
_) = MVarId -> Lookahead
WillTryReadMVar MVarId
m
lookahead (ATakeMVar (ModelMVar MVarId
m Ref n (Maybe a)
_) a -> Action n
_) = MVarId -> Lookahead
WillTakeMVar MVarId
m
lookahead (ATryTakeMVar (ModelMVar MVarId
m Ref n (Maybe a)
_) Maybe a -> Action n
_) = MVarId -> Lookahead
WillTryTakeMVar MVarId
m
lookahead (ANewIORef String
_ a
_ ModelIORef n a -> Action n
_) = Lookahead
WillNewIORef
lookahead (AReadIORef (ModelIORef IORefId
r Ref n (Map ThreadId a, Integer, a)
_) a -> Action n
_) = IORefId -> Lookahead
WillReadIORef IORefId
r
lookahead (AReadIORefCas (ModelIORef IORefId
r Ref n (Map ThreadId a, Integer, a)
_) ModelTicket a -> Action n
_) = IORefId -> Lookahead
WillReadIORefCas IORefId
r
lookahead (AModIORef (ModelIORef IORefId
r Ref n (Map ThreadId a, Integer, a)
_) a -> (a, b)
_ b -> Action n
_) = IORefId -> Lookahead
WillModIORef IORefId
r
lookahead (AModIORefCas (ModelIORef IORefId
r Ref n (Map ThreadId a, Integer, a)
_) a -> (a, b)
_ b -> Action n
_) = IORefId -> Lookahead
WillModIORefCas IORefId
r
lookahead (AWriteIORef (ModelIORef IORefId
r Ref n (Map ThreadId a, Integer, a)
_) a
_ Action n
_) = IORefId -> Lookahead
WillWriteIORef IORefId
r
lookahead (ACasIORef (ModelIORef IORefId
r Ref n (Map ThreadId a, Integer, a)
_) ModelTicket a
_ a
_ (Bool, ModelTicket a) -> Action n
_) = IORefId -> Lookahead
WillCasIORef IORefId
r
lookahead (ACommit ThreadId
t IORefId
c) = ThreadId -> IORefId -> Lookahead
WillCommitIORef ThreadId
t IORefId
c
lookahead (AAtom ModelSTM n a
_ a -> Action n
_) = Lookahead
WillSTM
lookahead (AThrow e
_) = Lookahead
WillThrow
lookahead (AThrowTo ThreadId
tid e
_ Action n
_) = ThreadId -> Lookahead
WillThrowTo ThreadId
tid
lookahead (ACatching e -> ModelConc n a
_ ModelConc n a
_ a -> Action n
_) = Lookahead
WillCatching
lookahead (APopCatching Action n
_) = Lookahead
WillPopCatching
lookahead (AMasking MaskingState
ms (forall b. ModelConc n b -> ModelConc n b) -> ModelConc n a
_ a -> Action n
_) = Bool -> MaskingState -> Lookahead
WillSetMasking Bool
False MaskingState
ms
lookahead (AResetMask Bool
b1 Bool
b2 MaskingState
ms Action n
_) = (if Bool
b1 then Bool -> MaskingState -> Lookahead
WillSetMasking else Bool -> MaskingState -> Lookahead
WillResetMasking) Bool
b2 MaskingState
ms
lookahead (AGetMasking MaskingState -> Action n
_) = Lookahead
WillGetMaskingState
lookahead (ALift n (Action n)
_) = Lookahead
WillLiftIO
lookahead (AYield Action n
_) = Lookahead
WillYield
lookahead (ADelay Int
n Action n
_) = Int -> Lookahead
WillThreadDelay Int
n
lookahead (AReturn Action n
_) = Lookahead
WillReturn
lookahead (AStop n ()
_) = Lookahead
WillStop
lookahead (ANewInvariant Invariant n ()
_ Action n
_) = Lookahead
WillRegisterInvariant

-------------------------------------------------------------------------------
-- * Invariants

-- | Invariants are atomic actions which can inspect the shared state
-- of your computation, and terminate it on failure.  Invariants have
-- no visible effects, and are checked after each scheduling point.
--
-- To be checked, an invariant must be created during the setup phase
-- of your 'Program', using 'Test.DejaFu.Conc.registerInvariant'.  The
-- invariant will then be checked in the main phase (but not in the
-- setup or teardown phase).  As a consequence of this, any shared
-- state you want your invariant to check must also be created in the
-- setup phase, and passed into the main phase as a parameter.
--
-- @since 2.0.0.0
newtype Invariant n a = Invariant { Invariant n a -> (a -> IAction n) -> IAction n
runInvariant :: (a -> IAction n) -> IAction n }

instance Functor (Invariant n) where
  fmap :: (a -> b) -> Invariant n a -> Invariant n b
fmap a -> b
f Invariant n a
m = ((b -> IAction n) -> IAction n) -> Invariant n b
forall (n :: * -> *) a.
((a -> IAction n) -> IAction n) -> Invariant n a
Invariant (((b -> IAction n) -> IAction n) -> Invariant n b)
-> ((b -> IAction n) -> IAction n) -> Invariant n b
forall a b. (a -> b) -> a -> b
$ \b -> IAction n
c -> Invariant n a -> (a -> IAction n) -> IAction n
forall (n :: * -> *) a.
Invariant n a -> (a -> IAction n) -> IAction n
runInvariant Invariant n a
m (b -> IAction n
c (b -> IAction n) -> (a -> b) -> a -> IAction n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
f)

instance Applicative (Invariant n) where
  pure :: a -> Invariant n a
pure a
x  = ((a -> IAction n) -> IAction n) -> Invariant n a
forall (n :: * -> *) a.
((a -> IAction n) -> IAction n) -> Invariant n a
Invariant (((a -> IAction n) -> IAction n) -> Invariant n a)
-> ((a -> IAction n) -> IAction n) -> Invariant n a
forall a b. (a -> b) -> a -> b
$ \a -> IAction n
c -> a -> IAction n
c a
x
  Invariant n (a -> b)
f <*> :: Invariant n (a -> b) -> Invariant n a -> Invariant n b
<*> Invariant n a
v = ((b -> IAction n) -> IAction n) -> Invariant n b
forall (n :: * -> *) a.
((a -> IAction n) -> IAction n) -> Invariant n a
Invariant (((b -> IAction n) -> IAction n) -> Invariant n b)
-> ((b -> IAction n) -> IAction n) -> Invariant n b
forall a b. (a -> b) -> a -> b
$ \b -> IAction n
c -> Invariant n (a -> b) -> ((a -> b) -> IAction n) -> IAction n
forall (n :: * -> *) a.
Invariant n a -> (a -> IAction n) -> IAction n
runInvariant Invariant n (a -> b)
f (\a -> b
g -> Invariant n a -> (a -> IAction n) -> IAction n
forall (n :: * -> *) a.
Invariant n a -> (a -> IAction n) -> IAction n
runInvariant Invariant n a
v (b -> IAction n
c (b -> IAction n) -> (a -> b) -> a -> IAction n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
g))

instance Monad (Invariant n) where
  return :: a -> Invariant n a
return  = a -> Invariant n a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
  Invariant n a
m >>= :: Invariant n a -> (a -> Invariant n b) -> Invariant n b
>>= a -> Invariant n b
k = ((b -> IAction n) -> IAction n) -> Invariant n b
forall (n :: * -> *) a.
((a -> IAction n) -> IAction n) -> Invariant n a
Invariant (((b -> IAction n) -> IAction n) -> Invariant n b)
-> ((b -> IAction n) -> IAction n) -> Invariant n b
forall a b. (a -> b) -> a -> b
$ \b -> IAction n
c -> Invariant n a -> (a -> IAction n) -> IAction n
forall (n :: * -> *) a.
Invariant n a -> (a -> IAction n) -> IAction n
runInvariant Invariant n a
m (\a
x -> Invariant n b -> (b -> IAction n) -> IAction n
forall (n :: * -> *) a.
Invariant n a -> (a -> IAction n) -> IAction n
runInvariant (a -> Invariant n b
k a
x) b -> IAction n
c)

#if MIN_VERSION_base(4,13,0)
#else
  fail = Fail.fail
#endif

instance Fail.MonadFail (Invariant n) where
  fail :: String -> Invariant n a
fail String
e = ((a -> IAction n) -> IAction n) -> Invariant n a
forall (n :: * -> *) a.
((a -> IAction n) -> IAction n) -> Invariant n a
Invariant (((a -> IAction n) -> IAction n) -> Invariant n a)
-> ((a -> IAction n) -> IAction n) -> Invariant n a
forall a b. (a -> b) -> a -> b
$ \a -> IAction n
_ -> MonadFailException -> IAction n
forall (n :: * -> *) e. Exception e => e -> IAction n
IThrow (String -> MonadFailException
MonadFailException String
e)

instance MonadThrow (Invariant n) where
  throwM :: e -> Invariant n a
throwM e
e = ((a -> IAction n) -> IAction n) -> Invariant n a
forall (n :: * -> *) a.
((a -> IAction n) -> IAction n) -> Invariant n a
Invariant (((a -> IAction n) -> IAction n) -> Invariant n a)
-> ((a -> IAction n) -> IAction n) -> Invariant n a
forall a b. (a -> b) -> a -> b
$ \a -> IAction n
_ -> e -> IAction n
forall (n :: * -> *) e. Exception e => e -> IAction n
IThrow e
e

instance MonadCatch (Invariant n) where
  catch :: Invariant n a -> (e -> Invariant n a) -> Invariant n a
catch Invariant n a
stm e -> Invariant n a
handler = ((a -> IAction n) -> IAction n) -> Invariant n a
forall (n :: * -> *) a.
((a -> IAction n) -> IAction n) -> Invariant n a
Invariant (((a -> IAction n) -> IAction n) -> Invariant n a)
-> ((a -> IAction n) -> IAction n) -> Invariant n a
forall a b. (a -> b) -> a -> b
$ (e -> Invariant n a)
-> Invariant n a -> (a -> IAction n) -> IAction n
forall (n :: * -> *) a e.
Exception e =>
(e -> Invariant n a)
-> Invariant n a -> (a -> IAction n) -> IAction n
ICatch e -> Invariant n a
handler Invariant n a
stm

-- | Invariants are represented as a sequence of primitive actions.
data IAction n
  = forall a. IInspectIORef (ModelIORef n a) (a -> IAction n)
  | forall a. IInspectMVar  (ModelMVar  n a) (Maybe a -> IAction n)
  | forall a. IInspectTVar  (ModelTVar  n a) (a -> IAction n)
  | forall a e. Exception e => ICatch (e -> Invariant n a) (Invariant n a) (a -> IAction n)
  | forall e. Exception e => IThrow e
  | IStop (n ())