From 2d3a29471d412a1876ca7919e31ca069729fb8e3 Mon Sep 17 00:00:00 2001
From: Scott Lystig Fritchie <slfritchie@snookles.com>
Date: Sun, 28 Sep 2014 14:10:44 +0900
Subject: [PATCH] Minimal FLU0 single register, plus Concuerror tests

---
 prototype/poc-machi/.gitignore               |  1 +
 prototype/poc-machi/Makefile                 |  9 ++
 prototype/poc-machi/src/machi_flu0.erl       | 86 ++++++++++++++++++++
 prototype/poc-machi/test/machi_flu0_test.erl | 66 +++++++++++++++
 4 files changed, 162 insertions(+)
 create mode 100644 prototype/poc-machi/src/machi_flu0.erl
 create mode 100644 prototype/poc-machi/test/machi_flu0_test.erl

diff --git a/prototype/poc-machi/.gitignore b/prototype/poc-machi/.gitignore
index 91f0c9c..8b6cb48 100644
--- a/prototype/poc-machi/.gitignore
+++ b/prototype/poc-machi/.gitignore
@@ -1,5 +1,6 @@
 .eunit
 .eqc-info
+concuerror_report.txt
 current_counterexample.eqc
 deps
 ebin/*.beam
diff --git a/prototype/poc-machi/Makefile b/prototype/poc-machi/Makefile
index c3bdbe5..2a86235 100644
--- a/prototype/poc-machi/Makefile
+++ b/prototype/poc-machi/Makefile
@@ -24,3 +24,12 @@ eunit:
 pulse: compile
 	env USE_PULSE=1 $(REBAR_BIN) skip_deps=true clean compile
 	env USE_PULSE=1 $(REBAR_BIN) skip_deps=true -D PULSE eunit
+
+CONC_ARGS = --pz ./.eunit --treat_as_normal shutdown --after_timeout 1000
+
+concuerror: deps compile
+	$(REBAR_BIN) -v skip_deps=true eunit suites=do_not_exist
+	concuerror -m machi_flu0_test -t concuerror1_test $(CONC_ARGS) && \
+	concuerror -m machi_flu0_test -t concuerror2_test $(CONC_ARGS) && \
+	concuerror -m machi_flu0_test -t concuerror3_test $(CONC_ARGS) && \
+	concuerror -m machi_flu0_test -t concuerror4_test $(CONC_ARGS)
diff --git a/prototype/poc-machi/src/machi_flu0.erl b/prototype/poc-machi/src/machi_flu0.erl
new file mode 100644
index 0000000..4e0ccc4
--- /dev/null
+++ b/prototype/poc-machi/src/machi_flu0.erl
@@ -0,0 +1,86 @@
+-module(machi_flu0).
+
+-behaviour(gen_server).
+
+-export([start_link/0, stop/1,
+         write/2, get/1, trim/1]).
+-ifdef(TEST).
+-compile(export_all).
+-endif.
+
+-export([init/1, handle_call/3, handle_cast/2, handle_info/2,
+         terminate/2, code_change/3]).
+
+-ifdef(TEST).
+-include_lib("eunit/include/eunit.hrl").
+-compile(export_all).
+-ifdef(PULSE).
+-compile({parse_transform, pulse_instrument}).
+-endif.
+-endif.
+
+-define(SERVER, ?MODULE).
+-define(LONG_TIME, infinity).
+%% -define(LONG_TIME, 30*1000).
+%% -define(LONG_TIME, 5*1000).
+
+-type register() :: 'unwritten' | binary() | 'trimmed'.
+
+-record(state, {
+          register = 'unwritten' :: register()
+         }).
+
+start_link() ->
+    gen_server:start_link(?MODULE, [], []).
+
+stop(Pid) ->
+    gen_server:call(Pid, stop, infinity).
+
+get(Pid) ->
+    gen_server:call(Pid, {get}, ?LONG_TIME).
+
+write(Pid, Bin) when is_binary(Bin) ->
+    gen_server:call(Pid, {write, Bin}, ?LONG_TIME).
+
+trim(Pid) ->
+    gen_server:call(Pid, {trim}, ?LONG_TIME).
+
+%%%% %%%% %%%% %%%% %%%% %%%% %%%% %%%% %%%% %%%% %%%% %%%%
+
+init([]) ->
+    {ok, #state{}}.
+
+handle_call({write, Bin}, _From, #state{register=unwritten} = S) ->
+    {reply, ok, S#state{register=Bin}};
+handle_call({write, _Bin}, _From, #state{register=B} = S) when is_binary(B) ->
+    {reply, error_written, S};
+handle_call({write, _Bin}, _From, #state{register=trimmed} = S) ->
+    {reply, error_trimmed, S};
+handle_call({get}, _From, #state{register=Reg} = S) ->
+    {reply, {ok, Reg}, S};
+handle_call({trim}, _From, #state{register=unwritten} = S) ->
+    {reply, ok, S#state{register=trimmed}};
+handle_call({trim}, _From, #state{register=B} = S) when is_binary(B) ->
+    {reply, ok, S#state{register=trimmed}};
+handle_call({trim}, _From, #state{register=trimmed} = S) ->
+    {reply, error_trimmed, S};
+handle_call(stop, _From, MLP) ->
+    {stop, normal, ok, MLP};
+handle_call(_Request, _From, MLP) ->
+    Reply = whaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa,
+    {reply, Reply, MLP}.
+
+handle_cast(_Msg, MLP) ->
+    {noreply, MLP}.
+
+handle_info(_Info, MLP) ->
+    {noreply, MLP}.
+
+terminate(_Reason, _MLP) ->
+    ok.
+
+code_change(_OldVsn, MLP, _Extra) ->
+    {ok, MLP}.
+
+%%%% %%%% %%%% %%%% %%%% %%%% %%%% %%%% %%%% %%%% %%%% %%%%
+
diff --git a/prototype/poc-machi/test/machi_flu0_test.erl b/prototype/poc-machi/test/machi_flu0_test.erl
new file mode 100644
index 0000000..ec5bc8b
--- /dev/null
+++ b/prototype/poc-machi/test/machi_flu0_test.erl
@@ -0,0 +1,66 @@
+
+-module(machi_flu0_test).
+
+-ifdef(TEST).
+-include_lib("eunit/include/eunit.hrl").
+-compile(export_all).
+-endif.
+
+-ifdef(TEST).
+-ifndef(PULSE).
+
+concuerror1_test() ->
+    ok.
+
+concuerror2_test() ->
+    {ok, F} = machi_flu0:start_link(),
+    ok = machi_flu0:stop(F),
+    ok.
+
+concuerror3_test() ->
+    Me = self(),
+    Fun = fun() -> {ok, F1} = machi_flu0:start_link(),
+                        ok = machi_flu0:stop(F1),
+                        Me ! done
+               end,
+    P1 = spawn(Fun),
+    P2 = spawn(Fun),
+    [receive done -> ok end || _ <- [P1, P2]],
+    
+    ok.
+
+concuerror4_test() ->
+    {ok, F1} = machi_flu0:start_link(),
+    Val = <<"val!">>,
+    ok = machi_flu0:write(F1, Val),
+    Me = self(),
+    TrimFun = fun() -> Res = machi_flu0:trim(F1),
+                       Me ! {self(), Res}
+               end,
+    TrimPids = [spawn(TrimFun), spawn(TrimFun),spawn(TrimFun)],
+    TrimExpected = [error_trimmed,error_trimmed,ok],
+
+    GetFun = fun() -> Res = machi_flu0:get(F1),
+                      Me ! {self(), Res}
+               end,
+    GetPids = [spawn(GetFun)],
+    GetExpected = fun(Results) ->
+                          [] = [X || X <- Results, X == unwritten],
+                          ok
+                  end,
+
+    TrimResults = lists:sort([receive
+                                  {TrimPid, Res} -> Res
+                              end || TrimPid <- TrimPids]),
+    TrimExpected = TrimResults,
+    GetResults = lists:sort([receive
+                                 {GetPid, Res} -> Res
+                             end || GetPid <- GetPids]),
+    ok = GetExpected(GetResults),
+
+    ok = machi_flu0:stop(F1),
+    ok.
+    
+
+-endif.
+-endif.