tcpconnection.sm

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

       segment.getSourcePort() == ctxt.getFarPort() &&
       segment.getAcknowledgeNumber() == ctxt.getSequenceNumber()]
        CLOSED
        {
            closeSocket();
            closed("");
        }

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

FIN_WAIT_1
Entry
{
    startTimer("CLOSE_ACK_TIMER",
               TcpConnection.ACK_TIMEOUT);
}
Exit
{
    stopTimer("CLOSE_ACK_TIMER");
}
{
    ACK(segment: TcpSegment)
      [(segment.getSourceAddress()).equals(ctxt.getFarAddress()) == true &&
       segment.getSourcePort() == ctxt.getFarPort() &&
       segment.getAcknowledgeNumber() == ctxt.getSequenceNumber()]
        FIN_WAIT_2
        {}

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

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

    CloseAckTimeout
        FIN_WAIT_2
        {
            closeSocket();
            closed("");
        }
}

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

CLOSING
Entry
{
    startTimer("CLOSE_ACK_TIMER",
               TcpConnection.ACK_TIMEOUT);
}
Exit
{
    stopTimer("CLOSE_ACK_TIMER");
}
{
    ACK(segment: TcpSegment)
      [(segment.getSourceAddress()).equals(ctxt.getFarAddress()) == true &&
       segment.getSourcePort() == ctxt.getFarPort() &&
       segment.getAcknowledgeNumber() == ctxt.getSequenceNumber()]
        TIME_WAIT
        {}

    CloseAckTimeout
        TIME_WAIT
        {
            closeSocket();
            closed("");
        }

    // Ignore undefined transitions.
    UNDEF(segment: TcpSegment)
		nil
        {}
}

TIME_WAIT
Entry
{
    startTimer("CLOSE_TIMER", TcpConnection.CLOSE_TIMEOUT);
}
{
    CloseTimeout
        CLOSED
        {
            closeSocket();
            closed("");
        }

    // Ignore undefined transitions.
    UNDEF(segment: TcpSegment)
		nil
        {}
}

