[erlang-questions] PropEr and the symbolic variables

[Aaron France]

Ah yes! That's a great conceptual help. It's very much more 'Zen' to 
trust in the postcondition to do the right thing and to assume in the 
next_state function.

Thanks!

On 17/09/13 18:52, Magnus Henoch wrote:
> 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