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

  FileName    [paKod.c]
  Revision    [$Revision: 77 $]
  Date        [$Date: 2013-04-29 21:10:06 +0200 (pon, 29 apr 2013) $]
  Authors     [Robert Meolic (meolic@uni-mb.si)]
  Description [File paKod.c implements encoding and decoding of LTSs.]
  SeeAlso     [pa.h, paInt.h]

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

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

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

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

#include <math.h>
#include "paInt.h"

/*-----------------------------------------------------------------------*/
/* Structure declarations                                                */
/*-----------------------------------------------------------------------*/

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

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

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

static Bdd_Edge EncodeMinterm(Bdd_Edge *tabVar, int n, int i, int min);

static void Composition2ProcessR(Pa_Composition *comp, Bdd_Edge F,
                  Est_Boolean mark, int *decodingTableR, int procnum);

static void Composition2ProcessRAS(Pa_Composition *comp, Bdd_Edge F,
                  Est_Boolean mark, int minA, int maxA,
                  int *decodingTableR, int *decodingTableS, int procnum);

static int DecodeSortBddA(Pa_Sort *sort, Bdd_Edge F,
                          Est_Boolean mark, int minA, int maxA,
                          Est_String *act, Est_Boolean write);

static int DecodeProcessBddR(Pa_Process *proc, Bdd_Edge F,
                             Est_Boolean mark, int minR, int maxR,
                             Est_Boolean write);

static int DecodeProcessBddRAS(Pa_Process *proc, Bdd_Edge F,
                               Est_Boolean mark,
                               int minR, int maxR, int minA, int maxA,
                               int minS, int maxS, Est_Boolean write);

static int DecodeCompBddR(Pa_Composition *comp, Bdd_Edge F,
                          Est_Boolean mark, int *decodingTableR,
                          Est_Boolean write);

static int DecodeCompBddRAS(Pa_Composition *comp, Bdd_Edge F,
                            Est_Boolean mark, int minA, int maxA,
                            int *decodingTableR, int *decodingTableS,
                            Est_Boolean write);

static int DecodeProcProcPairBddRP(
                           Pa_Process *p1, Pa_Process *p2, Bdd_Edge F,
                           Est_Boolean mark, int minR, int maxR,
                           int minP, int maxP, Est_Boolean write);

static int DecodeCompProcPairBddRP(
                           Pa_Composition *comp, Pa_Process *p, Bdd_Edge F,
                           Est_Boolean mark, int *decodingTableR,
                           int minP, int maxP, Est_Boolean write);

static int DecodeCompCompPairBddRP(
                           Pa_Composition *c1, Pa_Composition *c2, Bdd_Edge F,
                           Est_Boolean mark, int *decodingTableR,
                           int *decodingTableS, Est_Boolean write);

static int DecodeSortAction(Pa_Sort *s, int minA, int maxA, Est_String *act,
                            Est_Boolean write);

static int DecodeProcessState(Pa_Process *p, int minR, int maxR,
                              Est_Boolean write);

static int DecodeProcessTR(Pa_Process *p, int minR, int maxR,
                           int minA, int maxA, int minS, int maxS,
                           Est_Boolean write);

static int DecodeCompState(Pa_Composition *c, int *decodingTableR,
                           Est_Boolean write);

static int DecodeCompTR(Pa_Composition *c, int minA, int maxA,
                        int *decodingTableR, int *decodingTableS,
                        Est_Boolean write);

static int DecodeProcProcPair(Pa_Process *p1, Pa_Process *p2,
                              int minR, int maxR, int minP, int maxP,
                              Est_Boolean write);

static int DecodeCompProcPair(Pa_Composition *c, Pa_Process *p,
                              int *decodingTableR, int minP, int maxP,
                              Est_Boolean write);

static int DecodeCompCompPair(Pa_Composition *c1, Pa_Composition *c2,
                              int *decodingTableR, int *decodingTableS,
                              Est_Boolean write);

static int DecodeAction(Pa_Sort *s, int min, int max, int f, Est_String *act,
                        Est_Boolean write, int more);

static int DecodeState(Pa_Process *p, int min, int max, int f,
                       Est_Boolean write, Est_Boolean pname, int more);

static Est_Boolean ExtractProcTransition(Pa_Process *p, Bdd_Edge F,
                      Est_Boolean mark, int *minR, int *minA, int *minS);

static Est_Boolean ExtractCompTransition(Pa_Composition *comp, Bdd_Edge F,
                      Est_Boolean mark, int *minA, int *decodingTableR,
              int *decodingTableS);

static Est_Boolean ExtractProcState(Pa_Process *proc, Bdd_Edge F,
                      Est_Boolean mark, int *minR);

static Est_Boolean ExtractCompState(Pa_Composition *comp, Bdd_Edge F,
                      Est_Boolean mark, int *decodingTableR);

static Est_Boolean ExtractSortAction(Pa_Sort *sort, Bdd_Edge F,
              Est_Boolean mark, int *minA);

static void CompStates2ProcStates(Pa_Composition *c, int i,
                      int *decodingTableR, int min, int max, int f,
                      Bdd_Edge F, int procnum);

static void CompTR2ProcTR(Pa_Composition *c, int iR, int iS,
                      int *decodingTableR, int *decodingTableS, int minA,
                      int maxA, int minR, int maxR, int minS, int maxS,
                      int fA, int fR,int fS, Bdd_Edge FR, Bdd_Edge FS,
                      int procnum);

static void concat(Est_String *s1, const Est_String s2);

static void printstate(Est_String name);

static void setproccomp(Pa_Composition *comp);

static int getWeight(Bdd_Edge f);

static int getProcComp(Bdd_Edge f);

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


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

/**Function****************************************************************
  Synopsis    []
  Description [V tabeli sortov poiscemo sort z danim imenom in ga kodiramo.
               Action 'TAU' has to be the first action in the table!]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

void
Pa_EncodeSort(Est_String name)
{
  Pa_Sort *s;
  Bdd_Edge var;
  Bdd_Edge *tabVar;
  Est_String x;
  int i,n,w;

  i = Pa_FindSort(name);
  if (i == -1) return;
  s = &pa_sortTable[i];

  /* dolocimo stevilo potrebnih spremenljivk za kodiranje akcij */
  n = (int)(1.9999999+log(s->numActions+1)/log(2.0));
  s->numVar = n;

  /* tvorimo spremenljivke in dolocimo utezi */
  tabVar = (Bdd_Edge *) malloc(n * sizeof(Bdd_Edge));
  x = (Est_String) malloc(127);

  /* HERE IS GIVEN THE ORDER OF a,b VARIABLES */

  w = 1;
  for (i=0; i<n; i++) {

    /* variable 'a' */
    sprintf(x,"a%d",i);            /* format "a%d\0" */
    var = Bdd_FoaTerminal(x);
    Bdd_AddFormula(x,var); /* ensure overwriting of existing formula */
    Pa_InitVariable(Bdd_GetVariable(var));
    pa_variableTable[Bdd_GetVariable(var)].weight = w;
    tabVar[i] = var;

    /* variable 'b' */
    sprintf(x,"b%d",i);            /* format "b%d\0" */
    var = Bdd_FoaTerminal(x);
    Bdd_AddFormula(x,var); /* ensure overwriting of existing formula */
    Pa_InitVariable(Bdd_GetVariable(var));
    pa_variableTable[Bdd_GetVariable(var)].weight = w;

    w = w * 2;
  }

  free(x);

  /* spremenljivka, ki doloca tip akcije */

  s->a0 = tabVar[0];

  /* MAKE BDD FOR ACTION 'TAU' */

  s->table[0].p = EncodeMinterm(tabVar, 0, n-1, 0);
  Bdd_Fortify(s->table[0].p);

  /* MAKE BDDs FOR OTHER ACTIONS */

  for (i=1; i<s->numActions; i++) {
    s->table[i].p = EncodeMinterm(tabVar, 2*i, n-1, 1);
    Bdd_Fortify(s->table[i].p);
  }

  free(tabVar);

  s->encoded = 1;
  PaSaveSortActions(s);
  return;
}

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

