+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);
+ XBT_INFO("Send-deterministic : %s", !this->send_deterministic ? "No" : "Yes");
+ if (_sg_mc_comms_determinism)
+ XBT_INFO("Recv-deterministic : %s",
+ !this->recv_deterministic ? "No" : "Yes");
+}
+