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=0;
  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     //XBT_INFO("r (server) = %d", r);
  60
  61   }
  62   MC_assert_pair_stateful(atoi(MSG_task_get_name(task)) == 3);
  63
  64   XBT_INFO("OK");
  65   return 0;
  66 }
  67
  68 int client(int argc, char *argv[])
  69 {
  70
  71   m_task_t task =
  72       MSG_task_create(argv[1], 0 /*comp cost */ , 10000 /*comm size */ ,
  73                       NULL /*arbitrary data */ );
  74
  75   MSG_task_send(task, "mymailbox");
  76
  77   XBT_INFO("Sent!");
  78
  79   //r=(r+1)%3;
  80   //XBT_INFO("r (client) = %d", r);
  81
  82   return 0;
  83 }
  84
  85
  86
  87 int main(int argc, char **argv){
  88   init();
  89   yyparse();
  90   automaton = get_automaton();
  91   xbt_propositional_symbol_t ps = xbt_new_propositional_symbol(automaton,"p", &predP);
  92   ps = xbt_new_propositional_symbol(automaton,"q", &predQ);
  93   ps = xbt_new_propositional_symbol(automaton,"r", &predR);
  94   ps = xbt_new_propositional_symbol(automaton,"e", &predE);
  95   ps = xbt_new_propositional_symbol(automaton,"d", &predD);
  96
  97   //display_automaton();
  98
  99   MSG_global_init(&argc, argv);
 100
 101   MSG_create_environment("platform.xml");
 102
 103   MSG_function_register("server", server);
 104
 105   MSG_function_register("client", client);
 106
 107   MSG_launch_application("deploy_bugged1.xml");
 108
 109   //XBT_INFO("r=%d", r);
 110
 111   MSG_main_liveness_stateful(automaton);
 112
 113   MSG_clean();
 114
 115   return 0;
 116
 117 }