Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
model-checker: sed 's/m_task_t/msg_task_t/g' on MC examples
authorMarion Guthmuller <marion.guthmuller@loria.fr>
Mon, 2 Jul 2012 14:30:53 +0000 (16:30 +0200)
committerMarion Guthmuller <marion.guthmuller@loria.fr>
Mon, 2 Jul 2012 14:30:53 +0000 (16:30 +0200)
examples/msg/mc/bugged1.c
examples/msg/mc/bugged1_liveness.c
examples/msg/mc/bugged2.c
examples/msg/mc/bugged2_liveness.c
examples/msg/mc/bugged3.c
examples/msg/mc/centralized_liveness.c
examples/msg/mc/centralized_liveness_deadlock.c
examples/msg/mc/centralized_mutex.c
examples/msg/mc/test_snapshot.c

index 82bb266..c90257a 100644 (file)
@@ -5,6 +5,7 @@
 
 #include <msg/msg.h>
 #include <simgrid/modelchecker.h>
+
 #define N 3
 
 XBT_LOG_NEW_DEFAULT_CATEGORY(example, "this example");
@@ -14,7 +15,7 @@ int client(int argc, char *argv[]);
 
 int server(int argc, char *argv[])
 {
-  m_task_t task = NULL;
+  msg_task_t task = NULL;
   int count = 0;
   while (count < N) {
     if (task) {
@@ -33,7 +34,7 @@ int server(int argc, char *argv[])
 int client(int argc, char *argv[])
 {
 
-  m_task_t task =
+  msg_task_t task =
       MSG_task_create(argv[1], 0 /*comp cost */ , 10000 /*comm size */ ,
                       NULL /*arbitrary data */ );
 
index 672f9a9..be326e4 100644 (file)
@@ -29,7 +29,7 @@ int coordinator(int argc, char *argv[])
   int CS_used = 0;           
 
   while (1) {
-    m_task_t task = NULL;
+    msg_task_t task = NULL;
     MSG_task_receive(&task, "coordinator");
     const char *kind = MSG_task_get_name(task); 
     if (!strcmp(kind, "request")) {    
@@ -39,7 +39,7 @@ 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);
+          msg_task_t answer = MSG_task_create("grant", 0, 1000, NULL);
           MSG_task_send(answer, req);
           CS_used = 1;
         }
@@ -73,7 +73,7 @@ int client(int argc, char *argv[])
     }
 
 
-    m_task_t grant = NULL;
+    msg_task_t grant = NULL;
     MSG_task_receive(&grant, my_mailbox);
     const char *kind = MSG_task_get_name(grant);
 
index f703ec8..e4c00d2 100644 (file)
@@ -14,8 +14,8 @@ int client(int argc, char *argv[]);
 
 int server(int argc, char *argv[])
 {
-  m_task_t task1 = NULL;
-  m_task_t task2 = NULL;
+  msg_task_t task1 = NULL;
+  msg_task_t task2 = NULL;
   long val1, val2;
 
   MSG_task_receive(&task1, "mymailbox");
@@ -48,9 +48,9 @@ int server(int argc, char *argv[])
 
 int client(int argc, char *argv[])
 {
-  m_task_t task1 =
+  msg_task_t task1 =
       MSG_task_create("task", 0, 10000, (void *) atol(argv[1]));
-  m_task_t task2 =
+  msg_task_t task2 =
       MSG_task_create("task", 0, 10000, (void *) atol(argv[1]));
 
   XBT_INFO("Send %d!", atoi(argv[1]));
index c3337a4..03d9d6c 100644 (file)
@@ -40,29 +40,29 @@ int coordinator(int argc, char *argv[])
   int CS_used = 0;
 
   while(1) {
-    m_task_t task = NULL;
+    msg_task_t task = NULL;
     MSG_task_receive(&task, "coordinator");
     const char *kind = MSG_task_get_name(task);
     if (!strcmp(kind, "request")) {
       char *req = MSG_task_get_data(task);
       if (CS_used) {
-  XBT_INFO("CS already used. Queue the request");
-  xbt_dynar_push(requests, &req);
+        XBT_INFO("CS already used. Queue the request");
+        xbt_dynar_push(requests, &req);
       } else {
-  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");
+        msg_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 {
       if (xbt_dynar_length(requests) > 0) {
-  XBT_INFO("CS release. Grant to queued requests");
-  char *req;
-  xbt_dynar_pop(requests, &req);
-  MSG_task_send(MSG_task_create("grant", 0, 1000, NULL), req);
+        XBT_INFO("CS release. Grant to queued requests");
+        char *req;
+        xbt_dynar_pop(requests, &req);
+        MSG_task_send(MSG_task_create("grant", 0, 1000, NULL), req);
       } else {
-  XBT_INFO("CS_realase, ressource now idle");
-  CS_used = 0;
+        XBT_INFO("CS_realase, ressource now idle");
+        CS_used = 0;
       }
     }
 
@@ -92,7 +92,7 @@ int producer(int argc, char *argv[])
     MSG_task_send(MSG_task_create("request", 0, 1000, my_mailbox), "coordinator");
 
     /* Wait the answer */
-    m_task_t grant = NULL;
+    msg_task_t grant = NULL;
     MSG_task_receive(&grant, my_mailbox);
     MSG_task_destroy(grant);
 
@@ -133,7 +133,7 @@ int consumer(int argc, char *argv[])
     XBT_INFO("cready = 1");
 
     /* Wait the answer */
-    m_task_t grant = NULL;
+    msg_task_t grant = NULL;
     MSG_task_receive(&grant, my_mailbox);
     MSG_task_destroy(grant);
 
index 9e7bdfc..276c4a2 100644 (file)
@@ -17,7 +17,7 @@ int client(int argc, char *argv[]);
 
 int server(int argc, char *argv[])
 {
-  m_task_t task1;
+  msg_task_t task1;
   long val1;
   msg_comm_t comm1, comm2;
 
@@ -39,7 +39,7 @@ int client(int argc, char *argv[])
 {
   msg_comm_t comm;
   char *mbox;
-  m_task_t task1 =
+  msg_task_t task1 =
       MSG_task_create("task", 0, 10000, (void *) atol(argv[1]));
 
   mbox = bprintf("mymailbox%s", argv[1]);
index 3bf3138..46425de 100644 (file)
@@ -25,18 +25,18 @@ int coordinator(int argc, char *argv[])
   int CS_used = 0;              // initially the CS is idle
   
   while (1) {
-    m_task_t task = NULL;
+    msg_task_t task = NULL;
     MSG_task_receive(&task, "coordinator");
     const char *kind = MSG_task_get_name(task); //is it a request or a release?
     if (!strcmp(kind, "request")) {     // that's a request
       char *req = MSG_task_get_data(task);
       if (CS_used) { 
         XBT_INFO("CS already used.");
-        m_task_t answer = MSG_task_create("not grant", 0, 1000, NULL);
+        msg_task_t answer = MSG_task_create("not grant", 0, 1000, NULL);
         MSG_task_send(answer, req);
       } else {                  // can serve it immediatly
         XBT_INFO("CS idle. Grant immediatly");
-        m_task_t answer = MSG_task_create("grant", 0, 1000, NULL);
+        msg_task_t answer = MSG_task_create("grant", 0, 1000, NULL);
         MSG_task_send(answer, req);
         CS_used = 1;
       }
@@ -62,7 +62,7 @@ int client(int argc, char *argv[])
     MSG_task_send(MSG_task_create("request", 0, 1000, my_mailbox),
                   "coordinator");
     // wait the answer
-    m_task_t answer = NULL;
+    msg_task_t answer = NULL;
     MSG_task_receive(&answer, my_mailbox);
 
     kind = MSG_task_get_name(answer);
index b3c9d40..3e3fc3d 100644 (file)
@@ -26,7 +26,7 @@ int coordinator(int argc, char *argv[])
   int CS_used = 0;              // initially the CS is idle
   
   while (1) {
-    m_task_t task = NULL;
+    msg_task_t task = NULL;
     MSG_task_receive(&task, "coordinator");
     const char *kind = MSG_task_get_name(task); //is it a request or a release?
     if (!strcmp(kind, "request")) {     // that's a request
@@ -36,7 +36,7 @@ int coordinator(int argc, char *argv[])
         xbt_dynar_push(requests, &req);
       } else {                  // can serve it immediatly
         XBT_INFO("CS idle. Grant immediatly");
-        m_task_t answer = MSG_task_create("grant", 0, 1000, NULL);
+        msg_task_t answer = MSG_task_create("grant", 0, 1000, NULL);
         MSG_task_send(answer, req);
         CS_used = 1;
       }
@@ -69,7 +69,7 @@ int client(int argc, char *argv[])
     MSG_task_send(MSG_task_create("request", 0, 1000, my_mailbox),
                   "coordinator");
     // wait the answer
-    m_task_t grant = NULL;
+    msg_task_t grant = NULL;
     MSG_task_receive(&grant, my_mailbox);
 
     MSG_task_destroy(grant);
index 7e50729..22d1bea 100644 (file)
@@ -19,7 +19,7 @@ int coordinator(int argc, char *argv[])
   int CS_used = 0;              // initially the CS is idle
   int todo = AMOUNT_OF_CLIENTS * CS_PER_PROCESS;        // amount of releases we are expecting
   while (todo > 0) {
-    m_task_t task = NULL;
+    msg_task_t task = NULL;
     MSG_task_receive(&task, "coordinator");
     const char *kind = MSG_task_get_name(task); //is it a request or a release?
     if (!strcmp(kind, "request")) {     // that's a request
@@ -29,7 +29,7 @@ int coordinator(int argc, char *argv[])
         xbt_dynar_push(requests, &req);
       } else {                  // can serve it immediatly
         XBT_INFO("CS idle. Grant immediatly");
-        m_task_t answer = MSG_task_create("grant", 0, 1000, NULL);
+        msg_task_t answer = MSG_task_create("grant", 0, 1000, NULL);
         MSG_task_send(answer, req);
         CS_used = 1;
       }
@@ -65,7 +65,7 @@ int client(int argc, char *argv[])
     MSG_task_send(MSG_task_create("request", 0, 1000, my_mailbox),
                   "coordinator");
     // wait the answer
-    m_task_t grant = NULL;
+    msg_task_t grant = NULL;
     MSG_task_receive(&grant, my_mailbox);
     MSG_task_destroy(grant);
     XBT_INFO("got the answer. Sleep a bit and release it");
index 32de8df..32b6165 100644 (file)
@@ -53,7 +53,7 @@ int coordinator(int argc, char *argv[])
 
   while(i>0){
 
-    m_task_t task = NULL;
+    msg_task_t task = NULL;
     MSG_task_receive(&task, "coordinator");
     const char *kind = MSG_task_get_name(task);
 
@@ -61,7 +61,7 @@ int coordinator(int argc, char *argv[])
 
     if (!strcmp(kind, "request")) { 
       char *req = MSG_task_get_data(task);
-      m_task_t answer = MSG_task_create("received", 0, 1000, NULL);
+      msg_task_t answer = MSG_task_create("received", 0, 1000, NULL);
       MSG_task_send(answer, req); 
     }else{
       XBT_INFO("End of coordinator");
@@ -88,7 +88,7 @@ int client(int argc, char *argv[])
     check();
 
     // wait the answer
-    m_task_t task = NULL;
+    msg_task_t task = NULL;
     MSG_task_receive(&task, my_mailbox);
     MSG_task_destroy(task);