{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE Rank2Types #-}

module Test.Consensus.GSM (tests) where

import           Control.Concurrent.Class.MonadSTM.Strict.TVar.Checked
import           Control.Monad (replicateM_)
import           Control.Monad.Class.MonadAsync (poll, withAsync)
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.Tracer (Tracer (Tracer))
import           Data.Functor ((<&>))
import qualified Data.Map.Strict as Map
import qualified Data.Set as Set
import qualified Ouroboros.Consensus.Node.GSM as GSM
import           Ouroboros.Consensus.Util.IOLike (IOLike)
import           Ouroboros.Network.PeerSelection.LedgerPeers.Type
                     (LedgerStateJudgement (..))
import           Test.Consensus.GSM.Model
import           Test.Consensus.IOSimQSM.Test.StateMachine.Sequential
                     (runCommands')
import qualified Test.QuickCheck as QC
import qualified Test.QuickCheck.Monadic as QC
import qualified Test.StateMachine as QSM
import           Test.StateMachine (Concrete)
import qualified Test.StateMachine.Types as QSM
import           Test.Tasty (TestTree)
import           Test.Tasty.QuickCheck (testProperty)
import           Test.Util.Orphans.IOLike ()
import           Test.Util.TestEnv (adjustQuickCheckTests)
import           Test.Util.ToExpr ()

-----

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
ub 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 Maybe UpstreamPeer
ub
      | Maybe UpstreamPeer
ub <- 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"

----- the QSM code under test

-- 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 the model definition is in "Test.Consensus.GSM.Model".

semantics ::
     IOLike m
  => Vars m
  -> Command Concrete
  -> m (Response Concrete)
semantics :: forall (m :: * -> *).
IOLike m =>
Vars m -> Command Concrete -> m (Response Concrete)
semantics Vars m
vars Command Concrete
cmd = m (Response Concrete) -> m (Response Concrete)
forall {b}. m b -> m b
pre (m (Response Concrete) -> m (Response Concrete))
-> m (Response Concrete) -> m (Response Concrete)
forall a b. (a -> b) -> a -> b
$ case Command Concrete
cmd 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
        Response Concrete -> m (Response Concrete)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Response Concrete
forall (r :: * -> *). Response r
Unit
    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
b S
s <- StrictTVar m Selection -> STM m Selection
forall (m :: * -> *) a. MonadSTM m => StrictTVar m a -> STM m a
readTVar StrictTVar m Selection
varSelection
            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
$! B -> S -> Selection
Selection (B
b B -> B -> B
forall a. Num a => a -> a -> a
+ B
1) (S
s S -> S -> S
forall a. Num a => a -> a -> a
+ S
sdel)
        Response Concrete -> m (Response Concrete)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Response Concrete
forall (r :: * -> *). Response r
Unit
    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

            StrictTVar m PeerState
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
b <- PeerState -> Candidate
psCandidate (PeerState -> Candidate) -> STM m PeerState -> STM m Candidate
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> StrictTVar m PeerState -> STM m PeerState
forall (m :: * -> *) a. MonadSTM m => StrictTVar m a -> STM m a
readTVar StrictTVar m PeerState
v
            StrictTVar m PeerState -> PeerState -> STM m ()
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
StrictTVar m a -> a -> STM m ()
writeTVar StrictTVar m PeerState
v (PeerState -> STM m ()) -> PeerState -> STM m ()
forall a b. (a -> b) -> a -> b
$! Candidate -> Idling -> PeerState
PeerState (B -> Candidate
Candidate (B
b B -> B -> B
forall a. Num a => a -> a -> a
+ B
bdel)) (Bool -> Idling
Idling Bool
False)

        Response Concrete -> m (Response Concrete)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Response Concrete
forall (r :: * -> *). Response r
Unit
    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
b S
_s <- StrictTVar m Selection -> STM m Selection
forall (m :: * -> *) a. MonadSTM m => StrictTVar m a -> STM m a
readTVar StrictTVar m Selection
varSelection
            StrictTVar m PeerState
v <- PeerState -> STM m (StrictTVar m PeerState)
forall (m :: * -> *) a. MonadSTM m => a -> STM m (StrictTVar m a)
newTVar (PeerState -> STM m (StrictTVar m PeerState))
-> PeerState -> STM m (StrictTVar m PeerState)
forall a b. (a -> b) -> a -> b
$! Candidate -> Idling -> PeerState
PeerState (B -> Candidate
Candidate (B
b B -> B -> B
forall a. Num a => a -> a -> a
+ B
bdel)) (Bool -> Idling
Idling Bool
False)
            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
-> StrictTVar m PeerState
-> Map UpstreamPeer (StrictTVar m PeerState)
-> Map UpstreamPeer (StrictTVar m PeerState)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert UpstreamPeer
peer StrictTVar m PeerState
v
        Response Concrete -> m (Response Concrete)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Response Concrete
forall (r :: * -> *). Response r
Unit
    Command Concrete
ReadGsmState -> do
        (GsmState -> Response Concrete)
-> m GsmState -> m (Response Concrete)
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap GsmState -> Response Concrete
forall (r :: * -> *). GsmState -> Response r
ReadThisGsmState (m GsmState -> m (Response Concrete))
-> m GsmState -> m (Response Concrete)
forall a b. (a -> b) -> a -> b
$ STM m GsmState -> m GsmState
forall a. HasCallStack => STM m a -> m a
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
STM m a -> m a
atomically (STM m GsmState -> m GsmState) -> STM m GsmState -> m GsmState
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
    Command Concrete
ReadMarker -> do
        (MarkerState -> Response Concrete)
-> m MarkerState -> m (Response Concrete)
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap MarkerState -> Response Concrete
forall (r :: * -> *). MarkerState -> Response r
ReadThisMarker (m MarkerState -> m (Response Concrete))
-> m MarkerState -> m (Response Concrete)
forall a b. (a -> b) -> a -> b
$ STM m MarkerState -> m MarkerState
forall a. HasCallStack => STM m a -> m a
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
STM m a -> m a
atomically (STM m MarkerState -> m MarkerState)
-> STM m MarkerState -> m MarkerState
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 (Response Concrete) -> m (Response Concrete)
forall a. HasCallStack => STM m a -> m a
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
STM m a -> m a
atomically (STM m (Response Concrete) -> m (Response Concrete))
-> STM m (Response Concrete) -> m (Response Concrete)
forall a b. (a -> b) -> a -> b
$ do
        StrictTVar m PeerState
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
        StrictTVar m PeerState -> (PeerState -> PeerState) -> STM m ()
forall (m :: * -> *) a.
MonadSTM m =>
StrictTVar m a -> (a -> a) -> STM m ()
modifyTVar StrictTVar m PeerState
v ((PeerState -> PeerState) -> STM m ())
-> (PeerState -> PeerState) -> STM m ()
forall a b. (a -> b) -> a -> b
$ \ (PeerState Candidate
c Idling
_) -> Candidate -> Idling -> PeerState
PeerState Candidate
c (Bool -> Idling
Idling Bool
True)
        Response Concrete -> STM m (Response Concrete)
forall a. a -> STM m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Response Concrete
forall (r :: * -> *). Response r
Unit
    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)
        Response Concrete -> m (Response Concrete)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Response Concrete
forall (r :: * -> *). Response r
Unit
  where
    Vars
        StrictTVar m Selection
varSelection
        StrictTVar m (Map UpstreamPeer (StrictTVar m PeerState))
varStates
        StrictTVar m GsmState
varGsmState
        StrictTVar m MarkerState
varMarker
        EvRecorder m
varEvents
      = Vars m
vars

    pre :: m b -> m b
pre m b
m = do
        EvRecorder m -> Ev -> m ()
forall (m :: * -> *). IOLike m => EvRecorder m -> Ev -> m ()
push EvRecorder m
varEvents (Command Concrete -> Ev
EvBegin Command Concrete
cmd)
        b
x <- m b
m
        m ()
forall (m :: * -> *). MonadFork m => m ()
yieldSeveralTimes   -- see Note [Why yield after the command]
        EvRecorder m -> Ev -> m ()
forall (m :: * -> *). IOLike m => EvRecorder m -> Ev -> m ()
push EvRecorder m
varEvents Ev
EvEnd
        b -> m b
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure b
x

sm ::
     IOLike m
  => Maybe UpstreamPeer
  -> Vars m
  -> Context
  -> QSM.StateMachine Model Command m Response
sm :: forall (m :: * -> *).
IOLike m =>
Maybe UpstreamPeer
-> Vars m -> Context -> StateMachine Model Command m Response
sm Maybe UpstreamPeer
ub Vars m
vars Context
ctx = QSM.StateMachine {
    cleanup :: Model Concrete -> m ()
QSM.cleanup = \Model Concrete
_model -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  ,
    generator :: Model Symbolic -> Maybe (Gen (Command Symbolic))
QSM.generator = Maybe UpstreamPeer
-> Model Symbolic -> Maybe (Gen (Command Symbolic))
generator Maybe UpstreamPeer
ub
  ,
    initModel :: forall (r :: * -> *). Model r
QSM.initModel = Context -> Model r
forall (r :: * -> *). Context -> Model r
initModel Context
ctx
  ,
    invariant :: Maybe (Model Concrete -> Logic)
QSM.invariant = Maybe (Model Concrete -> Logic)
forall a. Maybe a
Nothing
  ,
    mock :: Model Symbolic -> Command Symbolic -> GenSym (Response Symbolic)
QSM.mock = \Model Symbolic
model Command Symbolic
cmd -> Response Symbolic -> GenSym (Response Symbolic)
forall a. a -> GenSym a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Response Symbolic -> GenSym (Response Symbolic))
-> Response Symbolic -> GenSym (Response Symbolic)
forall a b. (a -> b) -> a -> b
$ Model Symbolic -> Command Symbolic -> Response Symbolic
forall (r :: * -> *). Model r -> Command r -> Response r
mock Model Symbolic
model Command Symbolic
cmd
  ,
    postcondition :: Model Concrete -> Command Concrete -> Response Concrete -> Logic
QSM.postcondition = Model Concrete -> Command Concrete -> Response Concrete -> Logic
postcondition
  ,
    precondition :: Model Symbolic -> Command Symbolic -> Logic
QSM.precondition = Context -> Model Symbolic -> Command Symbolic -> Logic
precondition Context
ctx
  ,
    semantics :: Command Concrete -> m (Response Concrete)
QSM.semantics = Vars m -> Command Concrete -> m (Response Concrete)
forall (m :: * -> *).
IOLike m =>
Vars m -> Command Concrete -> m (Response Concrete)
semantics Vars m
vars
  ,
    shrinker :: Model Symbolic -> Command Symbolic -> [Command Symbolic]
QSM.shrinker = Model Symbolic -> Command Symbolic -> [Command Symbolic]
shrinker
  ,
    transition :: forall (r :: * -> *).
(Show1 r, Ord1 r) =>
Model r -> Command r -> Response r -> Model r
QSM.transition = Context -> Model r -> Command r -> Response r -> Model r
forall (r :: * -> *).
Context -> Model r -> Command r -> Response r -> Model r
transition Context
ctx
  }

