tcpconnection.sm

来自「SMC takes a state machine stored in a .s」· SM 代码 · 共 924 行 · 第 1/2 页

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

FIN_WAIT_1
Entry
{
    startTimer("CLOSE_ACK_TIMER", TcpConnection::ACK_TIMEOUT);
}
Exit
{
    stopTimer("CLOSE_ACK_TIMER");
}
{
    ACK(segment: const TcpSegment&)
      [segment.getSrcAddress() == ctxt.getFarAddress() &&
       segment.getSrcPort() == ctxt.getFarPort() &&
       segment.getAcknowledgeNumber() == ctxt.getSequenceNumber()]
        FIN_WAIT_2
        {
            deleteSegment(segment);
        }

    FIN(segment: const TcpSegment&)
      [segment.getSrcAddress() == ctxt.getFarAddress() &&
       segment.getSrcPort() == ctxt.getFarPort()]
        CLOSING
        {
            doSend(TcpSegment::ACK,
                   NULL,
                   0,
                   0,
                   &segment);
            deleteSegment(segment);
        }

    FIN_ACK(segment: const TcpSegment&)
      [segment.getSrcAddress() == ctxt.getFarAddress() &&
       segment.getSrcPort() == ctxt.getFarPort() &&
       segment.getAcknowledgeNumber() == ctxt.getSequenceNumber()]
        TIME_WAIT
        {
            doSend(TcpSegment::ACK,
                   NULL,
                   0,
                   0,
                   &segment);
            deleteSegment(segment);
        }

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

FIN_WAIT_2
Entry
{
    startTimer("CLOSE_ACK_TIMER", TcpConnection::ACK_TIMEOUT);
}
Exit
{
    stopTimer("CLOSE_ACK_TIMER");
}
{
    FIN(segment: const TcpSegment&)
      [segment.getSrcAddress() == ctxt.getFarAddress() &&
       segment.getSrcPort() == ctxt.getFarPort()]
        TIME_WAIT
        {
            doSend(TcpSegment::ACK,
                   NULL,
                   0,
                   0,
                   &segment);
            deleteSegment(segment);
        }

    CloseAckTimeout
        CLOSED
        {
            closeSocket();
        }

    // Ignore undefined transitions.
    UNDEF(segment: const TcpSegment&)
		nil
        {
            deleteSegment(segment);
        }
}

CLOSING
Entry
{
    startTimer("CLOSE_ACK_TIMER", TcpConnection::ACK_TIMEOUT);
}
Exit
{
    stopTimer("CLOSE_ACK_TIMER");
}
{
    ACK(segment: const TcpSegment&)
      [segment.getSrcAddress() == ctxt.getFarAddress() &&
       segment.getSrcPort() == ctxt.getFarPort() &&
       segment.getAcknowledgeNumber() == ctxt.getSequenceNumber()]
        TIME_WAIT
        {
            deleteSegment(segment);
        }

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

    // Ignore undefined transitions.
    UNDEF(segment: const TcpSegment&)
		nil
        {
            deleteSegment(segment);
        }
}

TIME_WAIT
Entry
{
    startTimer("CLOSE_TIMER", TcpConnection::CLOSE_TIMEOUT);
}
Exit
{
    stopTimer("CLOSE_TIMER");
}
{
    FIN_ACK(segment: const TcpSegment&)
      [segment.getSrcAddress() == ctxt.getFarAddress() &&
       segment.getSrcPort() == ctxt.getFarPort() &&
       segment.getAcknowledgeNumber() == ctxt.getSequenceNumber()]
        CLOSED
        {
            closeSocket();
            deleteSegment(segment);
        }

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

    // Ignore undefined transitions.
    UNDEF(segment: const TcpSegment&)
		nil
        {
            deleteSegment(segment);
        }
}

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

    ActiveOpen(address: const sockaddr_in*)
        nil
        {
            openFailed("already open");
        }

    Transmit(data: const char*, 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: const TcpSegment&)
      [segment.getSrcAddress() != ctxt.getFarAddress() ||
       segment.getSrcPort() != ctxt.getFarPort()]
        nil
        {
            doSend(TcpSegment::RST,
                   NULL,
                   0,
                   0,
                   &segment);
            closed("connection reset");
            deleteSegment(segment);
        }

    SYN(segment: const TcpSegment&)
      [segment.getSrcAddress() != ctxt.getFarAddress() ||
       segment.getSrcPort() != ctxt.getFarPort()]
        nil
        {
            doSend(TcpSegment::RST,
                   NULL,
                   0,
                   0,
                   &segment);
            closed("connection reset");
            deleteSegment(segment);
        }

    PSH(segment: const TcpSegment&)
      [segment.getSrcAddress() != ctxt.getFarAddress() ||
       segment.getSrcPort() != ctxt.getFarPort()]
        nil
        {
            doSend(TcpSegment::RST,
                   NULL,
                   0,
                   0,
                   &segment);
            closed("connection reset");
            deleteSegment(segment);
        }

    ACK(segment: const TcpSegment&)
      [segment.getSrcAddress() != ctxt.getFarAddress() ||
       segment.getSrcPort() != ctxt.getFarPort()]
        nil
        {
            doSend(TcpSegment::RST,
                   NULL,
                   0,
                   0,
                   &segment);
            closed("connection reset");
            deleteSegment(segment);
        }

    URG(segment: const TcpSegment&)
      [segment.getSrcAddress() != ctxt.getFarAddress() ||
       segment.getSrcPort() != ctxt.getFarPort()]
        nil
        {
            doSend(TcpSegment::RST,
                   NULL,
                   0,
                   0,
                   &segment);
            closed("connection reset");
            deleteSegment(segment);
        }

    FIN_ACK(segment: const TcpSegment&)
      [segment.getSrcAddress() != ctxt.getFarAddress() ||
       segment.getSrcPort() != ctxt.getFarPort()]
        nil
        {
            doSend(TcpSegment::RST,
                   NULL,
                   0,
                   0,
                   &segment);
            closed("connection reset");
            deleteSegment(segment);
        }

    SYN_ACK(segment: const TcpSegment&)
      [segment.getSrcAddress() != ctxt.getFarAddress() ||
       segment.getSrcPort() != ctxt.getFarPort()]
        nil
        {
            doSend(TcpSegment::RST,
                   NULL,
                   0,
                   0,
                   &segment);
            closed("connection reset");
            deleteSegment(segment);
        }

    PSH_ACK(segment: const TcpSegment&)
      [segment.getSrcAddress() != ctxt.getFarAddress() ||
       segment.getSrcPort() != ctxt.getFarPort()]
        nil
        {
            doSend(TcpSegment::RST,
                   NULL,
                   0,
                   0,
                   &segment);
            closed("connection reset");
            deleteSegment(segment);
        }

    UNDEF(segment: const TcpSegment&)
      [segment.getSrcAddress() != ctxt.getFarAddress() ||
       segment.getSrcPort() != ctxt.getFarPort()]
        nil
        {
            doSend(TcpSegment::RST,
                   NULL,
                   0,
                   0,
                   &segment);
            closed("connection reset");
            deleteSegment(segment);
        }

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

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

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

    SYN(segment: const TcpSegment&)
        CLOSED
        {
            doSend(TcpSegment::RST,
                   NULL,
                   0,
                   0,
                   &segment);
            closed("connection reset");
            deleteSegment(segment);
        }

    PSH(segment: const TcpSegment&)
        CLOSED
        {
            doSend(TcpSegment::RST,
                   NULL,
                   0,
                   0,
                   &segment);
            closed("connection reset");
            deleteSegment(segment);
        }

    ACK(segment: const TcpSegment&)
        CLOSED
        {
            doSend(TcpSegment::RST,
                   NULL,
                   0,
                   0,
                   &segment);
            closed("connection reset");
            deleteSegment(segment);
        }

    URG(segment: const TcpSegment&)
        CLOSED
        {
            doSend(TcpSegment::RST,
                   NULL,
                   0,
                   0,
                   &segment);
            closed("connection reset");
            deleteSegment(segment);
        }

    FIN_ACK(segment: const TcpSegment&)
        CLOSED
        {
            doSend(TcpSegment::RST,
                   NULL,
                   0,
                   0,
                   &segment);
            closed("connection reset");
            deleteSegment(segment);
        }

    SYN_ACK(segment: const TcpSegment&)
        CLOSED
        {
            doSend(TcpSegment::RST,
                   NULL,
                   0,
                   0,
                   &segment);
            closed("connection reset");
            deleteSegment(segment);
        }

    PSH_ACK(segment: const TcpSegment&)
        CLOSED
        {
            doSend(TcpSegment::RST,
                   NULL,
                   0,
                   0,
                   &segment);
            closed("connection reset");
            deleteSegment(segment);
        }

    UNDEF(segment: const TcpSegment&)
        nil
        {
            doSend(TcpSegment::RST,
                   NULL,
                   0,
                   0,
                   &segment);
            closed("connection reset");
            deleteSegment(segment);
        }

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

    TransAckTimeout
        nil
        {}

    CloseAckTimeout
        nil
        {}

    CloseTimeout
        nil
        {}
}

%%