{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}

module Test.Ouroboros.Storage.PerasVoteDB.StateMachine (tests) where

import qualified Cardano.Crypto.DSIGN.Class as SL
import qualified Cardano.Crypto.Seed as SL
import qualified Cardano.Ledger.Keys as SL
import Control.Concurrent.Class.MonadSTM (MonadSTM (..))
import Control.Monad (join)
import Control.Monad.Class.MonadThrow (MonadCatch (..))
import Control.Monad.State
  ( MonadState (..)
  , MonadTrans (..)
  , StateT
  , evalStateT
  )
import Control.Tracer (nullTracer)
import Data.Char (chr)
import Data.Functor (($>))
import qualified Data.List.NonEmpty as NE
import qualified Data.Map as Map
import Data.Map.Strict (Map)
import Data.Ratio ((%))
import Data.Set (Set)
import qualified Data.Set as Set
import Data.String (IsString (..))
import Data.Word (Word64)
import GHC.Generics (Generic)
import Ouroboros.Consensus.Block.Abstract (Point (..), SlotNo (..))
import Ouroboros.Consensus.Block.SupportsPeras
  ( BlockSupportsPeras (..)
  , HasPerasVoteBlock (..)
  , HasPerasVoteRound (..)
  , PerasRoundNo (..)
  , PerasVote (..)
  , PerasVoteId
  , PerasVoteStake (..)
  , PerasVoteTarget (..)
  , PerasVoterId (..)
  , ValidatedPerasCert
  , ValidatedPerasVote (..)
  , mkPerasParams
  )
import Ouroboros.Consensus.BlockchainTime.WallClock.Types
  ( RelativeTime (..)
  , WithArrivalTime (..)
  )
import Ouroboros.Consensus.Storage.PerasVoteDB
  ( AddPerasVoteResult (..)
  , PerasVoteDB
  , PerasVoteDbError
  , PerasVoteTicketNo
  )
import qualified Ouroboros.Consensus.Storage.PerasVoteDB as PerasVoteDB
import Ouroboros.Consensus.Storage.PerasVoteDB.Impl (PerasVoteDbError (..))
import Ouroboros.Consensus.Util.Orphans ()
import Test.Cardano.Ledger.Binary.Arbitrary ()
import Test.Ouroboros.Storage.Orphans ()
import qualified Test.Ouroboros.Storage.PerasVoteDB.Model as Model
import Test.QuickCheck
  ( Arbitrary (..)
  , Property
  , choose
  , elements
  , frequency
  , ioProperty
  , tabulate
  )
import Test.QuickCheck.Monadic (PropertyM, monadic)
import Test.QuickCheck.StateModel
  ( Actions
  , Any (..)
  , HasVariables (..)
  , RunModel (..)
  , StateModel (..)
  , counterexamplePost
  , runActions
  )
import Test.Tasty (TestTree, testGroup)
import Test.Tasty.QuickCheck (testProperty)
import Test.Util.TestBlock (TestBlock, TestHash (..))
import Test.Util.TestEnv (adjustQuickCheckMaxSize, adjustQuickCheckTests)

tests :: TestTree
tests :: TestTree
tests =
  TestName -> [TestTree] -> TestTree
testGroup
    TestName
