{-# 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 -Wno-orphans #-}

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.Set (Set)
import Data.Typeable
import Plutus.Contract.Test.ContractModel
import Plutus.Trace.Effects.EmulatorControl
import Plutus.Trace.Emulator.Types
import Test.QuickCheck as QC
import Test.QuickCheck.StateModel qualified as QCSM

-- | 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] }
                                                   deriving (forall x.
 WithCrashTolerance state -> Rep (WithCrashTolerance state) x)
-> (forall x.
    Rep (WithCrashTolerance state) x -> WithCrashTolerance state)
-> Generic (WithCrashTolerance state)
forall x.
Rep (WithCrashTolerance state) x -> WithCrashTolerance state
forall x.
WithCrashTolerance state -> Rep (WithCrashTolerance state) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall state x.
Rep (WithCrashTolerance state) x -> WithCrashTolerance state
forall state x.
WithCrashTolerance state -> Rep (WithCrashTolerance state) x
$cto :: forall state x.
Rep (WithCrashTolerance state) x -> WithCrashTolerance state
$cfrom :: forall state x.
WithCrashTolerance state -> Rep (WithCrashTolerance state) x
Generic
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
  -- | If your `ContractInstanceKey`s contain symbolic tokens or
  -- symbolic variables you **MUST** implement this function.
  contractInstanceVariables :: ContractInstanceKey state w s e p -> Set (QCSM.Any QCSM.Var)
  contractInstanceVariables ContractInstanceKey state w s e p
_ = Set (Any Var)
forall a. Monoid a => a
mempty

instance CrashTolerance state => QCSM.HasVariables (SomeContractInstanceKey state) where
  getAllVariables :: SomeContractInstanceKey state -> Set (Any Var)
getAllVariables (Key ContractInstanceKey state w s e p
k) = ContractInstanceKey state w s e p -> Set (Any Var)
forall state w (s :: Row *) e p.
CrashTolerance state =>
ContractInstanceKey state w s e p -> Set (Any Var)
contractInstanceVariables ContractInstanceKey state w s e p
k

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 => HasSymbolics (Action (WithCrashTolerance state)) where
  getAllSymbolics :: Action (WithCrashTolerance state) -> SymCollectionIndex
getAllSymbolics (UnderlyingAction a) = Action state -> SymCollectionIndex
forall a. HasSymbolics a => a -> SymCollectionIndex
getAllSymbolics Action state
a
  getAllSymbolics Action (WithCrashTolerance state)
_                    = SymCollectionIndex
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 p state.
(SchemaConstraints w s e, Typeable p) =>
ContractInstanceKey state w s e p -> p -> 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
         , CrashTolerance state) => ContractModel (WithCrashTolerance state) where

  data Action (WithCrashTolerance state) = Crash (SomeContractInstanceKey state)
                                         | Restart (SomeContractInstanceKey state)
                                         | UnderlyingAction (Action state)
                                         deriving (forall x.
 Action (WithCrashTolerance state)
 -> Rep (Action (WithCrashTolerance state)) x)
-> (forall x.
    Rep (Action (WithCrashTolerance state)) x
    -> Action (WithCrashTolerance state))
-> Generic (Action (WithCrashTolerance state))
forall x.
Rep (Action (WithCrashTolerance state)) x
-> Action (WithCrashTolerance state)
forall x.
Action (WithCrashTolerance state)
-> Rep (Action (WithCrashTolerance state)) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall state x.
Rep (Action (WithCrashTolerance state)) x
-> Action (WithCrashTolerance state)
forall state x.
Action (WithCrashTolerance state)
-> Rep (Action (WithCrashTolerance state)) x
$cto :: forall state x.
Rep (Action (WithCrashTolerance state)) x
-> Action (WithCrashTolerance state)
$cfrom :: forall state x.
Action (WithCrashTolerance state)
-> Rep (Action (WithCrashTolerance state)) x
Generic

  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 p state.
(SchemaConstraints w s e, Typeable p) =>
ContractInstanceKey state w s e p -> p -> 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 :: (forall t. HasSymbolicRep t => Symbolic t -> t)
-> ContractInstanceKey (WithCrashTolerance state) w s e p
-> p
-> Contract w s e ()
instanceContract forall t. HasSymbolicRep t => Symbolic t -> t
sa (UnderlyingContractInstanceKey k) p
p = (forall t. HasSymbolicRep t => Symbolic t -> t)
-> ContractInstanceKey state w s e p -> p -> Contract w s e ()
forall state w (s :: Row *) e p.
ContractModel state =>
(forall t. HasSymbolicRep t => Symbolic t -> t)
-> ContractInstanceKey state w s e p -> p -> Contract w s e ()
instanceContract forall t. HasSymbolicRep t => Symbolic t -> t
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 p state.
(SchemaConstraints w s e, Typeable p) =>
ContractInstanceKey state w s e p -> p -> 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)
-> (forall t. HasSymbolicRep t => Symbolic t -> t)
-> ModelState (WithCrashTolerance state)
-> Action (WithCrashTolerance state)
-> SpecificationEmulatorTrace ()
perform HandleFun (WithCrashTolerance state)
h forall t. HasSymbolicRep t => Symbolic t -> t
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
-> (forall t. HasSymbolicRep t => Symbolic t -> t)
-> ModelState state
-> Action state
-> SpecificationEmulatorTrace ()
forall state.
ContractModel state =>
HandleFun state
-> (forall t. HasSymbolicRep t => Symbolic t -> t)
-> 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) forall t. HasSymbolicRep t => Symbolic t -> t
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 state 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 state 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 state 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
  SymCreationIndex
  (ReaderT
     (Var SymIndex) (State (ModelState (WithCrashTolerance state))))
  (ModelState (WithCrashTolerance state))