void
Pa_EncodeProcess(Est_String name)
{
  int seq;
  Pa_Process *p;
  Bdd_Edge var;
  Bdd_Edge d,e;
  Bdd_Edge states;
  Bdd_Edge *tabVarR;
  Bdd_Edge *tabVarS;
  int *tabOrder;
  Pa_State *newtableS;
  Est_String x;
  int i,n,m,w,newNumStates;

  seq = Pa_FindProcess(name);
  if (seq == -1) {
    printf("ERROR Pa_EncodeProcess: Process does not exists.\n");
    return;
  }

  p = &pa_processTable[seq];

  if (p->sort == -1) {
    printf("ERROR Pa_EncodeProcess: Sort is not valid!\n");
    return;
  }

  if (p->sort >= pa_sorts) {
    printf("ERROR Pa_EncodeProcess: Sort is not valid!\n");
    return;
  }

  if (p->numStates == 0) {
    printf("WARNING Pa_EncodeProcess: State table is empty.\n");
    return;
  }

  /*
  fprintf(stderr,"Pa_EncodeProcess before Pa_ExpandGates: %s\n",name);
  Pa_WriteProcess(name,0);
  */

  /* razsirimo prehode do drugih procesov */
  if (Pa_ExpandGates(p) == -1) {
    printf("ERROR Pa_EncodeProcess: Process cannot be expanded!\n");
    return;
  }

  /*
  fprintf(stderr,"Pa_EncodeProcess after Pa_ExpandGates: %s\n",name);
  Pa_WriteProcess(name,0);
  */

  /* po potrebi kodiramo sort */
  if (!pa_sortTable[p->sort].encoded) {
    /*
    printf("Encoding sort:\n");
    printf("  %s...",pa_sortTable[p->sort].name);
    */
    Pa_EncodeSort(pa_sortTable[p->sort].name);
    /*
    printf(" OK\n");
    */
  }

  /* REORDER STATES TO FIND UNREACHABLE STATES */

  /* AT FIRST, CREATE REORDERING TABLE */
  /* tabOrder[0] = new order of state 0 */
  /* tabOrder[1] = new order of state 1 */
  /* etc */

  tabOrder = (int *) malloc(p->numStates * sizeof(int));

  for (i=0; i <  p->numStates; i++) {
    tabOrder[i] = -1;
  }

  /* FIND REACHABLE STATES */
  m = w = p->numStates;

  /* COMMENT OUT THIS INITIALIZATION IF YOU WANT TO USE HEURISTIC */
  /**/
  m = w = 0;
  /**/

  tabOrder[p->initial] = w++;
  while (m != w) {
    m++;
    for (i=0; i<p->numTransitions; i++) {
      if (tabOrder[p->tableT[i].source] == m-1) {
        if (tabOrder[p->tableT[i].dest] == -1) {
          tabOrder[p->tableT[i].dest] = w++;
        }
      }
    }
  }

  /* UNREACHABLE STATES */
  for (i=0; i<p->numTransitions; i++) {
    if (tabOrder[p->tableT[i].source] == -1) {
      tabOrder[p->tableT[i].source] = w++;
      if (strncmp(name,"COPY_",5)) {
        printf("WARNING: unreachable state %s\n",p->tableS[p->tableT[i].source].name);
      }
    }
  }

  newNumStates = w; /* BECAUSE HEURISTIC CHANGES w */

  /* REORDERING HEURISTIC FOR MINIMIZATION OF BDD NODES */
  /* IF USING THIS, YOU HAVE TO COMMENT OUT THE MARKED INITIALIZATION */
  /* THEN, STATES WILL HAVE BIGGER SEQUENTIAL NUMBERS AS NECCESSARY */
  /* HERE WE CHANGE (REORDER) SEQUENTIAL NUMBERS TO GET GOOD REORDERING */
  /* I AM NOT SURE ABOUT THE CORRETNESS IF UNREACHABLE STATES EXIST */
  /* I AM NOT SURE ABOUT THE EFFICENCY OF THIS METHOD */
  /*
  w = 0;
  tabOrder[p->initial] = w++;
  for (i=0; i<pa_sortTable[p->sort].numActions; i++) {
    for (j=0; j<p->numTransitions; j++) {
      if ((p->tableT[j].action == i) &&
          (tabOrder[p->tableT[j].source] >= p->numStates)) {
            tabOrder[p->tableT[j].source] = w++;
      }
    }
    for (j=0; j<p->numTransitions; j++) {
      if ((p->tableT[j].action == i) &&
          (tabOrder[p->tableT[j].dest] >= p->numStates)) {
            tabOrder[p->tableT[j].dest] = w++;
      }
    }
  }
  */

  /* TEST */
  /*
  fprintf(stderr,"PROCESS %s STATE ORDER:\n",name);
  for (i=0; i<p->numStates; i++) {
    fprintf(stderr,"(%d)",tabOrder[i]);
  }
  fprintf(stderr,"\n");
  */

  /* UPDATE STATE TABLE! */

  newtableS = (Pa_State *) malloc (newNumStates * sizeof(Pa_State));
  for (i=0; i<p->numStates; i++) {
    if (tabOrder[i] != -1) newtableS[tabOrder[i]] = p->tableS[i];
  }
  free(p->tableS);
  p->tableS = newtableS;
  p->initial = tabOrder[p->initial];
  p->numStates = newNumStates;
  for (i=0; i<p->numTransitions; i++) {
    p->tableT[i].source = tabOrder[p->tableT[i].source];
    p->tableT[i].dest = tabOrder[p->tableT[i].dest];
  }

  free(tabOrder);

  /* dolocimo stevilo potrebnih spremenljivk za kodiranje stanj */
  n = 0;
  if (p->numStates == 1) n = 1;
  if (p->numStates > 1) n = (int)(0.9999999+log(p->numStates)/log(2.0));
  p->numVar = n;

  /* tvorimo spremenljivke in dolocimo utezi */
  tabVarR = (Bdd_Edge *) malloc(n * sizeof(Bdd_Edge));
  tabVarS = (Bdd_Edge* ) malloc(n * sizeof(Bdd_Edge));
  x = (Est_String) malloc(127);

  /* HERE IS GIVEN THE ORDER OF r,s,p,q VARIABLES */

  /* HERE, r,s,p,q ARE INTERCHANGEABLE */
  /**/
  w = 1;
  for (i=0; i<n; i++) {

    sprintf(x,"r%d<%s>",i,name);
    var = Bdd_FoaTerminal(x);
    Bdd_AddFormula(x,var);
    Pa_InitVariable(Bdd_GetVariable(var));
    pa_variableTable[Bdd_GetVariable(var)].weight = w;
    tabVarR[i] = var;

    sprintf(x,"s%d<%s>",i,name);
    var = Bdd_FoaTerminal(x);
    Bdd_AddFormula(x,var);
    Pa_InitVariable(Bdd_GetVariable(var));
    pa_variableTable[Bdd_GetVariable(var)].weight = w;
    tabVarS[i] = var;

    sprintf(x,"p%d<%s>",i,name);
    var = Bdd_FoaTerminal(x);
    Bdd_AddFormula(x,var);
    Pa_InitVariable(Bdd_GetVariable(var));
    pa_variableTable[Bdd_GetVariable(var)].weight = w;

    sprintf(x,"q%d<%s>",i,name);
    var = Bdd_FoaTerminal(x);
    Bdd_AddFormula(x,var);
    Pa_InitVariable(Bdd_GetVariable(var));
    pa_variableTable[Bdd_GetVariable(var)].weight = w;

    w = w * 2;
  }
  /**/

  /* HERE, r,p ARE INTERCHANGEABLE AND THEN s,q ARE INTERCHANGEABLE */
  /* THIS SOLUTION SEEMS TO BE LESS EFFICIENT AS THE PREVIOUS ONE */
  /*
  w = 1;
  for (i=0; i<n; i++) {

    sprintf(x,"r%d<%s>",i,name);
    var = Bdd_FoaTerminal(x);
    Bdd_AddFormula(x,var);
    Pa_InitVariable(Bdd_GetVariable(var));
    pa_variableTable[Bdd_GetVariable(var)].weight = w;
    tabVarR[i] = var;

    sprintf(x,"p%d<%s>",i,name);
    var = Bdd_FoaTerminal(x);
    Bdd_AddFormula(x,var);
    Pa_InitVariable(Bdd_GetVariable(var));
    pa_variableTable[Bdd_GetVariable(var)].weight = w;

    w = w * 2;
  }

  w = 1;
  for (i=0; i<n; i++) {
    sprintf(x,"s%d<%s>",i,name);
    var = Bdd_FoaTerminal(x);
    Bdd_AddFormula(x,var);
    Pa_InitVariable(Bdd_GetVariable(var));
    pa_variableTable[Bdd_GetVariable(var)].weight = w;
    tabVarS[i] = var;

    sprintf(x,"q%d<%s>",i,name);
    var = Bdd_FoaTerminal(x);
    Bdd_AddFormula(x,var);
    Pa_InitVariable(Bdd_GetVariable(var));
    pa_variableTable[Bdd_GetVariable(var)].weight = w;

    w = w * 2;
  }
  */

  free(x);

  /* make BDD for each state */
  /* CAREFULY: ith STATE MUST BE ENCODED WITH ith MINTERM! */
  for (i=0; i<p->numStates; i++) {
    p->tableS[i].bddR = EncodeMinterm(tabVarR, i, n-1, 0);
    p->tableS[i].bddS = EncodeMinterm(tabVarS, i, n-1, 0);
    Bdd_Fortify(p->tableS[i].bddR);
    Bdd_Fortify(p->tableS[i].bddS);
  }
  states = bdd_termFalse;

  for (i=0; i<p->numStates; i++) {
    if (strcmp(p->tableS[i].name,"")) {
      states = Bdd_ITE(states,bdd_termTrue,p->tableS[i].bddR);
    }
  }
  p->stateBDD = states; /* DOES NOT INCLUDE DELETED STATES! */
  Bdd_Fortify(p->stateBDD);

  /* zgradimo prehajalno relacijo */
  d = bdd_termFalse;
  for (i=0; i<p->numTransitions; i++) {

    /*
    fprintf(stderr,"FOR p->numTransitions: %d/%d\n",i,p->numTransitions);
    fprintf(stderr,"p->tableT[i].source = %d, p->tableT[i].action = %d, p->tableT[i].dest = %d\n",
                    p->tableT[i].source,p->tableT[i].action,p->tableT[i].dest);
    */

    if (p->tableT[i].action == -1) {
      fprintf(stderr,"ERROR Pa_EncodeProcess (i=%d): transition table wrong (action = -1).\n",i);
      fprintf(stderr,"p->tableT[i].source = %d (%s)\n",p->tableT[i].source,p->tableS[p->tableT[i].source].name);
      fprintf(stderr,"p->tableT[i].dest = %d (%s)\n",p->tableT[i].dest,p->tableS[p->tableT[i].dest].name);
      exit(1);
    } else {
      if (p->tableT[i].type) {
        e = Bdd_ITE(pa_sortTable[p->sort].a0,
                    pa_sortTable[p->sort].table[p->tableT[i].action].p,
                    bdd_termFalse);
      } else {
        e = Bdd_ITE(pa_sortTable[p->sort].a0,
                    bdd_termFalse,
                    pa_sortTable[p->sort].table[p->tableT[i].action].p);
      }
    }

    if ((p->tableT[i].source) == -1) {
      fprintf(stderr,"ERROR Pa_EncodeProcess (i=%d/%d): transition table wrong (source = -1).\n",i,p->numTransitions);
      fprintf(stderr,"p->tableT[i].dest = %d (%s)\n",p->tableT[i].dest,p->tableS[p->tableT[i].dest].name);
      exit(1);
    } else {
      e = Bdd_ITE(e,p->tableS[p->tableT[i].source].bddR,bdd_termFalse);
    }

    if ((p->tableT[i].dest) == -1) {
      fprintf(stderr,"ERROR Pa_EncodeProcess (i=%d/%d): transition table wrong (dest = -1).\n",i,p->numTransitions);
      fprintf(stderr,"p->tableT[i].source = %d (%s)\n",p->tableT[i].source,p->tableS[p->tableT[i].source].name);
      exit(1);
    } else {
      e = Bdd_ITE(e,p->tableS[p->tableT[i].dest].bddS,bdd_termFalse);
    }

    d = Bdd_ITE(d,bdd_termTrue,e);

  }
  Bdd_Fortify(d);
  p->d =d;

  /*
  fprintf(stderr,"Prehajalna relacija %s\n",name);
  Bdd_FunctionStat(p->d,stderr);
  */

  /* zgradimo stab BDD */
  d = bdd_termTrue;
  for(i=0; i<p->numVar; i++) {
    e = Bdd_ITE(tabVarR[i],tabVarS[i],Bdd_NOT(tabVarS[i]));
    d = Bdd_ITE(d,e,bdd_termFalse);
  }
  Bdd_Fortify(d);
  p->stab =d;

  free(tabVarR);
  free(tabVarS);

  p->encoded = 1;

  PaSaveProcStates(p);
  Bdd_SaveFormula("D_",name,p->d);
  if (p->initial != -1) {
    Bdd_SaveFormula("Initial_",name,p->tableS[p->initial].bddR);
  } else {
    Bdd_SaveFormula("Initial_",name,bdd_termNull);
  }
  Bdd_SaveFormula("S_",name,p->stateBDD);

  /* POMOZNI IZPISI */

  /*
  Pa_DecodeProcessStates(p,p->stateBDD,FALSE);
  Pa_DecodeProcessTR(p,p->d,FALSE);
  */
}

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

void
Pa_EncodeMultiProcesses(Est_String plist)
{
  Est_String list,name;

  if (!plist) {
    printf("\nError: Pa_EncodeMultiProcesses got null string!\n");
    return;
  }

  /* first process */
  list = strdup(plist);
  name = strtok(list," ");

  if (!name) {
    printf("\nError: Pa_EncodeMultiProcesses got empty list!\n");
    return;
  }

  Pa_EncodeProcess(name);

  /* other procesees */

  name = strtok(NULL," ");
  while (name) {
    Pa_EncodeProcess(name);
    name = strtok(NULL," ");
  }

  free(list);
}

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

