#include "src/mc/Transition.hpp"
#include "src/mc/VisitedState.hpp"
#include "src/mc/checker/CommunicationDeterminismChecker.hpp"
-#include "src/mc/mc_exit.h"
-#include "src/mc/mc_private.h"
-#include "src/mc/mc_record.h"
-#include "src/mc/mc_request.h"
-#include "src/mc/mc_smx.h"
-#include "src/mc/mc_state.h"
+#include "src/mc/mc_exit.hpp"
+#include "src/mc/mc_private.hpp"
+#include "src/mc/mc_record.hpp"
+#include "src/mc/mc_request.hpp"
+#include "src/mc/mc_smx.hpp"
+#include "src/mc/mc_state.hpp"
#include "src/mc/remote/Client.hpp"
#include "smpi_request.hpp"
simgrid::kernel::activity::CommImpl* comm = temp_comm.getBuffer();
char* remote_name;
- mc_model_checker->process().read(&remote_name, remote(comm->mbox ? &comm->mbox->name_ : &comm->mbox_cpy->name_));
+ mc_model_checker->process().read(
+ &remote_name, remote(comm->mbox ? &simgrid::xbt::string::to_string_data(comm->mbox->name_).data
+ : &simgrid::xbt::string::to_string_data(comm->mbox_cpy->name_).data));
pattern->rdv = mc_model_checker->process().read_string(remote_name);
pattern->dst_proc = mc_model_checker->process().resolveActor(simgrid::mc::remote(comm->dst_proc))->pid;
pattern->dst_host = MC_smx_actor_get_host_name(issuer);
void CommunicationDeterminismChecker::logState() // override
{
- Checker::logState();
if (_sg_mc_comms_determinism && not this->recv_deterministic && this->send_deterministic) {
XBT_INFO("******************************************************");
XBT_INFO("**** Only-send-deterministic communication pattern ****");
/* Update statistics */
mc_model_checker->visited_states++;
- if (stack_.size() <= (std::size_t)_sg_mc_max_depth && (req = MC_state_get_request(state)) != nullptr &&
- (visited_state == nullptr)) {
+ if (stack_.size() <= (std::size_t)_sg_mc_max_depth)
+ req = MC_state_get_request(state);
+ else
+ req = nullptr;
+
+ if (req != nullptr && visited_state == nullptr) {
int req_num = state->transition.argument;
* with the initial pattern. */
bool compare_snapshots = all_communications_are_finished() && this->initial_communications_pattern_done;
- if (_sg_mc_max_visited_states == 0 ||
- (visited_state = visitedStates_.addVisitedState(expandedStatesCount_, next_state.get(), compare_snapshots)) ==
- nullptr) {
+ if (_sg_mc_max_visited_states != 0)
+ visited_state = visitedStates_.addVisitedState(expandedStatesCount_, next_state.get(), compare_snapshots);
+ else
+ visited_state = nullptr;
+
+ if (visited_state == nullptr) {
/* Get enabled actors and insert them in the interleave set of the next state */
for (auto& actor : mc_model_checker->process().actors())