"PerasVoteDB"
    [ (Int -> Int) -> TestTree -> TestTree
adjustQuickCheckMaxSize (Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
5) (TestTree -> TestTree) -> TestTree -> TestTree
forall a b. (a -> b) -> a -> b
$
        (Int -> Int) -> TestTree -> TestTree
adjustQuickCheckTests (Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
10) (TestTree -> TestTree) -> TestTree -> TestTree
forall a b. (a -> b) -> a -> b
$
          TestName -> (Actions Model -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"q-d" ((Actions Model -> Property) -> TestTree)
-> (Actions Model -> Property) -> TestTree
forall a b. (a -> b) -> a -> b
$
            Actions Model -> Property
prop_qd
    ]

perasTestCfg :: PerasCfg TestBlock
perasTestCfg :: PerasCfg TestBlock
perasTestCfg = PerasParams
PerasCfg TestBlock
mkPerasParams

prop_qd :: Actions Model -> Property
prop_qd :: Actions Model -> Property
prop_qd Actions Model
actions = (StateT (PerasVoteDB IO TestBlock) IO Property -> Property)
-> PropertyM (StateT (PerasVoteDB IO TestBlock) IO) () -> Property
forall a (m :: * -> *).
(Testable a, Monad m) =>
(m Property -> Property) -> PropertyM m a -> Property
monadic StateT (PerasVoteDB IO TestBlock) IO Property -> Property
runActualImplemMonad PropertyM (StateT (PerasVoteDB IO TestBlock) IO) ()
resultAsPropertyM
 where
  -- This runs actions on the model and the actual implementation alongside,
  -- and checks the postconditions after each action.
  -- The `PropertyM` wrapper is keeping track of success/failure of the
  -- postconditions, so we don't care about the payload returned by `runActions`.
  resultAsPropertyM :: PropertyM (StateT (PerasVoteDB IO TestBlock) IO) ()
  resultAsPropertyM :: PropertyM (StateT (PerasVoteDB IO TestBlock) IO) ()
resultAsPropertyM = Actions Model
-> PropertyM
     (StateT (PerasVoteDB IO TestBlock) IO) (Annotated Model, Env)
forall state (m :: * -> *) e.
(StateModel state, RunModel state m, e ~ Error state m,
 forall a. IsPerformResult e a) =>
Actions state -> PropertyM m (Annotated state, Env)
runActions Actions Model
actions PropertyM
  (StateT (PerasVoteDB IO TestBlock) IO) (Annotated Model, Env)
-> () -> PropertyM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall (f :: * -> *) a b. Functor f => f a -> b -> f b
$> ()

  -- This function is in charge of collapsing/running the different monadic
  -- layers on top of our property.
  runActualImplemMonad :: StateT (PerasVoteDB IO TestBlock) IO Property -> Property
  runActualImplemMonad :: StateT (PerasVoteDB IO TestBlock) IO Property -> Property
runActualImplemMonad StateT (PerasVoteDB IO TestBlock) IO Property
statefulIoProp =
    -- The _Model_ starts in `Model.open = False`, so `precondition` dictates
    -- that the first action must be `CreateDB`, and this `CreateDB` action will
    -- initialize the `StateT` state with a valid `PerasVoteDB` instance.
    -- The actual implementation state can only be read in `postcondition`, so
    -- we are sure that the `StateT` state will be properly initialized beforehand.
    let ioProp :: IO Property
ioProp = StateT (PerasVoteDB IO TestBlock) IO Property
-> PerasVoteDB IO TestBlock -> IO Property
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT StateT (PerasVoteDB IO TestBlock) IO Property
statefulIoProp (TestName -> PerasVoteDB IO TestBlock
forall a. HasCallStack => TestName -> a
error TestName
"Trying to access uninitialized PerasVoteDB")
     in IO Property -> Property
forall prop. Testable prop => IO prop -> Property
ioProperty IO Property
ioProp

newtype Model = Model (Model.Model TestBlock)
  deriving (Int -> Model -> ShowS
[Model] -> ShowS
Model -> TestName
(Int -> Model -> ShowS)
-> (Model -> TestName) -> ([Model] -> ShowS) -> Show Model
forall a.
(Int -> a -> ShowS) -> (a -> TestName) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Model -> ShowS
showsPrec :: Int -> Model -> ShowS
$cshow :: Model -> TestName
show :: Model -> TestName
$cshowList :: [Model] -> ShowS
showList :: [Model] -> ShowS
Show, (forall x. Model -> Rep Model x)
-> (forall x. Rep Model x -> Model) -> Generic Model
forall x. Rep Model x -> Model
forall x. Model -> Rep Model x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Model -> Rep Model x
from :: forall x. Model -> Rep Model x
$cto :: forall x. Rep Model x -> Model
to :: forall x. Rep Model x -> Model
Generic)

instance StateModel Model where
  data Action Model a where
    CreateDB ::
      Action Model ()
    AddVote ::
      WithArrivalTime (ValidatedPerasVote TestBlock) ->
      Action
        Model
        ( Either
            (PerasVoteDbError TestBlock)
            (AddPerasVoteResult TestBlock)
        )
    GetVoteIds ::
      Action Model (Set (PerasVoteId TestBlock))
    GetVotesAfter ::
      PerasVoteTicketNo ->
      Action
        Model
        ( Map
            PerasVoteTicketNo
            (WithArrivalTime (ValidatedPerasVote TestBlock))
        )
    GetForgedCertForRound ::
      PerasRoundNo ->
      Action Model (Maybe (ValidatedPerasCert TestBlock))
    GarbageCollect ::
      PerasRoundNo ->
      Action Model ()

  arbitraryAction :: VarContext -> Model -> Gen (Any (Action Model))
arbitraryAction VarContext
_ (Model Model TestBlock
m)
    | Bool -> Bool
not (Model TestBlock -> Bool
forall blk. Model blk -> Bool
Model.open Model TestBlock
m) =
        Action Model () -> Any (Action Model)
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some (Action Model () -> Any (Action Model))
-> Gen (Action Model ()) -> Gen (Any (Action Model))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (Action Model ())
genCreateDB
    | Bool
otherwise =
        [(Int, Gen (Any (Action Model)))] -> Gen (Any (Action Model))
forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency
          [ (Int
1000, Action
  Model
  (Either
     (PerasVoteDbError TestBlock) (AddPerasVoteResult TestBlock))
-> Any (Action Model)
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some (Action
   Model
   (Either
      (PerasVoteDbError TestBlock) (AddPerasVoteResult TestBlock))
 -> Any (Action Model))
-> Gen
     (Action
        Model
        (Either
           (PerasVoteDbError TestBlock) (AddPerasVoteResult TestBlock)))
-> Gen (Any (Action Model))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen
  (Action
     Model
     (Either
        (PerasVoteDbError TestBlock) (AddPerasVoteResult TestBlock)))
genAddVote)
          , (Int
10, Action Model (Set (PerasVoteId TestBlock)) -> Any (Action Model)
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some (Action Model (Set (PerasVoteId TestBlock)) -> Any (Action Model))
-> Gen (Action Model (Set (PerasVoteId TestBlock)))
-> Gen (Any (Action Model))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (Action Model (Set (PerasVoteId TestBlock)))
genGetVoteIds)
          , (Int
10, Action
  Model
  (Map
     PerasVoteTicketNo (WithArrivalTime (ValidatedPerasVote TestBlock)))
-> Any (Action Model)
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some (Action
   Model
   (Map
      PerasVoteTicketNo (WithArrivalTime (ValidatedPerasVote TestBlock)))
 -> Any (Action Model))
-> Gen
     (Action
        Model
        (Map
           PerasVoteTicketNo
           (WithArrivalTime (ValidatedPerasVote TestBlock))))
-> Gen (Any (Action Model))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen
  (Action
     Model
     (Map
        PerasVoteTicketNo
        (WithArrivalTime (ValidatedPerasVote TestBlock))))
genGetVotesAfter)
          , (Int
5, Action Model (Maybe (ValidatedPerasCert TestBlock))
-> Any (Action Model)
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some (Action Model (Maybe (ValidatedPerasCert TestBlock))
 -> Any (Action Model))
-> Gen (Action Model (Maybe (ValidatedPerasCert TestBlock)))
-> Gen (Any (Action Model))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (Action Model (Maybe (ValidatedPerasCert TestBlock)))
genGetForgedCertForRound)
          , (Int
2, Action Model () -> Any (Action Model)
forall a (f :: * -> *). (Typeable a, Eq (f a)) => f a -> Any f
Some (Action Model () -> Any (Action Model))
-> Gen (Action Model ()) -> Gen (Any (Action Model))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (Action Model ())
genGarbageCollect)
          ]
   where
    genCreateDB :: Gen (Action Model ())
genCreateDB = do
      Action Model () -> Gen (Action Model ())
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Action Model ()
CreateDB

    genAddVote :: Gen
  (Action
     Model
     (Either
        (PerasVoteDbError TestBlock) (AddPerasVoteResult TestBlock)))
genAddVote = do
      roundNo <- Gen PerasRoundNo
genRoundNo
      point <- genPoint
      voterId <- genVoterId
      stake <- genVoteStake
      now <- genRelativeTime
      let voteWithTime =
            RelativeTime
-> ValidatedPerasVote TestBlock
-> WithArrivalTime (ValidatedPerasVote TestBlock)
forall a. RelativeTime -> a -> WithArrivalTime a
WithArrivalTime RelativeTime
now (ValidatedPerasVote TestBlock
 -> WithArrivalTime (ValidatedPerasVote TestBlock))
-> ValidatedPerasVote TestBlock
-> WithArrivalTime (ValidatedPerasVote TestBlock)
forall a b. (a -> b) -> a -> b
$
              ValidatedPerasVote
                { vpvVote :: PerasVote TestBlock
vpvVote =
                    PerasVote
                      { pvVoteRound :: PerasRoundNo
pvVoteRound = PerasRoundNo
roundNo
                      , pvVoteBlock :: Point TestBlock
pvVoteBlock = Point TestBlock
point
                      , pvVoteVoterId :: PerasVoterId
pvVoteVoterId = PerasVoterId
voterId
                      }
                , vpvVoteStake :: PerasVoteStake
vpvVoteStake = PerasVoteStake
stake
                }
      return (AddVote voteWithTime)

    genGetVoteIds :: Gen (Action Model (Set (PerasVoteId TestBlock)))
genGetVoteIds = do
      Action Model (Set (PerasVoteId TestBlock))
-> Gen (Action Model (Set (PerasVoteId TestBlock)))
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Action Model (Set (PerasVoteId TestBlock))
GetVoteIds

    genGetVotesAfter :: Gen
  (Action
     Model
     (Map
        PerasVoteTicketNo
        (WithArrivalTime (ValidatedPerasVote TestBlock))))
genGetVotesAfter = do
      ticketNo <- Int -> PerasVoteTicketNo
forall a. Enum a => Int -> a
toEnum (Int -> PerasVoteTicketNo) -> Gen Int -> Gen PerasVoteTicketNo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Int, Int) -> Gen Int
forall a. Random a => (a, a) -> Gen a
choose (Int
0, PerasVoteTicketNo -> Int
forall a. Enum a => a -> Int
fromEnum (Model TestBlock -> PerasVoteTicketNo
forall blk. Model blk -> PerasVoteTicketNo
Model.lastTicketNo Model TestBlock
m) Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
      pure (GetVotesAfter ticketNo)

    genGetForgedCertForRound :: Gen (Action Model (Maybe (ValidatedPerasCert TestBlock)))
genGetForgedCertForRound = do
      roundNo <- Gen PerasRoundNo
genRoundNo
      pure (GetForgedCertForRound roundNo)

    genGarbageCollect :: Gen (Action Model ())
genGarbageCollect = do
      roundNo <- Gen PerasRoundNo
genRoundNo
      pure (GarbageCollect roundNo)

    genPoint :: Gen (Point TestBlock)
genPoint = do
      [(Int, Gen (Point TestBlock))] -> Gen (Point TestBlock)
forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency
        [
          ( Int
1
          , Point TestBlock -> Gen (Point TestBlock)
forall a. a -> Gen a
forall (m :: * -> *) a. Monad m => a -> m a
return Point TestBlock
forall {k} (block :: k). Point block
GenesisPoint
          )
        ,
          ( Int
50
          , do
              slotNo <- Word64 -> SlotNo
SlotNo (Word64 -> SlotNo) -> Gen Word64 -> Gen SlotNo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Random a => (a, a) -> Gen a
choose @Word64 (Word64
0, Word64
9)
              hash <- TestHash <$> NE.fromList . pure <$> choose (0, 9)
              return (BlockPoint slotNo hash)
          )
        ]

    genRoundNo :: Gen PerasRoundNo
genRoundNo = do
      n <- forall a. Random a => (a, a) -> Gen a
choose @Word64 (Word64
0, Word64
9)
      pure (PerasRoundNo n)

    genVoterId :: Gen PerasVoterId
genVoterId = do
      -- We want to force collisions when adding votes, so we need to restrict
      -- the key space a lot here. Otherwise we might never hit the case where
      -- the same voter casts two votes for the same round/block.
      let mkVoterKey :: Char -> ByteString
mkVoterKey = TestName -> ByteString
forall a. IsString a => TestName -> a
fromString (TestName -> ByteString)
-> (Char -> TestName) -> Char -> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Char -> TestName
forall a. Int -> a -> [a]
replicate Int
32
      bytes <- Char -> ByteString
mkVoterKey (Char -> ByteString) -> Gen Char -> Gen ByteString
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TestName -> Gen Char
forall a. HasCallStack => [a] -> Gen a
elements [Int -> Char
chr Int
c | Int
c <- [Int
0 .. Int
99]]
      let signKey = Seed -> SignKeyDSIGN DSIGN
forall v. DSIGNAlgorithm v => Seed -> SignKeyDSIGN v
SL.genKeyDSIGN (ByteString -> Seed
SL.mkSeedFromBytes ByteString
bytes)
      let verKey = SignKeyDSIGN DSIGN -> VerKeyDSIGN DSIGN
forall v. DSIGNAlgorithm v => SignKeyDSIGN v -> VerKeyDSIGN v
SL.deriveVerKeyDSIGN SignKeyDSIGN DSIGN
signKey
      let keyHash = VKey StakePool -> KeyHash StakePool
forall (kd :: KeyRole). VKey kd -> KeyHash kd
SL.hashKey (VerKeyDSIGN DSIGN -> VKey StakePool
forall (kd :: KeyRole). VerKeyDSIGN DSIGN -> VKey kd
SL.VKey VerKeyDSIGN DSIGN
verKey)
      pure (PerasVoterId keyHash)

    genVoteStake :: Gen PerasVoteStake
genVoteStake = do
      -- Make it so that we always require multiple votes to reach a quorum.
      -- This is assumming a quorum threshold strictly larger than 50%, which is
      -- a very conservative assumption for Peras.
      stake <- (Integer
1 Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
%) (Integer -> Rational) -> Gen Integer -> Gen Rational
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Integer, Integer) -> Gen Integer
forall a. Random a => (a, a) -> Gen a
choose (Integer
2, Integer
10) -- stake between 1/2 and 1/10
      pure (PerasVoteStake stake)

    genRelativeTime :: Gen RelativeTime