int
Pa_ExpandGates(Pa_Process *p)
{
  Pa_Process *q;
  Pa_Sort *ps;
  Pa_Sort *qs;
  int i,j,num;
  Est_String gate,state;
  Est_Boolean repeat;
  int state1,action,type,state2;

  ps = &pa_sortTable[p->sort];

  do {
    repeat = FALSE;

    if (Pa_IsGate(p->tableS[p->initial].name)) {

      /* DEBUGGING */
      /*
      fprintf(stderr,"Pa_ExpandGates INITIAL: %s\n",p->tableS[p->initial].name);
      */

      num = Pa_FindProcess(p->tableS[p->initial].name);

      if (num == -1) {

        /* PROCESS DOES NOT EXISTS */
        /* IT WILL NOT BE EXPANDED */

      } else {

        q = &pa_processTable[num];
        qs = &pa_sortTable[q->sort];

        Pa_DeleteStateProcess(p,p->initial);

        /* COPY ACTIONS */
        for (j=0; j<qs->numActions; j++) {

          /* DEBUGGING */
          /*
          fprintf(stderr,"Pa_ExpandGates COPY ACTIONS: %s\n",qs->table[j].name);
          */

          if (Pa_FOASortAction(ps,qs->table[j].name) == -1) {
            return -1;
          }
        }

        /* COPY STATES */
        for (j=0; j<q->numStates; j++) {
          state = q->tableS[j].name;
          if (strcmp(state,"")) {
            if (Pa_IsGate(state)) {
              if (j == q->initial) {
                p->initial = Pa_FOAGateProcess(p,state);
                repeat = TRUE;
              } else {
                Pa_FOAGateProcess(p,state);
              }
            } else {
              if (j == q->initial) {
                p->initial = Pa_FOAStateProcess(p,state);
              } else {
                Pa_FOAStateProcess(p,state);
              }
            }
          }
        }

        for (j=0; j<q->numTransitions; j++) {
          state1 = Pa_FindStateProcess(p,q->tableS[q->tableT[j].source].name);
          action = Pa_FindSortAction(ps,qs->table[q->tableT[j].action].name);
          type = q->tableT[j].type;
          state2 = Pa_FindStateProcess(p,q->tableS[q->tableT[j].dest].name);
          Pa_FOATransition(p,state1,action,type,state2);
        }

      }
    }

  } while (repeat);

  do {
    repeat = FALSE;

    for (i=0; i<p->numTransitions; i++) {
      gate = p->tableS[p->tableT[i].dest].name;

      if (Pa_IsGate(gate)) {

        /* DEBUGGING */
        /*
        printf("GATE: %s\n",gate);
        */

        num = Pa_FindProcess(gate);
        if (num == -1) {

          /* PROCESS DOES NOT EXISTS */
          /* IT WILL BE RECOGNIZED AS AN EMPTY PROCESS */

          concat(&p->tableS[p->tableT[i].dest].name,"<");
          concat(&p->tableS[p->tableT[i].dest].name,p->name); /* must become non-gate */
          concat(&p->tableS[p->tableT[i].dest].name,">");

        } else {

          q = &pa_processTable[num];
          qs = &pa_sortTable[q->sort];

          state = q->tableS[q->initial].name;
          num = Pa_FindStateProcess(p,state);

          /* DEBUGGING */
          /*
          printf("state = %s\n",state);
          printf("num = %d\n",num);
          */

          if (num != -1) {

            /*
            printf("DESTINATION WILL BE CHANGED\n");
            */

            p->tableT[i].dest = num;

          } else {

            /*
            printf("EXTERNAL PROCESS WILL BE INCLUDED\n");
            */

            repeat = TRUE;

            /* COPY ACTIONS */
            for (j=0; j<qs->numActions; j++) {
              if (Pa_FOASortAction(ps,qs->table[j].name) == -1) {
                return -1;
              }
            }

            /* COPY STATES */
            for (j=0; j<q->numStates; j++) {
              state = q->tableS[j].name;

              if (strcmp(state,"")) {
                if (Pa_IsGate(state)) {
                  Pa_FOAGateProcess(p,state);
                } else {
                  Pa_FOAStateProcess(p,state);
                }
              }
            }

            for (j=0; j<q->numTransitions; j++) {
              state1 = Pa_FindStateProcess(p,q->tableS[q->tableT[j].source].name);
              action = Pa_FindSortAction(ps,qs->table[q->tableT[j].action].name);
              type = q->tableT[j].type;
              state2 = Pa_FindStateProcess(p,q->tableS[q->tableT[j].dest].name);
              Pa_FOATransition(p,state1,action,type,state2);
            }

            p->tableT[i].dest = Pa_FindStateProcess(p,q->tableS[q->initial].name);
          }

          /* DEBUGGING */
          /*
          fprintf(stderr,"Process after this change\n");
          Pa_WriteProcess(p->name,0);
          */

        }
      }
    }

  } while (repeat);

  return 0;
}

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

int
Pa_Process2Composition(Est_String name)
{
  int procnum;
  int compnum;
  Pa_Process *p;
  Pa_Composition *c;

  procnum = Pa_FindProcess(name);
  if (procnum == -1) return -1;

  p  = &pa_processTable[procnum];
  if (!p->encoded) return -1;

  compnum = Pa_AddNewComposition(name,-1,1,0);
  c = &pa_compositionTable[compnum];

  c->tableP[0] = procnum;
  c->sort = p->sort;
  c->initialBDD = p->tableS[p->initial].bddR;
  c->stateBDD = p->stateBDD;
  c->transitionBDD = p->d;
  /* c->stab = p->stab; */

  return compnum;
}

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

int
Pa_Composition2Process(Est_String name, Est_Boolean full)
{
  int procnum;
  int compnum;
  Pa_Process *p;
  Pa_Composition *c;
  int *decodingTableR,*decodingTableS;
  int i,j,maxAction,maxState;
  Bdd_Edge substPR,substQS,sup1,sup2;

  compnum = Pa_FindComposition(name);
  if (compnum == -1) return -1;

  c = &pa_compositionTable[compnum];

  if (c->onthefly) {
    printf("\nERROR: Cannot transform on-the-fly composition\n");
    return -1;
  }

  /* WARNING: AddNewProcess calls realloc(pa_processTable) */
  procnum = Pa_AddNewProcess(name);
  p = &pa_processTable[procnum];

  p->compname = strdup(name);
  p->sort = c->sort;

  if (full) {

    decodingTableR = (int *) calloc (2 * c->numProcesses, sizeof(int));
    decodingTableS = (int *) calloc (2 * c->numProcesses, sizeof(int));

    maxAction = 1;
    for (i=0; i<pa_sortTable[c->sort].numVar; i++) maxAction = maxAction * 2;

    for (i=0; i<c->numProcesses; i++) {
      maxState = 1;
      for (j=0; j<pa_processTable[c->tableP[i]].numVar; j++)
        maxState = maxState * 2;
      decodingTableR[2*i] = 0;
      decodingTableR[2*i+1] = maxState-1;
      decodingTableS[2*i] = 0;
      decodingTableS[2*i+1] = maxState-1;
    }

    setproccomp(c);
    Composition2ProcessRAS(c,c->transitionBDD,bdd_termTrue.mark,0,
                         maxAction-1,decodingTableR,decodingTableS,procnum);

    pa_processTable[procnum].initial =
      Pa_FOAComposedStateProcess(&pa_processTable[procnum],c->initialBDD,name);

    Pa_EncodeProcess(name);

    free(decodingTableR);
    free(decodingTableS);

    return procnum;

  } else {

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

    decodingTableR = (int *) calloc (2 * c->numProcesses, sizeof(int));

    for (i=0; i<c->numProcesses; i++) {
      maxState = 1;
      for (j=0; j<pa_processTable[c->tableP[i]].numVar; j++)
        maxState = maxState * 2;
      decodingTableR[2*i] = 0;
      decodingTableR[2*i+1] = maxState-1;
    }

    setproccomp(c);
    Composition2ProcessR(c,c->stateBDD,bdd_termTrue.mark,
                         decodingTableR,procnum);

    Pa_EncodeProcess(name);

    /* *************** */
    /* ORIGINAL METHOD */
    /* *******************************************************************/

    substPR = bdd_termFalse;
    for (i=0; i<p->numStates; i++) {
      sup1 = Bdd_RelOpSimple(p->tableS[i].bddComp,"R2P",TRUE);
      sup2 = Bdd_ITE(p->tableS[i].bddR,sup1,bdd_termFalse);
      substPR = Bdd_ITE(substPR,bdd_termTrue,sup2);
      Bdd_IncCounter();
      Bdd_Fresh(substPR);
    }
    /******************************************************************* */

    /* ****************** */
    /* ALTERNATIVE METHOD */
    /* ********************************************************************

    substPR = bdd_termTrue;
    for (i=0; i<p->numStates; i++) {
      sup1 = Bdd_RelOpSimple(p->tableS[i].bddComp,"R2P",TRUE);
      sup2 = Bdd_ITE(p->tableS[i].bddR,sup1,Bdd_NOT(sup1));
      substPR = Bdd_ITE(substPR,sup2,bdd_termFalse);
      Bdd_IncCounter();
      Bdd_Fresh(substPR);
    }

    ******************************************************************** */

    Bdd_Fortify(substPR);
    Bdd_IncCounter();

    substQS = Bdd_RelOpSimple(substPR,"P2Q R2S",TRUE);

    Bdd_Fortify(substQS);
    Bdd_IncCounter();

    sup1 = Bdd_RelOpSimple(c->transitionBDD,"R2P S2Q",TRUE);

    Bdd_IncCounter();
    Bdd_Fresh(sup1);

    sup2 = Bdd_RelOp(substPR,sup1,"#AND Ex xP",TRUE);

    Bdd_IncCounter();
    Bdd_Fresh(sup2);

    p->d = Bdd_RelOp(substQS,sup2,"#AND Ex xQ",TRUE);
    Bdd_Fortify(p->d);
    Bdd_SaveFormula("D_",name,p->d);

    p->numTransitions = Pa_DecodeProcessTR(p,p->d,FALSE);

    free(decodingTableR);

    return procnum;
  }
}

/**Function****************************************************************
  Synopsis    []
  Description [Write and/or return the number of actions.]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

int
Pa_DecodeSortActions(Pa_Sort *s, Bdd_Edge F, Est_Boolean write)
{
  int i,maxAction;
  int number;

  if(s->encoded) {

    maxAction = 1;
    for (i=0; i<s->numVar; i++) maxAction= maxAction * 2;
    number = DecodeSortBddA(s, F, bdd_termTrue.mark, 0, maxAction-1, NULL, write);

  } else {
    printf("Sort %s is not encoded.\n",s->name);
    number = -1;
  }

  return number;
}

/**Function****************************************************************
  Synopsis    []
  Description [Return the string containing decoded actions.]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

Est_String
Pa_DecodeSortActions1(Pa_Sort *s, Bdd_Edge F, Est_Boolean write)
{
  int i,maxAction;
  int number;
  Est_String act;

  act = strdup("");
  if(s->encoded) {

    maxAction = 1;
    for (i=0; i<s->numVar; i++) maxAction= maxAction * 2;
    number = DecodeSortBddA(s, F, bdd_termTrue.mark, 0, maxAction-1, &act, write);
    if (number == 0) {
      printf("\nDecodeSortBdd == 0\n"); /* make compiler happy */
    }

  } else {
    printf("Sort %s is not encoded.\n",s->name);
  }

  return act;
}

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

void
Pa_DecodeProcess(Est_String name, Est_Boolean write)
{
  Pa_Process *p;
  int i;
  int number;

  i = Pa_FindProcess(name);
  if (i == -1) return;

  p = &pa_processTable[i];

  if(p->encoded) {
    printf("\nPROCESS %s\n",p->name);
    printf("Initial state: ");
    printstate(p->tableS[p->initial].name);
    printf("\n");
    if (write) {
      printf("Transitions:\n");
    }

    number = Pa_DecodeProcessTR(p, p->d, write);

    if (!write) {
      printf("Number of transitions = %d.\n",number);
    }

  } else {
    printf("Process %s is not encoded.\n",p->name);
  }
}

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

int
Pa_DecodeProcessStates(Pa_Process *p, Bdd_Edge F, Est_Boolean write)
{
  int i,maxState;
  int number;

  if(p->encoded) {

    maxState = 1;
    for (i=0; i<p->numVar; i++) maxState= maxState * 2;
    number = DecodeProcessBddR(p,F,bdd_termTrue.mark,0,maxState-1,write);

  } else {
    printf("Process %s is not encoded.\n",p->name);
    number = -1;
  }

  return number;
}

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

int
Pa_DecodeProcessTR(Pa_Process *p, Bdd_Edge F, Est_Boolean write)
{
  int i,maxAction,maxState;
  int number;

  if(p->encoded) {
    maxAction = 1;
    for (i=0; i<pa_sortTable[p->sort].numVar; i++) maxAction = maxAction * 2;
    maxState = 1;
    for (i=0; i<p->numVar; i++) maxState= maxState * 2;

    number = DecodeProcessBddRAS(p, F, bdd_termTrue.mark, 0, maxState-1,
                                 0, maxAction-1, 0, maxState-1, write);

  } else {
    printf("Process %s is not encoded.\n",p->name);
    number = -1;
  }

  return number;
}

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

void
Pa_DecodeComposition(Est_String name, Est_Boolean write)
{
  Pa_Composition *c;
  int i;
  int number;

  i = Pa_FindComposition(name);
  if (i == -1) return;

  c = &pa_compositionTable[i];

  number = Pa_DecodeCompTR(c, c->transitionBDD, write);

  if (!write) {
    printf("Number of transitions = %d.\n",number);
  }
}

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

int
Pa_DecodeCompStates(Pa_Composition *c, Bdd_Edge F, Est_Boolean write)
{
  int *decodingTableR;
  int i,j,maxState;
  int number;

  /*
  if (write && c->onthefly) {
    printf("Warning: This is an on-the-fly composition\n");
  }
  */

  decodingTableR = (int *) calloc (2 * c->numProcesses, sizeof(int));

  for (i=0; i<c->numProcesses; i++) {
    maxState = 1;
    for (j=0; j<pa_processTable[c->tableP[i]].numVar; j++)
      maxState = maxState * 2;
    decodingTableR[2*i] = 0;
    decodingTableR[2*i+1] = maxState-1;
  }

  setproccomp(c);
  number = DecodeCompBddR(c, F, bdd_termTrue.mark, decodingTableR, write);

  free(decodingTableR);

  return number;
}

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

