X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/a28877c438152045726c8882e363ff1422d99280..0c13871d73e933c1847faf8debea7b7745a3ff44:/examples/msg/mc/bugged1_liveness.c diff --git a/examples/msg/mc/bugged1_liveness.c b/examples/msg/mc/bugged1_liveness.c index 672f9a9d42..b646d82179 100644 --- a/examples/msg/mc/bugged1_liveness.c +++ b/examples/msg/mc/bugged1_liveness.c @@ -26,10 +26,10 @@ int predCS(){ int coordinator(int argc, char *argv[]) { - int CS_used = 0; + int CS_used = 0; + msg_task_t task = NULL, answer = NULL; while (1) { - m_task_t task = NULL; MSG_task_receive(&task, "coordinator"); const char *kind = MSG_task_get_name(task); if (!strcmp(kind, "request")) { @@ -39,9 +39,11 @@ int coordinator(int argc, char *argv[]) } else { if(strcmp(req, "2") == 0){ XBT_INFO("CS idle. Grant immediatly"); - m_task_t answer = MSG_task_create("grant", 0, 1000, NULL); + MC_compare(); + answer = MSG_task_create("grant", 0, 1000, NULL); MSG_task_send(answer, req); CS_used = 1; + answer = NULL; } } } else { @@ -49,6 +51,8 @@ int coordinator(int argc, char *argv[]) CS_used = 0; } MSG_task_destroy(task); + task = NULL; + kind = NULL; } return 0; @@ -59,6 +63,7 @@ int client(int argc, char *argv[]) int my_pid = MSG_process_get_PID(MSG_process_self()); char *my_mailbox = bprintf("%s", argv[1]); + msg_task_t grant = NULL, release = NULL; while(1) { @@ -72,8 +77,6 @@ int client(int argc, char *argv[]) XBT_INFO("Propositions changed : r=1, cs=0"); } - - m_task_t grant = NULL; MSG_task_receive(&grant, my_mailbox); const char *kind = MSG_task_get_name(grant); @@ -83,11 +86,18 @@ int client(int argc, char *argv[]) XBT_INFO("Propositions changed : r=0, cs=1"); } - MSG_task_destroy(grant); + grant = NULL; + kind = NULL; + XBT_INFO("%s got the answer. Sleep a bit and release it", argv[1]); + MSG_process_sleep(1); - MSG_task_send(MSG_task_create("release", 0, 1000, NULL), "coordinator"); + + release = MSG_task_create("release", 0, 1000, NULL); + MSG_task_send(release, "coordinator"); + + release = NULL; MSG_process_sleep(my_pid); @@ -107,7 +117,7 @@ int main(int argc, char *argv[]) MSG_init(&argc, argv); - MSG_config("model-check/property","promela1_bugged1_liveness"); + MSG_config("model-check/property","promela_bugged1_liveness"); MC_automaton_new_propositional_symbol("r", &predR); MC_automaton_new_propositional_symbol("cs", &predCS);