Stateful properties and application assigned identifiers

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

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