int
Pa_DecodeCompTR(Pa_Composition *c, Bdd_Edge F, Est_Boolean write)
{
  int *decodingTableR;
  int *decodingTableS;
  int i,j,maxAction,maxState;
  int number;

  /*
  if (write && c->onthefly) {
    printf("Warning: This is an on-the-fly composition\n");
  }
  */

  decodingTableR = (int *) calloc (2 * c->numProcesses, sizeof(int));
  decodingTableS = (int *) calloc (2 * c->numProcesses, sizeof(int));

  maxAction = 1;
  for (i=0; i<pa_sortTable[c->sort].numVar; i++) maxAction = maxAction * 2;

  for (i=0; i<c->numProcesses; i++) {
    maxState = 1;
    for (j=0; j<pa_processTable[c->tableP[i]].numVar; j++)
      maxState = maxState * 2;
    decodingTableR[2*i] = 0;
    decodingTableR[2*i+1] = maxState-1;
    decodingTableS[2*i] = 0;
    decodingTableS[2*i+1] = maxState-1;
  }

  setproccomp(c);
  number = DecodeCompBddRAS(c, F, bdd_termTrue.mark, 0, maxAction-1,
                            decodingTableR, decodingTableS, write);

  free(decodingTableR);
  free(decodingTableS);

  return number;
}

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

int
Pa_DecodeProcProcPair(Pa_Process *p1, Pa_Process *p2, Bdd_Edge F,
                      Est_Boolean write)
{
  int i,maxState1,maxState2;
  int number;

  if ((p1->encoded) && (p2->encoded)) {
    maxState1 = 1;
    for (i=0; i<p1->numVar; i++) maxState1 = maxState1 * 2;
    maxState2 = 1;
    for (i=0; i<p2->numVar; i++) maxState2 = maxState2 * 2;

    number = DecodeProcProcPairBddRP(p1, p2, F, bdd_termTrue.mark,
                                     0, maxState1-1, 0, maxState2-1, write);

  } else {
    printf("Processes are not encoded.\n");
    number = -1;
  }

  return number;
}

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

int
Pa_DecodeCompProcPair(Pa_Composition *c, Pa_Process *p, Bdd_Edge F,
                      Est_Boolean write)
{
  int i,j,maxState1,maxState2;
  int *decodingTableR;
  int number;

  /*
  if (write && c->onthefly) {
    printf("Warning: This is an on-the-fly composition\n");
  }
  */

  decodingTableR = (int *) calloc (2 * c->numProcesses, sizeof(int));

  if(p->encoded) {
    maxState1 = 1;
    for (i=0; i<p->numVar; i++) maxState1 = maxState1 * 2;

    for (i=0; i<c->numProcesses; i++) {
      maxState2 = 1;
      for (j=0; j<pa_processTable[c->tableP[i]].numVar; j++)
        maxState2 = maxState2 * 2;
      decodingTableR[2*i] = 0;
      decodingTableR[2*i+1] = maxState2-1;
    }

    setproccomp(c);
    number = DecodeCompProcPairBddRP(c, p, F, bdd_termTrue.mark,
                                 decodingTableR, 0, maxState1-1, write);

  } else {
    printf("Process is not encoded.\n");
    number = -1;
  }

  free(decodingTableR);

  return number;
}

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

int
Pa_DecodeCompCompPair(Pa_Composition *c1, Pa_Composition *c2, Bdd_Edge F,
                      Est_Boolean write)
{
  int i,j,maxState;
  int *decodingTableR,*decodingTableS;
  int number;

  /*
  if (write && (c1->onthefly || c2->onthefly)) {
    printf("Warning: This is an on-the-fly composition\n");
  }
  */

  decodingTableR = (int *) calloc (2 * c1->numProcesses, sizeof(int));
  decodingTableS = (int *) calloc (2 * c2->numProcesses, sizeof(int));

  for (i=0; i<c1->numProcesses; i++) {
    maxState = 1;
    for (j=0; j<pa_processTable[c1->tableP[i]].numVar; j++)
      maxState = maxState * 2;
    decodingTableR[2*i] = 0;
    decodingTableR[2*i+1] = maxState-1;
  }

  for (i=0; i<c2->numProcesses; i++) {
    maxState = 1;
    for (j=0; j<pa_processTable[c2->tableP[i]].numVar; j++)
      maxState = maxState * 2;
    decodingTableS[2*i] = 0;
    decodingTableS[2*i+1] = maxState-1;
  }

  setproccomp(c1);
  setproccomp(c2);
  number = DecodeCompCompPairBddRP(c1, c2, F, bdd_termTrue.mark,
                                   decodingTableR, decodingTableS, write);

  free(decodingTableR);
  free(decodingTableS);

  return number;
}

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

Bdd_Edge
Pa_ExtractProcTransition(Pa_Process *p, Bdd_Edge f)
{
  Est_Boolean OK;
  Bdd_Edge r,a,s,ras;
  int minR,minA,minS;

  if (Bdd_isEqv(f,bdd_termFalse)) {
    return bdd_termFalse;
  }

  minR = 0;
  minA = 0;
  minS = 0;

  OK = ExtractProcTransition(p,f,bdd_termTrue.mark,&minR,&minA,&minS);

  if (!OK) {
    fprintf(stderr,"ExtractProcTransition return FALSE!\n");
    exit(1);
  }

  /*
  printf("Extract state R:");
  printf(p->tableS[minR].name);
  */

  r = p->tableS[minR].bddR;

  /*
  printf("\nExtract action A:");
  printf(pa_sortTable[p->sort].table[(minA)/2].name);
  if (minA % 2) printf("!, "); else printf("?, ");
  */

  a = pa_sortTable[p->sort].table[(minA)/2].p;
  if (minA % 2) {
    a = Bdd_ITE(pa_sortTable[p->sort].a0,a,bdd_termFalse);
  } else {
    a = Bdd_ITE(pa_sortTable[p->sort].a0,bdd_termFalse,a);
  }

  /*
  printf("\nExtract state S:");
  printf(p->tableS[minS].name);
  printf("\n");
  */

  s = p->tableS[minS].bddS;

  ras = Bdd_ITE(r,s,bdd_termFalse);
  ras = Bdd_ITE(ras,a,bdd_termFalse);

  return ras;
}


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

Bdd_Edge
Pa_ExtractCompTransition(Pa_Composition *c, Bdd_Edge f)
{
  Est_Boolean OK;
  Bdd_Edge a,r,r1,s,s1,ras;
  int i;
  int minA;
  int *decodingTableR;
  int *decodingTableS;

  if (Bdd_isEqv(f,bdd_termFalse)) {
    return bdd_termFalse;
  }

  minA = 0;

  decodingTableR = (int *) calloc (2 * c->numProcesses, sizeof(int));
  decodingTableS = (int *) calloc (2 * c->numProcesses, sizeof(int));

  for (i=0; i<c->numProcesses; i++) {
    decodingTableR[2*i] = 0;     /* minR */
    decodingTableR[2*i+1] = -1;  /* maxR is not used */
    decodingTableS[2*i] = 0;     /* minS */
    decodingTableS[2*i+1] = -1;  /* maxS is not used */
  }

  setproccomp(c);
  OK = ExtractCompTransition(c,f,bdd_termTrue.mark,&minA,decodingTableR,
                             decodingTableS);

  if (!OK) {
    fprintf(stderr,"ExtractCompTransition return FALSE!\n");
    exit(1);
  }

  r = bdd_termTrue;
  for (i=0; i<c->numProcesses; i++) {

    /*
    fprintf(stderr,"\nExtract state R:");
    fprintf(stderr,pa_processTable[c->tableP[i]].tableS[decodingTableR[2*i]].name);
    */

    r1 = pa_processTable[c->tableP[i]].tableS[decodingTableR[2*i]].bddR;
    r = Bdd_ITE(r,r1,bdd_termFalse);  /* r = r * r1 */
  }

  /*
  fprintf(stderr,"\nExtract action A:");
  fprintf(stderr," (c->sort = %d, minA = %d) ",c->sort,minA);
  fprintf(stderr," (pa_sortTable[c->sort].numActions = %d) ",pa_sortTable[c->sort].numActions);
  fprintf(stderr,pa_sortTable[c->sort].table[(minA)/2].name);
  if (minA % 2) fprintf(stderr,"!, "); else fprintf(stderr,"?, ");
  */

  a = pa_sortTable[c->sort].table[(minA)/2].p;
  if (minA % 2) {
    a = Bdd_ITE(pa_sortTable[c->sort].a0,a,bdd_termFalse);
  } else {
    a = Bdd_ITE(pa_sortTable[c->sort].a0,bdd_termFalse,a);
  }

  s = bdd_termTrue;
  for (i=0; i<c->numProcesses; i++) {

    /*
    fprintf(stderr,"\nExtract state S:");
    fprintf(stderr,pa_processTable[c->tableP[i]].tableS[decodingTableS[2*i]].name);
    */

    s1 = pa_processTable[c->tableP[i]].tableS[decodingTableS[2*i]].bddS;
    s = Bdd_ITE(s,s1,bdd_termFalse);  /* s = s * s1 */
  }

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

  free(decodingTableR);
  free(decodingTableS);

  ras = Bdd_ITE(r,s,bdd_termFalse);
  ras = Bdd_ITE(ras,a,bdd_termFalse);

  return ras;
}

/**Function****************************************************************
  Synopsis    []
  Description [Return BDD for one state in set F]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

Bdd_Edge
Pa_ExtractProcState(Pa_Process *p, Bdd_Edge f)
{
  Est_Boolean OK;
  Bdd_Edge r;
  int minR;

  if (Bdd_isEqv(f,bdd_termFalse)) {
    return bdd_termFalse;
  }

  minR = 0;

  OK = ExtractProcState(p,f,bdd_termTrue.mark,&minR);

  if (!OK) {
    fprintf(stderr,"Pa_ExtractProcState got FALSE from ExtractProcState!\n");
    exit(1);
  }

  /*
  printf("Extract state R:");
  printf(p->tableS[minR].name);
  printf("\n");
  */

  r = p->tableS[minR].bddR;

  return r;
}

/**Function****************************************************************
  Synopsis    []
  Description [Return seq for one state in set F]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

int
Pa_EnumerateProcState(Pa_Process *p, Bdd_Edge f)
{
  Est_Boolean OK;
  int minR;

  if (Bdd_isEqv(f,bdd_termFalse)) {
    return -1;
  }

  minR = 0;

  OK = ExtractProcState(p,f,bdd_termTrue.mark,&minR);

  if (!OK) {
    fprintf(stderr,"Pa_EnumerateProcState got FALSE from ExtractProcState!\n");
    exit(1);
  }

  return minR;
}

/**Function****************************************************************
  Synopsis    []
  Description [Return BDD for one state in set F]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

Bdd_Edge
Pa_ExtractCompState(Pa_Composition *c, Bdd_Edge f)
{
  Est_Boolean OK;
  Bdd_Edge r,r1;
  int i;
  int *decodingTableR;

  if (Bdd_isEqv(f,bdd_termFalse)) {
    return bdd_termFalse;
  }

  decodingTableR = (int *) calloc (2 * c->numProcesses, sizeof(int));

  for (i=0; i<c->numProcesses; i++) {
    decodingTableR[2*i] = 0;     /* minR */
    decodingTableR[2*i+1] = -1;  /* maxR is not used */
  }

  setproccomp(c);
  OK = ExtractCompState(c,f,bdd_termTrue.mark,decodingTableR);

  if (!OK) {
    fprintf(stderr,"Pa_ExtractCompState got FALSE from ExtractCompState!\n");
    exit(1);
  }

  /*
  printf("Extract state R:");
  */

  r = bdd_termTrue;
  for (i=0; i<c->numProcesses; i++) {
    r1 = pa_processTable[c->tableP[i]].tableS[decodingTableR[2*i]].bddR;
    /*
    printf(pa_processTable[c->tableP[i]].tableS[decodingTableR[2*i]].name);
    */
    r = Bdd_ITE(r,r1,bdd_termFalse);  /* r = r * r1 */
  }

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

  free(decodingTableR);

  return r;
}


