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

  FileName    [mcDiagnostic.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 mcDiagnostic.c contains functions for generation
               of witnesses and counterexamples and the explanations.]
  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 Est_Boolean DiagnosticEEU(McDiagnosticType dgn,
                   Bdd_Edge D, McDiagnosticItem *item, Est_Boolean strict);

static Est_Boolean DiagnosticEEW(McDiagnosticType dgn,
                   Bdd_Edge D, McDiagnosticItem *item, Est_Boolean strict);

static Est_Boolean DiagnosticEEX(McDiagnosticType dgn,
                   Bdd_Edge D, McDiagnosticItem *item);

static Est_Boolean DiagnosticEEF(McDiagnosticType dgn,
                   Bdd_Edge D, McDiagnosticItem *item);

static Est_Boolean DiagnosticEEG(McDiagnosticType dgn,
                   Bdd_Edge D, McDiagnosticItem *item, Est_Boolean strict);

static Est_Boolean DiagnosticAAU(McDiagnosticType dgn,
                   Bdd_Edge D, McDiagnosticItem *item, Est_Boolean strict);

static Est_Boolean DiagnosticAAW(McDiagnosticType dgn,
                   Bdd_Edge D, McDiagnosticItem *item, Est_Boolean strict);

static Est_Boolean DiagnosticAAX(McDiagnosticType dgn,
                   Bdd_Edge D, McDiagnosticItem *item);

static Est_Boolean DiagnosticAAF(McDiagnosticType dgn,
                   Bdd_Edge D, McDiagnosticItem *item);

static Est_Boolean DiagnosticAAG(McDiagnosticType dgn,
                   Bdd_Edge D, McDiagnosticItem *item, Est_Boolean strict);

static Est_Boolean DiagnosticEU(McDiagnosticType dgn,
                   Bdd_Edge D, McDiagnosticItem *item);

static Est_Boolean DiagnosticAU(McDiagnosticType dgn,
                   Bdd_Edge D, McDiagnosticItem *item);

static Est_Boolean DiagnosticEX(McDiagnosticType dgn,
                   Bdd_Edge D, McDiagnosticItem *item);

static Est_Boolean DiagnosticAX(McDiagnosticType dgn,
                   Bdd_Edge D, McDiagnosticItem *item);

static Est_Boolean DiagnosticEF(McDiagnosticType dgn,
                   Bdd_Edge D, McDiagnosticItem *item);

static Est_Boolean DiagnosticAF(McDiagnosticType dgn,
                   Bdd_Edge D, McDiagnosticItem *item);

static Est_Boolean DiagnosticEG(McDiagnosticType dgn,
                   Bdd_Edge D, McDiagnosticItem *item);

static Est_Boolean DiagnosticAG(McDiagnosticType dgn,
                   Bdd_Edge D, McDiagnosticItem *item);

static Est_Boolean DiagnosticHME(McDiagnosticType dgn,
                   Bdd_Edge D, McDiagnosticItem *item);

static Est_Boolean DiagnosticHMA(McDiagnosticType dgn,
                   Bdd_Edge D, McDiagnosticItem *item);

static void pathValid(McDiagnosticType dgn, int num, Bdd_Edge state1,
              Bdd_Edge state2, Est_Boolean explain, Est_Boolean tracepath);

static void pathInvalid(McDiagnosticType dgn, int num, Bdd_Edge state1,
        Bdd_Edge state2, Est_Boolean explain, Est_Boolean tracepath);

static void transitionValid(McDiagnosticType dgn, int num, Bdd_Edge state1,
        Bdd_Edge state2, Est_Boolean explain, Est_Boolean tracepath);

static void transitionInvalid(McDiagnosticType dgn, int num, Bdd_Edge state1,
              Bdd_Edge state2, Est_Boolean explain, Est_Boolean tracepath);

static void transitionNone(McDiagnosticType dgn, int num,
              Est_Boolean explain, Est_Boolean tracepath);

static void transitionAll(McDiagnosticType dgn, int num,
              Est_Boolean explain, Est_Boolean tracepath);

static void deadlockedValid(McDiagnosticType dgn, int num, Bdd_Edge state1,
              McDiagnosticItem *nextitem, Est_Boolean explain,
              Est_Boolean tracepath);

static void deadlockedInvalid(McDiagnosticType dgn, int num, Bdd_Edge state1,
              McDiagnosticItem *nextitem, Est_Boolean explain,
              Est_Boolean tracepath);

static void stateValid(McDiagnosticType dgn, int num, Bdd_Edge state1,
              McDiagnosticItem *nextitem, Est_Boolean explain,
              Est_Boolean tracepath);

static void stateInvalid(McDiagnosticType dgn, int num, Bdd_Edge state1,
        McDiagnosticItem *nextitem, Est_Boolean explain,
              Est_Boolean tracepath);

static void stateInvalid2(McDiagnosticType dgn, int num, Bdd_Edge state1,
              int nextnum1, int nextnum2, Est_Boolean explain,
              Est_Boolean tracepath);

static void pathNone(McDiagnosticType dgn, int num, Est_Boolean explain,
        Est_Boolean tracepath);

static void pathAll(McDiagnosticType dgn, int num, Est_Boolean explain,
              Est_Boolean tracepath);

static void createSpinTrail(McDiagnosticType dgn, McFunctionSequence *seq,
              Pa_Sort *sort, Est_String *msc, Est_Boolean firstitem);

static void createPath(McDiagnosticType dgn, McFunctionSequence *fseq,
              Est_String *path, Est_String *spntrl, Est_String *msc,
              Est_Boolean explain, Est_Boolean tracepath);

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

static void concatInt(Est_String *s1, const int n);

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

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

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

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

McDiagnosticType
McCreateDiagnostic(Bdd_Edge D, Bdd_Edge init, int proc, int comp)
{
  McDiagnosticType dgn;

  dgn.proc = proc;
  dgn.comp = comp;
  dgn.D = D;
  dgn.init = init;
  dgn.item = NULL;
  dgn.tree = bdd_termFalse;
  dgn.automaton = bdd_termFalse;

  return dgn;
}

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

void
McAddDiagnostic(McDiagnosticItem **item, Bdd_Edge result, Bdd_Edge act1,
                Bdd_Edge form1, Bdd_Edge act2, Bdd_Edge form2, int type,
                Est_String s, Est_String sx,
                McDiagnosticItem *itemPrefix, McDiagnosticItem *itemFormula)
{
  *item = (McDiagnosticItem *) malloc(sizeof(McDiagnosticItem));
  (*item)->ready = FALSE;
  (*item)->num = 0;
  (*item)->state1 = bdd_termNull;
  (*item)->state2 = bdd_termNull;
  (*item)->lastaction = bdd_termTrue;
  (*item)->act1 = act1;
  (*item)->form1 = form1;
  (*item)->act2 = act2;
  (*item)->form2 = form2;
  (*item)->type = type;
  (*item)->r = FALSE;
  (*item)->global = result;
  (*item)->path = NULL;
  (*item)->s = strdup(s);
  (*item)->sx = strdup(sx);
  (*item)->R.num = 0;
  (*item)->R.tableT = NULL;
  (*item)->R.tableS = NULL;
  (*item)->nextPrefix = itemPrefix;
  (*item)->nextFormula = itemFormula;
}

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

void
McDeleteFunctionSequence(McFunctionSequence *path)
{
  McFunctionSequence *item;

  while (path) {
    item = path;
    path = path->nextFunction;
    free(item);
  }
}

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

void
McDeleteDiagnostic(McDiagnosticItem *item)
{
  if (item) {
    if (item->nextPrefix) McDeleteDiagnostic(item->nextPrefix);
    if (item->nextFormula) McDeleteDiagnostic(item->nextFormula);
    if (item->path) McDeleteFunctionSequence(item->path);
    if (item->s) free(item->s);
    if (item->sx) free(item->sx);
    if (item->R.tableT) free(item->R.tableT);
    if (item->R.tableS) free(item->R.tableS);
    free(item);
  }
}

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