-> Spec
     (WithCrashTolerance state) (ModelState (WithCrashTolerance state))
forall state a.
WriterT
  SymCreationIndex
  (ReaderT (Var SymIndex) (State (ModelState state)))
  a
-> Spec state a
Spec WriterT
  SymCreationIndex
  (ReaderT
     (Var SymIndex) (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

  nextReactiveState :: Slot -> Spec (WithCrashTolerance state) ()
nextReactiveState Slot
slot = Spec state () -> Spec (WithCrashTolerance state) ()
forall state 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
$ Slot -> Spec state ()
forall state. ContractModel state => Slot -> Spec state ()
nextReactiveState Slot
slot

  monitoring :: (ModelState (WithCrashTolerance state),
 ModelState (WithCrashTolerance state))
-> Action (WithCrashTolerance state) -> Property -> Property
monitoring (ModelState (WithCrashTolerance state)
s,ModelState (WithCrashTolerance state)
s') (UnderlyingAction a) = (ModelState state, ModelState state)
-> Action state -> Property -> Property
forall state.
ContractModel state =>
(ModelState state, ModelState state)
-> Action state -> Property -> Property
monitoring (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,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
  monitoring (ModelState (WithCrashTolerance state),
 ModelState (WithCrashTolerance state))
_      Action (WithCrashTolerance state)
_                    = Property -> Property
forall a. a -> a
id

  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, Gen (Action (WithCrashTolerance state)))]
 -> Gen (Action (WithCrashTolerance state)))
-> [(Int, Gen (Action (WithCrashTolerance state)))]
-> Gen (Action (WithCrashTolerance state))
forall a b. (a -> b) -> a -> b
$ [ (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, Gen (Action (WithCrashTolerance state)))]
-> [(Int, Gen (Action (WithCrashTolerance state)))]
-> [(Int, Gen (Action (WithCrashTolerance state)))]
forall a. [a] -> [a] -> [a]
++
                [ (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 [SomeContractInstanceKey state]
alive)
                | let alive :: [SomeContractInstanceKey state]
alive = 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
                , Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [SomeContractInstanceKey state] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SomeContractInstanceKey state]
alive ] [(Int, Gen (Action (WithCrashTolerance state)))]
-> [(Int, Gen (Action (WithCrashTolerance state)))]
-> [(Int, Gen (Action (WithCrashTolerance state)))]
forall a. [a] -> [a] -> [a]
++
                [ (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 [SomeContractInstanceKey state]
dead)
                | let dead :: [SomeContractInstanceKey state]
dead = 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
                , Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [SomeContractInstanceKey state] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [SomeContractInstanceKey state]
dead
                ]

  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

-- TODO: this should move to quickcheck-contractmodel
embed :: Spec state a -> Spec (WithCrashTolerance state) a
embed :: Spec state a -> Spec (WithCrashTolerance state) a
embed (Spec WriterT
  SymCreationIndex
  (ReaderT (Var SymIndex) (State (ModelState state)))
  a
comp) = WriterT
  SymCreationIndex
  (ReaderT
     (Var SymIndex) (State (ModelState (WithCrashTolerance state))))
  a
-> Spec (WithCrashTolerance state) a
forall state a.
WriterT
  SymCreationIndex
  (ReaderT (Var SymIndex) (State (ModelState state)))
  a
-> Spec state a
Spec (LensLike'
  (Zoomed
     (WriterT
        SymCreationIndex
        (ReaderT (Var SymIndex) (State (ModelState state))))
     a)
  (ModelState (WithCrashTolerance state))
  (ModelState state)
-> WriterT
     SymCreationIndex
     (ReaderT (Var SymIndex) (State (ModelState state)))
     a
-> WriterT
     SymCreationIndex
     (ReaderT
        (Var SymIndex) (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 (ModelState a -> Getting a (ModelState a) a -> a
forall s a. s -> Getting a s a -> a
^. Getting a (ModelState a) a
forall state1 state2.
Lens (ModelState state1) (ModelState state2) state1 state2
contractState) forall state. Lens' (WithCrashTolerance state) state
Lens' (WithCrashTolerance state) state
underlyingModelState) WriterT
  SymCreationIndex
  (ReaderT (Var SymIndex) (State (ModelState state)))
  a
comp)