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

  FileName    [mcAutomata.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 mcAutomata.c contains functions for w/c automata.]
  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                                                 */
/*-----------------------------------------------------------------------*/

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

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

static void build(int WCA, int t, int act, int type, int tprime,
                  int explain);

static int newstate(int WCA, Est_String sname);

static void addR(McTypeR *R, int t, int s);

static int findR(McTypeR R, int s);

static void deleteR(McTypeR *R);

static void printstate(Est_String name);

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

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

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

/**Function****************************************************************
  Synopsis    [Function WCAgenerator]
  Description [item = formula]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

int
WCAgenerator(Est_String LTSname, Est_String WCAname,
             McDiagnosticItem *item, int explain)
{
  int i;
  Est_String tmp;
  int LTS,WCA;
  int s,t;
  Est_Boolean WCAtype,OK;

  LTS = Pa_FindProcess(LTSname);

  /* create an empty automaton WCA */
  if (!WCAname) {
    i = 0;
    tmp = NULL;
    do {
      i++;
      if (tmp) free (tmp);
      tmp = (Est_String) malloc(127);
      sprintf(tmp,"WC%d%s",i,LTSname);
    } while (Pa_FindProcess(tmp) != -1);
    WCA = Pa_AddNewProcess(tmp);
    free(tmp);
  } else {
    WCA = Pa_AddNewProcess(WCAname);
  }

  if (item->r == FALSE) {
    WCAtype = FALSE;
    if (explain) {
      printf("@@");
      for (i=0; i<explain;i++) printf(" ");
      printf("Creating counterexample automaton\n");
    }
  } else {
    WCAtype = TRUE;
    if (explain) {
      printf("@@");
      for (i=0; i<explain;i++) printf(" ");
      printf("Creating witness automaton\n");
    }
  }

  if (explain) {
    printf("@@");
    for (i=0; i<explain;i++) printf(" ");
    if (WCAtype) {
      printf("WCAgenerator: created empty witness automaton\n");
    } else {
      printf("WCAgenerator: created empty counterexample automaton\n");
    }
  }

  /* initialization of WCA */
  s = pa_processTable[LTS].initial;
  pa_processTable[WCA].sort = pa_processTable[LTS].sort;

  /* create a new state tprime in WCA */
  t = newstate(WCA,pa_processTable[LTS].tableS[pa_processTable[LTS].initial].name);
  pa_processTable[WCA].initial = t;

  if (explain) {
    printf("@@");
    for (i=0; i<explain;i++) printf(" ");
    printf("WCAgenerator: created initial state ");
    printstate(pa_processTable[WCA].tableS[t].name);
    printf("\n");
  }

  OK = WCAgen(LTS,WCA,item,s,t,WCAtype,explain);

  if (!OK) {
    Pa_DeleteProcess(WCA);
    WCA = -1; /* automaton cannot be constructed */
  } else if (pa_processTable[WCA].numTransitions == 0) {
    Pa_DeleteProcess(WCA);
    WCA = -2; /* automaton is empty */
  }

  return WCA;
}

