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;
+xbt_automaton_t automaton;
+char *prog_name;
/**
* \brief Initialize the model-checker data structures
MC_UNSET_RAW_MEM;
- MC_ddfs_stateless_init(a, prgm);
+ automaton = a;
+ prog_name = strdup(prgm);
+
+ MC_ddfs_stateless_init();
}
{
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;