genRelativeTime = do
      time <- Word64 -> NominalDiffTime
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Word64 -> NominalDiffTime) -> Gen Word64 -> Gen NominalDiffTime
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Arbitrary a => Gen a
arbitrary @Word64
      pure (RelativeTime time)

  initialState :: Model
initialState =
    Model TestBlock -> Model
Model (PerasCfg TestBlock -> Model TestBlock
forall blk. PerasCfg blk -> Model blk
Model.initModel PerasCfg TestBlock
perasTestCfg)

  nextState :: forall a. Typeable a => Model -> Action Model a -> Var a -> Model
nextState (Model Model TestBlock
m) Action Model a
action Var a
_ =
    case Action Model a
action of
      Action Model a
R:ActionModela a
CreateDB -> Model TestBlock -> Model
Model (Model TestBlock -> Model) -> Model TestBlock -> Model
forall a b. (a -> b) -> a -> b
$ Model TestBlock -> Model TestBlock
forall blk. Model blk -> Model blk
Model.openDB Model TestBlock
m
      AddVote WithArrivalTime (ValidatedPerasVote TestBlock)
vote -> Model TestBlock -> Model
Model (Model TestBlock -> Model) -> Model TestBlock -> Model
forall a b. (a -> b) -> a -> b
$ (Either PerasVoteDbModelError (AddPerasVoteResult TestBlock),
 Model TestBlock)
