/**CFile*******************************************************************
  PackageName [pa]
  Synopsis    [Package 'pa' is a framework for implementation of
               process algebrae similar to Milner's CCS and Hoare's CSP.]

  FileName    [paMain.c]
  Revision    [$Revision: 76 $]
  Date        [$Date: 2013-04-26 14:26:09 +0200 (pet, 26 apr 2013) $]
  Authors     [Robert Meolic (meolic@uni-mb.si)]
  Description [File paMain.c contains main functions.]
  SeeAlso     [pa.h, paInt.h]

  Copyright   [This file is part of EST (Efficient Symbolic Tools).
               Copyright (C) 2003, 2013
               UM-FERI, Smetanova ulica 17, SI-2000 Maribor, Slovenia

               EST is free software; you can redistribute it and/or modify
               it under the terms of the GNU General Public License as
               published by the Free Software Foundation; either version 2
               of the License, or (at your option) any later version.

               EST is distributed in the hope that it will be useful,
               but WITHOUT ANY WARRANTY; without even the implied warranty of
               MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
               GNU General Public License for more details.

               You should have received a copy of the GNU General Public
               License along with this program; if not, write to the Free
               Software Foundation, Inc., 51 Franklin Street, Fifth Floor,
               Boston, MA 02110-1301 USA.]
  ************************************************************************/

#include "paInt.h"

/*-----------------------------------------------------------------------*/
/* Variable declarations                                                 */
/*-----------------------------------------------------------------------*/

/* EXPORTED VARIABLES */

int pa_status = 0;                           /* initialization status */
int pa_variables = 0;                        /* number of variables */
int pa_sorts = 0;                            /* number of sorts */
int pa_processes = 0;                        /* number of processes */
int pa_compositions = 0;                     /* number of compositions */
Pa_Variable *pa_variableTable = NULL;        /* variable table */
Pa_Sort *pa_sortTable = NULL;                /* table of sorts */
Pa_Process *pa_processTable = NULL;          /* table of processes */
Pa_Composition *pa_compositionTable = NULL;  /* table of compositions */

/* INTERNAL VARIABLES */

/* used and not initialized by flex/bison */
char *patext = NULL; /* from lex.pa.c */
void *paleng = NULL; /* from lex.pa.c */
int panerrs = 0;     /* from pa.tab.c: number of syntax errors so far */
int pachar = 0;      /* from pa.tab.c: the lookahead symbol */
struct pastype {void *i1;} palval = {NULL};
   /* the semantic value of the lookahead symbol */
   /* this should be compatible with the union from paParser.y */

/**AutomaticStart*********************************************************/

/*-----------------------------------------------------------------------*/
/* Static function prototypes                                            */
/*-----------------------------------------------------------------------*/

static int wordNumber(Est_String s);

static Est_String shortname(Est_String name);

/**AutomaticEnd***********************************************************/

/*-----------------------------------------------------------------------*/
/* Definition of exported functions                                      */
/*-----------------------------------------------------------------------*/

/**Function****************************************************************
  Synopsis    []
  Description []
  SideEffects []
  SeeAlso     []
  ************************************************************************/

/* To simplify building on MS WINDOWS - Pa_Init is stated in *.def file */

#ifndef TCLOUT
   void Pa_Init(void) {}
#endif

/**Function****************************************************************
  Synopsis    [Function Pa_InitPkg.]
  Description []
  SideEffects []
  SeeAlso     []
  ************************************************************************/

void
Pa_InitPkg()
{
  if (pa_status == 1) {
    printf("\nProcess algebra package is already initialized. ");
    return;
  } else {
    pa_status = 1;
  }

  pa_variables = 0;
  pa_sorts = 0;
  pa_processes = 0;
  pa_compositions = 0;

  /* INITIALIZATION OF VARIABLE TABLE */
  /* BDD VARIABLE WITH INDEX 0 IS CONSTANT 1 */
  if (!(pa_variableTable = (Pa_Variable *) malloc(sizeof(Pa_Variable)))) {
      fprintf(stderr,"\nPa_InitPkg: Out of memory error!\n");
      exit(1);
  }
  pa_variableTable[0].weight = -1;
  pa_variableTable[0].proccomp = -1;
}

/**Function****************************************************************
  Synopsis    [Function Pa_ExitPkg.]
  Description [Pa_ExitPkg deallocates all memory allocated by pa module.]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

void
Pa_ExitPkg()
{
  int i,j;
  Pa_Sort *s;
  Pa_Process *p;
  Pa_Composition *c;

  if (pa_status == 0) {
    printf("\nPA package is not initialized. ");
    return;
  } else {
    pa_status = 0;
  }

  /*
  printf("\n");
  */

  /* DELETE VARIABLES */
  /*
  printf("Delete variables...\n");
  */
  if (pa_variableTable) free(pa_variableTable);

  /* DELETE SORTS */
  /*
  printf("Delete sorts...\n");
  */
  for(i=0;i<pa_sorts;i++) {
    s = &pa_sortTable[i];
    free(s->name);
    if (!s->deleted) {
      for(i=0; i<s->numActions; i++) {
        free(s->table[i].name);
      }
      free(s->table);
    }
  }
  if (pa_sortTable) free(pa_sortTable);
  pa_sorts = 0;

  /* DELETE PROCESSES */
  /*
  printf("Delete processes...\n");
  */
  for(i=0;i<pa_processes;i++) {
    p = &pa_processTable[i];
    free(p->name);
    if (!p->deleted) {
      if (p->compname) free(p->compname);
      for(j=0; j<p->numStates; j++) {
        free(p->tableS[j].name);
        if (p->tableS[j].ccs) {
          if (p->tableS[j].ccs) free(p->tableS[j].ccs);
        }
      }
      if (p->tableS) free(p->tableS);
      if (p->tableT) free(p->tableT);
    }
  }
  if (pa_processTable) free(pa_processTable);
  pa_processes = 0;

  /* DELETE COMPOSITIONS */
  /*
  printf("Delete compositions...\n");
  */
  for(i=0;i<pa_compositions;i++) {
    c = &pa_compositionTable[i];
    free(c->name);
    if (c->tableP) free(c->tableP);
    if (c->tableA) free(c->tableA);
    if (c->di) free(c->di);
    if (c->dij) free(c->dij);
    if (c->alphabet) free(c->alphabet);
  }
  if (pa_compositionTable) free(pa_compositionTable);
  pa_compositions = 0;
}

