- if (not actor.is_todo() || not actor.is_enabled() || actor.is_done())
- continue;
-
- const Transition* transition = actor.get_transition(actor.get_times_considered());
-
- const CommRecvTransition* cast_recv = static_cast<CommRecvTransition const*>(transition);
- if (cast_recv != nullptr and mailbox_.count(cast_recv->get_mailbox()) > 0 and
- mailbox_.at(cast_recv->get_mailbox()) > 0)
- return std::make_pair(aid, value_of_state_ - 1); // This means we have waiting send corresponding to this recv
-
- const CommSendTransition* cast_send = static_cast<CommSendTransition const*>(transition);
- if (cast_send != nullptr and mailbox_.count(cast_send->get_mailbox()) > 0 and
- mailbox_.at(cast_send->get_mailbox()) < 0)
- return std::make_pair(aid, value_of_state_ - 1); // This means we have waiting recv corresponding to this send
-
- if (if_no_match.first == -1)
- if_no_match = std::make_pair(aid, value_of_state_);
+ if ((not actor.is_todo() && must_be_todo) || not actor.is_enabled() || actor.is_done())
+ continue;
+
+ int aid_value = value_of_state_;
+ const Transition* transition = actor.get_transition(actor.get_times_considered()).get();
+
+ const CommRecvTransition* cast_recv = dynamic_cast<CommRecvTransition const*>(transition);
+ if (cast_recv != nullptr) {
+ if (mailbox_.count(cast_recv->get_mailbox()) > 0 and
+ mailbox_.at(cast_recv->get_mailbox()) > 0) {
+ aid_value--; // This means we have waiting recv corresponding to this recv
+ } else {
+ aid_value++;
+ }
+ }
+
+ const CommSendTransition* cast_send = dynamic_cast<CommSendTransition const*>(transition);
+ if (cast_send != nullptr) {
+ if (mailbox_.count(cast_send->get_mailbox()) > 0 and
+ mailbox_.at(cast_send->get_mailbox()) < 0) {
+ aid_value--; // This means we have waiting recv corresponding to this send
+ }else {
+ aid_value++;
+ }
+ }
+
+ if (aid_value < min_found.second)
+ min_found = std::make_pair(aid, aid_value);