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 22 kB image not shown  

Quelle  fsacheckmult.c   Sprache: C

 
/* file fsacheckmult.c  21. 11. 94.
 * 6/8/98 large scale reorganisation to omit globals, etc.
 * 30/7/98 - put in code for fsa_checkmult_int
 * 13/1/98 - changes for `gen' type of generator replacing char.
 * 16.10.96. Put in code to check which generators actually occur as labels
 * of success states in the generalised multiplier, and to ignore any that
 * do not, when checking correctness. (The test is certain to fail for any that
 * do not occur.)
 * This is unnecessary in the normal shortlex case, where they all occur
 * in any case.
 *
 * 22.9.95. Added code for coset automatic groups case.
 * The code is now fairly uniform for the two cases.
 *
 * This file contains the routine fsa_checkmult, which is used by the program
 * gpcheckmult.
 * (See also comments in file ../src/gpcheckmult.c.)
 * Its input automaton *multptr is the general multiplier of an automatic group.
 * It goes through the transition table generation process of fsa_exists
 * on this automaton (but does not write the table, since it will not be
 * needed). It does remember definitions of states (as in fsa_triples).
 * These are needed to reconstruct the failing word  w (see below).
 * Each state is a subset of the states of *multptr. Each such subset
 * should contain an accept state of each individual multiplier. If the
 * generation process completes, and this always holds, then the checking
 * process succeeds, and the procedure returns 0.
 * If some state is constructed which does not contain an accept state of
 * mult_g, for some generator g of the group, and w is a word with target
 * this state, then there can be no word x so that (w,x) is accepted by
 * mult_g, and so the checking process fails,
 * and the word w and generator x are remembered.
 * The number of such words found by the end of the process is returned.
 * The word w must be accepted by the word-acceptor (for otherwise (w,y)
 * would map to 0 for all words y, and w would never be considered),
 * so we do not need to use the word-acceptor explicitly.
 */


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

static int fsa_checkmult_short(fsa *multptr, reduction_equation *eqnptr,
                               int maxeqns, boolean cosets, int separator);
static int fsa_checkmult_int(fsa *multptr, reduction_equation *eqnptr,
                             int maxeqns, boolean cosets, int separator);

/* If the checking fails, the failing words will be returned in the lhs of
 * eqnptr[i], and the associated generator in the rhs, for i=0,1,...
 * If more than maxeqns such words are found, we abort.
 * The function returns the number of equations found.
 */

int fsa_checkmult(fsa *multptr, reduction_equation *eqnptr, int maxeqns,
                  boolean cosets, int separator)
{
  if (kbm_print_level >= 3)
    printf(" #Calling fsa_checkmult.\n");
  if (multptr->states->size < MAXUSHORT)
    return fsa_checkmult_short(multptr, eqnptr, maxeqns, cosets, separator);
  else
    return fsa_checkmult_int(multptr, eqnptr, maxeqns, cosets, separator);
}

/* If the checking fails, the failing word will be returned in the lhs of
 * *eqnptr, and the associated generator in the rhs.
 */