prop_sequential ::
     Maybe UpstreamPeer
  -> LedgerStateJudgement
  -> QC.Fun (Set.Set UpstreamPeer) Bool
  -> QC.Property
prop_sequential :: Maybe UpstreamPeer
-> LedgerStateJudgement -> Fun (Set UpstreamPeer) Bool -> Property
prop_sequential Maybe UpstreamPeer
ub LedgerStateJudgement
initialJudgement (QC.Fn Set UpstreamPeer -> Bool
isHaaSatisfied) =
    StateMachine Model Command IO Response
-> Maybe Int -> (Commands Command Response -> Property) -> Property
forall prop (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *)
       (model :: (* -> *) -> *) (m :: * -> *).
(Testable prop, Show (cmd Symbolic), Show (resp Symbolic),
 Show (model Symbolic), Traversable cmd, Foldable resp) =>
StateMachine model cmd m resp
-> Maybe Int -> (Commands cmd resp -> prop) -> Property
QSM.forAllCommands
        StateMachine Model Command IO Response
commandArbitrarySM
        Maybe Int
mbMinimumCommandLen
        (Context -> Commands Command Response -> Property
prop_sequential1 Context
ctx)
  where
    ctx :: Context
ctx = Context {
        cInitialJudgement :: LedgerStateJudgement
cInitialJudgement = LedgerStateJudgement
initialJudgement
      ,
        cIsHaaSatisfied :: Set UpstreamPeer -> Bool
cIsHaaSatisfied = Set UpstreamPeer -> Bool
isHaaSatisfied
      }

    mbMinimumCommandLen :: Maybe Int