Default
{
    PassiveOpen(port: int)
        nil
        {
            openFailed("already open");
        }

    ActiveOpen(address: InetAddress, port: int)
        nil
        {
            openFailed("already open");
        }

    Transmit(data: byte[], offset: int, size: int)
        nil
        {
            transmitFailed("connection not established");
        }

    // The default action when an unknown client sends us a
    // segment is to reset the unknown client but remain in
    // the current state for a segment from the real client.
    FIN(segment: TcpSegment)
      [(segment.getSourceAddress()).equals(ctxt.getFarAddress()) == false ||
       segment.getSourcePort() != ctxt.getFarPort()]
        nil
        {
            send(TcpSegment.RST,
                 null,
                 0,
                 0,
                 segment);
            closed("connection reset");
        }

    SYN(segment: TcpSegment)
      [(segment.getSourceAddress()).equals(ctxt.getFarAddress()) == false ||
       segment.getSourcePort() != ctxt.getFarPort()]
        nil
        {
            send(TcpSegment.RST,
                 null,
                 0,
                 0,
                 segment);
            closed("connection reset");
        }

    PSH(segment: TcpSegment)
      [(segment.getSourceAddress()).equals(ctxt.getFarAddress()) == false ||
       segment.getSourcePort() != ctxt.getFarPort()]
        nil
        {
            send(TcpSegment.RST,
                 null,
                 0,
                 0,
                 segment);
            closed("connection reset");
        }

    ACK(segment: TcpSegment)
      [(segment.getSourceAddress()).equals(ctxt.getFarAddress()) == false ||
       segment.getSourcePort() != ctxt.getFarPort()]
        nil
        {
            send(TcpSegment.RST,
                 null,
                 0,
                 0,
                 segment);
            closed("connection reset");
        }

    URG(segment: TcpSegment)
      [(segment.getSourceAddress()).equals(ctxt.getFarAddress()) == false ||
       segment.getSourcePort() != ctxt.getFarPort()]
        nil
        {
            send(TcpSegment.RST,
                 null,
                 0,
                 0,
                 segment);
            closed("connection reset");
        }

    FIN_ACK(segment: TcpSegment)
      [(segment.getSourceAddress()).equals(ctxt.getFarAddress()) == false ||
       segment.getSourcePort() != ctxt.getFarPort()]
        nil
        {
            send(TcpSegment.RST,
                 null,
                 0,
                 0,
                 segment);
            closed("connection reset");
        }

    SYN_ACK(segment: TcpSegment)
      [(segment.getSourceAddress()).equals(ctxt.getFarAddress()) == false ||
       segment.getSourcePort() != ctxt.getFarPort()]
        nil
        {
            send(TcpSegment.RST,
                 null,
                 0,
                 0,
                 segment);
            closed("connection reset");
        }

   PSH_ACK(segment: TcpSegment)
      [(segment.getSourceAddress()).equals(ctxt.getFarAddress()) == false ||
       segment.getSourcePort() != ctxt.getFarPort()]
        nil
        {
            send(TcpSegment.RST,
                 null,
                 0,
                 0,
                 segment);
            closed("connection reset");
        }

    UNDEF(segment: TcpSegment)
      [(segment.getSourceAddress()).equals(ctxt.getFarAddress()) == false ||
       segment.getSourcePort() != ctxt.getFarPort()]
        nil
        {
            send(TcpSegment.RST,
                 null,
                 0,
                 0,
                 segment);
            closed("connection reset");
        }

    // Do not reset a reset. Just go to closed.
    RST(segment: TcpSegment)
        CLOSED
        {
            closed("connection reset by peer");
        }

    RST_ACK(segment: TcpSegment)
        CLOSED
        {
            closed("connection reset by peer");
        }

    // The remain transitions represent segments received
    // when they were not expected from the peer. The
    // connection is reset.
    FIN(segment: TcpSegment)
        CLOSED
        {
            send(TcpSegment.RST,
                 null,
                 0,
                 0,
                 segment);
            closed("connection reset");
        }

    SYN(segment: TcpSegment)
        CLOSED
        {
            send(TcpSegment.RST,
                 null,
                 0,
                 0,
                 segment);
            closed("connection reset");
        }

    PSH(segment: TcpSegment)
        CLOSED         
        {
            send(TcpSegment.RST,
                 null,
                 0,
                 0,
                 segment);
            closed("connection reset");
        }

    ACK(segment: TcpSegment)
        CLOSED
        {
            send(TcpSegment.RST,
                 null,
                 0,
                 0,
                 segment);
            closed("connection reset");
        }

    URG(segment: TcpSegment)
        CLOSED
        {
            send(TcpSegment.RST,
                 null,
                 0,
                 0,
                 segment);
            closed("connection reset");
        }

    FIN_ACK(segment: TcpSegment)
        CLOSED
        {
            send(TcpSegment.RST,
                 null,
                 0,
                 0,
                 segment);
            closed("connection reset");
        }

    SYN_ACK(segment: TcpSegment)
        CLOSED
        {
            send(TcpSegment.RST,
                 null,
                 0,
                 0,
                 segment);
            closed("connection reset");
        }

    PSH_ACK(segment: TcpSegment)
        CLOSED
        {
            send(TcpSegment.RST,
                 null,
                 0,
                 0,
                 segment);
            closed("connection reset");}

    UNDEF(segment: TcpSegment)
        nil
        {
            send(TcpSegment.RST,
                 null,
                 0,
                 0,
                 segment);
            closed("connection reset");
        }

    // Ignore timeouts which occur when not expected.
    ConnAckTimeout
        nil
        {}

    TransAckTimeout
        nil
        {}

    CloseAckTimeout
        nil
        {}

    CloseTimeout
        nil
        {}
}
%%