/**CFile*******************************************************************
  PackageName [mc]
  Synopsis    [Package 'mc' provides a symbolic ACTLW model checker]

  FileName    [mcMain.c]
  Revision    [$Revision: 76 $]
  Date        [$Date: 2013-04-26 14:26:09 +0200 (pet, 26 apr 2013) $]
  Author      [Robert Meolic (meolic@uni-mb.si)]
  Description [File mcMain.c contains main functions of a symbolic
               ACTLW model checker.]
  SeeAlso     [mc.h, mcInt.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 "mcInt.h"

/*-----------------------------------------------------------------------*/
/* Type declarations                                                     */
/*-----------------------------------------------------------------------*/

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

/* EXPORTED VARIABLES */

int mc_status = 0;                   /* initialization status */
int mc_formulae = 0;                 /* number of formulae */
Mc_Formula *mc_formulaTable = NULL;  /* table of formulae */
int mcMacros = 0;                    /* number of macros */
McMacro *mcMacroTable = NULL;        /* table of macros */

/* INTERNAL VARIABLES */

Est_Boolean trace = FALSE;          /* trace of ACTL parsing */
Est_Boolean xtrace = FALSE;         /* extended trace of ACTL parsing */
Est_Boolean explain = FALSE;        /* explain generated diagnostic */
Est_Boolean tracepath = FALSE;      /* full paths in diagnostic */
Est_Boolean diagnostic = FALSE;     /* generate linear w/c */
Est_Boolean automaton = FALSE;      /* generate w/c automaton */
Est_Boolean minimize = FALSE;       /* minimize w/c automaton */
Est_Boolean tree = FALSE;           /* generate tree-like w/c */
Est_Boolean progress = FALSE;       /* report progress of MC */

const int MC_SIMPLE = 0;
const int MC_TRACE = 1;
const int MC_XTRACE = 2;
const int MC_EXPLAIN = 4;
const int MC_TRACEPATH = 8;
const int MC_DIAGNOSTIC = 16;
const int MC_AUTOMATON = 32;
const int MC_MINIMIZE = 64;
const int MC_TREE = 128;
const int MC_PROGRESS = 256;

/* used and not initialized by flex/bison */
char *mctext = NULL; /* from lex.mc.c */
void *mcleng = NULL; /* from lex.mc.c */
int mcnerrs = 0;     /* from mc.tab.c: number of syntax errors so far */
int mcchar = 0;      /* from mc.tab.c: the lookahead symbol */
struct mcstype {Bdd_Edge i1; Bdd_Edge i2; Bdd_Edge i3; void *i4; void *i5; void *i6;}
   mclval = {{NULL,FALSE},{NULL,FALSE},{NULL,FALSE},NULL,NULL,NULL};
   /* the semantic value of the lookahead symbol */
   /* this should be compatible with the union from mcParser.y */

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

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

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

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

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

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

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

void
Mc_InitPkg()
{
  if (mc_status == 1) {
    printf("\nModel checking package is already initialized. ");
    return;
  } else {
    mc_status = 1;
  }

  mc_formulae = 0;

  return;
}

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

void
Mc_ExitPkg()
{
  int i;

  if (mc_status == 0) {
    printf("\nModel checking package is not initialized. ");
    return;
  } else {
    mc_status = 0;
  }

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

  /* DELETE FORMULAE */
  /*
  printf("Delete formulae...\n");
  */
  for(i=0;i<mc_formulae;i++) {
    free(mc_formulaTable[i].name);
    free(mc_formulaTable[i].formula);
  }
  if (mc_formulaTable) free(mc_formulaTable);
  mc_formulae = 0;

}

/**Function****************************************************************
  Synopsis    [Function Mc_AboutPkg]
  Description [Mc_AboutPkg reports release of Model checking package.]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

void
Mc_AboutPkg()
{
  printf("EST ");
  printf(EDITION);
  printf(", version ");
  printf(VERSION);
  printf(", ");
  printf("Model checking package");
  printf("\n");
}


/**Function****************************************************************
  Synopsis    [Function Mc_AddNewFormula]
  Description []
  SideEffects [Function checks if the formula with the same name exists
               and in such cases it overwrites the existing one.]
  SeeAlso     []
  ************************************************************************/

int
Mc_AddNewFormula(Est_String name, Est_String formula)
{
  Mc_Formula *f;
  int i;
  int formnum;
  Est_Boolean OK;

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

  if (mc_formulae == 0) {
    mc_formulaTable = (Mc_Formula *) malloc (sizeof(Mc_Formula));
    f = mc_formulaTable;
    mc_formulae = 1;
    formnum = 0;
  } else {

    if (OK) {
      formnum = i;
      f = &mc_formulaTable[i];
      free(f->name);
      free(f->formula);
      printf(" (formula overwritten) ");
    } else {
      formnum = mc_formulae;
      mc_formulae++;
      mc_formulaTable = (Mc_Formula *) realloc (
                         mc_formulaTable, mc_formulae * sizeof(Mc_Formula));
      f = &mc_formulaTable[mc_formulae-1];
    }
  }

  f->name = strdup(name);
  f->formula = strdup(formula);

  return formnum;
}


/**Function****************************************************************
  Synopsis    [Function Mc_FOANextFormula]
  Description [FOA formula. If new formula is created its name will be
               composed of given prefix and a number.]
  SideEffects [Formula exists and thus it is not added iff
               it has the same string and the same prefix.]
  SeeAlso     []
  ************************************************************************/

int
Mc_FOANextFormula(Est_String f, Est_String prefix)
{
  int i,n;
  Est_String x;

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

  i = 0;
  n = 1;
  while (i<mc_formulae) {
    if (!strcmp(f,mc_formulaTable[i].formula) &&
        !strncmp(prefix,mc_formulaTable[i].name,strlen(prefix))) {
      return i;
    } else {
      if (!strncmp(prefix,mc_formulaTable[i].name,strlen(prefix))) {
        n++;
      }
      i++;
    }
  }

  x = (Est_String) malloc(127);
  sprintf(x,"%s%d",prefix,n);

  i = Mc_AddNewFormula(x,f);

  free(x);
  return i;
}

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

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

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

  return -1;
}


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

void
Mc_WriteKnownFormulae()
{
  int i;
  Est_String pom;

  printf("The list of formulae:\n");
  for(i=0;i<mc_formulae;i++) {
    pom = (Est_String) malloc(255);
    sprintf(pom,"%4d. %s == %s\n",i+1,mc_formulaTable[i].name,mc_formulaTable[i].formula);
    printf("%s",pom);
    free(pom);
  }
  printf("\n");
}

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

void
Mc_WriteFormula(Est_String ime, char type)
{
  int f;

  f = Mc_FindFormula(ime);
  if (f != -1) {

    if (type > 0) {
      printf("%s == ",mc_formulaTable[f].name);
    }
    printf("%s\n",mc_formulaTable[f].formula);

  } else {
    printf("Formula does not exist!\n");
  }
  printf("\n");
}

/**Function****************************************************************
  Synopsis    [Function Mc_CheckEEU.]
  Description [Strict EEU. Formula EE[{chi} phi U {chi'} phi']]
  SideEffects [EEU is not valid in deadlocked state.]
  SeeAlso     []
  ************************************************************************/

Bdd_Edge
Mc_CheckEEU(Bdd_Edge D, Bdd_Edge a1, Bdd_Edge s1, Bdd_Edge a2,
            Bdd_Edge s2)
{
  Bdd_Edge sup1,sup2,last,Z;

  /* IF THERE ARE NO TRANSITIONS IN THE PROCESS !! */
  if (Bdd_isEqv(D,bdd_termFalse)) return bdd_termFalse; /* CAREFULLY !!! */

  sup2 = Bdd_RelOp(a2,s2,"#AND R2S",TRUE);
  sup2 = Bdd_RelOp(D,sup2,"#AND Ex xA xS",TRUE);   /* Z = ... -a2-> s2 */
  Bdd_Fortify(sup2);

  /* IF a1 == FALSE */
  if (Bdd_isEqv(a1,bdd_termFalse)) return sup2;

  sup1 = Bdd_ITE(s1,a1,bdd_termFalse);
  Bdd_Fortify(sup1);

  Z = sup2;
  last = bdd_termTrue;
  while (!Bdd_isEqv(Z,last)) {

    Bdd_IncCounter();
    Bdd_Fresh(Z);

    last = Z;
    Z = Bdd_RelOp(Z,sup1,"#AND R2S",TRUE);
    Z = Bdd_RelOp(Z,D,"#AND Ex xA xS",TRUE);        /* ... -a1-> (s1*Z) */
    Z = Bdd_ITE(Z,bdd_termTrue,sup2);                   /* Z = Z + sup2 */
  }

  /*
  printf("EEU calculation finished.\n");
  */

  Bdd_Fortify(Z);
  return Z;                               /* where EEU is valid */
}

/**Function****************************************************************
  Synopsis    [Function Mc_InevitableCheckEEU.]
  Description [Strict EEU. Formula EE[{chi} phi U {chi'} phi']]
  SideEffects [*f are already known to be inevitable valid
               *fx are already known to be inevitable invalid]
  SeeAlso     []
  ************************************************************************/

