examples/msg/mc/bugged2_liveness.c

   1 /***************** Producer/Consumer Algorithm *************************/
   2 /* This example implements a producer/consumer algorithm.              */
   3 /* If consumer work before producer, message is empty                  */
   4 /* LTL property checked : GF((pready U produce) -> (cready U consume)) */
   5 /* (pready = producer got CS, produce=message pushed in the buffer)    */
   6 /* (cready = consumer got CS, consume=message display by consumer)     */
   7 /***********************************************************************/
   8
   9
  10 #include "msg/msg.h"
  11 #include "mc/mc.h"
  12 #include "xbt/automaton.h"
  13 #include "xbt/automatonparse_promela.h"
  14 #include "bugged2_liveness.h"
  15 #include "y.tab.c"
  16
  17 XBT_LOG_NEW_DEFAULT_CATEGORY(example_liveness_with_cycle, "my log messages");
  18
  19 char* buffer;
  20
  21 int consume = 0;
  22 int produce = 0;
  23 int cready = 0;
  24 int pready = 0;
  25
  26 int predPready(){
  27   return pready;
  28 }
  29
  30 int predCready(){
  31   return cready;
  32 }
  33
  34 int predConsume(){
  35   return consume;
  36 }
  37
  38 int predProduce(){
  39   return produce;
  40 }
  41
  42 int coordinator(int argc, char *argv[])
  43 {
  44   xbt_dynar_t requests = xbt_dynar_new(sizeof(char *), NULL);
  45   int CS_used = 0;
  46
  47   while(1) {
  48     m_task_t task = NULL;
  49     MSG_task_receive(&task, "coordinator");
  50     const char *kind = MSG_task_get_name(task);
  51     if (!strcmp(kind, "request")) {
  52       char *req = MSG_task_get_data(task);
  53       if (CS_used) {
  54         XBT_INFO("CS already used. Queue the request");
  55         xbt_dynar_push(requests, &req);
  56       } else {
  57         m_task_t answer = MSG_task_create("grant", 0, 1000, NULL);
  58         MSG_task_send(answer, req);
  59         CS_used = 1;
  60         XBT_INFO("CS idle. Grant immediatly");
  61       }
  62     } else {
  63       if (xbt_dynar_length(requests) > 0) {
  64         XBT_INFO("CS release. Grant to queued requests");
  65         char *req;
  66         xbt_dynar_pop(requests, &req);
  67         MSG_task_send(MSG_task_create("grant", 0, 1000, NULL), req);
  68       } else {
  69         XBT_INFO("CS_realase, ressource now idle");
  70         CS_used = 0;
  71       }
  72     }
  73
  74     MSG_task_destroy(task);
  75
  76   }
  77
  78   return 0;
  79
  80 }
  81
  82 int producer(int argc, char *argv[])
  83 {
  84
  85   char * my_mailbox = bprintf("%s", argv[1]);
  86
  87   //while(1) {
  88
  89     /* Create message */
  90     const char *mess = "message";
  91
  92     /* CS request */
  93     XBT_INFO("Producer ask the request");
  94     MSG_task_send(MSG_task_create("request", 0, 1000, my_mailbox), "coordinator");
  95
  96     /* Wait the answer */
  97     m_task_t grant = NULL;
  98     MSG_task_receive(&grant, my_mailbox);
  99     MSG_task_destroy(grant);
 100
 101     pready = 1;
 102
 103     /* Push message (size of buffer = 1) */
 104     buffer = strdup(mess);
 105
 106     /* CS release */
 107     MSG_task_send(MSG_task_create("release", 0, 1000, my_mailbox), "coordinator");
 108
 109     produce = 1;
 110     pready = 0;
 111
 112     //produce = 0;
 113     //pready = 0;
 114
 115     //}
 116
 117   return 0;
 118
 119 }
 120
 121 int consumer(int argc, char *argv[])
 122 {
 123
 124   char * my_mailbox = bprintf("%s", argv[1]);
 125   char *mess;
 126
 127
 128   //while(1) {
 129
 130     /* CS request */
 131     XBT_INFO("Consumer ask the request");
 132     MSG_task_send(MSG_task_create("request", 0, 1000, my_mailbox), "coordinator");
 133
 134     /* Wait the answer */
 135     m_task_t grant = NULL;
 136     MSG_task_receive(&grant, my_mailbox);
 137     MSG_task_destroy(grant);
 138
 139     cready = 1;
 140
 141     /* Pop message  */
 142     mess = malloc(8*sizeof(char));
 143     mess = strdup(buffer);
 144     buffer[0] = '\0';
 145
 146     /* CS release */
 147     MSG_task_send(MSG_task_create("release", 0, 1000, my_mailbox), "coordinator");
 148
 149     /* Display message */
 150     XBT_INFO("Message : %s", mess);
 151     if(strcmp(mess, "") != 0)
 152       consume = 1;
 153
 154     cready = 0;
 155
 156     free(mess);
 157
 158     //consume = 0;
 159     //cready = 0;
 160
 161     //}
 162
 163   return 0;
 164
 165 }
 166
 167
 168 int main(int argc, char *argv[])
 169 {
 170
 171   buffer = malloc(8*sizeof(char));
 172   buffer[0]='\0';
 173
 174   init();
 175   yyparse();
 176   automaton = get_automaton();
 177   xbt_new_propositional_symbol(automaton,"pready", &predPready);
 178   xbt_new_propositional_symbol(automaton,"cready", &predCready);
 179   xbt_new_propositional_symbol(automaton,"consume", &predConsume);
 180   xbt_new_propositional_symbol(automaton,"produce", &predProduce);
 181
 182   MSG_global_init(&argc, argv);
 183   MSG_create_environment("../msg_platform.xml");
 184   MSG_function_register("coordinator", coordinator);
 185   MSG_function_register("consumer", consumer);
 186   MSG_function_register("producer", producer);
 187   MSG_launch_application("deploy_bugged2_liveness.xml");
 188   MSG_main_liveness(automaton, argv[0]);
 189
 190   return 0;
 191
 192 }