mbMinimumCommandLen = Int -> Maybe Int
forall a. a -> Maybe a
Just Int
20   -- just a guess

    -- NB the monad is irrelevant here but is ambiguous, so we merely ascribe a
    -- convenient concrete one
    commandArbitrarySM :: StateMachine Model Command IO Response
commandArbitrarySM = Maybe UpstreamPeer
-> Vars IO -> Context -> StateMachine Model Command IO Response
forall (m :: * -> *).
IOLike m =>
Maybe UpstreamPeer
-> Vars m -> Context -> StateMachine Model Command m Response
sm Maybe UpstreamPeer
ub (Vars IO
forall a. HasCallStack => a
undefined :: Vars IO) Context
ctx

prop_sequential1 ::
     Context
  -> QSM.Commands Command Response
  -> QC.Property
prop_sequential1 :: Context -> Commands Command Response -> Property
prop_sequential1 Context
ctx Commands Command Response
cmds = (forall s. IOSim s Property) -> Property
runSimQC ((forall s. IOSim s Property) -> Property)
-> (forall s. IOSim s Property) -> Property
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

    -- these variables are part of the 'GSM.GsmView'
    StrictTVar (IOSim s) Selection
varSelection  <- Selection -> IOSim s (StrictTVar (IOSim s) Selection)
forall (m :: * -> *) a. MonadSTM m => a -> m (StrictTVar m a)
newTVarIO (Model Any -> Selection
forall (r :: * -> *). Model r -> Selection
mSelection (Model Any -> Selection) -> Model Any -> Selection
forall a b. (a -> b) -> a -> b
$ Context -> Model Any
forall (r :: * -> *). Context -> Model r
initModel Context
ctx)
    StrictTVar
  (IOSim s) (Map UpstreamPeer (StrictTVar (IOSim s) PeerState))
