%{
/**CFile*****************************************************************

  FileName    [ctlsp.y]

  PackageName [ctlsp]

  Synopsis    [Yacc for CTL* formula parser.]

  SeeAlso     [ctlsp.h]

  Author      [Mohammad Awedh]

  Copyright   [This file was created at the University of Colorado at Boulder.
  The University of Colorado at Boulder makes no warranty about the suitability
  of this software for any purpose.  It is presented on an AS IS basis.]

******************************************************************************/

#include "ctlspInt.h"

/*
 * The following is a workaround for a bug in bison, which generates code
 * that uses alloca().  Their lengthy sequence of #ifdefs for defining
 * alloca() does the wrong thing for HPUX (it should do what is defined below)
 */
#ifdef __hpux
#  include <alloca.h>
#endif

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

#include "ctlspLex.c"

/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/

%}

/*---------------------------------------------------------------------------*/
/*      Grammar declarations                                                 */
/*---------------------------------------------------------------------------*/

%union {
  Ctlsp_Formula_t *sf;	/* state formula */
  char *str;
}

%type <sf> error formula propformula CTLsFormula
%type <str> name name_vector name_union name_or macro x_mult ax_mult ex_mult

/* %token YYERROR_VERBOSE */

%token TOK_DEFINE
%token TOK_MACRO
%token TOK_ID
%token TOK_ID2
%token TOK_ID_VECTOR
%token TOK_ID_UNION
%token TOK_COMMA
%token TOK_EQIV
%token TOK_FORALL
%token TOK_EXISTS
%token TOK_UNTIL
%token TOK_RELEASE
%token TOK_WEAK_UNTIL
%token TOK_NEXT
%token TOK_EVENTUALLY
%token TOK_GLOBALLY
%token TOK_FORALL_NEXT
%token TOK_FORALL_EVENTUALLY
%token TOK_FORALL_GLOBALLY
%token TOK_EXISTS_NEXT
%token TOK_EXISTS_EVENTUALLY
%token TOK_EXISTS_GLOBALLY
%token TOK_NEXT_MULT
%token TOK_FORALL_NEXT_MULT
%token TOK_EXISTS_NEXT_MULT
%token TOK_THEN
%token TOK_EQ
%token TOK_XOR
%token TOK_AND
%token TOK_OR
%token TOK_NOT
%token TOK_ASSIGN
%token TOK_TRUE
%token TOK_FALSE

/* precedence is specified here from lowest to highest */

%nonassoc TOK_UNTIL TOK_RELEASE TOK_WEAK_UNTIL
%left TOK_THEN
%left TOK_EQ
%left TOK_XOR
%left TOK_OR
%left TOK_AND
%nonassoc TOK_NEXT TOK_EVENTUALLY TOK_GLOBALLY
%nonassoc  TOK_FORALL TOK_EXISTS TOK_FORALL_EVENTUALLY TOK_FORALL_GLOBALLY TOK_EXISTS_NEXT TOK_EXISTS_EVENTUALLY TOK_EXISTS_GLOBALLY
%nonassoc TOK_NOT

%%

/*---------------------------------------------------------------------------*/
/*      Grammar rules                                                        */
/*---------------------------------------------------------------------------*/
formulas     : /* nothing */
	     | formulas formula
	     ;

