Convert Model to use q-d 2.0.0

Some remaining snags: * Had to remove warning for unneeded constraintes because of Typeable a in nextAction * Introduce RunMonad newtype wrapper * Remove counterexample on result because of lack of Show instance
input-output-hk · Dec 2, 2022 · c0659d4 · c0659d4
1 parent 88e1804
commit c0659d4
Show file tree

Hide file tree

Showing 3 changed files with 53 additions and 48 deletions.
diff --git a/hydra-node/hydra-node.cabal b/hydra-node/hydra-node.cabal
@@ -351,7 +351,7 @@ test-suite tests
     , plutus-ledger-api
     , process
     , QuickCheck
-    , quickcheck-dynamic                <2.0.0
+    , quickcheck-dynamic                ==2.0.0
     , quickcheck-instances
     , req
     , silently

diff --git a/hydra-node/test/Hydra/Model.hs b/hydra-node/test/Hydra/Model.hs
@@ -1,6 +1,8 @@
 {-# LANGUAGE DuplicateRecordFields #-}
 {-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE UndecidableInstances #-}
 {-# OPTIONS_GHC -Wno-orphans #-}
+{-# OPTIONS_GHC -Wno-redundant-constraints #-}
 
 -- | A /Model/ of the Hydra head Protocol.
 --
@@ -79,7 +81,7 @@ import qualified Hydra.Snapshot as Snapshot
 import Test.Consensus.Cardano.Generators ()
 import Test.QuickCheck (counterexample, elements, frequency, resize, sized, tabulate, vectorOf)
 import Test.QuickCheck.DynamicLogic (DynLogicModel)
-import Test.QuickCheck.StateModel (Any (..), LookUp, RunModel (..), StateModel (..), Var)
+import Test.QuickCheck.StateModel (Any (..), Realized, RunModel (..), StateModel (..), Var)
 import qualified Prelude
 
 -- | Global state of the Head protocol.
@@ -311,50 +313,50 @@ instance StateModel WorldState where
       ObserveConfirmedTx _ -> s
       StopTheWorld -> s
 
-  postcondition :: WorldState -> Action WorldState a -> LookUp -> a -> Bool
-  postcondition _st (Commit _party expectedCommitted) _ actualCommitted =
-    expectedCommitted == actualCommitted
-  postcondition _ _ _ _ = True
+deriving instance Show (Action WorldState a)
+deriving instance Eq (Action WorldState a)
+
+-- * Running the model
+
+newtype RunMonad m a = RunMonad {runMonad :: StateT (Nodes m) m a}
+  deriving newtype (Functor, Applicative, Monad, MonadState (Nodes m))
+
+instance MonadTrans RunMonad where
+  lift r = RunMonad $
+    StateT $ \s -> do
+      a <- r
+      pure (a, s)
+
+type instance Realized (RunMonad m) a = a
+
+instance
+  ( MonadDelay m
+  , MonadAsync m
+  , MonadCatch m
+  , MonadTimer m
+  , MonadThrow (STM m)
+  , MonadLabelledSTM m
+  ) =>
+  RunModel WorldState (RunMonad m)
+  where
+  postcondition (_, st) action _l result = pure $ checkOutcome st action result
 
-  monitoring (s, s') action l result =
+  monitoring (s, s') action _l result =
     decoratePostconditionFailure
       . decorateTransitions
    where
     -- REVIEW: This should be part of the quickcheck-dynamic runActions
     decoratePostconditionFailure
-      | postcondition s action l result = id
+      | checkOutcome s action result = id
       | otherwise =
         counterexample "postcondition failed"
           . counterexample ("Action: " <> show action)
           . counterexample ("State: " <> show s)
-          . counterexample ("Result: " <> show result)
 
     decorateTransitions =
       case (hydraState s, hydraState s') of
         (st, st') -> tabulate "Transitions" [unsafeConstructorName st <> " -> " <> unsafeConstructorName st']
 
-deriving instance Show (Action WorldState a)
-deriving instance Eq (Action WorldState a)
-
--- * Running the model
-
-runModel ::
-  (MonadAsync m, MonadCatch m, MonadTimer m, MonadThrow (STM m), MonadLabelledSTM m) =>
-  RunModel WorldState (StateT (Nodes m) m)
-runModel = RunModel{perform}
- where
-  perform ::
-    ( MonadDelay m
-    , MonadAsync m
-    , MonadCatch m
-    , MonadTimer m
-    , MonadThrow (STM m)
-    , MonadLabelledSTM m
-    ) =>
-    WorldState ->
-    Action WorldState a ->
-    LookUp ->
-    StateT (Nodes m) m a
   perform st command _ = do
     case command of
       Seed{seedKeys} ->
@@ -378,19 +380,24 @@ runModel = RunModel{perform}
       StopTheWorld ->
         stopTheWorld
 
-performAbort :: MonadDelay m => Party -> StateT (Nodes m) m ()
+performAbort :: MonadDelay m => Party -> RunMonad m ()
 performAbort party = do
   Nodes{nodes} <- get
   lift $ waitForReadyToCommit party nodes
   party `sendsInput` Input.Abort
 
+checkOutcome :: WorldState -> Action WorldState a -> a -> Bool
+checkOutcome _st (Commit _party expectedCommitted) actualCommitted =
+  expectedCommitted == actualCommitted
+checkOutcome _ _ _ = True
+
 waitForReadyToCommit ::
   forall m tx.
   MonadDelay m =>
   Party ->
   Map Party (TestHydraNode tx m) ->
   m ()
-waitForReadyToCommit party nodes = go 10
+waitForReadyToCommit party nodes = go 100
  where
   go :: Int -> m ()
   go = \case
@@ -406,11 +413,11 @@ waitForReadyToCommit party nodes = go 10
         Just{} ->
           pure ()
 
-stopTheWorld :: MonadAsync m => StateT (Nodes m) m ()
+stopTheWorld :: MonadAsync m => RunMonad m ()
 stopTheWorld =
   gets threads >>= mapM_ (void . lift . cancel)
 
-sendsInput :: Monad m => Party -> ClientInput Tx -> StateT (Nodes m) m ()
+sendsInput :: Monad m => Party -> ClientInput Tx -> RunMonad m ()
 sendsInput party command = do
   nodes <- gets nodes
   case Map.lookup party nodes of
@@ -426,7 +433,7 @@ seedWorld ::
   , MonadLabelledSTM m
   ) =>
   [(SigningKey HydraKey, CardanoSigningKey)] ->
-  StateT (Nodes m) m ()
+  RunMonad m ()
 seedWorld seedKeys = do
   let parties = map (deriveParty . fst) seedKeys
       dummyNodeState =
@@ -465,7 +472,7 @@ performCommit ::
   [CardanoSigningKey] ->
   Party ->
   [(CardanoSigningKey, Value)] ->
-  StateT (Nodes m) m ActualCommitted
+  RunMonad m ActualCommitted
 performCommit parties party paymentUTxO = do
   nodes <- gets nodes
   case Map.lookup party nodes of
@@ -507,7 +514,7 @@ performNewTx ::
   (MonadThrow m, MonadAsync m, MonadTimer m) =>
   Party ->
   Payment ->
-  StateT (Nodes m) m ()
+  RunMonad m ()
 performNewTx party tx = do
   let recipient = mkVkAddress testNetworkId . getVerificationKey . signingKey $ to tx
   nodes <- gets nodes

diff --git a/hydra-node/test/Hydra/ModelSpec.hs b/hydra-node/test/Hydra/ModelSpec.hs
@@ -78,9 +78,10 @@ import Hydra.Model (
   GlobalState (..),
   Nodes (Nodes, nodes),
   OffChainState (..),
+  RunMonad,
   WorldState (..),
   genPayment,
-  runModel,
+  runMonad,
  )
 import qualified Hydra.Model as Model
 import qualified Hydra.Model.Payment as Payment
@@ -97,7 +98,7 @@ import Test.QuickCheck.DynamicLogic (
  )
 import Test.QuickCheck.Gen.Unsafe (Capture (Capture), capture)
 import Test.QuickCheck.Monadic (PropertyM, assert, monadic', monitor, run)
-import Test.QuickCheck.StateModel (Actions, RunModel, Step ((:=)), runActions, stateAfter, pattern Actions)
+import Test.QuickCheck.StateModel (Actions, Step ((:=)), runActions, stateAfter, pattern Actions)
 import Test.Util (printTrace, traceInIOSim)
 
 spec :: Spec
@@ -118,12 +119,9 @@ prop_checkConflictFreeLiveness =
 prop_HydraModel :: Actions WorldState -> Property
 prop_HydraModel actions = property $
   runIOSimProp $ do
-    _ <- runActions runIt actions
+    _ <- runActions actions
     assert True
 
-runIt :: forall s. RunModel WorldState (StateT (Nodes (IOSim s)) (IOSim s))
-runIt = runModel
-
 -- • Conflict-Free Liveness (Head):
 --
 -- In presence of a network adversary, a conflict-free execution satisfies the following condition:
@@ -169,7 +167,7 @@ prop_checkModel actions =
   within 20000000 $
     property $
       runIOSimProp $ do
-        (WorldState{hydraParties, hydraState}, _symEnv) <- runActions runIt actions
+        (WorldState{hydraParties, hydraState}, _symEnv) <- runActions actions
         -- XXX: In the past we waited until the end of time here, which would
         -- robustly catch all the remaining asynchronous actions, but we have
         -- now a "more active" simulated chain which ticks away and not simply
@@ -189,7 +187,7 @@ assertBalancesInOpenHeadAreConsistent ::
   GlobalState ->
   Map Party (TestHydraNode Tx (IOSim s)) ->
   Party ->
-  PropertyM (StateT (Nodes (IOSim s)) (IOSim s)) ()
+  PropertyM (RunMonad (IOSim s)) ()
 assertBalancesInOpenHeadAreConsistent world nodes p = do
   let node = nodes ! p
   case world of
@@ -236,10 +234,10 @@ assertBalancesInOpenHeadAreConsistent world nodes p = do
 --
 
 -- | Specialised runner similar to <runSTGen https://hackage.haskell.org/package/QuickCheck-2.14.2/docs/src/Test.QuickCheck.Monadic.html#runSTGen>.
-runIOSimProp :: Testable a => (forall s. PropertyM (StateT (Nodes (IOSim s)) (IOSim s)) a) -> Gen Property
+runIOSimProp :: Testable a => (forall s. PropertyM (RunMonad (IOSim s)) a) -> Gen Property
 runIOSimProp p = do
   Capture eval <- capture
-  let tr = runSimTrace $ evalStateT (eval $ monadic' p) (Nodes mempty traceInIOSim mempty)
+  let tr = runSimTrace $ evalStateT (runMonad $ eval $ monadic' p) (Nodes mempty traceInIOSim mempty)
       traceDump = printTrace (Proxy :: Proxy Tx) tr
       logsOnError = counterexample ("trace:\n" <> toString traceDump)
   case traceResult False tr of