| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Test.Consensus.GSM.Model
Contents
Description
The definition of the GSM QSM model and its auxiliaries
Synopsis
- data Response (r ∷ Type → Type)
- newtype S = S Int
- newtype B = B Int
- data Context = Context {}
- data Model (r ∷ Type → Type) = Model {}
- generator ∷ Maybe UpstreamPeer → Model Symbolic → Maybe (Gen (Command Symbolic))
- data Command (r ∷ Type → Type)
- candidateOverSelection ∷ Selection → Candidate → CandidateVersusSelection
- data MarkerState
- mock ∷ ∀ (r ∷ Type → Type). Model r → Command r → Response r
- shrinker ∷ Model Symbolic → Command Symbolic → [Command Symbolic]
- postcondition ∷ Model Concrete → Command Concrete → Response Concrete → Logic
- precondition ∷ Context → Model Symbolic → Command Symbolic → Logic
- transition ∷ ∀ (r ∷ Type → Type). Context → Model r → Command r → Response r → Model r
- initModel ∷ ∀ (r ∷ Type → Type). Context → Model r
- data UpstreamPeer
- newtype Candidate = Candidate B
- data Notable
- newtype WhetherPrevTimePasses = WhetherPrevTimePasses Bool
- data Selection = Selection !B !S
- data ModelState
- addNotableWhen ∷ ∀ (r ∷ Type → Type). Notable → Bool → Model r → Model r
- atom ∷ String → Bool → Logic
- selectionIsBehind ∷ ∀ (r ∷ Type → Type). Model r → Bool
- selectionIsNotEarly ∷ ∀ (r ∷ Type → Type). Model r → Bool
- boringDur ∷ ∀ (r ∷ Type → Type). Model r → Int → Logic
- fixupModelState ∷ ∀ (r ∷ Type → Type). Context → Command r → Model r → Model r
- ageLimit ∷ Num a ⇒ a
- onset ∷ Selection → Time
- thrashLimit ∷ Num a ⇒ a
- toMarker ∷ GsmState → MarkerState
- toGsmState ∷ ModelState → GsmState
Documentation
data Response (r ∷ Type → Type) Source #
Constructors
| ReadThisGsmState GsmState | |
| ReadThisMarker MarkerState | |
| Unit |
Instances
A slot count
A block count
Constructors
| Context | |
data Model (r ∷ Type → Type) Source #
Constructors
| Model | |
Fields | |
Instances
| Generic (Model r) Source # | |||||
Defined in Test.Consensus.GSM.Model Associated Types
| |||||
| Show (Model r) Source # | |||||
| ToExpr (Model r) Source # | |||||
| type Rep (Model r) Source # | |||||
Defined in Test.Consensus.GSM.Model type Rep (Model r) = D1 ('MetaData "Model" "Test.Consensus.GSM.Model" "ouroboros-consensus-diffusion-0.23.0.0-inplace-consensus-test" 'False) (C1 ('MetaCons "Model" 'PrefixI 'True) ((S1 ('MetaSel ('Just "mCandidates") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map UpstreamPeer Candidate)) :*: (S1 ('MetaSel ('Just "mClock") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Time) :*: S1 ('MetaSel ('Just "mIdlers") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set UpstreamPeer)))) :*: ((S1 ('MetaSel ('Just "mNotables") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set Notable)) :*: S1 ('MetaSel ('Just "mPrev") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 WhetherPrevTimePasses)) :*: (S1 ('MetaSel ('Just "mSelection") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Selection) :*: S1 ('MetaSel ('Just "mState") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ModelState))))) | |||||
data Command (r ∷ Type → Type) Source #
TODO restarts (or maybe just killing the GSM thread)
Constructors
| Disconnect UpstreamPeer | INVARIANT must be an existing peer Mocks the necessary ChainSync client behavior. |
| ExtendSelection S | INVARIANT NOTE Harmless to assume it only advances by |
| 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
NOTE The generator does not yield consecutive |
Instances
| Foldable Command Source # | |||||
| Functor Command Source # | |||||
| Traversable Command Source # | |||||
Defined in Test.Consensus.GSM.Model | |||||
| Read (Command r) Source # | |||||
| Show (Command r) Source # | |||||
| Generic1 Command Source # | |||||
Defined in Test.Consensus.GSM.Model Associated Types
| |||||
| CommandNames Command Source # | |||||
| type Rep1 Command Source # | |||||
Defined in Test.Consensus.GSM.Model type Rep1 Command = D1 ('MetaData "Command" "Test.Consensus.GSM.Model" "ouroboros-consensus-diffusion-0.23.0.0-inplace-consensus-test" 'False) (((C1 ('MetaCons "Disconnect" 'PrefixI 'False) (S1 ('MetaSel ('Nothing ∷ Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 UpstreamPeer)) :+: C1 ('MetaCons "ExtendSelection" 'PrefixI 'False) (S1 ('MetaSel ('Nothing ∷ Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 S))) :+: (C1 ('MetaCons "ModifyCandidate" 'PrefixI 'False) (S1 ('MetaSel ('Nothing ∷ Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 UpstreamPeer) :*: S1 ('MetaSel ('Nothing ∷ Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 B)) :+: C1 ('MetaCons "NewCandidate" 'PrefixI 'False) (S1 ('MetaSel ('Nothing ∷ Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 UpstreamPeer) :*: S1 ('MetaSel ('Nothing ∷ Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 B)))) :+: ((C1 ('MetaCons "ReadGsmState" 'PrefixI 'False) (U1 ∷ (Type → Type) → Type) :+: C1 ('MetaCons "ReadMarker" 'PrefixI 'False) (U1 ∷ (Type → Type) → Type)) :+: (C1 ('MetaCons "StartIdling" 'PrefixI 'False) (S1 ('MetaSel ('Nothing ∷ Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 UpstreamPeer)) :+: C1 ('MetaCons "TimePasses" 'PrefixI 'False) (S1 ('MetaSel ('Nothing ∷ Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int))))) | |||||
data MarkerState Source #
Instances
| Arbitrary MarkerState Source # | |||||
Defined in Test.Consensus.GSM.Model | |||||
| Generic MarkerState Source # | |||||
Defined in Test.Consensus.GSM.Model Associated Types
| |||||
| Read MarkerState Source # | |||||
Defined in Test.Consensus.GSM.Model Methods readsPrec ∷ Int → ReadS MarkerState # readList ∷ ReadS [MarkerState] # | |||||
| Show MarkerState Source # | |||||
Defined in Test.Consensus.GSM.Model Methods showsPrec ∷ Int → MarkerState → ShowS # show ∷ MarkerState → String # showList ∷ [MarkerState] → ShowS # | |||||
| Eq MarkerState Source # | |||||
Defined in Test.Consensus.GSM.Model | |||||
| Ord MarkerState Source # | |||||
Defined in Test.Consensus.GSM.Model Methods compare ∷ MarkerState → MarkerState → Ordering # (<) ∷ MarkerState → MarkerState → Bool # (<=) ∷ MarkerState → MarkerState → Bool # (>) ∷ MarkerState → MarkerState → Bool # (>=) ∷ MarkerState → MarkerState → Bool # max ∷ MarkerState → MarkerState → MarkerState # min ∷ MarkerState → MarkerState → MarkerState # | |||||
| ToExpr MarkerState Source # | |||||
Defined in Test.Consensus.GSM.Model | |||||
| type Rep MarkerState Source # | |||||
Defined in Test.Consensus.GSM.Model | |||||
data UpstreamPeer Source #
Instances
| CoArbitrary UpstreamPeer Source # | |||||
Defined in Test.Consensus.GSM.Model Methods coarbitrary ∷ UpstreamPeer → Gen b → Gen b Source # | |||||
| Function UpstreamPeer Source # | |||||
Defined in Test.Consensus.GSM.Model Methods function ∷ (UpstreamPeer → b) → UpstreamPeer :-> b Source # | |||||
| Bounded UpstreamPeer Source # | |||||
Defined in Test.Consensus.GSM.Model | |||||
| Enum UpstreamPeer Source # | |||||
Defined in Test.Consensus.GSM.Model Methods succ ∷ UpstreamPeer → UpstreamPeer # pred ∷ UpstreamPeer → UpstreamPeer # toEnum ∷ Int → UpstreamPeer # fromEnum ∷ UpstreamPeer → Int # enumFrom ∷ UpstreamPeer → [UpstreamPeer] # enumFromThen ∷ UpstreamPeer → UpstreamPeer → [UpstreamPeer] # enumFromTo ∷ UpstreamPeer → UpstreamPeer → [UpstreamPeer] # enumFromThenTo ∷ UpstreamPeer → UpstreamPeer → UpstreamPeer → [UpstreamPeer] # | |||||
| Generic UpstreamPeer Source # | |||||
Defined in Test.Consensus.GSM.Model Associated Types
| |||||
| Read UpstreamPeer Source # | |||||
Defined in Test.Consensus.GSM.Model Methods readsPrec ∷ Int → ReadS UpstreamPeer # readList ∷ ReadS [UpstreamPeer] # | |||||
| Show UpstreamPeer Source # | |||||
Defined in Test.Consensus.GSM.Model Methods showsPrec ∷ Int → UpstreamPeer → ShowS # show ∷ UpstreamPeer → String # showList ∷ [UpstreamPeer] → ShowS # | |||||
| Eq UpstreamPeer Source # | |||||
Defined in Test.Consensus.GSM.Model | |||||
| Ord UpstreamPeer Source # | |||||
Defined in Test.Consensus.GSM.Model Methods compare ∷ UpstreamPeer → UpstreamPeer → Ordering # (<) ∷ UpstreamPeer → UpstreamPeer → Bool # (<=) ∷ UpstreamPeer → UpstreamPeer → Bool # (>) ∷ UpstreamPeer → UpstreamPeer → Bool # (>=) ∷ UpstreamPeer → UpstreamPeer → Bool # max ∷ UpstreamPeer → UpstreamPeer → UpstreamPeer # min ∷ UpstreamPeer → UpstreamPeer → UpstreamPeer # | |||||
| ToExpr UpstreamPeer Source # | |||||
Defined in Test.Consensus.GSM.Model | |||||
| type Rep UpstreamPeer Source # | |||||
Defined in Test.Consensus.GSM.Model type Rep UpstreamPeer = D1 ('MetaData "UpstreamPeer" "Test.Consensus.GSM.Model" "ouroboros-consensus-diffusion-0.23.0.0-inplace-consensus-test" 'False) ((C1 ('MetaCons "Amara" 'PrefixI 'False) (U1 ∷ Type → Type) :+: C1 ('MetaCons "Bao" 'PrefixI 'False) (U1 ∷ Type → Type)) :+: (C1 ('MetaCons "Cait" 'PrefixI 'False) (U1 ∷ Type → Type) :+: (C1 ('MetaCons "Dhani" 'PrefixI 'False) (U1 ∷ Type → Type) :+: C1 ('MetaCons "Eric" 'PrefixI 'False) (U1 ∷ Type → Type)))) | |||||
The age of the candidate is irrelevant, only its length matters
Instances
| Generic Candidate Source # | |||||
Defined in Test.Consensus.GSM.Model Associated Types
| |||||
| Show Candidate Source # | |||||
| Eq Candidate Source # | |||||
| Ord Candidate Source # | |||||
Defined in Test.Consensus.GSM.Model | |||||
| ToExpr Candidate Source # | |||||
| type Rep Candidate Source # | |||||
Defined in Test.Consensus.GSM.Model | |||||
Interesting events to record within the model
TODO some less superficial ones (eg even just combinations of these)
Constructors
| BigDurN | there was a "big" |
| 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 |
| TooOldN | the selection was old enough for |
newtype WhetherPrevTimePasses Source #
Constructors
| WhetherPrevTimePasses Bool |
Instances
| Generic WhetherPrevTimePasses Source # | |||||
Defined in Test.Consensus.GSM.Model Associated Types
Methods from ∷ WhetherPrevTimePasses → Rep WhetherPrevTimePasses x # | |||||
| Show WhetherPrevTimePasses Source # | |||||
Defined in Test.Consensus.GSM.Model Methods showsPrec ∷ Int → WhetherPrevTimePasses → ShowS # show ∷ WhetherPrevTimePasses → String # showList ∷ [WhetherPrevTimePasses] → ShowS # | |||||
| Eq WhetherPrevTimePasses Source # | |||||
Defined in Test.Consensus.GSM.Model Methods (==) ∷ WhetherPrevTimePasses → WhetherPrevTimePasses → Bool # (/=) ∷ WhetherPrevTimePasses → WhetherPrevTimePasses → Bool # | |||||
| Ord WhetherPrevTimePasses Source # | |||||
Defined in Test.Consensus.GSM.Model Methods compare ∷ WhetherPrevTimePasses → WhetherPrevTimePasses → Ordering # (<) ∷ WhetherPrevTimePasses → WhetherPrevTimePasses → Bool # (<=) ∷ WhetherPrevTimePasses → WhetherPrevTimePasses → Bool # (>) ∷ WhetherPrevTimePasses → WhetherPrevTimePasses → Bool # (>=) ∷ WhetherPrevTimePasses → WhetherPrevTimePasses → Bool # max ∷ WhetherPrevTimePasses → WhetherPrevTimePasses → WhetherPrevTimePasses # min ∷ WhetherPrevTimePasses → WhetherPrevTimePasses → WhetherPrevTimePasses # | |||||
| ToExpr WhetherPrevTimePasses Source # | |||||
Defined in Test.Consensus.GSM.Model Methods | |||||
| type Rep WhetherPrevTimePasses Source # | |||||
Defined in Test.Consensus.GSM.Model type Rep WhetherPrevTimePasses = D1 ('MetaData "WhetherPrevTimePasses" "Test.Consensus.GSM.Model" "ouroboros-consensus-diffusion-0.23.0.0-inplace-consensus-test" 'True) (C1 ('MetaCons "WhetherPrevTimePasses" 'PrefixI 'False) (S1 ('MetaSel ('Nothing ∷ Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool))) | |||||
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)
Instances
| Generic Selection Source # | |||||
Defined in Test.Consensus.GSM.Model Associated Types
| |||||
| Show Selection Source # | |||||
| Eq Selection Source # | |||||
| Ord Selection Source # | |||||
Defined in Test.Consensus.GSM.Model | |||||
| ToExpr Selection Source # | |||||
| type Rep Selection Source # | |||||
Defined in Test.Consensus.GSM.Model type Rep Selection = D1 ('MetaData "Selection" "Test.Consensus.GSM.Model" "ouroboros-consensus-diffusion-0.23.0.0-inplace-consensus-test" 'False) (C1 ('MetaCons "Selection" 'PrefixI 'False) (S1 ('MetaSel ('Nothing ∷ Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 B) :*: S1 ('MetaSel ('Nothing ∷ Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 S))) | |||||
data ModelState Source #
Constructors
| ModelPreSyncing | |
| ModelSyncing | |
| ModelCaughtUp !Time | when the model most recently transitioned to |
Instances
| Generic ModelState Source # | |||||
Defined in Test.Consensus.GSM.Model Associated Types
| |||||
| Show ModelState Source # | |||||
Defined in Test.Consensus.GSM.Model Methods showsPrec ∷ Int → ModelState → ShowS # show ∷ ModelState → String # showList ∷ [ModelState] → ShowS # | |||||
| Eq ModelState Source # | |||||
Defined in Test.Consensus.GSM.Model | |||||
| Ord ModelState Source # | |||||
Defined in Test.Consensus.GSM.Model Methods compare ∷ ModelState → ModelState → Ordering # (<) ∷ ModelState → ModelState → Bool # (<=) ∷ ModelState → ModelState → Bool # (>) ∷ ModelState → ModelState → Bool # (>=) ∷ ModelState → ModelState → Bool # max ∷ ModelState → ModelState → ModelState # min ∷ ModelState → ModelState → ModelState # | |||||
| ToExpr ModelState Source # | |||||
Defined in Test.Consensus.GSM.Model | |||||
| type Rep ModelState Source # | |||||
Defined in Test.Consensus.GSM.Model type Rep ModelState = D1 ('MetaData "ModelState" "Test.Consensus.GSM.Model" "ouroboros-consensus-diffusion-0.23.0.0-inplace-consensus-test" 'False) (C1 ('MetaCons "ModelPreSyncing" 'PrefixI 'False) (U1 ∷ Type → Type) :+: (C1 ('MetaCons "ModelSyncing" 'PrefixI 'False) (U1 ∷ Type → Type) :+: C1 ('MetaCons "ModelCaughtUp" 'PrefixI 'False) (S1 ('MetaSel ('Nothing ∷ Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Time)))) | |||||
boringDur ∷ ∀ (r ∷ Type → Type). Model r → Int → Logic Source #
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.
thrashLimit ∷ Num a ⇒ a Source #