formula : CTLsFormula ';'
	{
	  if  (Ctlsp_FormulaReadClass($1) == Ctlsp_pathformula_c )
	    {
	     Ctlsp_FormulaFree(CtlspGlobalFormula);
	     (void) fprintf(vis_stderr, "** CTL * error : Invalid CTL* formula (it is path formula) , line %d\n\n", CtlspYylineno);
	     CtlspGlobalFormula = NIL(Ctlsp_Formula_t);
	    }
	  else
	    {
	     CtlspFormulaAddToGlobalArray($1);
	     $$ = $1;
	     /*
	      * The formula is echoed by the lexical analyzer to stdout.
	      * Here we are just printing the line number after it.
	      */
	      CtlspGlobalFormula = NIL(Ctlsp_Formula_t);
	    }
	 }
	| TOK_DEFINE name CTLsFormula
	  { if (!CtlspFormulaAddToTable($2, $3, CtlspMacroTable)){
	     CtlspYyerror("** CTL* error : MACRO ERROR");
	     (void) fprintf(vis_stderr, "Macro \"%s\" is already in table.\n\n",$2);
	     Ctlsp_FormulaFree(CtlspGlobalFormula);
	     $$ = NULL;
	   }else{
	     $$ = $3;
	  }
	   CtlspGlobalFormula = NIL(Ctlsp_Formula_t);
	 }
	| error ';'
	  { $$ = NULL;
	   /*
	    * Error was detected reading the formula. Garbage collect
	    * and print error message.
	    */
	    Ctlsp_FormulaFree(CtlspGlobalFormula);
	    (void) fprintf(vis_stderr, "** ctl* error : Invalid CTL* formula, line %d\n\n", CtlspYylineno);
	    CtlspGlobalFormula = NIL(Ctlsp_Formula_t);
	 }
	 ;