void
Mc_InevitableCheckEEU(int cn, Bdd_Edge *f, Bdd_Edge *fx,
                      Bdd_Edge a1, Bdd_Edge s1, Bdd_Edge s1x,
                      Bdd_Edge a2, Bdd_Edge s2, Bdd_Edge s2x)
{
  Bdd_Edge tmp1,tmp2;
  Bdd_Edge sup1,sup2,last,Z;
  Bdd_Edge w,wtau;
  Bdd_Edge sall,sd,s1new,s2new;
  Est_String tmp;
  int gi,gj;

  tmp = (Est_String) malloc(255); /* THIS IS RELEASED AT THE END */

  /* USE di AND dij - calculate all current and next states */
  /**/
  sup1 = bdd_termFalse;
  sup2 = bdd_termFalse;
  for(gi=0; gi<pa_compositionTable[cn].numProcesses; gi++) {
    if (!Bdd_isEqv(pa_compositionTable[cn].di[gi],bdd_termFalse)) {
      tmp2 = Bdd_RelOpSimple(pa_compositionTable[cn].di[gi],"Ex xA xS",TRUE);
      sup1 = Bdd_ITE(sup1,bdd_termTrue,tmp2);
      sprintf(tmp,"Ex xA xR<%s> S2R*",pa_processTable[pa_compositionTable[cn].tableP[gi]].name);
      tmp2 = Bdd_RelOpComplex(pa_compositionTable[cn].di[gi],tmp,TRUE);
      sup2 = Bdd_ITE(sup2,bdd_termTrue,tmp2);
    }
    for(gj=0; gj<pa_compositionTable[cn].numProcesses; gj++)
    if (!Bdd_isNull(pa_compositionTable[cn].dij[
                    gi * pa_compositionTable[cn].numProcesses + gj]) &&
        !Bdd_isEqv(pa_compositionTable[cn].dij[
                    gi * pa_compositionTable[cn].numProcesses + gj],bdd_termFalse)
    ) {
      tmp2 = Bdd_RelOpSimple(pa_compositionTable[cn].dij[
             gi * pa_compositionTable[cn].numProcesses + gj],"Ex xA xS",TRUE);
      sup1 = Bdd_ITE(sup1,bdd_termTrue,tmp2);
      sprintf(tmp,"Ex xA xR<%s><%s> S2R*",
              pa_processTable[pa_compositionTable[cn].tableP[gi]].name,
              pa_processTable[pa_compositionTable[cn].tableP[gj]].name);
      tmp2 = Bdd_RelOpComplex(pa_compositionTable[cn].dij[
             gi * pa_compositionTable[cn].numProcesses + gj],tmp,TRUE);
      sup2 = Bdd_ITE(sup2,bdd_termTrue,tmp2);
    }
  }

  /* USE D  - calculate all current and next states */
  /*
  Bdd_Edge D;
  D = pa_compositionTable[cn].transitionBDD;
  sup1 = Bdd_RelOpSimple(D,"Ex xA xS",TRUE);
  sup2 = Bdd_RelOpSimple(D,"Ex xA xR S2R",TRUE);
  */

  sall = Bdd_ITE(sup1,bdd_termTrue,sup2); /* sall = the set of all states */
  sd = Bdd_ITE(sup1,bdd_termFalse,sup2);  /* the set of all deadlocked states */
  /* Bdd_Fortify(sall); */
  /* Bdd_Fortify(sd); */

  /* IF THERE ARE NO TRANSITIONS IN THE PROCESS - CAREFULLY! */
  if (Bdd_isEqv(sall,bdd_termFalse)) {
    *f = bdd_termFalse;
    *fx = bdd_termFalse;
    free(tmp);
    return;
  }

  /*
  printf("EEU inevitable valid fixed point calculation started.\n");
  */

  s1new = s1;
  s2new = s2;
  sup1 = Bdd_ITE(s1new,a1,bdd_termFalse);
  /* Bdd_Fortify(sup1); */

  sup2 = Bdd_RelOp(a2,s2new,"#AND R2S",TRUE);

  /* USE di AND dij - calculate ... -a2-> s2 */
  /**/
  tmp1 = bdd_termFalse;
  w = sup2;
  wtau = Bdd_ITE(w,McTau,bdd_termFalse);
  for(gi=0; gi<pa_compositionTable[cn].numProcesses; gi++) {
    sprintf(tmp,"S2R^<%s>",pa_processTable[pa_compositionTable[cn].tableP[gi]].name);
    tmp2 = Bdd_RelOpComplex(w,tmp,TRUE);
    tmp2 = Bdd_RelOp(tmp2,pa_compositionTable[cn].di[gi],"#AND Ex xA xS",TRUE);
    tmp1 = Bdd_ITE(tmp1,bdd_termTrue,tmp2);
    if (!Bdd_isEqv(wtau,bdd_termFalse)) {
      for(gj=0; gj<pa_compositionTable[cn].numProcesses; gj++)
      if (!Bdd_isNull(pa_compositionTable[cn].dij[
                      gi * pa_compositionTable[cn].numProcesses + gj])) {
        sprintf(tmp,"S2R^<%s><%s>",
                pa_processTable[pa_compositionTable[cn].tableP[gi]].name,
                pa_processTable[pa_compositionTable[cn].tableP[gj]].name);
        tmp2 = Bdd_RelOpComplex(wtau,tmp,TRUE);
        tmp2 = Bdd_RelOp(tmp2,pa_compositionTable[cn].dij[
               gi * pa_compositionTable[cn].numProcesses + gj],"#AND Ex xA xS",TRUE);
        tmp1 = Bdd_ITE(tmp1,bdd_termTrue,tmp2);
      }
    }
  }
  sup2 = tmp1;
  /**/

  /* USE D - calculate ... -a2-> s2 */
  /*
  sup2 = Bdd_RelOp(sup2,D,"#AND Ex xA xS",TRUE);
  */

  /* Bdd_Fortify(sup2); */

  /* DO NOT USE FIXPOINT FROM PREVIOUS CALCULATION */
  /*
  Z = sup2;
  */

  /* USE FIXPOINT FROM PREVIOUS CALCULATION */
  /**/
  Z = Bdd_ITE(*f,bdd_termTrue,sup2);
  /**/

  last = bdd_termTrue;
  while (!Bdd_isEqv(Z,last)) {

    /* CAREFULLY! */
    /*
    Bdd_IncCounter();

    for(gi=0; gi<pa_compositionTable[cn].numProcesses; gi++) {
      Bdd_Fresh(pa_compositionTable[cn].di[gi]);
      for(gj=0; gj<pa_compositionTable[cn].numProcesses; gj++)
      if (!Bdd_isNull(pa_compositionTable[cn].dij[
                      gi * pa_compositionTable[cn].numProcesses + gj])) {
        Bdd_Fresh(pa_compositionTable[cn].dij[
                  gi * pa_compositionTable[cn].numProcesses + gj]);
      }
    }

    Bdd_Fresh(pa_compositionTable[cn].stateBDD);
    Bdd_Fresh(pa_compositionTable[cn].snew);
    Bdd_Fresh(sall);
    Bdd_Fresh(sup1);
    Bdd_Fresh(sup2);
    Bdd_Fresh(Z);
    */

    /*
    printf("\nDEBUGING Z:\n");
    Pa_DecodeProcessStates(&pa_processTable[Pa_FindProcess("P")],Z,TRUE);
    printf("\n");
    */

    last = Z;
    Z = Bdd_RelOp(Z,sup1,"#AND R2S",TRUE);

    /* USE di AND dij - calculate ... -a1-> (s1*Z) */
    /**/
    tmp1 = bdd_termFalse;
    w = Z;
    wtau = Bdd_ITE(w,McTau,bdd_termFalse);
    for(gi=0; gi<pa_compositionTable[cn].numProcesses; gi++) {
      sprintf(tmp,"S2R^<%s>",pa_processTable[pa_compositionTable[cn].tableP[gi]].name);
      tmp2 = Bdd_RelOpComplex(w,tmp,TRUE);
      tmp2 = Bdd_RelOp(tmp2,pa_compositionTable[cn].di[gi],"#AND Ex xA xS",TRUE);
      tmp1 = Bdd_ITE(tmp1,bdd_termTrue,tmp2);
      if (!Bdd_isEqv(wtau,bdd_termFalse)) {
        for(gj=0; gj<pa_compositionTable[cn].numProcesses; gj++)
        if (!Bdd_isNull(pa_compositionTable[cn].dij[
                        gi * pa_compositionTable[cn].numProcesses + gj])) {
          sprintf(tmp,"S2R^<%s><%s>",
		  pa_processTable[pa_compositionTable[cn].tableP[gi]].name,
                  pa_processTable[pa_compositionTable[cn].tableP[gj]].name);
          tmp2 = Bdd_RelOpComplex(wtau,tmp,TRUE);
          tmp2 = Bdd_RelOp(tmp2,pa_compositionTable[cn].dij[
                 gi * pa_compositionTable[cn].numProcesses + gj],"#AND Ex xA xS",TRUE);
          tmp1 = Bdd_ITE(tmp1,bdd_termTrue,tmp2);
        }
      }
    }
    Z = tmp1;
    /**/

    /* USE D - calculate ... -a1-> (s1*Z)*/
    /*
    Z = Bdd_RelOp(Z,D,"#AND Ex xA xS",TRUE);
    */

    /*
    if (!Bdd_isEqv(Z,tmp1)) {
      printf("EEU (VALID) NISTA ENAKA!\n");
    }
    */

    /*
    if (!Bdd_isEqv(Z,tmp1)) {
      printf("DEBUGING TR:\n");
      Pa_DecodeCompTR(&pa_compositionTable[Pa_FindComposition("BRP")],D,TRUE);
      printf("DEBUGING Z:\n");
      num = Pa_DecodeCompStates(&pa_compositionTable[Pa_FindComposition("BRP")],Z,TRUE);
      printf("Z: %d STATES\n",num);
      printf("DEBUGING tmp1:\n");
      num = Pa_DecodeCompStates(&pa_compositionTable[Pa_FindComposition("BRP")],tmp1,TRUE);
      printf("tmp1: %d STATES\n",num);
      exit(1);
    }
    */

    Z = Bdd_ITE(Z,bdd_termTrue,sup2);                    /* Z = Z + sup2 */

    /*
    int num;
    num = Pa_DecodeCompStates(&pa_compositionTable[Pa_FindComposition("BRP")],Z,FALSE);
    printf("DEBUGING Z: %d STATES\n",num);
    */

  } /* while */

  Bdd_Fortify(Z);
  *f = Z;                              /* where EEU is inevitable valid */

  /* DO NOT CALCULATE INEVITABLE INVALID STATES FOR EEU */
  /*
  free(tmp);
  return;
  */

  /*
  printf("EEU inevitable invalid fixed point calculation started.\n");
  */

  s1new = Bdd_ITE(s1x,bdd_termFalse,sall);
  s2new = Bdd_ITE(s2x,bdd_termFalse,sall);
  sup1 = Bdd_ITE(s1new,a1,bdd_termFalse);
  /* Bdd_Fortify(sup1); */

  sup2 = Bdd_RelOp(a2,s2new,"#AND R2S",TRUE);

  /* USE di AND dij - calculate ... -a2-> s2x */
  /**/
  tmp1 = bdd_termFalse;
  w = sup2;
  wtau = Bdd_ITE(w,McTau,bdd_termFalse);
  for(gi=0; gi<pa_compositionTable[cn].numProcesses; gi++) {
    sprintf(tmp,"S2R^<%s>",pa_processTable[pa_compositionTable[cn].tableP[gi]].name);
    tmp2 = Bdd_RelOpComplex(w,tmp,TRUE);
    tmp2 = Bdd_RelOp(tmp2,pa_compositionTable[cn].di[gi],"#AND Ex xA xS",TRUE);
    tmp1 = Bdd_ITE(tmp1,bdd_termTrue,tmp2);
    if (!Bdd_isEqv(wtau,bdd_termFalse)) {
      for(gj=0; gj<pa_compositionTable[cn].numProcesses; gj++)
      if (!Bdd_isNull(pa_compositionTable[cn].dij[
                      gi * pa_compositionTable[cn].numProcesses + gj])) {
        sprintf(tmp,"S2R^<%s><%s>",
                pa_processTable[pa_compositionTable[cn].tableP[gi]].name,
                pa_processTable[pa_compositionTable[cn].tableP[gj]].name);
        tmp2 = Bdd_RelOpComplex(wtau,tmp,TRUE);
        tmp2 = Bdd_RelOp(tmp2,pa_compositionTable[cn].dij[
               gi * pa_compositionTable[cn].numProcesses + gj],"#AND Ex xA xS",TRUE);
        tmp1 = Bdd_ITE(tmp1,bdd_termTrue,tmp2);
      }
    }
  }
  sup2 = tmp1;
  /**/

  /* USE D - calculate ... -a2-> s2x */
  /*
  sup2 = Bdd_RelOp(sup2,D,"#AND Ex xA xS",TRUE);
  */

  sup2 = Bdd_ITE(sup2,bdd_termTrue,sd);          /* add deadlocked states */
  /* Bdd_Fortify(sup2); */

  /* DO NOT USE FIXPOINT FROM PREVIOUS CALCULATION */
  /*
  Z = sup2;
  */

  /* USE FIXPOINT FROM PREVIOUS CALCULATION */
  /**/
  Z = Bdd_ITE(*f,bdd_termTrue,sup2);
  /**/

  last = bdd_termTrue;
  while (!Bdd_isEqv(Z,last)) {

    /* CAREFULLY! */
    /*
    Bdd_IncCounter();

    for(gi=0; gi<pa_compositionTable[cn].numProcesses; gi++) {
      Bdd_Fresh(pa_compositionTable[cn].di[gi]);
      for(gj=0; gj<pa_compositionTable[cn].numProcesses; gj++)
      if (!Bdd_isNull(pa_compositionTable[cn].dij[
                      gi * pa_compositionTable[cn].numProcesses + gj])) {
        Bdd_Fresh(pa_compositionTable[cn].dij[
                  gi * pa_compositionTable[cn].numProcesses + gj]);
      }
    }

    Bdd_Fresh(pa_compositionTable[cn].stateBDD);
    Bdd_Fresh(pa_compositionTable[cn].snew);
    Bdd_Fresh(sall);
    Bdd_Fresh(sup1);
    Bdd_Fresh(sup2);
    Bdd_Fresh(Z);
    */

    /*
    printf("DEBUGING Z:");
    Pa_DecodeProcessStates(&pa_processTable[Pa_FindProcess("P")],Z,TRUE);
    printf("\n");
    */

    last = Z;
    Z = Bdd_RelOp(Z,sup1,"#AND R2S",TRUE);

    /* USE di AND dij - calculate ... -a1-> (s1x*Z) */
    /**/
    tmp1 = bdd_termFalse;
    wtau = Bdd_ITE(Z,McTau,bdd_termFalse);
    for(gi=0; gi<pa_compositionTable[cn].numProcesses; gi++) {
      sprintf(tmp,"S2R^<%s>",pa_processTable[pa_compositionTable[cn].tableP[gi]].name);
      tmp2 = Bdd_RelOpComplex(Z,tmp,TRUE);
      tmp2 = Bdd_RelOp(tmp2,pa_compositionTable[cn].di[gi],"#AND Ex xA xS",TRUE);
      tmp1 = Bdd_ITE(tmp1,bdd_termTrue,tmp2);
      if (!Bdd_isEqv(wtau,bdd_termFalse)) {
        for(gj=0; gj<pa_compositionTable[cn].numProcesses; gj++)
        if (!Bdd_isNull(pa_compositionTable[cn].dij[
                        gi * pa_compositionTable[cn].numProcesses + gj])) {
          sprintf(tmp,"S2R^<%s><%s>",
		  pa_processTable[pa_compositionTable[cn].tableP[gi]].name,
                  pa_processTable[pa_compositionTable[cn].tableP[gj]].name);
          tmp2 = Bdd_RelOpComplex(wtau,tmp,TRUE);
          tmp2 = Bdd_RelOp(tmp2,pa_compositionTable[cn].dij[
                 gi * pa_compositionTable[cn].numProcesses + gj],"#AND Ex xA xS",TRUE);
          tmp1 = Bdd_ITE(tmp1,bdd_termTrue,tmp2);
        }
      }
    }
    Z = tmp1;
    /**/

    /* USE D - calculate ... -a1-> (s1x*Z) */
    /*
    Z = Bdd_RelOp(Z,D,"#AND Ex xA xS",TRUE);
    */

    /*
    if (!Bdd_isEqv(Z,tmp1)) {
      printf("EEU (INVALID) NISTA ENAKA!\n");
    }
    */

    Z = Bdd_ITE(Z,bdd_termTrue,sup2);                    /* Z = Z + sup2 */

    /*
    int num;
    num = Pa_DecodeCompStates(&pa_compositionTable[Pa_FindComposition("BRP")],Z,FALSE);
    printf("DEBUGING Z: %d STATES\n",num);
    */

  } /* while */

  Z = Bdd_ITE(Z,bdd_termFalse,sall);
  Bdd_Fortify(Z);
  *fx = Z;                            /* where EEU is inevitable invalid */

  /*
  printf("Inevitable EEU calculation finished.\n");
  */

  free(tmp);
  return;
}

