|
17 | 17 |
|
18 | 18 | {-# OPTIONS_GHC -Wno-orphans #-}
|
19 | 19 |
|
20 |
| --- | Tests for the Genesis State Machine using the quickcheck-dynamic library |
21 |
| - |
| 20 | +-- | Tests for the Genesis State Machine using the [quickcheck-dynamic](https://hackage.haskell.org/package/quickcheck-dynamic) library. |
| 21 | +-- |
| 22 | +-- The instance 'QD.StateModel (Model params)' describes the actions that the model supports, |
| 23 | +-- and their semantics in terms for the model and the system-under-test. |
| 24 | +-- |
| 25 | +-- We use the [reflection](https://hackage.haskell.org/package/reflection) library to solve the problem of |
| 26 | +-- injecting user-supplied or quickcheck-generated values into the instance of QD.StateModel. |
| 27 | +-- See the definition of the 'initialState' method, where we access the reflected configuration, and |
| 28 | +-- see 'prop_sequential_iosim' for the construction and reification of the configuration. |
22 | 29 | module Test.Consensus.GSM.QD (tests) where
|
23 | 30 |
|
24 | 31 | import Control.Concurrent.Class.MonadSTM.Strict.TVar.Checked
|
@@ -63,10 +70,10 @@ tests = adhoc <> core
|
63 | 70 | adhoc = [ testProperty "GSM yield regression" prop_yield_regression
|
64 | 71 | ]
|
65 | 72 | core = [
|
66 |
| - adjustQuickCheckTests (* 10) $ |
67 |
| - testProperty ("GSM (" <> coreTestName upstreamPeerBound <> ")") $ |
68 |
| - prop_sequential_iosim upstreamPeerBound |
69 |
| - | upstreamPeerBound <- Nothing : map Just [minBound .. maxBound :: UpstreamPeer] |
| 73 | + adjustQuickCheckTests (* 10) |
| 74 | + $ testProperty ("GSM (" <> coreTestName upstreamPeerBound <> ")") |
| 75 | + $ prop_sequential_iosim upstreamPeerBound |
| 76 | + | upstreamPeerBound <- Nothing : map Just [minBound .. maxBound :: UpstreamPeer] |
70 | 77 | ]
|
71 | 78 |
|
72 | 79 | coreTestName = \case
|
@@ -97,14 +104,14 @@ prop_yield_regression =
|
97 | 104 | <> (wrapPositiveAction $ ExtendSelection (S (-4)))
|
98 | 105 | <> (wrapPositiveAction $ ReadMarker)
|
99 | 106 |
|
100 |
| -prop_sequential_iosim :: Maybe UpstreamPeer -> QC.Property |
101 |
| -prop_sequential_iosim pUpstreamPeerBound = |
102 |
| - QC.forAll QC.arbitrary $ \pInitialJudgement -> |
103 |
| - QC.forAll QC.arbitrary $ \(QC.Fun _ pIsHaaSatisfied) -> |
| 107 | +prop_sequential_iosim :: Maybe UpstreamPeer -> LedgerStateJudgement -> QC.Fun (Set.Set UpstreamPeer) Bool -> QC.Property |
| 108 | +prop_sequential_iosim pUpstreamPeerBound pInitialJudgement (QC.Fun _ pIsHaaSatisfied) = |
104 | 109 | Reflection.reify (StaticParams{ pUpstreamPeerBound
|
105 | 110 | , pInitialJudgement
|
106 | 111 | , pIsHaaSatisfied
|
107 | 112 | }) $ \(Proxy :: Proxy params) ->
|
| 113 | + -- NOTE: the actions have to be generated with an explicit call, as |
| 114 | + -- 'generator' relies on reflection for access to the parameters |
108 | 115 | QC.forAll QC.arbitrary $ \actions ->
|
109 | 116 | runIOSimProp $ prop_sequential_iosim1 @_ @params actions
|
110 | 117 |
|
|
0 commit comments