void
McPrepareDiagnostic(McDiagnosticType dgn, Bdd_Edge D,
                    McDiagnosticItem **item, Bdd_Edge init,
                    Est_Boolean first)
{
  Bdd_Edge sup,sup1,sup2;
  Est_Boolean strict,r;
  static int num;

  if ((*item)) {

    (*item)->ready = TRUE;

    if (first) num=0; else num++;

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

      case MC_CONST:
            (*item)->num=num;
            (*item)->state1 = init;
            (*item)->state2 = bdd_termNull;

            if (Bdd_isEqv((*item)->form1,bdd_termFalse)) (*item)->r = FALSE;
            if (Bdd_isEqv((*item)->form1,bdd_termTrue)) (*item)->r = TRUE;

            break;

      case MC_EEU_NS: strict = FALSE;
      case MC_EEU:
            (*item)->num=num;
            (*item)->state1 = init;
            r = DiagnosticEEU(dgn,D,*item,strict);
            (*item)->r = r;

            if (r) {

              /* TRUE */

              /* create diagnostic for subformula */
              McPrepareDiagnostic(dgn,
                D,&(*item)->nextFormula,(*item)->state2,FALSE);

            } else {

              /* FALSE => NOT APPLICABLE */

              /* we are not able to explain this */

            }

            if ((*item)->nextPrefix && !(*item)->nextPrefix->ready) {
              McDeleteDiagnostic((*item)->nextPrefix);
              (*item)->nextPrefix = NULL;
            }
            if ((*item)->nextFormula && !(*item)->nextFormula->ready) {
              McDeleteDiagnostic((*item)->nextFormula);
              (*item)->nextFormula = NULL;
            }

            /* USE THE FOLLOWING TWO LINES TO REMOVE DIAGNOSTIC */
            /*
            McDeleteDiagnostic(*item);
            *item = NULL;
            */

            break;

      case MC_EEW_NS: strict = FALSE;
      case MC_EEW:
            (*item)->num=num;
            (*item)->state1 = init;
            r = DiagnosticEEW(dgn,D,*item,strict);
            (*item)->r = (r != 0);

            if (r != 0) {

              if (r == 1) {

                /* TRUE (EUU TRUE) */

                /* create diagnostic for subformula (EEU) */
                McPrepareDiagnostic(dgn,
                  D,&(*item)->nextFormula,(*item)->state2,FALSE);

              }

              if ( r == 2) {

                /* TRUE (EUU FALSE, EEG TRUE) AND DEADLOCK AND NON-STRICT */

                /* create diagnostic for subformula (EEG) */
                McPrepareDiagnostic(dgn,
                  D,&(*item)->nextPrefix,(*item)->state2,FALSE);

              }

              if ( r == 3) {

                /* TRUE (EUU FALSE, EEG TRUE) AND DEADLOCK AND STRICT  => ALWAYS TRUE */
                /* TRUE (EUU FALSE, EEG TRUE) BUT NOT DEADLOCK => NOT APPLICABLE */

                /* we are not able to explain this */

              }

            } else {

              if (Bdd_isEqv(D,bdd_termFalse)) {

                /* FALSE AND DEADLOCK => POSSIBLE ONLY WITH NON-STRICT */

                /* create diagnostic for subformula */
                McPrepareDiagnostic(dgn,
                  D,&(*item)->nextPrefix,(*item)->state1,FALSE);

              } else {

                /* FALSE AND NOT DEADLOCK => NOT APPLICABLE */

                /* we are not able to explain this */

              }
            }

            if ((*item)->nextPrefix && !(*item)->nextPrefix->ready) {
              McDeleteDiagnostic((*item)->nextPrefix);
              (*item)->nextPrefix = NULL;
            }
            if ((*item)->nextFormula && !(*item)->nextFormula->ready) {
              McDeleteDiagnostic((*item)->nextFormula);
              (*item)->nextFormula = NULL;
            }

            /* USE THE FOLLOWING TWO LINES TO REMOVE DIAGNOSTIC */
            /*
            McDeleteDiagnostic(*item);
            *item = NULL;
            */

            break;

      case MC_EEX:
            (*item)->num=num;
            (*item)->state1 = init;
            r = DiagnosticEEX(dgn,D,*item);
            (*item)->r = r;

            if (r) {

              /* TRUE */

              /* create diagnostic for subformula */
              McPrepareDiagnostic(dgn,
                D,&(*item)->nextFormula,(*item)->state2,FALSE);

            } else {

              /* FALSE => NOT APPLICABLE */

              /* we are not able to explain this */

            }

            if ((*item)->nextPrefix && !(*item)->nextPrefix->ready) {
              McDeleteDiagnostic((*item)->nextPrefix);
              (*item)->nextPrefix = NULL;
            }
            if ((*item)->nextFormula && !(*item)->nextFormula->ready) {
              McDeleteDiagnostic((*item)->nextFormula);
              (*item)->nextFormula = NULL;
            }

            /* USE THE FOLLOWING TWO LINES TO REMOVE DIAGNOSTIC */
            /*
            McDeleteDiagnostic(*item);
            *item = NULL;
            */

            break;

      case MC_EEF:
            (*item)->num=num;
            (*item)->state1 = init;
            r = DiagnosticEEF(dgn,D,*item);
            (*item)->r = r;

            if (r) {

              /* TRUE */

              /* create diagnostic for subformula */
              McPrepareDiagnostic(dgn,
                D,&(*item)->nextFormula,(*item)->state2,FALSE);

            } else {

              /* FALSE => NOT APPLICABLE */

              /* we are not able to explain this */

            }

            if ((*item)->nextPrefix && !(*item)->nextPrefix->ready) {
              McDeleteDiagnostic((*item)->nextPrefix);
              (*item)->nextPrefix = NULL;
            }
            if ((*item)->nextFormula && !(*item)->nextFormula->ready) {
              McDeleteDiagnostic((*item)->nextFormula);
              (*item)->nextFormula = NULL;
            }

            /* USE THE FOLLOWING TWO LINES TO REMOVE DIAGNOSTIC */
            /*
            McDeleteDiagnostic(*item);
            *item = NULL;
            */

            break;

      case MC_EEG_NS: strict = FALSE;
      case MC_EEG:
            (*item)->num=num;
            (*item)->state1 = init;
            r = DiagnosticEEG(dgn,D,*item,strict);
            (*item)->r = r;

            if (r) {

              if (Bdd_isEqv(D,bdd_termFalse)) {

                if (Bdd_isEqv((*item)->lastaction,bdd_termFalse)) {

                  /* TRUE AND DEADLOCK AND NON-STRICT */

                  /* create diagnostic for subformula */
                  McPrepareDiagnostic(dgn,
                    D,&(*item)->nextPrefix,(*item)->state2,FALSE);

                } else {

                  /* TRUE AND DEADLOCK AND STRICT => ALWAYS TRUE */

                  /* we are not able to explain this */

                }

              } else {

                /* TRUE BUT NOT DEADLOCK => NOT APPLICABLE */

                /* we are not able to explain this in each state */

              }

            } else {

              if (Bdd_isEqv(D,bdd_termFalse)) {

                /* FALSE AND DEADLOCK => POSSIBLE ONLY WITH NON-STRICT */

                /* create diagnostic for subformula */
                McPrepareDiagnostic(dgn,
                  D,&(*item)->nextPrefix,(*item)->state1,FALSE);

              } else {

                /* FALSE AND NOT DEADLOCK => NOT APPLICABLE */

                /* we are not able to explain this */

              }
            }

            if ((*item)->nextPrefix && !(*item)->nextPrefix->ready) {
              McDeleteDiagnostic((*item)->nextPrefix);
              (*item)->nextPrefix = NULL;
            }
            if ((*item)->nextFormula && !(*item)->nextFormula->ready) {
              McDeleteDiagnostic((*item)->nextFormula);
              (*item)->nextFormula = NULL;
            }

            /* USE THE FOLLOWING TWO LINES TO REMOVE DIAGNOSTIC */
            /*
            McDeleteDiagnostic(*item);
            *item = NULL;
            */

            break;

      case MC_AAU_NS: strict = FALSE;
      case MC_AAU:
            (*item)->num=num;
            (*item)->state1 = init;
            r = DiagnosticAAU(dgn,D,*item,strict);
            (*item)->r = (r == 0);

            if (r == 1) {

              if (Bdd_isEqv(D,bdd_termFalse)) {

                /* FALSE (AAW FALSE) AND DEADLOCK => POSSIBLE ONLY WITH NON-STRICT */
                /* DEADLOCK => AAF IS ALWAYS FALSE => AAU_NS IS ALWAYS FALSE */

                /* we are not able to explain this */

              } else {

                if (Bdd_isEqv((*item)->lastaction,bdd_termFalse)) {

                  /* FALSE (AAW FALSE) AND NOT DEADLOCK */
                  /* NON-STRICT AND FIRST SUBFORMULA INVALID IN INITIAL STATE */

                  /* create diagnostic for subformula */
                  McPrepareDiagnostic(dgn,
                    D,&(*item)->nextPrefix,(*item)->state2,FALSE);

                } else {

                  if (Bdd_isNull((*item)->act2)) {
                    sup1 = Bdd_ITE((*item)->lastaction,(*item)->act1,bdd_termFalse);
                    sup2 = sup1;
                  } else {
                    sup1 = Bdd_ITE((*item)->lastaction,(*item)->act1,bdd_termFalse);
                    sup2 = Bdd_ITE((*item)->lastaction,(*item)->act2,bdd_termFalse);
                  }

                  /* FALSE (AAW FALSE) AND NOT DEADLOCK */
                  /* STRICT OR (NON-STRICT AND FIRST SUBFORMULA VALID IN INITIAL STATE) */
                  /* FIRST ACTION VALID, FIRST SUBFORMULA BECOMES INVALID */

                  if (!Bdd_isEqv(sup1,bdd_termFalse)) {
                    /* create diagnostic for subformula (AAW) */
                    McPrepareDiagnostic(dgn,
                      D,&(*item)->nextPrefix,(*item)->state2,FALSE);
                  }

                  /* FALSE (AAW FALSE) AND NOT DEADLOCK */
                  /* STRICT OR (NON-STRICT AND FIRST SUBFORMULA VALID IN INITIAL STATE) */
                  /* SECOND ACTION VALID, SECOND SUBFORMULA INVALID */

                  if (!Bdd_isEqv(sup2,bdd_termFalse)) {
                    /* create diagnostic for subformula (AAW) */
                    McPrepareDiagnostic(dgn,
                      D,&(*item)->nextFormula,(*item)->state2,FALSE);
                  }

                }
              }
            }

            if (r == 2) {

              if (Bdd_isEqv(D,bdd_termFalse)) {

                /* FALSE (AAW TRUE, AAF FALSE) AND DEADLOCK => ALWAYS FALSE */

                /* we are not able to explain this */

              } else {

                /* FALSE (AAW TRUE, AAF FALSE) AND NOT DEADLOCK => NOT APPLICABLE */

                /* we are not able to explain this */

              }

            }

            if (r == 0) {

              /* TRUE (POSSIBLE ONLY WITH NON DEADLOCK) => NOT APPLICABLE */

              /* we are not able to explain this */

            }

            if ((*item)->nextPrefix && !(*item)->nextPrefix->ready) {
              McDeleteDiagnostic((*item)->nextPrefix);
              (*item)->nextPrefix = NULL;
            }
            if ((*item)->nextFormula && !(*item)->nextFormula->ready) {
              McDeleteDiagnostic((*item)->nextFormula);
              (*item)->nextFormula = NULL;
            }

            /* USE THE FOLLOWING TWO LINES TO REMOVE DIAGNOSTIC */
            /*
            McDeleteDiagnostic(*item);
            *item = NULL;
            */

            break;

      case MC_AAW_NS: strict = FALSE;
      case MC_AAW:
            (*item)->num=num;
            (*item)->state1 = init;
            r = DiagnosticAAW(dgn,D,*item,strict);
            (*item)->r = r;

            if (!r) {

              if (Bdd_isEqv(D,bdd_termFalse)) {

                /* FALSE AND DEADLOCK => POSSIBLE ONLY WITH NON-STRICT */

                /* create diagnostic for subformula */
                McPrepareDiagnostic(dgn,
                  D,&(*item)->nextPrefix,(*item)->state2,FALSE);

              } else {

                if (Bdd_isEqv((*item)->lastaction,bdd_termFalse)) {

                  /* FALSE AND NOT DEADLOCK */
                  /* NON-STRICT AND FIRST SUBFORMULA INVALID IN INITIAL STATE */

                  /* create diagnostic for subformula */
                  McPrepareDiagnostic(dgn,
                    D,&(*item)->nextPrefix,(*item)->state2,FALSE);

                } else {

                  if (Bdd_isNull((*item)->act2)) {
                    sup1 = Bdd_ITE((*item)->lastaction,(*item)->act1,bdd_termFalse);
                    sup2 = sup1;
                  } else {
                    sup1 = Bdd_ITE((*item)->lastaction,(*item)->act1,bdd_termFalse);
                    sup2 = Bdd_ITE((*item)->lastaction,(*item)->act2,bdd_termFalse);
                  }

                  if (!Bdd_isEqv(sup1,bdd_termFalse)) {

                    /* FALSE AND NOT DEADLOCK */
                    /* STRICT OR (NON-STRICT AND FIRST SUBFORMULA VALID IN INITIAL STATE) */
                    /* FIRST ACTION VALID, FIRST SUBFORMULA BECOMES INVALID */

                    /* create diagnostic for subformula */
                    McPrepareDiagnostic(dgn,
                      D,&(*item)->nextPrefix,(*item)->state2,FALSE);

                  }

                  if (!Bdd_isEqv(sup2,bdd_termFalse)) {

                    /* FALSE AND NOT DEADLOCK */
                    /* STRICT OR (NON-STRICT AND FIRST SUBFORMULA VALID IN INITIAL STATE) */
                    /* SECOND ACTION VALID, SECOND SUBFORMULA INVALID */

                    /* create diagnostic for subformula */
                    McPrepareDiagnostic(dgn,
                      D,&(*item)->nextFormula,(*item)->state2,FALSE);
                  }
                }
              }

            } else {

              if (Bdd_isEqv(D,bdd_termFalse)) {

                if (Bdd_isEqv((*item)->lastaction,bdd_termFalse)) {

                  /* TRUE AND DEADLOCK AND NON-STRICT */

                  /* create diagnostic for subformula */
                  McPrepareDiagnostic(dgn,
                    D,&(*item)->nextPrefix,(*item)->state1,FALSE);

                } else {

                  /* TRUE AND DEADLOCK AND STRICT => ALWAYS TRUE */

                  /* we are not able to explain this */

                }

              } else {

                /* TRUE AND NOT DEADLOCK => NOT APPLICABLE */

                /* we are not able to explain this */

              }

            }

            if ((*item)->nextPrefix && !(*item)->nextPrefix->ready) {
              McDeleteDiagnostic((*item)->nextPrefix);
              (*item)->nextPrefix = NULL;
            }
            if ((*item)->nextFormula && !(*item)->nextFormula->ready) {
              McDeleteDiagnostic((*item)->nextFormula);
              (*item)->nextFormula = NULL;
            }

            /* USE THE FOLLOWING TWO LINES TO REMOVE DIAGNOSTIC */
            /*
            McDeleteDiagnostic(*item);
            *item = NULL;
            */

            break;

      case MC_AAX:
            (*item)->num=num;
            (*item)->state1 = init;
            r = DiagnosticAAX(dgn,D,*item);
            (*item)->r = r;

            if (!r) {

              sup = Bdd_ITE((*item)->lastaction,(*item)->act2,bdd_termFalse);
              if (!Bdd_isEqv(sup,bdd_termFalse)) {

                /* FALSE */
                /* ACTION VALID, SUBFORMULA INVALID */

                /* create diagnostic for subformula */
                McPrepareDiagnostic(dgn,
                  D,&(*item)->nextFormula,(*item)->state2,FALSE);

              }

            } else {

              /* TRUE => NOT APPLICABLE */

              /* we are not able to explain this */

            }

            if ((*item)->nextPrefix && !(*item)->nextPrefix->ready) {
              McDeleteDiagnostic((*item)->nextPrefix);
              (*item)->nextPrefix = NULL;
            }
            if ((*item)->nextFormula && !(*item)->nextFormula->ready) {
              McDeleteDiagnostic((*item)->nextFormula);
              (*item)->nextFormula = NULL;
            }

            /* USE THE FOLLOWING TWO LINES TO REMOVE DIAGNOSTIC */
            /*
            McDeleteDiagnostic(*item);
            *item = NULL;
            */

            break;

      case MC_AAF:
            (*item)->num=num;
            (*item)->state1 = init;
            r = DiagnosticAAF(dgn,D,*item);
            (*item)->r = r;

            if (!r) {

              if (Bdd_isEqv(D,bdd_termFalse)) {

                /* FALSE AND DEADLOCK => ALWAYS FALSE */

                /* we are not able to explain this */

              } else {

                /* FALSE AND NOT DEADLOCK => NOT APPLICABLE */

                /* we are not able to explain this */

              }

            } else {

              /* TRUE => NOT APPLICABLE */

              /* we are not able to explain this */

            }

            if ((*item)->nextPrefix && !(*item)->nextPrefix->ready) {
              McDeleteDiagnostic((*item)->nextPrefix);
              (*item)->nextPrefix = NULL;
            }
            if ((*item)->nextFormula && !(*item)->nextFormula->ready) {
              McDeleteDiagnostic((*item)->nextFormula);
              (*item)->nextFormula = NULL;
            }

            /* USE THE FOLLOWING TWO LINES TO REMOVE DIAGNOSTIC */
            /*
            McDeleteDiagnostic(*item);
            *item = NULL;
            */

            break;

      case MC_AAG_NS: strict = FALSE;
      case MC_AAG:
            (*item)->num=num;
            (*item)->state1 = init;
            r = DiagnosticAAG(dgn,D,*item,strict);
            (*item)->r = r;

            if (!r) {

              if (Bdd_isEqv((*item)->lastaction,bdd_termFalse)) {

                /* FALSE AND NON-STRICT AND SUBFORMULA INVALID IN INITIAL STATE */

                /* create diagnostic for subformula */
                McPrepareDiagnostic(dgn,
                  D,&(*item)->nextPrefix,(*item)->state2,FALSE);

              } else {

                sup = Bdd_ITE((*item)->lastaction,(*item)->act1,bdd_termFalse);
                if (!Bdd_isEqv(sup,bdd_termFalse)) {

                  /* FALSE */
                  /* STRICT OR (NON-STRICT AND SUBFORMULA VALID IN INITIAL STATE) */
                  /* ACTION VALID, SUBFORMULA INVALID */

                  /* create diagnostic for subformula */
                  McPrepareDiagnostic(dgn,
                    D,&(*item)->nextPrefix,(*item)->state2,FALSE);

                }

              }

            } else {

              if (Bdd_isEqv(D,bdd_termFalse)) {

                if (Bdd_isEqv((*item)->lastaction,bdd_termFalse)) {

                  /* TRUE AND DEADLOCK AND NON-STRICT */

                  /* create diagnostic for subformula */
                  McPrepareDiagnostic(dgn,
                    D,&(*item)->nextPrefix,(*item)->state1,FALSE);

                } else {

                  /* TRUE AND DEADLOCK AND STRICT => ALWAYS TRUE */

                  /* we are not able to explain this */

                }

              } else {

                /* TRUE AND NOT DEADLOCK => NOT APPLICABLE */

                /* we are not able to explain this */

              }

            }

            if ((*item)->nextPrefix && !(*item)->nextPrefix->ready) {
              McDeleteDiagnostic((*item)->nextPrefix);
              (*item)->nextPrefix = NULL;
            }
            if ((*item)->nextFormula && !(*item)->nextFormula->ready) {
              McDeleteDiagnostic((*item)->nextFormula);
              (*item)->nextFormula = NULL;
            }

            /* USE THE FOLLOWING TWO LINES TO REMOVE DIAGNOSTIC */
            /*
            McDeleteDiagnostic(*item);
            *item = NULL;
            */

            break;

      case MC_EU:
            (*item)->num=num;
            (*item)->state1 = init;
            r = DiagnosticEU(dgn,D,*item);
            (*item)->r = r;

            if (r) {

              /* TRUE */

              /* create diagnostic for subformula */
              McPrepareDiagnostic(dgn,
                D,&(*item)->nextFormula,(*item)->state2,FALSE);

            } else {

              /* FALSE => NOT APPLICABLE */

              /* we are not able to explain this */

            }

            if ((*item)->nextPrefix && !(*item)->nextPrefix->ready) {
              McDeleteDiagnostic((*item)->nextPrefix);
              (*item)->nextPrefix = NULL;
            }
            if ((*item)->nextFormula && !(*item)->nextFormula->ready) {
              McDeleteDiagnostic((*item)->nextFormula);
              (*item)->nextFormula = NULL;
            }

            /* USE THE FOLLOWING TWO LINES TO REMOVE DIAGNOSTIC */
            /*
            McDeleteDiagnostic(*item);
            *item = NULL;
            */

            break;

      case MC_EX:
            (*item)->num=num;
            (*item)->state1 = init;
            r = DiagnosticEX(dgn,D,*item);
            (*item)->r = r;

            if (r) {

              if (Bdd_isEqv(D,bdd_termFalse)) {

                /* TRUE AND DEADLOCK => POSSIBLE ONLY WITH TAU */

                /* create diagnostic for subformula */
                McPrepareDiagnostic(dgn,
                  D,&(*item)->nextFormula,(*item)->state1,FALSE);

              } else {

                /* TRUE AND NOT DEADLOCK */

                /* create diagnostic for subformula */
                McPrepareDiagnostic(dgn,
                  D,&(*item)->nextFormula,(*item)->state2,FALSE);

              }

            } else {

              if (Bdd_isEqv(D,bdd_termFalse) && Bdd_isEqv((*item)->lastaction,bdd_termFalse)) {

                /* FALSE AND DEADLOCK AND TAU */

                /* create diagnostic for subformula */
                McPrepareDiagnostic(dgn,
                  D,&(*item)->nextFormula,(*item)->state1,FALSE);

              } else {

                /* FALSE AND NOT (DEADLOCK AND TAU) => NOT APPLICABLE */

                /* we are not able to explain this */

              }
            }

            if ((*item)->nextPrefix && !(*item)->nextPrefix->ready) {
              McDeleteDiagnostic((*item)->nextPrefix);
              (*item)->nextPrefix = NULL;
            }
            if ((*item)->nextFormula && !(*item)->nextFormula->ready) {
              McDeleteDiagnostic((*item)->nextFormula);
              (*item)->nextFormula = NULL;
            }

            /* USE THE FOLLOWING TWO LINES TO REMOVE DIAGNOSTIC */
            /*
            McDeleteDiagnostic(*item);
            *item = NULL;
            */

            break;

      case MC_EF:
            (*item)->num=num;
            (*item)->state1 = init;
            r = DiagnosticEF(dgn,D,*item);
            (*item)->r = r;

            if (r) {

              /* TRUE */

              /* create diagnostic for subformula */
              McPrepareDiagnostic(dgn,
                D,&(*item)->nextFormula,(*item)->state2,FALSE);

            } else {

              if (Bdd_isEqv(D,bdd_termFalse)) {

                /* FALSE AND DEADLOCK */

                /* create diagnostic for subformula */
                McPrepareDiagnostic(dgn,
                  D,&(*item)->nextFormula,(*item)->state1,FALSE);

              } else {

                /* FALSE AND NOT DEADLOCK => NOT APPLICABLE */

                /* we are not able to explain this */

              }
            }

            if ((*item)->nextPrefix && !(*item)->nextPrefix->ready) {
              McDeleteDiagnostic((*item)->nextPrefix);
              (*item)->nextPrefix = NULL;
            }
            if ((*item)->nextFormula && !(*item)->nextFormula->ready) {
              McDeleteDiagnostic((*item)->nextFormula);
              (*item)->nextFormula = NULL;
            }

            /* USE THE FOLLOWING TWO LINES TO REMOVE DIAGNOSTIC */
            /*
            McDeleteDiagnostic(*item);
            *item = NULL;
            */

            break;

      case MC_EG:
            (*item)->num=num;
            (*item)->state1 = init;
            r = DiagnosticEG(dgn,D,*item);
            (*item)->r = r;

            if (r) {

              if (Bdd_isEqv(D,bdd_termFalse)) {

                /* TRUE AND DEADLOCK */

                /* create diagnostic for subformula */
                McPrepareDiagnostic(dgn,
                  D,&(*item)->nextPrefix,(*item)->state2,FALSE);

              } else {

                /* TRUE BUT NOT DEADLOCK => NOT APPLICABLE */

                /* we are not able to explain this */

              }

            } else {

              if (Bdd_isEqv(D,bdd_termFalse)) {

                /* FALSE AND DEADLOCK */

                /* create diagnostic for subformula */
                McPrepareDiagnostic(dgn,
                  D,&(*item)->nextPrefix,(*item)->state1,FALSE);

              } else {

                /* FALSE AND NOT DEADLOCK => NOT APPLICABLE */

                /* we are not able to explain this */

              }
            }

            if ((*item)->nextPrefix && !(*item)->nextPrefix->ready) {
              McDeleteDiagnostic((*item)->nextPrefix);
              (*item)->nextPrefix = NULL;
            }
            if ((*item)->nextFormula && !(*item)->nextFormula->ready) {
              McDeleteDiagnostic((*item)->nextFormula);
              (*item)->nextFormula = NULL;
            }

            /* USE THE FOLLOWING TWO LINES TO REMOVE DIAGNOSTIC */
            /*
            McDeleteDiagnostic(*item);
            *item = NULL;
            */

            break;

      case MC_AU:
            (*item)->num=num;
            (*item)->state1 = init;
            r = DiagnosticAU(dgn,D,*item);
            (*item)->r = ((r == 0) || (r == 3));

            if (r == 1) {

              if (Bdd_isEqv(D,bdd_termFalse)) {

                /* FALSE (AAW FALSE) AND DEADLOCK */
                /* DEADLOCK => AAF IS ALWAYS FALSE => AU IS ALWAYS FALSE */

                /* we are not able to explain this */

              } else {

                if (Bdd_isEqv((*item)->lastaction,bdd_termFalse)) {

                  /* FALSE (AAW FALSE) AND NOT DEADLOCK */
                  /* NON-STRICT AND FIRST SUBFORMULA INVALID IN INITIAL STATE */

                  /* create diagnostic for subformula */
                  McPrepareDiagnostic(dgn,
                    D,&(*item)->nextPrefix,(*item)->state2,FALSE);

                } else {

                  if (Bdd_isNull((*item)->act2)) {
                    sup1 = Bdd_ITE((*item)->lastaction,(*item)->act1,bdd_termFalse);
                    sup2 = sup1;
                  } else {
                    sup1 = Bdd_ITE((*item)->lastaction,(*item)->act1,bdd_termFalse);
                    sup2 = Bdd_ITE((*item)->lastaction,(*item)->act2,bdd_termFalse);
                  }

                  /* FALSE (AAW FALSE) AND NOT DEADLOCK */
                  /* NON-STRICT AND FIRST SUBFORMULA VALID IN INITIAL STATE */
                  /* FIRST ACTION VALID, FIRST SUBFORMULA BECOMES INVALID */

                  if (!Bdd_isEqv(sup1,bdd_termFalse)) {
                    /* create diagnostic for subformula (AAW) */
                    McPrepareDiagnostic(dgn,
                      D,&(*item)->nextPrefix,(*item)->state2,FALSE);
                  }

                  /* FALSE (AAW FALSE) AND NOT DEADLOCK */
                  /* NON-STRICT AND FIRST SUBFORMULA VALID IN INITIAL STATE */
                  /* SECOND ACTION VALID, SECOND SUBFORMULA INVALID */

                  if (!Bdd_isEqv(sup2,bdd_termFalse)) {
                    /* create diagnostic for subformula (AAW) */
                    McPrepareDiagnostic(dgn,
                      D,&(*item)->nextFormula,(*item)->state2,FALSE);
                  }

                }
              }
            }

            if (r == 2) {

              if (Bdd_isEqv(D,bdd_termFalse)) {

                /* FALSE (AAW TRUE, AAF FALSE) AND DEADLOCK => ALWAYS FALSE */

                /* we are not able to explain this */

              } else {

                /* FALSE (AAW TRUE, AAF FALSE) AND NOT DEADLOCK => NOT APPLICABLE */

                /* we are not able to explain this */

              }

            }

            if (r == 3) {

              /* TRUE AND SECOND SUBFORMULA VALID IN INITIAL STATE */

              /* create diagnostic for subformula */
              McPrepareDiagnostic(dgn,
                D,&(*item)->nextFormula,(*item)->state1,FALSE);

            }

            if (r == 0) {

              /* TRUE AND SECOND SUBFORMULA NOT VALID IN INITIAL STATE => NOT APPLICABLE */

              /* we are not able to explain this */

            }

            if ((*item)->nextPrefix && !(*item)->nextPrefix->ready) {
              McDeleteDiagnostic((*item)->nextPrefix);
              (*item)->nextPrefix = NULL;
            }
            if ((*item)->nextFormula && !(*item)->nextFormula->ready) {
              McDeleteDiagnostic((*item)->nextFormula);
              (*item)->nextFormula = NULL;
            }

            /* USE THE FOLLOWING TWO LINES TO REMOVE DIAGNOSTIC */
            /*
            McDeleteDiagnostic(*item);
            *item = NULL;
            */

            break;

      case MC_AX:
            (*item)->num=num;
            (*item)->state1 = init;
            r = DiagnosticAX(dgn,D,*item);
            (*item)->r = r;

            if (!r) {

              if (Bdd_isEqv(D,bdd_termFalse)) {

                if (Bdd_isEqv((*item)->act2,McTau)) {

                  /* FALSE AND DEADLOCK AND TAU */

                  /* create diagnostic for subformula */
                  McPrepareDiagnostic(dgn,
                    D,&(*item)->nextFormula,(*item)->state2,FALSE);

                } else {

                  /* FALSE AND DEADLOCK AND NOT TAU => ALWAYS FALSE */

                  /* we are not able to explain this */

                }

              } else {

                if (Bdd_isEqv((*item)->act2,McTau)) {
                  sup = Bdd_ITE((*item)->lastaction,McTau,bdd_termFalse);
                } else {
                  sup = Bdd_ITE((*item)->lastaction,(*item)->act2,bdd_termFalse);
                  sup = Bdd_ITE(McTau,bdd_termFalse,sup);
                }

                if (!Bdd_isEqv(sup,bdd_termFalse)) {

                  /* FALSE AND NOT DEADLOCK */
                  /* ACTION VALID, SUBFORMULA INVALID */

                  /* create diagnostic for subformula */
                  McPrepareDiagnostic(dgn,
                    D,&(*item)->nextFormula,(*item)->state2,FALSE);

                }
              }

            } else {

              if (Bdd_isEqv(D,bdd_termFalse) && Bdd_isEqv((*item)->lastaction,bdd_termFalse)) {

                /* TRUE AND DEADLOCK AND TAU */

                /* create diagnostic for subformula */
                McPrepareDiagnostic(dgn,
                  D,&(*item)->nextFormula,(*item)->state1,FALSE);

              } else {

                /* TRUE AND NOT (DEADLOCK AND TAU) => NOT APPLICABLE */

                /* we are not able to explain this */

              }
            }

            if ((*item)->nextPrefix && !(*item)->nextPrefix->ready) {
              McDeleteDiagnostic((*item)->nextPrefix);
              (*item)->nextPrefix = NULL;
            }
            if ((*item)->nextFormula && !(*item)->nextFormula->ready) {
              McDeleteDiagnostic((*item)->nextFormula);
              (*item)->nextFormula = NULL;
            }

            /* USE THE FOLLOWING TWO LINES TO REMOVE DIAGNOSTIC */
            /*
            McDeleteDiagnostic(*item);
            *item = NULL;
            */

            break;

      case MC_AF:
            (*item)->num=num;
            (*item)->state1 = init;
            r = DiagnosticAF(dgn,D,*item);
            (*item)->r = ((r == 0) || (r == 3));

            if (r == 2) {

              if (Bdd_isEqv(D,bdd_termFalse)) {

                /* FALSE AND DEADLOCK */

                /* create diagnostic for subformula */
                McPrepareDiagnostic(dgn,
                  D,&(*item)->nextFormula,(*item)->state1,FALSE);

              } else {

                /* FALSE AND NOT DEADLOCK => NOT APPLICABLE */

                /* we are not able to explain this */

              }

            }

            if (r == 3) {

              /* TRUE AND SUBFORMULA VALID IN INITIAL STATE */

              /* create diagnostic for subformula */
              McPrepareDiagnostic(dgn,
                D,&(*item)->nextFormula,(*item)->state1,FALSE);
            }

            if (r == 0) {

              /* TRUE AND SUBFORMULA VALID IN INITIAL STATE => NOT APPLICABLE */

              /* we are not able to explain this */

            }

            if ((*item)->nextPrefix && !(*item)->nextPrefix->ready) {
              McDeleteDiagnostic((*item)->nextPrefix);
              (*item)->nextPrefix = NULL;
            }
            if ((*item)->nextFormula && !(*item)->nextFormula->ready) {
              McDeleteDiagnostic((*item)->nextFormula);
              (*item)->nextFormula = NULL;
            }

            /* USE THE FOLLOWING TWO LINES TO REMOVE DIAGNOSTIC */
            /*
            McDeleteDiagnostic(*item);
            *item = NULL;
            */

            break;

      case MC_AG:
            (*item)->num=num;
            (*item)->state1 = init;
            r = DiagnosticAG(dgn,D,*item);
            (*item)->r = r;

            if (!r) {

              /* FALSE */

              /* create diagnostic for subformula */
              McPrepareDiagnostic(dgn,
                 D,&(*item)->nextPrefix,(*item)->state2,FALSE);

            } else {

              if (Bdd_isEqv(D,bdd_termFalse)) {

                /* TRUE AND DEADLOCK */

                /* create diagnostic for subformula */
                McPrepareDiagnostic(dgn,
                  D,&(*item)->nextPrefix,(*item)->state1,FALSE);

              } else {

                /* TRUE AND NOT DEADLOCK => NOT APPLICABLE */

                /* we are not able to explain this */

              }

            }

            if ((*item)->nextPrefix && !(*item)->nextPrefix->ready) {
              McDeleteDiagnostic((*item)->nextPrefix);
              (*item)->nextPrefix = NULL;
            }
            if ((*item)->nextFormula && !(*item)->nextFormula->ready) {
              McDeleteDiagnostic((*item)->nextFormula);
              (*item)->nextFormula = NULL;
            }

            /* USE THE FOLLOWING TWO LINES TO REMOVE DIAGNOSTIC */
            /*
            McDeleteDiagnostic(*item);
            *item = NULL;
            */

            break;

      case MC_HME:
            (*item)->num=num;
            (*item)->state1 = init;
            r = DiagnosticHME(dgn,D,*item);
            (*item)->r = r;

            if (r) {

              /* TRUE */

              /* create diagnostic for subformula */
              McPrepareDiagnostic(dgn,
                D,&(*item)->nextFormula,(*item)->state2,FALSE);

            } else {

              /* FALSE => NOT APPLICABLE */

              /* we are not able to explain this */

            }

            if ((*item)->nextPrefix && !(*item)->nextPrefix->ready) {
              McDeleteDiagnostic((*item)->nextPrefix);
              (*item)->nextPrefix = NULL;
            }
            if ((*item)->nextFormula && !(*item)->nextFormula->ready) {
              McDeleteDiagnostic((*item)->nextFormula);
              (*item)->nextFormula = NULL;
            }

            /* USE THE FOLLOWING TWO LINES TO REMOVE DIAGNOSTIC */
            /*
            McDeleteDiagnostic(*item);
            *item = NULL;
            */

            break;

      case MC_HMA:
            (*item)->num=num;
            (*item)->state1 = init;
            r = DiagnosticHMA(dgn,D,*item);
            (*item)->r = r;

            if (!r) {

              /* FALSE */

              /* create diagnostic for subformula */
              McPrepareDiagnostic(dgn,
                D,&(*item)->nextFormula,(*item)->state2,FALSE);

            } else {

              /* TRUE => NOT APPLICABLE */

              /* we are not able to explain this */

            }

            if ((*item)->nextPrefix && !(*item)->nextPrefix->ready) {
              McDeleteDiagnostic((*item)->nextPrefix);
              (*item)->nextPrefix = NULL;
            }
            if ((*item)->nextFormula && !(*item)->nextFormula->ready) {
              McDeleteDiagnostic((*item)->nextFormula);
              (*item)->nextFormula = NULL;
            }

            /* USE THE FOLLOWING TWO LINES TO REMOVE DIAGNOSTIC */
            /*
            McDeleteDiagnostic(*item);
            *item = NULL;
            */

            break;

      case MC_NOT:
            (*item)->num=num;
            (*item)->state1 = init;
            (*item)->state2 = init;

            McPrepareDiagnostic(dgn,
              D,&(*item)->nextFormula,(*item)->state2,FALSE);

            if ((*item)->nextFormula) {
              (*item)->r = !((*item)->nextFormula->r);
            } else {

            }

            if ((*item)->nextPrefix && !(*item)->nextPrefix->ready) {
              McDeleteDiagnostic((*item)->nextPrefix);
              (*item)->nextPrefix = NULL;
            }
            if ((*item)->nextFormula && !(*item)->nextFormula->ready) {
              McDeleteDiagnostic((*item)->nextFormula);
              (*item)->nextFormula = NULL;
            }

            break;

      case MC_AND:
            (*item)->num=num;
            (*item)->state1 = init;
            (*item)->state2 = init;

            McPrepareDiagnostic(dgn,
              D,&(*item)->nextPrefix,(*item)->state2,FALSE);

            McPrepareDiagnostic(dgn,
              D,&(*item)->nextFormula,(*item)->state2,FALSE);

            if ((*item)->nextPrefix && (*item)->nextFormula) {
              (*item)->r =
                ((*item)->nextPrefix->r) && ((*item)->nextFormula->r);
            } else {

            }

            if ((*item)->nextPrefix && !(*item)->nextPrefix->ready) {
              McDeleteDiagnostic((*item)->nextPrefix);
              (*item)->nextPrefix = NULL;
            }
            if ((*item)->nextFormula && !(*item)->nextFormula->ready) {
              McDeleteDiagnostic((*item)->nextFormula);
              (*item)->nextFormula = NULL;
            }

            break;

      case MC_OR:
            (*item)->num=num;
            (*item)->state1 = init;
            (*item)->state2 = init;

            McPrepareDiagnostic(dgn,
              D,&(*item)->nextPrefix,(*item)->state2,FALSE);

            McPrepareDiagnostic(dgn,
              D,&(*item)->nextFormula,(*item)->state2,FALSE);

            if ((*item)->nextPrefix && (*item)->nextFormula) {
              (*item)->r =
                ((*item)->nextPrefix->r) || ((*item)->nextFormula->r);
            } else {

            }

            if ((*item)->nextPrefix && !(*item)->nextPrefix->ready) {
              McDeleteDiagnostic((*item)->nextPrefix);
              (*item)->nextPrefix = NULL;
            }
            if ((*item)->nextFormula && !(*item)->nextFormula->ready) {
              McDeleteDiagnostic((*item)->nextFormula);
              (*item)->nextFormula = NULL;
            }

            break;

      case MC_EQV:
            (*item)->num=num;
            (*item)->state1 = init;
            (*item)->state2 = init;

            McPrepareDiagnostic(dgn,
              D,&(*item)->nextPrefix,(*item)->state2,FALSE);

            McPrepareDiagnostic(dgn,
              D,&(*item)->nextFormula,(*item)->state2,FALSE);

            if ((*item)->nextPrefix && (*item)->nextFormula) {
              (*item)->r =
                ((*item)->nextPrefix->r) == ((*item)->nextFormula->r);
            } else {

            }

            if ((*item)->nextPrefix && !(*item)->nextPrefix->ready) {
              McDeleteDiagnostic((*item)->nextPrefix);
              (*item)->nextPrefix = NULL;
            }
            if ((*item)->nextFormula && !(*item)->nextFormula->ready) {
              McDeleteDiagnostic((*item)->nextFormula);
              (*item)->nextFormula = NULL;
            }

            break;

      case MC_IMPL:
            (*item)->num=num;
            (*item)->state1 = init;
            (*item)->state2 = init;

            McPrepareDiagnostic(dgn,
              D,&(*item)->nextPrefix,(*item)->state2,FALSE);

            McPrepareDiagnostic(dgn,
              D,&(*item)->nextFormula,(*item)->state2,FALSE);

            if ((*item)->nextPrefix && (*item)->nextFormula) {
              (*item)->r =
                !((*item)->nextPrefix->r) || ((*item)->nextFormula->r);
            } else {

            }

            if ((*item)->nextPrefix && !(*item)->nextPrefix->ready) {
              McDeleteDiagnostic((*item)->nextPrefix);
              (*item)->nextPrefix = NULL;
            }
            if ((*item)->nextFormula && !(*item)->nextFormula->ready) {
              McDeleteDiagnostic((*item)->nextFormula);
              (*item)->nextFormula = NULL;
            }

            break;

    }
  }
}

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

