{-# LANGUAGE AllowAmbiguousTypes        #-}
{-# LANGUAGE ConstraintKinds            #-}
{-# LANGUAGE DataKinds                  #-}
{-# LANGUAGE DeriveDataTypeable         #-}
{-# LANGUAGE FlexibleContexts           #-}
{-# LANGUAGE FlexibleInstances          #-}
{-# LANGUAGE GADTs                      #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE OverloadedStrings          #-}
{-# LANGUAGE PolyKinds                  #-}
{-# LANGUAGE QuantifiedConstraints      #-}
{-# LANGUAGE RankNTypes                 #-}
{-# LANGUAGE ScopedTypeVariables        #-}
{-# LANGUAGE TemplateHaskell            #-}
{-# LANGUAGE TypeApplications           #-}
{-# LANGUAGE TypeFamilies               #-}
{-# LANGUAGE UndecidableInstances       #-}
{-# OPTIONS_GHC -Wno-redundant-constraints -fno-warn-name-shadowing -fno-warn-unused-do-bind #-}

module Plutus.Contract.Test.ContractModel.CrashTolerance
  ( -- * Extending contract models with a model of
    -- crashing and restarting contracts
    WithCrashTolerance
  , CrashTolerance(..)
  ) where

import Control.Lens
import Control.Monad.State
import Data.Functor.Compose
import Data.Typeable
import Plutus.Contract.Test.ContractModel.Internal
import Plutus.Trace.Effects.EmulatorControl
import Plutus.Trace.Emulator.Types
import Test.QuickCheck as QC

-- | This derived state is used to derive a new `ContractModel` on top of the `state` contract model
-- that also specifies how the contract(s) behave when contract instances crash and restart.
data WithCrashTolerance state = WithCrashTolerance { WithCrashTolerance state -> state
_underlyingModelState   :: state
                                                   , WithCrashTolerance state -> [SomeContractInstanceKey state]
_aliveContractInstances :: [SomeContractInstanceKey state]
                                                   , WithCrashTolerance state -> [SomeContractInstanceKey state]
_deadContractInstances  :: [SomeContractInstanceKey state] }
makeLenses ''WithCrashTolerance

deriving instance ContractModel state => Show (WithCrashTolerance state)
deriving instance (Eq state, ContractModel state) => Eq (WithCrashTolerance state)

class ContractModel state => CrashTolerance state where
  -- | Specifiy what happens when a contract instance crashes
  crash :: SomeContractInstanceKey state -> Spec state ()
  crash SomeContractInstanceKey state
_ = () -> Spec state ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  -- | Specify what happens when a contract instance is restarted
  restart :: SomeContractInstanceKey state -> Spec state ()
  restart SomeContractInstanceKey state
_ = () -> Spec state ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  -- | Specify the arguments to give to a restarted contract
  restartArguments :: ModelState state -> ContractInstanceKey state w s e p -> p
  -- | Check if an action is available given a list of alive
  -- contract instances.
  available :: Action state -> [SomeContractInstanceKey state] -> Bool

instance ContractModel state => Show (Action (WithCrashTolerance state)) where
  showsPrec :: Int -> Action (WithCrashTolerance state) -> ShowS
showsPrec Int
p (Crash cis)          = Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
11) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"Crash " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> SomeContractInstanceKey state -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 SomeContractInstanceKey state
cis
  showsPrec Int
p (Restart cis)        = Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
11) (ShowS -> ShowS) -> ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String -> ShowS
showString String
"Restart " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> SomeContractInstanceKey state -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
11 SomeContractInstanceKey state
cis
  showsPrec Int
p (UnderlyingAction a) = Int -> Action state -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
p Action state
a
deriving instance ContractModel state => Eq (Action (WithCrashTolerance state))

instance {-# OVERLAPPING #-} ContractModel state => HasActions (WithCrashTolerance state) where
  getAllSymtokens :: Action (WithCrashTolerance state) -> Set SymToken
getAllSymtokens (UnderlyingAction a) = Action state -> Set SymToken
forall state. HasActions state => Action state -> Set SymToken
getAllSymtokens Action state
a
  getAllSymtokens Action (WithCrashTolerance state)
_                    = Set SymToken
forall a. Monoid a => a
mempty

deriving instance Show (ContractInstanceKey state w s e p) => Show (ContractInstanceKey (WithCrashTolerance state) w s e p)
deriving instance Eq (ContractInstanceKey state w s e p) => Eq (ContractInstanceKey (WithCrashTolerance state) w s e p)

liftStartContract :: StartContract state -> StartContract (WithCrashTolerance state)
liftStartContract :: StartContract state -> StartContract (WithCrashTolerance state)
liftStartContract (StartContract ContractInstanceKey state w s e p
k p
p) = ContractInstanceKey (WithCrashTolerance state) w s e p
-> p -> StartContract (WithCrashTolerance state)
forall w (s :: Row *) e w state.
(SchemaConstraints w s e, Typeable w) =>
ContractInstanceKey state w s e w -> w -> StartContract state
StartContract (ContractInstanceKey state w s e p
-> ContractInstanceKey (WithCrashTolerance state) w s e p
forall state w (s :: Row *) e p.
ContractInstanceKey state w s e p
-> ContractInstanceKey (WithCrashTolerance state) w s e p
UnderlyingContractInstanceKey ContractInstanceKey state w s e p
k) p
p

instance forall state.
         ( Typeable state
         , Show (ContractInstanceSpec state)
         , Eq (ContractInstanceSpec state)
         , CrashTolerance state) => ContractModel (WithCrashTolerance state) where

  data Action (WithCrashTolerance state) = Crash (SomeContractInstanceKey state)
                                         | Restart (SomeContractInstanceKey state)
                                         | UnderlyingAction (Action state)

  data ContractInstanceKey (WithCrashTolerance state) w s e p where
    UnderlyingContractInstanceKey :: ContractInstanceKey state w s e p -> ContractInstanceKey (WithCrashTolerance state) w s e p

  initialState :: WithCrashTolerance state
initialState = state
-> [SomeContractInstanceKey state]
-> [SomeContractInstanceKey state]
-> WithCrashTolerance state
forall state.
state
-> [SomeContractInstanceKey state]
-> [SomeContractInstanceKey state]
-> WithCrashTolerance state
WithCrashTolerance state
forall state. ContractModel state => state
initialState [ContractInstanceKey state w s e p -> SomeContractInstanceKey state
forall w (s :: Row *) e p state.
(SchemaConstraints w s e, Typeable p) =>
ContractInstanceKey state w s e p -> SomeContractInstanceKey state
Key ContractInstanceKey state w s e p
k | StartContract ContractInstanceKey state w s e p
k p
_ <- ContractModel state => [StartContract state]
forall state. ContractModel state => [StartContract state]
initialInstances @state] []

  initialInstances :: [StartContract (WithCrashTolerance state)]
initialInstances = [ContractInstanceKey (WithCrashTolerance state) w s e p
-> p -> StartContract (WithCrashTolerance state)
forall w (s :: Row *) e w state.
(SchemaConstraints w s e, Typeable w) =>
ContractInstanceKey state w s e w -> w -> StartContract state
StartContract (ContractInstanceKey state w s e p
-> ContractInstanceKey (WithCrashTolerance state) w s e p
forall state w (s :: Row *) e p.
ContractInstanceKey state w s e p
-> ContractInstanceKey (WithCrashTolerance state) w s e p
UnderlyingContractInstanceKey ContractInstanceKey state w s e p
k) p
p | StartContract ContractInstanceKey state w s e p
k p
p <- ContractModel state => [StartContract state]
forall state. ContractModel state => [StartContract state]
initialInstances @state ]

  instanceWallet :: ContractInstanceKey (WithCrashTolerance state) w s e p -> Wallet
instanceWallet (UnderlyingContractInstanceKey k) = ContractInstanceKey state w s e p -> Wallet
forall state w (s :: Row *) e p.
ContractModel state =>
ContractInstanceKey state w s e p -> Wallet
instanceWallet ContractInstanceKey state w s e p
k

  instanceContract :: (SymToken -> AssetClass)
-> ContractInstanceKey (WithCrashTolerance state) w s e p
-> p
-> Contract w s e ()
instanceContract SymToken -> AssetClass
sa (UnderlyingContractInstanceKey k) p
p = (SymToken -> AssetClass)
-> ContractInstanceKey state w s e p -> p -> Contract w s e ()
forall state w (s :: Row *) e p.
ContractModel state =>
(SymToken -> AssetClass)
-> ContractInstanceKey state w s e p -> p -> Contract w s e ()
instanceContract SymToken -> AssetClass
sa ContractInstanceKey state w s e p
k p
p

  -- We piggy-back on the underlying mechanism for starting contract instances that we
  -- get from
  startInstances :: ModelState (WithCrashTolerance state)
-> Action (WithCrashTolerance state)
-> [StartContract (WithCrashTolerance state)]
startInstances ModelState (WithCrashTolerance state)
s (Restart (Key k))    = [ContractInstanceKey (WithCrashTolerance state) w s e p
-> p -> StartContract (WithCrashTolerance state)
forall w (s :: Row *) e w state.
(SchemaConstraints w s e, Typeable w) =>
ContractInstanceKey state w s e w -> w -> StartContract state
StartContract (ContractInstanceKey state w s e p
-> ContractInstanceKey (WithCrashTolerance state) w s e p
forall state w (s :: Row *) e p.
ContractInstanceKey state w s e p
-> ContractInstanceKey (WithCrashTolerance state) w s e p
UnderlyingContractInstanceKey ContractInstanceKey state w s e p
k) (ModelState state -> ContractInstanceKey state w s e p -> p
forall state w (s :: Row *) e p.
CrashTolerance state =>
ModelState state -> ContractInstanceKey state w s e p -> p
restartArguments (WithCrashTolerance state -> state
forall state. WithCrashTolerance state -> state
_underlyingModelState (WithCrashTolerance state -> state)
-> ModelState (WithCrashTolerance state) -> ModelState state
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ModelState (WithCrashTolerance state)
s) ContractInstanceKey state w s e p
k)]
  startInstances ModelState (WithCrashTolerance state)
s (UnderlyingAction a) = StartContract state -> StartContract (WithCrashTolerance state)
forall state.
StartContract state -> StartContract (WithCrashTolerance state)
liftStartContract (StartContract state -> StartContract (WithCrashTolerance state))
-> [StartContract state]
-> [StartContract (WithCrashTolerance state)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ModelState state -> Action state -> [StartContract state]
forall state.
ContractModel state =>
ModelState state -> Action state -> [StartContract state]
startInstances (WithCrashTolerance state -> state
forall state. WithCrashTolerance state -> state
_underlyingModelState (WithCrashTolerance state -> state)
-> ModelState (WithCrashTolerance state) -> ModelState state
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ModelState (WithCrashTolerance state)
s) Action state
a
  startInstances ModelState (WithCrashTolerance state)
_ Action (WithCrashTolerance state)
_                    = []

  perform :: HandleFun (WithCrashTolerance state)
-> (SymToken -> AssetClass)
-> ModelState (WithCrashTolerance state)
-> Action (WithCrashTolerance state)
-> SpecificationEmulatorTrace ()
perform HandleFun (WithCrashTolerance state)
h SymToken -> AssetClass
t ModelState (WithCrashTolerance state)
s Action (WithCrashTolerance state)
a = case Action (WithCrashTolerance state)
a of
    Crash (Key key) -> do
      -- I'm not sure why this has to take two slots but if you don't make it take
      -- two slots the crash doesn't happen if its the first action
      Integer -> SpecificationEmulatorTrace ()
delay Integer
1
      -- This turns out to be enough. Restarting a contract instance overrides the handle
      -- for the contract instance and the existing instance becomes garbage. This does
      -- leak memory, but only relatively little and only during a test.
      ContractInstanceId -> SpecificationEmulatorTrace ()
forall (effs :: [* -> *]).
Member EmulatorControl effs =>
ContractInstanceId -> Eff effs ()
freezeContractInstance (ContractInstanceId -> SpecificationEmulatorTrace ())
-> (ContractHandle w s e -> ContractInstanceId)
-> ContractHandle w s e
-> SpecificationEmulatorTrace ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ContractHandle w s e -> ContractInstanceId
forall w (s :: Row *) e. ContractHandle w s e -> ContractInstanceId
chInstanceId (ContractHandle w s e -> SpecificationEmulatorTrace ())
-> ContractHandle w s e -> SpecificationEmulatorTrace ()
forall a b. (a -> b) -> a -> b
$ ContractInstanceKey (WithCrashTolerance state) w s e p
-> ContractHandle w s e
HandleFun (WithCrashTolerance state)
h (ContractInstanceKey state w s e p
-> ContractInstanceKey (WithCrashTolerance state) w s e p
forall state w (s :: Row *) e p.
ContractInstanceKey state w s e p
-> ContractInstanceKey (WithCrashTolerance state) w s e p
UnderlyingContractInstanceKey ContractInstanceKey state w s e p
key)
      Integer -> SpecificationEmulatorTrace ()
delay Integer
1
    Restart _ -> do
      Integer -> SpecificationEmulatorTrace ()
delay Integer
1
    UnderlyingAction a -> do
      HandleFun state
-> (SymToken -> AssetClass)
-> ModelState state
-> Action state
-> SpecificationEmulatorTrace ()
forall state.
ContractModel state =>
HandleFun state
-> (SymToken -> AssetClass)
-> ModelState state
-> Action state
-> SpecificationEmulatorTrace ()
perform (ContractInstanceKey (WithCrashTolerance state) w schema err params
-> ContractHandle w schema err
HandleFun (WithCrashTolerance state)
h (ContractInstanceKey (WithCrashTolerance state) w schema err params
 -> ContractHandle w schema err)
-> (ContractInstanceKey state w schema err params
    -> ContractInstanceKey
         (WithCrashTolerance state) w schema err params)
-> ContractInstanceKey state w schema err params
-> ContractHandle w schema err
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ContractInstanceKey state w schema err params
-> ContractInstanceKey
     (WithCrashTolerance state) w schema err params
forall state w (s :: Row *) e p.
ContractInstanceKey state w s e p
-> ContractInstanceKey (WithCrashTolerance state) w s e p
UnderlyingContractInstanceKey) SymToken -> AssetClass
t (WithCrashTolerance state -> state
forall state. WithCrashTolerance state -> state
_underlyingModelState (WithCrashTolerance state -> state)
-> ModelState (WithCrashTolerance state) -> ModelState state
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ModelState (WithCrashTolerance state)
s) Action state
a

  precondition :: ModelState (WithCrashTolerance state)
-> Action (WithCrashTolerance state) -> Bool
precondition ModelState (WithCrashTolerance state)
s Action (WithCrashTolerance state)
a = case Action (WithCrashTolerance state)
a of
    -- Only crash alive contract instances
    Crash cis -> SomeContractInstanceKey state
cis SomeContractInstanceKey state
-> [SomeContractInstanceKey state] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` (ModelState (WithCrashTolerance state)
s ModelState (WithCrashTolerance state)
-> Getting
     [SomeContractInstanceKey state]
     (ModelState (WithCrashTolerance state))
     [SomeContractInstanceKey state]
-> [SomeContractInstanceKey state]
forall s a. s -> Getting a s a -> a
^. (WithCrashTolerance state
 -> Const
      [SomeContractInstanceKey state] (WithCrashTolerance state))
-> ModelState (WithCrashTolerance state)
-> Const
     [SomeContractInstanceKey state]
     (ModelState (WithCrashTolerance state))
forall state1 state2.
Lens (ModelState state1) (ModelState state2) state1 state2
contractState ((WithCrashTolerance state
  -> Const
       [SomeContractInstanceKey state] (WithCrashTolerance state))
 -> ModelState (WithCrashTolerance state)
 -> Const
      [SomeContractInstanceKey state]
      (ModelState (WithCrashTolerance state)))
-> (([SomeContractInstanceKey state]
     -> Const
          [SomeContractInstanceKey state] [SomeContractInstanceKey state])
    -> WithCrashTolerance state
    -> Const
         [SomeContractInstanceKey state] (WithCrashTolerance state))
-> Getting
     [SomeContractInstanceKey state]
     (ModelState (WithCrashTolerance state))
     [SomeContractInstanceKey state]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([SomeContractInstanceKey state]
 -> Const
      [SomeContractInstanceKey state] [SomeContractInstanceKey state])
-> WithCrashTolerance state
-> Const [SomeContractInstanceKey state] (WithCrashTolerance state)
forall state.
Lens' (WithCrashTolerance state) [SomeContractInstanceKey state]
aliveContractInstances)
    -- Only restart dead contract instances
    Restart cis -> SomeContractInstanceKey state
cis SomeContractInstanceKey state
-> [SomeContractInstanceKey state] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` (ModelState (WithCrashTolerance state)
s ModelState (WithCrashTolerance state)
-> Getting
     [SomeContractInstanceKey state]
     (ModelState (WithCrashTolerance state))
     [SomeContractInstanceKey state]
-> [SomeContractInstanceKey state]
forall s a. s -> Getting a s a -> a
^. (WithCrashTolerance state
 -> Const
      [SomeContractInstanceKey state] (WithCrashTolerance state))
-> ModelState (WithCrashTolerance state)
-> Const
     [SomeContractInstanceKey state]
     (ModelState (WithCrashTolerance state))
forall state1 state2.
Lens (ModelState state1) (ModelState state2) state1 state2
contractState ((WithCrashTolerance state
  -> Const
       [SomeContractInstanceKey state] (WithCrashTolerance state))
 -> ModelState (WithCrashTolerance state)
 -> Const
      [SomeContractInstanceKey state]
      (ModelState (WithCrashTolerance state)))
-> (([SomeContractInstanceKey state]
     -> Const
          [SomeContractInstanceKey state] [SomeContractInstanceKey state])
    -> WithCrashTolerance state
    -> Const
         [SomeContractInstanceKey state] (WithCrashTolerance state))
-> Getting
     [SomeContractInstanceKey state]
     (ModelState (WithCrashTolerance state))
     [SomeContractInstanceKey state]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([SomeContractInstanceKey state]
 -> Const
      [SomeContractInstanceKey state] [SomeContractInstanceKey state])
-> WithCrashTolerance state
-> Const [SomeContractInstanceKey state] (WithCrashTolerance state)
forall state.
Lens' (WithCrashTolerance state) [SomeContractInstanceKey state]
deadContractInstances)
    -- Run an underlying action if its available
    UnderlyingAction a -> ModelState state -> Action state -> Bool
forall state.
ContractModel state =>
ModelState state -> Action state -> Bool
precondition (WithCrashTolerance state -> state
forall state. WithCrashTolerance state -> state
_underlyingModelState (WithCrashTolerance state -> state)
-> ModelState (WithCrashTolerance state) -> ModelState state
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ModelState (WithCrashTolerance state)
s) Action state
a
                       Bool -> Bool -> Bool
&& Action state -> [SomeContractInstanceKey state] -> Bool
forall state.
CrashTolerance state =>
Action state -> [SomeContractInstanceKey state] -> Bool
available Action state
a (ModelState (WithCrashTolerance state)
s ModelState (WithCrashTolerance state)
-> Getting
     [SomeContractInstanceKey state]
     (ModelState (WithCrashTolerance state))
     [SomeContractInstanceKey state]
-> [SomeContractInstanceKey state]
forall s a. s -> Getting a s a -> a
^. (WithCrashTolerance state
 -> Const
      [SomeContractInstanceKey state] (WithCrashTolerance state))
-> ModelState (WithCrashTolerance state)
-> Const
     [SomeContractInstanceKey state]
     (ModelState (WithCrashTolerance state))
forall state1 state2.
Lens (ModelState state1) (ModelState state2) state1 state2
contractState ((WithCrashTolerance state
  -> Const
       [SomeContractInstanceKey state] (WithCrashTolerance state))
 -> ModelState (WithCrashTolerance state)
 -> Const
      [SomeContractInstanceKey state]
      (ModelState (WithCrashTolerance state)))
-> (([SomeContractInstanceKey state]
     -> Const
          [SomeContractInstanceKey state] [SomeContractInstanceKey state])
    -> WithCrashTolerance state
    -> Const
         [SomeContractInstanceKey state] (WithCrashTolerance state))
-> Getting
     [SomeContractInstanceKey state]
     (ModelState (WithCrashTolerance state))
     [SomeContractInstanceKey state]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([SomeContractInstanceKey state]
 -> Const
      [SomeContractInstanceKey state] [SomeContractInstanceKey state])
-> WithCrashTolerance state
-> Const [SomeContractInstanceKey state] (WithCrashTolerance state)
forall state.
Lens' (WithCrashTolerance state) [SomeContractInstanceKey state]
aliveContractInstances)

  nextState :: Action (WithCrashTolerance state)
-> Spec (WithCrashTolerance state) ()
nextState Action (WithCrashTolerance state)
a = case Action (WithCrashTolerance state)
a of
    Crash cis -> do
      Spec state () -> Spec (WithCrashTolerance state) ()
forall a. Spec state a -> Spec (WithCrashTolerance state) a
embed (Spec state () -> Spec (WithCrashTolerance state) ())
-> Spec state () -> Spec (WithCrashTolerance state) ()
forall a b. (a -> b) -> a -> b
$ SomeContractInstanceKey state -> Spec state ()
forall state.
CrashTolerance state =>
SomeContractInstanceKey state -> Spec state ()
crash SomeContractInstanceKey state
cis
      ([SomeContractInstanceKey state]
 -> Identity [SomeContractInstanceKey state])
-> WithCrashTolerance state -> Identity (WithCrashTolerance state)
forall state.
Lens' (WithCrashTolerance state) [SomeContractInstanceKey state]
deadContractInstances (([SomeContractInstanceKey state]
  -> Identity [SomeContractInstanceKey state])
 -> WithCrashTolerance state -> Identity (WithCrashTolerance state))
-> ([SomeContractInstanceKey state]
    -> [SomeContractInstanceKey state])
-> Spec (WithCrashTolerance state) ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= (SomeContractInstanceKey state
cisSomeContractInstanceKey state
-> [SomeContractInstanceKey state]
-> [SomeContractInstanceKey state]
forall a. a -> [a] -> [a]
:)
      ([SomeContractInstanceKey state]
 -> Identity [SomeContractInstanceKey state])
-> WithCrashTolerance state -> Identity (WithCrashTolerance state)
forall state.
Lens' (WithCrashTolerance state) [SomeContractInstanceKey state]
aliveContractInstances (([SomeContractInstanceKey state]
  -> Identity [SomeContractInstanceKey state])
 -> WithCrashTolerance state -> Identity (WithCrashTolerance state))
-> ([SomeContractInstanceKey state]
    -> [SomeContractInstanceKey state])
-> Spec (WithCrashTolerance state) ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= (SomeContractInstanceKey state -> Bool)
-> [SomeContractInstanceKey state]
-> [SomeContractInstanceKey state]
forall a. (a -> Bool) -> [a] -> [a]
filter (SomeContractInstanceKey state
-> SomeContractInstanceKey state -> Bool
forall a. Eq a => a -> a -> Bool
/=SomeContractInstanceKey state
cis)
      Integer -> Spec (WithCrashTolerance state) ()
forall state. ContractModel state => Integer -> Spec state ()
wait Integer
2
    Restart cis -> do
      Spec state () -> Spec (WithCrashTolerance state) ()
forall a. Spec state a -> Spec (WithCrashTolerance state) a
embed (Spec state () -> Spec (WithCrashTolerance state) ())
-> Spec state () -> Spec (WithCrashTolerance state) ()
forall a b. (a -> b) -> a -> b
$ SomeContractInstanceKey state -> Spec state ()
forall state.
CrashTolerance state =>
SomeContractInstanceKey state -> Spec state ()
restart SomeContractInstanceKey state
cis
      ([SomeContractInstanceKey state]
 -> Identity [SomeContractInstanceKey state])
-> WithCrashTolerance state -> Identity (WithCrashTolerance state)
forall state.
Lens' (WithCrashTolerance state) [SomeContractInstanceKey state]
deadContractInstances (([SomeContractInstanceKey state]
  -> Identity [SomeContractInstanceKey state])
 -> WithCrashTolerance state -> Identity (WithCrashTolerance state))
-> ([SomeContractInstanceKey state]
    -> [SomeContractInstanceKey state])
-> Spec (WithCrashTolerance state) ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= (SomeContractInstanceKey state -> Bool)
-> [SomeContractInstanceKey state]
-> [SomeContractInstanceKey state]
forall a. (a -> Bool) -> [a] -> [a]
filter (SomeContractInstanceKey state
-> SomeContractInstanceKey state -> Bool
forall a. Eq a => a -> a -> Bool
/=SomeContractInstanceKey state
cis)
      ([SomeContractInstanceKey state]
 -> Identity [SomeContractInstanceKey state])
-> WithCrashTolerance state -> Identity (WithCrashTolerance state)
forall state.
Lens' (WithCrashTolerance state) [SomeContractInstanceKey state]
aliveContractInstances (([SomeContractInstanceKey state]
  -> Identity [SomeContractInstanceKey state])
 -> WithCrashTolerance state -> Identity (WithCrashTolerance state))
-> ([SomeContractInstanceKey state]
    -> [SomeContractInstanceKey state])
-> Spec (WithCrashTolerance state) ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= (SomeContractInstanceKey state
cisSomeContractInstanceKey state
-> [SomeContractInstanceKey state]
-> [SomeContractInstanceKey state]
forall a. a -> [a] -> [a]
:)
      Integer -> Spec (WithCrashTolerance state) ()
forall state. ContractModel state => Integer -> Spec state ()
wait Integer
1
    UnderlyingAction a -> do
      Spec state () -> Spec (WithCrashTolerance state) ()
forall a. Spec state a -> Spec (WithCrashTolerance state) a
embed (Spec state () -> Spec (WithCrashTolerance state) ())
-> Spec state () -> Spec (WithCrashTolerance state) ()
forall a b. (a -> b) -> a -> b
$ Action state -> Spec state ()
forall state. ContractModel state => Action state -> Spec state ()
nextState Action state
a
      ModelState (WithCrashTolerance state)
s <- WriterT
  [SymToken]
  (ReaderT
     (Var AssetKey) (State (ModelState (WithCrashTolerance state))))
  (ModelState (WithCrashTolerance state))
-> Spec
     (WithCrashTolerance state) (ModelState (WithCrashTolerance state))
forall state a.
WriterT
  [SymToken] (ReaderT (Var AssetKey) (State (ModelState state))) a
-> Spec state a
Spec WriterT
  [SymToken]
  (ReaderT
     (Var AssetKey) (State (ModelState (WithCrashTolerance state))))
  (ModelState (WithCrashTolerance state))
forall s (m :: * -> *). MonadState s m => m s
get
      -- An action may start its own contract instances and we need to keep track of them
      ([SomeContractInstanceKey state]
 -> Identity [SomeContractInstanceKey state])
-> WithCrashTolerance state -> Identity (WithCrashTolerance state)
forall state.
Lens' (WithCrashTolerance state) [SomeContractInstanceKey state]
aliveContractInstances (([SomeContractInstanceKey state]
  -> Identity [SomeContractInstanceKey state])
 -> WithCrashTolerance state -> Identity (WithCrashTolerance state))
-> ([SomeContractInstanceKey state]
    -> [SomeContractInstanceKey state])
-> Spec (WithCrashTolerance state) ()
forall s (m :: * -> *) a b.
MonadState s m =>
ASetter s s a b -> (a -> b) -> m ()
%= ([ContractInstanceKey state w s e p -> SomeContractInstanceKey state
forall w (s :: Row *) e p state.
(SchemaConstraints w s e, Typeable p) =>
ContractInstanceKey state w s e p -> SomeContractInstanceKey state
Key ContractInstanceKey state w s e p
k | StartContract (UnderlyingContractInstanceKey k) p
_ <- ModelState (WithCrashTolerance state)
-> Action (WithCrashTolerance state)
-> [StartContract (WithCrashTolerance state)]
forall state.
ContractModel state =>
ModelState state -> Action state -> [StartContract state]
startInstances ModelState (WithCrashTolerance state)
s (Action state -> Action (WithCrashTolerance state)
forall state. Action state -> Action (WithCrashTolerance state)
UnderlyingAction Action state
a)] [SomeContractInstanceKey state]
-> [SomeContractInstanceKey state]
-> [SomeContractInstanceKey state]
forall a. [a] -> [a] -> [a]
++)
    where
      embed :: Spec state a -> Spec (WithCrashTolerance state) a
      embed :: Spec state a -> Spec (WithCrashTolerance state) a
embed (Spec WriterT
  [SymToken] (ReaderT (Var AssetKey) (State (ModelState state))) a
comp) = WriterT
  [SymToken]
  (ReaderT
     (Var AssetKey) (State (ModelState (WithCrashTolerance state))))
  a
-> Spec (WithCrashTolerance state) a
forall state a.
WriterT
  [SymToken] (ReaderT (Var AssetKey) (State (ModelState state))) a
-> Spec state a
Spec (LensLike'
  (Zoomed
     (WriterT
        [SymToken] (ReaderT (Var AssetKey) (State (ModelState state))))
     a)
  (ModelState (WithCrashTolerance state))
  (ModelState state)
-> WriterT
     [SymToken] (ReaderT (Var AssetKey) (State (ModelState state))) a
-> WriterT
     [SymToken]
     (ReaderT
        (Var AssetKey) (State (ModelState (WithCrashTolerance state))))
     a
forall (m :: * -> *) (n :: * -> *) s t c.
Zoom m n s t =>
LensLike' (Zoomed m c) t s -> m c -> n c
zoom ((forall a. ModelState a -> a)
-> Lens' (WithCrashTolerance state) state
-> Lens' (ModelState (WithCrashTolerance state)) (ModelState state)
forall (t :: * -> *) s a.
Functor t =>
(forall a. t a -> a) -> Lens' s a -> Lens' (t s) (t a)
liftL forall a. ModelState a -> a
_contractState forall state. Lens' (WithCrashTolerance state) state
Lens' (WithCrashTolerance state) state
underlyingModelState) WriterT
  [SymToken] (ReaderT (Var AssetKey) (State (ModelState state))) a
comp)

  arbitraryAction :: ModelState (WithCrashTolerance state)
-> Gen (Action (WithCrashTolerance state))
arbitraryAction ModelState (WithCrashTolerance state)
s = [(Int, Gen (Action (WithCrashTolerance state)))]
-> Gen (Action (WithCrashTolerance state))
forall a. [(Int, Gen a)] -> Gen a
frequency [ (Int
10, Action state -> Action (WithCrashTolerance state)
forall state. Action state -> Action (WithCrashTolerance state)
UnderlyingAction (Action state -> Action (WithCrashTolerance state))
-> Gen (Action state) -> Gen (Action (WithCrashTolerance state))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ModelState state -> Gen (Action state)
forall state.
ContractModel state =>
ModelState state -> Gen (Action state)
arbitraryAction (WithCrashTolerance state -> state
forall state. WithCrashTolerance state -> state
_underlyingModelState (WithCrashTolerance state -> state)
-> ModelState (WithCrashTolerance state) -> ModelState state
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ModelState (WithCrashTolerance state)
s))
                                , (Int
1, SomeContractInstanceKey state -> Action (WithCrashTolerance state)
forall state.
SomeContractInstanceKey state -> Action (WithCrashTolerance state)
Crash (SomeContractInstanceKey state
 -> Action (WithCrashTolerance state))
-> Gen (SomeContractInstanceKey state)
-> Gen (Action (WithCrashTolerance state))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SomeContractInstanceKey state]
-> Gen (SomeContractInstanceKey state)
forall a. [a] -> Gen a
QC.elements (ModelState (WithCrashTolerance state)
s ModelState (WithCrashTolerance state)
-> Getting
     [SomeContractInstanceKey state]
     (ModelState (WithCrashTolerance state))
     [SomeContractInstanceKey state]
-> [SomeContractInstanceKey state]
forall s a. s -> Getting a s a -> a
^. (WithCrashTolerance state
 -> Const
      [SomeContractInstanceKey state] (WithCrashTolerance state))
-> ModelState (WithCrashTolerance state)
-> Const
     [SomeContractInstanceKey state]
     (ModelState (WithCrashTolerance state))
forall state1 state2.
Lens (ModelState state1) (ModelState state2) state1 state2
contractState ((WithCrashTolerance state
  -> Const
       [SomeContractInstanceKey state] (WithCrashTolerance state))
 -> ModelState (WithCrashTolerance state)
 -> Const
      [SomeContractInstanceKey state]
      (ModelState (WithCrashTolerance state)))
-> (([SomeContractInstanceKey state]
     -> Const
          [SomeContractInstanceKey state] [SomeContractInstanceKey state])
    -> WithCrashTolerance state
    -> Const
         [SomeContractInstanceKey state] (WithCrashTolerance state))
-> Getting
     [SomeContractInstanceKey state]
     (ModelState (WithCrashTolerance state))
     [SomeContractInstanceKey state]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([SomeContractInstanceKey state]
 -> Const
      [SomeContractInstanceKey state] [SomeContractInstanceKey state])
-> WithCrashTolerance state
-> Const [SomeContractInstanceKey state] (WithCrashTolerance state)
forall state.
Lens' (WithCrashTolerance state) [SomeContractInstanceKey state]
aliveContractInstances))
                                , (Int
1, SomeContractInstanceKey state -> Action (WithCrashTolerance state)
forall state.
SomeContractInstanceKey state -> Action (WithCrashTolerance state)
Restart (SomeContractInstanceKey state
 -> Action (WithCrashTolerance state))
-> Gen (SomeContractInstanceKey state)
-> Gen (Action (WithCrashTolerance state))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [SomeContractInstanceKey state]
-> Gen (SomeContractInstanceKey state)
forall a. [a] -> Gen a
QC.elements (ModelState (WithCrashTolerance state)
s ModelState (WithCrashTolerance state)
-> Getting
     [SomeContractInstanceKey state]
     (ModelState (WithCrashTolerance state))
     [SomeContractInstanceKey state]
-> [SomeContractInstanceKey state]
forall s a. s -> Getting a s a -> a
^. (WithCrashTolerance state
 -> Const
      [SomeContractInstanceKey state] (WithCrashTolerance state))
-> ModelState (WithCrashTolerance state)
-> Const
     [SomeContractInstanceKey state]
     (ModelState (WithCrashTolerance state))
forall state1 state2.
Lens (ModelState state1) (ModelState state2) state1 state2
contractState ((WithCrashTolerance state
  -> Const
       [SomeContractInstanceKey state] (WithCrashTolerance state))
 -> ModelState (WithCrashTolerance state)
 -> Const
      [SomeContractInstanceKey state]
      (ModelState (WithCrashTolerance state)))
-> (([SomeContractInstanceKey state]
     -> Const
          [SomeContractInstanceKey state] [SomeContractInstanceKey state])
    -> WithCrashTolerance state
    -> Const
         [SomeContractInstanceKey state] (WithCrashTolerance state))
-> Getting
     [SomeContractInstanceKey state]
     (ModelState (WithCrashTolerance state))
     [SomeContractInstanceKey state]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([SomeContractInstanceKey state]
 -> Const
      [SomeContractInstanceKey state] [SomeContractInstanceKey state])
-> WithCrashTolerance state
-> Const [SomeContractInstanceKey state] (WithCrashTolerance state)
forall state.
Lens' (WithCrashTolerance state) [SomeContractInstanceKey state]
deadContractInstances)) ]

  shrinkAction :: ModelState (WithCrashTolerance state)
-> Action (WithCrashTolerance state)
-> [Action (WithCrashTolerance state)]
shrinkAction ModelState (WithCrashTolerance state)
s (UnderlyingAction a) = Action state -> Action (WithCrashTolerance state)
forall state. Action state -> Action (WithCrashTolerance state)
UnderlyingAction (Action state -> Action (WithCrashTolerance state))
-> [Action state] -> [Action (WithCrashTolerance state)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ModelState state -> Action state -> [Action state]
forall state.
ContractModel state =>
ModelState state -> Action state -> [Action state]
shrinkAction (WithCrashTolerance state -> state
forall state. WithCrashTolerance state -> state
_underlyingModelState (WithCrashTolerance state -> state)
-> ModelState (WithCrashTolerance state) -> ModelState state
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ModelState (WithCrashTolerance state)
s) Action state
a
  shrinkAction ModelState (WithCrashTolerance state)
_ Action (WithCrashTolerance state)
_                    = []

liftL :: Functor t => (forall a. t a -> a) -> Lens' s a -> Lens' (t s) (t a)
liftL :: (forall a. t a -> a) -> Lens' s a -> Lens' (t s) (t a)
liftL forall a. t a -> a
extr Lens' s a
l t a -> f (t a)
ft t s
ts = Compose f t s -> f (t s)
forall k1 (f :: k1 -> *) k2 (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose (Compose f t s -> f (t s)) -> (s -> Compose f t s) -> s -> f (t s)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Compose f t a) -> s -> Compose f t s
Lens' s a
l (f (t a) -> Compose f t a
forall k k1 (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (f (t a) -> Compose f t a) -> (a -> f (t a)) -> a -> Compose f t a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. t a -> f (t a)
ft (t a -> f (t a)) -> (a -> t a) -> a -> f (t a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> t s -> t a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ t s
ts)) (s -> f (t s)) -> s -> f (t s)
forall a b. (a -> b) -> a -> b
$ t s -> s
forall a. t a -> a
extr t s
ts