/**Function****************************************************************
  Synopsis    [Function WCAgen]
  Description [s = state in A, t = state in WCA, item = formula
               WCAtype: FALSE = counterexample, TRUE = witness
               In the paper, this function is divided into
               generate(), WAgen(), and CAgen().]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

Est_Boolean
WCAgen(int LTS, int WCA, McDiagnosticItem *item,
       int s, int t, Est_Boolean WCAtype, int explain)
{
  /* TESTING */
  /*
  static int sss=0;
  */

  Bdd_Edge phi1,chi1,chi2,phi2;
  Bdd_Edge sbdd;
  static Est_Boolean strict; /* STATIC TO MINIMIZE STACK PROBLEMS */
  static Est_Boolean linear; /* STATIC TO MINIMIZE STACK PROBLEMS */
  static Est_Boolean OK;     /* STATIC TO MINIMIZE STACK PROBLEMS */
  static Bdd_Edge tmp;       /* STATIC TO MINIMIZE STACK PROBLEMS */
  static int i;              /* STATIC TO MINIMIZE STACK PROBLEMS */

  /* TESTING */
  /*
  sss++;
  fprintf(stderr,"Zacetek WCAgen %d\n",sss);
  */

  /*
  printf("@@");
  for (i=0; i<explain;i++) printf(" ");
  printf("WCAgen: WCAtype = %d (",WCAtype);
  if (!item) printf("NULL)\n");
  if (item && WCAtype) printf("TRUE)\n");
  if (item && !WCAtype) printf("FALSE)\n");
  */

  if (!item) {
    /* WCAtype == NULL is denoted by item == NULL */

    pa_processTable[WCA].tableS[t].final = TRUE;
    if (explain) {
      printf("@@");
      for (i=0; i<explain;i++) printf(" ");
      printf("generate: state ");
      printstate(pa_processTable[WCA].tableS[t].name);
      printf(" marked as final\n");
    }
    return TRUE;

  } else {
    /* WCAtype is TRUE or FALSE */

    if (explain) {
      printf("@@");
      for (i=0; i<explain;i++) printf(" ");
      printf("generate: starting formula `%s' for (s=",item->s);
      printstate(pa_processTable[LTS].tableS[s].name);
      printf(", t=");
      printstate(pa_processTable[WCA].tableS[t].name);
      printf(")\n");
    }

    if (explain) {
      explain = explain + 2;
    }

    chi1 = item->act1;
    phi1 = item->form1;
    chi2 = item->act2;
    phi2 = item->form2;

    sbdd = pa_processTable[LTS].tableS[s].bddR;

    /* add the pair (t,s) to R */
    addR(&(item->R),t,s);

    if (explain) {
      printf("@@");
      for (i=0; i<explain;i++) printf(" ");
      printf("generate: added pair (");
      printstate(pa_processTable[WCA].tableS[t].name);
      printf(",");
      printstate(pa_processTable[LTS].tableS[s].name);
      printf(") to R for the current formula\n");
    }

    strict = TRUE;
    switch (item->type) {

      /* ***************************************************** */
      /* GENERAL RULES FOR WITNESS AND COUNTEREXAMPLE AUTOMATA */
      /* ***************************************************** */

      case MC_CONST:

        /*
        if (explain) {
          printf("@@");
          for (i=0; i<explain;i++) printf(" ");
          printf("WCAgen: type of formula is CONST\n");
        }
        */

        if ((!WCAtype) && (Bdd_isEqv(phi1,bdd_termFalse))) {
          WCAgen(LTS,WCA,NULL,s,t,-1,explain); /*WCAtype=NULL*/
        } else {
          if ((WCAtype) && (Bdd_isEqv(phi1,bdd_termTrue))) {
            WCAgen(LTS,WCA,NULL,s,t,-1,explain); /*WCAtype=NULL*/
          }
        }

        break;

      case MC_NOT:

        /*
        if (explain) {
          printf("@@");
          for (i=0; i<explain;i++) printf(" ");
          printf("WCAgen: type of formula is NOT\n");
        }
        */

        OK = WCAgen(LTS,WCA,item->nextFormula,s,t,!WCAtype,explain);
        if (!OK) return FALSE;

        break;

      case MC_IMPL:

        /*
        if (explain) {
          printf("@@");
          for (i=0; i<explain;i++) printf(" ");
          printf("WCAgen: type of formula is IMPL\n");
        }
        */

        if (WCAtype) {
          /* WITNESS */

          tmp = Bdd_ITE(sbdd,item->nextPrefix->global,bdd_termFalse);
          if (Bdd_isEqv(tmp,bdd_termFalse)) {
            OK = WCAgen(LTS,WCA,item->nextPrefix,s,t,!WCAtype,explain);
            if (!OK) return FALSE;
          }

          tmp = Bdd_ITE(sbdd,item->nextFormula->global,bdd_termFalse);
          if (!Bdd_isEqv(tmp,bdd_termFalse)) {
            OK = WCAgen(LTS,WCA,item->nextFormula,s,t,WCAtype,explain);
            if (!OK) return FALSE;
          }

        } else {
          /* COUNTEREXAMPLE */
          return FALSE;
        }

        break;

      case MC_EQV:

        return FALSE;
        break;

      /* *************************************** */
      /* EXISTENTIAL FRAGMENT - WITNESS AUTOMATA */
      /* *************************************** */

      case MC_OR:

        /*
        if (explain) {
          printf("@@");
          for (i=0; i<explain;i++) printf(" ");
          printf("WCAgen: type of formula is OR\n");
        }
        */

        if (WCAtype) {
          /* WITNESS */

          tmp = Bdd_ITE(sbdd,item->nextPrefix->global,bdd_termFalse);
          if (!Bdd_isEqv(tmp,bdd_termFalse)) {
            OK = WCAgen(LTS,WCA,item->nextPrefix,s,t,WCAtype,explain);
            if (!OK) return FALSE;
          }

          tmp = Bdd_ITE(sbdd,item->nextFormula->global,bdd_termFalse);
          if (!Bdd_isEqv(tmp,bdd_termFalse)) {
            OK = WCAgen(LTS,WCA,item->nextFormula,s,t,WCAtype,explain);
            if (!OK) return FALSE;
          }

        } else {
          /* COUNTEREXAMPLE */
          return FALSE;
        }

        break;

      case MC_EEX:

        /*
        if (explain) {
          printf("@@");
          for (i=0; i<explain;i++) printf(" ");
          printf("WCAgen: type of formula is EEX\n");
        }
        */

        if (WCAtype) {
          /* WITNESS */

          OK = WAbuild(LTS,WCA,item,s,t,bdd_termFalse,bdd_termFalse,
                       chi2,phi2,WCAtype,explain);
          if (!OK) return FALSE;

        } else {
          /* COUNTEREXAMPLE */
          return FALSE;
        }

        break;

      case MC_EEF:

        /*
        if (explain) {
          printf("@@");
          for (i=0; i<explain;i++) printf(" ");
          printf("WCAgen: type of formula is EEF\n");
        }
        */

        if (WCAtype) {
          /* WITNESS */

          OK = WAbuild(LTS,WCA,item,s,t,bdd_termTrue,bdd_termTrue,
                             chi2,phi2,WCAtype,explain);
          if (!OK) return FALSE;

        } else {
          /* COUNTEREXAMPLE */
         return FALSE;
        }

        break;

      case MC_EEU_NS: strict = FALSE;
      case MC_EEU:

        /*
        if (explain) {
          printf("@@");
          for (i=0; i<explain;i++) printf(" ");
          printf("WCAgen: type of formula is EEU\n");
        }
        */

        if (WCAtype) {
          /* WITNESS */

          linear = FALSE;
          if (Bdd_isEqv(phi1,bdd_termTrue)) linear = TRUE;
          if (strict && (Bdd_isEqv(chi1,bdd_termFalse))) linear = TRUE;
          if (strict && (Bdd_isEqv(phi1,bdd_termFalse))) linear = TRUE;

          if (!linear) {
            return FALSE;
          } else {
            OK = WAbuild(LTS,WCA,item,s,t,chi1,phi1,chi2,phi2,WCAtype,explain);
            if (!OK) return FALSE;
          }

        } else {
          /* COUNTEREXAMPLE */
          return FALSE;
        }

        break;

      case MC_EEG_NS: strict = FALSE;
      case MC_EEG:

        /*
        if (explain) {
          printf("@@");
          for (i=0; i<explain;i++) printf(" ");
          printf("WCAgen: type of formula is EEG\n");
        }
        */

        if (WCAtype) {
          /* WITNESS */

          linear = FALSE;
          if (Bdd_isEqv(phi1,bdd_termTrue)) linear = TRUE;

          if (!linear) {
            return FALSE;
          } else {

            tmp = Bdd_ITE(sbdd,pa_processTable[LTS].d,bdd_termFalse);
            if (Bdd_isEqv(tmp,bdd_termFalse)) {

              /*
              if (explain) {
                printf("@@");
                for (i=0; i<explain;i++) printf(" ");
                printf("WAgen: (EEG DEADLOCK)\n");
              }
              */

              WCAgen(LTS,WCA,NULL,s,t,-1,explain); /*WCAtype=NULL*/

            } else {

              /* ONLY IF NOT DEADLOCK */

              OK = WAbuild(LTS,WCA,item,s,t,chi1,phi1,
                             bdd_termFalse,bdd_termFalse,WCAtype,explain);
              if (!OK) return FALSE;

            }

          }

        } else {
          /* COUNTEREXAMPLE */
          return FALSE;
        }

        break;

      case MC_EEW_NS: strict = FALSE;
      case MC_EEW:

        /*
        if (explain) {
          printf("@@");
          for (i=0; i<explain;i++) printf(" ");
          printf("WCAgen: type of formula is EEW\n");
        }
        */

        if (WCAtype) {
          /* WITNESS */

          linear = FALSE;
          if (Bdd_isEqv(phi1,bdd_termTrue)) linear = TRUE;
          if (strict && (Bdd_isEqv(chi1,bdd_termFalse))) linear = TRUE;
          if (strict && (Bdd_isEqv(phi1,bdd_termFalse))) linear = TRUE;

          if (!linear) {
            return FALSE;
          } else {

            tmp = Bdd_ITE(sbdd,pa_processTable[LTS].d,bdd_termFalse);
            if (Bdd_isEqv(tmp,bdd_termFalse)) {

              /*
              if (explain) {
                printf("@@");
                for (i=0; i<explain;i++) printf(" ");
                printf("WAgen: (EEW DEADLOCK)\n");
              }
              */

              WCAgen(LTS,WCA,NULL,s,t,-1,explain); /*WCAtype=NULL*/

            } else {

              /* ONLY IF NOT DEADLOCK */

              OK = WAbuild(LTS,WCA,item,s,t,chi1,phi1,chi2,phi2,WCAtype,explain);
              if (!OK) return FALSE;

            }
          }

        } else {
          /* COUNTEREXAMPLE */
          return FALSE;
        }

        break;

      case MC_EX:

        /*
        if (explain) {
          printf("@@");
          for (i=0; i<explain;i++) printf(" ");
          printf("WCAgen: type of formula is EX\n");
        }
        */

        if (WCAtype) {
          /* WITNESS */

          if (!Bdd_isEqv(chi2,McTau)) {
            chi2 = Bdd_ITE(McTau,bdd_termFalse,chi2);
            Bdd_Fortify(chi2);

            OK = WAbuild(LTS,WCA,item,s,t,bdd_termFalse,bdd_termFalse,
                         chi2,phi2,WCAtype,explain);
            if (!OK) return FALSE;

          } else {

            /* THIS IS USED FOR IMPLICIT MANIPULATION OF DEADLOCKED STATES */
            /*
            tmp = Bdd_ITE(sbdd,pa_processTable[LTS].d,bdd_termFalse);
            */

            /* THIS IS USED FOR EXPLICIT MANIPULATION OF DEADLOCKED STATES */
            /**/
            tmp = bdd_termTrue;
            /**/

            if (Bdd_isEqv(tmp,bdd_termFalse)) {

              /*
              if (explain) {
                printf("@@");
                for (i=0; i<explain;i++) printf(" ");
                printf("WAgen: (EX_tau DEADLOCK)\n");
              }
              */

              OK = WCAgen(LTS,WCA,item->nextFormula,s,t,WCAtype,explain);
              if (!OK) return FALSE;

            } else {

              /* ONLY IF EXPLICIT OR (IMPLICIT AND NOT DEADLOCK) */

              OK = WAbuild(LTS,WCA,item,s,t,bdd_termFalse,bdd_termFalse,
                           chi2,phi2,WCAtype,explain);
              if (!OK) return FALSE;

            }
          }

        } else {
          /* COUNTEREXAMPLE */
          return FALSE;
        }

        break;

      case MC_EF:

        /*
        if (explain) {
          printf("@@");
          for (i=0; i<explain;i++) printf(" ");
          printf("WCAgen: type of formula is EF\n");
        }
        */

        if (WCAtype) {
          /* WITNESS */

          /* this decision is needed because formula is non-strict */
          tmp = Bdd_ITE(sbdd,item->nextFormula->global,bdd_termFalse);
          if (!Bdd_isEqv(tmp,bdd_termFalse)) {
            OK = WCAgen(LTS,WCA,item->nextFormula,s,t,WCAtype,explain);
            if (!OK) return FALSE;
          }

          OK = WAbuild(LTS,WCA,item,s,t,bdd_termTrue,bdd_termTrue,
                       bdd_termTrue,phi2,WCAtype,explain);
          if (!OK) return FALSE;

        } else {
          /* COUNTEREXAMPLE */
          return FALSE;
        }

        break;

      case MC_EG:

        /*
        if (explain) {
          printf("@@");
          for (i=0; i<explain;i++) printf(" ");
          printf("WCAgen: type of formula is EG\n");
        }
        */

        if (WCAtype) {
          /* WITNESS */

          linear = FALSE;
          if (Bdd_isEqv(phi1,bdd_termTrue)) linear = TRUE; /* ALWAYS TRUE */

          if (!linear) {
            return FALSE;
          } else {

            tmp = Bdd_ITE(sbdd,pa_processTable[LTS].d,bdd_termFalse);
            if (Bdd_isEqv(tmp,bdd_termFalse)) {

              /*
              if (explain) {
                printf("@@");
                for (i=0; i<explain;i++) printf(" ");
                printf("WAgen: (EG DEADLOCK)\n");
              }
              */

              WCAgen(LTS,WCA,NULL,s,t,-1,explain); /*WCAtype=NULL*/

            } else {

              /* ONLY IF NOT DEADLOCK */

              OK = WAbuild(LTS,WCA,item,s,t,chi1,phi1,
                           bdd_termFalse,bdd_termFalse,WCAtype,explain);
              if (!OK) return FALSE;

            }
          }

        } else {
          /* COUNTEREXAMPLE */
          return FALSE;
        }

        break;

      case MC_EU:

        /*
        if (explain) {
          printf("@@");
          for (i=0; i<explain;i++) printf(" ");
          printf("WCAgen: type of formula is EU\n");
        }
        */

        if (WCAtype) {
          /* WITNESS */

          linear = FALSE;
          if (Bdd_isEqv(phi1,bdd_termTrue)) linear = TRUE;

          if (!linear) {
            return FALSE;
          } else {

            if (Bdd_isNull(chi2)) {
              tmp = Bdd_ITE(sbdd,item->nextFormula->global,bdd_termFalse);
              if (!Bdd_isEqv(tmp,bdd_termFalse)) {
                OK = WCAgen(LTS,WCA,item->nextFormula,s,t,WCAtype,explain);
                if (!OK) return FALSE;
              }
            }

            if (Bdd_isNull(chi2)) {
              chi1 = Bdd_ITE(chi1,bdd_termTrue,McTau);
              Bdd_Fortify(chi1);
              chi2 = chi1;
            } else {
              chi1 = Bdd_ITE(chi1,bdd_termTrue,McTau);
              chi2 = Bdd_ITE(McTau,bdd_termFalse,chi2);
              Bdd_Fortify(chi1);
              Bdd_Fortify(chi2);
            }

            OK = WAbuild(LTS,WCA,item,s,t,chi1,phi1,chi2,phi2,WCAtype,explain);
            if (!OK) return FALSE;
          }

        } else {
          /* COUNTEREXAMPLE */
          return FALSE;
        }

        break;

      /* ******************************************** */
      /* UNIVERSAL FRAGMENT - COUNTEREXAMPLE AUTOMATA */
      /* ******************************************** */

      case MC_AND:

        /*
        if (explain) {
          printf("@@");
          for (i=0; i<explain;i++) printf(" ");
          printf("WCAgen: type of formula is AND\n");
        }
        */

        if (!WCAtype) {
          /* COUNTEREXAMPLE */

          tmp = Bdd_ITE(sbdd,item->nextPrefix->global,bdd_termFalse);
          if (Bdd_isEqv(tmp,bdd_termFalse)) {
            OK = WCAgen(LTS,WCA,item->nextPrefix,s,t,WCAtype,explain);
            if (!OK) return FALSE;
          }

          tmp = Bdd_ITE(sbdd,item->nextFormula->global,bdd_termFalse);
          if (Bdd_isEqv(tmp,bdd_termFalse)) {
            OK = WCAgen(LTS,WCA,item->nextFormula,s,t,WCAtype,explain);
            if (!OK) return FALSE;
          }

        } else {
          /* WITNESS */
          return FALSE;
        }

        break;

      case MC_AAX:

        /*
        if (explain) {
          printf("@@");
          for (i=0; i<explain;i++) printf(" ");
          printf("WCAgen: type of formula is AAX\n");
        }
        */

        if (!WCAtype) {
          /* COUNTEREXAMPLE */

          OK = CAbuild(LTS,WCA,item,s,t,bdd_termFalse,bdd_termFalse,
                       chi2,phi2,WCAtype,explain);
          if (!OK) return FALSE;

        } else {
          /* WITNESS */
          return FALSE;
        }

        break;

      case MC_AAG_NS: strict = FALSE;
      case MC_AAG:

        /*
        if (explain) {
          printf("@@");
          for (i=0; i<explain;i++) printf(" ");
          printf("WCAgen: type of formula is AAG\n");
        }
        */

        if (!WCAtype) {
          /* COUNTEREXAMPLE */

          if (item->type == MC_AAG_NS) {
            /* this decision is needed because formula is non-strict */
            tmp = Bdd_ITE(sbdd,item->nextPrefix->global,bdd_termFalse);
            if (Bdd_isEqv(tmp,bdd_termFalse)) {
              OK = WCAgen(LTS,WCA,item->nextPrefix,s,t,WCAtype,explain);
              if (!OK) return FALSE;
            }
          }

          OK = CAbuild(LTS,WCA,item,s,t,chi1,phi1,
                       bdd_termFalse,bdd_termFalse,WCAtype,explain);
          if (!OK) return FALSE;

        } else {
          /* WITNESS */
          return FALSE;
        }

        break;

      case MC_AAW_NS: strict = FALSE;
      case MC_AAW:

        /*
        if (explain) {
          printf("@@");
          for (i=0; i<explain;i++) printf(" ");
          printf("WCAgen: type of formula is AAW\n");
        }
        */

        if (!WCAtype) {
          /* COUNTEREXAMPLE */

          linear = FALSE;
          if (Bdd_isEqv(chi1,bdd_termFalse)) linear = TRUE;
          if (Bdd_isEqv(phi1,bdd_termFalse)) linear = TRUE; /* NON-STRICT => ALWAYS FALSE */
          if (Bdd_isEqv(chi2,bdd_termFalse)) linear = TRUE;
          if (Bdd_isEqv(phi2,bdd_termFalse)) linear = TRUE;
          if (Bdd_isEqv(phi2,bdd_termTrue)) linear = TRUE;

          if (!linear) {
            return FALSE;
          } else {

            if ((item->type == MC_AAW_NS) && item->nextPrefix) {
              /* this decision is needed because formula is non-strict */
              tmp = Bdd_ITE(sbdd,item->nextPrefix->global,bdd_termFalse);
              if (Bdd_isEqv(tmp,bdd_termFalse)) {
                OK = WCAgen(LTS,WCA,item->nextPrefix,s,t,WCAtype,explain);
                if (!OK) return FALSE;
              }
            }

            OK = CAbuild(LTS,WCA,item,s,t,chi1,phi1,chi2,phi2,WCAtype,explain);
            if (!OK) return FALSE;
          }

        } else {
          /* WITNESS */
          return FALSE;
        }

        break;

      case MC_AAF:

        /*
        if (explain) {
          printf("@@");
          for (i=0; i<explain;i++) printf(" ");
          printf("WCAgen: type of formula is AAF\n");
        }
        */

        if (!WCAtype) {
          /* COUNTEREXAMPLE */

          linear = FALSE;
          if (Bdd_isEqv(chi2,bdd_termFalse)) linear = TRUE; /* ALWAYS FALSE */
          if (Bdd_isEqv(phi2,bdd_termFalse)) linear = TRUE; /* ALWAYS FALSE */
          if (Bdd_isEqv(phi2,bdd_termTrue)) linear = TRUE;

          if (!linear) {
            return FALSE;
          } else {

            tmp = Bdd_ITE(sbdd,pa_processTable[LTS].d,bdd_termFalse);
            if (Bdd_isEqv(tmp,bdd_termFalse)) {

            /*
            if (explain) {
              printf("@@");
              for (i=0; i<explain;i++) printf(" ");
              printf("CAgen: (AAF DEADLOCK)\n");
            }
            */

            WCAgen(LTS,WCA,NULL,s,t,-1,explain); /*WCAtype=NULL*/

            } else {

              /* ONLY IF NOT DEADLOCK */

              OK = CAbuild(LTS,WCA,item,s,t,bdd_termTrue,bdd_termTrue,
                           chi2,phi2,WCAtype,explain);
              if (!OK) return FALSE;
            }
          }

        } else {
          /* WITNESS */
          return FALSE;
        }

        break;

      case MC_AAU_NS: strict = FALSE;
      case MC_AAU:

        /*
        if (explain) {
          printf("@@");
          for (i=0; i<explain;i++) printf(" ");
          printf("WCAgen: type of formula is AAU\n");
        }
        */

        if (!WCAtype) {
          /* COUNTEREXAMPLE */

          linear = FALSE;
          if (Bdd_isEqv(chi1,bdd_termFalse)) linear = TRUE;
          if (Bdd_isEqv(phi1,bdd_termFalse)) linear = TRUE; /* NON-STRICT => ALWAYS FALSE */
          if (Bdd_isEqv(chi2,bdd_termFalse)) linear = TRUE; /* ALWAYS FALSE */
          if (Bdd_isEqv(phi2,bdd_termFalse)) linear = TRUE; /* ALWAYS FALSE */
          if (Bdd_isEqv(phi2,bdd_termTrue)) linear = TRUE;

          if (!linear) {
            return FALSE;
          } else {

            tmp = Bdd_ITE(sbdd,pa_processTable[LTS].d,bdd_termFalse);
            if (Bdd_isEqv(tmp,bdd_termFalse)) {

              /*
              if (explain) {
                printf("@@");
                for (i=0; i<explain;i++) printf(" ");
                printf("CAgen: (AAU DEADLOCK)\n");
              }
              */

              WCAgen(LTS,WCA,NULL,s,t,-1,explain); /*WCAtype=NULL*/

            } else {

              /* ONLY IF NOT DEADLOCK */

              if ((item->type == MC_AAU_NS) && item->nextPrefix) {
                /* this decision is needed because formula is non-strict */
                tmp = Bdd_ITE(sbdd,item->nextPrefix->global,bdd_termFalse);
                if (Bdd_isEqv(tmp,bdd_termFalse)) {
                  OK = WCAgen(LTS,WCA,item->nextPrefix,s,t,WCAtype,explain);
                  if (!OK) return FALSE;
                }
              }

              OK = CAbuild(LTS,WCA,item,s,t,chi1,phi1,chi2,phi2,WCAtype,explain);
              if (!OK) return FALSE;

            }
          }

        } else {
          /* WITNESS */
          return FALSE;
        }

        break;

      case MC_AX:

        /*
        if (explain) {
          printf("@@");
          for (i=0; i<explain;i++) printf(" ");
          printf("WCAgen: type of formula is AX\n");
        }
        */

        if (!WCAtype) {
          /* COUNTEREXAMPLE */

          tmp = Bdd_ITE(sbdd,pa_processTable[LTS].d,bdd_termFalse);

          if (!Bdd_isEqv(chi2,McTau)) {

            if (Bdd_isEqv(tmp,bdd_termFalse)) {

              /*
              if (explain) {
                printf("@@");
                for (i=0; i<explain;i++) printf(" ");
                printf("CAgen: (AX DEADLOCK)\n");
              }
              */

              WCAgen(LTS,WCA,NULL,s,t,-1,explain); /*WCAtype=NULL*/

            } else {

              /* ONLY IF NOT DEADLOCK */

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

              OK = CAbuild(LTS,WCA,item,s,t,bdd_termFalse,bdd_termFalse,
                           chi2,phi2,WCAtype,explain);
              if (!OK) return FALSE;
            }

          } else {

            if (Bdd_isEqv(tmp,bdd_termFalse)) {

              /*
              if (explain) {
                printf("@@");
                for (i=0; i<explain;i++) printf(" ");
                printf("CAgen: (AX_tau DEADLOCK)\n");
              }
              */

              /* THIS IS USED FOR IMPLICIT MANIPULATION OF DEADLOCKED STATES */
              /*
              OK = WCAgen(LTS,WCA,item->nextFormula,s,t,WCAtype,explain);
              if (!OK) return FALSE;
              */

              /* THIS IS USED FOR EXPLICIT MANIPULATION OF DEADLOCKED STATES */
              /**/
              WCAgen(LTS,WCA,NULL,s,t,-1,explain); /*WCAtype=NULL*/
              /**/

            } else {

              /* ONLY IF NOT DEADLOCK */

              OK = CAbuild(LTS,WCA,item,s,t,bdd_termFalse,bdd_termFalse,
                           chi2,phi2,WCAtype,explain);
              if (!OK) return FALSE;
            }
          }

        } else {
          /* WITNESS */
          return FALSE;
        }

        break;

      case MC_AF:

        /*
        if (explain) {
          printf("@@");
          for (i=0; i<explain;i++) printf(" ");
          printf("WCAgen: type of formula is AF\n");
        }
        */

        if (!WCAtype) {
          /* COUNTEREXAMPLE */

          linear = FALSE;
          if (Bdd_isEqv(chi2,bdd_termFalse)) linear = TRUE; /* ALWAYS FALSE */
          if (Bdd_isEqv(phi2,bdd_termFalse)) linear = TRUE; /* ALWAYS FALSE */
          if (Bdd_isEqv(phi2,bdd_termTrue)) linear = TRUE;

          if (!linear) {
            return FALSE;
          } else {

            tmp = Bdd_ITE(sbdd,pa_processTable[LTS].d,bdd_termFalse);
            if (Bdd_isEqv(tmp,bdd_termFalse)) {

              /*
              if (explain) {
                printf("@@");
                for (i=0; i<explain;i++) printf(" ");
                printf("CAgen: (AF DEADLOCK)\n");
              }
              */

              WCAgen(LTS,WCA,NULL,s,t,-1,explain); /*WCAtype=NULL*/

            } else {

              /* ONLY IF NOT DEADLOCK */

              OK = CAbuild(LTS,WCA,item,s,t,bdd_termTrue,bdd_termTrue,
                           chi2,phi2,WCAtype,explain);
              if (!OK) return FALSE;

            }
          }

        } else {
          /* WITNESS */
          return FALSE;
        }

        break;

      case MC_AG:

        /*
        if (explain) {
          printf("@@");
          for (i=0; i<explain;i++) printf(" ");
          printf("WCAgen: type of formula is AG\n");
        }
        */

        if (!WCAtype) {
          /* COUNTEREXAMPLE */

          /* this decision is needed because formula is non-strict */
          tmp = Bdd_ITE(sbdd,item->nextPrefix->global,bdd_termFalse);
          if (Bdd_isEqv(tmp,bdd_termFalse)) {
            OK = WCAgen(LTS,WCA,item->nextPrefix,s,t,WCAtype,explain);
            if (!OK) return FALSE;
          }

          OK = CAbuild(LTS,WCA,item,s,t,bdd_termTrue,phi1,
                       bdd_termFalse,bdd_termFalse,WCAtype,explain);
          if (!OK) return FALSE;

        } else {
          /* WITNESS */
          return FALSE;
        }

        break;

      case MC_AU:

        /*
        if (explain) {
          printf("@@");
          for (i=0; i<explain;i++) printf(" ");
          printf("WCAgen: type of formula is AU\n");
        }
        */

        if (!WCAtype) {
          /* COUNTEREXAMPLE */

          if (Bdd_isNull(chi2)) {

            linear = FALSE;
            if (Bdd_isEqv(phi1,bdd_termFalse)) linear = TRUE; /* ALWAYS FALSE */
            if (Bdd_isEqv(phi2,bdd_termFalse)) linear = TRUE; /* ALWAYS FALSE */

          } else {

            linear = FALSE;
            if (Bdd_isEqv(phi1,bdd_termFalse)) linear = TRUE; /* ALWAYS FALSE */
            if (Bdd_isEqv(chi2,bdd_termFalse)) linear = TRUE; /* ALWAYS FALSE */
            if (Bdd_isEqv(phi2,bdd_termFalse)) linear = TRUE; /* ALWAYS FALSE */
            if (Bdd_isEqv(phi2,bdd_termTrue)) linear = TRUE;

          }

          if (!linear) {
            return FALSE;
          } else {

          tmp = Bdd_ITE(sbdd,pa_processTable[LTS].d,bdd_termFalse);
          if (Bdd_isEqv(tmp,bdd_termFalse)) {

            /*
            if (explain) {
              printf("@@ CAgen: (AU DEADLOCK)\n");
            }
            */

            WCAgen(LTS,WCA,NULL,s,t,-1,explain); /*WCAtype=NULL*/

          } else {

            /* ONLY IF NOT DEADLOCK */

              if (Bdd_isNull(chi2)) {

                tmp = Bdd_ITE(sbdd,item->nextFormula->global,bdd_termFalse);
                if (!Bdd_isEqv(tmp,bdd_termFalse)) {
                  OK = WCAgen(LTS,WCA,item->nextFormula,s,t,WCAtype,explain);
                  if (!OK) return FALSE;
                }

              } else {

                /* this decision is needed because formula is non-strict */
                if (item->nextPrefix) {
                  tmp = Bdd_ITE(sbdd,item->nextPrefix->global,bdd_termFalse);
                  if (Bdd_isEqv(tmp,bdd_termFalse)) {
                    OK = WCAgen(LTS,WCA,item->nextPrefix,s,t,WCAtype,explain);
                    if (!OK) return FALSE;
                  }
                }

                chi1 = Bdd_ITE(chi1,bdd_termTrue,McTau);
                chi2 = Bdd_ITE(McTau,bdd_termFalse,chi2);
                Bdd_Fortify(chi1);
                Bdd_Fortify(chi2);
                OK = CAbuild(LTS,WCA,item,s,t,chi1,phi1,chi2,phi2,WCAtype,explain);
                if (!OK) return FALSE;

              }
            }
          }

        } else {
          /* WITNESS */
          return FALSE;
        }

        break;

      /* ************************************* */
      /* OTHER                                 */
      /* ************************************* */

      case MC_HME:

        /*
        if (explain) {
          printf("@@");
          for (i=0; i<explain;i++) printf(" ");
          printf("WCAgen: type of formula is HME\n");
        }
        */

        if (WCAtype) {
          /* WITNESS */

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

          OK = WAbuild(LTS,WCA,item,s,t,bdd_termFalse,bdd_termFalse,
                       chi2,phi2,WCAtype,explain);
          if (!OK) return FALSE;

        } else {
          /* COUNTEREXAMPLE */
          return FALSE;
        }

        break;

      case MC_HMA:

        /*
        if (explain) {
          printf("@@");
          for (i=0; i<explain;i++) printf(" ");
          printf("WCAgen: type of formula is HMA\n");
        }
        */

        if (!WCAtype) {
          /* COUNTEREXAMPLE */

          Bdd_Edge D,sup1,sup2,sall,notphi2;

          D = pa_processTable[LTS].d;
          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);
            Bdd_Fortify(sall);                /* the set of all states */
          }

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

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

          OK = WAbuild(LTS,WCA,item,s,t,bdd_termFalse,bdd_termFalse,
                       chi2,notphi2,WCAtype,explain);
          if (!OK) return FALSE;

        } else {
          /* WITNESS */
          return FALSE;
        }

        break;

    } /* ***** END OF switch ***** */

    if (explain) {
      explain = explain - 2;
    }

    /*
    if (explain) {
      printf("@@");
      for (i=0; i<explain;i++) printf(" ");
      printf("generate: formula `%s' finished\n",item->s);
    }
    */

    /* TESTING */
    /*
    fprintf(stderr,"Konec WCAgen %d\n",sss);
    */

    return TRUE;
  }
}

