for (auto const& state : stack_) {
int value;
smx_simcall_t req = MC_state_get_executed_request(state.get(), &value);
- if (req) {
- char* req_str = simgrid::mc::request_to_string(
- req, value, simgrid::mc::RequestType::executed);
- trace.push_back(req_str);
- xbt_free(req_str);
- }
+ if (req)
+ trace.push_back(simgrid::mc::request_to_string(
+ req, value, simgrid::mc::RequestType::executed));
}
return trace;
}
XBT_DEBUG("**************************************************");
XBT_DEBUG(
- "Exploration depth=%zi (state=%p, num %d)(%u interleave)",
+ "Exploration depth=%zi (state=%p, num %d)(%zu interleave)",
stack_.size(), state, state->num,
- MC_state_interleave_size(state));
+ state->interleaveSize());
mc_stats->visited_states++;
// If there are processes to interleave and the maximum depth has not been
// reached then perform one step of the exploration algorithm.
+ XBT_DEBUG("Execute: %s",
+ simgrid::mc::request_to_string(
+ req, value, simgrid::mc::RequestType::simix).c_str());
- if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
- char* req_str = simgrid::mc::request_to_string(req, value, simgrid::mc::RequestType::simix);
- XBT_DEBUG("Execute: %s", req_str);
- xbt_free(req_str);
- }
-
- char* req_str = nullptr;
+ std::string req_str;
if (dot_output != nullptr)
req_str = simgrid::mc::request_get_dot_output(req, value);
}
if (dot_output != nullptr)
- std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str);
+ std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
+ state->num, next_state->num, req_str.c_str());
} else if (dot_output != nullptr)
- std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, visitedState_->other_num == -1 ? visitedState_->num : visitedState_->other_num, req_str);
+ std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
+ state->num,
+ visitedState_->other_num == -1 ? visitedState_->num : visitedState_->other_num, req_str.c_str());
stack_.push_back(std::move(next_state));
-
- if (dot_output != nullptr)
- xbt_free(req_str);
}
XBT_INFO("No property violation found.");
XBT_DEBUG("Dependent Transitions:");
int value;
smx_simcall_t prev_req = MC_state_get_executed_request(prev_state, &value);
- char* req_str = simgrid::mc::request_to_string(prev_req, value, simgrid::mc::RequestType::internal);
- XBT_DEBUG("%s (state=%d)", req_str, prev_state->num);
- xbt_free(req_str);
+ XBT_DEBUG("%s (state=%d)",
+ simgrid::mc::request_to_string(
+ prev_req, value, simgrid::mc::RequestType::internal).c_str(),
+ prev_state->num);
prev_req = MC_state_get_executed_request(state.get(), &value);
- req_str = simgrid::mc::request_to_string(prev_req, value, simgrid::mc::RequestType::executed);
- XBT_DEBUG("%s (state=%d)", req_str, state->num);
- xbt_free(req_str);
+ XBT_DEBUG("%s (state=%d)",
+ simgrid::mc::request_to_string(
+ prev_req, value, simgrid::mc::RequestType::executed).c_str(),
+ state->num);
}
- if (!MC_state_process_is_done(prev_state, issuer))
+ if (!prev_state->processStates[issuer->pid].done())
MC_state_interleave_process(prev_state, issuer);
else
XBT_DEBUG("Process %p is in done set", req->issuer);
}
}
- if (MC_state_interleave_size(state.get())
+ if (state->interleaveSize()
&& stack_.size() < (std::size_t) _sg_mc_max_depth) {
/* We found a back-tracking point, let's loop */
XBT_DEBUG("Back-tracking to state %d at depth %zi",