anchor.diff:          end, true, Recipients),
   
           All andalso MessageAcc
  -    end, true, Sent);
  +    end, true, Sent),
  +
  +    FailedToSendNotReceived = lists:foldl(fun({Message, Recipients}, MessageAcc) ->
  +        node_debug("verifying that message ~p was NOT received by ~p", [Message, Recipients]),
  +
  +        All = lists:foldl(fun(Recipient, NodeAcc) ->
  +            node_debug("=> verifying that message ~p was NOT received by ~p", [Message, Recipient]),
  +
  +            %% Did this node receive the message?
  +            Messages = dict:fetch(Recipient, Results),
  +
  +            %% Carry forward.
  +            case lists:member(Message, Messages) of 
  +                true ->
  +                    node_debug("=> => message received at node ~p: ~p", [Message, Recipient]),
  +                    NodeAcc andalso false;
  +                false ->
  +                    NodeAcc andalso true
  +            end
  +        end, true, Recipients),
  +
  +        All andalso MessageAcc
  +    end, true, FailedToSend),
  +
  +    AllSentAndReceived andalso FailedToSendNotReceived;
   node_postcondition(_NodeState, _Command, _Response) ->
       false.
   
  
positive.code:     true;
  node_postcondition(_NodeState, {call, ?MODULE, broadcast, [_Node, _Message]}, ok) ->
      true;
  node_postcondition(#node_state{sent=Sent}, {call, ?MODULE, check_mailbox, []}, Results) ->
      lists:foldl(fun({Message, Recipients}, MessageAcc) ->
          node_debug("verifying that message ~p was received by ~p", [Message, Recipients]),
  
          All = lists:foldl(fun(Recipient, NodeAcc) ->
  
negative.code: %%% Node Functions
  %%%===================================================================
  
  -record(node_state, {sent, failed_to_send}).
  
  %% What node-specific operations should be called.
  node_commands() ->
  