class interface SYNCH_NOTIFIER feature(s) from SYNCH_NOTIFIER -- Options set_latency (nlat_ms: INTEGER) -- Change maximum duration of a single wait operation. -- Default: infinite require ok: nlat_ms >= 0 ensure done: latency = nlat_ms feature(s) from SYNCH_NOTIFIER -- Wait has_events: BOOLEAN -- Is there at least one event to wait for? wait_once -- Wait for one event. require has_events: has_events wait -- Process all outstanding events. end of SYNCH_NOTIFIER