void
McPrintDiagnostic(McDiagnosticType dgn, McDiagnosticItem *item, int indent,
                  Est_String *path, Est_String *spntrl, Est_String *msc,
                  Est_Boolean explain, Est_Boolean tracepath)
{
  if (item) {

    if (explain) {
      printf("@@ #%d:%s:",item->num,item->s);
      if (item->r) printf("T:"); else printf("F:");
      if (dgn.proc != -1) Pa_DecodeProcessStates(&pa_processTable[dgn.proc],item->state1,TRUE);
      if (dgn.comp != -1) Pa_DecodeCompStates(&pa_compositionTable[dgn.comp],item->state1,TRUE);
      printf("\n");
    }

    switch (item->type) {

      case MC_CONST:

        if (item->r) {
          if (explain) {
            printf("@@ Formula #%d is always TRUE.\n",item->num);
          }
        } else {
          if (explain) {
            printf("@@ Formula #%d is always FALSE.\n",item->num);
          }
        }

        break;

      case MC_EEU:
      case MC_EEU_NS:

        if (item->r) {

          pathValid(dgn,item->num,item->state1,item->state2,explain,tracepath);

          if (item->path) {
            createPath(dgn,item->path->nextFunction,path,spntrl,msc,explain,tracepath);
          }
          if (explain) printf("\n");

          if ((item->nextFormula) && (item->nextFormula->ready))
            McPrintDiagnostic(dgn,item->nextFormula,indent+1,path,spntrl,msc,explain,tracepath);

        } else {

          if (Bdd_isEqv(dgn.D,bdd_termFalse)) {
            deadlockedInvalid(dgn,item->num,item->state1,NULL,explain,tracepath);
          } else {
            pathNone(dgn,item->num,explain,tracepath);
          }

          if (explain) printf("\n");
        }

        break;

      case MC_EEW:
      case MC_EEW_NS:

        if (item->r) {

          if (!Bdd_isEqv(dgn.D,bdd_termFalse)) {
            pathValid(dgn,item->num,item->state1,item->state2,explain,tracepath);
          } else {

            if (Bdd_isEqv(item->lastaction,bdd_termFalse)) {
              deadlockedValid(dgn,item->num,item->state1,item->nextPrefix,
                              explain,tracepath);
            } else {
              deadlockedValid(dgn,item->num,item->state1,NULL,explain,tracepath);
            }

          }

          if (item->path) {
            createPath(dgn,item->path->nextFunction,path,spntrl,msc,explain,tracepath);
          }
          if (explain) printf("\n");

          if ((item->nextPrefix) && (item->nextPrefix->ready))
            McPrintDiagnostic(dgn,item->nextPrefix,indent+1,path,spntrl,msc,explain,tracepath);

          if ((item->nextFormula) && (item->nextFormula->ready))
            McPrintDiagnostic(dgn,item->nextFormula,indent+1,path,spntrl,msc,explain,tracepath);

        } else {
          pathNone(dgn,item->num,explain,tracepath);
          if (explain) printf("\n");
        }

        break;

      case MC_AAU:
      case MC_AAU_NS:

        if (!(item->r)) {

          if (Bdd_isEqv(dgn.D,bdd_termFalse)) {
            deadlockedInvalid(dgn,item->num,item->state1,NULL,explain,tracepath);
          } else {
            if (Bdd_isEqv(item->lastaction,bdd_termFalse)) {
              stateInvalid(dgn,item->num,item->state1,
                           item->nextPrefix,explain,tracepath);
            } else {
              pathInvalid(dgn,item->num,item->state1,item->state2,explain,tracepath);
            }
          }

          if (item->path) {
            createPath(dgn,item->path->nextFunction,path,spntrl,msc,explain,tracepath);
          }
          if (explain) printf("\n");

          if ((item->nextPrefix) && (item->nextPrefix->ready))
            McPrintDiagnostic(dgn,item->nextPrefix,indent+1,path,spntrl,msc,explain,tracepath);

          if ((item->nextFormula) && (item->nextFormula->ready))
            McPrintDiagnostic(dgn,item->nextFormula,indent+1,path,spntrl,msc,explain,tracepath);

        } else {
          pathAll(dgn,item->num,explain,tracepath);
          if (explain) printf("\n");
        }

        break;

      case MC_AAW:
      case MC_AAW_NS:

        if (!(item->r)) {

          if (Bdd_isEqv(item->lastaction,bdd_termTrue)) {
            if (Bdd_isEqv(dgn.D,bdd_termFalse)) {
              deadlockedInvalid(dgn,item->num,item->state1,
                           item->nextPrefix,explain,tracepath);
            } else {
              stateInvalid(dgn,item->num,item->state1,
                           item->nextPrefix,explain,tracepath);
            }
          } else {
            pathInvalid(dgn,item->num,item->state1,item->state2,explain,tracepath);
          }

          if (item->path) {
            createPath(dgn,item->path->nextFunction,path,spntrl,msc,explain,tracepath);
          }
          if (explain) printf("\n");

          if ((item->nextPrefix) && (item->nextPrefix->ready))
            McPrintDiagnostic(dgn,item->nextPrefix,indent+1,path,spntrl,msc,explain,tracepath);

          if ((item->nextFormula) && (item->nextFormula->ready))
            McPrintDiagnostic(dgn,item->nextFormula,indent+1,path,spntrl,msc,explain,tracepath);

        } else {
          if (Bdd_isEqv(dgn.D,bdd_termFalse)) {

            deadlockedValid(dgn,item->num,item->state1,item->nextPrefix,
                            explain,tracepath);

          } else {
            pathAll(dgn,item->num,explain,tracepath);
          }
          if (explain) printf("\n");

          if ((item->nextPrefix) && (item->nextPrefix->ready))
            McPrintDiagnostic(dgn,item->nextPrefix,indent+1,path,spntrl,msc,explain,tracepath);
        }

        break;

      case MC_EEX:
      case MC_EX:

        if (item->r) {

          if (Bdd_isEqv(dgn.D,bdd_termFalse)) {

            deadlockedValid(dgn,item->num,item->state1,item->nextFormula,
                            explain,tracepath);

          } else {
            transitionValid(dgn,item->num,item->state1,item->state2,explain,tracepath);
          }

          if (item->path) {
            createPath(dgn,item->path->nextFunction,path,spntrl,msc,explain,explain);
          }
          if (explain) printf("\n");

          if ((item->nextFormula) && (item->nextFormula->ready))
            McPrintDiagnostic(dgn,item->nextFormula,indent+1,path,spntrl,msc,explain,tracepath);

        } else {

          if (Bdd_isEqv(dgn.D,bdd_termFalse)) {

            deadlockedInvalid(dgn,item->num,item->state1,item->nextFormula,
                              explain,tracepath);

          } else {
            transitionNone(dgn,item->num,explain,tracepath);
          }

          if (explain) printf("\n");

          if ((item->nextFormula) && (item->nextFormula->ready))
            McPrintDiagnostic(dgn,item->nextFormula,indent+1,path,spntrl,msc,explain,tracepath);
        }

        break;

      case MC_AAX:
      case MC_AX:

        if (!(item->r)) {

          if (Bdd_isEqv(dgn.D,bdd_termFalse)) {
            deadlockedInvalid(dgn,item->num,item->state1,item->nextFormula,explain,tracepath);
          } else {
            transitionInvalid(dgn,item->num,item->state1,item->state2,explain,tracepath);
          }

          if (item->path) {
            createPath(dgn,item->path->nextFunction,path,spntrl,msc,explain,explain);
          }
          if (explain) printf("\n");

          if ((item->nextFormula) && (item->nextFormula->ready))
            McPrintDiagnostic(dgn,item->nextFormula,indent+1,path,spntrl,msc,explain,tracepath);

        } else {

          if (Bdd_isEqv(dgn.D,bdd_termFalse)) {

            deadlockedValid(dgn,item->num,item->state1,item->nextFormula,
                            explain,tracepath);

          } else {
            transitionAll(dgn,item->num,explain,tracepath);
          }
          if (explain) printf("\n");

          if ((item->nextFormula) && (item->nextFormula->ready))
            McPrintDiagnostic(dgn,item->nextFormula,indent+1,path,spntrl,msc,explain,tracepath);
        }

        break;

      case MC_EEF:
      case MC_EF:

        if (item->r) {

          if (Bdd_isEqv(dgn.D,bdd_termFalse)) {
            deadlockedValid(dgn,item->num,item->state1,item->nextFormula,
                            explain,tracepath);
          } else {
            pathValid(dgn,item->num,item->state1,item->state2,explain,tracepath);
          }

          if (item->path) {
            createPath(dgn,item->path->nextFunction,path,spntrl,msc,explain,tracepath);
          }
          if (explain) printf("\n");

          if ((item->nextFormula) && (item->nextFormula->ready))
            McPrintDiagnostic(dgn,item->nextFormula,indent+1,path,spntrl,msc,explain,tracepath);

        } else {
          if (Bdd_isEqv(dgn.D,bdd_termFalse)) {

            deadlockedInvalid(dgn,item->num,item->state1,item->nextFormula,
                              explain,tracepath);

          } else {
            pathNone(dgn,item->num,explain,tracepath);
          }
          if (explain) printf("\n");

          if ((item->nextFormula) && (item->nextFormula->ready))
            McPrintDiagnostic(dgn,item->nextFormula,indent+1,path,spntrl,msc,explain,tracepath);
        }

        break;

      case MC_EEG:
      case MC_EEG_NS:
      case MC_EG:

        if (item->r) {

          if (Bdd_isEqv(dgn.D,bdd_termFalse)) {

            deadlockedValid(dgn,item->num,item->state2,item->nextPrefix,
                            explain,tracepath);

          } else {
            pathValid(dgn,item->num,item->state1,item->state2,explain,tracepath);
          }

          if (item->path) {
            createPath(dgn,item->path->nextFunction,path,spntrl,msc,explain,tracepath);
          }
          if (explain) printf("\n");

          if ((item->nextPrefix) && (item->nextPrefix->ready))
            McPrintDiagnostic(dgn,item->nextPrefix,indent+1,path,spntrl,msc,explain,tracepath);

        } else {

          if (Bdd_isEqv(dgn.D,bdd_termFalse)) {
            deadlockedInvalid(dgn,item->num,item->state1,item->nextPrefix,explain,tracepath);
          } else {
            pathNone(dgn,item->num,explain,tracepath);
          }
          if (explain) printf("\n");

          if ((item->nextPrefix) && (item->nextPrefix->ready))
            McPrintDiagnostic(dgn,item->nextPrefix,indent+1,path,spntrl,msc,explain,tracepath);
        }

        break;

      case MC_AAF:
      case MC_AF:

        if (!(item->r)) {

          if (Bdd_isEqv(dgn.D,bdd_termFalse)) {

             deadlockedInvalid(dgn,item->num,item->state1,item->nextFormula,
                               explain,tracepath);

          } else {
            pathInvalid(dgn,item->num,item->state1,item->state2,explain,tracepath);
          }

          if (item->path) {
            createPath(dgn,item->path->nextFunction,path,spntrl,msc,explain,tracepath);
          }
          if (explain) printf("\n");

          if ((item->nextFormula) && (item->nextFormula->ready))
            McPrintDiagnostic(dgn,item->nextFormula,indent+1,path,spntrl,msc,explain,tracepath);

        } else {

          if (Bdd_isEqv(item->lastaction,bdd_termFalse)) {
            stateValid(dgn,item->num,item->state1,item->nextFormula,
                       explain,tracepath);
          } else {
            pathAll(dgn,item->num,explain,tracepath);
          }

          if (explain) printf("\n");

          if ((item->nextFormula) && (item->nextFormula->ready))
            McPrintDiagnostic(dgn,item->nextFormula,indent+1,path,spntrl,msc,explain,tracepath);
        }

        break;

      case MC_AAG:
      case MC_AAG_NS:
      case MC_AG:

        if (!(item->r)) {

          if (Bdd_isEqv(item->lastaction,bdd_termFalse)) {

            if (Bdd_isEqv(dgn.D,bdd_termFalse)) {

              deadlockedInvalid(dgn,item->num,item->state1,item->nextPrefix,
                               explain,tracepath);

            } else {
              stateInvalid(dgn,item->num,item->state1,item->nextPrefix,
                           explain,tracepath);
            }

          } else {
            pathInvalid(dgn,item->num,item->state1,item->state2,explain,tracepath);
          }

          if (item->path) {
            createPath(dgn,item->path->nextFunction,path,spntrl,msc,explain,tracepath);
          }
          if (explain) printf("\n");

          if ((item->nextPrefix) && (item->nextPrefix->ready))
            McPrintDiagnostic(dgn,item->nextPrefix,indent+1,path,spntrl,msc,explain,tracepath);

        } else {
          if (Bdd_isEqv(dgn.D,bdd_termFalse)) {

            deadlockedValid(dgn,item->num,item->state1,item->nextPrefix,
                            explain,tracepath);

          } else {
            pathAll(dgn,item->num,explain,tracepath);
          }
          if (explain) printf("\n");

          if ((item->nextPrefix) && (item->nextPrefix->ready))
            McPrintDiagnostic(dgn,item->nextPrefix,indent+1,path,spntrl,msc,explain,tracepath);
        }

        break;

      case MC_EU:

        if (item->r) {

          if (Bdd_isNull(item->act2)) {

            if (Bdd_isEqv(dgn.D,bdd_termFalse)) {
              deadlockedValid(dgn,item->num,item->state1,item->nextFormula,
                              explain,tracepath);
            } else {
              if (Bdd_isEqv(item->lastaction,bdd_termFalse)) {
                stateValid(dgn,item->num,item->state1,item->nextFormula,
                           explain,tracepath);
              } else {
                pathValid(dgn,item->num,item->state1,item->state2,explain,tracepath);
              }
            }

          } else {
            pathValid(dgn,item->num,item->state1,item->state2,explain,tracepath);
          }

          if (item->path) {
            createPath(dgn,item->path->nextFunction,path,spntrl,msc,explain,tracepath);
          }
          if (explain) printf("\n");

          if ((item->nextFormula) && (item->nextFormula->ready))
            McPrintDiagnostic(dgn,item->nextFormula,indent+1,path,spntrl,msc,explain,tracepath);

        } else {
          if (Bdd_isEqv(dgn.D,bdd_termFalse)) {
            deadlockedInvalid(dgn,item->num,item->state1,item->nextFormula,explain,tracepath);
          } else {
            pathNone(dgn,item->num,explain,tracepath);
          }
          if (explain) printf("\n");
        }

        break;

      case MC_AU:

        if (!(item->r)) {

          if (Bdd_isEqv(dgn.D,bdd_termFalse)) {
            deadlockedInvalid(dgn,item->num,item->state1,item->nextFormula,explain,tracepath);
          } else {
            if (Bdd_isEqv(item->lastaction,bdd_termFalse)) {
              stateInvalid2(dgn,item->num,item->state1,item->nextPrefix->num,
                            item->nextFormula->num,explain,tracepath);
            } else {
              pathInvalid(dgn,item->num,item->state1,item->state2,explain,tracepath);
            }
          }

          if (item->path) {
            createPath(dgn,item->path->nextFunction,path,spntrl,msc,explain,tracepath);
          }
          if (explain) printf("\n");

          if ((item->nextPrefix) && (item->nextPrefix->ready))
            McPrintDiagnostic(dgn,item->nextPrefix,indent+1,path,spntrl,msc,explain,tracepath);

          if ((item->nextFormula) && (item->nextFormula->ready))
            McPrintDiagnostic(dgn,item->nextFormula,indent+1,path,spntrl,msc,explain,tracepath);

        } else {

          if (Bdd_isEqv(dgn.D,bdd_termFalse)) {
            deadlockedValid(dgn,item->num,item->state1,item->nextFormula,
                            explain,tracepath);
          } else {
            if (Bdd_isEqv(item->lastaction,bdd_termFalse)) {
              stateValid(dgn,item->num,item->state1,item->nextFormula,
                         explain,tracepath);
            } else {
              pathAll(dgn,item->num,explain,tracepath);
            }
          }
          if (explain) printf("\n");

          if ((item->nextFormula) && (item->nextFormula->ready))
            McPrintDiagnostic(dgn,item->nextFormula,indent+1,path,spntrl,msc,explain,tracepath);
        }

        break;

      case MC_HME:

        if (item->r) {

          if (Bdd_isNull(item->form1) && !Bdd_isNull(item->act2)) {

            /* CAREFULLY!! */
            /* WE PREFER TO USE STRONG HME, WHERE APPROPRIATE */
            transitionValid(dgn,item->num,item->state1,item->state2,explain,tracepath);

            /* IF USING ORIGINAL DEFINITION FROM DeNicola, Vaandrager, 1990 */
            /*
            pathValid(dgn,item->num,item->state1,item->state2,explain,tracepath);
            */

          } else {

            if (Bdd_isNull(item->act2)) {

              if (Bdd_isEqv(dgn.D,bdd_termFalse)) {
                deadlockedValid(dgn,item->num,item->state1,item->nextFormula,
                                explain,tracepath);
              } else {
                if (Bdd_isEqv(item->lastaction,bdd_termFalse)) {
                  stateValid(dgn,item->num,item->state1,item->nextFormula,
                             explain,tracepath);
                } else {
                  pathValid(dgn,item->num,item->state1,item->state2,explain,tracepath);
                }
              }

            } else {
              pathValid(dgn,item->num,item->state1,item->state2,explain,tracepath);
            }

          }

          if (item->path) {
            createPath(dgn,item->path->nextFunction,path,spntrl,msc,explain,tracepath);
          }
          if (explain) printf("\n");

          if ((item->nextFormula) && (item->nextFormula->ready))
            McPrintDiagnostic(dgn,item->nextFormula,indent+1,path,spntrl,msc,explain,tracepath);

        } else {

          if (Bdd_isEqv(dgn.D,bdd_termFalse)) {

            if (Bdd_isNull(item->form1) && !Bdd_isNull(item->act2)) {

              /* CAREFULLY!! */
              /* WE PREFER TO USE STRONG HME, WHERE APPROPRIATE */
              deadlockedInvalid(dgn,item->num,item->state1,NULL,explain,tracepath);

              /* IF USING ORIGINAL DEFINITION FROM DeNicola, Vaandrager, 1990 */
              /*
              deadlockedInvalid(dgn,item->num,item->state1,item->nextFormula,explain,tracepath);
              */

            } else {
              deadlockedInvalid(dgn,item->num,item->state1,item->nextFormula,explain,tracepath);
            }

          } else {

            if (Bdd_isNull(item->form1) && !Bdd_isNull(item->act2)) {

              /* CAREFULLY!! */
              /* WE PREFER TO USE STRONG HME, WHERE APPROPRIATE */
              transitionNone(dgn,item->num,explain,tracepath);

              /* IF USING ORIGINAL DEFINITION FROM DeNicola, Vaandrager, 1990 */
              /*
              pathNone(dgn,item->num,explain,tracepath);
              */

            } else {
              pathNone(dgn,item->num,explain,tracepath);
            }

          }
          if (explain) printf("\n");
        }

        break;

      case MC_HMA:

        if (!(item->r)) {

          if (!Bdd_isNull(item->act2)) {

            /* CAREFULLY!! */
            /* WE PREFER TO USE STRONG HMA, WHERE APPROPRIATE */
            transitionInvalid(dgn,item->num,item->state1,item->state2,explain,tracepath);

            /* IF USING ORIGINAL DEFINITION FROM DeNicola, Vaandrager, 1990 */
            /*
            if (Bdd_isEqv(item->lastaction,bdd_termFalse)) {
              stateInvalid(dgn,item->num,item->state1,NULL,explain,tracepath);
            } else {
              pathInvalid(dgn,item->num,item->state1,item->state2,explain,tracepath);
            }
            */

          } else {

            if (Bdd_isEqv(item->lastaction,bdd_termFalse)) {
              stateInvalid(dgn,item->num,item->state1,NULL,explain,tracepath);
            } else {
              pathInvalid(dgn,item->num,item->state1,item->state2,explain,tracepath);
            }

          }

          if (item->path) {
            createPath(dgn,item->path->nextFunction,path,spntrl,msc,explain,explain);
          }
          if (explain) printf("\n");

          if ((item->nextFormula) && (item->nextFormula->ready))
            McPrintDiagnostic(dgn,item->nextFormula,indent+1,path,spntrl,msc,explain,tracepath);

        } else {

          if (Bdd_isEqv(dgn.D,bdd_termFalse)) {
            deadlockedValid(dgn,item->num,item->state1,NULL,explain,tracepath);
          } else {

            if (!Bdd_isNull(item->act2)) {

              /* CAREFULLY!! */
              /* WE PREFER TO USE STRONG HME, WHERE APPROPRIATE */
              transitionAll(dgn,item->num,explain,tracepath);

              /* IF USING ORIGINAL DEFINITION FROM DeNicola, Vaandrager, 1990 */
              /*
              pathAll(dgn,item->num,explain,tracepath);
              */

            } else {
              pathAll(dgn,item->num,explain,tracepath);
            }

          }
          if (explain) printf("\n");
        }

        break;

      case MC_NOT:

        if (explain) {
          if (item->r) {
            printf("@@ Formula #%d is valid in state ",item->num);
            if (dgn.proc != -1) Pa_DecodeProcessStates(&pa_processTable[dgn.proc],item->state1,TRUE);
            if (dgn.comp != -1) Pa_DecodeCompStates(&pa_compositionTable[dgn.comp],item->state1,TRUE);
            printf(" because formula #%d is not valid in it.\n",
                   (item->nextFormula)->num);
          } else {
            printf("@@ Formula #%d is not valid in state ",item->num);
            if (dgn.proc != -1) Pa_DecodeProcessStates(&pa_processTable[dgn.proc],item->state1,TRUE);
            if (dgn.comp != -1) Pa_DecodeCompStates(&pa_compositionTable[dgn.comp],item->state1,TRUE);
            printf(" because formula #%d is valid in it.\n",
                   (item->nextFormula)->num);
          }
        }

        if ((item->nextFormula) && (item->nextFormula->ready))
          McPrintDiagnostic(dgn,item->nextFormula,indent+1,path,spntrl,msc,explain,tracepath);

        break;

      case MC_AND:
      case MC_OR:
      case MC_EQV:
      case MC_IMPL:

        if (explain) {
          if (item->r) {
            printf("@@ Formula #%d is valid in state ",item->num);
          } else {
            printf("@@ Formula #%d is not valid in state ",item->num);
          }

          if (dgn.proc != -1) Pa_DecodeProcessStates(&pa_processTable[dgn.proc],item->state1,TRUE);
          if (dgn.comp != -1) Pa_DecodeCompStates(&pa_compositionTable[dgn.comp],item->state1,TRUE);
          printf(" because:\n");
          printf("@@ 1. formula #%d ",(item->nextPrefix)->num);
          if ((item->nextPrefix)->r) {
            printf("is valid in it,\n");
          } else {
            printf("is not valid in it,\n");
          }
          printf("@@ 2. formula #%d ",(item->nextFormula)->num);
          if ((item->nextFormula)->r) {
            printf("is valid in it");
          } else {
            printf("is not valid in it");
          }
        }

        if (explain) printf(".\n");

        /* NEW IMPLEMENTATION */
        /**/
        if (item->type == MC_AND) {
          if ((item->nextPrefix)->r && (item->nextFormula)->r) {
            if (explain) printf("WARNING (operator AND): Cannot explain both part at once.\n");
          }
          else if (!(item->nextPrefix)->r && !(item->nextFormula)->r) {
            if (explain) printf("WARNING (operator AND): Cannot explain both part at once.\n");
          }
          else if (!(item->nextPrefix)->r) {
            if ((item->nextPrefix) && (item->nextPrefix->ready))
              McPrintDiagnostic(dgn,item->nextPrefix,indent+1,path,spntrl,msc,explain,tracepath);
          }
          else if (!(item->nextFormula)->r) {
            if ((item->nextFormula) && (item->nextFormula->ready))
              McPrintDiagnostic(dgn,item->nextFormula,indent+1,path,spntrl,msc,explain,tracepath);
          }
        }

        if (item->type == MC_OR) {
          if ((item->nextPrefix)->r && (item->nextFormula)->r) {
            if (explain) printf("WARNING (operator OR): Cannot explain both part at once.\n");
          }
          else if (!(item->nextPrefix)->r && !(item->nextFormula)->r) {
            if (explain) printf("WARNING (operator OR): Cannot explain both part at once.\n");
          }
          else if ((item->nextPrefix)->r) {
            if ((item->nextPrefix) && (item->nextPrefix->ready))
              McPrintDiagnostic(dgn,item->nextPrefix,indent+1,path,spntrl,msc,explain,tracepath);
          }
          else if ((item->nextFormula)->r) {
            if ((item->nextFormula) && (item->nextFormula->ready))
              McPrintDiagnostic(dgn,item->nextFormula,indent+1,path,spntrl,msc,explain,tracepath);
          }
        }

        if (item->type == MC_EQV) {
          if (explain) printf("WARNING (operator EQV): Cannot explain both part at once.\n");
        }


        if (item->type == MC_IMPL) {
          if (!(item->nextPrefix)->r) {
            if (explain) printf("WARNING (operator IMPL): Explaining first part, only.\n");
            if ((item->nextPrefix) && (item->nextPrefix->ready))
              McPrintDiagnostic(dgn,item->nextPrefix,indent+1,path,spntrl,msc,explain,tracepath);
          }
          else if ((item->nextPrefix)->r && !(item->nextFormula)->r) {
            if (explain) printf("WARNING (operator IMPL): Explaining second part, only.\n");
          }
          else if ((item->nextPrefix)->r && (item->nextFormula)->r) {
            if (explain) printf("WARNING (operator IMPL): Cannot explain both part at once.\n");
          }
        }
        /**/

        /* OLD IMPLEMENTATION */
        /*
        concat(path,"[");

        if ((item->nextPrefix) && (item->nextPrefix->ready))
          McPrintDiagnostic(dgn,item->nextPrefix,indent+1,path,spntrl,msc,explain,tracepath);

        if (item->type == MC_AND) concat(path,",AND,");
        if (item->type == MC_OR) concat(path,",OR,");
        if (item->type == MC_EQV) concat(path,",EQV,");
        if (item->type == MC_IMPL) concat(path,",IMPL,");

        if ((item->nextFormula) && (item->nextFormula->ready))
          McPrintDiagnostic(dgn,item->nextFormula,indent+1,path,spntrl,msc,explain,tracepath);

        concat(path,"]");
        */

        break;

    }
  }
}

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

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