/**Function****************************************************************
  Synopsis    [Function Mc_CheckAAU.]
  Description [Strict AAU. Formula AA[{chi} phi U {chi'} phi']]
  SideEffects [AAU is not valid in deadlocked state.]
  SeeAlso     []
  ************************************************************************/

Bdd_Edge
Mc_CheckAAU(Bdd_Edge D, Bdd_Edge a1, Bdd_Edge s1, Bdd_Edge a2,
            Bdd_Edge s2, Bdd_Edge *AAWfun, Bdd_Edge *AAFfun)
{
  Bdd_Edge r;

  /* IF THERE ARE NO TRANSITIONS IN THE PROCESS !! */ /* CAREFULLY !!! */
  if (Bdd_isEqv(D,bdd_termFalse)) {
    *AAWfun = bdd_termTrue;
    *AAFfun = bdd_termFalse;
    return bdd_termFalse;
  }

  *AAWfun = Mc_CheckAAW(D,a1,s1,a2,s2);          /* where AAW is valid */
  *AAFfun = Mc_CheckAAF(D,a2,s2);                /* where AAF is valid */

  r =  Bdd_ITE(*AAWfun,*AAFfun,bdd_termFalse);

  Bdd_Fortify(r);
  return r;                                      /* where AAU is valid */
}

/**Function****************************************************************
  Synopsis    [Function Mc_InevitableCheckAAU.]
  Description [Strict AAU. Formula AA[{chi} phi U {chi'} phi']]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

void
Mc_InevitableCheckAAU(int cn, Bdd_Edge *f, Bdd_Edge *fx,
                      Bdd_Edge *f1, Bdd_Edge *f1x,
                      Bdd_Edge *f2, Bdd_Edge *f2x,
                      Bdd_Edge a1, Bdd_Edge s1, Bdd_Edge s1x,
                      Bdd_Edge a2, Bdd_Edge s2, Bdd_Edge s2x)
{

  Mc_InevitableCheckAAW(cn,f1,f1x,a1,s1,s1x,a2,s2,s2x);
  Mc_InevitableCheckAAF(cn,f2,f2x,a2,s2,s2x);

  /* INEVITABLE VALID */
  *f =  Bdd_ITE(*f1,*f2,bdd_termFalse);
  Bdd_Fortify(*f);

  /* INEVITABLE INVALID */
  *fx =  Bdd_ITE(*f1x,bdd_termTrue,*f2x);
  Bdd_Fortify(*fx);

}


/**Function****************************************************************
  Synopsis    [Function Mc_CheckEEW.]
  Description [Strict EEW. Formula EE[{chi} phi W {chi'} phi']]
  SideEffects [EEW is valid in deadlocked state.]
  SeeAlso     []
  ************************************************************************/

Bdd_Edge
Mc_CheckEEW(Bdd_Edge D, Bdd_Edge a1, Bdd_Edge s1, Bdd_Edge a2,
            Bdd_Edge s2, Bdd_Edge *EEUfun, Bdd_Edge *EEGfun)
{
  Bdd_Edge r;

  /* IF THERE ARE NO TRANSITIONS IN THE PROCESS !! */ /* CAREFULLY !!! */
  if (Bdd_isEqv(D,bdd_termFalse)) {
    *EEUfun = bdd_termFalse;
    *EEGfun = bdd_termTrue;
    return bdd_termTrue;
  }

  *EEUfun = Mc_CheckEEU(D,a1,s1,a2,s2);          /* where EEU is valid */
  *EEGfun = Mc_CheckEEG(D,a1,s1);                /* where EEG is valid */

  r =  Bdd_ITE(*EEUfun,bdd_termTrue,*EEGfun);

  Bdd_Fortify(r);
  return r;                                      /* where EEW is valid */
}

/**Function****************************************************************
  Synopsis    [Function Mc_InevitableCheckEEW.]
  Description [Strict EEW. Formula EE[{chi} phi W {chi'} phi']]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

void
Mc_InevitableCheckEEW(int cn, Bdd_Edge *f, Bdd_Edge *fx,
                      Bdd_Edge *f1, Bdd_Edge *f1x,
                      Bdd_Edge *f2, Bdd_Edge *f2x,
                      Bdd_Edge a1, Bdd_Edge s1, Bdd_Edge s1x,
                      Bdd_Edge a2, Bdd_Edge s2, Bdd_Edge s2x)
{

  Mc_InevitableCheckEEU(cn,f1,f1x,a1,s1,s1x,a2,s2,s2x);
  Mc_InevitableCheckEEG(cn,f2,f2x,a1,s1,s1x);

  /* INEVITABLE VALID */
  *f = Bdd_ITE(*f1,bdd_termTrue,*f2);
  Bdd_Fortify(*f);

  /* INEVITABLE INVALID */
  *fx = Bdd_ITE(*f1x,*f2x,bdd_termFalse);
  Bdd_Fortify(*fx);

}

/**Function****************************************************************
  Synopsis    [Function Mc_CheckAAW.]
  Description [Strict AAW. Formula AA[{chi} phi W {chi'} phi']]
  SideEffects [AAW is valid in deadlocked state.]
  SeeAlso     []
  ************************************************************************/

Bdd_Edge
Mc_CheckAAW(Bdd_Edge D, Bdd_Edge a1, Bdd_Edge s1, Bdd_Edge a2,
            Bdd_Edge s2)
{
  Bdd_Edge sall,D1not,D2not_ras,D2not_sar;
  Bdd_Edge sup,sup1,sup2,last,Z;

  /* IF THERE ARE NO TRANSITIONS IN THE PROCESS !! */
  if (Bdd_isEqv(D,bdd_termFalse)) return bdd_termTrue; /* CAREFULLY !!! */

  sup1 = Bdd_RelOpSimple(D,"Ex xA xS",TRUE);
  sup2 = Bdd_RelOpSimple(D,"Ex xA xR S2R",TRUE);
  sall = Bdd_ITE(sup1,bdd_termTrue,sup2);
  Bdd_Fortify(sall);                 /* sall = the set of all states */

  sup = Bdd_ITE(a1,s1,bdd_termFalse);
  sup = Bdd_RelOpSimple(sup,"R2S",TRUE);
  D1not = Bdd_ITE(sup,bdd_termFalse,D);
  Bdd_Fortify(D1not);                    /* D1not = delta_not(a1,s1) */

  sup = Bdd_ITE(a2,s2,bdd_termFalse);
  sup = Bdd_RelOpSimple(sup,"R2S",TRUE);
  D2not_ras = Bdd_ITE(sup,bdd_termFalse,D);
  D2not_sar = Bdd_RelOpSimple(D2not_ras,"R2S S2R",TRUE);
  Bdd_Fortify(D2not_ras);                /* D2not = delta_not(a2,s2) */
  Bdd_Fortify(D2not_sar);                /* D2not = delta_not(a2,s2) */

  Z = Bdd_RelOp(D1not,D2not_ras,"#AND Ex xA xS",TRUE);
  Bdd_Fortify(Z);

  last = bdd_termTrue;
  while (!Bdd_isEqv(Z,last)) {
    Bdd_IncCounter();
    Bdd_Fresh(Z);

    last = Z;
    sup = Bdd_RelOp(Z,D2not_sar,"#AND Ex xA xR S2R",TRUE);
    Z = Bdd_ITE(sup,bdd_termTrue,Z);
  }

  /*
  printf("AAW calculation finished.\n");
  */

  /* Z is now set of states where AAW is not valid */
  /* Z must be set of states where AAW is valid */

  Z = Bdd_ITE(Z,bdd_termFalse,sall);
  Bdd_Fortify(Z);

  return Z;                                        /* where AAW is valid */
}

/**Function****************************************************************
  Synopsis    [Function Mc_InevitableCheckAAW.]
  Description [Strict AAW. Formula AA[{chi} phi W {chi'} phi']]
  SideEffects [*f are already known to be inevitable valid
               *fx are already known to be inevitable invalid]
  SeeAlso     []
  ************************************************************************/

