- XBT_DEBUG("**** Begin Replay ****");
-
- /* Intermediate backtracking */
- if(_sg_mc_checkpoint > 0) {
- item = xbt_fifo_get_first_item(stack);
- pair = (mc_pair_t) 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 = (mc_pair_t) 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 = MC_request_to_string(req, value, MC_REQUEST_SIMIX);
- XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, req_str, state);
- xbt_free(req_str);
- }
-
- }
-
- MC_simcall_handle(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
- * \param stack The stack to dump
- */
-void MC_dump_stack_safety(xbt_fifo_t stack)
-{
- MC_show_stack_safety(stack);
-
- mc_state_t state;
-
- while ((state = (mc_state_t) xbt_fifo_pop(stack)) != nullptr)
- MC_state_delete(state, !state->in_visited_states ? 1 : 0);
-}
-
-
-void MC_show_stack_safety(xbt_fifo_t stack)
-{
- int value;
- mc_state_t state;
- xbt_fifo_item_t item;
- smx_simcall_t req;
- char *req_str = nullptr;
-
- for (item = xbt_fifo_get_last_item(stack);
- item; item = xbt_fifo_get_prev_item(item)) {
- state = (mc_state_t)xbt_fifo_get_item_content(item);
- req = MC_state_get_executed_request(state, &value);
- if (req) {
- req_str = MC_request_to_string(req, value, MC_REQUEST_EXECUTED);
- XBT_INFO("%s", req_str);
- xbt_free(req_str);
- }
- }
-}
-
-void MC_show_deadlock(smx_simcall_t req)
-{
- /*char *req_str = nullptr; */
- XBT_INFO("**************************");
- XBT_INFO("*** DEAD-LOCK DETECTED ***");
- XBT_INFO("**************************");
- XBT_INFO("Locked request:");
- /*req_str = MC_request_to_string(req);
- XBT_INFO("%s", req_str);
- xbt_free(req_str); */
- XBT_INFO("Counter-example execution trace:");
- MC_dump_stack_safety(mc_stack);
- MC_print_statistics(mc_stats);
-}
-
-void MC_show_non_termination(void){
- XBT_INFO("******************************************");
- XBT_INFO("*** NON-PROGRESSIVE CYCLE DETECTED ***");
- XBT_INFO("******************************************");
- XBT_INFO("Counter-example execution trace:");
- MC_dump_stack_safety(mc_stack);
- MC_print_statistics(mc_stats);
-}
-
-
-void MC_show_stack_liveness(xbt_fifo_t stack)
-{
- int value;
- mc_pair_t pair;
- xbt_fifo_item_t item;
- smx_simcall_t req;
- char *req_str = nullptr;
-
- for (item = xbt_fifo_get_last_item(stack);
- item; item = xbt_fifo_get_prev_item(item)) {
- pair = (mc_pair_t) xbt_fifo_get_item_content(item);
- req = MC_state_get_executed_request(pair->graph_state, &value);
- if (req && req->call != SIMCALL_NONE) {
- req_str = MC_request_to_string(req, value, MC_REQUEST_EXECUTED);
- XBT_INFO("%s", req_str);
- xbt_free(req_str);
- }
- }
-}
-
-
-void MC_dump_stack_liveness(xbt_fifo_t stack)
-{
- mc_pair_t pair;
- while ((pair = (mc_pair_t) xbt_fifo_pop(stack)) != nullptr)
- MC_pair_delete(pair);
-}
-
-void MC_print_statistics(mc_stats_t stats)
-{
- if(_sg_mc_comms_determinism) {
- if (!initial_global_state->recv_deterministic && initial_global_state->send_deterministic){
- XBT_INFO("******************************************************");
- XBT_INFO("**** Only-send-deterministic communication pattern ****");
- XBT_INFO("******************************************************");
- XBT_INFO("%s", initial_global_state->recv_diff);
- }else if(!initial_global_state->send_deterministic && initial_global_state->recv_deterministic) {
- XBT_INFO("******************************************************");
- XBT_INFO("**** Only-recv-deterministic communication pattern ****");
- XBT_INFO("******************************************************");
- XBT_INFO("%s", initial_global_state->send_diff);
- }
- }
-
- if (stats->expanded_pairs == 0) {
- XBT_INFO("Expanded states = %lu", stats->expanded_states);
- XBT_INFO("Visited states = %lu", stats->visited_states);
- } else {
- XBT_INFO("Expanded pairs = %lu", stats->expanded_pairs);
- XBT_INFO("Visited pairs = %lu", stats->visited_pairs);
- }
- XBT_INFO("Executed transitions = %lu", stats->executed_transitions);
- if ((_sg_mc_dot_output_file != nullptr) && (_sg_mc_dot_output_file[0] != '\0')) {
- fprintf(dot_output, "}\n");
- fclose(dot_output);
- }
- if (initial_global_state != nullptr && (_sg_mc_comms_determinism || _sg_mc_send_determinism)) {
- XBT_INFO("Send-deterministic : %s", !initial_global_state->send_deterministic ? "No" : "Yes");
- if (_sg_mc_comms_determinism)
- XBT_INFO("Recv-deterministic : %s", !initial_global_state->recv_deterministic ? "No" : "Yes");
- }
- if (getenv("SIMGRID_MC_SYSTEM_STATISTICS")){
- int ret=system("free");
- if(ret!=0)XBT_WARN("system call did not return 0, but %d",ret);
- }
-}
-
-void MC_automaton_load(const char *file)
-{
- if (_mc_property_automaton == nullptr)
- _mc_property_automaton = xbt_automaton_new();
-
- xbt_automaton_load(_mc_property_automaton, file);
-}
-
-// TODO, fix cross-process access (this function is not used)
-static void MC_dump_stacks(FILE* file)
-{
- int nstack = 0;
- for (auto const& stack : mc_model_checker->process().stack_areas()) {
-
- xbt_die("Fix cross-process access to the context");
- unw_context_t * context = (unw_context_t *)stack.context;
- fprintf(file, "Stack %i:\n", nstack);
-
- int nframe = 0;
- char buffer[100];
- unw_cursor_t c;
- unw_init_local (&c, context);
- unw_word_t off;
- do {
- const char * name = !unw_get_proc_name(&c, buffer, 100, &off) ? buffer : "?";