The Test.Consensus.GSM module contains tests for the Genesis State Machine — a part of the Ouroborus Genesis consensus protocol implementation that determines if a Node is caught-up.

The Test.Consensus.GSM and Test.Consensus.GSM.Model use quickcheck-state-machine to specify the GSM and check some of its properties.
The test actually use a variation of quickcheck-state-machine defined in Test.Consensus.IOSimQSM.Test.StateMachine.Sequential that is abstracted over the IO monad using io-classes and thus allows using io-sim, and specifically IOSimPOR, which allows exploring various interleaving of the IO-like actions. However, the problem with using IOSimPOR as a drop in replacement for IO here is that the IO actions comprising the implementation of quickcheck-state-machine become the subject of analysis, together with the IO actions of the system under test. Exploring re-orderings of QSM's IO actions is undesirable, as it is not only irrelevant to the system under test, but may also lead to breaking the quickcheck-state-machine. We need an approach that would allow exploring re-orderings of the system actions, but keep the QSM implementation actions as-is.

The proposed approach is to use quickcheck-dynamic, which allows for integration with IOSim and IOSimPOR (see https://github.com/input-output-hk/quickcheck-dynamic/tree/main/quickcheck-dynamic-iosim).

switch to quickcheck-dynamic and/or upstream the io-sim-based QSM module #1149

Description

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions

switch to `quickcheck-dynamic` and/or upstream the `io-sim`-based QSM module #1149