The next transition is a withdrawal. Naively, we add another command:
open(_Data) ->
[
{open, {call, bank_statem, deposit, [pos_integer()]}},
{open, {call, bank_statem, withdraw, [pos_integer()]}}
].
Which causes an immediate failure:
===> Testing prop_bank_statem:prop_test()
...
=ERROR REPORT==== 29-Apr-2018::15:08:41 ===
** State machine bank_statem terminating
** Last event = {{call,{,#Ref}},
{withdraw,2}}
** When server state = {open,#{balance => 1}}
** Reason for termination = error:function_clause
** Callback mode = state_functions
** Stacktrace =
** [{bank_statem,open,
[{call,{,#Ref}},
{withdraw,2},
#{balance => 1}],
[{file,"/app/_build/test/lib/bank_statem/src/bank_statem.erl"},
{line,46}]},
...
Crash dump is being written to: erl_crash.dump...done
Having the entire process crash isn’t very useful, so we follow the recommendation to use the TRAPEXIT macro:
prop_test() ->
?FORALL(Cmds, proper_fsm:commands(?MODULE),
?TRAPEXIT(
begin
bank_statem:start_link(),
{History,State,Result} = proper_fsm:run_commands(?MODULE, Cmds),
bank_statem:stop(),
?WHENFAIL(io:format("History: ~p\nState: ~p\nResult: ~p\n", [History,State,Result]),
aggregate(zip(proper_fsm:state_names(History), command_names(Cmds)), Result =:= ok))
end)).
This allows shrinking to take place, and gives us (slightly) more useful output:
===> Testing prop_bank_statem:prop_test()
.!
Failed: After 2 test(s).
A linked process died with reason {function_clause,[{bank_statem,open,[{call,{,#Ref}},{withdraw,3},#{balance=>0}],[{file,[47,97,112,112,47,95,98,117,105,108,100,47,116,101,115,116,47,108,105,98,47,98,97,110,107,95,115,116,97,116,101,109,47,115,114,99,47,98,97,110,107,95,115,116,97,116,101,109,46,101,114,108]},{line,46}]},{gen_statem,call_state_function,5,[{file,[103,101,110,95,115,116,97,116,101,109,46,101,114,108]},{line,1633}]},{gen_statem,loop_event_state_function,6,[{file,[103,101,110,95,115,116,97,116,101,109,46,101,114,108]},{line,1023}]},{proc_lib,init_p_do_apply,3,[{file,[112,114,111,99,95,108,105,98,46,101,114,108]},{line,247}]}]}.
=ERROR REPORT==== 29-Apr-2018::15:11:36 ===
** State machine bank_statem terminating
** Last event = {{call,{,#Ref}},
{withdraw,3}}
** When server state = {open,#{balance => 0}}
** Reason for termination = error:function_clause
** Callback mode = state_functions
** Stacktrace =
** [{bank_statem,open,
[{call,{,#Ref}},
{withdraw,3},
#{balance => 0}],
[{file,"/app/_build/test/lib/bank_statem/src/bank_statem.erl"},
{line,46}]},
...
[{set,{var,1},{call,bank_statem,withdraw,[3]}}]
Shrinking (0 time(s))
[{set,{var,1},{call,bank_statem,withdraw,[3]}}]
=ERROR REPORT==== 29-Apr-2018::15:11:36 ===
** State machine bank_statem terminating
** Last event = {{call,{,#Ref}},
{withdraw,3}}
** When server state = {open,#{balance => 0}}
** Reason for termination = error:function_clause
** Callback mode = state_functions
** Stacktrace =
** [{bank_statem,open,
[{call,{,#Ref}},
{withdraw,3},
#{balance => 0}],
[{file,"/app/_build/test/lib/bank_statem/src/bank_statem.erl"},
{line,46}]},
....
===>
0/1 properties passed, 1 failed
===> Failed test cases:
prop_bank_statem:prop_test() -> false
We can see that the error is caused by trying to withdraw funds that don’t exist. This can be avoided by adding a pre-condition, to ensure that invalid commands aren’t generated:
precondition(_From, _To, #{balance:=Balance}, {call, bank_statem, withdraw, [Amount]}) ->
Balance - Amount >= 0;
And also update our model when a withdrawal occurs:
next_state_data(_From, _To, #{balance:=Balance}=Data, _Res, {call, bank_statem, withdraw, [Amount]}) ->
NewBalance = Balance - Amount,
Data#{balance:=NewBalance};
At this point, I would expect the property to pass, but it’s still failing:
===> Testing prop_bank_statem:prop_test()
...................!
Failed: After 20 test(s).
A linked process died with reason {function_clause,[{bank_statem,open,[{call,{,#Ref}},{withdraw,9},#{balance=>9}],[{file,[47,97,112,112,47,95,98,117,105,108,100,47,116,101,115,116,47,108,105,98,47,98,97,110,107,95,115,116,97,116,101,109,47,115,114,99,47,98,97,110,107,95,115,116,97,116,101,109,46,101,114,108]},{line,46}]},{gen_statem,call_state_function,5,[{file,[103,101,110,95,115,116,97,116,101,109,46,101,114,108]},{line,1633}]},{gen_statem,loop_event_state_function,6,[{file,[103,101,110,95,115,116,97,116,101,109,46,101,114,108]},{line,1023}]},{proc_lib,init_p_do_apply,3,[{file,[112,114,111,99,95,108,105,98,46,101,114,108]},{line,247}]}]}.
=ERROR REPORT==== 29-Apr-2018::15:14:34 ===
** State machine bank_statem terminating
** Last event = {{call,{,#Ref}},
{withdraw,9}}
** When server state = {open,#{balance => 9}}
** Reason for termination = error:function_clause
** Callback mode = state_functions
** Stacktrace =
** [{bank_statem,open,
[{call,{,#Ref}},
{withdraw,9},
#{balance => 9}],
[{file,"/app/_build/test/lib/bank_statem/src/bank_statem.erl"},
{line,46}]},
...
Shrinking .
=ERROR REPORT==== 29-Apr-2018::15:14:34 ===
** State machine bank_statem terminating
** Last event = {{call,{,#Ref}},
{withdraw,9}}
** When server state = {open,#{balance => 9}}
** Reason for termination = error:function_clause
** Callback mode = state_functions
** Stacktrace =
** [{bank_statem,open,
[{call,{,#Ref}},
{withdraw,9},
#{balance => 9}],
[{file,"/app/_build/test/lib/bank_statem/src/bank_statem.erl"},
{line,46}]},
...
.
=ERROR REPORT==== 29-Apr-2018::15:14:34 ===
** State machine bank_statem terminating
** Last event = {{call,{,#Ref}},
{withdraw,9}}
** When server state = {open,#{balance => 9}}
** Reason for termination = error:function_clause
** Callback mode = state_functions
** Stacktrace =
** [{bank_statem,open,
[{call,{,#Ref}},
{withdraw,9},
#{balance => 9}],
[{file,"/app/_build/test/lib/bank_statem/src/bank_statem.erl"},
{line,46}]},
...
(2 time(s))
=ERROR REPORT==== 29-Apr-2018::15:14:34 ===
** State machine bank_statem terminating
** Last event = {{call,{,#Ref}},
{withdraw,9}}
** When server state = {open,#{balance => 9}}
** Reason for termination = error:function_clause
** Callback mode = state_functions
** Stacktrace =
** [{bank_statem,open,
[{call,{,#Ref}},
{withdraw,9},
#{balance => 9}],
[{file,"/app/_build/test/lib/bank_statem/src/bank_statem.erl"},
{line,46}]},
...
[{set,{var,1},{call,bank_statem,deposit,[2]}},{set,{var,2},{call,bank_statem,deposit,[7]}},{set,{var,3},{call,bank_statem,withdraw,[9]}}]
===>
0/1 properties passed, 1 failed
===> Failed test cases:
prop_bank_statem:prop_test() -> false
Rather embarrassingly, that’s an actual bug in my code, the guard is checking that the remaining balance is strictly greater than 0. Hurray for property testing!