/**Function****************************************************************
  Synopsis    [Function WAbuild]
  Description [s = state in A, t = state in WCA, item = formula]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

Est_Boolean
WAbuild(int LTS, int WCA, McDiagnosticItem *item,
        int s, int t, Bdd_Edge chi1, Bdd_Edge phi1, Bdd_Edge chi2,
        Bdd_Edge phi2, Est_Boolean WCAtype, int explain)
{
  /* TESTING */
  /*
  static int sss=0;
  */

  static Bdd_Edge sbdd;   /* STATIC TO MINIMIZE STACK PROBLEMS */
  static Bdd_Edge state;  /* STATIC TO MINIMIZE STACK PROBLEMS */
  static Bdd_Edge actbdd; /* STATIC TO MINIMIZE STACK PROBLEMS */
  Bdd_Edge snext;
  Bdd_Edge transition;
  static int sprime;      /* STATIC TO MINIMIZE STACK PROBLEMS */
  static int act;         /* STATIC TO MINIMIZE STACK PROBLEMS */
  static int type;        /* STATIC TO MINIMIZE STACK PROBLEMS */
  static Est_Boolean OK;  /* STATIC TO MINIMIZE STACK PROBLEMS */
  static int i;           /* STATIC TO MINIMIZE STACK PROBLEMS */

  /* TESTING */
  /*
  sss++;
  fprintf(stderr,"Zacetek WAbuild %d\n",sss);
  */

  /* PART 1 */
  /* snext is the set of all (chi1,phi1)-transitions from s to phi-state */
  /* phi is formula given as an input to this function */

  sbdd = pa_processTable[LTS].tableS[s].bddR;
  snext = Bdd_RelOp(phi1,item->global,"#AND R2S",TRUE);
  snext = Bdd_ITE(chi1,snext,bdd_termFalse);
  snext = Bdd_ITE(pa_processTable[LTS].d,snext,bdd_termFalse);
  snext = Bdd_ITE(sbdd,snext,bdd_termFalse);

  while (!Bdd_isEqv(snext,bdd_termFalse)) {
    transition = Pa_ExtractProcTransition(&pa_processTable[LTS],snext);

    state = Bdd_RelOpSimple(transition,"Ex xR xA S2R",TRUE);
    actbdd = Bdd_RelOpSimple(transition,"Ex xR xS",TRUE);

    sprime = Pa_EnumerateProcState(&pa_processTable[LTS],state);
    act = Pa_EnumerateSortAction(&pa_sortTable[pa_processTable[LTS].sort],actbdd);
    if (act % 2) type = 1; else type = 0;
    act = act/2;

    if (explain) {
      printf("@@");
      for (i=0; i<explain;i++) printf(" ");
      printf("WAbuild: chosen transition ");
      printstate(pa_processTable[LTS].tableS[s].name);
      printf("-");
      printf("%s",pa_sortTable[pa_processTable[LTS].sort].table[act].name);
      if (type == 0) printf("?");
      if (type == 1) printf("!");
      printf("->");
      printstate(pa_processTable[LTS].tableS[sprime].name);
      printf(" from delta1\n");
    }

    OK = conbuild(LTS,WCA,item,act,type,sprime,t,WCAtype,explain);
    if (!OK) {

      /**/
      if (explain) {
        printf("@@");
        for (i=0; i<explain;i++) printf(" ");
        printf("WAbuild: conbuild for part 1 return FALSE\n");
      }
      /**/

      return FALSE;
    }

    snext = Bdd_ITE(transition,bdd_termFalse,snext);
  }

  /* PART 2 */
  /* snext is the set of all (chi2,phi2)-transitions from s */

  sbdd = pa_processTable[LTS].tableS[s].bddR;
  snext = Bdd_RelOp(chi2,phi2,"#AND R2S",TRUE);
  snext = Bdd_ITE(pa_processTable[LTS].d,snext,bdd_termFalse);
  snext = Bdd_ITE(sbdd,snext,bdd_termFalse);

  while (!Bdd_isEqv(snext,bdd_termFalse)) {
    transition = Pa_ExtractProcTransition(&pa_processTable[LTS],snext);

    state = Bdd_RelOpSimple(transition,"Ex xR xA S2R",TRUE);
    actbdd = Bdd_RelOpSimple(transition,"Ex xR xS",TRUE);

    sprime = Pa_EnumerateProcState(&pa_processTable[LTS],state);
    act = Pa_EnumerateSortAction(&pa_sortTable[pa_processTable[LTS].sort],actbdd);
    if (act % 2) type = 1; else type = 0;
    act = act/2;

    if (explain) {
      printf("@@");
      for (i=0; i<explain;i++) printf(" ");
      printf("WAbuild: chosen transition ");
      printstate(pa_processTable[LTS].tableS[s].name);
      printf("-");
      printf("%s",pa_sortTable[pa_processTable[LTS].sort].table[act].name);
      if (type == 0) printf("?");
      if (type == 1) printf("!");
      printf("->");
      printstate(pa_processTable[LTS].tableS[sprime].name);
      printf(" from delta2\n");
    }

    /* this is (chi2,phi2)-transitions, we must prove phi2 */
    OK = conbuild(LTS,WCA,item->nextFormula,act,type,sprime,t,WCAtype,explain);
    if (!OK) {

      /**/
      if (explain) {
        printf("@@");
        for (i=0; i<explain;i++) printf(" ");
        printf("WAbuild: conbuild for part 2 return FALSE\n");
      }
      /**/

      return FALSE;
    }

    snext = Bdd_ITE(transition,bdd_termFalse,snext);
  }

  /* TESTING */
  /*
  fprintf(stderr,"Konec WAbuild %d\n",sss);
  */

  return TRUE;
}

