<div dir="ltr"><br><br><div class="gmail_quote"><div dir="ltr">On Mon, Dec 10, 2018 at 4:29 PM Jesper Louis Andersen <<a href="mailto:jesper.louis.andersen@gmail.com">jesper.louis.andersen@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr"><div dir="ltr"><div class="gmail_quote"><div><div style="font-family:arial,helvetica,sans-serif"><br></div><div style="font-family:arial,helvetica,sans-serif">One important point about PropER testing is that you must try to shift as much choice to be controlled by the model. This often requires an API where one can inject parameters from the outside to control the setup of certain states. You can always have a sane default which initializes if not overriden, and this is what I've often done. Important examples are that randomness and time must be controlled from the outside in some way. Otherwise, the system tend to become impossible to test. And it also hides important details to the user of the API to boot.</div><div style="font-family:arial,helvetica,sans-serif"></div></div></div></div></div></blockquote><div><br></div><div>One of the tips I recommend on <a href="http://propertesting.com">propertesting.com</a> is to use shim modules. If the API is not  amenable to good control, the generator of the model at least has to be.</div><div><br></div><div>So you might have a single call to "add_item(Id, Name, ...)" but various reactions according to whether the item exists or not. The shim module will act as a wrapper where you can instead expose calls like "add_existing_item(...)", "add_unknown_item(...)", or "add_malformed_item(...)". The generator, preconditions, next_state, and postconditions callback can then build their expectations based on the type of operation even though the underlying system handles calls by itself. It also makes it easier to make calls synchronous or asynchronous as long as the underlying system exposes them. It also helps to do things like change a successful return value that you want to store in the state from {ok, Pid} to just Pid, and then pass it back to the next generated call such that it won't clash with the opaque placeholders the framework uses.<br></div><div><br></div><div>this does require the system under test to have at least some level of control given to build this higher-level test-only abstraction, but it helps make things simpler.</div><div><br></div><div>The one case I can think of where you may want to adapt your system is when it comes to timeout handling. Ensuring some calls timeout while succeeding or failing is rather difficult and may not always work with a shim, especially in async interfaces. For those, having a way to configure or override timers might be necessary.</div><div><br></div><div>But I would also like to violently agree with the notion that the model has to drive the test, which implies that you can, without looking at the system (aside from opaque types like generated IDs that you store in placeholders), create a full predictable execution with useful invariants to check. This can quickly become tricky when you have some non-deterministic results (N/M requests might be dropped), so you have to be careful.<br></div></div></div>