/**Function****************************************************************
  Synopsis    []
  Description [Return BDD for one action in set F]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

Bdd_Edge
Pa_ExtractSortAction(Pa_Sort *s, Bdd_Edge f)
{
  Est_Boolean OK;
  Bdd_Edge r;
  int minA;

  if (Bdd_isEqv(f,bdd_termFalse)) {
    return bdd_termFalse;
  }

  minA = 0;

  OK = ExtractSortAction(s,f,bdd_termTrue.mark,&minA);

  if (!OK) {
    fprintf(stderr,"Pa_ExtractSortAction got FALSE from ExtractSortAction!\n");
    exit(1);
  }

  /*
  printf("Extract action A:");
  printf(s->table[(minA)/2].name);
  if (minA % 2) printf("!"); else printf("?");
  printf("\n");
  */

  r = s->table[(minA)/2].p;

  return r;
}

/**Function****************************************************************
  Synopsis    []
  Description [Return seq for one action in set F]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

int
Pa_EnumerateSortAction(Pa_Sort *s, Bdd_Edge f)
{
  Est_Boolean OK;
  int minA;

  if (Bdd_isEqv(f,bdd_termFalse)) {
    return -1;
  }

  minA = 0;

  OK = ExtractSortAction(s,f,bdd_termTrue.mark,&minA);

  if (!OK) {
    fprintf(stderr,"Pa_EnumerateSortAction got FALSE from ExtractSortAction!\n");
    exit(1);
  }

  return minA;
}

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

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

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

static Bdd_Edge
EncodeMinterm(Bdd_Edge *tabVar, int n, int i, int min)
{
  int w;

  if (i < min) return bdd_termTrue;
  w = getWeight(tabVar[i]);
  if (w <= n) {
    return Bdd_ITE(tabVar[i],EncodeMinterm(tabVar,n-w,i-1,min),bdd_termFalse);
  } else {
    return Bdd_ITE(tabVar[i],bdd_termFalse,EncodeMinterm(tabVar,n,i-1,min));
  }
}

/**Function****************************************************************
  Synopsis    []
  Description [States are encoded with variables r]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

static void
Composition2ProcessR(Pa_Composition *comp, Bdd_Edge F, Est_Boolean mark,
                     int *decodingTableR, int procnum)
{
  int i,old;
  static int j;   /* STATIC TO MINIMIZE STACK PROBLEMS */
  static int fS;  /* STATIC TO MINIMIZE STACK PROBLEMS */
  static char ch; /* STATIC TO MINIMIZE STACK PROBLEMS */

  if (F.mark) mark = (!mark);
  if (Bdd_isTerminal(F)) {
    if (!mark) {
      fS = 1;
      for (j=0; j<pa_processTable[comp->tableP[0]].numVar; j++) fS = fS * 2;
      CompStates2ProcStates(comp,0,decodingTableR,decodingTableR[0],
                            decodingTableR[1],fS,bdd_termTrue,procnum);
    }
  } else {
    ch = Bdd_GetVariableChar(F);
    switch (ch) {
      case 'r': {
              i = getProcComp(F);

                  old = decodingTableR[2*i+1]; /* maxR */
                  decodingTableR[2*i+1] =
                    decodingTableR[2*i+1] - getWeight(F); /* maxR - weight */
                  Composition2ProcessR(
                    comp,Bdd_GetElse(F),mark,decodingTableR,procnum);
                  decodingTableR[2*i+1] = old;

                  old = decodingTableR[2*i]; /* minR */
                  decodingTableR[2*i] =
                    decodingTableR[2*i] + getWeight(F); /* minR + weight */
                  Composition2ProcessR(
                    comp,Bdd_GetThen(F),mark,decodingTableR,procnum);
                  decodingTableR[2*i] = old;

                  break;
                }
    }
  }
}

/**Function****************************************************************
  Synopsis    []
  Description [Transition relation is encoded with variables r,a,s.]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

void
Composition2ProcessRAS(Pa_Composition *comp, Bdd_Edge F, Est_Boolean mark,
                    int minA, int maxA, int *decodingTableR,
                    int *decodingTableS, int procnum)
{
  int i,old;
  static int j;   /* STATIC TO MINIMIZE STACK PROBLEMS */
  static int fS;  /* STATIC TO MINIMIZE STACK PROBLEMS */
  static int fA;  /* STATIC TO MINIMIZE STACK PROBLEMS */
  static char ch; /* STATIC TO MINIMIZE STACK PROBLEMS */

  if (F.mark) mark = (!mark);
  if (Bdd_isTerminal(F)) {
    if (!mark) {
      fS = 1;
      for (j=0; j<pa_processTable[comp->tableP[0]].numVar; j++) fS = fS * 2;
      fA = 1;
      for (j=1; j<pa_sortTable[comp->sort].numVar; j++) fA = fA * 2;
      CompTR2ProcTR(comp,0,0,decodingTableR,decodingTableS,minA,
                       maxA,decodingTableR[0],decodingTableR[1],
                       decodingTableS[0],decodingTableS[1],fA,fS,fS,
                       bdd_termTrue,bdd_termTrue,procnum);
    }
  } else {
    ch = Bdd_GetVariableChar(F);
    switch (ch) {
      case 'r': {
              i = getProcComp(F);

                  old = decodingTableR[2*i+1]; /* maxR */
                  decodingTableR[2*i+1] =
                    decodingTableR[2*i+1] - getWeight(F); /* maxR - weight */
                  Composition2ProcessRAS(comp,Bdd_GetElse(F),mark,minA,maxA,
                                       decodingTableR,decodingTableS,procnum);
                  decodingTableR[2*i+1] = old;

                  old = decodingTableR[2*i]; /* minR */
                  decodingTableR[2*i] =
                    decodingTableR[2*i] + getWeight(F); /* minR + weight */
                  Composition2ProcessRAS(comp,Bdd_GetThen(F),mark,minA,maxA,
                                       decodingTableR,decodingTableS,procnum);
                  decodingTableR[2*i] = old;

                  break;
                }
      case 's': {
              i = getProcComp(F);

                  old = decodingTableS[2*i+1]; /* maxR */
                  decodingTableS[2*i+1] =
                    decodingTableS[2*i+1] - getWeight(F); /* maxS - weight */
                  Composition2ProcessRAS(comp,Bdd_GetElse(F),mark,minA,maxA,
                                       decodingTableR,decodingTableS,procnum);
                  decodingTableS[2*i+1] = old;

                  old = decodingTableS[2*i]; /* minS */
                  decodingTableS[2*i] =
                    decodingTableS[2*i] + getWeight(F); /* minS + weight */
                  Composition2ProcessRAS(comp,Bdd_GetThen(F),mark,minA,maxA,
                                       decodingTableR,decodingTableS,procnum);
                  decodingTableS[2*i] = old;

                  break;
                }
      case 'a': {
                  Composition2ProcessRAS(comp,Bdd_GetElse(F),mark,minA,maxA-getWeight(F),
                                       decodingTableR,decodingTableS,procnum);

                  Composition2ProcessRAS(comp,Bdd_GetThen(F),mark,minA+getWeight(F),maxA,
                                       decodingTableR,decodingTableS,procnum);
                  break;
                }
    }
  }
}

/**Function****************************************************************
  Synopsis    []
  Description [Actions are encoded with variables a]
  SideEffects [If act==NULL and write=false then not create and not write out
               If act==NULL and write=true then not create and write out
               If act!=NULL and write=false then create and not write out
               If act!=NULL and write=true then create and write out]
  SeeAlso     []
  ************************************************************************/

static int
DecodeSortBddA(Pa_Sort *sort, Bdd_Edge F, Est_Boolean mark,
               int minA, int maxA, Est_String *act, Est_Boolean write)
{
  Est_String act1;
  int number;
  static char ch;  /* STATIC TO MINIMIZE STACK PROBLEMS */

  number = 0;
  if (F.mark) mark = (!mark);
  if (Bdd_isTerminal(F)) {
    if (!mark) {
       if (act) {
         act1 = strdup("");
         number = DecodeSortAction(sort,minA,maxA,&act1,write);
         concat(act,act1);
         free(act1);
       } else {
         number = DecodeSortAction(sort,minA,maxA,NULL,write);
       }
    }
  } else {
    ch = Bdd_GetVariableChar(F);
    switch (ch) {
      case 'a':
        {
          number = number +
            DecodeSortBddA(sort,Bdd_GetElse(F),mark,minA,maxA-getWeight(F),act,write);
          number = number +
            DecodeSortBddA(sort,Bdd_GetThen(F),mark,minA+getWeight(F),maxA,act,write);
          break;
        }
    }
  }

  return number;
}


/**Function****************************************************************
  Synopsis    []
  Description [States are encoded with variables r]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

static int
DecodeProcessBddR(Pa_Process *proc, Bdd_Edge F, Est_Boolean mark,
                  int minR, int maxR, Est_Boolean write)
{
  int number;
  static char ch;  /* STATIC TO MINIMIZE STACK PROBLEMS */

  number = 0;
  if (F.mark) mark = (!mark);
  if (Bdd_isTerminal(F)) {
    if (!mark) number = DecodeProcessState(proc,minR,maxR,write);
  } else {
    ch = Bdd_GetVariableChar(F);
    switch (ch) {
      case 'r':
        {
          number = number +
            DecodeProcessBddR(proc,Bdd_GetElse(F),mark,minR,maxR-getWeight(F),write);
          number = number +
            DecodeProcessBddR(proc,Bdd_GetThen(F),mark,minR+getWeight(F),maxR,write);
          break;
        }
    }
  }

  return number;
}

/**Function****************************************************************
  Synopsis    []
  Description [Transition relation is encoded with variables r,a,s]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

static int
DecodeProcessBddRAS(Pa_Process *proc, Bdd_Edge F, Est_Boolean mark,
                    int minR, int maxR, int minA, int maxA,
                    int minS, int maxS, Est_Boolean write)
{
  int number;
  static char ch;  /* STATIC TO MINIMIZE STACK PROBLEMS */

  number = 0;
  if (F.mark) mark = (!mark);
  if (Bdd_isTerminal(F)) {
    if (!mark)
      number = DecodeProcessTR(proc,minR,maxR,minA,maxA,minS,maxS,write);
  } else {
    ch = Bdd_GetVariableChar(F);
    switch (ch) {
      case 'r':
        {
          number = number + DecodeProcessBddRAS(proc,Bdd_GetElse(F),mark,
                                      minR,maxR-getWeight(F),
                                      minA,maxA,minS,maxS,write);
          number = number + DecodeProcessBddRAS(proc,Bdd_GetThen(F),mark,
                                      minR+getWeight(F),maxR,
                                      minA,maxA,minS,maxS,write);
          break;
        }

      case 'a':
        {
          number = number + DecodeProcessBddRAS(proc,Bdd_GetElse(F),mark,
                                      minR,maxR,
                                      minA,maxA-getWeight(F),
                                      minS,maxS,write);
          number = number + DecodeProcessBddRAS(proc,Bdd_GetThen(F),mark,
                                      minR,maxR,
                                      minA+getWeight(F),maxA,
                                      minS,maxS,write);
          break;
        }

      case 's':
        {
          number = number + DecodeProcessBddRAS(proc,Bdd_GetElse(F),mark,
                                      minR,maxR,minA,maxA,
                                      minS,maxS-getWeight(F),write);
          number = number + DecodeProcessBddRAS(proc,Bdd_GetThen(F),mark,
                                      minR,maxR,minA,maxA,
                                      minS+getWeight(F),maxS,write);
          break;
        }
    }
  }

  return number;
}