/**Function****************************************************************
  Synopsis    [Function Pa_AboutPkg]
  Description [Pa_AboutPkg reports release of Process algebra package.]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

void
Pa_AboutPkg() {
  printf("EST ");
  printf(EDITION);
  printf(", version ");
  printf(VERSION);
  printf(", ");
  printf("Process algebra package");
  printf("\n");
}


/**Function****************************************************************
  Synopsis    []
  Description []
  SideEffects []
  SeeAlso     []
  ************************************************************************/

void
Pa_InitVariable(int i)
{

  /* VARIABLE TABLE IS NEVER EMPTY. AT LEAST, THERE IS ELEMENT '1' AT INDEX [0] */
  if (i > pa_variables) {
    pa_variables = i;
    if (!(pa_variableTable = (Pa_Variable *)
        realloc(pa_variableTable, (pa_variables+1) * sizeof(Pa_Variable)))) {
      fprintf(stderr,"\nPa_InitVariable: Out of memory error!\n");
      exit(1);
    }
  }

  pa_variableTable[i].weight = -1;    /*  weight = 1,2,4... (decoding )  */
  pa_variableTable[i].proccomp = -1;   /* process-composition (decoding) */
}


/**Function****************************************************************
  Synopsis    []
  Description []
  SideEffects []
  SeeAlso     []
  ************************************************************************/

int
Pa_AddNewSort(Est_String name)
{
  Pa_Sort *s;
  int i;
  int sortnum;
  Est_Boolean OK;

  i = 0;
  OK = FALSE;
  if (pa_sorts > 0) {
    while (!OK && i<pa_sorts) {
      if (!strcmp(name,pa_sortTable[i].name)) {
        OK = TRUE;
      } else {
        i++;
      }
    }
  }

  if (pa_sorts == 0) {
    pa_sortTable = (Pa_Sort *) malloc (sizeof(Pa_Sort));
    s = pa_sortTable;
    pa_sorts = 1;
    sortnum = 0;
  } else {

    if (OK) {
      sortnum = i;
      Pa_DeleteSort(i);
      s = &pa_sortTable[i];
      free(s->name);
      /*
      printf(" (sort overwritten) ");
      */
    } else {
      sortnum = pa_sorts;
      pa_sorts++;
      pa_sortTable = (Pa_Sort *) realloc (pa_sortTable, pa_sorts * sizeof(Pa_Sort));
      s = &pa_sortTable[pa_sorts-1];
    }
  }

  s->name = strdup(name);
  s->deleted = FALSE;
  s->encoded = 0;
  s->numVar = 0;
  s->numActions = 0;
  s->table = NULL;
  s->a0 = bdd_termNull;

  /* ADD ACTION 'TAU' */
  /*
  s->numActions = 1;
  s->table = (Pa_Action *) malloc (sizeof(Pa_Action));
  s->table[0].name = strdup("TAU");
  s->table[0].p = bdd_termNull;
  */

  /* ADD ACTIONS 'TAU' and 'FINAL' */
  /* FINAL used for WCA */
  /**/
  s->numActions = 2;
  s->table = (Pa_Action *) malloc (2 * sizeof(Pa_Action));
  s->table[0].name = strdup("TAU");
  s->table[0].p = bdd_termNull;
  s->table[1].name = strdup("FINAL");
  s->table[1].p = bdd_termNull;
  /**/

  return sortnum;
}

/**Function****************************************************************
  Synopsis    []
  Description []
  SideEffects []
  SeeAlso     []
  ************************************************************************/

int
Pa_FindSort(Est_String name)
{
  int i = 0;

  if (!name) {
    printf("\nError: Pa_FindSort got null string!\n");
    return -1;
  }
  while (i<pa_sorts) {
    if (!strcmp(name,pa_sortTable[i].name))
      return i;
    else
      i++;
  }

  return -1;
}

/**Function****************************************************************
  Synopsis    []
  Description []
  SideEffects []
  SeeAlso     []
  ************************************************************************/

int
Pa_FOASortAction(Pa_Sort *sort, Est_String name)
{
  Pa_Action *a;
  int i;

  if (!sort) return -1;

  if (!name) {
    printf("\nError: Pa_FOASortAction got null string!\n");
    return -1;
  }

  /* SORT CANNOT BE EMPTY. ALWAYS EXIST AT LEAST ACTION 'TAU' */

  if (!strcasecmp(name,"TAU")) {
    return 0;
  }

  i = 1;
  while (i<sort->numActions) {
    if (!strcmp(name,sort->table[i].name))
      return i;
    else
      i++;
  }

  if (sort->encoded) {
    /*
    printf("\nError: You cannot add action %s to an encoded sort %s\n",name,sort->name);
    */
    return -1;
  }

  (sort->numActions)++;
  if (!(sort->table = (Pa_Action *) realloc(
  sort->table, sort->numActions * sizeof(Pa_Action)))) {
    printf("\nError: Pa_FOASortAction out of memory!\n");
    return -1;
  }


  a = &sort->table[sort->numActions-1];

  a->name = strdup(name);
  a->p = bdd_termNull;

  return (sort->numActions-1);
}

/**Function****************************************************************
  Synopsis    []
  Description []
  SideEffects []
  SeeAlso     []
  ************************************************************************/

int
Pa_FindSortAction(Pa_Sort *sort, Est_String name)
{
  int i = 0;

  if (!name) {
    printf("\nError: Pa_FindSortAction got null string!\n");
    return -1;
  }
  if (!sort) return -1;

  while (i<sort->numActions) {
    if (!strcmp(name,sort->table[i].name))
      return i;
    else
      i++;
  }

  return -1;
}

