/**CFile*******************************************************************
  PackageName [ccs]
  Synopsis    [Package 'ccs' provides an extended CCS parser.]

  FileName    [ccsParser.y]
  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 ccsParser.y is a bison file for CCS parser.]
  SeeAlso     [ccs.h, ccsInt.h, ccsParser.l]

  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.]
  ************************************************************************/

/* *********************************************************************** */
/* DIFFERENT TYPES OF COMPOSITIONS ARE IMPLEMENTED                         */
/*                                                                         */
/* COMPOSITION - full composition                                          */
/* NET - full composition                                                  */
/* CIRCUIT - parallel composition with fundamental-mode normalization      */
/* AUTOMATON -                                                             */
/* PRODUCT -                                                               */
/*                                                                         */
/* THESE KEYWORDS ARE COMBINED WITH THE FOLLOWING SYMBOLS                  */
/*                                                                         */
/* // - CCS parallel composition                                           */
/* /// - multi-way composition                                             */
/* | - CCS parallel composition                                            */
/* || - LOTOS synchronisation                                              */
/* ||| - LOTOS interleaving                                                */
/*                                                                         */
/* COMPOSITIONS ARE POSTPROCESSED WITH REGARD TO OPTIONAL PREFIXES         */
/* raw - composition is not postprocessed                                  */
/* full - return process instead of composition                            */
/* trace - return minimal deterministic process which is trace equivalent  */
/* weak - return minimal process which is weak equivalent                  */
/* strong - return minimal process which is strong equivalent              */
/* onthefly: COMPOSITION IS PREPARED BUT NOT CALCULATED                    */
/*                                                                         */
/* DIFFERENT TYPES OF COMPOSITIONS HAVE DIFFERENT DEFAULTS                 */
/* COMPOSITION - default is 'raw', all other types are allowed             */
/* NET - default is 'full', only 'raw' is allowed                          */
/* CIRCUIT - default is 'trace', only 'raw' is allowed                     */
/*                                                                         */
/* COMPOSED PROCESSES CAN BE MARKED                                        */
/* IN THIS CASE MINIMISED PROCESS WILL BE USED FOR COMPOSITION             */
/* trace - use minimal deterministic process which is trace equivalent     */
/* weak - use minimal process which is weak equivalent                     */
/* *********************************************************************** */

/* *********************************************************************** */
/* USE THE FOLLOWING TO TRASFORM FSP INTO CCS                              */
/* BE CAREFUL: FSP DOES NOT USE ! AND ? IN THE NAME OF ACTIONS             */
/* sed "s/,//g;s/\.//g;s/->/./g;s/|/+/g" example.fsp > example.ccs         */
/* *********************************************************************** */

%{
#include "ccsInt.h"
#define YYERROR_VERBOSE
#define YYMAXDEPTH 200
%}

%{
   typedef struct {
     int act;
     int type;
   } typedAction;
   typedef struct {
     typedAction *set;
     int len;
   } actionTrace;
%}

%{
   static void concat(Est_String *s1, const Est_String s2);
   static void outline(char *s);
   static void lowercase(char *s);
   static void addToSet(int **set, int *len, int state);
   static void addToTracelist(actionTrace **set, int *len, actionTrace trace);
   static void extendTrace(typedAction **set, int *len, int act, int type);
   static void extendTraces(actionTrace *set, int len, int act, int type);
   static void joinTraces(actionTrace **set, int *len, actionTrace *set1, int len1);
   static void concatTraces(actionTrace **set, int *len, actionTrace *set1, int len1);
   static void writeSet(int *set, int len);
   static void writeTraceSet(actionTrace *set, int len);
   static int error(const char *s);
%}

%{
  extern int yylex(void);
  int yywrap();
  int yyerror(const char *s);
%}

%{
   int CCSSort = 0;
   int CCSProc = 0;
   Est_String CCSinputfile = NULL;
   Est_String CCSsortname = NULL;
   Est_String CCSLowerProc = NULL;
   Est_String CCSPlist = NULL;
   Est_String CCSAlist = NULL;
   Est_String CCSOld = NULL;
   Est_String CCSNew = NULL;
   int CCSNum = 0;
   int CCSNump = 0;
   int CCSNuma = 0;
   int CCSCompType = 0;
   Est_Boolean CCSquiet = FALSE;
   Est_Boolean CCScircuit = FALSE;
   Est_Boolean CCSonthefly = FALSE;
   Est_Boolean CCSraw = FALSE;
   Est_Boolean CCSfull = FALSE;
   Est_Boolean CCStrace = FALSE;
   Est_Boolean CCSweak = FALSE;
   Est_Boolean CCSstrong = FALSE;
   Est_Boolean CCSptrace = FALSE;
   Est_Boolean CCSpweak = FALSE;
%}

%union {
  Est_String outline;
  Est_String word;
  Est_String line;
  struct {
    int *set;
    int len;
  } setOfStates;
  struct {
    actionTrace *set;
    int len;
  } setOfTraces;
}

%token UNKNOWN
%token <outline> OUTLINE
%token <word> PROCESS NAME ACTION SEP
%token <word> NET CIRCUIT COMPOSITION
%token <word> ONTHEFLY RAW FULL TRACE WEAK STRONG
%token <word> INTERLEAVE SYNCHRONOUS COMPOSE MULTIWAY
%token <word> STARTPARTIAL ENDPARTIAL
%token <word> PROPERTY AUTOMATON PRODUCT SYNPROD
%token <line> FORMULA
%type <setOfStates> procbody
%type <setOfTraces> onetrace
%type <setOfTraces> tracelist

%left '+'
%left SEP

