Put the same thing twice

[martinsumner]

aae_eqc:start("b", {parallel, leveled_ko}, false, {1, 1},
    [{0, 3}, {1, 3}, {2, 3}], Dir) ->
  <0.1634.0>
aae_eqc:start("a", {parallel, leveled_ko}, false, {1, 1},
    [{0, 3}, {1, 3}, {2, 3}], Dir) ->
  <0.1647.0>
aae_eqc:put("a", <0.1647.0>, [{0, 3}, {1, 3}, {2, 3}],
    <<98, 117, 99, 107, 101, 116, 49>>,
    <<36, 206, 131, 177, 96, 0, 47, 124, 22, 24, 123, 15, 166, 40,
      211, 99>>,
    [{e, 2}], [{e, 1}], {1, 1, 0, [{1549, 448000, 0}], []}) ->
  ok
aae_eqc:put("a", <0.1647.0>, [{0, 3}, {1, 3}, {2, 3}],
    <<98, 117, 99, 107, 101, 116, 49>>,
    <<36, 206, 131, 177, 96, 0, 47, 124, 22, 24, 123, 15, 166, 40,
      211, 99>>,
    [{e, 2}], [{e, 1}], {1, 1, 0, [{1549, 448000, 0}], []}) ->
  ok
aae_eqc:exchange("a", "b", [<0.1647.0>, [{0, 3}, {1, 3}, {2, 3}]],
    [<0.1634.0>, [{0, 3}, {1, 3}, {2, 3}]]) ->
  {root_compare, 0}

Reason:
  Post-condition failed:
  0 /= 1
false

Need to understand this better

[martinsumner]

This shrunk example is incorrect - in that the aae code is doing the right thing, but the shrunk eqc test is doing something incorrect. It has two PUTs on controller "a" for the same key that replace a current clock [{e, 1}] with a new clock [{e, 2}]. However, the original clock is never entered into the store, and then the second put makes no sense in repeating the replacement.

[martinsumner]

Looking at an un-shrunk example, there are faults in the model not just in the shrinking.

Take this:

aae_eqc:start("a", {parallel, leveled_ko}, true, {0, 3600},
    [{0, 3}, {1, 3}, {2, 3}], Dir) ->
  <0.9859.1>
aae_eqc:put("a", <0.9859.1>, [{0, 3}, {1, 3}, {2, 3}],
    <<98, 117, 99, 107, 101, 116, 51>>,
    <<209, 38, 73, 156, 43, 78, 114, 112, 108, 138, 231, 59, 255,
      173, 68, 6>>,
    [{c, 19}], none, {23, 12, 0, [{1549, 448001, 0}], []}) ->
  ok
aae_eqc:put("a", <0.9859.1>, [{0, 3}, {1, 3}, {2, 3}],
    <<98, 117, 99, 107, 101, 116, 49>>,
    <<5, 129, 35, 170, 171, 227, 112, 176, 143, 178, 169, 119, 204,
      4, 101, 238>>,
    [{a, 10}, {c, 41}, {e, 33}, {f, 11}], none,
    {22, 10, 0, [{1549, 448036, 0}], []}) ->
  ok
aae_eqc:put("a", <0.9859.1>, [{0, 3}, {1, 3}, {2, 3}],
    <<98, 117, 99, 107, 101, 116, 51>>,
    <<194, 70, 191, 230, 69, 135, 243, 124, 233, 102, 161, 91, 86,
      94, 13, 117>>,
    [{a, 0}, {b, 30}, {c, 21}, {f, 13}], none,
    {26, 15, 0, [{1549, 448017, 0}], []}) ->
  ok
aae_eqc:stop("a", <0.9859.1>) -> ok
aae_eqc:start("b", {parallel, leveled_ko}, true, {1, 1},
    [{0, 3}, {1, 3}, {2, 3}], Dir) ->
  <0.9872.1>
aae_eqc:nextrebuild("b", <0.9872.1>) -> false
aae_eqc:nextrebuild("b", <0.9872.1>) -> false
aae_eqc:nextrebuild("b", <0.9872.1>) -> false
aae_eqc:put("b", <0.9872.1>, [{0, 3}, {1, 3}, {2, 3}],
    <<98, 117, 99, 107, 101, 116, 51>>,
    <<194, 70, 191, 230, 69, 135, 243, 124, 233, 102, 161, 91, 86,
      94, 13, 117>>,
    [{a, 0}, {b, 30}, {c, 31}, {f, 13}],
    [{a, 0}, {b, 30}, {c, 21}, {f, 13}],
    {3, 28, 0, [{1549, 448075, 0}], []}) ->
  ok
aae_eqc:put("b", <0.9872.1>, [{0, 3}, {1, 3}, {2, 3}],
    <<98, 117, 99, 107, 101, 116, 49>>,
    <<202, 143, 206, 203, 168, 216, 38, 170, 169, 34, 20, 155, 125,
      147, 87, 71>>,
    [{b, 18}, {e, 21}, {f, 10}], none,
    {32, 32, 0, [{1549, 448036, 0}], []}) -> 
  ok
aae_eqc:start("a", {parallel, leveled_ko}, false, {0, 3600},
    [{0, 3}, {1, 3}, {2, 3}], Dir) ->
  <0.9885.1>
