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

  FileName    [mcParser.y]
  Revision    [$Revision: 77 $]
  Date        [$Date: 2013-04-29 21:10:06 +0200 (pon, 29 apr 2013) $]
  Author      [Robert Meolic (meolic@uni-mb.si)]
  Description [File  mcParser.y is a bison file for ACTLW parser.]
  SeeAlso     [mc.h, mcInt.h, mcParser.l]

  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"
#define YYERROR_VERBOSE
%}

%{
   static void concat(Est_String *s1, const Est_String s2);
   static int init(int par, Est_String name, int parserSettings);
   static Bdd_Edge findAction(Pa_Sort *s, Est_String act);
   static void outline(char *s);
   static int error(const char *s);
%}

%{
  extern int yylex(void);
  int yywrap();
  int yyerror(const char *s);
%}

%{
   int McSort = 0;
   int McProc = 0;
   int McComp = 0;
   Est_Boolean McAddFormula = FALSE;
   Est_Boolean McNotEvaluate = FALSE;
   Est_Boolean McInevitablePrepare = FALSE;
   Est_Boolean McInevitable = FALSE;
   Bdd_Edge McD = {NULL,FALSE};
   Bdd_Edge McInit = {NULL,FALSE};
   Est_String McFormulaName = NULL;
   Est_String McFileName = NULL;
   Est_String McWCAname = NULL;
   int McIdent = 0;
   Est_String McInputstring = NULL;       /* USED FOR REPORTING SYNTAX ERRORS */
   Est_String McRecognizedstring = NULL;  /* THE LAST RECOGNIZED FORMULA */
   Est_Boolean McResult = FALSE;          /* EVALUATION OF THE LAST RECOGNIZED FORMULA */
   Est_Boolean McResultX = FALSE;         /* EVALUATION OF THE LAST RECOGNIZED FORMULA */
   Bdd_Edge McResultSet = {NULL,FALSE};   /* STATES, WHERE THE LAST FORMULA IS TRUE */
   Bdd_Edge McResultSetX = {NULL,FALSE};  /* STATES, WHERE THE LAST FORMULA IS TRUE */

   Bdd_Edge McTau = {NULL,FALSE};
   McDiagnosticType McDgn
                    = {0,0,{NULL,FALSE},{NULL,FALSE},NULL,{NULL,FALSE},{NULL,FALSE}};
   McInevitableItem *inevitableLog = NULL;
   McInevitableItem *inevitableLogItem = NULL;
   McInevitableItem *inevitableLogLast = NULL;
%}

%union {
  Est_String unknown;
  Est_String outline;
  Est_String macro;
  Est_String operator;
  Est_String name;
  struct {
    Bdd_Edge f;               /* result set of states */
    Bdd_Edge fx;              /* result set of states, used by inevitable mc, only */
    McDiagnosticItem *item;   /* diagnostic */
    Est_String s;             /* input string */
    Est_String sx;            /* extended input string */
  } actlType;
  struct {
    Bdd_Edge f;               /* result set of actions */
    Est_String s;             /* input string */
  } actionType;
  struct {
    Bdd_Edge form;            /* result set of states */
    Bdd_Edge formx;           /* result set of states, used by inevitable mc, only  */
    Bdd_Edge act;             /* result set of actions */
    McDiagnosticItem *item;   /* diagnostic */
    Est_String s;             /* input string */
    Est_String sx;            /* extended input string */
  } actlActionType;
  struct {
    Est_Boolean r;            /* formula valid or not valid */
    Est_Boolean rx;           /* formula valid or not valid, used by inevitable mc, only */
    McDiagnosticItem *item;   /* diagnostic */
  } resultType;
}

%token <unknown> UNKNOWN
%token <outline> OUTLINE
%token <operator> E A UNTIL EX AX EF AF EG AG
%token <operator> EE AA UNLESS EEX AAX EEF AAF EEG AAG
%token <operator> NOT AND OR EQV IMPL
%token <name> VALTRUE VALFALSE ACTION TAU EPSILON
%type <actlType> actl std_actl unless_actl
%type <actlActionType> actl1
%type <actlActionType> actl2
%type <actionType> single_act act_form vis_act_form
%type <resultType> formula

%nonassoc IMPL
%nonassoc EQV
%left OR
%left AND
%right NOT
%right EX AX EF AF EG AG EEX AAX EEF AAF EEG AAG

%%
start     : formulas {} ;

formulas  : OUTLINE {

              Est_String tmpstr;

              if (!McNotEvaluate) {
                tmpstr = strdup($1);
                outline(tmpstr);
                free(tmpstr);
              }

              free($1);

            }

            otherformulas {} ;

          | formula {

              if (!McNotEvaluate) {

                if (diagnostic || automaton || tree) {
                  McDgn.item = $1.item;

                  /* Diagnostic should be already created by McCreateDiagnostic */
                  McPrepareDiagnostic(McDgn,McDgn.D,&McDgn.item,McDgn.init,TRUE);
                }

                if (diagnostic && $1.item) {
                  Est_String path;
                  Est_String st;
                  Est_String msc;

                  if (explain) {
                    printf("@@ Diagnostics\n");
                  }

                  path = strdup("");
                  st = strdup("");
                  msc = strdup("");
                  McPrintDiagnostic(McDgn,McDgn.item,0,&path,&st,&msc,explain,tracepath);

                  if (explain) {
                    printf("@@ ");
                  }
                  if (McDgn.item->r == FALSE) {
                    if (!strcmp(path,"")) {
                      printf("Counterexample not generated.");
                    } else {
                      printf("Counterexample: %s",path);

                      /* GENERATE SPIN TRAIL */
                      if (McDgn.comp != -1) {
                        FILE *stfile;

                        #ifdef ESTWIN32
                        stfile = fopen("C:\\Windows\\Temp\\wc.out","w");
                        #else
                        stfile = fopen("/tmp/wc.out","w");
                        #endif

                        if (!stfile) {
                        } else {
                          fprintf(stfile,"%s\n",st);
                          fclose(stfile);
                          printf("\n");
                          if (explain) {
                            printf("@@ ");
                          }
                          printf("Spin trail generated and saved into file /tmp/wc.out");
                        }
                      }

                      /* GENERATE MSC */
                      if (McDgn.comp != -1) {
                        FILE *mscfile;

                        #ifdef ESTWIN32
                        mscfile = fopen("C:\\Windows\\Temp\\wc.msc","w");
                        #else
                        mscfile = fopen("/tmp/wc.msc","w");
                        #endif

                        if (!mscfile) {
                        } else {
                          fprintf(mscfile,"# GENERATED BY EST (http://lms.uni-mb.si/EST/)\n");
                          fprintf(mscfile,"# USE mscgen TO VIEW THIS (http://www.mcternan.me.uk/mscgen/)\n");
                          fprintf(mscfile,"# mscgen -T png -o wc.png -i wc.msc\n");
                          fprintf(mscfile,"# You can rearrange the ordering of processes.\n\n");
                          fprintf(mscfile,"msc {\n");
                          fprintf(mscfile,"  hscale = \"2\";\n\n");
                          fprintf(mscfile,"%s",msc);
                          fprintf(mscfile,"}\n");
                          fclose(mscfile);
                          printf("\n");
                          if (explain) {
                            printf("@@ ");
                          }
                          printf("MSC generated and saved into file /tmp/wc.msc");
                        }
                      }

                    }
                  }
                  if (McDgn.item->r == TRUE) {
                    if (!strcmp(path,"")) {
                      printf("Witness not generated.");
                    } else {
                      printf("Witness: %s",path);

                      /* GENERATE SPIN TRAIL */
                      if (McDgn.comp != -1) {
                        FILE *stfile;

                        #ifdef ESTWIN32
                        stfile = fopen("C:\\Windows\\Temp\\wc.out","w");
                        #else
                        stfile = fopen("/tmp/wc.out","w");
                        #endif

                        if (!stfile) {
                        } else {
                          stfile = fopen("wc.out","w");
                          fprintf(stfile,"%s\n",st);
                          fclose(stfile);
                          printf("\n");
                          if (explain) {
                            printf("@@ ");
                          }
                          printf("Spin trail generated and saved into file /tmp/wc.out");
                        }
                      }

                      /* GENERATE MSC */
                      if (McDgn.comp != -1) {
                        FILE *mscfile;

                        #ifdef ESTWIN32
                        mscfile = fopen("C:\\Windows\\Temp\\wc.msc","w");
                        #else
                        mscfile = fopen("/tmp/wc.msc","w");
                        #endif

                        if (!mscfile) {
                        } else {
                          fprintf(mscfile,"# GENERATED BY EST (http://lms.uni-mb.si/EST/)\n");
                          fprintf(mscfile,"# USE mscgen TO VIEW THIS (http://www.mcternan.me.uk/mscgen/)\n");
                          fprintf(mscfile,"# mscgen -T png -o wc.png -i wc.msc\n");
                          fprintf(mscfile,"# You can rearrange the ordering of processes.\n\n");
                          fprintf(mscfile,"msc {\n");
                          fprintf(mscfile,"  hscale = \"2\";\n\n");
                          fprintf(mscfile,"%s",msc);
                          fprintf(mscfile,"}\n");
                          fclose(mscfile);
                          printf("\n");
                          if (explain) {
                            printf("@@ ");
                          }
                          printf("MSC generated and saved into file /tmp/wc.msc");
                        }
                      }

                    }
                  }
                  free(path);
                }

                if (automaton && $1.item && (McDgn.proc == -1)) {
                  int i;
                  printf("\n");
                  for (i=0; i<McIdent; i++) printf(" ");
                  printf("WARNING: WCA generation on compositions is not implemented\n");
                }

                if (automaton && $1.item && (McDgn.proc != -1)) {
                  int WCA,MINWCA;
                  int ident;

                  if (diagnostic && $1.item) {
                    printf("\n");
                  }

                  McDgn.item = $1.item;
                  McDgn.item->r = $1.r;
                  if (explain) ident = 1; else ident = 0;

                  WCA = WCAgenerator(pa_processTable[McDgn.proc].name,McWCAname,McDgn.item,ident);

                  if (WCA == -1) {
                    int i;

                    if (explain) {
                      printf("@@ ");
                    }
                    for (i=0; i<McIdent; i++) printf(" ");
                    if (McDgn.item->r == FALSE) {
                      printf("Counterexample automaton cannot be constructed.");
                    } else {
                      printf("Witness automaton cannot be constructed.");
                    }

                  } else if (WCA == -2) {
                    int i;

                    if (explain) {
                      printf("@@ ");
                    }
                    for (i=0; i<McIdent; i++) printf(" ");
                    if (McDgn.item->r == FALSE) {
                      printf("Counterexample not constructed.");
                    } else {
                      printf("Witness automaton not constructed.");
                    }

                  } else {
                    Est_Boolean OK;
                    int i;

                    OK = FALSE;
                    for(i=0; i<pa_processTable[WCA].numStates; i++) {
                      OK = OK || pa_processTable[WCA].tableS[i].final;
                    }

                    if (OK) {

                      Pa_EncodeProcess(pa_processTable[WCA].name);

                      if (explain) {
                        printf("@@ ");
                      }
                      for (i=0; i<McIdent; i++) printf(" ");
                      if (McDgn.item->r == FALSE) {
                        printf("Counterexample automaton %s has been constructed.",pa_processTable[WCA].name);
                      } else {
                        printf("Witness automaton %s has been constructed.",pa_processTable[WCA].name);
                      }
                      if (explain) {
                        Pa_WriteProcessCCS(pa_processTable[WCA].name,2);
                      } else {
                        /*
                        printf("\n");
                        Pa_WriteProcessCCS(pa_processTable[WCA].name,0);
                        */
                      }

                      if (minimize) {

                        Est_String tmp;

                        if (explain) {
                          printf("@@ ");
                        }
                        printf("\nMinimization of automaton %s",pa_processTable[WCA].name);
                        if (explain) {
                          printf("\n");
                        } else {
                          printf("... ");
                        }

                        tmp = strdup(pa_processTable[WCA].name);
                        MINWCA = Versis_Minimization(5,0,pa_processTable[WCA].name);
                        WCA = Pa_FindProcess(tmp); /* REFRESH THE NUMBER OF WCA! */
                        free(tmp);

                        Pa_EncodeProcess(pa_processTable[MINWCA].name);

                        if (explain) {
                          Pa_WriteProcessCCS(pa_processTable[MINWCA].name,2);
                        } else {
                          printf("OK");
                          /*
                          Pa_WriteProcessCCS(pa_processTable[MINWCA].name,0);
                          */
                       }
                      }

                    } else {
                      for (i=0; i<McIdent; i++) printf(" ");
                      if (McDgn.item->r == FALSE) {
                        printf("@@ There are no finite linear counterexamples.\n\n");
                      } else {
                        printf("@@ There are no finite linear witnesses.\n\n");
                      }
                      Pa_DeleteProcess(WCA);
                    }
                  }
                }

                if (tree && $1.item) {
                  if (!Bdd_isEqv(McDgn.tree,bdd_termNull)) {
                    if (Bdd_isEqv(McDgn.tree,bdd_termFalse)) {
                      printf("@@ Diagnostic tree not generated.");
                    } else {
                      printf("@@ Diagnostic tree:");
                      Pa_DecodeProcessTR(&pa_processTable[McDgn.proc],McDgn.tree,TRUE);
                    }
                  }
                }

                if ((diagnostic || automaton || tree) && explain) {
                  printf("\n@@ End Of Diagnostic\n");
                }

                if ((diagnostic || automaton || tree) && !explain) {
                  printf("\n");
                }

                if (diagnostic || automaton || tree) {
                  /* DELETE DIAGNOSTICS - WE DO NOT NEED IT ANYMORE */
                  McDeleteDiagnostic(McDgn.item);
                  /* CREATE NEW EMPTY DIAGNOSTICS */
                  /* WE NEED THIS, BECAUSE MORE FORMULAE MAY FOLLOW */
                  McDgn = McCreateDiagnostic(McD,McInit,McProc,McComp);
                }
              }

              if (McInputstring) {
                McInputstring = NULL;
              }
            }

            otherformulas {} ;

otherformulas : | {}
                formulas {} ;

formula   : actl ';' {

              Bdd_Edge tmp;

              if (McAddFormula) {
                Est_String f;
                f = (Est_String) malloc(strlen($1.s)+2);
                sprintf(f,"%s;",$1.s);
                if (!McFormulaName) {
                  if (!McFileName) {
                    McFormulaName = strdup("");
                  } else {
                    int i,j;
                    /* remove full path */
                    i = strlen(McFileName);
                    while (i>0 && McFileName[i] != '\\' && McFileName[i] != '/') i--;
                    if (McFileName[i] == '\\' || McFileName[i] == '/') i++;
                    /* remove extension after the first dot */
                    j = i;
                    while (j<strlen(McFileName) && McFileName[j] != '.') j++;
                    McFormulaName = strndup(&McFileName[i],j-i);
                    concat(&McFormulaName,"_");
                  }
                  concat(&McFormulaName,"F");
                  Mc_FOANextFormula(f,McFormulaName);
                  free(McFormulaName);
                  McFormulaName = NULL;
                } else {
                  Mc_AddNewFormula(McFormulaName,f);
                }

                free(f);
              }

              if (!McNotEvaluate) {

                if (!McInevitable) {
                  int i;

                  printf("\n");
                  for (i=0; i<McIdent; i++) printf(" ");
                  tmp = Bdd_ITE(McInit,$1.f,bdd_termFalse);
                  if (Bdd_isEqv(tmp,bdd_termFalse)) {
                    $$.r = FALSE;
                    if (xtrace) {
                      printf("%s ==> FALSE\n",$1.sx);
                    } else {
                      printf("%s ==> FALSE\n",$1.s);
                    }
                  } else {
                    $$.r = TRUE;
                    if (xtrace) {
                      printf("%s ==> TRUE\n",$1.sx);
                    } else {
                      printf("%s ==> TRUE\n",$1.s);
                    }
                  }
                  $$.item = $1.item;
                  McResult = $$.r;
                  McResultSet = $1.f;

                } else {

                  tmp = Bdd_ITE(McInit,$1.f,bdd_termFalse);
                  if (Bdd_isEqv(tmp,bdd_termFalse)) {
                    $$.r = FALSE;
                  } else {
                    $$.r = TRUE;
                  }

                  tmp = Bdd_ITE(McInit,$1.fx,bdd_termFalse);
                  if (Bdd_isEqv(tmp,bdd_termFalse)) {
                    $$.rx = FALSE;
                  } else {
                    $$.rx = TRUE;
                  }

                  McResult = $$.r;
                  McResultX = $$.rx;
                  McResultSet = $1.f;
                  McResultSetX = $1.fx;

                }

              }

              if (xtrace) {
                McRecognizedstring = strdup($1.sx);
              } else {
                McRecognizedstring = strdup($1.s);
              }

              free($1.s);
              free($1.sx);
            }

            | error ';' {
                yyerrok;
            } ;

