examples/msg/mc/test_snapshot.c

   1 #include "msg/msg.h"
   2 #include "mc/mc.h"
   3 #include "xbt/automaton.h"
   4 #include "test_snapshot.h"
   5 //#include "y.tab.c"
   6 #include <stdlib.h>
   7
   8 XBT_LOG_NEW_DEFAULT_CATEGORY(test_snapshot, "my log messages");
   9
  10 int r=0;
  11 int cs=0;
  12
  13 int i = 1;
  14 xbt_dynar_t d1 = NULL;
  15 xbt_dynar_t d2 = NULL;
  16 char *c1;
  17
  18 int predR(){
  19   return r;
  20 }
  21
  22 int predCS(){
  23   return cs;
  24 }
  25
  26 void check(){
  27   XBT_INFO("*** Check ***");
  28   if(d1!=NULL){
  29     XBT_INFO("Dynar d1 (%p -> %p) length : %lu", &d1, d1, xbt_dynar_length(d1));
  30     unsigned int cursor = 0;
  31     char *elem;
  32     xbt_dynar_foreach(d1, cursor, elem){
  33       XBT_INFO("Elem in dynar d1 : %s", elem);
  34     }
  35   }else{
  36     XBT_INFO("Dynar d1 NULL");
  37   }
  38   if(d2!=NULL){
  39     XBT_INFO("Dynar d2 (%p -> %p) length : %lu", &d2, d2, xbt_dynar_length(d2));
  40     unsigned int cursor = 0;
  41     char *elem;
  42     xbt_dynar_foreach(d2, cursor, elem){
  43       XBT_INFO("Elem in dynar d2 : %s", elem);
  44     }
  45   }else{
  46     XBT_INFO("Dynar d2 NULL");
  47   }
  48 }
  49
  50
  51 int coordinator(int argc, char *argv[])
  52 {
  53
  54   while(i>0){
  55
  56     m_task_t task = NULL;
  57     MSG_task_receive(&task, "coordinator");
  58     const char *kind = MSG_task_get_name(task);
  59
  60     //check();
  61
  62     if (!strcmp(kind, "request")) {
  63       char *req = MSG_task_get_data(task);
  64       m_task_t answer = MSG_task_create("received", 0, 1000, NULL);
  65       MSG_task_send(answer, req);
  66     }else{
  67       XBT_INFO("End of coordinator");
  68     }
  69
  70   }
  71
  72   return 0;
  73 }
  74
  75 int client(int argc, char *argv[])
  76 {
  77   int my_pid = MSG_process_get_PID(MSG_process_self());
  78
  79   char *my_mailbox = bprintf("%s", argv[1]);
  80
  81   while(i>0){
  82
  83     XBT_INFO("Ask the request");
  84     MSG_task_send(MSG_task_create("request", 0, 1000, my_mailbox), "coordinator");
  85
  86     r = 1;
  87
  88     check();
  89
  90     // wait the answer
  91     m_task_t task = NULL;
  92     MSG_task_receive(&task, my_mailbox);
  93     MSG_task_destroy(task);
  94
  95     check();
  96
  97     XBT_INFO("*** Update ***");
  98     xbt_dynar_reset(d1);
  99     free(c1);
 100     xbt_dynar_free(&d1);
 101     d2 = xbt_dynar_new(sizeof(char *), NULL);
 102     XBT_INFO("Dynar d2 : %p -> %p", &d2, d2);
 103     char *c2 = strdup("boooooooo");
 104     xbt_dynar_push(d2, &c2);
 105
 106     cs = 1;
 107
 108     check();
 109
 110     MSG_process_sleep(1);
 111     MSG_task_send(MSG_task_create("release", 0, 1000, NULL), "coordinator");
 112
 113     check();
 114
 115     MSG_process_sleep(my_pid);
 116
 117     i--;
 118   }
 119
 120   return 0;
 121 }
 122
 123 int main(int argc, char *argv[]) {
 124
 125   MSG_init(&argc, argv);
 126
 127   d1 = xbt_dynar_new(sizeof(char *), NULL);
 128   XBT_DEBUG("Dynar d1 : %p -> %p", &d1, d1);
 129   c1 = strdup("coucou");
 130   xbt_dynar_push(d1, &c1);
 131   xbt_dynar_push(d1, &c1);
 132
 133   MSG_config("model-check/property","promela_test_snapshot");
 134   MC_automaton_new_propositional_symbol("r", &predR);
 135   MC_automaton_new_propositional_symbol("cs", &predCS);
 136
 137   MSG_create_environment("../msg_platform.xml");
 138   MSG_function_register("coordinator", coordinator);
 139   MSG_function_register("client", client);
 140   MSG_launch_application("deploy_test_snapshot.xml");
 141   MSG_main();
 142
 143   return 0;
 144 }