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