actl      : UNKNOWN {
              Est_String tmpstr;

              tmpstr = (Est_String) malloc(127);
              sprintf(tmpstr,"unknown symbol %s",$1);
              error(tmpstr);
              free(tmpstr);
              free($1);
              YYERROR;
            } ;

          | VALTRUE {

              Bdd_Edge result;

              $$.s = strdup($1);
              $$.sx = strdup($1);
              McInputstring = $$.s;

              if (trace) printf(">> %s\n",$$.s);
              /*
              if (xtrace) printf("X> %s\n",$$.sx);
              */

              if (McInevitablePrepare) {

                /* printf("PREPARE> %s\n",$$.s); */

                inevitableLogItem = McAddEmptyInevitable($$.s,$$.sx);
                if (!inevitableLogLast) {
                  inevitableLog = inevitableLogLast = inevitableLogItem;
                } else {
                  inevitableLogLast = inevitableLogLast->next = inevitableLogItem;
                }

              }

              if (!McNotEvaluate) {

                if (McInevitable) {

                  /* fprintf(stderr,"McInevitable: %s\n",inevitableLogLast->sx); */

                  $$.f = bdd_termTrue;
                  $$.fx = bdd_termFalse;

                  inevitableLogLast = inevitableLogLast->next;

                } else {

                  result = bdd_termTrue;
                  $$.f = result;

                  if (diagnostic || tree || automaton) {
                    McAddDiagnostic(&$$.item,result,bdd_termNull,bdd_termTrue,
                                  bdd_termNull,bdd_termNull,MC_CONST,
                                  $$.s,$$.sx,NULL,NULL);
                  }

                }
              }

              free($1);
            } ;

          | VALFALSE {

              Bdd_Edge result;

              $$.s = strdup($1);
              $$.sx = strdup($1);
              McInputstring = $$.s;

              if (trace) printf(">> %s\n",$$.s);
              /*
              if (xtrace) printf("X> %s\n",$$.sx);
              */

              if (McInevitablePrepare) {

                /* printf("PREPARE> %s\n",$$.s); */

                inevitableLogItem = McAddEmptyInevitable($$.s,$$.sx);
                if (!inevitableLogLast) {
                  inevitableLog = inevitableLogLast = inevitableLogItem;
                } else {
                  inevitableLogLast = inevitableLogLast->next = inevitableLogItem;
                }

              }

              if (!McNotEvaluate) {

                if (McInevitable) {

                  /* fprintf(stderr,"McInevitable: %s\n",inevitableLogLast->sx); */

                  $$.f = bdd_termFalse;
                  $$.fx = bdd_termTrue;

                  inevitableLogLast = inevitableLogLast->next;

                } else {

                  result = bdd_termFalse;
                  $$.f = result;

                  if (diagnostic || tree || automaton) {
                    McAddDiagnostic(&$$.item,result,bdd_termNull,bdd_termFalse,
                                  bdd_termNull,bdd_termNull,MC_CONST,
                                  $$.s,$$.sx,NULL,NULL);
                  }

                }
              }

              free($1);
            } ;

          | NOT actl {

              Bdd_Edge result;

              $$.s = (Est_String) malloc(1024);
              $$.sx = (Est_String) malloc(1024);
              sprintf($$.s,"NOT %s",$2.s);
              sprintf($$.sx,"NOT %s",$2.sx);
              McInputstring = $$.s;

              if (trace) printf(">> %s\n",$$.s);
              /*
              if (xtrace) printf("X> %s\n",$$.sx);
              */

              if (McInevitablePrepare) {

                /* printf("PREPARE> %s\n",$$.s); */
                inevitableLogItem = McAddEmptyInevitable($$.s,$$.sx);
                inevitableLogLast = inevitableLogLast->next = inevitableLogItem;

              }

              if (!McNotEvaluate) {

                if (McInevitable) {

                  /* fprintf(stderr,"McInevitable: %s\n",inevitableLogLast->sx); */

                  $$.f = $2.fx;
                  $$.fx = $2.f;

                  inevitableLogLast = inevitableLogLast->next;

                } else {

                  result = Bdd_NOT($2.f); /* CAREFULLY! */
                  Bdd_Fortify(result);
                  $$.f = result;

                  if (diagnostic || tree || automaton) {
                    McAddDiagnostic(&$$.item,result,bdd_termNull,$2.f,
                                  bdd_termNull,bdd_termNull,MC_NOT,
                                  $$.s,$$.sx,NULL,$2.item);
                  }

                }
              }

              free($2.s);
              free($2.sx);
            } ;

          | actl AND actl {

              Bdd_Edge result;

              $$.s = (Est_String) malloc(1024);
              $$.sx = (Est_String) malloc(1024);
              sprintf($$.s,"%s AND %s",$1.s,$3.s);
              sprintf($$.sx,"%s AND %s",$1.sx,$3.sx);
              McInputstring = $$.s;

              if (trace) printf(">> %s\n",$$.s);
              /*
              if (xtrace) printf("X> %s\n",$$.sx);
              */

              if (McInevitablePrepare) {

                /* printf("PREPARE> %s\n",$$.s); */
                inevitableLogItem = McAddEmptyInevitable($$.s,$$.sx);
                inevitableLogLast = inevitableLogLast->next = inevitableLogItem;

              }

              if (!McNotEvaluate) {

                if (McInevitable) {

                  /* fprintf(stderr,"McInevitable: %s\n",inevitableLogLast->sx); */

                  result = Bdd_ITE($1.f,$3.f,bdd_termFalse);
                  Bdd_Fortify(result);
                  $$.f = result;

                  result = Bdd_ITE($1.fx,bdd_termTrue,$3.fx);
                  Bdd_Fortify(result);
                  $$.fx = result;

                  inevitableLogLast = inevitableLogLast->next;

                } else {

                  result = Bdd_ITE($1.f,$3.f,bdd_termFalse);
                  Bdd_Fortify(result);
                  $$.f = result;

                  if (diagnostic || tree || automaton) {
                    McAddDiagnostic(&$$.item,result,bdd_termNull,$1.f,
                                  bdd_termNull,$3.f,MC_AND,
                                  $$.s,$$.sx,$1.item,$3.item);
                  }

                }
              }

              free($1.s);
              free($1.sx);
              free($3.s);
              free($3.sx);
            } ;

          | actl OR actl {

              Bdd_Edge result;

              $$.s = (Est_String) malloc(1024);
              $$.sx = (Est_String) malloc(1024);
              sprintf($$.s,"%s OR %s",$1.s,$3.s);
              sprintf($$.sx,"%s OR %s",$1.sx,$3.sx);
              McInputstring = $$.s;

              if (trace) printf(">> %s\n",$$.s);
              /*
              if (xtrace) printf("X> %s\n",$$.sx);
              */

              if (McInevitablePrepare) {

                /* printf("PREPARE> %s\n",$$.s); */
                inevitableLogItem = McAddEmptyInevitable($$.s,$$.sx);
                inevitableLogLast = inevitableLogLast->next = inevitableLogItem;

              }

              if (!McNotEvaluate) {

                if (McInevitable) {

                  /* fprintf(stderr,"McInevitable: %s\n",inevitableLogLast->sx); */

                  result = Bdd_ITE($1.f,bdd_termTrue,$3.f);
                  Bdd_Fortify(result);
                  $$.f = result;

                  result = Bdd_ITE($1.fx,$3.fx,bdd_termFalse);
                  Bdd_Fortify(result);
                  $$.fx = result;

                  inevitableLogLast = inevitableLogLast->next;

                } else {

                  result = Bdd_ITE($1.f,bdd_termTrue,$3.f);
                  Bdd_Fortify(result);
                  $$.f = result;

                  if (diagnostic || tree || automaton) {
                    McAddDiagnostic(&$$.item,result,bdd_termNull,$1.f,
                                  bdd_termNull,$3.f,MC_OR,
                                  $$.s,$$.sx,$1.item,$3.item);
                  }

                }
              }

              free($1.s);
              free($1.sx);
              free($3.s);
              free($3.sx);
            } ;

          | actl EQV actl {

              Bdd_Edge result;

              $$.s = (Est_String) malloc(1024);
              $$.sx = (Est_String) malloc(1024);
              sprintf($$.s,"%s EQV %s",$1.s,$3.s);
              sprintf($$.sx,"%s EQV %s",$1.sx,$3.sx);
              McInputstring = $$.s;

              if (trace) printf(">> %s\n",$$.s);
              /*
              if (xtrace) printf("X> %s\n",$$.sx);
              */

              if (McInevitablePrepare) {

                /* printf("PREPARE> %s\n",$$.s); */
                inevitableLogItem = McAddEmptyInevitable($$.s,$$.sx);
                inevitableLogLast = inevitableLogLast->next = inevitableLogItem;

              }

              if (!McNotEvaluate) {

                if (McInevitable) {

                  /* fprintf(stderr,"McInevitable: %s\n",inevitableLogLast->sx); */

                  result = Bdd_ITE(Bdd_ITE($1.f,$3.f,bdd_termFalse),
                                   bdd_termTrue,
                                   Bdd_ITE($1.fx,$3.fx,bdd_termFalse));
                  Bdd_Fortify(result);
                  $$.f = result;

                  result = Bdd_ITE(Bdd_ITE($1.f,$3.fx,bdd_termFalse),
                                   bdd_termTrue,
                                   Bdd_ITE($1.fx,$3.f,bdd_termFalse));
                  Bdd_Fortify(result);
                  $$.fx = result;

                  inevitableLogLast = inevitableLogLast->next;

                } else {

                  result = Bdd_ITE($1.f,$3.f,Bdd_NOT($3.f));
                  Bdd_Fortify(result);
                  $$.f = result;

                  if (diagnostic || tree || automaton) {
                    McAddDiagnostic(&$$.item,result,bdd_termNull,$1.f,
                                  bdd_termNull,$3.f,MC_EQV,
                                  $$.s,$$.sx,$1.item,$3.item);
                  }

                }
              }

              free($1.s);
              free($1.sx);
              free($3.s);
              free($3.sx);
            } ;

          | actl IMPL actl {

              Bdd_Edge result;

              $$.s = (Est_String) malloc(1024);
              $$.sx = (Est_String) malloc(1024);
              sprintf($$.s,"%s IMPL %s",$1.s,$3.s);
              sprintf($$.sx,"%s IMPL %s",$1.sx,$3.sx);
              McInputstring = $$.s;

              if (trace) printf(">> %s\n",$$.s);
              /*
              if (xtrace) printf("X> %s\n",$$.sx);
              */

              if (McInevitablePrepare) {

                /* printf("PREPARE> %s\n",$$.s); */
                inevitableLogItem = McAddEmptyInevitable($$.s,$$.sx);
                inevitableLogLast = inevitableLogLast->next = inevitableLogItem;

              }

              if (!McNotEvaluate) {

                if (McInevitable) {

                  /* fprintf(stderr,"McInevitable: %s\n",inevitableLogLast->sx); */

                  result = Bdd_ITE($1.fx,bdd_termTrue,$3.f);
                  Bdd_Fortify(result);
                  $$.f = result;

                  result = Bdd_ITE($1.f,$3.fx,bdd_termFalse);
                  Bdd_Fortify(result);
                  $$.fx = result;

                  inevitableLogLast = inevitableLogLast->next;

                } else {

                  result = Bdd_ITE($1.f,$3.f,bdd_termTrue);
                  Bdd_Fortify(result);
                  $$.f = result;

                  if (diagnostic || tree || automaton) {
                    McAddDiagnostic(&$$.item,result,bdd_termNull,$1.f,
                                  bdd_termNull,$3.f,MC_IMPL,
                                  $$.s,$$.sx,$1.item,$3.item);
                  }

                }
              }

              free($1.s);
              free($1.sx);
              free($3.s);
              free($3.sx);
            } ;

          | '(' actl ')' {

              $$.s = (Est_String) malloc(1024);
              $$.sx = (Est_String) malloc(1024);
              sprintf($$.s,"(%s)",$2.s);
              sprintf($$.sx,"(%s)",$2.sx);
              McInputstring = $$.s;

              if (trace) printf(">> %s\n",$$.s);
              /*
              if (xtrace) printf("X> %s\n",$$.sx);
              */

              if (!McNotEvaluate) {
                $$.f = $2.f;
                $$.item = $2.item;
              }

              free($2.s);
              free($2.sx);

            } ;

          | std_actl {

              $$.s = strdup($1.s);
              $$.sx = strdup($1.sx);
              McInputstring = $$.s;

              if (!McNotEvaluate) {
                $$.f = $1.f;
                $$.item = $1.item;
              }

              free($1.s);
              free($1.sx);
            } ;

          | unless_actl {

              $$.s = strdup($1.s);
              $$.sx = strdup($1.sx);
              McInputstring = $$.s;

              if (!McNotEvaluate) {
                $$.f = $1.f;
                $$.item = $1.item;
              }

              free($1.s);
              free($1.sx);

            } ;

