examples/msg/mc/example2_liveness_without_cycle.c

   1 /**************** Shared buffer between asynchronous receives *****************/
   2 /* Server process assumes that the data from the second communication comm2   */
   3 /* will overwrite the one from the first communication, because of the order  */
   4 /* of the wait calls. This is not true because data copy can be triggered by  */
   5 /* a call to wait on the other end of the communication (client).             */
   6 /* NOTE that the communications use different mailboxes, but they share the   */
   7 /* same buffer for reception (task1).                                         */
   8 /******************************************************************************/
   9
  10 #include "xbt/automaton.h"
  11 #include "xbt/automatonparse_promela.h"
  12 #include "example2_liveness_without_cycle.h"
  13 #include "msg/msg.h"
  14 #include "mc/mc.h"
  15
  16 #include "y.tab.c"
  17
  18 XBT_LOG_NEW_DEFAULT_CATEGORY(example_liveness_with_cycle, "Example liveness with cycle");
  19
  20 extern xbt_automaton_t automaton;
  21
  22
  23 int p=1;
  24 int q=0;
  25
  26
  27 int predP(){
  28   return p;
  29 }
  30
  31
  32 int predQ(){
  33   return q;
  34 }
  35
  36
  37 int server(int argc, char *argv[]);
  38 int client(int argc, char *argv[]);
  39
  40 int server(int argc, char *argv[])
  41 {
  42   m_task_t task1;
  43   long val1;
  44   msg_comm_t comm1, comm2;
  45
  46   comm1 = MSG_task_irecv(&task1, "mymailbox1");
  47   comm2 = MSG_task_irecv(&task1, "mymailbox2");
  48   MSG_comm_wait(comm1, -1);
  49   MSG_comm_wait(comm2, -1);
  50
  51   val1 = (long) MSG_task_get_data(task1);
  52   XBT_INFO("Received %lu", val1);
  53
  54   //MC_assert_pair_stateless(val1 == 2);
  55
  56   /*if(val1 == 2)
  57     q = 1;
  58   else
  59   q = 0;*/
  60
  61   //XBT_INFO("q (server) = %d", q);
  62
  63   XBT_INFO("OK");
  64
  65   return 0;
  66 }
  67
  68 int client(int argc, char *argv[])
  69 {
  70   msg_comm_t comm;
  71   char *mbox;
  72   m_task_t task1 =
  73       MSG_task_create("task", 0, 10000, (void *) atol(argv[1]));
  74
  75   mbox = bprintf("mymailbox%s", argv[1]);
  76
  77   XBT_INFO("Send %d!", atoi(argv[1]));
  78   comm = MSG_task_isend(task1, mbox);
  79
  80   MSG_comm_wait(comm, -1);
  81
  82   xbt_free(mbox);
  83
  84   return 0;
  85 }
  86
  87 int main(int argc, char *argv[])
  88 {
  89
  90   init();
  91   yyparse();
  92   automaton = get_automaton();
  93   xbt_propositional_symbol_t ps = xbt_new_propositional_symbol(automaton,"p", &predP);
  94   ps = xbt_new_propositional_symbol(automaton,"q", &predQ);
  95
  96   //display_automaton();
  97
  98   MSG_global_init(&argc, argv);
  99
 100   MSG_create_environment("platform.xml");
 101
 102   MSG_function_register("server", server);
 103
 104   MSG_function_register("client", client);
 105
 106   MSG_launch_application("deploy_bugged3.xml");
 107
 108   MSG_main_liveness_stateless(automaton);
 109
 110   return 0;
 111 }