examples/msg/mc/example_liveness_without_cycle.c

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