Stateful properties and application assigned identifiers

[Jesper Louis Andersen]

On Wed, May 6, 2020 at 10:27 AM Frans Schneider <fchschneider@REDACTED>
wrote:

> The general question I have is how to handle things like dynamic
> generated id's or processes in stateful properties. Does somebody have
> an example of doing this?
>
>
Two general tactics for this (with one bonus tactic):

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.

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:

create() ->
  {ok, Pid} = s:spawn(),
  Pid.

+++

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.

+++

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].

[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.


-- 
J.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://erlang.org/pipermail/erlang-questions/attachments/20200506/adb83076/attachment.htm>