1 /***** ltl2ba : alternating.c *****/
2
3 /* Written by Denis Oddoux, LIAFA, France */
4 /* Copyright (c) 2001 Denis Oddoux */
5 /* Modified by Paul Gastin, LSV, France */
6 /* Copyright (c) 2007 Paul Gastin */
7 /* */
8 /* This program is free software; you can redistribute it and/or modify */
9 /* it under the terms of the GNU General Public License as published by */
10 /* the Free Software Foundation; either version 2 of the License, or */
11 /* (at your option) any later version. */
12 /* */
13 /* This program is distributed in the hope that it will be useful, */
14 /* but WITHOUT ANY WARRANTY; without even the implied warranty of */
15 /* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */
16 /* GNU General Public License for more details. */
17 /* */
18 /* You should have received a copy of the GNU General Public License */
19 /* along with this program; if not, write to the Free Software */
20 /* Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA*/
21 /* */
22 /* Based on the translation algorithm by Gastin and Oddoux, */
23 /* presented at the 13th International Conference on Computer Aided */
24 /* Verification, CAV 2001, Paris, France. */
25 /* Proceedings - LNCS 2102, pp. 53-65 */
26 /* */
27 /* Send bug-reports and/or questions to Paul Gastin */
28 /* http://www.lsv.ens-cachan.fr/~gastin */
29
30 #include "ltl2ba.h"
31
32 /********************************************************************\
33 |* Structures and shared variables *|
34 \********************************************************************/
35
36 extern FILE *tl_out;
37 extern int tl_verbose, tl_stats, tl_simp_diff;
38
39 Node **label;
40 char **sym_table;
41 ATrans **transition;
42 struct rusage tr_debut, tr_fin;
43 struct timeval t_diff;
44 int *final_set, node_id = 1, sym_id = 0, node_size, sym_size;
45 int astate_count = 0, atrans_count = 0;
46
47 ATrans *build_alternating(Node *p);
48
49 /********************************************************************\
50 |* Generation of the alternating automaton *|
51 \********************************************************************/
52
calculate_node_size(Node * p)53 int calculate_node_size(Node *p) /* returns the number of temporal nodes */
54 {
55 switch(p->ntyp) {
56 case AND:
57 case OR:
58 case U_OPER:
59 case V_OPER:
60 return(calculate_node_size(p->lft) + calculate_node_size(p->rgt) + 1);
61 #ifdef NXT
62 case NEXT:
63 return(calculate_node_size(p->lft) + 1);
64 #endif
65 default:
66 return 1;
67 break;
68 }
69 }
70
calculate_sym_size(Node * p)71 int calculate_sym_size(Node *p) /* returns the number of predicates */
72 {
73 switch(p->ntyp) {
74 case AND:
75 case OR:
76 case U_OPER:
77 case V_OPER:
78 return(calculate_sym_size(p->lft) + calculate_sym_size(p->rgt));
79 #ifdef NXT
80 case NEXT:
81 return(calculate_sym_size(p->lft));
82 #endif
83 case NOT:
84 case PREDICATE:
85 return 1;
86 default:
87 return 0;
88 }
89 }
90
dup_trans(ATrans * trans)91 ATrans *dup_trans(ATrans *trans) /* returns the copy of a transition */
92 {
93 ATrans *result;
94 if(!trans) return trans;
95 result = emalloc_atrans();
96 copy_set(trans->to, result->to, 0);
97 copy_set(trans->pos, result->pos, 1);
98 copy_set(trans->neg, result->neg, 1);
99 return result;
100 }
101
do_merge_trans(ATrans ** result,ATrans * trans1,ATrans * trans2)102 void do_merge_trans(ATrans **result, ATrans *trans1, ATrans *trans2)
103 { /* merges two transitions */
104 if(!trans1 || !trans2) {
105 free_atrans(*result, 0);
106 *result = (ATrans *)0;
107 return;
108 }
109 if(!*result)
110 *result = emalloc_atrans();
111 do_merge_sets((*result)->to, trans1->to, trans2->to, 0);
112 do_merge_sets((*result)->pos, trans1->pos, trans2->pos, 1);
113 do_merge_sets((*result)->neg, trans1->neg, trans2->neg, 1);
114 if(!empty_intersect_sets((*result)->pos, (*result)->neg, 1)) {
115 free_atrans(*result, 0);
116 *result = (ATrans *)0;
117 }
118 }
119
merge_trans(ATrans * trans1,ATrans * trans2)120 ATrans *merge_trans(ATrans *trans1, ATrans *trans2) /* merges two transitions */
121 {
122 ATrans *result = emalloc_atrans();
123 do_merge_trans(&result, trans1, trans2);
124 return result;
125 }
126
already_done(Node * p)127 int already_done(Node *p) /* finds the id of the node, if already explored */
128 {
129 int i;
130 for(i = 1; i<node_id; i++)
131 if (isequal(p, label[i]))
132 return i;
133 return -1;
134 }
135
get_sym_id(char * s)136 int get_sym_id(char *s) /* finds the id of a predicate, or attributes one */
137 {
138 int i;
139 for(i=0; i<sym_id; i++)
140 if (!strcmp(s, sym_table[i]))
141 return i;
142 sym_table[sym_id] = s;
143 return sym_id++;
144 }
145
boolean(Node * p)146 ATrans *boolean(Node *p) /* computes the transitions to boolean nodes -> next & init */
147 {
148 ATrans *t1, *t2, *lft, *rgt, *result = (ATrans *)0;
149 switch(p->ntyp) {
150 case TRUE:
151 result = emalloc_atrans();
152 clear_set(result->to, 0);
153 clear_set(result->pos, 1);
154 clear_set(result->neg, 1);
155 case FALSE:
156 break;
157 case AND:
158 lft = boolean(p->lft);
159 rgt = boolean(p->rgt);
160 for(t1 = lft; t1; t1 = t1->nxt) {
161 for(t2 = rgt; t2; t2 = t2->nxt) {
162 ATrans *tmp = merge_trans(t1, t2);
163 if(tmp) {
164 tmp->nxt = result;
165 result = tmp;
166 }
167 }
168 }
169 free_atrans(lft, 1);
170 free_atrans(rgt, 1);
171 break;
172 case OR:
173 lft = boolean(p->lft);
174 for(t1 = lft; t1; t1 = t1->nxt) {
175 ATrans *tmp = dup_trans(t1);
176 tmp->nxt = result;
177 result = tmp;
178 }
179 free_atrans(lft, 1);
180 rgt = boolean(p->rgt);
181 for(t1 = rgt; t1; t1 = t1->nxt) {
182 ATrans *tmp = dup_trans(t1);
183 tmp->nxt = result;
184 result = tmp;
185 }
186 free_atrans(rgt, 1);
187 break;
188 default:
189 build_alternating(p);
190 result = emalloc_atrans();
191 clear_set(result->to, 0);
192 clear_set(result->pos, 1);
193 clear_set(result->neg, 1);
194 add_set(result->to, already_done(p));
195 }
196 return result;
197 }
198
build_alternating(Node * p)199 ATrans *build_alternating(Node *p) /* builds an alternating automaton for p */
200 {
201 ATrans *t1, *t2, *t = (ATrans *)0;
202 int node = already_done(p);
203 if(node >= 0) return transition[node];
204
205 switch (p->ntyp) {
206
207 case TRUE:
208 t = emalloc_atrans();
209 clear_set(t->to, 0);
210 clear_set(t->pos, 1);
211 clear_set(t->neg, 1);
212 case FALSE:
213 break;
214
215 case PREDICATE:
216 t = emalloc_atrans();
217 clear_set(t->to, 0);
218 clear_set(t->pos, 1);
219 clear_set(t->neg, 1);
220 add_set(t->pos, get_sym_id(p->sym->name));
221 break;
222
223 case NOT:
224 t = emalloc_atrans();
225 clear_set(t->to, 0);
226 clear_set(t->pos, 1);
227 clear_set(t->neg, 1);
228 add_set(t->neg, get_sym_id(p->lft->sym->name));
229 break;
230
231 #ifdef NXT
232 case NEXT:
233 t = boolean(p->lft);
234 break;
235 #endif
236
237 case U_OPER: /* p U q <-> q || (p && X (p U q)) */
238 for(t2 = build_alternating(p->rgt); t2; t2 = t2->nxt) {
239 ATrans *tmp = dup_trans(t2); /* q */
240 tmp->nxt = t;
241 t = tmp;
242 }
243 for(t1 = build_alternating(p->lft); t1; t1 = t1->nxt) {
244 ATrans *tmp = dup_trans(t1); /* p */
245 add_set(tmp->to, node_id); /* X (p U q) */
246 tmp->nxt = t;
247 t = tmp;
248 }
249 add_set(final_set, node_id);
250 break;
251
252 case V_OPER: /* p V q <-> (p && q) || (p && X (p V q)) */
253 for(t1 = build_alternating(p->rgt); t1; t1 = t1->nxt) {
254 ATrans *tmp;
255
256 for(t2 = build_alternating(p->lft); t2; t2 = t2->nxt) {
257 tmp = merge_trans(t1, t2); /* p && q */
258 if(tmp) {
259 tmp->nxt = t;
260 t = tmp;
261 }
262 }
263
264 tmp = dup_trans(t1); /* p */
265 add_set(tmp->to, node_id); /* X (p V q) */
266 tmp->nxt = t;
267 t = tmp;
268 }
269 break;
270
271 case AND:
272 t = (ATrans *)0;
273 for(t1 = build_alternating(p->lft); t1; t1 = t1->nxt) {
274 for(t2 = build_alternating(p->rgt); t2; t2 = t2->nxt) {
275 ATrans *tmp = merge_trans(t1, t2);
276 if(tmp) {
277 tmp->nxt = t;
278 t = tmp;
279 }
280 }
281 }
282 break;
283
284 case OR:
285 t = (ATrans *)0;
286 for(t1 = build_alternating(p->lft); t1; t1 = t1->nxt) {
287 ATrans *tmp = dup_trans(t1);
288 tmp->nxt = t;
289 t = tmp;
290 }
291 for(t1 = build_alternating(p->rgt); t1; t1 = t1->nxt) {
292 ATrans *tmp = dup_trans(t1);
293 tmp->nxt = t;
294 t = tmp;
295 }
296 break;
297
298 default:
299 break;
300 }
301
302 transition[node_id] = t;
303 label[node_id++] = p;
304 return(t);
305 }
306
307 /********************************************************************\
308 |* Simplification of the alternating automaton *|
309 \********************************************************************/
310
simplify_atrans(ATrans ** trans)311 void simplify_atrans(ATrans **trans) /* simplifies the transitions */
312 {
313 ATrans *t, *father = (ATrans *)0;
314 for(t = *trans; t;) {
315 ATrans *t1;
316 for(t1 = *trans; t1; t1 = t1->nxt) {
317 if((t1 != t) &&
318 included_set(t1->to, t->to, 0) &&
319 included_set(t1->pos, t->pos, 1) &&
320 included_set(t1->neg, t->neg, 1))
321 break;
322 }
323 if(t1) {
324 if (father)
325 father->nxt = t->nxt;
326 else
327 *trans = t->nxt;
328 free_atrans(t, 0);
329 if (father)
330 t = father->nxt;
331 else
332 t = *trans;
333 continue;
334 }
335 atrans_count++;
336 father = t;
337 t = t->nxt;
338 }
339 }
340
simplify_astates()341 void simplify_astates() /* simplifies the alternating automaton */
342 {
343 ATrans *t;
344 int i, *acc = make_set(-1, 0); /* no state is accessible initially */
345
346 for(t = transition[0]; t; t = t->nxt, i = 0)
347 merge_sets(acc, t->to, 0); /* all initial states are accessible */
348
349 for(i = node_id - 1; i > 0; i--) {
350 if (!in_set(acc, i)) { /* frees unaccessible states */
351 label[i] = ZN;
352 free_atrans(transition[i], 1);
353 transition[i] = (ATrans *)0;
354 continue;
355 }
356 astate_count++;
357 simplify_atrans(&transition[i]);
358 for(t = transition[i]; t; t = t->nxt)
359 merge_sets(acc, t->to, 0);
360 }
361
362 tfree(acc);
363 }
364
365 /********************************************************************\
366 |* Display of the alternating automaton *|
367 \********************************************************************/
368
print_alternating()369 void print_alternating() /* dumps the alternating automaton */
370 {
371 int i;
372 ATrans *t;
373
374 fprintf(tl_out, "init :\n");
375 for(t = transition[0]; t; t = t->nxt) {
376 print_set(t->to, 0);
377 fprintf(tl_out, "\n");
378 }
379
380 for(i = node_id - 1; i > 0; i--) {
381 if(!label[i])
382 continue;
383 fprintf(tl_out, "state %i : ", i);
384 dump(label[i]);
385 fprintf(tl_out, "\n");
386 for(t = transition[i]; t; t = t->nxt) {
387 if (empty_set(t->pos, 1) && empty_set(t->neg, 1))
388 fprintf(tl_out, "1");
389 print_set(t->pos, 1);
390 if (!empty_set(t->pos,1) && !empty_set(t->neg,1)) fprintf(tl_out, " & ");
391 print_set(t->neg, 2);
392 fprintf(tl_out, " -> ");
393 print_set(t->to, 0);
394 fprintf(tl_out, "\n");
395 }
396 }
397 }
398
399 /********************************************************************\
400 |* Main method *|
401 \********************************************************************/
402
mk_alternating(Node * p)403 void mk_alternating(Node *p) /* generates an alternating automaton for p */
404 {
405 if(tl_stats) getrusage(RUSAGE_SELF, &tr_debut);
406
407 node_size = calculate_node_size(p) + 1; /* number of states in the automaton */
408 label = (Node **) tl_emalloc(node_size * sizeof(Node *));
409 transition = (ATrans **) tl_emalloc(node_size * sizeof(ATrans *));
410 node_size = node_size / (8 * sizeof(int)) + 1;
411
412 sym_size = calculate_sym_size(p); /* number of predicates */
413 if(sym_size) sym_table = (char **) tl_emalloc(sym_size * sizeof(char *));
414 sym_size = sym_size / (8 * sizeof(int)) + 1;
415
416 final_set = make_set(-1, 0);
417 transition[0] = boolean(p); /* generates the alternating automaton */
418
419 if(tl_verbose) {
420 fprintf(tl_out, "\nAlternating automaton before simplification\n");
421 print_alternating();
422 }
423
424 if(tl_simp_diff) {
425 simplify_astates(); /* keeps only accessible states */
426 if(tl_verbose) {
427 fprintf(tl_out, "\nAlternating automaton after simplification\n");
428 print_alternating();
429 }
430 }
431
432 if(tl_stats) {
433 getrusage(RUSAGE_SELF, &tr_fin);
434 timeval_subtract (&t_diff, &tr_fin.ru_utime, &tr_debut.ru_utime);
435 fprintf(tl_out, "\nBuilding and simplification of the alternating automaton: %ld.%06lis",
436 t_diff.tv_sec, t_diff.tv_usec);
437 fprintf(tl_out, "\n%i states, %i transitions\n", astate_count, atrans_count);
438 }
439
440 releasenode(1, p);
441 tfree(label);
442 }
443