CTLsFormula : propformula
	     {
		Ctlsp_FormulaSetClass($1, Ctlsp_propformula_c);
		Ctlsp_FormulaSetClassOfCTL($1, Ctlsp_CTL_c);
		$$ = $1;
		CtlspGlobalFormula= $$;
	      }
	     | '(' CTLsFormula ')'
	      {
		/*Ctlsp_FormulaSetClass($2,  Ctlsp_FormulaReadClass($2));
		  do nothing, and the formula keeps its old class
		*/
		$$ = $2;
		CtlspGlobalFormula= $$;
	      }
	     | TOK_NOT CTLsFormula
	       { $$ = Ctlsp_FormulaCreate(Ctlsp_NOT_c, $2, NIL(Ctlsp_Formula_t));
		 Ctlsp_FormulaSetClass($$, Ctlsp_FormulaReadClass($2));
		 Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_FormulaReadClassOfCTL($2));
		 CtlspGlobalFormula= $$;
	       }
	     |  CTLsFormula TOK_AND CTLsFormula
	       { $$ = Ctlsp_FormulaCreate(Ctlsp_AND_c, $1, $3);
		 Ctlsp_FormulaSetClass($$, table1(Ctlsp_FormulaReadClass($1),Ctlsp_FormulaReadClass($3)) );
		 if ((Ctlsp_FormulaReadClassOfCTL($1) ==  Ctlsp_CTL_c) && (Ctlsp_FormulaReadClassOfCTL($3) == Ctlsp_CTL_c))
		   {
		     Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_CTL_c);
		   }
		 else
		     Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_NotCTL_c);

		 CtlspGlobalFormula= $$;
	       }
	     | CTLsFormula TOK_OR CTLsFormula
	       { $$ = Ctlsp_FormulaCreate(Ctlsp_OR_c, $1, $3);
		 Ctlsp_FormulaSetClass($$, table1(Ctlsp_FormulaReadClass($1),Ctlsp_FormulaReadClass($3)) );

		 if ((Ctlsp_FormulaReadClassOfCTL($1) ==  Ctlsp_CTL_c) && (Ctlsp_FormulaReadClassOfCTL($3) == Ctlsp_CTL_c))
		   {
		     Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_CTL_c);
		   }
		 else
		     Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_NotCTL_c);

		 CtlspGlobalFormula= $$;
	       }
	     | CTLsFormula TOK_THEN CTLsFormula
	       { $$ = Ctlsp_FormulaCreate(Ctlsp_THEN_c, $1, $3);
		 Ctlsp_FormulaSetClass($$, table1(Ctlsp_FormulaReadClass($1),Ctlsp_FormulaReadClass($3)) );

		 if ((Ctlsp_FormulaReadClassOfCTL($1) ==  Ctlsp_CTL_c) && (Ctlsp_FormulaReadClassOfCTL($3) == Ctlsp_CTL_c))
		   {
		     Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_CTL_c);
		   }
		 else
		     Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_NotCTL_c);

		 CtlspGlobalFormula= $$;
	       }
	     | CTLsFormula TOK_EQ CTLsFormula
	       { $$ = Ctlsp_FormulaCreate(Ctlsp_EQ_c, $1, $3);
		 Ctlsp_FormulaSetClass($$, table1(Ctlsp_FormulaReadClass($1),Ctlsp_FormulaReadClass($3)) );

		 if ((Ctlsp_FormulaReadClassOfCTL($1) ==  Ctlsp_CTL_c) && (Ctlsp_FormulaReadClassOfCTL($3) == Ctlsp_CTL_c))
		   {
		     Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_CTL_c);
		   }
		 else
		     Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_NotCTL_c);

		 CtlspGlobalFormula= $$;
	       }
	     | CTLsFormula TOK_XOR CTLsFormula
	       { $$ = Ctlsp_FormulaCreate(Ctlsp_XOR_c, $1, $3);
		 Ctlsp_FormulaSetClass($$, table1(Ctlsp_FormulaReadClass($1),Ctlsp_FormulaReadClass($3)) );
		 if ((Ctlsp_FormulaReadClassOfCTL($1) ==  Ctlsp_CTL_c) && (Ctlsp_FormulaReadClassOfCTL($3) == Ctlsp_CTL_c))
		   {
		     Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_CTL_c);
		   }
		 else
		     Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_NotCTL_c);
		 CtlspGlobalFormula= $$;
	       }

	     | TOK_NEXT CTLsFormula
	       { $$ = Ctlsp_FormulaCreate(Ctlsp_X_c, $2, NIL(Ctlsp_Formula_t));
		 Ctlsp_FormulaSetClass($$, table2(Ctlsp_FormulaReadClass($2)));
		 if (Ctlsp_FormulaReadClassOfCTL($2) ==  Ctlsp_CTL_c)
		   {
		     Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_PathCTL_c);
		   }
		 else
		     Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_NotCTL_c);
		 CtlspGlobalFormula= $$;
	       }
	     | TOK_EVENTUALLY CTLsFormula
	       { $$ = Ctlsp_FormulaCreate(Ctlsp_F_c, $2, NIL(Ctlsp_Formula_t));
		 Ctlsp_FormulaSetClass($$, table2(Ctlsp_FormulaReadClass($2)));
		 if (Ctlsp_FormulaReadClassOfCTL($2) ==  Ctlsp_CTL_c)
		   {
		     Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_PathCTL_c);
		   }
		 else
		     Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_NotCTL_c);
		 CtlspGlobalFormula= $$;
	       }
	     | TOK_GLOBALLY CTLsFormula
	       { $$ = Ctlsp_FormulaCreate(Ctlsp_G_c, $2, NIL(Ctlsp_Formula_t));
		 Ctlsp_FormulaSetClass($$, table2(Ctlsp_FormulaReadClass($2)) );
		 if (Ctlsp_FormulaReadClassOfCTL($2) ==  Ctlsp_CTL_c)
		   {
		     Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_PathCTL_c);
		   }
		 else
		     Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_NotCTL_c);
		 CtlspGlobalFormula= $$;
	       }
	     | CTLsFormula TOK_UNTIL CTLsFormula
	       { $$ = Ctlsp_FormulaCreate(Ctlsp_U_c, $1, $3);
		 Ctlsp_FormulaSetClass($$, table3(Ctlsp_FormulaReadClass($1),Ctlsp_FormulaReadClass($3)) );
		 if ((Ctlsp_FormulaReadClassOfCTL($1) ==  Ctlsp_CTL_c) && (Ctlsp_FormulaReadClassOfCTL($3) == Ctlsp_CTL_c))
		   {
		     Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_PathCTL_c);
		   }
		 else
		   {
		     Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_NotCTL_c);
		   }
		 CtlspGlobalFormula= $$;
	       }
	     | CTLsFormula TOK_RELEASE CTLsFormula
	       { $$ = Ctlsp_FormulaCreate(Ctlsp_R_c, $1, $3);
		 Ctlsp_FormulaSetClass($$, table3(Ctlsp_FormulaReadClass($1),Ctlsp_FormulaReadClass($3)) );
		 if ((Ctlsp_FormulaReadClassOfCTL($1) ==  Ctlsp_CTL_c) && (Ctlsp_FormulaReadClassOfCTL($3) == Ctlsp_CTL_c))
		   {
		     Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_PathCTL_c);
		   }
		 else
		   {
		     Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_NotCTL_c);
		   }
		 CtlspGlobalFormula= $$;
	       }
	     | CTLsFormula TOK_WEAK_UNTIL CTLsFormula
	       { $$ = Ctlsp_FormulaCreate(Ctlsp_W_c, $1, $3);
		 Ctlsp_FormulaSetClass($$, table3(Ctlsp_FormulaReadClass($1),Ctlsp_FormulaReadClass($3)) );
		 if ((Ctlsp_FormulaReadClassOfCTL($1) ==  Ctlsp_CTL_c) && (Ctlsp_FormulaReadClassOfCTL($3) == Ctlsp_CTL_c))
		   {
		     Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_PathCTL_c);
		   }
		 else
		   {
		     Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_NotCTL_c);
		   }
		 CtlspGlobalFormula= $$;
	       }
	     | TOK_EXISTS CTLsFormula
	       { $$ = Ctlsp_FormulaCreate(Ctlsp_E_c, $2, NIL(Ctlsp_Formula_t));
		 Ctlsp_FormulaSetClass($$, Ctlsp_stateformula_c);
		 if (Ctlsp_FormulaReadClassOfCTL($2) ==  Ctlsp_PathCTL_c)
		   {
		     Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_CTL_c);
		   }
		 else
		   {
		     Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_NotCTL_c);
		   }
		 CtlspGlobalFormula= $$;
	       }
	     |  TOK_EXISTS_NEXT CTLsFormula
	       { $$ = Ctlsp_FormulaCreate(Ctlsp_X_c, $2, NIL(Ctlsp_Formula_t));
		 Ctlsp_FormulaSetClass($$, table2(Ctlsp_FormulaReadClass($2)));
		 $$ = Ctlsp_FormulaCreate(Ctlsp_E_c, $$, NIL(Ctlsp_Formula_t));
		 Ctlsp_FormulaSetClass($$, Ctlsp_stateformula_c);
		 if (Ctlsp_FormulaReadClassOfCTL($2) ==  Ctlsp_CTL_c)
		 {
		   Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_CTL_c);
		 }
		 else
		 {
		     Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_NotCTL_c);
		 }
		 CtlspGlobalFormula= $$;
	       }
	      | ex_mult '(' CTLsFormula ')'
		 { $$ = Ctlsp_FormulaCreateEXMult($1, $3);
		   if ($$ == NIL(Ctlsp_Formula_t)){
		   CtlspYyerror("** ctl* error : MULTIPLE EX ERROR");
		   (void) fprintf(vis_stderr,"Error during parsing line %d.\n\n", CtlspYylineno);
		   Ctlsp_FormulaFree(CtlspGlobalFormula);
		   }
		   FREE($1);
		   CtlspGlobalFormula= $$;
	       }
	     | TOK_EXISTS_EVENTUALLY CTLsFormula
	       { $$ = Ctlsp_FormulaCreate(Ctlsp_F_c, $2, NIL(Ctlsp_Formula_t));
		 Ctlsp_FormulaSetClass($$, table2(Ctlsp_FormulaReadClass($2)));
		 $$ = Ctlsp_FormulaCreate(Ctlsp_E_c, $$, NIL(Ctlsp_Formula_t));
		 Ctlsp_FormulaSetClass($$, Ctlsp_stateformula_c);
		 if (Ctlsp_FormulaReadClassOfCTL($2) ==  Ctlsp_CTL_c)
		   {
		     Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_CTL_c);
		   }
		 else
		     Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_NotCTL_c);
		 CtlspGlobalFormula= $$;
	       }
	     | TOK_EXISTS_GLOBALLY CTLsFormula
	       { $$ = Ctlsp_FormulaCreate(Ctlsp_G_c, $2, NIL(Ctlsp_Formula_t));
		 Ctlsp_FormulaSetClass($$, table2(Ctlsp_FormulaReadClass($2)));
		 $$ = Ctlsp_FormulaCreate(Ctlsp_E_c, $$, NIL(Ctlsp_Formula_t));
		 Ctlsp_FormulaSetClass($$, Ctlsp_stateformula_c);
		 if (Ctlsp_FormulaReadClassOfCTL($2) ==  Ctlsp_CTL_c)
		   {
		     Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_CTL_c);
		   }
		 else
		     Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_NotCTL_c);
		 CtlspGlobalFormula= $$;
	       }
	     | TOK_FORALL CTLsFormula
	       { $$ = Ctlsp_FormulaCreate(Ctlsp_A_c, $2, NIL(Ctlsp_Formula_t));
		 Ctlsp_FormulaSetClass($$, Ctlsp_stateformula_c);
		 if (Ctlsp_FormulaReadClassOfCTL($2) ==  Ctlsp_PathCTL_c)
		   {
		     Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_CTL_c);
		   }
		 else
		     Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_NotCTL_c);
		 CtlspGlobalFormula= $$;
	       }
	     | TOK_FORALL_GLOBALLY CTLsFormula
	       { $$ = Ctlsp_FormulaCreate(Ctlsp_G_c, $2, NIL(Ctlsp_Formula_t));
		 Ctlsp_FormulaSetClass($$, table2(Ctlsp_FormulaReadClass($2)));
		 $$ = Ctlsp_FormulaCreate(Ctlsp_A_c, $$, NIL(Ctlsp_Formula_t));
		 Ctlsp_FormulaSetClass($$, Ctlsp_stateformula_c);
		 if (Ctlsp_FormulaReadClassOfCTL($2) ==  Ctlsp_CTL_c)
		   {
		     Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_CTL_c);
		   }
		 else
		     Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_NotCTL_c);
		 CtlspGlobalFormula= $$;
	       }
	     | TOK_FORALL_NEXT CTLsFormula
	       { $$ = Ctlsp_FormulaCreate(Ctlsp_X_c, $2, NIL(Ctlsp_Formula_t));
		 Ctlsp_FormulaSetClass($$, table2(Ctlsp_FormulaReadClass($2)));
		 $$ = Ctlsp_FormulaCreate(Ctlsp_A_c, $$, NIL(Ctlsp_Formula_t));
		 Ctlsp_FormulaSetClass($$, Ctlsp_stateformula_c);
		 if (Ctlsp_FormulaReadClassOfCTL($2) ==  Ctlsp_CTL_c)
		   {
		     Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_CTL_c);
		   }
		 else
		     Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_NotCTL_c);
		 CtlspGlobalFormula= $$;
	       }
	      | ax_mult '(' CTLsFormula ')'
		 { $$ = Ctlsp_FormulaCreateAXMult($1, $3);
		   if ($$ == NIL(Ctlsp_Formula_t)){
		   CtlspYyerror("** ctl* error : MULTIPLE AX ERROR");
		   (void) fprintf(vis_stderr,"Error during parsing line %d.\n\n", CtlspYylineno);
		   Ctlsp_FormulaFree(CtlspGlobalFormula);
		   }
		   FREE($1);
		   CtlspGlobalFormula= $$;
	       }
	     | TOK_FORALL_EVENTUALLY CTLsFormula
	       { $$ = Ctlsp_FormulaCreate(Ctlsp_F_c, $2, NIL(Ctlsp_Formula_t));
		 Ctlsp_FormulaSetClass($$, table2(Ctlsp_FormulaReadClass($2)));
		 $$ = Ctlsp_FormulaCreate(Ctlsp_A_c, $$, NIL(Ctlsp_Formula_t));
		 Ctlsp_FormulaSetClass($$, Ctlsp_stateformula_c);
		 if (Ctlsp_FormulaReadClassOfCTL($2) ==  Ctlsp_CTL_c)
		   {
		     Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_CTL_c);
		   }
		 else
		     Ctlsp_FormulaSetClassOfCTL($$, Ctlsp_NotCTL_c);
		 CtlspGlobalFormula= $$;
	       }
	      | x_mult '(' CTLsFormula ')'
		 { $$ = Ctlsp_FormulaCreateXMult($1, $3);
		   if ($$ == NIL(Ctlsp_Formula_t)){
		   CtlspYyerror("** ctl* error : MULTIPLE X ERROR");
		   (void) fprintf(vis_stderr,"Error during parsing line %d.\n\n", CtlspYylineno);
		   Ctlsp_FormulaFree(CtlspGlobalFormula);
		   }
		   FREE($1);
		   CtlspGlobalFormula= $$;
	       }
	 ;

