Model PerasCertDiffusion idling in GSM state machine tests

Author: agustinmista

ouroboros-consensus-diffusion/test/consensus-test/Test/Consensus/GSM.hs

@@ -106,7 +106,7 @@ prop_yield_regression =
   yieldRegressionActions :: QD.Actions Model
   yieldRegressionActions =
     (wrapPositiveAction $ NewCandidate Amara (B 1))
-      <> (wrapPositiveAction $ StartIdling Amara)
+      <> (wrapPositiveAction $ ChainSyncStartIdling Amara)
       <> (wrapPositiveAction $ TimePasses 61)
       <> (wrapPositiveAction $ ExtendSelection (S (-4)))
       <> (wrapPositiveAction $ ReadMarker)
@@ -137,8 +137,8 @@ setupGsm isHaaSatisfied vars = do
     (id, tracer)
     GSM.GsmView
       { GSM.antiThunderingHerd = Nothing
-      , GSM.getCandidateOverSelection = pure $ \s (PeerState c _) ->
-          candidateOverSelection s c
+      , GSM.getCandidateOverSelection = pure $ \s peer ->
+          candidateOverSelection s (psCandidate peer)
       , GSM.peerIsIdle = isIdling
       , GSM.durationUntilTooOld = Just durationUntilTooOld
       , GSM.equivalent = (==) -- unsound, but harmless in this test
@@ -246,7 +246,8 @@ data StaticParams = StaticParams
 data Model = Model
   { mCandidates :: Map.Map UpstreamPeer Candidate
   , mClock :: SI.Time
-  , mIdlers :: Set.Set UpstreamPeer
+  , mChainSyncIdlers :: Set.Set UpstreamPeer
+  , mPerasCertDiffusionIdlers :: Set.Set UpstreamPeer
   , mNotables :: Set.Set Notable
   , mPrev :: WhetherPrevTimePasses
   , mSelection :: Selection
@@ -261,18 +262,20 @@ initModel =
   Model
     { mCandidates = Map.empty
     , mClock = SI.Time 0
-    , mIdlers = idlers
+    , mChainSyncIdlers = chainSyncIdlers
+    , mPerasCertDiffusionIdlers = perasCertDiffusionIdlers
     , mNotables = Set.empty
     , mPrev = WhetherPrevTimePasses True
     , mSelection = initialSelection pInitialJudgement
     , mState = case pInitialJudgement of
         TooOld
-          | pIsHaaSatisfied idlers -> ModelSyncing
+          | pIsHaaSatisfied chainSyncIdlers -> ModelSyncing
           | otherwise -> ModelPreSyncing
         YoungEnough -> ModelCaughtUp (SI.Time (-10000))
     }
  where
-  idlers = Set.empty
+  perasCertDiffusionIdlers = Set.empty
+  chainSyncIdlers = Set.empty
 
   StaticParams{pIsHaaSatisfied, pInitialJudgement} = Reflection.given
 
@@ -296,10 +299,16 @@ instance Reflection.Given StaticParams => QD.StateModel Model where
     NewCandidate :: UpstreamPeer -> B -> QD.Action Model ()
     -- \^ INVARIANT new peer
     --
-    -- Mocks the necessary ChainSync client behavior.z
+    -- Mocks the necessary ChainSync client behavior.
+    NewPerasCert :: UpstreamPeer -> QD.Action Model ()
+    -- \^ INVARIANT existing peer
+    --
+    -- Mocks the necessary PerasCertDiffusion client behavior.
     ReadGsmState :: QD.Action Model GSM.GsmState
     ReadMarker :: QD.Action Model MarkerState
-    StartIdling :: UpstreamPeer -> QD.Action Model ()
+    ChainSyncStartIdling :: UpstreamPeer -> QD.Action Model ()
+    -- \^ INVARIANT existing peer, not idling
+    PerasCertDiffusionStartIdling :: UpstreamPeer -> QD.Action Model ()
     -- \^ INVARIANT existing peer, not idling
     TimePasses :: Int -> QD.Action Model ()
 
@@ -437,23 +446,51 @@ instance (IOLike m, Reflection.Given StaticParams) => QD.RunModel Model (RunMona
       ModifyCandidate peer bdel -> do
         atomically $ do
           v <- (Map.! peer) <$> readTVar varStates
-          Candidate b <- psCandidate <$> readTVar v
-          writeTVar v $! PeerState (Candidate (b + bdel)) (Idling False)
-
+          modifyTVar v $! \ps ->
+            let Candidate b = psCandidate ps
+             in ps
+                  { psCandidate = Candidate (b + bdel)
+                  , psChainSyncIdling = Idling False
+                  }
         pure ()
       NewCandidate peer bdel -> do
         atomically $ do
           Selection b _s <- readTVar varSelection
-          v <- newTVar $! PeerState (Candidate (b + bdel)) (Idling False)
+          v <-
+            newTVar $!
+              PeerState
+                { psCandidate = Candidate (b + bdel)
+                , psChainSyncIdling = Idling False
+                , psPerasCertDiffusionIdling = Idling True
+                -- NOTE: this new peer will idle until it gets a 'NewPerasCert'
+                }
           modifyTVar varStates $ Map.insert peer v
         pure ()
+      NewPerasCert peer -> do
+        atomically $ do
+          v <- (Map.! peer) <$> readTVar varStates
+          modifyTVar v $ \ps ->
+            ps
+              { psPerasCertDiffusionIdling = Idling False
+              }
+        pure ()
       ReadGsmState -> do
         atomically $ readTVar varGsmState
       ReadMarker -> do
         atomically $ readTVar varMarker
-      StartIdling peer -> atomically $ do
+      ChainSyncStartIdling peer -> atomically $ do
         v <- (Map.! peer) <$> readTVar varStates
-        modifyTVar v $ \(PeerState c _) -> PeerState c (Idling True)
+        modifyTVar v $ \ps ->
+          ps
+            { psChainSyncIdling = Idling True
+            }
+        pure ()
+      PerasCertDiffusionStartIdling peer -> atomically $ do
+        v <- (Map.! peer) <$> readTVar varStates
+        modifyTVar v $ \ps ->
+          ps
+            { psPerasCertDiffusionIdling = Idling True
+            }
         pure ()
       TimePasses dur -> do
         SI.threadDelay (0.1 * fromIntegral dur)
@@ -596,20 +633,26 @@ precondition model = \case
     peer `Map.member` cands
   NewCandidate peer _bdel ->
     peer `Map.notMember` cands
+  NewPerasCert peer ->
+    peer `Map.member` cands
   ReadGsmState ->
     True
   ReadMarker ->
     True
-  StartIdling peer ->
+  ChainSyncStartIdling peer ->
+    peer `Map.member` cands
+      && peer `Set.notMember` chainSyncIdlers
+  PerasCertDiffusionStartIdling peer ->
     peer `Map.member` cands
-      && peer `Set.notMember` idlers
+      && peer `Set.notMember` perasCertDiffusionIdlers
   TimePasses dur ->
     0 < dur
       && boringDur model dur
  where
   Model
     { mCandidates = cands
-    , mIdlers = idlers
+    , mChainSyncIdlers = chainSyncIdlers
+    , mPerasCertDiffusionIdlers = perasCertDiffusionIdlers
     } = model
 
 generator ::
@@ -635,15 +678,29 @@ generator model =
                    )
          | notNull new
          ]
+      <> [ (,) 20 $ do
+             QD.Some . NewPerasCert <$> QC.elements old
+         | notNull old
+         ]
       <> [(,) 20 $ pure . QD.Some $ ReadGsmState]
       <> [(,) 20 $ pure . QD.Some $ ReadMarker]
-      <> [(,) 50 $ QD.Some . StartIdling <$> QC.elements oldNotIdling | notNull oldNotIdling]
+      <> [ (,) 50 $
+             QD.Some . ChainSyncStartIdling <$> do
+               QC.elements oldNotChainSyncIdling
+         | notNull oldNotChainSyncIdling
+         ]
+      <> [ (,) 50 $
+             QD.Some . PerasCertDiffusionStartIdling <$> do
+               QC.elements oldNotPerasCertDiffusionIdling
+         | notNull oldNotPerasCertDiffusionIdling
+         ]
       <> [(,) 100 $ QD.Some . TimePasses <$> genTimePassesDur | prev == WhetherPrevTimePasses False]
  where
   Model
     { mCandidates = cands
     , mClock = clk
-    , mIdlers = idlers
+    , mChainSyncIdlers = chainSyncIdlers
+    , mPerasCertDiffusionIdlers = perasCertDiffusionIdlers
     , mPrev = prev
     , mSelection = sel
     } = model
@@ -659,7 +716,8 @@ generator model =
     Nothing -> []
     Just peer -> [minBound .. peer] \\ old
 
-  oldNotIdling = old \\ Set.toList idlers
+  oldNotChainSyncIdling = old \\ Set.toList chainSyncIdlers
+  oldNotPerasCertDiffusionIdling = old \\ Set.toList perasCertDiffusionIdlers
 
   genTimePassesDur =
     QC.frequency $
@@ -700,11 +758,15 @@ shrinker _model = \case
     [QD.Some $ ModifyCandidate peer bdel' | bdel' <- shrinkB bdel, bdel' /= 0]
   NewCandidate peer bdel ->
     [QD.Some $ NewCandidate peer bdel' | bdel' <- shrinkB bdel, bdel' /= 0]
+  NewPerasCert{} ->
+    []
   ReadGsmState ->
     []
   ReadMarker ->
     []
-  StartIdling{} ->
+  ChainSyncStartIdling{} ->
+    []
+  PerasCertDiffusionStartIdling{} ->
     []
   TimePasses dur ->
     [QD.Some $ TimePasses dur' | dur' <- QC.shrink dur, 0 < dur']
@@ -722,23 +784,40 @@ transition model cmd =
       Disconnect peer ->
         model'
           { mCandidates = Map.delete peer cands
-          , mIdlers = Set.delete peer idlers
+          , mChainSyncIdlers = Set.delete peer chainSyncIdlers
+          , mPerasCertDiffusionIdlers = Set.delete peer perasCertDiffusionIdlers
           }
       ExtendSelection sdel ->
-        model'{mSelection = Selection (b + 1) (s + sdel)}
+        model'
+          { mSelection = Selection (b + 1) (s + sdel)
+          }
       ModifyCandidate peer bdel ->
         model'
           { mCandidates = Map.insertWith plusC peer (Candidate bdel) cands
-          , mIdlers = Set.delete peer idlers
+          , mChainSyncIdlers = Set.delete peer chainSyncIdlers
           }
       NewCandidate peer bdel ->
-        model'{mCandidates = Map.insert peer (Candidate (b + bdel)) cands}
+        model'
+          { mCandidates = Map.insert peer (Candidate (b + bdel)) cands
+          , mPerasCertDiffusionIdlers = Set.insert peer perasCertDiffusionIdlers
+          -- NOTE: this new peer will idle until it gets a 'NewPerasCert'
+          }
+      NewPerasCert peer ->
+        model'
+          { mPerasCertDiffusionIdlers = Set.delete peer perasCertDiffusionIdlers
+          }
       ReadGsmState ->
         model'
       ReadMarker ->
         model'
-      StartIdling peer ->
-        model'{mIdlers = Set.insert peer idlers}
+      ChainSyncStartIdling peer ->
+        model'
+          { mChainSyncIdlers = Set.insert peer chainSyncIdlers
+          }
+      PerasCertDiffusionStartIdling peer ->
+        model'
+          { mPerasCertDiffusionIdlers = Set.insert peer perasCertDiffusionIdlers
+          }
       TimePasses dur ->
         addNotableWhen BigDurN (dur > 300) $
           model
@@ -749,7 +828,8 @@ transition model cmd =
   Model
     { mCandidates = cands
     , mClock = clk
-    , mIdlers = idlers
+    , mChainSyncIdlers = chainSyncIdlers
+    , mPerasCertDiffusionIdlers = perasCertDiffusionIdlers
     , mSelection = Selection b s
     } = model
 
@@ -806,7 +886,8 @@ fixupModelState cmd model =
   Model
     { mCandidates = cands
     , mClock = clk
-    , mIdlers = idlers
+    , mChainSyncIdlers = chainSyncIdlers
+    , mPerasCertDiffusionIdlers = perasCertDiffusionIdlers
     , mSelection = sel
     , mState = st
     } = model
@@ -820,7 +901,9 @@ fixupModelState cmd model =
 
   some = 0 < Map.size cands
 
-  allIdling = idlers == Map.keysSet cands
+  allIdling =
+    chainSyncIdlers == Map.keysSet cands
+      && perasCertDiffusionIdlers == Map.keysSet cands
 
   ok cand =
     GSM.WhetherCandidateIsBetter False == candidateOverSelection sel cand
@@ -936,14 +1019,20 @@ instance TD.ToExpr Notable where toExpr = TD.defaultExprViaShow
 
 ---
 
-newtype Idling = Idling Bool
+newtype Idling = Idling {unIdling :: Bool}
   deriving (Eq, Ord, Show)
 
-data PeerState = PeerState {psCandidate :: !Candidate, psIdling :: !Idling}
+data PeerState = PeerState
+  { psCandidate :: !Candidate
+  , psChainSyncIdling :: !Idling
+  , psPerasCertDiffusionIdling :: !Idling
+  }
   deriving (Eq, Ord, Show)
 
 isIdling :: PeerState -> Bool
-isIdling (PeerState{psIdling = Idling i}) = i
+isIdling (PeerState{psChainSyncIdling, psPerasCertDiffusionIdling}) =
+  unIdling psChainSyncIdling
+    && unIdling psPerasCertDiffusionIdling
 
 -- | Ensure the GSM thread's transactions quiesce
 --