examples/msg/mc/bugged2.c

   1 #include <msg/msg.h>
   2 #include <mc/modelchecker.h>
   3 #define N 3
   4
   5 XBT_LOG_NEW_DEFAULT_CATEGORY(example,"this example");
   6
   7 int server(int argc,char *argv[]);
   8 int client(int argc,char *argv[]);
   9
  10 int server(int argc,char *argv[])
  11 {
  12   m_task_t task1, task2;
  13   long val1, val2;
  14
  15   MSG_task_receive(&task1,"mymailbox");
  16   val1 = (long)MSG_task_get_data(task1);
  17   INFO1("Received %lu", val1);
  18
  19   MSG_task_receive(&task2,"mymailbox");
  20   val2 = (long)MSG_task_get_data(task2);
  21   INFO1("Received %lu", val2);
  22
  23   MC_assert( min(val1, val2) == 1 );
  24
  25   INFO0("OK");
  26   return 0;
  27 }
  28
  29 int client(int argc,char *argv[])
  30 {
  31   m_task_t task1 = MSG_task_create("task", 0, 10000, (void *) atol(argv[1]));
  32   m_task_t task2 = MSG_task_create("task", 0, 10000, (void *) atol(argv[1]));
  33
  34   INFO1("Send %d!", atoi(argv[1]));
  35   MSG_task_send(task1,"mymailbox");
  36
  37   INFO1("Send %d!", atoi(argv[1]));
  38   MSG_task_send(task2,"mymailbox");
  39
  40   return 0;
  41 }
  42
  43 int main(int argc,char*argv[])
  44 {
  45   MSG_global_init(&argc,argv);
  46
  47   MSG_create_environment("platform.xml");
  48
  49   MSG_function_register("server", server);
  50
  51   MSG_function_register("client", client);
  52
  53   MSG_launch_application("deploy_bugged2.xml");
  54
  55   MSG_main();
  56
  57   return 0;
  58 }