anchor.diff:  
   %% --- syn ---
   
  -syn_pre(S) ->
  -  in_tcp_state(S, listen).
  -
  -syn_args(S) ->
  -  [S#state.ip, S#state.port, ip(), port(), uint32()].
  -
  -syn(Ip, Port, RemoteIp, RemotePort, RemoteSeq) ->
  +%% syn_pre(S) ->
  +%%   in_tcp_state(S, listen).
  +
  +syn_args(Ss) ->
  +  ?LET(S, elements(Ss),
  +       [S#state.ip, S#state.port, ip(), port(), uint32(), S#state.id]).
  +
  +syn(Ip, Port, RemoteIp, RemotePort, RemoteSeq, _Id) ->
     Packet =
       #pkt{sport = RemotePort,
            dport = Port,
  
positive.code:   inject(RemoteIp, Ip, Data),
    ok.
  
  syn_ack_callouts(_S, [_Ip, _Port, _RemoteIp, _RemotePort, Seq, _Ack]) ->
    ?SET(rseq, {Seq, 1}),
    ?UNBLOCK(syn_sent, ok).
  
  
  %% --- ack ---
  
  ack_pre(S) ->
    in_tcp_state(S, [syn_rcvd, last_ack, fin_wait_1, closing]) andalso
    S#state.seq == S#state.rcvd.
  
  ack_args(S) ->
    [S#state.ip, S#state.port,
     S#state.rip,
     S#state.rport,
     S#state.rseq,
     S#state.seq].
  
  ack_pre(S, Args) ->
    Args == ack_args(S).
  
  ack_adapt(S, _) -> ack_args(S).
  
  ack(Ip,  Port, RemoteIp, RemotePort, Seq, Ack) ->
    Packet =
      #pkt{sport = RemotePort,
           dport = Port,
  
negative.code: %% --- start ---
  
  start_args(_S) ->
    [ip(), 0].
  
  start(Ip, _) ->
    tcp_pool:start(ip2int(Ip)),
    iss:start(),
    tcp:start(),
    ok.
  
  start_next(_S, _, [Ip, Nr]) ->
    [#state{tcp_state = closed,
            ip = Ip, 
            id = N+1} || N<-lists:seq(0,Nr)].
  
  %% --- open (connect) ---
  
  %% open_pre(S) ->
  %%   in_tcp_state(S, closed).
  
  open_args(Ss) ->
    [ip(), port(), choose(1,length(Ss))].
  
  open_pre(Ss, [_, _, Id]) ->
    in_tcp_state(Ss, Id, closed).
  
  %% We cannot use the _next to bind the socket, because we block
  open(RemoteIp, RemotePort, _Id) ->
    mock:set_socket(tcp_con:usr_open(ip2int(RemoteIp), RemotePort)).
  
  open_process(_, _) ->
    spawn.
  
  open_callouts(_S, [RemoteIp, RemotePort, Id]) ->
    ?SET(Id, rip,   RemoteIp),
    ?SET(Id, rport, RemotePort),
    ?MATCH(Port, ?APPLY(sent_syn, [Id])),
    ?SET(Id, tcp_state, syn_sent),
    ?SET(Id, port, Port),
    ?BLOCK({syn_sent, Id}),
    ?PAR([ ?APPLY(set_socket, [Id])
         , ?APPLY(sent_ack, [Id]) ]),
    ?SET(Id, socket_type, connect),
    ?SET(Id, tcp_state, established).
  
  %% --- listen ---
  
  %% listen_pre(S) ->
  %%   in_tcp_state(S, closed).
  
  listen_args(Ss) ->
    [ port(), choose(1,length(Ss)) ].
  
  listen_pre(Ss, [_, Id]) ->
    in_tcp_state(Ss, Id, closed).
  
  listen(Port, _) ->
    tcp_con:usr_listen(Port).
  
  listen_callouts(_S, [Port, Id]) ->
    ?SET(Id, tcp_state, listen),
    ?SET(Id, socket_type, listen),
    ?SET(Id, port, Port).
  
  listen_next(Ss, V, [_, Id]) ->
    [ S ] = [ S || S<-Ss, S#state.id == Id],
    (Ss -- [S]) ++ [S#state{socket = V}].
  
  %% --- accept ---
  
  %% accept_pre(S) ->
  %%   in_tcp_state(S, [listen, syn_rcvd, established, close_wait]) andalso
  %%   S#state.socket_type == listen.
  
  accept_args(Ss) ->
    ?LET(S, elements(Ss),
         [S#state.socket, S#state.id]).
  
  accept_pre(Ss, [Socket, Id]) ->
    [ S ] = [ S || S<-Ss, S#state.id == Id ],
    S#state.socket == Socket andalso S#state.socket_type == listen andalso
      in_tcp_state(Ss, Id, [listen, syn_rcvd, established, close_wait]).
  
  accept_adapt(Ss, [_, Id]) -> 
    [ S ] = [ S || S<-Ss, S#state.id == Id ],
    [S#state.socket, Id].
  
  accept(Socket, _) ->
    mock:set_socket(tcp_con:usr_accept(Socket)).
  
  accept_callouts(Ss, [_Socket, Id]) ->
    ?SET(Id, socket_type, accept),
    ?WHEN(in_tcp_state(Ss, Id, [listen, syn_rcvd]), ?BLOCK({accept, Id})),
    ?APPLY(set_socket, [Id]),
    ?RET(ok).
  
  accept_process(_S, [_Socket, _]) ->
    spawn.
  
  %% --- close ---
  
  %% close_pre(S) ->
  %%   in_tcp_state(S, [established, close_wait, listen]) andalso
  %%   lists:member(S#state.socket_type, [accept, connect]).
  
  close_args(Ss) ->
    ?LET(S, elements(Ss),
         [S#state.socket, S#state.id]).
  
  close_pre(Ss, [Socket, Id]) ->
    [ S ] = [ S || S<-Ss, S#state.id == Id ],
    S#state.socket == Socket andalso
      in_tcp_state(Ss, Id, [established, close_wait, listen]) andalso
      lists:member(S#state.socket_type, [accept, connect]).
  
  closet_adapt(Ss, [_, Id]) -> 
    [ S ] = [ S || S<-Ss, S#state.id == Id ],
    [S#state.socket, Id].
  
  close(Socket, _) ->
    Root = self(),
    %% Work around for RACE CONDITION 4
    Pid = spawn(fun() -> Root ! {self(), tcp_con:usr_close(Socket)} end),
    receive {Pid, _Res} -> ok end.
  
  
  close_callouts(Ss, [_, Id]) ->
    [ S ] = [ S || S<-Ss, S#state.id == Id ],
    case S#state.tcp_state of
      close_wait ->
        ?APPLY(sent_fin, [Id]),
        ?SET(Id, tcp_state, last_ack),
        ?BLOCK({close, Id});
      established ->
        ?APPLY(sent_fin, [Id]),
        ?SET(Id, tcp_state, fin_wait_1),
        ?BLOCK({close, Id});
      _ ->
        ?APPLY(reset, [Id]),
        ?SET(Id, tcp_state, closed),
        ?SET(Id, socket_type, undefined),
        ?BLOCK({close, Id})
    end.
  
  close_process(_, _) -> spawn.
  