Interplay between model based testing and scheduler

[tskj]

Hey there, thanks for this fantastic library! I am trying to combine two ideas that are mentioned in the Tips section, namely model based testing and detecting race conditions with schedulers.

The setup I have is that I generate a sequence of commands for the system and run that against the system and model. The system can then (potentially) for every one of those commands fire off one promise. This promise I have configured as s.schedule(Promise.resolve()) in my mock. I am very happy with this setup, and what I want is for fast-check to re-order the promise resolutions to detect race conditions - but I also want it to do this arbitrarily interleaved with the commands. I hope this makes sense!

I tried making the commands async with AsyncCommand and .asyncModelRun, however then the tests just never finish within Jest's timelimit. I don't need the commands themselves to be async (I don't think? since they only fire off promises, but never await them or return promises themselves), so I just reverted that and now use regular commands. This is fine by me.

I also use await s.waitAll() to await all the promises. This has already found one race condition, so that's cool! But my question is this: is it valid to use regular un-async commands like this, together with scheduling promises? And will fast-check interleave these commands with the promises? Or will all commands run first, and then the promises will be resolved?

Hope that makes sense, look forward to hearing from you!

[dubzzz]

Probably worth checking this example: https://github.com/dubzzz/fast-check/blob/main/examples/005-race/todolist/main.spec.tsx

It uses a runner for model based testing tailored for scheduling.

[tskj]

Thanks for the quick reply! So there is an scheduledModelRun in addition to asyncModelRun and modelRun. I could not find this when looking for it initially, it does not appear to be in the documentation anywhere except for the API reference? I would like to know what the semantics for it are and exactly how I am supposed to use it.

I have now tried switching my code to use scheduledModelRun, including implementing AsyncCommand even though I don't really need my commands themselves to be async, but no matter what I do I get the Jest timeout:

Timeout - Async callback was not invoked within the 5000 ms timeout specified by jest.setTimeout.Timeout

I've tried all these configurations of fast-check like suggested in the documentation:

fc.configureGlobal({
    interruptAfterTimeLimit: 4000,
    markInterruptAsFailure: false,
});
// or
fc.configureGlobal({
    interruptAfterTimeLimit: 4000,
    markInterruptAsFailure: true,
});
// or
fc.configureGlobal({
    interruptAfterTimeLimit: 1000,
    markInterruptAsFailure: false,
});
// or
fc.configureGlobal({
    interruptAfterTimeLimit: 1000,
    markInterruptAsFailure: true,
});

but nothing makes a difference. I'm sure I have done something wrong, but without any explanation of how these APIs are supposed to work, I'm having a hard time reverse engineering it.

[dubzzz]

Unfortunately except the todo example and https://github.com/dubzzz/fast-check/blob/main/packages/fast-check/documentation/RaceConditions.md#model-based-testing-and-race-conditions I do not have much more documentation for this precise helper.

If you use one of the latest version of fast-check, using interruptAfterTimeLimit: 4000 should stop the test before Jest does and help you seeing what failed (should fail before Jest does).

[dubzzz]

If it can help, I recently updated these tests. They were running against old versions of React Testing Library. The updated version should probably work better for modern testing setups.

[dubzzz]

I also added a documentation dedicated to model based testing at https://fast-check.dev/docs/advanced/model-based-testing/