/**Function****************************************************************
  Synopsis    [Function CAbuild]
  Description [s = state in A, t = state in WCA, item = formula]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

Est_Boolean
CAbuild(int LTS, int WCA, McDiagnosticItem *item,
        int s, int t, Bdd_Edge chi1, Bdd_Edge phi1, Bdd_Edge chi2,
        Bdd_Edge phi2, Est_Boolean WCAtype, int explain)
{
  /* TESTING */
  /*
  static int sss=0;
  */

  static Bdd_Edge sup1;     /* STATIC TO MINIMIZE STACK PROBLEMS */
  static Bdd_Edge sup2;     /* STATIC TO MINIMIZE STACK PROBLEMS */
  static Bdd_Edge sbdd;     /* STATIC TO MINIMIZE STACK PROBLEMS */
  static Bdd_Edge sall;     /* STATIC TO MINIMIZE STACK PROBLEMS */
  static Bdd_Edge invalid;  /* STATIC TO MINIMIZE STACK PROBLEMS */
  static Bdd_Edge D1not;    /* STATIC TO MINIMIZE STACK PROBLEMS */
  static Bdd_Edge D2not;    /* STATIC TO MINIMIZE STACK PROBLEMS */
  Bdd_Edge snext;
  Bdd_Edge transition;
  static Bdd_Edge state;    /* STATIC TO MINIMIZE STACK PROBLEMS */
  Bdd_Edge actbdd;
  int sprime;
  int act;
  int type;
  static Est_Boolean OK;    /* STATIC TO MINIMIZE STACK PROBLEMS */
  static int i;             /* STATIC TO MINIMIZE STACK PROBLEMS */

  /* TESTING */
  /*
  sss++;
  fprintf(stderr,"Zacetek WAbuild %d\n",sss);
  recursion(0);
  */

  /* PART 1 */
  /* snext is the set of all (chi1,phi)-transitions from s to not-phi-state */
  /* phi is a formula given as an input to this function */
  /* sall is the set of all states in LTS */
  /* invalid is the set of all states in LTS, where AAW is not valid */

  sup1 = Bdd_RelOpSimple(pa_processTable[LTS].d,"Ex xA xS",TRUE);
  sup2 = Bdd_RelOpSimple(pa_processTable[LTS].d,"Ex xA xR S2R",TRUE);
  sall = Bdd_ITE(sup1,bdd_termTrue,sup2);
  invalid = Bdd_ITE(item->global,bdd_termFalse,sall);

  sbdd = pa_processTable[LTS].tableS[s].bddR;
  snext = Bdd_RelOp(phi1,invalid,"#AND R2S",TRUE);
  snext = Bdd_ITE(chi1,snext,bdd_termFalse);
  snext = Bdd_ITE(pa_processTable[LTS].d,snext,bdd_termFalse);
  snext = Bdd_ITE(sbdd,snext,bdd_termFalse);

  while (!Bdd_isEqv(snext,bdd_termFalse)) {
    transition = Pa_ExtractProcTransition(&pa_processTable[LTS],snext);

    state = Bdd_RelOpSimple(transition,"Ex xR xA S2R",TRUE);
    actbdd = Bdd_RelOpSimple(transition,"Ex xR xS",TRUE);

    sprime = Pa_EnumerateProcState(&pa_processTable[LTS],state);
    act = Pa_EnumerateSortAction(&pa_sortTable[pa_processTable[LTS].sort],actbdd);
    if (act % 2) type = 1; else type = 0;
    act = act/2;

    if (explain) {
      printf("@@");
      for (i=0; i<explain;i++) printf(" ");
      printf("CAbuild: chosen transition ");
      printstate(pa_processTable[LTS].tableS[s].name);
      printf("-");
      printf("%s",pa_sortTable[pa_processTable[LTS].sort].table[act].name);
      if (type == 0) printf("?");
      if (type == 1) printf("!");
      printf("->");
      printstate(pa_processTable[LTS].tableS[sprime].name);
      printf(" from delta1\n");
    }

    OK = conbuild(LTS,WCA,item,act,type,sprime,t,WCAtype,explain);
    if (!OK) {

      /**/
      if (explain) {
        printf("@@");
        for (i=0; i<explain;i++) printf(" ");
        printf("CAbuild: conbuild for part 1 return FALSE\n");
      }
      /**/

      return FALSE;
    }

    snext = Bdd_ITE(transition,bdd_termFalse,snext);
  }

  /* PART 2 */
  /* snext is the set of all not(chi1,phi1)-and-not(chi2,phi2)-transitions from s */
  /* D1not is the set of all not(chi1,phi1)-transitions in LTS */
  /* D2not is the set of all not(chi2,phi2)-transitions in LTS */

  sup1 = Bdd_ITE(chi1,phi1,bdd_termFalse);
  sup1 = Bdd_RelOpSimple(sup1,"R2S",TRUE);
  D1not = Bdd_ITE(sup1,bdd_termFalse,pa_processTable[LTS].d);
  Bdd_Fortify(D1not);

  sup2 = Bdd_ITE(chi2,phi2,bdd_termFalse);
  sup2 = Bdd_RelOpSimple(sup2,"R2S",TRUE);
  D2not = Bdd_ITE(sup2,bdd_termFalse,pa_processTable[LTS].d);
  Bdd_Fortify(D2not);

  sbdd = pa_processTable[LTS].tableS[s].bddR;
  snext = Bdd_ITE(D1not,D2not,bdd_termFalse);
  snext = Bdd_ITE(sbdd,snext,bdd_termFalse);

  while (!Bdd_isEqv(snext,bdd_termFalse)) {
    transition = Pa_ExtractProcTransition(&pa_processTable[LTS],snext);

    state = Bdd_RelOpSimple(transition,"Ex xR xA S2R",TRUE);
    actbdd = Bdd_RelOpSimple(transition,"Ex xR xS",TRUE);

    sprime = Pa_EnumerateProcState(&pa_processTable[LTS],state);
    act = Pa_EnumerateSortAction(&pa_sortTable[pa_processTable[LTS].sort],actbdd);
    if (act % 2) type = 1; else type = 0;
    act = act/2;

    if (explain) {
      printf("@@");
      for (i=0; i<explain;i++) printf(" ");
      printf("CAbuild: chosen transition ");
      printstate(pa_processTable[LTS].tableS[s].name);
      printf("-");
      printf("%s",pa_sortTable[pa_processTable[LTS].sort].table[act].name);
      if (type == 0) printf("?");
      if (type == 1) printf("!");
      printf("->");
      printstate(pa_processTable[LTS].tableS[sprime].name);
      printf(" from delta2\n");
    }

    /* PART 2A */
    /* if this is not-chi1-transition and not-chi2-transition */
    /* then the counterexample is finished and we do not need recursive calls */
    sup1 = Bdd_ITE(actbdd,chi1,bdd_termFalse);
    sup2 = Bdd_ITE(actbdd,chi2,bdd_termFalse);
    if (Bdd_isEqv(sup1,bdd_termFalse) && Bdd_isEqv(sup2,bdd_termFalse)) {
      OK = conbuild(LTS,WCA,NULL,act,type,sprime,t,-1,explain); /*WCAtype=NULL*/
      if (!OK) {

        /**/
        if (explain) {
          printf("@@");
          for (i=0; i<explain;i++) printf(" ");
          printf("CAbuild: conbuild for part 2A return FALSE\n");
        }
        /**/

        return FALSE;
      }
    }

    /* PART 2B */
    /* if this is chi1-transition we must prove not-phi1 */
    sup1 = Bdd_ITE(actbdd,chi1,bdd_termFalse);
    if (!Bdd_isEqv(sup1,bdd_termFalse)) {
      OK = conbuild(LTS,WCA,item->nextPrefix,act,type,sprime,t,WCAtype,explain);
      if (!OK) {

        /**/
        if (explain) {
          printf("@@");
          for (i=0; i<explain;i++) printf(" ");
          printf("CAbuild: conbuild for part 2B return FALSE\n");
        }
        /**/

        return FALSE;
      }
    }

    /* PART 2C */
    /* if this is chi2-transition we must prove not-phi2 */
    sup1 = Bdd_ITE(actbdd,chi2,bdd_termFalse);
    if (!Bdd_isEqv(sup1,bdd_termFalse)) {
      OK = conbuild(LTS,WCA,item->nextFormula,act,type,sprime,t,WCAtype,explain);
      if (!OK) {

        /**/
        if (explain) {
          printf("@@");
          for (i=0; i<explain;i++) printf(" ");
          printf("CAbuild: conbuild for part 2C return FALSE\n");
        }
        /**/

        return FALSE;
      }
    }

    snext = Bdd_ITE(transition,bdd_termFalse,snext);
  }

  /* TESTING */
  /*
  fprintf(stderr,"Konec WAbuild %d\n",sss);
  */

  return TRUE;
}

