anchor.diff:  
   %% Assuming the postcondition for a call was true, update the model
   %% accordingly for the test to proceed.
  -next_state(#state{byzantine_faults=ByzantineFaults0, active_faults=ActiveFaults}=State, _Res, {call, ?MODULE, induce_byzantine_message_corruption_fault, [SourceNode, DestinationNode, Value]}) -> 
  -    ByzantineFaults = add_byzantine_fault(SourceNode, DestinationNode, Value, ByzantineFaults0),
  -    State#state{byzantine_faults=ByzantineFaults, active_faults=ActiveFaults + 1};
  -next_state(#state{byzantine_faults=ByzantineFaults0, active_faults=ActiveFaults}=State, _Res, {call, ?MODULE, resolve_byzantine_message_corruption_fault, [SourceNode, DestinationNode]}) -> 
  -    ByzantineFaults = delete_byzantine_fault(SourceNode, DestinationNode, ByzantineFaults0),
  -    State#state{byzantine_faults=ByzantineFaults, active_faults=ActiveFaults - 1};
  -next_state(#state{partition_filters=PartitionFilters0, active_faults=ActiveFaults}=State, _Res, {call, ?MODULE, induce_async_partition, [SourceNode, DestinationNode]}) -> 
  -    PartitionFilters = add_async_partition(SourceNode, DestinationNode, PartitionFilters0),
  -    State#state{partition_filters=PartitionFilters, active_faults=ActiveFaults + 1};
  -next_state(#state{partition_filters=PartitionFilters0, active_faults=ActiveFaults}=State, _Res, {call, ?MODULE, resolve_async_partition, [SourceNode, DestinationNode]}) -> 
  -    PartitionFilters = delete_async_partition(SourceNode, DestinationNode, PartitionFilters0),
  -    State#state{partition_filters=PartitionFilters, active_faults=ActiveFaults - 1};
  -next_state(#state{partition_filters=PartitionFilters0}=State, _Res, {call, ?MODULE, induce_sync_partition, [SourceNode, DestinationNode]}) -> 
  -    PartitionFilters = add_sync_partition(SourceNode, DestinationNode, PartitionFilters0),
  -    State#state{partition_filters=PartitionFilters};
  -next_state(#state{partition_filters=PartitionFilters0}=State, _Res, {call, ?MODULE, resolve_sync_partition, [SourceNode, DestinationNode]}) -> 
  -    PartitionFilters = delete_sync_partition(SourceNode, DestinationNode, PartitionFilters0),
  -    State#state{partition_filters=PartitionFilters};
  -next_state(#state{partition_filters=PartitionFilters0}=State, _Res, {call, ?MODULE, delayed_resolve_sync_partition, [_Timeout, SourceNode, DestinationNode]}) -> 
  -    PartitionFilters = delete_sync_partition(SourceNode, DestinationNode, PartitionFilters0),
  -    State#state{partition_filters=PartitionFilters};
  -next_state(#state{partition_filters=PartitionFilters0}=State, _Res, {call, ?MODULE, induce_cluster_partition, [MajorityNodes, AllNodes]}) -> 
  -    MinorityNodes = AllNodes -- MajorityNodes,
  -    PartitionFilters = add_cluster_partition(MajorityNodes, MinorityNodes, PartitionFilters0),
  -    State#state{partition_filters=PartitionFilters, majority_nodes=MajorityNodes, minority_nodes=MinorityNodes};
  -next_state(#state{partition_filters=PartitionFilters0}=State, _Res, {call, ?MODULE, resolve_cluster_partition, [MajorityNodes, AllNodes]}) -> 
  -    MinorityNodes = AllNodes -- MajorityNodes,
  -    PartitionFilters = delete_cluster_partition(MajorityNodes, MinorityNodes, PartitionFilters0),
  -    State#state{partition_filters=PartitionFilters, majority_nodes=[], minority_nodes=[]};
   next_state(State, _Res, {call, ?MODULE, join_cluster, [Node, JoinedNodes]}) -> 
       case is_joined(Node, JoinedNodes) of
           true ->
  
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:     lists:member(Node, Cluster).
  
  cluster_commands(#state{joined_nodes=JoinedNodes}) ->
      MemberCommands = case ?PERFORM_LEAVES_AND_JOINS of
          true ->
              [
  