/* 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;

void  badusage_gpmigenmult();
int   (*reduce_word)();

/* Functions defined in other files used in this file */
void  fsa_read();
fsa  *fsa_mitriples();
void  fsa_print();
int   midfa_labeled_minimize();
void  fsa_clear();
int   diff_reduce_cos();
int   add_wd_fsa_cos();
int   calculate_inverses();
int   fsa_table_dptr_init();

main(argc, argv)
        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_gpmigenmult();
      if (strcmp(argv[arg],"d")==0)
        op_store = DENSE;
      else if (strcmp(argv[arg],"s")==0)
        op_store = SPARSE;
      else
        badusage_gpmigenmult();
    }
    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_gpmigenmult();
      maxwdiffs = atoi(argv[arg]);
    }
    else if (strcmp(argv[arg],"-m")==0) {
      arg++;
      if (arg >= argc)
        badusage_gpmigenmult();
      maxeqns = atoi(argv[arg]);
    }
    else if (argv[arg][0] == '-')
      badusage_gpmigenmult();
    else if (!seengpname) {
      seengpname=TRUE;
      strcpy(gpname,argv[arg]);
    }
    else if (!seencosname) {
      seencosname=TRUE;
      sprintf(inf1,"%s.%s",gpname,argv[arg]);
    }
    else
      badusage_gpmigenmult();
    arg++;
  }
  if (!seengpname)
    badusage_gpmigenmult();
  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_gpmigenmult()
{
    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);
}
