tcpconnection.sm

SMC takes a state machine stored in a .sm file and generates a State pattern in twelve programming l

// -*- tab-width: 4; -*-

%{
//
// The contents of this file are subject to the Mozilla Public
// License Version 1.1 (the "License"); you may not use this file
// except in compliance with the License. You may obtain a copy
// of the License at http://www.mozilla.org/MPL/
// 
// Software distributed under the License is distributed on an
// "AS IS" basis, WITHOUT WARRANTY OF ANY KIND, either express or
// implied. See the License for the specific language governing
// rights and limitations under the License.
// 
// The Original Code is State Machine Compiler (SMC).
// 
// The Initial Developer of the Original Code is Charles W. Rapp.
// Portions created by Charles W. Rapp are
// Copyright (C) 2000 - 2003 Charles W. Rapp.
// All Rights Reserved.
// 
// Contributor(s): 
//
// Name
//  TcpConnection.sm
//
// Description
//  The TCP/IP state transition diagram.
//
// RCS ID
// $Id: TcpConnection.sm,v 1.2 2007/08/05 13:28:02 cwrapp Exp $
//
// CHANGE LOG
// $Log: TcpConnection.sm,v $
// Revision 1.2  2007/08/05 13:28:02  cwrapp
// Version 5.0.1 check-in. See net/sf/smc/CODE_README.txt for more information.
//
// Revision 1.1  2005/05/28 12:49:21  cwrapp
// Added Ant examples 1 - 7.
//
// Revision 1.0  2004/05/31 13:25:19  charlesr
// Initial revision
//
%}

%class TcpConnection
%start MainMap::CLOSED
%package smc_ex6
%import java.net.InetAddress

%map MainMap
%%
CLOSED
{
    PassiveOpen(port: int)
        ServiceOpening
        {
            openServerSocket(port);
        }

    ActiveOpen(address: InetAddress, port: int)
        ClientOpening
        {
            openClientSocket(address, port);
        }

    AcceptOpen(segment: TcpSegment)
        SYN_RCVD
        {
            sendAcceptSynAck(segment);
        }

    // Ignore undefined transtions when closed.
    UNDEF(segment: TcpSegment)
		nil
        {}

    // Ignore close requests when closed.
    Close
        nil
        {}
}

// Wait here until service open has either succeeded or failed.
ServiceOpening
{
    Opened
        LISTEN
        {
            openSuccess();
        }

    OpenFailed(reason: String)
        CLOSED
        {
            openFailed(reason);
        }
}

// Wait here until client open has either succeeded or failed.
ClientOpening
{
    Opened(address: InetAddress, port: int)
        SYN_SENT
        {
            send(TcpSegment.SYN,
                 null,
                 0,
                 0,
                 address,
                 port,
                 null);}

    OpenFailed(reason: String)
        CLOSED
        {
            openFailed(reason);
        }
}

// Server sockets just sit here, creating new client sockets when
// a SYN is received.
LISTEN
{
    // Create a new client socket and send its port number in
    // the SYN/ACK response.
    SYN(segment: TcpSegment)
        nil
        {
            accept(segment);
        }

    Close
        CLOSED
        {
            closeSocket();
            closed("");
        }

    // But don't reset a reset message because there is no
    // connection to reset.
    RST(segment: TcpSegment)
        nil
        {}
}

// An "accepted" client socket starts life in this state.
SYN_RCVD
Entry
{
    startTimer("ACK_TIMER", TcpConnection.ACK_TIMEOUT);
}
Exit
{
    stopTimer("ACK_TIMER");
}
{
    // The connection was reset before it was established.
    // Close the datagram socket but don't tell anybody.
    RST(segment: TcpSegment)
        CLOSED
        {
            closeSocket();
            clearListener();
        }

    // The TCP state transition diagram shows the server socket
    // taking an ACK transtion to the ESTABLISHED state but that
    // is not quite true. The accepted client socket starts in
    // the ESTABLISHED state while the server socket goes back to
    // LISTEN.
    ACK(segment: TcpSegment)
      [(segment.getSourceAddress()).equals(ctxt.getFarAddress()) == true &&
       segment.getSourcePort() == ctxt.getFarPort() &&
       segment.getAcknowledgeNumber() == ctxt.getSequenceNumber()]
        ESTABLISHED
        {
            accepted();
        }

    Close
        FIN_WAIT_1
        {
            send(TcpSegment.FIN,
                 null,
                 0,
                 0,
                 null,
                 -1,
                 null);
        }

    AckTimeout
        CLOSED
        {
            closeSocket();
            openFailed("acknowledge timeout");
        }
}

