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

  FileName    [versisEqv.c]
  Revision    [$Revision: 76 $]
  Date        [$Date: 2013-04-26 14:26:09 +0200 (pet, 26 apr 2013) $]
  Authors     [Robert Meolic (meolic@uni-mb.si),
               Mirjam Sepesy Maucec (mirjam.sepesy@uni-mb.si),
               Tatjana Kapus (kapus@uni-mb.si)]
  Description [File versisEqv.c provides different equivalence checking
               algorithms.]
  SeeAlso     [versis.h, versisInt.h]

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

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

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

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

#include "versisInt.h"

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

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

/* EXPORTED VARIABLES */

/* INTERNAL VARIABLES */

VersisStateTable ST = {0,NULL};
Pa_Process *tmpproc1 = NULL;
Pa_Process *tmpproc2 = NULL;

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

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

static Est_Boolean Bisimulation(Bdd_Edge init, Bdd_Edge *eqv,
                                Bdd_Edge St1, Bdd_Edge St2,
                                Bdd_Edge D1, Bdd_Edge D2);

static Est_Boolean Bisimulation1(Bdd_Edge init, Bdd_Edge *eqv,
                                 Bdd_Edge St, Bdd_Edge D);

static Bdd_Edge BuildAcc(int par, Est_String name, Est_String newname,
                     Bdd_Edge D, Bdd_Edge init,
                     Bdd_Edge Ptau, Bdd_Edge trcl, Bdd_Edge Div, int s,
                     Bdd_Edge tau, Bdd_Edge *Acc, Bdd_Edge *AccFalse,
                     Bdd_Edge *AccNull, Bdd_Edge *InitNew);

static int BuildAccR(int par, Est_String name,
                     Bdd_Edge D, Bdd_Edge Ptau, Bdd_Edge S, Bdd_Edge tau,
                     Bdd_Edge Div, Est_Boolean b, int s);

static Bdd_Edge MakeAcc(Bdd_Edge D, Bdd_Edge tau, Bdd_Edge S);

static void MinAcc(int numNS, Pa_State *tabNS, int numS, Pa_State *tabS);

static Est_Boolean CmpAcc(Bdd_Edge acc1, Bdd_Edge acc2);

static int BuildDetR(Bdd_Edge Ptau, Bdd_Edge S, int s, Bdd_Edge final);

static void AddStateTable(Bdd_Edge S, Est_Boolean b, int t);

static Est_Boolean FindStateTable(Bdd_Edge S, Est_Boolean b, int *t);

static void WriteStateTable(int n);

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

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

/**Function****************************************************************
  Synopsis    [Function Versis_Equivalence.]
  Description [type = 0,1,2,3 - Strong, Weak, Test, Trace]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

Est_Boolean
Versis_Equivalence(int type, int par1, Est_String name1,
                             int par2, Est_String name2)
{

  int n1 = -1;
  int n2 = -1;
  int sort1 = -1;
  int sort2 = -1;
  int i;
  int newsort;
  int acc1,acc2,det1,det2;
  Est_String pom,newname1,newname2;
  Bdd_Edge eqv;
  Est_Boolean r;

  r = FALSE;
  newname1 = NULL;
  newname2 = NULL;

  /* FIRST PARAMETER */
  if (par1 == 0) {
    n1 = Pa_FindProcess(name1);
    if (n1 == -1) {
      printf("\nERROR: Process %s does not exist.\n",name1);
      return FALSE;
    }
    if (!pa_processTable[n1].encoded) {
      printf("\nERROR: Process %s is not encoded.\n",name1);
      return FALSE;
    }
    sort1 = pa_processTable[n1].sort;
  }
  if (par1 == 1) {
    n1 = Pa_FindComposition(name1);
    if (n1 == -1) {
      printf("\nERROR: Composition %s does not exist.\n",name1);
      return FALSE;
    }
    if (pa_compositionTable[n1].onthefly) {
      printf("\nERROR: Cannot check equivalence with on-the-fly composition %s.\n",name1);
      return FALSE;
    }
    sort1 = pa_compositionTable[n1].sort;
  }

  /* SECOND PARAMETER */
  if (par2 == 0) {
    n2 = Pa_FindProcess(name2);
    if (n2 == -1) {
      printf("\nERROR: Process %s does not exist.\n",name2);
      return FALSE;
    }
    if (!pa_processTable[n2].encoded) {
      printf("\nERROR: Process %s is not encoded.\n",name2);
      return FALSE;
    }
    sort2 = pa_processTable[n2].sort;
  }
  if (par2 == 1) {
    n2 = Pa_FindComposition(name2);
    if (n2 == -1) {
      printf("\nERROR: Composition %s does not exist.\n",name2);
      return FALSE;
    }
    if (pa_compositionTable[n2].onthefly) {
      printf("\nERROR: Cannot check equivalence with on-the-fly composition %s.\n",name2);
      return FALSE;
    }
    sort2 = pa_compositionTable[n2].sort;
  }

  if (sort1 != sort2) {

    /* THE FOLLOWING WARNING IS NOT USABLE */
    /*
    printf("\nWarning: ");
    if (par1 == 0) {
      printf("Process %s",name1);
    }
    if (par1 == 1) {
      printf("Composition %s",name1);
    }
    printf(" and ");
    if (par2 == 0) {
      printf("process %s",name2);
    }
    if (par2 == 1) {
      printf("composition %s",name2);
    }
    printf(" have sorts with different name!\n");

    printf("Warning: Copies of them will be made and used for equivalence checking!\n");
    */

    pom = (Est_String) malloc(1024);
    sprintf(pom,"%s-%s",pa_sortTable[sort1].name,pa_sortTable[sort2].name);
    newsort = Pa_AddNewSort(pom);
    free(pom);

    for (i=0; i<pa_sortTable[sort1].numActions; i++) {
      Pa_FOASortAction(&pa_sortTable[newsort],pa_sortTable[sort1].table[i].name);
    }

    for (i=0; i<pa_sortTable[sort2].numActions; i++) {
      Pa_FOASortAction(&pa_sortTable[newsort],pa_sortTable[sort2].table[i].name);
    }

    if (par1 == 1) {
      n1 = Pa_Composition2Process(name1,TRUE);
    }

    newname1 = (Est_String) malloc(1024);
    sprintf(newname1,"COPY_%s",name1);
    Pa_CopyProcess(name1,newname1,pa_sortTable[newsort].name,"","");
    if (par1 == 1) {Pa_DeleteProcess(n1);}
    Pa_EncodeProcess(newname1);

    if (par2 == 1) {
      n2 = Pa_Composition2Process(name2,TRUE);
    }

    newname2 = (Est_String) malloc(1024);
    sprintf(newname2,"COPY_%s",name2);
    Pa_CopyProcess(name2,newname2,pa_sortTable[newsort].name,"","");
    if (par2 == 1) {Pa_DeleteProcess(n2);}
    Pa_EncodeProcess(newname2);

    n1 = Pa_FindProcess(newname1);
    par1 = 0;

    n2 = Pa_FindProcess(newname2);
    par2 = 0;
  }

  switch (type) {
    case 0: {
              r = VersisStrongEquivalence(&eqv,par1,n1,par2,n2);
              break;
            }
    case 1: {
              r = VersisWeakEquivalence(&eqv,par1,n1,par2,n2);
              break;
            }
    case 2: {
              r = VersisTestEquivalence(&eqv,par1,n1,par2,n2,&acc1,&acc2);
              if (acc1 == acc2) {
                Pa_DeleteProcess(acc1);
              } else {
                pom = strdup(pa_processTable[acc2].name);
                Pa_DeleteProcess(acc1);
                Pa_DeleteProcess(Pa_FindProcess(pom));
                free(pom);
              }
              break;
            }
    case 3: {
              r = VersisTraceEquivalence(0,&eqv,par1,n1,par2,n2,&det1,&det2);
              if (det2 == -1) {
                Pa_DeleteProcess(det1);
              } else {
                pom = strdup(pa_processTable[det2].name);
                /* DELETE DET PROCESSES */
                /* COMMENT THIS OUT WHEN LOOKING FOR DIFFERENCE */
                /**/
                Pa_DeleteProcess(det1);
                Pa_DeleteProcess(Pa_FindProcess(pom));
                /**/
                free(pom);
              }
              break;
            }

    case 4: {
              r = VersisTraceEquivalence(1,&eqv,par1,n1,par2,n2,&det1,&det2);
              if (det2 == -1) {
                Pa_DeleteProcess(det1);
              } else {
                pom = strdup(pa_processTable[det2].name);
                Pa_DeleteProcess(det1);
                Pa_DeleteProcess(Pa_FindProcess(pom));
                free(pom);
              }
              break;
            }
  }


  if (newname1) {
    Pa_DeleteProcess(Pa_FindProcess(newname1));
    free(newname1);
  }

  if (newname2) {
    Pa_DeleteProcess(Pa_FindProcess(newname2));
    free(newname2);
  }

  return r;
}

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