varStates     <- Map UpstreamPeer (StrictTVar (IOSim s) PeerState)
-> IOSim
     s
     (StrictTVar
        (IOSim s) (Map UpstreamPeer (StrictTVar (IOSim s) PeerState)))
forall (m :: * -> *) a. MonadSTM m => a -> m (StrictTVar m a)
newTVarIO Map UpstreamPeer (StrictTVar (IOSim s) PeerState)
forall k a. Map k a
Map.empty
    StrictTVar (IOSim s) GsmState
varGsmState   <- GsmState -> IOSim s (StrictTVar (IOSim s) GsmState)
forall (m :: * -> *) a. MonadSTM m => a -> m (StrictTVar m a)
newTVarIO GsmState
initialGsmState
    StrictTVar (IOSim s) MarkerState
varMarker     <- MarkerState -> IOSim s (StrictTVar (IOSim s) MarkerState)
forall (m :: * -> *) a. MonadSTM m => a -> m (StrictTVar m a)
newTVarIO (GsmState -> MarkerState
toMarker GsmState
initialGsmState)

    -- this variable is for better 'QC.counterexample' messages
    EvRecorder (IOSim s)
varEvents <- IOSim s (EvRecorder (IOSim s))
forall (m :: * -> *). IOLike m => m (EvRecorder m)
newRecorder
    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

    let vars :: Vars (IOSim s)
vars =
            StrictTVar (IOSim s) Selection
-> StrictTVar
     (IOSim s) (Map UpstreamPeer (StrictTVar (IOSim s) PeerState))
-> StrictTVar (IOSim s) GsmState
-> StrictTVar (IOSim s) MarkerState
-> EvRecorder (IOSim s)
-> Vars (IOSim s)
forall (m :: * -> *).
StrictTVar m Selection
-> StrictTVar m (Map UpstreamPeer (StrictTVar m PeerState))
-> StrictTVar m GsmState
-> StrictTVar m MarkerState
-> EvRecorder m
-> Vars m
Vars
                StrictTVar (IOSim s) Selection
varSelection
                StrictTVar
  (IOSim s) (Map UpstreamPeer (StrictTVar (IOSim s) PeerState))