std_actl  : E '[' actl '{' vis_act_form '}' UNTIL '{' vis_act_form '}' actl ']' {

              Bdd_Edge act1,act2,form1,form2,form1x,form2x,result;

              $$.s = (Est_String) malloc(1024);
              $$.sx = (Est_String) malloc(1024);
              sprintf($$.s,"E[%s {%s}U{%s} %s]",$3.s,$5.s,$9.s,$11.s);
              sprintf($$.sx,"E[%s {%s}U{%s} %s]",$3.sx,$5.s,$9.s,$11.sx);
              McInputstring = $$.s;

              if (trace) printf(">> %s\n",$$.s);
              /*
              if (xtrace) printf("X> %s\n",$$.sx);
              */

              if (McInevitablePrepare) {

                /* printf("PREPARE> %s\n",$$.s); */
                inevitableLogItem = McAddEmptyInevitable($$.s,$$.sx);
                inevitableLogLast = inevitableLogLast->next = inevitableLogItem;
                inevitableLogLast->inevitableT = bdd_termFalse;
                inevitableLogLast->inevitableT1 = bdd_termFalse;
                inevitableLogLast->inevitableF = bdd_termFalse;
                inevitableLogLast->inevitableF1 = bdd_termFalse;

              }

              if (!McNotEvaluate) {
                act1 = $5.f;
                form1 = $3.f;
                act2 = $9.f;
                form2 = $11.f;

                if (McInevitable) {

                  form1x = $3.fx;
                  form2x = $11.fx;

                  /* fprintf(stderr,"McInevitable: %s\n",inevitableLogLast->sx); */

                  Mc_InevitableCheckEU(McComp,
                    &inevitableLogLast->inevitableT,&inevitableLogLast->inevitableF,
                    &inevitableLogLast->inevitableT1,&inevitableLogLast->inevitableF1,
                    form1,form1x,act1,act2,form2,form2x);

                  $$.f = inevitableLogLast->inevitableT;
                  $$.fx = inevitableLogLast->inevitableF;

                  inevitableLogLast = inevitableLogLast->next;

                } else {

                  result = Mc_CheckEU(McD,form1,act1,act2,form2);
                  $$.f = result;

                  if (diagnostic || tree || automaton) {
                    McAddDiagnostic(&$$.item,result,
                                  act1,form1,act2,form2,MC_EU,$$.s,$$.sx,
                                  $3.item,$11.item);
                  }

                }
              }

              free($3.s);
              free($3.sx);
              free($5.s);
              free($9.s);
              free($11.s);
              free($11.sx);
            } ;

          | E '[' actl '{' vis_act_form '}' UNTIL actl ']' {

              Bdd_Edge act1,act2,form1,form2,form1x,form2x,result;

              $$.s = (Est_String) malloc(1024);
              $$.sx = (Est_String) malloc(1024);
              sprintf($$.s,"E[%s {%s}U %s]",$3.s,$5.s,$8.s);
              sprintf($$.sx,"E[%s {%s}U %s]",$3.sx,$5.s,$8.sx);
              McInputstring = $$.s;

              if (trace) printf(">> %s\n",$$.s);
              /*
              if (xtrace) printf("X> %s\n",$$.sx);
              */

              if (McInevitablePrepare) {

                /* printf("PREPARE> %s\n",$$.s); */
                inevitableLogItem = McAddEmptyInevitable($$.s,$$.sx);
                inevitableLogLast = inevitableLogLast->next = inevitableLogItem;
                inevitableLogLast->inevitableT = bdd_termFalse;
                inevitableLogLast->inevitableT1 = bdd_termFalse;
                inevitableLogLast->inevitableF = bdd_termFalse;
                inevitableLogLast->inevitableF1 = bdd_termFalse;

              }

              if (!McNotEvaluate) {
                act1 = $5.f;
                form1 = $3.f;
                act2 = bdd_termNull;
                form2 = $8.f;

                if (McInevitable) {

                  form1x = $3.fx;
                  form2x = $8.fx;

                  /* fprintf(stderr,"McInevitable: %s\n",inevitableLogLast->sx); */

                  Mc_InevitableCheckEU(McComp,
                    &inevitableLogLast->inevitableT,&inevitableLogLast->inevitableF,
                    &inevitableLogLast->inevitableT1,&inevitableLogLast->inevitableF1,
                    form1,form1x,act1,act2,form2,form2x);

                  $$.f = inevitableLogLast->inevitableT;
                  $$.fx = inevitableLogLast->inevitableF;

                  inevitableLogLast = inevitableLogLast->next;

                } else {

                  result = Mc_CheckEU(McD,form1,act1,act2,form2);
                  $$.f = result;

                  if (diagnostic || tree || automaton) {
                    McAddDiagnostic(&$$.item,result,
                                  act1,form1,act2,form2,MC_EU,$$.s,$$.sx,
                                  $3.item,$8.item);
                  }

                }
              }

              free($3.s);
              free($3.sx);
              free($5.s);
              free($8.s);
              free($8.sx);
            } ;

          | E '[' actl UNTIL actl ']' {

              Bdd_Edge act1,act2,form1,form2,form1x,form2x,result;

              $$.s = (Est_String) malloc(1024);
              $$.sx = (Est_String) malloc(1024);
              sprintf($$.s,"E[%s U %s]",$3.s,$5.s);
              sprintf($$.sx,"E[%s U %s]",$3.sx,$5.sx);
              McInputstring = $$.s;

              if (trace) printf(">> %s\n",$$.s);
              /*
              if (xtrace) printf("X> %s\n",$$.sx);
              */

              if (McInevitablePrepare) {

                /* printf("PREPARE> %s\n",$$.s); */
                inevitableLogItem = McAddEmptyInevitable($$.s,$$.sx);
                inevitableLogLast = inevitableLogLast->next = inevitableLogItem;
                inevitableLogLast->inevitableT = bdd_termFalse;
                inevitableLogLast->inevitableT1 = bdd_termFalse;
                inevitableLogLast->inevitableF = bdd_termFalse;
                inevitableLogLast->inevitableF1 = bdd_termFalse;

              }

              if (!McNotEvaluate) {
                act1 = bdd_termTrue;
                form1 = $3.f;
                act2 = bdd_termNull;
                form2 = $5.f;

                if (McInevitable) {

                  form1x = $3.fx;
                  form2x = $5.fx;

                  /* fprintf(stderr,"McInevitable: %s\n",inevitableLogLast->sx); */

                  Mc_InevitableCheckEU(McComp,
                    &inevitableLogLast->inevitableT,&inevitableLogLast->inevitableF,
                    &inevitableLogLast->inevitableT1,&inevitableLogLast->inevitableF1,
                    form1,form1x,act1,act2,form2,form2x);

                  $$.f = inevitableLogLast->inevitableT;
                  $$.fx = inevitableLogLast->inevitableF;

                  inevitableLogLast = inevitableLogLast->next;

                } else {

                  result = Mc_CheckEU(McD,form1,act1,act2,form2);
                  $$.f = result;

                  if (diagnostic || tree || automaton) {
                    McAddDiagnostic(&$$.item,result,
                                  act1,form1,act2,form2,MC_EU,$$.s,$$.sx,
                                  $3.item,$5.item);
                  }

                }
              }

              free($3.s);
              free($3.sx);
              free($5.s);
              free($5.sx);
            } ;

          | A '[' actl '{' vis_act_form '}' UNTIL '{' vis_act_form '}' actl ']' {

              Bdd_Edge act1,act2,form1,form2,form1x,form2x,result;

              $$.s = (Est_String) malloc(1024);
              $$.sx = (Est_String) malloc(1024);
              sprintf($$.s,"A[%s {%s}U{%s} %s]",$3.s,$5.s,$9.s,$11.s);
              sprintf($$.sx,"A[%s {%s}U{%s} %s]",$3.sx,$5.s,$9.s,$11.sx);
              McInputstring = $$.s;

              if (trace) printf(">> %s\n",$$.s);
              /*
              if (xtrace) printf("X> %s\n",$$.sx);
              */

              if (McInevitablePrepare) {

                /* printf("PREPARE> %s\n",$$.s); */
                inevitableLogItem = McAddEmptyInevitable($$.s,$$.sx);
                inevitableLogLast = inevitableLogLast->next = inevitableLogItem;
                inevitableLogLast->inevitableT = bdd_termFalse;
                inevitableLogLast->inevitableT1 = bdd_termFalse;
                inevitableLogLast->inevitableT2 = bdd_termFalse;
                inevitableLogLast->inevitableF = bdd_termFalse;
                inevitableLogLast->inevitableF1 = bdd_termFalse;
                inevitableLogLast->inevitableF2 = bdd_termFalse;

              }

              if (!McNotEvaluate) {
                act1 = $5.f;
                form1 = $3.f;
                act2 = $9.f;
                form2 = $11.f;

                if (McInevitable) {

                  form1x = $3.fx;
                  form2x = $11.fx;

                  /* fprintf(stderr,"McInevitable: %s\n",inevitableLogLast->sx); */

                  Mc_InevitableCheckAU(McComp,
                    &inevitableLogLast->inevitableT,&inevitableLogLast->inevitableF,
                    &inevitableLogLast->inevitableT1,&inevitableLogLast->inevitableF1,
                    &inevitableLogLast->inevitableT2,&inevitableLogLast->inevitableF2,
                    form1,form1x,act1,act2,form2,form2x);

                  $$.f = inevitableLogLast->inevitableT;
                  $$.fx = inevitableLogLast->inevitableF;

                  inevitableLogLast = inevitableLogLast->next;

                } else {

                  result = Mc_CheckAU(McD,form1,act1,act2,form2);
                  $$.f = result;

                  if (diagnostic || tree || automaton) {
                    McAddDiagnostic(&$$.item,result,
                                  act1,form1,act2,form2,MC_AU,$$.s,$$.sx,
                                  $3.item,$11.item);
                  }

                }
              }

              free($3.s);
              free($3.sx);
              free($5.s);
              free($9.s);
              free($11.s);
              free($11.sx);
            } ;

          | A '[' actl '{' vis_act_form '}' UNTIL actl ']' {

              Bdd_Edge act1,act2,form1,form2,form1x,form2x,result;

              $$.s = (Est_String) malloc(1024);
              $$.sx = (Est_String) malloc(1024);
              sprintf($$.s,"A[%s {%s}U %s]",$3.s,$5.s,$8.s);
              sprintf($$.sx,"A[%s {%s}U %s]",$3.sx,$5.s,$8.sx);
              McInputstring = $$.s;

              if (trace) printf(">> %s\n",$$.s);
              /*
              if (xtrace) printf("X> %s\n",$$.sx);
              */

              if (McInevitablePrepare) {

                /* printf("PREPARE> %s\n",$$.s); */
                inevitableLogItem = McAddEmptyInevitable($$.s,$$.sx);
                inevitableLogLast = inevitableLogLast->next = inevitableLogItem;
                inevitableLogLast->inevitableT = bdd_termFalse;
                inevitableLogLast->inevitableT1 = bdd_termFalse;
                inevitableLogLast->inevitableT2 = bdd_termFalse;
                inevitableLogLast->inevitableF = bdd_termFalse;
                inevitableLogLast->inevitableF1 = bdd_termFalse;
                inevitableLogLast->inevitableF2 = bdd_termFalse;

              }

              if (!McNotEvaluate) {
                act1 = $5.f;
                form1 = $3.f;
                act2 = bdd_termNull;
                form2 = $8.f;

                if (McInevitable) {

                  form1x = $3.fx;
                  form2x = $8.fx;

                  /* fprintf(stderr,"McInevitable: %s\n",inevitableLogLast->sx); */

                  Mc_InevitableCheckAU(McComp,
                    &inevitableLogLast->inevitableT,&inevitableLogLast->inevitableF,
                    &inevitableLogLast->inevitableT1,&inevitableLogLast->inevitableF1,
                    &inevitableLogLast->inevitableT2,&inevitableLogLast->inevitableF2,
                    form1,form1x,act1,act2,form2,form2x);

                  $$.f = inevitableLogLast->inevitableT;
                  $$.fx = inevitableLogLast->inevitableF;

                  inevitableLogLast = inevitableLogLast->next;

                } else {

                  result = Mc_CheckAU(McD,form1,act1,act2,form2);
                  $$.f = result;

                  if (diagnostic || tree || automaton) {
                    McAddDiagnostic(&$$.item,result,
                                  act1,form1,act2,form2,MC_AU,$$.s,$$.sx,
                                  $3.item,$8.item);
                  }

                }
              }

              free($3.s);
              free($3.sx);
              free($5.s);
              free($8.s);
              free($8.sx);
            } ;

          | A '[' actl UNTIL actl ']' {

              Bdd_Edge act1,act2,form1,form2,form1x,form2x,result;

              $$.s = (Est_String) malloc(1024);
              $$.sx = (Est_String) malloc(1024);
              sprintf($$.s,"A[%s U %s]",$3.s,$5.s);
              sprintf($$.sx,"A[%s U %s]",$3.sx,$5.sx);
              McInputstring = $$.s;

              if (trace) printf(">> %s\n",$$.s);
              /*
              if (xtrace) printf("X> %s\n",$$.sx);
              */

              if (McInevitablePrepare) {

                /* printf("PREPARE> %s\n",$$.s); */
                inevitableLogItem = McAddEmptyInevitable($$.s,$$.sx);
                inevitableLogLast = inevitableLogLast->next = inevitableLogItem;
                inevitableLogLast->inevitableT = bdd_termFalse;
                inevitableLogLast->inevitableT1 = bdd_termFalse;
                inevitableLogLast->inevitableT2 = bdd_termFalse;
                inevitableLogLast->inevitableF = bdd_termFalse;
                inevitableLogLast->inevitableF1 = bdd_termFalse;
                inevitableLogLast->inevitableF2 = bdd_termFalse;

              }

              if (!McNotEvaluate) {
                act1 = bdd_termTrue;
                form1 = $3.f;
                act2 = bdd_termNull;
                form2 = $5.f;

                if (McInevitable) {

                  form1x = $3.fx;
                  form2x = $5.fx;

                  /* fprintf(stderr,"McInevitable: %s\n",inevitableLogLast->sx); */

                  Mc_InevitableCheckAU(McComp,
                    &inevitableLogLast->inevitableT,&inevitableLogLast->inevitableF,
                    &inevitableLogLast->inevitableT1,&inevitableLogLast->inevitableF1,
                    &inevitableLogLast->inevitableT2,&inevitableLogLast->inevitableF2,
                    form1,form1x,act1,act2,form2,form2x);

                  $$.f = inevitableLogLast->inevitableT;
                  $$.fx = inevitableLogLast->inevitableF;

                  inevitableLogLast = inevitableLogLast->next;

                } else {

                  result = Mc_CheckAU(McD,form1,act1,act2,form2);
                  $$.f = result;

                  if (diagnostic || tree || automaton) {
                    McAddDiagnostic(&$$.item,result,
                                  act1,form1,act2,form2,MC_AU,$$.s,$$.sx,
                                  $3.item,$5.item);
                  }

                }
              }

              free($3.s);
              free($3.sx);
              free($5.s);
              free($5.sx);
            } ;

          | EX '{' vis_act_form '}' actl {

              Bdd_Edge act2,form2,form2x,result;

              $$.s = (Est_String) malloc(1024);
              $$.sx = (Est_String) malloc(1024);
              sprintf($$.s,"EX{%s} %s",$3.s,$5.s);
              sprintf($$.sx,"EX{%s} %s",$3.s,$5.sx);
              McInputstring = $$.s;

              if (trace) printf(">> %s\n",$$.s);
              /*
              if (xtrace) printf("X> %s\n",$$.sx);
              */

              if (McInevitablePrepare) {

                /* printf("PREPARE> %s\n",$$.s); */
                inevitableLogItem = McAddEmptyInevitable($$.s,$$.sx);
                inevitableLogLast = inevitableLogLast->next = inevitableLogItem;
                inevitableLogLast->inevitableT = bdd_termFalse;
                inevitableLogLast->inevitableF = bdd_termFalse;

              }

              if (!McNotEvaluate) {
                act2 = $3.f;
                form2 = $5.f;

                if (McInevitable) {

                  form2x = $5.fx;

                  /* fprintf(stderr,"McInevitable: %s\n",inevitableLogLast->sx); */

                  Mc_InevitableCheckEX(McComp,
                    &inevitableLogLast->inevitableT,&inevitableLogLast->inevitableF,
                    act2,form2,form2x);

                  $$.f = inevitableLogLast->inevitableT;
                  $$.fx = inevitableLogLast->inevitableF;

                  inevitableLogLast = inevitableLogLast->next;

                } else {

                  result = Mc_CheckEX(McD,act2,form2);
                  $$.f = result;

                  if (diagnostic || tree || automaton) {
                    McAddDiagnostic(&$$.item,result,bdd_termNull,bdd_termNull,
                                 act2,form2,MC_EX,$$.s,$$.sx,NULL,$5.item);
                  }

                }
              }

              free($3.s);
              free($5.s);
              free($5.sx);

            } ;

          | EX '{' TAU '}' actl {

              Bdd_Edge act2,form2,form2x,result;

              $$.s = (Est_String) malloc(1024);
              $$.sx = (Est_String) malloc(1024);
              sprintf($$.s,"EX{TAU} %s",$5.s);
              sprintf($$.sx,"EX{TAU} %s",$5.sx);
              McInputstring = $$.s;

              if (trace) printf(">> %s\n",$$.s);
              /*
              if (xtrace) printf("X> %s\n",$$.sx);
              */

              if (McInevitablePrepare) {

                /* printf("PREPARE> %s\n",$$.s); */
                inevitableLogItem = McAddEmptyInevitable($$.s,$$.sx);
                inevitableLogLast = inevitableLogLast->next = inevitableLogItem;
                inevitableLogLast->inevitableT = bdd_termFalse;
                inevitableLogLast->inevitableF = bdd_termFalse;

              }

              if (!McNotEvaluate) {
                act2 = McTau;
                form2 = $5.f;

                if (McInevitable) {

                  form2x = $5.fx;

                  /* fprintf(stderr,"McInevitable: %s\n",inevitableLogLast->sx); */

                  Mc_InevitableCheckEX(McComp,
                    &inevitableLogLast->inevitableT,&inevitableLogLast->inevitableF,
                    act2,form2,form2x);

                  $$.f = inevitableLogLast->inevitableT;
                  $$.fx = inevitableLogLast->inevitableF;

                  inevitableLogLast = inevitableLogLast->next;

                } else {

                  result = Mc_CheckEX(McD,act2,form2);
                  $$.f = result;

                  if (diagnostic || tree || automaton) {
                    McAddDiagnostic(&$$.item,result,bdd_termNull,bdd_termNull,
                                 act2,form2,MC_EX,$$.s,$$.sx,NULL,$5.item);
                  }

                }
              }

              free($3);
              free($5.s);
              free($5.sx);
            } ;

          | AX '{' vis_act_form '}' actl {

              Bdd_Edge act2,form2,form2x,result;

              $$.s = (Est_String) malloc(1024);
              $$.sx = (Est_String) malloc(1024);
              sprintf($$.s,"AX{%s} %s",$3.s,$5.s);
              sprintf($$.sx,"AX{%s} %s",$3.s,$5.sx);
              McInputstring = $$.s;

              if (trace) printf(">> %s\n",$$.s);
              /*
              if (xtrace) printf("X> %s\n",$$.sx);
              */

              if (McInevitablePrepare) {

                /* printf("PREPARE> %s\n",$$.s); */
                inevitableLogItem = McAddEmptyInevitable($$.s,$$.sx);
                inevitableLogLast = inevitableLogLast->next = inevitableLogItem;
                inevitableLogLast->inevitableT = bdd_termFalse;
                inevitableLogLast->inevitableF = bdd_termFalse;

              }

              if (!McNotEvaluate) {
                act2 = $3.f;
                form2 = $5.f;

                if (McInevitable) {

                  form2x = $5.fx;

                  /* fprintf(stderr,"McInevitable: %s\n",inevitableLogLast->sx); */

                  Mc_InevitableCheckAX(McComp,
                    &inevitableLogLast->inevitableT,&inevitableLogLast->inevitableF,
                    act2,form2,form2x);

                  $$.f = inevitableLogLast->inevitableT;
                  $$.fx = inevitableLogLast->inevitableF;

                  inevitableLogLast = inevitableLogLast->next;

                } else {

                  result = Mc_CheckAX(McD,act2,form2);
                  $$.f = result;

                  if (diagnostic || tree || automaton) {
                    McAddDiagnostic(&$$.item,result,bdd_termNull,bdd_termNull,
                                 act2,form2,MC_AX,$$.s,$$.sx,NULL,$5.item);
                  }

                }
              }

              free($3.s);
              free($5.s);
              free($5.sx);
            } ;

          | AX '{' TAU '}' actl {

              Bdd_Edge act2,form2,form2x,result;

              $$.s = (Est_String) malloc(1024);
              $$.sx = (Est_String) malloc(1024);
              sprintf($$.s,"AX{TAU} %s",$5.s);
              sprintf($$.sx,"AX{TAU} %s",$5.sx);
              McInputstring = $$.s;

              if (trace) printf(">> %s\n",$$.s);
              /*
              if (xtrace) printf("X> %s\n",$$.sx);
              */

              if (McInevitablePrepare) {

                /* printf("PREPARE> %s\n",$$.s); */
                inevitableLogItem = McAddEmptyInevitable($$.s,$$.sx);
                inevitableLogLast = inevitableLogLast->next = inevitableLogItem;
                inevitableLogLast->inevitableT = bdd_termFalse;
                inevitableLogLast->inevitableF = bdd_termFalse;

              }

              if (!McNotEvaluate) {
                act2 = McTau;
                form2 = $5.f;

                if (McInevitable) {

                  form2x = $5.fx;

                  /* fprintf(stderr,"McInevitable: %s\n",inevitableLogLast->sx); */

                  Mc_InevitableCheckAX(McComp,
                    &inevitableLogLast->inevitableT,&inevitableLogLast->inevitableF,
                    act2,form2,form2x);

                  $$.f = inevitableLogLast->inevitableT;
                  $$.fx = inevitableLogLast->inevitableF;

                  inevitableLogLast = inevitableLogLast->next;

                } else {

                  result = Mc_CheckAX(McD,act2,form2);
                  $$.f = result;

                  if (diagnostic || tree || automaton) {
                    McAddDiagnostic(&$$.item,result,bdd_termNull,bdd_termNull,
                                 act2,form2,MC_AX,$$.s,$$.sx,NULL,$5.item);
                  }

                }
              }

              free($3);
              free($5.s);
              free($5.sx);
            } ;

          | EF actl {

              Bdd_Edge form2,form2x,result;

              $$.s = (Est_String) malloc(1024);
              $$.sx = (Est_String) malloc(1024);
              sprintf($$.s,"EF %s",$2.s);
              sprintf($$.sx,"EF %s",$2.sx);
              McInputstring = $$.s;

              if (trace) printf(">> %s\n",$$.s);
              /*
              if (xtrace) printf("X> %s\n",$$.sx);
              */

              if (McInevitablePrepare) {

                /* printf("PREPARE> %s\n",$$.s); */
                inevitableLogItem = McAddEmptyInevitable($$.s,$$.sx);
                inevitableLogLast = inevitableLogLast->next = inevitableLogItem;
                inevitableLogLast->inevitableT = bdd_termFalse;
                inevitableLogLast->inevitableT1 = bdd_termFalse;
                inevitableLogLast->inevitableF = bdd_termFalse;
                inevitableLogLast->inevitableF1 = bdd_termFalse;

              }

              if (!McNotEvaluate) {
                form2 = $2.f;

                if (McInevitable) {

                  form2x = $2.fx;

                  /* fprintf(stderr,"McInevitable: %s\n",inevitableLogLast->sx); */

                  Mc_InevitableCheckEF(McComp,
                    &inevitableLogLast->inevitableT,&inevitableLogLast->inevitableF,
                    &inevitableLogLast->inevitableT1,&inevitableLogLast->inevitableF1,
                    form2,form2x);

                  $$.f = inevitableLogLast->inevitableT;
                  $$.fx = inevitableLogLast->inevitableF;

                  inevitableLogLast = inevitableLogLast->next;

                } else {

                  result = Mc_CheckEF(McD,form2);
                  $$.f = result;

                  if (diagnostic || tree || automaton) {
                    McAddDiagnostic(&$$.item,result,bdd_termNull,bdd_termNull,bdd_termNull,
                                 form2,MC_EF,$$.s,$$.sx,NULL,$2.item);
                  }

                }
              }

              free($2.s);
              free($2.sx);
            } ;

          | AF actl {

              Bdd_Edge form2,form2x,result;

              $$.s = (Est_String) malloc(1024);
              $$.sx = (Est_String) malloc(1024);
              sprintf($$.s,"AF %s",$2.s);
              sprintf($$.sx,"AF %s",$2.sx);
              McInputstring = $$.s;

              if (trace) printf(">> %s\n",$$.s);
              /*
              if (xtrace) printf("X> %s\n",$$.sx);
              */

              if (McInevitablePrepare) {

                /* printf("PREPARE> %s\n",$$.s); */
                inevitableLogItem = McAddEmptyInevitable($$.s,$$.sx);
                inevitableLogLast = inevitableLogLast->next = inevitableLogItem;
                inevitableLogLast->inevitableT = bdd_termFalse;
                inevitableLogLast->inevitableT1 = bdd_termFalse;
                inevitableLogLast->inevitableF = bdd_termFalse;
                inevitableLogLast->inevitableF1 = bdd_termFalse;

              }

              if (!McNotEvaluate) {
                form2 = $2.f;

                if (McInevitable) {

                  form2x = $2.fx;

                  /* fprintf(stderr,"McInevitable: %s\n",inevitableLogLast->sx); */

                  Mc_InevitableCheckAF(McComp,
                    &inevitableLogLast->inevitableT,&inevitableLogLast->inevitableF,
                    &inevitableLogLast->inevitableT1,&inevitableLogLast->inevitableF1,
                    form2,form2x);

                  $$.f = inevitableLogLast->inevitableT;
                  $$.fx = inevitableLogLast->inevitableF;

                  inevitableLogLast = inevitableLogLast->next;

                } else {

                  result = Mc_CheckAF(McD,form2);
                  $$.f = result;

                  if (diagnostic || tree || automaton) {
                    McAddDiagnostic(&$$.item,result,bdd_termNull,bdd_termNull,
                                  bdd_termNull,form2,MC_AF,$$.s,$$.sx,NULL,$2.item);
                  }

                }
              }

              free($2.s);
              free($2.sx);
            } ;

          | EG actl {

              Bdd_Edge form1,form1x,result;

              $$.s = (Est_String) malloc(1024);
              $$.sx = (Est_String) malloc(1024);
              sprintf($$.s,"EG %s",$2.s);
              sprintf($$.sx,"EG %s",$2.sx);
              McInputstring = $$.s;

              if (trace) printf(">> %s\n",$$.s);
              /*
              if (xtrace) printf("X> %s\n",$$.sx);
              */

              if (McInevitablePrepare) {

                /* printf("PREPARE> %s\n",$$.s); */
                inevitableLogItem = McAddEmptyInevitable($$.s,$$.sx);
                inevitableLogLast = inevitableLogLast->next = inevitableLogItem;
                inevitableLogLast->inevitableT = bdd_termFalse;
                inevitableLogLast->inevitableT1 = bdd_termFalse;
                inevitableLogLast->inevitableF = bdd_termFalse;
                inevitableLogLast->inevitableF1 = bdd_termFalse;

              }

              if (!McNotEvaluate) {
                form1 = $2.f;

                if (McInevitable) {

                  form1x = $2.fx;

                  /* fprintf(stderr,"McInevitable: %s\n",inevitableLogLast->sx); */

                  Mc_InevitableCheckEG(McComp,
                    &inevitableLogLast->inevitableT,&inevitableLogLast->inevitableF,
                    &inevitableLogLast->inevitableT1,&inevitableLogLast->inevitableF1,
                    form1,form1x);

                  $$.f = inevitableLogLast->inevitableT;
                  $$.fx = inevitableLogLast->inevitableF;

                  inevitableLogLast = inevitableLogLast->next;

                } else {

                  result = Mc_CheckEG(McD,form1);
                  $$.f = result;

                  if (diagnostic || tree || automaton) {
                    McAddDiagnostic(&$$.item,result,bdd_termNull,form1,
                                  bdd_termNull,bdd_termNull,MC_EG,
                                  $$.s,$$.sx,$2.item,NULL);
                  }

                }
              }

              free($2.s);
              free($2.sx);
            } ;

          | AG actl {

              Bdd_Edge form1,form1x,result;

              $$.s = (Est_String) malloc(1024);
              $$.sx = (Est_String) malloc(1024);
              sprintf($$.s,"AG %s",$2.s);
              sprintf($$.sx,"AG %s",$2.sx);
              McInputstring = $$.s;

              if (trace) printf(">> %s\n",$$.s);
              /*
              if (xtrace) printf("X> %s\n",$$.sx);
              */

              if (McInevitablePrepare) {

                /* printf("PREPARE> %s\n",$$.s); */
                inevitableLogItem = McAddEmptyInevitable($$.s,$$.sx);
                inevitableLogLast = inevitableLogLast->next = inevitableLogItem;
                inevitableLogLast->inevitableT = bdd_termFalse;
                inevitableLogLast->inevitableT1 = bdd_termFalse;
                inevitableLogLast->inevitableF = bdd_termFalse;
                inevitableLogLast->inevitableF1 = bdd_termFalse;

              }

              if (!McNotEvaluate) {
                form1 = $2.f;

                if (McInevitable) {

                  form1x = $2.fx;

                  /* fprintf(stderr,"McInevitable: %s\n",inevitableLogLast->sx); */

                  Mc_InevitableCheckAG(McComp,
                    &inevitableLogLast->inevitableT,&inevitableLogLast->inevitableF,
                    &inevitableLogLast->inevitableT1,&inevitableLogLast->inevitableF1,
                    form1,form1x);

                  $$.f = inevitableLogLast->inevitableT;
                  $$.fx = inevitableLogLast->inevitableF;

                  inevitableLogLast = inevitableLogLast->next;

                } else {

                  result = Mc_CheckAG(McD,form1);
                  $$.f = result;

                  if (diagnostic || tree || automaton) {
                    McAddDiagnostic(&$$.item,result,bdd_termNull,form1,
                                  bdd_termNull,bdd_termNull,MC_AG,
                                  $$.s,$$.sx,$2.item,NULL);
                  }

                }
              }

              free($2.s);
              free($2.sx);
            } ;

          | actl '<' vis_act_form '>' actl {

              Bdd_Edge act,form1,form2,form1x,form2x,result;

              $$.s = (Est_String) malloc(1024);
              $$.sx = (Est_String) malloc(1024);
              sprintf($$.s,"%s <%s> %s",$1.s,$3.s,$5.s);
              sprintf($$.sx,"%s <%s> %s",$1.sx,$3.s,$5.sx);
              McInputstring = $$.s;

              if (trace) printf(">> %s\n",$$.s);
              /*
              if (xtrace) printf("X> %s\n",$$.sx);
              */

              if (McInevitablePrepare) {

                /* printf("PREPARE> %s\n",$$.s); */
                inevitableLogItem = McAddEmptyInevitable($$.s,$$.sx);
                inevitableLogLast = inevitableLogLast->next = inevitableLogItem;
                inevitableLogLast->inevitableT = bdd_termFalse;
                inevitableLogLast->inevitableT1 = bdd_termFalse;
                inevitableLogLast->inevitableF = bdd_termFalse;
                inevitableLogLast->inevitableF1 = bdd_termFalse;

              }

              if (!McNotEvaluate) {
                act = $3.f;
                form1 = $1.f;
                form2 = $5.f;

                if (McInevitable) {

                  form1x = $1.fx;
                  form2x = $5.fx;

                  /* fprintf(stderr,"McInevitable: %s\n",inevitableLogLast->sx); */

                  Mc_InevitableCheckHME(McComp,
                    &inevitableLogLast->inevitableT,&inevitableLogLast->inevitableF,
                    &inevitableLogLast->inevitableT1,&inevitableLogLast->inevitableF1,
                    form1,form1x,act,form2,form2x);

                  $$.f = inevitableLogLast->inevitableT;
                  $$.fx = inevitableLogLast->inevitableF;

                  inevitableLogLast = inevitableLogLast->next;

                } else {

                  result = Mc_CheckHME(McD,form1,act,form2);
                  $$.f = result;

                  if (diagnostic || tree || automaton) {
                    McAddDiagnostic(&$$.item,result,bdd_termNull,form1,
                                  act,form2,MC_HME,$$.s,$$.sx,$1.item,$5.item);
                  }

                }
              }

              free($1.s);
              free($1.sx);
              free($3.s);
              free($5.s);
              free($5.sx);
            } ;

          | '<' vis_act_form '>' actl {

              Bdd_Edge act,form1,form2,form1x,form2x,result;

              $$.s = (Est_String) malloc(1024);
              $$.sx = (Est_String) malloc(1024);
              sprintf($$.s,"<%s> %s",$2.s,$4.s);
              sprintf($$.sx,"<%s> %s",$2.s,$4.sx);
              McInputstring = $$.s;

              if (trace) printf(">> %s\n",$$.s);
              /*
              if (xtrace) printf("X> %s\n",$$.sx);
              */

              if (McInevitablePrepare) {

                /* printf("PREPARE> %s\n",$$.s); */
                inevitableLogItem = McAddEmptyInevitable($$.s,$$.sx);
                inevitableLogLast = inevitableLogLast->next = inevitableLogItem;
                inevitableLogLast->inevitableT = bdd_termFalse;
                inevitableLogLast->inevitableT1 = bdd_termFalse;
                inevitableLogLast->inevitableF = bdd_termFalse;
                inevitableLogLast->inevitableF1 = bdd_termFalse;

              }

              if (!McNotEvaluate) {
                act = $2.f;
                form1 = bdd_termNull;
                form2 = $4.f;

                if (McInevitable) {

                  form1x = bdd_termNull;
                  form2x = $4.fx;

                  /* fprintf(stderr,"McInevitable: %s\n",inevitableLogLast->sx); */

                  Mc_InevitableCheckHME(McComp,
                    &inevitableLogLast->inevitableT,&inevitableLogLast->inevitableF,
                    &inevitableLogLast->inevitableT1,&inevitableLogLast->inevitableF1,
                    form1,form1x,act,form2,form2x);

                  $$.f = inevitableLogLast->inevitableT;
                  $$.fx = inevitableLogLast->inevitableF;

                  inevitableLogLast = inevitableLogLast->next;

                } else {

                  result = Mc_CheckHME(McD,form1,act,form2);
                  $$.f = result;

                  if (diagnostic || tree || automaton) {
                    McAddDiagnostic(&$$.item,result,bdd_termNull,form1,
                                  act,form2,MC_HME,$$.s,$$.sx,NULL,$4.item);
                  }

                }
              }

              free($2.s);
              free($4.s);
              free($4.sx);
            } ;

          | actl '<' EPSILON '>' actl {

              Bdd_Edge act,form1,form2,form1x,form2x,result;

              $$.s = (Est_String) malloc(1024);
              $$.sx = (Est_String) malloc(1024);
              sprintf($$.s,"%s <EPSILON> %s",$1.s,$5.s);
              sprintf($$.sx,"%s <EPSILON> %s",$1.sx,$5.sx);
              McInputstring = $$.s;

              if (trace) printf(">> %s\n",$$.s);
              /*
              if (xtrace) printf("X> %s\n",$$.sx);
              */

              if (McInevitablePrepare) {

                /* printf("PREPARE> %s\n",$$.s); */
                inevitableLogItem = McAddEmptyInevitable($$.s,$$.sx);
                inevitableLogLast = inevitableLogLast->next = inevitableLogItem;
                inevitableLogLast->inevitableT = bdd_termFalse;
                inevitableLogLast->inevitableT1 = bdd_termFalse;
                inevitableLogLast->inevitableF = bdd_termFalse;
                inevitableLogLast->inevitableF1 = bdd_termFalse;

              }

              if (!McNotEvaluate) {
                act = bdd_termNull;
                form1 = $1.f;
                form2 = $5.f;

                if (McInevitable) {

                  form1x = $1.fx;
                  form2x = $5.fx;

                  /* fprintf(stderr,"McInevitable: %s\n",inevitableLogLast->sx); */

                  Mc_InevitableCheckHME(McComp,
                    &inevitableLogLast->inevitableT,&inevitableLogLast->inevitableF,
                    &inevitableLogLast->inevitableT1,&inevitableLogLast->inevitableF1,
                    form1,form1x,act,form2,form2x);

                  $$.f = inevitableLogLast->inevitableT;
                  $$.fx = inevitableLogLast->inevitableF;

                  inevitableLogLast = inevitableLogLast->next;

                } else {

                  result = Mc_CheckHME(McD,form1,act,form2);
                  $$.f = result;

                  if (diagnostic || tree || automaton) {
                    McAddDiagnostic(&$$.item,result,bdd_termNull,form1,
                                  act,form2,MC_HME,$$.s,$$.sx,$1.item,$5.item);
                  }

                }
              }

              free($1.s);
              free($1.sx);
              free($3);
              free($5.s);
              free($5.sx);
            } ;

            | '<' EPSILON '>' actl {

              Bdd_Edge act,form1,form2,form1x,form2x,result;

              $$.s = (Est_String) malloc(1024);
              $$.sx = (Est_String) malloc(1024);
              sprintf($$.s,"<EPSILON> %s",$4.s);
              sprintf($$.sx,"<EPSILON> %s",$4.sx);
              McInputstring = $$.s;

              if (trace) printf(">> %s\n",$$.s);
              /*
              if (xtrace) printf("X> %s\n",$$.sx);
              */

              if (McInevitablePrepare) {

                /* printf("PREPARE> %s\n",$$.s); */
                inevitableLogItem = McAddEmptyInevitable($$.s,$$.sx);
                inevitableLogLast = inevitableLogLast->next = inevitableLogItem;
                inevitableLogLast->inevitableT = bdd_termFalse;
                inevitableLogLast->inevitableT1 = bdd_termFalse;
                inevitableLogLast->inevitableF = bdd_termFalse;
                inevitableLogLast->inevitableF1 = bdd_termFalse;

              }

              if (!McNotEvaluate) {
                act = bdd_termNull;
                form1 = bdd_termNull;
                form2 = $4.f;


                if (McInevitable) {

                  form1x = bdd_termNull;
                  form2x = $4.fx;

                  /* fprintf(stderr,"McInevitable: %s\n",inevitableLogLast->sx); */

                  Mc_InevitableCheckHME(McComp,
                    &inevitableLogLast->inevitableT,&inevitableLogLast->inevitableF,
                    &inevitableLogLast->inevitableT1,&inevitableLogLast->inevitableF1,
                    form1,form1x,act,form2,form2x);

                  $$.f = inevitableLogLast->inevitableT;
                  $$.fx = inevitableLogLast->inevitableF;

                  inevitableLogLast = inevitableLogLast->next;

                } else {

                  result = Mc_CheckHME(McD,form1,act,form2);
                  $$.f = result;

                  if (diagnostic || tree || automaton) {
                    McAddDiagnostic(&$$.item,result,bdd_termNull,form1,
                                  act,form2,MC_HME,$$.s,$$.sx,NULL,$4.item);
                  }

                }
              }

              free($2);
              free($4.s);
              free($4.sx);
            } ;

          | '[' vis_act_form ']' actl {

              Bdd_Edge act,form1,form2,form2x,result;

              $$.s = (Est_String) malloc(1024);
              $$.sx = (Est_String) malloc(1024);
              sprintf($$.s,"[%s] %s",$2.s,$4.s);
              sprintf($$.sx,"[%s] %s",$2.s,$4.sx);
              McInputstring = $$.s;

              if (trace) printf(">> %s\n",$$.s);
              /*
              if (xtrace) printf("X> %s\n",$$.sx);
              */

              if (McInevitablePrepare) {

                /* printf("PREPARE> %s\n",$$.s); */
                inevitableLogItem = McAddEmptyInevitable($$.s,$$.sx);
                inevitableLogLast = inevitableLogLast->next = inevitableLogItem;
                inevitableLogLast->inevitableT = bdd_termFalse;
                inevitableLogLast->inevitableT1 = bdd_termFalse;
                inevitableLogLast->inevitableF = bdd_termFalse;
                inevitableLogLast->inevitableF1 = bdd_termFalse;

              }

              if (!McNotEvaluate) {
                act = $2.f;
                form1 = bdd_termNull;
                form2 = $4.f;

                if (McInevitable) {

                  form2x = $4.fx;

                  /* fprintf(stderr,"McInevitable: %s\n",inevitableLogLast->sx); */

                  Mc_InevitableCheckHMA(McComp,
                    &inevitableLogLast->inevitableT,&inevitableLogLast->inevitableF,
                    &inevitableLogLast->inevitableT1,&inevitableLogLast->inevitableF1,
                    act,form2,form2x);

                  $$.f = inevitableLogLast->inevitableT;
                  $$.fx = inevitableLogLast->inevitableF;

                  inevitableLogLast = inevitableLogLast->next;

                } else {

                  result = Mc_CheckHMA(McD,act,form2);
                  $$.f = result;

                  if (diagnostic || tree || automaton) {
                    McAddDiagnostic(&$$.item,result,bdd_termNull,form1,
                                  act,form2,MC_HMA,$$.s,$$.sx,NULL,$4.item);
                  }

                }
              }


              free($2.s);
              free($4.s);
              free($4.sx);
            } ;

          | '[' EPSILON ']' actl {

              Bdd_Edge act,form1,form2,form2x,result;

              $$.s = (Est_String) malloc(1024);
              $$.sx = (Est_String) malloc(1024);
              sprintf($$.s,"[EPSILON] %s",$4.s);
              sprintf($$.sx,"[EPSILON] %s",$4.sx);
              McInputstring = $$.s;

              if (trace) printf(">> %s\n",$$.s);
              /*
              if (xtrace) printf("X> %s\n",$$.sx);
              */

              if (McInevitablePrepare) {

                /* printf("PREPARE> %s\n",$$.s); */
                inevitableLogItem = McAddEmptyInevitable($$.s,$$.sx);
                inevitableLogLast = inevitableLogLast->next = inevitableLogItem;
                inevitableLogLast->inevitableT = bdd_termFalse;
                inevitableLogLast->inevitableT1 = bdd_termFalse;
                inevitableLogLast->inevitableF = bdd_termFalse;
                inevitableLogLast->inevitableF1 = bdd_termFalse;

              }

              if (!McNotEvaluate) {
                act = bdd_termNull;
                form1 = bdd_termNull;
                form2 = $4.f;

                if (McInevitable) {

                  form2x = $4.fx;

                  /* fprintf(stderr,"McInevitable: %s\n",inevitableLogLast->sx); */

                  Mc_InevitableCheckHMA(McComp,
                    &inevitableLogLast->inevitableT,&inevitableLogLast->inevitableF,
                    &inevitableLogLast->inevitableT1,&inevitableLogLast->inevitableF1,
                    act,form2,form2x);

                  $$.f = inevitableLogLast->inevitableT;
                  $$.fx = inevitableLogLast->inevitableF;

                  inevitableLogLast = inevitableLogLast->next;

                } else {

                  result = Mc_CheckHMA(McD,act,form2);
                  $$.f = result;

                  if (diagnostic || tree || automaton) {
                    McAddDiagnostic(&$$.item,result,bdd_termNull,form1,
                                  act,form2,MC_HMA,$$.s,$$.sx,NULL,$4.item);
                  }

                }
              }

              free($2);
              free($4.s);
              free($4.sx);
            } ;

