Safe Haskell	None
Language	Haskell2010

Test.Ouroboros.Storage.LedgerDB.V1.BackingStore.Lockstep

Synopsis

data BackingStoreState ks k vs d = BackingStoreState {
- bssMock ∷ Mock vs
- bssStats ∷ Stats ks k vs d
}
data RealEnv (m ∷ Type → Type) ks k vs d = RealEnv {
- reBackingStoreInit ∷ BackingStoreInitializer m ks k vs d
- reBackingStore ∷ StrictMVar m (BackingStore m ks k vs d)
}
type RealMonad (m ∷ Type → Type) ks k vs d = ReaderT (RealEnv m ks k vs d) m
maxOpenValueHandles ∷ Int

Documentation

data BackingStoreState ks k vs d Source #

Constructors

BackingStoreState
Fields bssMock ∷ Mock vs bssStats ∷ Stats ks k vs d

Instances

Instances details

InterpretOp Op (ModelValue (BackingStoreState ks k vs d) ∷ Type → Type) Source #

Instance details

Defined in Test.Ouroboros.Storage.LedgerDB.V1.BackingStore.Lockstep

Methods

intOp ∷ Op a b → ModelValue (BackingStoreState ks k vs d) a → Maybe (ModelValue (BackingStoreState ks k vs d) b) Source #

(Show ks, Show vs, Show k, Show d, Show (InitHint vs), Show (WriteHint d), Show (ReadHint vs), Eq ks, Eq k, Eq vs, Eq d, Eq (InitHint vs), Eq (WriteHint d), Eq (ReadHint vs), Typeable ks, Typeable k, Typeable vs, Typeable d, Typeable (WriteHint d), Arbitrary ks, Arbitrary k, Arbitrary vs, Arbitrary d, Arbitrary (RangeQuery ks), HasOps ks k vs d) ⇒ StateModel (Lockstep (BackingStoreState ks k vs d)) Source #

Instance details

Defined in Test.Ouroboros.Storage.LedgerDB.V1.BackingStore.Lockstep

Methods

actionName ∷ Action (Lockstep (BackingStoreState ks k vs d)) a → String Source #

arbitraryAction ∷ VarContext → Lockstep (BackingStoreState ks k vs d) → Gen (Any (Action (Lockstep (BackingStoreState ks k vs d)))) Source #

shrinkAction ∷ Typeable a ⇒ VarContext → Lockstep (BackingStoreState ks k vs d) → Action (Lockstep (BackingStoreState ks k vs d)) a → [Any (Action (Lockstep (BackingStoreState ks k vs d)))] Source #

initialState ∷ Lockstep (BackingStoreState ks k vs d) Source #

nextState ∷ Typeable a ⇒ Lockstep (BackingStoreState ks k vs d) → Action (Lockstep (BackingStoreState ks k vs d)) a → Var a → Lockstep (BackingStoreState ks k vs d) Source #

failureNextState ∷ Typeable a ⇒ Lockstep (BackingStoreState ks k vs d) → Action (Lockstep (BackingStoreState ks k vs d)) a → Lockstep (BackingStoreState ks k vs d) Source #

precondition ∷ Lockstep (BackingStoreState ks k vs d) → Action (Lockstep (BackingStoreState ks k vs d)) a → Bool Source #

validFailingAction ∷ Lockstep (BackingStoreState ks k vs d) → Action (Lockstep (BackingStoreState ks k vs d)) a → Bool Source #

(Show ks, Show vs, Show k, Show d, Show (InitHint vs), Show (WriteHint d), Show (ReadHint vs), Eq ks, Eq vs, Eq k, Eq d, Eq (InitHint vs), Eq (WriteHint d), Eq (ReadHint vs), Typeable ks, Typeable k, Typeable vs, Typeable d, Typeable (WriteHint d), Arbitrary ks, Arbitrary k, Arbitrary vs, Arbitrary d, Arbitrary (RangeQuery ks), HasOps ks k vs d) ⇒ RunModel (Lockstep (BackingStoreState ks k vs d)) (RealMonad IO ks k vs d) Source #

Instance details

Defined in Test.Ouroboros.Storage.LedgerDB.V1.BackingStore.Lockstep

Associated Types

type Error (Lockstep (BackingStoreState ks k vs d)) (RealMonad IO ks k vs d)
Instance details Defined in Test.Ouroboros.Storage.LedgerDB.V1.BackingStore.Lockstep type Error (Lockstep (BackingStoreState ks k vs d)) (RealMonad IO ks k vs d) = Void