/**Function****************************************************************
  Synopsis    []
  Description [par1,par2: 0 (process) or 1 (composition)
               par2 == -1 means, that par2 = par1 and n2 = n1]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

Est_Boolean
VersisStrongEquivalence(Bdd_Edge *eqv, int par1, int n1, int par2, int n2)
{
  Bdd_Edge St1, St2, D1, D2;
  Bdd_Edge ini,ini1,ini2;
  Est_Boolean EQV;
  /* Est_String name1,name2; */ /* for debugging */

  if ((par2 == par1) && (n2 == n1)) {
    par2 = -1;
    n2 = -1;
  }

  if (par1 == 0) {
    D1 = pa_processTable[n1].d;
    St1 = pa_processTable[n1].stateBDD;
    ini1 = pa_processTable[n1].tableS[pa_processTable[n1].initial].bddR;
    /* name1 = pa_processTable[n1].name; */ /* for debugging */
  } else {
    D1 = pa_compositionTable[n1].transitionBDD;
    St1 = pa_compositionTable[n1].stateBDD;
    ini1 = pa_compositionTable[n1].initialBDD;
    /* name1 = pa_compositionTable[n1].name; */ /* for debugging */
  }

  ini2 = bdd_termNull;
  if (par2 == 0) {
    D2 = pa_processTable[n2].d;
    St2 = pa_processTable[n2].stateBDD;
    ini2 = pa_processTable[n2].tableS[pa_processTable[n2].initial].bddR;
    /* name2 = pa_processTable[n2].name; */ /* for debugging */
  } else if (par2 == 1) {
    D2 = pa_compositionTable[n2].transitionBDD;
    St2 = pa_compositionTable[n2].stateBDD;
    ini2 = pa_compositionTable[n2].initialBDD;
    /* name2 = pa_compositionTable[n2].name; */ /* for debugging */
  }

  if (par2 == -1) {

    /* produkt zacetnih stanj */
    ini = Bdd_ITE(ini1,Bdd_RelOpSimple(ini1,"R2P",TRUE),bdd_termFalse);
    Bdd_Fortify(ini);

    *eqv = bdd_termTrue;
    EQV = Bisimulation1(ini,eqv,St1,D1);

  } else {

    /* produkt zacetnih stanj */
    ini = Bdd_ITE(ini1,Bdd_RelOpSimple(ini2,"R2P",TRUE),bdd_termFalse);
    Bdd_Fortify(ini);

    /* stanja D2 kodiramo s pomoznimi spremenljivkami */
    D2 = Bdd_RelOpSimple(D2,"R2P S2Q",TRUE);
    St2 = Bdd_RelOpSimple(St2,"R2P",TRUE);
    Bdd_Fortify(D2);
    Bdd_Fortify(St2);

    *eqv = bdd_termTrue;
    EQV = Bisimulation(ini,eqv,St1,St2,D1,D2);

  }

  return EQV;
}

/**Function****************************************************************
  Synopsis    []
  Description [par1, par2 = 0 (process) or 1 (composition)]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

Est_Boolean
VersisWeakEquivalence(Bdd_Edge *eqv, int par1, int n1, int par2, int n2)
{
  Bdd_Edge St1, St2, D1, D2;
  Bdd_Edge tau, stab1, stab2;
  Bdd_Edge eps, eps_rp, eps_qs;
  Bdd_Edge tr1_novi, tr2_novi;
  Bdd_Edge ini,ini1,ini2;
  Bdd_Edge pom, eqs;
  Est_Boolean EQV;
  int i;
  /* Est_String name1,name2; */ /* for debugging */

  if ((par2 == par1) && (n2 == n1)) {
    par2 = -1;
    n2 = -1;
  }

  if (par1 == 0) {
    D1 = pa_processTable[n1].d;
    St1 = pa_processTable[n1].stateBDD;
    ini1 = pa_processTable[n1].tableS[pa_processTable[n1].initial].bddR;
    tau = pa_sortTable[pa_processTable[n1].sort].table[0].p;
    /* name1 = pa_processTable[n1].name; */ /* for debugging */
  } else {
    D1 = pa_compositionTable[n1].transitionBDD;
    St1 = pa_compositionTable[n1].stateBDD;
    ini1 = pa_compositionTable[n1].initialBDD;
    tau = pa_sortTable[pa_compositionTable[n1].sort].table[0].p;
    /* name1 = pa_compositionTable[n1].name; */ /* for debugging */
  }

  if (par2 == 0) {
    D2 = pa_processTable[n2].d;
    St2 = pa_processTable[n2].stateBDD;
    ini2 = pa_processTable[n2].tableS[pa_processTable[n2].initial].bddR;
    /* name2 = pa_processTable[n2].name; */ /* for debugging */
  } else if (par2 == 1) {
    D2 = pa_compositionTable[n2].transitionBDD;
    St2 = pa_compositionTable[n2].stateBDD;
    ini2 = pa_compositionTable[n2].initialBDD;
    /* name2 = pa_compositionTable[n2].name; */ /* for debugging */
  }

  /* PRVI PROCES */

  /* spremenimo prvi proces */
  pom = Bdd_RelOp(D1,tau,"#AND Ex xA",TRUE);
  eps = VersisTrCl(pom);

  if (par1 == 0) {
    stab1 = pa_processTable[n1].stab;
  } else {
    stab1 = bdd_termTrue;
    for(i=0; i<pa_compositionTable[n1].numProcesses; i++) {
      stab1 = Bdd_ITE(stab1,
                     pa_processTable[pa_compositionTable[n1].tableP[i]].stab,
                     bdd_termFalse);
    }
  }

  tr1_novi = Bdd_ITE(St1,stab1,bdd_termFalse);
  tr1_novi = Bdd_ITE(tr1_novi,tau,bdd_termFalse);

  eps = Bdd_ITE(eps,bdd_termTrue,stab1);
  eps_rp = Bdd_RelOpSimple(eps,"S2P",TRUE);
  eps_qs = Bdd_RelOpSimple(eps,"R2Q",TRUE);
  Bdd_IncCounter();
  Bdd_Fresh(tr1_novi);
  Bdd_Fresh(eps_rp);
  Bdd_Fresh(eps_qs);

  pom = Bdd_RelOpSimple(D1,"R2P S2Q",TRUE);       /* preimenujemo stanja iz rs v pq */
  pom = Bdd_RelOp(pom,eps_rp,"#AND Ex xP",TRUE);
  pom = Bdd_RelOp(pom,eps_qs,"#AND Ex xQ",TRUE);

  tr1_novi = Bdd_ITE(tr1_novi,bdd_termTrue,pom);
  Bdd_Fortify(tr1_novi);
  Bdd_IncCounter();

  if (par2 != -1) {

    /* DRUGI PROCES */

    /* spremenimo drugi proces */
    pom = Bdd_RelOp(D2,tau,"#AND Ex xA",TRUE);
    eps = VersisTrCl(pom);

    if (par2 == 0) {
      stab2 = pa_processTable[n2].stab;
    } else if (par2 == 1) {
      stab2 = bdd_termTrue;
      for(i=0; i<pa_compositionTable[n2].numProcesses; i++) {
        stab2 = Bdd_ITE(stab2,
                       pa_processTable[pa_compositionTable[n2].tableP[i]].stab,
                       bdd_termFalse);
      }
    }

    tr2_novi = Bdd_ITE(St2,stab2,bdd_termFalse);
    tr2_novi = Bdd_ITE(tr2_novi,tau,bdd_termFalse);

    eps = Bdd_ITE(eps,bdd_termTrue,stab2);
    eps_rp = Bdd_RelOpSimple(eps,"S2P",TRUE);
    eps_qs = Bdd_RelOpSimple(eps,"R2Q",TRUE);
    Bdd_IncCounter();
    Bdd_Fresh(tr2_novi);
    Bdd_Fresh(eps_rp);
    Bdd_Fresh(eps_qs);

    pom = Bdd_RelOpSimple(D2,"R2P S2Q",TRUE);       /* preimenujemo stanja iz rs v pq */
    pom = Bdd_RelOp(pom,eps_rp,"#AND Ex xP",TRUE);
    pom = Bdd_RelOp(pom,eps_qs,"#AND Ex xQ",TRUE);

    tr2_novi = Bdd_ITE(tr2_novi,bdd_termTrue,pom);
    Bdd_Fortify(tr2_novi);
    Bdd_IncCounter();

  }

  /* SHRANJEVANJE VMESNIH GRAFOV */

  /*
  Bdd_SaveFormula("Obs_",name1,tr1_novi);
  Bdd_SaveFormula("Obs_",name2,tr2_novi);
  */

  /* SIBKA OPAZOVALNA EKVIVALENCA */

  if (par2 == -1) {

    /* initial state */
    ini = Bdd_ITE(ini1,Bdd_RelOpSimple(ini1,"R2P",TRUE),bdd_termFalse);
    Bdd_Fortify(ini);

    *eqv = bdd_termTrue;
    EQV = Bisimulation1(ini,eqv,St1,tr1_novi);

  } else {

    /* potrebno je preimenovanje drugega procesa */
    ini2 = Bdd_RelOpSimple(ini2,"R2P",TRUE);
    tr2_novi = Bdd_RelOpSimple(tr2_novi,"R2P S2Q",TRUE);
    St2 = Bdd_RelOpSimple(St2,"R2P",TRUE);
    Bdd_Fortify(ini2);
    Bdd_Fortify(tr2_novi);
    Bdd_Fortify(St2);
    Bdd_IncCounter();

    eqs = bdd_termTrue;

    /* initial eqs */
    /* this part is OK, but it is not necessary */
    /*
    pom1 = Bdd_RelOpSimple(tr1_novi,"Ex xS",TRUE);
    pom2 = Bdd_RelOpSimple(tr2_novi,"Ex xQ",TRUE);
    pom3 = Bdd_ITE(pom1,Bdd_NOT(pom2),pom2);
    pom = Bdd_RelOpSimple(pom3,"Ex xA",TRUE);

    eqs = Bdd_NOT(pom);
    eqs = Bdd_ITE(eqs,St1,bdd_termFalse);
    eqs = Bdd_ITE(eqs,St2,bdd_termFalse);
    Bdd_Fortify(eqs);
    Bdd_IncCounter();
    */

    *eqv = eqs;

    /* initial state */
    ini = Bdd_ITE(ini1,ini2,bdd_termFalse);
    Bdd_Fortify(ini);

    EQV = Bisimulation(ini,eqv,St1,St2,tr1_novi,tr2_novi);

  }

  return(EQV);
}

