+RecordTrace CommunicationDeterminismChecker::getRecordTrace() // override
+{
+ RecordTrace res;
+ for (auto const& state : stack_)
+ res.push_back(state->getTransition());
+ return res;
+}
+
+std::vector<std::string> CommunicationDeterminismChecker::getTextualTrace() // override
+{
+ std::vector<std::string> trace;
+ for (auto const& state : stack_) {
+ smx_simcall_t req = &state->executed_req;
+ if (req)
+ trace.push_back(simgrid::mc::request_to_string(
+ req, state->transition.argument, simgrid::mc::RequestType::executed));
+ }
+ return trace;
+}
+
+void CommunicationDeterminismChecker::logState() // override
+{
+ Checker::logState();
+ if (_sg_mc_comms_determinism &&
+ !this->recv_deterministic &&
+ this->send_deterministic) {
+ XBT_INFO("******************************************************");
+ XBT_INFO("**** Only-send-deterministic communication pattern ****");
+ XBT_INFO("******************************************************");
+ XBT_INFO("%s", this->recv_diff);
+ } else if(_sg_mc_comms_determinism &&
+ !this->send_deterministic &&
+ this->recv_deterministic) {
+ XBT_INFO("******************************************************");
+ XBT_INFO("**** Only-recv-deterministic communication pattern ****");
+ XBT_INFO("******************************************************");
+ XBT_INFO("%s", this->send_diff);
+ }
+ XBT_INFO("Expanded states = %lu", expandedStatesCount_);
+ XBT_INFO("Visited states = %lu", mc_model_checker->visited_states);
+ XBT_INFO("Executed transitions = %lu", mc_model_checker->executed_transitions);
+ if (this != nullptr)
+ XBT_INFO("Send-deterministic : %s",
+ !this->send_deterministic ? "No" : "Yes");
+ if (this != nullptr && _sg_mc_comms_determinism)
+ XBT_INFO("Recv-deterministic : %s",
+ !this->recv_deterministic ? "No" : "Yes");
+}
+