state->in_visited_states = 0;
state->incomplete_comm_pattern = NULL;
/* Stateful model checking */
- if(_sg_mc_checkpoint > 0 && mc_stats->expanded_states % _sg_mc_checkpoint == 0){
+ if((_sg_mc_checkpoint > 0 && (mc_stats->expanded_states % _sg_mc_checkpoint == 0)) || _sg_mc_termination){
state->system_state = MC_take_snapshot(state->num);
if(_sg_mc_comms_determinism || _sg_mc_send_determinism){
copy_incomplete_communications_pattern(state);
MC_EACH_SIMIX_PROCESS(process,
procstate = &state->proc_status[process->pid];
- if (procstate->state == MC_INTERLEAVE
- || procstate->state == MC_MORE_INTERLEAVE) {
- if (MC_process_is_enabled(process)) {
- switch (process->simcall.call) {
+ if (procstate->state != MC_INTERLEAVE
+ && procstate->state != MC_MORE_INTERLEAVE)
+ continue;
+ if (!MC_process_is_enabled(process))
+ continue;
+
+ switch (process->simcall.call) {
case SIMCALL_COMM_WAITANY:
*value = -1;
while (procstate->interleave_count <
*value = 0;
return &process->simcall;
break;
- }
- }
+
}
);