-> Model TestBlock
forall a b. (a, b) -> b
snd ((Either PerasVoteDbModelError (AddPerasVoteResult TestBlock),
  Model TestBlock)
 -> Model TestBlock)
-> (Either PerasVoteDbModelError (AddPerasVoteResult TestBlock),
    Model TestBlock)
-> Model TestBlock
forall a b. (a -> b) -> a -> b
$ WithArrivalTime (ValidatedPerasVote TestBlock)
-> Model TestBlock
-> (Either PerasVoteDbModelError (AddPerasVoteResult TestBlock),
    Model TestBlock)
forall blk.
StandardHash blk =>
WithArrivalTime (ValidatedPerasVote blk)
-> Model blk
-> (Either PerasVoteDbModelError (AddPerasVoteResult blk),
    Model blk)
Model.addVote WithArrivalTime (ValidatedPerasVote TestBlock)
vote Model TestBlock
m
      Action Model a
R:ActionModela a
GetVoteIds -> Model TestBlock -> Model
Model (Model TestBlock -> Model) -> Model TestBlock -> Model
forall a b. (a -> b) -> a -> b
$ Model TestBlock
m
      GetVotesAfter PerasVoteTicketNo
_ -> Model TestBlock -> Model
Model (Model TestBlock -> Model) -> Model TestBlock -> Model
forall a b. (a -> b) -> a -> b
$ Model TestBlock
m
      GetForgedCertForRound PerasRoundNo
_ -> Model TestBlock -> Model
Model (Model TestBlock -> Model) -> Model TestBlock -> Model
forall a b. (a -> b) -> a -> b
$ Model TestBlock
m
      GarbageCollect PerasRoundNo
roundNo -> Model TestBlock -> Model
Model (Model TestBlock -> Model) -> Model TestBlock -> Model
forall a b. (a -> b) -> a -> b
$ PerasRoundNo -> Model TestBlock -> Model TestBlock
forall blk. PerasRoundNo -> Model blk -> Model blk
Model.garbageCollect PerasRoundNo
roundNo Model TestBlock
m

  precondition :: forall a. Model -> Action Model a -> Bool
precondition (Model Model TestBlock
m) Action Model a
action =
    case Action Model a
action of
      Action Model a
R:ActionModela a
CreateDB -> Bool -> Bool
not (Model TestBlock -> Bool
forall blk. Model blk -> Bool
Model.open Model TestBlock
m)
      AddVote WithArrivalTime (ValidatedPerasVote TestBlock)
_ -> Model TestBlock -> Bool
forall blk. Model blk -> Bool
Model.open Model TestBlock
m
      Action Model a
R:ActionModela a
GetVoteIds -> Model TestBlock -> Bool
forall blk. Model blk -> Bool
Model.open Model TestBlock
m
      GetVotesAfter PerasVoteTicketNo
_ -> Model TestBlock -> Bool
forall blk. Model blk -> Bool
Model.open Model TestBlock
m
      GetForgedCertForRound PerasRoundNo
_ -> Model TestBlock -> Bool
forall blk. Model blk -> Bool
Model.open Model TestBlock
m
      GarbageCollect PerasRoundNo
_ -> Model TestBlock -> Bool
forall blk. Model blk -> Bool
Model.open Model TestBlock
m

deriving stock instance Show (Action Model a)
deriving stock instance Eq (Action Model a)

instance HasVariables (Action Model a) where
  getAllVariables :: Action Model a -> Set (Any Var)
getAllVariables Action Model a
_ = Set (Any Var)
forall a. Monoid a => a
mempty

instance RunModel Model (StateT (PerasVoteDB IO TestBlock) IO) where
  perform :: forall a.
Typeable a =>
Model
-> Action Model a
-> LookUp
-> StateT
     (PerasVoteDB IO TestBlock)
     IO
     (PerformResult Model (StateT (PerasVoteDB IO TestBlock) IO) a)
perform Model
_ Action Model a
action LookUp
_ =
    case Action Model a
action of
      Action Model a
R:ActionModela a
CreateDB -> do
        let args :: PerasVoteDbArgs Identity IO blk