/**Function****************************************************************
  Synopsis    []
  Description [par1, par2 = 0 (process) or 1 (composition)
               type: 0 = weak, 1 = strong, tau is not special action]
  SideEffects [Result of Trace_Equivalence are deterministic graphs.]
  SeeAlso     []
  ************************************************************************/

Est_Boolean
VersisTraceEquivalence(int type, Bdd_Edge *eqv, int par1, int n1, int par2, int n2,
                       int *det1, int *det2)
{
  Bdd_Edge D1, D2;
  Bdd_Edge tau, stab1, stab2, init1, init2, Ptau1, Ptau2, trcl1, trcl2;
  Bdd_Edge pom, eps, eps_rp, eps_qs;
  Bdd_Edge eqs;
  Bdd_Edge D1det, D2det, St1, St2, InitNew1, InitNew2, initNew;
  Est_Boolean EQV;
  int i,n,s;
  Est_String inname1, inname2, name1, name2, orgname;

  /* dolocimo s, D, St, inname, tau, stab in init */
  /* sort in tau sta za oba procesa enaka! */

  if (par1 == 0) {
    D1 = pa_processTable[n1].d;
    inname1 = pa_processTable[n1].name;
    init1 = pa_processTable[n1].tableS[pa_processTable[n1].initial].bddR;
    s = pa_processTable[n1].sort; /* sort */
    tau = pa_sortTable[s].table[0].p; /* tau */
  } else {
    D1 = pa_compositionTable[n1].transitionBDD;
    inname1 = pa_compositionTable[n1].name;
    init1 = pa_compositionTable[n1].initialBDD;
    s = pa_compositionTable[n1].sort; /* sort */
    tau = pa_sortTable[s].table[0].p; /* tau */
  }

  if (par2 == 0) {
    D2 = pa_processTable[n2].d;
    inname2 = pa_processTable[n2].name;
    init2 = pa_processTable[n2].tableS[pa_processTable[n2].initial].bddR;
  } else {
    D2 = pa_compositionTable[n2].transitionBDD;
    inname2 = pa_compositionTable[n2].name;
    init2 = pa_compositionTable[n2].initialBDD;
  }

  /* PRVI PROCES */

  /* dolocimo Ptau1 - kam vse lahko gres iz posameznega stanja */
  /* eps so tau prehodi v D1 */

  if (type == 0) {

    pom = Bdd_RelOp(D1,tau,"#AND Ex xA",TRUE);
    trcl1 = VersisTrCl(pom);
    Bdd_Fortify(trcl1);
    Bdd_IncCounter();

    if (par1 == 0) {
      stab1 = pa_processTable[n1].stab;
    } else {
      stab1 = bdd_termTrue;
      for(i=0; i<pa_compositionTable[n1].numProcesses; i++) {
        stab1 = Bdd_ITE(stab1,
                       pa_processTable[pa_compositionTable[n1].tableP[i]].stab,
                       bdd_termFalse);
      }
    }

    eps = Bdd_ITE(trcl1,bdd_termTrue,stab1);
    eps_rp = Bdd_RelOpSimple(eps,"S2P",TRUE);
    eps_qs = Bdd_RelOpSimple(eps,"R2Q",TRUE);
    Bdd_IncCounter();
    Bdd_Fresh(eps_rp);
    Bdd_Fresh(eps_qs);

    pom = Bdd_RelOpSimple(D1,"R2P S2Q",TRUE);
    pom = Bdd_RelOp(pom,eps_rp,"#AND Ex xP",TRUE);  /* z leve mnozimo s tau prehodi */
    pom = Bdd_RelOp(pom,eps_qs,"#AND Ex xQ",TRUE);  /* z desne mnozimo s tau prehodi */
    Ptau1 = Bdd_ITE(tau,bdd_termFalse,pom);         /* brisemo tau prehode */
    Bdd_Fortify(Ptau1);
    Bdd_IncCounter();

  }

  if (type == 1) {
    trcl1 = bdd_termFalse;
    Ptau1 = D1;
  }

  name1 = (Est_String) malloc(strlen(inname1) + 5);
  sprintf(name1,"DET_%s",inname1);

  while (Pa_FindProcess(name1) >= 0) {
    name1 = (Est_String) realloc(name1,strlen(name1)+2);
    strcat(name1,"'");
  }

  if (par1 == 0) {
    orgname = strdup(inname1);
  } else {
    orgname = NULL;
  }
  D1det = VersisBuildDet(orgname,name1,init1,Ptau1,trcl1,s);
  n = Pa_FindProcess(name1);
  St1 = pa_processTable[n].stateBDD;
  InitNew1 = pa_processTable[n].tableS[pa_processTable[n].initial].bddR;
  *det1 = n;
  free(name1);

  /*
  fprintf(stdout,"Deterministic graph %s is created.\n",name1);
  Bdd_SystemStat();
  */

  /* DRUGI PROCES */

  if ((par1 == par2) && (n1 == n2)) {

    *det2 = -1;
    *eqv = bdd_termNull;
    return(TRUE);

  } else {

    /* dolocimo Ptau2 - kam vse lahko gres iz posameznega stanja */
    /* eps so tau prehodi v D2 */

    if (type == 0) {

      pom = Bdd_RelOp(D2,tau,"#AND Ex xA",TRUE);
      trcl2 = VersisTrCl(pom);
      Bdd_Fortify(trcl2);
      Bdd_IncCounter();

      if (par2 == 0) {
        stab2 = pa_processTable[n2].stab;
      } else {
        stab2 = bdd_termTrue;
        for(i=0; i<pa_compositionTable[n2].numProcesses; i++) {
          stab2 = Bdd_ITE(stab2,
                         pa_processTable[pa_compositionTable[n2].tableP[i]].stab,
                         bdd_termFalse);
        }
      }

      eps = Bdd_ITE(trcl2,bdd_termTrue,stab2);
      eps_rp = Bdd_RelOpSimple(eps,"S2P",TRUE);
      eps_qs = Bdd_RelOpSimple(eps,"R2Q",TRUE);
      Bdd_IncCounter();
      Bdd_Fresh(eps_rp);
      Bdd_Fresh(eps_qs);

      pom = Bdd_RelOpSimple(D2,"R2P S2Q",TRUE);
      pom = Bdd_RelOp(pom,eps_rp,"#AND Ex xP",TRUE);      /* mnozimo s tau prehodi */
      pom = Bdd_RelOp(pom,eps_qs,"#AND Ex xQ",TRUE);      /* mnozimo s tau prehodi */
      Ptau2 = Bdd_ITE(tau,bdd_termFalse,pom);             /* brisemo tau prehode */
      Bdd_Fortify(Ptau2);
      Bdd_IncCounter();

    }

    if (type == 1) {
      trcl2 = bdd_termFalse;
      Ptau2 = D2;
    }

    name2 = (Est_String) malloc(strlen(inname2) + 5);
    sprintf(name2,"DET_%s",inname2);

    while (Pa_FindProcess(name2) >= 0) {
      name2 = (Est_String) realloc(name2,strlen(name2)+2);
      strcat(name2,"'");
    }

    if (par2 == 0) {
      orgname = strdup(inname2);
    } else {
      orgname = NULL;
    }
    D2det = VersisBuildDet(orgname,name2,init2,Ptau2,trcl2,s);
    n = Pa_FindProcess(name2);
    St2 = pa_processTable[n].stateBDD;
    InitNew2 = pa_processTable[n].tableS[pa_processTable[n].initial].bddR;
    *det2 = n;
    free(name2);

    /*
    fprintf(stdout,"Deterministic graph %s is created.\n",name2);
    Bdd_SystemStat();
    */

  }

  /* preimenovanje InitNew2, D2det in St2 */
  InitNew2 = Bdd_RelOpSimple(InitNew2,"R2P",TRUE);
  D2det = Bdd_RelOpSimple(D2det,"R2P S2Q",TRUE);
  St2 = Bdd_RelOpSimple(St2,"R2P",TRUE);

  Bdd_Fortify(InitNew2);
  Bdd_Fortify(D2det);
  Bdd_Fortify(St2);
  Bdd_IncCounter();

  /* zacetno stanje */
  initNew = Bdd_ITE(InitNew1,InitNew2,bdd_termFalse);
  Bdd_Fortify(initNew);
  Bdd_IncCounter();

  eqs = bdd_termTrue;

  /* zacetni eqs */
  /* this part is OK, but it is not necessary */
  /*
  pom1 = Bdd_RelOpSimple(D1det,"Ex xS",TRUE);
  pom2 = Bdd_RelOpSimple(D2det,"Ex xQ",TRUE);
  pom3 = Bdd_ITE(pom1,Bdd_NOT(pom2),pom2);
  pom = Bdd_RelOpSimple(pom3,"Ex xA",TRUE);

  eqs = Bdd_NOT(pom);
  eqs = Bdd_ITE(eqs,St1,bdd_termFalse);
  eqs = Bdd_ITE(eqs,St2,bdd_termFalse);
  Bdd_Fortify(eqs);
  Bdd_IncCounter();
  */

  /* USED IN BISIUMLATION WHEN LOOKING FOR DIFFERENCE */
  /*
  tmpproc1 = &pa_processTable[*det1];
  tmpproc2 = &pa_processTable[*det2];
  */

  *eqv = eqs;
  EQV = Bisimulation(initNew,eqv,St1,St2,D1det,D2det);

  return(EQV);
}