/**Function****************************************************************
  Synopsis    []
  Description [States are encoded with variables r]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

static int
DecodeCompBddR(Pa_Composition *comp, Bdd_Edge F, Est_Boolean mark,
               int *decodingTableR, Est_Boolean write)
{
  int i,old;
  int number;
  static char ch;  /* STATIC TO MINIMIZE STACK PROBLEMS */

  number = 0;
  if (F.mark) mark = (!mark);
  if (Bdd_isTerminal(F)) {
    if (!mark) {
      number = DecodeCompState(comp,decodingTableR,write);
      /*
      fprintf(stderr,"number = %d\n",number);
      */
    }
  } else {
    ch = Bdd_GetVariableChar(F);
    switch (ch) {
      case 'r': {
              i = getProcComp(F);

                  old = decodingTableR[2*i+1]; /* maxR */
                  decodingTableR[2*i+1] =
                    decodingTableR[2*i+1] - getWeight(F); /* maxR - weight */
                  number = number +
                    DecodeCompBddR(comp,Bdd_GetElse(F),mark,decodingTableR,write);
                  decodingTableR[2*i+1] = old;

                  old = decodingTableR[2*i]; /* minR */
                  decodingTableR[2*i] =
                    decodingTableR[2*i] + getWeight(F); /* minR + weight */
                  number = number +
                    DecodeCompBddR(comp,Bdd_GetThen(F),mark,decodingTableR,write);
                  decodingTableR[2*i] = old;

                  break;
                }
    }
  }

  return number;
}

/**Function****************************************************************
  Synopsis    []
  Description [Transition relation is encoded with variables r,a,s.]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

static int
DecodeCompBddRAS(Pa_Composition *comp, Bdd_Edge F, Est_Boolean mark,
                    int minA, int maxA, int *decodingTableR,
                    int *decodingTableS, Est_Boolean write)
{
  int i,old;
  int number;
  static char ch;  /* STATIC TO MINIMIZE STACK PROBLEMS */

  number = 0;
  if (F.mark) mark = (!mark);
  if (Bdd_isTerminal(F)) {
    if (!mark) {
       number =
         DecodeCompTR(comp,minA,maxA,decodingTableR,decodingTableS,write);
    }
  } else {
    ch = Bdd_GetVariableChar(F);
    switch (ch) {
      case 'r': {
              i = getProcComp(F);

                  old = decodingTableR[2*i+1]; /* maxR */
                  decodingTableR[2*i+1] =
                    decodingTableR[2*i+1] - getWeight(F); /* maxR - weight */
                  number = number +
                    DecodeCompBddRAS(comp,Bdd_GetElse(F),mark,minA,maxA,
                                     decodingTableR,decodingTableS,write);
                  decodingTableR[2*i+1] = old;

                  old = decodingTableR[2*i]; /* minR */
                  decodingTableR[2*i] =
                    decodingTableR[2*i] + getWeight(F); /* minR + weight */
                  number = number +
                    DecodeCompBddRAS(comp,Bdd_GetThen(F),mark,minA,maxA,
                                     decodingTableR,decodingTableS,write);
                  decodingTableR[2*i] = old;

                  break;
                }
      case 's': {
              i = getProcComp(F);

                  old = decodingTableS[2*i+1]; /* maxR */
                  decodingTableS[2*i+1] =
                    decodingTableS[2*i+1] - getWeight(F); /* maxS - weight */
                  number = number +
                    DecodeCompBddRAS(comp,Bdd_GetElse(F),mark,minA,maxA,
                                     decodingTableR,decodingTableS,write);
                  decodingTableS[2*i+1] = old;

                  old = decodingTableS[2*i]; /* minS */
                  decodingTableS[2*i] =
                    decodingTableS[2*i] + getWeight(F); /* minS + getWeight(F) */
                  number = number +
                    DecodeCompBddRAS(comp,Bdd_GetThen(F),mark,minA,maxA,
                                     decodingTableR,decodingTableS,write);
                  decodingTableS[2*i] = old;

                  break;
                }
      case 'a': {
                  number = number +
                    DecodeCompBddRAS(comp,Bdd_GetElse(F),mark,
                                     minA,maxA-getWeight(F),
                                     decodingTableR,decodingTableS,write);

                  number = number +
                    DecodeCompBddRAS(comp,Bdd_GetThen(F),mark,
                                     minA+getWeight(F),maxA,
                                     decodingTableR,decodingTableS,write);

                  break;
                }
    }
  }

  return number;
}

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

static int
DecodeProcProcPairBddRP(Pa_Process *p1, Pa_Process *p2, Bdd_Edge F,
                        Est_Boolean mark, int minR, int maxR, int minP,
                        int maxP, Est_Boolean write)
{
  int number;
  static char ch;  /* STATIC TO MINIMIZE STACK PROBLEMS */

  number = 0;
  if (F.mark) mark = (!mark);
  if (Bdd_isTerminal(F)) {
    if (!mark) {
      number = DecodeProcProcPair(p1,p2,minR,maxR,minP,maxP,write);
    }
  } else {
    ch = Bdd_GetVariableChar(F);
    switch (ch) {
      case 'r': {
                  number = number +
                    DecodeProcProcPairBddRP(p1,p2,Bdd_GetElse(F),mark,
                                            minR,maxR-getWeight(F),
                                            minP,maxP,write);
                  number = number +
                    DecodeProcProcPairBddRP(p1,p2,Bdd_GetThen(F),mark,
                                            minR+getWeight(F),maxR,
                                            minP,maxP,write);
                  break;
                }
      case 'p': {
                  number = number +
                    DecodeProcProcPairBddRP(p1,p2,Bdd_GetElse(F),mark,
                                            minR,maxR,
                                            minP,maxP-getWeight(F),write);
                  number = number +
                    DecodeProcProcPairBddRP(p1,p2,Bdd_GetThen(F),mark,
                                            minR,maxR,
                                            minP+getWeight(F),maxP,write);
                  break;
                }
    }
  }

  return number;
}

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

static int
DecodeCompProcPairBddRP(Pa_Composition *comp, Pa_Process *p, Bdd_Edge F,
                        Est_Boolean mark, int *decodingTableR, int minP,
                        int maxP, Est_Boolean write)
{
  int i,old;
  int number;
  static char ch;  /* STATIC TO MINIMIZE STACK PROBLEMS */

  number = 0;
  if (F.mark) mark = (!mark);
  if (Bdd_isTerminal(F)) {
    if (!mark) {
      number = DecodeCompProcPair(comp,p,decodingTableR,minP,maxP,write);
    }
  } else {
    ch = Bdd_GetVariableChar(F);
    switch (ch) {
      case 'r': {
              i = getProcComp(F);

          /*
                  i = strspn(&s->name[1],"0123456789");
                  pname = strdup(&s->name[i+2]);
                  pname[strlen(pname)-1] = 0;
                  i = Pa_FindProcessComp(comp,pname);
                  free(pname);
          */

                  old = decodingTableR[2*i+1]; /* maxR */
                  decodingTableR[2*i+1] =
                    decodingTableR[2*i+1] - getWeight(F); /* maxR - weight */
                  number = number +
                    DecodeCompProcPairBddRP(comp,p,Bdd_GetElse(F),mark,
                                            decodingTableR,minP,maxP,write);
                  decodingTableR[2*i+1] = old;

                  old = decodingTableR[2*i]; /* minR */
                  decodingTableR[2*i] =
                    decodingTableR[2*i] + getWeight(F); /* minR + weight */
                  number = number +
                    DecodeCompProcPairBddRP(comp,p,Bdd_GetThen(F),mark,
                                            decodingTableR,minP,maxP,write);
                  decodingTableR[2*i] = old;

                  break;
                }
      case 'p': {
                  number = number +
                    DecodeCompProcPairBddRP(comp,p,Bdd_GetElse(F),mark,
                                            decodingTableR,
                                            minP,maxP-getWeight(F),write);
                  number = number +
                    DecodeCompProcPairBddRP(comp,p,Bdd_GetThen(F),mark,
                                            decodingTableR,
                                            minP+getWeight(F),maxP,write);
                  break;
                }
    }
  }

  return number;
}

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

static int
DecodeCompCompPairBddRP(Pa_Composition *c1, Pa_Composition *c2, Bdd_Edge F,
                        Est_Boolean mark, int *decodingTableR,
                        int *decodingTableS, Est_Boolean write)
{
  int i,old;
  int number;
  static char ch;  /* STATIC TO MINIMIZE STACK PROBLEMS */

  number = 0;
  if (F.mark) mark = (!mark);
  if (Bdd_isTerminal(F)) {
    if (!mark) {
      number = DecodeCompCompPair(c1,c2,decodingTableR,decodingTableS,write);
    }
  } else {
    ch = Bdd_GetVariableChar(F);
    switch (ch) {
      case 'r': {
              i = getProcComp(F);

                  old = decodingTableR[2*i+1]; /* maxR */
                  decodingTableR[2*i+1] =
                    decodingTableR[2*i+1] - getWeight(F); /* maxR - weight */
                  number = number +
                    DecodeCompCompPairBddRP(c1,c2,Bdd_GetElse(F),mark,decodingTableR,
                                            decodingTableS,write);
                  decodingTableR[2*i+1] = old;

                  old = decodingTableR[2*i]; /* minR */
                  decodingTableR[2*i] =
                    decodingTableR[2*i] + getWeight(F); /* minR + weight */
                  number = number +
                    DecodeCompCompPairBddRP(c1,c2,Bdd_GetThen(F),mark,decodingTableR,
                                            decodingTableS,write);
                  decodingTableR[2*i] = old;

                  break;
                }

      case 'p': {
              i = getProcComp(F);

                  old = decodingTableS[2*i+1]; /* maxP */
                  decodingTableS[2*i+1] =
                    decodingTableS[2*i+1] - getWeight(F); /* maxP - weight */
                  number = number +
                    DecodeCompCompPairBddRP(c1,c2,Bdd_GetElse(F),mark,decodingTableR,
                                            decodingTableS,write);
                  decodingTableS[2*i+1] = old;

                  old = decodingTableS[2*i]; /* minP */
                  decodingTableS[2*i] =
                    decodingTableS[2*i] + getWeight(F); /* minP + weight */
                  number = number +
                    DecodeCompCompPairBddRP(c1,c2,Bdd_GetThen(F),mark,decodingTableR,
                                            decodingTableS,write);
                  decodingTableS[2*i] = old;

                  break;
                }
    }
  }

  return number;
}

/**Function****************************************************************
  Synopsis    []
  Description []
  SideEffects [If act==NULL and write=false then not create and not write out
               If act==NULL and write=true then not create and write out
               If act!=NULL and write=false then create and not write out
               If act!=NULL and write=true then create and write out]
  SeeAlso     []
  ************************************************************************/

static int
DecodeSortAction(Pa_Sort *s, int minA, int maxA, Est_String *act,
                 Est_Boolean write)
{
  int i,fA;
  int number;
  Est_String act1;
  Est_String act2;

  if (!act && write) {
    act2 = strdup("");
    act = &act2;
  }

  if (act) {
    act1 = strdup("");
    fA = 1;
    for (i=1; i<s->numVar; i++) fA = fA * 2;
    number = DecodeAction(s,minA,maxA,fA,&act1,write,0);
    concat(act,act1);
    free(act1);

  } else {

    if (minA == maxA) {
      number = 1;
    } else {
      fA = 1;
      for (i=1; i<s->numVar; i++) fA = fA * 2;
      number = DecodeAction(s,minA,maxA,fA,NULL,write,0);
    }
  }

  if (!act && write) {
    printf("%s",*act);
    free(*act);
    act = NULL;
  }

  return number;
}

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

static int
DecodeProcessState(Pa_Process *p, int minR, int maxR, Est_Boolean write)
{
  int i,fR;
  int number;

  if (write) {

    fR = 1;
    for (i=1; i<p->numVar; i++) fR = fR * 2;

    printf("(");
    number = DecodeState(p,minR,maxR,fR,write,FALSE,0);
    printf(")");

  } else {

    if (minR == maxR) {
      number = 1;
    } else {
      fR = 1;
      for (i=1; i<p->numVar; i++) fR = fR * 2;
      number = DecodeState(p,minR,maxR,fR,write,FALSE,0);
    }

  }
  return number;
}

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

