[erlang-questions] PropEr and the symbolic variables

[Magnus Henoch]

Aaron France <aaron.l.france@REDACTED> writes:

> Hi all,
>
> I'm creating a statem for a stateful system and am trying to model the
> various API calls.
>
> Essentially the system is a PUT/DELETE rest service, you can PUT data
> which is forevermore available via a further GET call and you can also
> DELETE said data and subsequent GETs will fail.
>
> This works well, mostly. However, I am not able to satisfactorily
> maintain what the state of the system is due to receiving symbolic
> variables in my next state function.
>
> Basically I am recording the state as:
>
> state{ dict() }
>
> and the dict contains:
>
> { username => boolean() }. Where the boolean represents whether that
> user has data which is in the system.
>
> The problem comes from the fact that my API calls return a status code
> for how the API call succeeded. Imagine deleting an already deleted
> piece of data, it would return e.g. a 404 instead of a 204. I model
> the state accordingly.
>
> When I receive the `Res` argument to my next_state/3 function, it is
> only sometimes a concrete value which I need. However, I need to
> change the state conditionally according to what that `Res` value is.
>
> Any ideas?

The basic idea is that since you're keeping track of the state in your
property, you know whether the API call should succeed or fail even
before you make the call.  If the item you are deleting was in the
dictionary before the call, then you should get a 204, otherwise you
should get a 404.  Something like:

next_state(State = #state{existing_usernames = Usernames},
           _Result,
           {call, _, delete, [Username]}) ->
    case lists:member(Username, Usernames) of
        true ->
            %% The user existed before deletion
            State#state{existing_usernames = Usernames -- [Username]};
        false ->
            %% The user didn't exist before deletion
            State
    end.

(In fact, in the example above you could unconditionally remove the
user, since the -- operator does nothing if what you're trying to remove
doesn't exist.)

You only really care about the status code in the postcondition
function, which is guaranteed to always get real return values, never
symbolic ones:

postcondition(#state{existing_usernames = Usernames},
              {call, _, delete, [Username]},
              StatusCode) ->
    case lists:member(Username, Usernames) of
        true ->
            StatusCode =:= 204;
        false ->
            StatusCode =:= 404
    end.

Hope this helps,
Magnus