%%
  start         : body ;

  body          : body outline
                | body process
                | body PROCESS process
                | body onthefly cprefix COMPOSITION {
                    CCScircuit = FALSE;
                    if (!CCSfull && !CCStrace && !CCSweak && !CCSstrong) CCSraw = TRUE;
                  } net
                | body onthefly cprefix NET {
                    CCScircuit = FALSE;
                    if (CCStrace) {printf("('trace' ignored)\n"); CCStrace = FALSE;}
                    if (CCSweak) {printf("('weak' ignored)\n"); CCSweak = FALSE;}
                    if (CCSstrong) {printf("('strong' ignored)\n"); CCSstrong = FALSE;}
                    if (!CCSraw) CCSfull = TRUE;
                  } net
                | body onthefly cprefix CIRCUIT {
                    CCScircuit = TRUE;
                    if (CCSfull) {printf("('full' ignored)\n"); CCSfull = FALSE;}
                    if (CCSweak) {printf("('weak' ignored)\n"); CCSweak = FALSE;}
                    if (CCSstrong) {printf("('strong' ignored)\n"); CCSstrong = FALSE;}
                    if (!CCSraw) CCStrace = TRUE;
                  } net
                | body PROPERTY property
                | body AUTOMATON automaton
                | body PRODUCT product
                | body INTERLEAVE {
                    printf("\n  ERROR in CCS parser: composition without NET!\n");
                  }
                | body SYNCHRONOUS {
                    printf("\n  ERROR in CCS parser: composition without NET!\n");
                  }
                | body COMPOSE {
                    printf("\n  ERROR in CCS parser: composition without NET!\n");
                  }
                | body MULTIWAY {
                    printf("\n  ERROR in CCS parser: composition without NET!\n");
                  }
                | body STARTPARTIAL {
                    printf("\n  ERROR in CCS parser: composition without NET!\n");
                    printf("  (morevoer, partial synchronisation is limited to two processes, yet)\n");
                  }
                | ;

  outline       : OUTLINE {

                    Est_String tmp;

                    tmp = strdup($1);
                    outline(tmp);
                    free(tmp);
                    free($1);
                  } ;

  property      : NAME FORMULA {

                    Est_String name;
                    Est_String formula;
                    int i;

                    name = strdup($1);
                    printf("  Property %s\n",name);

                    i = strspn(&$2[2]," ");
                    formula = strdup(&$2[i+2]);

                    /*
                    fprintf(stderr,"FORMULA NAME = %s\n",name);
                    fprintf(stderr,"FORMULA BODY = %s\n",formula);
                    */

                    Mc_ReadACTL(name,formula);

                    i = Mc_FindFormula(name);
                    if (i != -1) {
                      printf("    %s = %s\n",name,mc_formulaTable[i].formula);
                    }

                    free(name);
                    free(formula);
                    free($1);
                    free($2);
                  } ;

  automaton     : NAME '=' NAME '@' NAME {

                    Est_String aname,fname,pname;

                    aname = strdup($1);
                    fname = strdup($3);
                    pname = strdup($5);

                    printf("  Automaton %s\n",aname);
                    printf("    Creating automaton %s @ %s ... ",fname,pname);

                    Mc_GenerateWCA(pname,fname,aname);

                    free(aname);
                    free(fname);
                    free(pname);
                    free($1);
                    free($3);
                    free($5);
                  } ;

  product       : NAME {

                    Est_String name;

                    /*
                    fprintf(stderr,"PRODUCT NAME %s\n",$1);
                    */

                    name = strdup($1);
                    printf("  Product %s\n",name);

                    CCSNuma = 0;
                    CCSAlist = NULL;

                    free(name);
                  }

                  '=' '(' NAME SYNPROD NAME ')' restrlist {

                    Est_String name,pname,aname;

                    name = strdup($1);
                    pname = strdup($5);
                    aname = strdup($7);

                    Strucval_SyncProduct(name,pname,aname,CCSAlist);

                    free(name);
                    free(pname);
                    free(aname);
                    free(CCSAlist);
                    free($1);
                    free($5);
                    free($7);
                  } ;

  process       : NAME {

                    Est_String name;

                    /*
                    fprintf(stderr,"process NAME %s\n",$1);
                    */

                    name = strdup($1);
                    if (!CCSquiet) printf("  Process %s ... ",name);

                    CCSProc = Pa_AddNewProcess(name);
                    CCSLowerProc = strdup(name);
                    lowercase(CCSLowerProc);

                    CCSsortname = NULL;

                    free(name);
                  }
                  sort {
                    if (!CCSsortname) CCSsortname = strdup(CCSinputfile);
                    CCSSort = Pa_FindSort(CCSsortname);
                    if (CCSSort == -1) {
                      CCSSort = Pa_AddNewSort(CCSsortname);
                    }
                    pa_processTable[CCSProc].sort = CCSSort;
                    free(CCSsortname);
                  }
                  '='
                  procbody {

                    int i,j;
                    int state;
                    Est_String tmp;
                    Est_Boolean OK;

                    OK = TRUE;

                    if ($6.len == 1) {
                      pa_processTable[CCSProc].initial = $6.set[0];
                    } else {

                      for (i=0; i<$6.len; i++) {
                        tmp = strdup(pa_processTable[CCSProc].tableS[$6.set[i]].name);
                        if (!strchr(tmp,'<')) {
                          OK = FALSE;
                        }
                        free(tmp);
                      }

                      if (!OK) {
                        printf("\n  ERROR in CCS parser: the given usage of operator '+' is not supported, yet!\n");
                      }

                      for (i=0; i<$6.len; i++) {
                        Pa_DeleteStateProcess(&pa_processTable[CCSProc],$6.set[i]);
                      }

                      state = Pa_FOANextStateProcess(&pa_processTable[CCSProc],CCSLowerProc);
                      for (i=0; i<$6.len; i++) {
                        for(j=0; j<pa_processTable[CCSProc].numTransitions; j++) {
                          if (pa_processTable[CCSProc].tableT[j].source == $6.set[i]) {
                            pa_processTable[CCSProc].tableT[j].source = state;
                          }
                        }
                      }
                      pa_processTable[CCSProc].initial = state;
                    }

                    if (OK) {
                      if (!CCSquiet) printf("OK\n");
                    }

                    free($1);
                    free($6.set);
                    free(CCSLowerProc);
                  } ;

  onthefly      : ONTHEFLY {
                    CCSonthefly=TRUE;
                  }
                | {
                    CCSonthefly=FALSE;
                  };

  pprefix       : TRACE {
                    CCSptrace=TRUE;
                    CCSpweak=FALSE;
                  }

                | WEAK {
                    CCSptrace=FALSE;
                    CCSpweak=TRUE;
                  }

                | {
                    CCSptrace=FALSE;
                    CCSpweak=FALSE;
                  };

  cprefix       : RAW {
                    CCSraw=TRUE;
                    CCSfull=FALSE;
                    CCStrace=FALSE;
                    CCSweak=FALSE;
                    CCSstrong=FALSE;
                  }

                | FULL {
                    CCSraw=FALSE;
                    CCSfull=TRUE;
                    CCStrace=FALSE;
                    CCSweak=FALSE;
                    CCSstrong=FALSE;
                  }

                | TRACE {
                    CCSraw=FALSE;
                    CCSfull=FALSE;
                    CCStrace=TRUE;
                    CCSweak=FALSE;
                    CCSstrong=FALSE;
                  }

                | WEAK {
                    CCSraw=FALSE;
                    CCSfull=FALSE;
                    CCStrace=FALSE;
                    CCSweak=TRUE;
                    CCSstrong=FALSE;
                  }

                | STRONG {
                    CCSraw=FALSE;
                    CCSfull=FALSE;
                    CCStrace=FALSE;
                    CCSweak=FALSE;
                    CCSstrong=TRUE;
                  }

                | {
                    CCSraw=FALSE;
                    CCSfull=FALSE;
                    CCStrace=FALSE;
                    CCSweak=FALSE;
                    CCSstrong=FALSE;
                  } ;

  net           : NAME {

                    Est_String name;

                    /*
                    fprintf(stderr,"NET NAME %s\n",$1);
                    */

                    name = strdup($1);

                    if (CCSraw && !CCScircuit) {
                      printf("  Parallel composition %s ...",name);
                    }

                    if (!CCSraw && !CCScircuit) {
                      printf("  Net %s\n",name);
                      printf("    Composition ... ");
                    }

                    if (CCScircuit) {
                      printf("  Circuit %s\n",name);
                      printf("    Multi-way composition ... ");
                    }

                    CCSNump = 0;
                    CCSNuma = 0;
                    CCSPlist = NULL;
                    CCSAlist = NULL;

                    CCSsortname = NULL;

                    free(name);
                  }

                  sort {

                    Est_String name;

                    if (!CCSsortname) {
                      name = strdup($1);
                      CCSsortname = strdup(CCSinputfile);
                      concat(&CCSsortname,"-");
                      concat(&CCSsortname,name);
                      free(name);
                    }
                    CCSSort = Pa_FindSort(CCSsortname);
                    if (CCSSort == -1) {
                      CCSSort = Pa_AddNewSort(CCSsortname);
                    } else {
                      /* THIS WARNING IS NOT USABLE */
                      /* printf("\n    WARNING: two nets with the same sort!\n"); */
                    }
                    free(CCSsortname);

                  }

                  '=' compbody {

                    Est_String comp;
                    int n,m;
                    Bdd_Edge tau;

                    comp = strdup($1);

                    if (!pa_sortTable[CCSSort].encoded) {
                      Pa_EncodeSort(pa_sortTable[CCSSort].name);
                    }

                    /*
                    Pa_WriteSort(pa_sortTable[CCSSort].name);
                    */

                    Pa_EncodeMultiProcesses(CCSPlist);

                    Versis_Compose(comp,CCSCompType,CCSPlist,CCSAlist,CCSonthefly);
                    n = Pa_FindComposition(comp);
                    if (n != -1) {
                      pa_compositionTable[n].trace = CCStrace;
                      pa_compositionTable[n].weak = CCSweak;
                      pa_compositionTable[n].strong = CCSstrong;

                      if (!Bdd_isNull(pa_compositionTable[n].transitionBDD)) {

                        tau = pa_sortTable[CCSSort].table[0].p;

                        /* REPORT THE SIZE OF THE COMPOSITION */
                        /*
                        printf("(%ds, %dt, %dv) ",
                          Pa_DecodeCompStates(&pa_compositionTable[n],
                                              pa_compositionTable[n].stateBDD,FALSE),
                          Pa_DecodeCompTR(&pa_compositionTable[n],
                                              pa_compositionTable[n].transitionBDD,FALSE),
                          Pa_DecodeCompTR(&pa_compositionTable[n],
                             Bdd_ITE(tau,bdd_termFalse,
                                     pa_compositionTable[n].transitionBDD),FALSE));
                        */

                        printf("OK\n");
                        m = -1;

                        /* RETURN MINIMAL DETERMINISTIC TRACE-EQUIVALENT PROCESS INSTEAD OF COMPOSITION */
                        if (!CCSonthefly && CCStrace) {
                          printf("    Minimization ... ");
                          m = Versis_Minimization(3,1,comp);
                        }

                        /* RETURN MINIMAL WEAK-EQUIVALENT PROCESS INSTEAD OF COMPOSITION */
                        if (!CCSonthefly && CCSweak) {
                          printf("    Minimization ... ");
                          m = Versis_Minimization(1,1,comp);
                        }

                        /* RETURN MINIMAL STRONG-EQUIVALENT PROCESS INSTEAD OF COMPOSITION */
                        if (!CCSonthefly && CCSstrong) {
                          printf("    Minimization ... ");
                          m = Versis_Minimization(0,1,comp);
                        }

                        if (!CCSonthefly && (CCStrace || CCSweak || CCSstrong)) {

                          if (m!=-1) {

                            Pa_RenameProcess(pa_processTable[m].name,comp);

                            /* REPORT THE SIZE OF MINIMAL PROCESS */
                            printf("(%ds, %dt, %dv) ",
                              Pa_NumberStateProcess(&pa_processTable[m]),
                              Pa_DecodeProcessTR(&pa_processTable[m],pa_processTable[m].d,FALSE),
                              Pa_DecodeProcessTR(&pa_processTable[m],
                                Bdd_ITE(tau,bdd_termFalse,pa_processTable[m].d),FALSE)
                            );
                          }
                          printf("OK\n");
                        }

                        /* RETURN PROCESS INSTEAD OF COMPOSITION */
                        if (!CCSonthefly && CCSfull) {
                          printf("    Creating process %s ... ",comp);
                          Pa_Composition2Process(comp,TRUE);
                          printf("OK\n");
                        }

                        /* DO NOT DELETE COMPOSITION WHEN LOOKING FOR DIFFERENCE */
                        /**/
                        if (!CCSonthefly && !CCSraw) {
                          Pa_RemoveComposition(n);
                        }
                        /**/

                      } else {

                        if (!CCSonthefly) Pa_RemoveComposition(n);

                      }
                    }
                    free(comp);
                    free(CCSPlist);
                    free(CCSAlist);
                    free($1);
                  } ;

  sort          : '(' NAME ')'{
                    CCSsortname = strdup($2);
                  }

                | ;


  procbody      : NAME {

                    CCSNum = 0;

                  }

                  renlist {

                    int state;
                    Est_String name;

                    /*
                    fprintf(stderr,"procbody NAME == %s\n",$1);
                    */

                    if (CCSNum) {
                      printf("\n  ERROR in CCS parser: renaming list is supported only for nets, yet!\n");
                    }

                    name = strdup($1);
                    state = Pa_FOAGateProcess(&pa_processTable[CCSProc],name);

                    $$.set = NULL;
                    $$.len = 0;
                    addToSet(&$$.set,&$$.len,state);

                    free(name);
                    free($1);

                  }

                | procbody '+' procbody {

                    int i;

                    /*
                    fprintf(stderr,"PLUS\n");
                    */

                    $$.set = NULL;
                    $$.len = 0;
                    for (i=0; i<$1.len; i++) {
                      addToSet(&$$.set,&$$.len,($1.set)[i]);
                    }
                    for (i=0; i<$3.len; i++) {
                      addToSet(&$$.set,&$$.len,($3.set)[i]);
                    }

                    free($1.set);
                    free($3.set);
                  }

                | '(' procbody ')' {

                    int i,j;
                    int state;
                    Est_String tmp;
                    Est_Boolean OK;

                    /*
                    fprintf(stderr,"(procbody)\n");
                    */

                    OK = TRUE;

                    if ($2.len == 1) {
                      $$.set = $2.set;
                      $$.len = $2.len;
                    } else {

                      for (i=0; i<$2.len; i++) {
                        tmp = strdup(pa_processTable[CCSProc].tableS[$2.set[i]].name);
                        if (!strchr(tmp,'<')) {
                          OK = FALSE;
                        }
                        free(tmp);
                      }

                      if (!OK) {
                        printf("\n  ERROR in CCS parser: the given usage of operator '+' is not supported, yet!\n");
                      }

                      for (i=0; i<$2.len; i++) {
                        Pa_DeleteStateProcess(&pa_processTable[CCSProc],$2.set[i]);
                      }

                      state = Pa_FOANextStateProcess(&pa_processTable[CCSProc],CCSLowerProc);
                      for (i=0; i<$2.len; i++) {
                        for(j=0; j<pa_processTable[CCSProc].numTransitions; j++) {
                          if (pa_processTable[CCSProc].tableT[j].source == $2.set[i]) {
                            pa_processTable[CCSProc].tableT[j].source = state;
                          }
                        }
                      }
                      $$.set = NULL;
                      $$.len = 0;
                      addToSet(&$$.set,&$$.len,state);
                      free($2.set);
                    }

                  }

                | ACTION SEP procbody {

                    int state,len,act,type;
                    Est_String action;

                    /*
                    fprintf(stderr,"ACTION %s SEP procbody\n",$1);
                    */

                    type = 0; /* THIS IS TYPE FOR ACTION TAU */
                    action = strdup($1);

                    if ((action[0] == '?') || (action[0] == '!')) {

                      /* action with prefix */
                      if (action[0] == '?') {
                        type = 0;
                      } else
                      if (action[0] == '!') {
                        type = 1;
                      } else {
                        if (strcmp(action,"TAU"))
                          printf("ERROR in CCS parser: action %s without ? or !\n",action);
                      }

                      act = Pa_FOASortAction(&pa_sortTable[CCSSort],&action[1]);

                    } else {

                      /* action with suffix */
                      len = strlen(action);
                      if (action[len-1] == '?') {
                        type = 0;
                        action[len-1]='\0';
                      } else if (action[len-1] == '!') {
                        type = 1;
                        action[len-1]='\0';
                      }
                      act = Pa_FOASortAction(&pa_sortTable[CCSSort],action);
                    }

                    if ($3.len != 1) {
                      printf("ERROR in CCS parser: problem with operator '+'\n");
                    }

                    state = Pa_FOANextStateProcess(&pa_processTable[CCSProc],CCSLowerProc);
                    Pa_FOATransition(&pa_processTable[CCSProc],state,act,type,($3.set)[0]);

                    $$.set = NULL;
                    $$.len = 0;
                    addToSet(&$$.set,&$$.len,state);

                    /*
                    writeSet($$.set,$$.len);
                    */

                    free($3.set);
                    free(action);
                    free($1);
                  }

                | '(' tracelist ')' SEP procbody {

                    int i,j;
                    int act,type,state1,state2;
                    int *set;
                    int len;

                    /*
                    fprintf(stderr,"(tracelist len=%d) SEP procbody\n",$2.len);
                    */

                    if ($5.len != 1) {
                      printf("\n  ERROR in CCS parser: the given usage of operator '+' is not supported, yet!\n");
                    }

                    set=NULL;
                    len=0;
                    for (i=0; i<$2.len; i++) {

                      /* DEBUGING */
                      /*
                      fprintf(stderr,"FOR LOOP i=%d, set[i].len=%d\n",i,$2.set[i].len);
                      */

                      state1 = -1;
                      state2 = $5.set[0];
                      for (j=0; j<$2.set[i].len; j++) {

                        act = $2.set[i].set[j].act;
                        type = $2.set[i].set[j].type;

                        /* DEBUGING */
                        /*
                        fprintf(stderr,"%s\n",pa_sortTable[CCSSort].table[act].name);
                        */

                        state1 = Pa_FOANextStateProcess(&pa_processTable[CCSProc],CCSLowerProc);
                        Pa_FOATransition(&pa_processTable[CCSProc],state1,act,type,state2);
                        state2 = state1;
                      }

                      addToSet(&set,&len,state1);
                      free($2.set[i].set);
                    }

                    for (i=0; i<len; i++) {
                      Pa_DeleteStateProcess(&pa_processTable[CCSProc],set[i]);
                    }

                    state1 = Pa_FOANextStateProcess(&pa_processTable[CCSProc],CCSLowerProc);
                    for (i=0; i<len; i++) {
                      for(j=0; j<pa_processTable[CCSProc].numTransitions; j++) {
                        if (pa_processTable[CCSProc].tableT[j].source == set[i]) {
                          pa_processTable[CCSProc].tableT[j].source = state1;
                        }
                      }
                    }

                    $$.set = NULL;
                    $$.len = 0;
                    addToSet(&$$.set,&$$.len,state1);

                    free($2.set);

                  } ;

  tracelist     : '(' tracelist ')' SEP onetrace {

                    /*
                    fprintf(stderr,"(tracelist len=%d) SEP onetrace len=%d\n",$2.len,$5.len);
                    */

                    $$.set = $5.set;
                    $$.len = $5.len;

                    concatTraces(&$$.set,&$$.len,$2.set,$2.len);

                  }

                | '(' tracelist ')' SEP onetrace '+' tracelist {

                    /*
                    fprintf(stderr,"(tracelist len=%d) SEP onetrace len=%d + tracelist len=%d\n",$2.len,$5.len,$7.len);
                    */

                    $$.set = $5.set;
                    $$.len = $5.len;

                    concatTraces(&$$.set,&$$.len,$2.set,$2.len);
                    joinTraces(&$$.set,&$$.len,$7.set,$7.len);

                  }

                | onetrace '+' tracelist {

                    /*
                    fprintf(stderr,"onetrace len=%d + tracelist len=%d\n",$1.len,$3.len);
                    */

                    if ($1.len != 1) {
                      printf("ERROR in CCS parser: problem with operator '+'\n");
                    }

                    $$.set = $3.set;
                    $$.len = $3.len;
                    joinTraces(&$$.set,&$$.len,$1.set,$1.len);

                  }

                | onetrace {

                    /*
                    fprintf(stderr,"onetrace len=%d\n",$1.len);
                    */

                    $$.set = NULL;
                    $$.len = 0;
                    joinTraces(&$$.set,&$$.len,$1.set,$1.len);

                  } ;

  onetrace      : '(' tracelist ')' {

                    /*
                    fprintf(stderr,"(tracelist len=%d)\n",$2.len);
                    */

                    $$.set = $2.set;
                    $$.len = $2.len;

                  }

                | ACTION SEP onetrace {

                    int act,type,len;
                    Est_String action;

                    /*
                    fprintf(stderr,"ACTION %s SEP onetrace len=%d\n",$1,$3.len);
                    */

                    type = 0; /* THIS IS TYPE FOR ACTION TAU */
                    action = strdup($1);

                    if ((action[0] == '?') || (action[0] == '!')) {

                      /* action with prefix */
                      if (action[0] == '?') {
                        type = 0;
                      } else
                      if (action[0] == '!') {
                        type = 1;
                      } else {
                        if (strcmp(action,"TAU"))
                          printf("ERROR in CCS parser: action %s without ? or !\n",action);
                      }
                      act = Pa_FOASortAction(&pa_sortTable[CCSSort],&action[1]);

                    } else {

                      /* action with suffix */
                      len = strlen(action);
                      if (action[len-1] == '?') {
                        type = 0;
                        action[len-1]='\0';
                      } else if (action[len-1] == '!') {
                        type = 1;
                        action[len-1]='\0';
                      }
                      act = Pa_FOASortAction(&pa_sortTable[CCSSort],action);

                    }

                    $$.set = $3.set;
                    $$.len = $3.len;
                    extendTraces($$.set,$$.len,act,type);

                    free(action);
                    free($1);
                  }

                | ACTION {

                    int act,type,len;
                    Est_String action;
                    actionTrace *trace;

                    /*
                    fprintf(stderr,"ACTION %s\n",$1);
                    */

                    type = 0; /* THIS IS TYPE FOR ACTION TAU */
                    action = strdup($1);

                    if ((action[0] == '?') || (action[0] == '!')) {

                      /* action with prefix */
                      if (action[0] == '?') {
                        type = 0;
                      } else
                      if (action[0] == '!') {
                        type = 1;
                      } else {
                        if (strcmp(action,"TAU"))
                          printf("ERROR in CCS parser: action %s without ? or !\n",action);
                      }

                      act = Pa_FOASortAction(&pa_sortTable[CCSSort],&action[1]);

                    } else {

                      /* action with suffix */
                      len = strlen(action);
                      if (action[len-1] == '?') {
                        type = 0;
                        action[len-1]='\0';
                      } else if (action[len-1] == '!') {
                        type = 1;
                        action[len-1]='\0';
                      }
                      act = Pa_FOASortAction(&pa_sortTable[CCSSort],action);
                    }

                    trace = (actionTrace *) malloc (sizeof(actionTrace));
                    trace->set = NULL;
                    trace->len = 0;
                    extendTrace(&trace->set,&trace->len,act,type);

                    $$.set = NULL;
                    $$.len = 0;
                    addToTracelist(&$$.set,&$$.len,*trace);

                    free(action);
                    free($1);
                  } ;

  compbody      : COMPOSE '(' proclist ')' restrlist {

                    /* actions not in restrlist go alone and synchronised */
                    /* actions in restrlist go synchronised, only */
                    /* action tau goes alone */

                    /*
                    fprintf(stderr,"COMPOSE:\n");
                    fprintf(stderr,"(nump = %d) %s\n",CCSNump,CCSPlist);
                    */

                    CCSCompType = 0;
                  }


                | MULTIWAY '(' proclist ')' restrlist {

                    /* this is a multi-way composition */
                    /* actions not in restrlist go alone and synchronised */
                    /* actions in restrlist go synchronised, only */
                    /* action tau goes alone */
                    /* when composing circuits use fundamental-mode normalization */

                    /*
                    fprintf(stderr,"COMPOSE:\n");
                    fprintf(stderr,"(nump = %d) %s\n",CCSNump,CCSPlist);
                    */

                    if (CCScircuit) {
                      CCSCompType = 6;
                    } else {
                      CCSCompType = 3;
                    }
                  }

                | '(' oneproc COMPOSE composein ')' restrlist {

                    /* actions not in restrlist go alone and synchronised */
                    /* actions in restrlist go synchronised, only */
                    /* action tau goes alone */

                    /*
                    fprintf(stderr,"COMPOSE:\n");
                    fprintf(stderr,"(nump = %d) %s\n",CCSNump,CCSPlist);
                    */

                    CCSCompType = 0;
                  }

                | oneproc STARTPARTIAL actionlist ENDPARTIAL oneproc {

                    /* actions not in actionlist go alone, only */
                    /* actions in actionlist go synchronised, only */
                    /* action tau goes alone */

                    /*
                    fprintf(stderr,"PARTIAL COMPOSITION:\n");
                    fprintf(stderr,"(nump = %d) %s\n",CCSNump,CCSPlist);
                    fprintf(stderr,"(nump = %d) %s\n",CCSNump,CCSAlist);
                    */

                    CCSCompType = 2;
                  }

                | INTERLEAVE '(' proclist ')' {

                    /* all actions go alone, only */

                    /*
                    fprintf(stderr,"INTERLEAVE:\n");
                    fprintf(stderr,"(nump = %d) %s\n",CCSNump,CCSPlist);
                    */

                    CCSCompType = 2;

                  }

                | '(' oneproc INTERLEAVE interleavein ')' {

                    /* all actions go alone, only */

                    /*
                    fprintf(stderr,"INTERLEAVE:\n");
                    fprintf(stderr,"(nump = %d) %s\n",CCSNump,CCSPlist);
                    */

                    CCSCompType = 2;

                  }

                | SYNCHRONOUS '(' proclist ')' {

                    /* action tau goes alone */
                    /* all other actions go synchronised, only */

                    /*
                    fprintf(stderr,"SYNCHRONOUS:\n");
                    fprintf(stderr,"(nump = %d) %s\n",CCSNump,CCSPlist);
                    */

                    CCSCompType = 1;

                  }

                | '(' oneproc SYNCHRONOUS synchronousin ')' {

                    /* action tau goes alone */
                    /* all other actions go synchronised, only */

                    /*
                    fprintf(stderr,"SYNCHRONOUS:\n");
                    fprintf(stderr,"(nump = %d) %s\n",CCSNump,CCSPlist);
                    */

                    CCSCompType = 1;

                  } ;

  composein     : oneproc COMPOSE composein
                | oneproc ;

  interleavein  : oneproc INTERLEAVE interleavein
                | oneproc ;

  synchronousin : oneproc SYNCHRONOUS synchronousin
                | oneproc ;

  actionlist    : oneaction ',' moreactions
                | oneaction
                | ;

  moreactions   : moreactions ',' oneaction
                | oneaction ;

  oneaction    : NAME {
                    Est_String name;
                    Est_String tmp;

                    /*
                    fprintf(stderr,"NAME %s\n",$1);
                    */

                    name = strdup($1);
                    Pa_FOASortAction(&pa_sortTable[CCSSort],name);

                    CCSNuma++;
                    if (!CCSAlist) {
                      CCSAlist = strdup(name);
                    } else {
                      tmp = (Est_String) malloc(65536);
                      sprintf(tmp,"%s %s",CCSAlist,name);
                      free(CCSAlist);
                      CCSAlist = strdup(tmp);
                      free(tmp);
                    }

                    free(name);
                    free($1);
                  } ;

  proclist      : proclist ',' oneproc
                | oneproc ;

  oneproc       : pprefix NAME {
                    /*
                    fprintf(stderr,"NAME %s\n",$2);
                    */

                    CCSNum = 0;
                    CCSOld = NULL;
                    CCSNew = NULL;

                  } renlist {

                    Est_String name,newproc;
                    Est_String tmp;
                    int i;

                    name = strdup($2);

                    i = 0;
                    newproc = NULL;
                    do {
                      i++;
                      if (newproc) free(newproc);
                      newproc = (Est_String) malloc(65535);
                      sprintf(newproc,"%s#%d",name,i);
                    } while (Pa_FindProcess(newproc) != -1);

                    CCSNump++;
                    if (!CCSPlist) {
                      CCSPlist = strdup(newproc);
                    } else {
                      tmp = (Est_String) malloc(65535);
                      sprintf(tmp,"%s %s",CCSPlist,newproc);
                      free(CCSPlist);
                      CCSPlist = strdup(tmp);
                      free(tmp);
                    }

                    /*
                    fprintf(stderr,"Renaming old = [%s]\n",CCSOld);
                    fprintf(stderr,"Renaming new = [%s]\n",CCSNew);
                    */

                    if (Pa_FindProcess(name) == -1) {
                      printf("\n    WARNING: Added empty process %s ...",name);
                      i = Pa_AddNewProcess(newproc); /* ADD AN EMPTY PROCESS */
                      Pa_FOAStateProcess(&pa_processTable[i],name); /* INITIAL STATE */
                      pa_processTable[i].initial = 0;
                      pa_processTable[i].sort = CCSSort;
                    } else {
                      i = Pa_CopyProcess(name,newproc,pa_sortTable[CCSSort].name,CCSOld,CCSNew);
                    }

                    if (i == -1) {
                      printf("    ERROR in CCS parser: unsupported format, probably problem with sort\n");
                    } else {
                      pa_processTable[i].trace = CCSptrace;
                      pa_processTable[i].weak = CCSpweak;
                    }

                    free(name);
                    free(newproc);
                    free(CCSOld);
                    free(CCSNew);
                    free($2);
                  } ;

  renlist       : renlist '[' renaction ']'
                | ;

  renaction     : NAME '/' NAME {

                    Est_String name1,name2;
                    Est_String tmp;

                    name1 = strdup($1);
                    name2 = strdup($3);

                    CCSNum++;

                    Pa_FOASortAction(&pa_sortTable[CCSSort],name1);
                    if (!CCSNew) {
                      CCSNew = strdup(name1);
                    } else {
                      tmp = (Est_String) malloc(65536);
                      sprintf(tmp,"%s %s",CCSNew,name1);
                      free(CCSNew);
                      CCSNew = strdup(tmp);
                      free(tmp);
                    }

                    Pa_FOASortAction(&pa_sortTable[CCSSort],name2);
                    if (!CCSOld) {
                      CCSOld = strdup(name2);
                    } else {
                      tmp = (Est_String) malloc(65536);
                      sprintf(tmp,"%s %s",CCSOld,name2);
                      free(CCSOld);
                      CCSOld = strdup(tmp);
                      free(tmp);
                    }

                    free(name1);
                    free(name2);

                    free($1);
                    free($3);
                  }

                | ACTION '/' NAME {

                    Est_String name1,name2;
                    Est_String tmp;

                    name1 = strdup($1);
                    name2 = strdup($3);

                    if (strcmp(name1,"TAU")) {
                      printf("ERROR in CCS parser: do not use !? in renaming pairs\n");
                    } else {

                      CCSNum++;

                      if (!CCSNew) {
                        CCSNew = strdup(name1);
                      } else {
                        tmp = (Est_String) malloc(65536);
                        sprintf(tmp,"%s %s",CCSNew,name1);
                        free(CCSNew);
                        CCSNew = strdup(tmp);
                        free(tmp);
                      }

                      Pa_FOASortAction(&pa_sortTable[CCSSort],name2);
                      if (!CCSOld) {
                        CCSOld = strdup(name2);
                      } else {
                        tmp = (Est_String) malloc(65536);
                        sprintf(tmp,"%s %s",CCSOld,name2);
                        free(CCSOld);
                        CCSOld = strdup(tmp);
                        free(tmp);
                      }

                    }

                    free(name1);
                    free(name2);

                    free($1);
                    free($3);
                  }

                | NAME '/' ACTION {

                    Est_String name2;

                    name2 = strdup($3);

                    if (strcmp(name2,"TAU")) {
                      printf("ERROR in CCS parser: do not use !? in renaming pairs\n");
                    } else {
                      printf("ERROR in CCS parser: cannot rename action TAU\n");
                    }

                    free(name2);
                    free($1);
                    free($3);
                  }

                | ACTION '/' ACTION {

                    printf("ERROR in CCS parser: do not use !? in renaming pairs\n");

                    free($1);
                    free($3);

                  } ;

  restrlist     : restrlist restraction
                | ;

  restraction   : '\\' NAME {

                    Est_String name;
                    Est_String tmp;

                    /*
                    fprintf(stderr,"NAME %s\n",$2);
                    */

                    name = strdup($2);
                    Pa_FOASortAction(&pa_sortTable[CCSSort],name);

                    CCSNuma++;
                    if (!CCSAlist) {
                      CCSAlist = strdup(name);
                    } else {
                      tmp = (Est_String) malloc(65536);
                      sprintf(tmp,"%s %s",CCSAlist,name);
                      free(CCSAlist);
                      CCSAlist = strdup(tmp);
                      free(tmp);
                    }

                    free(name);
                    free($2);
                  };

