ssh: Enable property_test/ssh_eqc_client_server for PropEr

PropEr does not support the grouped statem-tests.  This commits
calls the grouped functions from the functions supported by PropEr.
Optimized with memoization.

Previously only EQC was supported, but the changes to support PROPER is not
just a wrapper. Since I don't have access to eqc I can't test the changes
and therefore eqc is disabeled.
However, with access to eqc it ought to be quite easy to re-enable eqc by
studying the diff.

1 files changed, 126 insertions, 75 deletions

diff --git a/lib/ssh/test/property_test/ssh_eqc_client_server.erl b/lib/ssh/test/property_test/ssh_eqc_client_server.erl
index 05c8abfd12..acb0faa0c7 100644
--- a/lib/ssh/test/property_test/ssh_eqc_client_server.erl
+++ b/lib/ssh/test/property_test/ssh_eqc_client_server.erl
@@ -22,25 +22,27 @@
 -module(ssh_eqc_client_server).
 
 -compile(export_all).
+ 
+-proptest([proper]).
 
--include_lib("common_test/include/ct.hrl").
-
--ifdef(PROPER).
-%% Proper is not supported.
--else.
--ifdef(TRIQ).
-%% Proper is not supported.
+-ifndef(PROPER).
 -else.
+%% Only use proper
+%% 
+%% Previously only EQC was supported, but the changes to support PROPER is not
+%% just a wrapper. Since we do not have access to eqc we can't test the changes
+%% so therefore eqc is disabeled.
+%% However, with access to eqc it ought to be quite easy to re-enable eqc by
+%% studying the diff.
 
+-include_lib("proper/include/proper.hrl").
+-define(MOD_eqc,proper).
+
+-include_lib("common_test/include/ct.hrl").
 
 %% Limit the testing time on CI server... this needs to be improved in % from total budget.
 -define(TESTINGTIME(Prop), eqc:testing_time(30,Prop)).
   
-
--include_lib("eqc/include/eqc.hrl").
--include_lib("eqc/include/eqc_statem.hrl").
--eqc_group_commands(true).
-
 -define(SSH_DIR,"ssh_eqc_client_server_dirs").
 
 -define(sec, *1000).
@@ -51,10 +53,6 @@
 	      port
 	     }).
 
