anchor.diff:  objects() ->
       non_empty(list(object())).
   
  +levels() ->
  +    frequency([{20, 1},
  +               { 5, 2}, % production
  +               { 1, 3}]).
  +
  +mem_levels() -> %% Number of memory levels - strongly favor defefault setting
  +    frequency([{20, 0},
  +               { 1, 1},
  +               { 1, 2},
  +               { 1, 3},
  +               { 1, 4}]).
  +
  +width() ->
  +    frequency([{  1,    8},
  +               {100,   16}, % pick for high density segments
  +               {  1,   32},
  +               {  1,   64},
  +               {  1,  128},
  +               {  1,  256},
  +               {  1,  512},
  +               { 50, 1024}]). % pick for production
  +
  +params() -> % {Segments, Width, MemLevels}
  +    %% Generate in terms of number of levels, from that work out the segments
  +    ?LET({Levels, Width, MemLevels},{levels(), width(), mem_levels()},
  +         {trunc(math:pow(Width, Levels)), Width, MemLevels}).
  +
   mark() ->
       frequency([{1, mark_empty}, {5, mark_open}]).
   
  -command(_S = #state{started = Started}) ->
  +%% Generate tree ids - the first one is used for the test, the others are added
  +%% as empty hashtrees.
  +ids() ->
  +    non_empty(list({?LET(X, nat(), 1+X), ?LET(X,nat(), min(X,255))})).
  +
  +%%
  +%% Generate the commands, split into two cases to force the start to happen as
  +%% the first command.
  +%%
  +command(_S = #state{started = false}) ->
  +    {call, ?MODULE, start, [params(), ids(), mark(), mark()]};
  +command(_S = #state{started = true, tree_id = TreeId,
  +                    params = {_Segments, _Width, MemLevels},
  +                    snap1 = Snap1, snap2 = Snap2}) ->
  +    %% Weights to increase snap frequency once update snapshot has begun
  +    SS = Snap1 /= undefined orelse Snap2 /= undefined,
  +    SF = case SS of true -> 100; _ -> 1 end,
       frequency(
  -        [{1, {call, ?MODULE, start,
  -              [{oneof(?POWERS), oneof(?POWERS), choose(0, 4)}, mark(), mark()]}} || not Started] ++
  -        [{1, {call, ?MODULE, update_tree, [t1]}} || Started] ++
  -        [{1, {call, ?MODULE, update_tree, [t2]}} || Started] ++
  -        [{50, {call, ?MODULE, write, [t1, objects()]}} || Started] ++
  -        [{50, {call, ?MODULE, write, [t2, objects()]}} || Started] ++
  -        [{100,{call, ?MODULE, write_both, [objects()]}} || Started] ++
  -        [{50, {call, ?MODULE, delete, [t1, key()]}} || Started] ++
  -        [{50, {call, ?MODULE, delete, [t2, key()]}} || Started] ++
  -        [{100,{call, ?MODULE, delete_both, [key()]}} || Started] ++
  -        [{1, {call, ?MODULE, reopen_tree, [t1]}} || Started] ++
  -        [{1, {call, ?MODULE, reopen_tree, [t2]}} || Started] ++
  -        [{1, {call, ?MODULE, unsafe_close, [t1]}} || Started] ++
  -        [{1, {call, ?MODULE, unsafe_close, [t2]}} || Started] ++
  -        [{1, {call, ?MODULE, rehash_tree, [t1]}} || Started] ++
  -        [{1, {call, ?MODULE, rehash_tree, [t2]}} || Started] ++
  -        [{1, {call, ?MODULE, reconcile, []}} || Started] ++
  -        []
  +      %% Update snapshots/trees. If memory is enabled must test with update_tree
  +      %% If not, can use the method used by kv/yz_index_hashtree and separate
  +      %% the two steps, dumping the result from update_perform.
  +        [{10*SF, {call, ?MODULE, update_tree,  [t1, s1]}} || Snap1 == undefined] ++
  +	[{10*SF, {call, ?MODULE, update_snapshot,  [t1, s1]}} || Snap1 == undefined, MemLevels == 0] ++
  +	[{10*SF, {call, ?MODULE, update_perform,   [t1]}} || Snap1 == created, MemLevels == 0] ++
  +	[{10*SF, {call, ?MODULE, set_next_rebuild, [t1]}} || Snap1 == updated] ++
  +        [{10*SF, {call, ?MODULE, update_tree,  [t2, s2]}} || Snap1 == undefined] ++
  +	[{10*SF, {call, ?MODULE, update_snapshot,  [t2, s2]}} || Snap2 == undefined, MemLevels == 0] ++
  +	[{10*SF, {call, ?MODULE, update_perform,   [t2]}} || Snap2 == created, MemLevels == 0] ++
  +	[{10*SF, {call, ?MODULE, set_next_rebuild, [t2]}} || Snap2 == updated] ++
  +
  +      %% Can only run compares when both snapshots are updated.  Boost the frequency
  +      %% when both are snapshotted (note this is guarded by both snapshot being updatable)
  +        [{100*SF, {call, ?MODULE, local_compare, []}} || Snap1 == updated, Snap2 == updated] ++
  +
  +      %% Modify the data in the two tables
  +        [{101-SF, {call, ?MODULE, write, [t1, objects()]}},
  +	 {101-SF, {call, ?MODULE, write, [t2, objects()]}},
  +         {101-SF, {call, ?MODULE, write_both, [objects()]}},
  +         {101-SF, {call, ?MODULE, delete, [t1, key()]}},
  +         {101-SF, {call, ?MODULE, delete, [t2, key()]}},
  +         {101-SF, {call, ?MODULE, delete_both, [key()]}},
  +
  +      %% Mess around with reopening, crashing and rehashing.
  +         {  1, {call, ?MODULE, reopen_tree, [t1, TreeId]}},
  +         {  1, {call, ?MODULE, reopen_tree, [t2, TreeId]}},
  +         {  1, {call, ?MODULE, unsafe_close, [t1, TreeId]}},
  +         {  1, {call, ?MODULE, unsafe_close, [t2, TreeId]}},
  +         {  1, {call, ?MODULE, rehash_tree, [t1]}},
  +         {  1, {call, ?MODULE, rehash_tree, [t2]}}
  +	]
       ).
   
  -start(Params, T1Mark, T2Mark) ->
  +%%
  +%% Start the model up - initialize two trees, either mark them as open and empty
  +%% or request they are checked.  Add additional unused hashtrees with ExtraIds
  +%% to make sure the iterator code is fully exercised.
  +%%
  +%% Store the hashtree records in the process dictionary under keys 't1' and 't2'.
  +%% 
  +start(Params, [TreeId | ExtraIds], T1Mark, T2Mark) ->
       {Segments, Width, MemLevels} = Params,
       %% Return now so we can store symbolic value in procdict in next_state call
  -    HT1 = hashtree:new({0,0}, [{segments, Segments},
  +    T1 = hashtree:new(TreeId, [{segments, Segments},
                                  {width, Width},
                                  {mem_levels, MemLevels}]),
   
  -    T1 = case T1Mark of
  -        mark_empty -> hashtree:mark_open_empty({0,0}, HT1);
  -        _ -> hashtree:mark_open_and_check({0,0}, HT1)
  +    T1A = case T1Mark of
  +        mark_empty -> hashtree:mark_open_empty(TreeId, T1);
  +        _ -> hashtree:mark_open_and_check(TreeId, T1)
       end,
   
  -    put(t1, T1),
  -
  -    HT2 = hashtree:new({0,0}, [{segments, Segments},
  -                               {width, Width},
  -                               {mem_levels, MemLevels}]),
  -
  -    T2 = case T2Mark of
  -        mark_empty -> hashtree:mark_open_empty({0,0}, HT2);
  -        _ -> hashtree:mark_open_and_check({0,0}, HT2)
  +    add_extra_hashtrees(ExtraIds, T1A),
  +
  +    put(t1, T1A),
  +
  +    T2 = hashtree:new(TreeId, [{segments, hashtree:segments(T1A)},
  +                               {width, hashtree:width(T1A)},
  +                               {mem_levels, hashtree:mem_levels(T1A)}]),
  +
  +    T2A = case T2Mark of
  +        mark_empty -> hashtree:mark_open_empty(TreeId, T2);
  +        _ -> hashtree:mark_open_and_check(TreeId, T2)
       end,
   
  -    put(t2, T2),
  -
  -    ets:new(t1, [named_table, public, set]),
  -    ets:new(t2, [named_table, public, set]),
  -    ok.
  -
  +    add_extra_hashtrees(ExtraIds, T2A),
  +
  +    put(t2, T2A),
  +
  +    %% Make sure ETS is pristine
  +    catch ets:delete(t1),
  +    catch ets:delete(t2),
  +    catch ets:delete(s1),
  +    catch ets:delete(s2),
  +    ets_new(t1),
  +    ets_new(t2),
  +    TreeId.
  +			   
  +
  +%% Add some extra tree ids and update the metadata to give
  +%% the iterator code a workout on non-matching ids.
  +add_extra_hashtrees(ExtraIds, T) ->
  +    lists:foldl(fun(ExtraId, Tacc) ->
  +			Tacc2 = hashtree:new(ExtraId, Tacc),
  +			Tacc3 = hashtree:mark_open_empty(ExtraId, Tacc2),
  +			Tacc4 = hashtree:insert(<<"k">>, <<"v">>, Tacc3),
  +			hashtree:flush_buffer(Tacc4)
  +		end, T, ExtraIds).
  +
  +%% Wrap the hashtree:update_tree call.  This works with memory levels
  +%% enabled.  Copy the model tree to a snapshot table.
  +update_tree(T, S) ->
  +    %% Snapshot the hashtree and store both states
  +    HT = hashtree:update_tree(get(T)),
  +    put(T, HT),
  +    %% Copy the current ets table to the snapshot table.
  +    copy_tree(T, S),
  +    ok.
  +
  +%% Wrap the hashtree:update_snapshot call and set the next rebuild type to full
  +%% to match the behavior needed by the *_index_hashtree modules that consume
  +%% hashtree.  Otherwise if the state is treated as incremental on a safe reopen
  +%% then the tree does not rebuild correctly.
  +%%
  +%% Store the snapshot state in the process dictionary under {snapstate, t1} or
  +%% {snapstate, t2} for use by update_perform.
  +%%
  +%% N.B. This does not work with memory levels enabled as update_perform uses the
  +%% snapshot state which is dumped.
  +%%
  +update_snapshot(T, S) ->
  +    %% Snapshot the hashtree and store both states
  +    {SS, HT} = hashtree:update_snapshot(get(T)),
  +
  +    %% Mark as a full rebuild until the update perfom step happens.
  +    HT2 = hashtree:set_next_rebuild(HT, full),
  +
  +    put(T, HT2),
  +    put({snapstate, T}, SS),
  +    %% Copy the current ets table to the snapshot table.
  +    copy_tree(T, S),
  +    ok.
  +
  +
  +%% 
  +%% Wrap the hashtree:update_perform call and erase the snapshot hashtree state.
  +%% Should only happen if a snapshot state exists.
  +%%
  +update_perform(T) ->
  +    _ = hashtree:update_perform(get({snapstate, T})),
  +    erase({snapstate, T}),
  +    ok.
  +
  +
  +%% Set the next rebuild state. Should only happen once update perform has
  +%% completed.
  +%%
  +set_next_rebuild(T) ->
  +    _ = hashtree:set_next_rebuild(get(T), incremental).
  +
  +
  +%% Wrap hashtree:insert to (over)write key with a new hash to a single
  +%% table and insert into the model tree.
  +%%
   write(T, Objects) ->
       lists:foreach(fun({Key, Hash}) ->
                             put(T, hashtree:insert(Key, Hash, get(T))),
  
positive.code:                     catch ets:delete(t1),
                      catch ets:delete(t2),
                      {_H,S,Res} = HSR = run_commands(?MODULE,Cmds),
                      pretty_commands(?MODULE, Cmds, HSR,
                                      ?WHENFAIL(
                                         begin
                                             catch hashtree:destroy(hashtree:close(get(t1))),
                                             catch hashtree:destroy(hashtree:close(get(t2)))
                                         end,
                              begin
                                      Unique1 = S#state.only1 -- S#state.only2,
                                      Unique2 = S#state.only2 -- S#state.only1,
                                      Expected =  [{missing, Key} || {Key, _} <-
                                          Unique2, not
                                          lists:keymember(Key, 1, S#state.only1)] ++
                                      [{remote_missing, Key} || {Key, _} <-
                                          Unique1, not
                                          lists:keymember(Key, 1, S#state.only2)] ++
                                      [{different, Key} || Key <-
                                          sets:to_list(sets:intersection(sets:from_list([Key
                                                          || {Key,_} <- Unique1]),
                                                  sets:from_list([Key || {Key,_}
                                                      <- Unique2])))],
  
                                  case S#state.started of
                                      false ->
                                          true;
                                      _ ->
                                          %% io:format("\nFinal update tree1:\n"),
                                          T10 = hashtree:update_tree(get(t1)),
                                          %% io:format("\nFinal update tree2:\n"),
                                          T20 = hashtree:update_tree(get(t2)),
  
                                          %% io:format("\nFinal compare:\n"),
                                          KeyDiff = hashtree:local_compare(T10, T20),
  
                                          D1 = try dump(T10) catch _:Err1 -> Err1 end,
                                          D2 = try dump(T20) catch _:Err2 -> Err2 end,
  
                                          T11 = hashtree:mark_clean_close({0,0}, T10),
                                          T21 = hashtree:mark_clean_close({0,0}, T20),
                                          catch hashtree:destroy(hashtree:close(T11)),
                                          catch hashtree:destroy(hashtree:close(T21)),
                                          {Segments, Width, MemLevels} = S#state.params,
  
                                          ?WHENFAIL(
                                             begin
                                                 eqc:format("only1:\n~p\n", [S#state.only1]),
                                                 eqc:format("only2:\n~p\n", [S#state.only2]),
                                                 eqc:format("t1:\n~p\n", [D1]),
                                                 eqc:format("t2:\n~p\n", [D2])
                                             end,
                                             collect(with_title(mem_levels), MemLevels,
                                             collect(with_title(segments), Segments,
                                             collect(with_title(width), Width,
                                             collect(with_title(length),
                                             length(S#state.only1) + length(S#state.only2),
                                                     conjunction([{cmds, equals(ok, Res)},
                                                                  {diff, equals(lists:usort(Expected),
                                                                                lists:usort(KeyDiff))}]))))))
                                  end
                              end
                                  ))
                          end)).
  
  dump(Tree) ->
      Fun = fun(Entries) ->
  
negative.code:         mark_empty -> eq(NextRebuildT2, incremental);
          _ -> eq(NextRebuildT2, full)
      end;
  %% After a comparison, check against the results against
  %% the ETS table containing the *snapshot* copies.
  postcondition(_S,{call, _, local_compare, _},  Result) ->
      Expect = expect_compare(),
      eq(Expect, lists:sort(Result));	
  postcondition(_S,{call,_,_,_},_R) ->
      true.
  
  next_state(S,R,{call, _, start, [Params,_ExtraIds,_,_]}) ->
      %% Start returns the TreeId used, stick in the state
      %% as no hashtree:tree_id call yet.
      S#state{started = true, tree_id = R, params = Params};
  next_state(S,_V,{call, _, update_tree, [t1, _]}) ->
      S#state{snap1 = updated};
  next_state(S,_V,{call, _, update_tree, [t2, _]}) ->
      S#state{snap2 = updated};
  next_state(S,_V,{call, _, update_snapshot, [t1, _]}) ->
      S#state{snap1 = created};
  next_state(S,_V,{call, _, update_snapshot, [t2, _]}) ->
      S#state{snap2 = created};
  next_state(S,_V,{call, _, update_perform, [t1]}) ->
      S#state{snap1 = updated};
  next_state(S,_V,{call, _, update_perform, [t2]}) ->
      S#state{snap2 = updated};
  next_state(S,_V,{call, _, set_next_rebuild, [t1]}) ->
      S#state{snap1 = undefined};
  next_state(S,_V,{call, _, set_next_rebuild, [t2]}) ->
      S#state{snap2 = undefined};
  next_state(S,_V,{call, _, write, [_T, Objs]}) ->
      S#state{num_updates = S#state.num_updates + length(Objs)};
  next_state(S,_R,{call, _, write_both, [Objs]}) ->
      S#state{num_updates = S#state.num_updates + 2*length(Objs)};
  next_state(S,_V,{call, _, delete, _}) ->
      S#state{num_updates = S#state.num_updates + 1};
  next_state(S,_R,{call, _, delete_both, _}) ->
      S#state{num_updates = S#state.num_updates + 2};
  next_state(S,_R,{call, _, reopen_tree, [t1, _]}) ->
      S#state{snap1 = undefined};
  next_state(S,_R,{call, _, reopen_tree, [t2, _]}) ->
      S#state{snap2 = undefined};
  next_state(S,_R,{call, _, unsafe_close, [t1, _]}) ->
      S#state{snap1 = undefined};
  next_state(S,_R,{call, _, unsafe_close, [t2, _]}) ->
      S#state{snap2 = undefined};
  next_state(S,_R,{call, _, rehash_tree, [t1]}) ->
      S#state{snap1 = undefined};
  next_state(S,_R,{call, _, rehash_tree, [t2]}) ->
      S#state{snap2 = undefined};
  next_state(S,_R,{call, _, local_compare, []}) ->
      S.
  
  prop_correct() ->
      ?FORALL(Cmds,commands(?MODULE, #state{}),
              aggregate(command_names(Cmds),
                  begin
                      %%io:format(user, "Starting in ~p\n", [self()]),
  