%%

#include <lex.ccs.c>

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

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

int
Ccs_ParseCCS(Est_String f, Est_Boolean q)
{
  YY_BUFFER_STATE buffer;

  printf("\n");

  yyin = fopen(f,"r");
  if (yyin != NULL) {
    CCSinputfile=strdup(f);
    CCSquiet = q;

    buffer = yy_create_buffer(yyin,YY_BUF_SIZE);
    yy_switch_to_buffer(buffer);
    yyparse();
    yy_delete_buffer(buffer);

    free(CCSinputfile);
    fclose(yyin);
  } else {
    printf("\n  ERROR: I can not open file %s.\n",f);
  }
  return 0;
}

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

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

static void
concat(Est_String *s1, const Est_String s2)
{
   *s1 = (char*) realloc(*s1,strlen(*s1)+strlen(s2)+1);
   strcat(*s1,s2);
}

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

static void
outline(char *s)
{
  if (strcmp(s,"")) printf("%s",&s[1]);
  printf("\n");
}

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

static void
lowercase(char *s)
{
   int  i = 0;

   while ( s[i] )
   {
      s[i] = tolower(s[i]);
      i++;
   }

   return;
}

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

static void
addToSet(int **set, int *len, int state)
{
  if (!*set) {
    *set = (int *) malloc (sizeof(int));
    (*set)[0] = state;
    *len = 1;
  } else {
    (*len)++;
    *set = (int *) realloc (*set, (*len) * sizeof(int));
    (*set)[(*len) - 1] = state;
  }
}

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

