diff --git a/games/pong_bot_e/current_counterexample.eqc b/games/pong_bot_e/current_counterexample.eqc new file mode 100644 index 0000000..b3e181a Binary files /dev/null and b/games/pong_bot_e/current_counterexample.eqc differ diff --git a/games/pong_bot_e/ggs_network.erl b/games/pong_bot_e/ggs_network.erl index b2506cb..713bd27 100644 --- a/games/pong_bot_e/ggs_network.erl +++ b/games/pong_bot_e/ggs_network.erl @@ -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), diff --git a/games/pong_bot_e/ggs_network_eqc_test.erl b/games/pong_bot_e/ggs_network_eqc_test.erl new file mode 100644 index 0000000..42b8f5c --- /dev/null +++ b/games/pong_bot_e/ggs_network_eqc_test.erl @@ -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))). + + diff --git a/games/pong_bot_e/pong_bot.erl b/games/pong_bot_e/pong_bot.erl index 4006303..ccc2e15 100644 --- a/games/pong_bot_e/pong_bot.erl +++ b/games/pong_bot_e/pong_bot.erl @@ -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), diff --git a/games/pong_bot_e/test/ggs_network_eqc_test.erl b/games/pong_bot_e/test/ggs_network_eqc_test.erl new file mode 100644 index 0000000..ebe69e5 --- /dev/null +++ b/games/pong_bot_e/test/ggs_network_eqc_test.erl @@ -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)). + diff --git a/games/pong_bot_e/v.01/ggs_network_eqc_test.erl b/games/pong_bot_e/v.01/ggs_network_eqc_test.erl new file mode 100644 index 0000000..5b830c0 --- /dev/null +++ b/games/pong_bot_e/v.01/ggs_network_eqc_test.erl @@ -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))). + + diff --git a/games/pong_bot_e/v0.2/ggs_network_eqc_test.erl b/games/pong_bot_e/v0.2/ggs_network_eqc_test.erl new file mode 100644 index 0000000..911c4e3 --- /dev/null +++ b/games/pong_bot_e/v0.2/ggs_network_eqc_test.erl @@ -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))). + + diff --git a/games/pong_bot_e/v0.3/ggs_network_eqc_test.erl b/games/pong_bot_e/v0.3/ggs_network_eqc_test.erl new file mode 100644 index 0000000..ed9e3d5 --- /dev/null +++ b/games/pong_bot_e/v0.3/ggs_network_eqc_test.erl @@ -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))). + +