1 /* file fsalogic.c 2. 11. 94.
2 * 9/2/98 - introduced function fsa_concat to concatenate the languages of
3 * two fsa's and fsa_star for starred language.
4 * 31/12/98 - adapt fsa_binop to deal with case in which first
5 * argument has type labeled. The output fsa acquires the same labels.
6 * Introduced new function fsa_laband to access this.
7 * 13/1/98 - changes for `gen' type of generator replacing char.
8 * 18.11.94. - added fsa_and_not
9 * This file contains routines for performing logical operations on
10 * finite state automata.
11 * The functions in this file currently only deal with deterministic fsa's
12 *
13 * The general methodology of some functions in this file, such as
14 * fsa_and, fsa_or and fsa_exists, and of several functions in different files
15 * is as follows.
16 * These functions construct a particular finite state automaton, of which
17 * the states are some kind of sets of states of the input automata,
18 * and the transition table is generated in order.
19 * The states are stored as records in a hash-table, so that they can be
20 * located easily.
21 * The initial state is constructed by hand and numbered 1, and then the
22 * transitions from each state are generated in order. If a new state is
23 * generated as target of a transition, then it is added to the end of the
24 * list of states. Eventually the process will terminate when the table closes,
25 * and all transitions have been generated from each state.
26 * The transitions from a particular state will not be needed again until
27 * the generation process is complete, and so they are output(in unformatted
28 * form) to a file (with name tempfilename).
29 * When the table is complete, the hash-table data can normally be discarded
30 * (once it has been used to identify accept-states in the constructed fsa),
31 * and then the transition table can be read back in.
32 * There is also an option to clear the space taken by the input automata
33 * before re-reading.
34 * This results in saving of core memory, because the transition table of
35 * the fsa being constructed and the data in the hash-table are never held
36 * in main memory at the same time.
37 */
38
39 #include <stdio.h>
40 #include "defs.h"
41 #include "fsa.h"
42 #include "hash.h"
43 #include "externals.h"
44
45 typedef enum { AND, OR, AND_NOT } kbm_binop;
46
47 static fsa *fsa_binop(fsa *fsaptr1, fsa *fsaptr2, storage_type op_table_type,
48 boolean destroy, char *tempfilename, kbm_binop op,
49 boolean labels);
50
51 static fsa *fsa_exists_short(fsa *fsaptr, storage_type op_table_type,
52 boolean destroy, char *tempfilename);
53
54 static fsa *fsa_exists_int(fsa *fsaptr, storage_type op_table_type,
55 boolean destroy, char *tempfilename);
56
57
58 /* Test equality of set records *srptr1 and *srptr2 */
srec_equal(srec * srptr1,srec * srptr2)59 boolean srec_equal(srec *srptr1, srec *srptr2)
60 {
61 int i, j, l, *il1, *il2;
62 if (srptr1->type != srptr2->type)
63 return FALSE;
64 if (srptr1->size != srptr2->size)
65 return FALSE;
66 if (srptr1->type == IDENTIFIERS || srptr1->type == STRINGS) {
67 for (i = 1; i <= srptr1->size; i++)
68 if (strcmp(srptr1->names[i], srptr2->names[i]))
69 return FALSE;
70 }
71 else if (srptr1->type == WORDS) {
72 for (i = 1; i <= srptr1->size; i++)
73 if (genstrcmp(srptr1->words[i], srptr2->words[i]))
74 return FALSE;
75 }
76 else if (srptr1->type == LISTOFWORDS) {
77 for (i = 1; i <= srptr1->size; i++) {
78 j = 0;
79 while (srptr1->wordslist[i][j]) {
80 if (!srptr2->wordslist[i][j])
81 return FALSE;
82 if (genstrcmp(srptr1->wordslist[i][j], srptr2->wordslist[i][j]))
83 return FALSE;
84 j++;
85 }
86 if (srptr2->wordslist[i][j])
87 return FALSE;
88 }
89 }
90 else if (srptr1->type == LISTOFINTS) {
91 for (i = 1; i <= srptr1->size; i++) {
92 il1 = srptr1->intlist[i];
93 il2 = srptr2->intlist[i];
94 l = il1[0];
95 for (j = 0; j <= l; j++)
96 if (il1[j] != il2[j])
97 return FALSE;
98 }
99 }
100 if (srptr1->type == WORDS || srptr1->type == LISTOFWORDS) {
101 for (i = 1; i <= srptr1->alphabet_size; i++)
102 if (strcmp(srptr1->alphabet[i], srptr2->alphabet[i]))
103 return FALSE;
104 }
105 if (srptr1->type == PRODUCT) {
106 if (!srec_equal(srptr1->base, srptr2->base))
107 return FALSE;
108 if (srptr1->arity != srptr2->arity)
109 return FALSE;
110 if (srptr1->padding != srptr2->padding)
111 return FALSE;
112 }
113
114 return TRUE;
115 }
116
117 /* Test equality of the transition tables *tableptr1 and *tableptr2.
118 * The storage-types don't need to be equal.
119 */
table_equal(table_struc * tableptr1,table_struc * tableptr2,int ne,int ns)120 boolean table_equal(table_struc *tableptr1, table_struc *tableptr2, int ne,
121 int ns)
122 {
123 int **table1, **table2, i, j, dr1, dr2;
124 boolean dense1, dense2;
125
126 dense1 = tableptr1->table_type == DENSE;
127 dense2 = tableptr2->table_type == DENSE;
128 table1 = tableptr1->table_data_ptr;
129 table2 = tableptr2->table_data_ptr;
130 dr1 = tableptr1->denserows;
131 dr2 = tableptr2->denserows;
132
133 for (j = 1; j <= ne; j++)
134 for (i = 1; i <= ns; i++)
135 if (target(dense1, table1, j, i, dr1) !=
136 target(dense2, table2, j, i, dr2))
137 return FALSE;
138
139 return TRUE;
140 }
141
142 /* Test equality of the fsa's fsaptr1 and fsaptr2 */
fsa_equal(fsa * fsaptr1,fsa * fsaptr2)143 boolean fsa_equal(fsa *fsaptr1, fsa *fsaptr2)
144 {
145 int ns, ne, ni, na, i;
146
147 if (kbm_print_level >= 3)
148 printf(" #Calling fsa_equal.\n");
149 if (!srec_equal(fsaptr1->alphabet, fsaptr2->alphabet))
150 return FALSE;
151
152 if (!srec_equal(fsaptr1->states, fsaptr2->states))
153 return FALSE;
154
155 ns = fsaptr1->states->size;
156 ne = fsaptr1->alphabet->size;
157
158 if (fsaptr1->num_initial != fsaptr2->num_initial)
159 return FALSE;
160 ni = fsaptr1->num_initial;
161 if (ni > 0 && ni < ns) {
162 fsa_set_is_initial(fsaptr1);
163 fsa_set_is_initial(fsaptr2);
164 for (i = 1; i <= ns; i++)
165 if (fsaptr1->is_initial[i] != fsaptr2->is_initial[i])
166 return FALSE;
167 tfree(fsaptr1->is_initial);
168 tfree(fsaptr2->is_initial);
169 }
170
171 if (fsaptr1->num_accepting != fsaptr2->num_accepting)
172 return FALSE;
173 na = fsaptr1->num_accepting;
174 if (na > 0 && na < ns) {
175 fsa_set_is_accepting(fsaptr1);
176 fsa_set_is_accepting(fsaptr2);
177 for (i = 1; i <= ns; i++)
178 if (fsaptr1->is_accepting[i] != fsaptr2->is_accepting[i])
179 return FALSE;
180 tfree(fsaptr1->is_accepting);
181 tfree(fsaptr2->is_accepting);
182 }
183
184 /* The flag strings are additional information, and needn't correspond */
185
186 if (!table_equal(fsaptr1->table, fsaptr2->table, ne, ns))
187 return FALSE;
188
189 return TRUE;
190 }
191
192 /* The code for the next 4 functions is so similar, that we combine them
193 * into a single function fsa_binop.
194 * (The negatives of these would be more difficult, because (0,0) would
195 * be an accept state - so use fsa_not for these.)
196 */
197
fsa_and(fsa * fsaptr1,fsa * fsaptr2,storage_type op_table_type,boolean destroy,char * tempfilename)198 fsa *fsa_and(fsa *fsaptr1, fsa *fsaptr2, storage_type op_table_type,
199 boolean destroy, char *tempfilename)
200 {
201 if (kbm_print_level >= 3)
202 printf(" #Calling fsa_and.\n");
203 return fsa_binop(fsaptr1, fsaptr2, op_table_type, destroy, tempfilename, AND,
204 FALSE);
205 }
206
fsa_laband(fsa * fsaptr1,fsa * fsaptr2,storage_type op_table_type,boolean destroy,char * tempfilename)207 fsa *fsa_laband(fsa *fsaptr1, fsa *fsaptr2, storage_type op_table_type,
208 boolean destroy, char *tempfilename)
209 {
210 if (kbm_print_level >= 3)
211 printf(" #Calling fsa_laband.\n");
212 return fsa_binop(fsaptr1, fsaptr2, op_table_type, destroy, tempfilename, AND,
213 TRUE);
214 }
215
fsa_or(fsa * fsaptr1,fsa * fsaptr2,storage_type op_table_type,boolean destroy,char * tempfilename)216 fsa *fsa_or(fsa *fsaptr1, fsa *fsaptr2, storage_type op_table_type,
217 boolean destroy, char *tempfilename)
218 {
219 if (kbm_print_level >= 3)
220 printf(" #Calling fsa_or.\n");
221 return fsa_binop(fsaptr1, fsaptr2, op_table_type, destroy, tempfilename, OR,
222 FALSE);
223 }
224
fsa_and_not(fsa * fsaptr1,fsa * fsaptr2,storage_type op_table_type,boolean destroy,char * tempfilename)225 fsa *fsa_and_not(fsa *fsaptr1, fsa *fsaptr2, storage_type op_table_type,
226 boolean destroy, char *tempfilename)
227 {
228 if (kbm_print_level >= 3)
229 printf(" #Calling fsa_and_not.\n");
230 return fsa_binop(fsaptr1, fsaptr2, op_table_type, destroy, tempfilename,
231 AND_NOT, FALSE);
232 }
233
fsa_binop(fsa * fsaptr1,fsa * fsaptr2,storage_type op_table_type,boolean destroy,char * tempfilename,kbm_binop op,const boolean labels)234 static fsa *fsa_binop(fsa *fsaptr1, fsa *fsaptr2, storage_type op_table_type,
235 boolean destroy, char *tempfilename, kbm_binop op,
236 const boolean labels)
237 {
238 int **table1, **table2, ne, ns, dr1, dr2, *fsarow, nt, cstate, csa, csb, im,
239 i, g, len = 0, ct, *ht_ptr;
240 boolean dense_ip1, dense_ip2, dense_op, accept;
241 fsa *and_or_not;
242 hash_table ht;
243 setToLabelsType *lab = 0;
244 FILE *tempfile;
245
246 if (kbm_print_level >= 3)
247 printf(" #Calling fsa_binop.\n");
248 if (!fsaptr1->flags[DFA] || !fsaptr2->flags[DFA]) {
249 fprintf(stderr, "Error: fsa_binop only applies to DFA's.\n");
250 return 0;
251 }
252
253 if (!srec_equal(fsaptr1->alphabet, fsaptr2->alphabet)) {
254 fprintf(stderr, "Error in fsa_binop: fsa's have different alphabets.\n");
255 return 0;
256 }
257
258 if (fsaptr1->flags[RWS])
259 fsa_clear_rws(fsaptr1);
260
261 if (fsaptr2->flags[RWS])
262 fsa_clear_rws(fsaptr2);
263
264 tmalloc(and_or_not, fsa, 1);
265 if (fsaptr2->num_initial == 0 && (op == AND_NOT || op == OR)) {
266 fsa_copy(and_or_not, fsaptr1);
267 and_or_not->table->printing_format = op_table_type;
268 if (destroy) {
269 fsa_clear(fsaptr1);
270 fsa_clear(fsaptr2);
271 }
272 return and_or_not;
273 }
274 if (fsaptr1->num_initial == 0 && op == OR) {
275 fsa_copy(and_or_not, fsaptr2);
276 and_or_not->table->printing_format = op_table_type;
277 if (fsaptr1->states->type == LABELED) {
278 srec_clear(and_or_not->states);
279 srec_copy(and_or_not->states, fsaptr1->states);
280 tfree(and_or_not->states->setToLabels);
281 ns = fsaptr2->states->size;
282 tmalloc(and_or_not->states->setToLabels, setToLabelsType, ns + 1);
283 for (i = 0; i <= ns; i++)
284 and_or_not->states->setToLabels[i] = 0;
285 }
286 if (destroy) {
287 fsa_clear(fsaptr1);
288 fsa_clear(fsaptr2);
289 }
290 return and_or_not;
291 }
292
293 fsa_init(and_or_not);
294 srec_copy(and_or_not->alphabet, fsaptr1->alphabet);
295 and_or_not->flags[DFA] = TRUE;
296 and_or_not->flags[ACCESSIBLE] = TRUE;
297 and_or_not->flags[BFS] = TRUE;
298
299 if (labels) {
300 if (fsaptr1->states->type != LABELED) {
301 fprintf(stderr,
302 "Error in fsa_binop: first fsa should have labeled states.\n");
303 return 0;
304 }
305 srec_copy(and_or_not->states, fsaptr1->states);
306 tfree(and_or_not->states->setToLabels);
307 lab = fsaptr1->states->setToLabels;
308 }
309 else
310 and_or_not->states->type = SIMPLE;
311
312 and_or_not->table->table_type = op_table_type;
313 and_or_not->table->denserows = 0;
314 and_or_not->table->printing_format = op_table_type;
315
316 if (fsaptr1->num_initial == 0 || fsaptr2->num_initial == 0) {
317 and_or_not->num_initial = 0;
318 and_or_not->num_accepting = 0;
319 and_or_not->states->size = 0;
320 if (destroy) {
321 fsa_clear(fsaptr1);
322 fsa_clear(fsaptr2);
323 }
324 return and_or_not;
325 }
326
327 ne = fsaptr1->alphabet->size;
328
329 fsa_set_is_accepting(fsaptr1);
330 fsa_set_is_accepting(fsaptr2);
331 table1 = fsaptr1->table->table_data_ptr;
332 table2 = fsaptr2->table->table_data_ptr;
333
334 dense_ip1 = fsaptr1->table->table_type == DENSE;
335 dense_ip2 = fsaptr2->table->table_type == DENSE;
336 dr1 = fsaptr1->table->denserows;
337 dr2 = fsaptr2->table->denserows;
338 dense_op = op_table_type == DENSE;
339
340 and_or_not->num_initial = 1;
341 tmalloc(and_or_not->initial, int, 2);
342 and_or_not->initial[1] = 1;
343
344 hash_init(&ht, TRUE, 2, 0, 0);
345 ht_ptr = ht.current_ptr;
346 ht_ptr[0] = fsaptr1->initial[1];
347 ht_ptr[1] = fsaptr2->initial[1];
348 im = hash_locate(&ht, 2);
349 if (im != 1) {
350 fprintf(stderr, "Hash-initialisation problem in fsa_binop.\n");
351 return 0;
352 }
353 if ((tempfile = fopen(tempfilename, "w")) == 0) {
354 fprintf(stderr, "Error: cannot open file %s\n", tempfilename);
355 return 0;
356 }
357 if (dense_op)
358 tmalloc(fsarow, int, ne) else tmalloc(fsarow, int, 2 * ne + 1)
359
360 cstate = 0;
361 if (dense_op)
362 len = ne; /* The length of the fsarow output. */
363 nt = 0; /* Number of transitions in and_or_not */
364
365 while (++cstate <= ht.num_recs) {
366 if (kbm_print_level >= 3) {
367 if ((cstate <= 1000 && cstate % 100 == 0) ||
368 (cstate <= 10000 && cstate % 1000 == 0) ||
369 (cstate <= 100000 && cstate % 5000 == 0) || cstate % 50000 == 0)
370 printf(" #cstate = %d; number of states = %d.\n", cstate,
371 ht.num_recs);
372 }
373 ht_ptr = hash_rec(&ht, cstate);
374 csa = ht_ptr[0];
375 csb = ht_ptr[1];
376 if (!dense_op)
377 len = 0;
378 for (g = 1; g <= ne; g++) {
379 /* Calculate action of generator g on state cstate */
380 ht_ptr = ht.current_ptr;
381 ht_ptr[0] = csa ? target(dense_ip1, table1, g, csa, dr1) : 0;
382 ht_ptr[1] = csb ? target(dense_ip2, table2, g, csb, dr2) : 0;
383 if ((op == AND && (ht_ptr[0] == 0 || ht_ptr[1] == 0)) ||
384 (op == AND_NOT && ht_ptr[0] == 0))
385 im = 0;
386 else
387 im = hash_locate(&ht, 2);
388 if (im == -1)
389 return 0;
390 if (dense_op)
391 fsarow[g - 1] = im;
392 else if (im > 0) {
393 fsarow[++len] = g;
394 fsarow[++len] = im;
395 }
396 if (im > 0)
397 nt++;
398 }
399 if (!dense_op)
400 fsarow[0] = len++;
401 fwrite((void *)fsarow, sizeof(int), (size_t)len, tempfile);
402 }
403 fclose(tempfile);
404
405 ns = and_or_not->states->size = ht.num_recs;
406 and_or_not->table->numTransitions = nt;
407 if (labels)
408 tmalloc(and_or_not->states->setToLabels, setToLabelsType, ns + 1);
409 /* Locate the accept states: first count them and then record them. */
410 ct = 0;
411 for (i = 1; i <= ns; i++) {
412 ht_ptr = hash_rec(&ht, i);
413 csa = ht_ptr[0];
414 csb = ht_ptr[1];
415 accept = op == AND
416 ? fsaptr1->is_accepting[csa] && fsaptr2->is_accepting[csb]
417 : op == OR ? fsaptr1->is_accepting[csa] ||
418 fsaptr2->is_accepting[csb]
419 : op == AND_NOT ? fsaptr1->is_accepting[csa] &&
420 !fsaptr2->is_accepting[csb]
421 : FALSE; /* default cannot occur */
422 if (accept)
423 ct++;
424 if (labels)
425 and_or_not->states->setToLabels[i] = csa == 0 ? 0 : lab[csa];
426 }
427 and_or_not->num_accepting = ct;
428 if (ct == 1 || ct != ns) {
429 tmalloc(and_or_not->accepting, int, ct + 1);
430 ct = 0;
431 for (i = 1; i <= ns; i++) {
432 ht_ptr = hash_rec(&ht, i);
433 csa = ht_ptr[0];
434 csb = ht_ptr[1];
435 accept =
436 op == AND
437 ? fsaptr1->is_accepting[csa] && fsaptr2->is_accepting[csb]
438 : op == OR
439 ? fsaptr1->is_accepting[csa] || fsaptr2->is_accepting[csb]
440 : op == AND_NOT ? fsaptr1->is_accepting[csa] &&
441 !fsaptr2->is_accepting[csb]
442 : FALSE; /* default cannot occur */
443 if (accept)
444 and_or_not->accepting[++ct] = i;
445 }
446 }
447 hash_clear(&ht);
448 tfree(fsarow);
449 tfree(fsaptr1->is_accepting);
450 tfree(fsaptr2->is_accepting);
451
452 if (destroy) {
453 fsa_clear(fsaptr1);
454 fsa_clear(fsaptr2);
455 }
456 /* Now read the transition table back in */
457 tempfile = fopen(tempfilename, "r");
458 compressed_transitions_read(and_or_not, tempfile);
459 fclose(tempfile);
460
461 unlink(tempfilename);
462
463 return and_or_not;
464 }
465
466 /* This function ought to be easy - just interchange accept and non-accept
467 * states. In fact it is complicated slightly by the fact that we are
468 * working with partial fsa's, so the 0 state has to become a new state,
469 * and a former state may become 0.
470 * The storage-type of the computed fsa *not will always be dense.
471 */
fsa_not(fsa * fsaptr,storage_type op_table_type)472 fsa *fsa_not(fsa *fsaptr, storage_type op_table_type)
473 {
474 int i, j, k, ns, ne, **oldtable, **newtable, newzero, dr;
475 fsa * not;
476 boolean dense, zero;
477
478 if (kbm_print_level >= 3)
479 printf(" #Calling fsa_not.\n");
480
481 if (!fsaptr->flags[DFA]) {
482 fprintf(stderr, "Error: fsa_not only applies to DFA's.\n");
483 return 0;
484 }
485
486 if (fsaptr->flags[RWS])
487 fsa_clear_rws(fsaptr);
488
489 tmalloc(not, fsa, 1);
490 fsa_init(not);
491 /* Most of the information is simply copied from *fsaptr to *not-
492 * but we allow room for an extra accept state of *not, to replace 0
493 */
494 ne = fsaptr->alphabet->size;
495 ns = fsaptr->states->size;
496
497 srec_copy(not->alphabet, fsaptr->alphabet);
498 not->states->type = SIMPLE;
499 not->states->size = ns;
500 not->num_initial = 1;
501 tmalloc(not->initial, int, 2);
502 not->initial[1] = fsaptr->num_initial == 0 ? 1 : fsaptr->initial[1];
503
504 fsa_table_init(not->table, ns + 1, ne);
505 oldtable = fsaptr->table->table_data_ptr;
506 newtable = not->table->table_data_ptr;
507 dense = fsaptr->table->table_type == DENSE;
508 dr = fsaptr->table->denserows;
509 not->table->printing_format = op_table_type;
510 not->table->denserows = 0;
511
512 zero = ns == 0;
513 for (j = 1; j <= ne; j++)
514 for (i = 1; i <= ns; i++) {
515 k = target(dense, oldtable, j, i, dr);
516 set_dense_target(newtable, j, i, k);
517 if (!zero && k == 0)
518 zero = TRUE;
519 }
520
521 tmalloc(not->is_accepting, boolean, ns + 2);
522 if (fsaptr->num_accepting == ns) {
523 for (i = 1; i <= ns; i++)
524 not->is_accepting[i] = FALSE;
525 not->is_accepting[ns + 1] = TRUE;
526 }
527 else {
528 for (i = 1; i <= ns + 1; i++)
529 not->is_accepting[i] = TRUE;
530 for (i = 1; i <= fsaptr->num_accepting; i++)
531 not->is_accepting[fsaptr->accepting[i]] = FALSE;
532 }
533
534 /* See if there is a new zero-state */
535 newzero = 0;
536 for (i = 1; i <= ns; i++)
537 if (!not->is_accepting[i]) {
538 newzero = i;
539 for (j = 1; j <= ne; j++)
540 if (dense_target(newtable, j, i) != i) {
541 newzero = 0;
542 break;
543 }
544 if (newzero)
545 break;
546 }
547
548 if (newzero == 0 && zero)
549 not->states->size = ++ns;
550
551 not->num_accepting = 0;
552 for (i = 1; i <= ns; i++)
553 if (not->is_accepting[i])
554 not->num_accepting++;
555 if (ns == 1 || not->num_accepting != ns) {
556 k = 0;
557 tmalloc(not->accepting, int, not->num_accepting + 1);
558 for (i = 1; i <= ns; i++)
559 if (not->is_accepting[i])
560 not->accepting[++k] = i;
561 }
562 tfree(not->is_accepting);
563
564 if (zero && newzero) {
565 /* swap zero with the new zero-state */
566 for (j = 1; j <= ne; j++)
567 for (i = 1; i <= ns; i++) {
568 if (i == newzero)
569 continue;
570 if (dense_target(newtable, j, i) == 0)
571 newtable[j][i] = newzero;
572 else if (dense_target(newtable, j, i) == newzero)
573 set_dense_target(newtable, j, i, 0);
574 }
575 }
576 else if (newzero)
577 fsa_delete_state(not, newzero);
578 else if (zero) {
579 for (j = 1; j <= ne; j++)
580 set_dense_target(newtable, j, ns, ns);
581 for (j = 1; j <= ne; j++)
582 for (i = 1; i < ns; i++)
583 if (dense_target(newtable, j, i) == 0)
584 set_dense_target(newtable, j, i, ns);
585 }
586
587 for (i = 0; i < num_kbm_flag_strings; i++)
588 not->flags[i] = fsaptr->flags[i];
589 not->flags[BFS] = FALSE;
590 /* BFS property would be ruined by 0 state of *fsaptr */
591
592 return not;
593 }
594
595 /* *fsaptr should be a deterministic fsa.
596 * A (usually) non-deterministic fsa accepting the star L* of
597 * the language L of *fsaptr is returned.
598 * The method is simply to insert epsilon-transitions from the accept states
599 * of *fsaptr to its initial state.
600 */
fsa_star(fsa * fsaptr,boolean destroy)601 fsa *fsa_star(fsa *fsaptr, boolean destroy)
602 {
603 int **itable, **table, ne, ns, nt1, dr, nt, *sparseptr, iin, ina, im, i, ct,
604 g;
605 boolean dense_ip;
606 fsa *star;
607
608 if (kbm_print_level >= 3)
609 printf(" #Calling fsa_star.\n");
610 if (!fsaptr->flags[DFA]) {
611 fprintf(stderr, "Error: fsa_star only applies to DFA's.\n");
612 return 0;
613 }
614
615 if (fsaptr->flags[RWS])
616 fsa_clear_rws(fsaptr);
617
618 tmalloc(star, fsa, 1);
619 if (fsaptr->num_initial == 0) {
620 fsa_copy(star, fsaptr);
621 if (destroy)
622 fsa_clear(fsaptr);
623 star->table->printing_format = SPARSE;
624 return star;
625 }
626
627 fsa_init(star);
628 srec_copy(star->alphabet, fsaptr->alphabet);
629 star->flags[NFA] = TRUE;
630 fsa_set_is_accepting(fsaptr);
631 ne = fsaptr->alphabet->size;
632 ns = fsaptr->states->size;
633 star->states->size = ns;
634
635 iin = fsaptr->initial[1];
636 tmalloc(star->initial, int, 2);
637 star->initial[1] = iin;
638 star->num_initial = 1;
639 ina = fsaptr->num_accepting;
640 if (!fsaptr->is_accepting[iin]) {
641 ina++;
642 fsaptr->is_accepting[iin] = TRUE;
643 }
644 star->num_accepting = ina;
645 if (ns == 1 || ina < ns) {
646 tmalloc(star->accepting, int, ina + 1);
647 ct = 0;
648 for (i = 1; i <= ns; i++)
649 if (fsaptr->is_accepting[i])
650 star->accepting[++ct] = i;
651 }
652
653 itable = fsaptr->table->table_data_ptr;
654 dense_ip = fsaptr->table->table_type == DENSE;
655 dr = fsaptr->table->denserows;
656 /* We won't rely on fsaptr->table->numTransitions being stored */
657 nt1 = 0;
658 for (g = 1; g <= ne; g++)
659 for (i = 1; i <= ns; i++)
660 if (target(dense_ip, itable, g, i, dr) != 0)
661 nt1++;
662
663 nt = nt1 + ina;
664 star->table->numTransitions = nt;
665 star->table->table_type = SPARSE;
666 star->table->denserows = 0;
667 star->table->printing_format = SPARSE;
668 tmalloc(star->table->table_data_ptr, int *, ns + 2);
669 table = star->table->table_data_ptr;
670 tmalloc(table[0], int, 2 * nt + 1);
671 sparseptr = table[0];
672
673 for (i = 1; i <= ns; i++) {
674 table[i] = sparseptr;
675 if (fsaptr->is_accepting[i]) {
676 *(sparseptr++) = 0;
677 *(sparseptr++) = iin;
678 }
679 for (g = 1; g <= ne; g++) {
680 im = target(dense_ip, itable, g, i, dr);
681 if (im) {
682 *(sparseptr++) = g;
683 *(sparseptr++) = im;
684 }
685 }
686 }
687 table[ns + 1] = sparseptr; /* to show end of data */
688
689 tfree(fsaptr->is_accepting);
690 if (destroy)
691 fsa_clear(fsaptr);
692 return star;
693 }
694
695 /* *fsaptr1 and *fsaptr2 should be two deterministic fsa's.
696 * A (usually) non-deterministic fsa accepting the concatenation of
697 * the languages of *fsaptr1 and *fsaptr2 is returned.
698 * The method is simply to take the union of the two fsa's, and
699 * insert epsilon-transitions from the accept states of *fsaptr1 to the
700 * initial states of *fsaptr2.
701 */
fsa_concat(fsa * fsaptr1,fsa * fsaptr2,boolean destroy)702 fsa *fsa_concat(fsa *fsaptr1, fsa *fsaptr2, boolean destroy)
703 {
704 int **table1, **table2, **table, ne, ns1, ns2, nt1, nt2, dr1, dr2, nt,
705 *sparseptr, in2, na2, im, i, g;
706 boolean dense_ip1, dense_ip2;
707 fsa *concat;
708
709 if (kbm_print_level >= 3)
710 printf(" #Calling fsa_concat.\n");
711 if (!fsaptr1->flags[DFA] || !fsaptr2->flags[DFA]) {
712 fprintf(stderr, "Error: fsa_concat only applies to DFA's.\n");
713 return 0;
714 }
715
716 if (!srec_equal(fsaptr1->alphabet, fsaptr2->alphabet)) {
717 fprintf(stderr, "Error in fsa_concat: fsa's have different alphabets.\n");
718 return 0;
719 }
720
721 if (fsaptr1->flags[RWS])
722 fsa_clear_rws(fsaptr1);
723 if (fsaptr2->flags[RWS])
724 fsa_clear_rws(fsaptr2);
725
726 tmalloc(concat, fsa, 1);
727 if (fsaptr1->num_initial == 0) {
728 fsa_copy(concat, fsaptr1);
729 if (destroy) {
730 fsa_clear(fsaptr1);
731 fsa_clear(fsaptr2);
732 }
733 concat->table->printing_format = SPARSE;
734 return concat;
735 }
736 if (fsaptr2->num_initial == 0) {
737 fsa_copy(concat, fsaptr2);
738 if (destroy) {
739 fsa_clear(fsaptr1);
740 fsa_clear(fsaptr2);
741 }
742 concat->table->printing_format = SPARSE;
743 return concat;
744 }
745
746 fsa_init(concat);
747 srec_copy(concat->alphabet, fsaptr1->alphabet);
748 concat->flags[NFA] = TRUE;
749 fsa_set_is_accepting(fsaptr1);
750 ne = fsaptr1->alphabet->size;
751 ns1 = fsaptr1->states->size;
752 ns2 = fsaptr2->states->size;
753 concat->states->size = ns1 + ns2;
754
755 tmalloc(concat->initial, int, 2);
756 concat->initial[1] = fsaptr1->initial[1];
757 concat->num_initial = 1;
758 na2 = fsaptr2->num_accepting;
759 concat->num_accepting = na2;
760 tmalloc(concat->accepting, int, na2 + 1);
761 if (na2 == ns2) {
762 for (i = 1; i <= na2; i++)
763 concat->accepting[i] = i + ns1;
764 }
765 else
766 for (i = 1; i <= na2; i++)
767 concat->accepting[i] = fsaptr2->accepting[i] + ns1;
768 in2 = fsaptr2->initial[1] + ns1;
769
770 table1 = fsaptr1->table->table_data_ptr;
771 table2 = fsaptr2->table->table_data_ptr;
772 dense_ip1 = fsaptr1->table->table_type == DENSE;
773 dense_ip2 = fsaptr2->table->table_type == DENSE;
774 dr1 = fsaptr1->table->denserows;
775 dr2 = fsaptr2->table->denserows;
776 /* We won't rely on fsaptr1/2->table->numTransitions being stored */
777 nt1 = 0;
778 for (g = 1; g <= ne; g++)
779 for (i = 1; i <= ns1; i++)
780 if (target(dense_ip1, table1, g, i, dr1) != 0)
781 nt1++;
782 nt2 = 0;
783 for (g = 1; g <= ne; g++)
784 for (i = 1; i <= ns2; i++)
785 if (target(dense_ip2, table2, g, i, dr2) != 0)
786 nt2++;
787
788 nt = nt1 + nt2 + fsaptr1->num_accepting;
789 concat->table->numTransitions = nt;
790 concat->table->table_type = SPARSE;
791 concat->table->denserows = 0;
792 concat->table->printing_format = SPARSE;
793 tmalloc(concat->table->table_data_ptr, int *, ns1 + ns2 + 2);
794 table = concat->table->table_data_ptr;
795 tmalloc(table[0], int, 2 * nt + 1);
796 sparseptr = table[0];
797
798 for (i = 1; i <= ns1; i++) {
799 table[i] = sparseptr;
800 if (fsaptr1->is_accepting[i]) {
801 *(sparseptr++) = 0;
802 *(sparseptr++) = in2;
803 }
804 for (g = 1; g <= ne; g++) {
805 im = target(dense_ip1, table1, g, i, dr1);
806 if (im) {
807 *(sparseptr++) = g;
808 *(sparseptr++) = im;
809 }
810 }
811 }
812 for (i = 1; i <= ns2; i++) {
813 table[i + ns1] = sparseptr;
814 for (g = 1; g <= ne; g++) {
815 im = target(dense_ip2, table2, g, i, dr2);
816 if (im) {
817 *(sparseptr++) = g;
818 *(sparseptr++) = im + ns1;
819 }
820 }
821 }
822 table[ns1 + ns2 + 1] = sparseptr; /* to show end of data */
823
824 tfree(fsaptr1->is_accepting);
825 if (destroy) {
826 fsa_clear(fsaptr1);
827 fsa_clear(fsaptr2);
828 }
829 return concat;
830 }
831
832 /* *fsaptr must be a 2-variable fsa.
833 * The returned fsa accepts a word w_1 iff (w_1,w_2) is accepted by *fsaptr,
834 * for some word w_2 (with the usual padding conventions).
835 * In fact, fsa_exists calls fsa_exists_int or (more usually) fsa_exists_short,
836 * the latter using the short hash table functions.
837 */
fsa_exists(fsa * fsaptr,storage_type op_table_type,boolean destroy,char * tempfilename)838 fsa *fsa_exists(fsa *fsaptr, storage_type op_table_type, boolean destroy,
839 char *tempfilename)
840 {
841 if (kbm_print_level >= 3)
842 printf(" #Calling fsa_exists.\n");
843 if (fsaptr->states->size < MAXUSHORT)
844 return fsa_exists_short(fsaptr, op_table_type, destroy, tempfilename);
845 else
846 return fsa_exists_int(fsaptr, op_table_type, destroy, tempfilename);
847 }
848
fsa_exists_short(fsa * fsaptr,storage_type op_table_type,boolean destroy,char * tempfilename)849 static fsa *fsa_exists_short(fsa *fsaptr, storage_type op_table_type,
850 boolean destroy, char *tempfilename)
851 {
852 int **table, ne, ngens, ns, dr, *fsarow, e, es, ef, nt, cstate, cs, csi, im,
853 i, g1, len = 0, ct;
854 unsigned short *ht_ptr, *ht_chptr, *ht_ptrb, *ht_ptre, *cs_ptr, *cs_ptre,
855 *ptr;
856 boolean dense_ip, dense_op, got;
857 short_hash_table ht;
858 fsa *exists;
859 FILE *tempfile;
860
861 if (kbm_print_level >= 3)
862 printf(" #Calling fsa_exists_short.\n");
863 if (!fsaptr->flags[DFA]) {
864 fprintf(stderr, "Error: fsa_exists only applies to DFA's.\n");
865 return 0;
866 }
867
868 if (fsaptr->alphabet->type != PRODUCT || fsaptr->alphabet->arity != 2) {
869 fprintf(stderr, "Error in fsa_exists: fsa must be 2-variable.\n");
870 return 0;
871 }
872
873 tmalloc(exists, fsa, 1);
874 fsa_init(exists);
875 srec_copy(exists->alphabet, fsaptr->alphabet->base);
876 exists->flags[DFA] = TRUE;
877 exists->flags[ACCESSIBLE] = TRUE;
878 exists->flags[BFS] = TRUE;
879
880 exists->states->type = SIMPLE;
881
882 exists->table->table_type = op_table_type;
883 exists->table->denserows = 0;
884 exists->table->printing_format = op_table_type;
885
886 if (fsaptr->num_initial == 0) {
887 exists->num_initial = 0;
888 exists->num_accepting = 0;
889 exists->states->size = 0;
890 if (destroy)
891 fsa_clear(fsaptr);
892 return exists;
893 }
894 ne = fsaptr->alphabet->size;
895 ngens = exists->alphabet->size;
896
897 if (ne != (ngens + 1) * (ngens + 1) - 1) {
898 fprintf(stderr, "Error: in a 2-variable fsa, alphabet size should = "
899 "(ngens+1)^2 - 1.\n");
900 return 0;
901 }
902
903 fsa_set_is_accepting(fsaptr);
904
905 dense_ip = fsaptr->table->table_type == DENSE;
906 dr = fsaptr->table->denserows;
907 dense_op = op_table_type == DENSE;
908 table = fsaptr->table->table_data_ptr;
909
910 exists->num_initial = 1;
911 tmalloc(exists->initial, int, 2);
912 exists->initial[1] = 1;
913
914 short_hash_init(&ht, FALSE, 0, 0, 0);
915 ht_ptr = ht.current_ptr;
916 ht_ptr[0] = fsaptr->initial[1];
917 im = short_hash_locate(&ht, 1);
918 if (im == -1)
919 return 0;
920 /* Each state in 'exists' will be represented as a subset of the set of states
921 * of *fsaptr. The initial state is one-element set containing the initial
922 * state of *fsaptr. A subset is an accept-state if it contains an accept
923 * state of *fsaptr, or if one can get to an accept-state by applying elements
924 * ($,x) where $ is the padding symbol.
925 * The subsets will be stored as variable-length records in the hash-table,
926 * always in increasing order.
927 */
928 if (im != 1) {
929 fprintf(stderr, "Hash-initialisation problem in fsa_exists.\n");
930 return 0;
931 }
932 if ((tempfile = fopen(tempfilename, "w")) == 0) {
933 fprintf(stderr, "Error: cannot open file %s\n", tempfilename);
934 return 0;
935 }
936 if (dense_op)
937 tmalloc(fsarow, int, ngens) else tmalloc(fsarow, int, 2 * ngens + 1)
938
939 cstate = 0;
940 if (dense_op)
941 len = ngens; /* The length of the fsarow output. */
942 nt = 0; /* Number of transitions in exists */
943
944 while (++cstate <= ht.num_recs) {
945 if (kbm_print_level >= 3) {
946 if ((cstate <= 1000 && cstate % 100 == 0) ||
947 (cstate <= 10000 && cstate % 1000 == 0) ||
948 (cstate <= 100000 && cstate % 5000 == 0) || cstate % 50000 == 0)
949 printf(" #cstate = %d; number of states = %d.\n", cstate,
950 ht.num_recs);
951 }
952 cs_ptr = short_hash_rec(&ht, cstate);
953 cs_ptre = short_hash_rec(&ht, cstate) + short_hash_rec_len(&ht, cstate) - 1;
954 if (!dense_op)
955 len = 0;
956
957 for (g1 = 1; g1 <= ngens; g1++) {
958 /* Calculate action of generator g1 on state cstate - to get the image,
959 * we have to apply (g1,g2) to each element in the subset corresponding to
960 * cstate, and this for each generator g2 of the base-alphabet (including
961 * the padding symbol).
962 */
963 ht_ptrb = ht.current_ptr;
964 ht_ptre = ht_ptrb - 1;
965 ptr = cs_ptr - 1;
966 es = (g1 - 1) * (ngens + 1) + 1;
967 ef = g1 * (ngens + 1);
968 /* As g2 ranges from 1 to ngens+1 in the pair (g1,g2), for fixed g1, the
969 * corresponding edge number in the fsa ranges from es to ef.
970 */
971 while (++ptr <= cs_ptre) {
972 cs = *ptr;
973 for (e = es; e <= ef; e++) {
974 csi = target(dense_ip, table, e, cs, dr);
975 if (csi == 0)
976 continue;
977 if (ht_ptrb > ht_ptre || csi > *ht_ptre) {
978 /* We have a new state for the image subset to be added to the end
979 */
980 *(++ht_ptre) = csi;
981 }
982 else {
983 ht_chptr = ht_ptrb;
984 while (*ht_chptr < csi)
985 ht_chptr++;
986 if (csi < *ht_chptr) {
987 /* we have a new state for the image subset to be added in the
988 * middle */
989 ht_ptr = ++ht_ptre;
990 while (ht_ptr > ht_chptr) {
991 *ht_ptr = *(ht_ptr - 1);
992 ht_ptr--;
993 }
994 *ht_ptr = csi;
995 }
996 }
997 }
998 }
999 im = short_hash_locate(&ht, ht_ptre - ht_ptrb + 1);
1000 if (im == -1)
1001 return 0;
1002 if (dense_op)
1003 fsarow[g1 - 1] = im;
1004 else if (im > 0) {
1005 fsarow[++len] = g1;
1006 fsarow[++len] = im;
1007 }
1008 if (im > 0)
1009 nt++;
1010 }
1011 if (!dense_op)
1012 fsarow[0] = len++;
1013 fwrite((void *)fsarow, sizeof(int), (size_t)len, tempfile);
1014 }
1015 fclose(tempfile);
1016
1017 ns = exists->states->size = ht.num_recs;
1018 exists->table->numTransitions = nt;
1019
1020 /* Locate the accept states. This is slightly cumbersome, since a state
1021 * is an accept state if either the corresponding subset contains an
1022 * accept state of *fsaptr, or we can get from some such state to an
1023 * accept state by applying elements ($,x).
1024 * We will need to use the array exists->is_accepting.
1025 */
1026 tmalloc(exists->is_accepting, boolean, ns + 1);
1027 for (i = 1; i <= ns; i++)
1028 exists->is_accepting[i] = FALSE;
1029 ct = 0;
1030 for (cstate = ns; cstate >= 1; cstate--) {
1031 /* We work backwards through the states, since we wish to add on additional
1032 * elements at the end of the list in the hash-table - this destroys
1033 * later entries, but that doesn't matter, since we have already dealt
1034 * with them.
1035 */
1036 cs_ptr = short_hash_rec(&ht, cstate);
1037 cs_ptre = short_hash_rec(&ht, cstate) + short_hash_rec_len(&ht, cstate) - 1;
1038 /* First see if the set itself contains an accept-state */
1039 ptr = cs_ptr - 1;
1040 while (++ptr <= cs_ptre)
1041 if (fsaptr->is_accepting[*ptr]) {
1042 exists->is_accepting[cstate] = TRUE;
1043 ct++;
1044 break;
1045 }
1046 if (exists->is_accepting[cstate])
1047 continue;
1048 /* Next apply generators ($,x) and see if we get anything new, and
1049 * if it is an accept state.
1050 * Anything new is added to the end of the list - we don't need to
1051 * bother about having them in increasing order this time.
1052 */
1053 es = ngens * (ngens + 1) + 1;
1054 ef = (ngens + 1) * (ngens + 1) - 1;
1055 ptr = cs_ptr - 1;
1056 while (++ptr <= cs_ptre) {
1057 cs = *ptr;
1058 for (e = es; e <= ef; e++) {
1059 csi = target(dense_ip, table, e, cs, dr);
1060 if (csi == 0)
1061 continue;
1062 if (fsaptr->is_accepting[csi]) {
1063 exists->is_accepting[cstate] = TRUE;
1064 ct++;
1065 break;
1066 }
1067 /* see if csi is new */
1068 ht_chptr = cs_ptr - 1;
1069 got = FALSE;
1070 while (++ht_chptr <= cs_ptre)
1071 if (csi == *ht_chptr) {
1072 got = TRUE;
1073 break;
1074 }
1075 if (!got)
1076 /* add csi to the end */
1077 *(++cs_ptre) = csi;
1078 }
1079 if (exists->is_accepting[cstate])
1080 break;
1081 }
1082 }
1083
1084 exists->num_accepting = ct;
1085 if (ct == 1 || ct != ns) {
1086 tmalloc(exists->accepting, int, ct + 1);
1087 ct = 0;
1088 for (i = 1; i <= ns; i++)
1089 if (exists->is_accepting[i])
1090 exists->accepting[++ct] = i;
1091 }
1092 tfree(fsaptr->is_accepting);
1093 tfree(exists->is_accepting);
1094 short_hash_clear(&ht);
1095 tfree(fsarow);
1096
1097 if (destroy)
1098 fsa_clear(fsaptr);
1099
1100 /* Now read the transition table back in */
1101 tempfile = fopen(tempfilename, "r");
1102 compressed_transitions_read(exists, tempfile);
1103 fclose(tempfile);
1104
1105 unlink(tempfilename);
1106
1107 return exists;
1108 }
1109
fsa_exists_int(fsa * fsaptr,storage_type op_table_type,boolean destroy,char * tempfilename)1110 fsa *fsa_exists_int(fsa *fsaptr, storage_type op_table_type, boolean destroy,
1111 char *tempfilename)
1112 {
1113 int **table, ne, ngens, ns, dr, *fsarow, e, es, ef, nt, cstate, cs, csi, im,
1114 i, g1, len = 0, ct;
1115 int *ht_ptr, *ht_chptr, *ht_ptrb, *ht_ptre, *cs_ptr, *cs_ptre, *ptr;
1116 boolean dense_ip, dense_op, got;
1117 hash_table ht;
1118 fsa *exists;
1119 FILE *tempfile;
1120
1121 if (kbm_print_level >= 3)
1122 printf(" #Calling fsa_exists_short.\n");
1123 if (!fsaptr->flags[DFA]) {
1124 fprintf(stderr, "Error: fsa_exists only applies to DFA's.\n");
1125 return 0;
1126 }
1127
1128 if (fsaptr->alphabet->type != PRODUCT || fsaptr->alphabet->arity != 2) {
1129 fprintf(stderr, "Error in fsa_exists: fsa must be 2-variable.\n");
1130 return 0;
1131 }
1132
1133 tmalloc(exists, fsa, 1);
1134 fsa_init(exists);
1135 srec_copy(exists->alphabet, fsaptr->alphabet->base);
1136 exists->flags[DFA] = TRUE;
1137 exists->flags[ACCESSIBLE] = TRUE;
1138 exists->flags[BFS] = TRUE;
1139
1140 exists->states->type = SIMPLE;
1141
1142 exists->table->table_type = op_table_type;
1143 exists->table->denserows = 0;
1144 exists->table->printing_format = op_table_type;
1145
1146 if (fsaptr->num_initial == 0) {
1147 exists->num_initial = 0;
1148 exists->num_accepting = 0;
1149 exists->states->size = 0;
1150 if (destroy)
1151 fsa_clear(fsaptr);
1152 return exists;
1153 }
1154 ne = fsaptr->alphabet->size;
1155 ngens = exists->alphabet->size;
1156
1157 if (ne != (ngens + 1) * (ngens + 1) - 1) {
1158 fprintf(stderr, "Error: in a 2-variable fsa, alphabet size should = "
1159 "(ngens+1)^2 - 1.\n");
1160 return 0;
1161 }
1162
1163 fsa_set_is_accepting(fsaptr);
1164
1165 dense_ip = fsaptr->table->table_type == DENSE;
1166 dr = fsaptr->table->denserows;
1167 dense_op = op_table_type == DENSE;
1168 table = fsaptr->table->table_data_ptr;
1169
1170 exists->num_initial = 1;
1171 tmalloc(exists->initial, int, 2);
1172 exists->initial[1] = 1;
1173
1174 hash_init(&ht, FALSE, 0, 0, 0);
1175 ht_ptr = ht.current_ptr;
1176 ht_ptr[0] = fsaptr->initial[1];
1177 im = hash_locate(&ht, 1);
1178 if (im == -1)
1179 return 0;
1180 /* Each state in 'exists' will be represented as a subset of the set of states
1181 * of *fsaptr. The initial state is one-element set containing the initial
1182 * state of *fsaptr. A subset is an accept-state if it contains an accept
1183 * state of *fsaptr, or if one can get to an accept-state by applying elements
1184 * ($,x) where $ is the padding symbol.
1185 * The subsets will be stored as variable-length records in the hash-table,
1186 * always in increasing order.
1187 */
1188 if (im != 1) {
1189 fprintf(stderr, "Hash-initialisation problem in fsa_exists.\n");
1190 return 0;
1191 }
1192 if ((tempfile = fopen(tempfilename, "w")) == 0) {
1193 fprintf(stderr, "Error: cannot open file %s\n", tempfilename);
1194 return 0;
1195 }
1196 if (dense_op)
1197 tmalloc(fsarow, int, ngens) else tmalloc(fsarow, int, 2 * ngens + 1)
1198
1199 cstate = 0;
1200 if (dense_op)
1201 len = ngens; /* The length of the fsarow output. */
1202 nt = 0; /* Number of transitions in exists */
1203
1204 while (++cstate <= ht.num_recs) {
1205 if (kbm_print_level >= 3) {
1206 if ((cstate <= 1000 && cstate % 100 == 0) ||
1207 (cstate <= 10000 && cstate % 1000 == 0) ||
1208 (cstate <= 100000 && cstate % 5000 == 0) || cstate % 50000 == 0)
1209 printf(" #cstate = %d; number of states = %d.\n", cstate,
1210 ht.num_recs);
1211 }
1212 cs_ptr = hash_rec(&ht, cstate);
1213 cs_ptre = hash_rec(&ht, cstate) + hash_rec_len(&ht, cstate) - 1;
1214 if (!dense_op)
1215 len = 0;
1216
1217 for (g1 = 1; g1 <= ngens; g1++) {
1218 /* Calculate action of generator g1 on state cstate - to get the image,
1219 * we have to apply (g1,g2) to each element in the subset corresponding to
1220 * cstate, and this for each generator g2 of the base-alphabet (including
1221 * the padding symbol).
1222 */
1223 ht_ptrb = ht.current_ptr;
1224 ht_ptre = ht_ptrb - 1;
1225 ptr = cs_ptr - 1;
1226 es = (g1 - 1) * (ngens + 1) + 1;
1227 ef = g1 * (ngens + 1);
1228 /* As g2 ranges from 1 to ngens+1 in the pair (g1,g2), for fixed g1, the
1229 * corresponding edge number in the fsa ranges from es to ef.
1230 */
1231 while (++ptr <= cs_ptre) {
1232 cs = *ptr;
1233 for (e = es; e <= ef; e++) {
1234 csi = target(dense_ip, table, e, cs, dr);
1235 if (csi == 0)
1236 continue;
1237 if (ht_ptrb > ht_ptre || csi > *ht_ptre) {
1238 /* We have a new state for the image subset to be added to the end
1239 */
1240 *(++ht_ptre) = csi;
1241 }
1242 else {
1243 ht_chptr = ht_ptrb;
1244 while (*ht_chptr < csi)
1245 ht_chptr++;
1246 if (csi < *ht_chptr) {
1247 /* we have a new state for the image subset to be added in the
1248 * middle */
1249 ht_ptr = ++ht_ptre;
1250 while (ht_ptr > ht_chptr) {
1251 *ht_ptr = *(ht_ptr - 1);
1252 ht_ptr--;
1253 }
1254 *ht_ptr = csi;
1255 }
1256 }
1257 }
1258 }
1259 im = hash_locate(&ht, ht_ptre - ht_ptrb + 1);
1260 if (im == -1)
1261 return 0;
1262 if (dense_op)
1263 fsarow[g1 - 1] = im;
1264 else if (im > 0) {
1265 fsarow[++len] = g1;
1266 fsarow[++len] = im;
1267 }
1268 if (im > 0)
1269 nt++;
1270 }
1271 if (!dense_op)
1272 fsarow[0] = len++;
1273 fwrite((void *)fsarow, sizeof(int), (size_t)len, tempfile);
1274 }
1275 fclose(tempfile);
1276
1277 ns = exists->states->size = ht.num_recs;
1278 exists->table->numTransitions = nt;
1279
1280 /* Locate the accept states. This is slightly cumbersome, since a state
1281 * is an accept state if either the corresponding subset contains an
1282 * accept state of *fsaptr, or we can get from some such state to an
1283 * accept state by applying elements ($,x).
1284 * We will need to use the array exists->is_accepting.
1285 */
1286 tmalloc(exists->is_accepting, boolean, ns + 1);
1287 for (i = 1; i <= ns; i++)
1288 exists->is_accepting[i] = FALSE;
1289 ct = 0;
1290 for (cstate = ns; cstate >= 1; cstate--) {
1291 /* We work backwards through the states, since we wish to add on additional
1292 * elements at the end of the list in the hash-table - this destroys
1293 * later entries, but that doesn't matter, since we have already dealt
1294 * with them.
1295 */
1296 cs_ptr = hash_rec(&ht, cstate);
1297 cs_ptre = hash_rec(&ht, cstate) + hash_rec_len(&ht, cstate) - 1;
1298 /* First see if the set itself contains an accept-state */
1299 ptr = cs_ptr - 1;
1300 while (++ptr <= cs_ptre)
1301 if (fsaptr->is_accepting[*ptr]) {
1302 exists->is_accepting[cstate] = TRUE;
1303 ct++;
1304 break;
1305 }
1306 if (exists->is_accepting[cstate])
1307 continue;
1308 /* Next apply generators ($,x) and see if we get anything new, and
1309 * if it is an accept state.
1310 * Anything new is added to the end of the list - we don't need to
1311 * bother about having them in increasing order this time.
1312 */
1313 es = ngens * (ngens + 1) + 1;
1314 ef = (ngens + 1) * (ngens + 1) - 1;
1315 ptr = cs_ptr - 1;
1316 while (++ptr <= cs_ptre) {
1317 cs = *ptr;
1318 for (e = es; e <= ef; e++) {
1319 csi = target(dense_ip, table, e, cs, dr);
1320 if (csi == 0)
1321 continue;
1322 if (fsaptr->is_accepting[csi]) {
1323 exists->is_accepting[cstate] = TRUE;
1324 ct++;
1325 break;
1326 }
1327 /* see if csi is new */
1328 ht_chptr = cs_ptr - 1;
1329 got = FALSE;
1330 while (++ht_chptr <= cs_ptre)
1331 if (csi == *ht_chptr) {
1332 got = TRUE;
1333 break;
1334 }
1335 if (!got)
1336 /* add csi to the end */
1337 *(++cs_ptre) = csi;
1338 }
1339 if (exists->is_accepting[cstate])
1340 break;
1341 }
1342 }
1343
1344 exists->num_accepting = ct;
1345 if (ct == 1 || ct != ns) {
1346 tmalloc(exists->accepting, int, ct + 1);
1347 ct = 0;
1348 for (i = 1; i <= ns; i++)
1349 if (exists->is_accepting[i])
1350 exists->accepting[++ct] = i;
1351 }
1352 tfree(fsaptr->is_accepting);
1353 tfree(exists->is_accepting);
1354 hash_clear(&ht);
1355 tfree(fsarow);
1356
1357 if (destroy)
1358 fsa_clear(fsaptr);
1359
1360 /* Now read the transition table back in */
1361 tempfile = fopen(tempfilename, "r");
1362 compressed_transitions_read(exists, tempfile);
1363 fclose(tempfile);
1364
1365 unlink(tempfilename);
1366
1367 return exists;
1368 }
1369
1370 /* This constructs the two-variable fsa with base-alphabet *alphptr
1371 * that accepts (w_1,w_2) iff w_1 > w_2 in the shortlex ordering.
1372 * The shorter of the two words (if any) is padded with the padding-symbol.
1373 * Any occurrence of the padding symbol in mid-word leads to failure.
1374 * The table-type of the returned fsa will always be dense.
1375 */
fsa_greater_than(srec * alphptr)1376 fsa *fsa_greater_than(srec *alphptr)
1377 {
1378 int ngens, ***dtable, i, j, p;
1379 fsa *greater_than;
1380
1381 if (kbm_print_level >= 3)
1382 printf(" #Calling fsa_greater_than.\n");
1383 tmalloc(greater_than, fsa, 1);
1384 fsa_init(greater_than);
1385
1386 ngens = alphptr->size;
1387 greater_than->alphabet->type = PRODUCT;
1388 greater_than->alphabet->size = (ngens + 1) * (ngens + 1) - 1;
1389 greater_than->alphabet->arity = 2;
1390 greater_than->alphabet->padding = '_';
1391 tmalloc(greater_than->alphabet->base, srec, 1);
1392 srec_copy(greater_than->alphabet->base, alphptr);
1393
1394 greater_than->states->type = SIMPLE;
1395 greater_than->states->size = 4;
1396 /* state 1 = initial (fail state),
1397 * state 2 = words of equal length, lhs leading (accept state),
1398 * state 3 = words of equal length, rhs leading (fail state),
1399 * state 4 = eos on rhs (accept state),
1400 * state 0 = eos on lhs (dead state)
1401 */
1402
1403 greater_than->num_initial = 1;
1404 tmalloc(greater_than->initial, int, 2);
1405 greater_than->initial[1] = 1;
1406
1407 greater_than->num_accepting = 2;
1408 tmalloc(greater_than->accepting, int, 3);
1409 greater_than->accepting[1] = 2;
1410 greater_than->accepting[2] = 4;
1411
1412 greater_than->flags[DFA] = TRUE;
1413 greater_than->flags[MINIMIZED] = TRUE;
1414
1415 fsa_table_init(greater_than->table, 4, greater_than->alphabet->size);
1416 greater_than->table->printing_format = DENSE;
1417 greater_than->table->denserows = 0;
1418 if (fsa_table_dptr_init(greater_than) == -1)
1419 return 0;
1420 dtable = greater_than->table->table_data_dptr;
1421 p = ngens + 1;
1422 for (i = 1; i <= ngens; i++) {
1423 set_dense_dtarget(dtable, i, p, 1, 4);
1424 set_dense_dtarget(dtable, i, p, 2, 4);
1425 set_dense_dtarget(dtable, i, p, 3, 4);
1426 set_dense_dtarget(dtable, i, p, 4, 4);
1427 set_dense_dtarget(dtable, p, i, 1, 0);
1428 set_dense_dtarget(dtable, p, i, 2, 0);
1429 set_dense_dtarget(dtable, p, i, 3, 0);
1430 set_dense_dtarget(dtable, p, i, 4, 0);
1431 set_dense_dtarget(dtable, i, i, 1, 1);
1432 set_dense_dtarget(dtable, i, i, 2, 2);
1433 set_dense_dtarget(dtable, i, i, 3, 3);
1434 set_dense_dtarget(dtable, i, i, 4, 0);
1435 }
1436 for (i = 2; i <= ngens; i++)
1437 for (j = 1; j < i; j++) {
1438 set_dense_dtarget(dtable, i, j, 1, 2);
1439 set_dense_dtarget(dtable, j, i, 1, 3);
1440 set_dense_dtarget(dtable, i, j, 2, 2);
1441 set_dense_dtarget(dtable, j, i, 2, 2);
1442 set_dense_dtarget(dtable, i, j, 3, 3);
1443 set_dense_dtarget(dtable, j, i, 3, 3);
1444 set_dense_dtarget(dtable, i, j, 4, 0);
1445 set_dense_dtarget(dtable, j, i, 4, 0);
1446 }
1447
1448 return greater_than;
1449 }
1450