examples/msg/mc/bugged2_liveness.c

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