static void
addToTracelist(actionTrace **set, int *len, actionTrace trace)
{
  if (!*set) {
    *set = (actionTrace *) malloc (sizeof(actionTrace));
    (*set)[0] = trace;
    *len = 1;
  } else {
    (*len)++;
    *set = (actionTrace *) realloc (*set, (*len) * sizeof(actionTrace));
    (*set)[(*len) - 1] = trace;
  }
}

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

static void
extendTrace(typedAction **set, int *len, int act, int type)
{
  if (!*set) {
    *set = (typedAction *) malloc (sizeof(typedAction));
    (*set)[0].act = act;
    (*set)[0].type = type;
    *len = 1;
  } else {
    (*len)++;
    *set = (typedAction *) realloc (*set, (*len) * sizeof(typedAction));
    (*set)[(*len) - 1].act = act;
    (*set)[(*len) - 1].type = type;
  }
}

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

static void
extendTraces(actionTrace *set, int len, int act, int type)
{
  int i;

  if (!set) {
   fprintf(stderr,"\n  ERROR in extendTraces!\n");
  } else {

    /*
    fprintf(stderr,"BEFORE EXTEND:\n");
    writeTraceSet(set,len);
    */

    for (i=0; i<len; i++) {
      extendTrace(&set[i].set,&set[i].len,act,type);
    }

    /*
    fprintf(stderr,"AFTER EXTEND:\n");
    writeTraceSet(set,len);
    */

  }
}