args = Tracer IO (TraceEvent blk)
-> HKD Identity (PerasCfg blk) -> PerasVoteDbArgs Identity IO blk
forall (f :: * -> *) (m :: * -> *) blk.
Tracer m (TraceEvent blk)
-> HKD f (PerasCfg blk) -> PerasVoteDbArgs f m blk
PerasVoteDB.PerasVoteDbArgs Tracer IO (TraceEvent blk)
forall (m :: * -> *) a. Applicative m => Tracer m a
nullTracer HKD Identity (PerasCfg blk)
PerasCfg TestBlock
perasTestCfg
        voteDB <- IO (PerasVoteDB IO TestBlock)
-> StateT (PerasVoteDB IO TestBlock) IO (PerasVoteDB IO TestBlock)
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (PerasVoteDB IO TestBlock) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (IO (PerasVoteDB IO TestBlock)
 -> StateT (PerasVoteDB IO TestBlock) IO (PerasVoteDB IO TestBlock))
-> IO (PerasVoteDB IO TestBlock)
-> StateT (PerasVoteDB IO TestBlock) IO (PerasVoteDB IO TestBlock)
forall a b. (a -> b) -> a -> b
$ Complete PerasVoteDbArgs IO TestBlock
-> IO (PerasVoteDB IO TestBlock)
forall (m :: * -> *) blk.
(IOLike m, StandardHash blk, Typeable blk) =>
Complete PerasVoteDbArgs m blk -> m (PerasVoteDB m blk)
PerasVoteDB.createDB Complete PerasVoteDbArgs IO TestBlock
forall {blk}. PerasVoteDbArgs Identity IO blk
args
        put voteDB
      AddVote WithArrivalTime (ValidatedPerasVote TestBlock)
vote -> do
        voteDB <- StateT (PerasVoteDB IO TestBlock) IO (PerasVoteDB IO TestBlock)
forall s (m :: * -> *). MonadState s m => m s
get
        lift $ try $ join $ atomically $ PerasVoteDB.addVote voteDB vote
      Action Model a
R:ActionModela a
GetVoteIds -> do
        voteDB <- StateT (PerasVoteDB IO TestBlock) IO (PerasVoteDB IO TestBlock)
forall s (m :: * -> *). MonadState s m => m s
get
        lift $ atomically $ PerasVoteDB.getVoteIds voteDB
      GetVotesAfter PerasVoteTicketNo
ticketNo -> do
        voteDB <- StateT (PerasVoteDB IO TestBlock) IO (PerasVoteDB IO TestBlock)
forall s (m :: * -> *). MonadState s m => m s
get
        lift $ atomically $ PerasVoteDB.getVotesAfter voteDB ticketNo
      GetForgedCertForRound PerasRoundNo
roundNo -> do
        voteDB <- StateT (PerasVoteDB IO TestBlock) IO (PerasVoteDB IO TestBlock)
forall s (m :: * -> *). MonadState s m => m s
get
        lift $ atomically $ PerasVoteDB.getForgedCertForRound voteDB roundNo
      GarbageCollect PerasRoundNo
roundNo -> do
        voteDB <- StateT (PerasVoteDB IO TestBlock) IO (PerasVoteDB IO TestBlock)
forall s (m :: * -> *). MonadState s m => m s
get
        lift $ join $ atomically $ PerasVoteDB.garbageCollect voteDB roundNo

  postcondition :: forall a.
(Model, Model)
-> Action Model a
-> LookUp
-> a
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) Bool
postcondition (Model Model TestBlock
model, Model
_) (AddVote WithArrivalTime (ValidatedPerasVote TestBlock)
vote) LookUp
_ a
actual = do
    let (Either PerasVoteDbModelError (AddPerasVoteResult TestBlock)
expected, Model TestBlock
_) = WithArrivalTime (ValidatedPerasVote TestBlock)
-> Model TestBlock
-> (Either PerasVoteDbModelError (AddPerasVoteResult TestBlock),
    Model TestBlock)
forall blk.
StandardHash blk =>
WithArrivalTime (ValidatedPerasVote blk)
-> Model blk
-> (Either PerasVoteDbModelError (AddPerasVoteResult blk),
    Model blk)
Model.addVote WithArrivalTime (ValidatedPerasVote TestBlock)
vote Model TestBlock
model
    case (Either PerasVoteDbModelError (AddPerasVoteResult TestBlock)
expected, a
actual) of
      (Right AddPerasVoteResult TestBlock
expectedRes, Right AddPerasVoteResult TestBlock
actualRes) -> do
        TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall (m :: * -> *). Monad m => TestName -> PostconditionM m ()
counterexamplePost (TestName
 -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ())
-> TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall a b. (a -> b) -> a -> b
$ TestName
"Mismatched success results:"
        TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall (m :: * -> *). Monad m => TestName -> PostconditionM m ()
counterexamplePost (TestName
 -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ())
-> TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall a b. (a -> b) -> a -> b
$ TestName
"Model: " TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> AddPerasVoteResult TestBlock -> TestName
forall a. Show a => a -> TestName
show AddPerasVoteResult TestBlock
expectedRes
        TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall (m :: * -> *). Monad m => TestName -> PostconditionM m ()
counterexamplePost (TestName
 -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ())
-> TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall a b. (a -> b) -> a -> b
$ TestName
"SUT: " TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> AddPerasVoteResult TestBlock -> TestName
forall a. Show a => a -> TestName
show AddPerasVoteResult TestBlock
actualRes
        Bool -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) Bool
forall a.
a -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool
 -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) Bool)
-> Bool
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) Bool
forall a b. (a -> b) -> a -> b
$ AddPerasVoteResult TestBlock
expectedRes AddPerasVoteResult TestBlock
-> AddPerasVoteResult TestBlock -> Bool
forall a. Eq a => a -> a -> Bool
== AddPerasVoteResult TestBlock
actualRes
      (Left PerasVoteDbModelError
expectedErr, Left PerasVoteDbError TestBlock
actualErr) -> do
        TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall (m :: * -> *). Monad m => TestName -> PostconditionM m ()