/**Function****************************************************************
  Synopsis    [Function conbuild]
  Description [s,s1 = states in A, t,t1 = states in WCA, item = formula]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

Est_Boolean
conbuild(int LTS, int WCA, McDiagnosticItem *item, int act, int type,
         int sprime, int t, Est_Boolean WCAtype, int explain)
{
  static int tprime;      /* STATIC TO MINIMIZE STACK PROBLEMS */
  static Est_Boolean OK;  /* STATIC TO MINIMIZE STACK PROBLEMS */
  static int i;           /* STATIC TO MINIMIZE STACK PROBLEMS */

  if (explain) {
    printf("@@");
    for (i=0; i<explain;i++) printf(" ");
    printf("conbuild: ");
  }

  /* check if sprime has been already visited with the given formula */

  if (!item) {
    tprime = -1;
  } else {
    tprime = findR(item->R,sprime);
  }

  if (tprime == -1) {

    /* create a new state tprime in WCA */
    tprime = newstate(WCA,pa_processTable[LTS].tableS[sprime].name);

    if (explain) {
      printf("created state ");
      printstate(pa_processTable[WCA].tableS[tprime].name);
      printf(", ");
    }

    /* add the transition t -> tprime in WCA */
    build(WCA,t,act,type,tprime,explain);

    /* compute the result for the given formula in (sprime,tprime) */
    OK = WCAgen(LTS,WCA,item,sprime,tprime,WCAtype,explain);
    if (!OK) return FALSE;

  } else {

    /* add the transition t -> tprime in WCA */
    build(WCA,t,act,type,tprime,explain);

  }

  return TRUE;
}

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

