use previous return value as parameter of new command in new state

[Spycsh]

Hi!

I tried to store the return value of a function call {call, _Mod, _Fun, _Args} in state so the next command generated can use the result of the previous function call as a parameter. However that seems impossible. Firstly I store the return value of the function call {call, _Mod, _Fun, _Args} in the State in next_state function, and then when I search for the value in command/1, I can only find tuples with the form like {var, _Count}, and afterwards I learn that command generation is likely in different loops in proper_statem.erl file so it cannot use the state value that is in run_command/2 in another loop, which means that the return value we get from next_state that called by run_command/2, which may be a random pid or something, cannot be passed as a parameter for the command in the new state, when we try to generate some new commands. Is my understanding correct?

Thanks a lot in advance!

[kostis]

What you are trying to do is (kind of) standard in statem-based Property-Based Testing. For example, the following statem tutorial explains how to store the password chosen by a user (when registering in a server) in a symbolic variable and then use that information in subsequent commands. I think it will help you to read that tutorial and understand how it works.

If the information in that tutorial is insufficient for your use, perhaps you can show us here how your application differs from it (by posting its code or some link to it) and what more you would have liked to see explained or added in PropEr. We can try to add this information in that or in some other tutorial.

From the current description, it seems to me that this is more of an issue in how you are trying to (ab)use statem's API rather than an issue in PropEr. But perhaps I am wrong. Some concrete code instead of an abstract description of the problem you are trying to solve will help.

[Spycsh]

Thanks for reply. Yes I have read the statem tutorial. Let's take movie_statem.erl for example. In the last state we run

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

that is to append the return value (password) of create_account to the state S#state.users. Later we will go to command/1 to generate a new command to run. My problem is that what if we want to use the return value in command/1? When I print out S#state.users in command/1 and next_state/3, they show totally different contents (although there must be some bindings). Actually, what is adopted in the file is to see whether S#state.users is empty, which is a clever way but we seem to be impossible to access the returned value "password" in the previous next_state, That means that we cannot access the exact return value (password) in the new command generation.

One potential problem from my scenario (a small draft, not the real code) is that if I in the next_state write

next_state(S, V, {call,_,get_random_pid_to_handle,_}) -> % get_random_pid_to_handle returns the pid,
                                                                                         % V is bound to the returned value
    S#state{pids = [V|S#state.pids]};

I cannot execute the process of "shut down with the pid" in the command/1 like