varStates
                StrictTVar (IOSim s) GsmState
varGsmState
                StrictTVar (IOSim s) MarkerState
varMarker
                EvRecorder (IOSim s)
varEvents

    let executionSM :: StateMachine Model Command (IOSim s) Response
executionSM = Maybe UpstreamPeer
-> Vars (IOSim s)
-> Context
-> StateMachine Model Command (IOSim s) Response
forall (m :: * -> *).
IOLike m =>
Maybe UpstreamPeer
-> Vars m -> Context -> StateMachine Model Command m Response
sm (UpstreamPeer -> Maybe UpstreamPeer
forall a. a -> Maybe a
Just UpstreamPeer
forall a. Bounded a => a
maxBound) Vars (IOSim s)
vars Context
ctx

        -- NB the specific IO type is unused here
        prettySM :: StateMachine Model Command IO Response
prettySM = Maybe UpstreamPeer
-> Vars IO -> Context -> StateMachine Model Command IO Response
forall (m :: * -> *).
IOLike m =>
Maybe UpstreamPeer
-> Vars m -> Context -> StateMachine Model Command m Response
sm Maybe UpstreamPeer
forall a. HasCallStack => a
undefined Vars IO
forall a. HasCallStack => a
undefined Context
ctx

    let gsm :: GsmEntryPoints (IOSim s)
gsm = (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
          }
        gsmEntryPoint :: IOSim s neverTerminates
gsmEntryPoint = case LedgerStateJudgement
initialJudgement 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

    ((History Command Response
hist, Model Concrete
model', Reason
res), Maybe SomeException
mbExn) <- IOSim
  s
  ((History Command Response, Model Concrete, Reason),
   Maybe SomeException)
-> IOSim
     s
     ((History Command Response, Model Concrete, Reason),
      Maybe SomeException)
forall a. a -> a
id
      (IOSim
   s
   ((History Command Response, Model Concrete, Reason),
    Maybe SomeException)
 -> IOSim
      s
      ((History Command Response, Model Concrete, Reason),
       Maybe SomeException))
-> IOSim
     s
     ((History Command Response, Model Concrete, Reason),
      Maybe SomeException)
-> IOSim
     s
     ((History Command Response, Model Concrete, Reason),
      Maybe SomeException)
forall a b. (a -> b) -> a -> b
$ IOSim s Any
-> (Async (IOSim s) Any
    -> IOSim
         s
         ((History Command Response, Model Concrete, Reason),
          Maybe SomeException))
-> IOSim
     s
     ((History Command Response, Model Concrete, Reason),
      Maybe SomeException)
forall a b.
IOSim s a -> (Async (IOSim s) a -> IOSim s b) -> IOSim s b
forall (m :: * -> *) a b.
MonadAsync m =>
m a -> (Async m a -> m b) -> m b
withAsync IOSim s Any
forall neverTerminates. IOSim s neverTerminates
gsmEntryPoint
      ((Async (IOSim s) Any
  -> IOSim
       s
       ((History Command Response, Model Concrete, Reason),
        Maybe SomeException))
 -> IOSim
      s
      ((History Command Response, Model Concrete, Reason),
       Maybe SomeException))
-> (Async (IOSim s) Any
    -> IOSim
         s
         ((History Command Response, Model Concrete, Reason),
          Maybe SomeException))
-> IOSim
     s
     ((History Command Response, Model Concrete, Reason),
      Maybe SomeException)
forall a b. (a -> b) -> a -> b
$ \Async (IOSim s) Any
hGSM -> do

          IOSim s ()
forall (m :: * -> *). MonadFork m => m ()
yieldSeveralTimes   -- see Note [Why yield after the command]

          (History Command Response, Model Concrete, Reason)
x <- IOSim s (StateMachine Model Command (IOSim s) Response)
-> Commands Command Response
-> IOSim s (History Command Response, Model Concrete, Reason)
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
       (model :: (* -> *) -> *).
(Show (cmd Concrete), Show (resp Concrete), Traversable cmd,
 Foldable resp, IOLike m, MonadSay m) =>
