-static void MC_modelcheck_safety_init(void)
-{
- _sg_mc_safety = 1;
-
- MC_init();
-
- xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
-
- /* Create exploration stack */
- mc_stack = xbt_fifo_new();
-
- MC_SET_STD_HEAP;
-
- MC_pre_modelcheck_safety();
-
- MC_SET_MC_HEAP;
- /* Save the initial state */
- initial_global_state = xbt_new0(s_mc_global_t, 1);
- initial_global_state->snapshot = MC_take_snapshot(0);
- MC_SET_STD_HEAP;
-
- MC_modelcheck_safety();
-
- mmalloc_set_current_heap(heap);
-
- xbt_abort();
- //MC_exit();
-}
-
-static void MC_modelcheck_liveness_init()
-{
- _sg_mc_liveness = 1;
-
- MC_init();
-
- xbt_mheap_t heap = mmalloc_set_current_heap(mc_heap);
-
- /* Create exploration stack */
- mc_stack = xbt_fifo_new();
-
- /* Create the initial state */
- initial_global_state = xbt_new0(s_mc_global_t, 1);
-
- MC_SET_STD_HEAP;
-
- MC_pre_modelcheck_liveness();
-
- /* We're done */
- MC_print_statistics(mc_stats);
- xbt_free(mc_time);
-
- mmalloc_set_current_heap(heap);
-
-}
-