deferred class interface ES_MULTIPLEXED_DEVICE
   -- 
   --  Common abstraction of things dispatched by an ES_MULTIPLEXER.
   -- 

feature(s) from ES_MULTIPLEXER_SINGLETON
   --  The Multiplexer

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

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 resources of this device.
      require
         now_open: open
      ensure
         not_in_multiplexer: not in_multiplexer;
         closed: closed

invariant

    in_multiplexer: in_multiplexer implies open;

    closed_is_not_open: closed = not open;

end of deferred ES_MULTIPLEXED_DEVICE