void
Mc_InevitableCheckAAW(int cn, Bdd_Edge *f, Bdd_Edge *fx,
                      Bdd_Edge a1, Bdd_Edge s1, Bdd_Edge s1x,
                      Bdd_Edge a2, Bdd_Edge s2, Bdd_Edge s2x)
{
  Bdd_Edge tmp1,tmp2;
  Bdd_Edge sup1,sup2,last,Z;
  Bdd_Edge sall,sd,s1new,s2new;
  Est_String tmp;
  int gi,gj,gk;

  tmp = (Est_String) malloc(255); /* THIS IS RELEASED AT THE END */

  /* USE di AND dij - calculate all current and next states */
  /**/
  sup1 = bdd_termFalse;
  sup2 = bdd_termFalse;
  for(gi=0; gi<pa_compositionTable[cn].numProcesses; gi++) {
    if (!Bdd_isEqv(pa_compositionTable[cn].di[gi],bdd_termFalse)) {
      tmp2 = Bdd_RelOpSimple(pa_compositionTable[cn].di[gi],"Ex xA xS",TRUE);
      sup1 = Bdd_ITE(sup1,bdd_termTrue,tmp2);
      sprintf(tmp,"Ex xA xR<%s> S2R*",pa_processTable[pa_compositionTable[cn].tableP[gi]].name);
      tmp2 = Bdd_RelOpComplex(pa_compositionTable[cn].di[gi],tmp,TRUE);
      sup2 = Bdd_ITE(sup2,bdd_termTrue,tmp2);
    }
    for(gj=0; gj<pa_compositionTable[cn].numProcesses; gj++)
    if (!Bdd_isNull(pa_compositionTable[cn].dij[
                    gi * pa_compositionTable[cn].numProcesses + gj]) &&
        !Bdd_isEqv(pa_compositionTable[cn].dij[
                    gi * pa_compositionTable[cn].numProcesses + gj],bdd_termFalse)
    ) {
      tmp2 = Bdd_RelOpSimple(pa_compositionTable[cn].dij[
             gi * pa_compositionTable[cn].numProcesses + gj],"Ex xA xS",TRUE);
      sup1 = Bdd_ITE(sup1,bdd_termTrue,tmp2);
      sprintf(tmp,"Ex xA xR<%s><%s> S2R*",
              pa_processTable[pa_compositionTable[cn].tableP[gi]].name,
              pa_processTable[pa_compositionTable[cn].tableP[gj]].name);
      tmp2 = Bdd_RelOpComplex(pa_compositionTable[cn].dij[
             gi * pa_compositionTable[cn].numProcesses + gj],tmp,TRUE);
      sup2 = Bdd_ITE(sup2,bdd_termTrue,tmp2);
    }
  }
  /**/

  /* USE D  - calculate all current and next states */
  /*
  Bdd_Edge D;
  D = pa_compositionTable[cn].transitionBDD;
  sup1 = Bdd_RelOpSimple(D,"Ex xA xS",TRUE);
  sup2 = Bdd_RelOpSimple(D,"Ex xA xR S2R",TRUE);
  */

  sall = Bdd_ITE(sup1,bdd_termTrue,sup2); /* sall = the set of all states */
  sd = Bdd_ITE(sup1,bdd_termFalse,sup2);  /* the set of all deadlocked states */
  /* Bdd_Fortify(sall); */
  /* Bdd_Fortify(sd); */

  /* IF THERE ARE NO TRANSITIONS IN THE PROCESS - CAREFULLY! */
  if (Bdd_isEqv(sall,bdd_termFalse)) {
    *f = bdd_termFalse;
    *fx = bdd_termFalse;
    free(tmp);
    return;
  }

  /*
  printf("AAW inevitable invalid fixed point calculation started.\n");
  */

  s1new = Bdd_ITE(s1x,bdd_termFalse,sall);
  s2new = Bdd_ITE(s2x,bdd_termFalse,sall);
  sup1 = Bdd_ITE(s1new,a1,bdd_termFalse);
  sup2 = Bdd_ITE(s2new,a2,bdd_termFalse);
  /* Bdd_Fortify(sup1); */
  /* Bdd_Fortify(sup2); */

  /* snotD = transitions not in D */
  /*
  Bdd_Edge snotD;
  snotD = Bdd_ITE(Bdd_NOT(D),sall,bdd_termFalse);
  */
  /* Bdd_Fortify(snotD); */

  /* DO NOT USE FIXPOINT FROM PREVIOUS CALCULATION */
  /*
  Z = bdd_termTrue;
  */

  /* USE FIXPOINT FROM PREVIOUS CALCULATION */
  /**/
  Z = Bdd_ITE(*fx,bdd_termFalse,sall);
  /**/

  last = bdd_termFalse;
  while (!Bdd_isEqv(Z,last)) {

    /* CAREFULLY! */
    /*
    Bdd_IncCounter();

    for(gi=0; gi<pa_compositionTable[cn].numProcesses; gi++) {
      Bdd_Fresh(pa_compositionTable[cn].di[gi]);
      for(gj=0; gj<pa_compositionTable[cn].numProcesses; gj++)
      if (!Bdd_isNull(pa_compositionTable[cn].dij[
                      gi * pa_compositionTable[cn].numProcesses + gj])) {
        Bdd_Fresh(pa_compositionTable[cn].dij[
                  gi * pa_compositionTable[cn].numProcesses + gj]);
      }
    }

    Bdd_Fresh(pa_compositionTable[cn].stateBDD);
    Bdd_Fresh(pa_compositionTable[cn].snew);
    Bdd_Fresh(sall);
    Bdd_Fresh(snotD);
    Bdd_Fresh(sup1);
    Bdd_Fresh(sup2);
    Bdd_Fresh(Z);
    */

    last = Z;
    Z = Bdd_ITE(Z,sup1,bdd_termFalse);                      /* Z = Z * sup1 */
    Z = Bdd_RelOp(Z,sup2,"#OR R2S",TRUE);                   /* Z = Z + sup2 */

    /* USE di AND dij - calculate AxA AxS (D => ...) */
    /* I DO NOT KNOW HOW TO AVOID stabs HERE */
    /**/
    tmp1 = sall;
    for(gi=0; gi<pa_compositionTable[cn].numProcesses; gi++) {
      tmp2 = pa_compositionTable[cn].di[gi];
      if (!Bdd_isEqv(tmp2,bdd_termFalse))
      for(gj=0; gj<pa_compositionTable[cn].numProcesses; gj++)
      if (gj != gi) {
        tmp2 = Bdd_ITE(pa_processTable[pa_compositionTable[cn].tableP[gj]].stab,
                       tmp2,bdd_termFalse);
      }
      tmp2 = Bdd_RelOp(tmp2,Z,"#IMPL Ax xA xS",TRUE);
      tmp1 = Bdd_ITE(tmp1,tmp2,bdd_termFalse);
      for(gj=0; gj<pa_compositionTable[cn].numProcesses; gj++)
      if (!Bdd_isNull(pa_compositionTable[cn].dij[
                      gi * pa_compositionTable[cn].numProcesses + gj])) {
        tmp2 = pa_compositionTable[cn].dij[
	       gi * pa_compositionTable[cn].numProcesses + gj];
        if (!Bdd_isEqv(tmp2,bdd_termFalse))
        for(gk=0; gk<pa_compositionTable[cn].numProcesses; gk++)
        if ((gk != gi) && (gk != gj)) {
        tmp2 = Bdd_ITE(pa_processTable[pa_compositionTable[cn].tableP[gk]].stab,
                       tmp2,bdd_termFalse);
        }
        tmp2 = Bdd_ITE(tmp2,McTau,bdd_termFalse);
        tmp2 = Bdd_RelOp(tmp2,Z,"#IMPL Ax xA xS",TRUE);
        tmp1 = Bdd_ITE(tmp1,tmp2,bdd_termFalse);
      }
    }
    Z = tmp1;
    /**/

    /* USE D - calculate AxA AxS (D => ...) */
    /*
    Z = Bdd_RelOp(Z,snotD,"#OR Ax xA xS",TRUE);
    */

    /*
    if (!Bdd_isEqv(Z,tmp1)) {
      printf("AAW (INVALID) NISTA ENAKA!\n");
    }
    */

    /*
    int num2;
    num2 = Pa_DecodeCompStates(&pa_compositionTable[Pa_FindComposition("BRP")],Z,FALSE);
    printf("DEBUGING Z: %d STATES\n",num2);
    */

  } /* while */

  Z = Bdd_ITE(Z,bdd_termFalse,sall);
  Bdd_Fortify(Z);
  *fx = Z;                                   /* where AAW is inevitable invalid */

  /* DO NOT CALCULATE INEVITABLE VALID STATES FOR AAW */
  /*
  free(tmp);
  return;
  */

  s1new = s1;
  s2new = s2;
  sup1 = Bdd_ITE(s1new,a1,bdd_termFalse);
  sup2 = Bdd_ITE(s2new,a2,bdd_termFalse);
  /* Bdd_Fortify(sup1); */
  /* Bdd_Fortify(sup2); */

  /* DO NOT USE FIXPOINT FROM PREVIOUS CALCULATION */
  /*
  Z = bdd_termTrue;
  */

  /* USE FIXPOINT FROM PREVIOUS CALCULATION */
  /**/
  Z = Bdd_ITE(*fx,bdd_termFalse,sall);
  /**/

  /*
  printf("AAW inevitable valid fixed point calculation started.\n");
  */

  last = bdd_termFalse;
  while (!Bdd_isEqv(Z,last)) {

    /* CAREFULLY! */
    /*
    Bdd_IncCounter();

    for(gi=0; gi<pa_compositionTable[cn].numProcesses; gi++) {
      Bdd_Fresh(pa_compositionTable[cn].di[gi]);
      for(gj=0; gj<pa_compositionTable[cn].numProcesses; gj++)
      if (!Bdd_isNull(pa_compositionTable[cn].dij[
                      gi * pa_compositionTable[cn].numProcesses + gj])) {
        Bdd_Fresh(pa_compositionTable[cn].dij[
                  gi * pa_compositionTable[cn].numProcesses + gj]);
      }
    }

    Bdd_Fresh(pa_compositionTable[cn].stateBDD);
    Bdd_Fresh(pa_compositionTable[cn].snew);
    Bdd_Fresh(sall);
    Bdd_Fresh(sd);
    Bdd_Fresh(snotD);
    Bdd_Fresh(sup1);
    Bdd_Fresh(sup2);
    Bdd_Fresh(Z);
    */

    /*
    printf("DEBUGING Z:");
    Pa_DecodeProcessStates(&pa_processTable[Pa_FindProcess("P")],Z,TRUE);
    printf("\n");
    */

    last = Z;
    Z = Bdd_ITE(Z,sup1,bdd_termFalse);                      /* Z = Z * sup1 */
    Z = Bdd_RelOp(Z,sup2,"#OR R2S",TRUE);                   /* Z = Z + sup2 */

    /* USE di AND dij - calculate AxA AxS (D => ...) */
    /* I DO NOT KNOW HOW TO AVOID stabs HERE */
    /**/
    tmp1 = sall;
    for(gi=0; gi<pa_compositionTable[cn].numProcesses; gi++) {
      tmp2 = pa_compositionTable[cn].di[gi];
      if (!Bdd_isEqv(tmp2,bdd_termFalse))
      for(gj=0; gj<pa_compositionTable[cn].numProcesses; gj++)
      if (gj != gi) {
        tmp2 = Bdd_ITE(pa_processTable[pa_compositionTable[cn].tableP[gj]].stab,
                       tmp2,bdd_termFalse);
      }
      tmp2 = Bdd_RelOp(tmp2,Z,"#IMPL Ax xA xS",TRUE);
      tmp1 = Bdd_ITE(tmp1,tmp2,bdd_termFalse);
      for(gj=0; gj<pa_compositionTable[cn].numProcesses; gj++)
      if (!Bdd_isNull(pa_compositionTable[cn].dij[
                      gi * pa_compositionTable[cn].numProcesses + gj])) {
        tmp2 = pa_compositionTable[cn].dij[
	       gi * pa_compositionTable[cn].numProcesses + gj];
        if (!Bdd_isEqv(tmp2,bdd_termFalse))
        for(gk=0; gk<pa_compositionTable[cn].numProcesses; gk++)
        if ((gk != gi) && (gk != gj)) {
        tmp2 = Bdd_ITE(pa_processTable[pa_compositionTable[cn].tableP[gk]].stab,
                       tmp2,bdd_termFalse);
        }
        tmp2 = Bdd_ITE(tmp2,McTau,bdd_termFalse);
        tmp2 = Bdd_RelOp(tmp2,Z,"#IMPL Ax xA xS",TRUE);
        tmp1 = Bdd_ITE(tmp1,tmp2,bdd_termFalse);
      }
    }
    Z = tmp1;
    /**/

    /* USE D - calculate AxA AxS (D => ...) */
    /*
    Z = Bdd_RelOp(Z,snotD,"#OR Ax xA xS",TRUE);
    */

    /*
    if (!Bdd_isEqv(Z,tmp1)) {
      printf("AAW (VALID) NISTA ENAKA!\n");
    }
    */

    Z = Bdd_ITE(sd,bdd_termFalse,Z);            /* remove deadlocked states */

    /*
    int num;
    num = Pa_DecodeCompStates(&pa_compositionTable[Pa_FindComposition("BRP")],Z,FALSE);
    printf("DEBUGING Z: %d STATES\n",num);
    */

  } /* while */


  Bdd_Fortify(Z);
  *f = Z;                              /* where AAW is inevitable valid */

  /*
  printf("Inevitable AAW calculation finished.\n");
  */

  free(tmp);
  return;
}

/**Function****************************************************************
  Synopsis    [Function Mc_CheckEEX.]
  Description [EEX {chi} phi]
  SideEffects [EEX is not valid in deadlocked state.]
  SeeAlso     []
  ************************************************************************/

Bdd_Edge
Mc_CheckEEX(Bdd_Edge D, Bdd_Edge a, Bdd_Edge s)
{
  Bdd_Edge r;

  /* IF THERE ARE NO TRANSITIONS IN THE PROCESS !! */
  if (Bdd_isEqv(D,bdd_termFalse)) return bdd_termFalse;   /* CAREFULLY !!! */

  r =  Mc_CheckEEU(D,bdd_termFalse,bdd_termFalse,a,s);

  return r;
}

/**Function****************************************************************
  Synopsis    [Function Mc_InevitableCheckEEX.]
  Description [EEX {chi} phi]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

void
Mc_InevitableCheckEEX(int cn, Bdd_Edge *f,  Bdd_Edge *fx,
                      Bdd_Edge a, Bdd_Edge s, Bdd_Edge sx)
{

  Mc_InevitableCheckEEU(cn,f,fx,bdd_termFalse,bdd_termFalse,bdd_termTrue,a,s,sx);

}

/**Function****************************************************************
  Synopsis    [Function Mc_CheckAAX.]
  Description [AAX {chi} phi]
  SideEffects [AAX is valid in deadlocked state.]
  SeeAlso     []
  ************************************************************************/

Bdd_Edge
Mc_CheckAAX(Bdd_Edge D, Bdd_Edge a, Bdd_Edge s)
{
  Bdd_Edge r;

  /* IF THERE ARE NO TRANSITIONS IN THE PROCESS !! */
  if (Bdd_isEqv(D,bdd_termFalse)) return bdd_termTrue;   /* CAREFULLY !!! */

  r =  Mc_CheckAAW(D,bdd_termFalse,bdd_termFalse,a,s);

  return r;
}

/**Function****************************************************************
  Synopsis    [Function Mc_InevitableCheckAAX.]
  Description [AAX {chi} phi]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

void
Mc_InevitableCheckAAX(int cn, Bdd_Edge *f,  Bdd_Edge *fx,
                      Bdd_Edge a, Bdd_Edge s, Bdd_Edge sx)
{

  Mc_InevitableCheckAAW(cn,f,fx,bdd_termFalse,bdd_termFalse,bdd_termTrue,a,s,sx);

}

/**Function****************************************************************
  Synopsis    [Function Mc_CheckEEF.]
  Description [Strict EEF. Formula EEF {chi} phi]
  SideEffects [EEF is not valid in deadlocked state.]
  SeeAlso     []
  ************************************************************************/

Bdd_Edge
Mc_CheckEEF(Bdd_Edge D, Bdd_Edge a, Bdd_Edge s)
{
  Bdd_Edge r;

  /* IF THERE ARE NO TRANSITIONS IN THE PROCESS !! */
  if (Bdd_isEqv(D,bdd_termFalse)) return bdd_termFalse;   /* CAREFULLY !!! */

  r = Mc_CheckEEU(D,bdd_termTrue,bdd_termTrue,a,s);

  return r;
}

/**Function****************************************************************
  Synopsis    [Function Mc_InevitableCheckEEF.]
  Description [Strict EEF. Formula EEF {chi} phi]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

void
Mc_InevitableCheckEEF(int cn, Bdd_Edge *f,  Bdd_Edge *fx,
                      Bdd_Edge a, Bdd_Edge s, Bdd_Edge sx)
{

  Mc_InevitableCheckEEU(cn,f,fx,bdd_termTrue,bdd_termTrue,bdd_termFalse,a,s,sx);

}

/**Function****************************************************************
  Synopsis    [Function Mc_CheckEEG.]
  Description [Strict EEG. Formula EEG {chi} phi]
  SideEffects [EEG is valid in deadlocked state.]
  SeeAlso     []
  ************************************************************************/

Bdd_Edge
Mc_CheckEEG(Bdd_Edge D, Bdd_Edge a, Bdd_Edge s)
{
  Bdd_Edge sup1,sup2,sd,last,Z;

  /* IF THERE ARE NO TRANSITIONS IN THE PROCESS !! */
  if (Bdd_isEqv(D,bdd_termFalse)) return bdd_termTrue;    /* CAREFULLY !!! */

  sup1 = Bdd_RelOpSimple(D,"Ex xA xS",TRUE);
  sup2 = Bdd_RelOpSimple(D,"Ex xA xR S2R",TRUE);
  sd = Bdd_ITE(sup1,bdd_termFalse,sup2);
  Bdd_Fortify(sd);                 /* the set of all deadlocked states */

  sup1 = Bdd_ITE(a,s,bdd_termFalse);
  Bdd_Fortify(sup1);

  Z = bdd_termTrue;
  last = bdd_termFalse;
  while (!Bdd_isEqv(Z,last)) {
    Bdd_IncCounter();
    Bdd_Fresh(Z);

    last = Z;
    Z = Bdd_RelOp(Z,sup1,"#AND R2S",TRUE);
    Z = Bdd_RelOp(Z,D,"#AND Ex xA xS",TRUE);          /* ... -a1-> (s*Z) */
    Z = Bdd_ITE(Z,bdd_termTrue,sd);             /* add deadlocked states */
  }

  /*
  printf("EEG calculation finished.\n");
  */

  Bdd_Fortify(Z);
  return Z;                                        /* where EEG is valid */
}