/**Function****************************************************************
  Synopsis    []
  Description [Join two sets of traces.]
  SideEffects [(a+b).c + (a+b).d = a.c + b.c + a.d + b.d]
  SeeAlso     []
  ************************************************************************/

static void
joinTraces(actionTrace **set, int *len, actionTrace *set1, int len1)
{
  int i;

  if (!*set) {
    *set = (actionTrace *) malloc (len1 * sizeof(actionTrace));
  } else {
    *set = (actionTrace *) realloc (*set, ((*len) + len1) * sizeof(actionTrace));
  }

  for (i=0; i<len1; i++) {
    (*len)++;
    (*set)[(*len) - 1] = set1[i];
  }
}

/**Function****************************************************************
  Synopsis    []
  Description [Add traces in the second set to the traces in the first set.]
  SideEffects [(a+b)(c+d) = a.c + a.d + b.c + b.d]
  SeeAlso     []
  ************************************************************************/

static void
concatTraces(actionTrace **set, int *len, actionTrace *set1, int len1)
{
  int i,j,k;

  if (!*set) {
   fprintf(stderr,"\n  ERROR in concatTraces!\n");
  } else {

    /*
    fprintf(stderr,"CONCAT LEN = %d, LEN1 = %d\n",*len,len1);
    */

    *set = (actionTrace *) realloc (*set, ((*len) * len1) * sizeof(actionTrace));

    /* MAKE len1 COPIES OF ACTION-TRACES IN set */
    for (i=1; i<len1; i++) {
      for (j=0; j<(*len); j++) {
        (*set)[i*(*len)+j].set = NULL;
        (*set)[i*(*len)+j].len = 0;
        for (k=0; k<(*set)[j].len; k++) {
          extendTrace(&(*set)[i*(*len)+j].set,&(*set)[i*(*len)+j].len,(*set)[j].set[k].act,(*set)[j].set[k].type);
        }
      }
    }

    /* CONCAT ACTION-TRACES IN set WITH ACTION-TRACES IN set1 */
    for (i=0; i<(*len); i++) {
      for (j=0; j<len1; j++) {

        /*
        fprintf(stderr,"BEFORE CONCAT i= %d, j = %d:\n",i,j);
        writeTraceSet((*set),(*len));
        */

        for (k=0; k<set1[j].len; k++) {
          extendTrace(&(*set)[j*(*len)+i].set,&(*set)[j*(*len)+i].len,set1[j].set[k].act,set1[j].set[k].type);
        }

        /*
        fprintf(stderr,"AFTER CONCAT:\n");
        writeTraceSet((*set),(*len));
        */

      }
    }

    (*len) = (*len) * len1;
  }
}

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

