2/6/98 - large-scale re-organisation. Abolish almost all global variables and make them components of the rws structure. 17/1/98 - changes resulting from introduction of `gen' type in place of char for generators.
8/8/96 - -ve option to print all equations as found to stdout. - -vv option for more diagnostic output.
8/1/96 - output a file gpname.kbprog.exitcode containing a GAP statement giving the exit code - for use with GAP interface
6/5/96 - introduced -vwd option (verbose word-differences) to output new word-differences as they are found, together with the reduction equation that they come from.
29/5/95 - introduced -mo option to limit length of overlap length in processed pairs.
27/3/95 - introduced Rabin-Karp as alternative reduction procedure for longer left hand sides, + associated "-rk minlen mineqns" option.
14/3/95 - introduced -ro option to resume, but re-including the original equations
3/3/95 - started introduction of wtlex and wreathprod orderings.
31/1/95 - bug corrected due to building full table when one lhs is a prefix of another. Patch by doing repeated tidyings before building full table. Also introduced variable lostinfo - this is set true if an equation is discarded because it is too long during tidying - when this happens, the monoid may have changed. Warning message printed at end when this occurs.
18/1/95 various reorganisation - extra components to rws structure (including test1, test2 -> rws.testword1,rws.testword2). automatic doubling of maxslowhistoryspace when required option -mrl n to set maxreducelen file rwsio.c reorganised and split into rwsio.c and rwsio2.c.
13/1/95 introduced exit code 0 for "successful" completion.
24/12/94 introduced variable current_maxstates - unlike maxstates, this may be increased (doubled) if necessary. If maxstates is set explicitly, then current_maxstates and maxstates are equal. Otherwise, the initial value of current_maxstates is determined by allotting INIT_FSASPACE space to the reduction automaton.
21/12/94 introduced wd_record array to remember progress of calculation and try to decide when to stop; also options -mt and -hf (see below).
9/11/94 introduced options -v, -silent for verbosity of output - same in all other programs.
6/10/94 - reduction algorithms moved to file reduce.c Also rws structure introduced.
27/9/94 - (i) Changed field-name generators to generatorOrder in input/output files. (ii) Introduced -op option to output prefixes corresponding to states of fsa.
22/9/94 - (i) introduced boolean array done. For i an equation number, done[i] true means that equation number i has been processed. So if done[i] and done[j] are both true, then there is no need to test for overlaps. This is mainly useful when re-running. (ii) The option -r (resume) to take input from group.kbprog, presumed to be output of a previous run. (iii) -cn confnum option introduced. If more than this number of pairs of equations.eqns are tested for overlaps with no new equations.eqns being discovered, then a fast check for confluence is made using routine conf_check. confnum=0 switches this test off.
This is the version with GAP input/output by dfh starting 13/9/94 (using some ideas and code by Peter Proehle of 9/5/94) A new feature - not all generators need have inverses listed, but all listed inverses must be 2-sided, and the inv_of function must be involutory. Only generators with inverses will be cancelled in the routine "insert".
!! options added by dfh starting 30/3/94. -mlr maxlenleft maxlenright Only equations with lhs having length at most maxlenleft, rhs having length at most maxlenright are stored.
-sort maxoplen Output rules up to length of lhs up to maxoplen in increasing order of length of lhs. (maxoplen=0 means no maximum)
Some changes were made to this code by Jamie P. Curmi during February/March 1992.
OPTIONS -r Resume. Take input from groupname.kbprog - output also goes to groupname.kbprog and overwrites input.
-ro Resume. Take input from groupname.kbprog, and also re-read the original equations from groupname and append them to the end - output also goes to groupname.kbprog and overwrites input.
-t tidyint Set the value of rws.tidyint equal to tidyint.
-me maxeqns At most maxeqns equations are allowed. If more are generated, tidying up and output occur.
-ms maxstates At most maxstates states are allowed in the fsa. If more are generated, tidying up and output occur.
-sort maxoplen The equations are sorted into increasing length order before output. Only those with lhs up to length maxoplen are output. maxoplen=0 means no restriction.
-mlr maxlenleft maxlenright Only equations with lhs and rhs of lengths at most maxlenleft and maxlenright are stored.
-mo maxoverlaplen Only overlaps of total length at most maxoverlaplen are processed.
-lex Short-lexicographical ordering ** THE DEFAULT SETTING ** This is the original ordering used in kbprog.c. The ordering is lexicographic, with longer words having higher order than shorter words.
-rec Recursive Path ordering ordering based on that described in the book "Confluent String Rewriting" by Matthias Jantzen, Defn 1.2.14, page 24. The algorithm is described at the header of 'rec_compare'
-rtrec Recursive Path ordering ordering based on that described in the book "Confluent String Rewriting" by Matthias Jantzen, Defn 1.2.14, page 24. The algorithm is described at the header of 'rt_rec_compare' rtrec orders from the right of the words, whereas rec orders from the left - sometimes one is more efficient than the other in particular examples.
-wtlex Weighted short-lexicographical ordering A generalisation of shortlex. All generators have a weight (specified in the input file), and the weights of the generators in a word are added up to determine the "length" of the word. So shortlex is the special case where all weights are 1.
-wreath Wreath product ordering, as defined in Sims' book. A generalisation of recursive, where the generators have levels, and words in genertators at a fixed level are compared using shortlex. Recursive is the special case where the levels are 1,2,3,...
-cn confnum If confnum pairs of equations are processed for overlaps and no new equations are discovered, then a fast confluence test is performed. Setting confnum=0 turns this off. -mt min_time -hf halting_factor Only applies when word-differences are being computed. (Roughly) if halting_factor is set to be > 0, and the number of equations and the number of states has increased by more than halting_factor percent since the number of word-differences was last less than what it now is, and at least min_time seconds have elapsed, then halt. Alternatively, halt irrespective of elapsed time if number of equations has increased by 2*halting_factor percent. These conditions are highly experimental. -op The states of the fsa correspond to prefixes of the left hand sides of equations When this option is set, these prefixes are output as state-names. -rk minlen mineqns When there are at least mineqns equations, start using the Rabin-Karp reduction method on left-hand-sides having length at least minlen -wd After each tidying, calculate word-differences and re-order equations so that those which result in the word-difference fsa changing get higher priority in the Knuth-Bendix. On completion, the word-difference machines are output instead of the updated rewriting system. -vwd (verbose word-differences) out put new word-differences as they are found, together with the equation they come from. -mwd maxwdiffs Set the maximum number of worddiffs to be maxwdiffs.
-silent No output to stdout. -v Verbose output. -ve Print all equations as found with overlap information. -vv Very verbose output - print more diagnostic information.
EXIT STATUS: 0 if completion is successful, in the sense that either a confluent set is produced, or the halting-factor conditions are satisfied when word- differences are being computed. This is for use in the "automata" shellscript. 1 for badusage_kbprog, failure of malloc, etc., 2 if there is output, but completion is not successful in the sense above.
CHANGES TO KBPROG The orderings options -red, -rtred above. I have tried to make the code as easy as possible to modify in case new ordering options are to be included (such as weighted lexicographical ordering) in the future.
The code has been 'beautified' using a C-Beautifier on our system. This helped with my understanding of the algorithms, and modifications. - J.P.Curmi (1992)
boolean kbm_onintr; /* set true on interrupt signal */ staticchar inf[100], /* name of input file */
outf[100], /* name of output file for rewriting system
= inf.kbprog */
outfr[100], /* name of output file for rws.reduction_fsa
for rewriting system - inf.reduce */
outf1[100], /* name of output file for first wd-machine
= inf.diff1 */
outf2[100], /* name of output file for second wd-machine
= inf.diff2 */
outfec[100], /* name of output file for GAP exit code
= inf.kbprog.ec */
outflog[100]; /* name of logfile for automata run */ static FILE *rfile, *wfile;
/* Functions defined in this file: */ staticvoid badusage(void); staticvoid output_and_exit_kbprog(rewriting_system *rwsptr);
/* When the program receives an interrupt signal, it continues until the * next tidying, and then stops and outputs.
*/ void interrupt_kbprog(int sig)
{
kbm_onintr = TRUE;
signal(SIGINT, SIG_DFL);
signal(SIGKILL, SIG_DFL);
signal(SIGQUIT, SIG_DFL);
}
int main(int argc, char *argv[])
{
rewriting_system rws;
rewriting_system *rwsptr; int i, k;
/* First set some default values of the rewriting-system fields. They may be * overridden by command-line or input in file.
*/
rwsptr = &rws;
set_defaults(rwsptr, FALSE);
read_kbprog_command(argc, argv, rwsptr);
rws.print_eqns = kbm_print_level > 2 && kbm_print_level % 5 == 0;
if (rws.resume) { if ((rfile = fopen(outf, "r")) == 0) {
fprintf(stderr, "Error: cannot open file %s\n", outf); exit(1);
}
read_kbinput(rfile, FALSE, rwsptr); /* If we are re-running from previous output, validity checks on input * should not be necessary.
*/
} else { if ((rfile = fopen(inf, "r")) == 0) {
fprintf(stderr, "Error: cannot open file %s\n", inf); exit(1);
}
read_kbinput(rfile, TRUE, rwsptr);
}
fclose(rfile);
if (rws.resume_with_orig) { if ((rfile = fopen(inf, "r")) == 0) {
fprintf(stderr, "Error: cannot open file %s\n", inf); exit(1);
}
read_extra_kbinput(rfile, FALSE, rwsptr);
fclose(rfile);
}
if (rws.maxlenleft > 0) {
k = rws.maxlenleft > rws.maxlenright ? rws.maxlenleft : rws.maxlenright; if (rws.maxreducelen > MAXREDUCELENFAC * k)
rws.maxreducelen = 50 * k;
}
if (rws.worddiffs) { /* if (rws.ordering != SHORTLEX) { fprintf(stderr, "Word-difference calculation only makes sense for the shortlex ordering.\n"); exit(1); }
*/ if (!rws.confnumset)
rws.confnum *= 8; /* If we are calculating word-differences, we are not interested in * lots of confluence tests.
*/ for (i = 1; i <= rws.num_gens; i++) if (rws.inv_of[i] == 0) {
fprintf(stderr, "Word-difference calculation requires that all " "generators have inverses.\n"); exit(1);
}
tmalloc(rws.wd_fsa, fsa, 1); if (initialise_wd_fsa(rws.wd_fsa, rws.reduction_fsa->alphabet,
rws.maxwdiffs) == -1) exit(1);
tmalloc(rws.wd_record, struct wdr, MAXCYCLES + 1);
rws.hadct = 0;
rws.tot_eqns = 0;
}
if (kbprog(rwsptr) == -1) exit(1);
output_and_exit_kbprog(rwsptr); return 0;
}
staticvoid output_and_exit_kbprog(rewriting_system *rwsptr)
{ int i, j, l;
gen **pref, *w; int ndiff1, ndiff2;
reduction_struct rs_rws;
rs_rws.rws = rwsptr; if (rwsptr->exit_status == 1) exit(rwsptr->exit_status); if (rwsptr->worddiffs) {
rwsptr->new_wd = 0;
build_wd_fsa(rwsptr->wd_fsa, rwsptr->new_wd, &rs_rws);
should_we_halt(rwsptr); /* to calculate factors */
ndiff1 = rwsptr->wd_fsa->states->size;
wfile = fopen(outf1, "w");
print_wdoutput(wfile, ".diff1", rwsptr);
fclose(wfile); if (make_full_wd_fsa(rwsptr->wd_fsa, rwsptr->inv_of, 1, &rs_rws) == -1) exit(1);
ndiff2 = rwsptr->wd_fsa->states->size;
wfile = fopen(outf2, "w");
print_wdoutput(wfile, ".diff2", rwsptr);
fclose(wfile);
fsa_clear(rwsptr->wd_fsa);
tfree(rwsptr->wd_fsa); if (kbm_print_level > 0) {
printf("#Halting with %d equations.\n", rwsptr->num_eqns);
printf("#First word-difference machine with %d states computed.\n",
ndiff1);
printf("#Second word-difference machine with %d states computed.\n",
ndiff2);
} if (kbm_print_level >= 2) {
printf(" #eqn_factor=%d, states_factor=%d\n", rwsptr->eqn_factor,
rwsptr->states_factor);
} if (rwsptr->exit_status == 0 && kbm_print_level > 0)
printf("#System is confluent, or halting factor condition holds.\n");
tfree(rwsptr->wd_record); if (rwsptr->rk_on)
rk_clear(rwsptr);
} else { if (rwsptr->sorteqns)
sort_eqns(rwsptr->maxoplen, rwsptr);
wfile = fopen(outf, "w");
print_kboutput(wfile, rwsptr);
fclose(wfile); /* We complete the definition of the fsa before printing it */
strcat(rwsptr->name, ".reductionFSA");
rwsptr->reduction_fsa->states->size = rwsptr->num_states;
rwsptr->reduction_fsa->num_accepting = rwsptr->num_states; if (rwsptr->num_states == 1) {
tmalloc(rwsptr->reduction_fsa->accepting, int, 2);
rwsptr->reduction_fsa->accepting[1] = 1;
} if (rwsptr->outputprefixes) { /* In this case we want to output the prefixes of the left-hand sides of * equations associated with the states. First we must calculate them.
*/
rwsptr->reduction_fsa->states->type = WORDS;
rwsptr->reduction_fsa->states->alphabet_size =
rwsptr->reduction_fsa->alphabet->size; for (i = 1; i <= rwsptr->reduction_fsa->alphabet->size; i++) {
tmalloc(rwsptr->reduction_fsa->states->alphabet[i], char,
stringlen(rwsptr->reduction_fsa->alphabet->names[i]) + 1);
strcpy(rwsptr->reduction_fsa->states->alphabet[i],
rwsptr->reduction_fsa->alphabet->names[i]);
}
tmalloc(rwsptr->reduction_fsa->states->words, gen *,
rwsptr->num_states + 1);
pref = rwsptr->reduction_fsa->states->words; for (i = 1; i <= rwsptr->num_states; i++) {
l = rwsptr->preflen[i];
w = rwsptr->eqns[rwsptr->prefno[i]].lhs; /* Copy prefix from w to pref[i] */
tmalloc(pref[i], gen, l + 1); for (j = 0; j < l; j++)
pref[i][j] = w[j];
pref[i][l] = 0;
}
}
wfile = fopen(outfr, "w");
fsa_print(wfile, rwsptr->reduction_fsa, rwsptr->name);
fclose(wfile); if (kbm_print_level > 0)
printf("#Halting with %d equations.\n", rwsptr->num_eqns);
}
rws_clear(rwsptr);
fsa_clear(rwsptr->reduction_fsa);
tfree(rwsptr->reduction_fsa); if (rwsptr->lostinfo && kbm_print_level > 0) {
printf( "WARNING: The monoid defined by the presentation may have changed, since\n\
equations have been discarded.\n\ If you re-run, include the original equations.\n");
} if (kbm_print_level > 1)
printf(" #Exit status is %d\n", rwsptr->exit_status);
wfile = fopen(outfec, "w");
fprintf(wfile, "_ExitCode := %d;\n", rwsptr->exit_status);
fclose(wfile); exit(rwsptr->exit_status);
}
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.