Home / Input Output / ouroboros-consensus
Jul 05, 3-4 AM (0)
Jul 05, 4-5 AM (0)
Jul 05, 5-6 AM (0)
Jul 05, 6-7 AM (0)
Jul 05, 7-8 AM (0)
Jul 05, 8-9 AM (0)
Jul 05, 9-10 AM (0)
Jul 05, 10-11 AM (0)
Jul 05, 11-12 PM (0)
Jul 05, 12-1 PM (0)
Jul 05, 1-2 PM (0)
Jul 05, 2-3 PM (0)
Jul 05, 3-4 PM (0)
Jul 05, 4-5 PM (0)
Jul 05, 5-6 PM (0)
Jul 05, 6-7 PM (0)
Jul 05, 7-8 PM (0)
Jul 05, 8-9 PM (0)
Jul 05, 9-10 PM (0)
Jul 05, 10-11 PM (0)
Jul 05, 11-12 AM (0)
Jul 06, 12-1 AM (0)
Jul 06, 1-2 AM (0)
Jul 06, 2-3 AM (0)
Jul 06, 3-4 AM (0)
Jul 06, 4-5 AM (0)
Jul 06, 5-6 AM (0)
Jul 06, 6-7 AM (0)
Jul 06, 7-8 AM (0)
Jul 06, 8-9 AM (0)
Jul 06, 9-10 AM (0)
Jul 06, 10-11 AM (0)
Jul 06, 11-12 PM (0)
Jul 06, 12-1 PM (0)
Jul 06, 1-2 PM (11)
Jul 06, 2-3 PM (0)
Jul 06, 3-4 PM (0)
Jul 06, 4-5 PM (0)
Jul 06, 5-6 PM (0)
Jul 06, 6-7 PM (0)
Jul 06, 7-8 PM (0)
Jul 06, 8-9 PM (0)
Jul 06, 9-10 PM (0)
Jul 06, 10-11 PM (0)
Jul 06, 11-12 AM (0)
Jul 07, 12-1 AM (0)
Jul 07, 1-2 AM (0)
Jul 07, 2-3 AM (0)
Jul 07, 3-4 AM (0)
Jul 07, 4-5 AM (0)
Jul 07, 5-6 AM (0)
Jul 07, 6-7 AM (0)
Jul 07, 7-8 AM (37)
Jul 07, 8-9 AM (2)
Jul 07, 9-10 AM (1)
Jul 07, 10-11 AM (0)
Jul 07, 11-12 PM (0)
Jul 07, 12-1 PM (0)
Jul 07, 1-2 PM (1)
Jul 07, 2-3 PM (2)
Jul 07, 3-4 PM (0)
Jul 07, 4-5 PM (0)
Jul 07, 5-6 PM (0)
Jul 07, 6-7 PM (0)
Jul 07, 7-8 PM (0)
Jul 07, 8-9 PM (0)
Jul 07, 9-10 PM (0)
Jul 07, 10-11 PM (0)
Jul 07, 11-12 AM (0)
Jul 08, 12-1 AM (0)
Jul 08, 1-2 AM (0)
Jul 08, 2-3 AM (0)
Jul 08, 3-4 AM (0)
Jul 08, 4-5 AM (0)
Jul 08, 5-6 AM (0)
Jul 08, 6-7 AM (0)
Jul 08, 7-8 AM (0)
Jul 08, 8-9 AM (1)
Jul 08, 9-10 AM (0)
Jul 08, 10-11 AM (5)
Jul 08, 11-12 PM (0)
Jul 08, 12-1 PM (8)
Jul 08, 1-2 PM (0)
Jul 08, 2-3 PM (0)
Jul 08, 3-4 PM (0)
Jul 08, 4-5 PM (1)
Jul 08, 5-6 PM (0)
Jul 08, 6-7 PM (1)
Jul 08, 7-8 PM (0)
Jul 08, 8-9 PM (0)
Jul 08, 9-10 PM (0)
Jul 08, 10-11 PM (0)
Jul 08, 11-12 AM (0)
Jul 09, 12-1 AM (0)
Jul 09, 1-2 AM (0)
Jul 09, 2-3 AM (0)
Jul 09, 3-4 AM (0)
Jul 09, 4-5 AM (0)
Jul 09, 5-6 AM (1)
Jul 09, 6-7 AM (0)
Jul 09, 7-8 AM (0)
Jul 09, 8-9 AM (1)
Jul 09, 9-10 AM (16)
Jul 09, 10-11 AM (1)
Jul 09, 11-12 PM (0)
Jul 09, 12-1 PM (0)
Jul 09, 1-2 PM (0)
Jul 09, 2-3 PM (0)
Jul 09, 3-4 PM (3)
Jul 09, 4-5 PM (0)
Jul 09, 5-6 PM (0)
Jul 09, 6-7 PM (0)
Jul 09, 7-8 PM (0)
Jul 09, 8-9 PM (0)
Jul 09, 9-10 PM (0)
Jul 09, 10-11 PM (0)
Jul 09, 11-12 AM (0)
Jul 10, 12-1 AM (0)
Jul 10, 1-2 AM (0)
Jul 10, 2-3 AM (0)
Jul 10, 3-4 AM (0)
Jul 10, 4-5 AM (0)
Jul 10, 5-6 AM (0)
Jul 10, 6-7 AM (0)
Jul 10, 7-8 AM (1)
Jul 10, 8-9 AM (0)
Jul 10, 9-10 AM (0)
Jul 10, 10-11 AM (3)
Jul 10, 11-12 PM (12)
Jul 10, 12-1 PM (0)
Jul 10, 1-2 PM (2)
Jul 10, 2-3 PM (2)
Jul 10, 3-4 PM (0)
Jul 10, 4-5 PM (0)
Jul 10, 5-6 PM (0)
Jul 10, 6-7 PM (0)
Jul 10, 7-8 PM (0)
Jul 10, 8-9 PM (0)
Jul 10, 9-10 PM (0)
Jul 10, 10-11 PM (0)
Jul 10, 11-12 AM (0)
Jul 11, 12-1 AM (0)
Jul 11, 1-2 AM (0)
Jul 11, 2-3 AM (0)
Jul 11, 3-4 AM (0)
Jul 11, 4-5 AM (0)
Jul 11, 5-6 AM (1)
Jul 11, 6-7 AM (3)
Jul 11, 7-8 AM (5)
Jul 11, 8-9 AM (1)
Jul 11, 9-10 AM (0)
Jul 11, 10-11 AM (2)
Jul 11, 11-12 PM (4)
Jul 11, 12-1 PM (0)
Jul 11, 1-2 PM (0)
Jul 11, 2-3 PM (0)
Jul 11, 3-4 PM (1)
Jul 11, 4-5 PM (0)
Jul 11, 5-6 PM (0)
Jul 11, 6-7 PM (0)
Jul 11, 7-8 PM (0)
Jul 11, 8-9 PM (0)
Jul 11, 9-10 PM (0)
Jul 11, 10-11 PM (0)
Jul 11, 11-12 AM (0)
Jul 12, 12-1 AM (0)
Jul 12, 1-2 AM (0)
Jul 12, 2-3 AM (0)
Jul 12, 3-4 AM (0)
129 commits this week Jul 05, 2025 - Jul 12, 2025
Test Genesis State Machine with `quickcheck-dynamic` (#1413)
Fixes https://github.com/IntersectMBO/ouroboros-consensus/issues/1149

"no changelog", as the changes only affect the
`ouroboros-consensus-diffusion:consensus-test` package.

In this PR, we refactor the `Test.Consensus.GSM` modules, which contain
the tests for the Genesis State Machine component, to use a different
state machine testing framework. Specifically, we are switching the
tests from `quickcheck-state-machine` to `quickcheck-dynamic`. The main
motivation for the switch is being able to run the Genesis State Machine
in `IOSim` in order to benefit from `IOSim`s ability to manipulate the
passage of time and this speed-up the tests.

While the current GSM tests do run in `IOSim`, this is only possible due
to vendoring a copy of `quickcheck-state-machine` that allows using
`IOSim`, which we would like to avoid long-term.

Specifically, this PR:

- adds QD-based tests
- groups definition used in both QSM and QD tests

Below, I describe some aspects of the switch that I consider worth
highlighting, hopefully making the review more manageable.

## Differences from `quickcheck-state-machine` tests

While I've tried to replicate the existing
`quickcheck-state-machine`-based tests as closely as possible, there are
some unavoidable differences between the test suites stemming from how
the `quickcheck-dynamic` library is structured and implemented.

### Different distributions of command sequences

While the user can specify the logic to generate individual commands,
both `quickcheck-dynamic` and `quickcheck-state-machine` have internal
hard-coded logic to generate sequences of commands:

| `quickcheck-dynamic` | `quickcheck-state-machine` |

|:--------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------|:--------------------------------------------------------------------------------------------------------------------------------------------------------------|
|
[generateActionsWithOptions](https://github.com/input-output-hk/quickcheck-dynamic/blob/5f662ced1c6d2cea81c63d6eb52a094adf0b1b40/quickcheck-dynamic/src/Test/QuickCheck/StateModel.hs#L410)
|
[generateCommandsState](https://hackage.haskell.org/package/quickcheck-state-machine-0.10.1/docs/src/Test.StateMachine.Sequential.html#generateCommandsState)
|
| | |

Here are the partial tests reports, which show that QSM produces more
uniform distribution of commands:

```
quickcheck-dynamic                     |             quickcheck-state-machine
                                       |
GSM (at most 1 peer):  OK (0.19s)      |             GSM (at most 1 peer):  OK (0.42s)
  +++ OK, passed 1000 tests.           |               +++ OK, passed 1000 tests.
                                       |
  Actions (24732 in total):            |               Commands (7336 in total):
  33.232% +TimePasses                  |               13.63% NewCandidate
  14.257% +ReadMarker                  |               13.63% StartIdling
  14.152% +ReadGsmState                |               13.63% TimePasses
  13.404% +ModifyCandidate             |               13.56% ReadMarker
  12.187% +StartIdling                 |               13.54% ReadGsmState
   6.740% +NewCandidate                |               13.41% ModifyCandidate
   3.324% +Disconnect                  |               10.17% Disconnect
   2.705% +ExtendSelection             |                8.42% ExtendSelection
                                       |
  Notables (2312 in total):            |               Notables (3347 in total):
  17.82% FellBehindN                   |               20.50% FellBehindN
  17.08% PreSyncingToSyncingN          |               19.30% PreSyncingToSyncingN
  16.09% <none>                        |               13.92% TooOldN
  11.98% TooOldN                       |               13.65% CaughtUpN
  10.86% CaughtUpN                     |                9.68% FlickerN
   9.34% SyncingToPreSyncingN          |                9.47% SyncingToPreSyncingN
   9.26% BigDurN                       |                9.20% BigDurN
   7.53% FlickerN                      |                4.27% <none>
   0.04% NotThrashingN                 |
```

Similarly, for 5 peers:

```
`quickcheck-dynamic`                   |             `quickcheck-state-machine`
                                       |
GSM (at most 5 peers): OK (0.25s)      |             GSM (at most 5 peers): OK (0.53s)
  +++ OK, passed 1000 tests.           |               +++ OK, passed 1000 tests.
                                       |
  Actions (26337 in total):            |               Commands (7314 in total):
  29.157% +TimePasses                  |               13.67% NewCandidate
  16.190% +StartIdling                 |               13.67% TimePasses
  15.643% +NewCandidate                |               13.65% StartIdling
  11.098% +ReadGsmState                |               13.29% ReadGsmState
  11.072% +ReadMarker                  |               13.28% ReadMarker
  10.024% +ModifyCandidate             |               13.04% ModifyCandidate
   4.291% +ExtendSelection             |               10.39% ExtendSelection
   2.525% +Disconnect                  |                9.01% Disconnect
                                       |
  Notables (2102 in total):            |               Notables (2788 in total):
  27.26% PreSyncingToSyncingN          |               31.17% PreSyncingToSyncingN
  21.93% SyncingToPreSyncingN          |               24.82% SyncingToPreSyncingN
  16.60% FellBehindN                   |               21.34% FellBehindN
  14.65% <none>                        |                6.85% BigDurN
   5.99% TooOldN                       |                6.71% TooOldN
   5.95% BigDurN                       |                6.56% CaughtUpN
   5.80% CaughtUpN                     |                1.94% FlickerN
   1.81% FlickerN                      |                0.61% <none>
```

QD also generates significantly more commands than QSM, probably due to
longer defaults length for command sequences.

### The glue code of `quickcheck-dymamic` is essentially pure and thus
allows to use `IOSim`

The type of `quickcheck-state-machine`'s
[runCommands](https://hackage.haskell.org/package/quickcheck-state-machine-0.10.1/docs/src/Test.StateMachine.Sequential.html#runCommands)
function constraints the underlying monad to IO:

```
runCommands :: (MonadMask m, MonadIO m)
            => ...
            -> PropertyM m (History cmd resp, model Concrete, Reason)
```

This is needed, because `quickcheck-state-machine` uses `TChan`s
internally to orchestrate the interaction between the model and the
system-under-test. This in particular makes it impossible to run the
system-under-test in `IOSim` and motivated us to vendor a
[copy](https://github.com/IntersectMBO/ouroboros-consensus/tree/main/ouroboros-consensus-diffusion/test/consensus-test/Test/Consensus/IOSimQSM/Test/StateMachine/Sequential.hs#L32)
of QSM with the types adapted to permit `IOSim`.

In `quickcheck-dymamic`, commands are called actions, and run using the

[runActions](https://github.com/input-output-hk/quickcheck-dynamic/blob/5f662ced1c6d2cea81c63d6eb52a094adf0b1b40/quickcheck-dynamic/src/Test/QuickCheck/StateModel.hs#L551)
function, whose type gives the user much more freedom:

```
runActions
  :: 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)

class (forall a. Show (Action state a), Monad m) => RunModel state m where
  ...
```

I.e. the user needs to instantiate the `RunModel` class, where the
library only requires `m` to be a `Monad`. The implementation of
`runActions` itself is essentially pure and only uses the facilities of
[Test.Quickcheck.Monadic](https://hackage.haskell.org/package/QuickCheck-2.15.0.1/docs/Test-QuickCheck-Monadic.html)
to invoke the underlying monadic code of the system-under-test.

### Slightly different test setup routine

While `quickcheck-state-machine` represents state machines as records of
functions, and thus gives a lot of flexibility to the user in terms
pasteurisation, `quickcheck-dynamic` is not as flexible, as it uses type
classes.

Specifically, I was having a hard time to emulate the pattern of
parameterising the state machine with a `Context` that exists in the
current QSM test (see
[here](https://github.com/IntersectMBO/ouroboros-consensus/blob/geo2a%2Fissue-1149-refactor-gsm-tests-reflection/ouroboros-consensus-diffusion/test/consensus-test/Test/Consensus/GSM/QSM.hs#L201),
for example). The `Context` data type contains parameters that are
generated with `quickcheck` and are fixed over the execution of one
property test, i.e. they are static from the state machine's point of
view.

`quickcheck-dynamic` does not provide a way to supply static information
to the state machine out of the box, thus not allowing to configure the
initial state according to some external static parameter and presenting
us with an instance of the classic configuration problem. I've tried
several ways to solve this particular instance, but the turned out to be
using [reflection](https://hackage.haskell.org/package/reflection) as
suggested by @nfrisby. Specifically, I've taken inspiration from this
[blogpost](https://newartisans.com/2017/02/a-case-of-reflection/) by
John Wiegley, where he uses reflection to provide configuration to
`quickcheck` generators --- this is almost exactly what we want here!

The essence of the solution is to constrain the `StateModel` instance
with an constraint provided by `reflection`. This way, we get to use
have the reflected parameters in the `initialState` method:

```
instance Reflection.Reifies params StaticParams => QD.StateModel (Model params) where
  ...

  initialState = initModel params
    where params = Reflection.reflect (Proxy @params)

initModel :: StaticParams -> Model params
```

We would then create a value of `StaticParams` in the property
definition:

```haskell
prop_sequential_iosim :: Maybe UpstreamPeer -> LedgerStateJudgement -> QC.Fun (Set.Set UpstreamPeer) Bool -> QC.Property
prop_sequential_iosim pUpstreamPeerBound pInitialJudgement (QC.Fun _ pIsHaaSatisfied) =
    Reflection.reify (StaticParams{ pUpstreamPeerBound
                                  , pInitialJudgement
                                  , pIsHaaSatisfied
                                  }) $ \(Proxy :: Proxy params) ->
     -- NOTE: the actions have to be generated with an explicit call, as
     -- 'generator' relies on reflection for access to the parameters
     QC.forAll QC.arbitrary $ \actions ->
       runIOSimProp $ prop_sequential_iosim1 @_ @params actions
```

The only tricky thing here is to explicitly invoke the generator for
actions, so that the reified value of StaticParams is in scope.

## Next steps

Once the reviewers are happy with the changes, we should:
- [x] remove the tests based on `quickcheck-state-machine`
- [x] remove [our copy
](https://github.com/IntersectMBO/ouroboros-consensus/tree/main/ouroboros-consensus-diffusion/test/consensus-test/Test/Consensus/IOSimQSM/Test/StateMachine/Sequential.hs#L32)
of `quickcheck-state-machien` that allows `IOSim`
- [x] restructure the GSM tests modules accordingly, i.e. move the QD
module one level up and rename it to `GSMTests`

Independently:
- [x] we need to make a Hackage release of `quickcheck-dynamic`, as this
PR relies on the version from `master` which is not yet released
- [x] once the release is uploaded, we will be able to remove the s-r-p