#include "src/mc/Session.hpp"
#include "src/mc/checker/SimcallInspector.hpp"
#include "src/mc/mc_comm_pattern.hpp"
+#include "src/mc/mc_exit.hpp"
#include "src/mc/mc_pattern.hpp"
#include "src/mc/mc_private.hpp"
#include "src/mc/mc_smx.hpp"
}
std::string Api::get_actor_string(smx_actor_t actor) const
-{
- std::string res = "(" + std::to_string(actor->get_pid()) + ")";
- if (actor->get_host())
- res += get_actor_host_name(actor);
- return res;
-}
-
-std::string Api::get_actor_string2(smx_actor_t actor) const
{
std::string res;
if (actor) {
return res;
}
+std::string Api::get_actor_dot_label(smx_actor_t actor) const
+{
+ std::string res = "(" + std::to_string(actor->get_pid()) + ")";
+ if (actor->get_host())
+ res += get_actor_host_name(actor);
+ return res;
+}
+
void Api::initialize(char** argv) const
{
simgrid::mc::session = new simgrid::mc::Session([argv] {
return mc_model_checker->executed_transitions;
}
-bool Api::mc_check_deadlock() const
+void Api::mc_check_deadlock() const
{
- return mc_model_checker->checkDeadlock();
-}
-
-void Api::mc_show_deadlock() const
-{
- MC_show_deadlock();
+ if (mc_model_checker->checkDeadlock()) {
+ MC_show_deadlock();
+ throw DeadlockError();
+ }
}
/** Get the issuer of a simcall (`req->issuer`)
return nullptr;
}
-std::list<transition_detail_t> Api::get_enabled_transitions(simgrid::mc::State* state)
+std::list<transition_detail_t> Api::get_enabled_transitions(simgrid::mc::State* state) const
{
std::list<transition_detail_t> tr_list{};
if (not simgrid::mc::actor_is_enabled(actor_impl))
continue;
- transition_detail_t transition = std::unique_ptr<s_transition_detail>(new s_transition_detail());
- Simcall simcall_call = actor_impl->simcall_.call_;
- smx_simcall_t simcall = &actor_impl->simcall_;
- transition->call_ = simcall_call;
+ 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:
switch (req->call_) {
case Simcall::COMM_ISEND:
type = "iSend";
- args = "src=" + get_actor_string2(issuer);
+ 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;
mc_model_checker->get_remote_simulation().read_bytes(&size, sizeof(size), remote(remote_size));
type = "iRecv";
- args = "dst=" + get_actor_string2(issuer);
+ 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;
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_string2(src_proc) + "-> " + get_actor_string2(dst_proc) + "]";
+ args += " [" + get_actor_string(src_proc) + "-> " + get_actor_string(dst_proc) + "]";
}
break;
}
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_string2(src_proc) + " -> " + get_actor_string2(dst_proc) + "]";
+ args += " [" + get_actor_string(src_proc) + " -> " + get_actor_string(dst_proc) + "]";
}
break;
}
break;
}
- return "[" + get_actor_string2(issuer) + "] " + type + "(" + args + ")";
+ return "[" + get_actor_string(issuer) + "] " + type + "(" + args + ")";
}
std::string Api::request_get_dot_output(smx_simcall_t req, int value) const
} else
switch (req->call_) {
case Simcall::COMM_ISEND:
- label = "[" + get_actor_string(issuer) + "] iSend";
+ label = "[" + get_actor_dot_label(issuer) + "] iSend";
break;
case Simcall::COMM_IRECV:
- label = "[" + get_actor_string(issuer) + "] iRecv";
+ label = "[" + get_actor_dot_label(issuer) + "] iRecv";
break;
case Simcall::COMM_WAIT:
if (value == -1) {
- label = "[" + get_actor_string(issuer) + "] WaitTimeout";
+ 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().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_string(issuer) + "] Wait";
+ 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) + ")]";
}
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_string(issuer) + "] Test FALSE";
+ label = "[" + get_actor_dot_label(issuer) + "] Test FALSE";
} else {
- label = "[" + get_actor_string(issuer) + "] Test TRUE";
+ label = "[" + get_actor_dot_label(issuer) + "] Test TRUE";
}
break;
}
case Simcall::COMM_WAITANY:
- label = "[" + get_actor_string(issuer) + "] 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_string(issuer) + "] TestAny FALSE";
+ label = "[" + get_actor_dot_label(issuer) + "] TestAny FALSE";
} else {
- label = "[" + get_actor_string(issuer) + "] TestAny TRUE";
+ label = "[" + get_actor_dot_label(issuer) + "] TestAny TRUE";
label += xbt::string_printf(" [%d of %zu]", value + 1, simcall_comm_testany__get__count(req));
}
break;
case Simcall::MUTEX_TRYLOCK:
- label = "[" + get_actor_string(issuer) + "] Mutex TRYLOCK";
+ label = "[" + get_actor_dot_label(issuer) + "] Mutex TRYLOCK";
break;
case Simcall::MUTEX_LOCK:
- label = "[" + get_actor_string(issuer) + "] Mutex LOCK";
+ label = "[" + get_actor_dot_label(issuer) + "] Mutex LOCK";
break;
default:
void Api::execute(Transition& transition, smx_simcall_t simcall) const
{
/* FIXME: once all simcalls have observers, kill the simcall parameter and use mc_model_checker->simcall_to_string() */
- auto textual =
- simgrid::mc::Api::get().request_to_string(simcall, transition.times_considered_, RequestType::executed);
- strcpy((char*)transition.textual, textual.c_str());
-
+ transition.textual = request_to_string(simcall, transition.times_considered_, RequestType::executed);
session->execute(transition);
}
