model-checker : separate bugged1_liveness (deleted) example in two cases : finite...

[simgrid.git] / examples / msg / mc / bugged1_for_liveness.c

diff --git a/examples/msg/mc/bugged1_liveness.c b/examples/msg/mc/bugged1_for_liveness.c
similarity index 91%
rename from examples/msg/mc/bugged1_liveness.c
rename to examples/msg/mc/bugged1_for_liveness.c
index eaeceb4..b45f9ce 100644 (file)
--- a/examples/msg/mc/bugged1_liveness.c
+++ b/examples/msg/mc/bugged1_for_liveness.c
@@ -1,6 +1,6 @@
 /***************** Centralized Mutual Exclusion Algorithm *********************/
 /* This example implements a centralized mutual exclusion algorithm.          */
 /***************** Centralized Mutual Exclusion Algorithm *********************/
 /* This example implements a centralized mutual exclusion algorithm.          */

-/* CS requests of client 2 not satisfied                                      */
+/* CS requests of client 1 not satisfied                                      */

 /* LTL property checked : G(r->F(cs)); (r=request of CS, cs=CS ok)            */
 /******************************************************************************/
 
 /* LTL property checked : G(r->F(cs)); (r=request of CS, cs=CS ok)            */
 /******************************************************************************/
 


@@ -12,7 +12,7 @@
 #include "y.tab.c"
 
 #define AMOUNT_OF_CLIENTS 2
 #include "y.tab.c"
 
 #define AMOUNT_OF_CLIENTS 2

-#define CS_PER_PROCESS 1
+#define CS_PER_PROCESS 2

 
 XBT_LOG_NEW_DEFAULT_CATEGORY(bugged1_liveness, "my log messages");
 
 
 XBT_LOG_NEW_DEFAULT_CATEGORY(bugged1_liveness, "my log messages");
 


@@ -44,7 +44,7 @@ int coordinator(int argc, char *argv[])
         XBT_INFO("CS already used. Queue the request of client %d", atoi(req) +1);
         xbt_dynar_push(requests, &req);
       } else {                  // can serve it immediatly
         XBT_INFO("CS already used. Queue the request of client %d", atoi(req) +1);
         xbt_dynar_push(requests, &req);
       } else {                  // can serve it immediatly

-       if(strcmp(req, "1") == 0){
+       if(strcmp(req, "2") == 0){

          m_task_t answer = MSG_task_create("grant", 0, 1000, NULL);
          MSG_task_send(answer, req);
          CS_used = 1;
          m_task_t answer = MSG_task_create("grant", 0, 1000, NULL);
          MSG_task_send(answer, req);
          CS_used = 1;


@@ -56,7 +56,7 @@ int coordinator(int argc, char *argv[])
         XBT_INFO("CS release. Grant to queued requests (queue size: %lu)", xbt_dynar_length(requests));
         char *req ;
        xbt_dynar_get_cpy(requests, (xbt_dynar_length(requests) - 1), &req);
         XBT_INFO("CS release. Grant to queued requests (queue size: %lu)", xbt_dynar_length(requests));
         char *req ;
        xbt_dynar_get_cpy(requests, (xbt_dynar_length(requests) - 1), &req);

-       if(strcmp(req, "1") == 0){
+       if(strcmp(req, "2") == 0){

          xbt_dynar_pop(requests, &req);
          MSG_task_send(MSG_task_create("grant", 0, 1000, NULL), req);
          todo--;
          xbt_dynar_pop(requests, &req);
          MSG_task_send(MSG_task_create("grant", 0, 1000, NULL), req);
          todo--;


@@ -85,13 +85,13 @@ int client(int argc, char *argv[])
   char *my_mailbox = bprintf("%s", argv[1]);
   int i;
 
   char *my_mailbox = bprintf("%s", argv[1]);
   int i;
 

-  // request the CS 4 times, sleeping a bit in between
+  // request the CS (CS_PER_PROCESS times), sleeping a bit in between

   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");
 
   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");
 

-    if(strcmp(my_mailbox, "2") == 0){
+    if(strcmp(my_mailbox, "1") == 0){

       r = 1;
       cs = 0;
       XBT_DEBUG("Propositions changed : r=1, cs=0");
       r = 1;
       cs = 0;
       XBT_DEBUG("Propositions changed : r=1, cs=0");


@@ -102,7 +102,7 @@ int client(int argc, char *argv[])
     MSG_task_receive(&grant, my_mailbox);
     const char *kind = MSG_task_get_name(grant);
 
     MSG_task_receive(&grant, my_mailbox);
     const char *kind = MSG_task_get_name(grant);
 

-    if((strcmp(my_mailbox, "2") == 0) && (strcmp("grant", kind) == 0)){
+    if((strcmp(my_mailbox, "1") == 0) && (strcmp("grant", kind) == 0)){

       cs = 1;
       r = 0;
       XBT_DEBUG("Propositions changed : r=0, cs=1");
       cs = 1;
       r = 0;
       XBT_DEBUG("Propositions changed : r=0, cs=1");


@@ -116,7 +116,7 @@ int client(int argc, char *argv[])
 
     MSG_process_sleep(my_pid);
     
 
     MSG_process_sleep(my_pid);
     

-    if(strcmp(my_mailbox, "2") == 0){
+    if(strcmp(my_mailbox, "1") == 0){

       cs=0;
       r=0;
       XBT_DEBUG("Propositions changed : r=0, cs=0");
       cs=0;
       r=0;
       XBT_DEBUG("Propositions changed : r=0, cs=0");