static int
DecodeProcessTR(Pa_Process *p, int minR, int maxR,
                int minA, int maxA, int minS, int maxS, Est_Boolean write)
{
  int i,fA,fS;
  int nr,na,ns,number;
  Est_String act;

  if (write) {

    fS = 1;
    fA = 1;

    for (i=1; i<p->numVar; i++) fS = fS * 2;
    for (i=1; i<pa_sortTable[p->sort].numVar; i++) fA = fA * 2;

    act = strdup("");

    printf("(");
    nr = DecodeState(p,minR,maxR,fS,write,FALSE,0);
    printf(") --- ");

    na = DecodeAction(&pa_sortTable[p->sort],minA,maxA,fA,&act,write,0);

    printf(" ---> (");
    ns = DecodeState(p,minS,maxS,fS,write,FALSE,0);
    printf(")\n");

    free(act);

  } else {

    fS = 1;

    if (minR == maxR) {
      nr = 1;
    } else {
      for (i=1; i<p->numVar; i++) fS = fS * 2;
      nr = DecodeState(p,minR,maxR,fS,write,FALSE,0);
    }

    if (minA == maxA) {
      na = 1;
    } else {
      fA = 1;
      for (i=1; i<pa_sortTable[p->sort].numVar; i++) fA = fA * 2;
      na = DecodeAction(&pa_sortTable[p->sort],minA,maxA,fA,NULL,write,0);
    }

    if (minS == maxS) {
      ns = 1;
    } else {
      if (fS == 1) for (i=1; i<p->numVar; i++) fS = fS * 2;
      ns = DecodeState(p,minS,maxS,fS,write,FALSE,0);
    }

  }

  number = nr * na * ns;
  return number;
}

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

static int
DecodeCompState(Pa_Composition *c, int *decodingTableR, Est_Boolean write)
{
  int i,j,fS;
  int number;

  number = 1;

  if (write) {

    printf("(");

    for (i=0; i<c->numProcesses; i++) {
      fS = 1;
      for (j=0; j<pa_processTable[c->tableP[i]].numVar; j++) fS = fS * 2;
      printf("(");
      number = number * DecodeState(&pa_processTable[c->tableP[i]],
               decodingTableR[2*i],decodingTableR[2*i+1],fS,write,TRUE,0);
      printf(")");
      if (i<c->numProcesses-1) printf(",");
    }

    printf(")");

  } else {

    for (i=0; i<c->numProcesses; i++) {
      if (decodingTableR[2*i] != decodingTableR[2*i+1]) {
        fS = 1;
        for (j=0; j<pa_processTable[c->tableP[i]].numVar; j++) fS = fS * 2;
        number = number * DecodeState(&pa_processTable[c->tableP[i]],
                 decodingTableR[2*i],decodingTableR[2*i+1],fS,write,TRUE,0);
      }
    }

  }

  return number;
}

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

static void
CompStates2ProcStates(Pa_Composition *c, int i, int *decodingTableR,
                      int min, int max, int f, Bdd_Edge F, int procnum)
{
  int decoded = 0;
  int j;
  int fS;
  Pa_Process *proc;

  if (min == max) {
    if (min < pa_processTable[c->tableP[i]].numStates) {
      F = Bdd_ITE(F,pa_processTable[c->tableP[i]].tableS[min].bddR,
                  bdd_termFalse);
      if (i == c->numProcesses - 1) {
        decoded++;
      } else {
        i++;
        fS = 1;
        for (j=0; j<pa_processTable[c->tableP[i]].numVar; j++) fS = fS * 2;
        CompStates2ProcStates(c,i,decodingTableR,decodingTableR[2*i],
                              decodingTableR[2*i+1],fS,F,procnum);
      }
    }
  } else {
    if ( (max - min) >= f ) {
      CompStates2ProcStates(c,i,decodingTableR,min+f,max,f/2,F,procnum);
      CompStates2ProcStates(c,i,decodingTableR,min,max-f,f/2,F,procnum);
    } else {
      CompStates2ProcStates(c,i,decodingTableR,min,max,f/2,F,procnum);
    }
  }

  if (decoded != 1) return;

  proc = &pa_processTable[procnum];
  Pa_FOAComposedStateProcess(proc,F,proc->name);
}

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

static void
CompTR2ProcTR(Pa_Composition *c, int iR, int iS, int *decodingTableR,
              int *decodingTableS, int minA, int maxA, int minR, int maxR,
              int minS, int maxS, int fA, int fR,int fS, Bdd_Edge FR,
              Bdd_Edge FS, int procnum)
{
  int decoded = 0;
  int j;
  Pa_Process *proc;
  int nr,ns;

  /*
  printf(
    "CompTR2ProcTR: minR=%d, maxR=%d, minA=%d, maxA=%d, minS=%d, maxS=%d\n",
    minR, maxR, minA, maxA, minS, maxS);
  */

  if (minR == maxR) {
    if (minR < pa_processTable[c->tableP[iR]].numStates) {
      FR = Bdd_ITE(FR,pa_processTable[c->tableP[iR]].tableS[minR].bddR,
                  bdd_termFalse);
      if (iR == c->numProcesses - 1) {
        decoded++;
      } else {
        iR++;
        fR = 1;
        for (j=0; j<pa_processTable[c->tableP[iR]].numVar; j++) fR = fR * 2;
        CompTR2ProcTR(c,iR,iS,decodingTableR,decodingTableS,
                      minA,maxA,decodingTableR[2*iR],decodingTableR[2*iR+1],
                      minS,maxS,fA,fR,fS,FR,FS,procnum);
      }
    }
  } else {
    if ( (maxR - minR) >= fR ) {
      CompTR2ProcTR(c,iR,iS,decodingTableR,decodingTableS,
                    minA,maxA,minR+fR,maxR,minS,maxS,fA,fR/2,fS,FR,FS,procnum);
      CompTR2ProcTR(c,iR,iS,decodingTableR,decodingTableS,
                    minA,maxA,minR,maxR-fR,minS,maxS,fA,fR/2,fS,FR,FS,procnum);
    } else {
      CompTR2ProcTR(c,iR,iS,decodingTableR,decodingTableS,
                    minA,maxA,minR,maxR,minS,maxS,fA,fR/2,fS,FR,FS,procnum);
    }
  }

  if (decoded != 1) return;

  if (minA == maxA) {
    if (minA <= 2 * pa_sortTable[c->sort].numActions) {
      decoded++;
    }
  } else {
    if ( (maxA - minA) >= fA ) {
      CompTR2ProcTR(c,iR,iS,decodingTableR,decodingTableS,
                    minA+fA,maxA,minR,maxR,minS,maxS,fA/2,fR,fS,FR,FS,procnum);
      CompTR2ProcTR(c,iR,iS,decodingTableR,decodingTableS,
                    minA,maxA-fA,minR,maxR,minS,maxS,fA/2,fR,fS,FR,FS,procnum);
    } else {
      CompTR2ProcTR(c,iR,iS,decodingTableR,decodingTableS,
                    minA,maxA,minR,maxR,minS,maxS,fA/2,fR,fS,FR,FS,procnum);
    }
  }

  if (decoded != 2) return;

  if (minS == maxS) {
    if (minS < pa_processTable[c->tableP[iS]].numStates) {
      FS = Bdd_ITE(FS,pa_processTable[c->tableP[iS]].tableS[minS].bddR,
                  bdd_termFalse);
      if (iS == c->numProcesses - 1) {
        decoded++;
      } else {
        iS++;
        fS = 1;
        for (j=0; j<pa_processTable[c->tableP[iS]].numVar; j++) fS = fS * 2;
        CompTR2ProcTR(c,iR,iS,decodingTableR,decodingTableS,
                      minA,maxA,minR,maxR,decodingTableS[2*iS],
                      decodingTableS[2*iS+1],fA,fR,fS,FR,FS,procnum);
        return;
      }
    }
  } else {
    if ( (maxS - minS) >= fS ) {
      CompTR2ProcTR(c,iR,iS,decodingTableR,decodingTableS,
                    minA,maxA,minR,maxR,minS+fS,maxS,fA,fR,fS/2,FR,FS,procnum);
      CompTR2ProcTR(c,iR,iS,decodingTableR,decodingTableS,
                    minA,maxA,minR,maxR,minS,maxS-fS,fA,fR,fS/2,FR,FS,procnum);
    } else {
      CompTR2ProcTR(c,iR,iS,decodingTableR,decodingTableS,
                    minA,maxA,minR,maxR,minS,maxS,fA,fR,fS/2,FR,FS,procnum);
    }
  }

  if (decoded != 3) return;

  /*
  Pa_DecodeCompTR(c,F,TRUE);
  */

  proc = &pa_processTable[procnum];
  nr = Pa_FOAComposedStateProcess(proc,FR,proc->name);
  ns = Pa_FOAComposedStateProcess(proc,FS,proc->name);

  /*
  fprintf(stderr,"Add transition: %d --%d=%d--> %d\n",nr,minA/2,minA%2,ns);
  */

  Pa_FOATransition(proc,nr,minA/2,minA%2,ns);
}


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

static int
DecodeCompTR(Pa_Composition *c, int minA, int maxA,
             int *decodingTableR, int *decodingTableS, Est_Boolean write)
{
  int i,j,fA,fS;
  int nr,na,ns,number;
  Est_String act;

  nr = 1;
  ns = 1;

  if (write) {

    printf("(");

    for (i=0; i<c->numProcesses; i++) {
      fS = 1;
      for (j=0; j<pa_processTable[c->tableP[i]].numVar; j++) fS = fS * 2;
      printf("(");
      nr = nr * DecodeState(&pa_processTable[c->tableP[i]],
           decodingTableR[2*i],decodingTableR[2*i+1],fS,write,TRUE,0);
      printf(")");
      if (i<c->numProcesses-1) printf(",");
    }

    printf(") --- ");

    act = strdup("");

    fA = 1;
    for (i=1; i<pa_sortTable[c->sort].numVar; i++) fA = fA * 2;

    na = DecodeAction(&pa_sortTable[c->sort],minA,maxA,fA,&act,write,0);

    printf(" ---> (");

    for (i=0; i<c->numProcesses; i++) {
      fS = 1;
      for (j=0; j<pa_processTable[c->tableP[i]].numVar; j++) fS = fS * 2;
      printf("(");
      ns = ns * DecodeState(&pa_processTable[c->tableP[i]],
           decodingTableS[2*i],decodingTableS[2*i+1],fS,write,TRUE,0);
        printf(")");
        if (i<c->numProcesses-1) printf(",");
    }

    printf(")\n");

    free(act);

  } else {

    for (i=0; i<c->numProcesses; i++) {
      if (decodingTableR[2*i] != decodingTableR[2*i+1]) {
        fS = 1;
        for (j=0; j<pa_processTable[c->tableP[i]].numVar; j++) fS = fS * 2;
        nr = nr * DecodeState(&pa_processTable[c->tableP[i]],
             decodingTableR[2*i],decodingTableR[2*i+1],fS,write,TRUE,0);
      }
    }

    if (minA == maxA) {
      na = 1;
    } else {
      fA = 1;
      for (i=1; i<pa_sortTable[c->sort].numVar; i++) fA = fA * 2;
      na = DecodeAction(&pa_sortTable[c->sort],minA,maxA,fA,NULL,write,0);
    }

    for (i=0; i<c->numProcesses; i++) {
      if (decodingTableS[2*i] != decodingTableS[2*i+1]) {
        fS = 1;
        for (j=0; j<pa_processTable[c->tableP[i]].numVar; j++) fS = fS * 2;
        ns = ns * DecodeState(&pa_processTable[c->tableP[i]],
             decodingTableS[2*i],decodingTableS[2*i+1],fS,write,TRUE,0);
      }
    }

  }

  number = nr * na * ns;
  return number;
}

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

static int
DecodeProcProcPair(Pa_Process *p1, Pa_Process *p2, int minR, int maxR,
                   int minP, int maxP, Est_Boolean write)
{
  int i, fR, fP;
  int number;

  fR = 1;
  fP = 1;

  for (i=1; i<p1->numVar; i++) fR = fR * 2;
  for (i=1; i<p2->numVar; i++) fP = fP * 2;

  number = 1;
  if (write) printf("<(");
  number = number * DecodeState(p1,minR,maxR,fR,write,TRUE,0);
  if (write) printf("),(");
  number = number * DecodeState(p2,minP,maxP,fP,write,TRUE,0);
  if (write) printf(")>\n");

  return number;
}

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

