xbt_fifo_t mc_stack_liveness_stateful = NULL;
mc_stats_pair_t mc_stats_pair = NULL;
xbt_fifo_t mc_stack_liveness_stateless = NULL;
+mc_snapshot_t initial_snapshot_liveness = NULL;
/**
MC_UNSET_RAW_MEM;
- MC_ddfs_stateful_init(a);
+ //MC_ddfs_stateful_init(a);
//MC_dpor2_init(a);
//MC_dpor3_init(a);
}
-void MC_init_liveness_stateless(xbt_automaton_t a){
+void MC_init_liveness_stateless(xbt_automaton_t a, char *prgm){
XBT_DEBUG("Start init mc");
MC_UNSET_RAW_MEM;
- MC_ddfs_stateless_init(a);
+ MC_ddfs_stateless_init(a, prgm);
}
MC_exit_liveness();
}
-void MC_modelcheck_liveness_stateless(xbt_automaton_t a){
- MC_init_liveness_stateless(a);
+void MC_modelcheck_liveness_stateless(xbt_automaton_t a, char *prgm){
+ MC_init_liveness_stateless(a, prgm);
MC_exit_liveness();
}
{
MC_print_statistics_pairs(mc_stats_pair);
//xbt_free(mc_time);
- MC_memory_exit();
+ //MC_memory_exit();
+ exit(0);
}
smx_req_t req;
unsigned int iter;
- while (xbt_dynar_length(simix_global->process_to_run)) {
+ while (!xbt_dynar_is_empty(simix_global->process_to_run)) {
SIMIX_process_runall();
xbt_dynar_foreach(simix_global->process_that_ran, iter, process) {
req = &process->request;
XBT_DEBUG("**** Begin Replay ****");
/* Restore the initial state */
- MC_restore_snapshot(initial_snapshot);
+ MC_restore_snapshot(initial_snapshot_liveness);
/* At the moment of taking the snapshot the raw heap was set, so restoring
* it will set it back again, we have to unset it to continue */
MC_UNSET_RAW_MEM;