Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/GAP/pkg/kbmag/standalone/lib/   (Algebra von RWTH Aachen Version 4.15.1©)  Datei vom 3.0.2023 mit Größe 18 kB image not shown  

Quelle  fsaminkb.c   Sprache: C

 
/* file fsaminkb.c  16. 12. 94.
 * 13/1/98 changes for introduction of `gen' type in place of char for
 * generators.
 * This file contains the routines necessary to calculate a 2-variable fsa
 * accepting precisely the minimal KB-rules of a short-lex automatic group.
 *
 * The first routine fsa_minred uses the word-acceptor to construct the
 * minimal reducible words - i.e. those for which all subwords are
 * accepted by the word-acceptor - clearly it is enough for the two words
 * obtained by omitting the first and last letters to be acceptable, so
 * it is essentially an application of fsa_and.
 *
 * The second routine fsa_minkb is a 2-variable machine accepting precisely the
 * minimal KB-reduction equations - i.e it accepts a pair (w1,w2) if w1 and w2
 * are equal in G, w1 is accepted by the fsa constructed by fsa_minred, and
 * w2 is accepted by the word-acceptor. Its construction is as in fsa_triples.
 *
 * The third routine, fsa_diff calculates the word-difference machine
 * associated with an fsa that accepts a collection of equations.
 * So, for example, it can be used with input the KB-reduction machine,
 * mentioned in the last paragraph, to calculate the correct diff1 machine,
 * or with the generalised multiplier to construct the correct diff2 machine.
 */


#include <stdio.h>
#include "defs.h"
#include "fsa.h"
#include "rws.h"
#include "hash.h"
#include "externals.h"

/* Functions defined in this file: */

extern int (*reduce_word)(gen *w, reduction_struct *rs_rws);
static gen testword[4096]; /* Used for reducing words */