static Est_Boolean
DiagnosticEEU(McDiagnosticType dgn, Bdd_Edge D, McDiagnosticItem *item,
              Est_Boolean strict)
{
  Bdd_Edge s1,s2,a1,a2,Xn,state2;
  Bdd_Edge sup,last,Z;
  McFunctionSequence *seq,*seq1;
  Est_Boolean r;

  a1 = item->act1;
  s1 = item->form1;
  a2 = item->act2;
  s2 = item->form2;

  seq = (McFunctionSequence *) malloc(sizeof(McFunctionSequence));
  seq->f = bdd_termNull;
  seq->nextFunction = NULL;
  seq->prevFunction = NULL;

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

    r = FALSE;
    item->lastaction = bdd_termNull;
    item->state2 = bdd_termNull;
    McDeleteFunctionSequence(seq);
    return r;

  }

  /*
  printf("Starting limited fixpoint calculation of EEU ...\n");
  */

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

  seq->f = Z;
  Xn = Bdd_ITE(item->state1,Z,bdd_termFalse);

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

    last = Z;
    if (!Bdd_isEqv(a1,bdd_termFalse)) {
      sup = Bdd_ITE(s1,a1,bdd_termFalse);
      sup = Bdd_RelOp(sup,Z,"#AND R2S",TRUE);
      sup = Bdd_RelOp(sup,D,"#AND Ex xA xS",TRUE);  /* ... -a1-> (s1*Z) */
      Z = Bdd_ITE(Z,bdd_termTrue,sup);                   /* Z = Z + sup */
      Bdd_Fortify(Z);
    }

    seq1 = (McFunctionSequence *) malloc(sizeof(McFunctionSequence));
    seq1->f = Z;
    seq1->nextFunction = seq;
    seq1->prevFunction = NULL; /* NOT IMPORTANT */
    seq->prevFunction = seq1;
    seq = seq1;

    Xn = Bdd_ITE(item->state1,Z,bdd_termFalse);
  }

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

  if (Bdd_isEqv(Xn,bdd_termFalse)) {

    r = FALSE;
    item->lastaction = bdd_termNull;
    item->state2 = bdd_termNull;
    McDeleteFunctionSequence(seq);

  } else {

    /* FORMULA IS VALID IN INIT STATE */

    r = TRUE;

    /* EXTRACT PATH */

    item->path = seq;
    item->lastaction = bdd_termFalse;
    state2 = item->state1;
    seq->f = item->state1;

    if (seq->nextFunction) {

      /* THE PATH IS NOT FINISHED IN THE FIRST STATE */

      seq = seq->nextFunction;
      while (seq->nextFunction) {

        sup = Bdd_ITE(seq->nextFunction->f,bdd_termFalse,seq->f); /* exclude */
        sup = Bdd_RelOpSimple(sup,"R2S",TRUE);
        sup = Bdd_ITE(sup,state2,bdd_termFalse);
        sup = Bdd_ITE(sup,a1,bdd_termFalse);
        sup = Bdd_ITE(sup,D,bdd_termFalse); /* sup = appropriate transitions */

        if (dgn.proc != -1) {
          sup = Pa_ExtractProcTransition(&pa_processTable[dgn.proc],sup);
        }
        if (dgn.comp != -1) {
          sup = Pa_ExtractCompTransition(&pa_compositionTable[dgn.comp],sup);
        }

        sup = Bdd_RelOpSimple(sup,"Ex xR S2R",TRUE);
        Bdd_Fortify(sup);

        seq->f = sup;
        seq = seq->nextFunction;

        state2 = Bdd_RelOpSimple(sup,"Ex xA",TRUE);
        Bdd_Fortify(state2);
      }

      /* THE LAST TRANSITION WHERE THE CONDITION IS VALID */

      sup = Bdd_RelOpSimple(seq->f,"R2S",TRUE);
      sup = Bdd_ITE(sup,state2,bdd_termFalse);
      sup = Bdd_ITE(sup,a1,bdd_termFalse);
      sup = Bdd_ITE(sup,D,bdd_termFalse);

      if (dgn.proc != -1) {
        sup = Pa_ExtractProcTransition(&pa_processTable[dgn.proc],sup);
      }
      if (dgn.comp != -1) {
        sup = Pa_ExtractCompTransition(&pa_compositionTable[dgn.comp],sup);
      }

      sup = Bdd_RelOpSimple(sup,"Ex xR S2R",TRUE);
      Bdd_Fortify(sup);

      seq->f = sup;
      state2 = Bdd_RelOpSimple(sup,"Ex xA",TRUE);
      Bdd_Fortify(state2);

    }

    /* A TRANSITION WHERE THE LAST CONDITION IS VALID */

    sup = Bdd_RelOpSimple(s2,"R2S",TRUE);
    sup = Bdd_ITE(sup,a2,bdd_termFalse);
    sup = Bdd_ITE(sup,state2,bdd_termFalse);
    sup = Bdd_ITE(sup,D,bdd_termFalse);

    if (dgn.proc != -1) {
      sup = Pa_ExtractProcTransition(&pa_processTable[dgn.proc],sup);
    }
    if (dgn.comp != -1) {
      sup = Pa_ExtractCompTransition(&pa_compositionTable[dgn.comp],sup);
    }

    sup = Bdd_RelOpSimple(sup,"Ex xR S2R",TRUE);
    Bdd_Fortify(sup);

    seq1 = (McFunctionSequence *) malloc(sizeof(McFunctionSequence));
    seq1->f = sup;
    seq1->nextFunction = NULL;
    seq1->prevFunction = seq;
    seq->nextFunction = seq1;

    state2 = Bdd_RelOpSimple(sup,"Ex xA",TRUE);
    Bdd_Fortify(state2);

    item->state2 = state2;

    item->lastaction = Bdd_RelOpSimple(sup,"Ex xR",TRUE);
    Bdd_Fortify(item->lastaction);
  }

  return r;
}

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