unless_actl : EE '[' actl1 UNTIL actl1 ']' {

                Bdd_Edge act1,act2,form1,form2,form1x,form2x,result;

                $$.s = (Est_String) malloc(1024);
                $$.sx = (Est_String) malloc(1024);
                sprintf($$.s,"EE[%s U %s]",$3.s,$5.s);
                sprintf($$.sx,"EE[%s U %s]",$3.sx,$5.sx);
                McInputstring = $$.s;

                if (trace) printf(">> %s\n",$$.s);
                /*
                if (xtrace) printf("X> %s\n",$$.sx);
                */

                if (McInevitablePrepare) {

                  /* printf("PREPARE> %s\n",$$.s); */
                  inevitableLogItem = McAddEmptyInevitable($$.s,$$.sx);
                  inevitableLogLast = inevitableLogLast->next = inevitableLogItem;
                  inevitableLogLast->inevitableT = bdd_termFalse;
                  inevitableLogLast->inevitableF = bdd_termFalse;

                }

                if (!McNotEvaluate) {
                  act1 = $3.act;
                  form1 = $3.form;
                  act2 = $5.act;
                  form2 = $5.form;

                  if (McInevitable) {

                    form1x = $3.formx;
                    form2x = $5.formx;

                    /* fprintf(stderr,"McInevitable: %s\n",inevitableLogLast->sx); */

                    Mc_InevitableCheckEEU(McComp,
                      &inevitableLogLast->inevitableT,&inevitableLogLast->inevitableF,
                      act1,form1,form1x,act2,form2,form2x);

                    $$.f = inevitableLogLast->inevitableT;
                    $$.fx = inevitableLogLast->inevitableF;

                    inevitableLogLast = inevitableLogLast->next;

                  } else {

                    result = Mc_CheckEEU(McD,act1,form1,act2,form2);
                    $$.f = result;

                    if (diagnostic || tree || automaton) {
                      McAddDiagnostic(&$$.item,result,
                                    act1,form1,act2,form2,MC_EEU,$$.s,$$.sx,
                                    $3.item,$5.item);
                    }

                  }
                }

                free($3.s);
                free($3.sx);
                free($5.s);
                free($5.sx);
              } ;

            | EE '[' actl2 UNTIL actl1 ']' {

                Bdd_Edge act1,act2,form1,form2,form1x,form2x,result;

                $$.s = (Est_String) malloc(1024);
                $$.sx = (Est_String) malloc(1024);
                sprintf($$.s,"EE[%s U %s]",$3.s,$5.s);
                sprintf($$.sx,"EE[%s U %s]",$3.sx,$5.sx);
                McInputstring = $$.s;

                if (trace) printf(">> %s\n",$$.s);
                /*
                if (xtrace) printf("X> %s\n",$$.sx);
                */

                if (McInevitablePrepare) {

                  /* printf("PREPARE> %s\n",$$.s); */
                  inevitableLogItem = McAddEmptyInevitable($$.s,$$.sx);
                  inevitableLogLast = inevitableLogLast->next = inevitableLogItem;
                  inevitableLogLast->inevitableT = bdd_termFalse;
                  inevitableLogLast->inevitableF = bdd_termFalse;

                }

                if (!McNotEvaluate) {
                  act1 = $3.act;
                  form1 = $3.form;
                  act2 = $5.act;
                  form2 = $5.form;

                  if (McInevitable) {

                    form1x = $3.formx;
                    form2x = $5.formx;

                    /* fprintf(stderr,"McInevitable: %s\n",inevitableLogLast->sx); */

                    Mc_InevitableCheckEEU(McComp,
                      &inevitableLogLast->inevitableT,&inevitableLogLast->inevitableF,
                      act1,form1,form1x,act2,form2,form2x);

                    /* NON-STRICT */
                    result = Bdd_ITE(inevitableLogLast->inevitableT,form1,bdd_termFalse);
                    Bdd_Fortify(result);
                    $$.f = result;

                    /* NON-STRICT */
                    result = Bdd_ITE(inevitableLogLast->inevitableF,bdd_termTrue,form1x);
                    Bdd_Fortify(result);
                    $$.fx = result;

                    inevitableLogLast = inevitableLogLast->next;

                  } else {

                    result = Mc_CheckEEU(McD,act1,form1,act2,form2);
                    result = Bdd_ITE(result,form1,bdd_termFalse); /* NON-STRICT */
                    $$.f = result;

                    if (diagnostic || tree || automaton) {
                      McAddDiagnostic(&$$.item,result,
                                    act1,form1,act2,form2,MC_EEU_NS,$$.s,$$.sx,
                                    $3.item,$5.item);
                    }

                  }
                }

                free($3.s);
                free($3.sx);
                free($5.s);
                free($5.sx);
              } ;

            | AA '[' actl1 UNTIL actl1 ']' {

                Bdd_Edge act1,act2,form1,form2,form1x,form2x,result;
                Bdd_Edge formAAW,formAAF;

                $$.s = (Est_String) malloc(1024);
                $$.sx = (Est_String) malloc(1024);
                sprintf($$.s,"AA[%s U %s]",$3.s,$5.s);
                sprintf($$.sx,"AA[%s U %s]",$3.sx,$5.sx);
                McInputstring = $$.s;

                if (trace) printf(">> %s\n",$$.s);
                /*
                if (xtrace) printf("X> %s\n",$$.sx);
                */

                if (McInevitablePrepare) {

                  /* printf("PREPARE> %s\n",$$.s); */
                  inevitableLogItem = McAddEmptyInevitable($$.s,$$.sx);
                  inevitableLogLast = inevitableLogLast->next = inevitableLogItem;
                  inevitableLogLast->inevitableT = bdd_termFalse;
                  inevitableLogLast->inevitableT1 = bdd_termFalse;
                  inevitableLogLast->inevitableT2 = bdd_termFalse;
                  inevitableLogLast->inevitableF = bdd_termFalse;
                  inevitableLogLast->inevitableF1 = bdd_termFalse;
                  inevitableLogLast->inevitableF2 = bdd_termFalse;

                }

                if (!McNotEvaluate) {
                  act1 = $3.act;
                  form1 = $3.form;
                  act2 = $5.act;
                  form2 = $5.form;

                  if (McInevitable) {

                    form1x = $3.formx;
                    form2x = $5.formx;

                    /* fprintf(stderr,"McInevitable: %s\n",inevitableLogLast->sx); */

                    Mc_InevitableCheckAAU(McComp,
                      &inevitableLogLast->inevitableT,&inevitableLogLast->inevitableF,
                      &inevitableLogLast->inevitableT1,&inevitableLogLast->inevitableF1,
                      &inevitableLogLast->inevitableT2,&inevitableLogLast->inevitableF2,
                      act1,form1,form1x,act2,form2,form2x);

                    $$.f = inevitableLogLast->inevitableT;
                    $$.fx = inevitableLogLast->inevitableF;

                    inevitableLogLast = inevitableLogLast->next;

                  } else {

                    result = Mc_CheckAAU(McD,act1,form1,act2,form2,
                                      &formAAW,&formAAF);
                    $$.f = result;

                    if (diagnostic || tree || automaton) {
                      McAddDiagnostic(&$$.item,result,
                                    act1,form1,act2,form2,MC_AAU,$$.s,$$.sx,
                                    $3.item,$5.item);
                    }

                  }
                }

                free($3.s);
                free($3.sx);
                free($5.s);
                free($5.sx);
              } ;

            | AA '[' actl2 UNTIL actl1 ']' {

                Bdd_Edge act1,act2,form1,form2,form1x,form2x,result;
                Bdd_Edge formAAW,formAAF;

                $$.s = (Est_String) malloc(1024);
                $$.sx = (Est_String) malloc(1024);
                sprintf($$.s,"AA[%s U %s]",$3.s,$5.s);
                sprintf($$.sx,"AA[%s U %s]",$3.sx,$5.sx);
                McInputstring = $$.s;

                if (trace) printf(">> %s\n",$$.s);
                /*
                if (xtrace) printf("X> %s\n",$$.sx);
                */

                if (McInevitablePrepare) {

                  /* printf("PREPARE> %s\n",$$.s); */
                  inevitableLogItem = McAddEmptyInevitable($$.s,$$.sx);
                  inevitableLogLast = inevitableLogLast->next = inevitableLogItem;
                  inevitableLogLast->inevitableT = bdd_termFalse;
                  inevitableLogLast->inevitableT1 = bdd_termFalse;
                  inevitableLogLast->inevitableT2 = bdd_termFalse;
                  inevitableLogLast->inevitableF = bdd_termFalse;
                  inevitableLogLast->inevitableF1 = bdd_termFalse;
                  inevitableLogLast->inevitableF2 = bdd_termFalse;

                }

                if (!McNotEvaluate) {
                  act1 = $3.act;
                  form1 = $3.form;
                  act2 = $5.act;
                  form2 = $5.form;

                  if (McInevitable) {

                    form1x = $3.formx;
                    form2x = $5.formx;

                    /* fprintf(stderr,"McInevitable: %s\n",inevitableLogLast->sx); */

                    Mc_InevitableCheckAAU(McComp,
                      &inevitableLogLast->inevitableT,&inevitableLogLast->inevitableF,
                      &inevitableLogLast->inevitableT1,&inevitableLogLast->inevitableF1,
                      &inevitableLogLast->inevitableT2,&inevitableLogLast->inevitableF2,
                      act1,form1,form1x,act2,form2,form2x);

                    /* NON-STRICT */
                    result = Bdd_ITE(inevitableLogLast->inevitableT,form1,bdd_termFalse);
                    Bdd_Fortify(result);
                    $$.f = result;

                    /* NON-STRICT */
                    result = Bdd_ITE(inevitableLogLast->inevitableF,bdd_termTrue,form1x);
                    Bdd_Fortify(result);
                    $$.fx = result;

                    inevitableLogLast = inevitableLogLast->next;

                  } else {

                    result = Mc_CheckAAU(McD,act1,form1,act2,form2,
                                      &formAAW,&formAAF);
                    formAAW = Bdd_ITE(formAAW,form1,bdd_termFalse); /* NON-STRICT */
                    result = Bdd_ITE(result,form1,bdd_termFalse); /* NON-STRICT */
                    $$.f = result;

                    if (diagnostic || tree || automaton) {
                      McAddDiagnostic(&$$.item,result,
                                    act1,form1,act2,form2,MC_AAU_NS,$$.s,$$.sx,
                                    $3.item,$5.item);
                    }

                  }
                }

                free($3.s);
                free($3.sx);
                free($5.s);
                free($5.sx);
              } ;

            | EE '[' actl1 UNLESS actl1 ']' {

                Bdd_Edge act1,act2,form1,form2,form1x,form2x,result;
                Bdd_Edge formEEU,formEEG;

                $$.s = (Est_String) malloc(1024);
                $$.sx = (Est_String) malloc(1024);
                sprintf($$.s,"EE[%s W %s]",$3.s,$5.s);
                sprintf($$.sx,"EE[%s W %s]",$3.sx,$5.sx);
                McInputstring = $$.s;

                if (trace) printf(">> %s\n",$$.s);
                /*
                if (xtrace) printf("X> %s\n",$$.sx);
                */

                if (McInevitablePrepare) {

                  /* printf("PREPARE> %s\n",$$.s); */
                  inevitableLogItem = McAddEmptyInevitable($$.s,$$.sx);
                  inevitableLogLast = inevitableLogLast->next = inevitableLogItem;
                  inevitableLogLast->inevitableT = bdd_termFalse;
                  inevitableLogLast->inevitableT1 = bdd_termFalse;
                  inevitableLogLast->inevitableT2 = bdd_termFalse;
                  inevitableLogLast->inevitableF = bdd_termFalse;
                  inevitableLogLast->inevitableF1 = bdd_termFalse;
                  inevitableLogLast->inevitableF2 = bdd_termFalse;

                }

                if (!McNotEvaluate) {
                  act1 = $3.act;
                  form1 = $3.form;
                  act2 = $5.act;
                  form2 = $5.form;

                  if (McInevitable) {

                    form1x = $3.formx;
                    form2x = $5.formx;

                    /* fprintf(stderr,"McInevitable: %s\n",inevitableLogLast->sx); */

                    Mc_InevitableCheckEEW(McComp,
                      &inevitableLogLast->inevitableT,&inevitableLogLast->inevitableF,
                      &inevitableLogLast->inevitableT1,&inevitableLogLast->inevitableF1,
                      &inevitableLogLast->inevitableT2,&inevitableLogLast->inevitableF2,
                      act1,form1,form1x,act2,form2,form2x);

                    $$.f = inevitableLogLast->inevitableT;
                    $$.fx = inevitableLogLast->inevitableF;

                    inevitableLogLast = inevitableLogLast->next;

                  } else {

                    result = Mc_CheckEEW(McD,act1,form1,act2,form2,
                                      &formEEU,&formEEG);
                    $$.f = result;

                    if (diagnostic || tree || automaton) {
                      McAddDiagnostic(&$$.item,result,
                                    act1,form1,act2,form2,MC_EEW,$$.s,$$.sx,
                                    $3.item,$5.item);
                    }

                  }
                }

                free($3.s);
                free($3.sx);
                free($5.s);
                free($5.sx);
              } ;

            | EE '[' actl2 UNLESS actl1 ']' {

                Bdd_Edge act1,act2,form1,form2,form1x,form2x,result;
                Bdd_Edge formEEU,formEEG;

                $$.s = (Est_String) malloc(1024);
                $$.sx = (Est_String) malloc(1024);
                sprintf($$.s,"EE[%s W %s]",$3.s,$5.s);
                sprintf($$.sx,"EE[%s W %s]",$3.sx,$5.sx);
                McInputstring = $$.s;

                if (trace) printf(">> %s\n",$$.s);
                /*
                if (xtrace) printf("X> %s\n",$$.sx);
                */

                if (McInevitablePrepare) {

                  /* printf("PREPARE> %s\n",$$.s); */
                  inevitableLogItem = McAddEmptyInevitable($$.s,$$.sx);
                  inevitableLogLast = inevitableLogLast->next = inevitableLogItem;
                  inevitableLogLast->inevitableT = bdd_termFalse;
                  inevitableLogLast->inevitableT1 = bdd_termFalse;
                  inevitableLogLast->inevitableT2 = bdd_termFalse;
                  inevitableLogLast->inevitableF = bdd_termFalse;
                  inevitableLogLast->inevitableF1 = bdd_termFalse;
                  inevitableLogLast->inevitableF2 = bdd_termFalse;

                }

                if (!McNotEvaluate) {
                  act1 = $3.act;
                  form1 = $3.form;
                  act2 = $5.act;
                  form2 = $5.form;

                  if (McInevitable) {

                    form1x = $3.formx;
                    form2x = $5.formx;

                    /* fprintf(stderr,"McInevitable: %s\n",inevitableLogLast->sx); */

                    Mc_InevitableCheckEEW(McComp,
                      &inevitableLogLast->inevitableT,&inevitableLogLast->inevitableF,
                      &inevitableLogLast->inevitableT1,&inevitableLogLast->inevitableF1,
                      &inevitableLogLast->inevitableT2,&inevitableLogLast->inevitableF2,
                      act1,form1,form1x,act2,form2,form2x);

                    /* NON-STRICT */
                    result = Bdd_ITE(inevitableLogLast->inevitableT,form1,bdd_termFalse);
                    Bdd_Fortify(result);
                    $$.f = result;

                    /* NON-STRICT */
                    result = Bdd_ITE(inevitableLogLast->inevitableF,bdd_termTrue,form1x);
                    Bdd_Fortify(result);
                    $$.fx = result;

                    inevitableLogLast = inevitableLogLast->next;

                  } else {

                    result = Mc_CheckEEW(McD,act1,form1,act2,form2,
                                       &formEEU,&formEEG);
                    formEEU = Bdd_ITE(formEEU,form1,bdd_termFalse); /* NON-STRICT */
                    formEEG = Bdd_ITE(formEEG,form1,bdd_termFalse); /* NON-STRICT */
                    result = Bdd_ITE(result,form1,bdd_termFalse); /* NON-STRICT */
                    $$.f = result;

                    if (diagnostic || tree || automaton) {
                      McAddDiagnostic(&$$.item,result,
                                    act1,form1,act2,form2,MC_EEW_NS,$$.s,$$.sx,
                                    $3.item,$5.item);
                    }

                  }
                }

                free($3.s);
                free($3.sx);
                free($5.s);
                free($5.sx);
              } ;

            | AA '[' actl1 UNLESS actl1 ']' {

                Bdd_Edge act1,act2,form1,form2,form1x,form2x,result;

                $$.s = (Est_String) malloc(1024);
                $$.sx = (Est_String) malloc(1024);
                sprintf($$.s,"AA[%s W %s]",$3.s,$5.s);
                sprintf($$.sx,"AA[%s W %s]",$3.sx,$5.sx);
                McInputstring = $$.s;

                if (trace) printf(">> %s\n",$$.s);
                /*
                if (xtrace) printf("X> %s\n",$$.sx);
                */

                if (McInevitablePrepare) {

                  /* printf("PREPARE> %s\n",$$.s); */
                  inevitableLogItem = McAddEmptyInevitable($$.s,$$.sx);
                  inevitableLogLast = inevitableLogLast->next = inevitableLogItem;
                  inevitableLogLast->inevitableT = bdd_termFalse;
                  inevitableLogLast->inevitableF = bdd_termFalse;

                }

                if (!McNotEvaluate) {
                  act1 = $3.act;
                  form1 = $3.form;
                  act2 = $5.act;
                  form2 = $5.form;

                  if (McInevitable) {

                    form1x = $3.formx;
                    form2x = $5.formx;

                    /* fprintf(stderr,"McInevitable: %s\n",inevitableLogLast->sx); */

                    Mc_InevitableCheckAAW(McComp,
                      &inevitableLogLast->inevitableT,&inevitableLogLast->inevitableF,
                      act1,form1,form1x,act2,form2,form2x);

                    $$.f = inevitableLogLast->inevitableT;
                    $$.fx = inevitableLogLast->inevitableF;

                    inevitableLogLast = inevitableLogLast->next;

                  } else {

                    result = Mc_CheckAAW(McD,act1,form1,act2,form2);
                    $$.f = result;

                    if (diagnostic || tree || automaton) {
                      McAddDiagnostic(&$$.item,result,
                                    act1,form1,act2,form2,MC_AAW,$$.s,$$.sx,
                                    $3.item,$5.item);
                    }

                  }
                }

                free($3.s);
                free($3.sx);
                free($5.s);
                free($5.sx);
              } ;

            | AA '[' actl2 UNLESS actl1 ']' {

                Bdd_Edge act1,act2,form1,form2,form1x,form2x,result;

                $$.s = (Est_String) malloc(1024);
                $$.sx = (Est_String) malloc(1024);
                sprintf($$.s,"AA[%s W %s]",$3.s,$5.s);
                sprintf($$.sx,"AA[%s W %s]",$3.sx,$5.sx);
                McInputstring = $$.s;

                if (trace) printf(">> %s\n",$$.s);
                /*
                if (xtrace) printf("X> %s\n",$$.sx);
                */

                if (McInevitablePrepare) {

                  /* printf("PREPARE> %s\n",$$.s); */
                  inevitableLogItem = McAddEmptyInevitable($$.s,$$.sx);
                  inevitableLogLast = inevitableLogLast->next = inevitableLogItem;
                  inevitableLogLast->inevitableT = bdd_termFalse;
                  inevitableLogLast->inevitableF = bdd_termFalse;

                }

                if (!McNotEvaluate) {
                  act1 = $3.act;
                  form1 = $3.form;
                  act2 = $5.act;
                  form2 = $5.form;

                  if (McInevitable) {

                    form1x = $3.formx;
                    form2x = $5.formx;

                    /* fprintf(stderr,"McInevitable: %s\n",inevitableLogLast->sx); */

                    Mc_InevitableCheckAAW(McComp,
                      &inevitableLogLast->inevitableT,&inevitableLogLast->inevitableF,
                      act1,form1,form1x,act2,form2,form2x);

                    /* NON-STRICT */
                    result = Bdd_ITE(inevitableLogLast->inevitableT,form1,bdd_termFalse);
                    Bdd_Fortify(result);
                    $$.f = result;

                    /* NON-STRICT */
                    result = Bdd_ITE(inevitableLogLast->inevitableF,bdd_termTrue,form1x);
                    Bdd_Fortify(result);
                    $$.fx = result;

                    inevitableLogLast = inevitableLogLast->next;

                  } else {

                    result = Mc_CheckAAW(McD,act1,form1,act2,form2);
                    result = Bdd_ITE(result,form1,bdd_termFalse); /* NON-STRICT */
                    $$.f = result;

                    if (diagnostic || tree || automaton) {
                      McAddDiagnostic(&$$.item,result,
                                    act1,form1,act2,form2,MC_AAW_NS,$$.s,$$.sx,
                                    $3.item,$5.item);
                    }

                  }
                }

                free($3.s);
                free($3.sx);
                free($5.s);
                free($5.sx);
              } ;

            | EEX actl1 {

                Bdd_Edge act2,form2,form2x,result;

                $$.s = (Est_String) malloc(1024);
                $$.sx = (Est_String) malloc(1024);
                sprintf($$.s,"EEX %s",$2.s);
                sprintf($$.sx,"EEX %s",$2.sx);
                McInputstring = $$.s;

                if (trace) printf(">> %s\n",$$.s);
                /*
                if (xtrace) printf("X> %s\n",$$.sx);
                */

                if (McInevitablePrepare) {

                  /* printf("PREPARE> %s\n",$$.s); */
                  inevitableLogItem = McAddEmptyInevitable($$.s,$$.sx);
                  inevitableLogLast = inevitableLogLast->next = inevitableLogItem;
                  inevitableLogLast->inevitableT = bdd_termFalse;
                  inevitableLogLast->inevitableF = bdd_termFalse;

                }

                if (!McNotEvaluate) {
                  act2 = $2.act;
                  form2 = $2.form;

                  if (McInevitable) {

                    form2x = $2.formx;

                    /* fprintf(stderr,"McInevitable: %s\n",inevitableLogLast->sx); */

                    Mc_InevitableCheckEEX(McComp,
                      &inevitableLogLast->inevitableT,&inevitableLogLast->inevitableF,
                      act2,form2,form2x);

                    $$.f = inevitableLogLast->inevitableT;
                    $$.fx = inevitableLogLast->inevitableF;

                    inevitableLogLast = inevitableLogLast->next;

                  } else {

                    result = Mc_CheckEEX(McD,act2,form2);
                    $$.f = result;

                    if (diagnostic || tree || automaton) {
                      McAddDiagnostic(&$$.item,result,bdd_termNull,bdd_termNull,
                                   act2,form2,MC_EEX,$$.s,$$.sx,NULL,$2.item);
                    }

                  }
                }

                free($2.s);
                free($2.sx);
              } ;

            | AAX actl1 {

                Bdd_Edge act2,form2,form2x,result;

                $$.s = (Est_String) malloc(1024);
                $$.sx = (Est_String) malloc(1024);
                sprintf($$.s,"AAX %s",$2.s);
                sprintf($$.sx,"AAX %s",$2.sx);
                McInputstring = $$.s;

                if (trace) printf(">> %s\n",$$.s);
                /*
                if (xtrace) printf("X> %s\n",$$.sx);
                */

                if (McInevitablePrepare) {

                  /* printf("PREPARE> %s\n",$$.s); */
                  inevitableLogItem = McAddEmptyInevitable($$.s,$$.sx);
                  inevitableLogLast = inevitableLogLast->next = inevitableLogItem;
                  inevitableLogLast->inevitableT = bdd_termFalse;
                  inevitableLogLast->inevitableF = bdd_termFalse;

                }

                if (!McNotEvaluate) {
                  act2 = $2.act;
                  form2 = $2.form;

                  if (McInevitable) {

                    form2x = $2.formx;

                    /* fprintf(stderr,"McInevitable: %s\n",inevitableLogLast->sx); */

                    Mc_InevitableCheckAAX(McComp,
                      &inevitableLogLast->inevitableT,&inevitableLogLast->inevitableF,
                      act2,form2,form2x);

                    $$.f = inevitableLogLast->inevitableT;
                    $$.fx = inevitableLogLast->inevitableF;

                    inevitableLogLast = inevitableLogLast->next;

                  } else {

                    result = Mc_CheckAAX(McD,act2,form2);
                    $$.f = result;

                    if (diagnostic || tree || automaton) {
                      McAddDiagnostic(&$$.item,result,bdd_termNull,bdd_termNull,
                                   act2,form2,MC_AAX,$$.s,$$.sx,NULL,$2.item);
                    }

                  }
                }

                free($2.s);
                free($2.sx);
              } ;

            | EEF actl1 {

                Bdd_Edge act2,form2,form2x,result;

                $$.s = (Est_String) malloc(1024);
                $$.sx = (Est_String) malloc(1024);
                sprintf($$.s,"EEF %s",$2.s);
                sprintf($$.sx,"EEF %s",$2.sx);
                McInputstring = $$.s;

                if (trace) printf(">> %s\n",$$.s);
                /*
                if (xtrace) printf("X> %s\n",$$.sx);
                */

                if (McInevitablePrepare) {

                  /* printf("PREPARE> %s\n",$$.s); */
                  inevitableLogItem = McAddEmptyInevitable($$.s,$$.sx);
                  inevitableLogLast = inevitableLogLast->next = inevitableLogItem;
                  inevitableLogLast->inevitableT = bdd_termFalse;
                  inevitableLogLast->inevitableF = bdd_termFalse;

                }

                if (!McNotEvaluate) {
                  act2 = $2.act;
                  form2 = $2.form;

                  if (McInevitable) {

                    form2x = $2.formx;

                    /* fprintf(stderr,"McInevitable: %s\n",inevitableLogLast->sx); */

                    Mc_InevitableCheckEEF(McComp,
                      &inevitableLogLast->inevitableT,&inevitableLogLast->inevitableF,
                      act2,form2,form2x);

                    $$.f = inevitableLogLast->inevitableT;
                    $$.fx = inevitableLogLast->inevitableF;

                    inevitableLogLast = inevitableLogLast->next;

                  } else {

                    result = Mc_CheckEEF(McD,act2,form2);
                    $$.f = result;

                    if (diagnostic || tree || automaton) {
                      McAddDiagnostic(&$$.item,result,bdd_termNull,bdd_termNull,act2,
                                    form2,MC_EEF,$$.s,$$.sx,NULL,$2.item);
                    }

                  }
                }

                free($2.s);
                free($2.sx);
              } ;

            | AAF actl1 {

                Bdd_Edge act2,form2,form2x,result;

                $$.s = (Est_String) malloc(1024);
                $$.sx = (Est_String) malloc(1024);
                sprintf($$.s,"AAF %s",$2.s);
                sprintf($$.sx,"AAF %s",$2.sx);
                McInputstring = $$.s;

                if (trace) printf(">> %s\n",$$.s);
                /*
                if (xtrace) printf("X> %s\n",$$.sx);
                */

                if (McInevitablePrepare) {

                  /* printf("PREPARE> %s\n",$$.s); */
                  inevitableLogItem = McAddEmptyInevitable($$.s,$$.sx);
                  inevitableLogLast = inevitableLogLast->next = inevitableLogItem;
                  inevitableLogLast->inevitableT = bdd_termFalse;
                  inevitableLogLast->inevitableF = bdd_termFalse;

                }

                if (!McNotEvaluate) {
                  act2 = $2.act;
                  form2 = $2.form;

                  if (McInevitable) {

                    form2x = $2.formx;

                    /* fprintf(stderr,"McInevitable: %s\n",inevitableLogLast->sx); */

                    Mc_InevitableCheckAAF(McComp,
                      &inevitableLogLast->inevitableT,&inevitableLogLast->inevitableF,
                      act2,form2,form2x);

                    $$.f = inevitableLogLast->inevitableT;
                    $$.fx = inevitableLogLast->inevitableF;

                    inevitableLogLast = inevitableLogLast->next;

                  } else {

                    result = Mc_CheckAAF(McD,act2,form2);
                    $$.f = result;

                    if (diagnostic || tree || automaton) {
                      McAddDiagnostic(&$$.item,result,bdd_termNull,bdd_termNull,
                                    act2,form2,MC_AAF,$$.s,$$.sx,NULL,$2.item);
                    }

                  }
                }

                free($2.s);
                free($2.sx);
              } ;

            | EEG actl1 {

                Bdd_Edge act1,form1,form1x,result;

                $$.s = (Est_String) malloc(1024);
                $$.sx = (Est_String) malloc(1024);
                sprintf($$.s,"EEG %s",$2.s);
                sprintf($$.sx,"EEG %s",$2.sx);
                McInputstring = $$.s;

                if (trace) printf(">> %s\n",$$.s);
                /*
                if (xtrace) printf("X> %s\n",$$.sx);
                */

                if (McInevitablePrepare) {

                  /* printf("PREPARE> %s\n",$$.s); */
                  inevitableLogItem = McAddEmptyInevitable($$.s,$$.sx);
                  inevitableLogLast = inevitableLogLast->next = inevitableLogItem;
                  inevitableLogLast->inevitableT = bdd_termFalse;
                  inevitableLogLast->inevitableF = bdd_termFalse;

                }

                if (!McNotEvaluate) {
                  act1 = $2.act;
                  form1 = $2.form;

                  if (McInevitable) {

                    form1x = $2.formx;

                    /* fprintf(stderr,"McInevitable: %s\n",inevitableLogLast->sx); */

                    Mc_InevitableCheckEEG(McComp,
                      &inevitableLogLast->inevitableT,&inevitableLogLast->inevitableF,
                      act1,form1,form1x);

                    $$.f = inevitableLogLast->inevitableT;
                    $$.fx = inevitableLogLast->inevitableF;

                    inevitableLogLast = inevitableLogLast->next;

                  } else {

                    result = Mc_CheckEEG(McD,act1,form1);
                    $$.f = result;

                    if (diagnostic || tree || automaton) {
                      McAddDiagnostic(&$$.item,result,act1,form1,
                                    bdd_termNull,bdd_termNull,MC_EEG,
                                    $$.s,$$.sx,$2.item,NULL);
                    }

                  }
                }

                free($2.s);
                free($2.sx);
              } ;

            | EEG actl2 {

                Bdd_Edge act1,form1,form1x,result;

                $$.s = (Est_String) malloc(1024);
                $$.sx = (Est_String) malloc(1024);
                sprintf($$.s,"EEG %s",$2.s);
                sprintf($$.sx,"EEG %s",$2.sx);
                McInputstring = $$.s;

                if (trace) printf(">> %s\n",$$.s);
                /*
                if (xtrace) printf("X> %s\n",$$.sx);
                */

                if (McInevitablePrepare) {

                  /* printf("PREPARE> %s\n",$$.s); */
                  inevitableLogItem = McAddEmptyInevitable($$.s,$$.sx);
                  inevitableLogLast = inevitableLogLast->next = inevitableLogItem;
                  inevitableLogLast->inevitableT = bdd_termFalse;
                  inevitableLogLast->inevitableF = bdd_termFalse;

                }

                if (!McNotEvaluate) {
                  act1 = $2.act;
                  form1 = $2.form;

                  if (McInevitable) {

                    form1x = $2.formx;

                    /* fprintf(stderr,"McInevitable: %s\n",inevitableLogLast->sx); */

                    Mc_InevitableCheckEEG(McComp,
                      &inevitableLogLast->inevitableT,&inevitableLogLast->inevitableF,
                      act1,form1,form1x);

                    /* NON-STRICT */
                    result = Bdd_ITE(inevitableLogLast->inevitableT,form1,bdd_termFalse);
                    Bdd_Fortify(result);
                    $$.f = result;

                    /* NON-STRICT */
                    result = Bdd_ITE(inevitableLogLast->inevitableF,bdd_termTrue,form1x);
                    Bdd_Fortify(result);
                    $$.fx = result;

                    inevitableLogLast = inevitableLogLast->next;

                  } else {

                    result = Mc_CheckEEG(McD,act1,form1);
                    result = Bdd_ITE(result,form1,bdd_termFalse); /* NON-STRICT */
                    $$.f = result;

                    if (diagnostic || tree || automaton) {
                      McAddDiagnostic(&$$.item,result,act1,form1,
                                    bdd_termNull,bdd_termNull,MC_EEG_NS,
                                    $$.s,$$.sx,$2.item,NULL);
                    }

                  }
                }

                free($2.s);
                free($2.sx);
              } ;

            | AAG actl1 {

                Bdd_Edge act1,form1,form1x,result;

                $$.s = (Est_String) malloc(1024);
                $$.sx = (Est_String) malloc(1024);
                sprintf($$.s,"AAG %s",$2.s);
                sprintf($$.sx,"AAG %s",$2.sx);
                McInputstring = $$.s;

                if (trace) printf(">> %s\n",$$.s);
                /*
                if (xtrace) printf("X> %s\n",$$.sx);
                */

                if (McInevitablePrepare) {

                  /* printf("PREPARE> %s\n",$$.s); */
                  inevitableLogItem = McAddEmptyInevitable($$.s,$$.sx);
                  inevitableLogLast = inevitableLogLast->next = inevitableLogItem;
                  inevitableLogLast->inevitableT = bdd_termFalse;
                  inevitableLogLast->inevitableF = bdd_termFalse;

                }

                if (!McNotEvaluate) {
                  act1 = $2.act;
                  form1 = $2.form;

                  if (McInevitable) {

                    form1x = $2.formx;

                    /* fprintf(stderr,"McInevitable: %s\n",inevitableLogLast->sx); */

                    Mc_InevitableCheckAAG(McComp,
                      &inevitableLogLast->inevitableT,&inevitableLogLast->inevitableF,
                      act1,form1,form1x);

                    $$.f = inevitableLogLast->inevitableT;
                    $$.fx = inevitableLogLast->inevitableF;

                    inevitableLogLast = inevitableLogLast->next;

                  } else {

                    result = Mc_CheckAAG(McD,act1,form1);
                    $$.f = result;

                    if (diagnostic || tree || automaton) {
                      McAddDiagnostic(&$$.item,result,act1,form1,
                                    bdd_termNull,bdd_termNull,MC_AAG,
                                    $$.s,$$.sx,$2.item,NULL);
                    }

                  }
                }

                free($2.s);
                free($2.sx);
              } ;

            | AAG actl2 {

                Bdd_Edge act1,form1,form1x,result;

                $$.s = (Est_String) malloc(1024);
                $$.sx = (Est_String) malloc(1024);
                sprintf($$.s,"AAG %s",$2.s);
                sprintf($$.sx,"AAG %s",$2.sx);
                McInputstring = $$.s;

                if (trace) printf(">> %s\n",$$.s);
                /*
                if (xtrace) printf("X> %s\n",$$.sx);
                */

                if (McInevitablePrepare) {

                  /* printf("PREPARE> %s\n",$$.s); */
                  inevitableLogItem = McAddEmptyInevitable($$.s,$$.sx);
                  inevitableLogLast = inevitableLogLast->next = inevitableLogItem;
                  inevitableLogLast->inevitableT = bdd_termFalse;
                  inevitableLogLast->inevitableF = bdd_termFalse;

                }

                if (!McNotEvaluate) {
                  act1 = $2.act;
                  form1 = $2.form;

                  if (McInevitable) {

                    form1x = $2.formx;

                    /* fprintf(stderr,"McInevitable: %s\n",inevitableLogLast->sx); */

                    Mc_InevitableCheckAAG(McComp,
                      &inevitableLogLast->inevitableT,&inevitableLogLast->inevitableF,
                      act1,form1,form1x);

                    /* NON-STRICT */
                    result = Bdd_ITE(inevitableLogLast->inevitableT,form1,bdd_termFalse);
                    Bdd_Fortify(result);
                    $$.f = result;

                    /* NON-STRICT */
                    result = Bdd_ITE(inevitableLogLast->inevitableF,bdd_termTrue,form1x);
                    Bdd_Fortify(result);
                    $$.fx = result;

                    inevitableLogLast = inevitableLogLast->next;

                  } else {

                    result = Mc_CheckAAG(McD,act1,form1);
                    result = Bdd_ITE(result,form1,bdd_termFalse); /* NON-STRICT */
                    $$.f = result;

                    if (diagnostic || tree || automaton) {
                      McAddDiagnostic(&$$.item,result,act1,form1,
                                    bdd_termNull,bdd_termNull,MC_AAG_NS,
                                    $$.s,$$.sx,$2.item,NULL);
                    }

                  }
                }

                free($2.s);
                free($2.sx);
              } ;

