From: Marion Guthmuller Date: Thu, 3 Nov 2011 13:37:08 +0000 (+0100) Subject: model-checker: new examples for liveness model checking X-Git-Tag: exp_20120216~133^2~52 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/4680606bad1fe9674554b6238add19de1bf6dde0 model-checker: new examples for liveness model checking --- diff --git a/examples/msg/mc/CMakeLists.txt b/examples/msg/mc/CMakeLists.txt index f330a040e8..40d5fdccad 100644 --- a/examples/msg/mc/CMakeLists.txt +++ b/examples/msg/mc/CMakeLists.txt @@ -11,9 +11,6 @@ add_executable(bugged3 bugged3.c) add_executable(random_test random_test.c) add_executable(example_liveness_without_cycle automaton.c automatonparse_promela.c example_liveness_without_cycle.c) -add_executable(example2_liveness_without_cycle automaton.c -automatonparse_promela.c -example2_liveness_without_cycle.c) add_executable(example_liveness_with_cycle automaton.c automatonparse_promela.c example_liveness_with_cycle.c) @@ -28,5 +25,4 @@ target_link_libraries(bugged2 simgrid m ) target_link_libraries(bugged3 simgrid m ) target_link_libraries(random_test simgrid m ) target_link_libraries(example_liveness_without_cycle simgrid m ) -target_link_libraries(example2_liveness_without_cycle simgrid m ) target_link_libraries(example_liveness_with_cycle simgrid m ) diff --git a/examples/msg/mc/example2_liveness_without_cycle.c b/examples/msg/mc/example2_liveness_without_cycle.c deleted file mode 100644 index a53a5f7056..0000000000 --- a/examples/msg/mc/example2_liveness_without_cycle.c +++ /dev/null @@ -1,111 +0,0 @@ -/**************** Shared buffer between asynchronous receives *****************/ -/* Server process assumes that the data from the second communication comm2 */ -/* will overwrite the one from the first communication, because of the order */ -/* of the wait calls. This is not true because data copy can be triggered by */ -/* a call to wait on the other end of the communication (client). */ -/* NOTE that the communications use different mailboxes, but they share the */ -/* same buffer for reception (task1). */ -/******************************************************************************/ - -#include "xbt/automaton.h" -#include "xbt/automatonparse_promela.h" -#include "example2_liveness_without_cycle.h" -#include "msg/msg.h" -#include "mc/mc.h" - -#include "y.tab.c" - -XBT_LOG_NEW_DEFAULT_CATEGORY(example_liveness_with_cycle, "Example liveness with cycle"); - -extern xbt_automaton_t automaton; - - -int p=0; -int q=0; - - -int predP(){ - return p; -} - - -int predQ(){ - return q; -} - - -int server(int argc, char *argv[]); -int client(int argc, char *argv[]); - -int server(int argc, char *argv[]) -{ - m_task_t task1; - long val1; - msg_comm_t comm1, comm2; - - comm1 = MSG_task_irecv(&task1, "mymailbox1"); - comm2 = MSG_task_irecv(&task1, "mymailbox2"); - MSG_comm_wait(comm1, -1); - MSG_comm_wait(comm2, -1); - - val1 = (long) MSG_task_get_data(task1); - XBT_INFO("Received %lu", val1); - - MC_assert_pair_stateless(val1 == 2); - - /*if(val1 == 2) - q = 1; - else - q = 0;*/ - - //XBT_INFO("q (server) = %d", q); - - XBT_INFO("OK"); - - return 0; -} - -int client(int argc, char *argv[]) -{ - msg_comm_t comm; - char *mbox; - m_task_t task1 = - MSG_task_create("task", 0, 10000, (void *) atol(argv[1])); - - mbox = bprintf("mymailbox%s", argv[1]); - - XBT_INFO("Send %d!", atoi(argv[1])); - comm = MSG_task_isend(task1, mbox); - - MSG_comm_wait(comm, -1); - - xbt_free(mbox); - - return 0; -} - -int main(int argc, char *argv[]) -{ - - init(); - yyparse(); - automaton = get_automaton(); - xbt_new_propositional_symbol(automaton,"p", &predP); - xbt_new_propositional_symbol(automaton,"q", &predQ); - - //display_automaton(); - - MSG_global_init(&argc, argv); - - MSG_create_environment("platform.xml"); - - MSG_function_register("server", server); - - MSG_function_register("client", client); - - MSG_launch_application("deploy_bugged3.xml"); - - MSG_main_liveness_stateless(automaton); - - return 0; -} diff --git a/examples/msg/mc/example2_liveness_without_cycle.h b/examples/msg/mc/example2_liveness_without_cycle.h deleted file mode 100644 index 8363b17426..0000000000 --- a/examples/msg/mc/example2_liveness_without_cycle.h +++ /dev/null @@ -1,14 +0,0 @@ -#ifndef _EXAMPLE2_LIVENESS_WITHOUT_CYCLE_H -#define _EXAMPLE2_LIVENESS_WITHOUT_CYCLE_H - -int yyparse(void); -int yywrap(void); -int yylex(void); - -int predP(void); -int predQ(void); - -int server(int argc, char **argv); -int client(int argc, char **argv); - -#endif diff --git a/examples/msg/mc/example_liveness_with_cycle.c b/examples/msg/mc/example_liveness_with_cycle.c index 17982c053a..58703a15e9 100644 --- a/examples/msg/mc/example_liveness_with_cycle.c +++ b/examples/msg/mc/example_liveness_with_cycle.c @@ -12,10 +12,11 @@ #include "y.tab.c" #define AMOUNT_OF_CLIENTS 2 -#define CS_PER_PROCESS 2 +#define CS_PER_PROCESS 1 XBT_LOG_NEW_DEFAULT_CATEGORY(example_liveness_with_cycle, "my log messages"); + int p=0; int q=0; @@ -47,14 +48,15 @@ int coordinator(int argc, char *argv[]) XBT_INFO("CS already used. Queue the request"); xbt_dynar_push(requests, &req); } else { // can serve it immediatly - XBT_INFO("CS idle. Grant immediatly"); if(strcmp(req, "1") == 0){ m_task_t answer = MSG_task_create("grant", 0, 1000, NULL); MSG_task_send(answer, req); CS_used = 1; + XBT_INFO("CS idle. Grant immediatly"); }else{ m_task_t answer = MSG_task_create("notgrant", 0, 1000, NULL); MSG_task_send(answer, req); + XBT_INFO("CS idle but not grant"); } } } else { // that's a release. Check if someone was waiting for the lock @@ -87,9 +89,11 @@ int client(int argc, char *argv[]) int my_pid = MSG_process_get_PID(MSG_process_self()); // use my pid as name of mailbox to contact me char *my_mailbox = bprintf("%s", argv[1]); - // request the CS 2 times, sleeping a bit in between + // request the CS 3 times, sleeping a bit in between int i; + for (i = 0; i < CS_PER_PROCESS; i++) { + XBT_INFO("Ask the request"); MSG_task_send(MSG_task_create("request", 0, 1000, my_mailbox), "coordinator"); @@ -101,24 +105,27 @@ int client(int argc, char *argv[]) m_task_t grant = NULL; MSG_task_receive(&grant, my_mailbox); const char *kind = MSG_task_get_name(grant); - if(!strcmp(kind, "grant")){ + if(strcmp(kind, "grant") == 0){ if(strcmp(my_mailbox, "2") == 0){ q = 1; p = 0; } - //answers ++; MSG_task_destroy(grant); - XBT_INFO("got the answer. Sleep a bit and release it"); + 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"); } - + MSG_process_sleep(my_pid); + + q=0; + p=0; + } - //XBT_INFO("Got all the CS I wanted (%s), quit now", my_mailbox); + XBT_INFO("Got all the CS I wanted (%s), quit now", my_mailbox); return 0; } diff --git a/examples/msg/mc/example_liveness_without_cycle.c b/examples/msg/mc/example_liveness_without_cycle.c index 11983b9e44..219524b010 100644 --- a/examples/msg/mc/example_liveness_without_cycle.c +++ b/examples/msg/mc/example_liveness_without_cycle.c @@ -12,7 +12,7 @@ XBT_LOG_NEW_DEFAULT_CATEGORY(example_liveness_without_cycle, "Example liveness w extern xbt_automaton_t automaton; -int r=1; +int r=0; int e=1; int d=1;