examples/msg/mc/example_automaton.c

   1 #include "xbt/automaton.h"
   2 #include "xbt/automatonparse_promela.h"
   3 #include "example_automaton.h"
   4 #include "msg/msg.h"
   5 #include "mc/mc.h"
   6
   7 #include "y.tab.c"
   8
   9 #define N 3
  10
  11 XBT_LOG_NEW_DEFAULT_CATEGORY(example, "Example with automaton");
  12
  13 extern xbt_automaton_t automaton;
  14
  15
  16 int p=1;
  17 int r=1;
  18 int q=1;
  19 int e=1;
  20 int d=1;
  21
  22
  23 int predP(){
  24   return p;
  25 }
  26
  27 int predR(){
  28   return r;
  29 }
  30
  31 int predQ(){
  32   return q;
  33 }
  34
  35
  36 int predD(){
  37   return d;
  38 }
  39
  40
  41 int predE(){
  42   return e;
  43 }
  44
  45
  46
  47 int server(int argc, char *argv[])
  48 {
  49   m_task_t task = NULL;
  50   int count = 0;
  51   while (count < N) {
  52     if (task) {
  53       MSG_task_destroy(task);
  54       task = NULL;
  55     }
  56     MSG_task_receive(&task, "mymailbox");
  57     count++;
  58     r=(r+1)%2;
  59     //d=(d+1)%2;
  60     //XBT_INFO("r (server) = %d", r);
  61
  62   }
  63   MC_assert_pair(atoi(MSG_task_get_name(task)) == 3);
  64
  65   XBT_INFO("OK");
  66   return 0;
  67 }
  68
  69 int client(int argc, char *argv[])
  70 {
  71
  72   m_task_t task =
  73       MSG_task_create(argv[1], 0 /*comp cost */ , 10000 /*comm size */ ,
  74                       NULL /*arbitrary data */ );
  75
  76   MSG_task_send(task, "mymailbox");
  77
  78   XBT_INFO("Sent!");
  79
  80   //r=(r+1)%3;
  81   //XBT_INFO("r (client) = %d", r);
  82
  83   return 0;
  84 }
  85
  86
  87
  88 int main(int argc, char **argv){
  89   init();
  90   yyparse();
  91   automaton = get_automaton();
  92   xbt_propositional_symbol_t ps = xbt_new_propositional_symbol(automaton,"p", &predP);
  93   ps = xbt_new_propositional_symbol(automaton,"q", &predQ);
  94   ps = xbt_new_propositional_symbol(automaton,"r", &predR);
  95   ps = xbt_new_propositional_symbol(automaton,"e", &predE);
  96   ps = xbt_new_propositional_symbol(automaton,"d", &predD);
  97
  98   //display_automaton();
  99
 100   MSG_global_init(&argc, argv);
 101
 102   MSG_create_environment("platform.xml");
 103
 104   MSG_function_register("server", server);
 105
 106   MSG_function_register("client", client);
 107
 108   MSG_launch_application("deploy_bugged1.xml");
 109
 110   //XBT_INFO("r=%d", r);
 111
 112   MSG_main_with_automaton(automaton);
 113
 114   MSG_clean();
 115
 116   return 0;
 117
 118 }