Quelle gpmigenmult.c Sprache: C

/* gpmigenmult.c 11/10/94.
* 6/8/98 large scale reorganisation to omit globals, etc.
* 16/3/96 - changed command-line syntax to
* gpmigenmult [options] groupname [cosname]
* where cosname defaults to "cos".
* Calculates the general multiplier with multiple initial states for a
* short-lex coset automatic group.
* Very similar to gpgenmult.c
*
* SYNOPSIS:
* gpmigenmult [-op d/s] [-silent] [-v] [-l/-h] [-c] [-mwd maxwdiffs]
*           [-m maxeqns] [-ns] groupname [cosname]
*
* Input is from groupname.cosname.wa and groupname.cosname.midiff2
*  (and possibly from groupname.cosname.midiff1 if -c option is called).
* Output is to groupname.cosname.migm
*  (or possibly to groupname.cosname.midiff1 if -c option is called).
*
* OPTIONS:
* -op d/s output in dense or sparse format - sparse is default
* -v verbose
* -silent no diagnostics
* -l/-h large/huge hash-tables (for big examples)
* -c (correction)
*              If equations are discovered which proves the word-acceptor
*              to be incorrect, then the first word-difference machine
*              (which should be in file groupname.cosname.midiff1) is updated
*              by making it accept these equations.
*              There is no point in calling this option if gpwa was run
*              with input from groupname.cosname.midiff2, since such an
*              equation cannot occur in that case.
* -mwd maxwdiffs
*              At most maxwdiffs word-differences possible.
* -m  maxeqns
* (only relevant if -c is called)
*              Abort the multiplier checking process after finding maxeqns
*              offending words w (see above) -  default is MAXEQNS
* -ns Don't stop if nontrivial equation found in word-acceptor
* language.
*
* EXIT STATUS:
* If new equations are discovered, then the exit status is 2
* (whether or not the correction option was called).
* Otherwise, with normal output to groupname.cosname.migm, status is 0.
*/

#include <stdio.h>
#include "defs.h"
#include "fsa.h"
#include "rws.h"
#include "definitions.h"
#define MAXWDIFFS 4096
#define MAXEQNS 512

static FILE *rfile, *wfile;

static void badusage(void);
int (*reduce_word)(gen *w, reduction_struct *rs_rws);

