}
// Does half the job
-bool Api::request_depend_asymmetric(smx_simcall_t r1, smx_simcall_t r2) const
+bool Api::request_depend_asymmetric(smx_simcall_t r1, smx_simcall_t r2) const
{
if (r1->call_ == Simcall::COMM_ISEND && r2->call_ == Simcall::COMM_IRECV)
return false;
const kernel::activity::CommImpl* synchro2 = get_comm(r2);
if ((r1->call_ == Simcall::COMM_ISEND || r1->call_ == Simcall::COMM_IRECV) && r2->call_ == Simcall::COMM_WAIT) {
- auto mbox = get_mbox_remote_addr(r1);;
+ auto mbox = get_mbox_remote_addr(r1);
RemotePtr<kernel::activity::MailboxImpl> synchro2_mbox_cpy = remote(synchro2->mbox_cpy);
- if (mbox != synchro2_mbox_cpy
- && simcall_comm_wait__get__timeout(r2) <= 0)
+ if (mbox != synchro2_mbox_cpy && simcall_comm_wait__get__timeout(r2) <= 0)
return false;
if ((r1->issuer_ != synchro2->src_actor_.get()) && (r1->issuer_ != synchro2->dst_actor_.get()) &&
RemotePtr<kernel::activity::CommImpl> Api::get_comm_waitany_raw_addr(smx_simcall_t request, int value) const
{
- auto addr = simgrid::simix::unmarshal_raw<simgrid::kernel::activity::CommImpl**>(request->args_[0]) + value;
+ auto addr = simgrid::simix::unmarshal_raw<simgrid::kernel::activity::CommImpl**>(request->args_[0]) + value;
auto comm_addr = mc_model_checker->get_remote_simulation().read(remote(addr));
return RemotePtr<kernel::activity::CommImpl>(static_cast<kernel::activity::CommImpl*>(comm_addr));
}
case Simcall::COMM_ISEND:
case Simcall::COMM_IRECV: {
auto mbox_addr_ptr = simix::unmarshal<smx_mailbox_t>(req->args_[1]);
- mbox_addr = remote(mbox_addr_ptr);
+ mbox_addr = remote(mbox_addr_ptr);
break;
}
default:
return nullptr;
}
+std::list<udpor_transition_t> Api::get_enabled_transitions(simgrid::mc::State* state)
+{
+ std::list<udpor_transition_t> tr_list{};
+
+ for (auto& actor : mc_model_checker->get_remote_simulation().actors()) {
+ auto actor_pid = actor.copy.get_buffer()->get_pid();
+ auto actor_impl = actor.copy.get_buffer();
+
+ // Only consider the actors that were marked as interleaving by the checker algorithm
+ if (not state->actor_states_[actor_pid].is_todo())
+ continue;
+ // Not executable in the application
+ if (not simgrid::mc::actor_is_enabled(actor_impl))
+ continue;
+
+ udpor_transition_t udpor_transition = std::unique_ptr<s_udpor_transition>(new s_udpor_transition());
+ Simcall simcall_call = actor_impl->simcall_.call_;
+ smx_simcall_t simcall = &actor_impl->simcall_;
+ udpor_transition->call_ = simcall_call;
+ switch (simcall_call) {
+ case Simcall::COMM_ISEND:
+ case Simcall::COMM_IRECV: {
+ udpor_transition->mbox_remote_addr = get_mbox_remote_addr(simcall);
+ udpor_transition->comm_remote_addr = get_comm_remote_addr(simcall);
+ break;
+ }
+
+ default:
+ break;
+ }
+ tr_list.emplace_back(std::move(udpor_transition));
+ }
+
+ return tr_list;
+}
+
bool Api::simcall_check_dependency(smx_simcall_t const req1, smx_simcall_t const req2) const
{
if (req1->issuer_ == req2->issuer_)
return false;
- /* Wait with timeout transitions are not considered by the independence theorem, thus we consider them as dependent with all other transitions */
+ /* Wait with timeout transitions are not considered by the independence theorem, thus we consider them as dependent
+ * with all other transitions */
if ((req1->call_ == Simcall::COMM_WAIT && simcall_comm_wait__get__timeout(req1) > 0) ||
(req2->call_ == Simcall::COMM_WAIT && simcall_comm_wait__get__timeout(req2) > 0))
return true;