Methods

perform ∷ Typeable a ⇒ Lockstep (BackingStoreState ks k vs d) → Action (Lockstep (BackingStoreState ks k vs d)) a → LookUp → RealMonad IO ks k vs d (PerformResult (Lockstep (BackingStoreState ks k vs d)) (RealMonad IO ks k vs d) a) Source #

postcondition ∷ (Lockstep (BackingStoreState ks k vs d), Lockstep (BackingStoreState ks k vs d)) → Action (Lockstep (BackingStoreState ks k vs d)) a → LookUp → a → PostconditionM (RealMonad IO ks k vs d) Bool Source #

postconditionOnFailure ∷ (Lockstep (BackingStoreState ks k vs d), Lockstep (BackingStoreState ks k vs d)) → Action (Lockstep (BackingStoreState ks k vs d)) a → LookUp → Either (Error (Lockstep (BackingStoreState ks k vs d)) (RealMonad IO ks k vs d)) a → PostconditionM (RealMonad IO ks k vs d) Bool Source #

monitoring ∷ (Lockstep (BackingStoreState ks k vs d), Lockstep (BackingStoreState ks k vs d)) → Action (Lockstep (BackingStoreState ks k vs d)) a → LookUp → Either (Error (Lockstep (BackingStoreState ks k vs d)) (RealMonad IO ks k vs d)) a → Property → Property Source #

monitoringFailure ∷ Lockstep (BackingStoreState ks k vs d) → Action (Lockstep (BackingStoreState ks k vs d)) a → LookUp → Error (Lockstep (BackingStoreState ks k vs d)) (RealMonad IO ks k vs d) → Property → Property Source #

(Show ks, Show vs, Show d, Show (InitHint vs), Show (WriteHint d), Show (ReadHint vs), Show (SerializeTablesHint vs)) ⇒ Show (LockstepAction (BackingStoreState ks k vs d) a) Source #

Instance details

Defined in Test.Ouroboros.Storage.LedgerDB.V1.BackingStore.Lockstep

Methods

showsPrec ∷ Int → LockstepAction (BackingStoreState ks k vs d) a → ShowS #

show ∷ LockstepAction (BackingStoreState ks k vs d) a → String #

showList ∷ [LockstepAction (BackingStoreState ks k vs d) a] → ShowS #

(Eq ks, Eq vs, Eq d, Eq (InitHint vs), Eq (WriteHint d), Eq (ReadHint vs), Eq (SerializeTablesHint vs)) ⇒ Eq (LockstepAction (BackingStoreState ks k vs d) a) Source #

Instance details

Defined in Test.Ouroboros.Storage.LedgerDB.V1.BackingStore.Lockstep

Methods

(==) ∷ LockstepAction (BackingStoreState ks k vs d) a → LockstepAction (BackingStoreState ks k vs d) a → Bool #

(/=) ∷ LockstepAction (BackingStoreState ks k vs d) a → LockstepAction (BackingStoreState ks k vs d) a → Bool #

Show vs ⇒ Show (BackingStoreState ks k vs d) Source #

Instance details

Defined in Test.Ouroboros.Storage.LedgerDB.V1.BackingStore.Lockstep

Methods

showsPrec ∷ Int → BackingStoreState ks k vs d → ShowS #

show ∷ BackingStoreState ks k vs d → String #

showList ∷ [BackingStoreState ks k vs d] → ShowS #

Eq vs ⇒ Eq (BackingStoreState ks k vs d) Source #

Instance details

Defined in Test.Ouroboros.Storage.LedgerDB.V1.BackingStore.Lockstep

Methods

(==) ∷ BackingStoreState ks k vs d → BackingStoreState ks k vs d → Bool #

(/=) ∷ BackingStoreState ks k vs d → BackingStoreState ks k vs d → Bool #

(Show ks, Show vs, Show d, Show k, Show (InitHint vs), Show (WriteHint d), Show (ReadHint vs), Eq ks, Eq vs, Eq k, Eq d, Eq (InitHint vs), Eq (WriteHint d), Eq (ReadHint vs), Typeable ks, Typeable k, Typeable vs, Typeable d, Typeable (WriteHint d), Arbitrary ks, Arbitrary k, Arbitrary vs, Arbitrary d, Arbitrary (RangeQuery ks), HasOps ks k vs d) ⇒ InLockstep (BackingStoreState ks k vs d) Source #

Instance details

Defined in Test.Ouroboros.Storage.LedgerDB.V1.BackingStore.Lockstep

