<div dir="ltr"><div dir="ltr"><div class="gmail_default" style="font-family:arial,helvetica,sans-serif"><span style="font-family:Arial,Helvetica,sans-serif">On Wed, May 6, 2020 at 10:27 AM Frans Schneider <<a href="mailto:fchschneider@gmail.com">fchschneider@gmail.com</a>> wrote:</span><br></div></div><div class="gmail_quote"><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">The general question I have is how to handle things like dynamic <br>
generated id's or processes in stateful properties. Does somebody have <br>
an example of doing this?<br>
<br></blockquote><div><br></div><div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif">Two general tactics for this (with one bonus tactic):</div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif"><br></div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif">You have a model, and you have a system-under-test (SUT). The key is that the model is generated before you run the test, so it doesn't know about choice in the SUT. This choice occurs when the SUT generates random data, or a Pid or something such.</div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif"><br></div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif">Your first option is to use symbolic execution in the model. You organize it such that your command returns the Pid or the random value, which is then inserted into the model as a symbolic reference `{ref, 234}` or such. Critically, you can't use this value to evaluate a post-condition, but it can be stored in state and fed back into the SUT at a later point in the test. That is, the reference has (unique) identity, but nothing else. This will allow you to refer back to the generated value in later commands in your stateful test, which is often quite useful. For Pids, this tends to be a useful method. Note, if your command returns something which is not the Pid, you will have to adapt in your command execution:</div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif"><br></div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif">create() -></div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif">  {ok, Pid} = s:spawn(),</div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif">  Pid.</div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif"><br></div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif">+++<br></div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif"><br></div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif">The other way you can approach this is to move the choice from the SUT into the Model. That is, you generate the UUID or random number in the model. Then you inject it into the SUT and it is built such that it will use the value given. Thus, the choice is now in a place where you can store it in your state as you have full control over its value. It may seem counter to the whole idea that the SUT needs to be adapted to fit the model, but I've found this often creates code that is easier to reason about anyway. It decouples effects like generating a Pid or UUID in your code from computation, so testing is easier, be it property or unit test.</div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif"><br></div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif">+++<br></div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif"><br></div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif">There is a third option in Erlang QuickCheck (EQC) which is to mock the UUID generation and then generate a random UUID which is fed into the SUT. Because it is generated by the mock, you have access to it. The key idea here is that you can rewrite your model transitions into callouts which are smaller steps that forms a single command. Along the call, you expect the SUT to callout to uuid:v5() or something such, which is mocked by the system to return a value decided on by the model. You then avoid having to rewrite the system to facilitate the injection as outlined above[0].</div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif"><br></div><div class="gmail_default" style="font-family:arial,helvetica,sans-serif">[0] There are some similarity to big-step / small-step semantics here. Without callouts, you only have one large state transition per command. The callout system of EQC allows you to break such a big step up into its smaller counterparts and interleave mocked calls in between.</div><br></div></div><div><br></div>-- <br><div dir="ltr" class="gmail_signature">J.</div></div>