-void Api::dump_record_path() const
-{
- simgrid::mc::dumpRecordPath();
-}
-
-smx_simcall_t Api::mc_state_choose_request(simgrid::mc::State* state) const
-{
- for (auto& actor : mc_model_checker->get_remote_simulation().actors()) {
- /* Only consider the actors that were marked as interleaving by the checker algorithm */
- if (not state->actor_states_[actor.copy.get_buffer()->get_pid()].is_todo())
- continue;
-
- smx_simcall_t res = MC_state_choose_request_for_process(state, actor.copy.get_buffer());
- if (res)
- return res;
- }
- return nullptr;
-}
-
-std::list<transition_detail_t> Api::get_enabled_transitions(simgrid::mc::State* state) const
-{
- std::list<transition_detail_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;
-
- auto transition = std::make_unique<s_transition_detail>();
- Simcall simcall_call = actor_impl->simcall_.call_;
- smx_simcall_t simcall = &actor_impl->simcall_;
- transition->call_ = simcall_call;
- switch (simcall_call) {
- case Simcall::COMM_ISEND:
- case Simcall::COMM_IRECV:
- transition->mbox_remote_addr = get_mbox_remote_addr(simcall);
- transition->comm_remote_addr = get_comm_remote_addr(simcall);
- break;
-
- default:
- break;
- }
- tr_list.emplace_back(std::move(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 */
- 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;
-
- if (req1->call_ != req2->call_)
- return request_depend_asymmetric(req1, req2) && request_depend_asymmetric(req2, req1);
-
- // Those are internal requests, we do not need indirection because those objects are copies:
- const kernel::activity::CommImpl* activity1 = get_comm(req1);
- const kernel::activity::CommImpl* activity2 = get_comm(req2);
-
- switch (req1->call_) {
- case Simcall::COMM_ISEND:
- return simcall_comm_isend__get__mbox(req1) == simcall_comm_isend__get__mbox(req2);
- case Simcall::COMM_IRECV:
- return simcall_comm_irecv__get__mbox(req1) == simcall_comm_irecv__get__mbox(req2);
- case Simcall::COMM_WAIT:
- if (activity1->src_buff_ == activity2->src_buff_ && activity1->dst_buff_ == activity2->dst_buff_)
- return false;
- if (activity1->src_buff_ != nullptr && activity1->dst_buff_ != nullptr && activity2->src_buff_ != nullptr &&
- activity2->dst_buff_ != nullptr && activity1->dst_buff_ != activity2->src_buff_ &&
- activity1->dst_buff_ != activity2->dst_buff_ && activity2->dst_buff_ != activity1->src_buff_)
- return false;
- return true;
- default:
- return true;
- }
-}
-
-std::string Api::request_to_string(smx_simcall_t req, int value) const
-{
- xbt_assert(mc_model_checker != nullptr, "Must be called from MCer");
-
- std::string type;
- std::string args;
-
- smx_actor_t issuer = simcall_get_issuer(req);
-
- if (issuer->simcall_.observer_ != nullptr)
- return mc_model_checker->simcall_to_string(issuer->get_pid(), value);
-
- switch (req->call_) {
- case Simcall::COMM_ISEND:
- type = "iSend";
- args = "src=" + get_actor_string(issuer);
- args += ", buff=" + pointer_to_string(simcall_comm_isend__get__src_buff(req));
- args += ", size=" + buff_size_to_string(simcall_comm_isend__get__src_buff_size(req));
- break;
-
- case Simcall::COMM_IRECV: {
- size_t* remote_size = simcall_comm_irecv__get__dst_buff_size(req);
- size_t size = 0;
- if (remote_size)
- mc_model_checker->get_remote_simulation().read_bytes(&size, sizeof(size), remote(remote_size));
-
- type = "iRecv";
- args = "dst=" + get_actor_string(issuer);
- args += ", buff=" + pointer_to_string(simcall_comm_irecv__get__dst_buff(req));
- args += ", size=" + buff_size_to_string(size);
- break;
- }
-
- case Simcall::COMM_WAIT: {
- simgrid::kernel::activity::CommImpl* remote_act = simcall_comm_wait__getraw__comm(req);
- if (value == -1) {
- type = "WaitTimeout";
- args = "comm=" + pointer_to_string(remote_act);
- } else {
- type = "Wait";
-
- simgrid::mc::Remote<simgrid::kernel::activity::CommImpl> temp_activity;
- const simgrid::kernel::activity::CommImpl* act;
- mc_model_checker->get_remote_simulation().read(temp_activity, remote(remote_act));
- act = temp_activity.get_buffer();
-
- smx_actor_t src_proc =
- mc_model_checker->get_remote_simulation().resolve_actor(simgrid::mc::remote(act->src_actor_.get()));
- smx_actor_t dst_proc =
- mc_model_checker->get_remote_simulation().resolve_actor(simgrid::mc::remote(act->dst_actor_.get()));
- args = "comm=" + pointer_to_string(remote_act);
- args += " [" + get_actor_string(src_proc) + "-> " + get_actor_string(dst_proc) + "]";
- }
- break;
- }
-
- case Simcall::COMM_TEST: {
- simgrid::kernel::activity::CommImpl* remote_act = simcall_comm_test__getraw__comm(req);
- simgrid::mc::Remote<simgrid::kernel::activity::CommImpl> temp_activity;
- const simgrid::kernel::activity::CommImpl* act;
- mc_model_checker->get_remote_simulation().read(temp_activity, remote(remote_act));
- act = temp_activity.get_buffer();
-
- if (act->src_actor_.get() == nullptr || act->dst_actor_.get() == nullptr) {
- type = "Test FALSE";
- args = "comm=" + pointer_to_string(remote_act);
- } else {
- type = "Test TRUE";
-
- smx_actor_t src_proc =
- mc_model_checker->get_remote_simulation().resolve_actor(simgrid::mc::remote(act->src_actor_.get()));
- smx_actor_t dst_proc =
- mc_model_checker->get_remote_simulation().resolve_actor(simgrid::mc::remote(act->dst_actor_.get()));
- args = "comm=" + pointer_to_string(remote_act);
- args += " [" + get_actor_string(src_proc) + " -> " + get_actor_string(dst_proc) + "]";
- }
- break;
- }
-
- case Simcall::COMM_WAITANY: {
- type = "WaitAny";
- size_t count = simcall_comm_waitany__get__count(req);
- if (count > 0) {
- simgrid::kernel::activity::CommImpl* remote_sync;
- remote_sync =
- mc_model_checker->get_remote_simulation().read(remote(simcall_comm_waitany__get__comms(req) + value));
- args = "comm=" + pointer_to_string(remote_sync) + xbt::string_printf("(%d of %zu)", value + 1, count);
- } else
- args = "comm at idx " + std::to_string(value);
- break;
- }
-
- case Simcall::COMM_TESTANY:
- if (value == -1) {
- type = "TestAny FALSE";
- args = "-";
- } else {
- type = "TestAny";
- args = xbt::string_printf("(%d of %zu)", value + 1, simcall_comm_testany__get__count(req));
- }
- break;
-
- default:
- type = SIMIX_simcall_name(req->call_);
- args = "??";
- break;
- }
-
- return "[" + get_actor_string(issuer) + "] " + type + "(" + args + ")";
-}
-
-std::string Api::request_get_dot_output(smx_simcall_t req, int value) const
-{
- const smx_actor_t issuer = simcall_get_issuer(req);
- const char* color = get_color(issuer->get_pid() - 1);
-
- std::string label;
-
- if (req->observer_ != nullptr) {
- label = mc_model_checker->simcall_dot_label(issuer->get_pid(), value);
- } else
- switch (req->call_) {
- case Simcall::COMM_ISEND:
- label = "[" + get_actor_dot_label(issuer) + "] iSend";
- break;
-
- case Simcall::COMM_IRECV:
- label = "[" + get_actor_dot_label(issuer) + "] iRecv";
- break;
-
- case Simcall::COMM_WAIT:
- if (value == -1) {
- label = "[" + get_actor_dot_label(issuer) + "] WaitTimeout";
- } else {
- kernel::activity::ActivityImpl* remote_act = simcall_comm_wait__getraw__comm(req);
- Remote<kernel::activity::CommImpl> temp_comm;
- mc_model_checker->get_remote_simulation().read(temp_comm,
- remote(static_cast<kernel::activity::CommImpl*>(remote_act)));
- const kernel::activity::CommImpl* comm = temp_comm.get_buffer();
-
- const kernel::actor::ActorImpl* src_proc =
- mc_model_checker->get_remote_simulation().resolve_actor(mc::remote(comm->src_actor_.get()));
- const kernel::actor::ActorImpl* dst_proc =
- mc_model_checker->get_remote_simulation().resolve_actor(mc::remote(comm->dst_actor_.get()));
- label = "[" + get_actor_dot_label(issuer) + "] Wait";
- label += " [(" + std::to_string(src_proc ? src_proc->get_pid() : 0) + ")";
- label += "->(" + std::to_string(dst_proc ? dst_proc->get_pid() : 0) + ")]";
- }
- break;
-
- case Simcall::COMM_TEST: {
- kernel::activity::ActivityImpl* remote_act = simcall_comm_test__getraw__comm(req);
- Remote<simgrid::kernel::activity::CommImpl> temp_comm;
- mc_model_checker->get_remote_simulation().read(temp_comm,
- remote(static_cast<kernel::activity::CommImpl*>(remote_act)));
- const kernel::activity::CommImpl* comm = temp_comm.get_buffer();
- if (comm->src_actor_.get() == nullptr || comm->dst_actor_.get() == nullptr) {
- label = "[" + get_actor_dot_label(issuer) + "] Test FALSE";
- } else {
- label = "[" + get_actor_dot_label(issuer) + "] Test TRUE";
- }
- break;
- }
-
- case Simcall::COMM_WAITANY:
- label = "[" + get_actor_dot_label(issuer) + "] WaitAny";
- label += xbt::string_printf(" [%d of %zu]", value + 1, simcall_comm_waitany__get__count(req));
- break;
-
- case Simcall::COMM_TESTANY:
- if (value == -1) {
- label = "[" + get_actor_dot_label(issuer) + "] TestAny FALSE";
- } else {
- label = "[" + get_actor_dot_label(issuer) + "] TestAny TRUE";
- label += xbt::string_printf(" [%d of %zu]", value + 1, simcall_comm_testany__get__count(req));
- }
- break;
-
- default:
- THROW_UNIMPLEMENTED;
- }
-
- return "label = \"" + label + "\", color = " + color + ", fontcolor = " + color;
-}
-
-#if HAVE_SMPI
-int Api::get_smpi_request_tag(smx_simcall_t const& simcall, simgrid::simix::Simcall type) const
-{
- simgrid::smpi::Request mpi_request;
- void* simcall_data = nullptr;
- if (type == Simcall::COMM_ISEND)
- simcall_data = simcall_comm_isend__get__data(simcall);
- else if (type == Simcall::COMM_IRECV)
- simcall_data = simcall_comm_irecv__get__data(simcall);
- mc_model_checker->get_remote_simulation().read(&mpi_request, remote(static_cast<smpi::Request*>(simcall_data)));
- return mpi_request.tag();
-}
-#endif
-