| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Test.Consensus.GSM.Model
Contents
Description
The definition of the GSM QSM model and its auxiliaries
Synopsis
- newtype B = B Int
- newtype S = S Int
- data Context = Context {}
- data Model r = Model {}
- data Response r
- data Command r
- data UpstreamPeer
- data MarkerState
- newtype Candidate = Candidate B
- data Notable
- newtype WhetherPrevTimePasses = WhetherPrevTimePasses Bool
- data Selection = Selection !B !S
- data ModelState
- candidateOverSelection ∷ Selection → Candidate → CandidateVersusSelection
- initModel ∷ Context → Model r
- transition ∷ Context → Model r → Command r → Response r → Model r
- precondition ∷ Context → Model Symbolic → Command Symbolic → Logic
- postcondition ∷ Model Concrete → Command Concrete → Response Concrete → Logic
- generator ∷ Maybe UpstreamPeer → Model Symbolic → Maybe (Gen (Command Symbolic))
- shrinker ∷ Model Symbolic → Command Symbolic → [Command Symbolic]
- mock ∷ Model r → Command r → Response r
- addNotableWhen ∷ Notable → Bool → Model r → Model r
- atom ∷ String → Bool → Logic
- selectionIsBehind ∷ Model r → Bool
- selectionIsNotEarly ∷ Model r → Bool
- boringDur ∷ Model r → Int → Logic
- fixupModelState ∷ 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
A block count
A slot count
Constructors
| Context | |
Constructors
| Model | |
Fields | |
Instances
Constructors
| ReadThisGsmState GsmState | |
| ReadThisMarker MarkerState | |
| Unit |
Instances
| Foldable Response Source # | |
| Functor Response Source # | |
| Traversable Response Source # | |
Defined in Test.Consensus.GSM.Model | |
| Read (Response r) Source # | |
| Show (Response r) Source # | |
| Generic1 Response Source # | |
| type Rep1 Response Source # | |
Defined in Test.Consensus.GSM.Model type Rep1 Response = D1 ('MetaData "Response" "Test.Consensus.GSM.Model" "main" 'False) (C1 ('MetaCons "ReadThisGsmState" 'PrefixI 'False) (S1 ('MetaSel ('Nothing ∷ Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 GsmState)) :+: (C1 ('MetaCons "ReadThisMarker" 'PrefixI 'False) (S1 ('MetaSel ('Nothing ∷ Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 MarkerState)) :+: C1 ('MetaCons "Unit" 'PrefixI 'False) (U1 ∷ (Type → Type) → Type))) | |
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
data UpstreamPeer Source #
Instances
data MarkerState Source #
Instances
The age of the candidate is irrelevant, only its length matters
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
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 # | |
| 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" "main" '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
selectionIsBehind ∷ Model r → Bool Source #
selectionIsNotEarly ∷ Model r → Bool Source #
boringDur ∷ 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 #