--record(conn,{ref,
-	      srvr_ref
-	     }).
-
 -record(chan, {ref,
 	       conn_ref,
 	       subsystem,
@@ -65,7 +63,7 @@
 	  initialized = false,
 	  servers = [],       % [#srvr{}]
 	  clients = [],
-	  connections = [],   % [#conn{}]
+	  connections = [],
 	  channels = [],      % [#chan{}]
 	  data_dir
 	 }).
@@ -103,10 +101,12 @@
 
 %% To be called as eqc:quickcheck( ssh_eqc_client_server:prop_seq() ).
 prop_seq() ->
-  ?TESTINGTIME(do_prop_seq(?SSH_DIR)).
+    error_logger:tty(false),
+    ?TESTINGTIME(do_prop_seq(?SSH_DIR)).
 
 %% To be called from a common_test test suite
 prop_seq(CT_Config) ->
+    error_logger:tty(false),
     do_prop_seq(full_path(?SSH_DIR, CT_Config)).
 
 
@@ -123,10 +123,12 @@ full_path(SSHdir, CT_Config) ->
 		  SSHdir).
 %%%----
 prop_parallel() ->
+    error_logger:tty(false),
     ?TESTINGTIME(do_prop_parallel(?SSH_DIR)).
 
 %% To be called from a common_test test suite
 prop_parallel(CT_Config) ->
+    error_logger:tty(false),
     do_prop_parallel(full_path(?SSH_DIR, CT_Config)).
 
 do_prop_parallel(DataDir) ->
@@ -138,22 +140,22 @@ do_prop_parallel(DataDir) ->
 	    end).
 
 %%%----
-prop_parallel_multi() ->
-    ?TESTINGTIME(do_prop_parallel_multi(?SSH_DIR)).
-
-%% To be called from a common_test test suite
-prop_parallel_multi(CT_Config) ->
-    do_prop_parallel_multi(full_path(?SSH_DIR, CT_Config)).
-
-do_prop_parallel_multi(DataDir) ->
-    setup_rsa(DataDir),
-    ?FORALL(Repetitions,?SHRINK(1,[10]),
-	    ?FORALL(Cmds,parallel_commands(?MODULE),
-		    ?ALWAYS(Repetitions,
-			    begin
-				{H,Sf,Result} = run_parallel_commands(?MODULE,Cmds,[{data_dir,DataDir}]),
-				present_result(?MODULE, Cmds, {H,Sf,Result}, Result==ok)
-			    end))).
+%% prop_parallel_multi() ->
+%%     ?TESTINGTIME(do_prop_parallel_multi(?SSH_DIR)).
+
+%% %% To be called from a common_test test suite
+%% prop_parallel_multi(CT_Config) ->
+%%     do_prop_parallel_multi(full_path(?SSH_DIR, CT_Config)).
+
+%% do_prop_parallel_multi(DataDir) ->
+%%     setup_rsa(DataDir),
+%%     ?FORALL(Repetitions,?SHRINK(1,[10]),
+%% 	    ?FORALL(Cmds,parallel_commands(?MODULE),
+%% 		    ?ALWAYS(Repetitions,
+%% 			    begin
+%% 				{H,Sf,Result} = run_parallel_commands(?MODULE,Cmds,[{data_dir,DataDir}]),
+%% 				present_result(?MODULE, Cmds, {H,Sf,Result}, Result==ok)
+%% 			    end))).
 
 %%%================================================================
 %%% State machine spec
@@ -168,13 +170,50 @@ initial_state(DataDir) ->
     ssh:start().
 
 %%%----------------
-weight(S, ssh_send) -> 5*length([C || C<-S#state.channels, has_subsyst(C)]);
-weight(S, ssh_start_subsyst) -> 3*length([C || C<-S#state.channels, no_subsyst(C)]);
+weight(S, ssh_send) -> 20*length([C || C<-S#state.channels, has_subsyst(C)]);
+weight(S, ssh_start_subsyst) -> 10*length([C || C<-S#state.channels, no_subsyst(C)]);
 weight(S, ssh_close_channel) -> 2*length([C || C<-S#state.channels, has_subsyst(C)]);
-weight(S, ssh_open_channel) ->  length(S#state.connections);
+weight(S, ssh_open_channel) ->  2*length(S#state.connections);
 weight(_S, _) -> 1.
 
 %%%----------------
+fns() -> [initial_state,
+          ssh_server,
+          ssh_client,
+          ssh_open_connection,
+          ssh_close_connection,
+          ssh_open_channel,
+          ssh_close_channel,
+          ssh_start_subsyst,
+          ssh_send
+         ].
+
+call_f(Name, Sfx) -> 
+    case get({Name,Sfx}) of
+        undefined -> F = list_to_atom(lists:concat([Name,"_",Sfx])),
+                     put({Name,Sfx}, F),
+                     F;
+        F when is_atom(F) -> F
+    end.
+
+-define(call(Name, What, Args), apply(?MODULE, call_f(Name,What), Args)).
+
+symbolic_call(S,Name) -> {call, ?MODULE, Name, ?call(Name,args,[S])}.
+
+may_generate(S, F) ->  ?call(F,pre,[S]).
+
+command(S) ->
+    frequency([{weight(S,F), symbolic_call(S,F)} || F <- fns(),
+                                                    may_generate(S, F)]
+             ).
+
+precondition(S,    {call,_M,F,As})      -> try ?call(F, pre, [S,As])
+                                           catch _:undef -> try ?call(F,pre,[S]) catch _:undef -> true end
+                                           end.
+next_state(S, Res, {call,_M,F,As})      -> try ?call(F, next, [S,Res,As]) catch _:undef -> S end.
+postcondition(S,   {call,_M,F,As}, Res) -> try ?call(F, post, [S,As,Res]) catch _:undef -> true end.
+
+%%%----------------
 %%% Initialize
 
 initial_state_pre(S) -> not S#state.initialized.
@@ -199,24 +238,34 @@ ssh_server_pre(S) -> S#state.initialized andalso
 
 ssh_server_args(_) -> [?SERVER_ADDRESS, {var,data_dir}, ?SERVER_EXTRA_OPTIONS]. 
 
-ssh_server({IP,Port}, DataDir, ExtraOptions) ->
-    ok(ssh:daemon(IP, Port, 
-		  [
-		   {system_dir, system_dir(DataDir)},
-		   {user_dir, user_dir(DataDir)},
-		   {subsystems, [{SS, {ssh_eqc_subsys, [SS]}} || SS <- ?SUBSYSTEMS]}
-		   | ExtraOptions
-		  ])).
-
-ssh_server_post(_S, _Args, {error,eaddrinuse}) -> true;
-ssh_server_post(_S, _Args, Result) -> is_ok(Result).
-
-ssh_server_next(S, {error,eaddrinuse}, _) -> S;
-ssh_server_next(S, Result, [{IP,Port},_,_]) ->
-    S#state{servers=[#srvr{ref = Result,
-			   address = IP,
-			   port = Port}
-		     | S#state.servers]}.
+ssh_server(IP0, DataDir, ExtraOptions) ->
+    case ssh:daemon(IP0, 0, 
+                    [
+                     {system_dir, system_dir(DataDir)},
+                     {user_dir, user_dir(DataDir)},
+                     {subsystems, [{SS, {ssh_eqc_subsys, [SS]}} || SS <- ?SUBSYSTEMS]}
+                     | ExtraOptions
+                    ]) of
+        {ok,DaemonRef} ->
+            case ssh:daemon_info(DaemonRef) of
+                {ok, Props} ->
+                    Port = proplists:get_value(port,Props),
+                    IP = proplists:get_value(ip,Props),
+                    #srvr{ref = DaemonRef,
+                          address = IP,
+                          port = Port};
+                Other ->
+                    Other
+            end;
+        Other ->
+            Other
+    end.
+
+ssh_server_post(_S, _Args, #srvr{port=Port}) -> (0 < Port) andalso (Port < 65536);
+ssh_server_post(_S, _Args, _) -> false.
+
+ssh_server_next(S, Srvr, _) ->
+    S#state{servers=[Srvr | S#state.servers]}.
 
 %%%----------------
 %%% Start a new client
@@ -270,8 +319,7 @@ ssh_open_connection(#srvr{address=Ip, port=Port}, DataDir) ->
 
 ssh_open_connection_post(_S, _Args, Result) -> is_ok(Result).
 
-ssh_open_connection_next(S, ConnRef, [#srvr{ref=SrvrRef},_]) -> 
-    S#state{connections=[#conn{ref=ConnRef, srvr_ref=SrvrRef}|S#state.connections]}.
+ssh_open_connection_next(S, ConnRef, [_,_]) -> S#state{connections=[ConnRef|S#state.connections]}.
 
 %%%----------------
 %%% Stop a new connection
@@ -281,12 +329,12 @@ ssh_close_connection_pre(S) -> S#state.connections /= [].
 
 ssh_close_connection_args(S) -> [oneof(S#state.connections)].
     
-ssh_close_connection(#conn{ref=ConnectionRef}) -> ssh:close(ConnectionRef).
+ssh_close_connection(ConnectionRef) -> ssh:close(ConnectionRef).
 
-ssh_close_connection_next(S, _, [Conn=#conn{ref=ConnRef}]) ->
-	S#state{connections = S#state.connections--[Conn],
-		channels = [C || C <- S#state.channels,
-				 C#chan.conn_ref /= ConnRef]
+ssh_close_connection_next(S, _, [ConnRef]) ->
+    S#state{connections = S#state.connections--[ConnRef],
+            channels = [C || C <- S#state.channels,
+                             C#chan.conn_ref /= ConnRef]
 	       }.
 
 %%%----------------
@@ -298,14 +346,14 @@ ssh_open_channel_pre(S) -> S#state.connections /= [].
 ssh_open_channel_args(S) -> [oneof(S#state.connections)].
 
 %%% For re-arrangement in parallel tests. 
-ssh_open_channel_pre(S,[C]) -> lists:member(C,S#state.connections).
+ssh_open_channel_pre(S,[C]) when is_record(S,state) -> lists:member(C,S#state.connections).
 
-ssh_open_channel(#conn{ref=ConnectionRef}) -> 
+ssh_open_channel(ConnectionRef) -> 
     ok(ssh_connection:session_channel(ConnectionRef, 20?sec)).
 
 ssh_open_channel_post(_S, _Args, Result) -> is_ok(Result).
 
-ssh_open_channel_next(S, ChannelRef, [#conn{ref=ConnRef}]) ->  
+ssh_open_channel_next(S, ChannelRef, [ConnRef]) ->  
     S#state{channels=[#chan{ref=ChannelRef,
 			    conn_ref=ConnRef}
 		      | S#state.channels]}.
@@ -325,9 +373,7 @@ ssh_close_channel_next(S, _, [C]) ->
     S#state{channels = [Ci || Ci <- S#state.channels,
 			      sig(C) /= sig(Ci)]}.
 
-			      
 sig(C) -> {C#chan.ref, C#chan.conn_ref}.
-    
 
 %%%----------------
 %%% Start a sub system on a channel
@@ -360,9 +406,10 @@ ssh_start_subsyst_next(S, _Result, [C,SS,Pid|_]) ->
 
 ssh_send_pre(S) -> lists:any(fun has_subsyst/1, S#state.channels).
 
-ssh_send_args(S) -> [oneof(lists:filter(fun has_subsyst/1, S#state.channels)),
-		     choose(0,1),
-		     message()].
+ssh_send_args(S) -> 
+    [oneof(lists:filter(fun has_subsyst/1, S#state.channels)),
+     choose(0,1),
+     message()].
 
 %% For re-arrangement in parallel tests. 
 ssh_send_pre(S, [C|_]) -> lists:member(C, S#state.channels).
@@ -387,17 +434,17 @@ ssh_send(C=#chan{conn_ref=ConnectionRef, ref=ChannelRef, client_pid=Pid}, Type,
        end).
 
 ssh_send_blocking(_S, _Args) ->
-    true.
+   true.
 
 ssh_send_post(_S, [C,_,Msg], Response) when is_binary(Response) ->
-    Expected = ssh_eqc_subsys:response(modify_msg(C,Msg), C#chan.subsystem),
+   Expected = ssh_eqc_subsys:response(modify_msg(C,Msg), C#chan.subsystem),
     case Response of
 	Expected -> true;
 	_ -> {send_failed, size(Response), size(Expected)}
     end;
 	    
 ssh_send_post(_S, _Args, Response) ->
-    {error,Response}.
+   {error,Response}.
     
 
 modify_msg(_, <<>>) -> <<>>;
@@ -439,7 +486,11 @@ present_result(_Module, Cmds, _Triple, true) ->
 	      true)))));
 
 present_result(Module, Cmds, Triple, false) -> 
-    pretty_commands(Module, Cmds, Triple, [{show_states,true}], false).
+    pretty_comands(Module, Cmds, Triple, [{show_states,true}], false),
+    false. % Proper dislikes non-boolean results while eqc treats non-true as false.
+
+pretty_comands(Module, Cmds, Triple, Opts, Bool) ->
+    ct:log("Module = ~p,~n Cmds = ~p,~n Triple = ~p,~n Opts = ~p,~n Bool = ~p",[Module, Cmds, Triple, Opts, Bool]).
 
 
 
@@ -488,6 +539,7 @@ print_frequencies(Ngroups) -> fun([]) -> io:format('Empty list!~n',[]);
                                       end
                               end.
 
+
 print_frequencies(Ngroups, MaxValue) -> fun(L) -> print_frequencies(L,Ngroups,0,MaxValue) end.
 
 print_frequencies(L, N, Min, Max) when N>Max -> print_frequencies(L++[{N,0}], N, Min, N);
@@ -627,4 +679,3 @@ erase_dir(Dir) ->
     file:del_dir(Dir).
 
 -endif.
--endif.