/**Function****************************************************************
  Synopsis    []
  Description [par1, par2 = 0 (process) or 1 (composition)]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

Est_Boolean
VersisTestEquivalence(Bdd_Edge *eqv, int par1, int n1, int par2, int n2,
                      int *acc1, int *acc2)
{
  Bdd_Edge St1, St2, D1, D2;
  Bdd_Edge tau, stab1, stab2, init1, init2, Ptau1, Ptau2, trcl1, trcl2;
  Bdd_Edge Div1, Div2;
  Bdd_Edge pom, pom1, pom2, pom3, eps, eps_rp, eps_qs;
  Bdd_Edge Acc1, Acc2, AccFalse1, AccFalse2, AccNull1, AccNull2;
  Bdd_Edge D1acc, D2acc;
  Bdd_Edge SR, QP, compat, compat0, compatNull;
  Bdd_Edge InitNew1, InitNew2, initNew, eqs;
  Est_Boolean EQV;
  int i,s;
  Est_String inname1, inname2, name1, name2;

  /* dolocimo s, D, St, inname, tau, stab in init */
  /* sort in tau sta za oba procesa enaka! */

  if (par1 == 0) {
    D1 = pa_processTable[n1].d;
    inname1 = pa_processTable[n1].name;
    init1 = pa_processTable[n1].tableS[pa_processTable[n1].initial].bddR;
    s = pa_processTable[n1].sort; /* sort */
    tau = pa_sortTable[s].table[0].p; /* tau */
  } else {
    D1 = pa_compositionTable[n1].transitionBDD;
    inname1 = pa_compositionTable[n1].name;
    init1 = pa_compositionTable[n1].initialBDD;
    s = pa_compositionTable[n1].sort; /* sort */
    tau = pa_sortTable[s].table[0].p; /* tau */
  }

  if (par2 == 0) {
    D2 = pa_processTable[n2].d;
    inname2 = pa_processTable[n2].name;
    init2 = pa_processTable[n2].tableS[pa_processTable[n2].initial].bddR;
  } else {
    D2 = pa_compositionTable[n2].transitionBDD;
    inname2 = pa_compositionTable[n2].name;
    init2 = pa_compositionTable[n2].initialBDD;
  }

  /* PRVI PROCES */

  /* dolocimo Ptau1 - kam vse lahko gres iz posameznega stanja */
  /* eps so tau prehodi v D1 */

  pom = Bdd_RelOp(D1,tau,"#AND Ex xA",TRUE);
  trcl1 = VersisTrCl(pom);
  Bdd_Fortify(trcl1);
  Bdd_IncCounter();

  if (par1 == 0) {
    stab1 = pa_processTable[n1].stab;
  } else {
    stab1 = bdd_termTrue;
    for(i=0; i<pa_compositionTable[n1].numProcesses; i++) {
      stab1 = Bdd_ITE(stab1,
                     pa_processTable[pa_compositionTable[n1].tableP[i]].stab,
                     bdd_termFalse);
    }
  }

  eps = Bdd_ITE(trcl1,bdd_termTrue,stab1);
  eps_rp = Bdd_RelOpSimple(eps,"S2P",TRUE);
  eps_qs = Bdd_RelOpSimple(eps,"R2Q",TRUE);
  Bdd_IncCounter();
  Bdd_Fresh(eps_rp);
  Bdd_Fresh(eps_qs);

  pom = Bdd_RelOpSimple(D1,"R2P S2Q",TRUE);
  pom = Bdd_RelOp(pom,eps_rp,"#AND Ex xP",TRUE);   /* z leve mnozimo s tau prehodi */
  pom = Bdd_RelOp(pom,eps_qs,"#AND Ex xQ",TRUE);   /* z desne mnozimo s tau prehodi */
  Ptau1 = Bdd_ITE(tau,bdd_termFalse,pom);          /* brisemo tau prehode */
  Bdd_Fortify(Ptau1);
  Bdd_IncCounter();

  /* dolocimo divergentna stanja */
  Div1 = Versis_CheckDivergence(D1,tau);
  Bdd_Fortify(Div1);
  Bdd_IncCounter();

  name1 = (Est_String) malloc(strlen(inname1) + 5);
  sprintf(name1,"ACC_%s",inname1);

  while (Pa_FindProcess(name1) >= 0) {
    name1 = (Est_String) realloc(name1,strlen(name1)+2);
    strcat(name1,"'");
  }

  D1acc = BuildAcc(par1,inname1,name1,D1,init1,Ptau1,trcl1,Div1,s,tau,
                   &Acc1,&AccFalse1,&AccNull1,&InitNew1);
  St1 = pa_processTable[Pa_FindProcess(name1)].stateBDD;

  /*
  fprintf(stdout,"Acceptance graph %s is created.\n",name1);
  */

  /* DRUGI PROCES */

  if ((par1 == par2) && (n1 == n2)) {

    name2 = strdup(name1);
    D2acc = D1acc;
    St2 = St1;
    Acc2 = Acc1;
    AccFalse2 = AccFalse1;
    AccNull2 = AccNull1;
    InitNew2 = InitNew1;

  } else {

    /* dolocimo Ptau2 - kam vse lahko gres iz posameznega stanja */
    /* eps so tau prehodi v D2 */

    pom = Bdd_RelOp(D2,tau,"#AND Ex xA",TRUE);
    trcl2 = VersisTrCl(pom);
    Bdd_Fortify(trcl2);
    Bdd_IncCounter();

    if (par2 == 0) {
      stab2 = pa_processTable[n2].stab;
    } else {
      stab2 = bdd_termTrue;
      for(i=0; i<pa_compositionTable[n2].numProcesses; i++) {
        stab2 = Bdd_ITE(stab2,
                       pa_processTable[pa_compositionTable[n2].tableP[i]].stab,
                       bdd_termFalse);
      }
    }

    eps = Bdd_ITE(trcl2,bdd_termTrue,stab2);
    eps_rp = Bdd_RelOpSimple(eps,"S2P",TRUE);
    eps_qs = Bdd_RelOpSimple(eps,"R2Q",TRUE);
    Bdd_IncCounter();
    Bdd_Fresh(eps_rp);
    Bdd_Fresh(eps_qs);

    pom = Bdd_RelOpSimple(D2,"R2P S2Q",TRUE);
    pom = Bdd_RelOp(pom,eps_rp,"#AND Ex xP",TRUE);      /* mnozimo s tau prehodi */
    pom = Bdd_RelOp(pom,eps_qs,"#AND Ex xQ",TRUE);      /* mnozimo s tau prehodi */
    Ptau2 = Bdd_ITE(tau,bdd_termFalse,pom);             /* brisemo tau prehode */
    Bdd_Fortify(Ptau2);
    Bdd_IncCounter();

    /* dolocimo divergentna stanja */
    Div2 = Versis_CheckDivergence(D2,tau);
    Bdd_Fortify(Div2);
    Bdd_IncCounter();

    name2 = (Est_String) malloc(strlen(inname2) + 5);
    sprintf(name2,"ACC_%s",inname2);

    while (Pa_FindProcess(name2) >= 0) {
      name2 = (Est_String) realloc(name2,strlen(name2)+2);
      strcat(name2,"'");
    }

    D2acc = BuildAcc(par2,inname2,name2,D2,init2,Ptau2,trcl2,Div2,s,tau,
                     &Acc2,&AccFalse2,&AccNull2,&InitNew2);
    St2 = pa_processTable[Pa_FindProcess(name2)].stateBDD;

    /*
    fprintf(stdout,"Acceptance graph %s is created.\n",name2);
    */

  }

  /* RETURN ACCEPTANCE GRAPHS */
  *acc1 = Pa_FindProcess(name1);
  *acc2 = Pa_FindProcess(name2);

  free(name1);
  free(name2);

  /*
  fprintf(stdout,"Both acceptance graphs are created.\n");
  */

  /* preimenovanje InitNew2, D2acc in St2 */
  InitNew2 = Bdd_RelOpSimple(InitNew2,"R2P",TRUE);
  D2acc = Bdd_RelOpSimple(D2acc,"R2P S2Q",TRUE);
  St2 = Bdd_RelOpSimple(St2,"R2P",TRUE);

  Bdd_Fortify(InitNew2);
  Bdd_Fortify(D2acc);
  Bdd_Fortify(St2);
  Bdd_IncCounter();

  /* compat0 */
  /* dobimo compat0 (r,p) */
  AccFalse2 = Bdd_RelOpSimple(AccFalse2,"R2P",TRUE);
  compat0 = Bdd_ITE(AccFalse1,AccFalse2,bdd_termFalse);

  /* compat */
  /* uporabljamo Acc1 (s,a,r) in Acc2 (q,a,p) */
  /* dobimo compat (r,p) */
  Acc2 = Bdd_RelOpSimple(Acc2,"R2P S2Q",TRUE);
  SR = Bdd_RelOpSimple(Acc1,"Ex xA",TRUE);
  QP = Bdd_RelOpSimple(Acc2,"Ex xA",TRUE);

  /* ORIGINAL VERSION */
  pom = Bdd_RelOp(Acc2,Acc1,"#IMPL Ax xA",TRUE); /* pom = AxA (Acc2 => Acc1) */
  pom = Bdd_RelOp(pom,QP,"#AND Ex xP",TRUE);     /* pom = ExP (QP * pom) */
  pom = Bdd_RelOp(SR,pom,"#IMPL Ax xR",TRUE);    /* pom = AxR (SR => pom) */
  compat = pom;
  pom = Bdd_RelOp(Acc1,Acc2,"#IMPL Ax xA",TRUE); /* pom = AxA (Acc1 => Acc2) */
  pom = Bdd_RelOp(pom,SR,"#AND Ex xR",TRUE);     /* pom = ExR (SR * pom) */
  pom = Bdd_RelOp(QP,pom,"#IMPL Ax xP",TRUE);    /* pom = AxP (QP => pom) */
  compat = Bdd_ITE(compat,pom,bdd_termFalse);
  compat = Bdd_RelOpSimple(compat,"S2R Q2P",TRUE);

  /* EXPERIMENTAL VERSION */
  /*
  pom = Bdd_RelOp(Acc1,Bdd_NOT(Acc2),"#OR Ax xA",TRUE);    /+* pom = AxA (Acc2 => Acc1) *+/
  pom = Bdd_RelOp(pom,QP,"#AND Ex xP",TRUE);               /+* pom = ExP (QP * pom) *+/
  pom = Bdd_RelOp(pom,Bdd_NOT(SR),"#OR Ax xR",TRUE);       /+* pom = AxR (SR => pom) *+/
  compat = pom;
  pom = Bdd_RelOp(Acc2,Bdd_NOT(Acc1),"#OR Ax xA",TRUE);    /+* pom = AxA (Acc1 => Acc2) *+/
  pom = Bdd_RelOp(pom,SR,"#AND Ex xR",TRUE);               /+* pom = ExR (SR * pom) *+/
  pom = Bdd_RelOp(pom,Bdd_NOT(QP),"#OR Ax xP",TRUE);       /+* pom = AxP (QP => pom) *+/
  compat = Bdd_ITE(compat,pom,bdd_termFalse);
  compat = Bdd_RelOpSimple(compat,"S2R Q2P",TRUE);
  */

  /* compatNull */
  /* dobimo compatNull (r,p) */
  AccNull2 = Bdd_RelOpSimple(AccNull2,"R2P",TRUE);
  compatNull = Bdd_ITE(AccNull1,AccNull2,bdd_termFalse);

  /* stanja z enakimi prehodi */
  /* uporabljamo D1acc (r,a,s) in D2acc (p,a,q) */
  /* dobimo eqs (r,p) */
  pom1 = Bdd_RelOpSimple(D1acc,"Ex xS",TRUE);
  pom2 = Bdd_RelOpSimple(D2acc,"Ex xQ",TRUE);

  /* ORIGINAL VERSION */
  pom3 = Bdd_ITE(pom1,pom2,Bdd_NOT(pom2));
  eqs = Bdd_RelOpSimple(pom3,"Ax xA",TRUE);

  /* EXPERIMENTAL VERSION */
  /*
  pom3 = Bdd_ITE(pom1,Bdd_NOT(pom2),pom2);
  pom = Bdd_RelOpSimple(pom3,"Ex xA",TRUE);
  eqs = Bdd_NOT(pom);
  */

  /* DELETE NONEXISTING STATES */
  eqs = Bdd_ITE(eqs,St1,bdd_termFalse);
  eqs = Bdd_ITE(eqs,St2,bdd_termFalse);

  /* celotna zacetna relacija */
  pom = Bdd_ITE(compat0,bdd_termTrue,compat);
  pom = Bdd_ITE(pom,bdd_termTrue,compatNull);
  eqs = Bdd_ITE(eqs,pom,bdd_termFalse);
  Bdd_Fortify(eqs);
  Bdd_IncCounter();

  /* zacetno stanje */
  initNew = Bdd_ITE(InitNew1,InitNew2,bdd_termFalse);
  Bdd_Fortify(initNew);
  Bdd_IncCounter();

  *eqv = eqs;
  EQV = Bisimulation(initNew,eqv,St1,St2,D1acc,D2acc);

  return(EQV);
}

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