/**Function****************************************************************
  Synopsis    []
  Description []
  SideEffects []
  SeeAlso     []
  ************************************************************************/

int
Pa_AddNewProcess(Est_String name)
{
  Pa_Process *p;
  int i;
  int procnum;
  Est_Boolean OK;

  i = 0;
  OK = FALSE;
  if (pa_processes > 0) {
    while (!OK && i<pa_processes) {
      if (!strcmp(name,pa_processTable[i].name)) {
        OK = TRUE;
      } else {
        i++;
      }
    }
  }

  if (pa_processes == 0) {
    pa_processTable = (Pa_Process *) malloc (sizeof(Pa_Process));
    p = pa_processTable;
    pa_processes = 1;
    procnum = 0;
  } else {

    if (OK) {
      procnum = i;
      Pa_DeleteProcess(i);
      p = &pa_processTable[i];
      free(p->name);
      /*
      printf(" (process overwritten) ");
      */
    } else {
      procnum = pa_processes;
      pa_processes++;
      pa_processTable = (Pa_Process *) realloc (
                         pa_processTable, pa_processes * sizeof(Pa_Process));
      p = &pa_processTable[pa_processes-1];
    }
  }

  p->name = strdup(name);
  p->trace = FALSE;
  p->weak = FALSE;
  p->deleted = FALSE;
  p->compname = NULL;
  p->encoded = 0;
  p->sort = -1;
  p->numStates = 0;
  p->tableS = NULL;
  p->initial = -1;
  p->numTransitions = 0;
  p->tableT = NULL;
  p->numVar = 0;
  p->d = bdd_termNull;
  p->stab = bdd_termNull;

  return procnum;
}


/**Function****************************************************************
  Synopsis    []
  Description []
  SideEffects []
  SeeAlso     []
  ************************************************************************/

int
Pa_FindProcess(Est_String name)
{
  int i = 0;

  if (!name) {
    printf("\nError: Pa_FindProcess got null string!\n");
    return -1;
  }

  while (i<pa_processes) {
    if (!strcmp(name,pa_processTable[i].name)) {
      return i;
    } else {
      i++;
    }
  }

  return -1;
}

/**Function****************************************************************
  Synopsis    []
  Description []
  SideEffects [Renamed process has the same seq as the original one.]
  SeeAlso     []
  ************************************************************************/

void
Pa_RenameProcess(Est_String old, Est_String new)
{
  int oldproc,newproc;
  int i,j;
  Pa_Process *p;
  Est_String state;
  Est_String sup1, sup2;

  oldproc = Pa_FindProcess(old);
  if (oldproc == -1) {
    /*
    printf("Process does not exists.\n");
    */
    return;
  }

  newproc = Pa_FindProcess(new);
  if (newproc != -1) {
    /*
    printf(" (process overwritten) ");
    */
    Pa_DeleteProcess(newproc);
  }

  /* CHANGE NAME OF PROCESS */
  free(pa_processTable[oldproc].name);
  pa_processTable[oldproc].name = strdup(new);

  /* CHANGE NAME OF STATES */
  p = &pa_processTable[oldproc];
  for (i=0; i<p->numStates; i++) {
    state = strdup(p->tableS[i].name);
    if (strcmp(state,"")) {

      if (Pa_IsGate(state)) {

        if (!strcmp(state,old)) {
          free(p->tableS[i].name);
          p->tableS[i].name = strdup(new);
        }

      } else {

        /* STATES WILL GET THE NAME OF NEW PROCESS */
        j=strcspn(state,"<");
        sup1 = (Est_String) malloc(j+1);
        memcpy(sup1,state,j);
        sup1[j]=0;
        sup2 = (Est_String) malloc(65535);
        sprintf(sup2,"%s<%s>",sup1,new);
        free(p->tableS[i].name);
        p->tableS[i].name = strdup(sup2);
        free(sup1);
        free(sup2);
      }

      free(state);

    }
  }

  /* RE-ENOCDE TO GET CORRRECT NAMES FOR BDD VARIABLES */
  if (p->encoded) {
    Pa_EncodeProcess(p->name);
  }

}