fsa *fsa_minred(fsa *waptr, storage_type op_table_type, boolean destroy,
                char *tempfilename)
{
  int **table, ne, nsi, nsi1, ns, dr, *fsarow, nt, cstate, csa, csb, im, i, g,
      len = 0, ct, *ht_ptr;
  boolean dense_ip, dense_op;
  fsa *minred;
  hash_table ht;
  FILE *tempfile;

  if (kbm_print_level >= 3)
    printf(" #Calling fsa_minred.\n");
  if (!waptr->flags[DFA]) {
    fprintf(stderr, "Error: fsa_minred only applies to DFA's.\n");
    return 0;
  }

  tmalloc(minred, fsa, 1);
  fsa_init(minred);
  srec_copy(minred->alphabet, waptr->alphabet);
  minred->flags[DFA] = TRUE;
  minred->flags[ACCESSIBLE] = TRUE;
  minred->flags[BFS] = TRUE;

  ne = waptr->alphabet->size;
  nsi = waptr->states->size;
  nsi1 = nsi + 1;

  table = waptr->table->table_data_ptr;

  dense_ip = waptr->table->table_type == DENSE;
  dr = waptr->table->denserows;
  dense_op = op_table_type == DENSE;

  minred->states->type = SIMPLE;
  minred->num_initial = 1;
  tmalloc(minred->initial, int, 2);
  minred->initial[1] = 1;
  minred->table->table_type = op_table_type;
  minred->table->denserows = 0;
  minred->table->printing_format = op_table_type;

  hash_init(&ht, TRUE, 2, 0, 0);
  ht_ptr = ht.current_ptr;
  ht_ptr[0] = waptr->initial[1];
  ht_ptr[1] = waptr->initial[1];
  im = hash_locate(&ht, 2);
  if (im != 1) {
    fprintf(stderr, "Hash-initialisation problem in fsa_minred.\n");
    return 0;
  }
  if ((tempfile = fopen(tempfilename, "w")) == 0) {
    fprintf(stderr, "Error: cannot open file %s\n", tempfilename);
    return 0;
  }
  if (dense_op)
    tmalloc(fsarow, int, ne) else tmalloc(fsarow, int, 2 * ne + 1)

        cstate = 0;
  if (dense_op)
    len = ne; /* The length of the fsarow output. */
  nt = 0;     /* Number of transitions in minred */

  /* A state of *minred will be essentially a pair of states of *waptr,
   * with the transitions coming from those of *waptr.
   * The differences are that the left hand side will accept words  w
   * which are not accepted by *waptr but whose maximal prefix is,
   * whereas the right hand side will accept words  w which are not accepted
   * by *waptr but whose maximal suffix is.
   * Thus, on the lhs, transitions to 0 in *waptr will go to a new accept-
   * state nsi1 instead (with no transitions from nsi1) whereas on the rhs
   * the first transition will be back to the initial state.
   * The initial state itself is non-accept.
   */

  while (++cstate <= ht.num_recs) {
    if (kbm_print_level >= 3) {
      if ((cstate <= 1000 && cstate % 100 == 0) ||
          (cstate <= 10000 && cstate % 1000 == 0) ||
          (cstate <= 100000 && cstate % 5000 == 0) || cstate % 50000 == 0)
        printf(" #cstate = %d; number of states = %d.\n", cstate,
               ht.num_recs);
    }
    ht_ptr = hash_rec(&ht, cstate);
    csa = ht_ptr[0];
    csb = ht_ptr[1];
    if (!dense_op)
      len = 0;
    for (g = 1; g <= ne; g++) {
      /* Calculate action of generator g on state cstate */
      ht_ptr = ht.current_ptr;
      if (csa == 0 || csa == nsi1)
        ht_ptr[0] = 0;
      else {
        ht_ptr[0] = target(dense_ip, table, g, csa, dr);
        if (ht_ptr[0] == 0)
          ht_ptr[0] = nsi1;
      }
      if (cstate == 1)
        ht_ptr[1] = csb;
      else
        ht_ptr[1] = csb ? target(dense_ip, table, g, csb, dr) : 0;
      if (ht_ptr[0] == 0 || ht_ptr[1] == 0)
        im = 0;
      else
        im = hash_locate(&ht, 2);
      if (dense_op)
        fsarow[g - 1] = im;
      else if (im > 0) {
        fsarow[++len] = g;
        fsarow[++len] = im;
      }
      if (im > 0)
        nt++;
    }
    if (!dense_op)
      fsarow[0] = len++;
    fwrite((void *)fsarow, sizeof(int), (size_t)len, tempfile);
  }
  fclose(tempfile);

  ns = minred->states->size = ht.num_recs;
  minred->table->numTransitions = nt;
  /* Locate the accept states: first count them and then record them. */
  ct = 0;
  for (i = 1; i <= ns; i++) {
    ht_ptr = hash_rec(&ht, i);
    if (ht_ptr[0] == nsi1)
      ct++;
  }
  minred->num_accepting = ct;
  if (ct == 1 || ct != ns) {
    tmalloc(minred->accepting, int, ct + 1);
    ct = 0;
    for (i = 1; i <= ns; i++) {
      ht_ptr = hash_rec(&ht, i);
      if (ht_ptr[0] == nsi1)
        minred->accepting[++ct] = i;
    }
  }
  hash_clear(&ht);
  tfree(fsarow);
  tfree(waptr->is_accepting);

  if (destroy)
    fsa_clear(waptr);

  /* Now read the transition table back in */
  tempfile = fopen(tempfilename, "r");
  compressed_transitions_read(minred, tempfile);
  fclose(tempfile);

  unlink(tempfilename);

  return minred;
}

/* *waptr is assumed to be the word-acceptor of an automatic group.
 * and *minredptr the fsa which accepts minimal reducible words
 * (computed using fsa_minred above).
 * In particular, all states of *waptr should be accepting.
 * *diffptr is assumed to be a word-difference machine of the same automatic
 *  group. Both are assumed to be stored in dense-format.
 * This routine constructs the fsa of which the states are triples (s1,s2,d),
 * with s1 and s2 states of *minredptr and *waptr and d a state of *diffptr.
 * (More precisely, if *waptr has n states, then s2 may also be equal
 * to n+1, meaning that the end of string symbol has been read on  rhs.
 * Since lhs is never shorter than rhs in an accpeted pair, the end of
 * string symbol on the lhs always leads to failure.)
 * The alphabet is 2-variable with base the alphabet of *waptr
 * (i.e. the same alphabet as *diffptr).
 * The alphabet member (g1,g2) maps (s1,s2,d) to (s1^g1,s2^g2,d^(g1,g2))
 * if all three components are nonzero, and to zero otherwise.
 * The transition-table of the resulting fsa is output in the usual way to
 * file tempfilename with table-type specified by op_table_type, before
 * minimisation.
 * A state is accept is s1, s2 and d all are (but s2 always is).
 * Short hash-tables will be used, so this routine won't work if *waptr
 * or *diffptr has more than 65535 states.
 *
 */

