- ssize_t received = model_checker_->channel().receive(answer);
- xbt_assert(received != -1, "Could not receive message");
- xbt_assert(received == sizeof(answer) && answer.type == MessageType::ACTORS_STATUS_REPLY,
- "Received unexpected message %s (%i, size=%i) "
- "expected MessageType::ACTORS_STATUS_REPLY (%i, size=%i)",
- to_c_str(answer.type), (int)answer.type, (int)received, (int)MessageType::ACTORS_STATUS_REPLY,
- (int)sizeof(answer));
+ ssize_t answer_size = model_checker_->channel().receive(answer);
+ xbt_assert(answer_size != -1, "Could not receive message");
+ xbt_assert(answer_size == sizeof answer, "Broken message (size=%zd; expected %zu)", answer_size, sizeof answer);
+ xbt_assert(answer.type == MessageType::ACTORS_STATUS_REPLY,
+ "Received unexpected message %s (%i); expected MessageType::ACTORS_STATUS_REPLY (%i)",
+ to_c_str(answer.type), (int)answer.type, (int)MessageType::ACTORS_STATUS_REPLY);
+
+ // Message sanity checks
+ xbt_assert(answer.count >= 0, "Received an ACTOR_STATUS_REPLY message with an actor count of '%d' < 0", answer.count);
+ xbt_assert(answer.transition_count >= 0, "Received an ACTOR_STATUS_REPLY message with transition_count '%d' < 0",
+ answer.transition_count);
+ xbt_assert(answer.transition_count == 0 || answer.count >= 0,
+ "Received an ACTOR_STATUS_REPLY message with no actor data "
+ "but with transition data nonetheless");
+
+ std::vector<s_mc_message_actors_status_one_t> status(answer.count);
+ if (answer.count > 0) {
+ size_t size = status.size() * sizeof(s_mc_message_actors_status_one_t);
+ ssize_t received = model_checker_->channel().receive(status.data(), size);
+ xbt_assert(static_cast<size_t>(received) == size);
+ }
+
+ // Ensures that each actor sends precisely `answer.transition_count` transitions. While technically
+ // this doesn't catch the edge case where actor A sends 3 instead of 2 and actor B sends 2 instead
+ // of 3 transitions, that is ignored here since that invariant needs to be enforced on the AppSide
+ const auto expected_transitions = std::accumulate(
+ status.begin(), status.end(), 0, [](int total, const auto& actor) { return total + actor.n_transitions; });
+ xbt_assert(expected_transitions == answer.transition_count,
+ "Expected to receive %d transition(s) but was only notified of %d by the app side", expected_transitions,
+ answer.transition_count);