{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
module Test.Ouroboros.Storage.VolatileDB.StateMachine (
showLabelledExamples
, tests
) where
import Control.Concurrent.Class.MonadSTM.Strict (newTMVar)
import Control.Monad (forM_, void)
import Data.Bifunctor (first)
import Data.ByteString.Lazy (ByteString)
import Data.Functor.Classes
import Data.Functor.Identity (Identity)
import Data.Kind (Type)
import qualified Data.List.NonEmpty as NE
import qualified Data.Map.Strict as Map
import Data.Maybe (catMaybes, listToMaybe, mapMaybe)
import Data.Set (Set)
import qualified Data.Set as Set
import Data.TreeDiff
import Data.Word
import qualified Generics.SOP as SOP
import GHC.Generics
import GHC.Stack
import Ouroboros.Consensus.Block
import Ouroboros.Consensus.Storage.Common
import Ouroboros.Consensus.Storage.VolatileDB
import Ouroboros.Consensus.Storage.VolatileDB.Impl.Types (FileId)
import Ouroboros.Consensus.Storage.VolatileDB.Impl.Util
import Ouroboros.Consensus.Util.IOLike
import Ouroboros.Consensus.Util.ResourceRegistry
import Ouroboros.Network.Block (MaxSlotNo)
import Prelude hiding (elem)
import System.FS.API.Lazy
import System.FS.Sim.Error
import qualified System.FS.Sim.MockFS as Mock
import System.Random (getStdRandom, randomR)
import Test.Ouroboros.Storage.Orphans ()
import Test.Ouroboros.Storage.TestBlock
import Test.Ouroboros.Storage.VolatileDB.Model
import Test.QuickCheck hiding (elements, forAll)
import Test.QuickCheck.Monadic
import Test.QuickCheck.Random (mkQCGen)
import Test.StateMachine hiding (showLabelledExamples,
showLabelledExamples')
import qualified Test.StateMachine.Labelling as C
import qualified Test.StateMachine.Sequential as QSM
import Test.StateMachine.Types
import qualified Test.StateMachine.Types.Rank2 as Rank2
import Test.Tasty (TestTree, testGroup)
import Test.Tasty.QuickCheck (testProperty)
import Test.Util.Orphans.Arbitrary ()
import Test.Util.Orphans.ToExpr ()
import Test.Util.QuickCheck
import Test.Util.SOP
import Test.Util.ToExpr ()
import Test.Util.Tracer (recordingTracerIORef)
import Text.Show.Pretty (ppShow)
type Block = TestBlock
newtype At t (r :: Type -> Type) = At {forall t (r :: * -> *). At t r -> t
unAt :: t}
deriving ((forall x. At t r -> Rep (At t r) x)
-> (forall x. Rep (At t r) x -> At t r) -> Generic (At t r)
forall x. Rep (At t r) x -> At t r
forall x. At t r -> Rep (At t r) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall t (r :: * -> *) x. Rep (At t r) x -> At t r
forall t (r :: * -> *) x. At t r -> Rep (At t r) x
$cfrom :: forall t (r :: * -> *) x. At t r -> Rep (At t r) x
from :: forall x. At t r -> Rep (At t r) x
$cto :: forall t (r :: * -> *) x. Rep (At t r) x -> At t r
to :: forall x. Rep (At t r) x -> At t r
Generic)
type (:@) t r = At t r
allComponents :: BlockComponent blk (AllComponents blk)
allComponents :: forall blk. BlockComponent blk (AllComponents blk)
allComponents = (,,,,,,,,,,)
(blk
-> blk
-> ByteString
-> Header blk
-> ByteString
-> HeaderHash blk
-> SlotNo
-> IsEBB
-> SizeInBytes
-> Word16
-> SomeSecond (NestedCtxt Header) blk
-> (blk, blk, ByteString, Header blk, ByteString, HeaderHash blk,
SlotNo, IsEBB, SizeInBytes, Word16,
SomeSecond (NestedCtxt Header) blk))
-> BlockComponent blk blk
-> BlockComponent
blk
(blk
-> ByteString
-> Header blk
-> ByteString
-> HeaderHash blk
-> SlotNo
-> IsEBB
-> SizeInBytes
-> Word16
-> SomeSecond (NestedCtxt Header) blk
-> (blk, blk, ByteString, Header blk, ByteString, HeaderHash blk,
SlotNo, IsEBB, SizeInBytes, Word16,
SomeSecond (NestedCtxt Header) blk))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BlockComponent blk blk
forall blk. BlockComponent blk blk
GetVerifiedBlock
BlockComponent
blk
(blk
-> ByteString
-> Header blk
-> ByteString
-> HeaderHash blk
-> SlotNo
-> IsEBB
-> SizeInBytes
-> Word16
-> SomeSecond (NestedCtxt Header) blk
-> (blk, blk, ByteString, Header blk, ByteString, HeaderHash blk,
SlotNo, IsEBB, SizeInBytes, Word16,
SomeSecond (NestedCtxt Header) blk))
-> BlockComponent blk blk
-> BlockComponent
blk
(ByteString
-> Header blk
-> ByteString
-> HeaderHash blk
-> SlotNo
-> IsEBB
-> SizeInBytes
-> Word16
-> SomeSecond (NestedCtxt Header) blk
-> (blk, blk, ByteString, Header blk, ByteString, HeaderHash blk,
SlotNo, IsEBB, SizeInBytes, Word16,
SomeSecond (NestedCtxt Header) blk))
forall a b.
BlockComponent blk (a -> b)
-> BlockComponent blk a -> BlockComponent blk b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> BlockComponent blk blk
forall blk. BlockComponent blk blk
GetBlock
BlockComponent
blk
(ByteString
-> Header blk
-> ByteString
-> HeaderHash blk
-> SlotNo
-> IsEBB
-> SizeInBytes
-> Word16
-> SomeSecond (NestedCtxt Header) blk
-> (blk, blk, ByteString, Header blk, ByteString, HeaderHash blk,
SlotNo, IsEBB, SizeInBytes, Word16,
SomeSecond (NestedCtxt Header) blk))
-> BlockComponent blk ByteString
-> BlockComponent
blk
(Header blk
-> ByteString
-> HeaderHash blk
-> SlotNo
-> IsEBB
-> SizeInBytes
-> Word16
-> SomeSecond (NestedCtxt Header) blk
-> (blk, blk, ByteString, Header blk, ByteString, HeaderHash blk,
SlotNo, IsEBB, SizeInBytes, Word16,
SomeSecond (NestedCtxt Header) blk))
forall a b.
BlockComponent blk (a -> b)
-> BlockComponent blk a -> BlockComponent blk b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> BlockComponent blk ByteString
forall blk. BlockComponent blk ByteString
GetRawBlock
BlockComponent
blk
(Header blk
-> ByteString
-> HeaderHash blk
-> SlotNo
-> IsEBB
-> SizeInBytes
-> Word16
-> SomeSecond (NestedCtxt Header) blk
-> (blk, blk, ByteString, Header blk, ByteString, HeaderHash blk,
SlotNo, IsEBB, SizeInBytes, Word16,
SomeSecond (NestedCtxt Header) blk))
-> BlockComponent blk (Header blk)
-> BlockComponent
blk
(ByteString
-> HeaderHash blk
-> SlotNo
-> IsEBB
-> SizeInBytes
-> Word16
-> SomeSecond (NestedCtxt Header) blk
-> (blk, blk, ByteString, Header blk, ByteString, HeaderHash blk,
SlotNo, IsEBB, SizeInBytes, Word16,
SomeSecond (NestedCtxt Header) blk))
forall a b.
BlockComponent blk (a -> b)
-> BlockComponent blk a -> BlockComponent blk b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> BlockComponent blk (Header blk)
forall blk. BlockComponent blk (Header blk)
GetHeader
BlockComponent
blk
(ByteString
-> HeaderHash blk
-> SlotNo
-> IsEBB
-> SizeInBytes
-> Word16
-> SomeSecond (NestedCtxt Header) blk
-> (blk, blk, ByteString, Header blk, ByteString, HeaderHash blk,
SlotNo, IsEBB, SizeInBytes, Word16,
SomeSecond (NestedCtxt Header) blk))
-> BlockComponent blk ByteString
-> BlockComponent
blk
(HeaderHash blk
-> SlotNo
-> IsEBB
-> SizeInBytes
-> Word16
-> SomeSecond (NestedCtxt Header) blk
-> (blk, blk, ByteString, Header blk, ByteString, HeaderHash blk,
SlotNo, IsEBB, SizeInBytes, Word16,
SomeSecond (NestedCtxt Header) blk))
forall a b.
BlockComponent blk (a -> b)
-> BlockComponent blk a -> BlockComponent blk b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> BlockComponent blk ByteString
forall blk. BlockComponent blk ByteString
GetRawHeader
BlockComponent
blk
(HeaderHash blk
-> SlotNo
-> IsEBB
-> SizeInBytes
-> Word16
-> SomeSecond (NestedCtxt Header) blk
-> (blk, blk, ByteString, Header blk, ByteString, HeaderHash blk,
SlotNo, IsEBB, SizeInBytes, Word16,
SomeSecond (NestedCtxt Header) blk))
-> BlockComponent blk (HeaderHash blk)
-> BlockComponent
blk
(SlotNo
-> IsEBB
-> SizeInBytes
-> Word16
-> SomeSecond (NestedCtxt Header) blk
-> (blk, blk, ByteString, Header blk, ByteString, HeaderHash blk,
SlotNo, IsEBB, SizeInBytes, Word16,
SomeSecond (NestedCtxt Header) blk))
forall a b.
BlockComponent blk (a -> b)
-> BlockComponent blk a -> BlockComponent blk b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> BlockComponent blk (HeaderHash blk)
forall blk. BlockComponent blk (HeaderHash blk)
GetHash
BlockComponent
blk
(SlotNo
-> IsEBB
-> SizeInBytes
-> Word16
-> SomeSecond (NestedCtxt Header) blk
-> (blk, blk, ByteString, Header blk, ByteString, HeaderHash blk,
SlotNo, IsEBB, SizeInBytes, Word16,
SomeSecond (NestedCtxt Header) blk))
-> BlockComponent blk SlotNo
-> BlockComponent
blk
(IsEBB
-> SizeInBytes
-> Word16
-> SomeSecond (NestedCtxt Header) blk
-> (blk, blk, ByteString, Header blk, ByteString, HeaderHash blk,
SlotNo, IsEBB, SizeInBytes, Word16,
SomeSecond (NestedCtxt Header) blk))
forall a b.
BlockComponent blk (a -> b)
-> BlockComponent blk a -> BlockComponent blk b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> BlockComponent blk SlotNo
forall blk. BlockComponent blk SlotNo
GetSlot
BlockComponent
blk
(IsEBB
-> SizeInBytes
-> Word16
-> SomeSecond (NestedCtxt Header) blk
-> (blk, blk, ByteString, Header blk, ByteString, HeaderHash blk,
SlotNo, IsEBB, SizeInBytes, Word16,
SomeSecond (NestedCtxt Header) blk))
-> BlockComponent blk IsEBB
-> BlockComponent
blk
(SizeInBytes
-> Word16
-> SomeSecond (NestedCtxt Header) blk
-> (blk, blk, ByteString, Header blk, ByteString, HeaderHash blk,
SlotNo, IsEBB, SizeInBytes, Word16,
SomeSecond (NestedCtxt Header) blk))
forall a b.
BlockComponent blk (a -> b)
-> BlockComponent blk a -> BlockComponent blk b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> BlockComponent blk IsEBB
forall blk. BlockComponent blk IsEBB
GetIsEBB
BlockComponent
blk
(SizeInBytes
-> Word16
-> SomeSecond (NestedCtxt Header) blk
-> (blk, blk, ByteString, Header blk, ByteString, HeaderHash blk,
SlotNo, IsEBB, SizeInBytes, Word16,
SomeSecond (NestedCtxt Header) blk))
-> BlockComponent blk SizeInBytes
-> BlockComponent
blk
(Word16
-> SomeSecond (NestedCtxt Header) blk
-> (blk, blk, ByteString, Header blk, ByteString, HeaderHash blk,
SlotNo, IsEBB, SizeInBytes, Word16,
SomeSecond (NestedCtxt Header) blk))
forall a b.
BlockComponent blk (a -> b)
-> BlockComponent blk a -> BlockComponent blk b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> BlockComponent blk SizeInBytes
forall blk. BlockComponent blk SizeInBytes
GetBlockSize
BlockComponent
blk
(Word16
-> SomeSecond (NestedCtxt Header) blk
-> (blk, blk, ByteString, Header blk, ByteString, HeaderHash blk,
SlotNo, IsEBB, SizeInBytes, Word16,
SomeSecond (NestedCtxt Header) blk))
-> BlockComponent blk Word16
-> BlockComponent
blk
(SomeSecond (NestedCtxt Header) blk
-> (blk, blk, ByteString, Header blk, ByteString, HeaderHash blk,
SlotNo, IsEBB, SizeInBytes, Word16,
SomeSecond (NestedCtxt Header) blk))
forall a b.
BlockComponent blk (a -> b)
-> BlockComponent blk a -> BlockComponent blk b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> BlockComponent blk Word16
forall blk. BlockComponent blk Word16
GetHeaderSize
BlockComponent
blk
(SomeSecond (NestedCtxt Header) blk
-> (blk, blk, ByteString, Header blk, ByteString, HeaderHash blk,
SlotNo, IsEBB, SizeInBytes, Word16,
SomeSecond (NestedCtxt Header) blk))
-> BlockComponent blk (SomeSecond (NestedCtxt Header) blk)
-> BlockComponent
blk
(blk, blk, ByteString, Header blk, ByteString, HeaderHash blk,
SlotNo, IsEBB, SizeInBytes, Word16,
SomeSecond (NestedCtxt Header) blk)
forall a b.
BlockComponent blk (a -> b)
-> BlockComponent blk a -> BlockComponent blk b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> BlockComponent blk (SomeSecond (NestedCtxt Header) blk)
forall blk. BlockComponent blk (SomeSecond (NestedCtxt Header) blk)
GetNestedCtxt
type AllComponents blk =
( blk
, blk
, ByteString
, Header blk
, ByteString
, HeaderHash blk
, SlotNo
, IsEBB
, SizeInBytes
, Word16
, SomeSecond (NestedCtxt Header) blk
)
data Cmd
= Close
| ReOpen
| GetBlockComponent (HeaderHash Block)
| PutBlock Block
| GarbageCollect SlotNo
| FilterByPredecessor [ChainHash Block]
| GetBlockInfo [HeaderHash Block]
| GetMaxSlotNo
| Corruption Corruptions
| DuplicateBlock FileId Block
deriving (Int -> Cmd -> ShowS
[Cmd] -> ShowS
Cmd -> String
(Int -> Cmd -> ShowS)
-> (Cmd -> String) -> ([Cmd] -> ShowS) -> Show Cmd
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Cmd -> ShowS
showsPrec :: Int -> Cmd -> ShowS
$cshow :: Cmd -> String
show :: Cmd -> String
$cshowList :: [Cmd] -> ShowS
showList :: [Cmd] -> ShowS
Show, (forall x. Cmd -> Rep Cmd x)
-> (forall x. Rep Cmd x -> Cmd) -> Generic Cmd
forall x. Rep Cmd x -> Cmd
forall x. Cmd -> Rep Cmd x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Cmd -> Rep Cmd x
from :: forall x. Cmd -> Rep Cmd x
$cto :: forall x. Rep Cmd x -> Cmd
to :: forall x. Rep Cmd x -> Cmd
Generic)
data CmdErr = CmdErr {
CmdErr -> Cmd
cmd :: Cmd
, CmdErr -> Maybe Errors
err :: Maybe Errors
} deriving Int -> CmdErr -> ShowS
[CmdErr] -> ShowS
CmdErr -> String
(Int -> CmdErr -> ShowS)
-> (CmdErr -> String) -> ([CmdErr] -> ShowS) -> Show CmdErr
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> CmdErr -> ShowS
showsPrec :: Int -> CmdErr -> ShowS
$cshow :: CmdErr -> String
show :: CmdErr -> String
$cshowList :: [CmdErr] -> ShowS
showList :: [CmdErr] -> ShowS
Show
data Success
= Unit ()
| MbAllComponents (Maybe (AllComponents Block))
| Bool Bool
| Successors [Set (HeaderHash Block)]
| BlockInfos [Maybe (BlockInfo Block)]
| MaxSlot MaxSlotNo
deriving (Int -> Success -> ShowS
[Success] -> ShowS
Success -> String
(Int -> Success -> ShowS)
-> (Success -> String) -> ([Success] -> ShowS) -> Show Success
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Success -> ShowS
showsPrec :: Int -> Success -> ShowS
$cshow :: Success -> String
show :: Success -> String
$cshowList :: [Success] -> ShowS
showList :: [Success] -> ShowS
Show, Success -> Success -> Bool
(Success -> Success -> Bool)
-> (Success -> Success -> Bool) -> Eq Success
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Success -> Success -> Bool
== :: Success -> Success -> Bool
$c/= :: Success -> Success -> Bool
/= :: Success -> Success -> Bool
Eq)
newtype Resp = Resp {
Resp -> Either (VolatileDBError Block) Success
getResp :: Either (VolatileDBError Block) Success
}
deriving (Resp -> Resp -> Bool
(Resp -> Resp -> Bool) -> (Resp -> Resp -> Bool) -> Eq Resp
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Resp -> Resp -> Bool
== :: Resp -> Resp -> Bool
$c/= :: Resp -> Resp -> Bool
/= :: Resp -> Resp -> Bool
Eq, Int -> Resp -> ShowS
[Resp] -> ShowS
Resp -> String
(Int -> Resp -> ShowS)
-> (Resp -> String) -> ([Resp] -> ShowS) -> Show Resp
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Resp -> ShowS
showsPrec :: Int -> Resp -> ShowS
$cshow :: Resp -> String
show :: Resp -> String
$cshowList :: [Resp] -> ShowS
showList :: [Resp] -> ShowS
Show)
deriving instance Generic1 (At Cmd)
deriving instance Generic1 (At CmdErr)
deriving instance Rank2.Foldable (At Cmd)
deriving instance Rank2.Foldable (At CmdErr)
deriving instance Rank2.Functor (At Cmd)
deriving instance Rank2.Functor (At CmdErr)
deriving instance Rank2.Traversable (At CmdErr)
deriving instance Show1 r => Show (CmdErr :@ r)
deriving instance Show1 r => Show (Cmd :@ r)
deriving instance SOP.Generic Cmd
deriving instance SOP.HasDatatypeInfo Cmd
deriving instance Generic1 (At Resp)
deriving instance Rank2.Foldable (At Resp)
deriving instance Show1 r => Show (Resp :@ r)
deriving instance ToExpr (Model r)
instance CommandNames (At Cmd) where
cmdName :: forall (r :: * -> *). At Cmd r -> String
cmdName (At Cmd
cmd) = Cmd -> String
forall a. HasDatatypeInfo a => a -> String
constrName Cmd
cmd
cmdNames :: forall (r :: * -> *). Proxy (At Cmd r) -> [String]
cmdNames (Proxy (At Cmd r)
_ :: Proxy (At Cmd r)) = Proxy Cmd -> [String]
forall a (proxy :: * -> *).
HasDatatypeInfo a =>
proxy a -> [String]
constrNames (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @Cmd)
instance CommandNames (At CmdErr) where
cmdName :: forall (r :: * -> *). At CmdErr r -> String
cmdName (At (CmdErr { Cmd
cmd :: CmdErr -> Cmd
cmd :: Cmd
cmd }) ) = Cmd -> String
forall a. HasDatatypeInfo a => a -> String
constrName Cmd
cmd
cmdNames :: forall (r :: * -> *). Proxy (At CmdErr r) -> [String]
cmdNames (Proxy (At CmdErr r)
_ :: Proxy (At CmdErr r)) = Proxy Cmd -> [String]
forall a (proxy :: * -> *).
HasDatatypeInfo a =>
proxy a -> [String]
constrNames (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @Cmd)
newtype Model (r :: Type -> Type) = Model {
forall (r :: * -> *). Model r -> DBModel Block
dbModel :: DBModel Block
}
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)
data Event r = Event {
forall (r :: * -> *). Event r -> Model r
eventBefore :: Model r
, forall (r :: * -> *). Event r -> At CmdErr r
eventCmd :: At CmdErr r
, forall (r :: * -> *). Event r -> Model r
eventAfter :: Model r
, forall (r :: * -> *). Event r -> Resp
eventMockResp :: Resp
}
deriving (Int -> Event r -> ShowS
[Event r] -> ShowS
Event r -> String
(Int -> Event r -> ShowS)
-> (Event r -> String) -> ([Event r] -> ShowS) -> Show (Event r)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (r :: * -> *). Show1 r => Int -> Event r -> ShowS
forall (r :: * -> *). Show1 r => [Event r] -> ShowS
forall (r :: * -> *). Show1 r => Event r -> String
$cshowsPrec :: forall (r :: * -> *). Show1 r => Int -> Event r -> ShowS
showsPrec :: Int -> Event r -> ShowS
$cshow :: forall (r :: * -> *). Show1 r => Event r -> String
show :: Event r -> String
$cshowList :: forall (r :: * -> *). Show1 r => [Event r] -> ShowS
showList :: [Event r] -> ShowS
Show)
lockstep :: forall r.
Model r
-> At CmdErr r
-> Event r
lockstep :: forall (r :: * -> *). Model r -> At CmdErr r -> Event r
lockstep Model r
model At CmdErr r
cmdErr = Event {
eventBefore :: Model r
eventBefore = Model r
model
, eventCmd :: At CmdErr r
eventCmd = At CmdErr r
cmdErr
, eventAfter :: Model r
eventAfter = Model r
forall {r :: * -> *}. Model r
model'
, eventMockResp :: Resp
eventMockResp = Resp
mockResp
}
where
(Resp
mockResp, DBModel Block
dbModel') = Model r -> At CmdErr r -> (Resp, DBModel Block)
forall (r :: * -> *).
Model r -> At CmdErr r -> (Resp, DBModel Block)
step Model r
model At CmdErr r
cmdErr
model' :: Model r
model' = DBModel Block -> Model r
forall (r :: * -> *). DBModel Block -> Model r
Model DBModel Block
dbModel'
toMock :: Model r -> At t r -> t
toMock :: forall (r :: * -> *) t. Model r -> At t r -> t
toMock Model r
_ (At t
t) = t
t
step :: Model r -> At CmdErr r -> (Resp, DBModel Block)
step :: forall (r :: * -> *).
Model r -> At CmdErr r -> (Resp, DBModel Block)
step model :: Model r
model@Model{DBModel Block
dbModel :: forall (r :: * -> *). Model r -> DBModel Block
dbModel :: DBModel Block
..} At CmdErr r
cmderr = DBModel Block -> CmdErr -> (Resp, DBModel Block)
runPureErr DBModel Block
dbModel (Model r -> At CmdErr r -> CmdErr
forall (r :: * -> *) t. Model r -> At t r -> t
toMock Model r
model At CmdErr r
cmderr)
runPure :: Cmd -> DBModel Block -> (Resp, DBModel Block)
runPure :: Cmd -> DBModel Block -> (Resp, DBModel Block)
runPure = \case
GetBlockComponent HeaderHash Block
h -> (Maybe
(Block, Block, ByteString, Header Block, ByteString,
TestHeaderHash, SlotNo, IsEBB, SizeInBytes, Word16,
SomeSecond (NestedCtxt Header) Block)
-> Success)
-> (DBModel Block
-> (Either
(VolatileDBError Block)
(Maybe
(Block, Block, ByteString, Header Block, ByteString,
TestHeaderHash, SlotNo, IsEBB, SizeInBytes, Word16,
SomeSecond (NestedCtxt Header) Block)),
DBModel Block))
-> DBModel Block
-> (Resp, DBModel Block)
forall a.
(a -> Success)
-> (DBModel Block
-> (Either (VolatileDBError Block) a, DBModel Block))
-> DBModel Block
-> (Resp, DBModel Block)
ok Maybe (AllComponents Block) -> Success
Maybe
(Block, Block, ByteString, Header Block, ByteString,
TestHeaderHash, SlotNo, IsEBB, SizeInBytes, Word16,
SomeSecond (NestedCtxt Header) Block)
-> Success
MbAllComponents ((DBModel Block
-> (Either
(VolatileDBError Block)
(Maybe
(Block, Block, ByteString, Header Block, ByteString,
TestHeaderHash, SlotNo, IsEBB, SizeInBytes, Word16,
SomeSecond (NestedCtxt Header) Block)),
DBModel Block))
-> DBModel Block -> (Resp, DBModel Block))
-> (DBModel Block
-> (Either
(VolatileDBError Block)
(Maybe
(Block, Block, ByteString, Header Block, ByteString,
TestHeaderHash, SlotNo, IsEBB, SizeInBytes, Word16,
SomeSecond (NestedCtxt Header) Block)),
DBModel Block))
-> DBModel Block
-> (Resp, DBModel Block)
forall a b. (a -> b) -> a -> b
$ (DBModel Block
-> Either
(VolatileDBError Block)
(Maybe
(Block, Block, ByteString, Header Block, ByteString,
TestHeaderHash, SlotNo, IsEBB, SizeInBytes, Word16,
SomeSecond (NestedCtxt Header) Block)))
-> DBModel Block
-> (Either
(VolatileDBError Block)
(Maybe
(Block, Block, ByteString, Header Block, ByteString,
TestHeaderHash, SlotNo, IsEBB, SizeInBytes, Word16,
SomeSecond (NestedCtxt Header) Block)),
DBModel Block)
forall {b} {a}. (b -> a) -> b -> (a, b)
queryE (BlockComponent
Block
(Block, Block, ByteString, Header Block, ByteString,
TestHeaderHash, SlotNo, IsEBB, SizeInBytes, Word16,
SomeSecond (NestedCtxt Header) Block)
-> HeaderHash Block
-> DBModel Block
-> Either
(VolatileDBError Block)
(Maybe
(Block, Block, ByteString, Header Block, ByteString,
TestHeaderHash, SlotNo, IsEBB, SizeInBytes, Word16,
SomeSecond (NestedCtxt Header) Block))
forall blk b.
(HasHeader blk, GetHeader blk, HasBinaryBlockInfo blk,
EncodeDisk blk blk, HasNestedContent Header blk) =>
BlockComponent blk b
-> HeaderHash blk
-> DBModel blk
-> Either (VolatileDBError blk) (Maybe b)
getBlockComponentModel BlockComponent Block (AllComponents Block)
BlockComponent
Block
(Block, Block, ByteString, Header Block, ByteString,
TestHeaderHash, SlotNo, IsEBB, SizeInBytes, Word16,
SomeSecond (NestedCtxt Header) Block)
forall blk. BlockComponent blk (AllComponents blk)
allComponents HeaderHash Block
h)
FilterByPredecessor [ChainHash Block]
hs -> ((ChainHash Block -> Set TestHeaderHash) -> Success)
-> (DBModel Block
-> (Either
(VolatileDBError Block) (ChainHash Block -> Set TestHeaderHash),
DBModel Block))
-> DBModel Block
-> (Resp, DBModel Block)
forall a.
(a -> Success)
-> (DBModel Block
-> (Either (VolatileDBError Block) a, DBModel Block))
-> DBModel Block
-> (Resp, DBModel Block)
ok ([Set (HeaderHash Block)] -> Success
[Set TestHeaderHash] -> Success
Successors ([Set TestHeaderHash] -> Success)
-> ((ChainHash Block -> Set TestHeaderHash)
-> [Set TestHeaderHash])
-> (ChainHash Block -> Set TestHeaderHash)
-> Success
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((ChainHash Block -> Set TestHeaderHash)
-> [ChainHash Block] -> [Set TestHeaderHash]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [ChainHash Block]
hs)) ((DBModel Block
-> (Either
(VolatileDBError Block) (ChainHash Block -> Set TestHeaderHash),
DBModel Block))
-> DBModel Block -> (Resp, DBModel Block))
-> (DBModel Block
-> (Either
(VolatileDBError Block) (ChainHash Block -> Set TestHeaderHash),
DBModel Block))
-> DBModel Block
-> (Resp, DBModel Block)
forall a b. (a -> b) -> a -> b
$ (DBModel Block
-> Either
(VolatileDBError Block) (ChainHash Block -> Set TestHeaderHash))
-> DBModel Block
-> (Either
(VolatileDBError Block) (ChainHash Block -> Set TestHeaderHash),
DBModel Block)
forall {b} {a}. (b -> a) -> b -> (a, b)
queryE DBModel Block
-> Either
(VolatileDBError Block) (ChainHash Block -> Set (HeaderHash Block))
DBModel Block
-> Either
(VolatileDBError Block) (ChainHash Block -> Set TestHeaderHash)
forall blk.
GetPrevHash blk =>
DBModel blk
-> Either
(VolatileDBError blk) (ChainHash blk -> Set (HeaderHash blk))
filterByPredecessorModel
GetBlockInfo [HeaderHash Block]
hs -> ((TestHeaderHash -> Maybe (BlockInfo Block)) -> Success)
-> (DBModel Block
-> (Either
(VolatileDBError Block)
(TestHeaderHash -> Maybe (BlockInfo Block)),
DBModel Block))
-> DBModel Block
-> (Resp, DBModel Block)
forall a.
(a -> Success)
-> (DBModel Block
-> (Either (VolatileDBError Block) a, DBModel Block))
-> DBModel Block
-> (Resp, DBModel Block)
ok ([Maybe (BlockInfo Block)] -> Success
BlockInfos ([Maybe (BlockInfo Block)] -> Success)
-> ((TestHeaderHash -> Maybe (BlockInfo Block))
-> [Maybe (BlockInfo Block)])
-> (TestHeaderHash -> Maybe (BlockInfo Block))
-> Success
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((HeaderHash Block -> Maybe (BlockInfo Block))
-> [HeaderHash Block] -> [Maybe (BlockInfo Block)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [HeaderHash Block]
hs)) ((DBModel Block
-> (Either
(VolatileDBError Block)
(TestHeaderHash -> Maybe (BlockInfo Block)),
DBModel Block))
-> DBModel Block -> (Resp, DBModel Block))
-> (DBModel Block
-> (Either
(VolatileDBError Block)
(TestHeaderHash -> Maybe (BlockInfo Block)),
DBModel Block))
-> DBModel Block
-> (Resp, DBModel Block)
forall a b. (a -> b) -> a -> b
$ (DBModel Block
-> Either
(VolatileDBError Block)
(TestHeaderHash -> Maybe (BlockInfo Block)))
-> DBModel Block
-> (Either
(VolatileDBError Block)
(TestHeaderHash -> Maybe (BlockInfo Block)),
DBModel Block)
forall {b} {a}. (b -> a) -> b -> (a, b)
queryE DBModel Block
-> Either
(VolatileDBError Block)
(HeaderHash Block -> Maybe (BlockInfo Block))
DBModel Block
-> Either
(VolatileDBError Block) (TestHeaderHash -> Maybe (BlockInfo Block))
forall blk.
(GetPrevHash blk, HasBinaryBlockInfo blk) =>
DBModel blk
-> Either
(VolatileDBError blk) (HeaderHash blk -> Maybe (BlockInfo blk))
getBlockInfoModel
GarbageCollect SlotNo
slot -> (() -> Success)
-> (DBModel Block
-> (Either (VolatileDBError Block) (), DBModel Block))
-> DBModel Block
-> (Resp, DBModel Block)
forall a.
(a -> Success)
-> (DBModel Block
-> (Either (VolatileDBError Block) a, DBModel Block))
-> DBModel Block
-> (Resp, DBModel Block)
ok () -> Success
Unit ((DBModel Block
-> (Either (VolatileDBError Block) (), DBModel Block))
-> DBModel Block -> (Resp, DBModel Block))
-> (DBModel Block
-> (Either (VolatileDBError Block) (), DBModel Block))
-> DBModel Block
-> (Resp, DBModel Block)
forall a b. (a -> b) -> a -> b
$ (DBModel Block -> Either (VolatileDBError Block) (DBModel Block))
-> DBModel Block
-> (Either (VolatileDBError Block) (), DBModel Block)
forall {b} {a}. (b -> Either a b) -> b -> (Either a (), b)
updateE_ (SlotNo
-> DBModel Block -> Either (VolatileDBError Block) (DBModel Block)
forall blk.
HasHeader blk =>
SlotNo -> DBModel blk -> Either (VolatileDBError blk) (DBModel blk)
garbageCollectModel SlotNo
slot)
Cmd
Close -> (() -> Success)
-> (DBModel Block
-> (Either (VolatileDBError Block) (), DBModel Block))
-> DBModel Block
-> (Resp, DBModel Block)
forall a.
(a -> Success)
-> (DBModel Block
-> (Either (VolatileDBError Block) a, DBModel Block))
-> DBModel Block
-> (Resp, DBModel Block)
ok () -> Success
Unit ((DBModel Block
-> (Either (VolatileDBError Block) (), DBModel Block))
-> DBModel Block -> (Resp, DBModel Block))
-> (DBModel Block
-> (Either (VolatileDBError Block) (), DBModel Block))
-> DBModel Block
-> (Resp, DBModel Block)
forall a b. (a -> b) -> a -> b
$ (DBModel Block -> DBModel Block)
-> DBModel Block
-> (Either (VolatileDBError Block) (), DBModel Block)
forall {t} {b} {a}. (t -> b) -> t -> (Either a (), b)
update_ DBModel Block -> DBModel Block
forall blk. DBModel blk -> DBModel blk
closeModel
Cmd
ReOpen -> (() -> Success)
-> (DBModel Block
-> (Either (VolatileDBError Block) (), DBModel Block))
-> DBModel Block
-> (Resp, DBModel Block)
forall a.
(a -> Success)
-> (DBModel Block
-> (Either (VolatileDBError Block) a, DBModel Block))
-> DBModel Block
-> (Resp, DBModel Block)
ok () -> Success
Unit ((DBModel Block
-> (Either (VolatileDBError Block) (), DBModel Block))
-> DBModel Block -> (Resp, DBModel Block))
-> (DBModel Block
-> (Either (VolatileDBError Block) (), DBModel Block))
-> DBModel Block
-> (Resp, DBModel Block)
forall a b. (a -> b) -> a -> b
$ (DBModel Block -> DBModel Block)
-> DBModel Block
-> (Either (VolatileDBError Block) (), DBModel Block)
forall {t} {b} {a}. (t -> b) -> t -> (Either a (), b)
update_ DBModel Block -> DBModel Block
forall blk. DBModel blk -> DBModel blk
reOpenModel
Cmd
GetMaxSlotNo -> (MaxSlotNo -> Success)
-> (DBModel Block
-> (Either (VolatileDBError Block) MaxSlotNo, DBModel Block))
-> DBModel Block
-> (Resp, DBModel Block)
forall a.
(a -> Success)
-> (DBModel Block
-> (Either (VolatileDBError Block) a, DBModel Block))
-> DBModel Block
-> (Resp, DBModel Block)
ok MaxSlotNo -> Success
MaxSlot ((DBModel Block
-> (Either (VolatileDBError Block) MaxSlotNo, DBModel Block))
-> DBModel Block -> (Resp, DBModel Block))
-> (DBModel Block
-> (Either (VolatileDBError Block) MaxSlotNo, DBModel Block))
-> DBModel Block
-> (Resp, DBModel Block)
forall a b. (a -> b) -> a -> b
$ (DBModel Block -> Either (VolatileDBError Block) MaxSlotNo)
-> DBModel Block
-> (Either (VolatileDBError Block) MaxSlotNo, DBModel Block)
forall {b} {a}. (b -> a) -> b -> (a, b)
queryE DBModel Block -> Either (VolatileDBError Block) MaxSlotNo
forall blk.
HasHeader blk =>
DBModel blk -> Either (VolatileDBError blk) MaxSlotNo
getMaxSlotNoModel
PutBlock Block
blk -> (() -> Success)
-> (DBModel Block
-> (Either (VolatileDBError Block) (), DBModel Block))
-> DBModel Block
-> (Resp, DBModel Block)
forall a.
(a -> Success)
-> (DBModel Block
-> (Either (VolatileDBError Block) a, DBModel Block))
-> DBModel Block
-> (Resp, DBModel Block)
ok () -> Success
Unit ((DBModel Block
-> (Either (VolatileDBError Block) (), DBModel Block))
-> DBModel Block -> (Resp, DBModel Block))
-> (DBModel Block
-> (Either (VolatileDBError Block) (), DBModel Block))
-> DBModel Block
-> (Resp, DBModel Block)
forall a b. (a -> b) -> a -> b
$ (DBModel Block -> Either (VolatileDBError Block) (DBModel Block))
-> DBModel Block
-> (Either (VolatileDBError Block) (), DBModel Block)
forall {b} {a}. (b -> Either a b) -> b -> (Either a (), b)
updateE_ (Block
-> DBModel Block -> Either (VolatileDBError Block) (DBModel Block)
forall blk.
HasHeader blk =>
blk -> DBModel blk -> Either (VolatileDBError blk) (DBModel blk)
putBlockModel Block
blk)
Corruption Corruptions
cors -> (() -> Success)
-> (DBModel Block
-> (Either (VolatileDBError Block) (), DBModel Block))
-> DBModel Block
-> (Resp, DBModel Block)
forall a.
(a -> Success)
-> (DBModel Block
-> (Either (VolatileDBError Block) a, DBModel Block))
-> DBModel Block
-> (Resp, DBModel Block)
ok () -> Success
Unit ((DBModel Block
-> (Either (VolatileDBError Block) (), DBModel Block))
-> DBModel Block -> (Resp, DBModel Block))
-> (DBModel Block
-> (Either (VolatileDBError Block) (), DBModel Block))
-> DBModel Block
-> (Resp, DBModel Block)
forall a b. (a -> b) -> a -> b
$ (DBModel Block -> DBModel Block)
-> DBModel Block
-> (Either (VolatileDBError Block) (), DBModel Block)
forall {t} {b} {a}. (t -> b) -> t -> (Either a (), b)
update_ ((DBModel Block -> DBModel Block) -> DBModel Block -> DBModel Block
forall {blk} {blk}.
(DBModel blk -> DBModel blk) -> DBModel blk -> DBModel blk
withClosedDB (Corruptions -> DBModel Block -> DBModel Block
forall blk.
EncodeDisk blk blk =>
Corruptions -> DBModel blk -> DBModel blk
runCorruptionsModel Corruptions
cors))
DuplicateBlock {} -> (() -> Success)
-> (DBModel Block
-> (Either (VolatileDBError Block) (), DBModel Block))
-> DBModel Block
-> (Resp, DBModel Block)
forall a.
(a -> Success)
-> (DBModel Block
-> (Either (VolatileDBError Block) a, DBModel Block))
-> DBModel Block
-> (Resp, DBModel Block)
ok () -> Success
Unit ((DBModel Block
-> (Either (VolatileDBError Block) (), DBModel Block))
-> DBModel Block -> (Resp, DBModel Block))
-> (DBModel Block
-> (Either (VolatileDBError Block) (), DBModel Block))
-> DBModel Block
-> (Resp, DBModel Block)
forall a b. (a -> b) -> a -> b
$ (DBModel Block -> DBModel Block)
-> DBModel Block
-> (Either (VolatileDBError Block) (), DBModel Block)
forall {t} {b} {a}. (t -> b) -> t -> (Either a (), b)
update_ ((DBModel Block -> DBModel Block) -> DBModel Block -> DBModel Block
forall {blk} {blk}.
(DBModel blk -> DBModel blk) -> DBModel blk -> DBModel blk
withClosedDB DBModel Block -> DBModel Block
forall {a}. a -> a
noop)
where
queryE :: (b -> a) -> b -> (a, b)
queryE b -> a
f b
m = (b -> a
f b
m, b
m)
update_ :: (t -> b) -> t -> (Either a (), b)
update_ t -> b
f t
m = (() -> Either a ()
forall a b. b -> Either a b
Right (), t -> b
f t
m)
updateE_ :: (b -> Either a b) -> b -> (Either a (), b)
updateE_ b -> Either a b
f b
m = case b -> Either a b
f b
m of
Left a
e -> (a -> Either a ()
forall a b. a -> Either a b
Left a
e, b
m)
Right b
m' -> (() -> Either a ()
forall a b. b -> Either a b
Right (), b
m')
ok :: (a -> Success)
-> (DBModel Block -> (Either (VolatileDBError Block) a, DBModel Block))
-> DBModel Block
-> (Resp, DBModel Block)
ok :: forall a.
(a -> Success)
-> (DBModel Block
-> (Either (VolatileDBError Block) a, DBModel Block))
-> DBModel Block
-> (Resp, DBModel Block)
ok a -> Success
toSuccess DBModel Block -> (Either (VolatileDBError Block) a, DBModel Block)
f DBModel Block
m = (Either (VolatileDBError Block) a -> Resp)
-> (Either (VolatileDBError Block) a, DBModel Block)
-> (Resp, DBModel Block)
forall a b c. (a -> b) -> (a, c) -> (b, c)
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (Either (VolatileDBError Block) Success -> Resp
Resp (Either (VolatileDBError Block) Success -> Resp)
-> (Either (VolatileDBError Block) a
-> Either (VolatileDBError Block) Success)
-> Either (VolatileDBError Block) a
-> Resp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> Success)
-> Either (VolatileDBError Block) a
-> Either (VolatileDBError Block) Success
forall a b.
(a -> b)
-> Either (VolatileDBError Block) a
-> Either (VolatileDBError Block) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Success
toSuccess) ((Either (VolatileDBError Block) a, DBModel Block)
-> (Resp, DBModel Block))
-> (Either (VolatileDBError Block) a, DBModel Block)
-> (Resp, DBModel Block)
forall a b. (a -> b) -> a -> b
$ DBModel Block -> (Either (VolatileDBError Block) a, DBModel Block)
f DBModel Block
m
withClosedDB :: (DBModel blk -> DBModel blk) -> DBModel blk -> DBModel blk
withClosedDB DBModel blk -> DBModel blk
action = DBModel blk -> DBModel blk
forall blk. DBModel blk -> DBModel blk
reOpenModel (DBModel blk -> DBModel blk)
-> (DBModel blk -> DBModel blk) -> DBModel blk -> DBModel blk
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DBModel blk -> DBModel blk
action (DBModel blk -> DBModel blk)
-> (DBModel blk -> DBModel blk) -> DBModel blk -> DBModel blk
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DBModel blk -> DBModel blk
forall blk. DBModel blk -> DBModel blk
closeModel
noop :: a -> a
noop = a -> a
forall {a}. a -> a
id
runPureErr :: DBModel Block -> CmdErr -> (Resp, DBModel Block)
runPureErr :: DBModel Block -> CmdErr -> (Resp, DBModel Block)
runPureErr DBModel Block
dbm (CmdErr Cmd
cmd Maybe Errors
_mbErrors) = Cmd -> DBModel Block -> (Resp, DBModel Block)
runPure Cmd
cmd DBModel Block
dbm
sm ::
VolatileDBEnv
-> DBModel Block
-> StateMachine Model (At CmdErr) IO (At Resp)
sm :: VolatileDBEnv
-> DBModel Block -> StateMachine Model (At CmdErr) IO (At Resp)
sm VolatileDBEnv
env DBModel Block
dbm = StateMachine {
initModel :: forall {r :: * -> *}. Model r
initModel = DBModel Block -> Model r
forall (r :: * -> *). DBModel Block -> Model r
initModelImpl DBModel Block
dbm
, transition :: forall (r :: * -> *).
(Show1 r, Ord1 r) =>
Model r -> At CmdErr r -> At Resp r -> Model r
transition = Model r -> At CmdErr r -> At Resp r -> Model r
forall (r :: * -> *).
(Show1 r, Ord1 r) =>
Model r -> At CmdErr r -> At Resp r -> Model r
forall (r :: * -> *).
Model r -> At CmdErr r -> At Resp r -> Model r
transitionImpl
, precondition :: Model Symbolic -> At CmdErr Symbolic -> Logic
precondition = Model Symbolic -> At CmdErr Symbolic -> Logic
preconditionImpl
, postcondition :: Model Concrete -> At CmdErr Concrete -> At Resp Concrete -> Logic
postcondition = Model Concrete -> At CmdErr Concrete -> At Resp Concrete -> Logic
postconditionImpl
, generator :: Model Symbolic -> Maybe (Gen (At CmdErr Symbolic))
generator = Model Symbolic -> Maybe (Gen (At CmdErr Symbolic))
generatorImpl
, shrinker :: Model Symbolic -> At CmdErr Symbolic -> [At CmdErr Symbolic]
shrinker = Model Symbolic -> At CmdErr Symbolic -> [At CmdErr Symbolic]
shrinkerImpl
, semantics :: At CmdErr Concrete -> IO (At Resp Concrete)
semantics = VolatileDBEnv -> At CmdErr Concrete -> IO (At Resp Concrete)
semanticsImpl VolatileDBEnv
env
, mock :: Model Symbolic -> At CmdErr Symbolic -> GenSym (At Resp Symbolic)
mock = Model Symbolic -> At CmdErr Symbolic -> GenSym (At Resp Symbolic)
mockImpl
, invariant :: Maybe (Model Concrete -> Logic)
invariant = Maybe (Model Concrete -> Logic)
forall a. Maybe a
Nothing
, cleanup :: Model Concrete -> IO ()
cleanup = Model Concrete -> IO ()
forall (m :: * -> *) (model :: (* -> *) -> *).
Monad m =>
model Concrete -> m ()
noCleanup
}
initModelImpl :: DBModel Block -> Model r
initModelImpl :: forall (r :: * -> *). DBModel Block -> Model r
initModelImpl = DBModel Block -> Model r
forall (r :: * -> *). DBModel Block -> Model r
Model
transitionImpl :: Model r -> At CmdErr r -> At Resp r -> Model r
transitionImpl :: forall (r :: * -> *).
Model r -> At CmdErr r -> At Resp r -> Model r
transitionImpl Model r
model At CmdErr r
cmd At Resp r
_ = Event r -> Model r
forall (r :: * -> *). Event r -> Model r
eventAfter (Event r -> Model r) -> Event r -> Model r
forall a b. (a -> b) -> a -> b
$ Model r -> At CmdErr r -> Event r
forall (r :: * -> *). Model r -> At CmdErr r -> Event r
lockstep Model r
model At CmdErr r
cmd
preconditionImpl :: Model Symbolic -> At CmdErr Symbolic -> Logic
preconditionImpl :: Model Symbolic -> At CmdErr Symbolic -> Logic
preconditionImpl Model{DBModel Block
dbModel :: forall (r :: * -> *). Model r -> DBModel Block
dbModel :: DBModel Block
..} (At (CmdErr Cmd
cmd Maybe Errors
mbErrors)) =
Logic
compatibleWithError Logic -> Logic -> Logic
.&& case Cmd
cmd of
Corruption Corruptions
cors ->
[FsPath] -> (FsPath -> Logic) -> Logic
forall a. Show a => [a] -> (a -> Logic) -> Logic
forAll (Corruptions -> [FsPath]
corruptionFiles Corruptions
cors) (FsPath -> [FsPath] -> Logic
forall (t :: * -> *) a.
(Foldable t, Eq a, Show a, Show (t a)) =>
a -> t a -> Logic
`member` DBModel Block -> [FsPath]
forall blk. DBModel blk -> [FsPath]
getDBFiles DBModel Block
dbModel)
DuplicateBlock Int
fileId Block
blk -> case HeaderHash Block -> Maybe Int
fileIdContainingBlock (Block -> HeaderHash Block
forall b. HasHeader b => b -> HeaderHash b
blockHash Block
blk) of
Maybe Int
Nothing -> Logic
Bot
Just Int
fileId' -> Int
fileId Int -> Int -> Logic
forall a. (Ord a, Show a) => a -> a -> Logic
.>= Int
fileId'
Cmd
_ -> Logic
Top
where
compatibleWithError :: Logic
compatibleWithError :: Logic
compatibleWithError
| Bool -> Bool
not (Cmd -> Bool
allowErrorFor Cmd
cmd), Just Errors
_ <- Maybe Errors
mbErrors
= Logic
Bot
| Bool
otherwise
= Logic
Top
fileIdContainingBlock :: HeaderHash Block -> Maybe FileId
fileIdContainingBlock :: HeaderHash Block -> Maybe Int
fileIdContainingBlock HeaderHash Block
hash = [Int] -> Maybe Int
forall a. [a] -> Maybe a
listToMaybe
[ Int
fileId
| (Int
fileId, BlocksInFile [Block]
blocks) <- Map Int (BlocksInFile Block) -> [(Int, BlocksInFile Block)]
forall k a. Map k a -> [(k, a)]
Map.toList (Map Int (BlocksInFile Block) -> [(Int, BlocksInFile Block)])
-> Map Int (BlocksInFile Block) -> [(Int, BlocksInFile Block)]
forall a b. (a -> b) -> a -> b
$ DBModel Block -> Map Int (BlocksInFile Block)
forall blk. DBModel blk -> Map Int (BlocksInFile blk)
fileIndex DBModel Block
dbModel
, Block
blk <- [Block]
blocks
, Block -> HeaderHash Block
forall b. HasHeader b => b -> HeaderHash b
blockHash Block
blk TestHeaderHash -> TestHeaderHash -> Bool
forall a. Eq a => a -> a -> Bool
== HeaderHash Block
TestHeaderHash
hash
]
postconditionImpl :: Model Concrete
-> At CmdErr Concrete
-> At Resp Concrete
-> Logic
postconditionImpl :: Model Concrete -> At CmdErr Concrete -> At Resp Concrete -> Logic
postconditionImpl Model Concrete
model At CmdErr Concrete
cmdErr At Resp Concrete
resp =
Model Concrete -> At Resp Concrete -> Resp
forall (r :: * -> *) t. Model r -> At t r -> t
toMock (Event Concrete -> Model Concrete
forall (r :: * -> *). Event r -> Model r
eventAfter Event Concrete
ev) At Resp Concrete
resp Resp -> Resp -> Logic
forall a. (Eq a, Show a) => a -> a -> Logic
.== Event Concrete -> Resp
forall (r :: * -> *). Event r -> Resp
eventMockResp Event Concrete
ev
where
ev :: Event Concrete
ev = Model Concrete -> At CmdErr Concrete -> Event Concrete
forall (r :: * -> *). Model r -> At CmdErr r -> Event r
lockstep Model Concrete
model At CmdErr Concrete
cmdErr
generatorCmdImpl :: Model Symbolic -> Gen Cmd
generatorCmdImpl :: Model Symbolic -> Gen Cmd
generatorCmdImpl Model {DBModel Block
dbModel :: forall (r :: * -> *). Model r -> DBModel Block
dbModel :: DBModel Block
..} = [(Int, Gen Cmd)] -> Gen Cmd
forall a. [(Int, Gen a)] -> Gen a
frequency
[ (Int
3, Block -> Cmd
PutBlock (Block -> Cmd) -> Gen Block -> Gen Cmd
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Block
genTestBlock)
, (Int
1, Cmd -> Gen Cmd
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return Cmd
Close)
, (if DBModel Block -> Bool
forall blk. DBModel blk -> Bool
open DBModel Block
dbModel then Int
1 else Int
5, Cmd -> Gen Cmd
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return Cmd
ReOpen)
, (Int
2, HeaderHash Block -> Cmd
TestHeaderHash -> Cmd
GetBlockComponent (TestHeaderHash -> Cmd) -> Gen TestHeaderHash -> Gen Cmd
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (HeaderHash Block)
Gen TestHeaderHash
genHash)
, (Int
2, SlotNo -> Cmd
GarbageCollect (SlotNo -> Cmd) -> Gen SlotNo -> Gen Cmd
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen SlotNo
genGCSlot)
, (Int
2, [HeaderHash Block] -> Cmd
[TestHeaderHash] -> Cmd
GetBlockInfo ([TestHeaderHash] -> Cmd) -> Gen [TestHeaderHash] -> Gen Cmd
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen TestHeaderHash -> Gen [TestHeaderHash]
forall a. Gen a -> Gen [a]
listOf Gen (HeaderHash Block)
Gen TestHeaderHash
genHash)
, (Int
2, [ChainHash Block] -> Cmd
FilterByPredecessor ([ChainHash Block] -> Cmd) -> Gen [ChainHash Block] -> Gen Cmd
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (ChainHash Block) -> Gen [ChainHash Block]
forall a. Gen a -> Gen [a]
listOf Gen (ChainHash Block)
genPrevHash)
, (Int
2, Cmd -> Gen Cmd
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return Cmd
GetMaxSlotNo)
, (if [FsPath] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [FsPath]
dbFiles then Int
0 else Int
1,
Corruptions -> Cmd
Corruption (Corruptions -> Cmd) -> Gen Corruptions -> Gen Cmd
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NonEmpty FsPath -> Gen Corruptions
generateCorruptions ([FsPath] -> NonEmpty FsPath
forall a. HasCallStack => [a] -> NonEmpty a
NE.fromList [FsPath]
dbFiles))
, (if Bool
isEmpty then Int
0 else Int
1, Gen Cmd
genDuplicateBlock)
]
where
blockIdx :: Map (HeaderHash Block) Block
blockIdx = DBModel Block -> Map (HeaderHash Block) Block
forall blk.
HasHeader blk =>
DBModel blk -> Map (HeaderHash blk) blk
blockIndex DBModel Block
dbModel
dbFiles :: [FsPath]
dbFiles = DBModel Block -> [FsPath]
forall blk. DBModel blk -> [FsPath]
getDBFiles DBModel Block
dbModel
isEmpty :: Bool
isEmpty = Map TestHeaderHash Block -> Bool
forall k a. Map k a -> Bool
Map.null Map TestHeaderHash Block
blockIdx
canContainEBB :: b -> Bool
canContainEBB = Bool -> b -> Bool
forall a b. a -> b -> a
const Bool
True
getSlot :: HeaderHash Block -> Maybe SlotNo
getSlot :: HeaderHash Block -> Maybe SlotNo
getSlot HeaderHash Block
hash = Block -> SlotNo
forall b. HasHeader b => b -> SlotNo
blockSlot (Block -> SlotNo) -> Maybe Block -> Maybe SlotNo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TestHeaderHash -> Map TestHeaderHash Block -> Maybe Block
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup HeaderHash Block
TestHeaderHash
hash Map TestHeaderHash Block
blockIdx
genSlotStartingFrom :: SlotNo -> Gen SlotNo
genSlotStartingFrom :: SlotNo -> Gen SlotNo
genSlotStartingFrom SlotNo
slot = SlotNo -> SlotNo -> Gen SlotNo
chooseSlot SlotNo
slot (SlotNo
slot SlotNo -> SlotNo -> SlotNo
forall a. Num a => a -> a -> a
+ SlotNo
20)
mbMinMaxSlotInModel :: Maybe (SlotNo, SlotNo)
mbMinMaxSlotInModel :: Maybe (SlotNo, SlotNo)
mbMinMaxSlotInModel = do
SlotNo
minSlot <- Block -> SlotNo
forall b. HasHeader b => b -> SlotNo
blockSlot (Block -> SlotNo)
-> ((Block, Map TestHeaderHash Block) -> Block)
-> (Block, Map TestHeaderHash Block)
-> SlotNo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Block, Map TestHeaderHash Block) -> Block
forall a b. (a, b) -> a
fst ((Block, Map TestHeaderHash Block) -> SlotNo)
-> Maybe (Block, Map TestHeaderHash Block) -> Maybe SlotNo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map TestHeaderHash Block -> Maybe (Block, Map TestHeaderHash Block)
forall k a. Map k a -> Maybe (a, Map k a)
Map.minView Map TestHeaderHash Block
blockIdx
SlotNo
maxSlot <- Block -> SlotNo
forall b. HasHeader b => b -> SlotNo
blockSlot (Block -> SlotNo)
-> ((Block, Map TestHeaderHash Block) -> Block)
-> (Block, Map TestHeaderHash Block)
-> SlotNo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Block, Map TestHeaderHash Block) -> Block
forall a b. (a, b) -> a
fst ((Block, Map TestHeaderHash Block) -> SlotNo)
-> Maybe (Block, Map TestHeaderHash Block) -> Maybe SlotNo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map TestHeaderHash Block -> Maybe (Block, Map TestHeaderHash Block)
forall k a. Map k a -> Maybe (a, Map k a)
Map.maxView Map TestHeaderHash Block
blockIdx
(SlotNo, SlotNo) -> Maybe (SlotNo, SlotNo)
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (SlotNo
minSlot, SlotNo
maxSlot)
genTestBlock :: Gen Block
genTestBlock :: Gen Block
genTestBlock = [(Int, Gen Block)] -> Gen Block
forall a. [(Int, Gen a)] -> Gen a
frequency
[ (Int
4, Gen (HeaderHash Block)
Gen TestHeaderHash
genHash Gen TestHeaderHash -> (TestHeaderHash -> Gen Block) -> Gen Block
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= HeaderHash Block -> Gen Block
TestHeaderHash -> Gen Block
genSuccessor)
, (Int
1, Gen Block
genRandomBlock)
]
genSuccessor :: HeaderHash Block -> Gen Block
genSuccessor :: HeaderHash Block -> Gen Block
genSuccessor HeaderHash Block
prevHash = do
Block
b <- Gen Block
genRandomBlock
SlotNo
slot <- SlotNo -> Gen SlotNo
genSlotStartingFrom (SlotNo -> Gen SlotNo) -> SlotNo -> Gen SlotNo
forall a b. (a -> b) -> a -> b
$ SlotNo -> (SlotNo -> SlotNo) -> Maybe SlotNo -> SlotNo
forall b a. b -> (a -> b) -> Maybe a -> b
maybe SlotNo
0 SlotNo -> SlotNo
forall a. Enum a => a -> a
succ (HeaderHash Block -> Maybe SlotNo
getSlot HeaderHash Block
prevHash)
let body :: TestBody
body = Block -> TestBody
testBody Block
b
th :: TestHeader
th = Block -> TestHeader
testHeader Block
b
no :: BlockNo
no = TestHeader -> BlockNo
thBlockNo TestHeader
th
clen :: ChainLength
clen = TestHeader -> ChainLength
thChainLength TestHeader
th
ebb :: Maybe EpochNo
ebb = Block -> Maybe EpochNo
forall blk. GetHeader blk => blk -> Maybe EpochNo
blockIsEBB Block
b
Block -> Gen Block
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (Block -> Gen Block) -> Block -> Gen Block
forall a b. (a -> b) -> a -> b
$ HasCallStack =>
(SlotNo -> Bool)
-> TestBody
-> ChainHash TestHeader
-> SlotNo
-> BlockNo
-> ChainLength
-> Maybe EpochNo
-> Block
(SlotNo -> Bool)
-> TestBody
-> ChainHash TestHeader
-> SlotNo
-> BlockNo
-> ChainLength
-> Maybe EpochNo
-> Block
mkBlock SlotNo -> Bool
forall {b}. b -> Bool
canContainEBB TestBody
body (HeaderHash TestHeader -> ChainHash TestHeader
forall {k} (b :: k). HeaderHash b -> ChainHash b
BlockHash HeaderHash TestHeader
HeaderHash Block
prevHash) SlotNo
slot BlockNo
no ChainLength
clen Maybe EpochNo
ebb
genRandomBlock :: Gen Block
genRandomBlock :: Gen Block
genRandomBlock = do
TestBody
body <- Word -> Bool -> TestBody
TestBody (Word -> Bool -> TestBody) -> Gen Word -> Gen (Bool -> TestBody)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Word
forall a. Arbitrary a => Gen a
arbitrary Gen (Bool -> TestBody) -> Gen Bool -> Gen TestBody
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Gen Bool
forall a. Arbitrary a => Gen a
arbitrary
ChainHash TestHeader
prevHash <- [(Int, Gen (ChainHash TestHeader))] -> Gen (ChainHash TestHeader)
forall a. [(Int, Gen a)] -> Gen a
frequency
[ (Int
1, ChainHash TestHeader -> Gen (ChainHash TestHeader)
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return ChainHash TestHeader
forall {k} (b :: k). ChainHash b
GenesisHash)
, (Int
6, HeaderHash TestHeader -> ChainHash TestHeader
TestHeaderHash -> ChainHash TestHeader
forall {k} (b :: k). HeaderHash b -> ChainHash b
BlockHash (TestHeaderHash -> ChainHash TestHeader)
-> (Int -> TestHeaderHash) -> Int -> ChainHash TestHeader
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> TestHeaderHash
TestHeaderHash (Int -> ChainHash TestHeader)
-> Gen Int -> Gen (ChainHash TestHeader)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Int
forall a. Arbitrary a => Gen a
arbitrary)
]
SlotNo
slot <- SlotNo -> Gen SlotNo
genSlotStartingFrom SlotNo
0
BlockNo
no <- Word64 -> BlockNo
BlockNo (Word64 -> BlockNo) -> Gen Word64 -> Gen BlockNo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Word64
forall a. Arbitrary a => Gen a
arbitrary
Maybe EpochNo
ebb <- Gen (Maybe EpochNo)
forall a. Arbitrary a => Gen a
arbitrary
let clen :: ChainLength
clen = Int -> ChainLength
ChainLength (Word64 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (BlockNo -> Word64
unBlockNo BlockNo
no))
Block -> Gen Block
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (Block -> Gen Block) -> Block -> Gen Block
forall a b. (a -> b) -> a -> b
$ HasCallStack =>
(SlotNo -> Bool)
-> TestBody
-> ChainHash TestHeader
-> SlotNo
-> BlockNo
-> ChainLength
-> Maybe EpochNo
-> Block
(SlotNo -> Bool)
-> TestBody
-> ChainHash TestHeader
-> SlotNo
-> BlockNo
-> ChainLength
-> Maybe EpochNo
-> Block
mkBlock SlotNo -> Bool
forall {b}. b -> Bool
canContainEBB TestBody
body ChainHash TestHeader
prevHash SlotNo
slot BlockNo
no ChainLength
clen Maybe EpochNo
ebb
genHash :: Gen (HeaderHash Block)
genHash :: Gen (HeaderHash Block)
genHash = [(Int, Gen TestHeaderHash)] -> Gen TestHeaderHash
forall a. [(Int, Gen a)] -> Gen a
frequency
[ (if Bool
isEmpty then Int
0 else Int
5, [TestHeaderHash] -> Gen TestHeaderHash
forall a. HasCallStack => [a] -> Gen a
elements ([TestHeaderHash] -> Gen TestHeaderHash)
-> [TestHeaderHash] -> Gen TestHeaderHash
forall a b. (a -> b) -> a -> b
$ Map TestHeaderHash Block -> [TestHeaderHash]
forall k a. Map k a -> [k]
Map.keys Map TestHeaderHash Block
blockIdx)
, (Int
1, Int -> TestHeaderHash
TestHeaderHash (Int -> TestHeaderHash) -> Gen Int -> Gen TestHeaderHash
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Int
forall a. Arbitrary a => Gen a
arbitrary)
, (Int
4, Block -> HeaderHash Block
Block -> TestHeaderHash
forall b. HasHeader b => b -> HeaderHash b
blockHash (Block -> TestHeaderHash) -> Gen Block -> Gen TestHeaderHash
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Block
genTestBlock)
]
genPrevHash :: Gen (ChainHash Block)
genPrevHash :: Gen (ChainHash Block)
genPrevHash = [(Int, Gen (ChainHash Block))] -> Gen (ChainHash Block)
forall a. [(Int, Gen a)] -> Gen a
frequency
[ (Int
1, ChainHash Block -> Gen (ChainHash Block)
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return ChainHash Block
forall {k} (b :: k). ChainHash b
GenesisHash)
, (Int
8, HeaderHash Block -> ChainHash Block
TestHeaderHash -> ChainHash Block
forall {k} (b :: k). HeaderHash b -> ChainHash b
BlockHash (TestHeaderHash -> ChainHash Block)
-> Gen TestHeaderHash -> Gen (ChainHash Block)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (HeaderHash Block)
Gen TestHeaderHash
genHash)
]
genGCSlot :: Gen SlotNo
genGCSlot :: Gen SlotNo
genGCSlot = case Maybe (SlotNo, SlotNo)
mbMinMaxSlotInModel of
Maybe (SlotNo, SlotNo)
Nothing -> SlotNo -> SlotNo -> Gen SlotNo
chooseSlot SlotNo
0 SlotNo
10
Just (SlotNo
minSlot, SlotNo
maxSlot) ->
SlotNo -> SlotNo -> Gen SlotNo
chooseSlot (SlotNo -> SlotNo -> SlotNo
forall a. (Num a, Ord a) => a -> a -> a
subtractNoUnderflow SlotNo
minSlot SlotNo
3) (SlotNo
maxSlot SlotNo -> SlotNo -> SlotNo
forall a. Num a => a -> a -> a
+ SlotNo
3)
subtractNoUnderflow :: (Num a, Ord a) => a -> a -> a
subtractNoUnderflow :: forall a. (Num a, Ord a) => a -> a -> a
subtractNoUnderflow a
x a
y
| a
x a -> a -> Bool
forall a. Ord a => a -> a -> Bool
>= a
y = a
x a -> a -> a
forall a. Num a => a -> a -> a
- a
y
| Bool
otherwise = a
0
chooseSlot :: SlotNo -> SlotNo -> Gen SlotNo
chooseSlot :: SlotNo -> SlotNo -> Gen SlotNo
chooseSlot (SlotNo Word64
start) (SlotNo Word64
end) = Word64 -> SlotNo
SlotNo (Word64 -> SlotNo) -> Gen Word64 -> Gen SlotNo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Word64, Word64) -> Gen Word64
forall a. Random a => (a, a) -> Gen a
choose (Word64
start, Word64
end)
genDuplicateBlock :: Gen Cmd
genDuplicateBlock = do
(Int
originalFileId, Block
blk) <- [(Int, Block)] -> Gen (Int, Block)
forall a. HasCallStack => [a] -> Gen a
elements
[ (Int
fileId, Block
blk)
| (Int
fileId, BlocksInFile [Block]
blks) <- Map Int (BlocksInFile Block) -> [(Int, BlocksInFile Block)]
forall k a. Map k a -> [(k, a)]
Map.toList (Map Int (BlocksInFile Block) -> [(Int, BlocksInFile Block)])
-> Map Int (BlocksInFile Block) -> [(Int, BlocksInFile Block)]
forall a b. (a -> b) -> a -> b
$ DBModel Block -> Map Int (BlocksInFile Block)
forall blk. DBModel blk -> Map Int (BlocksInFile blk)
fileIndex DBModel Block
dbModel
, Block
blk <- [Block]
blks
]
Int
fileId <- [Int] -> Gen Int
forall a. HasCallStack => [a] -> Gen a
elements (DBModel Block -> [Int]
forall blk. DBModel blk -> [Int]
getDBFileIds DBModel Block
dbModel) Gen Int -> (Int -> Bool) -> Gen Int
forall a. Gen a -> (a -> Bool) -> Gen a
`suchThat` (Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
originalFileId)
Cmd -> Gen Cmd
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (Cmd -> Gen Cmd) -> Cmd -> Gen Cmd
forall a b. (a -> b) -> a -> b
$ Int -> Block -> Cmd
DuplicateBlock Int
fileId Block
blk
generatorImpl :: Model Symbolic -> Maybe (Gen (At CmdErr Symbolic))
generatorImpl :: Model Symbolic -> Maybe (Gen (At CmdErr Symbolic))
generatorImpl m :: Model Symbolic
m@Model {DBModel Block
dbModel :: forall (r :: * -> *). Model r -> DBModel Block
dbModel :: DBModel Block
..} = Gen (At CmdErr Symbolic) -> Maybe (Gen (At CmdErr Symbolic))
forall a. a -> Maybe a
Just (Gen (At CmdErr Symbolic) -> Maybe (Gen (At CmdErr Symbolic)))
-> Gen (At CmdErr Symbolic) -> Maybe (Gen (At CmdErr Symbolic))
forall a b. (a -> b) -> a -> b
$ do
Cmd
cmd <- Model Symbolic -> Gen Cmd
generatorCmdImpl Model Symbolic
m
Maybe Errors
err <- [(Int, Gen (Maybe Errors))] -> Gen (Maybe Errors)
forall a. [(Int, Gen a)] -> Gen a
frequency
[ (Int
9, Maybe Errors -> Gen (Maybe Errors)
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Errors
forall a. Maybe a
Nothing)
, (if Cmd -> Bool
allowErrorFor Cmd
cmd Bool -> Bool -> Bool
&& DBModel Block -> Bool
forall blk. DBModel blk -> Bool
open DBModel Block
dbModel then Int
1 else Int
0,
Errors -> Maybe Errors
forall a. a -> Maybe a
Just (Errors -> Maybe Errors) -> Gen Errors -> Gen (Maybe Errors)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Bool -> Bool -> Gen Errors
genErrors Bool
True Bool
True)
]
At CmdErr Symbolic -> Gen (At CmdErr Symbolic)
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return (At CmdErr Symbolic -> Gen (At CmdErr Symbolic))
-> At CmdErr Symbolic -> Gen (At CmdErr Symbolic)
forall a b. (a -> b) -> a -> b
$ CmdErr -> At CmdErr Symbolic
forall t (r :: * -> *). t -> At t r
At (CmdErr -> At CmdErr Symbolic) -> CmdErr -> At CmdErr Symbolic
forall a b. (a -> b) -> a -> b
$ Cmd -> Maybe Errors -> CmdErr
CmdErr Cmd
cmd Maybe Errors
err
allowErrorFor :: Cmd -> Bool
allowErrorFor :: Cmd -> Bool
allowErrorFor Corruption {} = Bool
False
allowErrorFor DuplicateBlock {} = Bool
False
allowErrorFor Cmd
_ = Bool
True
shrinkerImpl :: Model Symbolic -> At CmdErr Symbolic -> [At CmdErr Symbolic]
shrinkerImpl :: Model Symbolic -> At CmdErr Symbolic -> [At CmdErr Symbolic]
shrinkerImpl Model Symbolic
m (At (CmdErr Cmd
cmd Maybe Errors
mbErr)) = (CmdErr -> At CmdErr Symbolic) -> [CmdErr] -> [At CmdErr Symbolic]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap CmdErr -> At CmdErr Symbolic
forall t (r :: * -> *). t -> At t r
At ([CmdErr] -> [At CmdErr Symbolic])
-> [CmdErr] -> [At CmdErr Symbolic]
forall a b. (a -> b) -> a -> b
$
[ Cmd -> Maybe Errors -> CmdErr
CmdErr Cmd
cmd Maybe Errors
mbErr' | Maybe Errors
mbErr' <- Maybe Errors -> [Maybe Errors]
forall a. Arbitrary a => a -> [a]
shrink Maybe Errors
mbErr ] [CmdErr] -> [CmdErr] -> [CmdErr]
forall a. [a] -> [a] -> [a]
++
[ Cmd -> Maybe Errors -> CmdErr
CmdErr Cmd
cmd' Maybe Errors
mbErr | Cmd
cmd' <- Model Symbolic -> Cmd -> [Cmd]
shrinkCmd Model Symbolic
m Cmd
cmd ]
shrinkCmd :: Model Symbolic -> Cmd -> [Cmd]
shrinkCmd :: Model Symbolic -> Cmd -> [Cmd]
shrinkCmd Model Symbolic
_ Cmd
cmd = case Cmd
cmd of
GetBlockInfo [HeaderHash Block]
bids -> [HeaderHash Block] -> Cmd
[TestHeaderHash] -> Cmd
GetBlockInfo ([TestHeaderHash] -> Cmd) -> [[TestHeaderHash]] -> [Cmd]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TestHeaderHash -> [TestHeaderHash])
-> [TestHeaderHash] -> [[TestHeaderHash]]
forall a. (a -> [a]) -> [a] -> [[a]]
shrinkList ([TestHeaderHash] -> TestHeaderHash -> [TestHeaderHash]
forall a b. a -> b -> a
const []) [HeaderHash Block]
[TestHeaderHash]
bids
FilterByPredecessor [ChainHash Block]
preds -> [ChainHash Block] -> Cmd
FilterByPredecessor ([ChainHash Block] -> Cmd) -> [[ChainHash Block]] -> [Cmd]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (ChainHash Block -> [ChainHash Block])
-> [ChainHash Block] -> [[ChainHash Block]]
forall a. (a -> [a]) -> [a] -> [[a]]
shrinkList ([ChainHash Block] -> ChainHash Block -> [ChainHash Block]
forall a b. a -> b -> a
const []) [ChainHash Block]
preds
Corruption Corruptions
cors -> Corruptions -> Cmd
Corruption (Corruptions -> Cmd) -> [Corruptions] -> [Cmd]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Corruptions -> [Corruptions]
shrinkCorruptions Corruptions
cors
Cmd
_ -> []
data VolatileDBEnv = VolatileDBEnv
{ VolatileDBEnv -> StrictTVar IO Errors
varErrors :: StrictTVar IO Errors
, VolatileDBEnv -> StrictTVar IO (VolatileDB IO Block)
varDB :: StrictTVar IO (VolatileDB IO Block)
, VolatileDBEnv -> VolatileDbArgs Identity IO Block
args :: VolatileDbArgs Identity IO Block
}
reopenDB :: VolatileDBEnv -> IO ()
reopenDB :: VolatileDBEnv -> IO ()
reopenDB VolatileDBEnv { StrictTVar IO (VolatileDB IO Block)
varDB :: VolatileDBEnv -> StrictTVar IO (VolatileDB IO Block)
varDB :: StrictTVar IO (VolatileDB IO Block)
varDB, VolatileDbArgs Identity IO Block
args :: VolatileDBEnv -> VolatileDbArgs Identity IO Block
args :: VolatileDbArgs Identity IO Block
args } = do
VolatileDB IO Block
db <- VolatileDbArgs Identity IO Block
-> (forall st.
WithTempRegistry st IO (VolatileDB IO Block, st)
-> IO (VolatileDB IO Block))
-> IO (VolatileDB IO Block)
forall (m :: * -> *) blk ans.
(HasCallStack, IOLike m, GetPrevHash blk,
VolatileDbSerialiseConstraints blk) =>
Complete VolatileDbArgs m blk
-> (forall st. WithTempRegistry st m (VolatileDB m blk, st) -> ans)
-> ans
openDB VolatileDbArgs Identity IO Block
args WithTempRegistry st IO (VolatileDB IO Block, st)
-> IO (VolatileDB IO Block)
forall st.
WithTempRegistry st IO (VolatileDB IO Block, st)
-> IO (VolatileDB IO Block)
forall (m :: * -> *) st a.
(IOLike m, HasCallStack) =>
WithTempRegistry st m (a, st) -> m a
runWithTempRegistry
IO (VolatileDB IO Block) -> IO ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (IO (VolatileDB IO Block) -> IO ())
-> IO (VolatileDB IO Block) -> IO ()
forall a b. (a -> b) -> a -> b
$ STM IO (VolatileDB IO Block) -> IO (VolatileDB IO Block)
forall a. HasCallStack => STM IO a -> IO a
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
STM m a -> m a
atomically (STM IO (VolatileDB IO Block) -> IO (VolatileDB IO Block))
-> STM IO (VolatileDB IO Block) -> IO (VolatileDB IO Block)
forall a b. (a -> b) -> a -> b
$ StrictTVar IO (VolatileDB IO Block)
-> VolatileDB IO Block -> STM IO (VolatileDB IO Block)
forall (m :: * -> *) a.
MonadSTM m =>
StrictTVar m a -> a -> STM m a
swapTVar StrictTVar IO (VolatileDB IO Block)
varDB VolatileDB IO Block
db
semanticsImpl :: VolatileDBEnv -> At CmdErr Concrete -> IO (At Resp Concrete)
semanticsImpl :: VolatileDBEnv -> At CmdErr Concrete -> IO (At Resp Concrete)
semanticsImpl env :: VolatileDBEnv
env@VolatileDBEnv { StrictTVar IO (VolatileDB IO Block)
varDB :: VolatileDBEnv -> StrictTVar IO (VolatileDB IO Block)
varDB :: StrictTVar IO (VolatileDB IO Block)
varDB, StrictTVar IO Errors
varErrors :: VolatileDBEnv -> StrictTVar IO Errors
varErrors :: StrictTVar IO Errors
varErrors } (At (CmdErr Cmd
cmd Maybe Errors
mbErrors)) =
Resp -> At Resp Concrete
forall t (r :: * -> *). t -> At t r
At (Resp -> At Resp Concrete)
-> (Either (VolatileDBError Block) Success -> Resp)
-> Either (VolatileDBError Block) Success
-> At Resp Concrete
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Either (VolatileDBError Block) Success -> Resp
Resp (Either (VolatileDBError Block) Success -> At Resp Concrete)
-> IO (Either (VolatileDBError Block) Success)
-> IO (At Resp Concrete)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> case Maybe Errors
mbErrors of
Maybe Errors
Nothing -> Proxy Block
-> IO Success -> IO (Either (VolatileDBError Block) Success)
forall (m :: * -> *) a blk.
(MonadCatch m, Typeable blk, StandardHash blk) =>
Proxy blk -> m a -> m (Either (VolatileDBError blk) a)
tryVolatileDB (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @Block) (HasCallStack => VolatileDBEnv -> Cmd -> IO Success
VolatileDBEnv -> Cmd -> IO Success
runDB VolatileDBEnv
env Cmd
cmd)
Just Errors
errors -> do
Either (VolatileDBError Block) Success
_ <- StrictTVar IO Errors
-> Errors
-> IO (Either (VolatileDBError Block) Success)
-> IO (Either (VolatileDBError Block) Success)
forall (m :: * -> *) a.
MonadSTM m =>
StrictTVar m Errors -> Errors -> m a -> m a
withErrors (StrictTVar IO Errors -> StrictTVar IO Errors
forall (m :: * -> *) a. StrictTVar m a -> StrictTVar m a
unsafeToUncheckedStrictTVar StrictTVar IO Errors
varErrors) Errors
errors (IO (Either (VolatileDBError Block) Success)
-> IO (Either (VolatileDBError Block) Success))
-> IO (Either (VolatileDBError Block) Success)
-> IO (Either (VolatileDBError Block) Success)
forall a b. (a -> b) -> a -> b
$
Proxy Block
-> IO Success -> IO (Either (VolatileDBError Block) Success)
forall (m :: * -> *) a blk.
(MonadCatch m, Typeable blk, StandardHash blk) =>
Proxy blk -> m a -> m (Either (VolatileDBError blk) a)
tryVolatileDB (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @Block) (HasCallStack => VolatileDBEnv -> Cmd -> IO Success
VolatileDBEnv -> Cmd -> IO Success
runDB VolatileDBEnv
env Cmd
cmd)
StrictTVar IO (VolatileDB IO Block) -> IO (VolatileDB IO Block)
forall (m :: * -> *) a. MonadSTM m => StrictTVar m a -> m a
readTVarIO StrictTVar IO (VolatileDB IO Block)
varDB IO (VolatileDB IO Block) -> (VolatileDB IO Block -> IO ()) -> IO ()
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= VolatileDB IO Block -> IO ()
idemPotentCloseDB
VolatileDBEnv -> IO ()
reopenDB VolatileDBEnv
env
Proxy Block
-> IO Success -> IO (Either (VolatileDBError Block) Success)
forall (m :: * -> *) a blk.
(MonadCatch m, Typeable blk, StandardHash blk) =>
Proxy blk -> m a -> m (Either (VolatileDBError blk) a)
tryVolatileDB (forall t. Proxy t
forall {k} (t :: k). Proxy t
Proxy @Block) (HasCallStack => VolatileDBEnv -> Cmd -> IO Success
VolatileDBEnv -> Cmd -> IO Success
runDB VolatileDBEnv
env Cmd
cmd)
idemPotentCloseDB :: VolatileDB IO Block -> IO ()
idemPotentCloseDB :: VolatileDB IO Block -> IO ()
idemPotentCloseDB VolatileDB IO Block
db =
(VolatileDBError Block -> Maybe ())
-> IO () -> (() -> IO ()) -> IO ()
forall e b a.
Exception e =>
(e -> Maybe b) -> IO a -> (b -> IO a) -> IO a
forall (m :: * -> *) e b a.
(MonadCatch m, Exception e) =>
(e -> Maybe b) -> m a -> (b -> m a) -> m a
catchJust
VolatileDBError Block -> Maybe ()
isClosedDBError
(VolatileDB IO Block -> HasCallStack => IO ()
forall (m :: * -> *) blk. VolatileDB m blk -> HasCallStack => m ()
closeDB VolatileDB IO Block
db)
(IO () -> () -> IO ()
forall a b. a -> b -> a
const (() -> IO ()
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return ()))
where
isClosedDBError :: VolatileDBError Block -> Maybe ()
isClosedDBError :: VolatileDBError Block -> Maybe ()
isClosedDBError (ApiMisuse (ClosedDBError Maybe SomeException
_)) = () -> Maybe ()
forall a. a -> Maybe a
Just ()
isClosedDBError VolatileDBError Block
_ = Maybe ()
forall a. Maybe a
Nothing
runDB :: HasCallStack => VolatileDBEnv -> Cmd -> IO Success
runDB :: HasCallStack => VolatileDBEnv -> Cmd -> IO Success
runDB env :: VolatileDBEnv
env@VolatileDBEnv { StrictTVar IO (VolatileDB IO Block)
varDB :: VolatileDBEnv -> StrictTVar IO (VolatileDB IO Block)
varDB :: StrictTVar IO (VolatileDB IO Block)
varDB, args :: VolatileDBEnv -> VolatileDbArgs Identity IO Block
args = VolatileDbArgs { volHasFS :: forall (f :: * -> *) (m :: * -> *) blk.
VolatileDbArgs f m blk -> HKD f (SomeHasFS m)
volHasFS = SomeHasFS HasFS IO h
hasFS } } Cmd
cmd = StrictTVar IO (VolatileDB IO Block) -> IO (VolatileDB IO Block)
forall (m :: * -> *) a. MonadSTM m => StrictTVar m a -> m a
readTVarIO StrictTVar IO (VolatileDB IO Block)
varDB IO (VolatileDB IO Block)
-> (VolatileDB IO Block -> IO Success) -> IO Success
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \VolatileDB IO Block
db -> case Cmd
cmd of
GetBlockComponent HeaderHash Block
hash -> Maybe (AllComponents Block) -> Success
Maybe
(Block, Block, ByteString, Header Block, ByteString,
TestHeaderHash, SlotNo, IsEBB, SizeInBytes, Word16,
SomeSecond (NestedCtxt Header) Block)
-> Success
MbAllComponents (Maybe
(Block, Block, ByteString, Header Block, ByteString,
TestHeaderHash, SlotNo, IsEBB, SizeInBytes, Word16,
SomeSecond (NestedCtxt Header) Block)
-> Success)
-> IO
(Maybe
(Block, Block, ByteString, Header Block, ByteString,
TestHeaderHash, SlotNo, IsEBB, SizeInBytes, Word16,
SomeSecond (NestedCtxt Header) Block))
-> IO Success
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VolatileDB IO Block
-> forall b.
HasCallStack =>
BlockComponent Block b -> HeaderHash Block -> IO (Maybe b)
forall (m :: * -> *) blk.
VolatileDB m blk
-> forall b.
HasCallStack =>
BlockComponent blk b -> HeaderHash blk -> m (Maybe b)
getBlockComponent VolatileDB IO Block
db BlockComponent Block (AllComponents Block)
BlockComponent
Block
(Block, Block, ByteString, Header Block, ByteString,
TestHeaderHash, SlotNo, IsEBB, SizeInBytes, Word16,
SomeSecond (NestedCtxt Header) Block)
forall blk. BlockComponent blk (AllComponents blk)
allComponents HeaderHash Block
hash
PutBlock Block
blk -> () -> Success
Unit (() -> Success) -> IO () -> IO Success
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VolatileDB IO Block -> HasCallStack => Block -> IO ()
forall (m :: * -> *) blk.
VolatileDB m blk -> HasCallStack => blk -> m ()
putBlock VolatileDB IO Block
db Block
blk
FilterByPredecessor [ChainHash Block]
hashes -> [Set (HeaderHash Block)] -> Success
[Set TestHeaderHash] -> Success
Successors ([Set TestHeaderHash] -> Success)
-> ((ChainHash Block -> Set TestHeaderHash)
-> [Set TestHeaderHash])
-> (ChainHash Block -> Set TestHeaderHash)
-> Success
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((ChainHash Block -> Set TestHeaderHash)
-> [ChainHash Block] -> [Set TestHeaderHash]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [ChainHash Block]
hashes) ((ChainHash Block -> Set TestHeaderHash) -> Success)
-> IO (ChainHash Block -> Set TestHeaderHash) -> IO Success
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> STM IO (ChainHash Block -> Set TestHeaderHash)
-> IO (ChainHash Block -> Set TestHeaderHash)
forall a. HasCallStack => STM IO a -> IO a
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
STM m a -> m a
atomically (VolatileDB IO Block
-> HasCallStack =>
STM IO (ChainHash Block -> Set (HeaderHash Block))
forall (m :: * -> *) blk.
VolatileDB m blk
-> HasCallStack => STM m (ChainHash blk -> Set (HeaderHash blk))
filterByPredecessor VolatileDB IO Block
db)
GetBlockInfo [HeaderHash Block]
hashes -> [Maybe (BlockInfo Block)] -> Success
BlockInfos ([Maybe (BlockInfo Block)] -> Success)
-> ((TestHeaderHash -> Maybe (BlockInfo Block))
-> [Maybe (BlockInfo Block)])
-> (TestHeaderHash -> Maybe (BlockInfo Block))
-> Success
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((HeaderHash Block -> Maybe (BlockInfo Block))
-> [HeaderHash Block] -> [Maybe (BlockInfo Block)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [HeaderHash Block]
hashes) ((TestHeaderHash -> Maybe (BlockInfo Block)) -> Success)
-> IO (TestHeaderHash -> Maybe (BlockInfo Block)) -> IO Success
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> STM IO (TestHeaderHash -> Maybe (BlockInfo Block))
-> IO (TestHeaderHash -> Maybe (BlockInfo Block))
forall a. HasCallStack => STM IO a -> IO a
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
STM m a -> m a
atomically (VolatileDB IO Block
-> HasCallStack =>
STM IO (HeaderHash Block -> Maybe (BlockInfo Block))
forall (m :: * -> *) blk.
VolatileDB m blk
-> HasCallStack => STM m (HeaderHash blk -> Maybe (BlockInfo blk))
getBlockInfo VolatileDB IO Block
db)
GarbageCollect SlotNo
slot -> () -> Success
Unit (() -> Success) -> IO () -> IO Success
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VolatileDB IO Block -> HasCallStack => SlotNo -> IO ()
forall (m :: * -> *) blk.
VolatileDB m blk -> HasCallStack => SlotNo -> m ()
garbageCollect VolatileDB IO Block
db SlotNo
slot
Cmd
GetMaxSlotNo -> MaxSlotNo -> Success
MaxSlot (MaxSlotNo -> Success) -> IO MaxSlotNo -> IO Success
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> STM IO MaxSlotNo -> IO MaxSlotNo
forall a. HasCallStack => STM IO a -> IO a
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
STM m a -> m a
atomically (VolatileDB IO Block -> HasCallStack => STM IO MaxSlotNo
forall (m :: * -> *) blk.
VolatileDB m blk -> HasCallStack => STM m MaxSlotNo
getMaxSlotNo VolatileDB IO Block
db)
Cmd
Close -> () -> Success
Unit (() -> Success) -> IO () -> IO Success
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VolatileDB IO Block -> HasCallStack => IO ()
forall (m :: * -> *) blk. VolatileDB m blk -> HasCallStack => m ()
closeDB VolatileDB IO Block
db
Cmd
ReOpen -> do
StrictTVar IO (VolatileDB IO Block) -> IO (VolatileDB IO Block)
forall (m :: * -> *) a. MonadSTM m => StrictTVar m a -> m a
readTVarIO StrictTVar IO (VolatileDB IO Block)
varDB IO (VolatileDB IO Block) -> (VolatileDB IO Block -> IO ()) -> IO ()
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= VolatileDB IO Block -> IO ()
idemPotentCloseDB
() -> Success
Unit (() -> Success) -> IO () -> IO Success
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VolatileDBEnv -> IO ()
reopenDB VolatileDBEnv
env
Corruption Corruptions
corrs ->
IO () -> IO Success
withClosedDB (IO () -> IO Success) -> IO () -> IO Success
forall a b. (a -> b) -> a -> b
$
Corruptions -> ((FileCorruption, FsPath) -> IO Bool) -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ Corruptions
corrs (((FileCorruption, FsPath) -> IO Bool) -> IO ())
-> ((FileCorruption, FsPath) -> IO Bool) -> IO ()
forall a b. (a -> b) -> a -> b
$ \(FileCorruption
corr, FsPath
file) -> HasFS IO h -> FileCorruption -> FsPath -> IO Bool
forall (m :: * -> *) h.
MonadThrow m =>
HasFS m h -> FileCorruption -> FsPath -> m Bool
corruptFile HasFS IO h
hasFS FileCorruption
corr FsPath
file
DuplicateBlock Int
fileId Block
blk -> do
IO () -> IO Success
withClosedDB (IO () -> IO Success) -> IO () -> IO Success
forall a b. (a -> b) -> a -> b
$
HasFS IO h -> FsPath -> OpenMode -> (Handle h -> IO ()) -> IO ()
forall (m :: * -> *) h a.
(HasCallStack, MonadThrow m) =>
HasFS m h -> FsPath -> OpenMode -> (Handle h -> m a) -> m a
withFile HasFS IO h
hasFS (Int -> FsPath
filePath Int
fileId) (AllowExisting -> OpenMode
AppendMode AllowExisting
AllowExisting) ((Handle h -> IO ()) -> IO ()) -> (Handle h -> IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ \Handle h
hndl ->
IO Word64 -> IO ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (IO Word64 -> IO ()) -> IO Word64 -> IO ()
forall a b. (a -> b) -> a -> b
$ HasFS IO h -> Handle h -> ByteString -> IO Word64
forall (m :: * -> *) h.
(HasCallStack, Monad m) =>
HasFS m h -> Handle h -> ByteString -> m Word64
hPutAll HasFS IO h
hasFS Handle h
hndl (Block -> ByteString
testBlockToLazyByteString Block
blk)
where
withClosedDB :: IO () -> IO Success
withClosedDB :: IO () -> IO Success
withClosedDB IO ()
action = do
StrictTVar IO (VolatileDB IO Block) -> IO (VolatileDB IO Block)
forall (m :: * -> *) a. MonadSTM m => StrictTVar m a -> m a
readTVarIO StrictTVar IO (VolatileDB IO Block)
varDB IO (VolatileDB IO Block) -> (VolatileDB IO Block -> IO ()) -> IO ()
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= VolatileDB IO Block -> IO ()
VolatileDB IO Block -> HasCallStack => IO ()
forall (m :: * -> *) blk. VolatileDB m blk -> HasCallStack => m ()
closeDB
IO ()
action
VolatileDBEnv -> IO ()
reopenDB VolatileDBEnv
env
Success -> IO Success
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (Success -> IO Success) -> Success -> IO Success
forall a b. (a -> b) -> a -> b
$ () -> Success
Unit ()
mockImpl :: Model Symbolic -> At CmdErr Symbolic -> GenSym (At Resp Symbolic)
mockImpl :: Model Symbolic -> At CmdErr Symbolic -> GenSym (At Resp Symbolic)
mockImpl Model Symbolic
model At CmdErr Symbolic
cmdErr = Resp -> At Resp Symbolic
forall t (r :: * -> *). t -> At t r
At (Resp -> At Resp Symbolic)
-> GenSym Resp -> GenSym (At Resp Symbolic)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Resp -> GenSym Resp
forall a. a -> GenSym a
forall (m :: * -> *) a. Monad m => a -> m a
return Resp
mockResp
where
(Resp
mockResp, DBModel Block
_dbModel') = Model Symbolic -> At CmdErr Symbolic -> (Resp, DBModel Block)
forall (r :: * -> *).
Model r -> At CmdErr r -> (Resp, DBModel Block)
step Model Symbolic
model At CmdErr Symbolic
cmdErr
prop_sequential :: Property
prop_sequential :: Property
prop_sequential = StateMachine Model (At CmdErr) IO (At Resp)
-> Maybe Int
-> (Commands (At CmdErr) (At Resp) -> 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
forAllCommands StateMachine Model (At CmdErr) IO (At Resp)
smUnused Maybe Int
forall a. Maybe a
Nothing ((Commands (At CmdErr) (At Resp) -> Property) -> Property)
-> (Commands (At CmdErr) (At Resp) -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \Commands (At CmdErr) (At Resp)
cmds -> PropertyM IO () -> Property
forall a. Testable a => PropertyM IO a -> Property
monadicIO (PropertyM IO () -> Property) -> PropertyM IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
(History (At CmdErr) (At Resp)
hist, Property
prop) <- IO (History (At CmdErr) (At Resp), Property)
-> PropertyM IO (History (At CmdErr) (At Resp), Property)
forall (m :: * -> *) a. Monad m => m a -> PropertyM m a
run (IO (History (At CmdErr) (At Resp), Property)
-> PropertyM IO (History (At CmdErr) (At Resp), Property))
-> IO (History (At CmdErr) (At Resp), Property)
-> PropertyM IO (History (At CmdErr) (At Resp), Property)
forall a b. (a -> b) -> a -> b
$ Commands (At CmdErr) (At Resp)
-> IO (History (At CmdErr) (At Resp), Property)
test Commands (At CmdErr) (At Resp)
cmds
let events :: [Event Symbolic]
events = Model Symbolic
-> Commands (At CmdErr) (At Resp) -> [Event Symbolic]
execCmds (StateMachine Model (At CmdErr) IO (At Resp)
-> forall {r :: * -> *}. Model r
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> forall (r :: * -> *). model r
initModel StateMachine Model (At CmdErr) IO (At Resp)
smUnused) Commands (At CmdErr) (At Resp)
cmds
StateMachine Model (At CmdErr) IO (At Resp)
-> History (At CmdErr) (At Resp) -> 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 ()
prettyCommands StateMachine Model (At CmdErr) IO (At Resp)
smUnused History (At CmdErr) (At Resp)
hist
(Property -> PropertyM IO ()) -> Property -> PropertyM IO ()
forall a b. (a -> b) -> a -> b
$ String -> [String] -> Property -> Property
forall prop.
Testable prop =>
String -> [String] -> prop -> Property
tabulate String
"Tags"
((Tag -> String) -> [Tag] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Tag -> String
forall a. Show a => a -> String
show ([Tag] -> [String]) -> [Tag] -> [String]
forall a b. (a -> b) -> a -> b
$ [Event Symbolic] -> [Tag]
tag [Event Symbolic]
events)
(Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ String -> [String] -> Property -> Property
forall prop.
Testable prop =>
String -> [String] -> prop -> Property
tabulate String
"Commands"
(At CmdErr Symbolic -> String
forall k (cmd :: k -> *) (r :: k).
CommandNames cmd =>
cmd r -> String
forall (r :: * -> *). At CmdErr r -> String
cmdName (At CmdErr Symbolic -> String)
-> (Event Symbolic -> At CmdErr Symbolic)
-> Event Symbolic
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Event Symbolic -> At CmdErr Symbolic
forall (r :: * -> *). Event r -> At CmdErr r
eventCmd (Event Symbolic -> String) -> [Event Symbolic] -> [String]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Event Symbolic]
events)
(Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ String -> [String] -> Property -> Property
forall prop.
Testable prop =>
String -> [String] -> prop -> Property
tabulate String
"Error Tags"
([Event Symbolic] -> [String]
tagSimulatedErrors [Event Symbolic]
events)
(Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ String -> [String] -> Property -> Property
forall prop.
Testable prop =>
String -> [String] -> prop -> Property
tabulate String
"GetBlockInfo: total number of Just's"
[Int -> String
forall {a}. (Ord a, Num a, Show a) => a -> String
groupIsMember (Int -> String) -> Int -> String
forall a b. (a -> b) -> a -> b
$ [Event Symbolic] -> Int
isMemberTrue [Event Symbolic]
events]
(Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ String -> [String] -> Property -> Property
forall prop.
Testable prop =>
String -> [String] -> prop -> Property
tabulate String
"Successors"
([Event Symbolic] -> [String]
tagFilterByPredecessor [Event Symbolic]
events)
(Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ Property
prop
where
dbm :: DBModel Block
dbm = BlocksPerFile -> CodecConfig Block -> DBModel Block
forall blk. BlocksPerFile -> CodecConfig blk -> DBModel blk
initDBModel BlocksPerFile
testMaxBlocksPerFile CodecConfig Block
TestBlockCodecConfig
smUnused :: StateMachine Model (At CmdErr) IO (At Resp)
smUnused = VolatileDBEnv
-> DBModel Block -> StateMachine Model (At CmdErr) IO (At Resp)
sm VolatileDBEnv
unusedEnv DBModel Block
dbm
groupIsMember :: a -> String
groupIsMember a
n
| a
n a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
5 = a -> String
forall a. Show a => a -> String
show a
n
| a
n a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
20 = String
"5-19"
| a
n a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
100 = String
"20-99"
| Bool
otherwise = String
">=100"
test :: Commands (At CmdErr) (At Resp)
-> IO (History (At CmdErr) (At Resp), Property)
test :: Commands (At CmdErr) (At Resp)
-> IO (History (At CmdErr) (At Resp), Property)
test Commands (At CmdErr) (At Resp)
cmds = do
StrictTVar IO Errors
varErrors <- Errors -> IO (StrictTVar IO Errors)
forall (m :: * -> *) a. MonadSTM m => a -> m (StrictTVar m a)
uncheckedNewTVarM Errors
emptyErrors
StrictTMVar IO MockFS
varFs <- STM IO (StrictTMVar IO MockFS) -> IO (StrictTMVar IO MockFS)
forall a. HasCallStack => STM IO a -> IO a
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
STM m a -> m a
atomically (STM IO (StrictTMVar IO MockFS) -> IO (StrictTMVar IO MockFS))
-> STM IO (StrictTMVar IO MockFS) -> IO (StrictTMVar IO MockFS)
forall a b. (a -> b) -> a -> b
$ MockFS -> STM IO (StrictTMVar IO MockFS)
forall (m :: * -> *) a. MonadSTM m => a -> STM m (StrictTMVar m a)
newTMVar MockFS
Mock.empty
(Tracer IO (TraceEvent Block)
tracer, IO [TraceEvent Block]
getTrace) <- IO (Tracer IO (TraceEvent Block), IO [TraceEvent Block])
forall ev. IO (Tracer IO ev, IO [ev])
recordingTracerIORef
let hasFS :: HasFS IO HandleMock
hasFS = StrictTMVar IO MockFS
-> StrictTVar IO Errors -> HasFS IO HandleMock
forall (m :: * -> *).
(MonadSTM m, MonadThrow m, PrimMonad m) =>
StrictTMVar m MockFS -> StrictTVar m Errors -> HasFS m HandleMock
simErrorHasFS StrictTMVar IO MockFS
varFs (StrictTVar IO Errors -> StrictTVar IO Errors
forall (m :: * -> *) a. StrictTVar m a -> StrictTVar m a
unsafeToUncheckedStrictTVar StrictTVar IO Errors
varErrors)
args :: VolatileDbArgs Identity IO Block
args = VolatileDbArgs {
volCheckIntegrity :: HKD Identity (Block -> Bool)
volCheckIntegrity = HKD Identity (Block -> Bool)
Block -> Bool
testBlockIsValid
, volCodecConfig :: HKD Identity (CodecConfig Block)
volCodecConfig = HKD Identity (CodecConfig Block)
CodecConfig Block
TestBlockCodecConfig
, volHasFS :: HKD Identity (SomeHasFS IO)
volHasFS = HasFS IO HandleMock -> SomeHasFS IO
forall h (m :: * -> *). Eq h => HasFS m h -> SomeHasFS m
SomeHasFS HasFS IO HandleMock
hasFS
, volMaxBlocksPerFile :: BlocksPerFile
volMaxBlocksPerFile = BlocksPerFile
testMaxBlocksPerFile
, volTracer :: Tracer IO (TraceEvent Block)
volTracer = Tracer IO (TraceEvent Block)
tracer
, volValidationPolicy :: BlockValidationPolicy
volValidationPolicy = BlockValidationPolicy
ValidateAll
}
(History (At CmdErr) (At Resp)
hist, Reason
res, [TraceEvent Block]
trace) <- IO (StrictTVar IO (VolatileDB IO Block))
-> (StrictTVar IO (VolatileDB IO Block) -> IO ())
-> (StrictTVar IO (VolatileDB IO Block)
-> IO (History (At CmdErr) (At Resp), Reason, [TraceEvent Block]))
-> IO (History (At CmdErr) (At Resp), Reason, [TraceEvent Block])
forall a b c. IO a -> (a -> IO b) -> (a -> IO c) -> IO c
forall (m :: * -> *) a b c.
MonadThrow m =>
m a -> (a -> m b) -> (a -> m c) -> m c
bracket
(VolatileDbArgs Identity IO Block
-> (forall st.
WithTempRegistry st IO (VolatileDB IO Block, st)
-> IO (VolatileDB IO Block))
-> IO (VolatileDB IO Block)
forall (m :: * -> *) blk ans.
(HasCallStack, IOLike m, GetPrevHash blk,
VolatileDbSerialiseConstraints blk) =>
Complete VolatileDbArgs m blk
-> (forall st. WithTempRegistry st m (VolatileDB m blk, st) -> ans)
-> ans
openDB VolatileDbArgs Identity IO Block
args WithTempRegistry st IO (VolatileDB IO Block, st)
-> IO (VolatileDB IO Block)
forall st.
WithTempRegistry st IO (VolatileDB IO Block, st)
-> IO (VolatileDB IO Block)
forall (m :: * -> *) st a.
(IOLike m, HasCallStack) =>
WithTempRegistry st m (a, st) -> m a
runWithTempRegistry IO (VolatileDB IO Block)
-> (VolatileDB IO Block
-> IO (StrictTVar IO (VolatileDB IO Block)))
-> IO (StrictTVar IO (VolatileDB IO Block))
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= VolatileDB IO Block -> IO (StrictTVar IO (VolatileDB IO Block))
forall (m :: * -> *) a.
(HasCallStack, MonadSTM m, NoThunks a) =>
a -> m (StrictTVar m a)
newTVarIO)
(\StrictTVar IO (VolatileDB IO Block)
varDB -> StrictTVar IO (VolatileDB IO Block) -> IO (VolatileDB IO Block)
forall (m :: * -> *) a. MonadSTM m => StrictTVar m a -> m a
readTVarIO StrictTVar IO (VolatileDB IO Block)
varDB IO (VolatileDB IO Block) -> (VolatileDB IO Block -> IO ()) -> IO ()
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= VolatileDB IO Block -> IO ()
VolatileDB IO Block -> HasCallStack => IO ()
forall (m :: * -> *) blk. VolatileDB m blk -> HasCallStack => m ()
closeDB)
((StrictTVar IO (VolatileDB IO Block)
-> IO (History (At CmdErr) (At Resp), Reason, [TraceEvent Block]))
-> IO (History (At CmdErr) (At Resp), Reason, [TraceEvent Block]))
-> (StrictTVar IO (VolatileDB IO Block)
-> IO (History (At CmdErr) (At Resp), Reason, [TraceEvent Block]))
-> IO (History (At CmdErr) (At Resp), Reason, [TraceEvent Block])
forall a b. (a -> b) -> a -> b
$ \StrictTVar IO (VolatileDB IO Block)
varDB -> do
let env :: VolatileDBEnv
env = VolatileDBEnv { StrictTVar IO Errors
varErrors :: StrictTVar IO Errors
varErrors :: StrictTVar IO Errors
varErrors, StrictTVar IO (VolatileDB IO Block)
varDB :: StrictTVar IO (VolatileDB IO Block)
varDB :: StrictTVar IO (VolatileDB IO Block)
varDB, VolatileDbArgs Identity IO Block
args :: VolatileDbArgs Identity IO Block
args :: VolatileDbArgs Identity IO Block
args }
sm' :: StateMachine Model (At CmdErr) IO (At Resp)
sm' = VolatileDBEnv
-> DBModel Block -> StateMachine Model (At CmdErr) IO (At Resp)
sm VolatileDBEnv
env DBModel Block
dbm
(History (At CmdErr) (At Resp)
hist, Model Concrete
_model, Reason
res) <- StateMachine Model (At CmdErr) IO (At Resp)
-> Commands (At CmdErr) (At Resp)
-> IO (History (At CmdErr) (At Resp), Model Concrete, Reason)
forall (cmd :: (* -> *) -> *) (resp :: (* -> *) -> *) (m :: * -> *)
(model :: (* -> *) -> *).
(Show (cmd Concrete), Show (resp Concrete), Traversable cmd,
Foldable resp, MonadMask m, MonadIO m) =>
StateMachine model cmd m resp
-> Commands cmd resp
-> m (History cmd resp, model Concrete, Reason)
QSM.runCommands' StateMachine Model (At CmdErr) IO (At Resp)
sm' Commands (At CmdErr) (At Resp)
cmds
[TraceEvent Block]
trace <- IO [TraceEvent Block]
getTrace
(History (At CmdErr) (At Resp), Reason, [TraceEvent Block])
-> IO (History (At CmdErr) (At Resp), Reason, [TraceEvent Block])
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (History (At CmdErr) (At Resp)
hist, Reason
res, [TraceEvent Block]
trace)
MockFS
fs <- STM IO MockFS -> IO MockFS
forall a. HasCallStack => STM IO a -> IO a
forall (m :: * -> *) a.
(MonadSTM m, HasCallStack) =>
STM m a -> m a
atomically (STM IO MockFS -> IO MockFS) -> STM IO MockFS -> IO MockFS
forall a b. (a -> b) -> a -> b
$ StrictTMVar IO MockFS -> STM IO MockFS
forall (m :: * -> *) a. MonadSTM m => StrictTMVar m a -> STM m a
readTMVar StrictTMVar IO MockFS
varFs
let prop :: Property
prop =
String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"Trace: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> [String] -> String
unlines ((TraceEvent Block -> String) -> [TraceEvent Block] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map TraceEvent Block -> String
forall a. Show a => a -> String
show [TraceEvent Block]
trace)) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"FS: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> MockFS -> String
Mock.pretty MockFS
fs) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
Reason
res Reason -> Reason -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Reason
Ok
(History (At CmdErr) (At Resp), Property)
-> IO (History (At CmdErr) (At Resp), Property)
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return (History (At CmdErr) (At Resp)
hist, Property
prop)
where
dbm :: DBModel Block
dbm = BlocksPerFile -> CodecConfig Block -> DBModel Block
forall blk. BlocksPerFile -> CodecConfig blk -> DBModel blk
initDBModel BlocksPerFile
testMaxBlocksPerFile CodecConfig Block
TestBlockCodecConfig
testMaxBlocksPerFile :: BlocksPerFile
testMaxBlocksPerFile :: BlocksPerFile
testMaxBlocksPerFile = Word32 -> BlocksPerFile
mkBlocksPerFile Word32
3
unusedEnv :: VolatileDBEnv
unusedEnv :: VolatileDBEnv
unusedEnv = String -> VolatileDBEnv
forall a. HasCallStack => String -> a
error String
"VolatileDBEnv used during command generation"
tests :: TestTree
tests :: TestTree
tests = String -> [TestTree] -> TestTree
testGroup String
"VolatileDB q-s-m" [
String -> Property -> TestTree
forall a. Testable a => String -> a -> TestTree
testProperty String
"sequential" Property
prop_sequential
]
type EventPred = C.Predicate (Event Symbolic) Tag
successful :: ( Event Symbolic
-> Success
-> Either Tag EventPred
)
-> EventPred
successful :: (Event Symbolic -> Success -> Either Tag EventPred) -> EventPred
successful Event Symbolic -> Success -> Either Tag EventPred
f = (Event Symbolic -> Either Tag EventPred) -> EventPred
forall a b. (a -> Either b (Predicate a b)) -> Predicate a b
C.predicate ((Event Symbolic -> Either Tag EventPred) -> EventPred)
-> (Event Symbolic -> Either Tag EventPred) -> EventPred
forall a b. (a -> b) -> a -> b
$ \Event Symbolic
ev -> case (Event Symbolic -> Resp
forall (r :: * -> *). Event r -> Resp
eventMockResp Event Symbolic
ev, Event Symbolic -> At CmdErr Symbolic
forall (r :: * -> *). Event r -> At CmdErr r
eventCmd Event Symbolic
ev) of
(Resp (Right Success
ok), At (CmdErr Cmd
_ Maybe Errors
Nothing)) -> Event Symbolic -> Success -> Either Tag EventPred
f Event Symbolic
ev Success
ok
(Resp, At CmdErr Symbolic)
_ -> EventPred -> Either Tag EventPred
forall a b. b -> Either a b
Right (EventPred -> Either Tag EventPred)
-> EventPred -> Either Tag EventPred
forall a b. (a -> b) -> a -> b
$ (Event Symbolic -> Success -> Either Tag EventPred) -> EventPred
successful Event Symbolic -> Success -> Either Tag EventPred
f
tag :: [Event Symbolic] -> [Tag]
tag :: [Event Symbolic] -> [Tag]
tag [] = [Tag
TagEmpty]
tag [Event Symbolic]
ls = [EventPred] -> [Event Symbolic] -> [Tag]
forall a b. [Predicate a b] -> [a] -> [b]
C.classify
[ EventPred
tagGetBlockComponentNothing
, Either Tag EventPred -> EventPred
tagGetJust (Either Tag EventPred -> EventPred)
-> Either Tag EventPred -> EventPred
forall a b. (a -> b) -> a -> b
$ Tag -> Either Tag EventPred
forall a b. a -> Either a b
Left Tag
TagGetJust
, EventPred
tagGetReOpenGet
, EventPred
tagReOpenJust
, Bool -> Set (HeaderHash Block) -> Maybe SlotNo -> EventPred
tagGarbageCollect Bool
True Set (HeaderHash Block)
Set TestHeaderHash
forall a. Set a
Set.empty Maybe SlotNo
forall a. Maybe a
Nothing
, EventPred
tagCorruptWriteFile
, EventPred
tagIsClosedError
, EventPred
tagGarbageCollectThenReOpen
] [Event Symbolic]
ls
where
tagGetBlockComponentNothing :: EventPred
tagGetBlockComponentNothing :: EventPred
tagGetBlockComponentNothing = (Event Symbolic -> Success -> Either Tag EventPred) -> EventPred
successful ((Event Symbolic -> Success -> Either Tag EventPred) -> EventPred)
-> (Event Symbolic -> Success -> Either Tag EventPred) -> EventPred
forall a b. (a -> b) -> a -> b
$ \Event Symbolic
ev Success
r -> case Success
r of
MbAllComponents Maybe (AllComponents Block)
Nothing | GetBlockComponent {} <- Event Symbolic -> Cmd
forall (r :: * -> *). Event r -> Cmd
getCmd Event Symbolic
ev ->
Tag -> Either Tag EventPred
forall a b. a -> Either a b
Left Tag
TagGetNothing
Success
_ -> EventPred -> Either Tag EventPred
forall a b. b -> Either a b
Right EventPred
tagGetBlockComponentNothing
tagReOpenJust :: EventPred
tagReOpenJust :: EventPred
tagReOpenJust = Bool -> Either Tag EventPred -> EventPred
tagReOpen Bool
False (Either Tag EventPred -> EventPred)
-> Either Tag EventPred -> EventPred
forall a b. (a -> b) -> a -> b
$ EventPred -> Either Tag EventPred
forall a b. b -> Either a b
Right (EventPred -> Either Tag EventPred)
-> EventPred -> Either Tag EventPred
forall a b. (a -> b) -> a -> b
$ Either Tag EventPred -> EventPred
tagGetJust (Either Tag EventPred -> EventPred)
-> Either Tag EventPred -> EventPred
forall a b. (a -> b) -> a -> b
$ Tag -> Either Tag EventPred
forall a b. a -> Either a b
Left Tag
TagReOpenGet
tagGetReOpenGet :: EventPred
tagGetReOpenGet :: EventPred
tagGetReOpenGet = Either Tag EventPred -> EventPred
tagGetJust (Either Tag EventPred -> EventPred)
-> Either Tag EventPred -> EventPred
forall a b. (a -> b) -> a -> b
$ EventPred -> Either Tag EventPred
forall a b. b -> Either a b
Right (EventPred -> Either Tag EventPred)
-> EventPred -> Either Tag EventPred
forall a b. (a -> b) -> a -> b
$ Bool -> Either Tag EventPred -> EventPred
tagReOpen Bool
False (Either Tag EventPred -> EventPred)
-> Either Tag EventPred -> EventPred
forall a b. (a -> b) -> a -> b
$
EventPred -> Either Tag EventPred
forall a b. b -> Either a b
Right (EventPred -> Either Tag EventPred)
-> EventPred -> Either Tag EventPred
forall a b. (a -> b) -> a -> b
$ Either Tag EventPred -> EventPred
tagGetJust (Either Tag EventPred -> EventPred)
-> Either Tag EventPred -> EventPred
forall a b. (a -> b) -> a -> b
$ Tag -> Either Tag EventPred
forall a b. a -> Either a b
Left Tag
TagGetReOpenGet
tagGarbageCollect ::
Bool
-> Set (HeaderHash Block)
-> Maybe SlotNo
-> EventPred
tagGarbageCollect :: Bool -> Set (HeaderHash Block) -> Maybe SlotNo -> EventPred
tagGarbageCollect Bool
keep Set (HeaderHash Block)
bids Maybe SlotNo
mbGCed = (Event Symbolic -> Success -> Either Tag EventPred) -> EventPred
successful ((Event Symbolic -> Success -> Either Tag EventPred) -> EventPred)
-> (Event Symbolic -> Success -> Either Tag EventPred) -> EventPred
forall a b. (a -> b) -> a -> b
$ \Event Symbolic
ev Success
suc ->
if Bool -> Bool
not Bool
keep then EventPred -> Either Tag EventPred
forall a b. b -> Either a b
Right (EventPred -> Either Tag EventPred)
-> EventPred -> Either Tag EventPred
forall a b. (a -> b) -> a -> b
$ Bool -> Set (HeaderHash Block) -> Maybe SlotNo -> EventPred
tagGarbageCollect Bool
keep Set (HeaderHash Block)
bids Maybe SlotNo
mbGCed
else case (Maybe SlotNo
mbGCed, Success
suc, Event Symbolic -> Cmd
forall (r :: * -> *). Event r -> Cmd
getCmd Event Symbolic
ev) of
(Maybe SlotNo
Nothing, Success
_, PutBlock TestBlock{testHeader :: Block -> TestHeader
testHeader = TestHeader{BlockNo
SlotNo
ChainHash TestHeader
HeaderHash TestHeader
ChainLength
EBB
TestBodyHash
thBlockNo :: TestHeader -> BlockNo
thChainLength :: TestHeader -> ChainLength
thHash :: HeaderHash TestHeader
thPrevHash :: ChainHash TestHeader
thBodyHash :: TestBodyHash
thSlotNo :: SlotNo
thBlockNo :: BlockNo
thChainLength :: ChainLength
thIsEBB :: EBB
thHash :: TestHeader -> HeaderHash TestHeader
thPrevHash :: TestHeader -> ChainHash TestHeader
thBodyHash :: TestHeader -> TestBodyHash
thSlotNo :: TestHeader -> SlotNo
thIsEBB :: TestHeader -> EBB
..}})
-> EventPred -> Either Tag EventPred
forall a b. b -> Either a b
Right (EventPred -> Either Tag EventPred)
-> EventPred -> Either Tag EventPred
forall a b. (a -> b) -> a -> b
$ Bool -> Set (HeaderHash Block) -> Maybe SlotNo -> EventPred
tagGarbageCollect
Bool
True
(TestHeaderHash -> Set TestHeaderHash -> Set TestHeaderHash
forall a. Ord a => a -> Set a -> Set a
Set.insert HeaderHash TestHeader
TestHeaderHash
thHash Set (HeaderHash Block)
Set TestHeaderHash
bids)
Maybe SlotNo
forall a. Maybe a
Nothing
(Maybe SlotNo
Nothing, Success
_, GarbageCollect SlotNo
sl)
-> EventPred -> Either Tag EventPred
forall a b. b -> Either a b
Right (EventPred -> Either Tag EventPred)
-> EventPred -> Either Tag EventPred
forall a b. (a -> b) -> a -> b
$ Bool -> Set (HeaderHash Block) -> Maybe SlotNo -> EventPred
tagGarbageCollect Bool
True Set (HeaderHash Block)
bids (SlotNo -> Maybe SlotNo
forall a. a -> Maybe a
Just SlotNo
sl)
(Just SlotNo
_gced, MbAllComponents Maybe (AllComponents Block)
Nothing, GetBlockComponent HeaderHash Block
bid)
| (TestHeaderHash -> Set TestHeaderHash -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member HeaderHash Block
TestHeaderHash
bid Set (HeaderHash Block)
Set TestHeaderHash
bids)
-> Tag -> Either Tag EventPred
forall a b. a -> Either a b
Left Tag
TagGarbageCollect
(Maybe SlotNo
_, Success
_, Corruption Corruptions
_)
-> EventPred -> Either Tag EventPred
forall a b. b -> Either a b
Right (EventPred -> Either Tag EventPred)
-> EventPred -> Either Tag EventPred
forall a b. (a -> b) -> a -> b
$ Bool -> Set (HeaderHash Block) -> Maybe SlotNo -> EventPred
tagGarbageCollect Bool
False Set (HeaderHash Block)
bids Maybe SlotNo
mbGCed
(Maybe SlotNo, Success, Cmd)
_ -> EventPred -> Either Tag EventPred
forall a b. b -> Either a b
Right (EventPred -> Either Tag EventPred)
-> EventPred -> Either Tag EventPred
forall a b. (a -> b) -> a -> b
$ Bool -> Set (HeaderHash Block) -> Maybe SlotNo -> EventPred
tagGarbageCollect Bool
True Set (HeaderHash Block)
bids Maybe SlotNo
mbGCed
tagGetJust :: Either Tag EventPred -> EventPred
tagGetJust :: Either Tag EventPred -> EventPred
tagGetJust Either Tag EventPred
next = (Event Symbolic -> Success -> Either Tag EventPred) -> EventPred
successful ((Event Symbolic -> Success -> Either Tag EventPred) -> EventPred)
-> (Event Symbolic -> Success -> Either Tag EventPred) -> EventPred
forall a b. (a -> b) -> a -> b
$ \Event Symbolic
_ev Success
suc -> case Success
suc of
MbAllComponents (Just AllComponents Block
_) -> Either Tag EventPred
next
Success
_ -> EventPred -> Either Tag EventPred
forall a b. b -> Either a b
Right (EventPred -> Either Tag EventPred)
-> EventPred -> Either Tag EventPred
forall a b. (a -> b) -> a -> b
$ Either Tag EventPred -> EventPred
tagGetJust Either Tag EventPred
next
tagReOpen :: Bool -> Either Tag EventPred -> EventPred
tagReOpen :: Bool -> Either Tag EventPred -> EventPred
tagReOpen Bool
hasClosed Either Tag EventPred
next = (Event Symbolic -> Success -> Either Tag EventPred) -> EventPred
successful ((Event Symbolic -> Success -> Either Tag EventPred) -> EventPred)
-> (Event Symbolic -> Success -> Either Tag EventPred) -> EventPred
forall a b. (a -> b) -> a -> b
$ \Event Symbolic
ev Success
_ ->
case (Bool
hasClosed, Event Symbolic -> Cmd
forall (r :: * -> *). Event r -> Cmd
getCmd Event Symbolic
ev) of
(Bool
True, Cmd
ReOpen) -> Either Tag EventPred
next
(Bool
False, Cmd
Close) -> EventPred -> Either Tag EventPred
forall a b. b -> Either a b
Right (EventPred -> Either Tag EventPred)
-> EventPred -> Either Tag EventPred
forall a b. (a -> b) -> a -> b
$ Bool -> Either Tag EventPred -> EventPred
tagReOpen Bool
True Either Tag EventPred
next
(Bool
False, Corruption Corruptions
_) -> EventPred -> Either Tag EventPred
forall a b. b -> Either a b
Right (EventPred -> Either Tag EventPred)
-> EventPred -> Either Tag EventPred
forall a b. (a -> b) -> a -> b
$ Bool -> Either Tag EventPred -> EventPred
tagReOpen Bool
True Either Tag EventPred
next
(Bool, Cmd)
_ -> EventPred -> Either Tag EventPred
forall a b. b -> Either a b
Right (EventPred -> Either Tag EventPred)
-> EventPred -> Either Tag EventPred
forall a b. (a -> b) -> a -> b
$ Bool -> Either Tag EventPred -> EventPred
tagReOpen Bool
hasClosed Either Tag EventPred
next
tagCorruptWriteFile :: EventPred
tagCorruptWriteFile :: EventPred
tagCorruptWriteFile = (Event Symbolic -> Success -> Either Tag EventPred) -> EventPred
successful ((Event Symbolic -> Success -> Either Tag EventPred) -> EventPred)
-> (Event Symbolic -> Success -> Either Tag EventPred) -> EventPred
forall a b. (a -> b) -> a -> b
$ \Event Symbolic
ev Success
_ -> case Event Symbolic -> Cmd
forall (r :: * -> *). Event r -> Cmd
getCmd Event Symbolic
ev of
Corruption Corruptions
cors
| let currentFile :: FsPath
currentFile = DBModel Block -> FsPath
forall blk. DBModel blk -> FsPath
getCurrentFile (DBModel Block -> FsPath) -> DBModel Block -> FsPath
forall a b. (a -> b) -> a -> b
$ Model Symbolic -> DBModel Block
forall (r :: * -> *). Model r -> DBModel Block
dbModel (Model Symbolic -> DBModel Block)
-> Model Symbolic -> DBModel Block
forall a b. (a -> b) -> a -> b
$ Event Symbolic -> Model Symbolic
forall (r :: * -> *). Event r -> Model r
eventBefore Event Symbolic
ev
, ((FileCorruption, FsPath) -> Bool) -> Corruptions -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (FsPath -> (FileCorruption, FsPath) -> Bool
forall {a}. Eq a => a -> (FileCorruption, a) -> Bool
currentFileGotCorrupted FsPath
currentFile) Corruptions
cors
-> Tag -> Either Tag EventPred
forall a b. a -> Either a b
Left Tag
TagCorruptWriteFile
Cmd
_ -> EventPred -> Either Tag EventPred
forall a b. b -> Either a b
Right EventPred
tagCorruptWriteFile
where
currentFileGotCorrupted :: a -> (FileCorruption, a) -> Bool
currentFileGotCorrupted a
currentFile (FileCorruption
cor, a
file)
| FileCorruption
DeleteFile <- FileCorruption
cor
= a
file a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
currentFile
| Bool
otherwise
= Bool
False
tagIsClosedError :: EventPred
tagIsClosedError :: EventPred
tagIsClosedError = (Event Symbolic -> Either Tag EventPred) -> EventPred
forall a b. (a -> Either b (Predicate a b)) -> Predicate a b
C.predicate ((Event Symbolic -> Either Tag EventPred) -> EventPred)
-> (Event Symbolic -> Either Tag EventPred) -> EventPred
forall a b. (a -> b) -> a -> b
$ \Event Symbolic
ev -> case Event Symbolic -> Resp
forall (r :: * -> *). Event r -> Resp
eventMockResp Event Symbolic
ev of
Resp (Left (ApiMisuse (ClosedDBError Maybe SomeException
_))) -> Tag -> Either Tag EventPred
forall a b. a -> Either a b
Left Tag
TagClosedError
Resp
_ -> EventPred -> Either Tag EventPred
forall a b. b -> Either a b
Right EventPred
tagIsClosedError
tagGarbageCollectThenReOpen :: EventPred
tagGarbageCollectThenReOpen :: EventPred
tagGarbageCollectThenReOpen = (Event Symbolic -> Success -> Either Tag EventPred) -> EventPred
successful ((Event Symbolic -> Success -> Either Tag EventPred) -> EventPred)
-> (Event Symbolic -> Success -> Either Tag EventPred) -> EventPred
forall a b. (a -> b) -> a -> b
$ \Event Symbolic
ev Success
_ -> case Event Symbolic -> Cmd
forall (r :: * -> *). Event r -> Cmd
getCmd Event Symbolic
ev of
GarbageCollect SlotNo
_ -> EventPred -> Either Tag EventPred
forall a b. b -> Either a b
Right (EventPred -> Either Tag EventPred)
-> EventPred -> Either Tag EventPred
forall a b. (a -> b) -> a -> b
$ Bool -> Either Tag EventPred -> EventPred
tagReOpen Bool
False (Either Tag EventPred -> EventPred)
-> Either Tag EventPred -> EventPred
forall a b. (a -> b) -> a -> b
$
Tag -> Either Tag EventPred
forall a b. a -> Either a b
Left Tag
TagGarbageCollectThenReOpen
Cmd
_ -> EventPred -> Either Tag EventPred
forall a b. b -> Either a b
Right (EventPred -> Either Tag EventPred)
-> EventPred -> Either Tag EventPred
forall a b. (a -> b) -> a -> b
$ EventPred
tagGarbageCollectThenReOpen
getCmd :: Event r -> Cmd
getCmd :: forall (r :: * -> *). Event r -> Cmd
getCmd Event r
ev = CmdErr -> Cmd
cmd (CmdErr -> Cmd) -> CmdErr -> Cmd
forall a b. (a -> b) -> a -> b
$ At CmdErr r -> CmdErr
forall t (r :: * -> *). At t r -> t
unAt (Event r -> At CmdErr r
forall (r :: * -> *). Event r -> At CmdErr r
eventCmd Event r
ev)
isMemberTrue :: [Event Symbolic] -> Int
isMemberTrue :: [Event Symbolic] -> Int
isMemberTrue [Event Symbolic]
events = [Int] -> Int
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ([Int] -> Int) -> [Int] -> Int
forall a b. (a -> b) -> a -> b
$ Event Symbolic -> Int
count (Event Symbolic -> Int) -> [Event Symbolic] -> [Int]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Event Symbolic]
events
where
count :: Event Symbolic -> Int
count :: Event Symbolic -> Int
count Event Symbolic
e = case Event Symbolic -> Resp
forall (r :: * -> *). Event r -> Resp
eventMockResp Event Symbolic
e of
Resp (Left VolatileDBError Block
_) -> Int
0
Resp (Right (BlockInfos [Maybe (BlockInfo Block)]
ls)) -> [BlockInfo Block] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([BlockInfo Block] -> Int) -> [BlockInfo Block] -> Int
forall a b. (a -> b) -> a -> b
$ [Maybe (BlockInfo Block)] -> [BlockInfo Block]
forall a. [Maybe a] -> [a]
catMaybes [Maybe (BlockInfo Block)]
ls
Resp (Right Success
_) -> Int
0
data Tag =
TagGetJust
| TagGetNothing
| TagGetReOpenGet
| TagReOpenGet
| TagGarbageCollect
| TagCorruptWriteFile
| TagEmpty
| TagClosedError
| TagGarbageCollectThenReOpen
deriving Int -> Tag -> ShowS
[Tag] -> ShowS
Tag -> String
(Int -> Tag -> ShowS)
-> (Tag -> String) -> ([Tag] -> ShowS) -> Show Tag
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Tag -> ShowS
showsPrec :: Int -> Tag -> ShowS
$cshow :: Tag -> String
show :: Tag -> String
$cshowList :: [Tag] -> ShowS
showList :: [Tag] -> ShowS
Show
tagSimulatedErrors :: [Event Symbolic] -> [String]
tagSimulatedErrors :: [Event Symbolic] -> [String]
tagSimulatedErrors [Event Symbolic]
events = (Event Symbolic -> String) -> [Event Symbolic] -> [String]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Event Symbolic -> String
tagError [Event Symbolic]
events
where
tagError :: Event Symbolic -> String
tagError :: Event Symbolic -> String
tagError Event Symbolic
ev = case Event Symbolic -> At CmdErr Symbolic
forall (r :: * -> *). Event r -> At CmdErr r
eventCmd Event Symbolic
ev of
At (CmdErr Cmd
_ Maybe Errors
Nothing) -> String
"NoError"
At (CmdErr Cmd
cmd Maybe Errors
_) -> At Cmd Any -> String
forall k (cmd :: k -> *) (r :: k).
CommandNames cmd =>
cmd r -> String
forall (r :: * -> *). At Cmd r -> String
cmdName (Cmd -> At Cmd Any
forall t (r :: * -> *). t -> At t r
At Cmd
cmd) String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
" Error"
tagFilterByPredecessor :: [Event Symbolic] -> [String]
tagFilterByPredecessor :: [Event Symbolic] -> [String]
tagFilterByPredecessor = (Event Symbolic -> Maybe String) -> [Event Symbolic] -> [String]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Event Symbolic -> Maybe String
f
where
f :: Event Symbolic -> Maybe String
f :: Event Symbolic -> Maybe String
f Event Symbolic
ev = case (Event Symbolic -> Cmd
forall (r :: * -> *). Event r -> Cmd
getCmd Event Symbolic
ev, Event Symbolic -> Resp
forall (r :: * -> *). Event r -> Resp
eventMockResp Event Symbolic
ev) of
(FilterByPredecessor [ChainHash Block]
_pid, Resp (Right (Successors [Set (HeaderHash Block)]
st))) ->
if (Set TestHeaderHash -> Bool) -> [Set TestHeaderHash] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Set TestHeaderHash -> Bool
forall a. Set a -> Bool
Set.null [Set (HeaderHash Block)]
[Set TestHeaderHash]
st then String -> Maybe String
forall a. a -> Maybe a
Just String
"Empty Successors"
else String -> Maybe String
forall a. a -> Maybe a
Just String
"Non empty Successors"
(Cmd, Resp)
_otherwise -> Maybe String
forall a. Maybe a
Nothing
execCmd :: Model Symbolic
-> Command (At CmdErr) (At Resp)
-> Event Symbolic
execCmd :: Model Symbolic -> Command (At CmdErr) (At Resp) -> Event Symbolic
execCmd Model Symbolic
model (Command At CmdErr Symbolic
cmdErr At Resp Symbolic
_resp [Var]
_vars) = Model Symbolic -> At CmdErr Symbolic -> Event Symbolic
forall (r :: * -> *). Model r -> At CmdErr r -> Event r
lockstep Model Symbolic
model At CmdErr Symbolic
cmdErr
execCmds :: Model Symbolic -> Commands (At CmdErr) (At Resp) -> [Event Symbolic]
execCmds :: Model Symbolic
-> Commands (At CmdErr) (At Resp) -> [Event Symbolic]
execCmds Model Symbolic
model (Commands [Command (At CmdErr) (At Resp)]
cs) = Model Symbolic
-> [Command (At CmdErr) (At Resp)] -> [Event Symbolic]
go Model Symbolic
model [Command (At CmdErr) (At Resp)]
cs
where
go :: Model Symbolic -> [Command (At CmdErr) (At Resp)] -> [Event Symbolic]
go :: Model Symbolic
-> [Command (At CmdErr) (At Resp)] -> [Event Symbolic]
go Model Symbolic
_ [] = []
go Model Symbolic
m (Command (At CmdErr) (At Resp)
c : [Command (At CmdErr) (At Resp)]
css) = let ev :: Event Symbolic
ev = Model Symbolic -> Command (At CmdErr) (At Resp) -> Event Symbolic
execCmd Model Symbolic
m Command (At CmdErr) (At Resp)
c in Event Symbolic
ev Event Symbolic -> [Event Symbolic] -> [Event Symbolic]
forall a. a -> [a] -> [a]
: Model Symbolic
-> [Command (At CmdErr) (At Resp)] -> [Event Symbolic]
go (Event Symbolic -> Model Symbolic
forall (r :: * -> *). Event r -> Model r
eventAfter Event Symbolic
ev) [Command (At CmdErr) (At Resp)]
css
showLabelledExamples :: IO ()
showLabelledExamples :: IO ()
showLabelledExamples = Maybe Int -> Int -> IO ()
showLabelledExamples' Maybe Int
forall a. Maybe a
Nothing Int
1000
showLabelledExamples' :: Maybe Int
-> Int
-> IO ()
showLabelledExamples' :: Maybe Int -> Int -> IO ()
showLabelledExamples' Maybe Int
mReplay Int
numTests = do
Int
replaySeed <- case Maybe Int
mReplay of
Maybe Int
Nothing -> (StdGen -> (Int, StdGen)) -> IO Int
forall (m :: * -> *) a. MonadIO m => (StdGen -> (a, StdGen)) -> m a
getStdRandom ((Int, Int) -> StdGen -> (Int, StdGen)
forall g. RandomGen g => (Int, Int) -> g -> (Int, g)
forall a g. (Random a, RandomGen g) => (a, a) -> g -> (a, g)
randomR (Int
1,Int
999999))
Just Int
seed -> Int -> IO Int
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return Int
seed
Args -> Property -> IO ()
forall prop. Testable prop => Args -> prop -> IO ()
labelledExamplesWith (Args
stdArgs { replay = Just (mkQCGen replaySeed, 0)
, maxSuccess = numTests
}) (Property -> IO ()) -> Property -> IO ()
forall a b. (a -> b) -> a -> b
$
Gen (Commands (At CmdErr) (At Resp))
-> (Commands (At CmdErr) (At Resp)
-> [Commands (At CmdErr) (At Resp)])
-> (Commands (At CmdErr) (At Resp) -> String)
-> (Commands (At CmdErr) (At Resp) -> Property)
-> Property
forall prop a.
Testable prop =>
Gen a -> (a -> [a]) -> (a -> String) -> (a -> prop) -> Property
forAllShrinkShow (StateMachine Model (At CmdErr) IO (At Resp)
-> Maybe Int -> Gen (Commands (At CmdErr) (At Resp))
forall (resp :: (* -> *) -> *) (model :: (* -> *) -> *)
(cmd :: (* -> *) -> *) (m :: * -> *).
(Foldable resp, Show (model Symbolic), Show (cmd Symbolic),
Show (resp Symbolic)) =>
StateMachine model cmd m resp
-> Maybe Int -> Gen (Commands cmd resp)
QSM.generateCommands StateMachine Model (At CmdErr) IO (At Resp)
smUnused Maybe Int
forall a. Maybe a
Nothing)
(StateMachine Model (At CmdErr) IO (At Resp)
-> Commands (At CmdErr) (At Resp)
-> [Commands (At CmdErr) (At Resp)]
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
(Traversable cmd, Foldable resp) =>
StateMachine model cmd m resp
-> Commands cmd resp -> [Commands cmd resp]
QSM.shrinkCommands StateMachine Model (At CmdErr) IO (At Resp)
smUnused)
Commands (At CmdErr) (At Resp) -> String
forall a. Show a => a -> String
ppShow ((Commands (At CmdErr) (At Resp) -> Property) -> Property)
-> (Commands (At CmdErr) (At Resp) -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \Commands (At CmdErr) (At Resp)
cmds ->
[Tag] -> Property -> Property
forall a. Show a => [a] -> Property -> Property
collects ([Event Symbolic] -> [Tag]
tag ([Event Symbolic] -> [Tag])
-> (Commands (At CmdErr) (At Resp) -> [Event Symbolic])
-> Commands (At CmdErr) (At Resp)
-> [Tag]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Model Symbolic
-> Commands (At CmdErr) (At Resp) -> [Event Symbolic]
execCmds (StateMachine Model (At CmdErr) IO (At Resp)
-> forall {r :: * -> *}. Model r
forall (model :: (* -> *) -> *) (cmd :: (* -> *) -> *)
(m :: * -> *) (resp :: (* -> *) -> *).
StateMachine model cmd m resp -> forall (r :: * -> *). model r
initModel StateMachine Model (At CmdErr) IO (At Resp)
smUnused) (Commands (At CmdErr) (At Resp) -> [Tag])
-> Commands (At CmdErr) (At Resp) -> [Tag]
forall a b. (a -> b) -> a -> b
$ Commands (At CmdErr) (At Resp)
cmds) (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
Bool -> Property
forall prop. Testable prop => prop -> Property
property Bool
True
where
dbm :: DBModel Block
dbm = BlocksPerFile -> CodecConfig Block -> DBModel Block
forall blk. BlocksPerFile -> CodecConfig blk -> DBModel blk
initDBModel BlocksPerFile
testMaxBlocksPerFile CodecConfig Block
TestBlockCodecConfig
smUnused :: StateMachine Model (At CmdErr) IO (At Resp)
smUnused = VolatileDBEnv
-> DBModel Block -> StateMachine Model (At CmdErr) IO (At Resp)
sm VolatileDBEnv
unusedEnv DBModel Block
dbm