[erlang-questions] PropEr statem: what does Res::term in next_state/3 mean?

[Manolis Papadakis]

The first definition of the next_state/3 clause corresponds to the real 
code example, where the server returns a single password on each account 
creation. In this scenario, next_state/3 will be called in two possible 
contexts: during the generation of a command sequence, where V will be a 
symbolic variable (e.g. {var,42}), and during actual testing, where V 
will be an actual concrete password, as returned by the server (e.g. 
"Password1" -- a fairly secure password: it contains capital and 
lowercase letters, and even numbers).

The second definition assumes a slightly different server interface, 
where create_account/1 returns a list of passwords, and the client is 
expected to only use the first one (this is obviously a contrived 
example). This alternative scenario is used to emphasize a side effect 
of the dual nature of next_state/3: Because it may be called with both 
symbolic and concrete values, it shouldn't treat its argument in a 
manner that is invalid for symbolic values.

In the first scenario, we simply add the returned value to a list, which 
makes sense for both symbolic and concrete values, and is thus allowed. 
In the second scenario, however, we'd want to get the first password 
from the returned list of passwords and only store that in our model. If 
next_state/3 were to only be called with concrete values (e.g. 
["Password1","123456","qwerty"]), then we would simply retrieve the head 
of the list directly:

%% WRONG CODE
next_state(S, V, {call,_,create_account,[_Name]}) ->
     S#state{users = [hd(V)|S#state.users]};

However, next_state/3 may also be called with a symbolic value, e.g. 
{var,42}, so the above code (which assumes that V is a list), will 
break. The way around this is to use symbolic calls to perform any 
computation that depends on the structure of the result:

next_state(S, V, {call,_,create_account,[_Name]}) ->
     S#state{users = [{call,erlang,hd,[V]}|S#state.users]};

PropEr will automatically evaluate the symbolic calls every time 
next_state/3 is called with concrete values.

On 05/30/2012 02:34 PM, Motiejus Jakštys wrote:
> Hi, PropEr team,
>
> sorry for writing you (again) on holiday time. ;)
>
> I was reading about proper_statem, and could not understand one thing.
>  From PropEr tutorial[1]:
> next_state(S, V, {call,_,create_account,[_Name]}) ->
>      S#state{users = [V|S#state.users]};
>
> <some text about the callback...>  Instead, next_state/3 should return:
>
> S#state{users = [{call,erlang,hd,[V]}|S#state.users]}
>
> Two things are unclear:
> 1. What is V after all?
> 2. How can I return abstract code in *my own state*? I.e. does PropEr
> do some magic to look at my state and call the appropriate commands?
>
> I read the edoc[2] too, but still it didn't make it clearer.
>
> [1]: http://proper.softlab.ntua.gr/Tutorials/PropEr_testing_of_generic_servers.html
> [2]: file:///home/motiejus/code/erlmpc/deps/proper/doc/index.html
>
> I would be very glad if you could shed some light on this.
>
> Thanks a lot,
> Motiejus Jakštys