/**Function****************************************************************
  Synopsis    []
  Description [name = original process, copy = new process,
               copysort = sort of new process,
               old = the list of actions to rename,
               new = new names for actions in list old]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

int
Pa_CopyProcess(Est_String name, Est_String copy, Est_String copysort,
               Est_String old, Est_String new)
{
  int procnum,copynum,oldsort,newsort;
  int n;
  Pa_Process *p,*cp;
  int i,j;
  Est_String state;
  Est_String sup1, sup2, sup1x, sup2x, act;
  int token;
  int *renamingTable;

  procnum = Pa_FindProcess(name);
  if (procnum == -1) {
    /*
    printf("Process does not exists.\n");
    */
    return -1;
  }

  /* if Pa_Composition2Process is used with option full=FALSE */
  /* then process does not have state and transition table */

  if ((pa_processTable[procnum].encoded) &&
                 (!pa_processTable[procnum].tableS)) {
    printf("ERROR: Cannot copy partly composed process.\n");
    return -1;
  }

  oldsort = pa_processTable[procnum].sort;
  if (!copysort) {
    newsort = oldsort;
  } else {

    if (Pa_FindSort(copysort) == -1) {
      printf("Sort %s does not exists.\n",copysort);
      return -1;
    }

    newsort = Pa_FindSort(copysort);
  }

  if (old) {
    sup1x = strdup(old);
  } else {
    sup1x = strdup("");
  }

  if (new) {
    sup2x = strdup(new);
  } else {
    sup2x = strdup("");
  }

  /* WARNING: AddNewProcess calls realloc(pa_processTable) */
  copynum = Pa_AddNewProcess(copy); /* add new process */

  p = &pa_processTable[procnum];
  cp = &pa_processTable[copynum];

  if (p->compname) cp->compname = strdup(p->compname);
  cp->sort = newsort;
  cp->initial = p->initial;
  cp->numVar = 0;
  cp->d = bdd_termNull;
  cp->stab = bdd_termNull;
  cp->numStates = p->numStates;
  cp->trace = p->trace;
  cp->weak = p->weak;

  /* COPY STATES */

  if (p->numStates > 0) {

    cp->tableS = (Pa_State *) malloc(p->numStates * sizeof(Pa_State));

    for (i=0; i<p->numStates; i++) {
      state = strdup(p->tableS[i].name);
      if (!strcmp(state,"")) {

         /*state is deleted */
         cp->tableS[i].name = strdup("");

      } else {

        if (Pa_IsGate(state)) {

          if (!strcmp(state,name)) {
            cp->tableS[i].name = strdup(cp->name);
          } else {
            cp->tableS[i].name = strdup(state);
          }

        } else {

          /* STATES WILL GET THE NAME SUFFIX OF NEW PROCESS */
          /**/
          j=strcspn(state,"<");
          sup1 = (Est_String) malloc(j+1);
          memcpy(sup1,state,j);
          sup1[j]=0;
          sup2 = (Est_String) malloc(65535);
          sprintf(sup2,"%s<%s>",sup1,shortname(cp->name)); /*ADDED shortname */
          cp->tableS[i].name = strdup(sup2);
          free(sup1);
          free(sup2);
          /**/

          /* STATES WILL REMAIN THE NAME SUFFIX OF OLD PROCESS */
          /* THIS SEEMS TO BE INCORRECT! */
          /*
          cp->tableS[i].name = strdup(state);
          */

        }
      }

      free(state);

      cp->tableS[i].bddR = bdd_termNull;
      cp->tableS[i].bddS = bdd_termNull;
      cp->tableS[i].bddComp = p->tableS[i].bddComp;
      cp->tableS[i].acc = bdd_termNull;
      cp->tableS[i].minacc = bdd_termNull;
      cp->tableS[i].final = p->tableS[i].final;
      cp->tableS[i].ccs = NULL;
    }
  }

  /* COPY TRANSITIONS */

  cp->numTransitions = p->numTransitions;
  if (p->numTransitions > 0) {
    cp->tableT = (Pa_Transition *)
                    malloc (p->numTransitions *sizeof(Pa_Transition));
    for (i=0; i<p->numTransitions; i++) {
      cp->tableT[i].source = p->tableT[i].source;

      if (p->tableT[i].action == 0) {
        /* OLD = TAU */
        cp->tableT[i].action = 0;
      } else {
        if ((cp->tableT[i].action = Pa_FOASortAction(&pa_sortTable[newsort],
             pa_sortTable[oldsort].table[p->tableT[i].action].name)) == -1)
        {
          printf("    ERROR: Cannot add actions to the encoded sort.\n");
          free(cp->tableT);
          cp->numTransitions = 0;
          cp->tableT = NULL;
          return -1;
        }
      }

      cp->tableT[i].type = p->tableT[i].type;
      cp->tableT[i].dest = p->tableT[i].dest;
    }
  } else {
    cp->tableT = NULL;
  }

  /* IF PROCESS IS NOT ENCODED (THEN IT IS EXPANDED) */
  /* THEN ALL GATES MUST BE EXPANDED BEFORE RENAMING */

  if (copysort && !p->encoded) {
    Pa_ExpandGates(cp);
  }

  /* RENAMING */
  /* FIRST CREATE TABLE */

  n = wordNumber(sup1x);
  if (n != wordNumber(sup2x)) {
    printf("Different number of old and new action names.\n");
    free(cp->tableT);
    cp->tableT = NULL;
    return -1;
  }

  renamingTable = (int *) calloc (2*n,sizeof(int));

  sup1 = sup1x;
  sup2 = sup2x;

  for (i=1; i<=n; i++) {
    token = strspn(sup1," ");
    sup1 = &sup1[token];
    token = strcspn(sup1," ");
    act = (Est_String) malloc(token+1);
    memcpy(act,sup1,token);
    act[token] = '\0';

    if (!strcmp(act,"tau") || !strcmp(act,"Tau") || !strcmp(act,"TAU")) {
      printf("    Warning: Action %s cannot be renamed!\n",act);
      renamingTable[2*i-2] = 0;
    } else {
      /* ADD ACTION IF IT DOES NOT EXISTS! */
      if ((renamingTable[2*i-2] = Pa_FOASortAction(&pa_sortTable[newsort],act)) == -1)
      {
        printf("    ERROR (rename): Cannot add actions to the encoded sort.\n");
        free(act);
        free(sup1x);
        free(sup2x);
        free(renamingTable);
        free(cp->tableT);
        cp->tableT = NULL;
        cp->numTransitions = 0;
        return -1;
      }
    }

    /*
    fprintf(stdout,"Action %s ",act);
    */

    free(act);
    sup1 = &sup1[token];

    token = strspn(sup2," ");
    sup2 = &sup2[token];
    token = strcspn(sup2," ");
    act = (Est_String) malloc(token+1);
    memcpy(act,sup2,token);
    act[token] = '\0';

    if (!strcmp(act,"tau") || !strcmp(act,"Tau") || !strcmp(act,"TAU")) {
      renamingTable[2*i-1] = 0;
    } else {
      /* ADD ACTION IF IT DOES NOT EXISTS! */
      if ((renamingTable[2*i-1] = Pa_FOASortAction(&pa_sortTable[newsort],act)) == -1)
      {
        printf("    ERROR (rename): Cannot add actions to the encoded sort.\n");
        free(act);
        free(sup1x);
        free(sup2x);
        free(renamingTable);
        free(cp->tableT);
        cp->tableT = NULL;
        cp->numTransitions = 0;
        return -1;
      }
    }

    /*
    fprintf(stdout,"will be renamed to action %s\n",act);
    */

    free(act);
    sup2 = &sup2[token];
  }

  free(sup1x);
  free(sup2x);

  /*
  fprintf(stdout,"Pa_CopyProcess\n");
  for (i=0; i<n; i++) {
    fprintf(stdout,"Action number %d will be ",renamingTable[2*i]);
    fprintf(stdout,"renamed to action number %d.\n",renamingTable[2*i+1]);
  }
  */

  /* RENAME ACTIONS */

  if (n>0) {
    for (i=0; i<cp->numTransitions; i++) {
      if (cp->tableT[i].action != 0) {
        for (j=0; j<n; j++) {
          if (renamingTable[2*j] == cp->tableT[i].action) {
            /* ACTION WILL BE RENAMED */
            cp->tableT[i].action = renamingTable[2*j+1];
            /* NEW = TAU */
            if (cp->tableT[i].action == 0) {
              cp->tableT[i].type = 0; /* THIS IS TYPE OF ACTION TAU */
            }
          }
        }
      }
    }
  }

  free(renamingTable);

  return copynum;
}


