1 /* file fsatriples.c 14/11/94
2 * 6/8/98 large scale reorganisation to omit globals, etc.
3 * 13/1/98 changes for the `gen' type replacing char for generators.
4 * 2/5/96 - changed to make all labeled states accept states.
5 * 2/10/95 changed state-label type for genmult fsa from identifiers to
6 * list of words in the normal case - this makes it consistent with the
7 * cosets case, and also allows us to assign more than one generator to
8 * a label if soem of the generators happen to be equal.
9 * Also abolished the parameter idlabel, which is always true.
10 *
11 * This file contains the routine fsa_triples, which is used to construct the
12 * general product fsa in an automatic group.
13 * For general methodology, see comment at top of file fsalogic.c.
14 */
15
16 #include <stdio.h>
17 #include "defs.h"
18 #include "fsa.h"
19 #include "hash.h"
20 #include "rws.h"
21 #include "externals.h"
22
23 /* Functions defined in this file: */
24 static fsa *fsa_triples_short(fsa *waptr, fsa *diffptr,
25 storage_type op_table_type, boolean destroy,
26 char *tempfilename, reduction_equation *eqnptr,
27 int maxeqns, boolean eqnstop, boolean *foundeqns,
28 boolean readback);
29 static fsa *fsa_triples_int(fsa *waptr, fsa *diffptr,
30 storage_type op_table_type, boolean destroy,
31 char *tempfilename, reduction_equation *eqnptr,
32 int maxeqns, boolean eqnstop, boolean *foundeqns,
33 boolean readback);
34
35 /* *waptr is assumed to be the word-acceptor of an automatic group.
36 * (In particular, all states should be accepting.)
37 * *diffptr is assumed to be a word-difference machine of the same automatic
38 * group. Both are assumed to be stored in dense-format.
39 * This routine constructs the fsa of which the states are triples (s1,s2,d),
40 * with s1 and s2 states of *waptr and d a state of *diffptr.
41 * (More precisely, if *waptr has n states, then s1 and s2 may also be equal
42 * to n+1, meaning that the end of string symbol has been read on lhs or rhs.)
43 * The alphabet is 2-variable with base the alphabet of *waptr
44 * (i.e. the same alphabet as *diffptr).
45 * The alphabet member (g1,g2) maps (s1,s2,d) to (s1^g1,s2^g2,d^(g1,g2))
46 * if all three components are nonzero, and to zero otherwise.
47 * The transition-table of the resulting fsa is output in the usual way to
48 * file tempfilename with table-type specified by op_table_type, before
49 * minimisation.
50 * There are several categories of accept-states - one for each distinct
51 * group element of word-length 0 or 1, and these are specified by
52 * the labels of the states, which are lists of words (all words of length 1
53 * for the appropriate group element).
54 *
55 * If during the construction, a nontrivial equation between two words is
56 * discovered as a result of encountering the identity word-difference,
57 * then the word-acceptor *waptr must be accepting both of these words
58 * which represent the same group-element, and must therefore be wrong.
59 * The procedure therefore aborts without returning an fsa.
60 * If the maxeqns is greater than zero, then a maximum of maxeqns such
61 * equations are returned as eqnptr[i] - in order to do this, it is necessary
62 * to store the defining transitions of the states as we proceed.
63 */
fsa_triples(fsa * waptr,fsa * diffptr,storage_type op_table_type,boolean destroy,char * tempfilename,reduction_equation * eqnptr,int maxeqns,boolean eqnstop,boolean * foundeqns,boolean readback)64 fsa *fsa_triples(fsa *waptr, fsa *diffptr, storage_type op_table_type,
65 boolean destroy, char *tempfilename,
66 reduction_equation *eqnptr, int maxeqns, boolean eqnstop,
67 boolean *foundeqns, boolean readback)
68 {
69 if (kbm_print_level >= 3)
70 printf(" #Calling fsa_triples.\n");
71 if (waptr->states->size >= MAXUSHORT || diffptr->states->size >= MAXUSHORT)
72 return fsa_triples_int(waptr, diffptr, op_table_type, destroy, tempfilename,
73 eqnptr, maxeqns, eqnstop, foundeqns, readback);
74 else
75 return fsa_triples_short(waptr, diffptr, op_table_type, destroy,
76 tempfilename, eqnptr, maxeqns, eqnstop, foundeqns,
77 readback);
78 }
79
fsa_triples_short(fsa * waptr,fsa * diffptr,storage_type op_table_type,boolean destroy,char * tempfilename,reduction_equation * eqnptr,int maxeqns,boolean eqnstop,boolean * foundeqns,boolean readback)80 static fsa *fsa_triples_short(fsa *waptr, fsa *diffptr,
81 storage_type op_table_type, boolean destroy,
82 char *tempfilename, reduction_equation *eqnptr,
83 int maxeqns, boolean eqnstop, boolean *foundeqns,
84 boolean readback)
85 {
86 int **watable, ***difftable, identity, ngens, ngens1, nswa1, ne, ns, *fsarow,
87 nt, cstate, cswa1, cswa2, csdiff, im, i, j, k, e, len = 0, ct, bstate, bigger,
88 numeqns;
89 gen reduced_genno[MAXGEN + 1], reduced_gen[2];
90 /* for calculating and storing reductions of generators in case some
91 * generators happen to be equal to others.
92 */
93 int labno[MAXGEN + 1], nlab;
94 unsigned short *ht_ptr;
95 boolean dense_op;
96 fsa *triples;
97 srec *labels;
98 short_hash_table ht;
99 FILE *tempfile;
100 gen g1, g2, bg1, bg2;
101 int maxv = 65536;
102 reduction_struct rs_wd;
103 struct vertexd {
104 gen g1;
105 gen g2;
106 int state;
107 } * definition = 0, *newdef;
108 /* This is used to store the defining transition for the states of *triples.
109 * If definition[i] = v, then state i is defined by the transition from
110 * state v.state, with generator (v.g1,v.g2).
111 * State 1 does not have a definition.
112 */
113
114 if (kbm_print_level >= 3)
115 printf(" #Calling fsa_triples_short.\n");
116
117 if (!waptr->flags[DFA] || !diffptr->flags[DFA]) {
118 fprintf(stderr, "Error: fsa__triples only applies to DFA's.\n");
119 return 0;
120 }
121 if (waptr->alphabet->type != IDENTIFIERS) {
122 fprintf(stderr, "Error in fsa_triples: first fsa has wrong type.\n");
123 return 0;
124 }
125 if (waptr->num_accepting != waptr->states->size) {
126 fprintf(stderr,
127 "Error in fsa_triples: first fsa should be a word-acceptor.\n");
128 return 0;
129 }
130 if (diffptr->alphabet->type != PRODUCT || diffptr->alphabet->arity != 2) {
131 fprintf(stderr, "Error in fsa_triples: second fsa must be 2-variable.\n");
132 return 0;
133 }
134 if (diffptr->states->type != WORDS) {
135 fprintf(stderr,
136 "Error in fsa_triples: second fsa must be word-difference type.\n");
137 return 0;
138 }
139 if (!srec_equal(diffptr->alphabet->base, waptr->alphabet)) {
140 fprintf(stderr, "Error in fsa_triples: fsa's alphabet's don't match.\n");
141 return 0;
142 }
143
144 if (fsa_table_dptr_init(diffptr) == -1)
145 return 0;
146
147 if (maxeqns > 0) {
148 /* We need to remember vertex definitions */
149 tmalloc(definition, struct vertexd, maxv);
150 ns = 1;
151 }
152 *foundeqns = 0;
153
154 tmalloc(triples, fsa, 1);
155 fsa_init(triples);
156 srec_copy(triples->alphabet, diffptr->alphabet);
157 triples->flags[DFA] = TRUE;
158 triples->flags[ACCESSIBLE] = TRUE;
159 triples->flags[BFS] = TRUE;
160
161 ngens = waptr->alphabet->size;
162 ngens1 = ngens + 1;
163 ne = diffptr->alphabet->size;
164 nswa1 = waptr->states->size + 1;
165
166 if (ne != ngens1 * ngens1 - 1) {
167 fprintf(
168 stderr,
169 "Error: in a 2-variable fsa, alphabet size should = ngens^2 - 1.\n");
170 return 0;
171 }
172
173 watable = waptr->table->table_data_ptr;
174 difftable = diffptr->table->table_data_dptr;
175
176 dense_op = op_table_type == DENSE;
177
178 triples->num_initial = 1;
179 tmalloc(triples->initial, int, 2);
180 triples->initial[1] = 1;
181 triples->table->table_type = op_table_type;
182 triples->table->denserows = 0;
183 triples->table->printing_format = op_table_type;
184 if (!readback) {
185 tmalloc(triples->table->filename, char, stringlen(tempfilename) + 1);
186 strcpy(triples->table->filename, tempfilename);
187 }
188
189 short_hash_init(&ht, TRUE, 3, 0, 0);
190 ht_ptr = ht.current_ptr;
191 ht_ptr[0] = waptr->initial[1];
192 ht_ptr[1] = waptr->initial[1];
193 ht_ptr[2] = identity = diffptr->initial[1];
194 im = short_hash_locate(&ht, 3);
195 if (im == -1)
196 return 0;
197 if (im != 1) {
198 fprintf(stderr, "Hash-initialisation problem in fsa_triples.\n");
199 return 0;
200 }
201 if ((tempfile = fopen(tempfilename, "w")) == 0) {
202 fprintf(stderr, "Error: cannot open file %s\n", tempfilename);
203 return 0;
204 }
205 if (dense_op)
206 tmalloc(fsarow, int, ne) else tmalloc(fsarow, int, 2 * ne + 1)
207
208 cstate = 0;
209 if (dense_op)
210 len = ne; /* The length of the fsarow output. */
211 nt = 0; /* Number of transitions in triples */
212
213 numeqns = 0; /* this becomes nonzero when we have started collecting
214 * equations of equal words both accepted by word-acceptor.
215 */
216 while (++cstate <= ht.num_recs) {
217 if (kbm_print_level >= 3) {
218 if ((cstate <= 1000 && cstate % 100 == 0) ||
219 (cstate <= 10000 && cstate % 1000 == 0) ||
220 (cstate <= 100000 && cstate % 5000 == 0) || cstate % 50000 == 0)
221 printf(" #cstate = %d; number of states = %d.\n", cstate,
222 ht.num_recs);
223 }
224 ht_ptr = short_hash_rec(&ht, cstate);
225 cswa1 = ht_ptr[0];
226 cswa2 = ht_ptr[1];
227 csdiff = ht_ptr[2];
228 if (!dense_op)
229 len = 0;
230 e = 0; /* e is the number of the edge corresponding to the pair (g1,g2) */
231 for (g1 = 1; g1 <= ngens1; g1++)
232 for (g2 = 1; g2 <= ngens1; g2++) {
233 e++;
234 /* Calculate action of generator-pair (g1,g2) on state cstate */
235 if (g1 == ngens1 && g2 == ngens1)
236 continue;
237 ht_ptr = ht.current_ptr;
238 ht_ptr[2] = dense_dtarget(difftable, g1, g2, csdiff);
239 if (ht_ptr[2] == 0)
240 im = 0;
241 else {
242 ht_ptr[0] =
243 g1 > ngens
244 ? nswa1
245 : cswa1 == nswa1 ? 0 : dense_target(watable, g1, cswa1);
246 if (ht_ptr[0] == 0)
247 im = 0;
248 else {
249 ht_ptr[1] =
250 g2 > ngens
251 ? nswa1
252 : cswa2 == nswa1 ? 0 : dense_target(watable, g2, cswa2);
253 if (ht_ptr[1] == 0)
254 im = 0;
255 else {
256 if (eqnstop && ht_ptr[2] == identity && g1 != g2) {
257 /* This means that we have found a new equation between two
258 * distinct words accepted by the word-acceptor *gpwa, and so
259 * *gpwa must have been wrong.
260 */
261 *foundeqns = TRUE;
262 if (kbm_print_level > 0 && numeqns == 0)
263 printf("#Equation found between two words accepted by "
264 "word-acceptor.\n");
265 if (maxeqns > 0) { /* We reconstruct the equation explicitly */
266 /* First we calculate the length of the equation */
267 if (kbm_print_level >= 3)
268 printf(" #Calculating equation number %d.\n",
269 numeqns + 1);
270 len = 1;
271 bg1 = g1;
272 bg2 = g2;
273 bstate = cstate;
274 bigger = g2 > ngens ? 1 : g1 > ngens ? 2 : 0;
275 /* bigger=1 or 2 means resp. lhs/rhs larger in shortlex order
276 */
277 while (bstate != 1) {
278 len++;
279 bg1 = definition[bstate].g1;
280 bg2 = definition[bstate].g2;
281 bstate = definition[bstate].state;
282 }
283 if (bigger == 0)
284 bigger = bg1 > bg2 ? 1 : 2;
285
286 /* Now we allocate space for it and store it -
287 */
288 tmalloc(eqnptr[numeqns].lhs, gen, len + 1);
289 tmalloc(eqnptr[numeqns].rhs, gen, len + 1);
290 eqnptr[numeqns].lhs[len] = eqnptr[numeqns].rhs[len] = 0;
291 bg1 = g1;
292 bg2 = g2;
293 bstate = cstate;
294 while (1) {
295 len--;
296 if (bigger == 1) {
297 eqnptr[numeqns].lhs[len] = bg1 > ngens ? 0 : bg1;
298 eqnptr[numeqns].rhs[len] = bg2 > ngens ? 0 : bg2;
299 }
300 else {
301 eqnptr[numeqns].rhs[len] = bg1 > ngens ? 0 : bg1;
302 eqnptr[numeqns].lhs[len] = bg2 > ngens ? 0 : bg2;
303 }
304 if (bstate == 1)
305 break;
306 bg1 = definition[bstate].g1;
307 bg2 = definition[bstate].g2;
308 bstate = definition[bstate].state;
309 }
310 }
311
312 if (numeqns == 0) {
313 /* We are no longer constructing the fsa, so we no longer need
314 * the file. */
315 fclose(tempfile);
316 unlink(tempfilename);
317 }
318 numeqns++;
319 if (numeqns >= maxeqns) { /* exit */
320 if (kbm_print_level >= 2 && maxeqns > 0)
321 printf(" #Found %d new equations - aborting.\n", maxeqns);
322 short_hash_clear(&ht);
323 tfree(fsarow);
324 fsa_clear(triples);
325 tfree(triples);
326 if (maxeqns > 0)
327 tfree(definition);
328 if (destroy)
329 fsa_clear(waptr);
330 return 0;
331 }
332 else
333 eqnptr[numeqns].lhs = 0; /* to mark how many we have later */
334 }
335 im = short_hash_locate(&ht, 3);
336 if (im == -1)
337 return 0;
338 if (maxeqns > 0 && im > ns) {
339 ns++;
340 if (ns == maxv) { /* need room for more definitions */
341 if (kbm_print_level >= 3)
342 printf(
343 " #Allocating more space for vertex definitions.\n");
344 tmalloc(newdef, struct vertexd, 2 * maxv);
345 for (i = 1; i < maxv; i++)
346 newdef[i] = definition[i];
347 tfree(definition);
348 definition = newdef;
349 maxv *= 2;
350 }
351 definition[ns].g1 = g1;
352 definition[ns].g2 = g2;
353 definition[ns].state = cstate;
354 }
355 }
356 }
357 }
358
359 if (dense_op)
360 fsarow[e - 1] = im;
361 else if (im > 0) {
362 fsarow[++len] = e;
363 fsarow[++len] = im;
364 }
365 if (im > 0)
366 nt++;
367 } /* for (g1=1;g1<=ngens1; ... */
368 if (!dense_op)
369 fsarow[0] = len++;
370 if (numeqns == 0)
371 fwrite((void *)fsarow, sizeof(int), (size_t)len, tempfile);
372 } /*while (++cstate <= ht.num_recs) */
373
374 if (numeqns > 0) {
375 short_hash_clear(&ht);
376 tfree(fsarow);
377 fsa_clear(triples);
378 tfree(triples);
379 tfree(definition);
380 if (destroy)
381 fsa_clear(waptr);
382 if (kbm_print_level >= 2)
383 printf(" #Found %d new equations - aborting with algorithm complete.\n",
384 numeqns);
385 return 0;
386 }
387
388 fclose(tempfile);
389
390 triples->states->type = LABELED;
391 tmalloc(triples->states->labels, srec, 1);
392 ns = triples->states->size = ht.num_recs;
393 triples->table->numTransitions = nt;
394
395 if (kbm_print_level >= 3) {
396 printf(" #Calculated transitions - %d states, %d transitions.\n", ns,
397 nt);
398 printf(" #Now calculating state labels.\n");
399 }
400 tmalloc(triples->states->setToLabels, setToLabelsType, ns + 1);
401 triples->states->setToLabels[0] = 0;
402 /* First we calculate the array reduced_genno, to record if any generators
403 * are equal to a lower one.
404 */
405 reduced_genno[0] = 0;
406 rs_wd.wd_fsa = diffptr;
407 for (i = 1; i <= ngens; i++) {
408 reduced_gen[0] = i;
409 reduced_gen[1] = 0;
410 diff_reduce(reduced_gen, &rs_wd);
411 reduced_genno[i] = reduced_gen[0]; /* also OK if equal to null-string */
412 }
413 for (i = 0; i <= ngens; i++)
414 labno[i] = 0;
415 labels = triples->states->labels;
416 labels->type = LISTOFWORDS;
417 for (i = 1; i <= ngens; i++) {
418 tmalloc(labels->alphabet[i], char,
419 stringlen(waptr->alphabet->names[i]) + 1);
420 strcpy(labels->alphabet[i], waptr->alphabet->names[i]);
421 }
422 labels->alphabet_size = ngens;
423 tmalloc(labels->wordslist, gen **, ngens + 2);
424 /* All states whose label has length <=1 will be classed as accept states,
425 * since they are accept-states for some generator.
426 * We need to mark them specifically in the "mi" case, since the information
427 * is needed by the minimsation function midfa_labeled_minimize".
428 */
429 tmalloc(triples->is_accepting, boolean, ns + 1);
430 for (i = 1; i <= ns; i++)
431 triples->is_accepting[i] = FALSE;
432 triples->num_accepting = 0;
433 nlab = 0;
434 for (i = 1; i <= ns; i++) {
435 ht_ptr = short_hash_rec(&ht, i);
436 csdiff = ht_ptr[2];
437 len = genstrlen(diffptr->states->words[csdiff]);
438 if (len <= 1) {
439 triples->is_accepting[i] = TRUE;
440 triples->num_accepting++;
441 j = (len == 0) ? 0 : diffptr->states->words[csdiff][0];
442 if (labno[j] > 0)
443 triples->states->setToLabels[i] = labno[j];
444 else {
445 /* new label - first see how many generators reduce to this */
446 nlab++;
447 ct = 0;
448 for (k = 0; k <= ngens; k++)
449 if (reduced_genno[k] == reduced_genno[j]) {
450 ct++;
451 labno[k] = nlab;
452 }
453 tmalloc(labels->wordslist[nlab], gen *, ct + 1);
454 ct = 0;
455 for (k = 0; k <= ngens; k++)
456 if (reduced_genno[k] == reduced_genno[j]) {
457 if (k == 0) {
458 tmalloc(labels->wordslist[nlab][ct], gen, 1);
459 labels->wordslist[nlab][ct][0] = 0;
460 }
461 else {
462 tmalloc(labels->wordslist[nlab][ct], gen, 2);
463 labels->wordslist[nlab][ct][0] = k;
464 labels->wordslist[nlab][ct][1] = 0;
465 }
466 ct++;
467 }
468 labels->wordslist[nlab][ct] = 0;
469 triples->states->setToLabels[i] = nlab;
470 }
471 }
472 else
473 triples->states->setToLabels[i] = 0;
474 }
475 labels->size = nlab;
476
477 short_hash_clear(&ht);
478 tfree(fsarow);
479 if (maxeqns > 0)
480 tfree(definition);
481 /* Now read the transition table back in */
482 if (readback) {
483 tempfile = fopen(tempfilename, "r");
484 compressed_transitions_read(triples, tempfile);
485 fclose(tempfile);
486 unlink(tempfilename);
487 }
488 tmalloc(triples->accepting, int, triples->num_accepting + 1);
489 ct = 0;
490 for (i = 1; i <= ns; i++)
491 if (triples->is_accepting[i])
492 triples->accepting[++ct] = i;
493 tfree(triples->is_accepting);
494 if (destroy) {
495 fsa_clear(waptr);
496 fsa_clear(diffptr);
497 }
498
499 return triples;
500 }
501
fsa_triples_int(fsa * waptr,fsa * diffptr,storage_type op_table_type,boolean destroy,char * tempfilename,reduction_equation * eqnptr,int maxeqns,boolean eqnstop,boolean * foundeqns,boolean readback)502 static fsa *fsa_triples_int(fsa *waptr, fsa *diffptr,
503 storage_type op_table_type, boolean destroy,
504 char *tempfilename, reduction_equation *eqnptr,
505 int maxeqns, boolean eqnstop, boolean *foundeqns,
506 boolean readback)
507 {
508 int **watable, ***difftable, identity, ngens, ngens1, nswa1, ne, ns, *fsarow,
509 nt, cstate, cswa1, cswa2, csdiff, im, i, j, k, e, len = 0, ct, bstate, bigger,
510 numeqns;
511 gen reduced_genno[MAXGEN + 1], reduced_gen[2];
512 /* for calculating and storing reductions of generators in case some
513 * generators happen to be equal to others.
514 */
515 int labno[MAXGEN + 1], nlab;
516 int *ht_ptr;
517 boolean dense_op;
518 fsa *triples;
519 srec *labels;
520 hash_table ht;
521 FILE *tempfile;
522 gen g1, g2, bg1, bg2;
523 int maxv = 65536;
524 reduction_struct rs_wd;
525 struct vertexd {
526 gen g1;
527 gen g2;
528 int state;
529 } * definition = 0, *newdef;
530 /* This is used to store the defining transition for the states of *triples.
531 * If definition[i] = v, then state i is defined by the transition from
532 * state v.state, with generator (v.g1,v.g2).
533 * State 1 does not have a definition.
534 */
535
536 if (kbm_print_level >= 3)
537 printf(" #Calling fsa_triples_short.\n");
538
539 if (!waptr->flags[DFA] || !diffptr->flags[DFA]) {
540 fprintf(stderr, "Error: fsa__triples only applies to DFA's.\n");
541 return 0;
542 }
543 if (waptr->alphabet->type != IDENTIFIERS) {
544 fprintf(stderr, "Error in fsa_triples: first fsa has wrong type.\n");
545 return 0;
546 }
547 if (waptr->num_accepting != waptr->states->size) {
548 fprintf(stderr,
549 "Error in fsa_triples: first fsa should be a word-acceptor.\n");
550 return 0;
551 }
552 if (diffptr->alphabet->type != PRODUCT || diffptr->alphabet->arity != 2) {
553 fprintf(stderr, "Error in fsa_triples: second fsa must be 2-variable.\n");
554 return 0;
555 }
556 if (diffptr->states->type != WORDS) {
557 fprintf(stderr,
558 "Error in fsa_triples: second fsa must be word-difference type.\n");
559 return 0;
560 }
561 if (!srec_equal(diffptr->alphabet->base, waptr->alphabet)) {
562 fprintf(stderr, "Error in fsa_triples: fsa's alphabet's don't match.\n");
563 return 0;
564 }
565
566 if (fsa_table_dptr_init(diffptr) == -1)
567 return 0;
568
569 if (maxeqns > 0) {
570 /* We need to remember vertex definitions */
571 tmalloc(definition, struct vertexd, maxv);
572 ns = 1;
573 }
574 *foundeqns = 0;
575
576 tmalloc(triples, fsa, 1);
577 fsa_init(triples);
578 srec_copy(triples->alphabet, diffptr->alphabet);
579 triples->flags[DFA] = TRUE;
580 triples->flags[ACCESSIBLE] = TRUE;
581 triples->flags[BFS] = TRUE;
582
583 ngens = waptr->alphabet->size;
584 ngens1 = ngens + 1;
585 ne = diffptr->alphabet->size;
586 nswa1 = waptr->states->size + 1;
587
588 if (ne != ngens1 * ngens1 - 1) {
589 fprintf(
590 stderr,
591 "Error: in a 2-variable fsa, alphabet size should = ngens^2 - 1.\n");
592 return 0;
593 }
594
595 watable = waptr->table->table_data_ptr;
596 difftable = diffptr->table->table_data_dptr;
597
598 dense_op = op_table_type == DENSE;
599
600 triples->num_initial = 1;
601 tmalloc(triples->initial, int, 2);
602 triples->initial[1] = 1;
603 triples->table->table_type = op_table_type;
604 triples->table->denserows = 0;
605 triples->table->printing_format = op_table_type;
606 if (!readback) {
607 tmalloc(triples->table->filename, char, stringlen(tempfilename) + 1);
608 strcpy(triples->table->filename, tempfilename);
609 }
610
611 hash_init(&ht, TRUE, 3, 0, 0);
612 ht_ptr = ht.current_ptr;
613 ht_ptr[0] = waptr->initial[1];
614 ht_ptr[1] = waptr->initial[1];
615 ht_ptr[2] = identity = diffptr->initial[1];
616 im = hash_locate(&ht, 3);
617 if (im == -1)
618 return 0;
619 if (im != 1) {
620 fprintf(stderr, "Hash-initialisation problem in fsa_triples.\n");
621 return 0;
622 }
623 if ((tempfile = fopen(tempfilename, "w")) == 0) {
624 fprintf(stderr, "Error: cannot open file %s\n", tempfilename);
625 return 0;
626 }
627 if (dense_op)
628 tmalloc(fsarow, int, ne) else tmalloc(fsarow, int, 2 * ne + 1)
629
630 cstate = 0;
631 if (dense_op)
632 len = ne; /* The length of the fsarow output. */
633 nt = 0; /* Number of transitions in triples */
634
635 numeqns = 0; /* this becomes nonzero when we have started collecting
636 * equations of equal words both accepted by word-acceptor.
637 */
638 while (++cstate <= ht.num_recs) {
639 if (kbm_print_level >= 3) {
640 if ((cstate <= 1000 && cstate % 100 == 0) ||
641 (cstate <= 10000 && cstate % 1000 == 0) ||
642 (cstate <= 100000 && cstate % 5000 == 0) || cstate % 50000 == 0)
643 printf(" #cstate = %d; number of states = %d.\n", cstate,
644 ht.num_recs);
645 }
646 ht_ptr = hash_rec(&ht, cstate);
647 cswa1 = ht_ptr[0];
648 cswa2 = ht_ptr[1];
649 csdiff = ht_ptr[2];
650 if (!dense_op)
651 len = 0;
652 e = 0; /* e is the number of the edge corresponding to the pair (g1,g2) */
653 for (g1 = 1; g1 <= ngens1; g1++)
654 for (g2 = 1; g2 <= ngens1; g2++) {
655 e++;
656 /* Calculate action of generator-pair (g1,g2) on state cstate */
657 if (g1 == ngens1 && g2 == ngens1)
658 continue;
659 ht_ptr = ht.current_ptr;
660 ht_ptr[2] = dense_dtarget(difftable, g1, g2, csdiff);
661 if (ht_ptr[2] == 0)
662 im = 0;
663 else {
664 ht_ptr[0] =
665 g1 > ngens
666 ? nswa1
667 : cswa1 == nswa1 ? 0 : dense_target(watable, g1, cswa1);
668 if (ht_ptr[0] == 0)
669 im = 0;
670 else {
671 ht_ptr[1] =
672 g2 > ngens
673 ? nswa1
674 : cswa2 == nswa1 ? 0 : dense_target(watable, g2, cswa2);
675 if (ht_ptr[1] == 0)
676 im = 0;
677 else {
678 if (eqnstop && ht_ptr[2] == identity && g1 != g2) {
679 /* This means that we have found a new equation between two
680 * distinct words accepted by the word-acceptor *gpwa, and so
681 * *gpwa must have been wrong.
682 */
683 *foundeqns = TRUE;
684 if (kbm_print_level > 0 && numeqns == 0)
685 printf("#Equation found between two words accepted by "
686 "word-acceptor.\n");
687 if (maxeqns > 0) { /* We reconstruct the equation explicitly */
688 /* First we calculate the length of the equation */
689 if (kbm_print_level >= 3)
690 printf(" #Calculating equation number %d.\n",
691 numeqns + 1);
692 len = 1;
693 bg1 = g1;
694 bg2 = g2;
695 bstate = cstate;
696 bigger = g2 > ngens ? 1 : g1 > ngens ? 2 : 0;
697 /* bigger=1 or 2 means resp. lhs/rhs larger in shortlex order
698 */
699 while (bstate != 1) {
700 len++;
701 bg1 = definition[bstate].g1;
702 bg2 = definition[bstate].g2;
703 bstate = definition[bstate].state;
704 }
705 if (bigger == 0)
706 bigger = bg1 > bg2 ? 1 : 2;
707
708 /* Now we allocate space for it and store it -
709 */
710 tmalloc(eqnptr[numeqns].lhs, gen, len + 1);
711 tmalloc(eqnptr[numeqns].rhs, gen, len + 1);
712 eqnptr[numeqns].lhs[len] = eqnptr[numeqns].rhs[len] = 0;
713 bg1 = g1;
714 bg2 = g2;
715 bstate = cstate;
716 while (1) {
717 len--;
718 if (bigger == 1) {
719 eqnptr[numeqns].lhs[len] = bg1 > ngens ? 0 : bg1;
720 eqnptr[numeqns].rhs[len] = bg2 > ngens ? 0 : bg2;
721 }
722 else {
723 eqnptr[numeqns].rhs[len] = bg1 > ngens ? 0 : bg1;
724 eqnptr[numeqns].lhs[len] = bg2 > ngens ? 0 : bg2;
725 }
726 if (bstate == 1)
727 break;
728 bg1 = definition[bstate].g1;
729 bg2 = definition[bstate].g2;
730 bstate = definition[bstate].state;
731 }
732 }
733
734 if (numeqns == 0) {
735 /* We are no longer constructing the fsa, so we no longer need
736 * the file. */
737 fclose(tempfile);
738 unlink(tempfilename);
739 }
740 numeqns++;
741 if (numeqns >= maxeqns) { /* exit */
742 if (kbm_print_level >= 2 && maxeqns > 0)
743 printf(" #Found %d new equations - aborting.\n", maxeqns);
744 hash_clear(&ht);
745 tfree(fsarow);
746 fsa_clear(triples);
747 tfree(triples);
748 if (maxeqns > 0)
749 tfree(definition);
750 if (destroy)
751 fsa_clear(waptr);
752 return 0;
753 }
754 else
755 eqnptr[numeqns].lhs = 0; /* to mark how many we have later */
756 }
757 im = hash_locate(&ht, 3);
758 if (im == -1)
759 return 0;
760 if (maxeqns > 0 && im > ns) {
761 ns++;
762 if (ns == maxv) { /* need room for more definitions */
763 if (kbm_print_level >= 3)
764 printf(
765 " #Allocating more space for vertex definitions.\n");
766 tmalloc(newdef, struct vertexd, 2 * maxv);
767 for (i = 1; i < maxv; i++)
768 newdef[i] = definition[i];
769 tfree(definition);
770 definition = newdef;
771 maxv *= 2;
772 }
773 definition[ns].g1 = g1;
774 definition[ns].g2 = g2;
775 definition[ns].state = cstate;
776 }
777 }
778 }
779 }
780
781 if (dense_op)
782 fsarow[e - 1] = im;
783 else if (im > 0) {
784 fsarow[++len] = e;
785 fsarow[++len] = im;
786 }
787 if (im > 0)
788 nt++;
789 } /* for (g1=1;g1<=ngens1; ... */
790 if (!dense_op)
791 fsarow[0] = len++;
792 if (numeqns == 0)
793 fwrite((void *)fsarow, sizeof(int), (size_t)len, tempfile);
794 } /*while (++cstate <= ht.num_recs) */
795
796 if (numeqns > 0) {
797 hash_clear(&ht);
798 tfree(fsarow);
799 fsa_clear(triples);
800 tfree(triples);
801 tfree(definition);
802 if (destroy)
803 fsa_clear(waptr);
804 if (kbm_print_level >= 2)
805 printf(" #Found %d new equations - aborting with algorithm complete.\n",
806 numeqns);
807 return 0;
808 }
809
810 fclose(tempfile);
811
812 triples->states->type = LABELED;
813 tmalloc(triples->states->labels, srec, 1);
814 ns = triples->states->size = ht.num_recs;
815 triples->table->numTransitions = nt;
816
817 if (kbm_print_level >= 3) {
818 printf(" #Calculated transitions - %d states, %d transitions.\n", ns,
819 nt);
820 printf(" #Now calculating state labels.\n");
821 }
822 tmalloc(triples->states->setToLabels, setToLabelsType, ns + 1);
823 triples->states->setToLabels[0] = 0;
824 /* First we calculate the array reduced_genno, to record if any generators
825 * are equal to a lower one.
826 */
827 reduced_genno[0] = 0;
828 rs_wd.wd_fsa = diffptr;
829 for (i = 1; i <= ngens; i++) {
830 reduced_gen[0] = i;
831 reduced_gen[1] = 0;
832 diff_reduce(reduced_gen, &rs_wd);
833 reduced_genno[i] = reduced_gen[0]; /* also OK if equal to null-string */
834 }
835 for (i = 0; i <= ngens; i++)
836 labno[i] = 0;
837 labels = triples->states->labels;
838 labels->type = LISTOFWORDS;
839 for (i = 1; i <= ngens; i++) {
840 tmalloc(labels->alphabet[i], char,
841 stringlen(waptr->alphabet->names[i]) + 1);
842 strcpy(labels->alphabet[i], waptr->alphabet->names[i]);
843 }
844 labels->alphabet_size = ngens;
845 tmalloc(labels->wordslist, gen **, ngens + 2);
846 /* All states whose label has length <=1 will be classed as accept states,
847 * since they are accept-states for some generator.
848 * We need to mark them specifically in the "mi" case, since the information
849 * is needed by the minimsation function midfa_labeled_minimize".
850 */
851 tmalloc(triples->is_accepting, boolean, ns + 1);
852 for (i = 1; i <= ns; i++)
853 triples->is_accepting[i] = FALSE;
854 triples->num_accepting = 0;
855 nlab = 0;
856 for (i = 1; i <= ns; i++) {
857 ht_ptr = hash_rec(&ht, i);
858 csdiff = ht_ptr[2];
859 len = genstrlen(diffptr->states->words[csdiff]);
860 if (len <= 1) {
861 triples->is_accepting[i] = TRUE;
862 triples->num_accepting++;
863 j = (len == 0) ? 0 : diffptr->states->words[csdiff][0];
864 if (labno[j] > 0)
865 triples->states->setToLabels[i] = labno[j];
866 else {
867 /* new label - first see how many generators reduce to this */
868 nlab++;
869 ct = 0;
870 for (k = 0; k <= ngens; k++)
871 if (reduced_genno[k] == reduced_genno[j]) {
872 ct++;
873 labno[k] = nlab;
874 }
875 tmalloc(labels->wordslist[nlab], gen *, ct + 1);
876 ct = 0;
877 for (k = 0; k <= ngens; k++)
878 if (reduced_genno[k] == reduced_genno[j]) {
879 if (k == 0) {
880 tmalloc(labels->wordslist[nlab][ct], gen, 1);
881 labels->wordslist[nlab][ct][0] = 0;
882 }
883 else {
884 tmalloc(labels->wordslist[nlab][ct], gen, 2);
885 labels->wordslist[nlab][ct][0] = k;
886 labels->wordslist[nlab][ct][1] = 0;
887 }
888 ct++;
889 }
890 labels->wordslist[nlab][ct] = 0;
891 triples->states->setToLabels[i] = nlab;
892 }
893 }
894 else
895 triples->states->setToLabels[i] = 0;
896 }
897 labels->size = nlab;
898
899 hash_clear(&ht);
900 tfree(fsarow);
901 if (maxeqns > 0)
902 tfree(definition);
903 /* Now read the transition table back in */
904 if (readback) {
905 tempfile = fopen(tempfilename, "r");
906 compressed_transitions_read(triples, tempfile);
907 fclose(tempfile);
908 unlink(tempfilename);
909 }
910 tmalloc(triples->accepting, int, triples->num_accepting + 1);
911 ct = 0;
912 for (i = 1; i <= ns; i++)
913 if (triples->is_accepting[i])
914 triples->accepting[++ct] = i;
915 tfree(triples->is_accepting);
916 if (destroy) {
917 fsa_clear(waptr);
918 fsa_clear(diffptr);
919 }
920
921 return triples;
922 }
923