static void
writeSet(int *set, int len)
{
  int i;

  fprintf(stderr,"SET:");
  for (i=0; i<len; i++) {
    fprintf(stderr," %d",set[i]);
  }
  fprintf(stderr,"\n");
}

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

static void
writeTraceSet(actionTrace *set, int len)
{
  int i,j;

  fprintf(stderr,"TRACE SET:\n");
  for (i=0; i<len; i++) {
    fprintf(stderr,"+");
    for (j=0; j<set[i].len; j++) {
      fprintf(stderr,"(act=%d, type=%d)",set[i].set[j].act,set[i].set[j].type);
    }
    fprintf(stderr,"\n");
  }
}

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

static int
error(const char *s)
{
  printf("\n  ERROR: ");
  if (strstr(s,"parse error, unexpected UNKNOWN")) {
     printf("unknown or badly placed symbol '%s'\n",ccstext);
     printf("%s",s);
  } else
  if (!strcmp(s,"parse error, unexpected UNKNOWN, expecting ACTION")) {
     printf("unknown or badly placed symbol '%s'\n",ccstext);
     printf("%s",s);
  } else
  if (!strcmp(s,"parse error, unexpected NAME, expecting ACTION")) {
     printf("incorrect action name '%s', missing ! or ?\n",ccstext);
     printf("%s",s);
  } else
  if (!strcmp(s,"parse error, unexpected ACTION, expecting NAME")) {
     printf("incorrect process name '%s'\n",ccstext);
     printf("%s",s);
  } else {
    printf("%s",s);
  }
  printf("\n");
  return 1;
}

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

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

int
yywrap()
{
  return 1;
}

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

int
yyerror(const char *s)
{
  error(s);
  return 1;
}
