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