int main(int argc, char *argv[])
{
  int arg, i, ct, *inv, ngens, maxwdiffs, maxeqns;
  fsa wa, diff1, diff2, *migenmultptr;
  char gpname[100], inf1[100], inf2[100], inf3[100], outf[100], fsaname[100],
      tempfilename[100];
  reduction_equation *eqnptr;
  reduction_struct rs_wd;
  boolean correction = FALSE;
  storage_type op_store = SPARSE;
  boolean eqnstop = TRUE;
  boolean foundeqns;
  boolean readback = TRUE;
  boolean seengpname, seencosname;

  setbuf(stdout, (char *)0);
  setbuf(stderr, (char *)0);

  maxwdiffs = MAXWDIFFS;
  maxeqns = MAXEQNS;
  inf1[0] = '\0';
  arg = 1;
  seengpname = seencosname = FALSE;
  while (argc > arg) {
    if (strcmp(argv[arg], "-op") == 0) {
      arg++;
      if (arg >= argc)
        badusage();
      if (strcmp(argv[arg], "d") == 0)
        op_store = DENSE;
      else if (strcmp(argv[arg], "s") == 0)
        op_store = SPARSE;
      else
        badusage();
    }
    else if (strcmp(argv[arg], "-silent") == 0)
      kbm_print_level = 0;
    else if (strcmp(argv[arg], "-v") == 0)
      kbm_print_level = 2;
    else if (strcmp(argv[arg], "-vv") == 0)
      kbm_print_level = 3;
    else if (strcmp(argv[arg], "-l") == 0)
      kbm_large = TRUE;
    else if (strcmp(argv[arg], "-h") == 0)
      kbm_huge = TRUE;
    else if (strcmp(argv[arg], "-c") == 0)
      correction = TRUE;
    else if (strcmp(argv[arg], "-ns") == 0)
      eqnstop = FALSE;
    else if (strcmp(argv[arg], "-f") == 0) {
      readback = FALSE;
      fprintf(stderr, "Sorry - readback option not yet available.\n");
      exit(1);
    }
    else if (strcmp(argv[arg], "-mwd") == 0) {
      arg++;
      if (arg >= argc)
        badusage();
      maxwdiffs = atoi(argv[arg]);
    }
    else if (strcmp(argv[arg], "-m") == 0) {
      arg++;
      if (arg >= argc)
        badusage();
      maxeqns = atoi(argv[arg]);
    }
    else if (argv[arg][0] == '-')
      badusage();
    else if (!seengpname) {
      seengpname = TRUE;
      strcpy(gpname, argv[arg]);
    }
    else if (!seencosname) {
      seencosname = TRUE;
      sprintf(inf1, "%s.%s", gpname, argv[arg]);
    }
    else
      badusage();
    arg++;
  }
  if (!seengpname)
    badusage();
  if (!seencosname)
    sprintf(inf1, "%s.cos", gpname);

  strcpy(tempfilename, inf1);
  strcat(tempfilename, "temp_triples_XXX");

  strcpy(inf2, inf1);
  strcat(inf2, ".midiff2");

  if (correction) {
    strcpy(inf3, inf1);
    strcat(inf3, ".midiff1");
  }

  strcpy(outf, inf1);
  strcat(outf, ".migm");

  strcat(inf1, ".wa");

  if ((rfile = fopen(inf1, "r")) == 0) {
    fprintf(stderr, "Cannot open file %s.\n", inf1);
    exit(1);
  }
  fsa_read(rfile, &wa, DENSE, 0, 0, TRUE, fsaname);
  fclose(rfile);
  if ((rfile = fopen(inf2, "r")) == 0) {
    fprintf(stderr, "Cannot open file %s.\n", inf2);
    exit(1);
  }
  fsa_read(rfile, &diff2, DENSE, 0, 0, TRUE, fsaname);
  fclose(rfile);

  if (correction)
    tmalloc(eqnptr, reduction_equation, maxeqns) else
    {
      eqnptr = 0;
      maxeqns = 0;
    }

  migenmultptr = fsa_mitriples(&wa, &diff2, op_store, TRUE, tempfilename,
                               eqnptr, maxeqns, eqnstop, &foundeqns, readback);

  if (foundeqns) { /*This is the case where new equations were found. */
    if (correction) {
      if (kbm_print_level > 1)
        printf(" #Altering wd-machine to make it accept new equations.\n");
      if ((rfile = fopen(inf3, "r")) == 0) {
        fprintf(stderr, "Cannot open file %s.\n", inf3);
        exit(1);
      }
      fsa_read(rfile, &diff1, DENSE, 0, maxwdiffs, TRUE, fsaname);
      fclose(rfile);
      if (fsa_table_dptr_init(&diff1) == -1)
        exit(1);
      tmalloc(diff1.is_initial, boolean, maxwdiffs + 1);
      for (i = 1; i <= maxwdiffs; i++)
        diff1.is_initial[i] = FALSE;
      for (i = 1; i <= diff1.num_initial; i++)
        diff1.is_initial[diff1.initial[i]] = TRUE;
      reduce_word = diff_reduce_cos;
      if (fsa_table_dptr_init(&diff1) == -1)
        exit(1);

      /* We need to know the inverses of generators - let's just work them out!
       */
      ngens = diff1.alphabet->base->size;
      rs_wd.wd_fsa = &diff2;
      rs_wd.separator = diff2.alphabet->base->size + 1;
      if (calculate_inverses(&inv, ngens, &rs_wd) == -1)
        exit(1);

      i = 0;
      while (eqnptr[i].lhs && i < maxeqns) {
        if (add_wd_fsa_cos(&diff1, eqnptr + i, inv, FALSE, &rs_wd) == -1)
          exit(1);
        i++;
      }
      tfree(diff1.initial);
      tmalloc(diff1.initial, int, diff1.num_initial + 1);
      ct = 0;
      for (i = 1; i <= diff1.states->size; i++)
        if (diff1.is_initial[i])
          diff1.initial[++ct] = i;
      tfree(diff1.is_initial);

      if (kbm_print_level > 1)
        printf(" #Word-difference machine now has %d states.\n",
               diff1.states->size);

      wfile = fopen(inf3, "w");
      fsa_print(wfile, &diff1, fsaname);
      fclose(wfile);

      tfree(inv);
      fsa_clear(&diff1);
      i = 0;
      while (eqnptr[i].lhs && i < maxeqns) {
        tfree(eqnptr[i].lhs);
        tfree(eqnptr[i].rhs);
        i++;
      }
      tfree(eqnptr);
    }
    fsa_clear(&diff2);
    exit(2);
  }

  if (migenmultptr == 0)
    exit(1);

  if (kbm_print_level > 1)
    printf(" #Number of states of mi-multiplier before minimisation = %d.\n",
           migenmultptr->states->size);
  if (readback) {
    if (midfa_labeled_minimize(migenmultptr) == -1)
      exit(1);
  }
  /*
    else
      fsa_ip_labeled_minimize(migenmultptr);
  */
  if (kbm_print_level > 1)
    printf(" #Number of states of mi-multipler after minimisation = %d.\n",
           migenmultptr->states->size);

  base_prefix(fsaname);
  strcat(fsaname, ".migm");
  wfile = fopen(outf, "w");
  fsa_print(wfile, migenmultptr, fsaname);
  fclose(wfile);

  if (kbm_print_level > 0)
    printf("#Generalised multiplier with %d states computed.\n",
           migenmultptr->states->size);

  fsa_clear(migenmultptr);
  tfree(migenmultptr);
  if (correction)
    tfree(eqnptr);
  exit(0);
}

void badusage(void)
{
  fprintf(stderr, "Usage: gpmigenmult [-op d/s] [-silent] [-v] [-l/-h] [-c] "
                  "[-mwd maxwdiffs]\n");
  fprintf(stderr, " [-m maxeqns] [-ns] groupname [cosname].\n");
  exit(1);
}

quality95%

¤ Dauer der Verarbeitung: 0.17 Sekunden (vorverarbeitet) ¤

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 ist noch experimentell.