From 136a7b4055f4f57ab4517e7d8267ffb0ed197590 Mon Sep 17 00:00:00 2001 From: Issac Trotts Date: Sun, 1 Jan 2017 19:18:56 -0800 Subject: [PATCH 1/5] Fix issue #132: Pretty print call sequences. https://github.com/manopapad/proper/issues/132 --- src/proper.erl | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/proper.erl b/src/proper.erl index 454bd804..613d00aa 100644 --- a/src/proper.erl +++ b/src/proper.erl @@ -1822,7 +1822,7 @@ print_imm_clean_input({'$conjunction',SubImmCExms}, Prefix, Print) -> end, lists:foreach(PrintSubImmCExm, SubImmCExms); print_imm_clean_input(Instance, Prefix, Print) -> - Print(Prefix ++ "~w~n", [Instance]). + Print(Prefix ++ "~s~n", [io_lib_pretty:print(Instance)]). -spec execute_actions(fail_actions()) -> 'ok'. execute_actions(Actions) -> From 9d30b5a2ea78faf21875575d6793f3303fe1afdd Mon Sep 17 00:00:00 2001 From: Issac Trotts Date: Mon, 2 Jan 2017 13:20:48 -0800 Subject: [PATCH 2/5] Allow an optional message in postconditions. This makes it a lot easier to understand what went wrong when a test fails. This fixes https://github.com/manopapad/proper/issues/131. --- examples/ets_statem.erl | 10 +++++++--- examples/pdict_statem.erl | 19 ++++++++++++++----- src/proper_statem.erl | 5 +++++ 3 files changed, 26 insertions(+), 8 deletions(-) diff --git a/examples/ets_statem.erl b/examples/ets_statem.erl index b8527f51..64f4131f 100644 --- a/examples/ets_statem.erl +++ b/examples/ets_statem.erl @@ -172,13 +172,15 @@ postcondition(S, {call,_,update_counter,[_Tab, Key, Incr]}, Res) -> lists:keyfind(Key, 1, S#state.stored) end, Value = element(2, Object), - Res =:= Value + Incr; + Pred = Res =:= Value + Incr, + Msg = "update_counter should return the result of updating the counter.", + {Pred, Msg}; postcondition(_S, {call,_,delete,[_Tab, _Key]}, Res) -> Res =:= true; postcondition(_S, {call,_,insert,[_Tab, _Object]}, Res) -> Res =:= true; postcondition(S, {call,_,lookup_element,[_Tab, Key, Pos]}, Res) -> - case S#state.type of + Pred = case S#state.type of ordered_set -> Res =:= element(Pos, lists:keyfind(Key, 1, S#state.stored)); set -> @@ -186,7 +188,9 @@ postcondition(S, {call,_,lookup_element,[_Tab, Key, Pos]}, Res) -> _ -> Res =:= [element(Pos, Tuple) || Tuple <- proplists:lookup_all(Key, S#state.stored)] - end. + end, + Msg = "lookup_element should return the result of looking up the element", + {Pred, Msg}. %%% Sample properties diff --git a/examples/pdict_statem.erl b/examples/pdict_statem.erl index bc806e08..9e178954 100644 --- a/examples/pdict_statem.erl +++ b/examples/pdict_statem.erl @@ -81,15 +81,24 @@ precondition(_, _) -> false. postcondition(Props, {call,erlang,put,[Key,_]}, undefined) -> - not proplists:is_defined(Key, Props); + Msg = "put should only return undefined if the key is new.", + Pred = not proplists:is_defined(Key, Props), + {Pred, Msg}; postcondition(Props, {call,erlang,put,[Key,_]}, Old) -> - {Key,Old} =:= proplists:lookup(Key, Props); + Msg = "put should return the old value for the key if there is one.", + Pred = {Key,Old} =:= proplists:lookup(Key, Props), + {Pred, Msg}; postcondition(Props, {call,erlang,get,[Key]}, Val) -> - {Key,Val} =:= proplists:lookup(Key, Props); + Msg = "get should return the correct value for the key", + Pred = {Key,Val} =:= proplists:lookup(Key, Props), + {Pred, Msg}; postcondition(Props, {call,erlang,erase,[Key]}, Val) -> - {Key,Val} =:= proplists:lookup(Key, Props); + Msg = "If erase returns a value, it should be the old value for the key", + Pred = {Key,Val} =:= proplists:lookup(Key, Props), + {Pred, Msg}; postcondition(_, _, _) -> - false. + Msg = "Default case", + {false, Msg}. next_state(Props, _Var, {call,erlang,put,[Key,Value]}) -> %% correct model diff --git a/src/proper_statem.erl b/src/proper_statem.erl index 815a0e81..f72a0d6d 100644 --- a/src/proper_statem.erl +++ b/src/proper_statem.erl @@ -538,8 +538,13 @@ run_commands(Cmds, Env, Mod, History, State) -> true -> State2 = proper_symb:eval(Env2, Mod:next_state(State, Res, Call)), run_commands(Rest, Env2, Mod, History2, State2); + {true,_Msg} -> + State2 = proper_symb:eval(Env2, Mod:next_state(State, Res, Call)), + run_commands(Rest, Env2, Mod, History2, State2); false -> {{lists:reverse(History2), State, {postcondition,false}}, []}; + {false,Msg} -> + {{lists:reverse(History2), State, {postcondition,false,Msg}}, []}; {exception,_,_,_} = Exception -> {{lists:reverse(History2), State, {postcondition,Exception}}, []} end; From 61a1ca0a1e844c4113ef74d49495b03daf0ee999 Mon Sep 17 00:00:00 2001 From: Issac Trotts Date: Mon, 2 Jan 2017 13:43:07 -0800 Subject: [PATCH 3/5] Fix broken spec for check_postcondition(). This was found by a dialyzer run: https://travis-ci.org/manopapad/proper/jobs/188348558 dialyzer -n -nn --plt .plt/proper_plt -Wunmatched_returns ebin --- src/proper_statem.erl | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/proper_statem.erl b/src/proper_statem.erl index f72a0d6d..15d243a0 100644 --- a/src/proper_statem.erl +++ b/src/proper_statem.erl @@ -568,7 +568,7 @@ check_precondition(Mod, State, Call) -> end. -spec check_postcondition(mod_name(), dynamic_state(), symbolic_call(), term()) -> - boolean() | proper:exception(). + boolean() | {boolean(), string()} | proper:exception(). check_postcondition(Mod, State, Call, Res) -> try Mod:postcondition(State, Call, Res) catch From a0a1953275fe6549191c2478b815dbcce61071ef Mon Sep 17 00:00:00 2001 From: Issac Trotts Date: Sat, 7 Jan 2017 14:00:46 -0800 Subject: [PATCH 4/5] Make it easier to try adding bugs and finding them Instead of testing methods on the erlang module, test proxies for them on ?MODULE so it's easy to replace them with buggy versions and see if the bugs are found. Also the error messages have been improved, comparing what happened to what was meant to happen. --- examples/pdict_statem.erl | 100 ++++++++++++++++++++++---------------- 1 file changed, 59 insertions(+), 41 deletions(-) diff --git a/examples/pdict_statem.erl b/examples/pdict_statem.erl index 9e178954..3b1b50c6 100644 --- a/examples/pdict_statem.erl +++ b/examples/pdict_statem.erl @@ -20,21 +20,27 @@ %%% @copyright 2010-2011 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 +%%% @doc Simple statem test for a modified API to the process dictionary -module(pdict_statem). -behaviour(proper_statem). +-export([get/1, put/2, erase/1]). -export([test/0, test/1]). -export([initial_state/0, command/1, precondition/2, postcondition/3, - next_state/3]). + next_state/3]). -include_lib("proper/include/proper.hrl"). -define(KEYS, [a,b,c,d]). +%%% New API in which only get/1 returns an interesting value. +get(K) -> erlang:get(K). +put(K,V) -> erlang:put(K,V). +erase(K) -> erlang:erase(K). + %% A simple statem test for the process dictionary; tests the -%% operations erlang:put/2, erlang:get/1, erlang:erase/1. +%% operations ?MODULE:put/2, ?MODULE:get/1, ?MODULE:erase/1. test() -> test(100). @@ -44,14 +50,17 @@ test(N) -> prop_pdict() -> ?FORALL(Cmds, commands(?MODULE), - begin - {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). + begin + {H,S,Res} = run_commands(?MODULE, Cmds), + clean_up(), + ?WHENFAIL( + begin + {_, _, Msg} = Res, + io:format("History: ~p~nState: ~p~nMsg: ~s~n", + [H, S, Msg]) + end, + aggregate(command_names(Cmds), Res =:= ok)) + end). clean_up() -> lists:foreach(fun(Key) -> erlang:erase(Key) end, ?KEYS). @@ -62,50 +71,59 @@ key() -> initial_state() -> []. command([]) -> - {call,erlang,put,[key(), integer()]}; + {call,?MODULE,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]} - ])). + {1, {key(),integer()}}]), + oneof([{call,?MODULE,put,[Key,Value]}, + {call,?MODULE,get,[Key]}, + {call,?MODULE,erase,[Key]} + ])). -precondition(_, {call,erlang,put,[_,_]}) -> +precondition(_Props, {call,?MODULE,put,[_Key,_Val]}) -> true; -precondition(Props, {call,erlang,get,[Key]}) -> +precondition(Props, {call,?MODULE,get,[Key]}) -> proplists:is_defined(Key, Props); -precondition(Props, {call,erlang,erase,[Key]}) -> +precondition(Props, {call,?MODULE,erase,[Key]}) -> proplists:is_defined(Key, Props); precondition(_, _) -> false. -postcondition(Props, {call,erlang,put,[Key,_]}, undefined) -> - Msg = "put should only return undefined if the key is new.", - Pred = not proplists:is_defined(Key, Props), - {Pred, Msg}; -postcondition(Props, {call,erlang,put,[Key,_]}, Old) -> - Msg = "put should return the old value for the key if there is one.", - Pred = {Key,Old} =:= proplists:lookup(Key, Props), - {Pred, Msg}; -postcondition(Props, {call,erlang,get,[Key]}, Val) -> +postcondition(Props, {call,?MODULE,put,[Key,_]}, Result) -> + case proplists:lookup(Key, Props) of + none -> + Pred = (Result =:= undefined), + Msg = io_lib:format("Want put(~p, _) to return undefined, got ~p.", [Key, Result]), + {Pred, Msg}; + {Key, OldVal} -> + Pred = (OldVal =:= Result), + Msg = io_lib:format("Want put(~p, _) to return old value ~p (props: ~p). Got ~p.", [Key, OldVal, Props, Result]), + {Pred, Msg} + end; +postcondition(Props, {call,?MODULE,get,[Key]}, Val) -> Msg = "get should return the correct value for the key", Pred = {Key,Val} =:= proplists:lookup(Key, Props), {Pred, Msg}; -postcondition(Props, {call,erlang,erase,[Key]}, Val) -> - Msg = "If erase returns a value, it should be the old value for the key", - Pred = {Key,Val} =:= proplists:lookup(Key, Props), - {Pred, Msg}; +postcondition(Props, {call,?MODULE,erase,[Key]}, Result) -> + case proplists:lookup(Key, Props) of + none -> + Msg = io_lib:format("Want Result to be undefined, got ~p.", [Result]), + Pred = (Result =:= undefined), + {Pred, Msg}; + {Key, ModelVal} -> + Pred = (ModelVal =:= Result), + Msg = io_lib:format("Want erase(~p) to return old value ~p. Got ~p.", [Key, ModelVal, Result]), + {Pred, Msg} + end; postcondition(_, _, _) -> Msg = "Default case", {false, Msg}. -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,[_]}) -> +next_state(Props, _Var, {call,?MODULE,put,[Key,Value]}) -> + NewProps = [{Key,Value}|proplists:delete(Key, Props)], + NewProps; +next_state(Props, _Var, {call,?MODULE,erase,[Key]}) -> + NewProps = proplists:delete(Key, Props), + NewProps; +next_state(Props, _Var, {call,?MODULE,get,[_]}) -> Props. From 440b1c0164a0e343fc360dc3a24bb3528ead0b61 Mon Sep 17 00:00:00 2001 From: Issac Trotts Date: Sun, 8 Jan 2017 14:08:36 -0800 Subject: [PATCH 5/5] Change put and erase to always return ok. This makes it a bit more challenging for PropEr to find bugs since it has less information to go on, so it makes for a slightly more interesting example. The change made it necessary to change the precondition for get/1 to always return true since we need to be able to get keys that should be undefined to detect if the erase function is no longer working. --- examples/pdict_statem.erl | 54 ++++++++++++++++++--------------------- 1 file changed, 25 insertions(+), 29 deletions(-) diff --git a/examples/pdict_statem.erl b/examples/pdict_statem.erl index 3b1b50c6..d798d23b 100644 --- a/examples/pdict_statem.erl +++ b/examples/pdict_statem.erl @@ -36,8 +36,12 @@ %%% New API in which only get/1 returns an interesting value. get(K) -> erlang:get(K). -put(K,V) -> erlang:put(K,V). -erase(K) -> erlang:erase(K). +put(K,V) -> + erlang:put(K,V), + ok. +erase(K) -> + erlang:erase(K), + ok. %% A simple statem test for the process dictionary; tests the %% operations ?MODULE:put/2, ?MODULE:get/1, ?MODULE:erase/1. @@ -82,39 +86,31 @@ command(Props) -> precondition(_Props, {call,?MODULE,put,[_Key,_Val]}) -> true; -precondition(Props, {call,?MODULE,get,[Key]}) -> - proplists:is_defined(Key, Props); +precondition(_Props, {call,?MODULE,get,[_Key]}) -> + true; precondition(Props, {call,?MODULE,erase,[Key]}) -> proplists:is_defined(Key, Props); precondition(_, _) -> false. -postcondition(Props, {call,?MODULE,put,[Key,_]}, Result) -> - case proplists:lookup(Key, Props) of - none -> - Pred = (Result =:= undefined), - Msg = io_lib:format("Want put(~p, _) to return undefined, got ~p.", [Key, Result]), - {Pred, Msg}; - {Key, OldVal} -> - Pred = (OldVal =:= Result), - Msg = io_lib:format("Want put(~p, _) to return old value ~p (props: ~p). Got ~p.", [Key, OldVal, Props, Result]), - {Pred, Msg} - end; -postcondition(Props, {call,?MODULE,get,[Key]}, Val) -> - Msg = "get should return the correct value for the key", - Pred = {Key,Val} =:= proplists:lookup(Key, Props), +postcondition(_Props, {call,?MODULE,put,[Key,Val]}, Result) -> + Want = ok, + Pred = (Result =:= Want), + Msg = io_lib:format("Want put(~p, ~p) to return ~p, got ~p\n", [Key, Val, Want, Result]), + {Pred, Msg}; +postcondition(Props, {call,?MODULE,get,[Key]}, Result) -> + Want = case proplists:lookup(Key, Props) of + none -> undefined; + {Key, Val} -> Val + end, + Pred = (Result =:= Want), + Msg = io_lib:format("Want get(~p) to return ~p, got ~p\n", [Key, Want, Result]), + {Pred, Msg}; +postcondition(_Props, {call,?MODULE,erase,[_Key]}, Result) -> + Want = ok, + Pred = (Result =:= Want), + Msg = io_lib:format("Want Result to be ~p, got ~p\n", [Want, Result]), {Pred, Msg}; -postcondition(Props, {call,?MODULE,erase,[Key]}, Result) -> - case proplists:lookup(Key, Props) of - none -> - Msg = io_lib:format("Want Result to be undefined, got ~p.", [Result]), - Pred = (Result =:= undefined), - {Pred, Msg}; - {Key, ModelVal} -> - Pred = (ModelVal =:= Result), - Msg = io_lib:format("Want erase(~p) to return old value ~p. Got ~p.", [Key, ModelVal, Result]), - {Pred, Msg} - end; postcondition(_, _, _) -> Msg = "Default case", {false, Msg}.