Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
model-checker : separate informations for safety stateful/stateless and liveness...
[simgrid.git] / 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 }