Bdd_Edge
VersisBuildDet(Est_String orgname, Est_String newname, Bdd_Edge init,
               Bdd_Edge Ptau, Bdd_Edge trcl, int s)
{
  Bdd_Edge final;
  Bdd_Edge pom;
  int i,n,org;

  /* tvorimo ogrodje novega procesa */
  n = Pa_FindProcess(newname);
  if (n != -1) {
    Pa_DeleteProcess(n);
  }
  n = Pa_AddNewProcess(newname);
  pa_processTable[n].sort = s;
  pa_processTable[n].numStates= 0;
  pa_processTable[n].initial = 0;

  ST.table = (VersisST *) malloc (sizeof(VersisST));
  ST.num = 0;

  /* dolocimo zacetno stanje */
  pom = Bdd_ITE(init,trcl,bdd_termFalse);
  pom = Bdd_NewState(pom);
  init = Bdd_ITE(init,bdd_termTrue,pom);
  Bdd_Fortify(init);

  /* zberemo koncna stanja originalnega procesa */
  final = bdd_termFalse;
  if (orgname) {
    org = Pa_FindProcess(orgname);
    if (org != -1) {
      for(i=0; i<pa_processTable[org].numStates; i++) {
        if (pa_processTable[org].tableS[i].final) {
          final = Bdd_ITE(final,bdd_termTrue,pa_processTable[org].tableS[i].bddR);
        }
      }
      Bdd_Fortify(final);
    }
  }

  /* rekurzivna funkcija, ki zgradi deterministicni proces */
  BuildDetR(Ptau,init,s,final);
  free(ST.table);

  /* encode process */
  Pa_EncodeProcess(newname);
  Bdd_IncCounter();

  return pa_processTable[n].d;
}


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

