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

Quelle  fsawacos.c   Sprache: C

 
/* file fsawacos.c 24/7/95 */

/* File fsawa.c adjusted for cosets.
 * The difference is that there can be more than one start state in the
 * word-difference machine, which are used at the beginning of the word.
 *
 * This file essentially consists of the function fsa_wa_cos
 * (although this function calls fsa_wa_cos_int or (more usually)
 * fsa_wa_cos_short, the latter using the short hash table functions).
 * For general methodology, see comment at top of file fsalogic.c.
 *
 * This function is intended to be called only in the construction of the
 * coset word-acceptor of a shortlex coset automatic group.
 * *fsaptr  is the word-difference machine.
 * The returned fsa accepts a word w_1 iff  w_1 contains no subword  x_1 such
 * that (x_1,x_2) is accepted by *fsaptr using initial state identity
 * only or using all initial states where x_1 is a prefix of w_1,
 * and w_2 < w_1 in the shortlex ordering,
 * for some word w_2 (with the usual padding conventions).
 * It is based on the function fsa_exists.
 *
 * The states of the fsa  *wa that we are calculating consist of subsets of
 * the "and" of *fsaptr with the "lhs greater-than rhs" automaton. Since the
 * latter has  4 states, the elements of these subsets are technically
 * pairs of the form (s,i), where s is a state of *fsaptr, and 1<=i<=4.
 * Here i=1 means lhs=rhs, i=2 means lhs>rhs with equal lengths,
 * i=3 means rhs>lhs with equal lengths, and i=4 means lhs is longer than rhs.
 * At most one of (s,1), (s,2), (s,3) needs to be stored, since
 * (s,2) is stronger than (s,1) which is stronger than (s,3).
 * In the records in the hash-table, in which the subsets are stored,
 * (s,1) is stores as s, (s,2) as ndiff+s and (s,3) as 2*ndiff+s
 * (where ndiff = no. of states of *fsaptr), and (s,4) as 3*ndiff + s.
 *
 * This function assumes that *fsaptr is a word-difference machine, with a
 * unique accept state, which should be equal to the first initial state, and
 * map onto the identity element of the group.
 * There will usually be more than one initial state.
 */


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

#define HTMARGIN 4096
/* if less space than this in hash-table, re-allocate */

/* Functions defined in this file: */
static fsa *fsa_wa_cos_short(fsa *fsaptr, storage_type op_table_type,
                             boolean destroy, char *tempfilename);
static fsa *fsa_wa_cos_int(fsa *fsaptr, storage_type op_table_type,
                           boolean destroy, char *tempfilename);

fsa *fsa_wa_cos(fsa *fsaptr, storage_type op_table_type, boolean destroy,
                char *tempfilename)
{
  if (kbm_print_level >= 3)
    printf(" #Calling fsa_wa.\n");
  if (4 * fsaptr->states->size < MAXUSHORT)
    return fsa_wa_cos_short(fsaptr, op_table_type, destroy, tempfilename);
  else
    return fsa_wa_cos_int(fsaptr, op_table_type, destroy, tempfilename);
}