static Est_Boolean
DiagnosticEEW(McDiagnosticType dgn, Bdd_Edge D, McDiagnosticItem *item,
              Est_Boolean strict)
{
  Est_Boolean r;

  if (DiagnosticEEU(dgn,D,item,strict)) {
    r = 1;
  } else {
    if (item->path) McDeleteFunctionSequence(item->path);
    item->state2 = bdd_termNull;
    item->lastaction = bdd_termTrue;
    item->path = NULL;
    if (DiagnosticEEG(dgn,D,item,strict)) {
      if (Bdd_isEqv(D,bdd_termFalse) && !strict) {
        r = 2;
      } else {
        r = 3;
      }
    } else {
      if (item->path) McDeleteFunctionSequence(item->path);
      item->state2 = bdd_termNull;
      item->lastaction = bdd_termTrue;
      item->path = NULL;
      r = 0;
    }
  }

  return r;
}

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

static Est_Boolean
DiagnosticEEX(McDiagnosticType dgn, Bdd_Edge D, McDiagnosticItem *item)
{
  Est_Boolean r;
  Bdd_Edge a1org,s1org;

  a1org = item->act1;
  s1org = item->form1;

  item->act1 = bdd_termFalse;
  item->form1 = bdd_termFalse;
  r = DiagnosticEEU(dgn,D,item,TRUE);

  item->act1 = a1org;
  item->form1 = s1org;
  return r;
}

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

static Est_Boolean
DiagnosticEEF(McDiagnosticType dgn, Bdd_Edge D, McDiagnosticItem *item)
{
  Est_Boolean r;
  Bdd_Edge a1org,s1org;

  a1org = item->act1;
  s1org = item->form1;

  item->act1 = bdd_termTrue;
  item->form1 = bdd_termTrue;
  r = DiagnosticEEU(dgn,D,item,TRUE);

  item->act1 = a1org;
  item->form1 = s1org;
  return r;
}

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

static Est_Boolean
DiagnosticEEG(McDiagnosticType dgn, Bdd_Edge D, McDiagnosticItem *item,
              Est_Boolean strict)
{
  Bdd_Edge sup,sup1,sup2,sd,last,Z;
  McFunctionSequence *seq, *seq1, *seq0;
  Bdd_Edge s,a,C,Yn,state2;
  Est_Boolean r,OK;

  a = item->act1;
  s = item->form1;

  seq = (McFunctionSequence *) malloc(sizeof(McFunctionSequence));
  seq->f = bdd_termNull;
  seq->nextFunction = NULL;
  seq->prevFunction = NULL;

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

    /* STRICT */
    if (strict) {

      r = TRUE;
      seq->f = item->state1;
      item->path = seq;
      item->lastaction = bdd_termNull;
      item->state2 = item->state1;
      return r;

    }

    /* NON-STRICT */
    if (!strict && (!Bdd_isEqv(Bdd_ITE(item->state1,s,bdd_termFalse),bdd_termFalse))) {

      r = TRUE;
      seq->f = item->state1;
      item->path = seq;
      item->lastaction = bdd_termFalse;
      item->state2 = item->state1;
      return r;

    }
  }

  /* init = NOT s1 AND NON-STRICT */
  if (!strict && (Bdd_isEqv(Bdd_ITE(item->state1,s,bdd_termFalse),bdd_termFalse))) {

    r = FALSE;
    item->lastaction = bdd_termNull;
    item->state2 = bdd_termNull;
    McDeleteFunctionSequence(seq);
    return r;

  }

  /*
  printf("Starting fixpoint calculation of EEG ...\n");
  */

  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-> (s1*Z) */
    Z = Bdd_ITE(Z,bdd_termTrue,sd);           /* add deadlocked states */
  }

  /* Z is set of states where EEG is valid */

  C = Z;
  Bdd_Fortify(C);

  state2 = Bdd_ITE(C,item->state1,bdd_termFalse); /* if valid in state1 */
  if (Bdd_isEqv(state2,bdd_termFalse)) {

    r = FALSE;
    item->lastaction = bdd_termNull;
    item->state2 = bdd_termNull;
    McDeleteFunctionSequence(seq);

  } else {

    /* FORMULA IS VALID IN INIT STATE */

    r = TRUE;

    item->path = seq;                /* here is the beginning of witness */
    seq->f = state2;

    OK = FALSE;
    while (!OK) {

      /* LOOKING FOR CYCLE */

      seq0 = seq;

      sup = Bdd_ITE(a,state2,bdd_termFalse);
      sup = Bdd_RelOp(D,sup,"#AND Ex xA xR S2R",TRUE);
      sup = Bdd_ITE(C,sup,bdd_termFalse);                 /* successors */

      Z = sup;
      Bdd_Fortify(Z);

      seq1 = (McFunctionSequence *) malloc(sizeof(McFunctionSequence));
      seq1->f = Z;
      seq1->nextFunction = NULL;
      seq1->prevFunction = NULL; /* NULL IS IMPORTANT HERE */
      seq->nextFunction = seq1;
      seq = seq1;

      Yn = Bdd_ITE(state2,Z,bdd_termFalse);

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

        last = Z;
        sup = Bdd_ITE(a,Z,bdd_termFalse);
        sup = Bdd_RelOp(D,sup,"#AND Ex xA xR S2R",TRUE);
        sup = Bdd_ITE(C,sup,bdd_termFalse);        /* sup = Z -a-> ... */

        Z = Bdd_ITE(Z,bdd_termTrue,sup);                /* Z = Z + sup */
        Bdd_Fortify(Z);

        seq1 = (McFunctionSequence *) malloc(sizeof(McFunctionSequence));
        seq1->f = Z;
        seq1->nextFunction = NULL;
        seq1->prevFunction = seq;
        seq->nextFunction = seq1;
        seq = seq1;

        Yn = Bdd_ITE(state2,Z,bdd_termFalse);
      }

      if (Bdd_isEqv(Yn,bdd_termFalse)) {

        /* DELETE NODES, BECAUSE THERE IS NO CYCLE */

        McDeleteFunctionSequence(seq0->nextFunction);

        seq = seq0;
        seq->nextFunction = NULL;

        /* GO TO THE NEXT NODE WHICH CAN BE START OF CYCLE */

        sup = Bdd_RelOpSimple(C,"R2S",TRUE);
        sup = Bdd_ITE(sup,a,bdd_termFalse);
        sup = Bdd_ITE(sup,state2,bdd_termFalse);
        sup = Bdd_ITE(sup,D,bdd_termFalse);

        if (Bdd_isEqv(sup,bdd_termFalse)) {

          /* DEADLOCKED STATE IS REACHED */

          OK = TRUE;
          item->state2 = state2;

  } else {

          if (dgn.proc != -1) {
            sup = Pa_ExtractProcTransition(&pa_processTable[dgn.proc],sup);
          }
          if (dgn.comp != -1) {
            sup = Pa_ExtractCompTransition(&pa_compositionTable[dgn.comp],sup);
          }

          sup = Bdd_RelOpSimple(sup,"Ex xR S2R",TRUE);
          Bdd_Fortify(sup);

          seq1 = (McFunctionSequence *) malloc(sizeof(McFunctionSequence));
          seq1->f = sup;
          seq1->nextFunction = NULL;  /* NOT IMPORTANT */
          seq1->prevFunction = seq;
          seq->nextFunction = seq1;
          seq = seq1;

          state2 = Bdd_RelOpSimple(sup,"Ex xA",TRUE);
          Bdd_Fortify(state2);
  }

      } else {

        OK = TRUE;
        item->state2 = state2;

        /* EXTRACT PATH */
        /* seq = YN */

        if (seq->prevFunction) {

          /* THE PATH IS NOT FINISHED IN THE FIRST STATE */

          seq = seq->prevFunction;
          while (seq->prevFunction) {
            sup = Bdd_ITE(seq->prevFunction->f,bdd_termFalse,seq->f); /* ex */
            sup = Bdd_ITE(sup,a,bdd_termFalse);
            sup1 = Bdd_RelOpSimple(state2,"R2S",TRUE);
            sup = Bdd_ITE(sup,sup1,bdd_termFalse);
            sup = Bdd_ITE(sup,D,bdd_termFalse);

            if (dgn.proc != -1) {
              sup = Pa_ExtractProcTransition(&pa_processTable[dgn.proc],sup);
            }
            if (dgn.comp != -1) {
              sup = Pa_ExtractCompTransition(&pa_compositionTable[dgn.comp],sup);
            }

            state2 = Bdd_RelOpSimple(sup,"Ex xA xS",TRUE);
            Bdd_Fortify(state2);

            sup = Bdd_RelOpSimple(sup,"Ex xR S2R",TRUE);
            Bdd_Fortify(sup);

            seq->nextFunction->f = sup;
            seq = seq->prevFunction;
    }

          /* THE SECOND TRANSITION IN CYCLE */

          sup = Bdd_RelOpSimple(state2,"R2S",TRUE);
          sup = Bdd_ITE(sup,seq->f,bdd_termFalse);           /* AND Y0 */
          sup = Bdd_ITE(sup,a,bdd_termFalse);
          sup = Bdd_ITE(sup,D,bdd_termFalse);

          if (dgn.proc != -1) {
            sup = Pa_ExtractProcTransition(&pa_processTable[dgn.proc],sup);
          }
          if (dgn.comp != -1) {
            sup = Pa_ExtractCompTransition(&pa_compositionTable[dgn.comp],sup);
          }

          state2 = Bdd_RelOpSimple(sup,"Ex xA xS",TRUE);
          Bdd_Fortify(state2);

          sup = Bdd_RelOpSimple(sup,"Ex xR S2R",TRUE);
          Bdd_Fortify(sup);

          seq->nextFunction->f = sup;
  }

        /* THE FIRST TRANSITION IN CYCLE */

        sup = Bdd_RelOpSimple(state2,"R2S",TRUE);
        sup = Bdd_ITE(sup,item->state2,bdd_termFalse);
        sup = Bdd_ITE(sup,a,bdd_termFalse);
        sup = Bdd_ITE(sup,D,bdd_termFalse);

        if (dgn.proc != -1) {
          sup = Pa_ExtractProcTransition(&pa_processTable[dgn.proc],sup);
        }
        if (dgn.comp != -1) {
          sup = Pa_ExtractCompTransition(&pa_compositionTable[dgn.comp],sup);
        }

        sup = Bdd_RelOpSimple(sup,"Ex xR S2R",TRUE);
        Bdd_Fortify(sup);

        seq->f = sup;
      }
    }
  }

  return r;
}

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

static Est_Boolean
DiagnosticAAU(McDiagnosticType dgn, Bdd_Edge D, McDiagnosticItem *item,
              Est_Boolean strict)
{
  Est_Boolean r;

  if (!DiagnosticAAW(dgn,D,item,strict)) {
    r = 1;
  } else {
    if (item->path) McDeleteFunctionSequence(item->path);
    item->lastaction = bdd_termNull;
    item->state2 = bdd_termNull;
    item->path = NULL;
    if (!DiagnosticAAF(dgn,D,item)) {
      r = 2;
    } else {
      if (item->path) McDeleteFunctionSequence(item->path);
      item->lastaction = bdd_termNull;
      item->state2 = bdd_termNull;
      item->path = NULL;
      r = 0;
    }
  }

  return r;
}

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