actl1     : '{' act_form '}' actl {

              $$.s = (Est_String) malloc(1024);
              $$.sx = (Est_String) malloc(1024);
              sprintf($$.s,"{%s} %s",$2.s,$4.s);
              sprintf($$.sx,"{%s} %s",$2.s,$4.sx);
              McInputstring = $$.s;

              if (trace) printf(">> %s\n",$$.s);
              /*
              if (xtrace) printf("X> %s\n",$$.sx);
              */

              if (!McNotEvaluate) {
                $$.act = $2.f;
                $$.form = $4.f;

                $$.item = $4.item;
              }

              free($2.s);
              free($4.s);
              free($4.sx);
            } ;

          | '{' act_form '}' {

              $$.s = (Est_String) malloc(1024);
              $$.sx = (Est_String) malloc(1024);
              sprintf($$.s,"{%s}",$2.s);
              sprintf($$.sx,"{%s} true",$2.s);
              McInputstring = $$.s;

              if (trace) printf(">> %s\n",$$.s);
              /*
              if (xtrace) printf("X> %s\n",$$.sx);
              */

              if (McInevitablePrepare) {

                /* printf("PREPARE> %s\n",$$.s); */

                inevitableLogItem = McAddEmptyInevitable("true","true");
                if (!inevitableLogLast) {
                  inevitableLog = inevitableLogLast = inevitableLogItem;
                } else {
                  inevitableLogLast = inevitableLogLast->next = inevitableLogItem;
                }

              }

              if (!McNotEvaluate) {
                $$.act = $2.f;

                if (McInevitable) {

                  /* fprintf(stderr,"McInevitable: %s\n",inevitableLogLast->sx); */

                  $$.form = bdd_termTrue;
                  $$.formx = bdd_termFalse;

                  inevitableLogLast = inevitableLogLast->next;

                } else {

                  $$.form = bdd_termTrue;

                  if (diagnostic || tree || automaton) {
                    McAddDiagnostic(&$$.item,bdd_termTrue,bdd_termNull,bdd_termTrue,
                                  bdd_termNull,bdd_termNull,MC_CONST,
                                  "true","true",NULL,NULL);
                  }

                }
              }

              free($2.s);
            } ;

          | actl {

              $$.s = (Est_String) malloc(1024);
              $$.sx = (Est_String) malloc(1024);
              sprintf($$.s,"%s",$1.s);
              sprintf($$.sx,"%s {true}",$1.sx);
              McInputstring = $$.s;

              if (trace) printf(">> %s\n",$$.s);
              /*
              if (xtrace) printf("X> %s\n",$$.sx);
              */

              if (!McNotEvaluate) {
                $$.act = bdd_termTrue;
                $$.form = $1.f;

                $$.item = $1.item;
              }

              free($1.s);
              free($1.sx);
            } ;

