- mc_procstate_t procstate = &state->proc_status[process->pid];
-
- if (procstate->state != MC_INTERLEAVE
- && procstate->state != MC_MORE_INTERLEAVE)
- return NULL;
- if (!MC_process_is_enabled(process))
- return NULL;
-
- switch (process->simcall.call) {
-
- case SIMCALL_COMM_WAITANY:
- *value = -1;
- while (procstate->interleave_count <
- MC_process_read_dynar_length(&mc_model_checker->process(),
- simcall_comm_waitany__get__comms(&process->simcall))) {
- if (MC_request_is_enabled_by_idx
- (&process->simcall, procstate->interleave_count++)) {
- *value = procstate->interleave_count - 1;
- break;
- }
- }
-
- if (procstate->interleave_count >=
- MC_process_read_dynar_length(&mc_model_checker->process(),
- simcall_comm_waitany__get__comms(&process->simcall)))
- procstate->state = MC_DONE;
-
- if (*value != -1)
- return &process->simcall;
-
- break;
-
- case SIMCALL_COMM_TESTANY: {
- unsigned start_count = procstate->interleave_count;
- *value = -1;
- while (procstate->interleave_count <
- MC_process_read_dynar_length(&mc_model_checker->process(),
- simcall_comm_testany__get__comms(&process->simcall))) {
- if (MC_request_is_enabled_by_idx
- (&process->simcall, procstate->interleave_count++)) {
- *value = procstate->interleave_count - 1;
- break;
- }
- }
-
- if (procstate->interleave_count >=
- MC_process_read_dynar_length(&mc_model_checker->process(),
- simcall_comm_testany__get__comms(&process->simcall)))
- procstate->state = MC_DONE;