aae_eqc:nextrebuild("b", <0.9872.1>) -> false
aae_eqc:sync("a", "b", [{0, 3}, {1, 3}, {2, 3}], [{0, 3}, {1, 3}, {2, 3}],
    <0.9885.1>, <0.9872.1>,
    [{{<<98, 117, 99, 107, 101, 116, 51>>,
       <<209, 38, 73, 156, 43, 78, 114, 112, 108, 138, 231, 59, 255,
         173, 68, 6>>},
      [{c, 19}], [{1549, 448001, 0}]},
     {{<<98, 117, 99, 107, 101, 116, 49>>,
       <<5, 129, 35, 170, 171, 227, 112, 176, 143, 178, 169, 119, 204,
         4, 101, 238>>},
      [{a, 10}, {c, 41}, {e, 33}, {f, 11}], [{1549, 448036, 0}]},
     {{<<98, 117, 99, 107, 101, 116, 51>>,
       <<194, 70, 191, 230, 69, 135, 243, 124, 233, 102, 161, 91, 86,
         94, 13, 117>>},
      [{a, 0}, {b, 30}, {c, 41}, {f, 13}], [{1549, 448026, 0}]},
     {{<<98, 117, 99, 107, 101, 116, 49>>,
       <<202, 143, 206, 203, 168, 216, 38, 170, 169, 34, 20, 155, 125,
         147, 87, 71>>},
      [{b, 18}, {e, 21}, {f, 10}], [{1549, 448036, 0}]}]) ->
  ok
aae_eqc:put("a", <0.9885.1>, [{0, 3}, {1, 3}, {2, 3}],
    <<98, 117, 99, 107, 101, 116, 49>>,
    <<202, 143, 206, 203, 168, 216, 38, 170, 169, 34, 20, 155, 125,
      147, 87, 71>>,
    [{b, 21}, {e, 21}, {f, 10}], [{b, 18}, {e, 21}, {f, 10}],
    {42, 2, 0, [{1549, 448032, 0}], []}) ->
  ok
aae_eqc:put("b", <0.9872.1>, [{0, 3}, {1, 3}, {2, 3}],
    <<98, 117, 99, 107, 101, 116, 51>>,
    <<194, 70, 191, 230, 69, 135, 243, 124, 233, 102, 161, 91, 86,
      94, 13, 117>>,
    [{a, 0}, {b, 30}, {c, 41}, {f, 13}],
    [{a, 0}, {b, 30}, {c, 21}, {f, 13}],
    {12, 34, 0, [{1549, 448053, 0}], []}) ->
  ok
aae_eqc:exchange("b", "a", [<0.9872.1>, [{0, 3}, {1, 3}, {2, 3}]],
    [<0.9885.1>, [{0, 3}, {1, 3}, {2, 3}]]) ->
  {repair, {clock_compare, 1},
     [{{<<98, 117, 99, 107, 101, 116, 49>>,
        <<202, 143, 206, 203, 168, 216, 38, 170, 169, 34, 20, 155, 125,
          147, 87, 71>>},
       {[{b, 18}, {e, 21}, {f, 10}], [{b, 21}, {e, 21}, {f, 10}]}}]}

Now manually filter all activity except that related to key
<<194, 70, 191, 230, 69, 135, 243, 124, 233, 102, 161, 91, 86, 94, 13, 117>>

aae_eqc:start("a", {parallel, leveled_ko}, true, {0, 3600},
    [{0, 3}, {1, 3}, {2, 3}], Dir) ->
  <0.9859.1>
aae_eqc:put("a", <0.9859.1>, [{0, 3}, {1, 3}, {2, 3}],
    <<98, 117, 99, 107, 101, 116, 51>>,
    <<194, 70, 191, 230, 69, 135, 243, 124, 233, 102, 161, 91, 86,
      94, 13, 117>>,
    [{a, 0}, {b, 30}, {c, 21}, {f, 13}], none,
    {26, 15, 0, [{1549, 448017, 0}], []}) ->
  ok
aae_eqc:start("b", {parallel, leveled_ko}, true, {1, 1},
    [{0, 3}, {1, 3}, {2, 3}], Dir) ->
  <0.9872.1>
aae_eqc:put("b", <0.9872.1>, [{0, 3}, {1, 3}, {2, 3}],
    <<98, 117, 99, 107, 101, 116, 51>>,
    <<194, 70, 191, 230, 69, 135, 243, 124, 233, 102, 161, 91, 86,
      94, 13, 117>>,
    [{a, 0}, {b, 30}, {c, 31}, {f, 13}],
    [{a, 0}, {b, 30}, {c, 21}, {f, 13}],
    {3, 28, 0, [{1549, 448075, 0}], []}) ->
  ok
...

The PUT into "b" is erroneous as it is an update to the previous clock `[{a, 0}, {b, 30}, {c, 21}, {f, 13}]` - but there is no entry for this key in "b" at this stage, this key is only in "a" under this clock.

[martinsumner]

kv_index_tictactree/test/aae_eqc.erl

Lines 56 to 64 in 792b02f

	gen_bkcm(S) ->
	?LET({B, K}, frequency([{length(maps:get(history, S, [])), ?LAZY(elements([F || {F, _, _} <-maps:get(history, S)]))},
	{10, {gen_bucket(), gen_key()}}]),
	case lists:keyfind({B, K}, 1, maps:get(history, S, [])) of
	false ->
	{B, K, none, gen_vclock(), gen_last_modified()};
	{_, PrevClock, _LastModifed} ->
	{B, K, PrevClock, gen_vclock(PrevClock), gen_last_modified()}
	end).

Looking at this code, the bucket key clock generator used in the PUT gets the previous clock from the history of changes to either controller ... not to the specific controller which is being modified.

This is incorrect and would cause the false failures that we see.

[ThomasArts]

But then we should modify this to get the correct previous and not always "undefined". With always having previous key undefined we test a different part of the code.