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