Add fill checking to PULSE model, minimal API coverage is complete

prototype/corfurl/src/corfurl.erl

@@ -25,7 +25,7 @@
          read_projection/2,
          save_projection/2]).
 -export([append_page/3, read_page/2, scan_forward/3,
-         fill_page/2]).
+         fill_page/2, trim_page/2]).
 
 -include("corfurl.hrl").
 
@@ -203,16 +203,21 @@ scan_forward(P, LPN, MaxPages, _Status, _MoreP, Acc) ->
 
 fill_page(#proj{epoch=Epoch} = P, LPN) ->
     Chain = project_to_chain(LPN, P),
-    fill_page2(Chain, Epoch, LPN).
+    fill_or_trim_page(Chain, Epoch, LPN, fill).
 
-fill_page2([], _Epoch, _LPN) ->
+trim_page(#proj{epoch=Epoch} = P, LPN) ->
+    Chain = project_to_chain(LPN, P),
+    fill_or_trim_page(Chain, Epoch, LPN, trim).
+
+fill_or_trim_page([], _Epoch, _LPN, _Func) ->
     ok;
-fill_page2([H|T], Epoch, LPN) ->
-    case corfurl_flu:fill(flu_pid(H), Epoch, LPN) of
+fill_or_trim_page([H|T], Epoch, LPN, Func) ->
+    case corfurl_flu:Func(flu_pid(H), Epoch, LPN) of
         ok ->
-            fill_page2(T, Epoch, LPN);
+            fill_or_trim_page(T, Epoch, LPN, Func);
         Else ->
             %% TODO: worth doing anything here, if we're in the middle of chain?
+            %% TODO: is that ^^ anything different for fill vs. trim?
             Else
     end.
 

prototype/corfurl/test/corfurl_pulse.erl

@@ -65,7 +65,7 @@
 %% Define true to fake bad behavior that model **must** notice & fail!
 
 -ifndef(TRIP_no_append_duplicates).
--define(TRIP_no_append_duplicates, false).
+-define(TRIP_no_append_duplicates, true).
 -endif.
 -ifndef(TRIP_bad_read).
 -define(TRIP_bad_read, false).
@@ -76,6 +76,9 @@
 -ifndef(TRIP_bad_fill).
 -define(TRIP_bad_fill, false).
 -endif.
+-ifndef(TRIP_bad_trim).
+-define(TRIP_bad_trim, false).
+-endif.
 
 initial_state() ->
     #state{}.
@@ -115,6 +118,8 @@ command(#state{run=Run} = S) ->
        || S#state.is_setup] ++
       [{4, {call, ?MODULE, fill, [Run, gen_approx_page()]}}
        || S#state.is_setup] ++
+      [{4, {call, ?MODULE, trim, [Run, gen_approx_page()]}}
+       || S#state.is_setup] ++
       [])).
 
 %% Precondition, checked before a command is added to the command sequence.
@@ -138,6 +143,8 @@ next_state(S, _, {call, _, read_approx, _}) ->
 next_state(S, _, {call, _, scan_forward, _}) ->
     S;
 next_state(S, _, {call, _, fill, _}) ->
+    S;
+next_state(S, _, {call, _, trim, _}) ->
     S.
 
 eqeq(X, X) -> true;
@@ -163,12 +170,14 @@ postcondition(_S, {call, _, scan_forward, _}, V) ->
         _ ->
             eqeq(V, {todoTODO_fixit,?LINE})
     end;
-postcondition(_S, {call, _, fill, _}, V) ->
+postcondition(_S, {call, _, FillTrim, _}, V)
+  when FillTrim == fill; FillTrim == trim ->
     case V of
         ok                -> true;
         error_trimmed     -> true;
+        error_unwritten   -> true;
         error_overwritten -> true;
-        _                 -> eqeq(V, {fill_error, V})
+        _                 -> eqeq(V, {error, FillTrim, V})
     end.
 
 valid_read_result(Pg) when is_binary(Pg) -> true;
@@ -305,7 +314,8 @@ check_trace(Trace0, _Cmds, _Seed) ->
     AllLPNsR = eqc_temporal:stateful(
                 fun({call, _Pid, {append, _Pg, will_be, LPN}}) -> LPN;
                    ({call, _Pid, {read, LPN}}) -> LPN;
-                   ({call, _Pid, {fill, LPN, will_be, ok}}) -> LPN
+                   ({call, _Pid, {fill, LPN, will_be, ok}}) -> LPN;
+                   ({call, _Pid, {trim, LPN, will_be, ok}}) -> LPN
                 end,
                 fun(x) -> [] end,
                 Calls),
@@ -333,8 +343,6 @@ check_trace(Trace0, _Cmds, _Seed) ->
                        []
                end,
                Events),
-    %%ModsX = filter_relation_facts(fun(T) when element(4,T) == fill; element(4,T) == trim -> true; (_) -> false end, Mods),
-    %%io:format("Modsx ~p\n", [ModsX]),
 
     %% StartMod contains {mod_start, Ttn, LPN, V} when a modification finished.
     %% DoneMod contains {mod_end, Ttn, LPN, V} when a modification finished.
@@ -675,6 +683,14 @@ fill(#run{seq=Seq, proj=Proj}, SeedInt) ->
              perhaps_trip_fill_page(?TRIP_bad_fill, Res, LPN)
          end).
 
+trim(#run{seq=Seq, proj=Proj}, SeedInt) ->
+    LPN = pick_an_LPN(Seq, SeedInt) + 2,
+    ?LOG({trim, LPN},
+         begin
+             Res = corfurl:trim_page(Proj, LPN),
+             perhaps_trip_trim_page(?TRIP_bad_trim, Res, LPN)
+         end).
+
 perhaps_trip_append_page(false, Res, _Page) ->
     Res;
 perhaps_trip_append_page(true, {ok, LPN}, _Page) when LPN > 3 ->
@@ -693,7 +709,7 @@ perhaps_trip_read_approx(true, Res, _LPN) ->
 
 perhaps_trip_scan_forward(false, Res, _EndLPN) ->
     Res;
-perhaps_trip_scan_forward(true, _Res, 20) ->
+perhaps_trip_scan_forward(true, _Res, 10) ->
     io:format(user, "TRIP: scan_forward\n", []),
     <<"magic number bingo, you are a winner">>;
 perhaps_trip_scan_forward(true, Res, _EndLPN) ->
@@ -701,12 +717,20 @@ perhaps_trip_scan_forward(true, Res, _EndLPN) ->
 
 perhaps_trip_fill_page(false, Res, _EndLPN) ->
     Res;
-perhaps_trip_fill_page(true, _Res, LPN) when 10 =< LPN, LPN =< 20 ->
+perhaps_trip_fill_page(true, _Res, LPN) when 3 =< LPN, LPN =< 5 ->
     io:format(user, "TRIP: fill_page\n", []),
     ok; % can trigger both invalid ttn and bad read
 perhaps_trip_fill_page(true, Res, _EndLPN) ->
     Res.
 
+perhaps_trip_trim_page(false, Res, _EndLPN) ->
+    Res;
+perhaps_trip_trim_page(true, _Res, LPN) when 3 =< LPN, LPN =< 5 ->
+    io:format(user, "TRIP: trim_page\n", []),
+    ok;
+perhaps_trip_trim_page(true, Res, _EndLPN) ->
+    Res.
+
 -endif. % PULSE
 -endif. % TEST