/*									*
 * LTSA model for DCCP, as of draft-ietf-dccp-spec-05.txt		*
 * (c) Mark Handley							*
 *									*/


/*
You'll be pleased to know that the model reveals no other problems
with the spec - at least so far.  I'm not yet modelling what happens
when one end loses state in the middle.  But ignoring state loss,
there are no other cases where lost packets or duplicates can cause us
to deadlock or fail to complete the connection.

I've included the model below, purely for your amusement.  I'm not
expecting you to do anything with it.  The LTSA web page is
  http://www.doc.ic.ac.uk/~jnm/

Of course this is a pretty high-level model - it ignores a lot of
detail.  But it is machine checkable for progress and deadlocks, so if
the model matches the spec (I think it probably does, but I need to
double check), then it serves as a formal proof that the rules are
sufficient to ensure that the connection always completes.

Cheers,
	Mark
*/


set Msgs = {request, response, data, dataack, ack, sync, syncack, close, closereq, reset}

CLIENT = CLOSED,
CLOSED = (send.request -> REQUEST),
REQUEST = (  send.request -> REQUEST
           | recv.response -> send.ack -> PARTOPEN
           | recv.closereq -> send.reset -> REQUEST
           | recv.reset -> TIMEWAIT 
          ),
PARTOPEN = (  recv.response-> send.ack -> PARTOPEN
            | partopentimeout -> send.sync -> PARTOPEN /*XXX not in spec - deadlocks without this */
            | appclose -> send.close -> CLOSING
            | recv.data-> OPEN
            | recv.dataack -> OPEN
            | recv.ack -> OPEN
            | recv.sync -> send.syncack -> OPEN
            | recv.syncack -> OPEN
            | recv.request -> PARTOPEN /*ignore?*/
            | recv.close -> send.reset -> CLIENTEND
            | recv.closereq -> CLOSING
),
OPEN = (  recv.data -> OPEN
        | recv.dataack -> OPEN
        | recv.ack -> OPEN
        | recv.syncack -> OPEN
        | send.data -> OPEN
        | send.dataack -> OPEN
        | send.ack -> OPEN
        | appclose -> send.close -> CLOSING
        | recv.close -> send.reset -> CLIENTEND
        | recv.closereq -> send.close -> CLOSING
        | recv.request -> send.sync -> OPEN /*or ignore?*/
        | recv.response -> send.sync -> OPEN /*ignore?*/
       ),
CLOSING = (  send.close -> CLOSING
           | recv.reset -> TIMEWAIT
           | recv.closereq -> send.close -> CLOSING
           | recv.close -> send.reset -> CLIENTEND
           | recv.data -> CLOSING /*not in spec*/
           | recv.ack -> CLOSING /*not in spec*/
           | recv.dataack -> CLOSING /*not in spec*/
           | recv.request -> send.sync -> CLOSING /*step 9*/
           | recv.response -> CLOSING /*not in spec*/
           | recv.sync -> send.syncack -> CLOSING /*step 16, should be close?*/
           | recv.syncack -> CLOSING /*not in spec*/
          ),
TIMEWAIT = ( recv.reset -> TIMEWAIT
            | recv.request -> send.reset -> TIMEWAIT
            | recv.response -> send.reset -> TIMEWAIT            
            | recv.data -> send.reset -> TIMEWAIT            
            | recv.dataack -> send.reset -> TIMEWAIT            
            | recv.ack -> send.reset -> TIMEWAIT
            | recv.sync -> send.reset -> TIMEWAIT
            | recv.syncack -> send.reset -> TIMEWAIT
            | recv.close -> send.reset -> TIMEWAIT
            | recv.closereq -> send.reset -> TIMEWAIT
            | timewaitexpired -> CLIENTEND
           ), 
CLIENTEND = ( recv.reset -> CLIENTEND
            | recv.request -> send.reset -> CLIENTEND
            | recv.response -> send.reset -> CLIENTEND            
            | recv.data -> send.reset -> CLIENTEND            
            | recv.dataack -> send.reset -> CLIENTEND            
            | recv.ack -> send.reset -> CLIENTEND
            | recv.sync -> send.reset -> CLIENTEND
            | recv.syncack -> send.reset -> CLIENTEND
            | recv.close -> send.reset -> CLIENTEND
            | recv.closereq -> send.reset -> CLIENTEND
            | end -> CLIENTEND
           ) + {send.response, send.closereq}. /*packets the client doesn't send*/


/* check client reaches ending closed state*/
progress DOESEND = {end}
   
/* DUPS tests what happens when every packet is duplicated */  
DUPS = (recv.request -> recv.request -> DUPS
        | recv.response -> recv.response -> DUPS
        | recv.data -> recv.data -> DUPS
        | recv.dataack -> recv.dataack -> DUPS
        | recv.ack -> recv.ack -> DUPS
        | recv.sync -> recv.sync -> DUPS
        | recv.syncack -> recv.syncack -> DUPS
        | recv.close -> recv.close -> DUPS
        | recv.closereq -> recv.closereq -> DUPS
        | recv.reset -> recv.reset -> DUPS).


||DUPSAFECLIENT = (CLIENT || DUPS).

SERVER = LISTEN,
LISTEN = (recv.request -> send.response -> RESPOND
          | recv.response -> send.reset -> LISTEN
          | recv.data -> send.reset -> LISTEN
          | recv.dataack -> send.reset -> LISTEN /*ignoring init cookie*/
          | recv.ack -> send.reset -> LISTEN
          | recv.sync -> send.reset -> LISTEN
          | recv.syncack -> send.reset -> LISTEN
          | recv.close -> send.reset -> LISTEN
          | recv.reset -> LISTEN),
