XBT_DEBUG("**** End Replay ****");
}
-void MC_replay_liveness(xbt_fifo_t stack)
-{
- xbt_fifo_item_t item;
- simgrid::mc::Pair* pair = nullptr;
- mc_state_t state = nullptr;
- smx_simcall_t req = nullptr, saved_req = NULL;
- int value, depth = 1;
- char *req_str;
-
- XBT_DEBUG("**** Begin Replay ****");
-
- /* Intermediate backtracking */
- if(_sg_mc_checkpoint > 0) {
- item = xbt_fifo_get_first_item(stack);
- pair = (simgrid::mc::Pair*) xbt_fifo_get_item_content(item);
- if(pair->graph_state->system_state){
- simgrid::mc::restore_snapshot(pair->graph_state->system_state);
- return;
- }
- }
-
- /* Restore the initial state */
- simgrid::mc::restore_snapshot(initial_global_state->snapshot);
-
- /* Traverse the stack from the initial state and re-execute the transitions */
- for (item = xbt_fifo_get_last_item(stack);
- item != xbt_fifo_get_first_item(stack);
- item = xbt_fifo_get_prev_item(item)) {
-
- pair = (simgrid::mc::Pair*) xbt_fifo_get_item_content(item);
-
- state = (mc_state_t) pair->graph_state;
-
- if (pair->exploration_started) {
-
- saved_req = MC_state_get_executed_request(state, &value);
-
- if (saved_req != nullptr) {
- /* because we got a copy of the executed request, we have to fetch the
- real one, pointed by the request field of the issuer process */
- const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req);
- req = &issuer->simcall;
-
- /* Debug information */
- if (XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)) {
- req_str = simgrid::mc::request_to_string(req, value, simgrid::mc::RequestType::simix);
- XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state);
- xbt_free(req_str);
- }
-
- }
-
- simgrid::mc::handle_simcall(req, value);
- mc_model_checker->wait_for_requests();
- }
-
- /* Update statistics */
- mc_stats->visited_pairs++;
- mc_stats->executed_transitions++;
-
- depth++;
-
- }
-
- XBT_DEBUG("**** End Replay ****");
-}
-
/**
* \brief Dumps the contents of a model-checker's stack and shows the actual
* execution trace
