module SCTP_Types{

  external function f_SCTP_enc(in SCTP_Packet pl_pdu) return octetstring
  with {
    extension "prototype(convert)"
  }
  external function f_SCTP_dec(in octetstring pl_stream, out SCTP_Packet pl_pdu) return integer
  with {
    extension "prototype(backtrack)"
  }

:
:
  type record SCTP_Packet{
    SCTP_Common_header    common_header,
    SCTP_Chunk_List       chunks
  } with {
    variant ""
  }
  
  type record of SCTP_Chunk SCTP_Chunk_List;
  
  type union SCTP_Chunk{
    SCTP_Data_chunk      data,
    SCTP_Init_chunk      init,
    SCTP_InitAck_chunk   init_ack,
    SCTP_SAck_chunk      sack,
    SCTP_Heartbeat_chunk heartbeat,
    SCTP_Heartbeat_ack_chunk heartbeat_ack,
    SCTP_abort_chunk     abort,
    SCTP_Shutdown_chunk  shutdown,
    SCTP_Shutdown_ack_chunk shutdown_ack,
    SCTP_error_chunk     error_,
    SCTP_CookieEcho_chunk cookie_echo,
    SCTP_Cookie_ack_chunk cookie_ack,
    SCTP_ShutdownComplete_chunk shutdown_complete,
    SCTP_Auth_chunk      auth,
    SCTP_IData_chunk     idata,
    SCTP_ASCONF_ack_chunk asconf_ack,
    SCTP_Re_Config_chunk re_config,
    SCTP_Padding_chunk   padding,
    SCTP_Forward_TSN_chunk forward_tsn,
    SCTP_ASCONF_chunk    asconf,
    SCTP_IForward_TSN_chunk iforward_tsn,
    SCTP_Unknown_chunk   unknown_chunk
  } with {
    variant "PADDING(dword32)"
    variant "TAG( data, chunk_type = 0;
                  init, chunk_type = 1;
                  init_ack, chunk_type = 2;
                  sack, chunk_type = 3;
                  heartbeat, chunk_type = 4;
                  heartbeat_ack, chunk_type = 5;
                  abort, chunk_type = 6;
                  shutdown, chunk_type = 7;
                  shutdown_ack, chunk_type = 8;
                  error_, chunk_type = 9;
                  cookie_echo, chunk_type = 10;
                  cookie_ack, chunk_type = 11;
                  shutdown_complete, chunk_type = 14;
                  auth, chunk_type = 15;
                  idata, chunk_type = 64;
                  asconf_ack, chunk_type = 128;
                  re_config, chunk_type = 130;
                  padding, chunk_type = 132;
                  forward_tsn, chunk_type = 192;
                  asconf, chunk_type = 193;
                  iforward_tsn, chunk_type = 194;
                  unknown_chunk, OTHERWISE;
                )"
  }
  
:
:
:

