Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
model-checker : examples updated with new lex and yacc parsing
[simgrid.git] / examples / msg / mc / test_snapshot.c
1 #include "msg/msg.h"
2 #include "mc/mc.h"
3 #include "xbt/automaton.h"
4 #include "xbt/automatonparse_promela.h"
5 #include "test_snapshot.h"
6 //#include "y.tab.c"
7 #include <stdlib.h>
8
9 XBT_LOG_NEW_DEFAULT_CATEGORY(test_snapshot, "my log messages");
10
11 int r=0; 
12 int cs=0;
13
14 int i = 1;
15 xbt_dynar_t d1 = NULL;
16 xbt_dynar_t d2 = NULL;
17 char *c1;
18
19 int predR(){
20   return r;
21 }
22
23 int predCS(){
24   return cs;
25 }
26
27 void check(){
28   XBT_INFO("*** Check ***"); 
29   if(d1!=NULL){
30     XBT_INFO("Dynar d1 (%p -> %p) length : %lu", &d1, d1, xbt_dynar_length(d1));
31     unsigned int cursor = 0;
32     char *elem;
33     xbt_dynar_foreach(d1, cursor, elem){
34       XBT_INFO("Elem in dynar d1 : %s", elem);
35     }
36   }else{
37     XBT_INFO("Dynar d1 NULL");
38   }
39   if(d2!=NULL){
40     XBT_INFO("Dynar d2 (%p -> %p) length : %lu", &d2, d2, xbt_dynar_length(d2));
41     unsigned int cursor = 0;
42     char *elem;
43     xbt_dynar_foreach(d2, cursor, elem){
44       XBT_INFO("Elem in dynar d2 : %s", elem);
45     }
46   }else{
47     XBT_INFO("Dynar d2 NULL");
48   }
49 }
50
51
52 int coordinator(int argc, char *argv[])
53 {
54
55   while(i>0){
56
57     m_task_t task = NULL;
58     MSG_task_receive(&task, "coordinator");
59     const char *kind = MSG_task_get_name(task);
60
61     //check();
62
63     if (!strcmp(kind, "request")) { 
64       char *req = MSG_task_get_data(task);
65       m_task_t answer = MSG_task_create("received", 0, 1000, NULL);
66       MSG_task_send(answer, req); 
67     }else{
68       XBT_INFO("End of coordinator");
69     }
70
71   }
72
73   return 0;
74 }
75
76 int client(int argc, char *argv[])
77 {
78   int my_pid = MSG_process_get_PID(MSG_process_self());
79
80   char *my_mailbox = bprintf("%s", argv[1]);
81
82   while(i>0){
83
84     XBT_INFO("Ask the request");
85     MSG_task_send(MSG_task_create("request", 0, 1000, my_mailbox), "coordinator");
86
87     r = 1;
88
89     check();
90
91     // wait the answer
92     m_task_t task = NULL;
93     MSG_task_receive(&task, my_mailbox);
94     MSG_task_destroy(task);
95
96     check();
97  
98     XBT_INFO("*** Update ***"); 
99     xbt_dynar_reset(d1);
100     free(c1);
101     xbt_dynar_free(&d1);
102     d2 = xbt_dynar_new(sizeof(char *), NULL);
103     XBT_INFO("Dynar d2 : %p -> %p", &d2, d2);
104     char *c2 = strdup("boooooooo");
105     xbt_dynar_push(d2, &c2);
106
107     cs = 1;
108
109     check();
110  
111     MSG_process_sleep(1);
112     MSG_task_send(MSG_task_create("release", 0, 1000, NULL), "coordinator");
113
114     check();
115
116     MSG_process_sleep(my_pid);
117
118     i--;
119   }
120     
121   return 0;
122 }
123
124 int main(int argc, char *argv[])
125 {
126
127   d1 = xbt_dynar_new(sizeof(char *), NULL);
128   XBT_DEBUG("Dynar d1 : %p -> %p", &d1, d1);
129   c1 = strdup("coucou");
130   xbt_dynar_push(d1, &c1);
131   xbt_dynar_push(d1, &c1);
132
133   init();
134   yyparse();
135   automaton = get_automaton();
136   xbt_new_propositional_symbol(automaton,"r", &predR); 
137   xbt_new_propositional_symbol(automaton,"cs", &predCS); 
138   
139   MSG_global_init(&argc, argv);
140   MSG_create_environment("../msg_platform.xml");
141   MSG_function_register("coordinator", coordinator);
142   MSG_function_register("client", client);
143   MSG_launch_application("deploy_test_snapshot.xml");
144   MSG_main_liveness(automaton);
145
146   return 0;
147 }