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!
Look on my works, ye Mighty, and despair! 