anchor.diff:  
   %% Postcondition, checked after command has been evaluated
   %% OBS: S is the state before next_state(S,_,<command>)
  -postcondition(#state{model=M},{call,vclock,increment,[ActorId, Vclock]},Res) ->
  -    %% Partial ordering property (descends)
  -    vclock:descends(Res,Vclock) andalso
  -    %% Counter has been incremented
  -        vclock:get_counter(ActorId, Res) == orddict:fetch(ActorId,M) + 1;
  -postcondition(#state{model=M}, {call,vclock,get_counter,[ActorId, _]}, Res) ->
  -    %% The counter for a given actor is the same as the model
  -    Res == orddict:fetch(ActorId, M);
  -postcondition(#state{model=M}, {call,_,merge,[{OM,Other},VClock]}, Res) ->
  -    Merged = model_merge(M, OM),
  -    %% The merged state has all the same actor counts
  -    lists:all(fun(A) -> orddict:fetch(A,Merged) == vclock:get_counter(A,Res) end, 
  -              ?ACTOR_IDS) andalso
  -        %% The merged vector clock descends from both inputs
  -        vclock:descends(Res, Other) andalso vclock:descends(Res, VClock);
  +postcondition(_S, {call, _, get_counter, _}, {MRes, Res}) ->
  +    MRes == Res;
  +postcondition(_S, {call, _, descends, _}, {MRes, Res}) ->
  +    MRes == Res;
  +postcondition(_S, {call, _, merge, [Items]}, {MRes, Res}) ->
  +    model_compare(MRes, Res) andalso 
  +        lists:all(fun({_, V}) ->
  +                          vclock:descends(Res, V)
  +                  end, Items);
  +postcondition(_S, _C, {MRes, Res}) ->
  +    model_compare(MRes, Res);
   postcondition(_S, _C, _Res) ->
       true.
   
  
positive.code:     elements(?ACTOR_IDS).
  
  gen_vclock() ->
      frequency([
                 {1, {new_model(), vclock:fresh()}},
                 {3, ?LAZY(gen_incr_vclock())}
                ]).
  
  gen_incr_vclock() ->
      ?LET({Actor, {M,Vc}},
           {gen_actor_id(), gen_vclock()},
           {orddict:update_counter(Actor, 1, M), vclock:increment(Actor, Vc)}).
  
  merge({_,O}, V) ->
      vclock:merge([O,V]).
  
  model_merge(M,OM) ->
      orddict:merge(fun(_K,A,B) -> erlang:max(A,B) end, M, OM).
  
  new_model() ->
      orddict:from_list([{ID, 0} || ID <- ?ACTOR_IDS]).
  -endif.
  
negative.code: 
  %% Initialize the state
  initial_state() ->
     #state{}.
  
  %% Command generator, S is the state
  command(#state{vclocks=Vs}) ->
      oneof([{call, ?MODULE, fresh, []}] ++
            [{call, ?MODULE, increment, [gen_actor_id(), elements(Vs)]} || length(Vs) > 0] ++
            [{call, ?MODULE, get_counter, [gen_actor_id(), elements(Vs)]} || length(Vs) > 0] ++
            [{call, ?MODULE, merge, [list(elements(Vs))]} || length(Vs) > 0] ++ 
            [{call, ?MODULE, descends, [elements(Vs), elements(Vs)]} || length(Vs) > 0]
            ).
  
  %% Next state transformation, S is the current state
  next_state(S,_V,{call,_,get_counter,[_, _]}) ->
      S;
  next_state(S,_V,{call,_,descends,[_, _]}) ->
      S;
  next_state(#state{vclocks=Vs}=S,V,{call,_,_,_}) ->
      S#state{vclocks=Vs ++ [V]}.
  
  %% Precondition, checked before command is added to the command sequence
  precondition(_S,{call,_,_,_}) ->
  