Mock mismatch with semantics

[luntain]

My system under test has an operation that returns a list of references, however, there is no way to precisely mock it using the model. I only know a constraint on the list of references the system can return. I get:

Continuing to execute commands at this point could result in scope
errors, because we might have commands that use references (returned
by mock) that are not available (returned by semantics), to avoid
this please fix the mismatch.

This is related to Issue 236. The mock and why it is needed is a mystery. This error message is hard to understand, because it is expressed in terms of the internals of the library. It feels that in order to understand it I would need to read the code of the lib.

[stevana]

This error message is hard to understand, because it is expressed in terms of the internals of the library.

What internals? I don't see a single concept in that error message that isn't exposed to the user?

It feels that in order to understand it I would need to read the code of the lib.

Go ahead, the code is fairly simple. Afterwards perhaps you can suggest how the error message can be improved, because I can't think of a better way to put it...

mock is a hack, as I admit in the issue you linked to. I don't know how to remove mock while retaining the possibility to return different references though, also it turns out mock can be used in unexpected but useful ways: https://www.well-typed.com/blog/2019/01/qsm-in-depth/ .