/**Function****************************************************************
  Synopsis    [Function Mc_InevitableCheckEEG.]
  Description [Strict EEG. Formula EEG {chi} phi]
  SideEffects [*f are already known to be inevitable valid
               *fx are already known to be inevitable invalid]
  SeeAlso     []
  ************************************************************************/

void
Mc_InevitableCheckEEG(int cn, Bdd_Edge *f, Bdd_Edge *fx,
                      Bdd_Edge a, Bdd_Edge s, Bdd_Edge sx)
{
  Bdd_Edge tmp1,tmp2;
  Bdd_Edge sup1,sup2,sd,last,Z;
  Bdd_Edge w,wtau;
  Bdd_Edge sall,snew;
  Est_String tmp;
  int gi,gj;

  tmp = (Est_String) malloc(255); /* THIS IS RELEASED AT THE END */

  /* USE di AND dij - calculate all current and next states */
  /**/
  sup1 = bdd_termFalse;
  sup2 = bdd_termFalse;
  for(gi=0; gi<pa_compositionTable[cn].numProcesses; gi++) {
    if (!Bdd_isEqv(pa_compositionTable[cn].di[gi],bdd_termFalse)) {
      tmp2 = Bdd_RelOpSimple(pa_compositionTable[cn].di[gi],"Ex xA xS",TRUE);
      sup1 = Bdd_ITE(sup1,bdd_termTrue,tmp2);
      sprintf(tmp,"Ex xA xR<%s> S2R*",pa_processTable[pa_compositionTable[cn].tableP[gi]].name);
      tmp2 = Bdd_RelOpComplex(pa_compositionTable[cn].di[gi],tmp,TRUE);
      sup2 = Bdd_ITE(sup2,bdd_termTrue,tmp2);
    }
    for(gj=0; gj<pa_compositionTable[cn].numProcesses; gj++)
    if (!Bdd_isNull(pa_compositionTable[cn].dij[
                    gi * pa_compositionTable[cn].numProcesses + gj]) &&
        !Bdd_isEqv(pa_compositionTable[cn].dij[
                    gi * pa_compositionTable[cn].numProcesses + gj],bdd_termFalse)
    ) {
      tmp2 = Bdd_RelOpSimple(pa_compositionTable[cn].dij[
             gi * pa_compositionTable[cn].numProcesses + gj],"Ex xA xS",TRUE);
      sup1 = Bdd_ITE(sup1,bdd_termTrue,tmp2);
      sprintf(tmp,"Ex xA xR<%s><%s> S2R*",
              pa_processTable[pa_compositionTable[cn].tableP[gi]].name,
              pa_processTable[pa_compositionTable[cn].tableP[gj]].name);
      tmp2 = Bdd_RelOpComplex(pa_compositionTable[cn].dij[
             gi * pa_compositionTable[cn].numProcesses + gj],tmp,TRUE);
      sup2 = Bdd_ITE(sup2,bdd_termTrue,tmp2);
    }
  }

  /* USE D  - calculate all current and next states */
  /*
  Bdd_Edge D;
  D = pa_compositionTable[cn].transitionBDD;
  sup1 = Bdd_RelOpSimple(D,"Ex xA xS",TRUE);
  sup2 = Bdd_RelOpSimple(D,"Ex xA xR S2R",TRUE);
  */

  sall = Bdd_ITE(sup1,bdd_termTrue,sup2); /* sall = the set of all states */
  sd = Bdd_ITE(sup1,bdd_termFalse,sup2);  /* the set of all deadlocked states */
  /* Bdd_Fortify(sall); */
  /* Bdd_Fortify(sd); */

  /* IF THERE ARE NO TRANSITIONS IN THE PROCESS - CAREFULLY! */
  if (Bdd_isEqv(sall,bdd_termFalse)) {
    *f = bdd_termFalse;
    *fx = bdd_termFalse;
    free(tmp);
    return;
  }

  /*
  printf("EEG inevitable invalid fixed point calculation started.\n");
  */

  snew = Bdd_ITE(sx,bdd_termFalse,sall);
  sup1 = Bdd_ITE(a,snew,bdd_termFalse);
  /* Bdd_Fortify(sup1); */

  /* DO NOT USE FIXPOINT FROM PREVIOUS CALCULATION */
  /*
  Z = bdd_termTrue;
  */

  /* USE FIXPOINT FROM PREVIOUS CALCULATION */
  /**/
  Z = Bdd_ITE(*fx,bdd_termFalse,sall);
  /**/

  last = bdd_termFalse;
  while (!Bdd_isEqv(Z,last)) {

    /* CAREFULLY! */
    /*
    Bdd_IncCounter();

    for(gi=0; gi<pa_compositionTable[cn].numProcesses; gi++) {
      Bdd_Fresh(pa_compositionTable[cn].di[gi]);
      for(gj=0; gj<pa_compositionTable[cn].numProcesses; gj++)
      if (!Bdd_isNull(pa_compositionTable[cn].dij[
                      gi * pa_compositionTable[cn].numProcesses + gj])) {
        Bdd_Fresh(pa_compositionTable[cn].dij[
                  gi * pa_compositionTable[cn].numProcesses + gj]);
      }
    }

    Bdd_Fresh(pa_compositionTable[cn].stateBDD);
    Bdd_Fresh(pa_compositionTable[cn].snew);
    Bdd_Fresh(sall);
    Bdd_Fresh(sd);
    Bdd_Fresh(sup1);
    Bdd_Fresh(Z);
    */

    /*
    printf("DEBUGING Z:");
    Pa_DecodeProcessStates(&pa_processTable[Pa_FindProcess("P")],Z,TRUE);
    printf("\n");
    */

    last = Z;
    Z = Bdd_RelOp(Z,sup1,"#AND R2S",TRUE);

    /* USE di AND dij - calculate ... -a1-> (sx*Z) */
    /**/
    tmp1 = bdd_termFalse;
    w = Z;
    wtau = Bdd_ITE(w,McTau,bdd_termFalse);
    for(gi=0; gi<pa_compositionTable[cn].numProcesses; gi++) {
      sprintf(tmp,"S2R^<%s>",pa_processTable[pa_compositionTable[cn].tableP[gi]].name);
      tmp2 = Bdd_RelOpComplex(w,tmp,TRUE);
      tmp2 = Bdd_RelOp(tmp2,pa_compositionTable[cn].di[gi],"#AND Ex xA xS",TRUE);
      tmp1 = Bdd_ITE(tmp1,bdd_termTrue,tmp2);
      if (!Bdd_isEqv(wtau,bdd_termFalse)) {
        for(gj=0; gj<pa_compositionTable[cn].numProcesses; gj++)
        if (!Bdd_isNull(pa_compositionTable[cn].dij[
                        gi * pa_compositionTable[cn].numProcesses + gj])) {
          sprintf(tmp,"S2R^<%s><%s>",
		  pa_processTable[pa_compositionTable[cn].tableP[gi]].name,
                  pa_processTable[pa_compositionTable[cn].tableP[gj]].name);
          tmp2 = Bdd_RelOpComplex(wtau,tmp,TRUE);
          tmp2 = Bdd_RelOp(tmp2,pa_compositionTable[cn].dij[
                 gi * pa_compositionTable[cn].numProcesses + gj],"#AND Ex xA xS",TRUE);
          tmp1 = Bdd_ITE(tmp1,bdd_termTrue,tmp2);
        }
      }
    }
    Z = tmp1;
    /**/

    /* USE D - calculate ... -a1-> (sx*Z) */
    /*
    Z = Bdd_RelOp(Z,D,"#AND Ex xA xS",TRUE);
    */

    /*
    if (!Bdd_isEqv(Z,tmp1)) {
      printf("EEG (INVALID) NISTA ENAKA!\n");
    }
    */

    Z = Bdd_ITE(Z,bdd_termTrue,sd);              /* add deadlocked states */

    /*
    int num;
    num = Pa_DecodeCompStates(&pa_compositionTable[Pa_FindComposition("BRP")],Z,FALSE);
    printf("DEBUGING Z: %d STATES\n",num);
    */

  } /* while */

  Z = Bdd_ITE(Z,bdd_termFalse,sall);
  Bdd_Fortify(Z);
  *fx = Z;                             /* where EEG is inevitable invalid */

  /* DO NOT CALCULATE INEVITABLE VALID STATES FOR EEG */
  /*
  free(tmp);
  return;
  */

  snew = s;
  sup1 = Bdd_ITE(a,snew,bdd_termFalse);
  /* Bdd_Fortify(sup1); */

  /* DO NOT USE FIXPOINT FROM PREVIOUS CALCULATION */
  /*
  Z = bdd_termTrue;
  */

  /* USE FIXPOINT FROM PREVIOUS CALCULATION */
  /**/
  Z = Bdd_ITE(*fx,bdd_termFalse,sall);
  /**/

  /*
  printf("EEG inevitable valid fixed point calculation started.\n");
  */

  last = bdd_termFalse;
  while (!Bdd_isEqv(Z,last)) {

    /* CAREFULLY! */
    /*
    Bdd_IncCounter();

    for(gi=0; gi<pa_compositionTable[cn].numProcesses; gi++) {
      Bdd_Fresh(pa_compositionTable[cn].di[gi]);
      for(gj=0; gj<pa_compositionTable[cn].numProcesses; gj++)
      if (!Bdd_isNull(pa_compositionTable[cn].dij[
                      gi * pa_compositionTable[cn].numProcesses + gj])) {
        Bdd_Fresh(pa_compositionTable[cn].dij[
                  gi * pa_compositionTable[cn].numProcesses + gj]);
      }
    }

    Bdd_Fresh(pa_compositionTable[cn].stateBDD);
    Bdd_Fresh(pa_compositionTable[cn].snew);
    Bdd_Fresh(sall);
    Bdd_Fresh(sd);
    Bdd_Fresh(sup1);
    Bdd_Fresh(Z);
    */

    /*
    printf("DEBUGING Z:");
    Pa_DecodeProcessStates(&pa_processTable[Pa_FindProcess("P")],Z,TRUE);
    printf("\n");
    */

    last = Z;
    Z = Bdd_RelOp(Z,sup1,"#AND R2S",TRUE);

    /* USE di AND dij  - calculate ... -a1-> (s*Z) */
    /**/
    tmp1 = bdd_termFalse;
    w = Z;
    wtau = Bdd_ITE(w,McTau,bdd_termFalse);
    for(gi=0; gi<pa_compositionTable[cn].numProcesses; gi++) {
      sprintf(tmp,"S2R^<%s>",pa_processTable[pa_compositionTable[cn].tableP[gi]].name);
      tmp2 = Bdd_RelOpComplex(w,tmp,TRUE);
      tmp2 = Bdd_RelOp(tmp2,pa_compositionTable[cn].di[gi],"#AND Ex xA xS",TRUE);
      tmp1 = Bdd_ITE(tmp1,bdd_termTrue,tmp2);
      if (!Bdd_isEqv(wtau,bdd_termFalse)) {
        for(gj=0; gj<pa_compositionTable[cn].numProcesses; gj++)
        if (!Bdd_isNull(pa_compositionTable[cn].dij[
                        gi * pa_compositionTable[cn].numProcesses + gj])) {
          sprintf(tmp,"S2R^<%s><%s>",
		  pa_processTable[pa_compositionTable[cn].tableP[gi]].name,
                  pa_processTable[pa_compositionTable[cn].tableP[gj]].name);
          tmp2 = Bdd_RelOpComplex(wtau,tmp,TRUE);
          tmp2 = Bdd_RelOp(tmp2,pa_compositionTable[cn].dij[
                 gi * pa_compositionTable[cn].numProcesses + gj],"#AND Ex xA xS",TRUE);
          tmp1 = Bdd_ITE(tmp1,bdd_termTrue,tmp2);
        }
      }
    }
    Z = tmp1;
    /**/

    /* USE D - calculate ... -a1-> (s*Z) */
    /*
    Z = Bdd_RelOp(Z,D,"#AND Ex xA xS",TRUE);
    */

    /*
    if (!Bdd_isEqv(Z,tmp1)) {
      printf("EEG (VALID) NISTA ENAKA!\n");
    }
    */

    /*
    int num;
    num = Pa_DecodeCompStates(&pa_compositionTable[Pa_FindComposition("BRP")],Z,FALSE);
    printf("DEBUGING Z: %d STATES\n",num);
    */

  } /* while */

  Bdd_Fortify(Z);
  *f = Z;                                /* where EEG is inevitable valid */

  /*
  printf("Inevitable EEG calculation finished.\n");
  */

  free(tmp);
  return;
}

/**Function****************************************************************
  Synopsis    [Function Mc_CheckAAF.]
  Description [Strict AAF. Formula AAF {chi} phi]
  SideEffects [AAF is not valid in deadlocked state.]
  SeeAlso     []
  ************************************************************************/

