Codebase list erlang-proper / HEAD test / pdict_statem.erl
HEAD

Tree @HEAD (Download .tar.gz)

pdict_statem.erl @HEAD — raw · history · blame 

  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
%%% Copyright 2010-2014 Manolis Papadakis <manopapad@gmail.com>,
%%%                     Eirini Arvaniti <eirinibob@gmail.com>
%%%                 and Kostis Sagonas <kostis@cs.ntua.gr>
%%%
%%% This file is part of PropEr.
%%%
%%% PropEr is free software: you can redistribute it and/or modify
%%% it under the terms of the GNU General Public License as published by
%%% the Free Software Foundation, either version 3 of the License, or
%%% (at your option) any later version.
%%%
%%% PropEr is distributed in the hope that it will be useful,
%%% but WITHOUT ANY WARRANTY; without even the implied warranty of
%%% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
%%% GNU General Public License for more details.
%%%
%%% You should have received a copy of the GNU General Public License
%%% along with PropEr.  If not, see <http://www.gnu.org/licenses/>.

%%% @copyright 2010-2014 Manolis Papadakis, Eirini Arvaniti and Kostis Sagonas
%%% @version {@version}
%%% @author Kresten Krab Thorup, edited by Eirini Arvaniti
%%% @doc Simple statem test for the process dictionary

-module(pdict_statem).

-export([test/0, test/1]).
-export([initial_state/0, command/1, precondition/2, postcondition/3,
	 next_state/3]).
-export([set_up/0, clean_up/0]).

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

-define(KEYS, [a,b,c,d]).

%% A simple statem test for the process dictionary; tests the
%% operations erlang:put/2, erlang:get/1, erlang:erase/1.

test() ->
    test(100).

test(N) ->
    proper:quickcheck(?MODULE:prop_pdict(), N).

prop_pdict() ->
    ?FORALL(Cmds, commands(?MODULE),
	    begin
		set_up(),
		{H,S,Res} = run_commands(?MODULE, Cmds),
		clean_up(),
		?WHENFAIL(
		   io:format("History: ~w\nState: ~w\nRes: ~w\n", [H, S, Res]),
		   aggregate(command_names(Cmds), Res =:= ok))
	    end).

set_up() -> ok.

clean_up() ->
    lists:foreach(fun(Key) -> erlang:erase(Key) end, ?KEYS).

key() ->
    elements(?KEYS).

initial_state() ->
    [KV || {Key, _} = KV <- erlang:get(), lists:member(Key, ?KEYS)].

command([]) ->
    {call,erlang,put,[key(),integer()]};
command(Props) ->
    ?LET({Key, Value}, weighted_union([{2, elements(Props)},
				       {1, {key(), integer()}}]),
	 oneof([{call,erlang,put,[Key,Value]},
		{call,erlang,get,[Key]},
		{call,erlang,erase,[Key]}])).

precondition(_, {call,erlang,put,[_,_]}) ->
    true;
precondition(Props, {call,erlang,get,[Key]}) ->
    proplists:is_defined(Key, Props);
precondition(Props, {call,erlang,erase,[Key]}) ->
    proplists:is_defined(Key, Props).

postcondition(Props, {call,erlang,put,[Key,_]}, undefined) ->
    not proplists:is_defined(Key, Props);
postcondition(Props, {call,erlang,put,[Key,_]}, Old) ->
    {Key,Old} =:= proplists:lookup(Key, Props);
postcondition(Props, {call,erlang,get,[Key]}, Val) ->
    {Key,Val} =:= proplists:lookup(Key, Props);
postcondition(Props, {call,erlang,erase,[Key]}, Val) ->
    {Key,Val} =:= proplists:lookup(Key, Props).

next_state(Props, _Var, {call,erlang,put,[Key,Value]}) ->
    %% correct model
    [{Key,Value}|proplists:delete(Key, Props)];
    %% wrong model
%% Props ++ [{Key,Value}];
next_state(Props, _Var, {call,erlang,erase,[Key]}) ->
    proplists:delete(Key, Props);
next_state(Props, _Var, {call,erlang,get,[_]}) ->
    Props.