-void MC_init_liveness_stateful(xbt_automaton_t a){
-
- XBT_DEBUG("Start init mc");
-
- 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;
-
- /* Initialize statistics */
- mc_stats_pair = xbt_new0(s_mc_stats_pair_t, 1);
- //mc_stats = xbt_new0(s_mc_stats_t, 1);
-
- XBT_DEBUG("Creating snapshot_stack");
-
- /* Create exploration stack */
- mc_stack_liveness_stateful = xbt_fifo_new();
-
-
- MC_UNSET_RAW_MEM;
-
- //MC_ddfs_stateful_init(a);
- //MC_dpor2_init(a);
- //MC_dpor3_init(a);
-}
-
-void MC_init_liveness_stateless(xbt_automaton_t a, char *prgm){