From cee502af6d0b9f251c6f36a7baa98a5342b08abf Mon Sep 17 00:00:00 2001 From: Marion Guthmuller Date: Wed, 5 Jun 2013 23:48:07 +0200 Subject: [PATCH] model-checker : add information in counter-example and dot output --- src/mc/mc_global.c | 18 ++++++++++++------ src/mc/mc_request.c | 42 +++++++++++++++++++++++------------------- 2 files changed, 35 insertions(+), 25 deletions(-) diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c index 9805ce20e1..70013ed9d5 100644 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@ -222,17 +222,22 @@ void MC_init(){ } -void MC_init_dot_output(){ +void MC_init_dot_output(){ /* FIXME : more colors */ colors[0] = "blue"; colors[1] = "red"; - colors[2] = "green"; - colors[3] = "pink"; + colors[2] = "green3"; + colors[3] = "goldenrod"; colors[4] = "brown"; colors[5] = "purple"; - colors[6] = "yellow"; - colors[7] = "orange"; - + colors[6] = "magenta"; + colors[7] = "turquoise4"; + colors[8] = "gray25"; + colors[9] = "forestgreen"; + colors[10] = "hotpink"; + colors[11] = "lightblue"; + colors[12] = "tan"; + dot_output = fopen(_sg_mc_dot_output_file, "w"); if(dot_output == NULL){ @@ -684,6 +689,7 @@ void MC_show_deadlock(smx_simcall_t req) xbt_free(req_str);*/ XBT_INFO("Counter-example execution trace:"); MC_dump_stack_safety(mc_stack_safety); + MC_print_statistics(mc_stats); } diff --git a/src/mc/mc_request.c b/src/mc/mc_request.c index 95b4b9ec71..67db7d9d91 100644 --- a/src/mc/mc_request.c +++ b/src/mc/mc_request.c @@ -181,14 +181,14 @@ char *MC_request_to_string(smx_simcall_t req, int value) type = xbt_strdup("iSend"); p = pointer_to_string(simcall_comm_isend__get__src_buff(req)); bs = buff_size_to_string(simcall_comm_isend__get__src_buff_size(req)); - args = bprintf("src=%s, buff=%s, size=%s", req->issuer->name, p, bs); + args = bprintf("src=(%lu)%s (%s), buff=%s, size=%s", req->issuer->pid, MSG_host_get_name(req->issuer->smx_host), req->issuer->name, p, bs); break; case SIMCALL_COMM_IRECV: size = simcall_comm_irecv__get__dst_buff_size(req) ? *simcall_comm_irecv__get__dst_buff_size(req) : 0; type = xbt_strdup("iRecv"); p = pointer_to_string(simcall_comm_irecv__get__dst_buff(req)); bs = buff_size_to_string(size); - args = bprintf("dst=%s, buff=%s, size=%s", req->issuer->name, p, bs); + args = bprintf("dst=(%lu)%s (%s), buff=%s, size=%s", req->issuer->pid, MSG_host_get_name(req->issuer->smx_host), req->issuer->name, p, bs); break; case SIMCALL_COMM_WAIT: act = simcall_comm_wait__get__comm(req); @@ -199,10 +199,12 @@ char *MC_request_to_string(smx_simcall_t req, int value) }else{ type = xbt_strdup("Wait"); p = pointer_to_string(act); - args = bprintf("comm=%s [(%lu)%s -> (%lu)%s]", p, + args = bprintf("comm=%s [(%lu)%s (%s)-> (%lu)%s (%s)]", p, act->comm.src_proc ? act->comm.src_proc->pid : 0, + act->comm.src_proc ? MSG_host_get_name(act->comm.src_proc->smx_host) : "", act->comm.src_proc ? act->comm.src_proc->name : "", act->comm.dst_proc ? act->comm.dst_proc->pid : 0, + act->comm.dst_proc ? MSG_host_get_name(act->comm.dst_proc->smx_host) : "", act->comm.dst_proc ? act->comm.dst_proc->name : ""); } break; @@ -215,9 +217,9 @@ char *MC_request_to_string(smx_simcall_t req, int value) }else{ type = xbt_strdup("Test TRUE"); p = pointer_to_string(act); - args = bprintf("comm=%s [(%lu)%s -> (%lu)%s]", p, - act->comm.src_proc->pid, act->comm.src_proc->name, - act->comm.dst_proc->pid, act->comm.dst_proc->name); + args = bprintf("comm=%s [(%lu)%s (%s) -> (%lu)%s (%s)]", p, + act->comm.src_proc->pid, act->comm.src_proc->name, MSG_host_get_name(act->comm.src_proc->smx_host), + act->comm.dst_proc->pid, act->comm.dst_proc->name, MSG_host_get_name(act->comm.dst_proc->smx_host)); } break; @@ -258,7 +260,7 @@ char *MC_request_to_string(smx_simcall_t req, int value) } if(args != NULL){ - str = bprintf("[(%lu)%s] %s (%s)", req->issuer->pid ,req->issuer->name, type, args); + str = bprintf("[(%lu)%s (%s)] %s (%s)", req->issuer->pid , MSG_host_get_name(req->issuer->smx_host), req->issuer->name, type, args); xbt_free(args); }else{ str = bprintf("[(%lu)%s] %s ", req->issuer->pid ,req->issuer->name, type); @@ -376,51 +378,53 @@ char *MC_request_get_dot_output(smx_simcall_t req, int value){ char *str = NULL, *label = NULL; smx_action_t act = NULL; + const char *host_name = MSG_host_get_name(MSG_process_get_host(req->issuer)); switch(req->call){ case SIMCALL_COMM_ISEND: - label = xbt_strdup("iSend"); + label = bprintf("[(%lu)%s] iSend", req->issuer->pid, host_name); break; case SIMCALL_COMM_IRECV: - label = xbt_strdup("iRecv"); + label = bprintf("[(%lu)%s] iRecv", req->issuer->pid, host_name); break; case SIMCALL_COMM_WAIT: - if(value == -1) - label = xbt_strdup("WaitTimeout"); + act = simcall_comm_wait__get__comm(req); + if(value == -1) + label = bprintf("[(%lu)%s] WaitTimeout", req->issuer->pid, host_name); else - label = xbt_strdup("Wait"); + label = bprintf("[(%lu)%s] Wait [(%lu)->(%lu)]", req->issuer->pid, host_name, act->comm.src_proc ? act->comm.src_proc->pid : 0, act->comm.dst_proc ? act->comm.dst_proc->pid : 0); break; case SIMCALL_COMM_TEST: act = simcall_comm_test__get__comm(req); if(act->comm.src_proc == NULL || act->comm.dst_proc == NULL) - label = xbt_strdup("Test FALSE"); + label = bprintf("[(%lu)%s] Test FALSE", req->issuer->pid, host_name); else - label = xbt_strdup("Test TRUE"); + label = bprintf("[(%lu)%s] Test TRUE", req->issuer->pid, host_name); break; case SIMCALL_MC_RANDOM: if(value == 0) - label = xbt_strdup("MC_RANDOM (0)"); + label = bprintf("[(%lu)%s] MC_RANDOM (0)", req->issuer->pid, host_name); else - label = xbt_strdup("MC_RANDOM (1)"); + label = bprintf("[(%lu)%s] MC_RANDOM (1)", req->issuer->pid, host_name); break; case SIMCALL_MC_SNAPSHOT: - label = xbt_strdup("MC_SNAPSHOT"); + label = bprintf("[(%lu)%s] MC_SNAPSHOT", req->issuer->pid, host_name); break; case SIMCALL_MC_COMPARE_SNAPSHOTS: - label = xbt_strdup("MC_COMPARE_SNAPSHOTS"); + label = bprintf("((%lu)%s) MC_COMPARE_SNAPSHOTS", req->issuer->pid, host_name); break; default: THROW_UNIMPLEMENTED; } - str = bprintf("label = \"%s\", color = %s", label, colors[req->issuer->pid-1]); + str = bprintf("label = \"%s\", color = %s, fontcolor = %s", label, colors[req->issuer->pid-1], colors[req->issuer->pid-1]); xbt_free(label); return str; -- 2.20.1