Stateful properties and application assigned identifiers

[Frans Schneider]

Dear list,

I have an application in which each new entity is assigned a unique id
(UUID) during runtime. All functions related to such an entity use this
id as a reference. I am in the process of writing property based tests
using PropEr using stateful properties. The problem I run into is how to
handle the system generated ids.

For example, I create something called a policy class with the call
pm_pap:c_pc(#pc{value=...}). This returns the record #pc{id=<<some
uuid>>, value=...}. Now, to delete the policy class, the call
pm_pap:d_pc(Id) is made with the id as returned by the pm_pap:c_pc/1 call.

For the commands/1 and next_state/3 and generator pc() I use something like:

command(#state{pcs = []}) ->
    {call, pm_pap, c_pc, [pc()]};
command(#state{pcs = [PC | _]}) ->
    {call, pm_pap, d_pc, [PC]};
...

next_state(#state{pcs = PCs} = State, _Res, {call, pm_pap, c_pc, [PC]}) ->
    State#state{pcs = [PC | PCs]};
next_state(State, _Res, {call, _Mod, _Fun, _Args}) ->
    NewState = State,
    NewState.

pc() ->
    ?LET(Name, string(), #pc{value = Name}).

During the first phase of the test run, obviously the id's are not yet
generated because no calls are made to the actual system. Using the PC
from the state in the command to delete the PC will than of course fail
because the PC in the state has doesn't have a valid id when the
symbolic call is created.

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?

Thanks,

Frans

[Jesper Louis Andersen]

On Wed, May 6, 2020 at 10:27 AM Frans Schneider <fchsch...@gmail.com> 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.

[Frans Schneider]

Thanks Jesper,

On 5/6/20 1:15 PM, Jesper Louis Andersen wrote:

On Wed, May 6, 2020 at 10:27 AM Frans Schneider <fchsch...@gmail.com> 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.

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.

It seems to work when I use the result of the calls in the next_state/3 function:

next_state(#state{pcs = PCs} = State, {ok, PC}, {call, pm_pap, c_pc, [_PC]}) ->

    State#state{pcs = [PC | PCs]};

Is it really this simple? There was something in the back of my memory about not using the result argument for updating the state.

--

J.

[Jacob]

Hello,

On 06.05.20 13:15, Jesper Louis Andersen wrote:
> On Wed, May 6, 2020 at 10:27 AM Frans Schneider <fchsch...@gmail.com
> <mailto:fchsch...@gmail.com>> 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.

We are successfully using a similar approach without the above
restriction concerning postconditions with PropEr for a rather complex
system.
The basic idea is to use a symbolic reference which can be evaluated the
the real id in the first phase where the command list is created. When
the commands are actually run, the real reference is used and can thus
be used in postconditions.

Example:

Assuming having a function create(Arg :: term()) -> {ok, Ref :: term()}
in the success case. I'm using a shim here (see
https://propertesting.com/book_state_machine_properties.html) to ensure
that we have the success case only.

The following code is just an illustration of the principle.

1. Get a reference term in next_state:

next_state(State = #{objs := Objs}, Res, {call, sut_shim, create,
[success, Arg]}) ->
Ref = get_ref(Res),
State#{objs => Objs#{Ref => Arg}}.

Note the Res will either be {var, N} (symbolic run) or {ok, RealRef}
(run with SUT). The magic lies in

get_ref({var, _} = Res) ->
{call, ?MODULE, get_ref, [Res]};
get_ref({ok, RealRef}) ->
RealRef.

As long as you always take Ref as opaque, it doesn't really matter which
of the two variants are used in the State.

It is important that this reference is only created in one place, since
in the symbolic run the Ref term will also include N which is different
for each command in the row. So a 'create' followed by some 'lookup' for
the same object would each provide a different Ref in the symbolic run
but (probably) the same Ref in the run with the SUT.

2. When generating subsequent commands, the keys in 'objs' can be used
as references for existing objects. Here the will always have the form
{call, ?MODULE, get_ref, [{var, N}]} having the advantage of being quite
comprehensible when inspecting the generated command lists.

3. In subsequent preconditions or next_state invocations you'll have to
search 'objs' based on the values (Arg) in State if you need the
reference unless its already part of the generated command arguments.
Note that the reference will have the form {call, ...} in the symbolic
run and the evaluated RealRef in the SUT run. This isn't an issue as
long as handle this as an opaque reference only.

4. In the postconditions, you will always have the evaluated RealRef as
objs key, so you can compare it with anything you get from the SUT when
executing another command.

HTH,

Jacob

[Schneider]

Perfect! Thanks

> Op 7 mei 2020 om 12:30 heeft Jacob <jac...@gmx.net> het volgende geschreven:
>
> Hello,