counterexamplePost (TestName
 -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ())
-> TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall a b. (a -> b) -> a -> b
$ TestName
"Mismatched failure results:"
        TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall (m :: * -> *). Monad m => TestName -> PostconditionM m ()
counterexamplePost (TestName
 -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ())
-> TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall a b. (a -> b) -> a -> b
$ TestName
"Model: " TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> PerasVoteDbModelError -> TestName
forall a. Show a => a -> TestName
show PerasVoteDbModelError
expectedErr
        TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall (m :: * -> *). Monad m => TestName -> PostconditionM m ()
counterexamplePost (TestName
 -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ())
-> TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall a b. (a -> b) -> a -> b
$ TestName
"SUT: " TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> PerasVoteDbError TestBlock -> TestName
forall a. Show a => a -> TestName
show PerasVoteDbError TestBlock
actualErr
        case (PerasVoteDbModelError
expectedErr, PerasVoteDbError TestBlock
actualErr) of
          ( Model.MultipleWinnersInRound PerasRoundNo
roundNo
            , MultipleWinnersInRound PerasRoundNo
roundNo' ExistingPerasRoundWinner TestBlock
_ BlockedPerasRoundWinner TestBlock
_
            ) ->
              Bool -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) Bool
forall a.
a -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool
 -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) Bool)
-> Bool
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) Bool
forall a b. (a -> b) -> a -> b
$ PerasRoundNo
roundNo PerasRoundNo -> PerasRoundNo -> Bool
forall a. Eq a => a -> a -> Bool
== PerasRoundNo
roundNo'
          (PerasVoteDbModelError, PerasVoteDbError TestBlock)
_ ->
            Bool -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) Bool
forall a.
a -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False
      (Right AddPerasVoteResult TestBlock
expectedRes, Left PerasVoteDbError TestBlock
actualErr) -> do
        TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall (m :: * -> *). Monad m => TestName -> PostconditionM m ()
counterexamplePost (TestName
 -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ())
-> TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall a b. (a -> b) -> a -> b
$ TestName
"Expected success, but got error"
        TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall (m :: * -> *). Monad m => TestName -> PostconditionM m ()
counterexamplePost (TestName
 -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ())
-> TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall a b. (a -> b) -> a -> b
$ TestName
"Model: " TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> AddPerasVoteResult TestBlock -> TestName
forall a. Show a => a -> TestName
show AddPerasVoteResult TestBlock
expectedRes
        TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall (m :: * -> *). Monad m => TestName -> PostconditionM m ()
counterexamplePost (TestName
 -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ())
-> TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall a b. (a -> b) -> a -> b
$ TestName
"SUT: " TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> PerasVoteDbError TestBlock -> TestName
forall a. Show a => a -> TestName
show PerasVoteDbError TestBlock
actualErr
        Bool -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) Bool
forall a.
a -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False
      (Left PerasVoteDbModelError
expectedErr, Right AddPerasVoteResult TestBlock
actualRes) -> do
        TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall (m :: * -> *). Monad m => TestName -> PostconditionM m ()
counterexamplePost (TestName
 -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ())
-> TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall a b. (a -> b) -> a -> b
$ TestName
"Expected error, but got success:"
        TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall (m :: * -> *). Monad m => TestName -> PostconditionM m ()
counterexamplePost (TestName
 -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ())
-> TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall a b. (a -> b) -> a -> b
$ TestName
"Model: " TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> PerasVoteDbModelError -> TestName
forall a. Show a => a -> TestName
show PerasVoteDbModelError
expectedErr
        TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall (m :: * -> *). Monad m => TestName -> PostconditionM m ()
counterexamplePost (TestName
 -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ())
-> TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall a b. (a -> b) -> a -> b
$ TestName
"SUT: " TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> AddPerasVoteResult TestBlock -> TestName
forall a. Show a => a -> TestName
show AddPerasVoteResult TestBlock
actualRes
        Bool -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) Bool
forall a.
a -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False
  postcondition (Model Model TestBlock
model, Model
_) (Action Model a
R:ActionModela a
GetVoteIds) LookUp
_ a
actual = do
    let expected :: Set (PerasVoteId TestBlock)
expected = Model TestBlock -> Set (PerasVoteId TestBlock)
forall blk. Model blk -> Set (PerasVoteId blk)
Model.getVoteIds Model TestBlock
model
    TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall (m :: * -> *). Monad m => TestName -> PostconditionM m ()
counterexamplePost (TestName
 -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ())
-> TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall a b. (a -> b) -> a -> b
$ TestName
"Mismatched result:"
    TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall (m :: * -> *). Monad m => TestName -> PostconditionM m ()
counterexamplePost (TestName
 -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ())
-> TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall a b. (a -> b) -> a -> b
$ TestName
"Model: " TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> Set (PerasVoteId TestBlock) -> TestName
forall a. Show a => a -> TestName
show Set (PerasVoteId TestBlock)
expected
    TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall (m :: * -> *). Monad m => TestName -> PostconditionM m ()
counterexamplePost (TestName
 -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ())
-> TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall a b. (a -> b) -> a -> b
$ TestName
"SUT: " TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> a -> TestName
forall a. Show a => a -> TestName
show a
actual
    Bool -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) Bool
forall a.
a -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool
 -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) Bool)
-> Bool
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) Bool
forall a b. (a -> b) -> a -> b
$ Set (PerasVoteId TestBlock)
expected Set (PerasVoteId TestBlock) -> Set (PerasVoteId TestBlock) -> Bool
forall a. Eq a => a -> a -> Bool
== a
Set (PerasVoteId TestBlock)
actual
  postcondition (Model Model TestBlock
model, Model
_) (GetVotesAfter PerasVoteTicketNo
ticketNo) LookUp
_ a
actual = do
    let expected :: Map
  PerasVoteTicketNo (WithArrivalTime (ValidatedPerasVote TestBlock))
expected = PerasVoteTicketNo
-> Model TestBlock
-> Map
     PerasVoteTicketNo (WithArrivalTime (ValidatedPerasVote TestBlock))