propformula: '(' propformula ')'
	       { $$ = $2;
		 CtlspGlobalFormula= $$;
	       }
	     | name TOK_ASSIGN name
	     { $$ = Ctlsp_FormulaCreate(Ctlsp_ID_c, $1, $3);
	       CtlspGlobalFormula= $$;
	     }
	     | name TOK_ASSIGN name_union
	     { $$ = Ctlsp_FormulaCreateOr($1, $3);
	       FREE($1);
	       FREE($3);
	       CtlspGlobalFormula= $$;
	     }
	     | name_vector TOK_ASSIGN name
	       { $$ = Ctlsp_FormulaCreateVectorAnd($1, $3);
		 if ($$ == NIL(Ctlsp_Formula_t))
		 {
		  CtlspYyerror("** ctl error : Matching ERROR");
		  (void) fprintf(vis_stderr,"LHS token is not matched to RHS token, line %d.\n\n", CtlspYylineno);
		  Ctlsp_FormulaFree(CtlspGlobalFormula);
		 }
		 FREE($1);
		 FREE($3);
		 CtlspGlobalFormula= $$;
	       }
	     | name_vector TOK_ASSIGN name_union
	       { $$ = Ctlsp_FormulaCreateVectorOr($1, $3);
		if ($$ == NIL(Ctlsp_Formula_t)){
		   CtlspYyerror("** ctl error : Matching ERROR");
		   (void) fprintf(vis_stderr,"LHS token is not matched to RHS token, line %d\n\n", CtlspYylineno);
		   Ctlsp_FormulaFree(CtlspGlobalFormula);
		}
		FREE($1);
		FREE($3);
		CtlspGlobalFormula= $$;
	       }
	     | name TOK_EQIV name
	       { $$ = Ctlsp_FormulaCreateEquiv($1, $3);
		 if ($$ == NIL(Ctlsp_Formula_t)){
		   CtlspYyerror("** ctl error : Matching ERROR");
		   (void) fprintf(vis_stderr,"LHS token is not matched to RHS token, line %d.\n\n", CtlspYylineno);
		   Ctlsp_FormulaFree(CtlspGlobalFormula);
		 }
		 FREE($1);
		 FREE($3);
		 CtlspGlobalFormula= $$;
	       }
	     | name_vector TOK_EQIV name_vector
	       { $$ = Ctlsp_FormulaCreateVectorEquiv($1, $3);
		 FREE($1);
		 FREE($3);
		 CtlspGlobalFormula= $$;
	       }
	     | name TOK_ASSIGN TOK_FORALL
	       { $$ = Ctlsp_FormulaCreate(Ctlsp_ID_c, $1, util_strsav("A"));
		 CtlspGlobalFormula= $$;
	       }
	     | name TOK_ASSIGN TOK_EXISTS
	       { $$ = Ctlsp_FormulaCreate(Ctlsp_ID_c, $1, util_strsav("E"));
		 CtlspGlobalFormula= $$;
	       }
	     | name TOK_ASSIGN TOK_EVENTUALLY
	       { $$ = Ctlsp_FormulaCreate(Ctlsp_ID_c, $1, util_strsav("F"));
		 CtlspGlobalFormula= $$;
	       }
	     | name TOK_ASSIGN TOK_GLOBALLY
	       { $$ = Ctlsp_FormulaCreate(Ctlsp_ID_c, $1, util_strsav("G"));
		 CtlspGlobalFormula= $$;
	       }
	     | name TOK_ASSIGN TOK_NEXT
	       { $$ = Ctlsp_FormulaCreate(Ctlsp_ID_c, $1, util_strsav("X"));
		 CtlspGlobalFormula= $$;
	       }
	     | name TOK_ASSIGN TOK_UNTIL
	       { $$ = Ctlsp_FormulaCreate(Ctlsp_ID_c, $1, util_strsav("U"));
		 CtlspGlobalFormula= $$;
	       }
	     | name TOK_ASSIGN TOK_WEAK_UNTIL
	       { $$ = Ctlsp_FormulaCreate(Ctlsp_ID_c, $1, util_strsav("W"));
		 CtlspGlobalFormula= $$;
	       }
	     | name TOK_ASSIGN TOK_RELEASE
	       { $$ = Ctlsp_FormulaCreate(Ctlsp_ID_c, $1, util_strsav("R"));
		 CtlspGlobalFormula= $$;
	       }
	     | TOK_FORALL TOK_ASSIGN name
	       { $$ = Ctlsp_FormulaCreate(Ctlsp_ID_c, util_strsav("A"), $3);
		 CtlspGlobalFormula= $$;
	       }
	     | TOK_EXISTS TOK_ASSIGN name
	       { $$ = Ctlsp_FormulaCreate(Ctlsp_ID_c, util_strsav("E"), $3);
		 CtlspGlobalFormula= $$;
	       }
	     | TOK_EVENTUALLY TOK_ASSIGN name
	       { $$ = Ctlsp_FormulaCreate(Ctlsp_ID_c, util_strsav("F"), $3);
		 CtlspGlobalFormula= $$;
	       }
	     | TOK_GLOBALLY TOK_ASSIGN name
	       { $$ = Ctlsp_FormulaCreate(Ctlsp_ID_c, util_strsav("G"), $3);
		 CtlspGlobalFormula= $$;
	       }
	     | TOK_NEXT TOK_ASSIGN name
	       { $$ = Ctlsp_FormulaCreate(Ctlsp_ID_c, util_strsav("X"), $3);
		 CtlspGlobalFormula= $$;
	       }
	     | TOK_UNTIL TOK_ASSIGN name
	       { $$ = Ctlsp_FormulaCreate(Ctlsp_ID_c, util_strsav("U"), $3);
		 CtlspGlobalFormula= $$;
	       }
	     | TOK_WEAK_UNTIL TOK_ASSIGN name
	       { $$ = Ctlsp_FormulaCreate(Ctlsp_ID_c, util_strsav("W"), $3);
		 CtlspGlobalFormula= $$;
	       }
	     | TOK_RELEASE TOK_ASSIGN name
	       { $$ = Ctlsp_FormulaCreate(Ctlsp_ID_c, util_strsav("R"), $3);
		 CtlspGlobalFormula= $$;
	       }
	     | TOK_TRUE
	       { $$ = Ctlsp_FormulaCreate(Ctlsp_TRUE_c, NIL(Ctlsp_Formula_t), NIL(Ctlsp_Formula_t));
		 CtlspGlobalFormula= $$;
	       }
	     | TOK_FALSE
	       { $$ = Ctlsp_FormulaCreate(Ctlsp_FALSE_c, NIL(Ctlsp_Formula_t), NIL(Ctlsp_Formula_t));
		 CtlspGlobalFormula= $$;
	       }
	     | macro
	       { $$ = CtlspFormulaFindInTable($1, CtlspMacroTable);
		 if ($$ == NIL(Ctlsp_Formula_t)){
		    CtlspYyerror("** ctl* error : Macro Error");
		    (void) fprintf(vis_stderr,"Macro \"%s\" is not defined.\n\n",$1);
		    FREE($1);
		    CtlspGlobalFormula= $$;
		    YYERROR;
		 }
		 FREE($1);
		 CtlspGlobalFormula= $$;

	       };

name:  TOK_ID
       { $$ = util_strsav(CtlspYytext); }
     | TOK_ID2
       { (void) CtlspChangeBracket(CtlspYytext);
	 $$ = util_strsav(CtlspYytext); };
name_vector: TOK_ID_VECTOR
       { $$ = util_strsav(CtlspYytext); };

name_union: '{' name_or '}'
       { $$ = $2; };
name_or: name
       { $$ = $1; }
      |  name_or TOK_COMMA name
       { $$ = util_strcat3($1,",",$3);
	 FREE($1);
	 FREE($3);
       }
      ;

macro: TOK_MACRO name
       { $$ = $2; } ;

x_mult: TOK_NEXT_MULT
       { $$ = util_strsav(CtlspYytext); } ;

ax_mult: TOK_FORALL_NEXT_MULT
       { $$ = util_strsav(CtlspYytext); } ;

ex_mult: TOK_EXISTS_NEXT_MULT
       { $$ = util_strsav(CtlspYytext); } ;
%%