mc_stats_t mc_stats = NULL;
mc_state_t mc_current_state = NULL;
char mc_replay_mode = FALSE;
-
+double *mc_time = NULL;
/**
* \brief Initialize the model-checker data structures
*/
if (initial_snapshot)
return;
+ mc_time = xbt_new0(double, simix_process_maxpid);
+
/* Initialize the data structures that must be persistent across every
iteration of the model-checker (in RAW memory) */
MC_SET_RAW_MEM;
void MC_exit(void)
{
+ xbt_free(mc_time);
MC_memory_exit();
}
: (NULL)); item = xbt_fifo_get_prev_item(item)) {
req = MC_state_get_executed_request(state, &value);
if(req){
- req_str = MC_request_to_string(req);
- INFO1("%s", req_str);
- xbt_free(req_str);
+ if(req->call == REQ_COMM_WAIT && value == -1)
+ INFO3("[(%lu)%s] Wait Timeout (comm=%p)",
+ req->issuer->pid, req->issuer->name, req->comm_wait.comm);
+ else{
+ req_str = MC_request_to_string(req);
+ INFO1("%s", req_str);
+ xbt_free(req_str);
+ }
}
}
}
}
}
+void MC_process_clock_add(smx_process_t process, double amount)
+{
+ mc_time[process->pid] += amount;
+}
+
+double MC_process_clock_get(smx_process_t process)
+{
+ if(mc_time)
+ return mc_time[process->pid];
+ else
+ return 0;
+}