44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
|
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
|
-
-
+
+
+
+
+
|
ping_server -> exit [label=alive];
ping_server -> remove_server_record [label=dead];
remove_server_record -> set_available;
set_available -> avail_delay [label="delay 3s"];
avail_delay -> "first_in_queue?";
"first_in_queue?" -> set_running [label=yes];
set_running -> handle_requests;
"first_in_queue?" -> "server_running?" [label=no];
set_running -> get_next_port -> handle_requests;
"first_in_queue?" -> "dead_entry_in_queue?" [label=no];
"dead_entry_in_queue?" -> "server_running?" [label=no];
"dead_entry_in_queue?" -> "remove_dead_entries" [label=yes];
remove_dead_entries -> "server_running?";
handle_requests -> start_shutdown [label="no traffic"];
handle_requests -> shutdown_request;
start_shutdown -> shutdown_delay;
shutdown_request -> shutdown_delay;
shutdown_delay -> exit;
|