static Est_Boolean
DiagnosticAAW(McDiagnosticType dgn, Bdd_Edge D, McDiagnosticItem *item,
              Est_Boolean strict)
{
  Bdd_Edge s1,s2,a1,a2,Xn,state2;
  Bdd_Edge sall,D1not,D2not_ras,D2not_sar;
  Bdd_Edge sup,sup1,sup2,last,Z;
  McFunctionSequence *seq,*seq1;
  Est_Boolean r;

  a1 = item->act1;
  s1 = item->form1;
  a2 = item->act2;
  s2 = item->form2;

  seq = (McFunctionSequence *) malloc(sizeof(McFunctionSequence));
  seq->f = bdd_termNull;
  seq->nextFunction = NULL;
  seq->prevFunction = NULL;

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

    /* STRICT */
    if (strict) {

      r = TRUE;
      item->lastaction = bdd_termNull;
      item->state2 = bdd_termNull;
      McDeleteFunctionSequence(seq);
      return r;

    }

    /* NON-STRICT */
    if (!strict && (!Bdd_isEqv(Bdd_ITE(item->state1,s1,bdd_termFalse),bdd_termFalse))) {

      r = TRUE;
      item->lastaction = bdd_termFalse;
      item->state2 = bdd_termNull;
      McDeleteFunctionSequence(seq);
      return r;

    }

  }

  /* init = NOT s1 AND NON-STRICT */
  if (!strict && (Bdd_isEqv(Bdd_ITE(item->state1,s1,bdd_termFalse),bdd_termFalse))) {

    r = FALSE;
    seq->f = item->state1;
    item->path = seq;
    item->lastaction = bdd_termFalse;
    item->state2 = item->state1;
    return r;

  }

  /*
  printf("Starting limited fixpoint calculation of AAW...\n");
  */

  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);

  seq->f = Z;
  Xn = Bdd_ITE(item->state1,Z,bdd_termFalse);

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

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

    seq1 = (McFunctionSequence *) malloc(sizeof(McFunctionSequence));
    seq1->f = Z;
    seq1->nextFunction = seq;
    seq1->prevFunction = NULL; /* NOT IMPORTANT */
    seq->prevFunction = seq1;
    seq = seq1;

    Xn = Bdd_ITE(item->state1,Z,bdd_termFalse);
  }

  /* Z is set of states where AAW is not valid */

  if (Bdd_isEqv(Xn,bdd_termFalse)) {

    r = TRUE;
    item->state2 = bdd_termNull;
    item->lastaction = bdd_termNull;
    McDeleteFunctionSequence(seq);

  } else {

    /* FORMULA IS NOT VALID IN INIT STATE */

    r = FALSE;

    /* EXTRACT PATH */

    item->path = seq;
    state2 = item->state1;
    seq->f = item->state1;

    if (seq->nextFunction) {

      /* THE PATH IS NOT FINISHED IN THE FIRST STATE */

      seq = seq->nextFunction;
      while (seq->nextFunction) {

        sup = Bdd_ITE(seq->nextFunction->f,bdd_termFalse,seq->f); /* exclude */
        sup = Bdd_RelOpSimple(sup,"R2S",TRUE);
        sup = Bdd_ITE(sup,state2,bdd_termFalse);
        sup = Bdd_ITE(sup,D2not_ras,bdd_termFalse);  /* sup = approp. trans. */

        if (dgn.proc != -1) {
          sup = Pa_ExtractProcTransition(&pa_processTable[dgn.proc],sup);
        }
        if (dgn.comp != -1) {
          sup = Pa_ExtractCompTransition(&pa_compositionTable[dgn.comp],sup);
        }

        sup = Bdd_RelOpSimple(sup,"Ex xR S2R",TRUE);
        Bdd_Fortify(sup);

        seq->f = sup;
        seq = seq->nextFunction;

        state2 = Bdd_RelOpSimple(sup,"Ex xA",TRUE);
        Bdd_Fortify(state2);
      }

      /* THE LAST TRANSITION WHERE THE CONDITION IS VALID */

      sup = Bdd_RelOpSimple(seq->f,"R2S",TRUE);
      sup = Bdd_ITE(sup,state2,bdd_termFalse);
      sup = Bdd_ITE(sup,D2not_ras,bdd_termFalse);  /* sup = approp. trans. */

      if (dgn.proc != -1) {
        sup = Pa_ExtractProcTransition(&pa_processTable[dgn.proc],sup);
      }
      if (dgn.comp != -1) {
        sup = Pa_ExtractCompTransition(&pa_compositionTable[dgn.comp],sup);
      }

      sup = Bdd_RelOpSimple(sup,"Ex xR S2R",TRUE);
      Bdd_Fortify(sup);

      seq->f = sup;

      state2 = Bdd_RelOpSimple(sup,"Ex xA",TRUE);
      Bdd_Fortify(state2);

    }

    /* A TRANSITION WHERE THE LAST CONDITION IS VALID */

    sup = Bdd_ITE(D1not,D2not_ras,bdd_termFalse);
    sup = Bdd_ITE(sup,state2,bdd_termFalse);

    if (dgn.proc != -1) {
      sup = Pa_ExtractProcTransition(&pa_processTable[dgn.proc],sup);
    }
    if (dgn.comp != -1) {
      sup = Pa_ExtractCompTransition(&pa_compositionTable[dgn.comp],sup);
    }

    sup = Bdd_RelOpSimple(sup,"Ex xR S2R",TRUE);
    Bdd_Fortify(sup);

    seq1 = (McFunctionSequence *) malloc(sizeof(McFunctionSequence));
    seq1->f = sup;
    seq1->nextFunction = NULL;
    seq1->prevFunction = seq;
    seq->nextFunction = seq1;

    state2 = Bdd_RelOpSimple(sup,"Ex xA",TRUE);
    Bdd_Fortify(state2);

    item->state2 = state2;

    item->lastaction = Bdd_RelOpSimple(sup,"Ex xR",TRUE);
    Bdd_Fortify(item->lastaction);
  }

  return r;
}

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

static Est_Boolean
DiagnosticAAX(McDiagnosticType dgn, Bdd_Edge D, McDiagnosticItem *item)
{
  Est_Boolean r;
  Bdd_Edge a1org,s1org;

  a1org = item->act1;
  s1org = item->form1;

  item->act1 = bdd_termFalse;
  item->form1 = bdd_termFalse;

  r = DiagnosticAAW(dgn,D,item,TRUE);

  item->act1 = a1org;
  item->form1 = s1org;
  return r;
}

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

static Est_Boolean
DiagnosticAAF(McDiagnosticType dgn, Bdd_Edge D, McDiagnosticItem *item)
{
  Bdd_Edge sall,Dnot_ras,Dnot_sar;
  Bdd_Edge sup,sup1,sup2,sd_r,sd_s,last,Z;
  McFunctionSequence *seq, *seq1, *seq0;
  Bdd_Edge s,a,C,Yn,state2;
  Est_Boolean r,OK;

  a = item->act2;
  s = item->form2;

  seq = (McFunctionSequence *) malloc(sizeof(McFunctionSequence));
  seq->f = bdd_termNull;
  seq->nextFunction = NULL;
  seq->prevFunction = NULL;

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

    r = FALSE;
    seq->f = item->state1;
    item->path = seq;
    item->lastaction = bdd_termFalse;
    item->state2 = item->state1;
    return r;

  }

  /*
  printf("Starting fixpoint calculation of AAF ...\n");
  */

  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 DON'T 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 */
  }

  /* Z is set of states where AAF is not valid */

  C = Z;
  Bdd_Fortify(C);

  state2 = Bdd_ITE(C,item->state1,bdd_termFalse); /* if invalid in state1 */
  if (Bdd_isEqv(state2,bdd_termFalse)) {

    r = TRUE;
    item->lastaction = bdd_termNull;
    item->state2 = bdd_termNull;
    McDeleteFunctionSequence(seq);

  } else {

    /* FORMULA IS NOT VALID IN INIT STATE */

    r = FALSE;

    item->path = seq;         /* here is the beginning of counterexample */
    seq->f = state2;

    /* IF THERE ARE NO TRANSITIONS IN THE PROCESS !! */      /* CAREFULLY !!! */
    if (Bdd_isEqv(D,bdd_termFalse)) {
       item->state2 = item->state1;
       return r;
    }

    OK = FALSE;
    while (!OK) {

      /* LOOKING FOR CYCLE */

      seq0 = seq;

      sup = Bdd_RelOp(state2,Dnot_ras,"#AND Ex xA xR S2R",TRUE);
      sup = Bdd_ITE(C,sup,bdd_termFalse);                 /* successors */

      Z = sup;
      Bdd_Fortify(Z);

      seq1 = (McFunctionSequence *) malloc(sizeof(McFunctionSequence));
      seq1->f = Z;
      seq1->nextFunction = NULL;
      seq1->prevFunction = NULL; /* NULL IS IMPORTANT HERE */
      seq->nextFunction = seq1;
      seq = seq1;

      Yn = Bdd_ITE(state2,Z,bdd_termFalse);

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

        last = Z;
        sup = Bdd_RelOp(Z,Dnot_ras,"#AND Ex xA xR S2R",TRUE);
        sup = Bdd_ITE(C,sup,bdd_termFalse);        /* sup = Z -Dnot-> ... */

        Z = Bdd_ITE(Z,bdd_termTrue,sup);                   /* Z = Z + sup */
        Bdd_Fortify(Z);

        seq1 = (McFunctionSequence *) malloc(sizeof(McFunctionSequence));
        seq1->f = Z;
        seq1->nextFunction = NULL;
        seq1->prevFunction = seq;
        seq->nextFunction = seq1;
        seq = seq1;

        Yn = Bdd_ITE(state2,Z,bdd_termFalse);
      }

      if (Bdd_isEqv(Yn,bdd_termFalse)) {

        /* DELETE NODES, BECAUSE THERE IS NO CYCLE */

        McDeleteFunctionSequence(seq0->nextFunction);

        seq = seq0;
        seq->nextFunction = NULL;

        /* GO TO THE NEXT NODE WHICH CAN BE START OF CYCLE */

        sup = Bdd_RelOpSimple(C,"R2S",TRUE);
        sup = Bdd_ITE(sup,state2,bdd_termFalse);
        sup = Bdd_ITE(sup,Dnot_ras,bdd_termFalse);

        if (Bdd_isEqv(sup,bdd_termFalse)) {

          /* DEADLOCKED STATE IS REACHED */

          OK = TRUE;
          item->state2 = state2;

  } else {

          if (dgn.proc != -1) {
            sup = Pa_ExtractProcTransition(&pa_processTable[dgn.proc],sup);
          }
          if (dgn.comp != -1) {
            sup = Pa_ExtractCompTransition(&pa_compositionTable[dgn.comp],sup);
          }

          sup = Bdd_RelOpSimple(sup,"Ex xR S2R",TRUE);
          Bdd_Fortify(sup);

          seq1 = (McFunctionSequence *) malloc(sizeof(McFunctionSequence));
          seq1->f = sup;
          seq1->nextFunction = NULL;  /* NOT IMPORTANT */
          seq1->prevFunction = seq;
          seq->nextFunction = seq1;
          seq = seq1;

          state2 = Bdd_RelOpSimple(sup,"Ex xA",TRUE);
          Bdd_Fortify(state2);
  }

      } else {

        OK = TRUE;
        item->state2 = state2;

        /* EXTRACT PATH */
        /* seq = YN */

        if (seq->prevFunction) {

          /* THE PATH IS NOT FINISHED IN THE FIRST STATE */

          seq = seq->prevFunction;
          while (seq->prevFunction) {
            sup = Bdd_ITE(seq->prevFunction->f,bdd_termFalse,seq->f); /* ex */
            sup1 = Bdd_RelOpSimple(state2,"R2S",TRUE);
            sup = Bdd_ITE(sup,sup1,bdd_termFalse);
            sup = Bdd_ITE(sup,Dnot_ras,bdd_termFalse);

            if (dgn.proc != -1) {
              sup = Pa_ExtractProcTransition(&pa_processTable[dgn.proc],sup);
            }
            if (dgn.comp != -1) {
              sup = Pa_ExtractCompTransition(&pa_compositionTable[dgn.comp],sup);
            }

            state2 = Bdd_RelOpSimple(sup,"Ex xA xS",TRUE);
            Bdd_Fortify(state2);

            sup = Bdd_RelOpSimple(sup,"Ex xR S2R",TRUE);
            Bdd_Fortify(sup);

            seq->nextFunction->f = sup;
            seq = seq->prevFunction;
    }

          /* THE SECOND TRANSITION IN CYCLE */

          sup = Bdd_RelOpSimple(state2,"R2S",TRUE);
          sup = Bdd_ITE(sup,seq->f,bdd_termFalse);           /* AND Y0 */
          sup = Bdd_ITE(sup,Dnot_ras,bdd_termFalse);

          if (dgn.proc != -1) {
            sup = Pa_ExtractProcTransition(&pa_processTable[dgn.proc],sup);
          }
          if (dgn.comp != -1) {
            sup = Pa_ExtractCompTransition(&pa_compositionTable[dgn.comp],sup);
          }

          state2 = Bdd_RelOpSimple(sup,"Ex xA xS",TRUE);
          Bdd_Fortify(state2);

          sup = Bdd_RelOpSimple(sup,"Ex xR S2R",TRUE);
          Bdd_Fortify(sup);

          seq->nextFunction->f = sup;
  }

        /* THE FIRST TRANSITION IN CYCLE */

        sup = Bdd_RelOpSimple(state2,"R2S",TRUE);
        sup = Bdd_ITE(sup,item->state2,bdd_termFalse);
        sup = Bdd_ITE(sup,Dnot_ras,bdd_termFalse);

        if (dgn.proc != -1) {
          sup = Pa_ExtractProcTransition(&pa_processTable[dgn.proc],sup);
        }
        if (dgn.comp != -1) {
          sup = Pa_ExtractCompTransition(&pa_compositionTable[dgn.comp],sup);
        }

        sup = Bdd_RelOpSimple(sup,"Ex xR S2R",TRUE);
        Bdd_Fortify(sup);

        seq->f = sup;
      }
    }
  }

  return r;
}

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

static Est_Boolean
DiagnosticAAG(McDiagnosticType dgn, Bdd_Edge D, McDiagnosticItem *item,
              Est_Boolean strict)
{
  Est_Boolean r;
  Bdd_Edge a2org,s2org;

  a2org = item->act2;
  s2org = item->form2;

  item->act2 = bdd_termFalse;
  item->form2 = bdd_termFalse;

  r = DiagnosticAAW(dgn,D,item,strict);

  item->act2 = a2org;
  item->form2 = s2org;
  return r;
}

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

static Est_Boolean
DiagnosticEU(McDiagnosticType dgn, Bdd_Edge D, McDiagnosticItem *item)
{
  Est_Boolean r;
  Bdd_Edge sup,a1org,a2org;
  McFunctionSequence *seq;

  a1org = item->act1;
  a2org = item->act2;

  if (Bdd_isNull(item->act2)) {
    sup = Bdd_ITE(item->form2,item->state1,bdd_termFalse);
    if (!Bdd_isEqv(sup,bdd_termFalse)) {
      seq = (McFunctionSequence *) malloc(sizeof(McFunctionSequence));
      seq->f = item->state1;
      seq->nextFunction = NULL;
      seq->prevFunction = NULL;
      item->path = seq;
      item->state2 = item->state1;
      item->lastaction = bdd_termFalse;
      r = TRUE;
    } else {
      item->act1 = Bdd_ITE(item->act1,bdd_termTrue,McTau);
      Bdd_Fortify(item->act1);
      item->act2 = item->act1;
      r =  DiagnosticEEU(dgn,D,item,FALSE);
    }
  } else {
    item->act1 = Bdd_ITE(item->act1,bdd_termTrue,McTau);
    item->act2 = Bdd_ITE(McTau,bdd_termFalse,item->act2);
    Bdd_Fortify(item->act1);
    Bdd_Fortify(item->act2);
    r =  DiagnosticEEU(dgn,D,item,FALSE);
  }

  item->act1 = a1org;
  item->act2 = a2org;
  return r;
}


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

static Est_Boolean
DiagnosticAU(McDiagnosticType dgn, Bdd_Edge D, McDiagnosticItem *item)
{
  Est_Boolean r;
  Bdd_Edge sup,a1org,a2org;

  a1org = item->act1;
  a2org = item->act2;

  if (Bdd_isNull(item->act2)) {
    sup = Bdd_ITE(item->form2,item->state1,bdd_termFalse);
    if (!Bdd_isEqv(sup,bdd_termFalse)) {
      item->lastaction = bdd_termFalse;
      item->state2 = item->state1;
      r = 3;
    } else {
      item->act1 = Bdd_ITE(item->act1,bdd_termTrue,McTau);
      Bdd_Fortify(item->act1);
      item->act2 = item->act1;
      r = DiagnosticAAU(dgn,D,item,FALSE);
    }
  } else {
    item->act1 = Bdd_ITE(item->act1,bdd_termTrue,McTau);
    item->act2 = Bdd_ITE(McTau,bdd_termFalse,item->act2);
    Bdd_Fortify(item->act1);
    Bdd_Fortify(item->act2);
    r = DiagnosticAAU(dgn,D,item,FALSE);
  }

  item->act1 = a1org;
  item->act2 = a2org;

  return r;
}


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

static Est_Boolean
DiagnosticEX(McDiagnosticType dgn, Bdd_Edge D, McDiagnosticItem *item)
{
  Est_Boolean r;
  Bdd_Edge a2org;

  a2org = item->act2;

  if (Bdd_isEqv(item->act2,McTau)) {

    r = DiagnosticEEX(dgn,D,item);

  } else {

    item->act2 = Bdd_ITE(McTau,bdd_termFalse,item->act2);
    Bdd_Fortify(item->act2);
    r = DiagnosticEEX(dgn,D,item);

  }

  item->act2 = a2org;
  return r;
}


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

static Est_Boolean
DiagnosticAX(McDiagnosticType dgn, Bdd_Edge D, McDiagnosticItem *item)
{
  Est_Boolean r;
  Bdd_Edge a2org;

  a2org = item->act2;

  if (Bdd_isEqv(item->act2,McTau)) {

    /* IF THERE ARE NO TRANSITIONS IN THE PROCESS !! */      /* CAREFULLY !!! */
    if (Bdd_isEqv(D,bdd_termFalse)) {
      item->lastaction = bdd_termFalse;
      item->state2 = item->state1;
      r = FALSE;

    } else {

      r = DiagnosticAAX(dgn,D,item);

    }

  } else {

    /* IF THERE ARE NO TRANSITIONS IN THE PROCESS !! */      /* CAREFULLY !!! */
    if (Bdd_isEqv(D,bdd_termFalse)) {
      item->lastaction = bdd_termFalse;
      item->state2 = item->state1;
      r = FALSE;

    } else {

      item->act2 = Bdd_ITE(McTau,bdd_termFalse,item->act2);
      Bdd_Fortify(item->act2);
      r = DiagnosticAAX(dgn,D,item);

    }

  }

  item->act2 = a2org;
  return r;
}


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

static Est_Boolean
DiagnosticEF(McDiagnosticType dgn, Bdd_Edge D, McDiagnosticItem *item)
{
  Est_Boolean r;
  Bdd_Edge sup;
  Bdd_Edge a2org;
  McFunctionSequence *seq;

  a2org = item->act2;
  item->act2 = bdd_termTrue;

  sup = Bdd_ITE(item->form2,item->state1,bdd_termFalse);
  if (!Bdd_isEqv(sup,bdd_termFalse)) {
    seq = (McFunctionSequence *) malloc(sizeof(McFunctionSequence));
    seq->f = item->state1;
    seq->nextFunction = NULL;
    seq->prevFunction = NULL;
    item->path = seq;
    item->lastaction = bdd_termFalse;
    item->state2 = item->state1;
    r = TRUE;
  } else {

    r =  DiagnosticEEF(dgn,D,item);

  }

  item->act2 = a2org;
  return r;
}


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

static Est_Boolean
DiagnosticAF(McDiagnosticType dgn, Bdd_Edge D, McDiagnosticItem *item)
{
  Est_Boolean r;
  Bdd_Edge sup;
  Bdd_Edge a2org;

  a2org = item->act2;
  item->act2 = bdd_termTrue;

  sup = Bdd_ITE(item->form2,item->state1,bdd_termFalse);
  if (!Bdd_isEqv(sup,bdd_termFalse)) {
    item->lastaction = bdd_termFalse;
    item->state2 = item->state1;
    r = 3;
  } else {
    if (!DiagnosticAAF(dgn,D,item)) {
      r = 2;
    } else {
      r = 0;
    }
  }

  item->act2 = a2org;
  return r;
}


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

static Est_Boolean
DiagnosticEG(McDiagnosticType dgn, Bdd_Edge D, McDiagnosticItem *item)
{
  Est_Boolean r;
  Bdd_Edge a1org;

  a1org = item->act1;

  item->act1 = bdd_termTrue;
  r = DiagnosticEEG(dgn,D,item,FALSE);

  item->act1 = a1org;
  return r;
}


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

static Est_Boolean
DiagnosticAG(McDiagnosticType dgn, Bdd_Edge D, McDiagnosticItem *item)
{
  Est_Boolean r;
  Bdd_Edge a1org;

  a1org = item->act1;

  item->act1 = bdd_termTrue;
  r = DiagnosticAAG(dgn,D,item,FALSE);

  item->act1 = a1org;
  return r;
}


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

static Est_Boolean
DiagnosticHME(McDiagnosticType dgn, Bdd_Edge D, McDiagnosticItem *item)
{
  Est_Boolean r;
  Bdd_Edge a1org,s1org;

  a1org = item->act1;
  s1org = item->form1;

  if (Bdd_isNull(item->form1) && !Bdd_isNull(item->act2)) {

    /* CAREFULLY!! */
    /* WE PREFER TO USE STRONG HME, WHERE APPROPRIATE */
    r = DiagnosticEX(dgn,D,item);

    /* THIS IS WEAK HME FROM DeNicola, Vaandrager, 1990 */
    /*
    item->act1 = bdd_termFalse;
    r = DiagnosticEU(dgn,D,item);
    */

  } else {

    if (Bdd_isNull(item->form1)) {
      item->form1 = bdd_termTrue;
    }

    item->act1 = bdd_termFalse;
    r = DiagnosticEU(dgn,D,item);

  }

  item->act1 = a1org;
  item->form1 = s1org;
  return r;
}


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