Bdd_Edge
Mc_CheckAAF(Bdd_Edge D, Bdd_Edge a, Bdd_Edge s)
{
  Bdd_Edge sall,Dnot_ras,Dnot_sar;
  Bdd_Edge sup,sup1,sup2,sd_r,sd_s,last,Z;

  /* IF THERE ARE NO TRANSITIONS IN THE PROCESS !! */
  if (Bdd_isEqv(D,bdd_termFalse)) return bdd_termFalse;   /* CAREFULLY !!! */

  sup1 = Bdd_RelOpSimple(D,"Ex xA xS",TRUE);
  sup2 = Bdd_RelOpSimple(D,"Ex xA xR S2R",TRUE);
  sall = Bdd_ITE(sup1,bdd_termTrue,sup2);
  Bdd_Fortify(sall);                   /* sall = the set of all states */

  sd_r = Bdd_ITE(sup1,bdd_termFalse,sup2);
  sd_s = Bdd_RelOpSimple(sd_r,"R2S",TRUE);
  Bdd_Fortify(sd_r);               /* the set of all deadlocked states */
  Bdd_Fortify(sd_s);               /* the set of all deadlocked states */

  sup = Bdd_ITE(a,s,bdd_termFalse);
  sup = Bdd_RelOpSimple(sup,"R2S",TRUE);
  Dnot_ras = Bdd_ITE(sup,bdd_termFalse,D);
  Dnot_sar = Bdd_RelOpSimple(Dnot_ras,"R2S S2R",TRUE);
  Bdd_Fortify(Dnot_ras);                      /* Dnot = delta_not(a,s) */
  Bdd_Fortify(Dnot_sar);                      /* Dnot = delta_not(a,s) */

  Z = bdd_termTrue;
  last = bdd_termFalse;
  while (!Bdd_isEqv(Z,last)) {
    Bdd_IncCounter();
    Bdd_Fresh(Z);

    last = Z;

    /* THERE ARE TWO STEPS IN ONE ITERATION */
    /* THIS IS BETER, YOU DO NOT NEED TO CALL R2S */

    sup = Bdd_RelOp(Z,Dnot_sar,"#AND Ex xA xR",TRUE);
    Z = Bdd_ITE(sup,bdd_termTrue,sd_s);         /* add deadlocked states */

    sup = Bdd_RelOp(Z,Dnot_ras,"#AND Ex xA xS",TRUE);
    Z = Bdd_ITE(sup,bdd_termTrue,sd_r);         /* add deadlocked states */
  }

  /*
  printf("AAF calculation finished.\n");
  */

  /* Z is now set of states where AF is not valid */
  /* Z must be set of states where AF is valid */

  Z = Bdd_ITE(Z,bdd_termFalse,sall);
  Bdd_Fortify(Z);

  return Z;                                        /* where AAF is valid */
}

/**Function****************************************************************
  Synopsis    [Function Mc_InevitableCheckAAF.]
  Description [Strict AAF. Formula AAF {chi} phi]
  SideEffects [*f are already known to be inevitable valid
               *fx are already known to be inevitable invalid]
  SeeAlso     []
  ************************************************************************/

void
Mc_InevitableCheckAAF(int cn, Bdd_Edge *f, Bdd_Edge *fx,
                      Bdd_Edge a, Bdd_Edge s, Bdd_Edge sx)
{
  Bdd_Edge tmp1,tmp2;
  Bdd_Edge sup1,sup2,last,Z;
  Bdd_Edge sall,sd,snew;
  Est_String tmp;
  int gi,gj,gk;

  tmp = (Est_String) malloc(255); /* THIS IS RELEASED AT THE END */

  /* USE di AND dij - calculate all current and next states */
  /**/
  sup1 = bdd_termFalse;
  sup2 = bdd_termFalse;
  for(gi=0; gi<pa_compositionTable[cn].numProcesses; gi++) {
    if (!Bdd_isEqv(pa_compositionTable[cn].di[gi],bdd_termFalse)) {
      tmp2 = Bdd_RelOpSimple(pa_compositionTable[cn].di[gi],"Ex xA xS",TRUE);
      sup1 = Bdd_ITE(sup1,bdd_termTrue,tmp2);
      sprintf(tmp,"Ex xA xR<%s> S2R*",pa_processTable[pa_compositionTable[cn].tableP[gi]].name);
      tmp2 = Bdd_RelOpComplex(pa_compositionTable[cn].di[gi],tmp,TRUE);
      sup2 = Bdd_ITE(sup2,bdd_termTrue,tmp2);
    }
    for(gj=0; gj<pa_compositionTable[cn].numProcesses; gj++)
    if (!Bdd_isNull(pa_compositionTable[cn].dij[
                    gi * pa_compositionTable[cn].numProcesses + gj]) &&
        !Bdd_isEqv(pa_compositionTable[cn].dij[
                    gi * pa_compositionTable[cn].numProcesses + gj],bdd_termFalse)
    ) {
      tmp2 = Bdd_RelOpSimple(pa_compositionTable[cn].dij[
             gi * pa_compositionTable[cn].numProcesses + gj],"Ex xA xS",TRUE);
      sup1 = Bdd_ITE(sup1,bdd_termTrue,tmp2);
      sprintf(tmp,"Ex xA xR<%s><%s> S2R*",
              pa_processTable[pa_compositionTable[cn].tableP[gi]].name,
              pa_processTable[pa_compositionTable[cn].tableP[gj]].name);
      tmp2 = Bdd_RelOpComplex(pa_compositionTable[cn].dij[
             gi * pa_compositionTable[cn].numProcesses + gj],tmp,TRUE);
      sup2 = Bdd_ITE(sup2,bdd_termTrue,tmp2);
    }
  }
  /**/

  /* USE D  - calculate all current and next states */
  /*
  Bdd_Edge D;
  D = pa_compositionTable[cn].transitionBDD;
  sup1 = Bdd_RelOpSimple(D,"Ex xA xS",TRUE);
  sup2 = Bdd_RelOpSimple(D,"Ex xA xR S2R",TRUE);
  */

  sall = Bdd_ITE(sup1,bdd_termTrue,sup2);         /* sall = the set of all states */
  sd = Bdd_ITE(sup1,bdd_termFalse,sup2);     /* the set of all deadlocked states */
  /* Bdd_Fortify(sall); */
  /* Bdd_Fortify(sd); */

  /* IF THERE ARE NO TRANSITIONS IN THE PROCESS - CAREFULLY! */
  if (Bdd_isEqv(sall,bdd_termFalse)) {
    *f = bdd_termFalse;
    *fx = bdd_termFalse;
    free(tmp);
    return;
  }

  /*
  printf("AAF inevitable valid fixed point calculation started.\n");
  */

  snew = s;
  sup1 = Bdd_ITE(a,snew,bdd_termFalse);
  /* Bdd_Fortify(sup1); */

  /* snotD = transitions not in D */
  /*
  Bdd_Edge snotD;
  snotD = Bdd_ITE(Bdd_NOT(D),sall,bdd_termFalse);
  */
  /* Bdd_Fortify(snotD); */

  /* DO NOT USE FIXPOINT FROM PREVIOUS CALCULATION */
  /*
  Z = bdd_termFalse;
  */

  /* USE FIXPOINT FROM PREVIOUS CALCULATION */
  /**/
  Z = *f;
  /**/

  last = bdd_termTrue;
  while (!Bdd_isEqv(Z,last)) {

    /* CAREFULLY! */
    /*
    Bdd_IncCounter();

    for(gi=0; gi<pa_compositionTable[cn].numProcesses; gi++) {
      Bdd_Fresh(pa_compositionTable[cn].di[gi]);
      for(gj=0; gj<pa_compositionTable[cn].numProcesses; gj++)
      if (!Bdd_isNull(pa_compositionTable[cn].dij[
                      gi * pa_compositionTable[cn].numProcesses + gj])) {
        Bdd_Fresh(pa_compositionTable[cn].dij[
                  gi * pa_compositionTable[cn].numProcesses + gj]);
      }
    }

    Bdd_Fresh(pa_compositionTable[cn].stateBDD);
    Bdd_Fresh(pa_compositionTable[cn].snew);
    Bdd_Fresh(sd);
    Bdd_Fresh(sall);
    Bdd_Fresh(snotD);
    Bdd_Fresh(sup1);
    Bdd_Fresh(Z);
    */

    /*
    printf("DEBUGING Z:");
    Pa_DecodeProcessStates(&pa_processTable[Pa_FindProcess("P")],Z,TRUE);
    printf("\n");
    */

    last = Z;
    Z = Bdd_RelOp(Z,sup1,"#OR R2S",TRUE);                   /* Z = Z + sup1 */

    /* USE di AND dij - calculate AxA AxS (D => sup1) */
    /**/
    tmp1 = sall;
    for(gi=0; gi<pa_compositionTable[cn].numProcesses; gi++) {
      tmp2 = pa_compositionTable[cn].di[gi];
      if (!Bdd_isEqv(tmp2,bdd_termFalse))
      for(gj=0; gj<pa_compositionTable[cn].numProcesses; gj++)
      if (gj != gi) {
        tmp2 = Bdd_ITE(pa_processTable[pa_compositionTable[cn].tableP[gj]].stab,
                       tmp2,bdd_termFalse);
      }
      tmp2 = Bdd_RelOp(tmp2,Z,"#IMPL Ax xA xS",TRUE);
      tmp1 = Bdd_ITE(tmp1,tmp2,bdd_termFalse);
      for(gj=0; gj<pa_compositionTable[cn].numProcesses; gj++)
      if (!Bdd_isNull(pa_compositionTable[cn].dij[
                      gi * pa_compositionTable[cn].numProcesses + gj])) {
        tmp2 = pa_compositionTable[cn].dij[
	       gi * pa_compositionTable[cn].numProcesses + gj];
        if (!Bdd_isEqv(tmp2,bdd_termFalse))
        for(gk=0; gk<pa_compositionTable[cn].numProcesses; gk++)
        if ((gk != gi) && (gk != gj)) {
        tmp2 = Bdd_ITE(pa_processTable[pa_compositionTable[cn].tableP[gk]].stab,
                       tmp2,bdd_termFalse);
        }
        tmp2 = Bdd_ITE(tmp2,McTau,bdd_termFalse);
        tmp2 = Bdd_RelOp(tmp2,Z,"#IMPL Ax xA xS",TRUE);
        tmp1 = Bdd_ITE(tmp1,tmp2,bdd_termFalse);
      }
    }
    Z = tmp1;
    /**/

    /* USE D  - calculate AxA AxS (D => sup1) */
    /*
    Z = Bdd_RelOp(Z,snotD,"#OR Ax xA xS",TRUE);
    */

    /*
    if (!Bdd_isEqv(Z,tmp1)) {
      printf("AAF (VALID) NISTA ENAKA!\n");
    }
    */

    Z = Bdd_ITE(sd,bdd_termFalse,Z);            /* remove deadlocked states */

    /*
    int num;
    num = Pa_DecodeCompStates(&pa_compositionTable[Pa_FindComposition("BRP")],Z,FALSE);
    printf("DEBUGING Z: %d STATES\n",num);
    */

  } /* while */

  Bdd_Fortify(Z);
  *f = Z;                                  /* where AAF is inevitable valid */

  /* DO NOT CALCULATE INEVITABLE INVALID STATES FOR AAF */
  /*
  free(tmp);
  return;
  */

  snew = Bdd_ITE(sx,bdd_termFalse,sall);
  sup1 = Bdd_ITE(a,snew,bdd_termFalse);
  /* Bdd_Fortify(sup1); */

  /* DO NOT USE FIXPOINT FROM PREVIOUS CALCULATION */
  /*
  Z = bdd_termFalse;
  */

  /* USE FIXPOINT FROM PREVIOUS CALCULATION */
  /**/
  Z = *f ;
  /**/

  /*
  printf("AAF inevitable invalid fixed point calculation started.\n");
  */

  last = bdd_termTrue;
  while (!Bdd_isEqv(Z,last)) {

    /* CAREFULLY! */
    /*
    Bdd_IncCounter();

    for(gi=0; gi<pa_compositionTable[cn].numProcesses; gi++) {
      Bdd_Fresh(pa_compositionTable[cn].di[gi]);
      for(gj=0; gj<pa_compositionTable[cn].numProcesses; gj++)
      if (!Bdd_isNull(pa_compositionTable[cn].dij[
                      gi * pa_compositionTable[cn].numProcesses + gj])) {
        Bdd_Fresh(pa_compositionTable[cn].dij[
                  gi * pa_compositionTable[cn].numProcesses + gj]);
      }
    }

    Bdd_Fresh(pa_compositionTable[cn].stateBDD);
    Bdd_Fresh(pa_compositionTable[cn].snew);
    Bdd_Fresh(sd);
    Bdd_Fresh(sall);
    Bdd_Fresh(snotD);
    Bdd_Fresh(sup1);
    Bdd_Fresh(Z);
    */

    /*
    printf("DEBUGING Z:");
    Pa_DecodeProcessStates(&pa_processTable[Pa_FindProcess("P")],Z,TRUE);
    printf("\n");
    */

    last = Z;
    Z = Bdd_RelOp(Z,sup1,"#OR R2S",TRUE);                   /* Z = Z + sup1 */

    /* USE di AND dij - calculate AxA AxS (D => sup1) */
    /**/
    tmp1 = sall;
    for(gi=0; gi<pa_compositionTable[cn].numProcesses; gi++) {
      tmp2 = pa_compositionTable[cn].di[gi];
      if (!Bdd_isEqv(tmp2,bdd_termFalse))
      for(gj=0; gj<pa_compositionTable[cn].numProcesses; gj++)
      if (gj != gi) {
        tmp2 = Bdd_ITE(pa_processTable[pa_compositionTable[cn].tableP[gj]].stab,
                       tmp2,bdd_termFalse);
      }
      tmp2 = Bdd_RelOp(tmp2,Z,"#IMPL Ax xA xS",TRUE);
      tmp1 = Bdd_ITE(tmp1,tmp2,bdd_termFalse);
      for(gj=0; gj<pa_compositionTable[cn].numProcesses; gj++)
      if (!Bdd_isNull(pa_compositionTable[cn].dij[
                      gi * pa_compositionTable[cn].numProcesses + gj])) {
        tmp2 = pa_compositionTable[cn].dij[
	       gi * pa_compositionTable[cn].numProcesses + gj];
        if (!Bdd_isEqv(tmp2,bdd_termFalse))
        for(gk=0; gk<pa_compositionTable[cn].numProcesses; gk++)
        if ((gk != gi) && (gk != gj)) {
        tmp2 = Bdd_ITE(pa_processTable[pa_compositionTable[cn].tableP[gk]].stab,
                       tmp2,bdd_termFalse);
        }
        tmp2 = Bdd_ITE(tmp2,McTau,bdd_termFalse);
        tmp2 = Bdd_RelOp(tmp2,Z,"#IMPL Ax xA xS",TRUE);
        tmp1 = Bdd_ITE(tmp1,tmp2,bdd_termFalse);
      }
    }
    Z = tmp1;
    /**/

    /* USE D  - calculate AxA AxS (D => sup1) */
    /*
    Z = Bdd_RelOp(Z,snotD,"#OR Ax xA xS",TRUE);
    */

    /*
    if (!Bdd_isEqv(Z,tmp1)) {
      printf("AAF (INVALID) NISTA ENAKA!\n");
    }
    */

    /*
    int num;
    num = Pa_DecodeCompStates(&pa_compositionTable[Pa_FindComposition("BRP")],Z,FALSE);
    printf("DEBUGING Z: %d STATES\n",num);
    */

  } /* while */


  Z = Bdd_ITE(Z,bdd_termFalse,sall);
  Bdd_Fortify(Z);
  *fx = Z;                               /* where AAF is inevitable invalid */

  /*
  printf("Inevitable AAF calculation finished.\n");
  */

  free(tmp);
  return;
}