m (StateMachine model cmd m resp)
-> Commands cmd resp
-> m (History cmd resp, model Concrete, Reason)
runCommands' (StateMachine Model Command (IOSim s) Response
-> IOSim s (StateMachine Model Command (IOSim s) Response)
forall a. a -> IOSim s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure StateMachine Model Command (IOSim s) Response
executionSM) Commands Command Response
cmds

          -- notice if the GSM thread raised an exception while processing the
          -- commands
          Async (IOSim s) Any -> IOSim s (Maybe (Either SomeException Any))
forall a.
Async (IOSim s) a -> IOSim s (Maybe (Either SomeException a))
forall (m :: * -> *) a.
MonadAsync m =>
Async m a -> m (Maybe (Either SomeException a))
poll Async (IOSim s) Any
hGSM IOSim s (Maybe (Either SomeException Any))
-> (Maybe (Either SomeException Any)
    -> ((History Command Response, Model Concrete, Reason),
        Maybe SomeException))
-> IOSim
     s
     ((History Command Response, Model Concrete, Reason),
      Maybe SomeException)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \case
              Just Right{}    ->
                  TestName
-> ((History Command Response, Model Concrete, Reason),
    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
                  ((History Command Response, Model Concrete, Reason)
x, SomeException -> Maybe SomeException
forall a. a -> Maybe a
Just SomeException
exn)
              Maybe (Either SomeException Any)
Nothing         ->
                  ((History Command Response, Model Concrete, Reason)
x, Maybe SomeException
forall a. Maybe a
Nothing)

    let noExn :: Property
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
    Property
lastCheck <- do
        Response Concrete
actual <- Vars (IOSim s) -> Command Concrete -> IOSim s (Response Concrete)
forall (m :: * -> *).
IOLike m =>
Vars m -> Command Concrete -> m (Response Concrete)
semantics Vars (IOSim s)
vars Command Concrete
forall (r :: * -> *). Command r
ReadGsmState
        let expected :: Response Concrete
expected = Model Concrete -> Command Concrete -> Response Concrete
forall (r :: * -> *). Model r -> Command r -> Response r
mock Model Concrete
model' Command Concrete
forall (r :: * -> *). Command r
ReadGsmState
        Property -> IOSim s Property
forall a. a -> IOSim s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> IOSim s Property) -> Property -> IOSim s Property
forall a b. (a -> b) -> a -> b
$ case (Response Concrete
actual, Response Concrete
expected) of
            (ReadThisGsmState GsmState
x, ReadThisGsmState GsmState
y) ->
                TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
