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!