static Est_Boolean
DiagnosticHMA(McDiagnosticType dgn, Bdd_Edge D, McDiagnosticItem *item)
{
  Bdd_Edge sup1,sup2,sall,snot;
  Est_Boolean r;
  Bdd_Edge s1org,s2org;

  s1org = item->form1;
  s2org = item->form2;

  if (Bdd_isEqv(D,bdd_termFalse)) {
    sall = dgn.init;
  } 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 */
  }

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

  item->form2 = snot;
  r = DiagnosticHME(dgn,D,item);

  item->form1 = s1org;
  item->form2 = s2org;

  return !r;
}

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

static void
pathValid(McDiagnosticType dgn, int num, Bdd_Edge state1, Bdd_Edge state2,
          Est_Boolean explain, Est_Boolean tracepath)
{
  if (explain) {
    if (!tracepath) {
      printf("@@ Path from ");
      if (dgn.proc != -1 ) Pa_DecodeProcessStates(&pa_processTable[dgn.proc],state1,TRUE);
      if (dgn.comp != -1) Pa_DecodeCompStates(&pa_compositionTable[dgn.comp],state1,TRUE);
      printf(" to ");
      if (dgn.proc != -1) Pa_DecodeProcessStates(&pa_processTable[dgn.proc],state2,TRUE);
      if (dgn.comp != -1) Pa_DecodeCompStates(&pa_compositionTable[dgn.comp],state2,TRUE);
      printf(" satisfies formula #%d.",num);
    } else {
      printf("@@ There exist a path satisfying formula #%d: ",num);
      if (dgn.proc != -1) Pa_DecodeProcessStates(&pa_processTable[dgn.proc],state1,TRUE);
      if (dgn.comp != -1) Pa_DecodeCompStates(&pa_compositionTable[dgn.comp],state1,TRUE);
    }
  }
}

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

static void
pathInvalid(McDiagnosticType dgn, int num, Bdd_Edge state1, Bdd_Edge state2,
          Est_Boolean explain, Est_Boolean tracepath)
{
  if (explain) {
    if (!tracepath) {
       printf("@@ Path from ");
       if (dgn.proc != -1) Pa_DecodeProcessStates(&pa_processTable[dgn.proc],state1,TRUE);
       if (dgn.comp != -1) Pa_DecodeCompStates(&pa_compositionTable[dgn.comp],state1,TRUE);
       printf(" to ");
       if (dgn.proc != -1) Pa_DecodeProcessStates(&pa_processTable[dgn.proc],state2,TRUE);
       if (dgn.comp != -1) Pa_DecodeCompStates(&pa_compositionTable[dgn.comp],state2,TRUE);
       printf(" does not satisfy formula #%d.",num);
    } else {
       printf("@@ There exist a path not satisfying formula #%d: ",num);
       if (dgn.proc != -1) Pa_DecodeProcessStates(&pa_processTable[dgn.proc],state1,TRUE);
       if (dgn.comp != -1) Pa_DecodeCompStates(&pa_compositionTable[dgn.comp],state1,TRUE);
    }
  }
}

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

static void
transitionValid(McDiagnosticType dgn, int num, Bdd_Edge state1, Bdd_Edge state2,
                Est_Boolean explain, Est_Boolean tracepath)
{
  if (explain) {
    printf("@@ There exist a transition satisfying formula #%d: ",num);
    if (dgn.proc != -1) Pa_DecodeProcessStates(&pa_processTable[dgn.proc],state1,TRUE);
    if (dgn.comp != -1) Pa_DecodeCompStates(&pa_compositionTable[dgn.comp],state1,TRUE);
  }
}

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

static void
transitionInvalid(McDiagnosticType dgn, int num, Bdd_Edge state1, Bdd_Edge state2,
                  Est_Boolean explain, Est_Boolean tracepath)
{
  if (explain) {
    printf("@@ There exist a transition not satisfying formula #%d: ",num);
    if (dgn.proc != -1) Pa_DecodeProcessStates(&pa_processTable[dgn.proc],state1,TRUE);
    if (dgn.comp != -1) Pa_DecodeCompStates(&pa_compositionTable[dgn.comp],state1,TRUE);
  }
}

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

static void
transitionNone(McDiagnosticType dgn, int num, Est_Boolean explain,
               Est_Boolean tracepath)
{
  if (explain) {
    printf("@@ There is no transition satisfying formula #%d.",num);
  }
}

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

static void
transitionAll(McDiagnosticType dgn, int num,
              Est_Boolean explain, Est_Boolean tracepath)
{
  if (explain) {
    printf("@@ All transitions satisfy formula #%d.",num);
  }
}

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

static void
deadlockedValid(McDiagnosticType dgn, int num, Bdd_Edge state1,
                McDiagnosticItem *nextitem, Est_Boolean explain,
                Est_Boolean tracepath)
{
  if (explain) {
    printf("@@ Formula #%d is valid in deadlocked state ",num);
    if (dgn.proc != -1) Pa_DecodeProcessStates(&pa_processTable[dgn.proc],state1,TRUE);
    if (dgn.comp != -1) Pa_DecodeCompStates(&pa_compositionTable[dgn.comp],state1,TRUE);
    if (nextitem) {
      printf(" because formula #%d is valid in it.",nextitem->num);
    } else {
      printf(".");
    }
  }
}

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

static void
deadlockedInvalid(McDiagnosticType dgn, int num, Bdd_Edge state1,
                  McDiagnosticItem *nextitem, Est_Boolean explain,
                  Est_Boolean tracepath)
{
  if (explain) {
    printf("@@ Formula #%d is not valid in deadlocked state ",num);
    if (dgn.proc != -1) Pa_DecodeProcessStates(&pa_processTable[dgn.proc],state1,TRUE);
    if (dgn.comp != -1) Pa_DecodeCompStates(&pa_compositionTable[dgn.comp],state1,TRUE);
    if (nextitem) {
      printf(" because formula #%d is not valid in it.",nextitem->num);
    } else {
      printf(".");
    }
  }
}

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

static void
stateValid(McDiagnosticType dgn, int num, Bdd_Edge state1,
           McDiagnosticItem *nextitem, Est_Boolean explain,
           Est_Boolean tracepath)
{
  if (explain) {
    printf("@@ Formula #%d is valid in state ",num);
    if (dgn.proc != -1) Pa_DecodeProcessStates(&pa_processTable[dgn.proc],state1,TRUE);
    if (dgn.comp != -1) Pa_DecodeCompStates(&pa_compositionTable[dgn.comp],state1,TRUE);
    if (nextitem) {
      printf(" because formula #%d is valid in it.",nextitem->num);
    } else {
      printf(".");
    }
  }
}

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

static void
stateInvalid(McDiagnosticType dgn, int num, Bdd_Edge state1,
             McDiagnosticItem *nextitem, Est_Boolean explain,
             Est_Boolean tracepath)
{
  if (explain) {
    printf("@@ Formula #%d is not valid in state ",num);
    if (dgn.proc != -1) Pa_DecodeProcessStates(&pa_processTable[dgn.proc],state1,TRUE);
    if (dgn.comp != -1) Pa_DecodeCompStates(&pa_compositionTable[dgn.comp],state1,TRUE);
    if (nextitem) {
      printf(" because formula #%d is not valid in it.",nextitem->num);
    } else {
      printf(".");
    }
  }
}

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

static void
stateInvalid2(McDiagnosticType dgn, int num, Bdd_Edge state1, int nextnum1,
              int nextnum2, Est_Boolean explain, Est_Boolean tracepath)
{
  if (explain) {
    printf("@@ Formula #%d is not valid in state ",num);
    if (dgn.proc != -1) Pa_DecodeProcessStates(&pa_processTable[dgn.proc],state1,TRUE);
    if (dgn.comp != -1) Pa_DecodeCompStates(&pa_compositionTable[dgn.comp],state1,TRUE);
    printf(" because formulae #%d and #%d are not valid in it.",
           nextnum1,nextnum2);
  }
}

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

static void
pathNone(McDiagnosticType dgn, int num, Est_Boolean explain,
         Est_Boolean tracepath)
{
  if (explain) {
    printf("@@ There is no path satisfying formula #%d.",num);
  }
}

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

static void
pathAll(McDiagnosticType dgn, int num, Est_Boolean explain,
         Est_Boolean tracepath)
{
  if (explain) {
    printf("@@ All paths satisfy formula #%d.",num);
  }
}

/**Function****************************************************************
  Synopsis    []
  Description [Generate witness/counterexample as a Spin trail.
               Thanks to Tim Kovse and Vladimir Smrekar for prototype
               implementation.]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

static void
createSpinTrail(McDiagnosticType dgn, McFunctionSequence *seq, Pa_Sort *sort,
          Est_String *msc, Est_Boolean firstitem)
{
  int i;
  int line;

  /* YOU CAN CONVERT SPIN TRAIL TO MSC (ITU-T Z.120) BY USING       */
  /* http://matrix.uni-mb.si/en/science/tools/st2msc-tool/          */

  /* SOME DOCUMENTATION                                             */
  /* T. Kovše, B. Vlaovič, A. Vreže, and Z. Brezočnik.              */
  /* Spin Trail to a Message Sequence Chart Conversion Tool,        */
  /* ConTEL, Zagreb, Croatia. 2009.                                 */
  /* http://matrix.uni-mb.si/fileadmin/datoteke/osebno/clanki/      */
  /*      Automated_Generation_of_Models_from_SDL_specification.pdf */
  /*                                                                */
  /* NOTES:                                                         */
  /* ENVIRONMENT ID = -1                                            */

  /* BASIC ELEMENTS                                                 */
  /* COMPATIBLE WITH spin v.5 AND st2msc v2.0, date 2009.05.15      */
  /*
  Create new process ENVIRONMENT
  0: proc -2 (:init:) creates proc -1 (ENVIRONMENT)

  Send message kr1 with parameter (data) null
  3: proc 4 (K1#1) line 3 'pan_in' (state -) [values: kr1!null]

  Get message kr1 with parameter (data) null
  4: proc 1 (R0#1) line 3 'pan_in' (state -) [values: kr1?null]
  */

  /* BASIC ELEMENTS                                                 */
  /* COMPATIBLE WITH spin v.6 AND st2msc (new version)              */
  /*
  Create new process ENVIRONMENT
  0: proc -2 (:init:) creates proc -1 (ENVIRONMENT)

  Send message kr1 with parameter (data) null
  3: proc 4 (K1#1) pan_in:3 (state -) [values: kr1!null]

  Get message kr1 with parameter (data) null
  4: proc 1 (R0#1) pan_in:3 (state -) [values: kr1?null]
  */

  line = 0;
  *msc = strdup("");

  /* GENERATE INITIAL PART OF SPIN TRAIL - ONLY ONCE! */
  if (firstitem) {
    concat(msc,"0: proc -2 (:init:) creates proc -1 (ENVIRONMENT)\n");
    for (i=0; i<pa_compositionTable[dgn.comp].numProcesses; i++) {
      concat(msc,"0: proc -2 (:init:) creates proc ");
      concatInt(msc,i);
      concat(msc," (");
      concat(msc,pa_processTable[pa_compositionTable[dgn.comp].tableP[i]].name);
      concat(msc,")");
      concat(msc,"\n");
    }
  }

  /* GENERATION OF SPIN TRAIL IS DIVIDED INTO TWO PARTS */
  /* INTERNAL STEPS ARE IGNORED */
  while (seq) {
    line++;

    if (Bdd_isEqv(Bdd_ITE(seq->f,McTau,bdd_termFalse),bdd_termFalse)) {

      /* PART 1: COMMUNICATION BETWEEN PROCESS AND ENVIRONMENT */

      int A;
      Bdd_Edge f;
      Est_String act;

      A = -1;
      f = Bdd_RelOpSimple(seq->f,"Ex xR",TRUE);
      for (i=0; i<pa_compositionTable[dgn.comp].numProcesses; i++) {
        if (!Bdd_isEqv(
             Bdd_ITE(pa_processTable[pa_compositionTable[dgn.comp].tableP[i]].d,
                     f,bdd_termFalse),bdd_termFalse)
           )
        {
          A = i;
        }
      }

      if (A!=-1) {

        if (!Bdd_isEqv(Bdd_ITE(sort->a0,bdd_termFalse,f),bdd_termFalse)) {
          /* INPUT ACTION */

          /* SEND - SPIN v.5 */
          concatInt(msc,line);
          concat(msc,": proc ");
          concat(msc,"-1");
          concat(msc," (");
          concat(msc,"ENVIRONMENT");

          /* SEND - SPIN v.5 */
          /**/
          concat(msc,") line ");
          concatInt(msc,line);
          concat(msc," 'pan_in'");
          /**/

          /* SEND - SPIN v.6 */
          /*
          concat(msc,") 'pan_in':");
          concatInt(msc,line);
          */

          concat(msc," (state -) [values: ");
          act = Pa_DecodeSortActions1(sort,f,FALSE);
          if (act[(strlen(act)-1)] == '!' || act[(strlen(act)-1)] == '?') {
            act[(strlen(act)-1)] = '\0';
          }
          concat(msc,act);
          concat(msc,"!null]");
          concat(msc,"\n");

          /* RECEIVE */
          concatInt(msc,line);
          concat(msc,": proc ");
          concatInt(msc,A);
          concat(msc," (");
          concat(msc,pa_processTable[pa_compositionTable[dgn.comp].tableP[A]].name);

          /* RECEIVE - SPIN v.5 */
          /**/
          concat(msc,") line ");
          concatInt(msc,line);
          concat(msc," 'pan_in'");
          /**/

          /* RECEIVE - SPIN v.6 */
          /*
          concat(msc,") 'pan_in':");
          concatInt(msc,line);
          */

          concat(msc," (state -) [values: ");
          concat(msc,act);
          free(act);
          concat(msc,"?null]");
          concat(msc,"\n");

        } else {
          /* OUTPUT ACTION */

          /* SEND */
          concatInt(msc,line);
          concat(msc,": proc ");
          concatInt(msc,A);
          concat(msc," (");
          concat(msc,pa_processTable[pa_compositionTable[dgn.comp].tableP[A]].name);

          /* SEND - SPIN v.5 */
          /**/
          concat(msc,") line ");
          concatInt(msc,line);
          concat(msc," 'pan_in'");
          /**/

          /* SEND - SPIN v.6 */
          /*
          concat(msc,") 'pan_in':");
          concatInt(msc,line);
          */

          concat(msc," (state -) [values: ");
          act = Pa_DecodeSortActions1(sort,f,FALSE);
          if (act[(strlen(act)-1)] == '!' || act[(strlen(act)-1)] == '?') {
            act[(strlen(act)-1)] = '\0';
          }
          concat(msc,act);
          concat(msc,"!null]");
          concat(msc,"\n");

          /* RECEIVE */
          concatInt(msc,line);
          concat(msc,": proc ");
          concat(msc,"-1");
          concat(msc," (");
          concat(msc,"ENVIRONMENT");

          /* RECEIVE - SPIN v.5 */
          /**/
          concat(msc,") line ");
          concatInt(msc,line);
          concat(msc," 'pan_in'");
          /**/

          /* RECEIVE - SPIN v.6 */
          /*
          concat(msc,") 'pan_in':");
          concatInt(msc,line);
          */

          concat(msc," (state -) [values: ");
          concat(msc,act);
          free(act);
          concat(msc,"?null]");
          concat(msc,"\n");

        }

      }

    } else {

      /* PART 2: COMMUNICATION BETWEEN TWO PROCESSES */

      int A,B;
      Est_String s;
      Bdd_Edge f,f1,f2,f3,fact;
      Est_String act;

      A = -1;
      B = -1;
      fact = bdd_termTrue;
      for (i=0; i<pa_compositionTable[dgn.comp].numProcesses; i++) {
        s = (Est_String) malloc(255);
        sprintf(s,"Ex xA xR^<%s>",pa_processTable[pa_compositionTable[dgn.comp].tableP[i]].name);
        f1 = Bdd_RelOpComplex(seq->prevFunction->f,s,TRUE);
        f2 = Bdd_RelOpComplex(seq->f,s,TRUE);
        free(s);
        if (!Bdd_isEqv(f1,f2)) {
          if (A == -1) A = i; else B = i;
          f = Bdd_RelOp(
                Bdd_ITE(f1,Bdd_RelOpSimple(f2,"R2S",TRUE),bdd_termFalse),
                pa_processTable[pa_compositionTable[dgn.comp].tableP[i]].d,
                "#AND Ex xR xS",TRUE);
          fact = Bdd_ITE(fact,Bdd_E(f,Bdd_GetVariable(sort->a0)),bdd_termFalse);
        }
      }
      fact = Pa_ExtractSortAction(sort,fact); /* EXTRACT ONE ACTION */
      s = (Est_String) malloc(255);
      sprintf(s,"Ex xA xR^<%s>",pa_processTable[pa_compositionTable[dgn.comp].tableP[A]].name);
      f1 = Bdd_RelOpComplex(seq->prevFunction->f,s,TRUE);
      f2 = Bdd_RelOpComplex(seq->f,s,TRUE);
      free(s);
      f = Bdd_RelOp(
            Bdd_ITE(f1,Bdd_RelOpSimple(f2,"R2S",TRUE),bdd_termFalse),
            pa_processTable[pa_compositionTable[dgn.comp].tableP[A]].d,
            "#AND Ex xR xS",TRUE);
      f = Bdd_ITE(f,fact,bdd_termFalse);
      if (!Bdd_isEqv(Bdd_ITE(sort->a0,bdd_termFalse,f),bdd_termFalse)) {
        /* EXCHANGE SOURCE AND DESTINATION */
        i = A;
        A = B;
        B = i;
      }

      if ((A==-1) && (Bdd_isEqv(Bdd_ITE(fact,McTau,bdd_termFalse),bdd_termFalse))) {
        f = Bdd_ITE(fact,sort->a0,bdd_termFalse);
        for (i=0; i<pa_compositionTable[dgn.comp].numProcesses; i++) {
          s = (Est_String) malloc(255);
          sprintf(s,"Ex xA xR^<%s>",pa_processTable[pa_compositionTable[dgn.comp].tableP[i]].name);
          f1 = Bdd_RelOpComplex(seq->prevFunction->f,s,TRUE);
          f2 = Bdd_RelOpSimple(Bdd_RelOpComplex(seq->f,s,TRUE),"R2S",TRUE);
          free(s);
          f3 = Bdd_ITE(Bdd_ITE(f1,f2,bdd_termFalse),f,bdd_termFalse);
          f3 = Bdd_ITE(pa_processTable[pa_compositionTable[dgn.comp].tableP[i]].d,f3,bdd_termFalse);
          if (!Bdd_isEqv(f3,bdd_termFalse)) {
            A = i;
            fact = Bdd_E(Bdd_RelOpSimple(f3,"Ex xR xS",TRUE),Bdd_GetVariable(sort->a0));
          }
        }
      }

      if ((B==-1) && (Bdd_isEqv(Bdd_ITE(fact,McTau,bdd_termFalse),bdd_termFalse))) {
        f = Bdd_ITE(fact,bdd_termFalse,sort->a0);
        for (i=0; i<pa_compositionTable[dgn.comp].numProcesses; i++) {
          s = (Est_String) malloc(255);
          sprintf(s,"Ex xA xR^<%s>",pa_processTable[pa_compositionTable[dgn.comp].tableP[i]].name);
          f1 = Bdd_RelOpComplex(seq->prevFunction->f,s,TRUE);
          f2 = Bdd_RelOpSimple(Bdd_RelOpComplex(seq->f,s,TRUE),"R2S",TRUE);
          free(s);
          f3 = Bdd_ITE(Bdd_ITE(f1,f2,bdd_termFalse),f,bdd_termFalse);
          f3 = Bdd_ITE(pa_processTable[pa_compositionTable[dgn.comp].tableP[i]].d,f3,bdd_termFalse);
          if (!Bdd_isEqv(f3,bdd_termFalse)) {
            B = i;
            fact = Bdd_E(Bdd_RelOpSimple(f3,"Ex xR xS",TRUE),Bdd_GetVariable(sort->a0));
          }
        }
      }

      if ((A!=-1) && (B!=-1)) {

        /* SEND */
        concatInt(msc,line);
        concat(msc,": proc ");
        concatInt(msc,A);
        concat(msc," (");
        concat(msc,pa_processTable[pa_compositionTable[dgn.comp].tableP[A]].name);

        /* SEND - SPIN v.5 */
        /**/
        concat(msc,") line ");
        concatInt(msc,line);
        concat(msc," 'pan_in'");
        /**/

        /* SEND - SPIN v.6 */
        /*
        concat(msc,") 'pan_in':");
        concatInt(msc,line);
        */

        concat(msc," (state -) [values: ");
        act = Pa_DecodeSortActions1(sort,Bdd_ITE(fact,sort->a0,bdd_termFalse),FALSE);
        if (act[(strlen(act)-1)] == '!'){
          act[(strlen(act)-1)] = '\0';
        }
        concat(msc,act);
        concat(msc,"!null]");
        concat(msc,"\n");

        /* RECEIVE */
        concatInt(msc,line);
        concat(msc,": proc ");
        concatInt(msc,B);
        concat(msc," (");
        concat(msc,pa_processTable[pa_compositionTable[dgn.comp].tableP[B]].name);

        /* RECEIVE - SPIN v.5 */
        /**/
        concat(msc,") line ");
        concatInt(msc,line);
        concat(msc," 'pan_in'");
        /**/

        /* RECEIVE - SPIN v.6 */
        /*
        concat(msc,") 'pan_in':");
        concatInt(msc,line);
        */

        concat(msc," (state -) [values: ");
        concat(msc,act);
        free(act);
        concat(msc,"?null]");
        concat(msc,"\n");
      }

    }

    seq = seq->nextFunction;
  }
}