/**Function****************************************************************
  Synopsis    [Function build]
  Description [t,t1 = states in WCA,
               In the paper, this is a part of conbuild().]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

static void
build(int WCA, int t, int act, int type, int tprime, int explain)
{
  int before,after;

  /* add the transition t -> tprime in WCA */
  before = pa_processTable[WCA].numTransitions;
  Pa_FOATransition(&pa_processTable[WCA], t, act, type, tprime);
  after = pa_processTable[WCA].numTransitions;

  if (explain) {
    if (before == after) {
      printf("transition ");
    } else {
      printf("created transition ");
    }
    printstate(pa_processTable[WCA].tableS[t].name);
    printf("-");
    printf("%s",pa_sortTable[pa_processTable[WCA].sort].table[act].name);
    if (type == 0) printf("?");
    if (type == 1) printf("!");
    printf("->");
    printstate(pa_processTable[WCA].tableS[tprime].name);

    if (before == after) {
      printf(" exists");
    }

    printf("\n");
  }
}

/**Function****************************************************************
  Synopsis    [Function newstate]
  Description [create a new state in WCA]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

static int
newstate(int WCA, Est_String sname)
{
  int tprime;
  Est_String prefix;

  /* choose one of the following methods */

  /* 1. Names of states in WCA will consist of prefix and sequence number */
  /**/
  prefix = strdup("wc");
  tprime = Pa_FOANextStateProcess(&pa_processTable[WCA],prefix);
  free(prefix);
  /**/

  /* 2. Names of states in WCA will be related to the names in LTS */
  /*    I do not use this, because CCS parser produce bad LTS names */
  /*
  int i;
  Est_String tname;
  i = strcspn(sname,"<");
  tname = (char *) malloc(i+1);
  memcpy(tname,sname,i);
  tname[i]=0;
  tprime = Pa_AddStateProcess(&pa_processTable[WCA],tname);
  free(tname);
  */

  return tprime;
}

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

static void
addR(McTypeR *R, int t, int s)
{

  if (R->num == 0) {
    R->tableT = (int *) malloc (sizeof(int));
    R->tableS = (int *) malloc (sizeof(int));
    R->tableT[0] = t;
    R->tableS[0] = s;
    R->num = 1;
  } else {
    (R->num)++;
    R->tableT = (int *) realloc (R->tableT, R->num * sizeof(int));
    R->tableS = (int *) realloc (R->tableS, R->num * sizeof(int));
    R->tableT[(R->num)-1] = t;
    R->tableS[(R->num)-1] = s;
  }
}

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

static int
findR(McTypeR R, int s)
{
  int i;
  int t;

  t = -1;
  for(i=0; i<R.num; i++) {
    if (s == R.tableS[i]) {
      t = R.tableT[i];
    }
  }

  return t;
}

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

static void
deleteR(McTypeR *R)
{
  R->num = 0;
  if (R->tableT) free(R->tableT);
  if (R->tableS) free(R->tableS);
}

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

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

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