anchor.diff:  %% Given the state `State' *prior* to the call `{call, Mod, Fun, Args}',
   %% determine whether the result `Res' (coming from the actual system)
   %% makes sense.
  -postcondition(_State, {call, ?MODULE, induce_byzantine_message_corruption_fault, [_SourceNode, _DestinationNode, _Value]}, ok) ->
  -    postcondition_debug("postcondition induce_byzantine_message_corruption_fault: succeeded", []),
  -    %% Added message filter.
  -    true;
  -postcondition(_State, {call, ?MODULE, resolve_byzantine_message_corruption_fault, [_SourceNode, _DestinationNode]}, ok) ->
  -    postcondition_debug("postcondition resolve_byzantine_message_corruption_fault: succeeded", []),
  -    %% Remove message filter.
  -    true;
  -postcondition(_State, {call, ?MODULE, induce_async_partition, [_SourceNode, _DestinationNode]}, ok) ->
  -    postcondition_debug("postcondition induce_async_partition: succeeded", []),
  -    %% Added message filter.
  -    true;
  -postcondition(_State, {call, ?MODULE, resolve_async_partition, [_SourceNode, _DestinationNode]}, ok) ->
  -    postcondition_debug("postcondition resolve_async_partition: succeeded", []),
  -    %% Removed message filter.
  -    true;
  -postcondition(_State, {call, ?MODULE, induce_sync_partition, [_SourceNode, _DestinationNode]}, ok) ->
  -    postcondition_debug("postcondition induce_sync_partition: succeeded", []),
  -    %% Added message filter.
  -    true;
  -postcondition(_State, {call, ?MODULE, resolve_sync_partition, [_SourceNode, _DestinationNode]}, ok) ->
  -    postcondition_debug("postcondition resolve_sync_partition: succeeded", []),
  -    %% Removed message filter.
  -    true;
  -postcondition(_State, {call, ?MODULE, delayed_resolve_sync_partition, [_Timeout, _SourceNode, _DestinationNode]}, ok) ->
  -    postcondition_debug("postcondition delayed_resolve_sync_partition: succeeded", []),
  -    %% Removed message filter.
  -    true;
  -postcondition(_State, {call, ?MODULE, induce_cluster_partition, [_MajorityNodes, _MinorityNodes]}, ok) ->
  -    postcondition_debug("postcondition induce_cluster_partition: succeeded", []),
  -    %% Added message filter.
  -    true;
  -postcondition(_State, {call, ?MODULE, resolve_cluster_partition, [_MajorityNodes, _MinorityNodes]}, ok) ->
  -    postcondition_debug("postcondition resolve_cluster_partition: succeeded", []),
  -    %% Removed message filter.
  -    true;
   postcondition(_State, {call, ?MODULE, join_cluster, [_Node, _JoinedNodes]}, ok) ->
       postcondition_debug("postcondition join_cluster: succeeded", []),
       %% Accept joins that succeed.
  
positive.code: 
  %% Debug.
  -define(DEBUG, true).
  -define(PARTITION_DEBUG, true).
  -define(INITIAL_STATE_DEBUG, false).
  -define(PRECONDITION_DEBUG, false).
  -define(POSTCONDITION_DEBUG, false).
  
negative.code: 
  -define(SUPPORT, partisan_support).
  
  %% General test configuration
  -define(NUM_NODES, 3).
  -define(COMMAND_MULTIPLE, 1).
  