/**Function****************************************************************
  Synopsis    []
  Description []
  SideEffects [Difference between state and gate is the name!
               Gates are closely related to implementation of CCS parser.]
  SeeAlso     []
  ************************************************************************/

Est_Boolean
Pa_IsGate(Est_String name)
{
  Est_Boolean r;

  r = FALSE;

  if (!name) {
    printf("\nError: Pa_IsGate got null string!\n");
    return r;
  }

  if (!strcmp(name,"")) {
    r = FALSE;
  } else {
    if (strchr(name,'<')) {
      r = FALSE;
    } else {
      r = TRUE;
    }
  }

  return r;
}

/**Function****************************************************************
  Synopsis    []
  Description []
  SideEffects [Suffix '<'+proc->name+'>' is added]
  SeeAlso     []
  ************************************************************************/

int
Pa_FOAStateProcess(Pa_Process *proc, Est_String name)
{
  Est_String name1;
  Pa_State *s;
  int i;

  if (!proc) {
    printf("\nError: Pa_FOAStateProcess got null proc!\n");
    return -1;
  }

  if (!name) {
    printf("\nError: Pa_FOAStateProcess got null name!\n");
    return -1;
  }

  if (!strcmp(name,"")) {
     name1 = strdup(name);
  } else {
    if (strchr(name,'<')) {
      name1 = strdup(name);
    } else {
      name1 = (Est_String) malloc(127);
      sprintf(name1,"%s<%s>",name,shortname(proc->name)); /*ADDED shortname */
    }
  }

  i = 0;
  if (proc->numStates == 0) {
    proc->numStates = 1;
    proc->tableS = (Pa_State *) malloc (sizeof(Pa_State));
    s = proc->tableS;
  } else {
    while (i<proc->numStates) {
      if (!strcmp(name1,proc->tableS[i].name)) {
        free (name1);
        return i;
      } else {
        i++;
      }
    }

    if (proc->encoded) {
      printf("\nError: You cannot add states to an encoded process!\n");
      free (name1);
      return -1;
    }

    (proc->numStates)++;
    proc->tableS = (Pa_State *) realloc (proc->tableS,
                                    proc->numStates * sizeof(Pa_State));
    s = &proc->tableS[proc->numStates-1];
  }

  s->name = strdup(name1);
  s->bddR = bdd_termNull;
  s->bddS = bdd_termNull;
  s->bddComp = bdd_termNull;
  s->acc = bdd_termNull;
  s->minacc = bdd_termNull;
  s->final = FALSE;
  s->ccs = NULL;

  free (name1);
  return (proc->numStates-1);
}

/**Function****************************************************************
  Synopsis    []
  Description []
  SideEffects [Almost copy of FOAState.]
  SeeAlso     []
  ************************************************************************/

int
Pa_FOAGateProcess(Pa_Process *proc, Est_String name)
{
  Est_String name1;
  Pa_State *s;
  int i;

  if (!proc) {
    printf("\nError: Pa_FOAGateProcess got null proc!\n");
    return -1;
  }

  if (!name) {
    printf("\nError: Pa_FOAGateProcess got null string!\n");
    return -1;
  }

  if (strchr(name,'<')) {
    printf("\nError: The name of GATE must not contain '<>'!\n");
    return -1;
  } else {
    name1 = strdup(name);
  }

  i = 0;
  if (proc->numStates == 0) {
    proc->numStates = 1;
    proc->tableS = (Pa_State *) malloc (sizeof(Pa_State));
    s = proc->tableS;
  } else {
    while (i<proc->numStates) {
      if (!strcmp(name1,proc->tableS[i].name)) {
        free (name1);
        return i;
      } else {
        i++;
      }
    }

    if (proc->encoded) {
      printf("\nError: You cannot add gates to an encoded process!\n");
      free (name1);
      return -1;
    }

    (proc->numStates)++;
    proc->tableS = (Pa_State *) realloc (proc->tableS,
                                   proc->numStates * sizeof(Pa_State));
    s = &proc->tableS[proc->numStates-1];
  }

  s->name = strdup(name1);
  s->bddR = bdd_termNull;
  s->bddS = bdd_termNull;
  s->bddComp = bdd_termNull;
  s->acc = bdd_termNull;
  s->minacc = bdd_termNull;
  s->final = FALSE;
  s->ccs = NULL;

  free (name1);
  return (proc->numStates-1);
}

/**Function****************************************************************
  Synopsis    []
  Description []
  SideEffects []
  SeeAlso     []
  ************************************************************************/

int
Pa_FOAComposedStateProcess(Pa_Process *proc, Bdd_Edge F, Est_String prefix)
{
  int i = 0;

  if (Bdd_isNull(F)) {
    printf("\nError: Pa_FOAComposedStateProcess got bdd_termNull!\n");
    return -1;
  }

  if (Bdd_isEqv(F,bdd_termFalse)) {
    printf("\nError: Pa_FOAComposedStateProcess got bdd_termFalse!\n");
    return -1;
  }

  if (Bdd_isEqv(F,bdd_termTrue)) {
    printf("\nError: Pa_FOAComposedStateProcess got bdd_termTrue!\n");
    return -1;
  }

  if (!proc) return -1;
  if (proc->numStates > 0) {
    while (i<proc->numStates) {
      if (Bdd_isEqv(F,proc->tableS[i].bddComp)) {
        return i;
      } else {
        i++;
      }
    }
  }

  if (!prefix) {
    printf("ERROR: Pa_FOAComposedStateProcess got empty prefix!\n");
    i = -1;
  } else {
    Bdd_Fortify(F);
    i = Pa_FOANextStateProcess(proc,prefix);
    proc->tableS[i].bddComp = F;
  }

  return (i);
}