command(S) ->
    HasPid = (S#state.pids =/= []),                                              % this will work
    oneof([{call, ?SERVER, shut_down, [oneof(S#state.pids)]} || HasPid]). % this will not work because it cannot access the exact pid
                                                                  % so it cannot shut_down the connection to pid

Hope you can understand what I mean, thank a lot in advance!

[kostis]

I still do not understand what you mean and what you are trying to do which does not work. The fact that you are not showing us the real code (why?) but just a draft -with typos!- does not make it any easier... Anyway, I will try to guess what you are trying to do and reply here.

You have some command which returns a pid() - this is what the get_random_pid_to_handle command does. Then you (should) add this in the state{} record so that this Pid is known in the system at this point. This is (sort of) done with the next_state/3 function above ("sort of" because the body should read S#state{pids = [V|S#state.pids]}; instead). So far so good.

Now, if I understand correctly, you want to shut down that particular pid. There are two ways of doing this.

1. Either you do not have/keep any other Pids in the state (e.g. you've issued only one get_random_pid_to_handle call before in the command sequence) or use S#state{pids = [V]}, in which case the code you have for the shut_down command will work out of the box (once you use ?oneof(S#state.pids) instead of S#state.pid).
2. Or there are many Pids in the state. You can (try to) force this by using a precondition/2 for the shut_down command (and try your luck in command generation). An alternative is to keep a selected_pid field in the state and use that one.

If something is not clear, please show us the actual code and describe why/where it does not work.

[Spycsh]

-module(prop_example).
-include_lib("proper/include/proper.hrl").

-record(state, {pids  :: [] }).
% -export([initial_state/0, command/1, precondition/2, postcondition/3,
%    next_state/3, head/1]).
-compile(export_all).

prop_test() ->
    ?FORALL(Cmds, commands(?MODULE),
        ?TRAPEXIT(
           begin
           {History,State,Result} = run_commands(?MODULE, Cmds),
           ?WHENFAIL(io:format("History: ~w~nState: ~w\nResult: ~w~n",
                       [History,State,Result]),
                 aggregate(command_names(Cmds), Result =:= ok))
           end)).

initial_state() ->
    #state{pids = []}.

command(S) ->
    % io:format("the current state: ~p~n",[head(S#state.pids)]),
    HasPids = (S#state.pids =/= []),
    NotHasPids = (S#state.pids =:= []),
    oneof(
        [{call, prop_example, get_random_pid_to_handle, []} || NotHasPids] ++
        [{call, prop_example, shut_down, [head(S#state.pids)]} || HasPids]
    ).

precondition(S, {call, _, _, _}) ->
    true.

postcondition(S, {call, _, _, _}, _Res) ->
    true.

next_state(S, V, {call, _, get_random_pid_to_handle, _}) ->
    {_, Pid} = V,
    S#state{pids = [Pid|S#state.pids]};
next_state(S, V, {call, _, shut_down, [Pid]}) ->
    S#state{pids = lists:delete(Pid, S#state.pids)}.

%%% server api
get_random_pid_to_handle() ->
    N = rand:uniform(10),
    io:format("get pid: ~p~n", [N]),
    {ok, N}.    % notice here the system is specified to return a tuple, how can I get this N ?

shut_down(Pid) ->
    io:format("pid ~p is successfully shut down~n", [Pid]).

head([]) ->
    0;
head([H|T]) ->
    H.

Hi @kostis , thanks and I write a minimal example to show the problem. This piece of code should output two printing results (I try to simplify the real system I test). I expect the pid printed in two adjacent lines should be same. For example, the print log should display "get pid 5" and next line "pid 5 should be successfully shut down", which means that the pid number should be identical. However the Pid here is not identical. That is strange for me.

[Spycsh]

-module(prop_example).
-include_lib("proper/include/proper.hrl").

-record(state, {pids  :: [] }).
% -export([initial_state/0, command/1, precondition/2, postcondition/3,
%    next_state/3, head/1]).
-compile(export_all).

prop_test() ->
    ?FORALL(Cmds, commands(?MODULE),
        ?TRAPEXIT(
           begin
           {History,State,Result} = run_commands(?MODULE, Cmds),
           ?WHENFAIL(io:format("History: ~w~nState: ~w\nResult: ~w~n",
                       [History,State,Result]),
                 aggregate(command_names(Cmds), Result =:= ok))
           end)).

initial_state() ->
    #state{pids = []}.

command(S) ->
    % io:format("the current state: ~p~n",[head(S#state.pids)]),
    HasPids = (S#state.pids =/= []),
    NotHasPids = (S#state.pids =:= []),
    oneof(
        [{call, prop_example, get_random_pid_to_handle, []} || NotHasPids] ++
        [{call, prop_example, shut_down, [head(S#state.pids)]} || HasPids]
    ).

precondition(S, {call, _, _, _}) ->
    true.

postcondition(S, {call, _, _, _}, _Res) ->
    true.

next_state(S, V, {call, _, get_random_pid_to_handle, _}) ->
    % {_, Pid} = V,
    S#state{pids = [V|S#state.pids]};
next_state(S, V, {call, _, shut_down, [Pid]}) ->
    S#state{pids = lists:delete(Pid, S#state.pids)}.

%%% server api
get_random_pid_to_handle() ->
    N = rand:uniform(10),
    io:format("get pid: ~p~n", [N]),
    % {ok, N}.    % notice here the system is specified to return a tuple, how can I get this N ?
    N.

shut_down(Pid) ->
    io:format("pid ~p is successfully shut down~n", [Pid]).

head([]) ->
    0;
head([H|T]) ->
    H.

And I do some other experiments that if I change some lines to the code above, then I can get the correct result that the pid of adjacent printed lines to be identical. I suspect that I cannot do match of the result (namely the V) in next_state, and I do not know exactly why.

[kostis]

Both the statem tutorial and the example you sketched first had a code of the form:

next_state(S, V, {call, ...}) ->
   S#state{f = [V|S#state.f]};

This code works and does what you want to do.

You need to understand that V is a symbolic variable and that statem works on symbolic calls and arguments.

In your first code attempt, it seems to me that you are trying to to do pattern matching on symbolic variables and treat them as concrete terms (e.g. Pids). This can possibly work in PropEr, but only when using vanilla PBT, not when using statem's machinery. You cannot expect that things will work when you are not respecting the API.

I will close this issue now.