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 =
  37       MSG_task_create("task", 0, 10000, (void *) atol(argv[1]));
  38   m_task_t task2 =
  39       MSG_task_create("task", 0, 10000, (void *) atol(argv[1]));
  40
  41   INFO1("Send %d!", atoi(argv[1]));
  42   MSG_task_send(task1, "mymailbox");
  43
  44   INFO1("Send %d!", atoi(argv[1]));
  45   MSG_task_send(task2, "mymailbox");
  46
  47   return 0;
  48 }
  49
  50 int main(int argc, char *argv[])
  51 {
  52   MSG_global_init(&argc, argv);
  53
  54   MSG_create_environment("platform.xml");
  55
  56   MSG_function_register("server", server);
  57
  58   MSG_function_register("client", client);
  59
  60   MSG_launch_application("deploy_bugged2.xml");
  61
  62   MSG_main();
  63
  64   return 0;
  65 }