actl2     : actl '{' act_form '}' {

              $$.s = (Est_String) malloc(1024);
              $$.sx = (Est_String) malloc(1024);
              sprintf($$.s,"%s {%s}",$1.s,$3.s);
              sprintf($$.sx,"%s {%s}",$1.sx,$3.s);
              McInputstring = $$.s;

              if (trace) printf(">> %s\n",$$.s);
              /*
              if (xtrace) printf("X> %s\n",$$.sx);
              */

              if (!McNotEvaluate) {
                $$.act = $3.f;
                $$.form = $1.f;

                $$.item = $1.item;
              }

              free($1.s);
              free($1.sx);
              free($3.s);
            } ;

single_act  : UNKNOWN {
                Est_String tmpstr;
                tmpstr = (Est_String) malloc(127);
                sprintf(tmpstr,"incorrect action name %s",$1);
                error(tmpstr);
                free(tmpstr);
                free($1);
                YYERROR;
              } ;

            | VALTRUE {

                $$.s = strdup($1);

                if (!McNotEvaluate) {
                  $$.f = bdd_termTrue;
                }

                free($1);
              } ;

            | VALFALSE {

                $$.s = strdup($1);

                if (!McNotEvaluate) {
                  $$.f = bdd_termFalse;
                }

                free($1);
              } ;

            | ACTION {

                Est_String action;
                Bdd_Edge p;

                $$.s = strdup($1);

                if (!McNotEvaluate) {
                  action = strdup($1);
                  p = findAction(&pa_sortTable[McSort],action);
                  if (Bdd_isEqv(p,bdd_termNull)) {
                    Est_String tmpstr;

                    tmpstr = (Est_String) malloc(127);
                    sprintf(tmpstr,"ERROR: unknown action %s",action);
                    error(tmpstr);
                    free(tmpstr);

                    free(action);
                    free($1);
                    YYERROR;
                  } else {

                    if (Bdd_isEqv(p,bdd_termFalse)) {
                      printf("WARNING: unknown action %s\n",action);
                    }

                    Bdd_Fortify(p);
                    $$.f = p;
                    free(action);
                  }
                }

                free($1);
              } ;