static int fsa_checkmult_short(fsa *multptr, reduction_equation *eqnptr,
                               int maxeqns, boolean cosets, int separator)
{
  int **table, dr, ne, ngens, ngens1, ns, nsnew, bstate, numeqns, e, es, ef,
      espad, efpad, cstate, cs, csi, i, j, g1, bg1, im, len;
  unsigned short *ht_ptr, *ht_chptr, *ht_ptrb, *ht_ptre, *cs_ptr, *cs_ptre,
      *ptr;
  gen **genlist, *genptr;
  boolean dense_ip, *occurs, *includes, got;
  setToLabelsType *state_label;
  short_hash_table ht;
  int maxv = 65536;
  struct vertexd {
    gen g;
    int state;
  } * definition, *newdef;
  /* This is used to store the defining transition for the states of the new
   * fsa. If definition[i] = v, then state i is defined by the transition from
   * state v.state, with generator v.g.
   * State 1 does not have a definition.
   */


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

  if (multptr->alphabet->type != PRODUCT || multptr->alphabet->arity != 2) {
    fprintf(stderr, "Error in fsa_checkmult: fsa must be 2-variable.\n");
    return -1;
  }
  if (multptr->states->type != LABELED) {
    fprintf(stderr,
            "Error in fsa_checkmult: states of fsa must be of labeled type.\n");
    return -1;
  }

  /* We are not actually going to construct a new fsa - we just go through the
   * motions of constructing the hash-table that represents its states.
   */

  ne = multptr->alphabet->size;
  ngens = multptr->alphabet->base->size;
  ngens1 = ngens + 1;
  state_label = multptr->states->setToLabels;
  ns = multptr->states->size;

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

  tmalloc(occurs, boolean, ngens + 1);
  for (i = 0; i <= ngens; i++)
    occurs[i] = FALSE;
  for (i = 1; i <= ns; i++)
    if ((j = state_label[i])) {
      genlist = multptr->states->labels->wordslist[j];
      /* the list of words that is the label for state number *ptr */
      while ((genptr = *(genlist++)))
        occurs[genptr[0]] = TRUE;
    }

  dense_ip = multptr->table->table_type == DENSE;
  dr = multptr->table->denserows;
  table = multptr->table->table_data_ptr;

  short_hash_init(&ht, FALSE, 0, 0, 0);
  ht_ptr = ht.current_ptr;
  ht_ptr[0] = multptr->initial[1];
  im = short_hash_locate(&ht, 1);
  /* Each state in the new fsa will be represented as a subset of the set of
   * states * of *multptr. The initial state is one-element set containing
   * the initial state of *multptr.
   * The subsets will be stored as variable-length records in the hash-table,
   * always in increasing order.
   */

  if (im != 1) {
    fprintf(stderr, "Hash-initialisation problem in fsa_checkmult.\n");
    return -1;
  }

  /* Set up the array of structures to remember state-definitions. */
  tmalloc(definition, struct vertexd, maxv);
  nsnew = 1;

  tmalloc(includes, boolean, ngens + 2);
  /* this will be used for checking validity of new states -
   * includes[ngens+1] is not used, but may be referenced accidentally
   */

  cstate = 0;
  numeqns = 0;

  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);
    }
    cs_ptr = short_hash_rec(&ht, cstate);
    cs_ptre = short_hash_rec(&ht, cstate) + short_hash_rec_len(&ht, cstate) - 1;
    for (g1 = 1; g1 <= ngens; g1++) {
      /* Calculate action of generator g1 on state cstate  - to get the image,
       * we have to apply (g1,g2) to each element in the subset corresponding to
       * cstate, and this for each generator g2 of the base-alphabet (including
       * the padding symbol).
       */

      ht_ptrb = ht.current_ptr;
      ht_ptre = ht_ptrb - 1;
      ptr = cs_ptr - 1;
      es = (g1 - 1) * ngens1 + 1;
      ef = g1 * ngens1;
      /* As g2 ranges from 1 to ngens+1 in the pair (g1,g2), for fixed g1, the
       * corresponding edge number in the fsa ranges from es to ef.
       */


      while (++ptr <= cs_ptre) {
        cs = *ptr;
        for (e = es; e <= ef; e++) {
          csi = target(dense_ip, table, e, cs, dr);
          if (csi == 0)
            continue;
          if (ht_ptrb > ht_ptre || csi > *ht_ptre) {
            /* We have a new state for the image subset to be added to the end
             */

            *(++ht_ptre) = csi;
          }
          else {
            ht_chptr = ht_ptrb;
            while (*ht_chptr < csi)
              ht_chptr++;
            if (csi < *ht_chptr) {
              /* we have a new state for the image subset to be added in the
               * middle */

              ht_ptr = ++ht_ptre;
              while (ht_ptr > ht_chptr) {
                *ht_ptr = *(ht_ptr - 1);
                ht_ptr--;
              }
              *ht_ptr = csi;
            }
          }
        }
      }
      im = short_hash_locate(&ht, ht_ptre - ht_ptrb + 1);
      if (im == -1)
        return -1;
      if (im > nsnew) {
        /* We have a new state. We must check to see if it is valid - i.e.
         * contains an accept-state of each multiplier. But first we have to
         * close it under the action of ($,g) for generators g. (We can put
         * extra states found at the end - this will not disturb the
         *  hash-table.)
         */

        espad = ngens * ngens1 + 1;
        efpad = ngens1 * ngens1 - 1;
        ptr = ht_ptrb - 1;
        while (++ptr <= ht_ptre) {
          cs = *ptr;
          for (e = espad; e <= efpad; e++) {
            csi = target(dense_ip, table, e, cs, dr);
            if (csi == 0)
              continue;
            /* see if csi is new */
            ht_chptr = ht_ptrb - 1;
            got = FALSE;
            while (++ht_chptr < ht_ptre)
              if (csi == *ht_chptr) {
                got = TRUE;
                break;
              }
            if (!got)
              /* add csi to the end */
              *(++ht_ptre) = csi;
          }
        }
        /* State is now closed under ($,g) - so check validity */
        for (i = 0; i <= ngens; i++)
          includes[i] = FALSE;
        ptr = ht_ptrb - 1;
        while (++ptr <= ht_ptre)
          if ((j = state_label[*ptr])) {
            genlist = multptr->states->labels->wordslist[j];
            /* the list of words that is the label for state number *ptr */
            while ((genptr = *(genlist++)))
              includes[genptr[0]] = TRUE;
          }

        for (i = 0; i <= ngens; i++)
          if (occurs[i] && !includes[i]) {
            /* The state is invalid for generator number i.
             * We reconstruct the offending word w, using the state-definitions,
             * and then abort.
             */

            if (numeqns == 0 && kbm_print_level > 0)
              printf("#Multiplier incorrect with generator number %d.\n", i);
            /* First see how long the word is */
            len = 1;
            bg1 = g1;
            bstate = cstate;
            while (bstate != 1) {
              len++;
              bg1 = definition[bstate].g;
              bstate = definition[bstate].state;
            }
            /* Now allocate space for it - allow an extra place for multiplying
             * by a generator.
             * In the cosets case, also an extra place for the separator
             * that we insert at the beginning of the word.
             */

            if (cosets)
              len++;
            tmalloc(eqnptr[numeqns].lhs, gen, len + 2);
            eqnptr[numeqns].lhs[len] = 0;
            bg1 = g1;
            bstate = cstate;
            while (1) {
              eqnptr[numeqns].lhs[--len] = bg1;
              if (bstate == 1)
                break;
              bg1 = definition[bstate].g;
              bstate = definition[bstate].state;
            }
            if (cosets)
              eqnptr[numeqns].lhs[--len] = separator;
            /* Put the offending generator in the rhs of *eqnptr */
            if (i == 0) {
              tmalloc(eqnptr[numeqns].rhs, gen, 1);
              eqnptr[numeqns].rhs[0] = 0;
            }
            else {
              tmalloc(eqnptr[numeqns].rhs, gen, 2);
              eqnptr[numeqns].rhs[0] = i;
              eqnptr[numeqns].rhs[1] = 0;
            }
            numeqns++;
            if (kbm_print_level >= 3)
              printf(" #Found offending word number %d.\n", numeqns);

            if (numeqns >= maxeqns) {
              tfree(definition);
              tfree(occurs);
              tfree(includes);
              short_hash_clear(&ht);
              if (kbm_print_level >= 2)
                printf(" #Found %d new equations. Aborting.\n", maxeqns);
              return numeqns;
            }
          }
        /* We have now checked that the new state is valid  -
         * so remember its definition
         */

        nsnew++;
        if (nsnew == maxv) { /* need room for more definitions */
          if (kbm_print_level >= 3)
            printf(" #Allocating more space for vertex definitions.\n");
          tmalloc(newdef, struct vertexd, 2 * maxv);
          for (i = 1; i < maxv; i++)
            newdef[i] = definition[i];
          tfree(definition);
          definition = newdef;
          maxv *= 2;
        }
        definition[nsnew].g = g1;
        definition[nsnew].state = cstate;
      }
    }
  }

  /* If we get to the end of the loop safely, then we have completed the
   * multiplier correctness checking test.
   */

  tfree(definition);
  tfree(occurs);
  tfree(includes);
  short_hash_clear(&ht);

  return numeqns;
}

