/**CFile*******************************************************************
  PackageName [versis]
  Synopsis    [Package 'versis' provides basic tools for formal
               verification of concurrent systems]

  FileName    [versisComp.c]
  Revision    [$Revision: 76 $]
  Date        [$Date: 2013-04-26 14:26:09 +0200 (pet, 26 apr 2013) $]
  Authors     [Robert Meolic (meolic@uni-mb.si),
               Mirjam Sepesy Maucec (mirjam.sepesy@uni-mb.si),
               Tatjana Kapus (kapus@uni-mb.si)]
  Description [File versisComp.c provides parallel composition.]
  SeeAlso     [versis.h, versisInt.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 "versisInt.h"

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

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

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

static void Compose(Pa_Composition *c);

static int ComposeStep(Pa_Composition *c, int N);

static int wordNumber(Est_String s);

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

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

/**Function****************************************************************
  Synopsis    [Versis_Compose]
  Description [0 - CCS compose general (using restricted actions),
               1 - CCS compose with non-restricted actions,
               2 - CCS compose with restricted actions,
               3 - multi-way general (using restricted actions),
               4 - multi-way with non-restricted actions,
               5 - multi-way with restricted actions,
               6 - fundamental-mode multi-way general (using restr. act.),
               7 - fundamental-mode multi-way with non-restricted actions,
               8 - fundamental-mode multi-way with restricted actions

               general (0) = given actions sync others sync and non-sync
               non-restricted actions (1) = they and tau non-sync, others sync
               restricted actions (2) = they sync, others non-sync
               multi-way = more than two processes can synchronise
               fundamental-mode = delete inputs if there is an output

               CCS COMPOSITION: type = 0, actions = given
               LOTOS SYNCHRONISING (only tau goes alone): type = 1, actions = NULL
               LOTOS INTERLEAVING (all actions go alone, only): type = 2, actions = NULL
              ]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

void
Versis_Compose(Est_String name, int type, Est_String process,
               Est_String actions, Est_Boolean onthefly)
{
  int i,j,k,n,m;
  int numP,numA,numcomp;
  int token;
  Pa_Composition *c;
  Pa_Process *p,*cp;
  Est_String sup,sup_next;
  Est_String s;
  Bdd_Edge tau;
  Bdd_Edge sup1,sup2,supinout;
  Est_Boolean minimize;

  /*
  fprintf(stderr,"Compose: <%s>\n",name);
  fprintf(stderr,"Processes: <%s>\n",process);
  fprintf(stderr,"Actions: <%s>\n",actions);
  */

  numP = wordNumber(process);
  numA = wordNumber(actions);

  if ( numP < 1) {
    printf(" ERROR: there are no processes to compose.\n");
    return;
  }

  if ( onthefly && (numP == 1)) {
    printf(" ERROR: on-the-fly composition of single process.\n");
    return;
  }

  if ((type < 3) && (numP == 1)) {
    printf(" ERROR: only multi-way composition (///) allows single process.\n");
    return;
  }

  i = pa_compositions;

  numcomp = Pa_AddNewComposition(name,type,numP,numA);

  if (pa_compositions == i) {
    printf(" (composition overwritten) ");
  }
  c = &pa_compositionTable[numcomp];

  /* PROCESSES */

  token = strspn(process," \t");
  sup = (Est_String) strdup(&process[token]);

  token = strcspn(sup," \t");
  s = (Est_String) malloc(token+1);
  strncpy(s,sup,token); /* name of first process */
  s[token] = '\0';

  i = Pa_FindProcess(s);
  free(s);

  if (i == -1) {
    Pa_RemoveComposition(numcomp);
    printf(" ERROR: First process must exist.\n");
    return;
  }

  if (!pa_processTable[i].encoded) {
    Pa_EncodeProcess(pa_processTable[i].name);
  }

  c->tableP[0] = i; /* number of the first process */
  c->sort = pa_processTable[i].sort;
  tau = pa_sortTable[c->sort].table[0].p;

  if ( numP > 1) {

    k = 1;
    while (k < numP) {
      while ((sup[token] == ' ') || (sup[token] == '\t')) token = token + 1;
      sup_next = (Est_String) strdup(&sup[token]);
      free(sup);
      sup = sup_next;

      token = strcspn(sup," \t");
      s = (Est_String) malloc(token+1);
      strncpy(s,sup,token); /* name of next process */
      s[token] = '\0';

      i = Pa_FindProcess(s);
      if (i == -1) {
        printf(" WARNING: Process %s does not exist ...",s);
        i = Pa_AddNewProcess(s); /* ADD AN EMPTY PROCESS */
        Pa_FOAStateProcess(&pa_processTable[i],name); /* INITIAL STATE */
        pa_processTable[i].initial = 0;
        pa_processTable[i].sort = c->sort;
      }
      free(s);

      if (c->sort != pa_processTable[i].sort) {
        Pa_RemoveComposition(numcomp);
        printf(" ERROR: Processes have different sorts!\n");
        return;
      }

      if (!pa_processTable[i].encoded) {
        Pa_EncodeProcess(pa_processTable[i].name);
      }

      c->tableP[k++] = i; /* CAREFULLY IF NEW PROCESSES ARE NOT ADDED AT THE END */

    }
    free(sup);

  }

  /* DO MINIMIZATION OF PROCESSES IF REQUIRED */

  minimize = FALSE;
  for(i=0; i<numP; i++) {

    if (pa_processTable[c->tableP[i]].trace || pa_processTable[c->tableP[i]].weak) {

      if (!minimize) {
         printf("\n");
         minimize = TRUE;
      }

      printf("      minimization of process %s ... ",pa_processTable[c->tableP[i]].name);

      m = -1;

      /* RETURN MINIMAL WEAK-EQUIVALENT PROCESS INSTEAD OF ORIGINAL ONE */
      if (pa_processTable[c->tableP[i]].weak) {
        m = Versis_Minimization(1,0,pa_processTable[c->tableP[i]].name);
      }

      /* RETURN MINIMAL DETERMINISTIC TRACE-EQUIVALENT PROCESS INSTEAD OF ORIGINAL ONE */
      if (pa_processTable[c->tableP[i]].trace) {
        m = Versis_Minimization(3,0,pa_processTable[c->tableP[i]].name);
      }

      if (m!=-1) {

        /* REPORT THE SIZE OF ORIGINAL PROCESS */
        printf("(%ds, %dt, %dv) -> ",
        Pa_NumberStateProcess(&pa_processTable[c->tableP[i]]),
        Pa_DecodeProcessTR(&pa_processTable[c->tableP[i]],pa_processTable[c->tableP[i]].d,FALSE),
        Pa_DecodeProcessTR(&pa_processTable[c->tableP[i]],
          Bdd_ITE(tau,bdd_termFalse,pa_processTable[c->tableP[i]].d),FALSE)
        );

        sup = strdup(pa_processTable[c->tableP[i]].name);
        Pa_DeleteProcess(c->tableP[i]);
        Pa_RenameProcess(pa_processTable[m].name,sup);
        free(sup);
        c->tableP[i] = m;

        /* 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");
    }
  }

  if (minimize) {
       printf("      calculating composition ... ");
  }

  /* ACTIONS */

  if ( numA ) {

    token = strspn(actions," \t");
    sup = (Est_String) strdup(&actions[token]);

    token = strcspn(sup," \t");
    s = (Est_String) malloc(token+1);
    strncpy(s,sup,token); /* name of first action */
    s[token] = '\0';

    i = Pa_FindSortAction(&pa_sortTable[c->sort],s);
    free(s);

    if (i == -1) {
      Pa_RemoveComposition(numcomp);
      printf("    ERROR (composition): Action %%%d does not exist.\n",1);
      return;
    }

    c->tableA[0] = i; /* number of first action */

    k = 1;
    while (k < numA) {
      while ((sup[token] == ' ') || (sup[token] == '\t')) token = token + 1;
      sup_next = (Est_String) strdup(&sup[token]);
      free(sup);
      sup = sup_next;

      token = strcspn(sup," \t");
      s = (Est_String) malloc(token+1);
      strncpy(s,sup,token); /* name of next action */
      s[token] = '\0';

      i = Pa_FindSortAction(&pa_sortTable[c->sort],s);
      free(s);

      if (i == -1) {
        Pa_RemoveComposition(numcomp);
        printf("    ERROR (composition): Action %%%d does not exist.\n",k+1);
        return;
      }
      c->tableA[k++] = i;
    }
    free(sup);
  }

  /* CIRCUITS ONLY */
  /* REMOVE HAZARDS TO GET MORE USEFUL RESULTS FROM THE COMPOSITION */
  if ((numP > 1) && ((type == 6) || (type == 7) || (type == 8))) {
    for(i=0; i<numP; i++) {
      sup1 = Bdd_RelOp(pa_processTable[c->tableP[i]].d,Bdd_NOT(pa_sortTable[c->sort].a0),"#AND Ex xA xS",TRUE); /*?*/
      sup2 = Bdd_RelOp(pa_processTable[c->tableP[i]].d,pa_sortTable[c->sort].a0,"#AND Ex xA xS",TRUE); /*!*/

      supinout = Bdd_ITE(sup1,sup2,bdd_termFalse);
      if (!Bdd_isEqv(supinout,bdd_termFalse)) {
        p = &pa_processTable[c->tableP[i]];
        printf("\n    WARNING: Circuit %s has hazards!",p->name);

        if (!Bdd_isEqv(Bdd_ITE(p->tableS[p->initial].bddR,supinout,bdd_termFalse),bdd_termFalse)) {
          printf("\n    ERROR: Hazards in initial state are not supported!");
        }

        sup = strdup(p->name);
        j = strlen(sup);
        sup = (Est_String) realloc(sup,j+2);
        sup[j]='H';
        sup[j+1]=0;
        k = Pa_CopyProcess(p->name,sup,NULL,NULL,NULL);
        free(sup);

        p = &pa_processTable[c->tableP[i]]; /* Pa_CopyProcess reallocate process table */
        cp = &pa_processTable[k];
        c->tableP[i] = k;

        for (j=0; j<p->numStates; j++) {
          sup1 = Bdd_ITE(p->tableS[j].bddR,supinout,bdd_termFalse);
          if (!Bdd_isEqv(sup1,bdd_termFalse)) {
            n = strcspn(p->tableS[j].name,"<");
            sup = (Est_String) malloc(n+3);
            memcpy(sup,p->tableS[j].name,n);
            sup[n]='#';
            sup[n+1]='H';
            sup[n+2]=0;
            n = Pa_FOAStateProcess(cp,sup);
            free(sup);

            for (k=0; k<p->numTransitions; k++) {
              if ((p->tableT[k].type == 0) && (p->tableT[k].source == j)) {
                Pa_FOATransition(cp,n,p->tableT[k].action,0,p->tableT[k].dest);
                if (p->tableT[k].dest == j) {
                  Pa_FOATransition(cp,n,p->tableT[k].action,0,n);
                }
              }
              if (p->tableT[k].dest == j) {
                Pa_FOATransition(cp,p->tableT[k].source,p->tableT[k].action,p->tableT[k].type,n);
              }

            }
          }
        }

        for (j=0; j<p->numStates; j++) {
          sup1 = Bdd_ITE(p->tableS[j].bddR,supinout,bdd_termFalse);
          if (!Bdd_isEqv(sup1,bdd_termFalse)) {
            for (k=p->numTransitions; k<cp->numTransitions; k++) {
              if (cp->tableT[k].dest == j) {
                n = strcspn(p->tableS[j].name,"<");
                sup = (Est_String) malloc(n+3);
                memcpy(sup,p->tableS[j].name,n);
                sup[n]='#';
                sup[n+1]='H';
                sup[n+2]=0;
                n = Pa_FOAStateProcess(cp,sup);
                free(sup);

                Pa_FOATransition(cp,cp->tableT[k].source,cp->tableT[k].action,cp->tableT[k].type,n);
              }
            }
          }
        }

        Pa_EncodeProcess(pa_processTable[c->tableP[i]].name);
        printf("\n    WARNING: Replaced with process %s ...",pa_processTable[c->tableP[i]].name);
      }
    }
  }

  /* COLLECT INFORMATION ABOUT ALPHABET OF PROCESSES */

  c->alphabet = (Bdd_Edge *) calloc (numP,sizeof(Bdd_Edge));
  for(k=0; k<numP; k++) {
    sup1 = pa_processTable[c->tableP[k]].d;
    sup1 = Bdd_E(sup1,Bdd_GetVariable(pa_sortTable[c->sort].a0));
    c->alphabet[k] = Bdd_RelOpSimple(sup1,"Ex xR xS",TRUE);
    Bdd_Fortify(c->alphabet[k]);
  }

  /* CREATE SUPPLEMENTAL STRUCTURES */

  c->di = (Bdd_Edge *) calloc (numP,sizeof(Bdd_Edge));
  c->dij = (Bdd_Edge *) calloc (numP*numP,sizeof(Bdd_Edge));

  /* WITH REGARD TO THE TYPE OF COMPOSITION CALCULATE:                 */
  /* 0 OR 3 OR 6 - actionsBDD CONTAINS RESTRICTED ACTIONS */
  /* 1 OR 4 OR 7 - actionsBDD CONTAINS NON-RESTRICTED ACTIONS AND TAU   */
  /* 2 OR 5 OR 8 - actionsBDD CONTAINS RESTRICTED ACTIONS */

  if ((type == 0) || (type == 3) || (type == 6)) {

    c->actionsBDD = VersisComposeActions(c);
    Bdd_Fortify(c->actionsBDD);

  }

  if ((type == 1) || (type == 4) || (type == 7)) {

    c->actionsBDD = VersisComposeActions(c);
    c->actionsBDD = Bdd_ITE(c->actionsBDD,bdd_termTrue,tau);  /* add action 'TAU' */
    Bdd_Fortify(c->actionsBDD);

  }

  if ((type == 2) || (type == 5) || (type == 8)) {

    c->actionsBDD = VersisComposeActions(c);
    Bdd_Fortify(c->actionsBDD);

  }

  /* CALCULATE INITIAL STATE OF THE COMPOSITION */

  sup1 = bdd_termTrue;
  for(i=0; i<numP; i++) {
    p = &pa_processTable[c->tableP[i]];
    if (p->initial != -1) {
      sup1 = Bdd_ITE(sup1,p->tableS[p->initial].bddR,bdd_termFalse);
    }
  }
  Bdd_Fortify(sup1);
  c->initialBDD = sup1;

  /* CALCULATE TRANSITION RELATION OF THE COMPOSITION */

  if (onthefly) {
    c->onthefly = TRUE;
    c->stateBDD = c->initialBDD;
    c->transitionBDD = bdd_termFalse;
  } else {

    c->onthefly = FALSE;
    Compose(c);
    Versis_ComposeFinish(numcomp);
    Bdd_IncCounter();

    /* SAVE RESULTS */

    Bdd_SaveFormula("D_COMP_",c->name,c->transitionBDD);
    Bdd_SaveFormula("Initial_COMP_",c->name,c->initialBDD);
    Bdd_SaveFormula("S_COMP",c->name,c->stateBDD);

    /*
    fprintf(stdout,"\nStatistic after Composition\n");
    fprintf(stdout,"About composition:\n");
    Bdd_FunctionStat(stdout,c->transitionBDD);
    fprintf(stdout,"About system:\n");
    Bdd_SystemStat(stdout);
    */

  }

  return;
}

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

void
Versis_ComposeInit(Est_String name)
{
  Pa_Composition *c;
  int i,j,numP;
  Bdd_Edge sup;
  /* int type; */  /* for debugging */
  /* Bdd_Edge tau; */ /* for debugging */

  i = Pa_FindComposition(name);

  if (i == -1) {

    printf(" Composition %s does not exist.\n",name);
    return;

  } else {

    c = &pa_compositionTable[i];
    numP = c->numProcesses;
    /* type = c->type; */ /* for debugging */
    /* tau = pa_sortTable[c->sort].table[0].p; */ /* for debugging */

    /* INITIALIZE SUPPLEMENTAL STRUCTURES */
    /* ALSO CHECK FOR CONNECTIONS BETWEEN PROCESSES */

    for(i=0; i<numP; i++) {
      c->di[i] = bdd_termFalse;
    }

    for(i=0; i<numP; i++) {
      for(j=0; j<numP; j++) {
        sup = Bdd_ITE(c->alphabet[i],c->alphabet[j],bdd_termFalse);
        if (Bdd_isEqv(sup,bdd_termFalse)) {
          c->dij[i * numP + j] = bdd_termNull;
        } else {
          c->dij[i * numP + j] = bdd_termFalse;
        }
      }
    }

    /* INITIALIZE RESULTS */

    c->snew = c->stateBDD = c->initialBDD;
    c->transitionBDD = bdd_termFalse;

  }
}

/**Function****************************************************************
  Synopsis    []
  Description [Calculates next N steps of composition]
  SideEffects [Use Versis_ComposeInit before this.
               c->stateBDD and c->snew not fortified.
               c->transitionBDD not calculated.
               Use Versis_ComposeFinish after this.]
  SeeAlso     []
  ************************************************************************/

int
Versis_ComposeStep(int numcomp, int N)
{
  int loop;
  Pa_Composition *c;

  c = &pa_compositionTable[numcomp];
  loop = ComposeStep(c,N);

  /* REPORT BDD SIZE */
  /*
  {
  int nodes,gi,gj,numP;
  fprintf(stdout,"[REPORT AFTER %d STEP(S)]",loop);
  numP = c->numProcesses;
  nodes = 0;
  for(gi=0; gi<numP; gi++) {
    fprintf(stdout,"[di:");
    nodes = nodes + Bdd_FunctionStat(stdout,c->di[gi]);
    fprintf(stdout,"]");
    for(gj=0; gj<numP; gj++)
    if (!Bdd_isNull(c->dij[gi * numP + gj])) {
      fprintf(stdout,"[dij:");
      nodes = nodes + Bdd_FunctionStat(stdout,c->dij[gi * numP + gj]);
      fprintf(stdout,"]");
    }
  }
  fprintf(stdout,"[SUM: %d]\n",nodes);
  printf("[BDD NODES: %d]",nodes);
  }
  */

  return loop;
}

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

void
Versis_ComposeFinish(int numcomp)
{
  Pa_Composition *c;
  int type;
  int i,j,k,numP;
  Bdd_Edge tau,tr1,tr2,sup,sup1,sup2;

  c = &pa_compositionTable[numcomp];
  numP = c->numProcesses;
  type = c->type;
  tau = pa_sortTable[c->sort].table[0].p;

  if (type < 3) {

    /* IF STANDARD CCS COMPOSITION IS COMPUTED di AND dij */
    /* WITH ADDED stab MUST BE COLLECTED                  */

    /* ADD stab AND COLLECT di */

    tr1 = bdd_termFalse;
    for(i=0; i<numP; i++) {

      sup = bdd_termTrue;
      for(k=0; k<numP; k++) {
        if (k != i) {
          sup = Bdd_ITE(sup,pa_processTable[c->tableP[k]].stab,bdd_termFalse);
    }
      }
      sup = Bdd_ITE(sup,c->di[i],bdd_termFalse);

      /*
      sup = c->di[i];
      for(k=0; k<numP; k++) {
        if (k != i) {
          sup = Bdd_ITE(sup,pa_processTable[c->tableP[k]].stab,bdd_termFalse);
        }
      }
      */

      tr1 = Bdd_ITE(tr1,bdd_termTrue,sup);
    }

    /* ADD stab AND COLLECT dij */

    tr2 = bdd_termFalse;
    for(i=0; i<numP; i++) {
      for(j=0; j<i; j++)
      if (!Bdd_isNull(c->dij[i * numP + j])) {

        /**/
        sup = bdd_termTrue;
        for(k=0; k<numP; k++) {
          if ((k != i) && (k != j)) {
            sup = Bdd_ITE(sup,pa_processTable[c->tableP[k]].stab,bdd_termFalse);
          }
        }
        sup1 = Bdd_ITE(sup,c->dij[i * numP + j],bdd_termFalse);
        sup2 = Bdd_ITE(sup,c->dij[j * numP + i],bdd_termFalse);
        /**/

        /*
        sup1 = c->dij[i * numP + j];
        sup2 = c->dij[j * numP + i];
        for(k=0; k<numP; k++) {
          if ((k != i) && (k != j)) {
            sup1 = Bdd_ITE(sup1,pa_processTable[c->tableP[k]].stab,bdd_termFalse);
            sup2 = Bdd_ITE(sup2,pa_processTable[c->tableP[k]].stab,bdd_termFalse);
          }
        }
        */

        tr2 = Bdd_ITE(tr2,bdd_termTrue,sup1);
        tr2 = Bdd_ITE(tr2,bdd_termTrue,sup2);

      }
    }
    tr2 = Bdd_ITE(tau,tr2,bdd_termFalse); /* tr2 = 'tau' * tr2 */

  } else {

    /* IF MULTI-WAY COMPOSITION WITH ISOCHRONIC FORKS IS COMPUTED */
    /* di AND dij MUST BE SIMPLY COLLECTED                        */

    /* COLLECT di */

    tr1 = bdd_termFalse;
    for(i=0; i<numP; i++) {
      tr1 = Bdd_ITE(tr1,bdd_termTrue,c->di[i]);
    }

    /* ADD stab AND COLLECT dij */

    tr2 = bdd_termFalse;
    for(i=0; i<numP; i++) {
      for(j=0; j<i; j++)
      if (!Bdd_isNull(c->dij[i * numP + j])) {
        tr2 = Bdd_ITE(tr2,bdd_termTrue,c->dij[i * numP + j]);
        tr2 = Bdd_ITE(tr2,bdd_termTrue,c->dij[j * numP + i]);
      }
    }
    tr2 = Bdd_ITE(tau,tr2,bdd_termFalse); /* tr2 = 'tau' * tr2 */

  } /* if (type) */

  c->transitionBDD = Bdd_ITE(tr1,bdd_termTrue,tr2);
  Bdd_Fortify(c->transitionBDD);

  /*
  printf("\n");
  Pa_DecodeCompTR(c,c->transitionBDD,FALSE);
  Pa_DecodeCompTR(c,Bdd_ITE(tau,bdd_termFalse,c->transitionBDD),FALSE);
  printf("\n");
  */
}

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

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

/**Function****************************************************************
  Synopsis    []
  Description []
  SideEffects [This should be somehow identical to ComposeStep.]
  SeeAlso     []
  ************************************************************************/

static void
Compose(Pa_Composition *c)
{
  int numP;
  int type;
  int i,j,k;
  int gi,gj;
  Bdd_Edge s_new, s_acc;
  Bdd_Edge sup, sup1, sup2;     /* supplemental functions */
  Bdd_Edge sup2b, sup2bin, sup2bout; /* supplemental functions */
  Bdd_Edge s1, s2, s3;        /* supplemental functions */
  Bdd_Edge new1, new2;        /* supplemental functions */
  Est_String s;
  /* Bdd_Edge tau; */ /* for debugging */

  /* NOTE: PROCESSES HAVE TO BE ENCODED WITH DIFFERENT STATE-VARIABLES! */

  numP = c->numProcesses;
  type = c->type;
  /* tau = pa_sortTable[c->sort].table[0].p; */ /* for debugging */

  /* INITIALIZE SUPPLEMENTAL STRUCTURES */
  /* ALSO CHECK FOR CONNECTIONS BETWEEN PROCESSES */

  for(i=0; i<numP; i++) {
    c->di[i] = bdd_termFalse;
  }

  for(i=0; i<numP; i++) {
    for(j=0; j<numP; j++) {
      sup = Bdd_ITE(c->alphabet[i],c->alphabet[j],bdd_termFalse);
      if (Bdd_isEqv(sup,bdd_termFalse)) {
        c->dij[i * numP + j] = bdd_termNull;
      } else {
        c->dij[i * numP + j] = bdd_termFalse;
      }
    }
  }

  /* INITIALIZE RESULTS */

  c->snew = c->stateBDD = c->initialBDD;
  c->transitionBDD = bdd_termFalse;

  /* s_new (RRR) CONTAIN NEW STATES FOUND IN PREVIOUSLY STEP OF CALCULATION */
  /* s_acc (RRR) CONTAIN ALL REACHED STATES */

  s_new = c->snew;
  s_acc = c->stateBDD;

  /* LOOP UNTIL NO NEW STATE IS REACHED */

  do {

    /*
    printf("\nNew states to be processed:\n");
    Pa_DecodeCompStates(c,s_new,TRUE);
    */

    new1 = bdd_termFalse;
    new2 = bdd_termFalse;

    /* PART ONE */
    /* CALCULATE NEW STATES, WHICH ARE REACHED WITHOUT COMMUNICATION */
    /* BETWEEN PROCESSES AND STORE THEM IN new1 (RRR)                */

    for(i=0; i<numP; i++) {

      /* COMPUTE ALL TRANSITIONS IN PROCESS i WHICH ARE ALLOWED   */
      /* WITHOUT COMMUNICATION AND STORE THEM IN s1 (RRRAS)       */

      if ((type == 1) || (type == 4) || (type == 7)) {
        s1 = Bdd_ITE(c->actionsBDD,pa_processTable[c->tableP[i]].d,bdd_termFalse);
      }

      if ((type == 0) || (type == 3) || (type == 6) ||
          (type == 2) || (type == 5) || (type == 8)) {
        s1 = Bdd_ITE(c->actionsBDD,bdd_termFalse,pa_processTable[c->tableP[i]].d);
      }

      /* UPDATE s1 (RRRAS)                                          */
      /* IT NOW CONTAINS ONLY TRANSITIONS STARTING FROM s_new (RRR) */

      s1 = Bdd_ITE(s1,s_new,bdd_termFalse);

      /*
      printf("COMPOSE DEBUG (TRANSITIONS WITHOUT COMMUNICATION, NOT TAU):\n");
      Pa_DecodeCompTR(c,Bdd_ITE(tau,bdd_termFalse,s1),TRUE);
      */

      if (type < 3) {

        /* IF STANDARD CCS COMPOSITION IS COMPUTED THEN:           */
        /* 1. ACCUMULATE TRANSITIONS s1 (RRRAS) IN c->di (RRRASSS) */

        c->di[i] = Bdd_ITE(c->di[i],bdd_termTrue,s1);

        /* 2. CALCULATE STATES REACHED WITH TRANSITIONS FROM       */
        /*    s1 (RRRASSS) AND STORE THEM IN sup (RRR)             */

        sup = Bdd_NewState1(s1,pa_processTable[c->tableP[i]].name);

        /* 3. ADD STATES FROM sup (RRR) TO new1 (RRR)              */
        new1 = Bdd_ITE(new1,bdd_termTrue,sup);

      } else {

        /* IF MULTI-WAY COMPOSITION WITH ISOCHRONIC FORKS IS COMPUTED THEN: */
        /* 1. CHECK IN OTHER PROCESSES IF THEY CAN PERFORM EQUAL ACTIONS.   */
        /*    STORE COMPLETE TRANSITIONS IN s1 (RRRAS+S)                    */
        /* WARNING: CURRENTLY, INPUT AND OUTPUT ACTIONS BOTH MULTISYNC      */
        /* THIS IS OK, BECAUSE IN CIRCUITS OUTPUT ACTIONS ARE UNIQUE        */
        for(j=0; j<numP; j++) {
          if (j != i) {

            if (Bdd_isNull(c->dij[i * numP + j])) {

              /* I AND J CANNOT SYNCHRONISE */
              sup1 = bdd_termFalse;
              sup2b = s1;

            } else {

              sup1 = Bdd_ITE(s1,pa_processTable[c->tableP[j]].d,bdd_termFalse);
              sup2 = Bdd_RelOpSimple(sup1,"Ex xS",TRUE);
              sup2 = Bdd_ITE(sup2,bdd_termFalse,s1);

              /* sup3 = sup1 + sup2 */
              /* sup1 CONTAINS TRANSITIONS, WHERE J IS ALREADY SYNCHRONISED */
              /* sup2 CONTAINS TRANSITIONS, WITH WHICH J CANNOT SYNCHRONISE */

              /* sup2 = sup2a + sup2b */
              /* sup2a ARE THOSE IN ALPHABET OF J                           */
              /* sup2b ARE THOSE NOT IN ALPHABET OF J                       */

              /*
              sup2a = Bdd_ITE(c->alphabet[j],sup2,bdd_termFalse);
              */

              sup2b = Bdd_ITE(c->alphabet[j],bdd_termFalse,sup2);

            }

            /* TRANSITIONS FROM sup2a ARE WRONG - COMPUTATION INTERFERENCE */
            /* TRANSITIONS FROM sup2b ARE ALLOWED, PROCESS J SIMPLY WAIT   */

            /* FUNDAMENTAL-MODE NORMALIZATION */
            /* FOR INPUT ACTIONS, J DOESN'T WAIT IF IT HAS OUTPUT TRANSITION */
            /* STATES MUST NOT HAVE BOTH, INPUT AND OUTPUT ACTIONS */

            if ((type == 6) || (type == 7) || (type == 8)) {

              /*
              printf("\nFUNDAMENTAL-MODE NORMALIZATION - input sup2b:\n");
              Pa_DecodeCompTR(c,sup2b,TRUE);
              */

              sup2bin = Bdd_ITE(pa_sortTable[c->sort].a0,bdd_termFalse,sup2b); /*?*/
              sup2bout = Bdd_ITE(pa_sortTable[c->sort].a0,sup2b,bdd_termFalse); /*!*/

              /* DELETE INPUT TRANISITIONS FROM STATES, WHERE I HAS OUTPUT TRANSITIONS */
              /* HAZARDS MUST BE PREPROCESED ! */
              sup2bin = Bdd_ITE(sup2bout,bdd_termFalse,sup2bin);

              /* DELETE INPUT TRANISITIONS FROM STATES, WHERE J HAS OUTPUT TRANSITIONS */
              /* BUT ONLY FROM THOSE WITHOUT INPUT TRANSITIONS - THERE ARE HAZARDS */
              /* HAZARDS MAY FIRE OR NOT FIRE */

              sup = Bdd_RelOp(pa_processTable[c->tableP[j]].d,pa_sortTable[c->sort].a0,"#AND Ex xA xS",TRUE); /*!*/
              sup2bin = Bdd_ITE(sup,bdd_termFalse,sup2bin);

              /* ALLOWED TRANSITIONS, WHERE ACTION IS NOT IN ALPHABET OF J */
              sup2b = Bdd_ITE(sup2bin,bdd_termTrue,sup2bout);

              /*
              printf("\nFUNDAMENTAL-MODE NORMALIZATION - output sup2b:\n");
              Pa_DecodeCompTR(c,sup2b,TRUE);
              */

            }

            sup2 = Bdd_ITE(sup2b,pa_processTable[c->tableP[j]].stab,
                           bdd_termFalse);
            s1 = Bdd_ITE(sup1,bdd_termTrue,sup2);
        }}

        /* 2. ACCUMULATE TRANSITIONS s1 (RRRASSS) IN c->di (RRRASSS)  */

        c->di[i] = Bdd_ITE(c->di[i],bdd_termTrue,s1);

      } /* else if (type < 3) */

      /* PURGE BDD NODES AFTER PART ONE */

      /*
      Bdd_IncCounter();
      Bdd_Fresh(new1);
      Bdd_Fresh(new2);
      Bdd_Fresh(s_new);
      Bdd_Fresh(s_acc);
      for(gi=0; gi<numP; gi++) {
        Bdd_Fresh(c->di[gi]);
        for(gj=0; gj<numP; gj++)
        if (!Bdd_isNull(c->dij[gi * numP + gj])) {
          Bdd_Fresh(c->dij[gi * numP + gj]);
        }
      }
      */

    } /* for (i) */

    /* PART TWO */
    /* CALCULATE NEW STATES, WHICH ARE REACHED WITH COMMUNICATION */
    /* BETWEEN PROCESSES AND STORE THEM IN new2 (RRR)             */

    for(i=0; i<numP; i++) {

      /* FOR ALL J FIND COMMUNICATION BETWEEN PROCESSES I AND J */

      for(j=0; j<numP; j++) {
        if (j != i) {
          if (!Bdd_isNull(c->dij[i * numP + j])) {

            /* COMPUTE TRANSITIONS WITHOUT a0  */
            /* IN PROCESS I WITH OUTPUT ACTIONS s1 (RAS)  */
            /* IN PROCESS J WITH INPUT ACTIONS s2 (RAS)   */
            /* ONLY RESTRICTED ACTIONS ARE COMPOSED TOGETHER! */

            s1 = Bdd_Restrict(pa_processTable[c->tableP[i]].d,
                            Bdd_GetVariable(pa_sortTable[c->sort].a0), TRUE);

            s2 = Bdd_Restrict(pa_processTable[c->tableP[j]].d,
                            Bdd_GetVariable(pa_sortTable[c->sort].a0), FALSE);

            if ((type == 1) || (type == 4) || (type == 7)) { /* not-restricted actions */
              s1 = Bdd_ITE(c->actionsBDD,bdd_termFalse,s1);
              s2 = Bdd_ITE(c->actionsBDD,bdd_termFalse,s2);
            }

            if ((type == 2) || (type == 5) || (type == 8)) { /* restricted actions */
              s1 = Bdd_ITE(c->actionsBDD,s1,bdd_termFalse);
              s2 = Bdd_ITE(c->actionsBDD,s2,bdd_termFalse);
            }

            if (type < 3) {

              /* IF STANDARD CCS COMPOSITION IS COMPUTED THEN:                  */
              /* 1. COMPOSE s1 (RAS) AND s2 (RAS) TOGETHER AND CREATE s3 (RRSS) */
              /* 2. UPDATE s3 (RRRSS) TO CONTAIN ONLY TRANSITIONS FROM s_new    */

              s3 = Bdd_RelOp(s1,s2,"#AND Ex xA",TRUE);
              s3 = Bdd_ITE(s_new,s3,bdd_termFalse);

              /*
              printf("COMPOSE DEBUG (TRANSITIONS WITH COMMUNICATION):\n");
              Pa_DecodeCompTR(c,Bdd_ITE(Bdd_ITE(s3,s1,bdd_termFalse),s2,bdd_termFalse),TRUE);
              */

              /* 3. ACCUMULATE TRANSITIONS s3 (RRRSS) IN c->dij (RRRSS)  */

              c->dij[i * numP + j] = Bdd_ITE(c->dij[i * numP + j],
                                             bdd_termTrue, s3);

              /* 4. CALCULATE STATES REACHED WITH TRANSITIONS FROM   */
              /*    s3 (RRRSS) AND STORE THEM IN sup (RRR)           */

              sup = Bdd_NewState2(s3,
                                pa_processTable[c->tableP[i]].name,
                                pa_processTable[c->tableP[j]].name);

              /* 5. ADD STATES FROM sup (RRR) TO new2 (RRR) */
              new2 = Bdd_ITE(new2,bdd_termTrue,sup);

            } else {

              /* IF MULTI-WAY COMPOSITION IS COMPUTED THEN                        */
              /* 1. COMPOSE s1 (RAS) AND s2 (RAS) TOGETHER AND CREATE s3 (RRASS)  */
              /*    s3 (RRASS) DOES NOT CONTAIN a0                                */

              s3 = Bdd_ITE(s1,s2,bdd_termFalse); /* s1 = output(i), s2 = input(j) */

              /* 2. CHECK IN OTHER PROCESSES IF THEY CAN PERFORM THE SAME ACTION. */
              /*    STORE COMPLETE TRANSITIONS IN s3 (RRRASS)                     */
              /* WARNING: CURRENTLY, INPUT AND OUTPUT ACTIONS BOTH MULTISYNC      */
              /* THIS IS OK, BECAUSE IN CIRCUITS OUTPUT ACTIONS ARE UNIQUE        */

              for(k=0; k<numP; k++) {
                if ((k != i) && (k != j)) {
                  if ((!Bdd_isNull(c->dij[i * numP + k]))
                      && (!Bdd_isNull(c->dij[j * numP + k]))) {

                    sup1 = Bdd_ITE(s3,pa_processTable[c->tableP[k]].d,bdd_termFalse);
                    sup2 = Bdd_RelOpSimple(sup1,"Ex xS",TRUE);
                    sup2 = Bdd_E(sup2,Bdd_GetVariable(pa_sortTable[c->sort].a0));

                    s = (Est_String) malloc(255);
                    sprintf(s,"Ex xR<%s>",pa_processTable[c->tableP[k]].name);
                    sup2 = Bdd_RelOpComplex(sup2,s,TRUE);
                    free(s);

                    sup2 = Bdd_ITE(sup2,bdd_termFalse,s3);

                    /* sup3 = sup1 + sup2 */
                    /* sup1 CONTAINS TRANSITIONS, WHERE K CAN SYNCHRONISE          */
                    /* sup2 CONTAINS TRANSITIONS, WITH WHICH K CANNOT SYNCHRONISE  */

                    /* sup2 = sup2a + sup2b */
                    /* sup2a ARE THOSE IN ALPHABET OF J                           */
                    /* sup2b ARE THOSE NOT IN ALPHABET OF J                       */

                    /*
                    sup2a = Bdd_ITE(sup2,c->alphabet[k],bdd_termFalse);
                    */

                    sup2b = Bdd_ITE(c->alphabet[k],bdd_termFalse,sup2);

                    /* TRANSITIONS FROM sup2a ARE WRONG - COMPUTATION INTERFERENCE */
                    /* TRANSITIONS FROM sup2b ARE ALLOWED, PROCESS K SIMPLY WAIT   */

                    sup2b = Bdd_ITE(sup2b,pa_processTable[c->tableP[k]].stab,
                                    bdd_termFalse);
                    s3 = Bdd_ITE(sup1,bdd_termTrue,sup2b);

                  } else {

                    s3 = Bdd_ITE(s3,pa_processTable[c->tableP[k]].stab,bdd_termFalse);

                  }
                }
              }

              /* 3. REMOVE ACTION VARIABLES FROM s3                      */
              /* 4. s3 (RRRSSS) TO CONTAIN ONLY TRANSITIONS FROM s_new   */

              s3 = Bdd_RelOpSimple(s3,"Ex xA",TRUE);
              s3 = Bdd_ITE(s_new,s3,bdd_termFalse);

              /* 5. ACCUMULATE TRANSITIONS s3 (RRRSS) IN c->dij (RRRSS)  */

              c->dij[i * numP + j] = Bdd_ITE(c->dij[i * numP + j], bdd_termTrue, s3);

            }  /* else if (type < 3) */

          } /* for (j) */
        }
      }

      /* PURGE BDD NODES AFTER PART TWO */

      /*
      Bdd_IncCounter();
      Bdd_Fresh(new1);
      Bdd_Fresh(new2);
      Bdd_Fresh(s_new);
      Bdd_Fresh(s_acc);
      for(gi=0; gi<numP; gi++) {
        Bdd_Fresh(c->di[gi]);
        for(gj=0; gj<numP; gj++)
        if (!Bdd_isNull(c->dij[gi * numP + gj])) {
          Bdd_Fresh(c->dij[gi * numP + gj]);
        }
      }
      */

    } /* for (i) */

    /* PART THREE */
    /* GET RESULTS OF ONE STEP */

    if (type < 3) {
      /* NOT MULTI-WAY COMPOSITION */

      /* CALCULATION OF NEW STATES */
      s_new = Bdd_ITE(new1,bdd_termTrue,new2);

    } else {
      /* MULTI-WAY COMPOSITION */

      /* CALCULATION OF NEW STATES */
      new1 = bdd_termFalse;
      for(i=0; i<numP; i++) {

        /* CALCULATE STATES REACHED WITH TRANSITIONS c->di[i] (RRRASSS) */
        /* AND STORE THEM IN sup (RRR)                                  */

        sup = Bdd_NewState(c->di[i]);

        /* ADD STATES FROM sup (RRR) TO new1 (RRR) */
        new1 = Bdd_ITE(new1,bdd_termTrue,sup);

      } /* for (i) */

      new2 = bdd_termFalse;
      for(i=0; i<numP; i++) {
        for(j=0; j<numP; j++) {
          if (i != j) {
            if (!Bdd_isNull(c->dij[i * numP + j])) {

              /* CALCULATE STATES REACHED WITH TRANSITIONS FROM   */
              /* c->dij (RRRSS) AND STORE THEM IN sup (RRR)       */

              sup = Bdd_NewState(c->dij[i * numP + j]);

              /* ADD STATES FROM sup (RRR) TO new2 (RRR) */
              new2 = Bdd_ITE(new2,bdd_termTrue,sup);

            }
          }
        }
      }

      /* UPDATE s_new (RRR) */
      s_new = Bdd_ITE(new1,bdd_termTrue,new2);

    }

    /*
    printf("\nNew states found and stored in new1:\n");
    Pa_DecodeCompStates(c,new1,TRUE);
    printf("\nNew states found and stored in new2:\n");
    Pa_DecodeCompStates(c,new2,TRUE);
    */

    /* UPDATE s_new (RRR) */
    s_new = Bdd_ITE(s_acc,bdd_termFalse,s_new);

    /* UPDATE s_acc (RRR) */
    s_acc = Bdd_ITE(s_acc,bdd_termTrue,s_new);

    /* PURGE BDD NODES AFTER PART THREE */

    Bdd_IncCounter();
    Bdd_Fresh(s_new);
    Bdd_Fresh(s_acc);
    for(gi=0; gi<numP; gi++) {
      Bdd_Fresh(c->di[gi]);
      for(gj=0; gj<numP; gj++)
      if (!Bdd_isNull(c->dij[gi * numP + gj])) {
        Bdd_Fresh(c->dij[gi * numP + gj]);
      }
    }

    /* FORCE GARBAGE COLLECTION - USED FOR TESTING */
    /*
    Bdd_Garbage();
    */

  } while(!(Bdd_isEqv(s_new,bdd_termFalse)));

  c->stateBDD = s_acc;
  Bdd_Fortify(c->stateBDD);

  c->snew = s_new;
  Bdd_Fortify(c->snew);

  /*
  printf("\n");
  Pa_DecodeCompStates(c,c->stateBDD,FALSE);
  Pa_DecodeCompStates(c,c->snew,FALSE);
  printf("\n");
  */

}


/**Function****************************************************************
  Synopsis    []
  Description []
  SideEffects [This should be somehow identical to Compose.]
  SeeAlso     []
  ************************************************************************/

static int
ComposeStep(Pa_Composition *c, int N)
{
  int numP;
  int type;
  int i,j,k;
  int gi,gj;
  Bdd_Edge s_new, s_acc;
  Bdd_Edge sup, sup1, sup2;     /* supplemental functions */
  Bdd_Edge sup2b, sup2bin, sup2bout; /* supplemental functions */
  Bdd_Edge s1, s2, s3;        /* supplemental functions */
  Bdd_Edge new1, new2;        /* supplemental functions */
  Est_String s;
  int loop;
  /* Bdd_Edge tau; */ /* for debugging */

  /* NOTE: PROCESSES HAVE TO BE ENCODED WITH DIFFERENT STATE-VARIABLES! */

  numP = c->numProcesses;
  type = c->type;
  /* tau = pa_sortTable[c->sort].table[0].p; */ /* for debugging */

  /* s_new (RRR) CONTAIN NEW STATES FOUND IN PREVIOUSLY STEP OF CALCULATION */
  /* s_acc (RRR) CONTAIN ALL REACHED STATES */

  s_new = c->snew;
  s_acc = c->stateBDD;

  /* LOOP N TIMES, STOP IF NO NEW STATE IS REACHED */

  loop = 0;
  do {

    loop++;

    /*
    fprintf(stderr,"\nLOOP [%d/%d] STARTED\n",loop,N);
    */

    /*
    printf("\nNew states to be processed in loop %d:\n",loop);
    Pa_DecodeCompStates(c,s_new,TRUE);
    */

    new1 = bdd_termFalse;
    new2 = bdd_termFalse;

    /* PART ONE */
    /* CALCULATE NEW STATES, WHICH ARE REACHED WITHOUT COMMUNICATION */
    /* BETWEEN PROCESSES AND STORE THEM IN new1 (RRR)                */

    for(i=0; i<numP; i++) {

      /*
      fprintf(stderr,"[%d/%d]",i,numP);
      */

      /* COMPUTE ALL TRANSITIONS IN PROCESS I WHICH ARE ALLOWED   */
      /* WITHOUT COMMUNICATION AND STORE THEM IN s1 (RRRAS)       */

      if ((type == 1) || (type == 4) || (type == 7)) {
        s1 = Bdd_ITE(c->actionsBDD,pa_processTable[c->tableP[i]].d,bdd_termFalse);
      }

      if ((type == 0) || (type == 3) || (type == 6) ||
          (type == 2) || (type == 5) || (type == 8)) {
        s1 = Bdd_ITE(c->actionsBDD,bdd_termFalse,pa_processTable[c->tableP[i]].d);
      }

      /* UPDATE s1 (RRRAS)                                          */
      /* IT NOW CONTAINS ONLY TRANSITIONS STARTING FROM s_new (RRR) */

      s1 = Bdd_ITE(s1,s_new,bdd_termFalse);

      if (type < 3) {

        /* IF STANDARD CCS COMPOSITION IS COMPUTED THEN:           */
        /* 1. ACCUMULATE TRANSITIONS s1 (RRRAS) IN c->di (RRRASSS) */

        c->di[i] = Bdd_ITE(c->di[i],bdd_termTrue,s1);

        /* 2. CALCULATE STATES REACHED WITH TRANSITIONS FROM       */
        /*    s1 (RRRASSS) AND STORE THEM IN sup (RRR)             */

        sup = Bdd_NewState1(s1,pa_processTable[c->tableP[i]].name);

        /* 3. ADD STATES FROM sup (RRR) TO new1 (RRR)              */
        new1 = Bdd_ITE(new1,bdd_termTrue,sup);

      } else {

        /* IF MULTI-WAY COMPOSITION WITH ISOCHRONIC FORKS IS COMPUTED THEN: */
        /* 1. CHECK IN OTHER PROCESSES IF THEY CAN PERFORM EQUAL ACTIONS.   */
        /*    STORE COMPLETE TRANSITIONS IN s1 (RRRAS+S)                      */
        /* WARNING: CURRENTLY, INPUT AND OUTPUT ACTIONS BOTH MULTISYNC      */
        /* THIS IS OK, BECAUSE IN CIRCUITS OUTPUT ACTIONS ARE UNIQUE        */
        for(j=0; j<numP; j++) {
          if (j != i) {

            if (Bdd_isNull(c->dij[i * numP + j])) {

              /* I AND J CANNOT SYNCHRONISE */
          sup1 = bdd_termFalse;
              sup2b = s1;

        } else {

              sup1 = Bdd_ITE(s1,pa_processTable[c->tableP[j]].d,bdd_termFalse);
              sup2 = Bdd_RelOpSimple(sup1,"Ex xS",TRUE);
              sup2 = Bdd_ITE(sup2,bdd_termFalse,s1);

              /* sup3 = sup1 + sup2 */
              /* sup1 CONTAINS TRANSITIONS, WHERE J IS ALREADY SYNCHRONISED */
              /* sup2 CONTAINS TRANSITIONS, WITH WHICH J CANNOT SYNCHRONISE */

              /* sup2 = sup2a + sup2b */
              /* sup2a ARE THOSE IN ALPHABET OF J                           */
              /* sup2b ARE THOSE NOT IN ALPHABET OF J                       */

          /*
              sup2a = Bdd_ITE(c->alphabet[j],sup2,bdd_termFalse);
          */

              sup2b = Bdd_ITE(c->alphabet[j],bdd_termFalse,sup2);

        }

            /* TRANSITIONS FROM sup2a ARE WRONG - COMPUTATION INTERFERENCE */
            /* TRANSITIONS FROM sup2b ARE ALLOWED, PROCESS J SIMPLY WAIT   */

            /* FUNDAMENTAL-MODE NORMALIZATION */
            /* FOR INPUT ACTIONS, J DOESN'T WAIT IF IT HAS OUTPUT TRANSITION */
            /* STATES MUST NOT HAVE BOTH, INPUT AND OUTPUT ACTIONS */

            if ((type == 6) || (type == 7) || (type == 8)) {

          /*
              printf("\nFUNDAMENTAL-MODE NORMALIZATION - input sup2b:\n");
              Pa_DecodeCompTR(c,sup2b,TRUE);
          */

              sup2bin = Bdd_ITE(pa_sortTable[c->sort].a0,bdd_termFalse,sup2b); /*?*/
              sup2bout = Bdd_ITE(pa_sortTable[c->sort].a0,sup2b,bdd_termFalse); /*!*/

              /* DELETE INPUT TRANISITIONS FROM STATES, WHERE I HAS OUTPUT TRANSITIONS */
              /* HAZARDS MUST BE PREPROCESED ! */
              sup2bin = Bdd_ITE(sup2bout,bdd_termFalse,sup2bin);

              /* DELETE INPUT TRANISITIONS FROM STATES, WHERE J HAS OUTPUT TRANSITIONS */
              /* BUT ONLY FROM THOSE WITHOUT INPUT TRANSITIONS - THERE ARE HAZARDS */
              /* HAZARDS MAY FIRE OR NOT FIRE */

              sup = Bdd_RelOp(pa_processTable[c->tableP[j]].d,pa_sortTable[c->sort].a0,"#AND Ex xA xS",TRUE); /*!*/
              sup2bin = Bdd_ITE(sup,bdd_termFalse,sup2bin);

              /* ALLOWED TRANSITIONS, WHERE ACTION IS NOT IN ALPHABET OF J */
              sup2b = Bdd_ITE(sup2bin,bdd_termTrue,sup2bout);

          /*
              printf("\nFUNDAMENTAL-MODE NORMALIZATION - output sup2b:\n");
              Pa_DecodeCompTR(c,sup2b,TRUE);
          */

        }

            sup2 = Bdd_ITE(sup2b,pa_processTable[c->tableP[j]].stab,
                           bdd_termFalse);
            s1 = Bdd_ITE(sup1,bdd_termTrue,sup2);
    }}

        /* 2. ACCUMULATE TRANSITIONS s1 (RRRASSS) IN c->di (RRRASSS)  */

        c->di[i] = Bdd_ITE(c->di[i],bdd_termTrue,s1);

      } /* else if (type < 3) */

      /* PURGE BDD NODES AFTER PART ONE */

      /*
      Bdd_IncCounter();
      Bdd_Fresh(new1);
      Bdd_Fresh(new2);
      Bdd_Fresh(s_new);
      Bdd_Fresh(s_acc);
      for(gi=0; gi<numP; gi++) {
        Bdd_Fresh(c->di[gi]);
        for(gj=0; gj<numP; gj++)
        if (!Bdd_isNull(c->dij[gi * numP + gj])) {
          Bdd_Fresh(c->dij[gi * numP + gj]);
        }
      }
      */

    } /* for (i) */

    /*
    fprintf(stderr,"\nPART ONE [%d/%d] FINISHED\n",loop,N);
    Bdd_SystemStat(stderr);
    */

    /* PART TWO */
    /* CALCULATE NEW STATES, WHICH ARE REACHED WITH COMMUNICATION */
    /* BETWEEN PROCESSES AND STORE THEM IN new2 (RRR)             */

    for(i=0; i<numP; i++) {

      /* FOR ALL J FIND COMMUNICATION BETWEEN PROCESSES I AND J */

      for(j=0; j<numP; j++)
      if (j != i)
      if (!Bdd_isNull(c->dij[i * numP + j])) {

        /*
        fprintf(stderr,"[%d-%d/%d]",i,j,numP);
        */

        /* COMPUTE TRANSITIONS WITHOUT a0  */
        /* IN PROCESS I WITH OUTPUT ACTIONS s1 (RAS)  */
        /* IN PROCESS J WITH INPUT ACTIONS s2 (RAS)   */
        /* ONLY RESTRICTED ACTIONS ARE COMPOSED TOGETHER! */

        s1 = Bdd_Restrict(pa_processTable[c->tableP[i]].d,
                        Bdd_GetVariable(pa_sortTable[c->sort].a0), TRUE);

        s2 = Bdd_Restrict(pa_processTable[c->tableP[j]].d,
                        Bdd_GetVariable(pa_sortTable[c->sort].a0), FALSE);

        if ((type == 1) || (type == 4) || (type == 7)) { /* not-restricted actions */
          s1 = Bdd_ITE(c->actionsBDD,bdd_termFalse,s1);
          s2 = Bdd_ITE(c->actionsBDD,bdd_termFalse,s2);
        }

        if ((type == 2) || (type == 5) || (type == 8)) { /* restricted actions */
          s1 = Bdd_ITE(c->actionsBDD,s1,bdd_termFalse);
          s2 = Bdd_ITE(c->actionsBDD,s2,bdd_termFalse);
        }

        if (type < 3) {

          /* IF STANDARD CCS COMPOSITION IS COMPUTED THEN:                  */
          /* 1. COMPOSE s1 (RAS) AND s2 (RAS) TOGETHER AND CREATE s3 (RRSS) */
          /* 2. UPDATE s3 (RRRSS) TO CONTAIN ONLY TRANSITIONS FROM s_new    */

          s3 = Bdd_RelOp(s1,s2,"#AND Ex xA",TRUE);
          s3 = Bdd_ITE(s_new,s3,bdd_termFalse);

          /* 3. ACCUMULATE TRANSITIONS s3 (RRRSS) IN c->dij (RRRSS)  */

          c->dij[i * numP + j] = Bdd_ITE(c->dij[i * numP + j],
                                         bdd_termTrue, s3);

          /* 4. CALCULATE STATES REACHED WITH TRANSITIONS FROM   */
          /*    s3 (RRRSS) AND STORE THEM IN sup (RRR)           */

          sup = Bdd_NewState2(s3,
                            pa_processTable[c->tableP[i]].name,
                            pa_processTable[c->tableP[j]].name);

          /* 5. ADD STATES FROM sup (RRR) TO new2 (RRR) */
          new2 = Bdd_ITE(new2,bdd_termTrue,sup);

        } else {

          /* IF MULTI-WAY COMPOSITION IS COMPUTED THEN                        */
          /* 1. COMPOSE s1 (RAS) AND s2 (RAS) TOGETHER AND CREATE s3 (RRASS)  */
          /*    s3 (RRASS) DOES NOT CONTAIN a0                                */

          s3 = Bdd_ITE(s1,s2,bdd_termFalse); /* s1 = output(i), s2 = input(j) */

          /* 2. CHECK IN OTHER PROCESSES IF THEY CAN PERFORM THE SAME ACTION. */
          /*    STORE COMPLETE TRANSITIONS IN s3 (RRRASS)                     */
          /* WARNING: CURRENTLY, INPUT AND OUTPUT ACTIONS BOTH MULTISYNC      */
          /* THIS IS OK, BECAUSE IN CIRCUITS OUTPUT ACTIONS ARE UNIQUE        */

          for(k=0; k<numP; k++) {
            if ((k != i) && (k != j)) {
            if ((!Bdd_isNull(c->dij[i * numP + k]))
                && (!Bdd_isNull(c->dij[j * numP + k]))) {

              sup1 = Bdd_ITE(s3,pa_processTable[c->tableP[k]].d,bdd_termFalse);
              sup2 = Bdd_RelOpSimple(sup1,"Ex xS",TRUE);
              sup2 = Bdd_E(sup2,Bdd_GetVariable(pa_sortTable[c->sort].a0));

              s = (Est_String) malloc(255);
              sprintf(s,"Ex xR<%s>",pa_processTable[c->tableP[k]].name);
              sup2 = Bdd_RelOpComplex(sup2,s,TRUE);
              free(s);

              sup2 = Bdd_ITE(sup2,bdd_termFalse,s3);

              /* sup3 = sup1 + sup2 */
              /* sup1 CONTAINS TRANSITIONS, WHERE K CAN SYNCHRONISE          */
              /* sup2 CONTAINS TRANSITIONS, WITH WHICH K CANNOT SYNCHRONISE  */

              /* sup2 = sup2a + sup2b */
              /* sup2a ARE THOSE IN ALPHABET OF J                           */
              /* sup2b ARE THOSE NOT IN ALPHABET OF J                       */

              /*
              sup2a = Bdd_ITE(sup2,c->alphabet[k],bdd_termFalse);
              */

              sup2b = Bdd_ITE(c->alphabet[k],bdd_termFalse,sup2);

              /* TRANSITIONS FROM sup2a ARE WRONG - COMPUTATION INTERFERENCE */
              /* TRANSITIONS FROM sup2b ARE ALLOWED, PROCESS K SIMPLY WAIT   */

              sup2b = Bdd_ITE(sup2b,pa_processTable[c->tableP[k]].stab,
                              bdd_termFalse);
              s3 = Bdd_ITE(sup1,bdd_termTrue,sup2b);

        } else {

              s3 = Bdd_ITE(s3,pa_processTable[c->tableP[k]].stab,bdd_termFalse);

        }}
          }

          /* 3. REMOVE ACTION VARIABLES FROM s3                      */
          /* 4. s3 (RRRSSS) TO CONTAIN ONLY TRANSITIONS FROM s_new   */

          s3 = Bdd_RelOpSimple(s3,"Ex xA",TRUE);
          s3 = Bdd_ITE(s_new,s3,bdd_termFalse);

          /* 5. ACCUMULATE TRANSITIONS s3 (RRRSS) IN c->dij (RRRSS)  */

          c->dij[i * numP + j] = Bdd_ITE(c->dij[i * numP + j], bdd_termTrue, s3);

        }  /* else if (type < 3) */

      } /* for (j) */

      /* PURGE BDD NODES AFTER PART TWO */

      /*
      Bdd_IncCounter();
      Bdd_Fresh(new1);
      Bdd_Fresh(new2);
      Bdd_Fresh(s_new);
      Bdd_Fresh(s_acc);
      for(gi=0; gi<numP; gi++) {
        Bdd_Fresh(c->di[gi]);
        for(gj=0; gj<numP; gj++)
        if (!Bdd_isNull(c->dij[gi * numP + gj])) {
          Bdd_Fresh(c->dij[gi * numP + gj]);
        }
      }
      */

    } /* for (i) */

    /*
    fprintf(stderr,"\nPART TWO [%d/%d] FINISHED\n",loop,N);
    Bdd_SystemStat(stderr);
    */

    /* PART THREE */
    /* GET RESULTS OF ONE STEP */

    /* NOT MULTI-WAY COMPOSITION */
    if (type < 3) {
      /* NOT MULTI-WAY COMPOSITION */

      /* CALCULATION OF NEW STATES */
      s_new = Bdd_ITE(new1,bdd_termTrue,new2);

    } else {
      /* MULTI-WAY COMPOSITION */

      /* CALCULATION OF NEW STATES */

      new1 = bdd_termFalse;
      for(i=0; i<numP; i++) {

        /* CALCULATE STATES REACHED WITH TRANSITIONS c->di[i] (RRRASSS) */
        /* AND STORE THEM IN sup (RRR)                                  */

        sup = Bdd_NewState(c->di[i]);

        /* ADD STATES FROM sup (RRR) TO new1 (RRR) */
        new1 = Bdd_ITE(new1,bdd_termTrue,sup);

      } /* for (i) */

      new2 = bdd_termFalse;
      for(i=0; i<numP; i++) {
        for(j=0; j<numP; j++)
        if (i != j)
        if (!Bdd_isNull(c->dij[i * numP + j])) {

          /* CALCULATE STATES REACHED WITH TRANSITIONS FROM   */
          /* c->dij (RRRSS) AND STORE THEM IN sup (RRR)       */

          sup = Bdd_NewState(c->dij[i * numP + j]);

          /* ADD STATES FROM sup (RRR) TO new2 (RRR) */
          new2 = Bdd_ITE(new2,bdd_termTrue,sup);

        }
      }

      /* UPDATE s_new (RRR) */
      s_new = Bdd_ITE(new1,bdd_termTrue,new2);

    }

    /* UPDATE s_new (RRR) */
    s_new = Bdd_ITE(s_acc,bdd_termFalse,s_new);

    /* UPDATE s_acc (RRR) */
    s_acc = Bdd_ITE(s_acc,bdd_termTrue,s_new);

    /* PURGE BDD NODES AFTER PART THREE */

    /*
    Bdd_IncCounter();
    Bdd_Fresh(s_new);
    Bdd_Fresh(s_acc);
    for(gi=0; gi<numP; gi++) {
      Bdd_Fresh(c->di[gi]);
      for(gj=0; gj<numP; gj++)
      if (!Bdd_isNull(c->dij[gi * numP + gj])) {
        Bdd_Fresh(c->dij[gi * numP + gj]);
      }
    }
    */

    /* FORCE GARBAGE COLLECTION - USED FOR TESTING */
    /*
    Bdd_Garbage();
    */

    /*
    fprintf(stderr,"\nPART THREE [%d,%d] FINISHED\n",loop,N);
    Bdd_SystemStat(stderr);
    */

  } while(!(Bdd_isEqv(s_new,bdd_termFalse)) && (loop<N)); /* END OF LOOP */

  /*
  fprintf(stderr,"\nLOOP [%d/%d] FINISHED\n",loop,N);
  */

  if (Bdd_isEqv(s_new,bdd_termFalse)) loop--;

  c->stateBDD = s_acc;
  c->snew = s_new;

  /* PURGE BDD NODES AFTER THE END OF LOOP */

  /**/
  Bdd_IncCounter();
  Bdd_Fresh(c->stateBDD);
  Bdd_Fresh(c->snew);
  for(gi=0; gi<numP; gi++) {
    Bdd_Fresh(c->di[gi]);
    for(gj=0; gj<numP; gj++)
    if (!Bdd_isNull(c->dij[gi * numP + gj])) {
      Bdd_Fresh(c->dij[gi * numP + gj]);
    }
  }
  /**/

  /* CAREFULLY! */
  /* MUST BE USED IF ON-THE-FLY MODEL CHECKER CALLS Bdd_IncCounter() */
  /* IN REGULAR COMPOSITION, di AND dij ARE NOT FORTIFIED */

  /*
  Bdd_Fortify(c->stateBDD);
  Bdd_Fortify(c->snew);
  for(i=0; i<numP; i++) {
    Bdd_Fortify(c->di[i]);
    for(j=0; j<numP; j++)
    if (!Bdd_isNull(c->dij[i * numP + j])) {
      Bdd_Fortify(c->dij[i * numP + j]);
    }
  }
  */

  /*
  fprintf(stdout,"\nStatistic after Composition\n");
  fprintf(stdout,"About system:\n");
  Bdd_SystemStat(stdout);
  */

  return loop;
}

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

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

  if (!s) return 0;

  num = 0;
  sup = strdup(s);

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

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

    token = strspn(sup," \t");
  }

  free(sup);
  return num;
}