fsa *fsa_minkb(fsa *minredptr, fsa *waptr, fsa *diffptr,
               storage_type op_table_type, boolean destroy, char *tempfilename)
{
  int **minredtable, **watable, ***difftable, identity, ngens, ngens1, nswa1,
      ne, ns, *fsarow, nt, cstate, cswa1, cswa2, csdiff, im, i, e, len = 0, ct;
  unsigned short *ht_ptr;
  boolean dense_op;
  fsa *minkbptr;
  short_hash_table ht;
  FILE *tempfile;
  gen g1, g2;

  if (kbm_print_level >= 3)
    printf(" #Calling fsa_minkbptr.\n");

  if (!minredptr->flags[DFA] || !waptr->flags[DFA] || !diffptr->flags[DFA]) {
    fprintf(stderr, "Error: fsa_minkbptr only applies to DFA's.\n");
    return 0;
  }
  if (minredptr->alphabet->type != IDENTIFIERS ||
      waptr->alphabet->type != IDENTIFIERS) {
    fprintf(stderr, "Error in fsa_minkbptr: an fsa has wrong type.\n");
    return 0;
  }
  if (waptr->num_accepting != waptr->states->size) {
    fprintf(stderr,
            "Error in fsa_minkbptr: second fsa should be a word-acceptor.\n");
    return 0;
  }
  if (diffptr->alphabet->type != PRODUCT || diffptr->alphabet->arity != 2) {
    fprintf(stderr, "Error in fsa_minkbptr: third fsa must be 2-variable.\n");
    return 0;
  }
  if (diffptr->states->type != WORDS) {
    fprintf(stderr,
            "Error in fsa_minkbptr: third fsa must be word-difference type.\n");
    return 0;
  }
  if (!srec_equal(diffptr->alphabet->base, waptr->alphabet)) {
    fprintf(stderr, "Error in fsa_minkbptr: fsa's alphabet's don't match.\n");
    return 0;
  }
  if (minredptr->states->size >= MAXUSHORT ||
      waptr->states->size >= MAXUSHORT || diffptr->states->size >= MAXUSHORT) {
    fprintf(stderr,
            "Error in fsa_minkbptr: one of the fsa's has too many states.\n");
    return 0;
  }

  if (fsa_table_dptr_init(diffptr) == -1)
    return 0;

  tmalloc(minkbptr, fsa, 1);
  fsa_init(minkbptr);
  srec_copy(minkbptr->alphabet, diffptr->alphabet);
  minkbptr->flags[DFA] = TRUE;
  minkbptr->flags[ACCESSIBLE] = TRUE;
  minkbptr->flags[BFS] = TRUE;

  ngens = waptr->alphabet->size;
  ngens1 = ngens + 1;
  ne = diffptr->alphabet->size;
  nswa1 = waptr->states->size + 1;

  if (ne != ngens1 * ngens1 - 1) {
    fprintf(
        stderr,
        "Error: in a 2-variable fsa, alphabet size should = ngens^2 - 1.\n");
    return 0;
  }

  minredtable = minredptr->table->table_data_ptr;
  watable = waptr->table->table_data_ptr;
  difftable = diffptr->table->table_data_dptr;

  dense_op = op_table_type == DENSE;

  minkbptr->states->type = SIMPLE;

  minkbptr->num_initial = 1;
  tmalloc(minkbptr->initial, int, 2);
  minkbptr->initial[1] = 1;
  minkbptr->table->table_type = op_table_type;
  minkbptr->table->denserows = 0;
  minkbptr->table->printing_format = op_table_type;

  short_hash_init(&ht, TRUE, 3, 0, 0);
  ht_ptr = ht.current_ptr;
  ht_ptr[0] = minredptr->initial[1];
  ht_ptr[1] = waptr->initial[1];
  ht_ptr[2] = identity = diffptr->initial[1];
  im = short_hash_locate(&ht, 3);
  if (im != 1) {
    fprintf(stderr, "Hash-initialisation problem in fsa_minkbptr.\n");
    return 0;
  }
  if ((tempfile = fopen(tempfilename, "w")) == 0) {
    fprintf(stderr, "Error: cannot open file %s\n", tempfilename);
    return 0;
  }
  if (dense_op)
    tmalloc(fsarow, int, ne) else tmalloc(fsarow, int, 2 * ne + 1)

        cstate = 0;
  if (dense_op)
    len = ne; /* The length of the fsarow output. */
  nt = 0;     /* Number of transitions in minkbptr */

  while (++cstate <= ht.num_recs) {
    if (kbm_print_level >= 3) {
      if ((cstate <= 1000 && cstate % 100 == 0) ||
          (cstate <= 10000 && cstate % 1000 == 0) ||
          (cstate <= 100000 && cstate % 5000 == 0) || cstate % 50000 == 0)
        printf(" #cstate = %d; number of states = %d.\n", cstate,
               ht.num_recs);
    }
    ht_ptr = short_hash_rec(&ht, cstate);
    cswa1 = ht_ptr[0];
    cswa2 = ht_ptr[1];
    csdiff = ht_ptr[2];
    if (dense_op)
      for (i = 0; i < ne; i++)
        fsarow[i] = 0;
    else
      len = 0;
    e = 0; /* e is the number of the edge corresponding to the pair (g1,g2) */
    for (g1 = 1; g1 <= ngens; g1++)
      for (g2 = 1; g2 <= ngens1; g2++) {
        e++;
        /* Calculate action of generator-pair (g1,g2) on state cstate - since
         * the padding symbol cannot occur on the lhs, g1 only goes up to ngens.
         */

        ht_ptr = ht.current_ptr;
        ht_ptr[2] = dense_dtarget(difftable, g1, g2, csdiff);
        if (ht_ptr[2] == 0)
          im = 0;
        else {
          ht_ptr[0] = dense_target(minredtable, g1, cswa1);
          if (ht_ptr[0] == 0)
            im = 0;
          else {
            ht_ptr[1] =
                g2 == ngens1
                    ? nswa1
                    : cswa2 == nswa1 ? 0 : dense_target(watable, g2, cswa2);
            if (ht_ptr[1] == 0)
              im = 0;
            else
              im = short_hash_locate(&ht, 3);
          }
        }

        if (dense_op)
          fsarow[e - 1] = im;
        else if (im > 0) {
          fsarow[++len] = e;
          fsarow[++len] = im;
        }
        if (im > 0)
          nt++;
      } /* for (g1=1;g1<=ngens1; ... */
    if (!dense_op)
      fsarow[0] = len++;
    fwrite((void *)fsarow, sizeof(int), (size_t)len, tempfile);
  } /*while (++cstate <= ht.num_recs) */
  fclose(tempfile);

  ns = minkbptr->states->size = ht.num_recs;
  minkbptr->table->numTransitions = nt;

  if (kbm_print_level >= 3)
    printf(" #Calculated transitions - %d states, %d transitions.\n", ns,
           nt);

  /* Now locate the accept states */

  fsa_set_is_accepting(minredptr);
  ct = 0;
  for (i = 1; i <= ns; i++) {
    ht_ptr = short_hash_rec(&ht, i);
    if (minredptr->is_accepting[ht_ptr[0]] && ht_ptr[2] == identity)
      ct++;
  }
  minkbptr->num_accepting = ct;
  if (ct == 1 || ct != ns) {
    tmalloc(minkbptr->accepting, int, ct + 1);
    ct = 0;
    for (i = 1; i <= ns; i++) {
      ht_ptr = short_hash_rec(&ht, i);
      if (minredptr->is_accepting[ht_ptr[0]] && ht_ptr[2] == identity)
        minkbptr->accepting[++ct] = i;
    }
  }

  short_hash_clear(&ht);
  tfree(minredptr->is_accepting);
  tfree(fsarow);
  if (destroy) {
    fsa_clear(minredptr);
    fsa_clear(waptr);
    fsa_clear(diffptr);
  }
  /* Now read the transition table back in */
  tempfile = fopen(tempfilename, "r");
  compressed_transitions_read(minkbptr, tempfile);
  fclose(tempfile);

  unlink(tempfilename);

  return minkbptr;
}