forall blk.
PerasVoteTicketNo
-> Model blk
-> Map PerasVoteTicketNo (WithArrivalTime (ValidatedPerasVote blk))
Model.getVotesAfter PerasVoteTicketNo
ticketNo Model TestBlock
model
    TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall (m :: * -> *). Monad m => TestName -> PostconditionM m ()
counterexamplePost (TestName
 -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ())
-> TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall a b. (a -> b) -> a -> b
$ TestName
"Mismatched result:"
    TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall (m :: * -> *). Monad m => TestName -> PostconditionM m ()
counterexamplePost (TestName
 -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ())
-> TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall a b. (a -> b) -> a -> b
$ TestName
"Model: " TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> Map
  PerasVoteTicketNo (WithArrivalTime (ValidatedPerasVote TestBlock))
-> TestName
forall a. Show a => a -> TestName
show Map
  PerasVoteTicketNo (WithArrivalTime (ValidatedPerasVote TestBlock))
expected
    TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall (m :: * -> *). Monad m => TestName -> PostconditionM m ()
counterexamplePost (TestName
 -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ())
-> TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall a b. (a -> b) -> a -> b
$ TestName
"SUT: " TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> a -> TestName
forall a. Show a => a -> TestName
show a
actual
    Bool -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) Bool
forall a.
a -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool
 -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) Bool)
-> Bool
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) Bool
forall a b. (a -> b) -> a -> b
$ Map
  PerasVoteTicketNo (WithArrivalTime (ValidatedPerasVote TestBlock))
expected Map
  PerasVoteTicketNo (WithArrivalTime (ValidatedPerasVote TestBlock))
-> Map
     PerasVoteTicketNo (WithArrivalTime (ValidatedPerasVote TestBlock))
-> Bool
forall a. Eq a => a -> a -> Bool
== a
Map
  PerasVoteTicketNo (WithArrivalTime (ValidatedPerasVote TestBlock))
actual
  postcondition (Model Model TestBlock
model, Model
_) (GetForgedCertForRound PerasRoundNo
roundNo) LookUp
_ a
actual = do
    let expected :: Maybe (ValidatedPerasCert TestBlock)
expected = PerasRoundNo
-> Map PerasRoundNo (ValidatedPerasCert TestBlock)
-> Maybe (ValidatedPerasCert TestBlock)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup PerasRoundNo
roundNo (Model TestBlock -> Map PerasRoundNo (ValidatedPerasCert TestBlock)
forall blk. Model blk -> Map PerasRoundNo (ValidatedPerasCert blk)
Model.certs Model TestBlock
model)
    TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall (m :: * -> *). Monad m => TestName -> PostconditionM m ()
counterexamplePost (TestName
 -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ())
-> TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall a b. (a -> b) -> a -> b
$ TestName
"Mismatched result:"
    TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall (m :: * -> *). Monad m => TestName -> PostconditionM m ()
counterexamplePost (TestName
 -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ())
-> TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall a b. (a -> b) -> a -> b
$ TestName
"Model: " TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> Maybe (ValidatedPerasCert TestBlock) -> TestName
forall a. Show a => a -> TestName
show Maybe (ValidatedPerasCert TestBlock)
expected
    TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall (m :: * -> *). Monad m => TestName -> PostconditionM m ()
counterexamplePost (TestName
 -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ())
-> TestName
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) ()
forall a b. (a -> b) -> a -> b
$ TestName
"SUT: " TestName -> ShowS
forall a. Semigroup a => a -> a -> a
<> a -> TestName
forall a. Show a => a -> TestName
show a
actual
    Bool -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) Bool
forall a.
a -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool
 -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) Bool)
-> Bool
-> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) Bool
forall a b. (a -> b) -> a -> b
$ Maybe (ValidatedPerasCert TestBlock)
expected Maybe (ValidatedPerasCert TestBlock)
-> Maybe (ValidatedPerasCert TestBlock) -> Bool
forall a. Eq a => a -> a -> Bool
== a
Maybe (ValidatedPerasCert TestBlock)
actual
  postcondition (Model, Model)
_ Action Model a
_ LookUp
_ a
_ = Bool -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) Bool
forall a.
a -> PostconditionM (StateT (PerasVoteDB IO TestBlock) IO) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True

  monitoring :: forall a.
(Model, Model)
-> Action Model a
-> LookUp
-> Either (Error Model (StateT (PerasVoteDB IO TestBlock) IO)) a
-> Property
-> Property
monitoring (Model
_, Model Model TestBlock
model') (AddVote WithArrivalTime (ValidatedPerasVote TestBlock)
vote) LookUp
_ (Right a
res) = do
    TestName -> [TestName] -> Property -> Property
forall prop.
Testable prop =>
TestName -> [TestName] -> prop -> Property
tabulate TestName
"AddVote" [(PerasVoteDbError TestBlock -> TestName)
-> (AddPerasVoteResult TestBlock -> TestName)
-> Either
     (PerasVoteDbError TestBlock) (AddPerasVoteResult TestBlock)
-> TestName
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either PerasVoteDbError TestBlock -> TestName
perasVoteDBErrorTag AddPerasVoteResult TestBlock -> TestName
addVoteResultTag a
Either (PerasVoteDbError TestBlock) (AddPerasVoteResult TestBlock)
res]
      -- In addition to the result of the command, we also tabulate how many
      -- votes were needed to reach quorum (if quorum was reached).
      (Property -> Property)
-> (Property -> Property) -> Property -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TestName -> [TestName] -> Property -> Property
forall prop.
Testable prop =>
TestName -> [TestName] -> prop -> Property
tabulate TestName
"Votes until quorum" (Model TestBlock
-> WithArrivalTime (ValidatedPerasVote TestBlock)
-> Either
     (PerasVoteDbError TestBlock) (AddPerasVoteResult TestBlock)
-> [TestName]
votesToReachQuorum Model TestBlock
model' WithArrivalTime (ValidatedPerasVote TestBlock)
vote a
Either (PerasVoteDbError TestBlock) (AddPerasVoteResult TestBlock)
res)
  monitoring (Model, Model)