/**Function****************************************************************
  Synopsis    []
  Description []
  SideEffects []
  SeeAlso     []
  ************************************************************************/

int
Pa_FindStateProcess(Pa_Process *proc, Est_String name)
{
  int i = 0;

  if (!name) {
    printf("\nError: Pa_FindStateProcess got null string!\n");
    return -1;
  }

  if (!proc) return -1;

  i = 0;
  while (i<proc->numStates) {
    if (!strcmp(name,proc->tableS[i].name)) {
      return i;
    } else {
      i++;
    }
  }

  return -1;
}

/**Function****************************************************************
  Synopsis    []
  Description []
  SideEffects [Suffix after '<' is removed, '<'+proc->name+'>' is added]
  SeeAlso     []
  ************************************************************************/

int
Pa_AddStateProcess(Pa_Process *proc, Est_String name)
{
  Est_String name1,name2;
  int i = 0;

  if (!name) {
    printf("\nError: Pa_AddStateProcess got null string!\n");
    return -1;
  }

  if (strchr(name,'<')) {
    i = strcspn(name,"<");
    name1 = (Est_String) malloc(i+1);
    memcpy(name1,name,i);
    name1[i]=0;
  } else {
    name1 = strdup(name);
  }

  name2 = (Est_String) malloc(255);
  sprintf(name2,"%s<%s>",name1,shortname(proc->name)); /*ADDED shortname */
  while (Pa_FindStateProcess(proc,name2) != -1) {
    i = strlen(name1);
    name1 = (Est_String) realloc(name1,i+2);
    name1[i] = 0x27;
    name1[i+1] = 0x00;
    sprintf(name2,"%s<%s>",name1,shortname(proc->name)); /*ADDED shortname */
  }

  i = Pa_FOAStateProcess(proc,name2);

  free(name1);
  free(name2);
  return i;
}

/**Function****************************************************************
  Synopsis    []
  Description [Add a state to the proces. The name of the state will be
               composed of given prefix and a number.]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

int
Pa_FOANextStateProcess(Pa_Process *proc, Est_String prefix)
{
  int i;
  Est_String x;

  if (!prefix) {
    printf("\nError: Pa_FOANextStateProcess got null string!\n");
    return -1;
  }

  x = (Est_String) malloc(127);
  sprintf(x,"%s%d<%s>",prefix,proc->numStates+1,shortname(proc->name)); /*ADDED shortname */

  i = Pa_FOAStateProcess(proc,x);

  free(x);
  return i;
}


/**Function****************************************************************
  Synopsis    []
  Description []
  SideEffects []
  SeeAlso     []
  ************************************************************************/

int
Pa_NumberStateProcess(Pa_Process *proc)
{
  int i;
  int n;

  n = 0;
  for(i=0; i<proc->numStates; i++) {
    if (strcmp(proc->tableS[i].name,"")) {
      if (!Pa_IsGate(proc->tableS[i].name)) {
        n++;
      }
    }
  }

  return n;
}

/**Function****************************************************************
  Synopsis    []
  Description [type 0 = output, type 1 = input]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

int
Pa_FOATransition(Pa_Process *proc, int state1, int action, int type,
                 int state2)
{
  Pa_Transition *t;
  int i = 0;

  if (!proc) return -1;
  if (proc->numTransitions == 0) {
    proc->numTransitions = 1;
    proc->tableT = (Pa_Transition *) malloc (sizeof(Pa_Transition));
    t = proc->tableT;
  } else {
    while (i<proc->numTransitions) {
      if ((state1 == proc->tableT[i].source) &&
          (action == proc->tableT[i].action) &&
          (type == proc->tableT[i].type) &&
          (state2 == proc->tableT[i].dest))
      {
        return i;
      } else {
        i++;
      }
    }

    if (proc->encoded) {
      printf("\nError: You cannot add transitions to an encoded process!\n");
      return -1;
    }

    (proc->numTransitions)++;
    proc->tableT = (Pa_Transition *) realloc (proc->tableT,
                                proc->numTransitions * sizeof(Pa_Transition));

    t = &proc->tableT[proc->numTransitions-1];
  }

  t->source = state1;
  t->action = action;
  t->type = type;
  t->dest = state2;

  return (proc->numTransitions-1);
}

/**Function****************************************************************
  Synopsis    []
  Description []
  SideEffects []
  SeeAlso     []
  ************************************************************************/

int
Pa_AddNewComposition(Est_String name, int type, int numP, int numA)
{
  Pa_Composition *c;
  int i = 0;
  int compnum;
  Est_Boolean OK;

  if (pa_compositions > 0) {
    OK = FALSE;
    while (!OK && i<pa_compositions) {
      if (!strcmp(name,pa_compositionTable[i].name)) {
        OK = TRUE;
      } else {
        i++;
      }
    }
    if (OK) {
      Pa_RemoveComposition(i);
    }
  }

  if (pa_compositions == 0) {
    pa_compositionTable = (Pa_Composition *) malloc (sizeof(Pa_Composition));
    c = pa_compositionTable;
    pa_compositions = 1;
    compnum = 0;
  } else {
    compnum = pa_compositions;
    pa_compositions++;
    pa_compositionTable = (Pa_Composition *) realloc (pa_compositionTable,
                           pa_compositions * sizeof(Pa_Composition));
    c = &pa_compositionTable[compnum];
  }

  c->name = strdup(name);
  c->type = type;
  c->numProcesses = numP;
  c->tableP = (int *) calloc (numP,sizeof(int));
  c->numActions = numA;
  if (numA > 0) {
    c->tableA = (int *) calloc (numA,sizeof(int));
  } else {
    c->tableA = NULL;
  }
  c->sort = -1;
  c->initialBDD = bdd_termNull;
  c->stateBDD = bdd_termNull;
  c->transitionBDD = bdd_termNull;
  /* c->stab = bdd_termNull; */
  c->di = NULL;
  c->dij = NULL;
  c->alphabet = NULL;
  c->snew = bdd_termNull;
  c->onthefly = FALSE;
  c->full = FALSE;
  c->trace = FALSE;
  c->weak = FALSE;
  c->strong = FALSE;

  return (compnum);
}

