+ MC_SET_RAW_MEM;
+
+ initial_system_snapshot = xbt_new0(s_mc_snapshot_t, 1);
+
+ initial_graph_state = MC_state_new();
+ xbt_swag_foreach(process, simix_global->process_list){
+ if(MC_process_is_enabled(process)){
+ MC_state_interleave_process(initial_graph_state, process);
+ break;
+ }
+ }
+
+ MC_take_snapshot(initial_system_snapshot);
+
+ initial_state = new_state_ws(initial_system_snapshot, initial_graph_state);
+ xbt_fifo_unshift(mc_stack_safety_stateful, initial_state);
+
+ MC_UNSET_RAW_MEM;
+
+}
+
+void MC_dpor_stateful(){
+
+ smx_process_t process = NULL;
+
+ if(xbt_fifo_size(mc_stack_safety_stateful) == 0)
+ return;
+
+ int value;
+ mc_state_t next_graph_state = NULL;
+ smx_simcall_t req = NULL, prev_req = NULL;
+ char *req_str;
+ xbt_fifo_item_t item = NULL;
+
+ mc_snapshot_t next_snapshot;
+ mc_state_ws_t current_state;
+ mc_state_ws_t prev_state;
+ mc_state_ws_t next_state;
+
+ while(xbt_fifo_size(mc_stack_safety_stateful) > 0){
+
+ current_state = (mc_state_ws_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_safety_stateful));
+
+
+ XBT_DEBUG("**************************************************");
+ XBT_DEBUG("Depth : %d, State : %p , %u interleave", xbt_fifo_size(mc_stack_safety_stateful),current_state, MC_state_interleave_size(current_state->graph_state));
+
+ mc_stats->visited_states++;
+ if(mc_stats->expanded_states>1100)
+ exit(0);
+ //sleep(1);
+
+ if((xbt_fifo_size(mc_stack_safety_stateful) < MAX_DEPTH) && (req = MC_state_get_request(current_state->graph_state, &value))){
+
+ /* Debug information */
+ if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
+ req_str = MC_request_to_string(req, value);
+ //XBT_INFO("Visited states = %lu",mc_stats->visited_states );
+ XBT_DEBUG("Execute: %s",req_str);
+ xbt_free(req_str);