/**Function****************************************************************
  Synopsis    []
  Description [Transition relations must be D1(r,a,s) and D2(p,a,q)]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

static Est_Boolean
Bisimulation(Bdd_Edge init, Bdd_Edge *eqv, Bdd_Edge St1, Bdd_Edge St2,
             Bdd_Edge D1, Bdd_Edge D2)
{
  Bdd_Edge eqs, eqs_old_rp, eqs1, eqs2;
  Bdd_Edge pom;
  int i;

  eqs = *eqv;

  /* COMPARE INITIAL STATES */
  pom = Bdd_ITE(init,eqs,bdd_termFalse);
  if (Bdd_isEqv(pom,bdd_termFalse)) return FALSE;

  /*
  printf("<Bisimulation>");
  */

  /* ITERATION */
  i = 0;
  do {
    /* LOOKING FOR DIFFERENCE */
    /* YOU NEED TO SET VARIABLES tmpproc1 AND tmpproc2 IN VersisXXXEquivalence */
    /*
    printf("\nBisimulation before %d iteration.\n",i);
    Pa_DecodeProcProcPair(tmpproc1,tmpproc2,eqs,TRUE);
    printf("\n");
    */

    /*
    printf("\nNOT EQUIVALENT STATES OF PROCESS %s before %d iteration.\n",tmpproc1->name,i);
    pom = Bdd_RelOpSimple(eqs,"Ex xP",TRUE);
    pom = Bdd_ITE(pom,bdd_termFalse,tmpproc1->stateBDD);
    Pa_DecodeProcessStates(tmpproc1,pom,TRUE);
    printf("\n");

    printf("\nNOT EQUIVALENT STATES OF PROCESS %s before %d iteration.\n",tmpproc2->name,i);
    pom = Bdd_RelOpSimple(eqs,"R2P P2R",TRUE);
    pom = Bdd_RelOpSimple(pom,"Ex xP",TRUE);
    pom = Bdd_ITE(pom,bdd_termFalse,tmpproc2->stateBDD);
    Pa_DecodeProcessStates(tmpproc2,pom,TRUE);
    printf("\n");
    */

    i++;

    eqs_old_rp = eqs;                           /* eqs = eqs(r,p) */
    eqs = Bdd_RelOpSimple(eqs,"R2S P2Q",TRUE);

    /* Part 1 */
    pom = Bdd_RelOp(D2,eqs,"#AND Ex xQ",TRUE);  /* pom = pom(a,p,s) */
    eqs1 = Bdd_NewEq(D1,pom);                   /* eqs1 = eqs1(r,p) */
    eqs1 = Bdd_ITE(eqs1,St1,bdd_termFalse);

    Bdd_IncCounter();
    Bdd_Fresh(eqs);
    Bdd_Fresh(eqs1);
    Bdd_Fresh(eqs_old_rp);

    /* Part 2 */
    pom = Bdd_RelOp(D1,eqs,"#AND Ex xS",TRUE);  /* pom = pom(a,r,q) */
    eqs2 = Bdd_NewEq(D2,pom);                   /* eqs2 = eqs2(r,p) */
    eqs2 = Bdd_ITE(eqs2,St2,bdd_termFalse);

    Bdd_IncCounter();
    Bdd_Fresh(eqs1);
    Bdd_Fresh(eqs2);
    Bdd_Fresh(eqs_old_rp);

    /* new eqs */
    eqs = Bdd_ITE(eqs1,eqs2,bdd_termFalse);
    eqs = Bdd_ITE(eqs,eqs_old_rp,bdd_termFalse);

    /* are initial states still equivalent? */
    pom = Bdd_ITE(init,eqs,bdd_termFalse);
    if (Bdd_isEqv(pom,bdd_termFalse)) {
      return FALSE;
    }

    Bdd_IncCounter();
    Bdd_Fresh(eqs);

    /*
    printf("<%d>",i);
    */

  } while (!Bdd_isEqv(eqs_old_rp,eqs));

  *eqv = eqs;
  return TRUE;
}