_ (Action Model a
R:ActionModela a
GetVoteIds) LookUp
_ (Right a
res) = do
    let tag :: TestName
tag = if Set (PerasVoteId TestBlock) -> Bool
forall a. Set a -> Bool
Set.null a
Set (PerasVoteId TestBlock)
res then TestName
"NoVoteIds" else TestName
"HasVoteIds"
    TestName -> [TestName] -> Property -> Property
forall prop.
Testable prop =>
TestName -> [TestName] -> prop -> Property
tabulate TestName
"GetVoteIds" [TestName
tag]
  monitoring (Model, Model)
_ (GetVotesAfter PerasVoteTicketNo
_) LookUp
_ (Right a
res) = do
    let tag :: TestName
tag = if Map
  PerasVoteTicketNo (WithArrivalTime (ValidatedPerasVote TestBlock))
-> Bool
forall k a. Map k a -> Bool
Map.null a
Map
  PerasVoteTicketNo (WithArrivalTime (ValidatedPerasVote TestBlock))
res then TestName
"NoVotesAfter" else TestName
"HasVotesAfter"
    TestName -> [TestName] -> Property -> Property
forall prop.
Testable prop =>
TestName -> [TestName] -> prop -> Property
tabulate TestName
"GetVotesAfter" [TestName
tag]
  monitoring (Model, Model)
_ (GetForgedCertForRound{}) LookUp
_ (Right a
res) = do
    let tag :: TestName
tag = TestName
-> (ValidatedPerasCert TestBlock -> TestName)
-> Maybe (ValidatedPerasCert TestBlock)
-> TestName
forall b a. b -> (a -> b) -> Maybe a -> b
maybe TestName
"NoCert" (TestName -> ValidatedPerasCert TestBlock -> TestName
forall a b. a -> b -> a
const TestName
"FoundCert") a
Maybe (ValidatedPerasCert TestBlock)
res
    TestName -> [TestName] -> Property -> Property
forall prop.
Testable prop =>
TestName -> [TestName] -> prop -> Property
tabulate TestName
"GetForgedCertForRound" [TestName
tag]
  monitoring (Model, Model)
_ Action Model a
_ LookUp
_ Either (Error Model (StateT (PerasVoteDB IO TestBlock) IO)) a
_ =
    Property -> Property
forall a. a -> a
id

-- * Helpers

perasVoteDBErrorTag :: PerasVoteDbError TestBlock -> String
perasVoteDBErrorTag :: PerasVoteDbError TestBlock -> TestName
perasVoteDBErrorTag PerasVoteDbError TestBlock
err =
  case PerasVoteDbError TestBlock
err of
    MultipleWinnersInRound{} ->
      TestName
"MultipleWinnersInRound"
    ForgingCertError{} ->
      TestName
"ForgingCertError"

addVoteResultTag :: AddPerasVoteResult TestBlock -> String
addVoteResultTag :: AddPerasVoteResult TestBlock -> TestName
addVoteResultTag AddPerasVoteResult TestBlock
res =
  case AddPerasVoteResult TestBlock
res of
    AddPerasVoteResult TestBlock
PerasVoteAlreadyInDB ->
      TestName
"PerasVoteAlreadyInDB"
    AddedPerasVoteAndGeneratedNewCert{} ->
      TestName
"AddedPerasVoteAndGeneratedNewCert"
    AddPerasVoteResult TestBlock
AddedPerasVoteButDidntGenerateNewCert ->
      TestName
"AddedPerasVoteButDidntGenerateNewCert"

votesToReachQuorum ::
  Model.Model TestBlock ->
  WithArrivalTime (ValidatedPerasVote TestBlock) ->
  Either (PerasVoteDbError TestBlock) (AddPerasVoteResult TestBlock) ->
  [String]
votesToReachQuorum :: Model TestBlock
-> WithArrivalTime (ValidatedPerasVote TestBlock)
-> Either
     (PerasVoteDbError TestBlock) (AddPerasVoteResult TestBlock)
-> [TestName]
votesToReachQuorum Model TestBlock
model WithArrivalTime (ValidatedPerasVote TestBlock)
vote Either (PerasVoteDbError TestBlock) (AddPerasVoteResult TestBlock)
res =
  case Either (PerasVoteDbError TestBlock) (AddPerasVoteResult TestBlock)
res of
    Right AddedPerasVoteAndGeneratedNewCert{} ->
      [Int -> TestName
forall a. Show a => a -> TestName
show (Set (VoteEntry TestBlock) -> Int
forall a. Set a -> Int
Set.size Set (VoteEntry TestBlock)
votesInRound)]
    Either (PerasVoteDbError TestBlock) (AddPerasVoteResult TestBlock)
_ ->
      []
 where
  votesInRound :: Set (VoteEntry TestBlock)
votesInRound =
    Set (VoteEntry TestBlock)
-> PerasVoteTarget TestBlock
-> Map (PerasVoteTarget TestBlock) (Set (VoteEntry TestBlock))
-> Set (VoteEntry TestBlock)
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault
      Set (VoteEntry TestBlock)
forall a. Set a
Set.empty
      PerasVoteTarget
        { pvtRoundNo :: PerasRoundNo
pvtRoundNo = WithArrivalTime (ValidatedPerasVote TestBlock) -> PerasRoundNo
forall vote. HasPerasVoteRound vote => vote -> PerasRoundNo
getPerasVoteRound WithArrivalTime (ValidatedPerasVote TestBlock)
vote
        , pvtBlock :: Point TestBlock
pvtBlock = WithArrivalTime (ValidatedPerasVote TestBlock) -> Point TestBlock
forall vote blk. HasPerasVoteBlock vote blk => vote -> Point blk
getPerasVoteBlock WithArrivalTime (ValidatedPerasVote TestBlock)
vote
        }
      (Model TestBlock
-> Map (PerasVoteTarget TestBlock) (Set (VoteEntry TestBlock))
forall blk.
Model blk -> Map (PerasVoteTarget blk) (Set (VoteEntry blk))
Model.votes Model TestBlock
model)