class interface ES_CONNECT_MECHANISM
   -- 
   --  A mechanism class that works on behalf of a user defined
   --  ES_NON_BLOCKING_CONNECTOR
   -- 

feature(s) from ES_MULTIPLEXED_DEVICE
   --  Accessors

   id: INTEGER
      --  Unique integer that identifies this device

   open: BOOLEAN
      --  Is the underlying I/O device open?

   closed: BOOLEAN
      --  Is the underlying I/O device closed?

   in_multiplexer: BOOLEAN
      --  Is this object in the multiplexer?
      ensure
         definition: Result = multiplexer.has(Current)

feature(s) from ES_MULTIPLEXED_DEVICE
   --  Multiplexer State Control

   put_in_multiplexer
      --  Put Current into the multiplexer.
      require
         not_yet_in_multiplexer: not in_multiplexer
      ensure
         in_multiplexer: in_multiplexer

   remove_from_multiplexer
      --  Remove Current from the multiplexer.
      require
         in_multiplexer: in_multiplexer
      ensure
         not_in_multiplexer: not in_multiplexer

feature(s) from ES_MULTIPLEXED_DEVICE
   --  Cleanup

   clean_up
      --  Clean up the connection
      require
         now_open: open
      ensure
         not_in_multiplexer: not in_multiplexer;
         closed: closed

feature(s) from ES_MULTIPLEXER_SINGLETON
   --  The Multiplexer

   multiplexer: ES_STANDALONE_MULTIPLEXER_POLL
      --  The Multiplexer
      ensure
         not_void: Result /= Void

feature(s) from ES_TIMEOUT_HANDLER
   --  Manage Timeouts

   timeout_set: BOOLEAN
      --  Is a timout set?

   time_left: INTEGER
      --  How much time left on clock?
      require
         timeout_set
      ensure
         non_negative: Result > 0

   set_timeout (seconds: INTEGER)
      --  Set for a timeout callback after aprox. seconds.
      require
         not_currently_set: not timeout_set;
         non_negative: seconds >= 0
      ensure
         now_set: timeout_set;
         time_left_proper: time_left <= seconds

   stop_timeout
      --  Stop the countdown.
      require
         currently_set: timeout_set
      ensure
         not_set: not timeout_set

feature(s) from ES_CONNECT_MECHANISM
   --  Accessors

   pending: BOOLEAN
      --  Is this connection pending?

invariant

    in_multiplexer: in_multiplexer implies open;

    closed_is_not_open: closed = not open;

    manager_present: manager_rep /= Void;

    socket_present: managed_socket /= Void;

end of ES_CONNECT_MECHANISM