-}
-
-smx_simcall_t MC_state_get_executed_request(simgrid::mc::State* state, int *value)
-{
- *value = state->req_num;
- return &state->executed_req;
-}
-
-smx_simcall_t MC_state_get_internal_request(simgrid::mc::State* state)
-{
- return &state->internal_req;
-}
-
-static inline smx_simcall_t MC_state_get_request_for_process(
- simgrid::mc::State* state, int*value, smx_process_t process)
-{
- simgrid::mc::ProcessState* procstate = &state->processStates[process->pid];
-
- if (!procstate->interleave())
- return nullptr;
- if (!simgrid::mc::process_is_enabled(process))
- return nullptr;
-
- switch (process->simcall.call) {
-
- case SIMCALL_COMM_WAITANY:
- *value = -1;
- while (procstate->interleave_count <
- read_length(mc_model_checker->process(),
- remote(simcall_comm_waitany__get__comms(&process->simcall)))) {
- if (simgrid::mc::request_is_enabled_by_idx(&process->simcall,
- procstate->interleave_count++)) {
- *value = procstate->interleave_count - 1;
- break;
- }
- }
-
- if (procstate->interleave_count >=
- simgrid::mc::read_length(mc_model_checker->process(),
- simgrid::mc::remote(simcall_comm_waitany__get__comms(&process->simcall))))
- procstate->state = simgrid::mc::ProcessInterleaveState::done;
-
- if (*value != -1)
- return &process->simcall;
-
- break;
-
- case SIMCALL_COMM_TESTANY: {
- unsigned start_count = procstate->interleave_count;
- *value = -1;
- while (procstate->interleave_count <
- read_length(mc_model_checker->process(),
- remote(simcall_comm_testany__get__comms(&process->simcall))))
- if (simgrid::mc::request_is_enabled_by_idx(&process->simcall,
- procstate->interleave_count++)) {
- *value = procstate->interleave_count - 1;
- break;
- }
-
- if (procstate->interleave_count >=
- read_length(mc_model_checker->process(),
- remote(simcall_comm_testany__get__comms(&process->simcall))))
- procstate->state = simgrid::mc::ProcessInterleaveState::done;