Associated Types

type ModelOp (BackingStoreState ks k vs d)
Instance details Defined in Test.Ouroboros.Storage.LedgerDB.V1.BackingStore.Lockstep type ModelOp (BackingStoreState ks k vs d) = Op

Methods

observeModel ∷ ModelValue (BackingStoreState ks k vs d) a → Observable (BackingStoreState ks k vs d) a Source #

usedVars ∷ LockstepAction (BackingStoreState ks k vs d) a → [AnyGVar (ModelOp (BackingStoreState ks k vs d))] Source #

modelNextState ∷ LockstepAction (BackingStoreState ks k vs d) a → ModelVarContext (BackingStoreState ks k vs d) → BackingStoreState ks k vs d → (ModelValue (BackingStoreState ks k vs d) a, BackingStoreState ks k vs d) Source #

arbitraryWithVars ∷ ModelVarContext (BackingStoreState ks k vs d) → BackingStoreState ks k vs d → Gen (Any (LockstepAction (BackingStoreState ks k vs d))) Source #

shrinkWithVars ∷ ModelVarContext (BackingStoreState ks k vs d) → BackingStoreState ks k vs d → LockstepAction (BackingStoreState ks k vs d) a → [Any (LockstepAction (BackingStoreState ks k vs d))] Source #

tagStep ∷ (BackingStoreState ks k vs d, BackingStoreState ks k vs d) → LockstepAction (BackingStoreState ks k vs d) a → ModelValue (BackingStoreState ks k vs d) a → [String] Source #

(Show ks, Show vs, Show k, Show d, Show (InitHint vs), Show (WriteHint d), Show (ReadHint vs), Eq ks, Eq vs, Eq k, Eq d, Eq (InitHint vs), Eq (WriteHint d), Eq (ReadHint vs), Typeable ks, Typeable vs, Typeable k, Typeable d, Typeable (WriteHint d), Arbitrary ks, Arbitrary vs, Arbitrary k, Arbitrary d, Arbitrary (RangeQuery ks), HasOps ks k vs d) ⇒ RunLockstep (BackingStoreState ks k vs d) (RealMonad IO ks k vs d) Source #

Instance details

Defined in Test.Ouroboros.Storage.LedgerDB.V1.BackingStore.Lockstep

Methods

observeReal ∷ Proxy (RealMonad IO ks k vs d) → LockstepAction (BackingStoreState ks k vs d) a → a → Observable (BackingStoreState ks k vs d) a Source #

showRealResponse ∷ Proxy (RealMonad IO ks k vs d) → LockstepAction (BackingStoreState ks k vs d) a → Maybe (Dict (Show a)) Source #

data Action (Lockstep (BackingStoreState ks k vs d)) a Source #

Instance details

Defined in Test.Ouroboros.Storage.LedgerDB.V1.BackingStore.Lockstep

data Action (Lockstep (BackingStoreState ks k vs d)) a where

BSInitFromValues ∷ ∀ vs ks k d. WithOrigin SlotNo → InitHint vs → Values vs → Action (Lockstep (BackingStoreState ks k vs d)) (Either Err ())
BSInitFromCopy ∷ ∀ vs ks k d. InitHint vs → FsPath → Action (Lockstep (BackingStoreState ks k vs d)) (Either Err ())
BSClose ∷ ∀ ks k vs d. Action (Lockstep (BackingStoreState ks k vs d)) (Either Err ())
BSCopy ∷ ∀ vs ks k d. SerializeTablesHint vs → FsPath → Action (Lockstep (BackingStoreState ks k vs d)) (Either Err ())
BSValueHandle ∷ ∀ ks k vs d. Action (Lockstep (BackingStoreState ks k vs d)) (Either Err (BackingStoreValueHandle IO ks k vs))
BSWrite ∷ ∀ d ks k vs. SlotNo → WriteHint d → d → Action (Lockstep (BackingStoreState ks k vs d)) (Either Err ())
BSVHClose ∷ ∀ ks k vs d. BSVar ks k vs d (BackingStoreValueHandle IO ks k vs) → Action (Lockstep (BackingStoreState ks k vs d)) (Either Err ())
BSVHRangeRead ∷ ∀ ks k vs d. BSVar ks k vs d (BackingStoreValueHandle IO ks k vs) → ReadHint vs → RangeQuery ks → Action (Lockstep (BackingStoreState ks k vs d)) (Either Err (Values vs, Maybe k))
BSVHRead ∷ ∀ ks k vs d. BSVar ks k vs d (BackingStoreValueHandle IO ks k vs) → ReadHint vs → ks → Action (Lockstep (BackingStoreState ks k vs d)) (Either Err (Values vs))
BSVHAtSlot ∷ ∀ ks k vs d. BSVar ks k vs d (BackingStoreValueHandle IO ks k vs) → Action (Lockstep (BackingStoreState ks k vs d)) (Either Err (WithOrigin SlotNo))
BSVHStat ∷ ∀ ks k vs d. BSVar ks k vs d (BackingStoreValueHandle IO ks k vs) → Action (Lockstep (BackingStoreState ks k vs d)) (Either Err Statistics)