act_form  : TAU {

              $$.s = strdup($1);

              if (!McNotEvaluate) {
                $$.f = McTau;
              }

              free($1);
            } ;

          | single_act {

              $$.s = strdup($1.s);

              if (!McNotEvaluate) {
                $$.f = $1.f;
              }

              free($1.s);
            } ;

vis_act_form  : single_act {

                  $$.s = strdup($1.s);

                  if (!McNotEvaluate) {
                    $$.f = $1.f;
                  }

                  free($1.s);
                } ;

act_form  : NOT act_form {

              Bdd_Edge result;

              $$.s = (Est_String) malloc(1024);
              sprintf($$.s,"NOT %s",$2.s);

              if (!McNotEvaluate) {
                result = Bdd_NOT($2.f); /* CAREFULLY! */
                Bdd_Fortify(result);
                $$.f = result;
              }

              free($2.s);
            } ;

          | act_form AND act_form {

              Bdd_Edge result;

              $$.s = (Est_String) malloc(1024);
              sprintf($$.s,"%s AND %s",$1.s,$3.s);

              if (!McNotEvaluate) {
                result = Bdd_ITE($1.f,$3.f,bdd_termFalse);
                Bdd_Fortify(result);
                $$.f = result;
              }

              free($1.s);
              free($3.s);
            } ;

          | act_form OR act_form {

              Bdd_Edge result;

              $$.s = (Est_String) malloc(1024);
              sprintf($$.s,"%s OR %s",$1.s,$3.s);

              if (!McNotEvaluate) {
                result = Bdd_ITE($1.f,bdd_termTrue,$3.f);
                Bdd_Fortify(result);
                $$.f = result;
              }

              free($1.s);
              free($3.s);
            } ;

          | act_form EQV act_form {

              Bdd_Edge result;

              $$.s = (Est_String) malloc(1024);
              sprintf($$.s,"%s EQV %s",$1.s,$3.s);

              if (!McNotEvaluate) {
                result = Bdd_ITE($1.f,$3.f,Bdd_NOT($3.f));
                Bdd_Fortify(result);
                $$.f = result;
              }

              free($1.s);
              free($3.s);
            } ;

          | act_form IMPL act_form {

              Bdd_Edge result;

              $$.s = (Est_String) malloc(1024);
              sprintf($$.s,"%s IMPL %s",$1.s,$3.s);

              if (!McNotEvaluate) {
                result = Bdd_ITE($1.f,$3.f,bdd_termTrue);
                Bdd_Fortify(result);
                $$.f = result;
              }

              free($1.s);
              free($3.s);
            } ;

          | '(' act_form ')' {

              $$.s = (Est_String) malloc(1024);
              sprintf($$.s,"(%s)",$2.s);

              if (!McNotEvaluate) {
                $$.f = $2.f;
              }

              free($2.s);
            } ;

vis_act_form  : NOT vis_act_form {

                  Bdd_Edge result;

                  $$.s = (Est_String) malloc(1024);
                  sprintf($$.s,"NOT %s",$2.s);

                  if (!McNotEvaluate) {
                    result = Bdd_NOT($2.f); /* CAREFULLY! */
                    Bdd_Fortify(result);
                    $$.f = result;
                  }

                  free($2.s);
                } ;

              | vis_act_form AND vis_act_form {

                  Bdd_Edge result;

                  $$.s = (Est_String) malloc(1024);
                  sprintf($$.s,"%s AND %s",$1.s,$3.s);

                  if (!McNotEvaluate) {
                    result = Bdd_ITE($1.f,$3.f,bdd_termFalse);
                    Bdd_Fortify(result);
                    $$.f = result;
                  }

                  free($1.s);
                  free($3.s);
                } ;

              | vis_act_form OR vis_act_form {

                  Bdd_Edge result;

                  $$.s = (Est_String) malloc(1024);
                  sprintf($$.s,"%s OR %s",$1.s,$3.s);

                  if (!McNotEvaluate) {
                    result = Bdd_ITE($1.f,bdd_termTrue,$3.f);
                    Bdd_Fortify(result);
                    $$.f = result;
                  }

                  free($1.s);
                  free($3.s);
                } ;

              | vis_act_form EQV vis_act_form {

                  Bdd_Edge result;

                  $$.s = (Est_String) malloc(1024);
                  sprintf($$.s,"%s EQV %s",$1.s,$3.s);

                  if (!McNotEvaluate) {
                    result = Bdd_ITE($1.f,$3.f,Bdd_NOT($3.f));
                    Bdd_Fortify(result);
                    $$.f = result;
                  }

                  free($1.s);
                  free($3.s);
                } ;

              | vis_act_form IMPL vis_act_form {

                  Bdd_Edge result;

                  $$.s = (Est_String) malloc(1024);
                  sprintf($$.s,"%s IMPL %s",$1.s,$3.s);

                  if (!McNotEvaluate) {
                    result = Bdd_ITE($1.f,$3.f,bdd_termTrue);
                    Bdd_Fortify(result);
                    $$.f = result;
                  }

                  free($1.s);
                  free($3.s);
                } ;

              | '(' vis_act_form ')' {

                  $$.s = (Est_String) malloc(1024);
                  sprintf($$.s,"(%s)",$2.s);

                  if (!McNotEvaluate) {
                    $$.f =$2.f;
                  }

                  free($2.s);
                } ;

%%

#include <lex.mc.c>

/* I need this on MACOSX with flex 2.5.35 and bison 2.3 */
#ifdef ESTMACOSX
#define yy_scan_string mc_scan_string
#endif

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

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

void
Mc_CheckACTL(int par, Est_String name, Est_String f, int parserSettings)
{
  int i;

  i = Mc_FindFormula(f);
  if (i == -1) {
    printf("\nERROR: Formula %s does not exist.\n",f);
    return;
  }

  Mc_CheckACTLString(par,name,mc_formulaTable[i].formula,parserSettings);
}

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

