Stateful properties and application assigned identifiers

[Schneider]

Perfect! Thanks

> Op 7 mei 2020 om 12:30 heeft Jacob <jacob01@REDACTED> het volgende geschreven:
> 
> 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