static int
DecodeCompProcPair(Pa_Composition *c, Pa_Process *p, int *decodingTableR,
                   int minP, int maxP, Est_Boolean write)
{
  int i,j,fS,fP;
  int nr,ns,number;

  nr = 1;
  if (write) printf("<<");

  for (i=0; i<c->numProcesses; i++) {
    fS = 1;
    for (j=0; j<pa_processTable[c->tableP[i]].numVar; j++) fS = fS * 2;
    if (write) printf("(");
    nr = nr * DecodeState(&pa_processTable[c->tableP[i]],
         decodingTableR[2*i],decodingTableR[2*i+1],fS,write,TRUE,0);
    if (write) printf("),");
  }

  if (write) printf(">,(");

  fP = 1;
  for (i=1; i<p->numVar; i++) fP = fP * 2;
  ns = DecodeState(p,minP,maxP,fP,write,TRUE,0);

  if (write) printf(")>\n");

  number = nr * ns;
  return number;
}

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

static int
DecodeCompCompPair(Pa_Composition *c1, Pa_Composition *c2,
                   int *decodingTableR, int *decodingTableS,
                   Est_Boolean write)
{
  int i,j,fR,fS;
  int nr,ns,number;

  nr = 1;
  ns = 1;
  if (write) printf("<<");

  for (i=0; i<c1->numProcesses; i++) {
    fR = 1;
    for (j=0; j<pa_processTable[c1->tableP[i]].numVar; j++) fR = fR * 2;
    if (write) printf("(");
    nr = nr * DecodeState(&pa_processTable[c1->tableP[i]],
         decodingTableR[2*i],decodingTableR[2*i+1],fR,write,TRUE,0);
    if (write) printf("),");
  }

  if (write) printf(">,<");

  for (i=0; i<c2->numProcesses; i++) {
    fS = 1;
    for (j=0; j<pa_processTable[c2->tableP[i]].numVar; j++) fS = fS * 2;
    if (write) printf("(");
    ns = ns * DecodeState(&pa_processTable[c2->tableP[i]],
         decodingTableS[2*i],decodingTableS[2*i+1],fS,write,TRUE,0);
    if (write) printf("),");
  }

  if (write) printf(">>\n");

  number = nr * ns;
  return number;
}


/**Function****************************************************************
  Synopsis    []
  Description []
  SideEffects [Type variable (a0) should have weight = 1.
               If act==NULL and write=false then not create and not write out
               If act==NULL and write=true then not create AND NOT WRITE OUT
               If act!=NULL and write=false then create and not write out
               If act!=NULL and write=true then create and write out]
  SeeAlso     []
  ************************************************************************/

static int
DecodeAction(Pa_Sort *s, int min, int max, int f, Est_String *act,
             Est_Boolean write, int more)
{
  int number;
  Est_String act1;

  if (min == max) {
    number = 1;

    if (act) {
      act1 = strdup("");
      if (min >= 2 * s->numActions) {
        if (more>0) concat(&act1,",");
        if (min % 2) concat(&act1,"!!"); else concat(&act1,"??");
      } else {
        if (min > 0) {
          if (more>0) concat(&act1,",");
          concat(&act1,s->table[(min)/2].name);
          if (min % 2) concat(&act1,"!"); else concat(&act1,"?");
        } else {
          if (more>0) concat(&act1,",");
          concat(&act1,"TAU");
        }
      }

      if (write) printf("%s",act1);
      concat(act,act1);
      free(act1);
    }


  } else {

    if (min > max) {
      number = -1;
      fprintf(stdout,"DecodeAction ERROR!\n");
      fprintf(stdout,"name = %s, min = %d, max = %d\n",s->name,min,max);
      exit(1);
    } else {

      if ( (max - min) >= f ) {
        number = DecodeAction(s,min+f,max,f/2,act,write,more)
               + DecodeAction(s,min,max-f,f/2,act,write,more+1);
      } else {
        number = DecodeAction(s,min,max,f/2,act,write,more);
      }

    }
  }

  return number;
}

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

static int
DecodeState(Pa_Process *p, int min, int max, int f, Est_Boolean write,
            Est_Boolean pname, int more)
{
  int number;

  if (min == max) {
    number = 1;

    if (write) {
      if (min >= p->numStates) {
        printf("??");
      } else {
        if (more>0) printf(")(");
        if (pname) {
          printf("%s",p->tableS[min].name);
        } else {
          printstate(p->tableS[min].name);
    }
      }
    }

  } else {

    if (min > max) {
      number = -1;
      fprintf(stderr,"DecodeState ERROR!\n");
      fprintf(stderr,"name = %s, min = %d, max = %d\n",p->name,min,max);
      exit(1);
    } else {

      if ( (max - min) >= f ) {
        number = DecodeState(p,min+f,max,f/2,write,pname,more)
               + DecodeState(p,min,max-f,f/2,write,pname,more+1);
      } else {
        number = DecodeState(p,min,max,f/2,write,pname,more);
      }

    }
  }

  return number;
}

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

static Est_Boolean
ExtractProcTransition(Pa_Process *p, Bdd_Edge F, Est_Boolean mark,
                      int *minR, int *minA, int *minS)
{
  static char ch;    /* STATIC TO MINIMIZE STACK PROBLEMS */

  if (F.mark) mark = (!mark);
  if (Bdd_isTerminal(F)) {
    if (!mark) return TRUE; else return FALSE;
  } else {
    ch = Bdd_GetVariableChar(F);
    switch (ch) {
      case 'r':
        {
          if (ExtractProcTransition(p,Bdd_GetElse(F),mark,minR,minA,minS)) {
            return TRUE;
      }

          *minR = *minR + getWeight(F);
          return ExtractProcTransition(p,Bdd_GetThen(F),mark,minR,minA,minS);

          break;
        }

      case 'a':
        {
          if (ExtractProcTransition(p,Bdd_GetElse(F),mark,minR,minA,minS)) {
            return TRUE;
      }

          *minA = *minA + getWeight(F);
          return ExtractProcTransition(p,Bdd_GetThen(F),mark,minR,minA,minS);

          break;
        }

      case 's':
        {
          if (ExtractProcTransition(p,Bdd_GetElse(F),mark,minR,minA,minS)) {
            return TRUE;
      }

          *minS = *minS + getWeight(F);
          return ExtractProcTransition(p,Bdd_GetThen(F),mark,minR,minA,minS);

          break;
        }

    }
  }

  return FALSE;
}

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

static Est_Boolean
ExtractCompTransition(Pa_Composition *comp, Bdd_Edge F, Est_Boolean mark,
                    int *minA, int *decodingTableR, int *decodingTableS)
{
  int i;
  static char ch;  /* STATIC TO MINIMIZE STACK PROBLEMS */

  if (F.mark) mark = (!mark);
  if (Bdd_isTerminal(F)) {
    if (!mark) return TRUE; else return FALSE;
  } else {
    ch = Bdd_GetVariableChar(F);
    switch (ch) {
      case 'r':
        {
          i = getProcComp(F);

          if (ExtractCompTransition(comp,Bdd_GetElse(F),mark,
                                    minA,decodingTableR,decodingTableS)) {
            return TRUE;
      }

          decodingTableR[2*i] =
            decodingTableR[2*i] + getWeight(F); /* minR + weight */

          return ExtractCompTransition(comp,Bdd_GetThen(F),mark,minA,
                                       decodingTableR,decodingTableS);

          break;
        }

      case 'a':
        {
          if (ExtractCompTransition(comp,Bdd_GetElse(F),mark,
                    minA,decodingTableR,decodingTableS)) {
            return TRUE;
      }


          *minA = *minA + getWeight(F);
          return ExtractCompTransition(comp,Bdd_GetThen(F),mark,
                                       minA,decodingTableR,decodingTableS);

          break;
        }

      case 's':
        {
          i = getProcComp(F);

          if (ExtractCompTransition(comp,Bdd_GetElse(F),mark,
                                    minA,decodingTableR,decodingTableS)) {
            return TRUE;
      }

          decodingTableS[2*i] =
            decodingTableS[2*i] + getWeight(F); /* minS + weight */

          return ExtractCompTransition(comp,Bdd_GetThen(F),mark,minA,
                                       decodingTableR,decodingTableS);

          break;
        }
    }
  }

  return FALSE;
}

/**Function****************************************************************
  Synopsis    []
  Description [States are encoded with variables r]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

static Est_Boolean
ExtractProcState(Pa_Process *proc, Bdd_Edge F, Est_Boolean mark, int *minR)
{
  static char ch;   /* STATIC TO MINIMIZE STACK PROBLEMS */

  if (F.mark) mark = (!mark);
  if (Bdd_isTerminal(F)) {
    if (!mark) return TRUE; else return FALSE;
  } else {
    ch = Bdd_GetVariableChar(F);
    switch (ch) {
      case 'r':
        {
          if (ExtractProcState(proc,Bdd_GetElse(F),mark,minR)) {
            return TRUE;
      }

          *minR = *minR + getWeight(F);
          return ExtractProcState(proc,Bdd_GetThen(F),mark,minR);

          break;
        }
    }
  }

  return FALSE;
}

/**Function****************************************************************
  Synopsis    []
  Description [States are encoded with variables r]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

static Est_Boolean
ExtractCompState(Pa_Composition *comp, Bdd_Edge F, Est_Boolean mark,
                 int *decodingTableR)
{
  int i;
  static char ch;           /* STATIC TO MINIMIZE STACK PROBLEMS */

  if (F.mark) mark = (!mark);
  if (Bdd_isTerminal(F)) {
    if (!mark) return TRUE; else return FALSE;
  } else {
    ch = Bdd_GetVariableChar(F);
    switch (ch) {
      case 'r': {
                  i = getProcComp(F);

                  if (ExtractCompState(comp,Bdd_GetElse(F),mark,decodingTableR)) {
                    return TRUE;
              }

                  decodingTableR[2*i] =
                    decodingTableR[2*i] + getWeight(F); /* minR + weight */

                  return ExtractCompState(comp,Bdd_GetThen(F),mark,decodingTableR);

                  break;
      }
    }
  }

  return FALSE;
}

/**Function****************************************************************
  Synopsis    []
  Description [Actions are encoded with variables a]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

static Est_Boolean
ExtractSortAction(Pa_Sort *sort, Bdd_Edge F, Est_Boolean mark, int *minA)
{
  static char ch;  /* STATIC TO MINIMIZE STACK PROBLEMS */

  if (F.mark) mark = (!mark);
  if (Bdd_isTerminal(F)) {
    if (!mark) return TRUE; else return FALSE;
  } else {
    ch = Bdd_GetVariableChar(F);
    switch (ch) {
      case 'a':
        {
          if (ExtractSortAction(sort,Bdd_GetElse(F),mark,minA)) {
            return TRUE;
      }

          *minA = *minA + getWeight(F);
          return ExtractSortAction(sort,Bdd_GetThen(F),mark,minA);

          break;
        }
    }
  }

  return FALSE;
}

/**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    [Function printstate]
  Description []
  SideEffects []
  SeeAlso     []
  ************************************************************************/

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

  i = strcspn(name,"<");
  shortname = (char *) malloc(i+1);
  memcpy(shortname,name,i);
  shortname[i]=0;
  printf("%s",shortname);
  free(shortname);
}

/**Function****************************************************************
  Synopsis    [Function setproccomp]
  Description [Set proccomp (to which proccess it belongs) for variables.]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

static void
setproccomp(Pa_Composition *comp)
{
  int i,n;
  Est_String name,pname;

  for (i=0;i<pa_variables;i++) {
    name = Bdd_GetIthVariableName(i);
    n = strspn(&name[1],"0123456789");
    if (n<strlen(&name[1])) {
      pname = strdup(&name[n+2]);
      pname[strlen(pname)-1] = 0;
      pa_variableTable[i].proccomp = Pa_FindProcessComp(comp,pname);
      free(pname);
    }
  }
}


/**Function****************************************************************
  Synopsis    [Function getWeight]
  Description [Return weight of top variable.]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

static int
getWeight(Bdd_Edge f)
{
  return pa_variableTable[Bdd_GetVariable(f)].weight;
}

/**Function****************************************************************
  Synopsis    [Function getProcComp]
  Description [Return proccomp of top variable.]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

static int
getProcComp(Bdd_Edge f)
{
  return pa_variableTable[Bdd_GetVariable(f)].proccomp;
}
