{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE StandaloneKindSignatures #-}

{-# OPTIONS_GHC -Wno-orphans #-}

-- | The definition of the GSM QSM model and its auxiliaries

module Test.Consensus.GSM.Model (module Test.Consensus.GSM.Model) where

import qualified Control.Monad.Class.MonadTime.SI as SI
import           Data.Kind (Type)
import           Data.List ((\\))
import qualified Data.Map.Strict as Map
import qualified Data.Set as Set
import           Data.Time (diffTimeToPicoseconds)
import qualified Data.TreeDiff as TD
import           GHC.Generics (Generic, Generic1)
import qualified Ouroboros.Consensus.Node.GSM as GSM
import           Ouroboros.Network.PeerSelection.LedgerPeers.Type
                     (LedgerStateJudgement (..))
import qualified Test.QuickCheck as QC
import           Test.QuickCheck (choose, elements, shrink)
import qualified Test.StateMachine as QSM
import           Test.StateMachine (Concrete, Symbolic)
import qualified Test.StateMachine.Types.Rank2 as QSM
import           Test.Util.Orphans.ToExpr ()

----- the QSM model

-- These definitions are in the exact same order as the QSM tutorial at
-- <https://github.com/stevana/quickcheck-state-machine/blob/3748220bffacb61847e35e3808403f3e7187a7c6/README.md>,
-- except @semantics@ and the property itself are defined in
-- "Test.Consensus.GSM".

-- | TODO restarts (or maybe just killing the GSM thread)
type Command :: (Type -> Type) -> Type
data Command r =
    Disconnect UpstreamPeer
    -- ^ INVARIANT must be an existing peer
    --
    -- Mocks the necessary ChainSync client behavior.
  |
    ExtendSelection S
    -- ^ INVARIANT 'selectionIsBehind'
    --
    -- NOTE Harmless to assume it only advances by @'B' 1@ at a time.
  |
    ModifyCandidate UpstreamPeer B
    -- ^ INVARIANT existing peer
    --
    -- Mocks the necessary ChainSync client behavior.
  |
    NewCandidate UpstreamPeer B
    -- ^ INVARIANT new peer
    --
    -- Mocks the necessary ChainSync client behavior.
  |
    ReadGsmState
  |
    ReadMarker
  |
    StartIdling UpstreamPeer
    -- ^ INVARIANT existing peer, not idling
  |
    TimePasses Int
    -- ^ 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.
    --

    -- DRAFT NOTE An earlier design attempted to prevent TimePasses from ever landing
    -- exactly on an interesting moment, ie when some timeout expires. Notably:
    -- when a slot becomes too old or when the anti-thrashing limit expires.
    -- This is feasible and its complexity is tolerable for the generators.
    -- However, shrinking------wait, doesn't precondition guard against it?
  deriving stock    ((forall (a :: * -> *). Command a -> Rep1 Command a)
-> (forall (a :: * -> *). Rep1 Command a -> Command a)
-> Generic1 Command
forall k (f :: k -> *).
(forall (a :: k). f a -> Rep1 f a)
-> (forall (a :: k). Rep1 f a -> f a) -> Generic1 f
forall (a :: * -> *). Rep1 Command a -> Command a
forall (a :: * -> *). Command a -> Rep1 Command a
$cfrom1 :: forall (a :: * -> *). Command a -> Rep1 Command a
from1 :: forall (a :: * -> *). Command a -> Rep1 Command a
$cto1 :: forall (a :: * -> *). Rep1 Command a -> Command a
to1 :: forall (a :: * -> *). Rep1 Command a -> Command a
Generic1, ReadPrec [Command r]
ReadPrec (Command r)
Int -> ReadS (Command r)
ReadS [Command r]
(Int -> ReadS (Command r))
-> ReadS [Command r]
-> ReadPrec (Command r)
-> ReadPrec [Command r]
-> Read (Command r)
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
forall (r :: * -> *). ReadPrec [Command r]
forall (r :: * -> *). ReadPrec (Command r)
forall (r :: * -> *). Int -> ReadS (Command r)
forall (r :: * -> *). ReadS [Command r]
$creadsPrec :: forall (r :: * -> *). Int -> ReadS (Command r)
readsPrec :: Int -> ReadS (Command r)
$creadList :: forall (r :: * -> *). ReadS [Command r]
readList :: ReadS [Command r]
$creadPrec :: forall (r :: * -> *). ReadPrec (Command r)
readPrec :: ReadPrec (Command r)
$creadListPrec :: forall (r :: * -> *). ReadPrec [Command r]
readListPrec :: ReadPrec [Command r]
Read, Int -> Command r -> ShowS
[Command r] -> ShowS
Command r -> String
(Int -> Command r -> ShowS)
-> (Command r -> String)
-> ([Command r] -> ShowS)
-> Show (Command r)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (r :: * -> *). Int -> Command r -> ShowS
forall (r :: * -> *). [Command r] -> ShowS
forall (r :: * -> *). Command r -> String
$cshowsPrec :: forall (r :: * -> *). Int -> Command r -> ShowS
showsPrec :: Int -> Command r -> ShowS
$cshow :: forall (r :: * -> *). Command r -> String
show :: Command r -> String
$cshowList :: forall (r :: * -> *). [Command r] -> ShowS
showList :: [Command r] -> ShowS
Show)
  deriving anyclass ((forall (r :: * -> *). Command r -> String)
-> (forall (r :: * -> *). Proxy (Command r) -> [String])
-> CommandNames Command
forall k (cmd :: k -> *).
(forall (r :: k). cmd r -> String)
-> (forall (r :: k). Proxy (cmd r) -> [String]) -> CommandNames cmd
forall (r :: * -> *). Proxy (Command r) -> [String]
forall (r :: * -> *). Command r -> String
$ccmdName :: forall (r :: * -> *). Command r -> String
cmdName :: forall (r :: * -> *). Command r -> String
$ccmdNames :: forall (r :: * -> *). Proxy (Command r) -> [String]
cmdNames :: forall (r :: * -> *). Proxy (Command r) -> [String]
QSM.CommandNames, (forall m (p :: * -> *).
 Monoid m =>
 (forall x. p x -> m) -> Command p -> m)
-> Foldable Command
forall m (p :: * -> *).
Monoid m =>
(forall x. p x -> m) -> Command p -> m
forall k (f :: (k -> *) -> *).
(forall m (p :: k -> *).
 Monoid m =>
 (forall (x :: k). p x -> m) -> f p -> m)
-> Foldable f
$cfoldMap :: forall m (p :: * -> *).
Monoid m =>
(forall x. p x -> m) -> Command p -> m
foldMap :: forall m (p :: * -> *).
Monoid m =>
(forall x. p x -> m) -> Command p -> m
QSM.Foldable, (forall (p :: * -> *) (q :: * -> *).
 (forall x. p x -> q x) -> Command p -> Command q)
-> Functor Command
forall k (f :: (k -> *) -> *).
(forall (p :: k -> *) (q :: k -> *).
 (forall (x :: k). p x -> q x) -> f p -> f q)
-> Functor f
forall (p :: * -> *) (q :: * -> *).
(forall x. p x -> q x) -> Command p -> Command q
$cfmap :: forall (p :: * -> *) (q :: * -> *).
(forall x. p x -> q x) -> Command p -> Command q
fmap :: forall (p :: * -> *) (q :: * -> *).
(forall x. p x -> q x) -> Command p -> Command q
QSM.Functor, Foldable Command
Functor Command
(Functor Command, Foldable Command) =>
(forall (f :: * -> *) (p :: * -> *) (q :: * -> *).
 Applicative f =>
 (forall a. p a -> f (q a)) -> Command p -> f (Command q))
-> Traversable Command
forall k (t :: (k -> *) -> *).
(Functor t, Foldable t) =>
(forall (f :: * -> *) (p :: k -> *) (q :: k -> *).
 Applicative f =>
 (forall (a :: k). p a -> f (q a)) -> t p -> f (t q))
-> Traversable t
forall (f :: * -> *) (p :: * -> *) (q :: * -> *).
Applicative f =>
(forall a. p a -> f (q a)) -> Command p -> f (Command q)
$ctraverse :: forall (f :: * -> *) (p :: * -> *) (q :: * -> *).
Applicative f =>
(forall a. p a -> f (q a)) -> Command p -> f (Command q)
traverse :: forall (f :: * -> *) (p :: * -> *) (q :: * -> *).
Applicative f =>
(forall a. p a -> f (q a)) -> Command p -> f (Command q)
QSM.Traversable)

type Response :: (Type -> Type) -> Type
data Response r =
    ReadThisGsmState GSM.GsmState
  |
    ReadThisMarker MarkerState
  |
    Unit
  deriving stock    ((forall (a :: * -> *). Response a -> Rep1 Response a)
-> (forall (a :: * -> *). Rep1 Response a -> Response a)
-> Generic1 Response
forall k (f :: k -> *).
(forall (a :: k). f a -> Rep1 f a)
-> (forall (a :: k). Rep1 f a -> f a) -> Generic1 f
forall (a :: * -> *). Rep1 Response a -> Response a
forall (a :: * -> *). Response a -> Rep1 Response a
$cfrom1 :: forall (a :: * -> *). Response a -> Rep1 Response a
from1 :: forall (a :: * -> *). Response a -> Rep1 Response a
$cto1 :: forall (a :: * -> *). Rep1 Response a -> Response a
to1 :: forall (a :: * -> *). Rep1 Response a -> Response a
Generic1, ReadPrec [Response r]
ReadPrec (Response r)
Int -> ReadS (Response r)
ReadS [Response r]
(Int -> ReadS (Response r))
-> ReadS [Response r]
-> ReadPrec (Response r)
-> ReadPrec [Response r]
-> Read (Response r)
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
forall (r :: * -> *). ReadPrec [Response r]
forall (r :: * -> *). ReadPrec (Response r)
forall (r :: * -> *). Int -> ReadS (Response r)
forall (r :: * -> *). ReadS [Response r]
$creadsPrec :: forall (r :: * -> *). Int -> ReadS (Response r)
readsPrec :: Int -> ReadS (Response r)
$creadList :: forall (r :: * -> *). ReadS [Response r]
readList :: ReadS [Response r]
$creadPrec :: forall (r :: * -> *). ReadPrec (Response r)
readPrec :: ReadPrec (Response r)
$creadListPrec :: forall (r :: * -> *). ReadPrec [Response r]
readListPrec :: ReadPrec [Response r]
Read, Int -> Response r -> ShowS
[Response r] -> ShowS
Response r -> String
(Int -> Response r -> ShowS)
-> (Response r -> String)
-> ([Response r] -> ShowS)
-> Show (Response r)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (r :: * -> *). Int -> Response r -> ShowS
forall (r :: * -> *). [Response r] -> ShowS
forall (r :: * -> *). Response r -> String
$cshowsPrec :: forall (r :: * -> *). Int -> Response r -> ShowS
showsPrec :: Int -> Response r -> ShowS
$cshow :: forall (r :: * -> *). Response r -> String
show :: Response r -> String
$cshowList :: forall (r :: * -> *). [Response r] -> ShowS
showList :: [Response r] -> ShowS
Show)
  deriving anyclass ((forall m (p :: * -> *).
 Monoid m =>
 (forall x. p x -> m) -> Response p -> m)
-> Foldable Response
forall m (p :: * -> *).
Monoid m =>
(forall x. p x -> m) -> Response p -> m
forall k (f :: (k -> *) -> *).
(forall m (p :: k -> *).
 Monoid m =>
 (forall (x :: k). p x -> m) -> f p -> m)
-> Foldable f
$cfoldMap :: forall m (p :: * -> *).
Monoid m =>
(forall x. p x -> m) -> Response p -> m
foldMap :: forall m (p :: * -> *).
Monoid m =>
(forall x. p x -> m) -> Response p -> m
QSM.Foldable, (forall (p :: * -> *) (q :: * -> *).
 (forall x. p x -> q x) -> Response p -> Response q)
-> Functor Response
forall k (f :: (k -> *) -> *).
(forall (p :: k -> *) (q :: k -> *).
 (forall (x :: k). p x -> q x) -> f p -> f q)
-> Functor f
forall (p :: * -> *) (q :: * -> *).
(forall x. p x -> q x) -> Response p -> Response q
$cfmap :: forall (p :: * -> *) (q :: * -> *).
(forall x. p x -> q x) -> Response p -> Response q
fmap :: forall (p :: * -> *) (q :: * -> *).
(forall x. p x -> q x) -> Response p -> Response q
QSM.Functor, Foldable Response
Functor Response
(Functor Response, Foldable Response) =>
(forall (f :: * -> *) (p :: * -> *) (q :: * -> *).
 Applicative f =>
 (forall a. p a -> f (q a)) -> Response p -> f (Response q))
-> Traversable Response
forall k (t :: (k -> *) -> *).
(Functor t, Foldable t) =>
(forall (f :: * -> *) (p :: k -> *) (q :: k -> *).
 Applicative f =>
 (forall (a :: k). p a -> f (q a)) -> t p -> f (t q))
-> Traversable t
forall (f :: * -> *) (p :: * -> *) (q :: * -> *).
Applicative f =>
(forall a. p a -> f (q a)) -> Response p -> f (Response q)
$ctraverse :: forall (f :: * -> *) (p :: * -> *) (q :: * -> *).
Applicative f =>
(forall a. p a -> f (q a)) -> Response p -> f (Response q)
traverse :: forall (f :: * -> *) (p :: * -> *) (q :: * -> *).
Applicative f =>
(forall a. p a -> f (q a)) -> Response p -> f (Response q)
QSM.Traversable)

data Context = Context {
    Context -> LedgerStateJudgement
cInitialJudgement :: LedgerStateJudgement
  ,
    Context -> Set UpstreamPeer -> Bool
cIsHaaSatisfied   :: Set.Set UpstreamPeer -> Bool
  }

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

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

initModel :: Context -> Model r
initModel :: forall (r :: * -> *). Context -> Model r
initModel Context
ctx = 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 = B -> S -> Selection
Selection B
0 S
s
  ,
    mState :: ModelState
mState = case LedgerStateJudgement
j of
        LedgerStateJudgement
TooOld
          | Set UpstreamPeer -> Bool
isHaaSatisfied 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
    Context {
        cInitialJudgement :: Context -> LedgerStateJudgement
cInitialJudgement = LedgerStateJudgement
j
      ,
        cIsHaaSatisfied :: Context -> Set UpstreamPeer -> Bool
cIsHaaSatisfied = Set UpstreamPeer -> Bool
isHaaSatisfied
      } = Context
ctx

    idlers :: Set a
idlers = Set a
forall {a}. Set a
Set.empty

    s :: S
s = Int -> S
S (Int -> S) -> Int -> S
forall a b. (a -> b) -> a -> b
$ case LedgerStateJudgement
j of
        LedgerStateJudgement
TooOld      -> (-Int
11)
        LedgerStateJudgement
YoungEnough -> Int
0

-- The extra expressivity of 'QSM.Logic' beyond 'Bool' will not be useful in
-- this test module as-is, since we only run commands (via 'runCommands'') that
-- the library generated, which ensures the preconditions. On the other hand,
-- if you're debugging a failure by manually altering commands, then these
-- annotations may be helpful.
precondition :: Context -> Model Symbolic -> Command Symbolic -> QSM.Logic
precondition :: Context -> Model Symbolic -> Command Symbolic -> Logic
precondition Context
ctx Model Symbolic
model = (Command Symbolic -> Logic) -> Command Symbolic -> Logic
forall {a}. Show a => (a -> Logic) -> a -> Logic
pre ((Command Symbolic -> Logic) -> Command Symbolic -> Logic)
-> (Command Symbolic -> Logic) -> Command Symbolic -> Logic
forall a b. (a -> b) -> a -> b
$ \case
    cmd :: Command Symbolic
cmd@ExtendSelection{} ->
        let model' :: Model Symbolic
model' = Context
-> Model Symbolic
-> Command Symbolic
-> Response Symbolic
-> Model Symbolic
forall (r :: * -> *).
Context -> Model r -> Command r -> Response r -> Model r
transition Context
ctx Model Symbolic
model Command Symbolic
cmd Response Symbolic
forall (r :: * -> *). Response r
Unit
        in
            String
"syncing node got ahead" String -> Bool -> Logic
`atom` Model Symbolic -> Bool
forall (r :: * -> *). Model r -> Bool
selectionIsBehind Model Symbolic
model
         Logic -> Logic -> Logic
QSM..&&
            String
"early selection" String -> Bool -> Logic
`atom` Model Symbolic -> Bool
forall (r :: * -> *). Model r -> Bool
selectionIsNotEarly Model Symbolic
model'
         Logic -> Logic -> Logic
QSM..&&
            Model Symbolic -> Int -> Logic
forall (r :: * -> *). Model r -> Int -> Logic
boringDur Model Symbolic
model' Int
0
    Disconnect UpstreamPeer
peer ->
        String
"double disconnect" String -> Bool -> Logic
`atom` (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 ->
        String
"modify after disconnect" String -> Bool -> Logic
`atom` (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 ->
        String
"double connect" String -> Bool -> Logic
`atom` (UpstreamPeer
peer UpstreamPeer -> Map UpstreamPeer Candidate -> Bool
forall k a. Ord k => k -> Map k a -> Bool
`Map.notMember` Map UpstreamPeer Candidate
cands)
    Command Symbolic
ReadGsmState ->
        Logic
QSM.Top
    Command Symbolic
ReadMarker ->
        Logic
QSM.Top
    StartIdling UpstreamPeer
peer ->
        String
"idle after disconnect" String -> Bool -> Logic
`atom` (UpstreamPeer
peer UpstreamPeer -> Map UpstreamPeer Candidate -> Bool
forall k a. Ord k => k -> Map k a -> Bool
`Map.member` Map UpstreamPeer Candidate
cands)
     Logic -> Logic -> Logic
QSM..&&
        String
"double idle" String -> Bool -> Logic
`atom` (UpstreamPeer
peer UpstreamPeer -> Set UpstreamPeer -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.notMember` Set UpstreamPeer
idlers)
    TimePasses Int
dur ->
        String
"non-positive duration" String -> Bool -> Logic
`atom` (Int
0 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
dur)
     Logic -> Logic -> Logic
QSM..&&
        Model Symbolic -> Int -> Logic
forall (r :: * -> *). Model r -> Int -> Logic
boringDur Model Symbolic
model Int
dur
  where
    Model {
        mCandidates :: forall (r :: * -> *). Model r -> Map UpstreamPeer Candidate
mCandidates = Map UpstreamPeer Candidate
cands
      ,
        mIdlers :: forall (r :: * -> *). Model r -> Set UpstreamPeer
mIdlers = Set UpstreamPeer
idlers
      } = Model Symbolic
model

    pre :: (a -> Logic) -> a -> Logic
pre a -> Logic
f a
cmd = a -> Logic
f a
cmd Logic -> String -> Logic
QSM..// a -> String
forall a. Show a => a -> String
show a
cmd

transition :: Context -> Model r -> Command r -> Response r -> Model r
transition :: forall (r :: * -> *).
Context -> Model r -> Command r -> Response r -> Model r
transition Context
ctx Model r
model Command r
cmd Response r
resp = Context -> Command r -> Model r -> Model r
forall (r :: * -> *). Context -> Command r -> Model r -> Model r
fixupModelState Context
ctx Command r
cmd (Model r -> Model r) -> Model r -> Model r
forall a b. (a -> b) -> a -> b
$ case (Command r
cmd, Response r
resp) of
    (Disconnect UpstreamPeer
peer, Response r
Unit) ->
        Model Any
forall {r :: * -> *}. Model r
model' {
            mCandidates = Map.delete peer cands
          ,
            mIdlers = Set.delete peer idlers
          }
    (ExtendSelection S
sdel, Response r
Unit) ->
        Model Any
forall {r :: * -> *}. Model r
model' { mSelection = Selection (b + 1) (s + sdel) }
    (ModifyCandidate UpstreamPeer
peer B
bdel, Response r
Unit) ->
        Model Any
forall {r :: * -> *}. Model r
model' {
            mCandidates = Map.insertWith plusC peer (Candidate bdel) cands
          ,
            mIdlers = Set.delete peer idlers
          }
    (NewCandidate UpstreamPeer
peer B
bdel, Response r
Unit) ->
        Model Any
forall {r :: * -> *}. Model r
model' { mCandidates = Map.insert peer (Candidate (b + bdel)) cands }
    (Command r
ReadGsmState, ReadThisGsmState{}) ->
        Model r
forall {r :: * -> *}. Model r
model'
    (Command r
ReadMarker, ReadThisMarker{}) ->
        Model r
forall {r :: * -> *}. Model r
model'
    (StartIdling UpstreamPeer
peer, Response r
Unit) ->
        Model Any
forall {r :: * -> *}. Model r
model' { mIdlers = Set.insert peer idlers }
    (TimePasses Int
dur, Response r
Unit) ->
        Notable -> Bool -> Model r -> Model r
forall (r :: * -> *). Notable -> Bool -> Model r -> Model r
addNotableWhen Notable
BigDurN (Int
dur Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
300)
      (Model r -> Model r) -> Model r -> Model r
forall a b. (a -> b) -> a -> b
$ Model r
model {
            mClock = SI.addTime (0.1 * fromIntegral dur) clk
          ,
            mPrev = WhetherPrevTimePasses True
          }
    (Command r, Response r)
o -> String -> Model r
forall a. HasCallStack => String -> a
error (String -> Model r) -> String -> Model r
forall a b. (a -> b) -> a -> b
$ String
"impossible response: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> (Command r, Response r) -> String
forall a. Show a => a -> String
show (Command r, Response r)
o
  where
    Model {
        mCandidates :: forall (r :: * -> *). Model r -> Map UpstreamPeer Candidate
mCandidates = Map UpstreamPeer Candidate
cands
      ,
        mClock :: forall (r :: * -> *). Model r -> Time
mClock = Time
clk
      ,
        mIdlers :: forall (r :: * -> *). Model r -> Set UpstreamPeer
mIdlers = Set UpstreamPeer
idlers
      ,
        mSelection :: forall (r :: * -> *). Model r -> Selection
mSelection = Selection B
b S
s
      } = Model r
model

    model' :: Model r
model' = Model r
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 :: Context -> Command r -> Model r -> Model r
fixupModelState :: forall (r :: * -> *). Context -> Command r -> Model r -> Model r
fixupModelState Context
ctx Command r
cmd Model r
model =
    case ModelState
st of
        ModelState
ModelPreSyncing
          | Bool
haaSatisfied ->
            Model r -> Model r
avoidTransientState
          (Model r -> Model r) -> Model r -> Model r
forall a b. (a -> b) -> a -> b
$ Notable -> Bool -> Model r -> Model r
forall (r :: * -> *). Notable -> Bool -> Model r -> Model r
addNotableWhen Notable
PreSyncingToSyncingN Bool
True
          (Model r -> Model r) -> Model r -> Model r
forall a b. (a -> b) -> a -> b
$ Model r
model { mState = ModelSyncing }
          | Bool
otherwise ->
            Model r
model
        ModelState
ModelSyncing
          | Bool -> Bool
not Bool
haaSatisfied ->
            Notable -> Bool -> Model r -> Model r
forall (r :: * -> *). Notable -> Bool -> Model r -> Model r
addNotableWhen Notable
SyncingToPreSyncingN Bool
True
          (Model r -> Model r) -> Model r -> Model r
forall a b. (a -> b) -> a -> b
$ Model r
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 r -> Model r
forall (r :: * -> *). Notable -> Bool -> Model r -> Model r
addNotableWhen Notable
CaughtUpN Bool
True
          (Model r -> Model r) -> Model r -> Model r
forall a b. (a -> b) -> a -> b
$ Model r
model { mState = ModelCaughtUp clk }
          | Bool
otherwise ->
            Model r
model
        ModelCaughtUp Time
timestamp
          | Time -> Bool
flicker Time
timestamp ->
            Notable -> Bool -> Model r -> Model r
forall (r :: * -> *). Notable -> Bool -> Model r -> Model r
addNotableWhen Notable
FlickerN    Bool
True
          (Model r -> Model r) -> Model r -> Model r
forall a b. (a -> b) -> a -> b
$ Model r
model { mState = ModelCaughtUp (flickerTimestamp timestamp) }
          | Time -> Bool
fellBehind Time
timestamp ->
            Model r -> Model r
avoidTransientState
          (Model r -> Model r) -> Model r -> Model r
forall a b. (a -> b) -> a -> b
$ Notable -> Bool -> Model r -> Model r
forall (r :: * -> *). Notable -> Bool -> Model r -> Model r
addNotableWhen Notable
FellBehindN Bool
True
          (Model r -> Model r) -> Model r -> Model r
forall a b. (a -> b) -> a -> b
$ Model r
model { mState = ModelPreSyncing }
          | Bool
otherwise ->
            -- NB in this branch, these notables are mutually exclusive
            Notable -> Bool -> Model r -> Model r
forall (r :: * -> *). Notable -> Bool -> Model r -> Model r
addNotableWhen Notable
TooOldN (Time
expiryAge Time -> Time -> Bool
forall a. Ord a => a -> a -> Bool
< Time
clk)
          (Model r -> Model r) -> Model r -> Model r
forall a b. (a -> b) -> a -> b
$ Notable -> Bool -> Model r -> Model r
forall (r :: * -> *). Notable -> Bool -> Model r -> Model r
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 r -> Model r) -> Model r -> Model r
forall a b. (a -> b) -> a -> b
$ Model r
model
  where
    Model {
        mCandidates :: forall (r :: * -> *). Model r -> Map UpstreamPeer Candidate
mCandidates = Map UpstreamPeer Candidate
cands
      ,
        mClock :: forall (r :: * -> *). Model r -> Time
mClock = Time
clk
      ,
        mIdlers :: forall (r :: * -> *). Model r -> Set UpstreamPeer
mIdlers = Set UpstreamPeer
idlers
      ,
        mSelection :: forall (r :: * -> *). Model r -> Selection
mSelection = Selection
sel
      ,
        mState :: forall (r :: * -> *). Model r -> ModelState
mState = ModelState
st
      } = Model r
model

    Context {
        cIsHaaSatisfied :: Context -> Set UpstreamPeer -> Bool
cIsHaaSatisfied = Set UpstreamPeer -> Bool
isHaaSatisfied
      } = Context
ctx

    haaSatisfied :: Bool
haaSatisfied         = Set UpstreamPeer -> Bool
isHaaSatisfied (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 Command r
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)   -- NB 'boringDur' prevents ==
          ([Time] -> [Time]) -> [Time] -> [Time]
forall a b. (a -> b) -> a -> b
$ (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)
        Command r
_ ->
            String -> Time
forall a. HasCallStack => String -> a
error
          (String -> Time) -> String -> Time
forall a b. (a -> b) -> a -> b
$     String
"impossible! flicker but neither "
             String -> ShowS
forall a. Semigroup a => a -> a -> a
<>
                String
"negative ExtendSelection nor TimePasses: "
             String -> ShowS
forall a. Semigroup a => a -> a -> a
<>
                Command r -> String
forall a. Show a => a -> String
show Command r
cmd

    avoidTransientState :: Model r -> Model r
avoidTransientState = Context -> Command r -> Model r -> Model r
forall (r :: * -> *). Context -> Command r -> Model r -> Model r
fixupModelState Context
ctx Command r
cmd

postcondition ::
     Model Concrete
  -> Command Concrete
  -> Response Concrete
  -> QSM.Logic
postcondition :: Model Concrete -> Command Concrete -> Response Concrete -> Logic
postcondition Model Concrete
model Command Concrete
_cmd = \case
    ReadThisGsmState GsmState
s' ->
        GsmState
s' GsmState -> GsmState -> Logic
forall a. (Eq a, Show a) => a -> a -> Logic
QSM..== GsmState
s
    ReadThisMarker MarkerState
m' ->
        MarkerState
m' MarkerState -> MarkerState -> Logic
forall a. (Eq a, Show a) => a -> a -> Logic
QSM..== GsmState -> MarkerState
toMarker GsmState
s
    Response Concrete
Unit ->
        Logic
QSM.Top
  where
    s :: GsmState
s = ModelState -> GsmState
toGsmState (ModelState -> GsmState) -> ModelState -> GsmState
forall a b. (a -> b) -> a -> b
$ Model Concrete -> ModelState
forall (r :: * -> *). Model r -> ModelState
mState Model Concrete
model

generator ::
     Maybe UpstreamPeer
  -> Model Symbolic
  -> Maybe (QC.Gen (Command Symbolic))
generator :: Maybe UpstreamPeer
-> Model Symbolic -> Maybe (Gen (Command Symbolic))
generator Maybe UpstreamPeer
ub Model Symbolic
model = Gen (Command Symbolic) -> Maybe (Gen (Command Symbolic))
forall a. a -> Maybe a
Just (Gen (Command Symbolic) -> Maybe (Gen (Command Symbolic)))
-> Gen (Command Symbolic) -> Maybe (Gen (Command Symbolic))
forall a b. (a -> b) -> a -> b
$ [(Int, Gen (Command Symbolic))] -> Gen (Command Symbolic)
forall a. HasCallStack => [(Int, Gen a)] -> Gen a
QC.frequency ([(Int, Gen (Command Symbolic))] -> Gen (Command Symbolic))
-> [(Int, Gen (Command Symbolic))] -> Gen (Command Symbolic)
forall a b. (a -> b) -> a -> b
$
    [ (,) Int
5 (Gen (Command Symbolic) -> (Int, Gen (Command Symbolic)))
-> Gen (Command Symbolic) -> (Int, Gen (Command Symbolic))
forall a b. (a -> b) -> a -> b
$ UpstreamPeer -> Command Symbolic
forall (r :: * -> *). UpstreamPeer -> Command r
Disconnect (UpstreamPeer -> Command Symbolic)
-> Gen UpstreamPeer -> Gen (Command Symbolic)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [UpstreamPeer] -> Gen UpstreamPeer
forall a. HasCallStack => [a] -> Gen a
elements [UpstreamPeer]
old | [UpstreamPeer] -> Bool
forall a. [a] -> Bool
notNull [UpstreamPeer]
old ]
 [(Int, Gen (Command Symbolic))]
-> [(Int, Gen (Command Symbolic))]
-> [(Int, Gen (Command Symbolic))]
forall a. Semigroup a => a -> a -> a
<>
    [ (,) Int
10 (Gen (Command Symbolic) -> (Int, Gen (Command Symbolic)))
-> Gen (Command Symbolic) -> (Int, Gen (Command Symbolic))
forall a b. (a -> b) -> a -> b
$ S -> Command Symbolic
forall (r :: * -> *). S -> Command r
ExtendSelection (S -> Command Symbolic) -> Gen S -> Gen (Command Symbolic)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [S] -> Gen S
forall a. HasCallStack => [a] -> Gen a
elements [S]
sdels
    | [S] -> Bool
forall a. [a] -> Bool
notNull [S]
sdels
    , Model Symbolic -> Bool
forall (r :: * -> *). Model r -> Bool
selectionIsBehind Model Symbolic
model   -- NB harmless to assume this node never mints
    ]
 [(Int, Gen (Command Symbolic))]
-> [(Int, Gen (Command Symbolic))]
-> [(Int, Gen (Command Symbolic))]
forall a. Semigroup a => a -> a -> a
<>
    [ (,) Int
20 (Gen (Command Symbolic) -> (Int, Gen (Command Symbolic)))
-> Gen (Command Symbolic) -> (Int, Gen (Command Symbolic))
forall a b. (a -> b) -> a -> b
$ do
          (UpstreamPeer
peer, [B]
bdel) <- [(UpstreamPeer, [B])] -> Gen (UpstreamPeer, [B])
forall a. HasCallStack => [a] -> Gen a
elements [(UpstreamPeer, [B])]
bdels
          UpstreamPeer -> B -> Command Symbolic
forall (r :: * -> *). UpstreamPeer -> B -> Command r
ModifyCandidate UpstreamPeer
peer (B -> Command Symbolic) -> Gen B -> Gen (Command Symbolic)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [B] -> Gen B
forall a. HasCallStack => [a] -> Gen a
elements [B]
bdel
    | [(UpstreamPeer, [B])] -> Bool
forall a. [a] -> Bool
notNull [(UpstreamPeer, [B])]
bdels
    ]
 [(Int, Gen (Command Symbolic))]
-> [(Int, Gen (Command Symbolic))]
-> [(Int, Gen (Command Symbolic))]
forall a. Semigroup a => a -> a -> a
<>
    [ (,) Int
100 (Gen (Command Symbolic) -> (Int, Gen (Command Symbolic)))
-> Gen (Command Symbolic) -> (Int, Gen (Command Symbolic))
forall a b. (a -> b) -> a -> b
$
            UpstreamPeer -> B -> Command Symbolic
forall (r :: * -> *). UpstreamPeer -> B -> Command r
NewCandidate
        (UpstreamPeer -> B -> Command Symbolic)
-> Gen UpstreamPeer -> Gen (B -> Command Symbolic)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [UpstreamPeer] -> Gen UpstreamPeer
forall a. HasCallStack => [a] -> Gen a
elements [UpstreamPeer]
new
        Gen (B -> Command Symbolic) -> Gen B -> Gen (Command Symbolic)
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
choose (-Int
10, Int
10))
    | [UpstreamPeer] -> Bool
forall a. [a] -> Bool
notNull [UpstreamPeer]
new
    ]
 [(Int, Gen (Command Symbolic))]
-> [(Int, Gen (Command Symbolic))]
-> [(Int, Gen (Command Symbolic))]
forall a. Semigroup a => a -> a -> a
<>
    [ (,) Int
20 (Gen (Command Symbolic) -> (Int, Gen (Command Symbolic)))
-> Gen (Command Symbolic) -> (Int, Gen (Command Symbolic))
forall a b. (a -> b) -> a -> b
$ Command Symbolic -> Gen (Command Symbolic)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Command Symbolic
forall (r :: * -> *). Command r
ReadGsmState ]
 [(Int, Gen (Command Symbolic))]
-> [(Int, Gen (Command Symbolic))]
-> [(Int, Gen (Command Symbolic))]
forall a. Semigroup a => a -> a -> a
<>
    [ (,) Int
20 (Gen (Command Symbolic) -> (Int, Gen (Command Symbolic)))
-> Gen (Command Symbolic) -> (Int, Gen (Command Symbolic))
forall a b. (a -> b) -> a -> b
$ Command Symbolic -> Gen (Command Symbolic)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Command Symbolic
forall (r :: * -> *). Command r
ReadMarker ]
 [(Int, Gen (Command Symbolic))]
-> [(Int, Gen (Command Symbolic))]
-> [(Int, Gen (Command Symbolic))]
forall a. Semigroup a => a -> a -> a
<>
    [ (,) Int
50 (Gen (Command Symbolic) -> (Int, Gen (Command Symbolic)))
-> Gen (Command Symbolic) -> (Int, Gen (Command Symbolic))
forall a b. (a -> b) -> a -> b
$ UpstreamPeer -> Command Symbolic
forall (r :: * -> *). UpstreamPeer -> Command r
StartIdling (UpstreamPeer -> Command Symbolic)
-> Gen UpstreamPeer -> Gen (Command Symbolic)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [UpstreamPeer] -> Gen UpstreamPeer
forall a. HasCallStack => [a] -> Gen a
elements [UpstreamPeer]
oldNotIdling | [UpstreamPeer] -> Bool
forall a. [a] -> Bool
notNull [UpstreamPeer]
oldNotIdling ]
 [(Int, Gen (Command Symbolic))]
-> [(Int, Gen (Command Symbolic))]
-> [(Int, Gen (Command Symbolic))]
forall a. Semigroup a => a -> a -> a
<>
    [ (,) Int
100 (Gen (Command Symbolic) -> (Int, Gen (Command Symbolic)))
-> Gen (Command Symbolic) -> (Int, Gen (Command Symbolic))
forall a b. (a -> b) -> a -> b
$ Int -> Command Symbolic
forall (r :: * -> *). Int -> Command r
TimePasses (Int -> Command Symbolic) -> Gen Int -> Gen (Command Symbolic)
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 :: forall (r :: * -> *). Model r -> Map UpstreamPeer Candidate
mCandidates = Map UpstreamPeer Candidate
cands
      ,
        mClock :: forall (r :: * -> *). Model r -> Time
mClock = Time
clk
      ,
        mIdlers :: forall (r :: * -> *). Model r -> Set UpstreamPeer
mIdlers = Set UpstreamPeer
idlers
      ,
        mPrev :: forall (r :: * -> *). Model r -> WhetherPrevTimePasses
mPrev = WhetherPrevTimePasses
prev
      ,
        mSelection :: forall (r :: * -> *). Model r -> Selection
mSelection = Selection
sel
      } = Model Symbolic
model

    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
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
choose (Int
300, Int
600)
        | case Model Symbolic -> ModelState
forall (r :: * -> *). Model r -> ModelState
mState Model Symbolic
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 Symbolic -> Command Symbolic -> [Command Symbolic]
shrinker :: Model Symbolic -> Command Symbolic -> [Command Symbolic]
shrinker Model Symbolic
_model = \case
    Disconnect{} ->
        []
    ExtendSelection S
sdel ->
        [ S -> Command Symbolic
forall (r :: * -> *). S -> Command r
ExtendSelection S
sdel' | S
sdel' <- S -> [S]
shrinkS S
sdel ]
    ModifyCandidate UpstreamPeer
peer B
bdel ->
        [ UpstreamPeer -> B -> Command Symbolic
forall (r :: * -> *). UpstreamPeer -> B -> Command r
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 ->
        [ UpstreamPeer -> B -> Command Symbolic
forall (r :: * -> *). UpstreamPeer -> B -> Command r
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  ]
    Command Symbolic
ReadGsmState ->
        []
    Command Symbolic
ReadMarker ->
        []
    StartIdling{} ->
        []
    TimePasses Int
dur ->
        [ Int -> Command Symbolic
forall (r :: * -> *). Int -> Command r
TimePasses Int
dur' | Int
dur' <- Int -> [Int]
forall a. Arbitrary a => a -> [a]
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]
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]
shrink Int
x ]

mock :: Model r -> Command r -> Response r
mock :: forall (r :: * -> *). Model r -> Command r -> Response r
mock Model r
model = \case
    Disconnect{} ->
        Response r
forall (r :: * -> *). Response r
Unit
    ExtendSelection{} ->
        Response r
forall (r :: * -> *). Response r
Unit
    ModifyCandidate{} ->
        Response r
forall (r :: * -> *). Response r
Unit
    NewCandidate{} ->
        Response r
forall (r :: * -> *). Response r
Unit
    Command r
ReadGsmState ->
        GsmState -> Response r
forall (r :: * -> *). GsmState -> Response r
ReadThisGsmState GsmState
s
    Command r
ReadMarker ->
        MarkerState -> Response r
forall (r :: * -> *). MarkerState -> Response r
ReadThisMarker (MarkerState -> Response r) -> MarkerState -> Response r
forall a b. (a -> b) -> a -> b
$ GsmState -> MarkerState
toMarker GsmState
s
    StartIdling{} ->
        Response r
forall (r :: * -> *). Response r
Unit
    TimePasses{} ->
        Response r
forall (r :: * -> *). Response r
Unit
  where
    s :: GsmState
s = ModelState -> GsmState
toGsmState (ModelState -> GsmState) -> ModelState -> GsmState
forall a b. (a -> b) -> a -> b
$ Model r -> ModelState
forall (r :: * -> *). Model r -> ModelState
mState Model r
model

-----

-- | 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 -> ShowS
[B] -> ShowS
B -> String
(Int -> B -> ShowS) -> (B -> String) -> ([B] -> ShowS) -> Show B
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> B -> ShowS
showsPrec :: Int -> B -> ShowS
$cshow :: B -> String
show :: B -> String
$cshowList :: [B] -> ShowS
showList :: [B] -> ShowS
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 -> ShowS
[S] -> ShowS
S -> String
(Int -> S -> ShowS) -> (S -> String) -> ([S] -> ShowS) -> Show S
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> S -> ShowS
showsPrec :: Int -> S -> ShowS
$cshow :: S -> String
show :: S -> String
$cshowList :: [S] -> ShowS
showList :: [S] -> ShowS
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 -> ShowS
[UpstreamPeer] -> ShowS
UpstreamPeer -> String
(Int -> UpstreamPeer -> ShowS)
-> (UpstreamPeer -> String)
-> ([UpstreamPeer] -> ShowS)
-> Show UpstreamPeer
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> UpstreamPeer -> ShowS
showsPrec :: Int -> UpstreamPeer -> ShowS
$cshow :: UpstreamPeer -> String
show :: UpstreamPeer -> String
$cshowList :: [UpstreamPeer] -> ShowS
showList :: [UpstreamPeer] -> ShowS
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 -> ShowS
[Selection] -> ShowS
Selection -> String
(Int -> Selection -> ShowS)
-> (Selection -> String)
-> ([Selection] -> ShowS)
-> Show Selection
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Selection -> ShowS
showsPrec :: Int -> Selection -> ShowS
$cshow :: Selection -> String
show :: Selection -> String
$cshowList :: [Selection] -> ShowS
showList :: [Selection] -> ShowS
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 -> ShowS
[Candidate] -> ShowS
Candidate -> String
(Int -> Candidate -> ShowS)
-> (Candidate -> String)
-> ([Candidate] -> ShowS)
-> Show Candidate
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Candidate -> ShowS
showsPrec :: Int -> Candidate -> ShowS
$cshow :: Candidate -> String
show :: Candidate -> String
$cshowList :: [Candidate] -> ShowS
showList :: [Candidate] -> ShowS
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 -> ShowS
[MarkerState] -> ShowS
MarkerState -> String
(Int -> MarkerState -> ShowS)
-> (MarkerState -> String)
-> ([MarkerState] -> ShowS)
-> Show MarkerState
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> MarkerState -> ShowS
showsPrec :: Int -> MarkerState -> ShowS
$cshow :: MarkerState -> String
show :: MarkerState -> String
$cshowList :: [MarkerState] -> ShowS
showList :: [MarkerState] -> ShowS
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 -> ShowS
[WhetherPrevTimePasses] -> ShowS
WhetherPrevTimePasses -> String
(Int -> WhetherPrevTimePasses -> ShowS)
-> (WhetherPrevTimePasses -> String)
-> ([WhetherPrevTimePasses] -> ShowS)
-> Show WhetherPrevTimePasses
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> WhetherPrevTimePasses -> ShowS
showsPrec :: Int -> WhetherPrevTimePasses -> ShowS
$cshow :: WhetherPrevTimePasses -> String
show :: WhetherPrevTimePasses -> String
$cshowList :: [WhetherPrevTimePasses] -> ShowS
showList :: [WhetherPrevTimePasses] -> ShowS
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
  |
    ModelCaughtUp !SI.Time
    -- ^ when the model most recently transitioned to 'GSM.CaughtUp'.
  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 -> ShowS
[ModelState] -> ShowS
ModelState -> String
(Int -> ModelState -> ShowS)
-> (ModelState -> String)
-> ([ModelState] -> ShowS)
-> Show ModelState
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ModelState -> ShowS
showsPrec :: Int -> ModelState -> ShowS
$cshow :: ModelState -> String
show :: ModelState -> String
$cshowList :: [ModelState] -> ShowS
showList :: [ModelState] -> ShowS
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 =
    BigDurN
    -- ^ there was a "big" 'TimesPasses' command
  |
    CaughtUpN
    -- ^ the node transitioned from Syncing to CaughtUp
  |
    FellBehindN
    -- ^ the node transitioned from CaughtUp to PreSyncing
  |
    SyncingToPreSyncingN
    -- ^ the node transition from Syncing to PreSyncing
  |
    PreSyncingToSyncingN
    -- ^ the node transition from PreSyncing to Syncing
  |
    FlickerN
    -- ^ the node transitioned from CaughtUp to PreSyncing to Syncing and back
    -- to CaughtUp "instantly"
  |
    NotThrashingN
    -- ^ the anti-thrashing would have allowed 'FellBehindN', but the selection
    -- wasn't old enough
  |
    TooOldN
    -- ^ the selection was old enough for 'FellBehindN', but the anti-thrashing
    -- prevented it
  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 -> ShowS
[Notable] -> ShowS
Notable -> String
(Int -> Notable -> ShowS)
-> (Notable -> String) -> ([Notable] -> ShowS) -> Show Notable
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Notable -> ShowS
showsPrec :: Int -> Notable -> ShowS
$cshow :: Notable -> String
show :: Notable -> String
$cshowList :: [Notable] -> ShowS
showList :: [Notable] -> ShowS
Show)

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

----- orphans

deriving instance Read 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 -> []

-----

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')

-----

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

-----

atom :: String -> Bool -> QSM.Logic
atom :: String -> Bool -> Logic
atom String
s Bool
b = Bool -> Logic
QSM.Boolean Bool
b Logic -> String -> Logic
QSM..// String
s

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

selectionIsBehind :: Model r -> Bool
selectionIsBehind :: forall (r :: * -> *). Model r -> Bool
selectionIsBehind Model r
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 :: forall (r :: * -> *). Model r -> Map UpstreamPeer Candidate
mCandidates = Map UpstreamPeer Candidate
cands
      ,
        mSelection :: forall (r :: * -> *). Model r -> Selection
mSelection = Selection B
b S
_s
      } = Model r
model

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

-- | 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.
boringDur :: Model r -> Int -> QSM.Logic
boringDur :: forall (r :: * -> *). Model r -> Int -> Logic
boringDur Model r
model Int
dur =
    Logic
boringSelection Logic -> Logic -> Logic
QSM..&& Logic
boringState
  where
    Model {
        mClock :: forall (r :: * -> *). Model r -> Time
mClock = Time
clk
      ,
        mSelection :: forall (r :: * -> *). Model r -> Selection
mSelection = Selection
sel
      ,
        mState :: forall (r :: * -> *). Model r -> ModelState
mState = ModelState
st
      } = Model r
model

    -- 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 :: Logic
boringSelection = String
"boringDur selection" String -> Bool -> Logic
`atom` (Time
clk' Time -> Time -> Bool
forall a. Eq a => a -> a -> Bool
/= Time
expiryAge)

    boringState :: Logic
boringState = case ModelState
st of
        ModelState
ModelPreSyncing         -> Logic
QSM.Top
        ModelState
ModelSyncing            -> Logic
QSM.Top
        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
            String
"boringDur state" String -> Bool -> Logic
`atom` (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)