Use a generator to init models

[mikesol]

It seems like the source could be refatored so that initModel could return Gen Model r instead of Model r and then the initial model would be generated at the same time as the request. This would allow for the state machine to start at arbitrary initial states. It would also require an additional function similar to cleanup with a signature model Command -> IO () that does any necessary setup (ie initializing a database) from the model.

For me personally, when testing systems whose behavior is often only revealed when the database is in a certain state, having the ability to sync it with a model before the tests run would be quite beneficial! But it would also be a breaking change to the API.

Does this sound like a welcome/reasonable addition?

[stevana]

Being able to start in arbitrary initial state is something I've considered for testing sequential algorithms, e.g. binary search, where you wanna test that your algorithm preserves some invariants and the input to your algorithm is part of the initial state. This would not require the extra model Command -> IO () (model Symbolic you mean?) function as far as I can see.

I'm still not convinced about your use case, could you give a concrete example of where this would actually be beneficial over starting with an empty database? My intuition says that this "revealed when the database is in a certain state" is a state you can get to by max 15-20 commands (more likely 5), and the benefit from being able to "skip" generating and executing those commands is smaller than: having to worry about generating consistent initial states and being able to figure out why the counterexamples make sense. But I'm happy to be convinced otherwise.

[mikesol]

For example, if there is an orders microservice that checks orders' states and deletes orders once they are delivered but cannot create orders, it is useful to start with 0 orders, with several orders and with many orders. In this case, one could just run a few different checks with different initModels, but if there are several of these parameters (ie orders, users, addresses), the permutations start to grow.

The above strategy is what I'm doing for the time being - I am initializing a read-only DB to 0, several and many entries in three different tests. It's fine for now, but it feels like quickcheck could make that sort of strategy more powerful by automating it.

[stevana]

Hmm, what about a property of properties? Something like:

forAll genFixtures $ \fixture -> monadicIO $ do   -- fixture is zero, several, or many orders
  setupDb fixture
  quickCheck (prop_foo (initialModelFromFixture fixture))

[mikesol]

That works, thanks!