-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* synchro1 = get_comm(req1);
- const kernel::activity::CommImpl* synchro2 = 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 (synchro1->src_buff_ == synchro2->src_buff_ && synchro1->dst_buff_ == synchro2->dst_buff_)
- return false;
- if (synchro1->src_buff_ != nullptr && synchro1->dst_buff_ != nullptr && synchro2->src_buff_ != nullptr &&
- synchro2->dst_buff_ != nullptr && synchro1->dst_buff_ != synchro2->src_buff_ &&
- synchro1->dst_buff_ != synchro2->dst_buff_ && synchro2->dst_buff_ != synchro1->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_synchro;
- const simgrid::kernel::activity::CommImpl* act;
- mc_model_checker->get_remote_simulation().read(temp_synchro, remote(remote_act));
- act = temp_synchro.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_synchro;
- const simgrid::kernel::activity::CommImpl* act;
- mc_model_checker->get_remote_simulation().read(temp_synchro, remote(remote_act));
- act = temp_synchro.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;
-
- case Simcall::MUTEX_LOCK: {
- type = "Mutex LOCK";
- simgrid::mc::Remote<simgrid::kernel::activity::MutexImpl> mutex;
- mc_model_checker->get_remote_simulation().read_bytes(mutex.get_buffer(), sizeof(mutex),
- remote(simcall_mutex_lock__get__mutex(req)));
- args = "locked = " + std::to_string(mutex.get_buffer()->is_locked()) + ", owner = ";
- if (mutex.get_buffer()->get_owner() != nullptr)
- args += std::to_string(mc_model_checker->get_remote_simulation()
- .resolve_actor(simgrid::mc::remote(mutex.get_buffer()->get_owner()))
- ->get_pid());
- else
- args += "-1";
- args += ", sleeping = n/a";
- 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