/* *fsaptr should be a two-variable automaton that accepts pairs of equations
 * It must be stored in dense format.
 * The corresponding word-difference machine is computed and returned.
 * For example, if fsaptr is minkb as returned by fsa_minkb (above),
 * then the correct diff1 machine for the shortlex automatic group is computed.
 */

fsa *fsa_diff(fsa *fsaptr, reduction_struct *rs_wd, storage_type op_table_type)
{
  int i, l, n, ngens, ngens1, ne, ns, g1, g2, fsaptr_state, diff_state,
      *state_diff, ***fsaptr_table, ***wd_table, **table, fsaptr_im, diff_im,
      *inv;
  fsa *diffptr;
  gen *stw;

  if (kbm_print_level >= 3)
    printf(" #Calling fsa_diff.\n");
  if (!fsaptr->flags[DFA]) {
    fprintf(stderr, "Error: fsa_diff only applies to DFA's.\n");
    return 0;
  }

  if (fsaptr->alphabet->type != PRODUCT || fsaptr->alphabet->arity != 2) {
    fprintf(stderr, "Error in fsa_diff: fsa must be 2-variable.\n");
    return 0;
  }

  ne = fsaptr->alphabet->size;
  ngens = fsaptr->alphabet->base->size;
  ngens1 = ngens + 1;
  ns = fsaptr->states->size;
  if (fsa_table_dptr_init(fsaptr) == -1)
    return 0;
  fsaptr_table = fsaptr->table->table_data_dptr;

  if (ne != ngens1 * ngens1 - 1) {
    fprintf(
        stderr,
        "Error: in a 2-variable fsa, alphabet size should = ngens^2 - 1.\n");
    return 0;
  }

  tmalloc(diffptr, fsa, 1);
  fsa_init(diffptr);
  srec_copy(diffptr->alphabet, fsaptr->alphabet);

  /* Maximum possible number of states of diff is of course ns */
  diffptr->states->type = WORDS;
  tmalloc(diffptr->states->words, gen *, ns + 1);
  diffptr->states->alphabet_size = fsaptr->alphabet->base->size;
  for (i = 1; i <= fsaptr->alphabet->base->size; i++) {
    tmalloc(diffptr->states->alphabet[i], char,
            stringlen(fsaptr->alphabet->base->names[i]) + 1);
    strcpy(diffptr->states->alphabet[i], fsaptr->alphabet->base->names[i]);
  }
  diffptr->states->size = 1;
  /* Set up first state, which is the empty word. */
  tmalloc(diffptr->states->words[1], gen, 1);
  diffptr->states->words[1][0] = 0;

  diffptr->num_initial = 1;
  tmalloc(diffptr->initial, int, 2);
  diffptr->initial[1] = 1;
  diffptr->num_accepting = 1;
  tmalloc(diffptr->accepting, int, 2);
  diffptr->accepting[1] = 1; /* Only the initial state is accepting */

  diffptr->flags[DFA] = TRUE;
  diffptr->flags[TRIM] = TRUE;

  fsa_table_init(diffptr->table, ns, diffptr->alphabet->size);
  diffptr->table->printing_format = op_table_type;
  if (fsa_table_dptr_init(diffptr) == -1)
    return 0;
  wd_table = diffptr->table->table_data_dptr;
  table = diffptr->table->table_data_ptr;
  for (i = 1; i <= ne; i++)
    table[i][1] = 0;

  reduce_word = diff_reduce;
  if (calculate_inverses(&inv, ngens, rs_wd) == -1)
    return 0;

  /* Now build the transition-table of diffptr, using that of fsaptr.
   * Each state of fsaptr maps onto one of *diffptr, with the mapping
   * stored in the list state_diff.
   */

  tmalloc(state_diff, int, ns + 1);
  for (i = 1; i <= ns; i++)
    state_diff[i] = 0;
  state_diff[1] = 1;
  for (fsaptr_state = 1; fsaptr_state <= ns; fsaptr_state++) {
    diff_state = state_diff[fsaptr_state];
    for (g1 = 1; g1 <= ngens1; g1++)
      for (g2 = 1; g2 <= ngens1; g2++) {
        if (g1 == ngens1 && g2 == ngens1)
          continue;
        fsaptr_im = dense_dtarget(fsaptr_table, g1, g2, fsaptr_state);
        if (fsaptr_im == 0)
          continue;
        diff_im = state_diff[fsaptr_im];
        if (diff_im == 0) {
          /* We have to work out what word-difference the state maps onto */
          stw = diffptr->states->words[diff_state];
          l = genstrlen(stw);
          if (g1 == ngens1) {
            genstrcpy(testword, stw);
            testword[l] = g2;
            testword[l + 1] = 0;
          }
          else if (g2 == ngens1) {
            testword[0] = inv[g1];
            genstrcpy(testword + 1, stw);
            testword[l + 1] = 0;
          }
          else {
            testword[0] = inv[g1];
            genstrcpy(testword + 1, stw);
            testword[l + 1] = g2;
            testword[l + 2] = 0;
          }
          if ((*reduce_word)(testword, rs_wd) == -1)
            return 0;
          n = diff_no(diffptr, testword);
          if (n == 0) {
            n = ++diffptr->states->size;
            tmalloc(diffptr->states->words[n], gen, genstrlen(testword) + 1);
            genstrcpy(diffptr->states->words[n], testword);
            for (i = 1; i <= ne; i++)
              table[i][n] = 0;
          }
          state_diff[fsaptr_im] = diff_im = n;
        }
        set_dense_dtarget(wd_table, g1, g2, diff_state, diff_im);
      }
  }

  tfree(inv);
  tfree(state_diff);
  return diffptr;
}

Messung V0.5
C=95 H=80 G=87

¤ Dauer der Verarbeitung: 0.10 Sekunden  ¤

*© Formatika GbR, Deutschland






Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

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 und die Messung sind noch experimentell.