anchor.diff:              precondition_debug("precondition leave_cluster: no nodes left to remove.", []),
               false %% Might need to be changed when there's no read/write operations.
       end;
  -precondition(#state{majority_nodes=MajorityNodes, minority_nodes=MinorityNodes, fault_model_state=FaultModelState, node_state=NodeState, joined_nodes=JoinedNodes}, {call, Mod, Fun, [Node|_]=Args}=Call) -> 
  -    precondition_debug("precondition fired for node function: ~p, majority_nodes: ~p, minority_nodes ~p", [Fun, MajorityNodes, MinorityNodes]),
  +precondition(#state{fault_model_state=FaultModelState, node_state=NodeState, joined_nodes=JoinedNodes}, {call, Mod, Fun, [Node|_]=Args}=Call) -> 
  +    precondition_debug("precondition fired for node function: ~p", [Fun]),
   
       case lists:member(Fun, node_functions()) of
           true ->
  -            case ?BIAS_MINORITY andalso length(MinorityNodes) > 0 of
  -                true ->
  -                    precondition_debug("precondition fired for node function where minority is biased: ~p, bias_minority: ~p, checking whether node ~p is in minority", [Fun, ?BIAS_MINORITY, Node]),
  -                    case lists:member(Node, MinorityNodes) of
  -                        true ->
  -                            debug("=> bias towards minority, write is going to node ~p in minority", [Node]),
  -                            ClusterCondition = enough_nodes_connected(JoinedNodes) andalso is_joined(Node, JoinedNodes),
  -                            NodePrecondition = node_precondition(NodeState, Call),
  -                            FaultPrecondition = not fault_is_crashed(FaultModelState, Node),
  -                            ClusterCondition andalso NodePrecondition andalso FaultPrecondition;
  -                        false ->
  -                            false
  -                    end;
  -                false ->
  -                    ClusterCondition = enough_nodes_connected(JoinedNodes) andalso is_joined(Node, JoinedNodes),
  -                    NodePrecondition = node_precondition(NodeState, Call),
  -                    FaultPrecondition = not fault_is_crashed(FaultModelState, Node),
  -                    ClusterCondition andalso NodePrecondition andalso FaultPrecondition
  -            end;
  +            ClusterCondition = enough_nodes_connected(JoinedNodes) andalso is_joined(Node, JoinedNodes),
  +            NodePrecondition = node_precondition(NodeState, Call),
  +            FaultPrecondition = not fault_is_crashed(FaultModelState, Node),
  +            ClusterCondition andalso NodePrecondition andalso FaultPrecondition;
           false ->
               case lists:member(Fun, fault_functions()) of 
                   true ->
  
positive.code:         ?LET(Names, names(), 
              ?LET(Sublist, lists:sublist(Names, trunc(MajorityCount)), Sublist))).
  
  %% Is a node involved in a byzantine fault?
  is_involved_in_byzantine_fault(SourceNode, DestinationNode, ByzantineFaults) ->
      Source = case dict:find({SourceNode, DestinationNode}, ByzantineFaults) of
          error ->
              false;
          _ ->
              true
      end,
  
      Destination = case dict:find({DestinationNode, SourceNode}, ByzantineFaults) of
          error ->
              false;
          _ ->
              true
      end,
  
      Source orelse Destination.
  
  %% Is a node involved in an sync partition?
  is_involved_in_partition(SourceNode, DestinationNode, PartitionFilters) ->
      Source = case dict:find({SourceNode, DestinationNode}, PartitionFilters) of
          error ->
              false;
          _ ->
              true
      end,
  
      Destination = case dict:find({DestinationNode, SourceNode}, PartitionFilters) of
          error ->
              false;
          _ ->
              true
      end,
  
      Source orelse Destination.
  
  delete_sync_partition(SourceNode, DestinationNode, PartitionFilters) ->
      delete_async_partition(DestinationNode, SourceNode, 
          delete_async_partition(SourceNode, DestinationNode, PartitionFilters)).
  
  delete_async_partition(SourceNode, DestinationNode, PartitionFilters) ->
      dict:erase({SourceNode, DestinationNode}, PartitionFilters).
  
  add_sync_partition(SourceNode, DestinationNode, PartitionFilters) ->
      add_async_partition(SourceNode, DestinationNode,
          add_async_partition(DestinationNode, SourceNode, PartitionFilters)).
  
  add_async_partition(SourceNode, DestinationNode, PartitionFilters) ->
      dict:store({SourceNode, DestinationNode}, true, PartitionFilters).
  
  add_byzantine_fault(SourceNode, DestinationNode, Value, ByzantineFaults) ->
      dict:store({SourceNode, DestinationNode}, Value, ByzantineFaults).
  
  delete_byzantine_fault(SourceNode, DestinationNode, ByzantineFaults) ->
      dict:erase({SourceNode, DestinationNode}, ByzantineFaults).
  
  add_cluster_partition(MajorityNodes, AllNodes, PartitionFilters) ->
      MinorityNodes = AllNodes -- MajorityNodes,
  
      lists:foldl(fun(SourceNode, Filters) ->
          lists:foldl(fun(DestinationNode, Filters2) ->
              add_sync_partition(SourceNode, DestinationNode, Filters2)
              end, Filters, MinorityNodes)
          end, PartitionFilters, MajorityNodes).
  
  delete_cluster_partition(MajorityNodes, AllNodes, PartitionFilters) ->
      MinorityNodes = AllNodes -- MajorityNodes,
  
      lists:foldl(fun(SourceNode, Filters) ->
          lists:foldl(fun(DestinationNode, Filters2) ->
              delete_sync_partition(SourceNode, DestinationNode, Filters2)
              end, Filters, MinorityNodes)
          end, PartitionFilters, MajorityNodes).
  
  induce_cluster_partition(MajorityNodes, AllNodes) ->
      MinorityNodes = AllNodes -- MajorityNodes,
      debug("induce_cluster_partition: majority_nodes ~p minority_nodes ~p", [MajorityNodes, MinorityNodes]),
  
      Results = lists:flatmap(fun(SourceNode) ->
          lists:flatmap(fun(DestinationNode) ->
              [
               induce_async_partition(SourceNode, DestinationNode),
               induce_async_partition(DestinationNode, SourceNode)
              ]
              end, MinorityNodes)
          end, MajorityNodes),
      all_to_ok_or_error(Results).
  
  resolve_cluster_partition(MajorityNodes, AllNodes) ->
      MinorityNodes = AllNodes -- MajorityNodes,
  
      debug("resolve_cluster_partition: majority_nodes ~p minority_nodes ~p", [MajorityNodes, MinorityNodes]),
      Results = lists:flatmap(fun(SourceNode) ->
          lists:flatmap(fun(DestinationNode) ->
              [
               resolve_async_partition(SourceNode, DestinationNode),
               resolve_async_partition(DestinationNode, SourceNode)
              ]
              end, MinorityNodes)
          end, MajorityNodes),
      all_to_ok_or_error(Results).
  
  is_involved_in_x_partitions(Node, X, PartitionFilters) ->
      Count = dict:fold(fun(Key, _Value, AccIn) ->
              case Key of
                  {Node, _} ->
                      AccIn + 1;
                  _ ->
                      AccIn
              end
          end, 0, PartitionFilters),
      postcondition_debug("is_involved_in_x_partitions is ~p and should be ~p", [Count, X]),
      Count >= X.
  
  is_valid_partition(SourceNode, DestinationNode) ->
      SourceNode =/= DestinationNode.
  
  induce_byzantine_message_corruption_fault(SourceNode, DestinationNode0, Value) ->
      partition_debug("induce_byzantine_message_corruption_fault: source_node ~p destination_node ~p value ~p", [SourceNode, DestinationNode0, Value]),
  
      %% Convert to real node name and not symbolic name.
      DestinationNode = name_to_nodename(DestinationNode0),
  
      InterpositionFun = fun({forward_message, N, Message}) ->
          case N of
              DestinationNode ->
                  lager:info("~p: rewriting packet from ~p to ~p for message from ~p to ~p due to interposition.", [node(), Message, Value, SourceNode, DestinationNode]),
                  Value;
              OtherNode ->
                  lager:info("~p: allowing message, doesn't match interposition as destination is ~p and not ~p", [node(), OtherNode, DestinationNode]),
                  Message
          end;
          ({receive_message, _N, Message}) -> Message
      end,
      rpc:call(name_to_nodename(SourceNode), ?MANAGER, add_interposition_fun, [{corruption, DestinationNode}, InterpositionFun]).
  
  resolve_byzantine_message_corruption_fault(SourceNode, DestinationNode0) ->
      partition_debug("resolve_byzantine_message_corruption_fault: source_node ~p destination_node ~p", [SourceNode, DestinationNode0]),
  
      %% Convert to real node name and not symbolic name.
      DestinationNode = name_to_nodename(DestinationNode0),
  
      rpc:call(name_to_nodename(SourceNode), ?MANAGER, remove_interposition_fun, [{corruption, DestinationNode}]).
  
  induce_async_partition(SourceNode, DestinationNode0) ->
      partition_debug("induce_async_partition: source_node ~p destination_node ~p", [SourceNode, DestinationNode0]),
  
      %% Convert to real node name and not symbolic name.
      DestinationNode = name_to_nodename(DestinationNode0),
  
      InterpositionFun = fun({forward_message, N, Message}) ->
          case N of
              DestinationNode ->
                  lager:info("~p: dropping packet from ~p to ~p due to interposition.", [node(), SourceNode, DestinationNode]),
                  undefined;
              OtherNode ->
                  lager:info("~p: allowing message, doesn't match interposition as destination is ~p and not ~p", [node(), OtherNode, DestinationNode]),
                  Message
          end;
          ({receive_message, _N, Message}) -> Message
      end,
      rpc:call(name_to_nodename(SourceNode), ?MANAGER, add_interposition_fun, [{async, DestinationNode}, InterpositionFun]).
  
  resolve_async_partition(SourceNode, DestinationNode0) ->
      partition_debug("resolve_async_partition: source_node ~p destination_node ~p", [SourceNode, DestinationNode0]),
  
      %% Convert to real node name and not symbolic name.
      DestinationNode = name_to_nodename(DestinationNode0),
  
      rpc:call(name_to_nodename(SourceNode), ?MANAGER, remove_interposition_fun, [{async, DestinationNode}]).
  
  induce_sync_partition(SourceNode, DestinationNode) ->
      partition_debug("induce_sync_partition: source_node ~p destination_node ~p", [SourceNode, DestinationNode]),
      SourceResult = induce_async_partition(SourceNode, DestinationNode),
      DestinationResult = induce_async_partition(DestinationNode, SourceNode),
      all_to_ok_or_error([SourceResult, DestinationResult]).
  
  resolve_sync_partition(SourceNode, DestinationNode) ->
      partition_debug("resolve_sync_partition: source_node ~p destination_node ~p", [SourceNode, DestinationNode]),
      SourceResult = resolve_async_partition(SourceNode, DestinationNode),
      DestinationResult = resolve_async_partition(DestinationNode, SourceNode),
      all_to_ok_or_error([SourceResult, DestinationResult]).
  
  delayed_resolve_sync_partition(Timeout, SourceNode, DestinationNode) ->
      partition_debug("delayed_resolve_sync_partition: source_node ~p destination_node ~p", [SourceNode, DestinationNode]),
      timer:sleep(Timeout),
      SourceResult = resolve_async_partition(SourceNode, DestinationNode),
      DestinationResult = resolve_async_partition(DestinationNode, SourceNode),
      all_to_ok_or_error([SourceResult, DestinationResult]).
  
  leave_cluster(Name, JoinedNames) ->
      Node = name_to_nodename(Name),
      debug("leave_cluster: leaving node ~p from cluster with members ~p", [Node, JoinedNames]),
  
negative.code:             []
      end,
  
      MemberCommands.
  
  name_to_nodename(Name) ->
      [{_, NodeName}] = ets:lookup(?MODULE, Name),
      NodeName.
  
  ensure_tracing_started() ->
      partisan_trace_orchestrator:start_link().