/**Function****************************************************************
  Synopsis    []
  Description []
  SideEffects [ The state is only erased and not deleted from the table.
                Positions of states in the state table are not changed.]
  SeeAlso     []
  ************************************************************************/

void
Pa_DeleteStateProcess(Pa_Process *proc, int num)
{
  Pa_State *s;

  s = &proc->tableS[num];

  if (s->name) {
    free(s->name);
    s->name = strdup("");
  }
  s->bddR = bdd_termNull;
  s->bddS = bdd_termNull;
  s->bddComp = bdd_termNull;
  s->acc = bdd_termNull;
  s->minacc = bdd_termNull;
  s->final = FALSE;
  if (s->ccs) {
    free(s->ccs);
    s->ccs = NULL;
  }
}

/**Function****************************************************************
  Synopsis    []
  Description []
  SideEffects [Sort is erased and not removed from the table!
               The sequence numbers of other sorts are not changed.]
  SeeAlso     []
  ************************************************************************/

void
Pa_DeleteSort(int num)
{
  int i;
  Pa_Sort *s;

  if (num == -1) return;
  s = &pa_sortTable[num];
  free(s->name);
  s->name = strdup("DELETED");

  for(i=0; i<s->numActions; i++) {
    if (s->table[i].name) {
      free(s->table[i].name);
      s->table[i].name = NULL;
    }
  }

  free(s->table);

  s->deleted = TRUE;
  s->encoded = 0;
  s->numVar = 0;
  s->numActions = 0;
  s->table = NULL;
  s->a0 = bdd_termNull;
}

/**Function****************************************************************
  Synopsis    []
  Description []
  SideEffects [The sequence numbers of sorts can be changed!]
  SeeAlso     []
  ************************************************************************/

void
Pa_RemoveDeletedSorts()
{
  int i;

  i = 0;
  while (i < pa_sorts) {
    if (pa_sortTable[i].deleted) {
      free(pa_sortTable[i].name);
      if (pa_sorts == 1) {
        free(pa_sortTable);
        pa_sorts = 0;
      } else {
        pa_sorts--;
        if (i != pa_sorts) {
          pa_sortTable[i] = pa_sortTable[pa_sorts];
        }
        pa_sortTable = (Pa_Sort *) realloc (pa_sortTable,
                        pa_sorts * sizeof(Pa_Sort));
      }
    } else {
      i++;
    }
  }
}

/**Function****************************************************************
  Synopsis    []
  Description []
  SideEffects [Process is erased and not removed from the table!
               The sequence numbers of other processes are not changed.]
  SeeAlso     []
  ************************************************************************/

void
Pa_DeleteProcess(int num)
{
  int i;
  Pa_Process *p;

  if (num == -1) return;
  p = &pa_processTable[num];

  if (p->name) free(p->name);
  p->name = strdup("DELETED");

  if (p->compname) free(p->compname);
  p->compname = NULL;

  for(i=0; i<p->numStates; i++) {
    if (p->tableS[i].name) {
      free(p->tableS[i].name);
      p->tableS[i].name = NULL;
    }
    if (p->tableS[i].ccs) {
      free(p->tableS[i].ccs);
      p->tableS[i].ccs = NULL;
    }
  }

  if (p->tableS) free(p->tableS);
  if (p->tableT) free(p->tableT);

  p->deleted = TRUE;
  p->encoded = 0;
  p->sort = -1;
  p->numStates = 0;
  p->tableS = NULL;
  p->initial = -1;
  p->numTransitions = 0;
  p->tableT = NULL;
  p->numVar = 0;
  p->d = bdd_termNull;
  p->stab = bdd_termNull;
}

/**Function****************************************************************
  Synopsis    []
  Description []
  SideEffects [The sequence numbers of processes can be changed!]
  SeeAlso     []
  ************************************************************************/

void
Pa_RemoveDeletedProcesses()
{
  int i;

  i = 0;
  while (i < pa_processes) {
    if (pa_processTable[i].deleted) {
      free(pa_processTable[i].name);
      if (pa_processes == 1) {
        free(pa_processTable);
        pa_processTable = NULL;
        pa_processes = 0;
      } else {
        pa_processes--;
        if (i != pa_processes) {
          pa_processTable[i] = pa_processTable[pa_processes];
        }
        pa_processTable = (Pa_Process *) realloc (pa_processTable,
                           pa_processes * sizeof(Pa_Process));
      }
    } else {
      i++;
    }
  }
}

/**Function****************************************************************
  Synopsis    []
  Description []
  SideEffects []
  SeeAlso     []
  ************************************************************************/

void
Pa_RemoveComposition(int num)
{
  Pa_Composition *c;

  if (num == -1) return;
  c = &pa_compositionTable[num];

  free(c->name);
  c->name = NULL;

  if (c->tableP) free(c->tableP);
  if (c->tableA) free(c->tableA);
  if (c->di) free(c->di);
  if (c->dij) free(c->dij);
  if (c->alphabet) free(c->alphabet);

  if (pa_compositions == 1) {
    free(pa_compositionTable);
    pa_compositionTable = NULL;
    pa_compositions = 0;
  } else {
    pa_compositions--;
    if (num != pa_compositions) {
      pa_compositionTable[num] = pa_compositionTable[pa_compositions];
    }
    pa_compositionTable = (Pa_Composition *) realloc (pa_compositionTable,
                            pa_compositions * sizeof(Pa_Composition));
  }
}

/**Function****************************************************************
  Synopsis    []
  Description []
  SideEffects []
  SeeAlso     []
  ************************************************************************/

