examples/msg/mc/bugged1.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  m_task_t task = NULL;
  17  int count = 0;
  18  while(count < N){
  19    if(task){
  20      MSG_task_destroy(task);
  21      task = NULL;
  22    }
  23    MSG_task_receive(&task,"mymailbox");
  24    count++;
  25  }
  26  MC_assert(atoi(MSG_task_get_name(task)) == 3);
  27
  28   INFO0("OK");
  29  return 0;
  30 }
  31
  32 int client(int argc,char *argv[]) {
  33
  34  m_task_t task = MSG_task_create(argv[1], 0/*comp cost*/, 10000/*comm size*/, NULL /*arbitrary data*/);
  35
  36  MSG_task_send(task,"mymailbox");
  37
  38  INFO0("Sent!");
  39  return 0;
  40 }
  41
  42 int main(int argc,char*argv[]) {
  43
  44  MSG_global_init(&argc,argv);
  45
  46  MSG_create_environment("platform.xml");
  47
  48  MSG_function_register("server", server);
  49
  50  MSG_function_register("client", client);
  51
  52  MSG_launch_application("deploy_bugged1.xml");
  53
  54  MSG_main();
  55
  56  return 0;
  57
  58 }
  59
  60