/**Function****************************************************************
  Synopsis    []
  Description [Generate witness/counterexample as a MSC.
               You can rearrange the ordering of processes.
               Thanks to Tim Kovse and Vladimir Smrekar for prototype
               implementation.]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

static void
createMsc(McDiagnosticType dgn, McFunctionSequence *seq, Pa_Sort *sort,
          Est_String *msc, Est_Boolean firstitem)
{
  int i;

  /* YOU CAN VIEW MSC BY USING                                */
  /* http://www.mcternan.me.uk/mscgen/                        */

  /* BASIC ELEMENTS (COMPATIBLE WITH mscgen v0.20 from 2010)  */
  /*
  Create new processes A,B,C
  a,b,c;

  Send message kr1 from a to b
  a->b [ label = "kr1" ];
  */

  *msc = strdup("");

  /* GENERATE INITIAL PART OF MSC - ONLY ONCE! */
  if (firstitem) {

    /* THE LIST OF PROCESSES */
    concat(msc,"  ENVIRONMENT [textcolour=\"red\"]");
    for (i=0; i<pa_compositionTable[dgn.comp].numProcesses; i++) {
      concat(msc,",\n  \"");
      concat(msc,pa_processTable[pa_compositionTable[dgn.comp].tableP[i]].name);
      concat(msc,"\"");
    }
    concat(msc,";\n\n");

    /* INITIAL STATES */
    concat(msc,"  #");
    for (i=0; i<pa_compositionTable[dgn.comp].numProcesses; i++) {
      concat(msc,",\n  \"");
      concat(msc,pa_processTable[pa_compositionTable[dgn.comp].tableP[i]].name);
      concat(msc,"\" rbox \"");
      concat(msc,pa_processTable[pa_compositionTable[dgn.comp].tableP[i]].name);
      concat(msc,"\" [label=\"");
      concat(msc,pa_processTable[pa_compositionTable[dgn.comp].tableP[i]].
                 tableS[pa_processTable[pa_compositionTable[dgn.comp].tableP[i]].initial].name);
      concat(msc,"\", textbgcolour=\"#7f7fff\"]");
    }
    concat(msc,";\n\n");
  }

  /* GENERATION OF MSC IS DIVIDED INTO TWO PARTS */
  while (seq) {

    if (Bdd_isEqv(Bdd_ITE(seq->f,McTau,bdd_termFalse),bdd_termFalse)) {

      /* PART 1: COMMUNICATION BETWEEN PROCESS AND ENVIRONMENT */

      int A,As;
      Est_String s;
      Bdd_Edge f;
      Est_String act;

      A = -1;

      f = Bdd_RelOpSimple(seq->f,"Ex xR",TRUE);
      for (i=0; i<pa_compositionTable[dgn.comp].numProcesses; i++) {
        if (!Bdd_isEqv(
             Bdd_ITE(pa_processTable[pa_compositionTable[dgn.comp].tableP[i]].d,
                     f,bdd_termFalse),bdd_termFalse)
           )
        {
          A = i;
        }
      }

      if (A!=-1) {

        if (!Bdd_isEqv(Bdd_ITE(sort->a0,bdd_termFalse,f),bdd_termFalse)) {
          /* INPUT ACTION */
          concat(msc,"  |||;ENVIRONMENT->\"");
          concat(msc,pa_processTable[pa_compositionTable[dgn.comp].tableP[A]].name);
          concat(msc,"\"");
          concat(msc," [ label = \"");
          act = Pa_DecodeSortActions1(sort,f,FALSE);
          if (act[(strlen(act)-1)] == '!' || act[(strlen(act)-1)] == '?') {
            act[(strlen(act)-1)] = '\0';
          }
          concat(msc,act);
          concat(msc,"\", textcolour=\"red\", linecolour=\"red\"];\n");
        } else {
          /* OUTPUT ACTION */
          concat(msc,"  |||;\"");
          concat(msc,pa_processTable[pa_compositionTable[dgn.comp].tableP[A]].name);
          concat(msc,"\"");
          concat(msc,"->");
          concat(msc,"ENVIRONMENT");
          concat(msc," [ label = \"");
          act = Pa_DecodeSortActions1(sort,f,FALSE);
          if (act[(strlen(act)-1)] == '!') {
            act[(strlen(act)-1)] = '\0';
          }
          concat(msc,act);
          concat(msc,"\", textcolour=\"red\", linecolour=\"red\"];\n");
        }

        /* NEW STATE */
        concat(msc,"  \"");
        concat(msc,pa_processTable[pa_compositionTable[dgn.comp].tableP[A]].name);
        concat(msc,"\" rbox \"");
        concat(msc,pa_processTable[pa_compositionTable[dgn.comp].tableP[A]].name);
        concat(msc,"\" [label=\"");
        s = (Est_String) malloc(255);
        sprintf(s,"Ex xA xR^<%s>",pa_processTable[pa_compositionTable[dgn.comp].tableP[A]].name);
        f = Bdd_RelOpComplex(seq->f,s,TRUE);
        free(s);
        As = Pa_EnumerateProcState(
               &pa_processTable[pa_compositionTable[dgn.comp].tableP[A]],f);
        concat(msc,pa_processTable[pa_compositionTable[dgn.comp].tableP[A]].tableS[As].name);
        if (As == pa_processTable[pa_compositionTable[dgn.comp].tableP[A]].initial) {
          concat(msc,"\", textbgcolour=\"#7f7fff\"];\n");
        } else {
          concat(msc,"\", textbgcolour=\"#7fff7f\"];\n");
        }
      }

    } else {

      /* PART 2: COMMUNICATION BETWEEN TWO PROCESSES */
      /* COMMUNICATION NOT RESULTING IN STATE CHANGE IS IGNORED */

      int A,As,B,Bs;
      Est_String s;
      Bdd_Edge f,f1,f2,f3,fact;
      Est_String act;

      A = -1;
      B = -1;
      fact = bdd_termTrue;
      for (i=0; i<pa_compositionTable[dgn.comp].numProcesses; i++) {
        s = (Est_String) malloc(255);
        sprintf(s,"Ex xA xR^<%s>",pa_processTable[pa_compositionTable[dgn.comp].tableP[i]].name);
        f1 = Bdd_RelOpComplex(seq->prevFunction->f,s,TRUE);
        f2 = Bdd_RelOpComplex(seq->f,s,TRUE);
        free(s);
        if (!Bdd_isEqv(f1,f2)) {
          if (A == -1) A = i; else B = i;
          f = Bdd_RelOp(
                Bdd_ITE(f1,Bdd_RelOpSimple(f2,"R2S",TRUE),bdd_termFalse),
                pa_processTable[pa_compositionTable[dgn.comp].tableP[i]].d,
                "#AND Ex xR xS",TRUE);
          fact = Bdd_ITE(fact,Bdd_E(f,Bdd_GetVariable(sort->a0)),bdd_termFalse);
        }
      }
      fact = Pa_ExtractSortAction(sort,fact); /* EXTRACT ONE ACTION */
      s = (Est_String) malloc(255);
      sprintf(s,"Ex xA xR^<%s>",pa_processTable[pa_compositionTable[dgn.comp].tableP[A]].name);
      f1 = Bdd_RelOpComplex(seq->prevFunction->f,s,TRUE);
      f2 = Bdd_RelOpComplex(seq->f,s,TRUE);
      free(s);
      f = Bdd_RelOp(
            Bdd_ITE(f1,Bdd_RelOpSimple(f2,"R2S",TRUE),bdd_termFalse),
            pa_processTable[pa_compositionTable[dgn.comp].tableP[A]].d,
            "#AND Ex xR xS",TRUE);
      f = Bdd_ITE(f,fact,bdd_termFalse);
      if (!Bdd_isEqv(Bdd_ITE(sort->a0,bdd_termFalse,f),bdd_termFalse)) {
        /* EXCHANGE SOURCE AND DESTINATION */
        i = A;
        A = B;
        B = i;
      }

      if ((A==-1) && (Bdd_isEqv(Bdd_ITE(fact,McTau,bdd_termFalse),bdd_termFalse))) {
        f = Bdd_ITE(fact,sort->a0,bdd_termFalse);
        for (i=0; i<pa_compositionTable[dgn.comp].numProcesses; i++) {
          s = (Est_String) malloc(255);
          sprintf(s,"Ex xA xR^<%s>",pa_processTable[pa_compositionTable[dgn.comp].tableP[i]].name);
          f1 = Bdd_RelOpComplex(seq->prevFunction->f,s,TRUE);
          f2 = Bdd_RelOpSimple(Bdd_RelOpComplex(seq->f,s,TRUE),"R2S",TRUE);
          free(s);
          f3 = Bdd_ITE(Bdd_ITE(f1,f2,bdd_termFalse),f,bdd_termFalse);
          f3 = Bdd_ITE(pa_processTable[pa_compositionTable[dgn.comp].tableP[i]].d,f3,bdd_termFalse);
          if (!Bdd_isEqv(f3,bdd_termFalse)) {
            A = i;
            fact = Bdd_E(Bdd_RelOpSimple(f3,"Ex xR xS",TRUE),Bdd_GetVariable(sort->a0));
          }
        }
      }

      if ((B==-1) && (Bdd_isEqv(Bdd_ITE(fact,McTau,bdd_termFalse),bdd_termFalse))) {
        f = Bdd_ITE(fact,bdd_termFalse,sort->a0);
        for (i=0; i<pa_compositionTable[dgn.comp].numProcesses; i++) {
          s = (Est_String) malloc(255);
          sprintf(s,"Ex xA xR^<%s>",pa_processTable[pa_compositionTable[dgn.comp].tableP[i]].name);
          f1 = Bdd_RelOpComplex(seq->prevFunction->f,s,TRUE);
          f2 = Bdd_RelOpSimple(Bdd_RelOpComplex(seq->f,s,TRUE),"R2S",TRUE);
          free(s);
          f3 = Bdd_ITE(Bdd_ITE(f1,f2,bdd_termFalse),f,bdd_termFalse);
          f3 = Bdd_ITE(pa_processTable[pa_compositionTable[dgn.comp].tableP[i]].d,f3,bdd_termFalse);
          if (!Bdd_isEqv(f3,bdd_termFalse)) {
            B = i;
            fact = Bdd_E(Bdd_RelOpSimple(f3,"Ex xR xS",TRUE),Bdd_GetVariable(sort->a0));
          }
        }
      }

      if ((A!=-1) && (B!=-1)) {
        concat(msc,"  |||;\"");
        concat(msc,pa_processTable[pa_compositionTable[dgn.comp].tableP[A]].name);
        concat(msc,"\"->\"");
        concat(msc,pa_processTable[pa_compositionTable[dgn.comp].tableP[B]].name);
        concat(msc,"\" [ label = \"");
        act = Pa_DecodeSortActions1(sort,Bdd_ITE(fact,sort->a0,bdd_termFalse),FALSE);
        if (act[(strlen(act)-1)] == '!'){
          act[(strlen(act)-1)] = '\0';
        }
        concat(msc,act);
        concat(msc,"\" ];\n");

        /* NEW STATE FOR A */
        concat(msc,"  \"");
        concat(msc,pa_processTable[pa_compositionTable[dgn.comp].tableP[A]].name);
        concat(msc,"\" rbox \"");
        concat(msc,pa_processTable[pa_compositionTable[dgn.comp].tableP[A]].name);
        concat(msc,"\" [label=\"");
        s = (Est_String) malloc(255);
        sprintf(s,"Ex xA xR^<%s>",pa_processTable[pa_compositionTable[dgn.comp].tableP[A]].name);
        f = Bdd_RelOpComplex(seq->f,s,TRUE);
        free(s);
        As = Pa_EnumerateProcState(
               &pa_processTable[pa_compositionTable[dgn.comp].tableP[A]],f);
        concat(msc,pa_processTable[pa_compositionTable[dgn.comp].tableP[A]].tableS[As].name);
        if (As == pa_processTable[pa_compositionTable[dgn.comp].tableP[A]].initial) {
          concat(msc,"\", textbgcolour=\"#7f7fff\"]");
        } else {
          concat(msc,"\", textbgcolour=\"#7fff7f\"]");
        }

        /* NEW STATE FOR B */
        if (A != B) {
          concat(msc,",\n  \"");
          concat(msc,pa_processTable[pa_compositionTable[dgn.comp].tableP[B]].name);
          concat(msc,"\" rbox \"");
          concat(msc,pa_processTable[pa_compositionTable[dgn.comp].tableP[B]].name);
          concat(msc,"\" [label=\"");
          s = (Est_String) malloc(255);
          sprintf(s,"Ex xA xR^<%s>",pa_processTable[pa_compositionTable[dgn.comp].tableP[B]].name);
          f = Bdd_RelOpComplex(seq->f,s,TRUE);
          free(s);
          Bs = Pa_EnumerateProcState(
                 &pa_processTable[pa_compositionTable[dgn.comp].tableP[B]],f);
          concat(msc,pa_processTable[pa_compositionTable[dgn.comp].tableP[B]].tableS[Bs].name);
          if (Bs == pa_processTable[pa_compositionTable[dgn.comp].tableP[B]].initial) {
            concat(msc,"\", textbgcolour=\"#7f7fff\"];\n");
          } else {
            concat(msc,"\", textbgcolour=\"#7fff7f\"];\n");
          }
        } else {
          concat(msc,";\n");
        }
      }

    }

    seq = seq->nextFunction;
  }
}

/**Function****************************************************************
  Synopsis    []
  Description [When diagnostic is required, model checker calls
               McPrepareDiagnostic to prepare some structures.
               Afterwards, function McPrintDiagnostic is called
               which creates textual representation of diagnostic.
               Function McPrintDiagnostic uses static function createPath,
               to produce the path. Please note that McPrintDiagnostic
               is recursive and one call of function McPrintDiagnostic
               results in many calls of function createPath.]
  SideEffects []
  SeeAlso     []
  ************************************************************************/

static void
createPath(McDiagnosticType dgn, McFunctionSequence *fseq, Est_String *path,
           Est_String *spntrl, Est_String *msc, Est_Boolean explain,
           Est_Boolean tracepath)
{
  McFunctionSequence *seq;
  Pa_Sort *sort = NULL;
  Bdd_Edge f;
  Est_String act;
  Est_String spntrlpart;
  Est_String mscpart;

  if (dgn.proc != -1) sort = &pa_sortTable[pa_processTable[dgn.proc].sort];
  if (dgn.comp != -1) sort = &pa_sortTable[pa_compositionTable[dgn.comp].sort];

  spntrlpart = NULL;
  mscpart = NULL;
  if (dgn.comp != -1) {
    createSpinTrail(dgn,fseq,sort,&spntrlpart,(strcmp(*spntrl,"") == 0));
    concat(spntrl,spntrlpart);
    createMsc(dgn,fseq,sort,&mscpart,(strcmp(*msc,"") == 0));
    concat(msc,mscpart);
  }

  seq = fseq; /*WE SHOULD NOT CHANGE fseq */
  while (seq) {
    f = Bdd_RelOpSimple(seq->f,"Ex xR",TRUE);
    if (explain && tracepath) printf("--");
    act = Pa_DecodeSortActions1(sort,f,explain&&tracepath);
    concat(path,"(");
    concat(path,act);
    concat(path,")");
    free(act);
    f = Bdd_RelOpSimple(seq->f,"Ex xA",TRUE);
    if (explain && tracepath) printf("->");
    if (dgn.proc != -1) Pa_DecodeProcessStates(&pa_processTable[dgn.proc],f,explain&&tracepath);
    if (dgn.comp != -1) Pa_DecodeCompStates(&pa_compositionTable[dgn.comp],f,explain&&tracepath);
    seq = seq->nextFunction;
  }
}

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

static void
concat(Est_String *s1, const Est_String s2)
{
  *s1 = (char*) realloc(*s1,strlen(*s1)+strlen(s2)+1);
  strcat(*s1,s2);
}

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

static void
concatInt(Est_String *s1, const int n)
{
  Est_String s2;

  s2 = (Est_String) malloc(32); /* 32 chars is enough for int */
  sprintf(s2,"%d",n);
  *s1 = (char*) realloc(*s1,strlen(*s1)+strlen(s2)+1);
  strcat(*s1,s2);
}