int
Pa_FindComposition(Est_String name)
{
  int i = 0;

  if (!name) {
    printf("\nError: Pa_FindComposition got null string!\n");
    return -1;
  }

  while (i<pa_compositions) {
    if (!strcmp(name,pa_compositionTable[i].name)) {
      return i;
    } else {
      i++;
    }
  }

  return -1;
}

/**Function****************************************************************
  Synopsis    []
  Description []
  SideEffects []
  SeeAlso     []
  ************************************************************************/

int
Pa_FindProcessComp(Pa_Composition *c, Est_String name)
{
  int i = 0;

  if (!name) {
    printf("\nError: Pa_FindProcessComp got null string!\n");
    return -1;
  }

  if (!c) return -1;

  while (i<c->numProcesses) {
    if (!strcmp(name,pa_processTable[c->tableP[i]].name))
      return i;
    else
      i++;
  }

  return -1;
}

/**Function****************************************************************
  Synopsis    []
  Description [THIS FUNCTION IS WRONG - DO NOT USE IT!]
  SideEffects [Name must be enclosed in "<>".
               There can be multiple names.]
  SeeAlso     []
  ************************************************************************/

Bdd_Edge
Pa_AddStab(Bdd_Edge d, Est_String name)
{
  Bdd_Edge f0, f1, h0, h1;

  static Est_String zname; /* STATIC TO MINIMIZE STACK PROBLEMS */
  static Est_String pname; /* STATIC TO MINIMIZE STACK PROBLEMS */
  static Est_String v;     /* STATIC TO MINIMIZE STACK PROBLEMS */
  static Bdd_Edge h;       /* STATIC TO MINIMIZE STACK PROBLEMS */

  /* IT IS NOT POSSIBLE TO ADD stabs WITH BDD-BASED MANIPULATION */

  fprintf(stderr,"FUNCTION Pa_AddStab IS WRONG - DO NOT USE IT!\n");
  exit(1);

  if (Bdd_isTerminal(d)) return d;

  /* DETERMINING THE SUCCESSORS */

  f0 = Bdd_TransferMark(Bdd_GetElse(d), d.mark);
  f1 = Bdd_TransferMark(Bdd_GetThen(d), d.mark);

  /* DO RECURSIVE CALLS */

  h0 = Pa_AddStab(f0,name);
  h1 = Pa_AddStab(f1,name);

  /* DETERMINING TOP VARIABLE */

  zname = Bdd_GetVariableName(d);

  /* FIND OUT THE NAME OF THE PROCESS */

  if (zname[0] == 'r') {
    pname = &zname[1+strspn(&zname[1],"0123456789")];
  }

  /* COMPOSE PARTIAL RESULTS */

  if ( (zname[0] == 'r') && !strstr(name,pname)) {

    v = strdup(zname);
    v[0] = 's';

    h = Bdd_ITE(Bdd_FoaTerminal(zname),
                Bdd_ITE(Bdd_FoaTerminal(v),h1,bdd_termFalse),
                Bdd_ITE(Bdd_FoaTerminal(v),bdd_termFalse,h0));

    free(v);

  } else {

    h = Bdd_ITE(Bdd_FoaTerminal(zname),h1,h0);

  }

  return h;
}

/**Function****************************************************************
  Synopsis    []
  Description []
  SideEffects []
  SeeAlso     []
  ************************************************************************/

void
PaSaveSortActions(Pa_Sort *s)
{
  int i;
  Est_String x;

  for (i=1; i<s->numActions; i++) {
    x = (Est_String) malloc(10 + strlen(s->name) + strlen(s->table[i].name));
    sprintf(x,"Action_%s_%s!",s->name,s->table[i].name);
    Bdd_AddFormula(x,Bdd_ITE(s->a0,s->table[i].p,bdd_termFalse));
    x[strlen(x)-1] = '?';
    Bdd_AddFormula(x,Bdd_ITE(s->a0,bdd_termFalse,s->table[i].p));
    free(x);
  }

  /* ACTION TAU */

  x = (Est_String) malloc(12 + strlen(s->name));
  sprintf(x,"Action_%s_TAU",s->name);
  Bdd_AddFormula(x,s->table[0].p);
  free(x);
}

/**Function****************************************************************
  Synopsis    []
  Description []
  SideEffects []
  SeeAlso     []
  ************************************************************************/

void
PaSaveProcStates(Pa_Process *p)
{
  int i;
  Est_String x;

  for (i=0; i<(p->numStates); i++) {
    x = (Est_String) malloc(8 + strlen(p->name) + strlen(p->tableS[i].name));
    sprintf(x,"State_%s_%s",p->name,p->tableS[i].name);
    Bdd_AddFormula(x,p->tableS[i].bddR);
    free(x);
  }
}

/*-----------------------------------------------------------------------*/
/* Definition of internal functions                                      */
/*-----------------------------------------------------------------------*/

/*-----------------------------------------------------------------------*/
/* Definition of static functions                                        */
/*-----------------------------------------------------------------------*/

/**Function****************************************************************
  Synopsis    []
  Description []
  SideEffects []
  SeeAlso     []
  ************************************************************************/

static int
wordNumber(Est_String s)
{
  int num;
  int token;
  Est_String sup,sup_next;

  num = 0;
  sup = strdup(s);

  token = strspn(sup," ");
  while (strspn(sup," ") < strlen(sup)) {
    sup_next = (Est_String) strdup(&sup[token]);
    free(sup);
    sup = sup_next;

    num++;
    token = strcspn(sup," ");
    sup_next = (Est_String) strdup(&sup[token]);
    free(sup);
    sup = sup_next;

    token = strspn(sup," ");
  }

  free(sup);
  return num;
}

/**Function****************************************************************
  Synopsis    [Function shortname]
  Description [Remove text after '#']
  SideEffects [This may be different than in other files.]
  SeeAlso     []
  ************************************************************************/

static Est_String
shortname(Est_String name) {
  int i;
  Est_String shortname;

  i = strcspn(name,"#");
  shortname = (char *) malloc(i+1);
  memcpy(shortname,name,i);
  shortname[i]=0;
  return(shortname);
}
