fenollp
commented
9 months ago to introduce another mode that allows us to use the model for guided transition generation based on implementation state
+1 from me: I'd like a statem strategy that does not generate the sequence of calls ahead of time.
Instead I'd imagine a strategy that generates either the next call or a special value that represents the end of the test. Calling this successively and given current calls history then gives the next call to SUT, or ends.
I am creating this issue to initiate a discussion about extending the current proptest state machine to support guided transition generation based on a model that is aware of the implementation. This enhancement aims to improve the accuracy of transition generation.
Problem: The current approach in proptest state machine testing requires the model to have full context in order to generate reasonable transitions for the implementation. However, implementing the model can become as costly as re-implementing the system under test when the implementation is complex.
For instance, consider a scenario where we need to test a service that offers a client API and periodically queries a backend for additional information. If the client calls directly match one-to-one with the backend calls, the model can be relatively straightforward. However, adding extra logic to share backend calls between clients complicates the implementation and makes it difficult to mock the backend calls without implementing logic that directly matches the client calls. Furthermore, it is challenging for the model to predict whether a query for the backend will occur in the first place, as the service might cache the result. Consequently, generating transitions becomes too random without information about the implementation.
Suggestion: Instead of requiring a model that fully matches the implementation, my suggestion is to introduce another mode that allows us to use the model for guided transition generation based on implementation state. The rationale behind this suggestion is that once the implementation is available to the model, it can make more informed decisions regarding mocked calls and generate specific transitions based on the system under test's current state.
The proposed implementation of this mode involves an iterative process where transitions are generated, validated with both the model and the system under test, and then potentially shrunk based on M transitions before the crash. Shrinking is the crucial point, which prompted the creation of this issue, as it's affected by this approach.
To summarise the necessary changes roughly looks like this:
Enable the model to access the implementation when generating transitions.
When generating the initial N transitions, validate each of them not only with the model but also with the system under test.
If a failure occurs during the validation with the implementation, we can identify it as a failing test and proceed to perform shrinking.
Utilize the implementation during the shrinking process as well since every following state of the model might require up-to-date information from the implementation.
I wonder what do you think about the suggested approach?