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 d=1;
  17 int r=1;
  18 int e=1;
  19
  20 int predD(){
  21   return d;
  22 }
  23
  24 int predR(){
  25   return r;
  26 }
  27
  28 int predE(){
  29   return e;
  30 }
  31
  32 int server(int argc, char *argv[])
  33 {
  34   m_task_t task = NULL;
  35   int count = 0;
  36   while (count < N) {
  37     if (task) {
  38       MSG_task_destroy(task);
  39       task = NULL;
  40     }
  41     MSG_task_receive(&task, "mymailbox");
  42     count++;
  43     r++;
  44     r=r%2;
  45   }
  46   MC_assert(atoi(MSG_task_get_name(task)) == 3);
  47
  48   XBT_INFO("OK");
  49   return 0;
  50 }
  51
  52 int client(int argc, char *argv[])
  53 {
  54
  55   m_task_t task =
  56       MSG_task_create(argv[1], 0 /*comp cost */ , 10000 /*comm size */ ,
  57                       NULL /*arbitrary data */ );
  58
  59   MSG_task_send(task, "mymailbox");
  60
  61   XBT_INFO("Sent!");
  62   return 0;
  63 }
  64
  65
  66
  67 int main(int argc, char **argv){
  68   init();
  69   yyparse();
  70   automaton = get_automaton();
  71   xbt_propositional_symbol_t ps = xbt_new_propositional_symbol(automaton,"d", &predD);
  72   ps = xbt_new_propositional_symbol(automaton,"e", &predE);
  73   ps = xbt_new_propositional_symbol(automaton,"r", &predR);
  74
  75   //display_automaton();
  76
  77   MSG_global_init(&argc, argv);
  78
  79   MSG_create_environment("platform.xml");
  80
  81   MSG_function_register("server", server);
  82
  83   MSG_function_register("client", client);
  84
  85   MSG_launch_application("deploy_bugged1.xml");
  86
  87   MSG_main_with_automaton(automaton);
  88
  89   MSG_clean();
  90
  91   return 0;
  92
  93 }