model-checker: new examples for liveness model checking

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

diff --git a/examples/msg/mc/example_liveness_with_cycle.c b/examples/msg/mc/example_liveness_with_cycle.c
index 09deb12..58703a1 100644 (file)
--- 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;
 }
 
@@ -127,8 +134,8 @@ int main(int argc, char *argv[])
   init();
   yyparse();
   automaton = get_automaton();
-  xbt_propositional_symbol_t ps = xbt_new_propositional_symbol(automaton,"p", &predP); 
-  ps = xbt_new_propositional_symbol(automaton,"q", &predQ); 
+  xbt_new_propositional_symbol(automaton,"p", &predP); 
+  xbt_new_propositional_symbol(automaton,"q", &predQ); 
   
   MSG_global_init(&argc, argv);
   MSG_create_environment("../msg_platform.xml");