/**Function****************************************************************
  Synopsis    []
  Description [Transition relation must be D(r,a,s)]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

static Est_Boolean
Bisimulation1(Bdd_Edge init, Bdd_Edge *eqv, Bdd_Edge St, Bdd_Edge D)
{
  Bdd_Edge D1, D2;
  Bdd_Edge eqs, eqs1, eqs2, eqs_old_rp;
  Bdd_Edge pom;
  int i;

  eqs = *eqv;
  D1 = D;
  D2 = Bdd_RelOpSimple(D,"R2P S2Q",TRUE);
  Bdd_Fortify(D2);

  /* COMPARE INITIAL STATES */
  pom = Bdd_ITE(init,eqs,bdd_termFalse);
  if (Bdd_isEqv(pom,bdd_termFalse)) return FALSE;

  /* ITERATION */
  i = 0;
  do {
    i++;

    eqs_old_rp = eqs;                       /* eqs = eqs(r,p) */
    eqs = Bdd_RelOpSimple(eqs,"R2S P2Q",TRUE);

    /* Part 1 and 2 */
    eqs1 = Bdd_RelOp(D2,eqs,"#AND Ex xQ",TRUE);                 /* eqs1 = eqs1(p,a,s) */
    eqs1 = Bdd_NewEq(D1,eqs1);              /* eqs1 = eqs1(r,p) */
    eqs1 = Bdd_ITE(eqs1,St,bdd_termFalse);

    eqs2 = Bdd_RelOpSimple(eqs1,"R2P P2R",TRUE);

    Bdd_IncCounter();
    Bdd_Fresh(eqs1);
    Bdd_Fresh(eqs2);
    Bdd_Fresh(eqs_old_rp);

    /* novi eqs */
    eqs = Bdd_ITE(eqs1,eqs2,bdd_termFalse);
    eqs = Bdd_ITE(eqs,eqs_old_rp,bdd_termFalse);

    /* are initial states still equivalent? */
    pom = Bdd_ITE(init,eqs,bdd_termFalse);
    if (Bdd_isEqv(pom,bdd_termFalse)) {
      return FALSE;
    }

    Bdd_IncCounter();
    Bdd_Fresh(eqs);

  } while (!Bdd_isEqv(eqs_old_rp,eqs));

  *eqv = eqs;
  return TRUE;
}

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

static Bdd_Edge
BuildAcc(int par, Est_String name, Est_String newname,
         Bdd_Edge D, Bdd_Edge init, Bdd_Edge Ptau,
         Bdd_Edge trcl, Bdd_Edge Div, int s, Bdd_Edge tau,
         Bdd_Edge *Acc, Bdd_Edge *AccFalse, Bdd_Edge *AccNull,
         Bdd_Edge *InitNew)
{
  Pa_State *tabS;
  Bdd_Edge pom,pom1;
  int n,i;
  Est_Boolean b;

  /* tvorimo ogrodje novega procesa */
  n = Pa_FindProcess(newname);
  if (n != -1) {
    Pa_DeleteProcess(n);
  }
  n = Pa_AddNewProcess(newname);
  pa_processTable[n].sort = s;
  pa_processTable[n].numStates= 0;
  pa_processTable[n].initial = 0;

  ST.table = (VersisST *) malloc (sizeof(VersisST));
  ST.num = 0;

  /* dolocimo zacetno stanje */
  pom = Bdd_ITE(init,trcl,bdd_termFalse);
  pom = Bdd_NewState(pom);
  init = Bdd_ITE(init,bdd_termTrue,pom);
  Bdd_Fortify(init);

  /* rekurzivna funkcija, ki zgradi acc proces */
  pom1 = Bdd_ITE(init,Div,bdd_termFalse);
  b = Bdd_isEqv(pom1,bdd_termFalse);
  BuildAccR(par,name,D,Ptau,init,tau,Div,b,s);
  free(ST.table);

  /* encode process */
  Pa_EncodeProcess(newname);
  Bdd_IncCounter();

  /* initial state */
  *InitNew = pa_processTable[n].tableS[pa_processTable[n].initial].bddR;

  /* build acceptance relations */
  tabS = pa_processTable[n].tableS;
  *Acc = bdd_termFalse;
  *AccFalse = bdd_termFalse;
  *AccNull = bdd_termFalse;
  for (i=0; i<pa_processTable[n].numStates; i++) {
    if (Bdd_isNull(tabS[i].acc)) {
      *AccNull = Bdd_ITE(*AccNull,bdd_termTrue,tabS[i].bddR);
    } else {
      if (Bdd_isEqv(tabS[i].acc,bdd_termFalse)) {
        *AccFalse = Bdd_ITE(*AccFalse,bdd_termTrue,tabS[i].bddR);
      } else {
        pom = Bdd_ITE(tabS[i].bddS,tabS[i].acc,bdd_termFalse);
        *Acc = Bdd_ITE(*Acc,bdd_termTrue,pom);
      }
    }
  }

  Bdd_Fortify(*Acc);
  Bdd_Fortify(*AccFalse);
  Bdd_Fortify(*AccNull);
  Bdd_IncCounter();

  return pa_processTable[n].d;
}

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

static int
BuildAccR(int par, Est_String name,
          Bdd_Edge D, Bdd_Edge Ptau, Bdd_Edge S, Bdd_Edge tau,
          Bdd_Edge Div, Est_Boolean b, int s)
{
  int j;
  int t,tnew;
  Bdd_Edge a;
  static Bdd_Edge pom;  /* STATIC TO MINIMIZE STACK PROBLEMS */
  static Bdd_Edge Sa;   /* STATIC TO MINIMIZE STACK PROBLEMS */
  static Est_Boolean c; /* STATIC TO MINIMIZE STACK PROBLEMS */
  static Est_String x;  /* STATIC TO MINIMIZE STACK PROBLEMS */

  /*
  if (b) printf("b TRUE\n"); else printf("b FALSE\n");
  */

  if (b) {
   pom = MakeAcc(D,tau,S);
   Bdd_Fortify(pom);
  } else {
   pom = bdd_termNull;
  }

  if (b) x = (Est_String) strdup("s"); else x = (Est_String) strdup("e");
  t = Pa_FOANextStateProcess(&pa_processTable[pa_processes-1],x);
  free(x);

  pa_processTable[pa_processes-1].tableS[t].acc = pom;
  AddStateTable(S,b,t);

  /* za vsako akcijo, ki gre iz S dodamo prehode */
  /* akcija pa_sortTable[0] je akcija TAU, ki jo preskocimo! */

  for (j=1; j<pa_sortTable[s].numActions; j++) {
    a = pa_sortTable[s].table[j].p;

    /*
    printf("Action: %s\n",pa_sortTable[s].table[j].name);
    Bdd_PutsFunction(a);
    */

    /* output action */

    pom = Bdd_ITE(pa_sortTable[s].a0,a,bdd_termFalse);
    Sa = Bdd_ITE(S,pom,bdd_termFalse);
    Sa = Bdd_ITE(Sa,Ptau,bdd_termFalse);
    if (!Bdd_isEqv(Sa,bdd_termFalse)) {
      Sa = Bdd_NewState(Sa);
      Bdd_Fortify(Sa);
      pom = Bdd_ITE(Sa,Div,bdd_termFalse);
      c = (b && Bdd_isEqv(pom,bdd_termFalse));

      /*
      printf("OUTPUT Sa:\n");
      Bdd_PutsFunction(Sa);
      */

      if (!FindStateTable(Sa,c,&tnew))
        tnew = BuildAccR(par,name,D,Ptau,Sa,tau,Div,c,s);
      Pa_FOATransition(&pa_processTable[pa_processes-1], t, j, 1, tnew);
    }

    /* input action */

    pom = Bdd_ITE(pa_sortTable[s].a0,bdd_termFalse,a);
    Sa = Bdd_ITE(S,pom,bdd_termFalse);
    Sa = Bdd_ITE(Sa,Ptau,bdd_termFalse);
    if (!Bdd_isEqv(Sa,bdd_termFalse)) {
      Sa = Bdd_NewState(Sa);
      Bdd_Fortify(Sa);
      pom = Bdd_ITE(Sa,Div,bdd_termFalse);
      c = (b && Bdd_isEqv(pom,bdd_termFalse));

      /*
      printf("INPUT Sa:\n");
      Bdd_PutsFunction(Sa);
      */

      if (!FindStateTable(Sa,c,&tnew))
        tnew = BuildAccR(par,name,D,Ptau,Sa,tau,Div,c,s);
      Pa_FOATransition(&pa_processTable[pa_processes-1], t, j, 0, tnew);
    }
  }

  return t;
}