module SCTP_Engine_PortTypes {


// Upper side test port. Provides the SCTP API

// Signature definitions of the procedure calls
// Client -> SCTP Engine component

// If the requested operation was executed successfully all
// procedures returns SCTP_Engine_result
// If something went wrong an exception will be raised.

// The assoc-id of the listen port is returned.
// A separate assoc_id will be created for the accepted connections
signature S_SCTP_Listen(in SCTP_Listen_data pl_arg) 
          return SCTP_Engine_result
          exception (SCTP_operation_exception)

signature S_SCTP_Connect(in SCTP_Connect_data pl_arg) 
          return SCTP_Engine_result
          exception (SCTP_operation_exception)


// The shutdown procedure and the release of the assoc_id shoud be done as:
//
//  User initiated shutdown is a 3 step procedure:
//     call    S_SCTP_Shutdown
//     receive S_SCTP_Shutdown_ind
//     call    S_SCTP_Shutdown_conf
//
//  Remote side initiated shutdown
//     receive S_SCTP_Shutdown_ind
//     call    S_SCTP_Shutdown_conf
//
// The assoc_id is released only after the call of the S_SCTP_Shutdown_conf

signature S_SCTP_Shutdown(in SCTP_Shutdown_data pl_arg) 
          return SCTP_Engine_result
          exception (SCTP_operation_exception)


signature S_SCTP_Shutdown_conf(in integer assoc_id) 
          return SCTP_Engine_result
          exception (SCTP_operation_exception)


// Request sending of user data

signature S_SCTP_Send_req(in SCTP_MSG_data pl_arg)
          return SCTP_Engine_result
          exception (SCTP_operation_exception)


// Set options
signature S_SCTP_options(in SCTP_Options_data pl_arg)
          return SCTP_Engine_result
          exception (SCTP_operation_exception)

// Reconfiguration request
signature S_SCTP_reconfig(in SCTP_Reconfiguration_req pl_arg)
          return SCTP_Engine_result
          exception (SCTP_operation_exception)


// SCTP engine -> Client

// Shutdown indication
signature S_SCTP_Shutdown_ind(in SCTP_Shutdown_data pl_arg) 

// Connected indication. 
// called by the SCTP engine, when accepting a new client connection
signature S_SCTP_Connected_ind(in SCTP_Connected_data pl_arg) 

// Receive data indication
signature S_SCTP_Received_ind(in SCTP_MSG_data pl_arg) 

// Notification indication
signature S_SCTP_Notification_ind(in SCTP_Notification_data pl_arg) 

:
:
:
// Why procedure based?
// Because the each operation is a request to execute some operation:
// S_SCTP_Listen: means please start to
// listen for an incoming association request
// 
// The result of the operation should be syncronized and paired with the 
// request. The result should be available immediately without delay
//
// The procedure based port are represents a client-server connections
// That is why we need 2 ports.
//  SCTP_Engine_API_request_PT : The SCTP user calls the operation of the 
//                               SCTP engine component
//  SCTP_Engine_API_indication_PT: The SCTP engine notifies the user via this
//
// Using only one test port can mix up the result of the ongoing operation and 
// of the incoming indication calls

// The SCTP API test port
type port SCTP_Engine_API_request_PT procedure {
  inout S_SCTP_Listen, S_SCTP_Connect, S_SCTP_Shutdown,S_SCTP_Shutdown_conf
  inout S_SCTP_Send_req, S_SCTP_options, S_SCTP_reconfig
} with {
  extension "internal"
}

type port SCTP_Engine_API_indication_PT procedure {
  inout S_SCTP_Shutdown_ind, S_SCTP_Connected_ind, S_SCTP_Received_ind
  inout S_SCTP_Notification_ind
} with {
  extension "internal"
}

module SCTP_Engine_PortTypes {

:
:

//******************************************************************************
// Lower side port. Exchanges the encoded SCTP packets

// Used to represent a SCTP packet in encoded form
type record SCTP_Engine_packet {
  integer        transport_id,  // The identifier used to identify the transport connection
                                // The identifier is specified in a Listen/Connect operation
                                // The associations using the same transport id are distinguished by the SCTP port numbers
  octetstring    sctp_packet    // The SCTP packet 
}

type record SCTP_Addr_change_notification{
  integer        transport_id  // The identifier used to identify the transport connection
}

// used only between components
type port SCTP_Engine_packet_PT message {
  inout SCTP_Engine_packet
  inout SCTP_Addr_change_notification
} with {
  extension "internal"
}

:
:

                                   +-----------------------+
                                   |                       |
                                   |     User protocol     |
                                   +-------^--^------------+
+-----------------+ +-------------------+  |  |  +-------------------+
|SCTP             | |SCTP               |  |  |  |                   |
|protocol         +->protocol           |  |  |  |   SCTP test port  |
|module           | |emulation          <--+  +-->                   |
+-----------------+ +-------+-----------+        +--------^----------+
                            |                             |    kernel stack
                            |                    +--------v----------+
                            |                    |                   |
                            |                    |     SCTP          |
                            |                    +-------------------+
                            |                    |                   |
                            +-------------------->       IP          |
                                                 |                   |
                                                 +-------------------+
                                                 |     ...           |
                                                 |                   |
                                                 +-------------------+