XBT_PUBLIC(void) MC_assert(int);
XBT_PUBLIC(void) MC_modelcheck(void);
XBT_PUBLIC(int) MC_random(int, int);
+XBT_PUBLIC(void) MC_process_clock_add(smx_process_t, double);
+XBT_PUBLIC(double) MC_process_clock_get(smx_process_t);
/********************************* Memory *************************************/
XBT_PUBLIC(void) MC_memory_init(void); /* Initialize the memory subsystem */
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();
}
}
}
+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;
+}
void MC_free_snapshot(mc_snapshot_t);
/********************************* MC Global **********************************/
+extern double *mc_time;
/* Bound of the MC depth-first search algorithm */
#define MAX_DEPTH 1000
#include "xbt/log.h"
#include "xbt/str.h"
#include "xbt/ex.h" /* ex_backtrace_display */
+#include "mc/mc.h"
XBT_LOG_EXTERNAL_CATEGORY(simix);
XBT_LOG_EXTERNAL_CATEGORY(simix_action);
*/
XBT_INLINE double SIMIX_get_clock(void)
{
- return surf_get_clock();
+ if(MC_IS_ENABLED){
+ return MC_process_clock_get(SIMIX_process_self());
+ }else{
+ return surf_get_clock();
+ }
}
void SIMIX_run(void)
"Logging specific to SIMIX (process)");
unsigned long simix_process_maxpid = 0;
-/* FIXME: Ugly hack!*/
-extern double NOW;
/**
* \brief Returns the current agent.
void SIMIX_pre_process_sleep(smx_req_t req)
{
if (MC_IS_ENABLED) {
- NOW += req->process_sleep.duration;
+ MC_process_clock_add(req->issuer, req->process_sleep.duration);
req->process_sleep.result = SIMIX_DONE;
SIMIX_request_answer(req);
return;