/**Function****************************************************************
  Synopsis    []
  Description [Determine acceptance set. The resulting set is not minimal!
               Special functions for comparing them should be used.]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

static Bdd_Edge
MakeAcc(Bdd_Edge D, Bdd_Edge tau, Bdd_Edge S)
{
  Bdd_Edge pom,pom1,eps,acc;

  pom = Bdd_RelOp(S,D,"#AND Ex xS",TRUE);
  pom1 = Bdd_RelOpSimple(pom,"Ex xA",TRUE);

  if (Bdd_isEqv(pom1,S)) {
    eps = Bdd_RelOp(pom,tau,"#AND Ex xA",TRUE);
    acc = Bdd_ITE(eps,bdd_termFalse,pom);
  } else {
    acc = bdd_termFalse;
  }

  return acc;
}

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

static void
MinAcc(int numNS, Pa_State *tabNS, int numS, Pa_State *tabS)
{
  Bdd_Edge f,ri,pom;
  int i,j;

  for (i=0; i<numNS; i++) {
    f = tabNS[i].acc;
    if (!Bdd_isNull(f)) {
      if (!Bdd_isEqv(f,bdd_termFalse)) {
        for (j=0; j<numS; j++) {
          ri = tabS[j].bddR;
          pom = Bdd_RelOp(f,ri,"#AND Ex xR",TRUE);
          pom = Bdd_NOT(pom);
          if (!Bdd_isEqv(pom,bdd_termTrue)) {
            pom = Bdd_RelOp(pom,f,"#AND Ex xA",TRUE);
            pom = Bdd_ITE(pom,bdd_termTrue,ri);
          }
          f = Bdd_ITE(f,pom,bdd_termFalse);
        }
      }
      tabNS[i].minacc = f;
    }
  }
}

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

static Est_Boolean
CmpAcc(Bdd_Edge acc1, Bdd_Edge acc2)
{
  Bdd_Edge pom,pom1;
  Bdd_Edge R,S;

  acc2 = Bdd_RelOpSimple(acc2,"R2S",TRUE);
  R = Bdd_RelOpSimple(acc1,"Ex xA",TRUE);
  S = Bdd_RelOpSimple(acc2,"Ex xA",TRUE);

  pom = Bdd_RelOp(acc1,Bdd_NOT(acc2),"#OR Ax xA",TRUE);    /* pom = AxA (acc2 => acc1) */
  pom = Bdd_RelOp(pom,S,"#AND Ex xS",TRUE);                /* pom = ExS (S * pom) */
  pom = Bdd_RelOp(pom,Bdd_NOT(R),"#OR Ax xR",TRUE);        /* must = AxR (R => pom) */
  pom1 = pom;

  pom = Bdd_RelOp(acc2,Bdd_NOT(acc1),"#OR Ax xA",TRUE);    /* pom = AxA (acc1 => acc2) */
  pom = Bdd_RelOp(pom,R,"#AND Ex xR",TRUE);                /* pom = ExR (R * pom) */
  pom = Bdd_RelOp(pom,Bdd_NOT(S),"#OR Ax xS",TRUE);        /* must = AxS (S => pom) */
  pom1 = Bdd_ITE(pom1,pom,bdd_termFalse);

  if (Bdd_isEqv(pom1,bdd_termTrue)) {
    return TRUE;
  } else {
    return FALSE;
  }
}

/**Function****************************************************************
  Synopsis    []
  Description [type: 0 = weak, 1 = strong, tau is not special action]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

static int
BuildDetR(Bdd_Edge Ptau, Bdd_Edge S, int s, Bdd_Edge final)
{
  int j;
  int t,tnew;
  Bdd_Edge a;
  static Bdd_Edge pom;  /* STATIC TO MINIMIZE STACK PROBLEMS */
  static Bdd_Edge Sa;   /* STATIC TO MINIMIZE STACK PROBLEMS */
  static Est_String x;  /* STATIC TO MINIMIZE STACK PROBLEMS */

  x = (Est_String) strdup("s");
  t = Pa_FOANextStateProcess(&pa_processTable[pa_processes-1],x);
  free(x);

  pa_processTable[pa_processes-1].tableS[t].acc = bdd_termFalse;
  AddStateTable(S,TRUE,t);

  /* dolocimo, ali je stanje koncno */
  /* stanje je koncno, ce je VSAJ ENO izmed stanj v pripadajocem razredu koncno! */

  pom = Bdd_ITE(S,final,bdd_termFalse);
  if (!Bdd_isEqv(pom,bdd_termFalse)) {
    pa_processTable[pa_processes-1].tableS[t].final = TRUE;
  }

  /* za vsako akcijo, ki gre iz S dodamo prehode */

  /*
  printf("\nZacetek BuildDetR...\n");
  */

  for (j=0; j<pa_sortTable[s].numActions; j++) {
    a = pa_sortTable[s].table[j].p;

    /*
    printf("Action: %s\n",pa_sortTable[s].table[j].name);
    Bdd_WriteFunction(a);
    */

    /* output action */

    pom = Bdd_ITE(pa_sortTable[s].a0,a,bdd_termFalse);
    Sa = Bdd_ITE(S,pom,bdd_termFalse);
    Sa = Bdd_ITE(Sa,Ptau,bdd_termFalse);
    if (!Bdd_isEqv(Sa,bdd_termFalse)) {
      Sa = Bdd_NewState(Sa);
      Bdd_Fortify(Sa);
      if (!FindStateTable(Sa,TRUE,&tnew))
        tnew = BuildDetR(Ptau,Sa,s,final);
      Pa_FOATransition(&pa_processTable[pa_processes-1], t, j, 1, tnew);
    }

    /* input action */

    pom = Bdd_ITE(pa_sortTable[s].a0,bdd_termFalse,a);
    Sa = Bdd_ITE(S,pom,bdd_termFalse);
    Sa = Bdd_ITE(Sa,Ptau,bdd_termFalse);
    if (!Bdd_isEqv(Sa,bdd_termFalse)) {
      Sa = Bdd_NewState(Sa);
      Bdd_Fortify(Sa);
      if (!FindStateTable(Sa,TRUE,&tnew))
        tnew = BuildDetR(Ptau,Sa,s,final);
      Pa_FOATransition(&pa_processTable[pa_processes-1], t, j, 0, tnew);
    }
  }

  /*
  printf("Konec BuildDetR!\n\n");
  */

  return t;
}

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

static void
AddStateTable(Bdd_Edge S, Est_Boolean b, int t)
{

  if (ST.num == 0) {
    ST.table[0].S = S;
    ST.table[0].b = b;
    ST.table[0].t = t;
    ST.num++;
  } else {
    ST.num++;
    ST.table = (VersisST *) realloc (ST.table, ST.num * sizeof(VersisST));
    ST.table[ST.num-1].S = S;
    ST.table[ST.num-1].b = b;
    ST.table[ST.num-1].t = t;
  }
}

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

static Est_Boolean
FindStateTable(Bdd_Edge S, Est_Boolean b, int *t)
{
  int i=0;

  while (i<ST.num) {
    if ((Bdd_isEqv(ST.table[i].S,S)) && (ST.table[i].b == b)) {
      *t = ST.table[i].t;
      return TRUE;
    } else {
      i++;
    }
  }

  return FALSE;
}

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

static void
WriteStateTable(int n)
{
  int i;

  printf("\nSTATE TABLE:\n");
  for (i=0; i<ST.num; i++) {

    printf("State %d: ",i);
    Pa_DecodeProcessStates(&pa_processTable[n], ST.table[i].S, TRUE);
    printf("\n");
  }
}