RESPOND = (  recv.ack -> OPEN
           | recv.dataack -> OPEN
           | recv.reset -> TIMEWAIT
           | recv.request -> send.response -> RESPOND 
           | appclose -> send.closereq -> CLOSEREQ
           | recv.response -> send.sync -> RESPOND 
           | recv.close -> send.reset -> SERVEREND 
           | recv.closereq -> send.sync -> RESPOND 
           | recv.data -> send.sync -> RESPOND 
           | recv.sync -> send.syncack -> RESPOND
           | recv.syncack -> RESPOND),
OPEN = (  recv.data -> OPEN
        | recv.dataack -> OPEN
        | recv.ack -> OPEN
        | recv.syncack -> OPEN
        | send.data -> OPEN
        | send.dataack -> OPEN
        | send.ack -> OPEN
        | appclose -> send.closereq -> CLOSEREQ
        | recv.close -> send.reset -> SERVEREND
        | recv.closereq -> send.sync -> OPEN
        | recv.request -> send.sync -> OPEN 
        | recv.response -> send.sync -> OPEN 
       ),
CLOSEREQ = ( send.closereq -> CLOSEREQ
           | recv.reset -> TIMEWAIT
           | recv.closereq -> send.sync -> CLOSEREQ /*step 9*/
           | recv.close -> send.reset -> SERVEREND
           | recv.data -> CLOSEREQ /*not in spec*/
           | recv.ack -> CLOSEREQ /*not in spec*/
           | recv.dataack -> CLOSEREQ /*not in spec*/
           | recv.request -> CLOSEREQ /*not in spec*/
           | recv.response -> send.sync -> CLOSEREQ /*step 9*/
           | recv.sync -> send.syncack -> CLOSEREQ /*step 16*/
           | recv.syncack -> CLOSEREQ /*step 7*/
          ),
TIMEWAIT = ( recv.reset -> TIMEWAIT
            | recv.request -> send.reset -> TIMEWAIT
            | recv.response -> send.reset -> TIMEWAIT            
            | recv.data -> send.reset -> TIMEWAIT            
            | recv.dataack -> send.reset -> TIMEWAIT            
            | recv.ack -> send.reset -> TIMEWAIT
            | recv.sync -> send.reset -> TIMEWAIT
            | recv.syncack -> send.reset -> TIMEWAIT
            | recv.close -> send.reset -> TIMEWAIT
            | recv.closereq -> send.reset -> TIMEWAIT
            | timewaitexpired -> SERVEREND
           ), 
SERVEREND = ( recv.reset -> SERVEREND
            | recv.request -> send.reset -> SERVEREND
            | recv.response -> send.reset -> SERVEREND            
            | recv.data -> send.reset -> SERVEREND            
            | recv.dataack -> send.reset -> SERVEREND            
            | recv.ack -> send.reset -> SERVEREND
            | recv.sync -> send.reset -> SERVEREND
            | recv.syncack -> send.reset -> SERVEREND
            | recv.close -> send.reset -> SERVEREND
            | recv.closereq -> send.reset -> SERVEREND
            | end -> SERVEREND
           )+ {send.request, send.close}. /*packets the server doesn't send*/

||DUPSAFESERVER = (SERVER || DUPS).


/* channel from client to server that can pass, lose or duplicate messages */
LOSSYCHANNEL1 = (c.send[i:Msgs] -> (s.recv[i] -> ( csnormal -> LOSSYCHANNEL1
                                                  | s.recv[i] -> LOSSYCHANNEL1)
                                    | csloss[i] -> LOSSYCHANNEL1 ))\{null}.
LOSSYCHANNEL2 = (s.send[j:Msgs] -> (c.recv[j] -> ( scnormal -> LOSSYCHANNEL2
                                                  | c.recv[j] -> LOSSYCHANNEL2)
                                    | scloss[j] -> LOSSYCHANNEL2 )).

/* channel that doesn't duplicate packets */
CHANNEL1 = (c.send[i:Msgs] -> ( s.recv[i] -> CHANNEL1
                               | csloss[i] -> CHANNEL1 )).
CHANNEL2 = (s.send[j:Msgs] -> (c.recv[j] ->  CHANNEL2
                               | scloss[j] -> CHANNEL2 )).

||CLIENTSERVER = (c:CLIENT || s:SERVER || LOSSYCHANNEL1 || LOSSYCHANNEL2)
                  /{end/{c.end,s.end}}.

||CLIENTSERVERNODUPS = (c:CLIENT || s:SERVER || LOSSYCHANNEL1 || LOSSYCHANNEL2)
                       /{end/{c.end,s.end}}<<{csnormal, scnormal}.

||CLIENTSERVERNOLOSS = (c:CLIENT || s:SERVER || LOSSYCHANNEL1 || LOSSYCHANNEL2)
                       /{end/{c.end,s.end}}>>{csloss[Msgs],scloss[Msgs]}.

||CLIENTSERVERPERFECT = (c:CLIENT || s:SERVER || CHANNEL1 || CHANNEL2)
                       /{end/{c.end,s.end}}>>{csloss[Msgs],scloss[Msgs]}.


/* don't allow the client to close - insist the server closes */
||CLIENTSERVERSERVCLOSE = (c:CLIENT || s:SERVER || LOSSYCHANNEL1 || LOSSYCHANNEL2)
                       /{end/{c.end,s.end}}>>{c.appclose}.


/* don't allow the server to close - insist the client closes */
||CLIENTSERVERCLIENTCLOSE = (c:CLIENT || s:SERVER || LOSSYCHANNEL1 || LOSSYCHANNEL2)
                       /{end/{c.end,s.end}}>>{s.appclose}.