void
Mc_CheckACTLString(int par, Est_String name, Est_String f, int parserSettings)
{
  YY_BUFFER_STATE buffer;
  Est_String formula;
  int step = 1; /* NUMBER OF STEPS IN ONE LOOP */
  int i,n;
  Est_Boolean onthefly,inevitableTrue,inevitableFalse,isd,ist,isa;
  int num1,num2;
  Bdd_Edge snew,swait;

  McInputstring = NULL;
  McFormulaName = NULL;
  McFileName = NULL;
  McWCAname = NULL;
  McAddFormula = FALSE;
  McNotEvaluate = FALSE;
  McInevitablePrepare = FALSE;
  McInevitable = FALSE;
  McIdent = 0;

  if (init(par,name,parserSettings) == -1) {
    return;
  }

  formula = strdup(f);

  if (McComp == -1) {
    onthefly = FALSE;
  } else {
    onthefly = pa_compositionTable[McComp].onthefly;
  }

  /* TESTING: CREATE FULL COMPOSITION WITHOUT INEVITABLE MC */
  /*
  if (onthefly) {
    i = 0;
    Versis_ComposeInit(name);
    do {
      i++;
      n = Versis_ComposeStep(McComp,step);
      if (progress) {
        num1 = Pa_DecodeCompStates(&pa_compositionTable[McComp],
                                   pa_compositionTable[McComp].stateBDD,FALSE);
        num2 = Pa_DecodeCompStates(&pa_compositionTable[McComp],
                                   pa_compositionTable[McComp].snew,FALSE);
        printf("[%d:%d/%d]",i,num1,num2);
      }
    } while (!(n < step));
    Bdd_Fortify(pa_compositionTable[McComp].stateBDD);
    Bdd_Fortify(pa_compositionTable[McComp].snew);
    Versis_ComposeFinish(McComp);
    McD = pa_compositionTable[McComp].transitionBDD;
    Bdd_IncCounter();

    onthefly = FALSE;
    printf("==> SKIPPED\n");
  }
  */

  if ((McComp != -1) && onthefly) {

    isd = diagnostic;
    ist = tree;
    isa = automaton;

    diagnostic = FALSE;
    tree = FALSE;
    automaton = FALSE;

    /* ON-THE-FLY MODEL CHECKING */

    /* PREPARE INEVITABLE MODEL CHECKING */

    McNotEvaluate = TRUE;
    McInevitablePrepare = TRUE;
    McInevitable = FALSE;
    McIdent = 0;

    inevitableLog = NULL;
    inevitableLogLast = NULL;

    buffer = mc_scan_string(formula);
    yyparse();
    yy_delete_buffer(buffer);

    /*
    inevitableLogLast = inevitableLog;
    while (inevitableLogLast) {
      fprintf(stderr,"INEVITABLE INIT: %s\n",inevitableLogLast->sx);
      inevitableLogLast = inevitableLogLast->next;
    }
    */

    /* DO STEP COMPOSTION + INEVITABLE MODEL CHECKING */

    i = 0;
    Versis_ComposeInit(name);

    /* REPORT ABOUT PROGRESS */
    if (progress) {
      num1 = Pa_DecodeCompStates(&pa_compositionTable[McComp],
                                 pa_compositionTable[McComp].stateBDD,FALSE);
      num2 = Pa_DecodeCompStates(&pa_compositionTable[McComp],
                                 pa_compositionTable[McComp].snew,FALSE);
      /* fprintf(stdout,"[STEP %d STATES: %dall/%dnew]",i,num1,num2); */
      printf("[STEP %d STATES: %dall/%dnew]",i,num1,num2);
    }

    do {

      i++;

      /* HEVRISTICS FOR ON-THE-FLY MODEL CHECKING */
      /* DIVIDE NEW STATES INTO TWO PARTS */
      /* snew WILL BE INVESTIGATED IN THE NEXT STEP */
      /* swait WILL NOT BE INVESTIGATED IN THE NEXT STEP */

      /* USE ALL NEW STATES */
      snew = pa_compositionTable[McComp].snew;
      swait = bdd_termFalse;

      /* USE SOME OF NEW STATES */
      /*
      snew = Bdd_ExtractBranch(pa_compositionTable[McComp].snew);
      Bdd_Fortify(snew);
      swait = Bdd_ITE(snew,bdd_termFalse,pa_compositionTable[McComp].snew);
      Bdd_Fortify(swait);
      */

      /* STEP-BY-STEP COMPOSITION */

      pa_compositionTable[McComp].snew = snew;
      n = Versis_ComposeStep(McComp,step);

      /* USE THIS IF MC USES transitionBDD, NOT NEEDED IF MC USES di AND dij */
      /*
      Versis_ComposeFinish(McComp);
      McD = pa_compositionTable[McComp].transitionBDD;
      */

      pa_compositionTable[McComp].snew = Bdd_ITE(pa_compositionTable[McComp].snew,
                                                 bdd_termTrue,swait);

      /* REPORT ABOUT PROGRESS */
      if (progress) {
        num1 = Pa_DecodeCompStates(&pa_compositionTable[McComp],
                                   pa_compositionTable[McComp].stateBDD,FALSE);
        num2 = Pa_DecodeCompStates(&pa_compositionTable[McComp],
                                   pa_compositionTable[McComp].snew,FALSE);
        /* fprintf(stdout,"[STEP %d STATES: %dall/%dnew]",i,num1,num2); */
        printf("[STEP %d STATES: %dall/%dnew]",i,num1,num2);
      }

      /* CALCULATE INEVITABLE TRUE/FALSE STATES */

      McNotEvaluate = FALSE;
      McInevitablePrepare = FALSE;
      McInevitable = TRUE;
      McIdent = 0;

      inevitableLogLast = inevitableLog;

      buffer = mc_scan_string(formula);
      yyparse();
      yy_delete_buffer(buffer);

      inevitableTrue = McResult;
      inevitableFalse = McResultX;

      /*
      num1 = Pa_DecodeCompStates(&pa_compositionTable[McComp],McResultSet,FALSE);
      fprintf(stderr,"Obtained %d INEVITABLE TRUE STATES\n",num1);
      */

      /*
      num1 = Pa_DecodeCompStates(&pa_compositionTable[McComp],McResultSetX,FALSE);
      fprintf(stderr,"Obtained %d INEVITABLE FALSE STATES\n",num1);
      */
      /* REPORT ABOUT SUBFORMULAE */

      /*
      inevitableLogLast = inevitableLog;
      while (inevitableLogLast) {

        fprintf(stderr,"(%d) SUBFORMULA: %s\n",i,inevitableLogLast->sx);
        if (!Bdd_isNull(inevitableLogLast->inevitable1)) {
          num1 = Pa_DecodeCompStates(&pa_compositionTable[McComp],inevitableLogLast->inevitable1,FALSE);
          fprintf(stderr,"inevitable1: %d states ",num1);

          if (num1 == 25) {
            printf("\n STATES:\n");
            Pa_DecodeCompStates(&pa_compositionTable[McComp],inevitableLogLast->inevitable1,TRUE);
            printf("\n TRANSITIONS:\n");
            Pa_DecodeCompTR(&pa_compositionTable[McComp],Bdd_ITE(pa_compositionTable[McComp].transitionBDD,inevitableLogLast->inevitable1,bdd_termFalse),TRUE);
          }

        } else fprintf(stderr,"inevitable1: NULL ");
        if (!Bdd_isNull(inevitableLogLast->inevitable2)) {
          num1 = Pa_DecodeCompStates(&pa_compositionTable[McComp],inevitableLogLast->inevitable2,FALSE);
          fprintf(stderr,"inevitable2: %d states ",num1);
        }

        inevitableLogLast = inevitableLogLast->next;
      }
      */

    } while (!((n < step) && Bdd_isEqv(swait,bdd_termFalse)) &&
             !inevitableFalse &&
             !inevitableTrue);

    Bdd_Fortify(pa_compositionTable[McComp].stateBDD);
    Bdd_Fortify(pa_compositionTable[McComp].snew);

    /* USE THIS IF MC USES di AND dij, NOT NEEDED IF MC USES transitionBDD */
    /**/
    Versis_ComposeFinish(McComp);
    McD = pa_compositionTable[McComp].transitionBDD;
    /**/

    if (progress) {

      if (inevitableFalse) {
        printf(" ==> INEVITABLE FALSE\n");
      }

      if (inevitableTrue) {
        printf(" ==> INEVITABLE TRUE\n");
      }

      if (!inevitableFalse && !inevitableTrue) {
        printf(" ==> UNDECIDABLE\n");
      }

    }

    diagnostic = isd;
    tree = ist;
    automaton = isa;

    /* TO GET MORE USABLE RESULTS FROM FOLLOWED MODEL CHECKING */
    /* PERFORM MINIMIZATION WHEN REQUIRED BY COMPOSITION */
    /* THIS IS EXPERIMENTAL, ONLY */

    /* TRACE MINIMIZATION */
    if ((diagnostic || tree || automaton) && pa_compositionTable[McComp].trace) {
      printf("Generating deterministic trace-equivalent process ...");
      McProc = Versis_Minimization(3,1,name);
    }

    /* WEAK MINIMIZATION */
    if ((diagnostic || tree || automaton) && pa_compositionTable[McComp].weak) {
      printf("Generating weak-equivalent process ...");
      McProc = Versis_Minimization(1,1,name);
    }

    /* STRONG MINIMIZATION */
    if ((diagnostic || tree || automaton) && pa_compositionTable[McComp].strong) {
      printf("Generating strong-equivalent process ...");
      McProc = Versis_Minimization(0,1,name);
    }

    /* IN MODEL CHECKING, COMPOSITIONS ARE TREATED EQUAL TO PROCESSES */
    if (pa_compositionTable[McComp].full) {
    }

    if (McProc != -1) {
      Pa_RenameProcess(pa_processTable[McProc].name,name);
      McInit = pa_processTable[McProc].tableS[pa_processTable[McProc].initial].bddR;
      McD = pa_processTable[McProc].d;
      McComp = -1;
      printf(" OK\n");
    }

    printf("System partially composed (DEPTH = %d)",i);
  }

  /* PERFORM NORMAL MODEL CHECKING */

  McNotEvaluate = FALSE;
  McInevitablePrepare = FALSE;
  McInevitable = FALSE;
  McIdent = 0;

  if (diagnostic || tree || automaton){
     McDgn = McCreateDiagnostic(McD,McInit,McProc,McComp);
  }

  buffer = mc_scan_string(formula);
  yyparse();
  yy_delete_buffer(buffer);

  if (diagnostic || tree || automaton) {
    McDeleteDiagnostic(McDgn.item);
  }

  free(formula);

  return;
}

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

void
Mc_CheckACTLFile(int par, Est_String name, Est_String f, int parserSettings)
{
  YY_BUFFER_STATE buffer;

  McInputstring = NULL;
  McFormulaName = NULL;
  McFileName = strdup(f);
  McWCAname = NULL;
  McAddFormula = TRUE;
  McNotEvaluate = FALSE;
  McInevitablePrepare = FALSE;
  McInevitable = FALSE;
  McIdent = 0;

  if (init(par,name,parserSettings) == -1) {
    return;
  }

  if ((McComp != -1) && pa_compositionTable[McComp].onthefly) {
    free(McFileName);
    printf("ERROR: Mc_CheckACTLFile cannot perform on-the-fly model checking.\n");
    printf("Please, use Mc_ReadACTLFile + Mc_CheckACTL or Mc_CheckACTLString\n");
    return;
  }

  yyin = fopen(f,"r");
  if(yyin != NULL) {
    if (diagnostic || tree || automaton){
       McDgn = McCreateDiagnostic(McD,McInit,McProc,McComp);
    }

    buffer = yy_create_buffer(yyin,YY_BUF_SIZE);
    yy_switch_to_buffer(buffer);
    yyparse();
    yy_delete_buffer(buffer);

    fclose(yyin);
    if (diagnostic || tree || automaton) {
      McDeleteDiagnostic(McDgn.item);
    }
  } else {
    printf("ERROR: Cannot open file %s.\n",f);
  }

  free(McFileName);

  return;
}

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

void
Mc_GenerateWCA(Est_String name, Est_String f, Est_String aname)
{
  YY_BUFFER_STATE buffer;
  Est_String formula;
  int i;

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

  McInputstring = NULL;
  McFormulaName = NULL;
  McFileName = NULL;
  McWCAname = strdup(aname);
  McAddFormula = FALSE;
  McNotEvaluate = FALSE;
  McInevitablePrepare = FALSE;
  McInevitable = FALSE;
  McIdent = 4;

  i = Pa_FindProcess(name);
  if (i == -1) {
    free(McWCAname);
    printf("\nProces %s does not exist.\n",name);
    return;
  }
  if (!pa_processTable[i].encoded) {
    /* if process is not encoded, do this now */
    Pa_EncodeProcess(name);
  }
  McProc = i;
  McComp = -1;
  McSort = pa_processTable[i].sort;
  McInit = pa_processTable[i].tableS[pa_processTable[i].initial].bddR;
  McD = pa_processTable[i].d;
  McTau = pa_sortTable[McSort].table[0].p;

  McDgn = McCreateDiagnostic(McD,McInit,McProc,McComp);

  i = Mc_FindFormula(f);
  if (i == -1) {
    free(McWCAname);
    printf("  Formula %s does not exist.\n",f);
    return;
  }
  formula = strdup(mc_formulaTable[i].formula);

  buffer = mc_scan_string(formula);
  yyparse();
  yy_delete_buffer(buffer);

  McDeleteDiagnostic(McDgn.item);

  free(McWCAname);
  free(formula);
  return;
}

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

void
Mc_ReadACTL(Est_String name, Est_String f)
{
  YY_BUFFER_STATE buffer;
  Est_String formula;

  McInputstring = NULL;
  McFormulaName = strdup(name);
  McFileName = NULL;
  McWCAname = NULL;
  McAddFormula = TRUE;
  McNotEvaluate = TRUE;
  McInevitablePrepare = FALSE;
  McInevitable = FALSE;
  McIdent = 0;

  formula = strdup(f);

  buffer = mc_scan_string(formula);
  yyparse();
  yy_delete_buffer(buffer);

  free(formula);
  free(McFormulaName);

  return;
}

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

void
Mc_ReadACTLFile(Est_String f)
{
  YY_BUFFER_STATE buffer;

  McInputstring = NULL;
  McFormulaName = NULL;
  McFileName = strdup(f);
  McWCAname = NULL;
  McAddFormula = TRUE;
  McNotEvaluate = TRUE;
  McInevitablePrepare = FALSE;
  McInevitable = FALSE;
  McIdent = 0;

  yyin = fopen(f,"r");
  if(yyin != NULL) {

    buffer = yy_create_buffer(yyin,YY_BUF_SIZE);
    yy_switch_to_buffer(buffer);
    yyparse();
    yy_delete_buffer(buffer);

    fclose(yyin);
  } else {
    printf("ERROR: Cannot open file %s.\n",f);
  }

  free(McFileName);

  return;
}

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

/**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 int
init(int par, Est_String name, int parserSettings)
{
  int i;

  trace = ((parserSettings & MC_TRACE) != 0);            /* trace of ACTL parsing */
  xtrace = ((parserSettings & MC_XTRACE) != 0);          /* extended trace of ACTL parsing */
  explain = ((parserSettings & MC_EXPLAIN) != 0);        /* explain generated diagnostic */
  tracepath = ((parserSettings & MC_TRACEPATH) != 0);    /* full paths in diagnostic */
  diagnostic = ((parserSettings & MC_DIAGNOSTIC) != 0);  /* generate linear w/c */
  automaton = ((parserSettings & MC_AUTOMATON) != 0);    /* generate w/c automaton */
  minimize = ((parserSettings & MC_MINIMIZE) != 0);      /* minimize w/c automaton */
  tree = ((parserSettings & MC_TREE) != 0);              /* generate tree-like w/c */
  progress = ((parserSettings & MC_PROGRESS) != 0);      /* report progress of MC */

  /*
  if (diagnostic) fprintf(stderr,"DIAGNOSTIC IS ON\n");
    else fprintf(stderr,"DIAGNOSTIC IS OFF\n");
  if (tree) fprintf(stderr,"TREE IS ON\n");
    else fprintf(stderr,"TREE IS OFF\n");
  */

  i = -1;
  if (par == 0) {
    i = Pa_FindProcess(name);
    if (i == -1) {
      printf("\nProces %s does not exist.\n",name);
      return -1;
    }
    if (!pa_processTable[i].encoded) {
      /* if process is not encoded, do this now */
      Pa_EncodeProcess(name);
      /* if encoding is not possible */
      if (!pa_processTable[i].encoded) return -1;
    }
    McProc = i;
    McComp = -1;
  }

  if (par == 1) {
    i = Pa_FindComposition(name);
    if (i == -1) {
      printf("\nComposition %s does not exist.\n",name);
      return -1;
    }

    McProc = -1;
    McComp = i;
  }

  if (par == 0) {
    McSort = pa_processTable[i].sort;
    McInit = pa_processTable[i].tableS[pa_processTable[i].initial].bddR;
    McD = pa_processTable[i].d;
  } else {
    McSort = pa_compositionTable[i].sort;
    McInit = pa_compositionTable[i].initialBDD;

    if (pa_compositionTable[i].onthefly) {
      printf(" (On-the-fly)\n");
      McD = bdd_termNull;
    } else {
      McD = pa_compositionTable[i].transitionBDD;
    }

  }

  McTau = pa_sortTable[McSort].table[0].p;
  McResultSet = bdd_termNull;

  return 0;
}

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

static Bdd_Edge
findAction(Pa_Sort *s, Est_String act)
{
  int type,len,i;
  Bdd_Edge p;

  /* THIS FUNCTION SHOULD NOT BE CALLED FOR ACTION TAU */
  /**/
  if (!strcmp(act,"TAU") || !strcmp(act,"tau") || !strcmp(act,"Tau")) {
    printf("WARNING: Find_Action got action TAU!\n");
    return McTau;
  }
  /**/

  i = -1;
  type = -1;
  if ((act[0] == '?') || (act[0] == '!')) {

    /* action with prefix */
    if (act[0] == '?') {
      type = 0;
    }
    if (act[0] == '!') {
      type = 1;
    }
    i = Pa_FindSortAction(s,&act[1]);

  } else {

    /* action with suffix */
    len = strlen(act);
    if (act[len-1] == '?') {
      type = 0;
    } else if (act[len-1] == '!') {
      type = 1;
    } else {
      return bdd_termNull;
    }
    act[len-1]=0;
    i = Pa_FindSortAction(s,act);

  }

  if (i == -1) {
    return bdd_termFalse;
  } else {
    p = s->table[i].p;
    if (type == 0) {
      p = Bdd_ITE(s->a0,bdd_termFalse,p);
    } else {
      p = Bdd_ITE(s->a0,p,bdd_termFalse);
    }
  }

  return p;
}

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

static void
outline(char *s)
{
  if (strcmp(s,"")) printf("%s",&s[1]);
  printf("\n");
}

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

static int
error(const char *s)
{
  if (McInputstring) {
   printf("%s ??\n",McInputstring);
   McInputstring = NULL;
  } else {
   printf("??\n");
  }
  if (explain) {
    printf("@@ ");
  }
  printf("ERROR in ACTL formula: ");
  if (strstr(s,"UNKNOWN")) {
    printf("unexpected or unknown symbol\n");
  } else {
    printf("%s\n",s);
  }
  return 1;
}

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

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

int
yywrap()
{
  return 1;
}

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

int
yyerror(const char *s)
{
  error(s);
  return 1;
}