type Error (Lockstep (BackingStoreState ks k vs d)) (RealMonad IO ks k vs d) Source #

Instance details

Defined in Test.Ouroboros.Storage.LedgerDB.V1.BackingStore.Lockstep

type Error (Lockstep (BackingStoreState ks k vs d)) (RealMonad IO ks k vs d) = Void

type ModelOp (BackingStoreState ks k vs d) Source #

Instance details

Defined in Test.Ouroboros.Storage.LedgerDB.V1.BackingStore.Lockstep

type ModelOp (BackingStoreState ks k vs d) = Op

data ModelValue (BackingStoreState ks k vs d) a Source #

Instance details

Defined in Test.Ouroboros.Storage.LedgerDB.V1.BackingStore.Lockstep

data ModelValue (BackingStoreState ks k vs d) a where

MValueHandle ∷ ∀ vs ks k d. ValueHandle vs → ModelValue (BackingStoreState ks k vs d) (BackingStoreValueHandle IO ks k vs)
MErr ∷ ∀ ks k vs d. Err → ModelValue (BackingStoreState ks k vs d) Err
MSlotNo ∷ ∀ ks k vs d. WithOrigin SlotNo → ModelValue (BackingStoreState ks k vs d) (WithOrigin SlotNo)
MValues ∷ ∀ vs ks k d. vs → ModelValue (BackingStoreState ks k vs d) (Values vs)
MValuesAndLast ∷ ∀ vs k ks d. (vs, Maybe k) → ModelValue (BackingStoreState ks k vs d) (Values vs, Maybe k)
MUnit ∷ ∀ ks k vs d. () → ModelValue (BackingStoreState ks k vs d) ()
MStatistics ∷ ∀ ks k vs d. Statistics → ModelValue (BackingStoreState ks k vs d) Statistics
MEither ∷ ∀ ks k vs d a1 b. Either (BSVal ks k vs d a1) (BSVal ks k vs d b) → ModelValue (BackingStoreState ks k vs d) (Either a1 b)
MPair ∷ ∀ ks k vs d a1 b. (BSVal ks k vs d a1, BSVal ks k vs d b) → ModelValue (BackingStoreState ks k vs d) (a1, b)

data Observable (BackingStoreState ks k vs d) a Source #

Instance details

Defined in Test.Ouroboros.Storage.LedgerDB.V1.BackingStore.Lockstep

data Observable (BackingStoreState ks k vs d) a where

OValueHandle ∷ ∀ ks k vs d. Observable (BackingStoreState ks k vs d) (BackingStoreValueHandle IO ks k vs)
OValues ∷ ∀ a1 ks k vs d. (Show a1, Eq a1, Typeable a1) ⇒ a1 → Observable (BackingStoreState ks k vs d) (Values a1)
OValuesAndLast ∷ ∀ a1 k ks vs d. (Show a1, Eq a1, Typeable a1) ⇒ (a1, Maybe k) → Observable (BackingStoreState ks k vs d) (Values a1, Maybe k)
OId ∷ ∀ a ks k vs d. (Show a, Eq a, Typeable a) ⇒ a → Observable (BackingStoreState ks k vs d) a
OEither ∷ ∀ ks k vs d a1 b. Either (BSObs ks k vs d a1) (BSObs ks k vs d b) → Observable (BackingStoreState ks k vs d) (Either a1 b)
OPair ∷ ∀ ks k vs d a1 b. (BSObs ks k vs d a1, BSObs ks k vs d b) → Observable (BackingStoreState ks k vs d) (a1, b)

data RealEnv (m ∷ Type → Type) ks k vs d Source #

Constructors

RealEnv
Fields reBackingStoreInit ∷ BackingStoreInitializer m ks k vs d reBackingStore ∷ StrictMVar m (BackingStore m ks k vs d)

Instances

Instances details

