4 void worker_started
();
5 // A worker has started
7 void worker_finished
();
8 // A worker has finished
12 void start_workers
(in short worker_count
,
14 in Controller the_controller
);
15 // Start <worker_count> workers, each one runs for the pescribed
16 // number of milliseconds, and report progress to <the_controller>
18 oneway
void shutdown
();
19 // Shutdown the Manager's ORB, just for cleanup purposes