Quickcheck for ggs_network. Part of the pongbot.
This commit is contained in:
parent
e6ff8b6f16
commit
9efd739cbb
8 changed files with 381 additions and 3 deletions
BIN
games/pong_bot_e/current_counterexample.eqc
Normal file
BIN
games/pong_bot_e/current_counterexample.eqc
Normal file
Binary file not shown.
|
@ -2,10 +2,12 @@
|
|||
-export([connect/0,append_key_value_strings_to_dict/2,key_value_string_to_list/1]).
|
||||
-export([read/2, send_command/3]).
|
||||
|
||||
%For quickcheck
|
||||
-export([receive_content/1,receive_data/3]).
|
||||
|
||||
connect() ->
|
||||
%{ok,Socket} = gen_tcp:connect("ggs.jeena.net", 9000,[{active, false}]),
|
||||
{ok,Socket} = gen_tcp:connect("localhost", 9000,[{active, false}]),
|
||||
Socket.
|
||||
{ok,Socket} = gen_tcp:connect("localhost", 9000,[{active, false}]).
|
||||
|
||||
read(Socket, Ref) ->
|
||||
Content = receive_content(Socket),
|
||||
|
|
86
games/pong_bot_e/ggs_network_eqc_test.erl
Normal file
86
games/pong_bot_e/ggs_network_eqc_test.erl
Normal file
|
@ -0,0 +1,86 @@
|
|||
-module(ggs_network_eqc_test).
|
||||
|
||||
-include_lib("../../lib/eqc/include/eqc.hrl").
|
||||
|
||||
-compile(export_all).
|
||||
|
||||
|
||||
start() ->
|
||||
{ok, ListenSocket} = listen(),
|
||||
eqc:quickcheck(prop_connect()),
|
||||
gen_tcp:close(ListenSocket),
|
||||
|
||||
{ok, ListenSocket2} = listen(),
|
||||
eqc:quickcheck(prop_receive_content(ListenSocket2)),
|
||||
%gen_tcp:close(ListenSocket2),
|
||||
%timer:sleep(100),
|
||||
|
||||
%{ok, ListenSocket} = listen(),
|
||||
eqc:quickcheck(prop_receive_data(ListenSocket2)).
|
||||
|
||||
|
||||
prop_connect() ->
|
||||
{Atom, Socket} = ggs_network:connect(),
|
||||
gen_tcp:close(Socket),
|
||||
eqc:equals(Atom, ok).
|
||||
|
||||
%% ?String++\n\n -> ok
|
||||
prop_receive_content(ListenSocket) ->
|
||||
G = fun(N) -> String = integer_to_list(N) ++"\n\n",
|
||||
accept_run_compare(String,ListenSocket, fun(X) -> ggs_network:receive_content(X) end, "\n") end,
|
||||
?FORALL(NaturalNumber, nat(), G(NaturalNumber)).
|
||||
|
||||
%% old(String) == new(String)
|
||||
prop_receive_data(ListenSocket) ->
|
||||
G = fun(N) -> String = integer_to_list(N),
|
||||
Length = length(String),
|
||||
accept_run_compare(String,ListenSocket, fun(S) -> ggs_network:receive_data(S,Length,"") end, "") end,
|
||||
?FORALL(NaturalNumber, nat(), G(NaturalNumber)).
|
||||
|
||||
%% Helpers
|
||||
accept_run_compare(Arg, ListenSocket, Fun, Newline) ->
|
||||
spawn(fun() -> {ok, AcceptSocket} = accept(ListenSocket),
|
||||
gen_tcp:send(AcceptSocket, Arg),
|
||||
gen_tcp:close(AcceptSocket) end),
|
||||
|
||||
{ok, ConnectSocket} = ggs_network:connect(),
|
||||
Pid = spawn(fun() -> C = Fun(ConnectSocket),
|
||||
gen_tcp:close(ConnectSocket),
|
||||
receive
|
||||
{From, getcontent} -> From!{C} end end ),
|
||||
Pid!{self(), getcontent},
|
||||
receive
|
||||
{C} -> eqc:equals(C++Newline,Arg) end.
|
||||
|
||||
listen() ->
|
||||
listen(9000).
|
||||
|
||||
listen(Port) ->
|
||||
case gen_tcp:listen(Port, [binary, {packet, 0}, {active, false}]) of
|
||||
{ok, LSock} ->
|
||||
{ok, LSock};
|
||||
{error, Reason} ->
|
||||
io:format("Creation of listen socket failed: ~s~n", [Reason])
|
||||
end.
|
||||
|
||||
recv(AcceptSocket) ->
|
||||
gen_tcp:recv(AcceptSocket, 0).
|
||||
|
||||
accept(ListenSocket) ->
|
||||
case gen_tcp:accept(ListenSocket) of
|
||||
{ok, Socket} -> {ok, Socket};
|
||||
{error, Reason} -> io:format("Error accepting listen socket~s~n", [Reason]);
|
||||
_ -> io:format("Something bad happened with accept/1~n")
|
||||
end.
|
||||
|
||||
|
||||
%% new(length) == old(length) or
|
||||
%% new(length) == old(length) + 1
|
||||
prop_setItem() ->
|
||||
ggs_db:init(),
|
||||
F = (fun(T,N,K,V) -> ggs_db:setItem(T,N,K,V), ggs_db:length(T,N) end),
|
||||
?FORALL({T,N,K,V},{bitstring(),bitstring(),bitstring(),bitstring()},
|
||||
(ggs_db:length(T,N) + 1 == F(T,N,K,V)) or
|
||||
(ggs_db:length(T,N) == F(T,N,K,V))).
|
||||
|
||||
|
|
@ -34,7 +34,7 @@ init(_Args) ->
|
|||
Ball = new_pos(),
|
||||
Paused = true,
|
||||
Start = false,
|
||||
Socket = ggs_network:connect(), %Localhost is set internally inside ggs_network.
|
||||
{ok, Socket} = ggs_network:connect(), %Localhost is set internally inside ggs_network.
|
||||
State1 = dict:new(),
|
||||
State2 = dict:store(player1, Player1, State1),
|
||||
State3 = dict:store(player2, Player2, State2),
|
||||
|
|
62
games/pong_bot_e/test/ggs_network_eqc_test.erl
Normal file
62
games/pong_bot_e/test/ggs_network_eqc_test.erl
Normal file
|
@ -0,0 +1,62 @@
|
|||
-module(ggs_network_eqc_test).
|
||||
|
||||
-include_lib("../../lib/eqc/include/eqc.hrl").
|
||||
|
||||
-compile(export_all).
|
||||
|
||||
|
||||
start() ->
|
||||
eqc:quickcheck(prop_connect()).
|
||||
|
||||
prop_connect() ->
|
||||
{Atom, Value} = ggs_network:connect(),
|
||||
eqc:equals(Atom, ok).
|
||||
|
||||
|
||||
%% new(length) == old(length) or
|
||||
%% new(length) == old(length) + 1
|
||||
prop_setItem() ->
|
||||
ggs_db:init(),
|
||||
F = (fun(T,N,K,V) -> ggs_db:setItem(T,N,K,V), ggs_db:length(T,N) end),
|
||||
?FORALL({T,N,K,V},{bitstring(),bitstring(),bitstring(),bitstring()},
|
||||
(ggs_db:length(T,N) + 1 == F(T,N,K,V)) or
|
||||
(ggs_db:length(T,N) == F(T,N,K,V))).
|
||||
|
||||
|
||||
%% new(length) >= 0 and
|
||||
%% old(length) == new(length) or
|
||||
%% old(length) - 1 == new(length)
|
||||
prop_removeItem() ->
|
||||
ggs_db:init(),
|
||||
F = (fun(T,N,K) -> ggs_db:removeItem(T,N,K), ggs_db:length(T,N) end),
|
||||
G = (fun(A,B) -> ((A == B) or (A == B + 1)) and (B >= 0) end),
|
||||
?FORALL({T,N,K},{bitstring(),bitstring(),bitstring()},
|
||||
G(ggs_db:length(T,N), F(T,N,K))).
|
||||
|
||||
|
||||
%% clear(X) -> (length(X,?) == 0)
|
||||
prop_clear() ->
|
||||
ggs_db:init(),
|
||||
F = (fun(T,N) -> ggs_db:clear(T), ggs_db:length(T,N) end),
|
||||
?FORALL({T,N},{bitstring(),bitstring()},
|
||||
F(T,N) == 0).
|
||||
|
||||
%% ? -> length(?,?) >= 0
|
||||
prop_length() ->
|
||||
ggs_db:init(),
|
||||
F = fun(T,N,K,V) -> ggs_db:setItem(T,N,K,V), ggs_db:length(T,N) end,
|
||||
G = fun(T,N,K) -> ggs_db:removeItem(T,N,K), ggs_db:length(T,N) end,
|
||||
?FORALL({{T,N,K,V},{T2,N2,K2}},
|
||||
{{bitstring(),bitstring(),bitstring(),bitstring()},
|
||||
{bitstring(),bitstring(),bitstring()}},
|
||||
(((F(T,N,K,V) >= 0) and (G(T2,N2,K2) >= 0)))).
|
||||
|
||||
|
||||
%% key(X,Y,length(X,Y)) -> Exists
|
||||
prop_key() ->
|
||||
ggs_db:init(),
|
||||
F = fun(T,N) -> case ggs_db:length(T,N) of 0 -> true; X ->
|
||||
case ggs_db:key(T,N,X) of _ -> true end end end,
|
||||
?FORALL({T,N},{bitstring(),bitstring()},
|
||||
F(T,N)).
|
||||
|
90
games/pong_bot_e/v.01/ggs_network_eqc_test.erl
Normal file
90
games/pong_bot_e/v.01/ggs_network_eqc_test.erl
Normal file
|
@ -0,0 +1,90 @@
|
|||
-module(ggs_network_eqc_test).
|
||||
|
||||
-include_lib("../../lib/eqc/include/eqc.hrl").
|
||||
|
||||
-compile(export_all).
|
||||
|
||||
|
||||
start() ->
|
||||
{ok, ListenSocket} = listen(),
|
||||
register(listen, ListenSocket),
|
||||
Pid = spawn(fun() -> {ok, AcceptSocket} = accept(ListenSocket),
|
||||
|
||||
receive {From, accept} -> From!{AcceptSocket} end end),
|
||||
{ok, ConnectSocket} = ggs_network:connect(),
|
||||
Pid!{self(), accept},
|
||||
receive
|
||||
{AcceptSocket} ->
|
||||
io:format("AcceptSocket created~n"),
|
||||
%eqc:quickcheck(prop_connect()),
|
||||
%eqc:quickcheck(prop_receive_content(AcceptSocket, ConnectSocket))
|
||||
prop_receive_content(AcceptSocket, ConnectSocket)
|
||||
end.
|
||||
|
||||
prop_connect() ->
|
||||
{Atom, _} = ggs_network:connect(),
|
||||
eqc:equals(Atom, ok).
|
||||
|
||||
prop_receive_content(AcceptSocket, ConnectSocket) ->
|
||||
%{ok, ConnectSocket} = ggs_network:connect(),
|
||||
io:format("Connected~n"),
|
||||
%spawn(fun() -> {ok, B} = gen_tcp:recv(ConnectSocket, 1), io:format("Data: ~s~n",[B]) end),
|
||||
%timer:sleep(300),
|
||||
Pid = spawn(fun() -> C = receive_content(ConnectSocket),
|
||||
io:format("Content: ~s~n", [C]) end),
|
||||
|
||||
io:format("Before send to AcceptSocket~n"),
|
||||
gen_tcp:send(AcceptSocket, "Hello\n\n"),
|
||||
io:format("After send to AcceptSocket~n"),
|
||||
eqc:equals(ok,ok).
|
||||
|
||||
receive_content(Socket) ->
|
||||
receive_content_(0, "", Socket).
|
||||
|
||||
receive_content_(Amount, Headers, Socket) ->
|
||||
{ok, Char1} = gen_tcp:recv(Socket, 1),
|
||||
case Char1 of
|
||||
"\n" -> case Amount of
|
||||
1 -> Headers;
|
||||
_ -> receive_content_(Amount + 1,
|
||||
Headers ++ Char1,
|
||||
Socket)
|
||||
end;
|
||||
_ -> receive_content_(0, Headers ++ Char1, Socket)
|
||||
end.
|
||||
|
||||
|
||||
|
||||
%% Helpers
|
||||
listen() ->
|
||||
listen(9000).
|
||||
|
||||
listen(Port) ->
|
||||
case gen_tcp:listen(Port, [binary, {packet, 0}, {active, false}]) of
|
||||
{ok, LSock} ->
|
||||
{ok, LSock};
|
||||
{error, Reason} ->
|
||||
io:format("Creation of listen socket failed: ~s~n", [Reason])
|
||||
end.
|
||||
|
||||
recv(AcceptSocket) ->
|
||||
gen_tcp:recv(AcceptSocket, 0).
|
||||
|
||||
accept(ListenSocket) ->
|
||||
case gen_tcp:accept(ListenSocket) of
|
||||
{ok, Socket} -> {ok, Socket};
|
||||
{error, Reason} -> io:format("Error accepting listen socket~s~n", [Reason]);
|
||||
_ -> io:format("Something bad happened with accept/1~n")
|
||||
end.
|
||||
|
||||
|
||||
%% new(length) == old(length) or
|
||||
%% new(length) == old(length) + 1
|
||||
prop_setItem() ->
|
||||
ggs_db:init(),
|
||||
F = (fun(T,N,K,V) -> ggs_db:setItem(T,N,K,V), ggs_db:length(T,N) end),
|
||||
?FORALL({T,N,K,V},{bitstring(),bitstring(),bitstring(),bitstring()},
|
||||
(ggs_db:length(T,N) + 1 == F(T,N,K,V)) or
|
||||
(ggs_db:length(T,N) == F(T,N,K,V))).
|
||||
|
||||
|
66
games/pong_bot_e/v0.2/ggs_network_eqc_test.erl
Normal file
66
games/pong_bot_e/v0.2/ggs_network_eqc_test.erl
Normal file
|
@ -0,0 +1,66 @@
|
|||
-module(ggs_network_eqc_test).
|
||||
|
||||
-include_lib("../../lib/eqc/include/eqc.hrl").
|
||||
|
||||
-compile(export_all).
|
||||
|
||||
|
||||
start() ->
|
||||
{ok, ListenSocket} = listen(),
|
||||
register(listen, ListenSocket),
|
||||
Pid = spawn(fun() -> {ok, AcceptSocket} = accept(ListenSocket),
|
||||
gen_tcp:send(AcceptSocket, "Hello\n\n"),
|
||||
gen_tcp:close(AcceptSocket) end),
|
||||
eqc:quickcheck(prop_receive_content()),
|
||||
gen_tcp:close(ListenSocket).
|
||||
|
||||
|
||||
|
||||
prop_connect() ->
|
||||
{Atom, _} = ggs_network:connect(),
|
||||
eqc:equals(Atom, ok).
|
||||
|
||||
prop_receive_content() ->
|
||||
{ok, ConnectSocket} = ggs_network:connect(),
|
||||
Pid = spawn(fun() -> C = ggs_network:receive_content(ConnectSocket),
|
||||
gen_tcp:close(ConnectSocket),
|
||||
receive
|
||||
{From, getcontent} -> From!{C} end end ),
|
||||
Pid!{self(), getcontent},
|
||||
receive
|
||||
{C} -> eqc:equals(C,"Hello\n")
|
||||
end.
|
||||
|
||||
%% Helpers
|
||||
listen() ->
|
||||
listen(9000).
|
||||
|
||||
listen(Port) ->
|
||||
case gen_tcp:listen(Port, [binary, {packet, 0}, {active, false}]) of
|
||||
{ok, LSock} ->
|
||||
{ok, LSock};
|
||||
{error, Reason} ->
|
||||
io:format("Creation of listen socket failed: ~s~n", [Reason])
|
||||
end.
|
||||
|
||||
recv(AcceptSocket) ->
|
||||
gen_tcp:recv(AcceptSocket, 0).
|
||||
|
||||
accept(ListenSocket) ->
|
||||
case gen_tcp:accept(ListenSocket) of
|
||||
{ok, Socket} -> {ok, Socket};
|
||||
{error, Reason} -> io:format("Error accepting listen socket~s~n", [Reason]);
|
||||
_ -> io:format("Something bad happened with accept/1~n")
|
||||
end.
|
||||
|
||||
|
||||
%% new(length) == old(length) or
|
||||
%% new(length) == old(length) + 1
|
||||
prop_setItem() ->
|
||||
ggs_db:init(),
|
||||
F = (fun(T,N,K,V) -> ggs_db:setItem(T,N,K,V), ggs_db:length(T,N) end),
|
||||
?FORALL({T,N,K,V},{bitstring(),bitstring(),bitstring(),bitstring()},
|
||||
(ggs_db:length(T,N) + 1 == F(T,N,K,V)) or
|
||||
(ggs_db:length(T,N) == F(T,N,K,V))).
|
||||
|
||||
|
72
games/pong_bot_e/v0.3/ggs_network_eqc_test.erl
Normal file
72
games/pong_bot_e/v0.3/ggs_network_eqc_test.erl
Normal file
|
@ -0,0 +1,72 @@
|
|||
-module(ggs_network_eqc_test).
|
||||
|
||||
-include_lib("../../lib/eqc/include/eqc.hrl").
|
||||
|
||||
-compile(export_all).
|
||||
|
||||
|
||||
start() ->
|
||||
{ok, ListenSocket} = listen(),
|
||||
eqc:quickcheck(prop_connect()),
|
||||
gen_tcp:close(ListenSocket),
|
||||
{ok, ListenSocket2} = listen(),
|
||||
eqc:quickcheck(prop_receive_content(ListenSocket2)).
|
||||
|
||||
|
||||
|
||||
prop_connect() ->
|
||||
{Atom, Socket} = ggs_network:connect(),
|
||||
gen_tcp:close(Socket),
|
||||
eqc:equals(Atom, ok).
|
||||
|
||||
%% ?String++\n\n -> ok
|
||||
prop_receive_content(ListenSocket) ->
|
||||
F = fun(X) -> Pid2 = spawn(fun() -> {ok, AcceptSocket} = accept(ListenSocket),
|
||||
gen_tcp:send(AcceptSocket, X),
|
||||
gen_tcp:close(AcceptSocket) end),
|
||||
|
||||
{ok, ConnectSocket} = ggs_network:connect(),
|
||||
Pid = spawn(fun() -> C = ggs_network:receive_content(ConnectSocket),
|
||||
gen_tcp:close(ConnectSocket),
|
||||
receive
|
||||
{From, getcontent} -> From!{C} end end ),
|
||||
Pid!{self(), getcontent},
|
||||
receive
|
||||
{C} -> eqc:equals(C++"\n",X) end end,
|
||||
G = fun(N) -> String = integer_to_list(N) ++"\n\n",
|
||||
F(String) end,
|
||||
?FORALL(NaturalNumber, nat(), G(NaturalNumber)).
|
||||
|
||||
%% Helpers
|
||||
listen() ->
|
||||
listen(9000).
|
||||
|
||||
listen(Port) ->
|
||||
case gen_tcp:listen(Port, [binary, {packet, 0}, {active, false}]) of
|
||||
{ok, LSock} ->
|
||||
{ok, LSock};
|
||||
{error, Reason} ->
|
||||
io:format("Creation of listen socket failed: ~s~n", [Reason])
|
||||
end.
|
||||
|
||||
recv(AcceptSocket) ->
|
||||
gen_tcp:recv(AcceptSocket, 0).
|
||||
|
||||
accept(ListenSocket) ->
|
||||
case gen_tcp:accept(ListenSocket) of
|
||||
{ok, Socket} -> {ok, Socket};
|
||||
{error, Reason} -> io:format("Error accepting listen socket~s~n", [Reason]);
|
||||
_ -> io:format("Something bad happened with accept/1~n")
|
||||
end.
|
||||
|
||||
|
||||
%% new(length) == old(length) or
|
||||
%% new(length) == old(length) + 1
|
||||
prop_setItem() ->
|
||||
ggs_db:init(),
|
||||
F = (fun(T,N,K,V) -> ggs_db:setItem(T,N,K,V), ggs_db:length(T,N) end),
|
||||
?FORALL({T,N,K,V},{bitstring(),bitstring(),bitstring(),bitstring()},
|
||||
(ggs_db:length(T,N) + 1 == F(T,N,K,V)) or
|
||||
(ggs_db:length(T,N) == F(T,N,K,V))).
|
||||
|
||||
|
Reference in a new issue