QC.counterexample TestName
"lastCheck" (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ GsmState
x GsmState -> GsmState -> Property
forall a. (Eq a, Show a) => a -> a -> Property
QC.=== GsmState
y
            (Response Concrete, Response Concrete)
_ ->
                TestName -> Property
forall a. HasCallStack => TestName -> a
error TestName
"impossible! lastCheck response"

    [(Time, Ev)]
watcherEvents <- EvRecorder (IOSim s) -> IOSim s [(Time, Ev)]
forall (m :: * -> *). IOLike m => EvRecorder m -> m [(Time, Ev)]
dumpEvents EvRecorder (IOSim s)
varEvents

    Property -> IOSim s Property
forall a. a -> IOSim s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
      (Property -> IOSim s Property) -> Property -> IOSim s Property
forall a b. (a -> b) -> a -> b
$ PropertyM IO () -> Property
forall a. Testable a => PropertyM IO a -> Property
QC.monadicIO
      (PropertyM IO () -> Property) -> PropertyM IO () -> Property
forall a b. (a -> b) -> a -> b
$ StateMachine Model Command IO Response
-> History Command Response -> Property -> PropertyM IO ()
forall (m :: * -> *) (model :: (* -> *) -> *)
       (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
(MonadIO m, CanDiff (model Concrete), Show (cmd Concrete),
 Show (resp Concrete)) =>
StateMachine model cmd m resp
-> History cmd resp -> Property -> PropertyM m ()
QSM.prettyCommands StateMachine Model Command IO Response
prettySM History Command Response
hist
      (Property -> PropertyM IO ()) -> Property -> PropertyM IO ()
forall a b. (a -> b) -> a -> b
$ TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
QC.counterexample
            ([TestName] -> TestName
unlines
               ([TestName] -> TestName) -> [TestName] -> TestName
forall a b. (a -> b) -> a -> b
$ (:) TestName
"WATCHER"
               ([TestName] -> [TestName]) -> [TestName] -> [TestName]
forall a b. (a -> b) -> a -> b
$ ((Time, Ev) -> TestName) -> [(Time, Ev)] -> [TestName]
forall a b. (a -> b) -> [a] -> [b]
map ((TestName
"    " TestName -> TestName -> TestName
forall a. Semigroup a => a -> a -> a
<>) (TestName -> TestName)
-> ((Time, Ev) -> TestName) -> (Time, Ev) -> TestName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Time, Ev) -> TestName
forall a. Show a => a -> TestName
show)
               ([(Time, Ev)] -> [TestName]) -> [(Time, Ev)] -> [TestName]
forall a b. (a -> b) -> a -> b
$ [(Time, Ev)]
watcherEvents
            )
      (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ TestName -> [TestName] -> Property -> Property
forall prop.
Testable prop =>
TestName -> [TestName] -> prop -> Property
QC.tabulate
            TestName
"Notables"
            (case Set Notable -> [Notable]
forall a. Set a -> [a]
Set.toList (Set Notable -> [Notable]) -> Set Notable -> [Notable]
forall a b. (a -> b) -> a -> b
$ Model Concrete -> Set Notable
forall (r :: * -> *). Model r -> Set Notable
mNotables Model Concrete
model' 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
            )
      (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ Commands Command Response -> Property -> Property
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
CommandNames cmd =>
Commands cmd resp -> Property -> Property
QSM.checkCommandNames Commands Command Response
cmds
      (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ Property
noExn Property -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
QC..&&. Property
lastCheck Property -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
QC..&&. Reason
res Reason -> Reason -> Property
forall a. (Eq a, Show a) => a -> a -> Property
QC.=== Reason
QSM.Ok
  where
    Context {
        cInitialJudgement :: Context -> LedgerStateJudgement
cInitialJudgement = LedgerStateJudgement
initialJudgement
      ,
        cIsHaaSatisfied :: Context -> Set UpstreamPeer -> Bool
cIsHaaSatisfied = Set UpstreamPeer -> Bool
isHaaSatisfied
      } = Context
ctx

-----

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
    Time
now <- IOSim s Time
forall (m :: * -> *). MonadMonotonicTime m => m Time
SI.getMonotonicTime
    DurationFromNow -> IOSim s DurationFromNow
forall a. a -> IOSim s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (DurationFromNow -> IOSim s DurationFromNow)
-> DurationFromNow -> IOSim s DurationFromNow
forall a b. (a -> b) -> a -> b
$ case Time -> Time -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Time
expiryAge Time
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

-----

-- | 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 ()
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.

-}

-- | 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 =
   Property -> Property
forall prop. Testable prop => prop -> Property
QC.once
 (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ Context -> Commands Command Response -> Property
prop_sequential1 Context
ctx
 (Commands Command Response -> Property)
-> Commands Command Response -> Property
forall a b. (a -> b) -> a -> b
$ [Command Command Response] -> Commands Command Response
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
[Command cmd resp] -> Commands cmd resp
QSM.Commands
     [ Command Symbolic
-> Response Symbolic -> [Var] -> Command Command Response
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
cmd Symbolic -> resp Symbolic -> [Var] -> Command cmd resp
QSM.Command (UpstreamPeer -> B -> Command Symbolic
forall (r :: * -> *). UpstreamPeer -> B -> Command r
NewCandidate UpstreamPeer
Amara (Int -> B
B Int
1)) Response Symbolic
forall (r :: * -> *). Response r
Unit []
     , Command Symbolic
-> Response Symbolic -> [Var] -> Command Command Response
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
cmd Symbolic -> resp Symbolic -> [Var] -> Command cmd resp
QSM.Command (UpstreamPeer -> Command Symbolic
forall (r :: * -> *). UpstreamPeer -> Command r
StartIdling UpstreamPeer
Amara) Response Symbolic
forall (r :: * -> *). Response r
Unit []
     , Command Symbolic
-> Response Symbolic -> [Var] -> Command Command Response
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
cmd Symbolic -> resp Symbolic -> [Var] -> Command cmd resp
QSM.Command (Int -> Command Symbolic
forall (r :: * -> *). Int -> Command r
TimePasses Int
61) Response Symbolic
forall (r :: * -> *). Response r
Unit []
     , Command Symbolic
-> Response Symbolic -> [Var] -> Command Command Response
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
cmd Symbolic -> resp Symbolic -> [Var] -> Command cmd resp
QSM.Command (S -> Command Symbolic
forall (r :: * -> *). S -> Command r
ExtendSelection (Int -> S
S (-Int
4))) Response Symbolic
forall (r :: * -> *). Response r
Unit []
     , Command Symbolic
-> Response Symbolic -> [Var] -> Command Command Response
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *).
cmd Symbolic -> resp Symbolic -> [Var] -> Command cmd resp
QSM.Command Command Symbolic
forall (r :: * -> *). Command r
ReadMarker (MarkerState -> Response Symbolic
forall (r :: * -> *). MarkerState -> Response r
ReadThisMarker MarkerState
Absent) []
     ]
  where
    ctx :: Context
ctx = Context {
        cInitialJudgement :: LedgerStateJudgement
cInitialJudgement = LedgerStateJudgement
YoungEnough
      ,
        cIsHaaSatisfied :: Set UpstreamPeer -> Bool
cIsHaaSatisfied = \Set UpstreamPeer
_peers -> Bool
True
      }

----- trivial event accumulator, useful for debugging test failures

data Ev =
    EvBegin (Command Concrete)
    -- ^ 'semantics' started stimulating the GSM code being tested
  |
    EvEnd
    -- ^ 'semantics' stopped stimulating the GSM code being tested
  |
    EvGsm (GSM.TraceGsmEvent Selection)
    -- ^ the GSM code being tested emitted an event
  deriving (Int -> Ev -> TestName -> TestName
[Ev] -> TestName -> TestName
Ev -> TestName
(Int -> Ev -> TestName -> TestName)
-> (Ev -> TestName) -> ([Ev] -> TestName -> TestName) -> Show Ev
forall a.
(Int -> a -> TestName -> TestName)
-> (a -> TestName) -> ([a] -> TestName -> TestName) -> Show a
$cshowsPrec :: Int -> Ev -> TestName -> TestName
showsPrec :: Int -> Ev -> TestName -> TestName
$cshow :: Ev -> TestName
show :: Ev -> TestName
$cshowList :: [Ev] -> TestName -> TestName
showList :: [Ev] -> TestName -> TestName
Show)

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
    Time
now <- m Time
forall (m :: * -> *). MonadMonotonicTime m => m Time
SI.getMonotonicTime
    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
$ StrictTVar m [(Time, Ev)]
-> ([(Time, Ev)] -> [(Time, Ev)]) -> STM m ()
forall (m :: * -> *) a.
MonadSTM m =>
StrictTVar m a -> (a -> a) -> STM m ()
modifyTVar StrictTVar m [(Time, Ev)]
var (([(Time, Ev)] -> [(Time, Ev)]) -> STM m ())
-> ([(Time, Ev)] -> [(Time, Ev)]) -> STM m ()
forall a b. (a -> b) -> a -> b
$ (:) (Time
now, Ev
ev)

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

-----

-- | merely a tidy bundle of arguments
data Vars m = Vars
    (StrictTVar m Selection)
    (StrictTVar m (Map.Map UpstreamPeer (StrictTVar m PeerState)))
    (StrictTVar m GSM.GsmState)
    (StrictTVar m MarkerState)
    (EvRecorder m)

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)

-----

-- | a straight-forwardtrivial alias
runSimQC :: (forall s. IOSim.IOSim s QC.Property) -> QC.Property
runSimQC :: (forall s. IOSim s Property) -> Property
runSimQC forall s. IOSim s Property
m = case (forall s. IOSim s Property) -> Either Failure Property
forall a. (forall s. IOSim s a) -> Either Failure a
IOSim.runSim IOSim s Property
forall s. IOSim s Property
m of
    Left  Failure
failure -> TestName -> Bool -> Property
forall prop. Testable prop => TestName -> prop -> Property
QC.counterexample (Failure -> TestName
forall a. Show a => a -> TestName
show Failure
failure) Bool
False
    Right Property
prop    -> Property
prop