<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body>
<p>Thanks Jesper,</p>
<div class="moz-cite-prefix">On 5/6/20 1:15 PM, Jesper Louis
Andersen wrote:<br>
</div>
<blockquote type="cite"
cite="mid:CAGrdgiVF4OAfvxiacc2Og7R7kzjWgK_MiRYoM+217Rz2wffpnA@mail.gmail.com">
<meta http-equiv="content-type" content="text/html; charset=UTF-8">
<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"
moz-do-not-send="true">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>
</div>
</div>
</blockquote>
<p>Using symbolic execution is what I was planning for. I could use
your other suggestions if the SUT would always be under my
control, but I hope to be able to use the same tests for the
system my application replaces.</p>
<p>It seems to work when I use the result of the calls in the
next_state/3 function:</p>
<p>next_state(#state{pcs = PCs} = State, {ok, PC}, {call, pm_pap,
c_pc, [_PC]}) -><br>
State#state{pcs = [PC | PCs]};</p>
Is it really this simple? There was something in the back of my
memory about not using the result argument for updating the state.<br>
<blockquote type="cite"
cite="mid:CAGrdgiVF4OAfvxiacc2Og7R7kzjWgK_MiRYoM+217Rz2wffpnA@mail.gmail.com">
<div dir="ltr">-- <br>
<div dir="ltr" class="gmail_signature">J.</div>
</div>
</blockquote>
<br>
</body>
</html>