(Show ks, Show vs, Show k, Show d, Show (InitHint vs), Show (WriteHint d), Show (ReadHint vs), Eq ks, Eq vs, Eq k, Eq d, Eq (InitHint vs), Eq (WriteHint d), Eq (ReadHint vs), Typeable ks, Typeable k, Typeable vs, Typeable d, Typeable (WriteHint d), Arbitrary ks, Arbitrary k, Arbitrary vs, Arbitrary d, Arbitrary (RangeQuery ks), HasOps ks k vs d) ⇒ RunModel (Lockstep (BackingStoreState ks k vs d)) (RealMonad IO ks k vs d) Source #

Instance details

Defined in Test.Ouroboros.Storage.LedgerDB.V1.BackingStore.Lockstep

Associated Types

type Error (Lockstep (BackingStoreState ks k vs d)) (RealMonad IO ks k vs d)
Instance details Defined in Test.Ouroboros.Storage.LedgerDB.V1.BackingStore.Lockstep type Error (Lockstep (BackingStoreState ks k vs d)) (RealMonad IO ks k vs d) = Void

Methods

perform ∷ Typeable a ⇒ Lockstep (BackingStoreState ks k vs d) → Action (Lockstep (BackingStoreState ks k vs d)) a → LookUp → RealMonad IO ks k vs d (PerformResult (Lockstep (BackingStoreState ks k vs d)) (RealMonad IO ks k vs d) a) Source #

postcondition ∷ (Lockstep (BackingStoreState ks k vs d), Lockstep (BackingStoreState ks k vs d)) → Action (Lockstep (BackingStoreState ks k vs d)) a → LookUp → a → PostconditionM (RealMonad IO ks k vs d) Bool Source #

postconditionOnFailure ∷ (Lockstep (BackingStoreState ks k vs d), Lockstep (BackingStoreState ks k vs d)) → Action (Lockstep (BackingStoreState ks k vs d)) a → LookUp → Either (Error (Lockstep (BackingStoreState ks k vs d)) (RealMonad IO ks k vs d)) a → PostconditionM (RealMonad IO ks k vs d) Bool Source #

monitoring ∷ (Lockstep (BackingStoreState ks k vs d), Lockstep (BackingStoreState ks k vs d)) → Action (Lockstep (BackingStoreState ks k vs d)) a → LookUp → Either (Error (Lockstep (BackingStoreState ks k vs d)) (RealMonad IO ks k vs d)) a → Property → Property Source #

monitoringFailure ∷ Lockstep (BackingStoreState ks k vs d) → Action (Lockstep (BackingStoreState ks k vs d)) a → LookUp → Error (Lockstep (BackingStoreState ks k vs d)) (RealMonad IO ks k vs d) → Property → Property Source #

(Show ks, Show vs, Show k, Show d, Show (InitHint vs), Show (WriteHint d), Show (ReadHint vs), Eq ks, Eq vs, Eq k, Eq d, Eq (InitHint vs), Eq (WriteHint d), Eq (ReadHint vs), Typeable ks, Typeable vs, Typeable k, Typeable d, Typeable (WriteHint d), Arbitrary ks, Arbitrary vs, Arbitrary k, Arbitrary d, Arbitrary (RangeQuery ks), HasOps ks k vs d) ⇒ RunLockstep (BackingStoreState ks k vs d) (RealMonad IO ks k vs d) Source #

Instance details

Defined in Test.Ouroboros.Storage.LedgerDB.V1.BackingStore.Lockstep

Methods

observeReal ∷ Proxy (RealMonad IO ks k vs d) → LockstepAction (BackingStoreState ks k vs d) a → a → Observable (BackingStoreState ks k vs d) a Source #

showRealResponse ∷ Proxy (RealMonad IO ks k vs d) → LockstepAction (BackingStoreState ks k vs d) a → Maybe (Dict (Show a)) Source #

type Error (Lockstep (BackingStoreState ks k vs d)) (RealMonad IO ks k vs d) Source #

Instance details

Defined in Test.Ouroboros.Storage.LedgerDB.V1.BackingStore.Lockstep

type Error (Lockstep (BackingStoreState ks k vs d)) (RealMonad IO ks k vs d) = Void

type RealMonad (m ∷ Type → Type) ks k vs d = ReaderT (RealEnv m ks k vs d) m Source #

maxOpenValueHandles ∷ Int Source #

Maximum number of LMDB readers that can be active at a time.

32 is an arbitrary number of readers. We can increase or decrease this at will.