1: <Initial predicate>
/\ server_req = NULL
/\ server_resp = NULL
/\ server_log = {}
/\ ws = "init"
2: <WorkerNext line 50, col 5 to line 52, col 27 of module system>
/\ server_req = NULL
/\ server_resp = NULL
/\ server_log = {}
/\ ws = "ready"
3: <WorkerNext line 50, col 5 to line 52, col 27 of module system>
/\ server_req = "c"
/\ server_resp = NULL
/\ server_log = {}
/\ ws = "requesting"
4: <ServerNext line 46, col 5 to line 47, col 19 of module system>
/\ server_req = NULL
/\ server_resp = "invalid"
/\ server_log = {"c"}
/\ ws = "requesting"
5: <WorkerNext line 50, col 5 to line 52, col 27 of module system>
/\ server_req = NULL
/\ server_resp = "invalid"
/\ server_log = {"c"}
/\ ws = "error"
6: <WorkerNext line 50, col 5 to line 52, col 27 of module system>
/\ server_req = NULL
/\ server_resp = "invalid"
/\ server_log = {"c"}
/\ ws = "ready"
7: <WorkerNext line 50, col 5 to line 52, col 27 of module system>
/\ server_req = "b"
/\ server_resp = NULL
/\ server_log = {"c"}
/\ ws = "requesting"
8: <ServerNext line 46, col 5 to line 47, col 19 of module system>
/\ server_req = NULL
/\ server_resp = "invalid"
/\ server_log = {"b", "c"}
/\ ws = "requesting"
9: <WorkerNext line 50, col 5 to line 52, col 27 of module system>
/\ server_req = NULL
/\ server_resp = "invalid"
/\ server_log = {"b", "c"}
/\ ws = "error"
10: <WorkerNext line 50, col 5 to line 52, col 27 of module system>
/\ server_req = NULL
/\ server_resp = "invalid"
/\ server_log = {"b", "c"}
/\ ws = "ready"
11: <WorkerNext line 50, col 5 to line 52, col 27 of module system>
/\ server_req = "b"
/\ server_resp = NULL
/\ server_log = {"b", "c"}
/\ ws = "requesting"