anchor.diff:  -define(QC_OUT(P),
           eqc:on_output(fun(Str, Args) -> io:format(user, Str, Args) end, P)).
   
  --record(state,{vclock, model}).
  +-record(state, {vclocks = []}).
   
   eqc_test_() ->
       ?_assert(eqc:quickcheck(?QC_OUT(prop_vclock()))).
  
positive.code: 
  %% 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, _C, _Res) ->
      true.
  
  
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,_,_,_}) ->
  