/* If the checking fails, the failing word will be returned in the lhs of
 * *eqnptr, and the associated generator in the rhs.
 */

static int fsa_checkmult_int(fsa *multptr, reduction_equation *eqnptr,
                             int maxeqns, boolean cosets, int separator)
{
  int **table, dr, ne, ngens, ngens1, ns, nsnew, bstate, numeqns, e, es, ef,
      espad, efpad, cstate, cs, csi, i, j, g1, bg1, im, len;
  int *ht_ptr, *ht_chptr, *ht_ptrb, *ht_ptre, *cs_ptr, *cs_ptre, *ptr;
  gen **genlist, *genptr;
  boolean dense_ip, *occurs, *includes, got;
  setToLabelsType *state_label;
  hash_table ht;
  int maxv = 65536;
  struct vertexd {
    gen g;
    int state;
  } * definition, *newdef;
  /* This is used to store the defining transition for the states of the new
   * fsa. If definition[i] = v, then state i is defined by the transition from
   * state v.state, with generator v.g.
   * State 1 does not have a definition.
   */


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

  if (multptr->alphabet->type != PRODUCT || multptr->alphabet->arity != 2) {
    fprintf(stderr, "Error in fsa_checkmult: fsa must be 2-variable.\n");
    return -1;
  }
  if (multptr->states->type != LABELED) {
    fprintf(stderr,
            "Error in fsa_checkmult: states of fsa must be of labeled type.\n");
    return -1;
  }

  /* We are not actually going to construct a new fsa - we just go through the
   * motions of constructing the hash-table that represents its states.
   */

  ne = multptr->alphabet->size;
  ngens = multptr->alphabet->base->size;
  ngens1 = ngens + 1;
  state_label = multptr->states->setToLabels;
  ns = multptr->states->size;

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

  tmalloc(occurs, boolean, ngens + 1);
  for (i = 0; i <= ngens; i++)
    occurs[i] = FALSE;
  for (i = 1; i <= ns; i++)
    if ((j = state_label[i])) {
      genlist = multptr->states->labels->wordslist[j];
      /* the list of words that is the label for state number *ptr */
      while ((genptr = *(genlist++)))
        occurs[genptr[0]] = TRUE;
    }

  dense_ip = multptr->table->table_type == DENSE;
  dr = multptr->table->denserows;
  table = multptr->table->table_data_ptr;

  hash_init(&ht, FALSE, 0, 0, 0);
  ht_ptr = ht.current_ptr;
  ht_ptr[0] = multptr->initial[1];
  im = hash_locate(&ht, 1);
  /* Each state in the new fsa will be represented as a subset of the set of
   * states * of *multptr. The initial state is one-element set containing
   * the initial state of *multptr.
   * The subsets will be stored as variable-length records in the hash-table,
   * always in increasing order.
   */

  if (im != 1) {
    fprintf(stderr, "Hash-initialisation problem in fsa_checkmult.\n");
    return -1;
  }

  /* Set up the array of structures to remember state-definitions. */
  tmalloc(definition, struct vertexd, maxv);
  nsnew = 1;

  tmalloc(includes, boolean, ngens + 2);
  /* this will be used for checking validity of new states -
   * includes[ngens+1] is not used, but may be referenced accidentally
   */

  cstate = 0;
  numeqns = 0;

  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);
    }
    cs_ptr = hash_rec(&ht, cstate);
    cs_ptre = hash_rec(&ht, cstate) + hash_rec_len(&ht, cstate) - 1;
    for (g1 = 1; g1 <= ngens; g1++) {
      /* Calculate action of generator g1 on state cstate  - to get the image,
       * we have to apply (g1,g2) to each element in the subset corresponding to
       * cstate, and this for each generator g2 of the base-alphabet (including
       * the padding symbol).
       */

      ht_ptrb = ht.current_ptr;
      ht_ptre = ht_ptrb - 1;
      ptr = cs_ptr - 1;
      es = (g1 - 1) * ngens1 + 1;
      ef = g1 * ngens1;
      /* As g2 ranges from 1 to ngens+1 in the pair (g1,g2), for fixed g1, the
       * corresponding edge number in the fsa ranges from es to ef.
       */


      while (++ptr <= cs_ptre) {
        cs = *ptr;
        for (e = es; e <= ef; e++) {
          csi = target(dense_ip, table, e, cs, dr);
          if (csi == 0)
            continue;
          if (ht_ptrb > ht_ptre || csi > *ht_ptre) {
            /* We have a new state for the image subset to be added to the end
             */

            *(++ht_ptre) = csi;
          }
          else {
            ht_chptr = ht_ptrb;
            while (*ht_chptr < csi)
              ht_chptr++;
            if (csi < *ht_chptr) {
              /* we have a new state for the image subset to be added in the
               * middle */

              ht_ptr = ++ht_ptre;
              while (ht_ptr > ht_chptr) {
                *ht_ptr = *(ht_ptr - 1);
                ht_ptr--;
              }
              *ht_ptr = csi;
            }
          }
        }
      }
      im = hash_locate(&ht, ht_ptre - ht_ptrb + 1);
      if (im == -1)
        return -1;
      if (im > nsnew) {
        /* We have a new state. We must check to see if it is valid - i.e.
         * contains an accept-state of each multiplier. But first we have to
         * close it under the action of ($,g) for generators g. (We can put
         * extra states found at the end - this will not disturb the
         *  hash-table.)
         */

        espad = ngens * ngens1 + 1;
        efpad = ngens1 * ngens1 - 1;
        ptr = ht_ptrb - 1;
        while (++ptr <= ht_ptre) {
          cs = *ptr;
          for (e = espad; e <= efpad; e++) {
            csi = target(dense_ip, table, e, cs, dr);
            if (csi == 0)
              continue;
            /* see if csi is new */
            ht_chptr = ht_ptrb - 1;
            got = FALSE;
            while (++ht_chptr < ht_ptre)
              if (csi == *ht_chptr) {
                got = TRUE;
                break;
              }
            if (!got)
              /* add csi to the end */
              *(++ht_ptre) = csi;
          }
        }
        /* State is now closed under ($,g) - so check validity */
        for (i = 0; i <= ngens; i++)
          includes[i] = FALSE;
        ptr = ht_ptrb - 1;
        while (++ptr <= ht_ptre)
          if ((j = state_label[*ptr])) {
            genlist = multptr->states->labels->wordslist[j];
            /* the list of words that is the label for state number *ptr */
            while ((genptr = *(genlist++)))
              includes[genptr[0]] = TRUE;
          }

        for (i = 0; i <= ngens; i++)
          if (occurs[i] && !includes[i]) {
            /* The state is invalid for generator number i.
             * We reconstruct the offending word w, using the state-definitions,
             * and then abort.
             */

            if (numeqns == 0 && kbm_print_level > 0)
              printf("#Multiplier incorrect with generator number %d.\n", i);
            /* First see how long the word is */
            len = 1;
            bg1 = g1;
            bstate = cstate;
            while (bstate != 1) {
              len++;
              bg1 = definition[bstate].g;
              bstate = definition[bstate].state;
            }
            /* Now allocate space for it - allow an extra place for multiplying
             * by a generator.
             * In the cosets case, also an extra place for the separator
             * that we insert at the beginning of the word.
             */

            if (cosets)
              len++;
            tmalloc(eqnptr[numeqns].lhs, gen, len + 2);
            eqnptr[numeqns].lhs[len] = 0;
            bg1 = g1;
            bstate = cstate;
            while (1) {
              eqnptr[numeqns].lhs[--len] = bg1;
              if (bstate == 1)
                break;
              bg1 = definition[bstate].g;
              bstate = definition[bstate].state;
            }
            if (cosets)
              eqnptr[numeqns].lhs[--len] = separator;
            /* Put the offending generator in the rhs of *eqnptr */
            if (i == 0) {
              tmalloc(eqnptr[numeqns].rhs, gen, 1);
              eqnptr[numeqns].rhs[0] = 0;
            }
            else {
              tmalloc(eqnptr[numeqns].rhs, gen, 2);
              eqnptr[numeqns].rhs[0] = i;
              eqnptr[numeqns].rhs[1] = 0;
            }
            numeqns++;
            if (kbm_print_level >= 3)
              printf(" #Found offending word number %d.\n", numeqns);

            if (numeqns >= maxeqns) {
              tfree(definition);
              tfree(occurs);
              tfree(includes);
              hash_clear(&ht);
              if (kbm_print_level >= 2)
                printf(" #Found %d new equations. Aborting.\n", maxeqns);
              return numeqns;
            }
          }
        /* We have now checked that the new state is valid  -
         * so remember its definition
         */

        nsnew++;
        if (nsnew == maxv) { /* need room for more definitions */
          if (kbm_print_level >= 3)
            printf(" #Allocating more space for vertex definitions.\n");
          tmalloc(newdef, struct vertexd, 2 * maxv);
          for (i = 1; i < maxv; i++)
            newdef[i] = definition[i];
          tfree(definition);
          definition = newdef;
          maxv *= 2;
        }
        definition[nsnew].g = g1;
        definition[nsnew].state = cstate;
      }
    }
  }

  /* If we get to the end of the loop safely, then we have completed the
   * multiplier correctness checking test.
   */

  tfree(definition);
  tfree(occurs);
  tfree(includes);
  hash_clear(&ht);

  return numeqns;
}

Messung V0.5
C=93 H=58 G=77

¤ Dauer der Verarbeitung: 0.8 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.