/**Function****************************************************************
  Synopsis    [Function Mc_CheckAAG.]
  Description [Strict AAG. Formula AAG {chi} phi]
  SideEffects [AAG is valid in deadlocked state.]
  SeeAlso     []
  ************************************************************************/

Bdd_Edge
Mc_CheckAAG(Bdd_Edge D, Bdd_Edge a, Bdd_Edge s)
{
  Bdd_Edge r;

  /* IF THERE ARE NO TRANSITIONS IN THE PROCESS !! */   /* CAREFULLY !!! */
  if (Bdd_isEqv(D,bdd_termFalse)) return bdd_termTrue;

  r = Mc_CheckAAW(D,a,s,bdd_termFalse,bdd_termFalse);

  return r;
}

/**Function****************************************************************
  Synopsis    [Function Mc_InevitableCheckAAG.]
  Description [Strict AAG. Formula AAG {chi} phi]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

void
Mc_InevitableCheckAAG(int cn, Bdd_Edge *f, Bdd_Edge *fx,
                      Bdd_Edge a, Bdd_Edge s, Bdd_Edge sx)
{

  Mc_InevitableCheckAAW(cn,f,fx,a,s,sx,bdd_termFalse,bdd_termFalse,bdd_termTrue);

}

/**Function****************************************************************
  Synopsis    [Function Mc_CheckEU.]
  Description [E[phi {chi} U {chi'} phi']]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

Bdd_Edge
Mc_CheckEU(Bdd_Edge D, Bdd_Edge s1, Bdd_Edge a1, Bdd_Edge a2,
            Bdd_Edge s2)
{
  Bdd_Edge r;

  if (Bdd_isNull(a2)) {

    a1 = Bdd_ITE(a1,bdd_termTrue,McTau);
    Bdd_Fortify(a1);
    r = Mc_CheckEEU(D,a1,s1,a1,s2);
    r = Bdd_ITE(r,s1,bdd_termFalse);
    r = Bdd_ITE(r,bdd_termTrue,s2);

  } else {

    a1 = Bdd_ITE(a1,bdd_termTrue,McTau);
    a2 = Bdd_ITE(McTau,bdd_termFalse,a2);
    Bdd_Fortify(a1);
    Bdd_Fortify(a2);
    r = Mc_CheckEEU(D,a1,s1,a2,s2);
    r = Bdd_ITE(r,s1,bdd_termFalse);

  }

  Bdd_Fortify(r);
  return r;
}

/**Function****************************************************************
  Synopsis    [Function Mc_InevitableCheckEU.]
  Description [E[phi {chi} U {chi'} phi']]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

void
Mc_InevitableCheckEU(int cn, Bdd_Edge *f, Bdd_Edge *fx,
                     Bdd_Edge *f1, Bdd_Edge *f1x,
                     Bdd_Edge s1, Bdd_Edge s1x, Bdd_Edge a1,
                     Bdd_Edge a2, Bdd_Edge s2, Bdd_Edge s2x)
{

  if (Bdd_isNull(a2)) {

    a1 = Bdd_ITE(a1,bdd_termTrue,McTau);
    Bdd_Fortify(a1);
    Mc_InevitableCheckEEU(cn,f1,f1x,a1,s1,s1x,a1,s2,s2x);

    /* INEVITABLE VALID */
    *f = Bdd_ITE(*f1,s1,bdd_termFalse);
    *f = Bdd_ITE(*f,bdd_termTrue,s2);
    Bdd_Fortify(*f);

    /* INEVITABLE INVALID */
    *fx = Bdd_ITE(*f1x,bdd_termTrue,s1x);
    *fx = Bdd_ITE(*fx,s2x,bdd_termFalse);

  } else {

    a1 = Bdd_ITE(a1,bdd_termTrue,McTau);
    a2 = Bdd_ITE(McTau,bdd_termFalse,a2);
    Bdd_Fortify(a1);
    Bdd_Fortify(a2);
    Mc_InevitableCheckEEU(cn,f1,f1x,a1,s1,s1x,a2,s2,s2x);

    /* INEVITABLE VALID */
    *f = Bdd_ITE(*f1,s1,bdd_termFalse);
    Bdd_Fortify(*f);

    /* INEVITABLE INVALID */
    *fx = Bdd_ITE(*f1x,bdd_termTrue,s1x);
    Bdd_Fortify(*fx);

  }
}

/**Function****************************************************************
  Synopsis    [Function Mc_CheckAU.]
  Description [A[phi {chi} U {chi'} phi']]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

Bdd_Edge
Mc_CheckAU(Bdd_Edge D, Bdd_Edge s1, Bdd_Edge a1, Bdd_Edge a2,
            Bdd_Edge s2)
{
  Bdd_Edge r;
  Bdd_Edge sup1,sup2;

  if (Bdd_isNull(a2)) {

    a1 = Bdd_ITE(a1,bdd_termTrue,McTau);
    Bdd_Fortify(a1);
    r =  Mc_CheckAAU(D,a1,s1,a1,s2,&sup1,&sup2);
    r = Bdd_ITE(r,s1,bdd_termFalse);
    r = Bdd_ITE(r,bdd_termTrue,s2);

  } else {

    a1 = Bdd_ITE(a1,bdd_termTrue,McTau);
    a2 = Bdd_ITE(McTau,bdd_termFalse,a2);
    Bdd_Fortify(a1);
    Bdd_Fortify(a2);
    r =  Mc_CheckAAU(D,a1,s1,a2,s2,&sup1,&sup2);
    r = Bdd_ITE(r,s1,bdd_termFalse);

  }

  Bdd_Fortify(r);
  return r;
}

/**Function****************************************************************
  Synopsis    [Function Mc_InevitableCheckAU.]
  Description [A[phi {chi} U {chi'} phi']]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

void
Mc_InevitableCheckAU(int cn, Bdd_Edge *f, Bdd_Edge *fx,
                     Bdd_Edge *f1, Bdd_Edge *f1x,
                     Bdd_Edge *f2, Bdd_Edge *f2x,
                     Bdd_Edge s1, Bdd_Edge s1x, Bdd_Edge a1,
                     Bdd_Edge a2, Bdd_Edge s2, Bdd_Edge s2x)
{
  Bdd_Edge sup,supx;

  sup = bdd_termNull;
  supx = bdd_termNull;

  if (Bdd_isNull(a2)) {

    a1 = Bdd_ITE(a1,bdd_termTrue,McTau);
    Bdd_Fortify(a1);
    Mc_InevitableCheckAAU(cn,&sup,&supx,f1,f1x,f2,f2x,a1,s1,s1x,a1,s2,s2x);

    /* INEVITABLE VALID */
    *f = Bdd_ITE(sup,s1,bdd_termFalse);
    *f = Bdd_ITE(*f,bdd_termTrue,s2);
    Bdd_Fortify(*f);

    /* INEVITABLE INVALID */
    *fx = Bdd_ITE(supx,bdd_termTrue,s1x);
    *fx = Bdd_ITE(*fx,s2x,bdd_termFalse);
    Bdd_Fortify(*fx);

  } else {

    a1 = Bdd_ITE(a1,bdd_termTrue,McTau);
    a2 = Bdd_ITE(McTau,bdd_termFalse,a2);
    Bdd_Fortify(a1);
    Bdd_Fortify(a2);
    Mc_InevitableCheckAAU(cn,&sup,&supx,f1,f1x,f2,f2x,a1,s1,s1x,a2,s2,s2x);

    /* INEVITABLE VALID */
    *f = Bdd_ITE(sup,s1,bdd_termFalse);
    Bdd_Fortify(*f);

    /* INEVITABLE INVALID */
    *fx = Bdd_ITE(supx,bdd_termTrue,s1x);
    Bdd_Fortify(*fx);

  }
}

/**Function****************************************************************
  Synopsis    [Function Mc_CheckEX.]
  Description [EX {chi} phi]
  SideEffects [EX {tau} phi is not valid in deadlocked state.]
  SeeAlso     []
  ************************************************************************/

Bdd_Edge
Mc_CheckEX(Bdd_Edge D, Bdd_Edge a, Bdd_Edge s)
{
  Bdd_Edge r;

  if (Bdd_isEqv(a,McTau)) {

    /* IF THERE ARE NO TRANSITIONS IN THE PROCESS !! */
    /* NOP */

    r =  Mc_CheckEEU(D,bdd_termFalse,bdd_termFalse,a,s);  /* Mc_CheckEEX(D,a,s) */

  } else {

    /* IF THERE ARE NO TRANSITIONS IN THE PROCESS !! */
    /* NOP */

    a = Bdd_ITE(McTau,bdd_termFalse,a);
    Bdd_Fortify(a);
    r =  Mc_CheckEEU(D,bdd_termFalse,bdd_termFalse,a,s);  /* Mc_CheckEEX(D,a,s) */

  }

  return r;
}
/**Function****************************************************************
  Synopsis    [Function Mc_InevitableCheckEX.]
  Description [EX {chi} phi]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

void
Mc_InevitableCheckEX(int cn,  Bdd_Edge *f,  Bdd_Edge *fx,
                     Bdd_Edge a, Bdd_Edge s, Bdd_Edge sx)
{

  if (Bdd_isEqv(a,McTau)) {

    /* IF THERE ARE NO TRANSITIONS IN THE PROCESS !! */
    /* NOP */

    /* Mc_CheckEEX(D,a,s) */
    Mc_InevitableCheckEEU(cn,f,fx,bdd_termFalse,bdd_termFalse,bdd_termTrue,a,s,sx);

  } else {

    /* IF THERE ARE NO TRANSITIONS IN THE PROCESS !! */
    /* NOP */

    a = Bdd_ITE(McTau,bdd_termFalse,a);
    Bdd_Fortify(a);

    /* Mc_CheckEEX(D,a,s) */
    Mc_InevitableCheckEEU(cn,f,fx,bdd_termFalse,bdd_termFalse,bdd_termTrue,a,s,sx);

  }

}

/**Function****************************************************************
  Synopsis    [Function Mc_CheckAX.]
  Description [AX {chi} phi]
  SideEffects [AX {tau} phi is not valid in deadlocked state.]
  SeeAlso     []
  ************************************************************************/

