Water Jugs puzzle with QuickCheck/PropEr

erlang_shell.txt

1> c("jug_statem.erl").
{ok,jug_statem}


2> jug_statem:test(100).
....................................................................................................
OK: Passed 100 test(s).

18% {jug_statem,fill_big,0}
17% {jug_statem,big_to_small,0}
16% {jug_statem,empty_small,0}
16% {jug_statem,fill_small,0}
15% {jug_statem,small_to_big,0}
15% {jug_statem,empty_big,0}
true

3> jug_statem:test(1000).
.....................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................!
Failed: After 646 test(s).
...
Shrinking .....(5 time(s))
[{set,{var,16},{call,movie_statem,fill_big,[]}},{set,{var,18},{call,movie_statem,big_to_small,[]}},{set,{var,20},{call,movie_statem,empty_small,[]}},{set,{var,21},{call,movie_statem,big_to_small,[]}},{set,{var,25},{call,movie_statem,fill_big,[]}},{set,{var,26},{call,movie_statem,big_to_small,[]}},{set,{var,27},{call,movie_statem,small_to_big,[]}}]
History: [{{state,0,0},ok},{{state,0,5},ok},{{state,3,2},ok},{{state,0,2},ok},{{state,2,0},ok},{{state,2,5},ok},{{state,3,4},ok}]
State: {state,3,4}
Result: {postcondition,false}
false

jug_statem.erl

-module(jug_statem).

-behaviour(proper_statem).

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

-export([test/1]).

-export([big_to_small/0, empty_big/0, empty_small/0,
	 fill_big/0, fill_small/0, small_to_big/0]).

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

-record(state,
	{small  :: pos_integer(), big  :: pos_integer()}).

%%--------------------------------------------------------------------
%%% Statem callbacks
%%--------------------------------------------------------------------

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

prop_never_four_litres() ->
    ?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{small = 0, big = 0}.

command(_S) ->
    frequency([{1, {call, ?MODULE, fill_small, []}},
	       {1, {call, ?MODULE, fill_big, []}}]
		++
		[{1, {call, ?MODULE, empty_small, []}}] ++
		  [{1, {call, ?MODULE, empty_big, []}}] ++
		    [{1, {call, ?MODULE, big_to_small, []}}] ++
		      [{1, {call, ?MODULE, small_to_big, []}}]).

%%-----------------------------------------------------------------------------
%% Mock commands
%%-----------------------------------------------------------------------------

fill_small() -> ok.

fill_big() -> ok.

empty_small() -> ok.

empty_big() -> ok.

small_to_big() -> ok.

big_to_small() -> ok.

%%-----------------------------------------------------------------------------
%% Preconditions
%%-----------------------------------------------------------------------------

precondition(_, _) -> true.

%%-----------------------------------------------------------------------------
%% Transitions
%%-----------------------------------------------------------------------------

next_state(S, _V, {call, _, fill_small, []}) ->
    S#state{small = 3};
next_state(S, _V, {call, _, fill_big, []}) ->
    S#state{big = 5};
next_state(S, _V, {call, _, empty_small, []}) ->
    S#state{small = 0};
next_state(S, _V, {call, _, empty_big, []}) ->
    S#state{big = 0};
next_state(#state{small = Small, big = Big}, _V,
	   {call, _, small_to_big, []})
    when Small + Big =< 5 ->
    #state{small = 0, big = Small + Big};
next_state(#state{small = Small, big = Big}, _V,
	   {call, _, small_to_big, []}) ->
    #state{small = Small + Big - 5, big = 5};
next_state(#state{small = Small, big = Big}, _V,
	   {call, _, big_to_small, []})
    when Small + Big =< 3 ->
    #state{small = Small + Big, big = 0};
next_state(#state{small = Small, big = Big}, _V,
	   {call, _, big_to_small, []}) ->
    #state{small = 3, big = Small + Big - 3}.

%%-----------------------------------------------------------------------------
%% Postconditions
%%-----------------------------------------------------------------------------

postcondition(S, {call, _, small_to_big, []},
	      _Result) ->
    S#state.big =/= 4;
postcondition(S, {call, _, big_to_small, []},
	      _Result) ->
    S#state.big =/= 4;
postcondition(_, _, _) -> true.