static fsa *fsa_wa_cos_short(fsa *fsaptr, storage_type op_table_type,
                             boolean destroy, char *tempfilename)
{
  int ***dtable, ne, ngens, ndiff, ns, *fsarow, nt, cstate, cs, csdiff, csi, im,
      i, k, g1, g2, len = 0, identity;
  unsigned short *ht_ptr, *ht_ptrb, *ht_ptre, *cs_ptr, *cs_ptre, *ptr;
  boolean dense_op, no_trans, good;
  char *cf;
  short_hash_table ht;
  fsa *wa;
  FILE *tempfile;

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

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

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

  ne = fsaptr->alphabet->size;
  ngens = wa->alphabet->size;
  ndiff = fsaptr->states->size;

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

  identity = fsaptr->accepting[1]; /* assumed to be unique */
  if (fsaptr->num_accepting != 1 || (identity != fsaptr->initial[1])) {
    fprintf(stderr,
            "Error: Input to fsa_wa_cos not a word-difference machine.\n");
    return 0;
  }

  if (fsaptr->table->table_type != DENSE) {
    fprintf(stderr, "Error: function fsa_wa_cos can only be called with a "
                    "densely-stored fsa.\n");
    return 0;
  }
  dense_op = op_table_type == DENSE;
  if (fsa_table_dptr_init(fsaptr) == -1)
    return 0;
  dtable = fsaptr->table->table_data_dptr;

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

  short_hash_init(&ht, FALSE, 0, 0, 0);
  ht_ptr = ht.current_ptr;
  for (i = 0; i < fsaptr->num_initial; i++)
    ht_ptr[i] = fsaptr->initial[i + 1];
  im = short_hash_locate(&ht, fsaptr->num_initial);
  /* See discussion at top of file for storing of states of *wa.
   * Only the initial state which consists of the singleton {identity} contains
   * identity.
   */

  if (im != 1) {
    fprintf(stderr, "Hash-initialisation problem in fsa_wa.\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, ngens) else tmalloc(fsarow, int, 2 * ngens + 1)

        cstate = 0;
  if (dense_op)
    len = ngens; /* The length of the fsarow output. */
  nt = 0;        /* Number of transitions in exists */
  tmalloc(cf, char, ndiff + 1);

  /* As we build up the subset that represents a state of *wa, we use the
   * characteristic function cf, to record what we have found already.
   * For n a state number  of *fsaptr,
   * cf[n] is an integer between 0 and 7 with following
   * meanings (see comment at top of file for notation):
   *
   * cf[n] = 0  -  n nas not been found at all
   * cf[n] = 1  -  (n,1) has been found but not (n,2) or (n,4)
   * cf[n] = 2  -  (n,2) has been found but not (n,4)
   * cf[n] = 3  -  (n,3) has been found but not (n,1), (n,2) or (n,4)
   * cf[n] = 4  -  (n,4) has been found but not (n,1), (n,2) or (n,3)
   * cf[n] = 5  -  (n,1) and (n,4) have been found but not (n,2)
   * cf[n] = 6  -  (n,2) and (n,4) have been found
   * cf[n] = 7  -  (n,3) and (n,4) have been found but not (n,1) or (n,2)
   */


  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;
    if (!dense_op)
      len = 0;
    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). Since we are excluding words that contain subwords
       * w_1 s.t. (w_1,w_2) is accepted by *fsaptr, we also have to apply
       * (g1,g2) to the initial state of *fsaptr.
       */

      for (i = 1; i <= ndiff; i++)
        cf[i] = 0;
      ptr = cs_ptr - 1;
      no_trans = FALSE;
      /* We will set no_trans to be true if we find that the transition leads to
       * failure.
       */

      while (ptr <= cs_ptre) {
        /* We add the identity state of *fsaptr to the subset representing
         * cstate */

        cs = ptr < cs_ptr ? identity : *ptr;
        csdiff = cs % ndiff;
        if (csdiff == 0)
          csdiff = ndiff;
        /* csdiff is the state of *fsaptr corresponding to cs */
        ptr++;
        if (cs > 3 * ndiff) {
          /* The state csdiff is one where lhs>rhs. We can assume that the
           * length of w_1 does not exceed that of w_2 by more than 2 in a
           * substitution. Thus either the action of generator g1 leads
           * immediately to failure, or we can forget about this state.
           */

          csi = dense_dtarget(dtable, g1, ngens + 1, csdiff);
          if (csi == identity) {
            no_trans = TRUE;
            break;
          }
          continue;
        }
        for (g2 = 1; g2 <= ngens + 1; g2++) {
          csi = dense_dtarget(dtable, g1, g2, csdiff);
          if (csi == 0)
            continue;
          if (g2 == ngens + 1) { /*lhs gets longer than rhs */
            if (csi == identity) {
              no_trans = TRUE;
              break;
            }
            if (cf[csi] < 4)
              cf[csi] += 4;
          }
          else {
            good = cs <= ndiff ? g2 < g1 : cs <= 2 * ndiff;
            if (csi == identity) {
              if (good) {
                no_trans = TRUE;
                break;
              }
              continue;
            }
            if (good)
              cf[csi] = cf[csi] <= 3 ? 2 : 6;
            else if (cs <= ndiff && g1 == g2) {
              if (cf[csi] == 0 || cf[csi] == 3)
                cf[csi] = 1;
              else if (cf[csi] == 4 || cf[csi] == 7)
                cf[csi] = 5;
            }
            else if (cf[csi] == 0 || cf[csi] == 4)
              cf[csi] += 3;
          }
        }
        if (no_trans)
          break;
      }
      if (no_trans) {
        if (dense_op)
          fsarow[g1 - 1] = 0;
        continue;
      }
      /* Now we have the image stored in the array cf, and we translate it to a
       * list and insert it into the hash-table.
       */

      ht_ptrb = ht.current_ptr;
      ht_ptre = ht_ptrb - 1;
      for (i = 1; i <= ndiff; i++) {
        k = cf[i];
        if (k == 1)
          *(++ht_ptre) = i;
        else if (k == 2)
          *(++ht_ptre) = ndiff + i;
        else if (k == 3)
          *(++ht_ptre) = 2 * ndiff + i;
        else if (k == 4)
          *(++ht_ptre) = 3 * ndiff + i;
        else if (k == 5) {
          *(++ht_ptre) = 3 * ndiff + i;
          *(++ht_ptre) = i;
        }
        else if (k == 6) {
          *(++ht_ptre) = 3 * ndiff + i;
          *(++ht_ptre) = ndiff + i;
        }
        else if (k == 7) {
          *(++ht_ptre) = 3 * ndiff + i;
          *(++ht_ptre) = 2 * ndiff + i;
        }
      }
      im = short_hash_locate(&ht, ht_ptre - ht_ptrb + 1);
      if (dense_op)
        fsarow[g1 - 1] = im;
      else if (im > 0) {
        fsarow[++len] = g1;
        fsarow[++len] = im;
      }
      if (im > 0)
        nt++;
    }
    if (!dense_op)
      fsarow[0] = len++;
    fwrite((void *)fsarow, sizeof(int), (size_t)len, tempfile);
  }
  fclose(tempfile);

  short_hash_clear(&ht);
  tfree(fsarow);
  tfree(cf);

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

  /* All states of wa will be accept states. */
  wa->num_accepting = ns;
  if (ns == 1) {
    tmalloc(wa->accepting, int, 2);
    wa->accepting[1] = 1;
  }
  tfree(fsaptr->is_accepting);
  if (destroy)
    fsa_clear(fsaptr);

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

  unlink(tempfilename);

  return wa;
}

static fsa *fsa_wa_cos_int(fsa *fsaptr, storage_type op_table_type,
                           boolean destroy, char *tempfilename)
{
  fprintf(stderr, "Sorry - fsa_wa is not yet implemented.\n");
  fprintf(stderr, "for machines with more than 65536 states.\n");
  return 0;
}

Messung V0.5
C=93 H=84 G=88

¤ Dauer der Verarbeitung: 0.24 Sekunden  (vorverarbeitet)  ¤

*© 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.