class interface ES_STANDALONE_MULTIPLEXER_POLL
   -- 
   --  An application multiplexer for standalone applications, e.g. console
   --  programs or daemon servers. It uses the SV Unix poll method.
   -- 

feature(s) from ES_MULTIPLEXER
   --  Public Accessors

   count: INTEGER
      --  The number of controlled devices

feature(s) from ES_IMPORTED_EXTERNALS
   --  Once

   externals_: ES_EXTERNALS
      --  Access those compatability commands.

feature(s) from KL_SHARED_EXCEPTIONS
   --  Access

   exceptions: KL_EXCEPTIONS
      --  Exception handling
      ensure
         exceptions_not_void: Result /= Void

feature(s) from ES_STANDALONE_MULTIPLEXER_POLL
   --  Run Multiplexer

   number_of_active_elements: INTEGER
      --  Number of elements set for possible dispatch
      ensure
         sanity: Result >= 0 and Result <= count + timeout_queue.count

   do_one_cycle
      --  Dispatch one set of messages.
      require
         active_elements: number_of_active_elements > 0

   cycle
      --  Repeatedly cycle as long as active elements remain.
      require
         some_active: number_of_active_elements > 0
      ensure
         none_active: number_of_active_elements = 0 or halted

   halted: BOOLEAN
      --  Has the cycle been commanded to halt?

   halt
      --  Halts the cycle after then next pass.
      ensure
         halted: halted

invariant

    non_negative: count >= 0;

    has_time_queue: timeout_queue /= Void;

    non_negative_time: current_time >= 0;

    has_devices: devices /= Void;

    positive_capacity: poll_array_capacity > 0;

end of ES_STANDALONE_MULTIPLEXER_POLL