Add property test for deposit

rebar.config

@@ -1,6 +1,15 @@
 {erl_opts, [debug_info]}.
 
+{plugins, [rebar3_proper]}.
+
+{profiles,
+    [{test, [
+        {deps, [{proper, "1.2.0"}]}
+    ]}
+]}.
+
 {deps, []}.
+
 {relx, [{release, {default, "0.0.1"},
          [bank_statem]},
 

src/bank_statem.erl

@@ -2,14 +2,14 @@
 
 -behaviour(gen_statem).
 
--export([start/0, stop/0, get_balance/0, close/0, reopen/0, deposit/1, withdraw/1, place_hold/0, remove_hold/0, available_to_withdraw/0]).
+-export([start_link/0, stop/0, get_balance/0, close/0, reopen/0, deposit/1, withdraw/1, place_hold/0, remove_hold/0, available_to_withdraw/0]).
 -export([init/1, callback_mode/0]).
 -export([open/3, held/3, closed/3]).
 
 name() -> bank_statem.
 
-start() ->
-    gen_statem:start({local, name()}, ?MODULE, [], []).
+start_link() ->
+    gen_statem:start_link({local, name()}, ?MODULE, [], []).
 
 get_balance() ->
     gen_statem:call(name(), get_balance).

test/prop_bank_statem.erl

@@ -0,0 +1,31 @@
+-module(prop_bank_statem).
+
+-include_lib("proper/include/proper.hrl").
+
+-compile(export_all).
+
+prop_test() ->
+    ?FORALL(Cmds, proper_fsm:commands(?MODULE),
+        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).
+
+initial_state() -> open.
+
+initial_state_data() -> #{}.
+
+open(_Data) -> [{open, {call, bank_statem, deposit, [pos_integer()]}}].
+
+weight(_FromState, _ToState, _Call) -> 1.
+
+precondition(_From, _To, #{}, {call, _Mod, _Fun, _Args}) -> true.
+
+postcondition(_From, _To, _Data, {call, _Mod, _Fun, _Args}, _Res) -> true.
+
+next_state_data(_From, _To, Data, _Res, {call, _Mod, _Fun, _Args}) ->
+    NewData = Data,
+    NewData.