- while ((state = xbt_fifo_shift(mc_stack_safety_stateless)) != NULL) {
- req = MC_state_get_internal_request(state);
- xbt_fifo_foreach(mc_stack_safety_stateless, item, prev_state, mc_state_t) {
- if(MC_request_depend(req, MC_state_get_internal_request(prev_state))){
- if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
- XBT_DEBUG("Dependent Transitions:");
- prev_req = MC_state_get_executed_request(prev_state, &value);
- req_str = MC_request_to_string(prev_req, value);
- XBT_DEBUG("%s (state=%p)", req_str, prev_state);
- xbt_free(req_str);
- prev_req = MC_state_get_executed_request(state, &value);
- req_str = MC_request_to_string(prev_req, value);
- XBT_DEBUG("%s (state=%p)", req_str, state);
- xbt_free(req_str);
- }
-
- if(!MC_state_process_is_done(prev_state, req->issuer))
- MC_state_interleave_process(prev_state, req->issuer);
- else
- XBT_DEBUG("Process %p is in done set", req->issuer);
-
- break;
- }
- }
- if (MC_state_interleave_size(state)) {
- /* We found a back-tracking point, let's loop */
- xbt_fifo_unshift(mc_stack_safety_stateless, state);
- XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety_stateless));
- MC_UNSET_RAW_MEM;
- MC_replay(mc_stack_safety_stateless);
- break;
- } else {
- MC_state_delete(state);
- }
- }
- MC_UNSET_RAW_MEM;
- }
- }
- MC_UNSET_RAW_MEM;
- return;
-}
-
-
-/********************* DPOR stateful *********************/
-
-mc_state_ws_t new_state_ws(mc_snapshot_t s, mc_state_t gs){
- mc_state_ws_t sws = NULL;
- sws = xbt_new0(s_mc_state_ws_t, 1);
- sws->system_state = s;
- sws->graph_state = gs;
- return sws;
-}
-
-void MC_dpor_stateful_init(){
-
- XBT_DEBUG("**************************************************");
- XBT_DEBUG("DPOR (stateful) init");
- XBT_DEBUG("**************************************************");
-
- mc_state_t initial_graph_state;
- smx_process_t process;
- mc_snapshot_t initial_system_snapshot;
- mc_state_ws_t initial_state ;
-
- MC_wait_for_requests();
-
- 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;
-
-}