{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralisedNewtypeDeriving #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}

-- | Tests for the Genesis State Machine using the [quickcheck-dynamic](https://hackage.haskell.org/package/quickcheck-dynamic) library.
--
--   The instance 'QD.StateModel Model' describes the actions that the model supports,
--   and their semantics in terms for the model and the system-under-test.
--
--   We use the [reflection](https://hackage.haskell.org/package/reflection) library to solve the problem of
--   injecting user-supplied or quickcheck-generated values into the instance of QD.StateModel.
--   See the definition of the 'initialState' method, where we access the reflected configuration, and
--   see 'prop_sequential_iosim' for the construction and reification of the configuration.
module Test.Consensus.GSM (tests) where

import Cardano.Network.Types (LedgerStateJudgement (..))
import Control.Concurrent.Class.MonadSTM.Strict.TVar.Checked
import Control.Exception (SomeException (..))
import qualified Control.Monad as Monad
import Control.Monad.Class.MonadAsync
  ( async
  , poll
  , uninterruptibleCancel
  )
import Control.Monad.Class.MonadFork (MonadFork, yield)
import Control.Monad.Class.MonadSTM
import qualified Control.Monad.Class.MonadTime.SI as SI
import qualified Control.Monad.Class.MonadTimer.SI as SI
import qualified Control.Monad.IOSim as IOSim
import Control.Monad.Reader
import Control.Tracer (Tracer (Tracer))
import Data.Functor ((<&>))
import Data.List ((\\))
import qualified Data.Map.Strict as Map
import qualified Data.Reflection as Reflection
import qualified Data.Set as Set
import Data.Time (diffTimeToPicoseconds)
import qualified Data.TreeDiff as TD
import Data.Typeable (Typeable)
import GHC.Generics (Generic)
import qualified Ouroboros.Consensus.Node.GSM as GSM
import Ouroboros.Consensus.Util.IOLike (IOLike)
import Test.QuickCheck (elements, shrink)
import qualified Test.QuickCheck as QC
import Test.QuickCheck.Gen.Unsafe (Capture (Capture), capture)
import qualified Test.QuickCheck.Monadic as QC
import qualified Test.QuickCheck.StateModel as QD
import Test.Tasty (TestTree)
import Test.Tasty.QuickCheck (testProperty)
import Test.Util.Orphans.IOLike ()
import Test.Util.Orphans.ToExpr ()
import Test.Util.TestEnv (adjustQuickCheckTests)
import Test.Util.ToExpr ()
import qualified Text.PrettyPrint as Pretty

tests :: [TestTree]
tests :: [TestTree]
tests = [TestTree]
adhoc [TestTree] -> [TestTree] -> [TestTree]
forall a. Semigroup a => a -> a -> a
<> [TestTree]
core
 where
  adhoc :: [TestTree]
adhoc =
    [ TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"GSM yield regression" Property
prop_yield_regression
    ]
  core :: [TestTree]
core =
    [ (Int -> Int) -> TestTree -> TestTree
adjustQuickCheckTests (Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
10) (TestTree -> TestTree) -> TestTree -> TestTree
forall a b. (a -> b) -> a -> b
$
        TestName
-> (LedgerStateJudgement
    -> Fun (Set UpstreamPeer) Bool -> Property)
-> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty (TestName
"GSM (" TestName -> TestName -> TestName
forall a. Semigroup a => a -> a -> a
<> Maybe UpstreamPeer -> TestName
coreTestName Maybe UpstreamPeer
upstreamPeerBound TestName -> TestName -> TestName
forall a. Semigroup a => a -> a -> a
<> TestName
")") ((LedgerStateJudgement -> Fun (Set UpstreamPeer) Bool -> Property)
 -> TestTree)
-> (LedgerStateJudgement
    -> Fun (Set UpstreamPeer) Bool -> Property)
-> TestTree
forall a b. (a -> b) -> a -> b
$
          Maybe UpstreamPeer
-> LedgerStateJudgement -> Fun (Set UpstreamPeer) Bool -> Property
prop_sequential_iosim Maybe UpstreamPeer
upstreamPeerBound
    | Maybe UpstreamPeer
upstreamPeerBound <- Maybe UpstreamPeer
forall a. Maybe a
Nothing Maybe UpstreamPeer -> [Maybe UpstreamPeer] -> [Maybe UpstreamPeer]
forall a. a -> [a] -> [a]
: (UpstreamPeer -> Maybe UpstreamPeer)
-> [UpstreamPeer] -> [Maybe UpstreamPeer]
forall a b. (a -> b) -> [a] -> [b]
map UpstreamPeer -> Maybe UpstreamPeer
forall a. a -> Maybe a
Just [UpstreamPeer
forall a. Bounded a => a
minBound .. UpstreamPeer
forall a. Bounded a => a
maxBound :: UpstreamPeer]
    ]

  coreTestName :: Maybe UpstreamPeer -> TestName
coreTestName = \case
    Maybe UpstreamPeer
Nothing -> TestName
"no peers"
    Just UpstreamPeer
ub ->
      TestName
"at most " TestName -> TestName -> TestName
forall a. Semigroup a => a -> a -> a
<> case UpstreamPeer -> Int
forall a. Enum a => a -> Int
fromEnum UpstreamPeer
ub of
        Int
0 -> TestName
"1 peer"
        Int
n -> Int -> TestName
forall a. Show a => a -> TestName
show (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) TestName -> TestName -> TestName
forall a. Semigroup a => a -> a -> a
<> TestName
" peers"

-- | Test the example from the Note [Why yield after the command]
--
-- This property fails when 'yieldSeveralTimes' is removed/redefined to @pure
-- ()@.
prop_yield_regression :: QC.Property
prop_yield_regression :: Property
prop_yield_regression =
  StaticParams -> (Given StaticParams => Property) -> Property
forall a r. a -> (Given a => r) -> r
Reflection.give
    ( StaticParams
        { pUpstreamPeerBound :: Maybe UpstreamPeer
pUpstreamPeerBound = Maybe UpstreamPeer
forall a. Maybe a
Nothing
        , pInitialJudgement :: LedgerStateJudgement
pInitialJudgement = LedgerStateJudgement
YoungEnough
        , pIsHaaSatisfied :: Set UpstreamPeer -> Bool
pIsHaaSatisfied = Bool -> Set UpstreamPeer -> Bool
forall a b. a -> b -> a
const Bool
True
        }
    )
    ((Given StaticParams => Property) -> Property)
-> (Given StaticParams => Property) -> Property
forall a b. (a -> b) -> a -> b
$ Property -> Property
forall prop. Testable prop => prop -> Property
QC.once
    (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ (forall s. PropertyM (RunMonad (IOSim s)) Property) -> Property
forall a.
Testable a =>
(forall s. PropertyM (RunMonad (IOSim s)) a) -> Property
runIOSimProp
    ((forall s. PropertyM (RunMonad (IOSim s)) Property) -> Property)
-> (forall s. PropertyM (RunMonad (IOSim s)) Property) -> Property
forall a b. (a -> b) -> a -> b
$ Actions Model -> PropertyM (RunMonad (IOSim s)) Property
forall s.
Given StaticParams =>
Actions Model -> PropertyM (RunMonad (IOSim s)) Property
prop_sequential_iosim1 Actions Model
yieldRegressionActions
 where
  yieldRegressionActions :: QD.Actions Model
  yieldRegressionActions :: Actions Model
yieldRegressionActions =
    (Action Model () -> Actions Model
forall state a.
(Show (Action state a), Eq (Action state a), Typeable a) =>
Action state a -> Actions state
wrapPositiveAction (Action Model () -> Actions Model)
-> Action Model () -> Actions Model
forall a b. (a -> b) -> a -> b
$ UpstreamPeer -> B -> Action Model ()
NewCandidate UpstreamPeer
Amara (Int -> B
B Int
1))
      Actions Model -> Actions Model -> Actions Model
forall a. Semigroup a => a -> a -> a
<> (Action Model () -> Actions Model
forall state a.
(Show (Action state a), Eq (Action state a), Typeable a) =>
Action state a -> Actions state
wrapPositiveAction (Action Model () -> Actions Model)
-> Action Model () -> Actions Model
forall a b. (a -> b) -> a -> b
$ UpstreamPeer -> Action Model ()
StartIdling UpstreamPeer
Amara)
      Actions Model -> Actions Model -> Actions Model
forall a. Semigroup a => a -> a -> a
<> (Action Model () -> Actions Model
forall state a.
(Show (Action state a), Eq (Action state a), Typeable a) =>
Action state a -> Actions state
wrapPositiveAction (Action Model () -> Actions Model)
-> Action Model () -> Actions Model
forall a b. (a -> b) -> a -> b
$ Int -> Action Model ()
TimePasses Int
61)
      Actions Model -> Actions Model -> Actions Model
forall a. Semigroup a => a -> a -> a
<> (Action Model () -> Actions Model
forall state a.
(Show (Action state a), Eq (Action state a), Typeable a) =>
Action state a -> Actions state
wrapPositiveAction (Action Model () -> Actions Model)
-> Action Model () -> Actions Model
forall a b. (a -> b) -> a -> b
$ S -> Action Model ()
ExtendSelection (Int -> S
S (-Int
4)))
      Actions Model -> Actions Model -> Actions Model
forall a. Semigroup a => a -> a -> a
<> (Action Model MarkerState -> Actions Model
forall state a.
(Show (Action state a), Eq (Action state a), Typeable a) =>
Action state a -> Actions state
wrapPositiveAction (Action Model MarkerState -> Actions Model)
-> Action Model MarkerState -> Actions Model
forall a b. (a -> b) -> a -> b
$ Action Model MarkerState
ReadMarker)

prop_sequential_iosim ::
  Maybe UpstreamPeer -> LedgerStateJudgement -> QC.Fun (Set.Set UpstreamPeer) Bool -> QC.Property
prop_sequential_iosim :: Maybe UpstreamPeer
-> LedgerStateJudgement -> Fun (Set UpstreamPeer) Bool -> Property
prop_sequential_iosim Maybe UpstreamPeer
pUpstreamPeerBound LedgerStateJudgement
pInitialJudgement (QC.Fun (Set UpstreamPeer :-> Bool, Bool, Shrunk)
_ Set UpstreamPeer -> Bool
pIsHaaSatisfied) =
  StaticParams -> (Given StaticParams => Property) -> Property
forall a r. a -> (Given a => r) -> r
Reflection.give
    ( StaticParams
        { Maybe UpstreamPeer
pUpstreamPeerBound :: Maybe UpstreamPeer
pUpstreamPeerBound :: Maybe UpstreamPeer
pUpstreamPeerBound
        , LedgerStateJudgement
pInitialJudgement :: LedgerStateJudgement
pInitialJudgement :: LedgerStateJudgement
pInitialJudgement
        , Set UpstreamPeer -> Bool
pIsHaaSatisfied :: Set UpstreamPeer -> Bool
pIsHaaSatisfied :: Set UpstreamPeer -> Bool
pIsHaaSatisfied
        }
    )
    -- NOTE: the actions have to be generated within the application of 'Reflection.give',
    -- as 'generator' relies on reflection for access to the parameters.
    ((Given StaticParams => Property) -> Property)
-> (Given StaticParams => Property) -> Property
forall a b. (a -> b) -> a -> b
$ (Actions Model -> Property) -> Property
forall prop. Testable prop => prop -> Property
QC.property
    ((Actions Model -> Property) -> Property)
-> (Actions Model -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \Actions Model
actions ->
      (forall s. PropertyM (RunMonad (IOSim s)) Property) -> Property
forall a.
Testable a =>
(forall s. PropertyM (RunMonad (IOSim s)) a) -> Property
runIOSimProp ((forall s. PropertyM (RunMonad (IOSim s)) Property) -> Property)
-> (forall s. PropertyM (RunMonad (IOSim s)) Property) -> Property
forall a b. (a -> b) -> a -> b
$ Actions Model -> PropertyM (RunMonad (IOSim s)) Property
forall s.
Given StaticParams =>
Actions Model -> PropertyM (RunMonad (IOSim s)) Property
prop_sequential_iosim1 Actions Model
actions

setupGsm ::
  (Set.Set UpstreamPeer -> Bool) ->
  SystemStateVars (IOSim.IOSim s) ->
  GSM.GsmEntryPoints (IOSim.IOSim s)
setupGsm :: forall s.
(Set UpstreamPeer -> Bool)
-> SystemStateVars (IOSim s) -> GsmEntryPoints (IOSim s)
setupGsm Set UpstreamPeer -> Bool
isHaaSatisfied SystemStateVars (IOSim s)
vars = do
  let tracer :: Tracer (IOSim s) (TraceGsmEvent Selection)
tracer = (TraceGsmEvent Selection -> IOSim s ())
-> Tracer (IOSim s) (TraceGsmEvent Selection)
forall (m :: * -> *) a. (a -> m ()) -> Tracer m a
Tracer ((TraceGsmEvent Selection -> IOSim s ())
 -> Tracer (IOSim s) (TraceGsmEvent Selection))
-> (TraceGsmEvent Selection -> IOSim s ())
-> Tracer (IOSim s) (TraceGsmEvent Selection)
forall a b. (a -> b) -> a -> b
$ EvRecorder (IOSim s) -> Ev -> IOSim s ()
forall (m :: * -> *). IOLike m => EvRecorder m -> Ev -> m ()
push EvRecorder (IOSim s)
varEvents (Ev -> IOSim s ())
-> (TraceGsmEvent Selection -> Ev)
-> TraceGsmEvent Selection
-> IOSim s ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TraceGsmEvent Selection -> Ev
EvGsm
  (Selection -> Selection,
 Tracer (IOSim s) (TraceGsmEvent Selection))
-> GsmView (IOSim s) UpstreamPeer Selection PeerState
-> GsmEntryPoints (IOSim s)
forall (m :: * -> *) upstreamPeer selection tracedSelection
       candidate.
(MonadDelay m, MonadTimer m) =>
(selection -> tracedSelection,
 Tracer m (TraceGsmEvent tracedSelection))
-> GsmView m upstreamPeer selection candidate -> GsmEntryPoints m
GSM.realGsmEntryPoints
    (Selection -> Selection
forall a. a -> a
id, Tracer (IOSim s) (TraceGsmEvent Selection)
tracer)
    GSM.GsmView
      { antiThunderingHerd :: Maybe StdGen
GSM.antiThunderingHerd = Maybe StdGen
forall a. Maybe a
Nothing
      , candidateOverSelection :: Selection -> PeerState -> CandidateVersusSelection
GSM.candidateOverSelection = \Selection
s (PeerState Candidate
c Idling
_) -> Selection -> Candidate -> CandidateVersusSelection
candidateOverSelection Selection
s Candidate
c
      , peerIsIdle :: PeerState -> Bool
GSM.peerIsIdle = PeerState -> Bool
isIdling
      , durationUntilTooOld :: Maybe (Selection -> IOSim s DurationFromNow)
GSM.durationUntilTooOld = (Selection -> IOSim s DurationFromNow)
-> Maybe (Selection -> IOSim s DurationFromNow)
forall a. a -> Maybe a
Just Selection -> IOSim s DurationFromNow
forall s. Selection -> IOSim s DurationFromNow
durationUntilTooOld
      , equivalent :: Selection -> Selection -> Bool
GSM.equivalent = Selection -> Selection -> Bool
forall a. Eq a => a -> a -> Bool
(==) -- unsound, but harmless in this test
      , getChainSyncStates :: STM (IOSim s) (Map UpstreamPeer (StrictTVar (IOSim s) PeerState))
GSM.getChainSyncStates = StrictTVar
  (IOSim s) (Map UpstreamPeer (StrictTVar (IOSim s) PeerState))
-> STM
     (IOSim s) (Map UpstreamPeer (StrictTVar (IOSim s) PeerState))
forall (m :: * -> *) a. MonadSTM m => StrictTVar m a -> STM m a
readTVar StrictTVar
  (IOSim s) (Map UpstreamPeer (StrictTVar (IOSim s) PeerState))
varStates
      , getCurrentSelection :: STM (IOSim s) Selection
GSM.getCurrentSelection = StrictTVar (IOSim s) Selection -> STM (IOSim s) Selection
forall (m :: * -> *) a. MonadSTM m => StrictTVar m a -> STM m a
readTVar StrictTVar (IOSim s) Selection
varSelection
      , minCaughtUpDuration :: NominalDiffTime
GSM.minCaughtUpDuration = NominalDiffTime
forall a. Num a => a
thrashLimit
      , setCaughtUpPersistentMark :: Bool -> IOSim s ()
GSM.setCaughtUpPersistentMark = \Bool
b ->
          STM (IOSim s) () -> IOSim s ()
forall a. HasCallStack => STM (IOSim s) a -> IOSim s a
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
STM m a -> m a
atomically (STM (IOSim s) () -> IOSim s ()) -> STM (IOSim s) () -> IOSim s ()
forall a b. (a -> b) -> a -> b
$ do
            StrictTVar (IOSim s) MarkerState -> MarkerState -> STM (IOSim s) ()
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
StrictTVar m a -> a -> STM m ()
writeTVar StrictTVar (IOSim s) MarkerState
varMarker (MarkerState -> STM (IOSim s) ())
-> MarkerState -> STM (IOSim s) ()
forall a b. (a -> b) -> a -> b
$ if Bool
b then MarkerState
Present else MarkerState
Absent
      , writeGsmState :: GsmState -> IOSim s ()
GSM.writeGsmState = \GsmState
x -> STM (IOSim s) () -> IOSim s ()
forall a. HasCallStack => STM (IOSim s) a -> IOSim s a
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
STM m a -> m a
atomically (STM (IOSim s) () -> IOSim s ()) -> STM (IOSim s) () -> IOSim s ()
forall a b. (a -> b) -> a -> b
$ do
          StrictTVar (IOSim s) GsmState -> GsmState -> STM (IOSim s) ()
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
StrictTVar m a -> a -> STM m ()
writeTVar StrictTVar (IOSim s) GsmState
varGsmState GsmState
x
      , isHaaSatisfied :: STM (IOSim s) Bool
GSM.isHaaSatisfied =
          Set UpstreamPeer -> Bool
isHaaSatisfied (Set UpstreamPeer -> Bool)
-> (Map UpstreamPeer (StrictTVar (IOSim s) PeerState)
    -> Set UpstreamPeer)
-> Map UpstreamPeer (StrictTVar (IOSim s) PeerState)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map UpstreamPeer (StrictTVar (IOSim s) PeerState)
-> Set UpstreamPeer
forall k a. Map k a -> Set k
Map.keysSet (Map UpstreamPeer (StrictTVar (IOSim s) PeerState) -> Bool)
-> STM s (Map UpstreamPeer (StrictTVar (IOSim s) PeerState))
-> STM s Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StrictTVar
  (IOSim s) (Map UpstreamPeer (StrictTVar (IOSim s) PeerState))
-> STM
     (IOSim s) (Map UpstreamPeer (StrictTVar (IOSim s) PeerState))
forall (m :: * -> *) a. MonadSTM m => StrictTVar m a -> STM m a
readTVar StrictTVar
  (IOSim s) (Map UpstreamPeer (StrictTVar (IOSim s) PeerState))
varStates
      }
 where
  SystemStateVars{StrictTVar (IOSim s) Selection
varSelection :: StrictTVar (IOSim s) Selection
varSelection :: forall (m :: * -> *). SystemStateVars m -> StrictTVar m Selection
varSelection, StrictTVar
  (IOSim s) (Map UpstreamPeer (StrictTVar (IOSim s) PeerState))
varStates :: StrictTVar
  (IOSim s) (Map UpstreamPeer (StrictTVar (IOSim s) PeerState))
varStates :: forall (m :: * -> *).
SystemStateVars m
-> StrictTVar m (Map UpstreamPeer (StrictTVar m PeerState))
varStates, StrictTVar (IOSim s) GsmState
varGsmState :: StrictTVar (IOSim s) GsmState
varGsmState :: forall (m :: * -> *). SystemStateVars m -> StrictTVar m GsmState
varGsmState, StrictTVar (IOSim s) MarkerState
varMarker :: StrictTVar (IOSim s) MarkerState
varMarker :: forall (m :: * -> *). SystemStateVars m -> StrictTVar m MarkerState
varMarker, EvRecorder (IOSim s)
varEvents :: EvRecorder (IOSim s)
varEvents :: forall (m :: * -> *). SystemStateVars m -> EvRecorder m
varEvents} = SystemStateVars (IOSim s)
vars

prop_sequential_iosim1 ::
  forall s.
  Reflection.Given StaticParams =>
  QD.Actions Model ->
  QC.PropertyM (RunMonad (IOSim.IOSim s)) QC.Property
prop_sequential_iosim1 :: forall s.
Given StaticParams =>
Actions Model -> PropertyM (RunMonad (IOSim s)) Property
prop_sequential_iosim1 Actions Model
actions = do
  vars@SystemStateVars{varEvents} <- RunMonad (IOSim s) (SystemStateVars (IOSim s))
-> PropertyM (RunMonad (IOSim s)) (SystemStateVars (IOSim s))
forall (m :: * -> *) a. Monad m => m a -> PropertyM m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift RunMonad (IOSim s) (SystemStateVars (IOSim s))
forall r (m :: * -> *). MonadReader r m => m r
ask

  let StaticParams{pInitialJudgement, pIsHaaSatisfied} = Reflection.given

  -- initialise the SUT state using the model params
  lift . lift $ initVars pInitialJudgement vars

  let model = Model
forall state. StateModel state => state
QD.initialState
  let gsm = (Set UpstreamPeer -> Bool)
-> SystemStateVars (IOSim s) -> GsmEntryPoints (IOSim s)
forall s.
(Set UpstreamPeer -> Bool)
-> SystemStateVars (IOSim s) -> GsmEntryPoints (IOSim s)
setupGsm Set UpstreamPeer -> Bool
pIsHaaSatisfied SystemStateVars (IOSim s)
vars
      gsmEntryPoint = case LedgerStateJudgement
pInitialJudgement of
        LedgerStateJudgement
TooOld -> GsmEntryPoints (IOSim s)
-> forall neverTerminates. IOSim s neverTerminates
forall (m :: * -> *).
GsmEntryPoints m -> forall neverTerminates. m neverTerminates
GSM.enterPreSyncing GsmEntryPoints (IOSim s)
gsm
        LedgerStateJudgement
YoungEnough -> GsmEntryPoints (IOSim s)
-> forall neverTerminates. IOSim s neverTerminates
forall (m :: * -> *).
GsmEntryPoints m -> forall neverTerminates. m neverTerminates
GSM.enterCaughtUp GsmEntryPoints (IOSim s)
gsm

  lift . lift $ yieldSeveralTimes

  -- start the GSM
  hGSM <- lift . lift $ async gsmEntryPoint

  (metadata, mbExn) <- do
    (metadata, _env) <- QD.runActions actions
    (lift . lift $ poll hGSM) <&> \case
      Just Right{} ->
        TestName -> (Annotated Model, Maybe SomeException)
forall a. HasCallStack => TestName -> a
error TestName
"impossible! GSM terminated"
      Just (Left SomeException
exn) ->
        -- we don't simply rethrow it, since we still want to pretty print
        -- the command sequence
        (Annotated Model
metadata, SomeException -> Maybe SomeException
forall a. a -> Maybe a
Just SomeException
exn)
      Maybe (Either SomeException (ZonkAny 0))
Nothing ->
        (Annotated Model
metadata, Maybe SomeException
forall a. Maybe a
Nothing)

  -- stop the GSM
  _ <- lift . lift $ uninterruptibleCancel hGSM

  let modelStateAfterActions = Annotated Model -> Model
forall state. Annotated state -> state
QD.underlyingState Annotated Model
metadata

  let noExn = case Maybe SomeException
mbExn of
        Maybe SomeException
Nothing -> () -> Property
forall prop. Testable prop => prop -> Property
QC.property ()
        Just SomeException
exn -> TestName -> Bool -> Property
forall prop. Testable prop => TestName -> prop -> Property
QC.counterexample (SomeException -> TestName
forall a. Show a => a -> TestName
show SomeException
exn) Bool
False

  -- effectively add a 'ReadGsmState' to the end of the command list
  let readFinalStateAction = Action Model GsmState
ReadGsmState
  (finalStateCheck, finalModelState) <-
    takeActionInBoth
      ("Difference after final action " <> show readFinalStateAction)
      modelStateAfterActions
      readFinalStateAction

  watcherEvents <- lift . lift $ dumpEvents varEvents

  pure
    $ QC.counterexample
      ( unlines $
          (:) "WATCHER" $
            map (("    " <>) . show) $
              watcherEvents
      )
    $ QC.counterexample
      ( ("ediff Initial Final " <>)
          . Pretty.render
          . TD.prettyEditExpr
          $ TD.ediff model finalModelState
      )
    $ QC.tabulate
      "Notables"
      ( case Set.toList $ mNotables finalModelState of
          [] -> [TestName
"<none>"]
          [Notable]
notables -> (Notable -> TestName) -> [Notable] -> [TestName]
forall a b. (a -> b) -> [a] -> [b]
map Notable -> TestName
forall a. Show a => a -> TestName
show [Notable]
notables
      )
      noExn
      QC..&&. finalStateCheck

---

-- | The parameters needed by 'Model' and the 'StateModel' instance.
data StaticParams = StaticParams
  { StaticParams -> Maybe UpstreamPeer
pUpstreamPeerBound :: Maybe UpstreamPeer
  , StaticParams -> LedgerStateJudgement
pInitialJudgement :: LedgerStateJudgement
  , StaticParams -> Set UpstreamPeer -> Bool
pIsHaaSatisfied :: Set.Set UpstreamPeer -> Bool
  }

-- | The model state
data Model = Model
  { Model -> Map UpstreamPeer Candidate
mCandidates :: Map.Map UpstreamPeer Candidate
  , Model -> Time
mClock :: SI.Time
  , Model -> Set UpstreamPeer
mIdlers :: Set.Set UpstreamPeer
  , Model -> Set Notable
mNotables :: Set.Set Notable
  , Model -> WhetherPrevTimePasses
mPrev :: WhetherPrevTimePasses
  , Model -> Selection
mSelection :: Selection
  , Model -> ModelState
mState :: ModelState
  }
  deriving (Int -> Model -> TestName -> TestName
[Model] -> TestName -> TestName
Model -> TestName
(Int -> Model -> TestName -> TestName)
-> (Model -> TestName)
-> ([Model] -> TestName -> TestName)
-> Show Model
forall a.
(Int -> a -> TestName -> TestName)
-> (a -> TestName) -> ([a] -> TestName -> TestName) -> Show a
$cshowsPrec :: Int -> Model -> TestName -> TestName
showsPrec :: Int -> Model -> TestName -> TestName
$cshow :: Model -> TestName
show :: Model -> TestName
$cshowList :: [Model] -> TestName -> TestName
showList :: [Model] -> TestName -> TestName
Show, (forall x. Model -> Rep Model x)
-> (forall x. Rep Model x -> Model) -> Generic Model
forall x. Rep Model x -> Model
forall x. Model -> Rep Model x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Model -> Rep Model x
from :: forall x. Model -> Rep Model x
$cto :: forall x. Rep Model x -> Model
to :: forall x. Rep Model x -> Model
Generic)
  deriving anyclass [Model] -> Expr
Model -> Expr
(Model -> Expr) -> ([Model] -> Expr) -> ToExpr Model
forall a. (a -> Expr) -> ([a] -> Expr) -> ToExpr a
$ctoExpr :: Model -> Expr
toExpr :: Model -> Expr
$clistToExpr :: [Model] -> Expr
listToExpr :: [Model] -> Expr
TD.ToExpr

-- | Initialise the 'Model' state from 'StaticParams'
initModel :: Reflection.Given StaticParams => Model
initModel :: Given StaticParams => Model
initModel =
  Model
    { mCandidates :: Map UpstreamPeer Candidate
mCandidates = Map UpstreamPeer Candidate
forall k a. Map k a
Map.empty
    , mClock :: Time
mClock = DiffTime -> Time
SI.Time DiffTime
0
    , mIdlers :: Set UpstreamPeer
mIdlers = Set UpstreamPeer
forall {a}. Set a
idlers
    , mNotables :: Set Notable
mNotables = Set Notable
forall {a}. Set a
Set.empty
    , mPrev :: WhetherPrevTimePasses
mPrev = Bool -> WhetherPrevTimePasses
WhetherPrevTimePasses Bool
True
    , mSelection :: Selection
mSelection = LedgerStateJudgement -> Selection
initialSelection LedgerStateJudgement
pInitialJudgement
    , mState :: ModelState
mState = case LedgerStateJudgement
pInitialJudgement of
        LedgerStateJudgement
TooOld
          | Set UpstreamPeer -> Bool
pIsHaaSatisfied Set UpstreamPeer
forall {a}. Set a
idlers -> ModelState
ModelSyncing
          | Bool
otherwise -> ModelState
ModelPreSyncing
        LedgerStateJudgement
YoungEnough -> Time -> ModelState
ModelCaughtUp (DiffTime -> Time
SI.Time (-DiffTime
10000))
    }
 where
  idlers :: Set a
idlers = Set a
forall {a}. Set a
Set.empty

  StaticParams{Set UpstreamPeer -> Bool
pIsHaaSatisfied :: StaticParams -> Set UpstreamPeer -> Bool
pIsHaaSatisfied :: Set UpstreamPeer -> Bool
pIsHaaSatisfied, LedgerStateJudgement
pInitialJudgement :: StaticParams -> LedgerStateJudgement
pInitialJudgement :: LedgerStateJudgement
pInitialJudgement} = StaticParams
forall a. Given a => a
Reflection.given

-- | The 'StaticParams' are supplied through reflection because this seems to be
--   the cleanest way to pass static configuration needed by the 'initState' and
--   'arbitraryAction' methods
instance Reflection.Given StaticParams => QD.StateModel Model where
  data Action Model a where
    Disconnect :: UpstreamPeer -> QD.Action Model ()
    -- \^ INVARIANT must be an existing peer
    --
    -- Mocks the necessary ChainSync client behavior.
    ExtendSelection :: S -> QD.Action Model ()
    -- \^ INVARIANT 'selectionIsBehind'
    --
    -- NOTE Harmless to assume it only advances by @'B' 1@ at a time.
    ModifyCandidate :: UpstreamPeer -> B -> QD.Action Model ()
    -- \^ INVARIANT existing peer
    --
    -- Mocks the necessary ChainSync client behavior.
    NewCandidate :: UpstreamPeer -> B -> QD.Action Model ()
    -- \^ INVARIANT new peer
    --
    -- Mocks the necessary ChainSync client behavior.z
    ReadGsmState :: QD.Action Model GSM.GsmState
    ReadMarker :: QD.Action Model MarkerState
    StartIdling :: UpstreamPeer -> QD.Action Model ()
    -- \^ INVARIANT existing peer, not idling
    TimePasses :: Int -> QD.Action Model ()

  -- \^ tenths of a second
  --
  -- INVARIANT positive
  --
  -- INVARIANT does not end /exactly/ on an interesting time point; see
  -- 'boringDur'.
  --
  -- NOTE The generator does not yield consecutive 'TimePasses' commands,
  -- though shrinking might.
  precondition :: forall a. Model -> Action Model a -> Bool
precondition = Model -> Action Model a -> Bool
forall a. Given StaticParams => Model -> Action Model a -> Bool
precondition

  arbitraryAction :: VarContext -> Model -> Gen (Any (Action Model))
arbitraryAction VarContext
_ctx Model
model = Given StaticParams => Model -> Gen (Any (Action Model))
Model -> Gen (Any (Action Model))
generator Model
model

  shrinkAction :: forall a.
Typeable a =>
VarContext -> Model -> Action Model a -> [Any (Action Model)]
shrinkAction VarContext
_ctx Model
model = Model -> Action Model a -> [Any (Action Model)]
forall a. Model -> Action Model a -> [Any (Action Model)]
shrinker Model
model

  initialState :: Model
initialState = Model
Given StaticParams => Model
initModel

  nextState :: forall a. Typeable a => Model -> Action Model a -> Var a -> Model
nextState Model
model Action Model a
action Var a
_ = Model -> Action Model a -> Model
forall a. Given StaticParams => Model -> Action Model a -> Model
transition Model
model Action Model a
action

deriving instance Show (QD.Action Model a)
deriving instance Eq (QD.Action Model a)

instance QD.HasVariables SI.DiffTime where
  getAllVariables :: DiffTime -> Set (Any Var)
getAllVariables DiffTime
_ = Set (Any Var)
forall a. Monoid a => a
mempty

instance QD.HasVariables (QD.Action Model a) where
  getAllVariables :: Action Model a -> Set (Any Var)
getAllVariables Action Model a
_ = Set (Any Var)
forall a. Monoid a => a
mempty

instance QD.HasVariables Model where
  getAllVariables :: Model -> Set (Any Var)
getAllVariables Model
_ = Set (Any Var)
forall a. Monoid a => a
mempty

--- System Under Test

-- | Trivial event accumulator, useful for debugging test failures
data Ev
  = -- | 'perform' started stimulating the GSM code being tested
    forall a. EvBegin (QD.Action Model a)
  | -- | 'perform' stopped stimulating the GSM code being tested
    EvEnd
  | -- | the GSM code being tested emitted an event
    EvGsm (GSM.TraceGsmEvent Selection)

deriving instance Show Ev

newtype EvRecorder m = EvRecorder (StrictTVar m [(SI.Time, Ev)])

newRecorder :: IOLike m => m (EvRecorder m)
newRecorder :: forall (m :: * -> *). IOLike m => m (EvRecorder m)
newRecorder = StrictTVar m [(Time, Ev)] -> EvRecorder m
forall (m :: * -> *). StrictTVar m [(Time, Ev)] -> EvRecorder m
EvRecorder (StrictTVar m [(Time, Ev)] -> EvRecorder m)
-> m (StrictTVar m [(Time, Ev)]) -> m (EvRecorder m)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Time, Ev)] -> m (StrictTVar m [(Time, Ev)])
forall (m :: * -> *) a. MonadSTM m => a -> m (StrictTVar m a)
newTVarIO []

dumpEvents :: IOLike m => EvRecorder m -> m [(SI.Time, Ev)]
dumpEvents :: forall (m :: * -> *). IOLike m => EvRecorder m -> m [(Time, Ev)]
dumpEvents (EvRecorder StrictTVar m [(Time, Ev)]
var) = [(Time, Ev)] -> [(Time, Ev)]
forall a. [a] -> [a]
reverse ([(Time, Ev)] -> [(Time, Ev)]) -> m [(Time, Ev)] -> m [(Time, Ev)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StrictTVar m [(Time, Ev)] -> m [(Time, Ev)]
forall (m :: * -> *) a. MonadSTM m => StrictTVar m a -> m a
readTVarIO StrictTVar m [(Time, Ev)]
var

push :: IOLike m => EvRecorder m -> Ev -> m ()
push :: forall (m :: * -> *). IOLike m => EvRecorder m -> Ev -> m ()
push (EvRecorder StrictTVar m [(Time, Ev)]
var) Ev
ev = do
  now <- m Time
forall (m :: * -> *). MonadMonotonicTime m => m Time
SI.getMonotonicTime
  atomically $ modifyTVar var $ (:) (now, ev)

-- | The state of the system under test
data SystemStateVars m
  = SystemStateVars
  { forall (m :: * -> *). SystemStateVars m -> StrictTVar m Selection
varSelection :: (StrictTVar m Selection)
  , forall (m :: * -> *).
SystemStateVars m
-> StrictTVar m (Map UpstreamPeer (StrictTVar m PeerState))
varStates :: (StrictTVar m (Map.Map UpstreamPeer (StrictTVar m PeerState)))
  , forall (m :: * -> *). SystemStateVars m -> StrictTVar m GsmState
varGsmState :: (StrictTVar m GSM.GsmState)
  , forall (m :: * -> *). SystemStateVars m -> StrictTVar m MarkerState
varMarker :: (StrictTVar m MarkerState)
  , forall (m :: * -> *). SystemStateVars m -> EvRecorder m
varEvents :: (EvRecorder m)
  }

setupVars :: IOLike m => LedgerStateJudgement -> m (SystemStateVars m)
setupVars :: forall (m :: * -> *).
IOLike m =>
LedgerStateJudgement -> m (SystemStateVars m)
setupVars LedgerStateJudgement
initStateInitialJudgement = do
  let initialGsmState :: GsmState
initialGsmState = case LedgerStateJudgement
initStateInitialJudgement of
        LedgerStateJudgement
TooOld -> GsmState
GSM.PreSyncing
        LedgerStateJudgement
YoungEnough -> GsmState
GSM.CaughtUp

  -- these variables are part of the 'GSM.GsmView'
  varSelection <- Selection -> m (StrictTVar m Selection)
forall (m :: * -> *) a. MonadSTM m => a -> m (StrictTVar m a)
newTVarIO (LedgerStateJudgement -> Selection
initialSelection LedgerStateJudgement
initStateInitialJudgement)
  varStates <- newTVarIO Map.empty
  varGsmState <- newTVarIO initialGsmState
  varMarker <- newTVarIO (toMarker initialGsmState)

  -- this variable is for better 'QC.counterexample' messages
  varEvents <- newRecorder

  pure $
    SystemStateVars{varSelection, varStates, varGsmState, varMarker, varEvents}

-- | Initialise the values in 'SystemStateVars' based on 'StaticParams'
initVars :: IOLike m => LedgerStateJudgement -> SystemStateVars m -> m ()
initVars :: forall (m :: * -> *).
IOLike m =>
LedgerStateJudgement -> SystemStateVars m -> m ()
initVars LedgerStateJudgement
initialJudgement SystemStateVars m
vars = do
  let SystemStateVars
        { StrictTVar m Selection
varSelection :: forall (m :: * -> *). SystemStateVars m -> StrictTVar m Selection
varSelection :: StrictTVar m Selection
varSelection
        , StrictTVar m (Map UpstreamPeer (StrictTVar m PeerState))
varStates :: forall (m :: * -> *).
SystemStateVars m
-> StrictTVar m (Map UpstreamPeer (StrictTVar m PeerState))
varStates :: StrictTVar m (Map UpstreamPeer (StrictTVar m PeerState))
varStates
        , StrictTVar m GsmState
varGsmState :: forall (m :: * -> *). SystemStateVars m -> StrictTVar m GsmState
varGsmState :: StrictTVar m GsmState
varGsmState
        , StrictTVar m MarkerState
varMarker :: forall (m :: * -> *). SystemStateVars m -> StrictTVar m MarkerState
varMarker :: StrictTVar m MarkerState
varMarker
        } = SystemStateVars m
vars
  STM m () -> m ()
forall a. HasCallStack => STM m a -> m a
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
STM m a -> m a
atomically (STM m () -> m ()) -> STM m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
    let initialGsmState :: GsmState
initialGsmState = case LedgerStateJudgement
initialJudgement of
          LedgerStateJudgement
TooOld -> GsmState
GSM.PreSyncing
          LedgerStateJudgement
YoungEnough -> GsmState
GSM.CaughtUp
    StrictTVar m Selection -> Selection -> STM m ()
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
StrictTVar m a -> a -> STM m ()
writeTVar StrictTVar m Selection
varSelection (Selection -> STM m ()) -> Selection -> STM m ()
forall a b. (a -> b) -> a -> b
$ (LedgerStateJudgement -> Selection
initialSelection LedgerStateJudgement
initialJudgement)
    StrictTVar m (Map UpstreamPeer (StrictTVar m PeerState))
-> Map UpstreamPeer (StrictTVar m PeerState) -> STM m ()
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
StrictTVar m a -> a -> STM m ()
writeTVar StrictTVar m (Map UpstreamPeer (StrictTVar m PeerState))
varStates (Map UpstreamPeer (StrictTVar m PeerState) -> STM m ())
-> Map UpstreamPeer (StrictTVar m PeerState) -> STM m ()
forall a b. (a -> b) -> a -> b
$ Map UpstreamPeer (StrictTVar m PeerState)
forall k a. Map k a
Map.empty
    StrictTVar m GsmState -> GsmState -> STM m ()
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
StrictTVar m a -> a -> STM m ()
writeTVar StrictTVar m GsmState
varGsmState (GsmState -> STM m ()) -> GsmState -> STM m ()
forall a b. (a -> b) -> a -> b
$ GsmState
initialGsmState
    StrictTVar m MarkerState -> MarkerState -> STM m ()
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
StrictTVar m a -> a -> STM m ()
writeTVar StrictTVar m MarkerState
varMarker (MarkerState -> STM m ()) -> MarkerState -> STM m ()
forall a b. (a -> b) -> a -> b
$ (GsmState -> MarkerState
toMarker GsmState
initialGsmState)

newtype RunMonad m a = RunMonad {forall (m :: * -> *) a.
RunMonad m a -> ReaderT (SystemStateVars m) m a
runMonad :: ReaderT (SystemStateVars m) m a}
  deriving newtype ((forall a b. (a -> b) -> RunMonad m a -> RunMonad m b)
-> (forall a b. a -> RunMonad m b -> RunMonad m a)
-> Functor (RunMonad m)
forall a b. a -> RunMonad m b -> RunMonad m a
forall a b. (a -> b) -> RunMonad m a -> RunMonad m b
forall (m :: * -> *) a b.
Functor m =>
a -> RunMonad m b -> RunMonad m a
forall (m :: * -> *) a b.
Functor m =>
(a -> b) -> RunMonad m a -> RunMonad m b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall (m :: * -> *) a b.
Functor m =>
(a -> b) -> RunMonad m a -> RunMonad m b
fmap :: forall a b. (a -> b) -> RunMonad m a -> RunMonad m b
$c<$ :: forall (m :: * -> *) a b.
Functor m =>
a -> RunMonad m b -> RunMonad m a
<$ :: forall a b. a -> RunMonad m b -> RunMonad m a
Functor, Functor (RunMonad m)
Functor (RunMonad m) =>
(forall a. a -> RunMonad m a)
-> (forall a b.
    RunMonad m (a -> b) -> RunMonad m a -> RunMonad m b)
-> (forall a b c.
    (a -> b -> c) -> RunMonad m a -> RunMonad m b -> RunMonad m c)
-> (forall a b. RunMonad m a -> RunMonad m b -> RunMonad m b)
-> (forall a b. RunMonad m a -> RunMonad m b -> RunMonad m a)
-> Applicative (RunMonad m)
forall a. a -> RunMonad m a
forall a b. RunMonad m a -> RunMonad m b -> RunMonad m a
forall a b. RunMonad m a -> RunMonad m b -> RunMonad m b
forall a b. RunMonad m (a -> b) -> RunMonad m a -> RunMonad m b
forall a b c.
(a -> b -> c) -> RunMonad m a -> RunMonad m b -> RunMonad m c
forall (f :: * -> *).
Functor f =>
(forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
forall (m :: * -> *). Applicative m => Functor (RunMonad m)
forall (m :: * -> *) a. Applicative m => a -> RunMonad m a
forall (m :: * -> *) a b.
Applicative m =>
RunMonad m a -> RunMonad m b -> RunMonad m a
forall (m :: * -> *) a b.
Applicative m =>
RunMonad m a -> RunMonad m b -> RunMonad m b
forall (m :: * -> *) a b.
Applicative m =>
RunMonad m (a -> b) -> RunMonad m a -> RunMonad m b
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> c) -> RunMonad m a -> RunMonad m b -> RunMonad m c
$cpure :: forall (m :: * -> *) a. Applicative m => a -> RunMonad m a
pure :: forall a. a -> RunMonad m a
$c<*> :: forall (m :: * -> *) a b.
Applicative m =>
RunMonad m (a -> b) -> RunMonad m a -> RunMonad m b
<*> :: forall a b. RunMonad m (a -> b) -> RunMonad m a -> RunMonad m b
$cliftA2 :: forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> c) -> RunMonad m a -> RunMonad m b -> RunMonad m c
liftA2 :: forall a b c.
(a -> b -> c) -> RunMonad m a -> RunMonad m b -> RunMonad m c
$c*> :: forall (m :: * -> *) a b.
Applicative m =>
RunMonad m a -> RunMonad m b -> RunMonad m b
*> :: forall a b. RunMonad m a -> RunMonad m b -> RunMonad m b
$c<* :: forall (m :: * -> *) a b.
Applicative m =>
RunMonad m a -> RunMonad m b -> RunMonad m a
<* :: forall a b. RunMonad m a -> RunMonad m b -> RunMonad m a
Applicative, Applicative (RunMonad m)
Applicative (RunMonad m) =>
(forall a b. RunMonad m a -> (a -> RunMonad m b) -> RunMonad m b)
-> (forall a b. RunMonad m a -> RunMonad m b -> RunMonad m b)
-> (forall a. a -> RunMonad m a)
-> Monad (RunMonad m)
forall a. a -> RunMonad m a
forall a b. RunMonad m a -> RunMonad m b -> RunMonad m b
forall a b. RunMonad m a -> (a -> RunMonad m b) -> RunMonad m b
forall (m :: * -> *). Monad m => Applicative (RunMonad m)
forall (m :: * -> *) a. Monad m => a -> RunMonad m a
forall (m :: * -> *) a b.
Monad m =>
RunMonad m a -> RunMonad m b -> RunMonad m b
forall (m :: * -> *) a b.
Monad m =>
RunMonad m a -> (a -> RunMonad m b) -> RunMonad m b
forall (m :: * -> *).
Applicative m =>
(forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
$c>>= :: forall (m :: * -> *) a b.
Monad m =>
RunMonad m a -> (a -> RunMonad m b) -> RunMonad m b
>>= :: forall a b. RunMonad m a -> (a -> RunMonad m b) -> RunMonad m b
$c>> :: forall (m :: * -> *) a b.
Monad m =>
RunMonad m a -> RunMonad m b -> RunMonad m b
>> :: forall a b. RunMonad m a -> RunMonad m b -> RunMonad m b
$creturn :: forall (m :: * -> *) a. Monad m => a -> RunMonad m a
return :: forall a. a -> RunMonad m a
Monad, MonadReader (SystemStateVars m))

instance MonadTrans RunMonad where
  lift :: forall (m :: * -> *) a. Monad m => m a -> RunMonad m a
lift = ReaderT (SystemStateVars m) m a -> RunMonad m a
forall (m :: * -> *) a.
ReaderT (SystemStateVars m) m a -> RunMonad m a
RunMonad (ReaderT (SystemStateVars m) m a -> RunMonad m a)
-> (m a -> ReaderT (SystemStateVars m) m a) -> m a -> RunMonad m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m a -> ReaderT (SystemStateVars m) m a
forall (m :: * -> *) a.
Monad m =>
m a -> ReaderT (SystemStateVars m) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift

instance (IOLike m, Reflection.Given StaticParams) => QD.RunModel Model (RunMonad m) where
  perform :: forall a.
Typeable a =>
Model
-> Action Model a
-> LookUp
-> RunMonad m (PerformResult Model (RunMonad m) a)
perform Model
_ Action Model a
action LookUp
_ = do
    SystemStateVars{varSelection, varStates, varGsmState, varMarker, varEvents} <- RunMonad m (SystemStateVars m)
forall r (m :: * -> *). MonadReader r m => m r
ask
    let
      pre :: m a -> RunMonad m a
      pre m a
m = m a -> RunMonad m a
forall (m :: * -> *) a. Monad m => m a -> RunMonad m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m a -> RunMonad m a) -> m a -> RunMonad m a
forall a b. (a -> b) -> a -> b
$ do
        EvRecorder m -> Ev -> m ()
forall (m :: * -> *). IOLike m => EvRecorder m -> Ev -> m ()
push EvRecorder m
varEvents (Action Model a -> Ev
forall a. Action Model a -> Ev
EvBegin Action Model a
action)
        x <- m a
m
        yieldSeveralTimes -- see Note [Why yield after the command]
        push varEvents EvEnd
        pure x

    pre $ case action of
      Disconnect UpstreamPeer
peer -> do
        STM m () -> m ()
forall a. HasCallStack => STM m a -> m a
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
STM m a -> m a
atomically (STM m () -> m ()) -> STM m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
          StrictTVar m (Map UpstreamPeer (StrictTVar m PeerState))
-> (Map UpstreamPeer (StrictTVar m PeerState)
    -> Map UpstreamPeer (StrictTVar m PeerState))
-> STM m ()
forall (m :: * -> *) a.
MonadSTM m =>
StrictTVar m a -> (a -> a) -> STM m ()
modifyTVar StrictTVar m (Map UpstreamPeer (StrictTVar m PeerState))
varStates ((Map UpstreamPeer (StrictTVar m PeerState)
  -> Map UpstreamPeer (StrictTVar m PeerState))
 -> STM m ())
-> (Map UpstreamPeer (StrictTVar m PeerState)
    -> Map UpstreamPeer (StrictTVar m PeerState))
-> STM m ()
forall a b. (a -> b) -> a -> b
$ UpstreamPeer
-> Map UpstreamPeer (StrictTVar m PeerState)
-> Map UpstreamPeer (StrictTVar m PeerState)
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete UpstreamPeer
peer
        a -> m a
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
      ExtendSelection S
sdel -> do
        STM m () -> m ()
forall a. HasCallStack => STM m a -> m a
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
STM m a -> m a
atomically (STM m () -> m ()) -> STM m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
          Selection b s <- StrictTVar m Selection -> STM m Selection
forall (m :: * -> *) a. MonadSTM m => StrictTVar m a -> STM m a
readTVar StrictTVar m Selection
varSelection
          writeTVar varSelection $! Selection (b + 1) (s + sdel)
        a -> m a
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
      ModifyCandidate UpstreamPeer
peer B
bdel -> do
        STM m () -> m ()
forall a. HasCallStack => STM m a -> m a
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
STM m a -> m a
atomically (STM m () -> m ()) -> STM m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
          v <- (Map UpstreamPeer (StrictTVar m PeerState)
-> UpstreamPeer -> StrictTVar m PeerState
forall k a. Ord k => Map k a -> k -> a
Map.! UpstreamPeer
peer) (Map UpstreamPeer (StrictTVar m PeerState)
 -> StrictTVar m PeerState)
-> STM m (Map UpstreamPeer (StrictTVar m PeerState))
-> STM m (StrictTVar m PeerState)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StrictTVar m (Map UpstreamPeer (StrictTVar m PeerState))
-> STM m (Map UpstreamPeer (StrictTVar m PeerState))
forall (m :: * -> *) a. MonadSTM m => StrictTVar m a -> STM m a
readTVar StrictTVar m (Map UpstreamPeer (StrictTVar m PeerState))
varStates
          Candidate b <- psCandidate <$> readTVar v
          writeTVar v $! PeerState (Candidate (b + bdel)) (Idling False)

        a -> m a
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
      NewCandidate UpstreamPeer
peer B
bdel -> do
        STM m () -> m ()
forall a. HasCallStack => STM m a -> m a
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
STM m a -> m a
atomically (STM m () -> m ()) -> STM m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
          Selection b _s <- StrictTVar m Selection -> STM m Selection
forall (m :: * -> *) a. MonadSTM m => StrictTVar m a -> STM m a
readTVar StrictTVar m Selection
varSelection
          v <- newTVar $! PeerState (Candidate (b + bdel)) (Idling False)
          modifyTVar varStates $ Map.insert peer v
        a -> m a
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
      Action Model a
R:ActionModela a
ReadGsmState -> do
        STM m a -> m a
forall a. HasCallStack => STM m a -> m a
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
STM m a -> m a
atomically (STM m a -> m a) -> STM m a -> m a
forall a b. (a -> b) -> a -> b
$ StrictTVar m GsmState -> STM m GsmState
forall (m :: * -> *) a. MonadSTM m => StrictTVar m a -> STM m a
readTVar StrictTVar m GsmState
varGsmState
      Action Model a
R:ActionModela a
ReadMarker -> do
        STM m a -> m a
forall a. HasCallStack => STM m a -> m a
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
STM m a -> m a
atomically (STM m a -> m a) -> STM m a -> m a
forall a b. (a -> b) -> a -> b
$ StrictTVar m MarkerState -> STM m MarkerState
forall (m :: * -> *) a. MonadSTM m => StrictTVar m a -> STM m a
readTVar StrictTVar m MarkerState
varMarker
      StartIdling UpstreamPeer
peer -> STM m a -> m a
forall a. HasCallStack => STM m a -> m a
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
STM m a -> m a
atomically (STM m a -> m a) -> STM m a -> m a
forall a b. (a -> b) -> a -> b
$ do
        v <- (Map UpstreamPeer (StrictTVar m PeerState)
-> UpstreamPeer -> StrictTVar m PeerState
forall k a. Ord k => Map k a -> k -> a
Map.! UpstreamPeer
peer) (Map UpstreamPeer (StrictTVar m PeerState)
 -> StrictTVar m PeerState)
-> STM m (Map UpstreamPeer (StrictTVar m PeerState))
-> STM m (StrictTVar m PeerState)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StrictTVar m (Map UpstreamPeer (StrictTVar m PeerState))
-> STM m (Map UpstreamPeer (StrictTVar m PeerState))
forall (m :: * -> *) a. MonadSTM m => StrictTVar m a -> STM m a
readTVar StrictTVar m (Map UpstreamPeer (StrictTVar m PeerState))
varStates
        modifyTVar v $ \(PeerState Candidate
c Idling
_) -> Candidate -> Idling -> PeerState
PeerState Candidate
c (Bool -> Idling
Idling Bool
True)
        pure ()
      TimePasses Int
dur -> do
        DiffTime -> m ()
forall (m :: * -> *). MonadDelay m => DiffTime -> m ()
SI.threadDelay (DiffTime
0.1 DiffTime -> DiffTime -> DiffTime
forall a. Num a => a -> a -> a
* Int -> DiffTime
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
dur)
        a -> m a
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

---

runIOSimProp ::
  QC.Testable a => (forall s. QC.PropertyM (RunMonad (IOSim.IOSim s)) a) -> QC.Property
runIOSimProp :: forall a.
Testable a =>
(forall s. PropertyM (RunMonad (IOSim s)) a) -> Property
runIOSimProp forall s. PropertyM (RunMonad (IOSim s)) a
p =
  Gen Property -> Property
forall prop. Testable prop => prop -> Property
QC.property (Gen Property -> Property) -> Gen Property -> Property
forall a b. (a -> b) -> a -> b
$ (forall s. Gen (RunMonad (IOSim s) Property)) -> Gen Property
forall a.
Testable a =>
(forall s. Gen (RunMonad (IOSim s) a)) -> Gen Property
runRunMonadIOSimGen (PropertyM (RunMonad (IOSim s)) a
-> Gen (RunMonad (IOSim s) Property)
forall a (m :: * -> *).
(Testable a, Monad m) =>
PropertyM m a -> Gen (m Property)
QC.monadic' PropertyM (RunMonad (IOSim s)) a
forall s. PropertyM (RunMonad (IOSim s)) a
p)
 where
  -- Borrowed from Hydra
  runRunMonadIOSimGen ::
    forall a.
    QC.Testable a =>
    (forall s. QC.Gen ((RunMonad (IOSim.IOSim s)) a)) ->
    QC.Gen QC.Property
  runRunMonadIOSimGen :: forall a.
Testable a =>
(forall s. Gen (RunMonad (IOSim s) a)) -> Gen Property
runRunMonadIOSimGen forall s. Gen (RunMonad (IOSim s) a)
f = do
    Capture eval <- Gen Capture
capture
    let tr = (forall s. IOSim s a) -> SimTrace a
forall a. (forall s. IOSim s a) -> SimTrace a
IOSim.runSimTrace (Gen (RunMonad (IOSim s) a)
-> (Gen (RunMonad (IOSim s) a) -> RunMonad (IOSim s) a)
-> IOSim s a
forall s a.
Gen (RunMonad (IOSim s) a)
-> (Gen (RunMonad (IOSim s) a) -> RunMonad (IOSim s) a)
-> IOSim s a
sim Gen (RunMonad (IOSim s) a)
forall s. Gen (RunMonad (IOSim s) a)
f Gen (RunMonad (IOSim s) a) -> RunMonad (IOSim s) a
forall a. Gen a -> a
eval)
    return $
      case IOSim.traceResult False tr of
        Right a
a -> a -> Property
forall prop. Testable prop => prop -> Property
QC.property a
a
        Left (IOSim.FailureException (SomeException e
ex)) ->
          TestName -> Bool -> Property
forall prop. Testable prop => TestName -> prop -> Property
QC.counterexample (e -> TestName
forall a. Show a => a -> TestName
show e
ex) Bool
False
        Left Failure
ex ->
          TestName -> Bool -> Property
forall prop. Testable prop => TestName -> prop -> Property
QC.counterexample (Failure -> TestName
forall a. Show a => a -> TestName
show Failure
ex) Bool
False

  sim ::
    forall s a.
    (QC.Gen ((RunMonad (IOSim.IOSim s)) a)) ->
    (QC.Gen (RunMonad (IOSim.IOSim s) a) -> (RunMonad (IOSim.IOSim s) a)) ->
    IOSim.IOSim s a
  sim :: forall s a.
Gen (RunMonad (IOSim s) a)
-> (Gen (RunMonad (IOSim s) a) -> RunMonad (IOSim s) a)
-> IOSim s a
sim Gen (RunMonad (IOSim s) a)
f Gen (RunMonad (IOSim s) a) -> RunMonad (IOSim s) a
eval = do
    vars <- LedgerStateJudgement -> IOSim s (SystemStateVars (IOSim s))
forall (m :: * -> *).
IOLike m =>
LedgerStateJudgement -> m (SystemStateVars m)
setupVars LedgerStateJudgement
TooOld
    runReaderT (runMonad (eval f)) vars

-- | Execute an action in both the model and the system under test, returning
--   the modified model and a property that checks that the action brought
--   the model and the SUT into the same state.
takeActionInBoth ::
  (IOLike m, Reflection.Given StaticParams) =>
  String ->
  Model ->
  QD.Action Model GSM.GsmState ->
  QC.PropertyM (RunMonad m) (QC.Property, Model)
takeActionInBoth :: forall (m :: * -> *).
(IOLike m, Given StaticParams) =>
TestName
-> Model
-> Action Model GsmState
-> PropertyM (RunMonad m) (Property, Model)
takeActionInBoth TestName
conterexampleMessage Model
model Action Model GsmState
action = do
  -- run the action in the model
  let expected :: Model
expected = Model -> Action Model GsmState -> Var GsmState -> Model
forall a. Typeable a => Model -> Action Model a -> Var a -> Model
forall state a.
(StateModel state, Typeable a) =>
state -> Action state a -> Var a -> state
QD.nextState Model
model Action Model GsmState
action Var GsmState
forall {a}. a
impossibleError
  -- run the action in the real system under test
  actual <- RunMonad m GsmState -> PropertyM (RunMonad m) GsmState
forall (m :: * -> *) a. Monad m => m a -> PropertyM m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (RunMonad m GsmState -> PropertyM (RunMonad m) GsmState)
-> RunMonad m GsmState -> PropertyM (RunMonad m) GsmState
forall a b. (a -> b) -> a -> b
$ Model
-> Action Model GsmState
-> LookUp
-> RunMonad m (PerformResult Model (RunMonad m) GsmState)
forall a.
Typeable a =>
Model
-> Action Model a
-> LookUp
-> RunMonad m (PerformResult Model (RunMonad m) a)
forall state (m :: * -> *) a.
(RunModel state m, Typeable a) =>
state -> Action state a -> LookUp -> m (PerformResult state m a)
QD.perform Model
model Action Model GsmState
action Var a -> a
forall {a}. a
LookUp
impossibleError
  -- check that the states are the same after
  pure
    ( QC.counterexample conterexampleMessage $
        ((toGsmState . mState $ expected) QC.=== actual)
    , expected
    )
 where
  impossibleError :: a
impossibleError = TestName -> a
forall a. HasCallStack => TestName -> a
error TestName
"Impossible: unused argument"

-- | Wrap an 'Action' into singleton 'Actions'.
--   This function is useful for constructing adhoc test scenarios,
--   see 'prop_yield_regression' for an example.
--
--   Note: this may break some invariant related to Variables,
--         but we do not care about Variables in these tests.
wrapPositiveAction ::
  ( Show (QD.Action state a)
  , Eq (QD.Action state a)
  , Typeable a
  ) =>
  QD.Action state a ->
  QD.Actions state
wrapPositiveAction :: forall state a.
(Show (Action state a), Eq (Action state a), Typeable a) =>
Action state a -> Actions state
wrapPositiveAction Action state a
action =
  [Step state] -> Actions state
forall state. [Step state] -> Actions state
QD.Actions [Var a -> ActionWithPolarity state a -> Step state
forall a state.
(Typeable a, Eq (Action state a), Show (Action state a)) =>
Var a -> ActionWithPolarity state a -> Step state
(QD.:=) Var a
forall a. Var a
dummyVar (Action state a -> Polarity -> ActionWithPolarity state a
forall state a.
Eq (Action state a) =>
Action state a -> Polarity -> ActionWithPolarity state a
QD.ActionWithPolarity Action state a
action Polarity
QD.PosPolarity)]

-- | See 'boringDurImpl'
boringDur :: Model -> Int -> Bool
boringDur :: Model -> Int -> Bool
boringDur Model
model = Time -> Selection -> ModelState -> Int -> Bool
boringDurImpl Time
clk Selection
sel ModelState
st
 where
  Model
    { mClock :: Model -> Time
mClock = Time
clk
    , mSelection :: Model -> Selection
mSelection = Selection
sel
    , mState :: Model -> ModelState
mState = ModelState
st
    } = Model
model

addNotableWhen :: Notable -> Bool -> Model -> Model
addNotableWhen :: Notable -> Bool -> Model -> Model
addNotableWhen Notable
n Bool
b Model
model =
  if Bool -> Bool
not Bool
b
    then Model
model
    else
      Model
model{mNotables = n `Set.insert` mNotables model}

selectionIsBehind :: Model -> Bool
selectionIsBehind :: Model -> Bool
selectionIsBehind Model
model =
  (Candidate -> Bool) -> Map UpstreamPeer Candidate -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (\(Candidate B
b') -> B
b' B -> B -> Bool
forall a. Ord a => a -> a -> Bool
> B
b) Map UpstreamPeer Candidate
cands
 where
  Model
    { mCandidates :: Model -> Map UpstreamPeer Candidate
mCandidates = Map UpstreamPeer Candidate
cands
    , mSelection :: Model -> Selection
mSelection = Selection B
b S
_s
    } = Model
model

selectionIsNotEarly :: Model -> Bool
selectionIsNotEarly :: Model -> Bool
selectionIsNotEarly Model
model =
  Selection -> Time
onset Selection
sel Time -> Time -> Bool
forall a. Ord a => a -> a -> Bool
<= Time
clk
 where
  Model
    { mClock :: Model -> Time
mClock = Time
clk
    , mSelection :: Model -> Selection
mSelection = Selection
sel
    } = Model
model

initialSelection :: LedgerStateJudgement -> Selection
initialSelection :: LedgerStateJudgement -> Selection
initialSelection LedgerStateJudgement
initStateInitialJudgement = B -> S -> Selection
Selection B
0 S
s
 where
  s :: S
s = Int -> S
S (Int -> S) -> Int -> S
forall a b. (a -> b) -> a -> b
$ case LedgerStateJudgement
initStateInitialJudgement of
    LedgerStateJudgement
TooOld -> (-Int
11)
    LedgerStateJudgement
YoungEnough -> Int
0

---

dummyVar :: QD.Var a
dummyVar :: forall a. Var a
dummyVar = Int -> Var a
forall a. Int -> Var a
QD.mkVar Int
0

--- Definitions used in the 'ModelState' instance

precondition ::
  forall a.
  Reflection.Given StaticParams =>
  Model -> QD.Action Model a -> Bool
precondition :: forall a. Given StaticParams => Model -> Action Model a -> Bool
precondition Model
model = \case
  cmd :: Action Model a
cmd@ExtendSelection{} ->
    let model' :: Model
model' = Model -> Action Model a -> Var a -> Model
forall a. Typeable a => Model -> Action Model a -> Var a -> Model
forall state a.
(StateModel state, Typeable a) =>
state -> Action state a -> Var a -> state
QD.nextState Model
model Action Model a
cmd Var a
forall a. Var a
dummyVar
     in Model -> Bool
selectionIsBehind Model
model
          Bool -> Bool -> Bool
&& Model -> Bool
selectionIsNotEarly Model
model'
          Bool -> Bool -> Bool
&& Model -> Int -> Bool
boringDur Model
model' Int
0
  Disconnect UpstreamPeer
peer ->
    UpstreamPeer
peer UpstreamPeer -> Map UpstreamPeer Candidate -> Bool
forall k a. Ord k => k -> Map k a -> Bool
`Map.member` Map UpstreamPeer Candidate
cands
  ModifyCandidate UpstreamPeer
peer B
_bdel ->
    UpstreamPeer
peer UpstreamPeer -> Map UpstreamPeer Candidate -> Bool
forall k a. Ord k => k -> Map k a -> Bool
`Map.member` Map UpstreamPeer Candidate
cands
  NewCandidate UpstreamPeer
peer B
_bdel ->
    UpstreamPeer
peer UpstreamPeer -> Map UpstreamPeer Candidate -> Bool
forall k a. Ord k => k -> Map k a -> Bool
`Map.notMember` Map UpstreamPeer Candidate
cands
  Action Model a
R:ActionModela a
ReadGsmState ->
    Bool
True
  Action Model a
R:ActionModela a
ReadMarker ->
    Bool
True
  StartIdling UpstreamPeer
peer ->
    UpstreamPeer
peer UpstreamPeer -> Map UpstreamPeer Candidate -> Bool
forall k a. Ord k => k -> Map k a -> Bool
`Map.member` Map UpstreamPeer Candidate
cands
      Bool -> Bool -> Bool
&& UpstreamPeer
peer UpstreamPeer -> Set UpstreamPeer -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.notMember` Set UpstreamPeer
idlers
  TimePasses Int
dur ->
    Int
0 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
dur
      Bool -> Bool -> Bool
&& Model -> Int -> Bool
boringDur Model
model Int
dur
 where
  Model
    { mCandidates :: Model -> Map UpstreamPeer Candidate
mCandidates = Map UpstreamPeer Candidate
cands
    , mIdlers :: Model -> Set UpstreamPeer
mIdlers = Set UpstreamPeer
idlers
    } = Model
model

generator ::
  Reflection.Given StaticParams =>
  Model -> QC.Gen (QD.Any (QD.Action Model))
generator :: Given StaticParams => Model -> Gen (Any (Action Model))
generator Model
model =
  [(Int, Gen (Any (Action Model)))] -> Gen (Any (Action Model))
forall a. HasCallStack => [(Int, Gen a)] -> Gen a
QC.frequency ([(Int, Gen (Any (Action Model)))] -> Gen (Any (Action Model)))
-> [(Int, Gen (Any (Action Model)))] -> Gen (Any (Action Model))
forall a b. (a -> b) -> a -> b
$
    [(,) Int
5 (Gen (Any (Action Model)) -> (Int, Gen (Any (Action Model))))
-> Gen (Any (Action Model)) -> (Int, Gen (Any (Action Model)))
forall a b. (a -> b) -> a -> b
$ Action Model () -> Any (Action Model)
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
QD.Some (Action Model () -> Any (Action Model))
-> (UpstreamPeer -> Action Model ())
-> UpstreamPeer
-> Any (Action Model)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UpstreamPeer -> Action Model ()
Disconnect (UpstreamPeer -> Any (Action Model))
-> Gen UpstreamPeer -> Gen (Any (Action Model))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [UpstreamPeer] -> Gen UpstreamPeer
forall a. HasCallStack => [a] -> Gen a
QC.elements [UpstreamPeer]
old | [UpstreamPeer] -> Bool
forall a. [a] -> Bool
notNull [UpstreamPeer]
old]
      [(Int, Gen (Any (Action Model)))]
-> [(Int, Gen (Any (Action Model)))]
-> [(Int, Gen (Any (Action Model)))]
forall a. Semigroup a => a -> a -> a
<> [ (,) Int
10 (Gen (Any (Action Model)) -> (Int, Gen (Any (Action Model))))
-> Gen (Any (Action Model)) -> (Int, Gen (Any (Action Model)))
forall a b. (a -> b) -> a -> b
$ Action Model () -> Any (Action Model)
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
QD.Some (Action Model () -> Any (Action Model))
-> (S -> Action Model ()) -> S -> Any (Action Model)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. S -> Action Model ()
ExtendSelection (S -> Any (Action Model)) -> Gen S -> Gen (Any (Action Model))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [S] -> Gen S
forall a. HasCallStack => [a] -> Gen a
QC.elements [S]
sdels
         | [S] -> Bool
forall a. [a] -> Bool
notNull [S]
sdels
         , Model -> Bool
selectionIsBehind Model
model -- NB harmless to assume this node never mints
         ]
      [(Int, Gen (Any (Action Model)))]
-> [(Int, Gen (Any (Action Model)))]
-> [(Int, Gen (Any (Action Model)))]
forall a. Semigroup a => a -> a -> a
<> [ (,) Int
20 (Gen (Any (Action Model)) -> (Int, Gen (Any (Action Model))))
-> Gen (Any (Action Model)) -> (Int, Gen (Any (Action Model)))
forall a b. (a -> b) -> a -> b
$ do
             (peer, bdel) <- [(UpstreamPeer, [B])] -> Gen (UpstreamPeer, [B])
forall a. HasCallStack => [a] -> Gen a
QC.elements [(UpstreamPeer, [B])]
bdels
             QD.Some . ModifyCandidate peer <$> QC.elements bdel
         | [(UpstreamPeer, [B])] -> Bool
forall a. [a] -> Bool
notNull [(UpstreamPeer, [B])]
bdels
         ]
      [(Int, Gen (Any (Action Model)))]
-> [(Int, Gen (Any (Action Model)))]
-> [(Int, Gen (Any (Action Model)))]
forall a. Semigroup a => a -> a -> a
<> [ (,) Int
100 (Gen (Any (Action Model)) -> (Int, Gen (Any (Action Model))))
-> Gen (Any (Action Model)) -> (Int, Gen (Any (Action Model)))
forall a b. (a -> b) -> a -> b
$
             Action Model () -> Any (Action Model)
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
QD.Some
               (Action Model () -> Any (Action Model))
-> Gen (Action Model ()) -> Gen (Any (Action Model))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ( UpstreamPeer -> B -> Action Model ()
NewCandidate
                       (UpstreamPeer -> B -> Action Model ())
-> Gen UpstreamPeer -> Gen (B -> Action Model ())
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [UpstreamPeer] -> Gen UpstreamPeer
forall a. HasCallStack => [a] -> Gen a
QC.elements [UpstreamPeer]
new
                       Gen (B -> Action Model ()) -> Gen B -> Gen (Action Model ())
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Int -> B
B (Int -> B) -> Gen Int -> Gen B
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Int, Int) -> Gen Int
forall a. Random a => (a, a) -> Gen a
QC.choose (-Int
10, Int
10))
                   )
         | [UpstreamPeer] -> Bool
forall a. [a] -> Bool
notNull [UpstreamPeer]
new
         ]
      [(Int, Gen (Any (Action Model)))]
-> [(Int, Gen (Any (Action Model)))]
-> [(Int, Gen (Any (Action Model)))]
forall a. Semigroup a => a -> a -> a
<> [(,) Int
20 (Gen (Any (Action Model)) -> (Int, Gen (Any (Action Model))))
-> Gen (Any (Action Model)) -> (Int, Gen (Any (Action Model)))
forall a b. (a -> b) -> a -> b
$ Any (Action Model) -> Gen (Any (Action Model))
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Any (Action Model) -> Gen (Any (Action Model)))
-> (Action Model GsmState -> Any (Action Model))
-> Action Model GsmState
-> Gen (Any (Action Model))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Action Model GsmState -> Any (Action Model)
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
QD.Some (Action Model GsmState -> Gen (Any (Action Model)))
-> Action Model GsmState -> Gen (Any (Action Model))
forall a b. (a -> b) -> a -> b
$ Action Model GsmState
ReadGsmState]
      [(Int, Gen (Any (Action Model)))]
-> [(Int, Gen (Any (Action Model)))]
-> [(Int, Gen (Any (Action Model)))]
forall a. Semigroup a => a -> a -> a
<> [(,) Int
20 (Gen (Any (Action Model)) -> (Int, Gen (Any (Action Model))))
-> Gen (Any (Action Model)) -> (Int, Gen (Any (Action Model)))
forall a b. (a -> b) -> a -> b
$ Any (Action Model) -> Gen (Any (Action Model))
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Any (Action Model) -> Gen (Any (Action Model)))
-> (Action Model MarkerState -> Any (Action Model))
-> Action Model MarkerState
-> Gen (Any (Action Model))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Action Model MarkerState -> Any (Action Model)
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
QD.Some (Action Model MarkerState -> Gen (Any (Action Model)))
-> Action Model MarkerState -> Gen (Any (Action Model))
forall a b. (a -> b) -> a -> b
$ Action Model MarkerState
ReadMarker]
      [(Int, Gen (Any (Action Model)))]
-> [(Int, Gen (Any (Action Model)))]
-> [(Int, Gen (Any (Action Model)))]
forall a. Semigroup a => a -> a -> a
<> [(,) Int
50 (Gen (Any (Action Model)) -> (Int, Gen (Any (Action Model))))
-> Gen (Any (Action Model)) -> (Int, Gen (Any (Action Model)))
forall a b. (a -> b) -> a -> b
$ Action Model () -> Any (Action Model)
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
QD.Some (Action Model () -> Any (Action Model))
-> (UpstreamPeer -> Action Model ())
-> UpstreamPeer
-> Any (Action Model)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UpstreamPeer -> Action Model ()
StartIdling (UpstreamPeer -> Any (Action Model))
-> Gen UpstreamPeer -> Gen (Any (Action Model))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [UpstreamPeer] -> Gen UpstreamPeer
forall a. HasCallStack => [a] -> Gen a
QC.elements [UpstreamPeer]
oldNotIdling | [UpstreamPeer] -> Bool
forall a. [a] -> Bool
notNull [UpstreamPeer]
oldNotIdling]
      [(Int, Gen (Any (Action Model)))]
-> [(Int, Gen (Any (Action Model)))]
-> [(Int, Gen (Any (Action Model)))]
forall a. Semigroup a => a -> a -> a
<> [(,) Int
100 (Gen (Any (Action Model)) -> (Int, Gen (Any (Action Model))))
-> Gen (Any (Action Model)) -> (Int, Gen (Any (Action Model)))
forall a b. (a -> b) -> a -> b
$ Action Model () -> Any (Action Model)
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
QD.Some (Action Model () -> Any (Action Model))
-> (Int -> Action Model ()) -> Int -> Any (Action Model)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Action Model ()
TimePasses (Int -> Any (Action Model)) -> Gen Int -> Gen (Any (Action Model))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Int
genTimePassesDur | WhetherPrevTimePasses
prev WhetherPrevTimePasses -> WhetherPrevTimePasses -> Bool
forall a. Eq a => a -> a -> Bool
== Bool -> WhetherPrevTimePasses
WhetherPrevTimePasses Bool
False]
 where
  Model
    { mCandidates :: Model -> Map UpstreamPeer Candidate
mCandidates = Map UpstreamPeer Candidate
cands
    , mClock :: Model -> Time
mClock = Time
clk
    , mIdlers :: Model -> Set UpstreamPeer
mIdlers = Set UpstreamPeer
idlers
    , mPrev :: Model -> WhetherPrevTimePasses
mPrev = WhetherPrevTimePasses
prev
    , mSelection :: Model -> Selection
mSelection = Selection
sel
    } = Model
model

  StaticParams{pUpstreamPeerBound :: StaticParams -> Maybe UpstreamPeer
pUpstreamPeerBound = Maybe UpstreamPeer
ub} = StaticParams
forall a. Given a => a
Reflection.given

  notNull :: [a] -> Bool
  notNull :: forall a. [a] -> Bool
notNull = Bool -> Bool
not (Bool -> Bool) -> ([a] -> Bool) -> [a] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null

  old :: [UpstreamPeer]
old = Map UpstreamPeer Candidate -> [UpstreamPeer]
forall k a. Map k a -> [k]
Map.keys Map UpstreamPeer Candidate
cands

  new :: [UpstreamPeer]
new = case Maybe UpstreamPeer
ub of
    Maybe UpstreamPeer
Nothing -> []
    Just UpstreamPeer
peer -> [UpstreamPeer
forall a. Bounded a => a
minBound .. UpstreamPeer
peer] [UpstreamPeer] -> [UpstreamPeer] -> [UpstreamPeer]
forall a. Eq a => [a] -> [a] -> [a]
\\ [UpstreamPeer]
old

  oldNotIdling :: [UpstreamPeer]
oldNotIdling = [UpstreamPeer]
old [UpstreamPeer] -> [UpstreamPeer] -> [UpstreamPeer]
forall a. Eq a => [a] -> [a] -> [a]
\\ Set UpstreamPeer -> [UpstreamPeer]
forall a. Set a -> [a]
Set.toList Set UpstreamPeer
idlers

  genTimePassesDur :: Gen Int
genTimePassesDur =
    [(Int, Gen Int)] -> Gen Int
forall a. HasCallStack => [(Int, Gen a)] -> Gen a
QC.frequency ([(Int, Gen Int)] -> Gen Int) -> [(Int, Gen Int)] -> Gen Int
forall a b. (a -> b) -> a -> b
$
      [(,) Int
10 (Gen Int -> (Int, Gen Int)) -> Gen Int -> (Int, Gen Int)
forall a b. (a -> b) -> a -> b
$ (Int, Int) -> Gen Int
forall a. Random a => (a, a) -> Gen a
QC.choose (Int
1, Int
70)]
        [(Int, Gen Int)] -> [(Int, Gen Int)] -> [(Int, Gen Int)]
forall a. Semigroup a => a -> a -> a
<> [ (,) Int
1 (Gen Int -> (Int, Gen Int)) -> Gen Int -> (Int, Gen Int)
forall a b. (a -> b) -> a -> b
$ (Int, Int) -> Gen Int
forall a. Random a => (a, a) -> Gen a
QC.choose (Int
300, Int
600)
           | case Model -> ModelState
mState Model
model of
               ModelCaughtUp{} -> Bool
True
               ModelPreSyncing{} -> Bool
False
               ModelSyncing{} -> Bool
False
           ]

  -- sdels that would not cause the selection to be in the future
  sdels :: [S]
sdels =
    let Selection B
b S
s = Selection
sel
     in [ S
sdel
        | S
sdel <- (Int -> S) -> [Int] -> [S]
forall a b. (a -> b) -> [a] -> [b]
map Int -> S
S [-Int
4 .. Int
10]
        , S
0 S -> S -> Bool
forall a. Eq a => a -> a -> Bool
/= S
sdel
        , Selection -> Time
onset (B -> S -> Selection
Selection B
b (S
s S -> S -> S
forall a. Num a => a -> a -> a
+ S
sdel)) Time -> Time -> Bool
forall a. Ord a => a -> a -> Bool
<= Time
clk
        ]

  -- bdels that keep the candidates' lengths near the selection
  bdels :: [(UpstreamPeer, [B])]
bdels =
    let Selection B
b S
_s = Selection
sel
        lim :: B
lim = B
3
     in [ (,)
            UpstreamPeer
peer
            ((B -> Bool) -> [B] -> [B]
forall a. (a -> Bool) -> [a] -> [a]
filter (B -> B -> Bool
forall a. Eq a => a -> a -> Bool
/= B
0) [B
b B -> B -> B
forall a. Num a => a -> a -> a
+ B
offset B -> B -> B
forall a. Num a => a -> a -> a
- B
c | B
offset <- [-B
lim .. B
lim]])
        | (UpstreamPeer
peer, Candidate B
c) <- Map UpstreamPeer Candidate -> [(UpstreamPeer, Candidate)]
forall k a. Map k a -> [(k, a)]
Map.assocs Map UpstreamPeer Candidate
cands
        ]

shrinker :: Model -> QD.Action Model a -> [QD.Any (QD.Action Model)]
shrinker :: forall a. Model -> Action Model a -> [Any (Action Model)]
shrinker Model
_model = \case
  Disconnect{} ->
    []
  ExtendSelection S
sdel ->
    [Action Model () -> Any (Action Model)
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
QD.Some (Action Model () -> Any (Action Model))
-> Action Model () -> Any (Action Model)
forall a b. (a -> b) -> a -> b
$ S -> Action Model ()
ExtendSelection S
sdel' | S
sdel' <- S -> [S]
shrinkS S
sdel]
  ModifyCandidate UpstreamPeer
peer B
bdel ->
    [Action Model () -> Any (Action Model)
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
QD.Some (Action Model () -> Any (Action Model))
-> Action Model () -> Any (Action Model)
forall a b. (a -> b) -> a -> b
$ UpstreamPeer -> B -> Action Model ()
ModifyCandidate UpstreamPeer
peer B
bdel' | B
bdel' <- B -> [B]
shrinkB B
bdel, B
bdel' B -> B -> Bool
forall a. Eq a => a -> a -> Bool
/= B
0]
  NewCandidate UpstreamPeer
peer B
bdel ->
    [Action Model () -> Any (Action Model)
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
QD.Some (Action Model () -> Any (Action Model))
-> Action Model () -> Any (Action Model)
forall a b. (a -> b) -> a -> b
$ UpstreamPeer -> B -> Action Model ()
NewCandidate UpstreamPeer
peer B
bdel' | B
bdel' <- B -> [B]
shrinkB B
bdel, B
bdel' B -> B -> Bool
forall a. Eq a => a -> a -> Bool
/= B
0]
  Action Model a
R:ActionModela a
ReadGsmState ->
    []
  Action Model a
R:ActionModela a
ReadMarker ->
    []
  StartIdling{} ->
    []
  TimePasses Int
dur ->
    [Action Model () -> Any (Action Model)
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
QD.Some (Action Model () -> Any (Action Model))
-> Action Model () -> Any (Action Model)
forall a b. (a -> b) -> a -> b
$ Int -> Action Model ()
TimePasses Int
dur' | Int
dur' <- Int -> [Int]
forall a. Arbitrary a => a -> [a]
QC.shrink Int
dur, Int
0 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
dur']
 where
  shrinkB :: B -> [B]
shrinkB (B Int
x) = [Int -> B
B Int
x' | Int
x' <- Int -> [Int]
forall a. Arbitrary a => a -> [a]
QC.shrink Int
x]
  shrinkS :: S -> [S]
shrinkS (S Int
x) = [Int -> S
S Int
x' | Int
x' <- Int -> [Int]
forall a. Arbitrary a => a -> [a]
QC.shrink Int
x]

transition ::
  forall a.
  Reflection.Given StaticParams =>
  Model -> QD.Action Model a -> Model
transition :: forall a. Given StaticParams => Model -> Action Model a -> Model
transition Model
model Action Model a
cmd =
  Action Model a -> Model -> Model
forall a. Given StaticParams => Action Model a -> Model -> Model
fixupModelState Action Model a
cmd (Model -> Model) -> Model -> Model
forall a b. (a -> b) -> a -> b
$
    case Action Model a
cmd of
      Disconnect UpstreamPeer
peer ->
        Model
model'
          { mCandidates = Map.delete peer cands
          , mIdlers = Set.delete peer idlers
          }
      ExtendSelection S
sdel ->
        Model
model'{mSelection = Selection (b + 1) (s + sdel)}
      ModifyCandidate UpstreamPeer
peer B
bdel ->
        Model
model'
          { mCandidates = Map.insertWith plusC peer (Candidate bdel) cands
          , mIdlers = Set.delete peer idlers
          }
      NewCandidate UpstreamPeer
peer B
bdel ->
        Model
model'{mCandidates = Map.insert peer (Candidate (b + bdel)) cands}
      Action Model a
R:ActionModela a
ReadGsmState ->
        Model
model'
      Action Model a
R:ActionModela a
ReadMarker ->
        Model
model'
      StartIdling UpstreamPeer
peer ->
        Model
model'{mIdlers = Set.insert peer idlers}
      TimePasses Int
dur ->
        Notable -> Bool -> Model -> Model
addNotableWhen Notable
BigDurN (Int
dur Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
300) (Model -> Model) -> Model -> Model
forall a b. (a -> b) -> a -> b
$
          Model
model
            { mClock = SI.addTime (0.1 * fromIntegral dur) clk
            , mPrev = WhetherPrevTimePasses True
            }
 where
  Model
    { mCandidates :: Model -> Map UpstreamPeer Candidate
mCandidates = Map UpstreamPeer Candidate
cands
    , mClock :: Model -> Time
mClock = Time
clk
    , mIdlers :: Model -> Set UpstreamPeer
mIdlers = Set UpstreamPeer
idlers
    , mSelection :: Model -> Selection
mSelection = Selection B
b S
s
    } = Model
model

  model' :: Model
  model' :: Model
model' = Model
model{mPrev = WhetherPrevTimePasses False}

  plusC :: Candidate -> Candidate -> Candidate
plusC (Candidate B
x) (Candidate B
y) = B -> Candidate
Candidate (B
x B -> B -> B
forall a. Num a => a -> a -> a
+ B
y)

-- | Update the 'mState', assuming that's the only stale field in the given
-- 'Model'
fixupModelState ::
  forall a.
  Reflection.Given StaticParams =>
  QD.Action Model a -> Model -> Model
fixupModelState :: forall a. Given StaticParams => Action Model a -> Model -> Model
fixupModelState Action Model a
cmd Model
model =
  case ModelState
st of
    ModelState
ModelPreSyncing
      | Bool
haaSatisfied ->
          Model -> Model
avoidTransientState (Model -> Model) -> Model -> Model
forall a b. (a -> b) -> a -> b
$
            Notable -> Bool -> Model -> Model
addNotableWhen Notable
PreSyncingToSyncingN Bool
True (Model -> Model) -> Model -> Model
forall a b. (a -> b) -> a -> b
$
              Model
model{mState = ModelSyncing}
      | Bool
otherwise ->
          Model
model
    ModelState
ModelSyncing
      | Bool -> Bool
not Bool
haaSatisfied ->
          Notable -> Bool -> Model -> Model
addNotableWhen Notable
SyncingToPreSyncingN Bool
True (Model -> Model) -> Model -> Model
forall a b. (a -> b) -> a -> b
$
            Model
model{mState = ModelPreSyncing}
      | Bool
caughtUp ->
          -- ASSUMPTION This new state was /NOT/ incurred by the 'TimePasses'
          -- command.
          --
          -- Therefore the current clock is necessarily the correct timestamp
          -- to record.
          Notable -> Bool -> Model -> Model
addNotableWhen Notable
CaughtUpN Bool
True (Model -> Model) -> Model -> Model
forall a b. (a -> b) -> a -> b
$
            Model
model{mState = ModelCaughtUp clk}
      | Bool
otherwise ->
          Model
model
    ModelCaughtUp Time
timestamp
      | Time -> Bool
flicker Time
timestamp ->
          Notable -> Bool -> Model -> Model
addNotableWhen Notable
FlickerN Bool
True (Model -> Model) -> Model -> Model
forall a b. (a -> b) -> a -> b
$
            Model
model{mState = ModelCaughtUp (flickerTimestamp timestamp)}
      | Time -> Bool
fellBehind Time
timestamp ->
          Model -> Model
avoidTransientState (Model -> Model) -> Model -> Model
forall a b. (a -> b) -> a -> b
$
            Notable -> Bool -> Model -> Model
addNotableWhen Notable
FellBehindN Bool
True (Model -> Model) -> Model -> Model
forall a b. (a -> b) -> a -> b
$
              Model
model{mState = ModelPreSyncing}
      | Bool
otherwise ->
          -- NB in this branch, these notables are mutually exclusive
          Notable -> Bool -> Model -> Model
addNotableWhen Notable
TooOldN (Time
expiryAge Time -> Time -> Bool
forall a. Ord a => a -> a -> Bool
< Time
clk)
            (Model -> Model) -> Model -> Model
forall a b. (a -> b) -> a -> b
$ Notable -> Bool -> Model -> Model
addNotableWhen
              Notable
NotThrashingN
              (DiffTime -> Time
SI.Time DiffTime
0 Time -> Time -> Bool
forall a. Ord a => a -> a -> Bool
< Time
timestamp Bool -> Bool -> Bool
&& Time -> Time
expiryThrashing Time
timestamp Time -> Time -> Bool
forall a. Ord a => a -> a -> Bool
< Time
clk)
            (Model -> Model) -> Model -> Model
forall a b. (a -> b) -> a -> b
$ Model
model
 where
  Model
    { mCandidates :: Model -> Map UpstreamPeer Candidate
mCandidates = Map UpstreamPeer Candidate
cands
    , mClock :: Model -> Time
mClock = Time
clk
    , mIdlers :: Model -> Set UpstreamPeer
mIdlers = Set UpstreamPeer
idlers
    , mSelection :: Model -> Selection
mSelection = Selection
sel
    , mState :: Model -> ModelState
mState = ModelState
st
    } = Model
model

  StaticParams{Set UpstreamPeer -> Bool
pIsHaaSatisfied :: StaticParams -> Set UpstreamPeer -> Bool
pIsHaaSatisfied :: Set UpstreamPeer -> Bool
pIsHaaSatisfied} = StaticParams
forall a. Given a => a
Reflection.given

  haaSatisfied :: Bool
haaSatisfied = Set UpstreamPeer -> Bool
pIsHaaSatisfied (Set UpstreamPeer -> Bool) -> Set UpstreamPeer -> Bool
forall a b. (a -> b) -> a -> b
$ Map UpstreamPeer Candidate -> Set UpstreamPeer
forall k a. Map k a -> Set k
Map.keysSet Map UpstreamPeer Candidate
cands
  caughtUp :: Bool
caughtUp = Bool
some Bool -> Bool -> Bool
&& Bool
allIdling Bool -> Bool -> Bool
&& (Candidate -> Bool) -> Map UpstreamPeer Candidate -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Candidate -> Bool
ok Map UpstreamPeer Candidate
cands
  fellBehind :: Time -> Bool
fellBehind Time
timestamp = Time -> Time
expiry Time
timestamp Time -> Time -> Bool
forall a. Ord a => a -> a -> Bool
< Time
clk -- NB 'boringDur' prevents ==
  flicker :: Time -> Bool
flicker Time
timestamp = Time -> Bool
fellBehind Time
timestamp Bool -> Bool -> Bool
&& Bool
caughtUp Bool -> Bool -> Bool
&& Bool
haaSatisfied

  some :: Bool
some = Int
0 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Map UpstreamPeer Candidate -> Int
forall k a. Map k a -> Int
Map.size Map UpstreamPeer Candidate
cands

  allIdling :: Bool
allIdling = Set UpstreamPeer
idlers Set UpstreamPeer -> Set UpstreamPeer -> Bool
forall a. Eq a => a -> a -> Bool
== Map UpstreamPeer Candidate -> Set UpstreamPeer
forall k a. Map k a -> Set k
Map.keysSet Map UpstreamPeer Candidate
cands

  ok :: Candidate -> Bool
ok Candidate
cand =
    Bool -> CandidateVersusSelection
GSM.WhetherCandidateIsBetter Bool
False CandidateVersusSelection -> CandidateVersusSelection -> Bool
forall a. Eq a => a -> a -> Bool
== Selection -> Candidate -> CandidateVersusSelection
candidateOverSelection Selection
sel Candidate
cand

  -- the first time the node would transition to PreSyncing
  expiry :: Time -> Time
expiry Time
timestamp = Time
expiryAge Time -> Time -> Time
forall a. Ord a => a -> a -> a
`max` Time -> Time
expiryThrashing Time
timestamp
  expiryAge :: Time
expiryAge = DiffTime -> Time -> Time
SI.addTime DiffTime
forall a. Num a => a
ageLimit (Selection -> Time
onset Selection
sel)
  expiryThrashing :: Time -> Time
expiryThrashing Time
timestamp = DiffTime -> Time -> Time
SI.addTime DiffTime
forall a. Num a => a
thrashLimit Time
timestamp

  -- It's possible for the node to instantly return to CaughtUp, but that
  -- might have happened /during/ the 'TimePasses' command, not only when it
  -- ends.
  --
  -- Therefore the age limit of the selection is the correct timestamp to
  -- record, instead of the current clock (ie when the 'TimePasses' ended).
  --
  -- NOTE Superficially, in the real implementation, the Diffusion Layer
  -- should be discarding all peers when transitioning from CaughtUp to
  -- PreSyncing. However, it would be plausible for an implementation to
  -- retain any bootstrap/ledger peers it happened to have, so the
  -- idiosyncratic behavior of the system under test in this module is not
  -- totally irrelevant.
  --
  -- the /last/ time the node instantaneously visited PreSyncing during the
  -- 'TimePasses' command, assuming it did so at least once
  flickerTimestamp :: Time -> Time
flickerTimestamp Time
timestamp = case Action Model a
cmd of
    ExtendSelection S
sdel
      | S
sdel S -> S -> Bool
forall a. Ord a => a -> a -> Bool
< S
0 ->
          Time
clk
    TimePasses{} ->
      (Time -> Time -> Time) -> Time -> [Time] -> Time
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl Time -> Time -> Time
forall a. Ord a => a -> a -> a
max (Time -> Time
expiry Time
timestamp) ([Time] -> Time) -> [Time] -> Time
forall a b. (a -> b) -> a -> b
$
        (Time -> Bool) -> [Time] -> [Time]
forall a. (a -> Bool) -> [a] -> [a]
takeWhile (Time -> Time -> Bool
forall a. Ord a => a -> a -> Bool
< Time
clk) ([Time] -> [Time]) -> [Time] -> [Time]
forall a b. (a -> b) -> a -> b
$ -- NB 'boringDur' prevents ==
          (Time -> Time) -> Time -> [Time]
forall a. (a -> a) -> a -> [a]
iterate (DiffTime -> Time -> Time
SI.addTime DiffTime
forall a. Num a => a
thrashLimit) (Time -> Time
expiry Time
timestamp)
    Action Model a
_ ->
      TestName -> Time
forall a. HasCallStack => TestName -> a
error (TestName -> Time) -> TestName -> Time
forall a b. (a -> b) -> a -> b
$
        TestName
"impossible! flicker but neither "
          TestName -> TestName -> TestName
forall a. Semigroup a => a -> a -> a
<> TestName
"negative ExtendSelection nor TimePasses: "
          TestName -> TestName -> TestName
forall a. Semigroup a => a -> a -> a
<> Action Model a -> TestName
forall a. Show a => a -> TestName
show Action Model a
cmd

  avoidTransientState :: Model -> Model
  avoidTransientState :: Model -> Model
avoidTransientState = Action Model a -> Model -> Model
forall a. Given StaticParams => Action Model a -> Model -> Model
fixupModelState Action Model a
cmd

-- | A block count
newtype B = B Int
  deriving stock (B -> B -> Bool
(B -> B -> Bool) -> (B -> B -> Bool) -> Eq B
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: B -> B -> Bool
== :: B -> B -> Bool
$c/= :: B -> B -> Bool
/= :: B -> B -> Bool
Eq, Eq B
Eq B =>
(B -> B -> Ordering)
-> (B -> B -> Bool)
-> (B -> B -> Bool)
-> (B -> B -> Bool)
-> (B -> B -> Bool)
-> (B -> B -> B)
-> (B -> B -> B)
-> Ord B
B -> B -> Bool
B -> B -> Ordering
B -> B -> B
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: B -> B -> Ordering
compare :: B -> B -> Ordering
$c< :: B -> B -> Bool
< :: B -> B -> Bool
$c<= :: B -> B -> Bool
<= :: B -> B -> Bool
$c> :: B -> B -> Bool
> :: B -> B -> Bool
$c>= :: B -> B -> Bool
>= :: B -> B -> Bool
$cmax :: B -> B -> B
max :: B -> B -> B
$cmin :: B -> B -> B
min :: B -> B -> B
Ord, (forall x. B -> Rep B x) -> (forall x. Rep B x -> B) -> Generic B
forall x. Rep B x -> B
forall x. B -> Rep B x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. B -> Rep B x
from :: forall x. B -> Rep B x
$cto :: forall x. Rep B x -> B
to :: forall x. Rep B x -> B
Generic, ReadPrec [B]
ReadPrec B
Int -> ReadS B
ReadS [B]
(Int -> ReadS B)
-> ReadS [B] -> ReadPrec B -> ReadPrec [B] -> Read B
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS B
readsPrec :: Int -> ReadS B
$creadList :: ReadS [B]
readList :: ReadS [B]
$creadPrec :: ReadPrec B
readPrec :: ReadPrec B
$creadListPrec :: ReadPrec [B]
readListPrec :: ReadPrec [B]
Read, Int -> B -> TestName -> TestName
[B] -> TestName -> TestName
B -> TestName
(Int -> B -> TestName -> TestName)
-> (B -> TestName) -> ([B] -> TestName -> TestName) -> Show B
forall a.
(Int -> a -> TestName -> TestName)
-> (a -> TestName) -> ([a] -> TestName -> TestName) -> Show a
$cshowsPrec :: Int -> B -> TestName -> TestName
showsPrec :: Int -> B -> TestName -> TestName
$cshow :: B -> TestName
show :: B -> TestName
$cshowList :: [B] -> TestName -> TestName
showList :: [B] -> TestName -> TestName
Show)
  deriving newtype (Int -> B
B -> Int
B -> [B]
B -> B
B -> B -> [B]
B -> B -> B -> [B]
(B -> B)
-> (B -> B)
-> (Int -> B)
-> (B -> Int)
-> (B -> [B])
-> (B -> B -> [B])
-> (B -> B -> [B])
-> (B -> B -> B -> [B])
-> Enum B
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: B -> B
succ :: B -> B
$cpred :: B -> B
pred :: B -> B
$ctoEnum :: Int -> B
toEnum :: Int -> B
$cfromEnum :: B -> Int
fromEnum :: B -> Int
$cenumFrom :: B -> [B]
enumFrom :: B -> [B]
$cenumFromThen :: B -> B -> [B]
enumFromThen :: B -> B -> [B]
$cenumFromTo :: B -> B -> [B]
enumFromTo :: B -> B -> [B]
$cenumFromThenTo :: B -> B -> B -> [B]
enumFromThenTo :: B -> B -> B -> [B]
Enum, Integer -> B
B -> B
B -> B -> B
(B -> B -> B)
-> (B -> B -> B)
-> (B -> B -> B)
-> (B -> B)
-> (B -> B)
-> (B -> B)
-> (Integer -> B)
-> Num B
forall a.
(a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> (Integer -> a)
-> Num a
$c+ :: B -> B -> B
+ :: B -> B -> B
$c- :: B -> B -> B
- :: B -> B -> B
$c* :: B -> B -> B
* :: B -> B -> B
$cnegate :: B -> B
negate :: B -> B
$cabs :: B -> B
abs :: B -> B
$csignum :: B -> B
signum :: B -> B
$cfromInteger :: Integer -> B
fromInteger :: Integer -> B
Num)
  deriving anyclass [B] -> Expr
B -> Expr
(B -> Expr) -> ([B] -> Expr) -> ToExpr B
forall a. (a -> Expr) -> ([a] -> Expr) -> ToExpr a
$ctoExpr :: B -> Expr
toExpr :: B -> Expr
$clistToExpr :: [B] -> Expr
listToExpr :: [B] -> Expr
TD.ToExpr

-- | A slot count
newtype S = S Int
  deriving stock (S -> S -> Bool
(S -> S -> Bool) -> (S -> S -> Bool) -> Eq S
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: S -> S -> Bool
== :: S -> S -> Bool
$c/= :: S -> S -> Bool
/= :: S -> S -> Bool
Eq, Eq S
Eq S =>
(S -> S -> Ordering)
-> (S -> S -> Bool)
-> (S -> S -> Bool)
-> (S -> S -> Bool)
-> (S -> S -> Bool)
-> (S -> S -> S)
-> (S -> S -> S)
-> Ord S
S -> S -> Bool
S -> S -> Ordering
S -> S -> S
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: S -> S -> Ordering
compare :: S -> S -> Ordering
$c< :: S -> S -> Bool
< :: S -> S -> Bool
$c<= :: S -> S -> Bool
<= :: S -> S -> Bool
$c> :: S -> S -> Bool
> :: S -> S -> Bool
$c>= :: S -> S -> Bool
>= :: S -> S -> Bool
$cmax :: S -> S -> S
max :: S -> S -> S
$cmin :: S -> S -> S
min :: S -> S -> S
Ord, (forall x. S -> Rep S x) -> (forall x. Rep S x -> S) -> Generic S
forall x. Rep S x -> S
forall x. S -> Rep S x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. S -> Rep S x
from :: forall x. S -> Rep S x
$cto :: forall x. Rep S x -> S
to :: forall x. Rep S x -> S
Generic, ReadPrec [S]
ReadPrec S
Int -> ReadS S
ReadS [S]
(Int -> ReadS S)
-> ReadS [S] -> ReadPrec S -> ReadPrec [S] -> Read S
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS S
readsPrec :: Int -> ReadS S
$creadList :: ReadS [S]
readList :: ReadS [S]
$creadPrec :: ReadPrec S
readPrec :: ReadPrec S
$creadListPrec :: ReadPrec [S]
readListPrec :: ReadPrec [S]
Read, Int -> S -> TestName -> TestName
[S] -> TestName -> TestName
S -> TestName
(Int -> S -> TestName -> TestName)
-> (S -> TestName) -> ([S] -> TestName -> TestName) -> Show S
forall a.
(Int -> a -> TestName -> TestName)
-> (a -> TestName) -> ([a] -> TestName -> TestName) -> Show a
$cshowsPrec :: Int -> S -> TestName -> TestName
showsPrec :: Int -> S -> TestName -> TestName
$cshow :: S -> TestName
show :: S -> TestName
$cshowList :: [S] -> TestName -> TestName
showList :: [S] -> TestName -> TestName
Show)
  deriving newtype (Int -> S
S -> Int
S -> [S]
S -> S
S -> S -> [S]
S -> S -> S -> [S]
(S -> S)
-> (S -> S)
-> (Int -> S)
-> (S -> Int)
-> (S -> [S])
-> (S -> S -> [S])
-> (S -> S -> [S])
-> (S -> S -> S -> [S])
-> Enum S
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: S -> S
succ :: S -> S
$cpred :: S -> S
pred :: S -> S
$ctoEnum :: Int -> S
toEnum :: Int -> S
$cfromEnum :: S -> Int
fromEnum :: S -> Int
$cenumFrom :: S -> [S]
enumFrom :: S -> [S]
$cenumFromThen :: S -> S -> [S]
enumFromThen :: S -> S -> [S]
$cenumFromTo :: S -> S -> [S]
enumFromTo :: S -> S -> [S]
$cenumFromThenTo :: S -> S -> S -> [S]
enumFromThenTo :: S -> S -> S -> [S]
Enum, Integer -> S
S -> S
S -> S -> S
(S -> S -> S)
-> (S -> S -> S)
-> (S -> S -> S)
-> (S -> S)
-> (S -> S)
-> (S -> S)
-> (Integer -> S)
-> Num S
forall a.
(a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> (Integer -> a)
-> Num a
$c+ :: S -> S -> S
+ :: S -> S -> S
$c- :: S -> S -> S
- :: S -> S -> S
$c* :: S -> S -> S
* :: S -> S -> S
$cnegate :: S -> S
negate :: S -> S
$cabs :: S -> S
abs :: S -> S
$csignum :: S -> S
signum :: S -> S
$cfromInteger :: Integer -> S
fromInteger :: Integer -> S
Num)
  deriving anyclass [S] -> Expr
S -> Expr
(S -> Expr) -> ([S] -> Expr) -> ToExpr S
forall a. (a -> Expr) -> ([a] -> Expr) -> ToExpr a
$ctoExpr :: S -> Expr
toExpr :: S -> Expr
$clistToExpr :: [S] -> Expr
listToExpr :: [S] -> Expr
TD.ToExpr

data UpstreamPeer = Amara | Bao | Cait | Dhani | Eric
  deriving stock (UpstreamPeer
UpstreamPeer -> UpstreamPeer -> Bounded UpstreamPeer
forall a. a -> a -> Bounded a
$cminBound :: UpstreamPeer
minBound :: UpstreamPeer
$cmaxBound :: UpstreamPeer
maxBound :: UpstreamPeer
Bounded, Int -> UpstreamPeer
UpstreamPeer -> Int
UpstreamPeer -> [UpstreamPeer]
UpstreamPeer -> UpstreamPeer
UpstreamPeer -> UpstreamPeer -> [UpstreamPeer]
UpstreamPeer -> UpstreamPeer -> UpstreamPeer -> [UpstreamPeer]
(UpstreamPeer -> UpstreamPeer)
-> (UpstreamPeer -> UpstreamPeer)
-> (Int -> UpstreamPeer)
-> (UpstreamPeer -> Int)
-> (UpstreamPeer -> [UpstreamPeer])
-> (UpstreamPeer -> UpstreamPeer -> [UpstreamPeer])
-> (UpstreamPeer -> UpstreamPeer -> [UpstreamPeer])
-> (UpstreamPeer -> UpstreamPeer -> UpstreamPeer -> [UpstreamPeer])
-> Enum UpstreamPeer
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
$csucc :: UpstreamPeer -> UpstreamPeer
succ :: UpstreamPeer -> UpstreamPeer
$cpred :: UpstreamPeer -> UpstreamPeer
pred :: UpstreamPeer -> UpstreamPeer
$ctoEnum :: Int -> UpstreamPeer
toEnum :: Int -> UpstreamPeer
$cfromEnum :: UpstreamPeer -> Int
fromEnum :: UpstreamPeer -> Int
$cenumFrom :: UpstreamPeer -> [UpstreamPeer]
enumFrom :: UpstreamPeer -> [UpstreamPeer]
$cenumFromThen :: UpstreamPeer -> UpstreamPeer -> [UpstreamPeer]
enumFromThen :: UpstreamPeer -> UpstreamPeer -> [UpstreamPeer]
$cenumFromTo :: UpstreamPeer -> UpstreamPeer -> [UpstreamPeer]
enumFromTo :: UpstreamPeer -> UpstreamPeer -> [UpstreamPeer]
$cenumFromThenTo :: UpstreamPeer -> UpstreamPeer -> UpstreamPeer -> [UpstreamPeer]
enumFromThenTo :: UpstreamPeer -> UpstreamPeer -> UpstreamPeer -> [UpstreamPeer]
Enum, UpstreamPeer -> UpstreamPeer -> Bool
(UpstreamPeer -> UpstreamPeer -> Bool)
-> (UpstreamPeer -> UpstreamPeer -> Bool) -> Eq UpstreamPeer
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: UpstreamPeer -> UpstreamPeer -> Bool
== :: UpstreamPeer -> UpstreamPeer -> Bool
$c/= :: UpstreamPeer -> UpstreamPeer -> Bool
/= :: UpstreamPeer -> UpstreamPeer -> Bool
Eq, Eq UpstreamPeer
Eq UpstreamPeer =>
(UpstreamPeer -> UpstreamPeer -> Ordering)
-> (UpstreamPeer -> UpstreamPeer -> Bool)
-> (UpstreamPeer -> UpstreamPeer -> Bool)
-> (UpstreamPeer -> UpstreamPeer -> Bool)
-> (UpstreamPeer -> UpstreamPeer -> Bool)
-> (UpstreamPeer -> UpstreamPeer -> UpstreamPeer)
-> (UpstreamPeer -> UpstreamPeer -> UpstreamPeer)
-> Ord UpstreamPeer
UpstreamPeer -> UpstreamPeer -> Bool
UpstreamPeer -> UpstreamPeer -> Ordering
UpstreamPeer -> UpstreamPeer -> UpstreamPeer
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: UpstreamPeer -> UpstreamPeer -> Ordering
compare :: UpstreamPeer -> UpstreamPeer -> Ordering
$c< :: UpstreamPeer -> UpstreamPeer -> Bool
< :: UpstreamPeer -> UpstreamPeer -> Bool
$c<= :: UpstreamPeer -> UpstreamPeer -> Bool
<= :: UpstreamPeer -> UpstreamPeer -> Bool
$c> :: UpstreamPeer -> UpstreamPeer -> Bool
> :: UpstreamPeer -> UpstreamPeer -> Bool
$c>= :: UpstreamPeer -> UpstreamPeer -> Bool
>= :: UpstreamPeer -> UpstreamPeer -> Bool
$cmax :: UpstreamPeer -> UpstreamPeer -> UpstreamPeer
max :: UpstreamPeer -> UpstreamPeer -> UpstreamPeer
$cmin :: UpstreamPeer -> UpstreamPeer -> UpstreamPeer
min :: UpstreamPeer -> UpstreamPeer -> UpstreamPeer
Ord, (forall x. UpstreamPeer -> Rep UpstreamPeer x)
-> (forall x. Rep UpstreamPeer x -> UpstreamPeer)
-> Generic UpstreamPeer
forall x. Rep UpstreamPeer x -> UpstreamPeer
forall x. UpstreamPeer -> Rep UpstreamPeer x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. UpstreamPeer -> Rep UpstreamPeer x
from :: forall x. UpstreamPeer -> Rep UpstreamPeer x
$cto :: forall x. Rep UpstreamPeer x -> UpstreamPeer
to :: forall x. Rep UpstreamPeer x -> UpstreamPeer
Generic, ReadPrec [UpstreamPeer]
ReadPrec UpstreamPeer
Int -> ReadS UpstreamPeer
ReadS [UpstreamPeer]
(Int -> ReadS UpstreamPeer)
-> ReadS [UpstreamPeer]
-> ReadPrec UpstreamPeer
-> ReadPrec [UpstreamPeer]
-> Read UpstreamPeer
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS UpstreamPeer
readsPrec :: Int -> ReadS UpstreamPeer
$creadList :: ReadS [UpstreamPeer]
readList :: ReadS [UpstreamPeer]
$creadPrec :: ReadPrec UpstreamPeer
readPrec :: ReadPrec UpstreamPeer
$creadListPrec :: ReadPrec [UpstreamPeer]
readListPrec :: ReadPrec [UpstreamPeer]
Read, Int -> UpstreamPeer -> TestName -> TestName
[UpstreamPeer] -> TestName -> TestName
UpstreamPeer -> TestName
(Int -> UpstreamPeer -> TestName -> TestName)
-> (UpstreamPeer -> TestName)
-> ([UpstreamPeer] -> TestName -> TestName)
-> Show UpstreamPeer
forall a.
(Int -> a -> TestName -> TestName)
-> (a -> TestName) -> ([a] -> TestName -> TestName) -> Show a
$cshowsPrec :: Int -> UpstreamPeer -> TestName -> TestName
showsPrec :: Int -> UpstreamPeer -> TestName -> TestName
$cshow :: UpstreamPeer -> TestName
show :: UpstreamPeer -> TestName
$cshowList :: [UpstreamPeer] -> TestName -> TestName
showList :: [UpstreamPeer] -> TestName -> TestName
Show)
  deriving anyclass ([UpstreamPeer] -> Expr
UpstreamPeer -> Expr
(UpstreamPeer -> Expr)
-> ([UpstreamPeer] -> Expr) -> ToExpr UpstreamPeer
forall a. (a -> Expr) -> ([a] -> Expr) -> ToExpr a
$ctoExpr :: UpstreamPeer -> Expr
toExpr :: UpstreamPeer -> Expr
$clistToExpr :: [UpstreamPeer] -> Expr
listToExpr :: [UpstreamPeer] -> Expr
TD.ToExpr, (forall b. UpstreamPeer -> Gen b -> Gen b)
-> CoArbitrary UpstreamPeer
forall b. UpstreamPeer -> Gen b -> Gen b
forall a. (forall b. a -> Gen b -> Gen b) -> CoArbitrary a
$ccoarbitrary :: forall b. UpstreamPeer -> Gen b -> Gen b
coarbitrary :: forall b. UpstreamPeer -> Gen b -> Gen b
QC.CoArbitrary, (forall b. (UpstreamPeer -> b) -> UpstreamPeer :-> b)
-> Function UpstreamPeer
forall b. (UpstreamPeer -> b) -> UpstreamPeer :-> b
forall a. (forall b. (a -> b) -> a :-> b) -> Function a
$cfunction :: forall b. (UpstreamPeer -> b) -> UpstreamPeer :-> b
function :: forall b. (UpstreamPeer -> b) -> UpstreamPeer :-> b
QC.Function)

-- | The cumulative growth relative to whatever length the initial selection
-- was and the slot relative to the start of the test (which is assumed to be
-- the exact onset of some slot)
data Selection = Selection !B !S
  deriving stock (Selection -> Selection -> Bool
(Selection -> Selection -> Bool)
-> (Selection -> Selection -> Bool) -> Eq Selection
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Selection -> Selection -> Bool
== :: Selection -> Selection -> Bool
$c/= :: Selection -> Selection -> Bool
/= :: Selection -> Selection -> Bool
Eq, Eq Selection
Eq Selection =>
(Selection -> Selection -> Ordering)
-> (Selection -> Selection -> Bool)
-> (Selection -> Selection -> Bool)
-> (Selection -> Selection -> Bool)
-> (Selection -> Selection -> Bool)
-> (Selection -> Selection -> Selection)
-> (Selection -> Selection -> Selection)
-> Ord Selection
Selection -> Selection -> Bool
Selection -> Selection -> Ordering
Selection -> Selection -> Selection
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Selection -> Selection -> Ordering
compare :: Selection -> Selection -> Ordering
$c< :: Selection -> Selection -> Bool
< :: Selection -> Selection -> Bool
$c<= :: Selection -> Selection -> Bool
<= :: Selection -> Selection -> Bool
$c> :: Selection -> Selection -> Bool
> :: Selection -> Selection -> Bool
$c>= :: Selection -> Selection -> Bool
>= :: Selection -> Selection -> Bool
$cmax :: Selection -> Selection -> Selection
max :: Selection -> Selection -> Selection
$cmin :: Selection -> Selection -> Selection
min :: Selection -> Selection -> Selection
Ord, (forall x. Selection -> Rep Selection x)
-> (forall x. Rep Selection x -> Selection) -> Generic Selection
forall x. Rep Selection x -> Selection
forall x. Selection -> Rep Selection x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Selection -> Rep Selection x
from :: forall x. Selection -> Rep Selection x
$cto :: forall x. Rep Selection x -> Selection
to :: forall x. Rep Selection x -> Selection
Generic, Int -> Selection -> TestName -> TestName
[Selection] -> TestName -> TestName
Selection -> TestName
(Int -> Selection -> TestName -> TestName)
-> (Selection -> TestName)
-> ([Selection] -> TestName -> TestName)
-> Show Selection
forall a.
(Int -> a -> TestName -> TestName)
-> (a -> TestName) -> ([a] -> TestName -> TestName) -> Show a
$cshowsPrec :: Int -> Selection -> TestName -> TestName
showsPrec :: Int -> Selection -> TestName -> TestName
$cshow :: Selection -> TestName
show :: Selection -> TestName
$cshowList :: [Selection] -> TestName -> TestName
showList :: [Selection] -> TestName -> TestName
Show)
  deriving anyclass [Selection] -> Expr
Selection -> Expr
(Selection -> Expr) -> ([Selection] -> Expr) -> ToExpr Selection
forall a. (a -> Expr) -> ([a] -> Expr) -> ToExpr a
$ctoExpr :: Selection -> Expr
toExpr :: Selection -> Expr
$clistToExpr :: [Selection] -> Expr
listToExpr :: [Selection] -> Expr
TD.ToExpr

-- | The age of the candidate is irrelevant, only its length matters
newtype Candidate = Candidate B
  deriving stock (Candidate -> Candidate -> Bool
(Candidate -> Candidate -> Bool)
-> (Candidate -> Candidate -> Bool) -> Eq Candidate
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Candidate -> Candidate -> Bool
== :: Candidate -> Candidate -> Bool
$c/= :: Candidate -> Candidate -> Bool
/= :: Candidate -> Candidate -> Bool
Eq, Eq Candidate
Eq Candidate =>
(Candidate -> Candidate -> Ordering)
-> (Candidate -> Candidate -> Bool)
-> (Candidate -> Candidate -> Bool)
-> (Candidate -> Candidate -> Bool)
-> (Candidate -> Candidate -> Bool)
-> (Candidate -> Candidate -> Candidate)
-> (Candidate -> Candidate -> Candidate)
-> Ord Candidate
Candidate -> Candidate -> Bool
Candidate -> Candidate -> Ordering
Candidate -> Candidate -> Candidate
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Candidate -> Candidate -> Ordering
compare :: Candidate -> Candidate -> Ordering
$c< :: Candidate -> Candidate -> Bool
< :: Candidate -> Candidate -> Bool
$c<= :: Candidate -> Candidate -> Bool
<= :: Candidate -> Candidate -> Bool
$c> :: Candidate -> Candidate -> Bool
> :: Candidate -> Candidate -> Bool
$c>= :: Candidate -> Candidate -> Bool
>= :: Candidate -> Candidate -> Bool
$cmax :: Candidate -> Candidate -> Candidate
max :: Candidate -> Candidate -> Candidate
$cmin :: Candidate -> Candidate -> Candidate
min :: Candidate -> Candidate -> Candidate
Ord, (forall x. Candidate -> Rep Candidate x)
-> (forall x. Rep Candidate x -> Candidate) -> Generic Candidate
forall x. Rep Candidate x -> Candidate
forall x. Candidate -> Rep Candidate x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Candidate -> Rep Candidate x
from :: forall x. Candidate -> Rep Candidate x
$cto :: forall x. Rep Candidate x -> Candidate
to :: forall x. Rep Candidate x -> Candidate
Generic, Int -> Candidate -> TestName -> TestName
[Candidate] -> TestName -> TestName
Candidate -> TestName
(Int -> Candidate -> TestName -> TestName)
-> (Candidate -> TestName)
-> ([Candidate] -> TestName -> TestName)
-> Show Candidate
forall a.
(Int -> a -> TestName -> TestName)
-> (a -> TestName) -> ([a] -> TestName -> TestName) -> Show a
$cshowsPrec :: Int -> Candidate -> TestName -> TestName
showsPrec :: Int -> Candidate -> TestName -> TestName
$cshow :: Candidate -> TestName
show :: Candidate -> TestName
$cshowList :: [Candidate] -> TestName -> TestName
showList :: [Candidate] -> TestName -> TestName
Show)
  deriving anyclass [Candidate] -> Expr
Candidate -> Expr
(Candidate -> Expr) -> ([Candidate] -> Expr) -> ToExpr Candidate
forall a. (a -> Expr) -> ([a] -> Expr) -> ToExpr a
$ctoExpr :: Candidate -> Expr
toExpr :: Candidate -> Expr
$clistToExpr :: [Candidate] -> Expr
listToExpr :: [Candidate] -> Expr
TD.ToExpr

data MarkerState = Present | Absent
  deriving stock (MarkerState -> MarkerState -> Bool
(MarkerState -> MarkerState -> Bool)
-> (MarkerState -> MarkerState -> Bool) -> Eq MarkerState
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: MarkerState -> MarkerState -> Bool
== :: MarkerState -> MarkerState -> Bool
$c/= :: MarkerState -> MarkerState -> Bool
/= :: MarkerState -> MarkerState -> Bool
Eq, Eq MarkerState
Eq MarkerState =>
(MarkerState -> MarkerState -> Ordering)
-> (MarkerState -> MarkerState -> Bool)
-> (MarkerState -> MarkerState -> Bool)
-> (MarkerState -> MarkerState -> Bool)
-> (MarkerState -> MarkerState -> Bool)
-> (MarkerState -> MarkerState -> MarkerState)
-> (MarkerState -> MarkerState -> MarkerState)
-> Ord MarkerState
MarkerState -> MarkerState -> Bool
MarkerState -> MarkerState -> Ordering
MarkerState -> MarkerState -> MarkerState
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: MarkerState -> MarkerState -> Ordering
compare :: MarkerState -> MarkerState -> Ordering
$c< :: MarkerState -> MarkerState -> Bool
< :: MarkerState -> MarkerState -> Bool
$c<= :: MarkerState -> MarkerState -> Bool
<= :: MarkerState -> MarkerState -> Bool
$c> :: MarkerState -> MarkerState -> Bool
> :: MarkerState -> MarkerState -> Bool
$c>= :: MarkerState -> MarkerState -> Bool
>= :: MarkerState -> MarkerState -> Bool
$cmax :: MarkerState -> MarkerState -> MarkerState
max :: MarkerState -> MarkerState -> MarkerState
$cmin :: MarkerState -> MarkerState -> MarkerState
min :: MarkerState -> MarkerState -> MarkerState
Ord, (forall x. MarkerState -> Rep MarkerState x)
-> (forall x. Rep MarkerState x -> MarkerState)
-> Generic MarkerState
forall x. Rep MarkerState x -> MarkerState
forall x. MarkerState -> Rep MarkerState x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. MarkerState -> Rep MarkerState x
from :: forall x. MarkerState -> Rep MarkerState x
$cto :: forall x. Rep MarkerState x -> MarkerState
to :: forall x. Rep MarkerState x -> MarkerState
Generic, ReadPrec [MarkerState]
ReadPrec MarkerState
Int -> ReadS MarkerState
ReadS [MarkerState]
(Int -> ReadS MarkerState)
-> ReadS [MarkerState]
-> ReadPrec MarkerState
-> ReadPrec [MarkerState]
-> Read MarkerState
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS MarkerState
readsPrec :: Int -> ReadS MarkerState
$creadList :: ReadS [MarkerState]
readList :: ReadS [MarkerState]
$creadPrec :: ReadPrec MarkerState
readPrec :: ReadPrec MarkerState
$creadListPrec :: ReadPrec [MarkerState]
readListPrec :: ReadPrec [MarkerState]
Read, Int -> MarkerState -> TestName -> TestName
[MarkerState] -> TestName -> TestName
MarkerState -> TestName
(Int -> MarkerState -> TestName -> TestName)
-> (MarkerState -> TestName)
-> ([MarkerState] -> TestName -> TestName)
-> Show MarkerState
forall a.
(Int -> a -> TestName -> TestName)
-> (a -> TestName) -> ([a] -> TestName -> TestName) -> Show a
$cshowsPrec :: Int -> MarkerState -> TestName -> TestName
showsPrec :: Int -> MarkerState -> TestName -> TestName
$cshow :: MarkerState -> TestName
show :: MarkerState -> TestName
$cshowList :: [MarkerState] -> TestName -> TestName
showList :: [MarkerState] -> TestName -> TestName
Show)
  deriving anyclass [MarkerState] -> Expr
MarkerState -> Expr
(MarkerState -> Expr)
-> ([MarkerState] -> Expr) -> ToExpr MarkerState
forall a. (a -> Expr) -> ([a] -> Expr) -> ToExpr a
$ctoExpr :: MarkerState -> Expr
toExpr :: MarkerState -> Expr
$clistToExpr :: [MarkerState] -> Expr
listToExpr :: [MarkerState] -> Expr
TD.ToExpr

newtype WhetherPrevTimePasses = WhetherPrevTimePasses Bool
  deriving stock (WhetherPrevTimePasses -> WhetherPrevTimePasses -> Bool
(WhetherPrevTimePasses -> WhetherPrevTimePasses -> Bool)
-> (WhetherPrevTimePasses -> WhetherPrevTimePasses -> Bool)
-> Eq WhetherPrevTimePasses
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: WhetherPrevTimePasses -> WhetherPrevTimePasses -> Bool
== :: WhetherPrevTimePasses -> WhetherPrevTimePasses -> Bool
$c/= :: WhetherPrevTimePasses -> WhetherPrevTimePasses -> Bool
/= :: WhetherPrevTimePasses -> WhetherPrevTimePasses -> Bool
Eq, Eq WhetherPrevTimePasses
Eq WhetherPrevTimePasses =>
(WhetherPrevTimePasses -> WhetherPrevTimePasses -> Ordering)
-> (WhetherPrevTimePasses -> WhetherPrevTimePasses -> Bool)
-> (WhetherPrevTimePasses -> WhetherPrevTimePasses -> Bool)
-> (WhetherPrevTimePasses -> WhetherPrevTimePasses -> Bool)
-> (WhetherPrevTimePasses -> WhetherPrevTimePasses -> Bool)
-> (WhetherPrevTimePasses
    -> WhetherPrevTimePasses -> WhetherPrevTimePasses)
-> (WhetherPrevTimePasses
    -> WhetherPrevTimePasses -> WhetherPrevTimePasses)
-> Ord WhetherPrevTimePasses
WhetherPrevTimePasses -> WhetherPrevTimePasses -> Bool
WhetherPrevTimePasses -> WhetherPrevTimePasses -> Ordering
WhetherPrevTimePasses
-> WhetherPrevTimePasses -> WhetherPrevTimePasses
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: WhetherPrevTimePasses -> WhetherPrevTimePasses -> Ordering
compare :: WhetherPrevTimePasses -> WhetherPrevTimePasses -> Ordering
$c< :: WhetherPrevTimePasses -> WhetherPrevTimePasses -> Bool
< :: WhetherPrevTimePasses -> WhetherPrevTimePasses -> Bool
$c<= :: WhetherPrevTimePasses -> WhetherPrevTimePasses -> Bool
<= :: WhetherPrevTimePasses -> WhetherPrevTimePasses -> Bool
$c> :: WhetherPrevTimePasses -> WhetherPrevTimePasses -> Bool
> :: WhetherPrevTimePasses -> WhetherPrevTimePasses -> Bool
$c>= :: WhetherPrevTimePasses -> WhetherPrevTimePasses -> Bool
>= :: WhetherPrevTimePasses -> WhetherPrevTimePasses -> Bool
$cmax :: WhetherPrevTimePasses
-> WhetherPrevTimePasses -> WhetherPrevTimePasses
max :: WhetherPrevTimePasses
-> WhetherPrevTimePasses -> WhetherPrevTimePasses
$cmin :: WhetherPrevTimePasses
-> WhetherPrevTimePasses -> WhetherPrevTimePasses
min :: WhetherPrevTimePasses
-> WhetherPrevTimePasses -> WhetherPrevTimePasses
Ord, (forall x. WhetherPrevTimePasses -> Rep WhetherPrevTimePasses x)
-> (forall x. Rep WhetherPrevTimePasses x -> WhetherPrevTimePasses)
-> Generic WhetherPrevTimePasses
forall x. Rep WhetherPrevTimePasses x -> WhetherPrevTimePasses
forall x. WhetherPrevTimePasses -> Rep WhetherPrevTimePasses x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. WhetherPrevTimePasses -> Rep WhetherPrevTimePasses x
from :: forall x. WhetherPrevTimePasses -> Rep WhetherPrevTimePasses x
$cto :: forall x. Rep WhetherPrevTimePasses x -> WhetherPrevTimePasses
to :: forall x. Rep WhetherPrevTimePasses x -> WhetherPrevTimePasses
Generic, Int -> WhetherPrevTimePasses -> TestName -> TestName
[WhetherPrevTimePasses] -> TestName -> TestName
WhetherPrevTimePasses -> TestName
(Int -> WhetherPrevTimePasses -> TestName -> TestName)
-> (WhetherPrevTimePasses -> TestName)
-> ([WhetherPrevTimePasses] -> TestName -> TestName)
-> Show WhetherPrevTimePasses
forall a.
(Int -> a -> TestName -> TestName)
-> (a -> TestName) -> ([a] -> TestName -> TestName) -> Show a
$cshowsPrec :: Int -> WhetherPrevTimePasses -> TestName -> TestName
showsPrec :: Int -> WhetherPrevTimePasses -> TestName -> TestName
$cshow :: WhetherPrevTimePasses -> TestName
show :: WhetherPrevTimePasses -> TestName
$cshowList :: [WhetherPrevTimePasses] -> TestName -> TestName
showList :: [WhetherPrevTimePasses] -> TestName -> TestName
Show)
  deriving anyclass [WhetherPrevTimePasses] -> Expr
WhetherPrevTimePasses -> Expr
(WhetherPrevTimePasses -> Expr)
-> ([WhetherPrevTimePasses] -> Expr)
-> ToExpr WhetherPrevTimePasses
forall a. (a -> Expr) -> ([a] -> Expr) -> ToExpr a
$ctoExpr :: WhetherPrevTimePasses -> Expr
toExpr :: WhetherPrevTimePasses -> Expr
$clistToExpr :: [WhetherPrevTimePasses] -> Expr
listToExpr :: [WhetherPrevTimePasses] -> Expr
TD.ToExpr

data ModelState
  = ModelPreSyncing
  | ModelSyncing
  | -- | when the model most recently transitioned to 'GSM.CaughtUp'.
    ModelCaughtUp !SI.Time
  deriving stock (ModelState -> ModelState -> Bool
(ModelState -> ModelState -> Bool)
-> (ModelState -> ModelState -> Bool) -> Eq ModelState
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ModelState -> ModelState -> Bool
== :: ModelState -> ModelState -> Bool
$c/= :: ModelState -> ModelState -> Bool
/= :: ModelState -> ModelState -> Bool
Eq, Eq ModelState
Eq ModelState =>
(ModelState -> ModelState -> Ordering)
-> (ModelState -> ModelState -> Bool)
-> (ModelState -> ModelState -> Bool)
-> (ModelState -> ModelState -> Bool)
-> (ModelState -> ModelState -> Bool)
-> (ModelState -> ModelState -> ModelState)
-> (ModelState -> ModelState -> ModelState)
-> Ord ModelState
ModelState -> ModelState -> Bool
ModelState -> ModelState -> Ordering
ModelState -> ModelState -> ModelState
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: ModelState -> ModelState -> Ordering
compare :: ModelState -> ModelState -> Ordering
$c< :: ModelState -> ModelState -> Bool
< :: ModelState -> ModelState -> Bool
$c<= :: ModelState -> ModelState -> Bool
<= :: ModelState -> ModelState -> Bool
$c> :: ModelState -> ModelState -> Bool
> :: ModelState -> ModelState -> Bool
$c>= :: ModelState -> ModelState -> Bool
>= :: ModelState -> ModelState -> Bool
$cmax :: ModelState -> ModelState -> ModelState
max :: ModelState -> ModelState -> ModelState
$cmin :: ModelState -> ModelState -> ModelState
min :: ModelState -> ModelState -> ModelState
Ord, (forall x. ModelState -> Rep ModelState x)
-> (forall x. Rep ModelState x -> ModelState) -> Generic ModelState
forall x. Rep ModelState x -> ModelState
forall x. ModelState -> Rep ModelState x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. ModelState -> Rep ModelState x
from :: forall x. ModelState -> Rep ModelState x
$cto :: forall x. Rep ModelState x -> ModelState
to :: forall x. Rep ModelState x -> ModelState
Generic, Int -> ModelState -> TestName -> TestName
[ModelState] -> TestName -> TestName
ModelState -> TestName
(Int -> ModelState -> TestName -> TestName)
-> (ModelState -> TestName)
-> ([ModelState] -> TestName -> TestName)
-> Show ModelState
forall a.
(Int -> a -> TestName -> TestName)
-> (a -> TestName) -> ([a] -> TestName -> TestName) -> Show a
$cshowsPrec :: Int -> ModelState -> TestName -> TestName
showsPrec :: Int -> ModelState -> TestName -> TestName
$cshow :: ModelState -> TestName
show :: ModelState -> TestName
$cshowList :: [ModelState] -> TestName -> TestName
showList :: [ModelState] -> TestName -> TestName
Show)
  deriving anyclass [ModelState] -> Expr
ModelState -> Expr
(ModelState -> Expr) -> ([ModelState] -> Expr) -> ToExpr ModelState
forall a. (a -> Expr) -> ([a] -> Expr) -> ToExpr a
$ctoExpr :: ModelState -> Expr
toExpr :: ModelState -> Expr
$clistToExpr :: [ModelState] -> Expr
listToExpr :: [ModelState] -> Expr
TD.ToExpr

-- | Interesting events to record /within the model/
--
-- TODO some less superficial ones (eg even just combinations of these)
data Notable
  = -- | there was a "big" 'TimesPasses' command
    BigDurN
  | -- | the node transitioned from Syncing to CaughtUp
    CaughtUpN
  | -- | the node transitioned from CaughtUp to PreSyncing
    FellBehindN
  | -- | the node transition from Syncing to PreSyncing
    SyncingToPreSyncingN
  | -- | the node transition from PreSyncing to Syncing
    PreSyncingToSyncingN
  | -- | the node transitioned from CaughtUp to PreSyncing to Syncing and back
    -- to CaughtUp "instantly"
    FlickerN
  | -- | the anti-thrashing would have allowed 'FellBehindN', but the selection
    -- wasn't old enough
    NotThrashingN
  | -- | the selection was old enough for 'FellBehindN', but the anti-thrashing
    -- prevented it
    TooOldN
  deriving (Notable -> Notable -> Bool
(Notable -> Notable -> Bool)
-> (Notable -> Notable -> Bool) -> Eq Notable
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Notable -> Notable -> Bool
== :: Notable -> Notable -> Bool
$c/= :: Notable -> Notable -> Bool
/= :: Notable -> Notable -> Bool
Eq, Eq Notable
Eq Notable =>
(Notable -> Notable -> Ordering)
-> (Notable -> Notable -> Bool)
-> (Notable -> Notable -> Bool)
-> (Notable -> Notable -> Bool)
-> (Notable -> Notable -> Bool)
-> (Notable -> Notable -> Notable)
-> (Notable -> Notable -> Notable)
-> Ord Notable
Notable -> Notable -> Bool
Notable -> Notable -> Ordering
Notable -> Notable -> Notable
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Notable -> Notable -> Ordering
compare :: Notable -> Notable -> Ordering
$c< :: Notable -> Notable -> Bool
< :: Notable -> Notable -> Bool
$c<= :: Notable -> Notable -> Bool
<= :: Notable -> Notable -> Bool
$c> :: Notable -> Notable -> Bool
> :: Notable -> Notable -> Bool
$c>= :: Notable -> Notable -> Bool
>= :: Notable -> Notable -> Bool
$cmax :: Notable -> Notable -> Notable
max :: Notable -> Notable -> Notable
$cmin :: Notable -> Notable -> Notable
min :: Notable -> Notable -> Notable
Ord, Int -> Notable -> TestName -> TestName
[Notable] -> TestName -> TestName
Notable -> TestName
(Int -> Notable -> TestName -> TestName)
-> (Notable -> TestName)
-> ([Notable] -> TestName -> TestName)
-> Show Notable
forall a.
(Int -> a -> TestName -> TestName)
-> (a -> TestName) -> ([a] -> TestName -> TestName) -> Show a
$cshowsPrec :: Int -> Notable -> TestName -> TestName
showsPrec :: Int -> Notable -> TestName -> TestName
$cshow :: Notable -> TestName
show :: Notable -> TestName
$cshowList :: [Notable] -> TestName -> TestName
showList :: [Notable] -> TestName -> TestName
Show)

instance TD.ToExpr Notable where toExpr :: Notable -> Expr
toExpr = Notable -> Expr
forall a. Show a => a -> Expr
TD.defaultExprViaShow

---

newtype Idling = Idling Bool
  deriving (Idling -> Idling -> Bool
(Idling -> Idling -> Bool)
-> (Idling -> Idling -> Bool) -> Eq Idling
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Idling -> Idling -> Bool
== :: Idling -> Idling -> Bool
$c/= :: Idling -> Idling -> Bool
/= :: Idling -> Idling -> Bool
Eq, Eq Idling
Eq Idling =>
(Idling -> Idling -> Ordering)
-> (Idling -> Idling -> Bool)
-> (Idling -> Idling -> Bool)
-> (Idling -> Idling -> Bool)
-> (Idling -> Idling -> Bool)
-> (Idling -> Idling -> Idling)
-> (Idling -> Idling -> Idling)
-> Ord Idling
Idling -> Idling -> Bool
Idling -> Idling -> Ordering
Idling -> Idling -> Idling
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Idling -> Idling -> Ordering
compare :: Idling -> Idling -> Ordering
$c< :: Idling -> Idling -> Bool
< :: Idling -> Idling -> Bool
$c<= :: Idling -> Idling -> Bool
<= :: Idling -> Idling -> Bool
$c> :: Idling -> Idling -> Bool
> :: Idling -> Idling -> Bool
$c>= :: Idling -> Idling -> Bool
>= :: Idling -> Idling -> Bool
$cmax :: Idling -> Idling -> Idling
max :: Idling -> Idling -> Idling
$cmin :: Idling -> Idling -> Idling
min :: Idling -> Idling -> Idling
Ord, Int -> Idling -> TestName -> TestName
[Idling] -> TestName -> TestName
Idling -> TestName
(Int -> Idling -> TestName -> TestName)
-> (Idling -> TestName)
-> ([Idling] -> TestName -> TestName)
-> Show Idling
forall a.
(Int -> a -> TestName -> TestName)
-> (a -> TestName) -> ([a] -> TestName -> TestName) -> Show a
$cshowsPrec :: Int -> Idling -> TestName -> TestName
showsPrec :: Int -> Idling -> TestName -> TestName
$cshow :: Idling -> TestName
show :: Idling -> TestName
$cshowList :: [Idling] -> TestName -> TestName
showList :: [Idling] -> TestName -> TestName
Show)

data PeerState = PeerState {PeerState -> Candidate
psCandidate :: !Candidate, PeerState -> Idling
psIdling :: !Idling}
  deriving (PeerState -> PeerState -> Bool
(PeerState -> PeerState -> Bool)
-> (PeerState -> PeerState -> Bool) -> Eq PeerState
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: PeerState -> PeerState -> Bool
== :: PeerState -> PeerState -> Bool
$c/= :: PeerState -> PeerState -> Bool
/= :: PeerState -> PeerState -> Bool
Eq, Eq PeerState
Eq PeerState =>
(PeerState -> PeerState -> Ordering)
-> (PeerState -> PeerState -> Bool)
-> (PeerState -> PeerState -> Bool)
-> (PeerState -> PeerState -> Bool)
-> (PeerState -> PeerState -> Bool)
-> (PeerState -> PeerState -> PeerState)
-> (PeerState -> PeerState -> PeerState)
-> Ord PeerState
PeerState -> PeerState -> Bool
PeerState -> PeerState -> Ordering
PeerState -> PeerState -> PeerState
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: PeerState -> PeerState -> Ordering
compare :: PeerState -> PeerState -> Ordering
$c< :: PeerState -> PeerState -> Bool
< :: PeerState -> PeerState -> Bool
$c<= :: PeerState -> PeerState -> Bool
<= :: PeerState -> PeerState -> Bool
$c> :: PeerState -> PeerState -> Bool
> :: PeerState -> PeerState -> Bool
$c>= :: PeerState -> PeerState -> Bool
>= :: PeerState -> PeerState -> Bool
$cmax :: PeerState -> PeerState -> PeerState
max :: PeerState -> PeerState -> PeerState
$cmin :: PeerState -> PeerState -> PeerState
min :: PeerState -> PeerState -> PeerState
Ord, Int -> PeerState -> TestName -> TestName
[PeerState] -> TestName -> TestName
PeerState -> TestName
(Int -> PeerState -> TestName -> TestName)
-> (PeerState -> TestName)
-> ([PeerState] -> TestName -> TestName)
-> Show PeerState
forall a.
(Int -> a -> TestName -> TestName)
-> (a -> TestName) -> ([a] -> TestName -> TestName) -> Show a
$cshowsPrec :: Int -> PeerState -> TestName -> TestName
showsPrec :: Int -> PeerState -> TestName -> TestName
$cshow :: PeerState -> TestName
show :: PeerState -> TestName
$cshowList :: [PeerState] -> TestName -> TestName
showList :: [PeerState] -> TestName -> TestName
Show)

isIdling :: PeerState -> Bool
isIdling :: PeerState -> Bool
isIdling (PeerState{psIdling :: PeerState -> Idling
psIdling = Idling Bool
i}) = Bool
i

-- | Ensure the GSM thread's transactions quiesce
--
-- I'm unsure how many 'yield's are actually necessary, but ten is both small
-- and also seems likely to suffice.
--
-- Despite the crudeness, this seems much more compositional than invasive
-- explicit synchronization.
yieldSeveralTimes :: MonadFork m => m ()
yieldSeveralTimes :: forall (m :: * -> *). MonadFork m => m ()
yieldSeveralTimes = Int -> m () -> m ()
forall (m :: * -> *) a. Applicative m => Int -> m a -> m ()
Monad.replicateM_ Int
10 m ()
forall (m :: * -> *). MonadFork m => m ()
yield

{-

Note [Why yield after the command]

For this 'prop_sequential1' repro

@
   YoungEnough

   Command (NewCandidate Amara (B 1)) Unit []
   Command (StartIdling Amara) Unit []
   Command (TimePasses 61) Unit []
   Command (ExtendSelection (S (-4))) Unit []
   Command ReadMarker (ReadThisMarker Absent) []

   (Command ReadGsmState _ [])   -- this last command is baked into the property
@

If we yield after the command, then both GSM flicker writes happen during the
'ExtendSelection'.

If we yield before the command, then both GSM flicker writes happen during the
'ReadMarker'.

If we don't yield, one write happens during the ReadMarker and the other
happens /between/ 'ReadMarker' and 'ReadGsmState'.

It seems most intuitive for the updates to happen "as part of" the
'ExtendSelection', so I'm favoring yielding after.

And since we're yielding after the command, we should also yield before the
first command, for consistency.

-}

----- orphans

deriving instance Read LedgerStateJudgement

deriving anyclass instance TD.ToExpr LedgerStateJudgement

instance QC.Arbitrary LedgerStateJudgement where
  arbitrary :: Gen LedgerStateJudgement
arbitrary = [LedgerStateJudgement] -> Gen LedgerStateJudgement
forall a. HasCallStack => [a] -> Gen a
elements [LedgerStateJudgement
TooOld, LedgerStateJudgement
YoungEnough]
  shrink :: LedgerStateJudgement -> [LedgerStateJudgement]
shrink = \case
    LedgerStateJudgement
TooOld -> [LedgerStateJudgement
YoungEnough]
    LedgerStateJudgement
YoungEnough -> []

instance QC.Arbitrary MarkerState where
  arbitrary :: Gen MarkerState
arbitrary = [MarkerState] -> Gen MarkerState
forall a. HasCallStack => [a] -> Gen a
elements [MarkerState
Absent, MarkerState
Present]
  shrink :: MarkerState -> [MarkerState]
shrink = \case
    MarkerState
Absent -> [MarkerState
Present]
    MarkerState
Present -> []

-----

toGsmState :: ModelState -> GSM.GsmState
toGsmState :: ModelState -> GsmState
toGsmState = \case
  ModelState
ModelPreSyncing -> GsmState
GSM.PreSyncing
  ModelState
ModelSyncing -> GsmState
GSM.Syncing
  ModelCaughtUp{} -> GsmState
GSM.CaughtUp

toMarker :: GSM.GsmState -> MarkerState
toMarker :: GsmState -> MarkerState
toMarker = \case
  GsmState
GSM.PreSyncing -> MarkerState
Absent
  GsmState
GSM.Syncing -> MarkerState
Absent
  GsmState
GSM.CaughtUp -> MarkerState
Present

-----

onset :: Selection -> SI.Time
onset :: Selection -> Time
onset (Selection B
_b (S Int
s)) = DiffTime -> Time
SI.Time (DiffTime -> Time) -> DiffTime -> Time
forall a b. (a -> b) -> a -> b
$ Int -> DiffTime
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
s

ageLimit :: Num a => a
ageLimit :: forall a. Num a => a
ageLimit = a
10 -- seconds

thrashLimit :: Num a => a
thrashLimit :: forall a. Num a => a
thrashLimit = a
8 -- seconds

durationUntilTooOld :: Selection -> IOSim.IOSim s GSM.DurationFromNow
durationUntilTooOld :: forall s. Selection -> IOSim s DurationFromNow
durationUntilTooOld Selection
sel = do
  let expiryAge :: Time
expiryAge = DiffTime
forall a. Num a => a
ageLimit DiffTime -> Time -> Time
`SI.addTime` Selection -> Time
onset Selection
sel
  now <- IOSim s Time
forall (m :: * -> *). MonadMonotonicTime m => m Time
SI.getMonotonicTime
  pure $ case compare expiryAge now of
    Ordering
LT -> DurationFromNow
GSM.Already
    Ordering
GT -> NominalDiffTime -> DurationFromNow
GSM.After (NominalDiffTime -> DurationFromNow)
-> NominalDiffTime -> DurationFromNow
forall a b. (a -> b) -> a -> b
$ DiffTime -> NominalDiffTime
forall a b. (Real a, Fractional b) => a -> b
realToFrac (DiffTime -> NominalDiffTime) -> DiffTime -> NominalDiffTime
forall a b. (a -> b) -> a -> b
$ Time
expiryAge Time -> Time -> DiffTime
`SI.diffTime` Time
now
    -- 'boringDur' cannot prevent this case. In particular, this case
    -- necessarily arises in the GSM itself during a 'TimePasses' that
    -- incurs a so-called /flicker/ event, in which the anti-thrashing
    -- timer expires and yet the node state at that moment still
    -- _immediately_ indicates that it's CaughtUp. For the specific case of
    -- this test suite, the answer here must be 'GSM.Already'.
    Ordering
EQ -> DurationFromNow
GSM.Already

candidateOverSelection ::
  Selection ->
  Candidate ->
  GSM.CandidateVersusSelection
candidateOverSelection :: Selection -> Candidate -> CandidateVersusSelection
candidateOverSelection (Selection B
b S
_s) (Candidate B
b') =
  -- TODO this ignores CandidateDoesNotIntersect, which seems harmless, but
  -- I'm not quite sure
  Bool -> CandidateVersusSelection
GSM.WhetherCandidateIsBetter (B
b B -> B -> Bool
forall a. Ord a => a -> a -> Bool
< B
b')

-- | Checks that a 'TimePasses' command does not end exactly when a timeout
-- could fire and that a 'ExtendSelection' does not incur a timeout that would
-- fire immediately
--
-- This insulates the test from race conditions that are innocuous in the real
-- world.
boringDurImpl :: SI.Time -> Selection -> ModelState -> Int -> Bool
boringDurImpl :: Time -> Selection -> ModelState -> Int -> Bool
boringDurImpl Time
clk Selection
sel ModelState
st Int
dur =
  Bool
boringSelection Bool -> Bool -> Bool
&& Bool
boringState
 where
  -- the first time the node would transition to PreSyncing
  expiry :: Time -> Time
expiry Time
timestamp = Time
expiryAge Time -> Time -> Time
forall a. Ord a => a -> a -> a
`max` Time -> Time
expiryThrashing Time
timestamp
  expiryAge :: Time
expiryAge = DiffTime -> Time -> Time
SI.addTime DiffTime
forall a. Num a => a
ageLimit (Selection -> Time
onset Selection
sel)
  expiryThrashing :: Time -> Time
expiryThrashing Time
timestamp = DiffTime -> Time -> Time
SI.addTime DiffTime
forall a. Num a => a
thrashLimit Time
timestamp

  clk' :: Time
clk' = DiffTime -> Time -> Time
SI.addTime (DiffTime
0.1 DiffTime -> DiffTime -> DiffTime
forall a. Num a => a -> a -> a
* Int -> DiffTime
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
dur) Time
clk

  boringSelection :: Bool
boringSelection = Time
clk' Time -> Time -> Bool
forall a. Eq a => a -> a -> Bool
/= Time
expiryAge

  boringState :: Bool
boringState = case ModelState
st of
    ModelState
ModelPreSyncing -> Bool
True
    ModelState
ModelSyncing -> Bool
True
    ModelCaughtUp Time
timestamp ->
      let gap :: DiffTime
gap = Time
clk' Time -> Time -> DiffTime
`SI.diffTime` Time -> Time
expiry Time
timestamp
          n :: Integer
n =
            Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
mod
              (DiffTime -> Integer
diffTimeToPicoseconds DiffTime
gap)
              (Integer -> Integer
forall {a}. Num a => a -> a
secondsToPicoseconds Integer
forall a. Num a => a
thrashLimit)
       in DiffTime
gap DiffTime -> DiffTime -> Bool
forall a. Ord a => a -> a -> Bool
< DiffTime
0 Bool -> Bool -> Bool
|| Integer
0 Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
n

  secondsToPicoseconds :: a -> a
secondsToPicoseconds a
x = a
x a -> a -> a
forall a. Num a => a -> a -> a
* a
10 a -> Int -> a
forall a b. (Num a, Integral b) => a -> b -> a
^ (Int
12 :: Int)