Stateful properties and application assigned identifiers

[Jacob]

Hello,

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

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