Bdd_Edge
Mc_CheckAX(Bdd_Edge D, Bdd_Edge a, Bdd_Edge s)
{
  Bdd_Edge r;
  Bdd_Edge sup1,sup2,sd;

  if (Bdd_isEqv(a,McTau)) {

    /* IF THERE ARE NO TRANSITIONS IN THE PROCESS !! */
    if (Bdd_isEqv(D,bdd_termFalse)) return bdd_termFalse;            /* CAREFULLY !!! */

    r =  Mc_CheckAAW(D,bdd_termFalse,bdd_termFalse,a,s);      /* Mc_CheckAAX(D,a,s) */

  } else {

    /* IF THERE ARE NO TRANSITIONS IN THE PROCESS !! */
    if (Bdd_isEqv(D,bdd_termFalse)) return bdd_termFalse;            /* CAREFULLY !!! */

    a = Bdd_ITE(McTau,bdd_termFalse,a);
    Bdd_Fortify(a);
    r =  Mc_CheckAAW(D,bdd_termFalse,bdd_termFalse,a,s);      /* Mc_CheckAAX(D,a,s) */

  }

  sup1 = Bdd_RelOpSimple(D,"Ex xA xS",TRUE);
  sup2 = Bdd_RelOpSimple(D,"Ex xA xR S2R",TRUE);
  sd = Bdd_ITE(sup1,bdd_termFalse,sup2);      /* the set of all deadlocked states */

  r = Bdd_ITE(sd,bdd_termFalse,r);                    /* remove deadlocked states */
  Bdd_Fortify(r);
  return r;
}

/**Function****************************************************************
  Synopsis    [Function Mc_InevitableCheckAX.]
  Description [AX {chi} phi]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

void
Mc_InevitableCheckAX(int cn, Bdd_Edge *f, Bdd_Edge *fx,
                     Bdd_Edge a, Bdd_Edge s, Bdd_Edge sx)
{

  if (Bdd_isEqv(a,McTau)) {

    /* Mc_CheckAAX(D,a,s) */
    Mc_InevitableCheckAAW(cn,f,fx,bdd_termFalse,bdd_termFalse,bdd_termTrue,a,s,sx);

  } else {

    a = Bdd_ITE(McTau,bdd_termFalse,a);
    Bdd_Fortify(a);

    /* Mc_CheckAAX(D,a,s) */
    Mc_InevitableCheckAAW(cn,f,fx,bdd_termFalse,bdd_termFalse,bdd_termTrue,a,s,sx);

  }

}

/**Function****************************************************************
  Synopsis    [Function Mc_CheckHME.]
  Description [phi <chi> phi', <chi> phi',
               phi <EPSILON> phi', <EPSILON> phi']
  SideEffects []
  SeeAlso     []
  ************************************************************************/

Bdd_Edge
Mc_CheckHME(Bdd_Edge D, Bdd_Edge s1, Bdd_Edge a, Bdd_Edge s2)
{
  Bdd_Edge r;

  if (Bdd_isNull(s1) && !Bdd_isNull(a)) {

    /* CAREFULLY!! */
    /* WE PREFER TO USE STRONG HME, WHERE APPROPRIATE */
    r = Mc_CheckEX(D,a,s2);

    /* THIS IS WEAK VARIANT FROM DeNicola, Vaandrager, 1990 */
    /*
    r = Mc_CheckEU(D,bdd_termTrue,bdd_termFalse,a,s2);
    */

  } else {

    if (Bdd_isNull(s1)) s1 = bdd_termTrue;
    r = Mc_CheckEU(D,s1,bdd_termFalse,a,s2);

  }

  return r;
}

/**Function****************************************************************
  Synopsis    [Function Mc_InevitableCheckHME.]
  Description [phi <chi> phi', <chi> phi',
               phi <EPSILON> phi', <EPSILON> phi']
  SideEffects []
  SeeAlso     []
  ************************************************************************/

void
Mc_InevitableCheckHME(int cn, Bdd_Edge *f, Bdd_Edge *fx,
                      Bdd_Edge *f1, Bdd_Edge *f1x,
                      Bdd_Edge s1, Bdd_Edge s1x, Bdd_Edge a,
                      Bdd_Edge s2, Bdd_Edge s2x)
{

  if (Bdd_isNull(s1) && !Bdd_isNull(s1x)) {
    fprintf(stderr,"Mc_InevitableCheckHME error!\n");
    return;
  }

  if (!Bdd_isNull(s1) && Bdd_isNull(s1x)) {
    fprintf(stderr,"Mc_InevitableCheckHME error!\n");
    return;
  }

  if (Bdd_isNull(s1) && Bdd_isNull(s1x) && !Bdd_isNull(a)) {

    /* CAREFULLY!! */
    /* WE PREFER TO USE STRONG HME, WHERE APPROPRIATE */
    Mc_InevitableCheckEX(cn,f,fx,a,s2,s2x);

    /* THIS IS WEAK VARIANT FROM DeNicola, Vaandrager, 1990 */
    /*
    Mc_InevitableCheckEU(cn,f,fx,f1,f1x,bdd_termTrue,bdd_termFalse,bdd_termFalse,a,s2,s2x);
    */

  } else {

    if (Bdd_isNull(s1) && Bdd_isNull(s1x)) {
      s1 = bdd_termTrue;
      s1x = bdd_termFalse;
    }
    Mc_InevitableCheckEU(cn,f,fx,f1,f1x,s1,s1x,bdd_termFalse,a,s2,s2x);

  }

}

/**Function****************************************************************
  Synopsis    [Function Mc_CheckHMA.]
  Description [[chi] phi, [EPSILON] phi]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

Bdd_Edge
Mc_CheckHMA(Bdd_Edge D, Bdd_Edge a, Bdd_Edge s)
{
  Bdd_Edge sup1,sup2,sall,snot,r;

  if (Bdd_isEqv(D,bdd_termFalse)) {
    sall = bdd_termTrue;
  } else {
    sup1 = Bdd_RelOpSimple(D,"Ex xA xS",TRUE);
    sup2 = Bdd_RelOpSimple(D,"Ex xA xR S2R",TRUE);
    sall = Bdd_ITE(sup1,bdd_termTrue,sup2);      /* the set of all states */
  }

  snot = Bdd_ITE(s,bdd_termFalse,sall);
  Bdd_Fortify(snot);                        /* the set of states not in s */

  r = Mc_CheckHME(D,bdd_termNull,a,snot);
  r = Bdd_ITE(r,bdd_termFalse,sall);
  Bdd_Fortify(r);

  return r;
}

/**Function****************************************************************
  Synopsis    [Function Mc_InevitableCheckHMA.]
  Description [[chi] phi, [EPSILON] phi]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

void
Mc_InevitableCheckHMA(int cn,  Bdd_Edge *f,  Bdd_Edge *fx,
                      Bdd_Edge *f1, Bdd_Edge *f1x,
                      Bdd_Edge a, Bdd_Edge s, Bdd_Edge sx)
{

  Mc_InevitableCheckHME(cn,fx,f,f1x,f1,bdd_termNull,bdd_termNull,a,sx,s);

}

/**Function****************************************************************
  Synopsis    [Function Mc_CheckEF.]
  Description [EF phi]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

Bdd_Edge
Mc_CheckEF(Bdd_Edge D, Bdd_Edge s)
{
  Bdd_Edge r;

  /* Mc_CheckEEF(D,bdd_termTrue,s) */
  r = Mc_CheckEEU(D,bdd_termTrue,bdd_termTrue,bdd_termTrue,s);

  r = Bdd_ITE(r,bdd_termTrue,s);

  Bdd_Fortify(r);
  return r;
}

/**Function****************************************************************
  Synopsis    [Function Mc_InevitableCheckEF.]
  Description [EF phi]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

void
Mc_InevitableCheckEF(int cn, Bdd_Edge *f, Bdd_Edge *fx,
                     Bdd_Edge *f1,  Bdd_Edge *f1x,
                     Bdd_Edge s, Bdd_Edge sx)
{

  /* Mc_CheckEEF(D,bdd_termTrue,s) */
  Mc_InevitableCheckEEU(cn,f1,f1x,bdd_termTrue,bdd_termTrue,bdd_termFalse,bdd_termTrue,s,sx);

  /* INEVITABLE VALID */
  *f = Bdd_ITE(*f1,bdd_termTrue,s);
  Bdd_Fortify(*f);

  /* INEVITABLE INVALID */
  *fx = Bdd_ITE(*f1x,sx,bdd_termFalse);
  Bdd_Fortify(*fx);

}

/**Function****************************************************************
  Synopsis    [Function Mc_CheckEG.]
  Description [EG phi]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

Bdd_Edge
Mc_CheckEG(Bdd_Edge D, Bdd_Edge s)
{
  Bdd_Edge r;

  r = Mc_CheckEEG(D,bdd_termTrue,s);
  r = Bdd_ITE(r,s,bdd_termFalse);

  Bdd_Fortify(r);
  return r;
}

/**Function****************************************************************
  Synopsis    [Function Mc_InevitableCheckEG.]
  Description [EG phi]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

void
Mc_InevitableCheckEG(int cn, Bdd_Edge *f, Bdd_Edge *fx,
                     Bdd_Edge *f1,  Bdd_Edge *f1x,
                     Bdd_Edge s, Bdd_Edge sx)
{

  Mc_InevitableCheckEEG(cn,f1,f1x,bdd_termTrue,s,sx);

  /* INEVITABLE VALID */
  *f = Bdd_ITE(*f1,s,bdd_termFalse);
  Bdd_Fortify(*f);

  /* INEVITABLE INVALID */
  *fx = Bdd_ITE(*f1x,bdd_termTrue,sx);
  Bdd_Fortify(*fx);

}

/**Function****************************************************************
  Synopsis    [Function Mc_CheckAF.]
  Description [AF phi]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

Bdd_Edge
Mc_CheckAF(Bdd_Edge D, Bdd_Edge s)
{
  Bdd_Edge r;

  r = Mc_CheckAAF(D,bdd_termTrue,s);
  r = Bdd_ITE(r,bdd_termTrue,s);

  Bdd_Fortify(r);
  return r;
}

/**Function****************************************************************
  Synopsis    [Function Mc_InevitableCheckAF.]
  Description [AF phi]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

void
Mc_InevitableCheckAF(int cn, Bdd_Edge *f, Bdd_Edge *fx,
                     Bdd_Edge *f1,  Bdd_Edge *f1x,
                     Bdd_Edge s, Bdd_Edge sx)
{

  Mc_InevitableCheckAAF(cn,f1,f1x,bdd_termTrue,s,sx);

  /* INEVITABLE VALID */
  *f = Bdd_ITE(*f1,bdd_termTrue,s);
  Bdd_Fortify(*f);

  /* INEVITABLE INVALID */
  *fx = Bdd_ITE(*f1x,sx,bdd_termFalse);
  Bdd_Fortify(*fx);

}

/**Function****************************************************************
  Synopsis    [Function Mc_CheckAG.]
  Description [AG phi]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

Bdd_Edge
Mc_CheckAG(Bdd_Edge D, Bdd_Edge s)
{
  Bdd_Edge r;

  /* Mc_CheckAAG(D,s,bdd_termTrue) */
  r = Mc_CheckAAW(D,bdd_termTrue,s,bdd_termFalse,bdd_termFalse);

  r = Bdd_ITE(r,s,bdd_termFalse);

  Bdd_Fortify(r);
  return r;
}

/**Function****************************************************************
  Synopsis    [Function Mc_InevitableCheckAG.]
  Description [AG phi]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

void
Mc_InevitableCheckAG(int cn, Bdd_Edge *f, Bdd_Edge *fx,
                     Bdd_Edge *f1,  Bdd_Edge *f1x,
                     Bdd_Edge s, Bdd_Edge sx)
{

  /* Mc_CheckAAG(D,s,bdd_termTrue) */
  Mc_InevitableCheckAAW(cn,f1,f1x,bdd_termTrue,s,sx,bdd_termFalse,bdd_termFalse,bdd_termTrue);

  /* INEVITABLE VALID */
  *f = Bdd_ITE(*f1,s,bdd_termFalse);
  Bdd_Fortify(*f);

  /* INEVITABLE INVALID */
  *fx = Bdd_ITE(*f1x,bdd_termTrue,sx);
  Bdd_Fortify(*fx);

}

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

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


McInevitableItem *
McAddEmptyInevitable(Est_String s, Est_String sx)
{
  McInevitableItem *item;

  item = (McInevitableItem *) malloc(sizeof(McInevitableItem));
  item->s = strdup(s);
  item->sx = strdup(sx);
  item->inevitableT = bdd_termNull;
  item->inevitableF = bdd_termNull;
  item->inevitableT1 = bdd_termNull;
  item->inevitableF1 = bdd_termNull;
  item->inevitableT2 = bdd_termNull;
  item->inevitableF2 = bdd_termNull;
  item->next = NULL;

  return item;
}

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

void
McAddMacro(Est_String name, Est_String body)
{
  McMacro *f;
  int i;
  Est_Boolean OK;

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

  if (mcMacros == 0) {
    mcMacroTable = (McMacro *) malloc (sizeof(McMacro));
    f = mcMacroTable;
    mcMacros = 1;
  } else {

    if (OK) {
      f = &mcMacroTable[i];
      free(f->name);
      free(f->body);
      /*
      printf(" (macro overwritten) ");
      */
    } else {
      mcMacros++;
      mcMacroTable = (McMacro *) realloc (
                         mcMacroTable, mcMacros * sizeof(McMacro));
      f = &mcMacroTable[mcMacros-1];
    }
  }

  f->name = strdup(name);
  f->body = strdup(body);
}

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

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

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

  return -1;
}

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