examples/msg/mc/bugged2.c

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