// A application-created client starts life in this state.
SYN_SENT
Entry
{
    startTimer("CONN_ACK_TIMER", TcpConnection.ACK_TIMEOUT);
}
Exit
{
    stopTimer("CONN_ACK_TIMER");
}
{
    SYN_ACK(segment: TcpSegment)
      [(segment.getSourceAddress()).equals(ctxt.getFarAddress()) == true &&
       segment.getSourcePort() == ctxt.getFarPort() &&
       segment.getAcknowledgeNumber() == ctxt.getSequenceNumber()]
        ESTABLISHED
        {
            setDestinationPort(segment);
            send(TcpSegment.ACK,
                 null,
                 0,
                 0,
                 segment);
            openSuccess();
        }

    Close
        CLOSED
        {
            closeSocket();
            closed("");
        }

    ConnAckTimeout
        CLOSED
        {
            closeSocket();
            openFailed("acknowledge timeout");
        }
}

ESTABLISHED
{
    FIN(segment: TcpSegment)
      [(segment.getSourceAddress()).equals(ctxt.getFarAddress())
            == true &&
       segment.getSourcePort() == ctxt.getFarPort()]
        CLOSE_WAIT
        {
            send(TcpSegment.ACK,
                 null,
                 0,
                 0,
                 segment);
            halfClosed();
        }

    PSH(segment: TcpSegment)
      [(segment.getSourceAddress()).equals(ctxt.getFarAddress())
            == true &&
       segment.getSourcePort() == ctxt.getFarPort()]
        nil
        {
            send(TcpSegment.ACK,
                 null,
                 0,
                 0,
                 segment);
            receive(segment);
        }

    Transmit(data: byte[], offset: int, size: int)
        Transmitting
        {
            send(TcpSegment.PSH,
                 data,
                 offset,
                 size,
                 null,
                 0,
                 null);
        }

    Close
        FIN_WAIT_1
        {
            send(TcpSegment.FIN,
                 null,
                 0,
                 0,
                 null,
                 0,
                 null);
        }
}

Transmitting
Entry
{
    startTimer("TRANS_ACK_TIMER",
               TcpConnection.ACK_TIMEOUT);
}
Exit
{
    stopTimer("TRANS_ACK_TIMER");}
{
/*
    Transmitted
        nil
        {
            startTimer("TRANS_ACK_TIMER",
                       TcpConnection.ACK_TIMEOUT);
        }

    TransmitFailed(reason: String)
        nil
        {
            transmitFailed(reason);
        }
 */

    ACK(segment: TcpSegment)
      [(segment.getSourceAddress()).equals(ctxt.getFarAddress()) == true &&
       segment.getSourcePort() == ctxt.getFarPort() &&
       segment.getAcknowledgeNumber() == ctxt.getSequenceNumber()]
        ESTABLISHED
        {
            transmitted();
        }

    PSH_ACK(segment: TcpSegment)
      [(segment.getSourceAddress()).equals(ctxt.getFarAddress()) == true &&
       segment.getSourcePort() == ctxt.getFarPort() &&
       segment.getAcknowledgeNumber() == ctxt.getSequenceNumber()]
        ESTABLISHED
        {
            send(TcpSegment.ACK,
                 null,
                 0,
                 0,
                 segment);
            transmitted();
            receive(segment);
        }

    FIN(segment: TcpSegment)
      [(segment.getSourceAddress()).equals(ctxt.getFarAddress()) == true &&
       segment.getSourcePort() == ctxt.getFarPort()]
        CLOSE_WAIT
        {
            send(TcpSegment.ACK,
                 null,
                 0,
                 0,
                 segment);
            halfClosed();
        }

    Close
        FIN_WAIT_1
        {
            send(TcpSegment.FIN,
                 null,
                 0,
                 0,
                 null,
                 0,
                 null);
        }

    TransAckTimeout
        CLOSED
        {
            transmitFailed("peer did not acknowledge");
            closed("connection lost");
        }
}

CLOSE_WAIT
{
    Close
        LAST_ACK
        {
            send(TcpSegment.FIN,
                 null,
                 0,
                 0,
                 null,
                 0,
                 null);
        }
}

LAST_ACK
Entry
{
    startTimer("CLOSE_ACK_TIMER",
               TcpConnection.ACK_TIMEOUT);
}
Exit
{
    stopTimer("CLOSE_ACK_TIMER");
}
{
    ACK(segment: TcpSegment)
      [(segment.getSourceAddress()).equals(ctxt.getFarAddress()) == true &&