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

  FileName    [ctlsp.l]

  PackageName [ctlsp]

  Synopsis    [Lexical analyzer for CTL* formula parser.]

  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.]

  Revision    [$Id: ctlsp.l,v 1.4 2010/04/09 23:31:37 fabio Exp $]

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

#include "ctlspRead.h"

/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/

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


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

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


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


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

/**Function********************************************************************

  Synopsis    [Initializes global variables for parsing file.]

  SideEffects []

******************************************************************************/
void
CtlspFileSetup(
  FILE * fp)
{
  CtlspYyin             = fp;
  CtlspYylineno         = 1;
}

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

/**Function********************************************************************

  Synopsis    [Prints error message and sets global error flag.]

  SideEffects []

******************************************************************************/
static void
CtlspYyerror(
  char * errmsg)
{
  (void) fprintf(vis_stderr, "%s in line %d with token \"%s\"\n", errmsg, CtlspYylineno, yytext); 
  CtlspGlobalError = 1;
}

%}

/*---------------------------------------------------------------------------*/
/*      Lexical analyzer rules                                               */
/*---------------------------------------------------------------------------*/

%option noyywrap
%option yylineno

/* substitution strings */
/* alnum is the same set in alnumsymbol in io.l except [ and ] being removed here for the until and release operators */
/* - , =, and ; are intentionally removed because: 
   - is used for -> and <->
   = is used for foo = bar 
   ; is used for delimitters */
/* ( and ) are intentionally removed since they are used as parentheses */
/* +, *, and ^ have to be used surrounded by spaces since they are symbols. 
   ! can be attached immediately w/o spaces since it is not a symbol */

alnum	[A-Za-z0-9\^\?\|\/\+\*\$\<\>~@\_#\$%\:\"\'\.]

%%

[ \t\n\r]	;

"#".*   ;   

A	{ return(TOK_FORALL); }
E	{ return(TOK_EXISTS); }

AX	{ return(TOK_FORALL_NEXT); }
EX	{ return(TOK_EXISTS_NEXT); }
AF	{ return(TOK_FORALL_EVENTUALLY); }
EF	{ return(TOK_EXISTS_EVENTUALLY); }
AG	{ return(TOK_FORALL_GLOBALLY); }
EG	{ return(TOK_EXISTS_GLOBALLY); }


X	{ return(TOK_NEXT); }
F	{ return(TOK_EVENTUALLY); }
G	{ return(TOK_GLOBALLY); }

X:[0-9]+  { return(TOK_NEXT_MULT); }

AX:[0-9]+  { return(TOK_FORALL_NEXT_MULT); }
EX:[0-9]+  { return(TOK_EXISTS_NEXT_MULT); }

U	{ return(TOK_UNTIL); }
R	{ return(TOK_RELEASE); }
W	{ return(TOK_WEAK_UNTIL); }


TRUE    { return(TOK_TRUE); }

FALSE   { return(TOK_FALSE); }

\\DEFINE |
\\Define |
\\define  { return(TOK_DEFINE); }

\+	{ return(TOK_OR); }
\|\|	{ return(TOK_OR); }
\*	{ return(TOK_AND); }
\&\&	{ return(TOK_AND); }
!	{ return(TOK_NOT); }
"^"	{ return(TOK_XOR); }
"->"	{ return(TOK_THEN); }
"<->"	{ return(TOK_EQ); }
=       { return(TOK_ASSIGN); }
==      { return(TOK_EQIV); }
\,      { return(TOK_COMMA); }
\\      { return(TOK_MACRO); }

{alnum}+                                   { return(TOK_ID); }
{alnum}+\[[ ]*[0-9]+[ ]*\]                 { return(TOK_ID2); }
{alnum}+\[[ ]*[0-9]+[ ]*\:[ ]*[0-9]+[ ]*\] { return(TOK_ID_VECTOR); }

.       { return CtlspYytext[0]; }
%%