Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
model-checker : lex and yacc parsing moved in src/xbt/automaton/
authorMarion Guthmuller <marion.guthmuller@loria.fr>
Thu, 14 Jun 2012 21:22:07 +0000 (23:22 +0200)
committerMarion Guthmuller <marion.guthmuller@loria.fr>
Thu, 14 Jun 2012 21:22:07 +0000 (23:22 +0200)
15 files changed:
buildtools/Cmake/DefinePackages.cmake
examples/msg/mc/automaton_parse.yy.c [new file with mode: 0644]
include/simgrid/modelchecker.h
include/xbt/automaton.h
include/xbt/automatonparse_promela.h
src/mc/mc_global.c
src/xbt/automaton/automaton.c [new file with mode: 0644]
src/xbt/automaton/automaton_create.c [new file with mode: 0644]
src/xbt/automaton/automaton_create.h [new file with mode: 0644]
src/xbt/automaton/automaton_parse.yy.c [new file with mode: 0644]
src/xbt/automaton/automatonparse_promela.c [new file with mode: 0644]
src/xbt/automaton/parserPromela.lex [new file with mode: 0644]
src/xbt/automaton/parserPromela.yacc [new file with mode: 0644]
src/xbt/automaton/y.tab.c [new file with mode: 0644]
src/xbt/automaton/y.tab.h [new file with mode: 0644]

index 5765fe7..95a15b7 100644 (file)
@@ -16,7 +16,6 @@ set(EXTRA_DIST
        src/xbt/backtrace_windows.c
        src/xbt/backtrace_dummy.c
        src/xbt/setset_private.h
-       src/xbt/automatonparse_promela.c
        src/xbt/mmalloc/mfree.c
        src/xbt/mmalloc/mmalloc.c
        src/xbt/mmalloc/mmalloc.info
@@ -89,12 +88,8 @@ set(EXTRA_DIST
        examples/gras/console/ping.h
        examples/gras/mmrpc/mmrpc.h
        
-    examples/msg/mc/parserPromela.yacc
-    examples/msg/mc/parserPromela.lex
-    examples/msg/mc/automaton.h
     examples/msg/mc/bugged1_liveness.h
     examples/msg/mc/centralized_liveness.h
-    examples/msg/mc/automatonparse_promela.h
     examples/msg/mc/bugged2_liveness.h
     examples/msg/mc/y.tab.h
 
@@ -184,7 +179,11 @@ set(XBT_SRC
        src/xbt/parmap.c
        src/xbt/xbt_replay.c
        src/xbt/lib.c
-       src/xbt/automaton.c
+       src/xbt/automaton/automaton.c
+       src/xbt/automaton/automatonparse_promela.c
+       src/xbt/automaton/automaton.c
+       src/xbt/automaton/automatonparse_promela.c
+       src/xbt/automaton/automaton_create.c
        src/xbt/datadesc/ddt_create.c
        src/xbt/datadesc/ddt_convert.c
        src/xbt/datadesc/ddt_exchange.c
@@ -401,6 +400,8 @@ set(headers_to_install
        include/xbt/hash.h
        include/xbt/function_types.h
        include/xbt/asserts.h 
+       include/xbt/automaton.h
+       include/xbt/automatonparse_promela.h
        include/xbt/ex.h
        include/xbt/log.h
        include/xbt/module.h
@@ -427,8 +428,6 @@ set(headers_to_install
        include/xbt/mmalloc.h
        include/xbt/replay.h
        include/xbt/parmap.h
-       include/xbt/automaton.h
-       include/xbt/automatonparse_promela.h
        include/xbt/datadesc.h
        include/xbt/socket.h
        include/xbt/file_stat.h
diff --git a/examples/msg/mc/automaton_parse.yy.c b/examples/msg/mc/automaton_parse.yy.c
new file mode 100644 (file)
index 0000000..a7395b1
--- /dev/null
@@ -0,0 +1,1947 @@
+#line 2 "automaton_parse.yy.c"
+
+#line 4 "automaton_parse.yy.c"
+
+#define  YY_INT_ALIGNED short int
+
+/* A lexical scanner generated by flex */
+
+#define yy_create_buffer xbt_automaton_parse__create_buffer
+#define yy_delete_buffer xbt_automaton_parse__delete_buffer
+#define yy_flex_debug xbt_automaton_parse__flex_debug
+#define yy_init_buffer xbt_automaton_parse__init_buffer
+#define yy_flush_buffer xbt_automaton_parse__flush_buffer
+#define yy_load_buffer_state xbt_automaton_parse__load_buffer_state
+#define yy_switch_to_buffer xbt_automaton_parse__switch_to_buffer
+#define yyin xbt_automaton_parse_in
+#define yyleng xbt_automaton_parse_leng
+#define yylex xbt_automaton_parse_lex
+#define yylineno xbt_automaton_parse_lineno
+#define yyout xbt_automaton_parse_out
+#define yyrestart xbt_automaton_parse_restart
+#define yytext xbt_automaton_parse_text
+#define yywrap xbt_automaton_parse_wrap
+#define yyalloc xbt_automaton_parse_alloc
+#define yyrealloc xbt_automaton_parse_realloc
+#define yyfree xbt_automaton_parse_free
+
+#define FLEX_SCANNER
+#define YY_FLEX_MAJOR_VERSION 2
+#define YY_FLEX_MINOR_VERSION 5
+#define YY_FLEX_SUBMINOR_VERSION 35
+#if YY_FLEX_SUBMINOR_VERSION > 0
+#define FLEX_BETA
+#endif
+
+/* First, we deal with  platform-specific or compiler-specific issues. */
+
+/* begin standard C headers. */
+#include <stdio.h>
+#include <string.h>
+#include <errno.h>
+#include <stdlib.h>
+
+/* end standard C headers. */
+
+/* flex integer type definitions */
+
+#ifndef FLEXINT_H
+#define FLEXINT_H
+
+/* C99 systems have <inttypes.h>. Non-C99 systems may or may not. */
+
+#if defined (__STDC_VERSION__) && __STDC_VERSION__ >= 199901L
+
+/* C99 says to define __STDC_LIMIT_MACROS before including stdint.h,
+ * if you want the limit (max/min) macros for int types. 
+ */
+#ifndef __STDC_LIMIT_MACROS
+#define __STDC_LIMIT_MACROS 1
+#endif
+
+#include <inttypes.h>
+typedef int8_t flex_int8_t;
+typedef uint8_t flex_uint8_t;
+typedef int16_t flex_int16_t;
+typedef uint16_t flex_uint16_t;
+typedef int32_t flex_int32_t;
+typedef uint32_t flex_uint32_t;
+#else
+typedef signed char flex_int8_t;
+typedef short int flex_int16_t;
+typedef int flex_int32_t;
+typedef unsigned char flex_uint8_t; 
+typedef unsigned short int flex_uint16_t;
+typedef unsigned int flex_uint32_t;
+
+/* Limits of integral types. */
+#ifndef INT8_MIN
+#define INT8_MIN               (-128)
+#endif
+#ifndef INT16_MIN
+#define INT16_MIN              (-32767-1)
+#endif
+#ifndef INT32_MIN
+#define INT32_MIN              (-2147483647-1)
+#endif
+#ifndef INT8_MAX
+#define INT8_MAX               (127)
+#endif
+#ifndef INT16_MAX
+#define INT16_MAX              (32767)
+#endif
+#ifndef INT32_MAX
+#define INT32_MAX              (2147483647)
+#endif
+#ifndef UINT8_MAX
+#define UINT8_MAX              (255U)
+#endif
+#ifndef UINT16_MAX
+#define UINT16_MAX             (65535U)
+#endif
+#ifndef UINT32_MAX
+#define UINT32_MAX             (4294967295U)
+#endif
+
+#endif /* ! C99 */
+
+#endif /* ! FLEXINT_H */
+
+#ifdef __cplusplus
+
+/* The "const" storage-class-modifier is valid. */
+#define YY_USE_CONST
+
+#else  /* ! __cplusplus */
+
+/* C99 requires __STDC__ to be defined as 1. */
+#if defined (__STDC__)
+
+#define YY_USE_CONST
+
+#endif /* defined (__STDC__) */
+#endif /* ! __cplusplus */
+
+#ifdef YY_USE_CONST
+#define yyconst const
+#else
+#define yyconst
+#endif
+
+/* Returned upon end-of-file. */
+#define YY_NULL 0
+
+/* Promotes a possibly negative, possibly signed char to an unsigned
+ * integer for use as an array index.  If the signed char is negative,
+ * we want to instead treat it as an 8-bit unsigned char, hence the
+ * double cast.
+ */
+#define YY_SC_TO_UI(c) ((unsigned int) (unsigned char) c)
+
+/* Enter a start condition.  This macro really ought to take a parameter,
+ * but we do it the disgusting crufty way forced on us by the ()-less
+ * definition of BEGIN.
+ */
+#define BEGIN (yy_start) = 1 + 2 *
+
+/* Translate the current start state into a value that can be later handed
+ * to BEGIN to return to the state.  The YYSTATE alias is for lex
+ * compatibility.
+ */
+#define YY_START (((yy_start) - 1) / 2)
+#define YYSTATE YY_START
+
+/* Action number for EOF rule of a given start state. */
+#define YY_STATE_EOF(state) (YY_END_OF_BUFFER + state + 1)
+
+/* Special action meaning "start processing a new file". */
+#define YY_NEW_FILE xbt_automaton_parse_restart(xbt_automaton_parse_in  )
+
+#define YY_END_OF_BUFFER_CHAR 0
+
+/* Size of default input buffer. */
+#ifndef YY_BUF_SIZE
+#ifdef __ia64__
+/* On IA-64, the buffer size is 16k, not 8k.
+ * Moreover, YY_BUF_SIZE is 2*YY_READ_BUF_SIZE in the general case.
+ * Ditto for the __ia64__ case accordingly.
+ */
+#define YY_BUF_SIZE 32768
+#else
+#define YY_BUF_SIZE 16384
+#endif /* __ia64__ */
+#endif
+
+/* The state buf must be large enough to hold one state per character in the main buffer.
+ */
+#define YY_STATE_BUF_SIZE   ((YY_BUF_SIZE + 2) * sizeof(yy_state_type))
+
+#ifndef YY_TYPEDEF_YY_BUFFER_STATE
+#define YY_TYPEDEF_YY_BUFFER_STATE
+typedef struct yy_buffer_state *YY_BUFFER_STATE;
+#endif
+
+extern int xbt_automaton_parse_leng;
+
+extern FILE *xbt_automaton_parse_in, *xbt_automaton_parse_out;
+
+#define EOB_ACT_CONTINUE_SCAN 0
+#define EOB_ACT_END_OF_FILE 1
+#define EOB_ACT_LAST_MATCH 2
+
+    #define YY_LESS_LINENO(n)
+    
+/* Return all but the first "n" matched characters back to the input stream. */
+#define yyless(n) \
+       do \
+               { \
+               /* Undo effects of setting up xbt_automaton_parse_text. */ \
+        int yyless_macro_arg = (n); \
+        YY_LESS_LINENO(yyless_macro_arg);\
+               *yy_cp = (yy_hold_char); \
+               YY_RESTORE_YY_MORE_OFFSET \
+               (yy_c_buf_p) = yy_cp = yy_bp + yyless_macro_arg - YY_MORE_ADJ; \
+               YY_DO_BEFORE_ACTION; /* set up xbt_automaton_parse_text again */ \
+               } \
+       while ( 0 )
+
+#define unput(c) yyunput( c, (yytext_ptr)  )
+
+#ifndef YY_TYPEDEF_YY_SIZE_T
+#define YY_TYPEDEF_YY_SIZE_T
+typedef size_t yy_size_t;
+#endif
+
+#ifndef YY_STRUCT_YY_BUFFER_STATE
+#define YY_STRUCT_YY_BUFFER_STATE
+struct yy_buffer_state
+       {
+       FILE *yy_input_file;
+
+       char *yy_ch_buf;                /* input buffer */
+       char *yy_buf_pos;               /* current position in input buffer */
+
+       /* Size of input buffer in bytes, not including room for EOB
+        * characters.
+        */
+       yy_size_t yy_buf_size;
+
+       /* Number of characters read into yy_ch_buf, not including EOB
+        * characters.
+        */
+       int yy_n_chars;
+
+       /* Whether we "own" the buffer - i.e., we know we created it,
+        * and can realloc() it to grow it, and should free() it to
+        * delete it.
+        */
+       int yy_is_our_buffer;
+
+       /* Whether this is an "interactive" input source; if so, and
+        * if we're using stdio for input, then we want to use getc()
+        * instead of fread(), to make sure we stop fetching input after
+        * each newline.
+        */
+       int yy_is_interactive;
+
+       /* Whether we're considered to be at the beginning of a line.
+        * If so, '^' rules will be active on the next match, otherwise
+        * not.
+        */
+       int yy_at_bol;
+
+    int yy_bs_lineno; /**< The line count. */
+    int yy_bs_column; /**< The column count. */
+    
+       /* Whether to try to fill the input buffer when we reach the
+        * end of it.
+        */
+       int yy_fill_buffer;
+
+       int yy_buffer_status;
+
+#define YY_BUFFER_NEW 0
+#define YY_BUFFER_NORMAL 1
+       /* When an EOF's been seen but there's still some text to process
+        * then we mark the buffer as YY_EOF_PENDING, to indicate that we
+        * shouldn't try reading from the input source any more.  We might
+        * still have a bunch of tokens to match, though, because of
+        * possible backing-up.
+        *
+        * When we actually see the EOF, we change the status to "new"
+        * (via xbt_automaton_parse_restart()), so that the user can continue scanning by
+        * just pointing xbt_automaton_parse_in at a new input file.
+        */
+#define YY_BUFFER_EOF_PENDING 2
+
+       };
+#endif /* !YY_STRUCT_YY_BUFFER_STATE */
+
+/* Stack of input buffers. */
+static size_t yy_buffer_stack_top = 0; /**< index of top of stack. */
+static size_t yy_buffer_stack_max = 0; /**< capacity of stack. */
+static YY_BUFFER_STATE * yy_buffer_stack = 0; /**< Stack as an array. */
+
+/* We provide macros for accessing buffer states in case in the
+ * future we want to put the buffer states in a more general
+ * "scanner state".
+ *
+ * Returns the top of the stack, or NULL.
+ */
+#define YY_CURRENT_BUFFER ( (yy_buffer_stack) \
+                          ? (yy_buffer_stack)[(yy_buffer_stack_top)] \
+                          : NULL)
+
+/* Same as previous macro, but useful when we know that the buffer stack is not
+ * NULL or when we need an lvalue. For internal use only.
+ */
+#define YY_CURRENT_BUFFER_LVALUE (yy_buffer_stack)[(yy_buffer_stack_top)]
+
+/* yy_hold_char holds the character lost when xbt_automaton_parse_text is formed. */
+static char yy_hold_char;
+static int yy_n_chars;         /* number of characters read into yy_ch_buf */
+int xbt_automaton_parse_leng;
+
+/* Points to current character in buffer. */
+static char *yy_c_buf_p = (char *) 0;
+static int yy_init = 0;                /* whether we need to initialize */
+static int yy_start = 0;       /* start state number */
+
+/* Flag which is used to allow xbt_automaton_parse_wrap()'s to do buffer switches
+ * instead of setting up a fresh xbt_automaton_parse_in.  A bit of a hack ...
+ */
+static int yy_did_buffer_switch_on_eof;
+
+void xbt_automaton_parse_restart (FILE *input_file  );
+void xbt_automaton_parse__switch_to_buffer (YY_BUFFER_STATE new_buffer  );
+YY_BUFFER_STATE xbt_automaton_parse__create_buffer (FILE *file,int size  );
+void xbt_automaton_parse__delete_buffer (YY_BUFFER_STATE b  );
+void xbt_automaton_parse__flush_buffer (YY_BUFFER_STATE b  );
+void xbt_automaton_parse_push_buffer_state (YY_BUFFER_STATE new_buffer  );
+void xbt_automaton_parse_pop_buffer_state (void );
+
+static void xbt_automaton_parse_ensure_buffer_stack (void );
+static void xbt_automaton_parse__load_buffer_state (void );
+static void xbt_automaton_parse__init_buffer (YY_BUFFER_STATE b,FILE *file  );
+
+#define YY_FLUSH_BUFFER xbt_automaton_parse__flush_buffer(YY_CURRENT_BUFFER )
+
+YY_BUFFER_STATE xbt_automaton_parse__scan_buffer (char *base,yy_size_t size  );
+YY_BUFFER_STATE xbt_automaton_parse__scan_string (yyconst char *yy_str  );
+YY_BUFFER_STATE xbt_automaton_parse__scan_bytes (yyconst char *bytes,int len  );
+
+void *xbt_automaton_parse_alloc (yy_size_t  );
+void *xbt_automaton_parse_realloc (void *,yy_size_t  );
+void xbt_automaton_parse_free (void *  );
+
+#define yy_new_buffer xbt_automaton_parse__create_buffer
+
+#define yy_set_interactive(is_interactive) \
+       { \
+       if ( ! YY_CURRENT_BUFFER ){ \
+        xbt_automaton_parse_ensure_buffer_stack (); \
+               YY_CURRENT_BUFFER_LVALUE =    \
+            xbt_automaton_parse__create_buffer(xbt_automaton_parse_in,YY_BUF_SIZE ); \
+       } \
+       YY_CURRENT_BUFFER_LVALUE->yy_is_interactive = is_interactive; \
+       }
+
+#define yy_set_bol(at_bol) \
+       { \
+       if ( ! YY_CURRENT_BUFFER ){\
+        xbt_automaton_parse_ensure_buffer_stack (); \
+               YY_CURRENT_BUFFER_LVALUE =    \
+            xbt_automaton_parse__create_buffer(xbt_automaton_parse_in,YY_BUF_SIZE ); \
+       } \
+       YY_CURRENT_BUFFER_LVALUE->yy_at_bol = at_bol; \
+       }
+
+#define YY_AT_BOL() (YY_CURRENT_BUFFER_LVALUE->yy_at_bol)
+
+/* Begin user sect3 */
+
+#define xbt_automaton_parse_wrap(n) 1
+#define YY_SKIP_YYWRAP
+
+typedef unsigned char YY_CHAR;
+
+FILE *xbt_automaton_parse_in = (FILE *) 0, *xbt_automaton_parse_out = (FILE *) 0;
+
+typedef int yy_state_type;
+
+extern int xbt_automaton_parse_lineno;
+
+int xbt_automaton_parse_lineno = 1;
+
+extern char *xbt_automaton_parse_text;
+#define yytext_ptr xbt_automaton_parse_text
+
+static yy_state_type yy_get_previous_state (void );
+static yy_state_type yy_try_NUL_trans (yy_state_type current_state  );
+static int yy_get_next_buffer (void );
+static void yy_fatal_error (yyconst char msg[]  );
+
+/* Done after the current pattern has been matched and before the
+ * corresponding action - sets up xbt_automaton_parse_text.
+ */
+#define YY_DO_BEFORE_ACTION \
+       (yytext_ptr) = yy_bp; \
+       xbt_automaton_parse_leng = (size_t) (yy_cp - yy_bp); \
+       (yy_hold_char) = *yy_cp; \
+       *yy_cp = '\0'; \
+       (yy_c_buf_p) = yy_cp;
+
+#define YY_NUM_RULES 25
+#define YY_END_OF_BUFFER 26
+/* This struct is not used in this scanner,
+   but its presence is necessary. */
+struct yy_trans_info
+       {
+       flex_int32_t yy_verify;
+       flex_int32_t yy_nxt;
+       };
+static yyconst flex_int16_t yy_accept[54] =
+    {   0,
+        0,    0,   26,   24,   18,   23,    8,   24,   24,    9,
+       10,   24,   24,   20,   14,   12,   13,   22,   22,   22,
+       22,   22,   15,   24,   16,   18,    0,    0,   21,    0,
+        6,    4,    0,    0,   20,   11,   22,    3,   22,    2,
+       22,    7,    0,    0,    0,   19,   22,   22,   17,    5,
+       22,    1,    0
+    } ;
+
+static yyconst flex_int32_t yy_ec[256] =
+    {   0,
+        1,    1,    1,    1,    1,    1,    1,    1,    2,    3,
+        1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
+        1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
+        1,    4,    5,    6,    1,    1,    1,    7,    1,    8,
+        9,   10,    1,    1,   11,   12,   13,   14,   15,   14,
+       14,   14,   14,   14,   14,   14,   14,   16,   17,    1,
+        1,   18,    1,    1,   19,   19,   19,   19,   19,   19,
+       19,   19,   19,   19,   19,   19,   19,   19,   19,   19,
+       19,   19,   19,   19,   19,   19,   19,   19,   19,   19,
+        1,   20,    1,    1,   21,    1,   19,   19,   19,   19,
+
+       22,   23,   24,   19,   25,   19,   19,   19,   19,   26,
+       27,   19,   19,   28,   19,   29,   19,   30,   19,   19,
+       19,   19,   31,   32,   33,    1,    1,    1,    1,    1,
+        1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
+        1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
+        1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
+        1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
+        1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
+        1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
+        1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
+
+        1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
+        1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
+        1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
+        1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
+        1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
+        1,    1,    1,    1,    1
+    } ;
+
+static yyconst flex_int32_t yy_meta[34] =
+    {   0,
+        1,    1,    2,    2,    1,    2,    1,    1,    1,    1,
+        1,    1,    3,    4,    4,    1,    1,    1,    4,    2,
+        4,    4,    4,    4,    4,    4,    4,    4,    4,    4,
+        1,    1,    1
+    } ;
+
+static yyconst flex_int16_t yy_base[57] =
+    {   0,
+        0,    0,   89,   90,   32,   90,   90,   34,   81,   90,
+       90,   69,   76,   27,   31,   69,   90,    0,   59,   56,
+       58,   55,   90,   42,   90,   45,   47,    0,    0,    0,
+       90,   90,   52,   43,   49,   90,    0,    0,   44,    0,
+       42,   90,   56,   65,   52,   56,   25,   26,   90,    0,
+       16,    0,   90,   74,   31,   78
+    } ;
+
+static yyconst flex_int16_t yy_def[57] =
+    {   0,
+       53,    1,   53,   53,   53,   53,   53,   54,   53,   53,
+       53,   53,   53,   53,   53,   53,   53,   55,   55,   55,
+       55,   55,   53,   53,   53,   53,   54,   27,   27,   27,
+       53,   53,   56,   53,   53,   53,   55,   55,   55,   55,
+       55,   53,   56,   56,   53,   53,   55,   55,   53,   55,
+       55,   55,    0,   53,   53,   53
+    } ;
+
+static yyconst flex_int16_t yy_nxt[124] =
+    {   0,
+        4,    5,    6,    5,    7,    8,    9,   10,   11,    4,
+       12,    4,   13,   14,   15,   16,   17,    4,   18,    4,
+        4,   18,   19,   20,   21,   22,   18,   18,   18,   18,
+       23,   24,   25,   26,   37,   26,   27,   28,   34,   29,
+       35,   35,   34,   52,   35,   35,   26,   51,   26,   27,
+       28,   50,   29,   27,   44,   44,   46,   46,   44,   44,
+       34,   45,   35,   35,   49,   45,   27,   44,   44,   46,
+       46,   48,   47,   42,   45,   30,   41,   30,   43,   43,
+       40,   43,   39,   38,   36,   33,   32,   31,   53,    3,
+       53,   53,   53,   53,   53,   53,   53,   53,   53,   53,
+
+       53,   53,   53,   53,   53,   53,   53,   53,   53,   53,
+       53,   53,   53,   53,   53,   53,   53,   53,   53,   53,
+       53,   53,   53
+    } ;
+
+static yyconst flex_int16_t yy_chk[124] =
+    {   0,
+        1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
+        1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
+        1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
+        1,    1,    1,    5,   55,    5,    8,    8,   14,    8,
+       14,   14,   15,   51,   15,   15,   26,   48,   26,   27,
+       27,   47,   27,    8,   33,   33,   34,   34,   43,   43,
+       35,   33,   35,   35,   45,   43,   27,   44,   44,   46,
+       46,   41,   39,   24,   44,   54,   22,   54,   56,   56,
+       21,   56,   20,   19,   16,   13,   12,    9,    3,   53,
+       53,   53,   53,   53,   53,   53,   53,   53,   53,   53,
+
+       53,   53,   53,   53,   53,   53,   53,   53,   53,   53,
+       53,   53,   53,   53,   53,   53,   53,   53,   53,   53,
+       53,   53,   53
+    } ;
+
+static yy_state_type yy_last_accepting_state;
+static char *yy_last_accepting_cpos;
+
+extern int xbt_automaton_parse__flex_debug;
+int xbt_automaton_parse__flex_debug = 0;
+
+/* The intent behind this definition is that it'll catch
+ * any uses of REJECT which flex missed.
+ */
+#define REJECT reject_used_but_not_detected
+#define yymore() yymore_used_but_not_detected
+#define YY_MORE_ADJ 0
+#define YY_RESTORE_YY_MORE_OFFSET
+char *xbt_automaton_parse_text;
+#line 1 "parserPromela.lex"
+#line 4 "parserPromela.lex"
+
+
+#include <stdio.h>
+#include "y.tab.h"
+  
+  extern YYSTYPE yylval;
+#line 533 "automaton_parse.yy.c"
+
+#define INITIAL 0
+
+#ifndef YY_NO_UNISTD_H
+/* Special case for "unistd.h", since it is non-ANSI. We include it way
+ * down here because we want the user's section 1 to have been scanned first.
+ * The user has a chance to override it with an option.
+ */
+#include <unistd.h>
+#endif
+
+#ifndef YY_EXTRA_TYPE
+#define YY_EXTRA_TYPE void *
+#endif
+
+static int yy_init_globals (void );
+
+/* Accessor methods to globals.
+   These are made visible to non-reentrant scanners for convenience. */
+
+int xbt_automaton_parse_lex_destroy (void );
+
+int xbt_automaton_parse_get_debug (void );
+
+void xbt_automaton_parse_set_debug (int debug_flag  );
+
+YY_EXTRA_TYPE xbt_automaton_parse_get_extra (void );
+
+void xbt_automaton_parse_set_extra (YY_EXTRA_TYPE user_defined  );
+
+FILE *xbt_automaton_parse_get_in (void );
+
+void xbt_automaton_parse_set_in  (FILE * in_str  );
+
+FILE *xbt_automaton_parse_get_out (void );
+
+void xbt_automaton_parse_set_out  (FILE * out_str  );
+
+int xbt_automaton_parse_get_leng (void );
+
+char *xbt_automaton_parse_get_text (void );
+
+int xbt_automaton_parse_get_lineno (void );
+
+void xbt_automaton_parse_set_lineno (int line_number  );
+
+/* Macros after this point can all be overridden by user definitions in
+ * section 1.
+ */
+
+#ifndef YY_SKIP_YYWRAP
+#ifdef __cplusplus
+extern "C" int xbt_automaton_parse_wrap (void );
+#else
+extern int xbt_automaton_parse_wrap (void );
+#endif
+#endif
+
+    static void yyunput (int c,char *buf_ptr  );
+    
+#ifndef yytext_ptr
+static void yy_flex_strncpy (char *,yyconst char *,int );
+#endif
+
+#ifdef YY_NEED_STRLEN
+static int yy_flex_strlen (yyconst char * );
+#endif
+
+#ifndef YY_NO_INPUT
+
+#ifdef __cplusplus
+static int yyinput (void );
+#else
+static int input (void );
+#endif
+
+#endif
+
+/* Amount of stuff to slurp up with each read. */
+#ifndef YY_READ_BUF_SIZE
+#ifdef __ia64__
+/* On IA-64, the buffer size is 16k, not 8k */
+#define YY_READ_BUF_SIZE 16384
+#else
+#define YY_READ_BUF_SIZE 8192
+#endif /* __ia64__ */
+#endif
+
+/* Copy whatever the last rule matched to the standard output. */
+#ifndef ECHO
+/* This used to be an fputs(), but since the string might contain NUL's,
+ * we now use fwrite().
+ */
+#define ECHO do { if (fwrite( xbt_automaton_parse_text, xbt_automaton_parse_leng, 1, xbt_automaton_parse_out )) {} } while (0)
+#endif
+
+/* Gets input and stuffs it into "buf".  number of characters read, or YY_NULL,
+ * is returned in "result".
+ */
+#ifndef YY_INPUT
+#define YY_INPUT(buf,result,max_size) \
+       if ( YY_CURRENT_BUFFER_LVALUE->yy_is_interactive ) \
+               { \
+               int c = '*'; \
+               size_t n; \
+               for ( n = 0; n < max_size && \
+                            (c = getc( xbt_automaton_parse_in )) != EOF && c != '\n'; ++n ) \
+                       buf[n] = (char) c; \
+               if ( c == '\n' ) \
+                       buf[n++] = (char) c; \
+               if ( c == EOF && ferror( xbt_automaton_parse_in ) ) \
+                       YY_FATAL_ERROR( "input in flex scanner failed" ); \
+               result = n; \
+               } \
+       else \
+               { \
+               errno=0; \
+               while ( (result = fread(buf, 1, max_size, xbt_automaton_parse_in))==0 && ferror(xbt_automaton_parse_in)) \
+                       { \
+                       if( errno != EINTR) \
+                               { \
+                               YY_FATAL_ERROR( "input in flex scanner failed" ); \
+                               break; \
+                               } \
+                       errno=0; \
+                       clearerr(xbt_automaton_parse_in); \
+                       } \
+               }\
+\
+
+#endif
+
+/* No semi-colon after return; correct usage is to write "yyterminate();" -
+ * we don't want an extra ';' after the "return" because that will cause
+ * some compilers to complain about unreachable statements.
+ */
+#ifndef yyterminate
+#define yyterminate() return YY_NULL
+#endif
+
+/* Number of entries by which start-condition stack grows. */
+#ifndef YY_START_STACK_INCR
+#define YY_START_STACK_INCR 25
+#endif
+
+/* Report a fatal error. */
+#ifndef YY_FATAL_ERROR
+#define YY_FATAL_ERROR(msg) yy_fatal_error( msg )
+#endif
+
+/* end tables serialization structures and prototypes */
+
+/* Default declaration of generated scanner - a define so the user can
+ * easily add parameters.
+ */
+#ifndef YY_DECL
+#define YY_DECL_IS_OURS 1
+
+extern int xbt_automaton_parse_lex (void);
+
+#define YY_DECL int xbt_automaton_parse_lex (void)
+#endif /* !YY_DECL */
+
+/* Code executed at the beginning of each rule, after xbt_automaton_parse_text and xbt_automaton_parse_leng
+ * have been set up.
+ */
+#ifndef YY_USER_ACTION
+#define YY_USER_ACTION
+#endif
+
+/* Code executed at the end of each rule. */
+#ifndef YY_BREAK
+#define YY_BREAK break;
+#endif
+
+#define YY_RULE_SETUP \
+       YY_USER_ACTION
+
+/** The main scanner function which does all the work.
+ */
+YY_DECL
+{
+       register yy_state_type yy_current_state;
+       register char *yy_cp, *yy_bp;
+       register int yy_act;
+    
+#line 28 "parserPromela.lex"
+
+
+#line 723 "automaton_parse.yy.c"
+
+       if ( !(yy_init) )
+               {
+               (yy_init) = 1;
+
+#ifdef YY_USER_INIT
+               YY_USER_INIT;
+#endif
+
+               if ( ! (yy_start) )
+                       (yy_start) = 1; /* first start state */
+
+               if ( ! xbt_automaton_parse_in )
+                       xbt_automaton_parse_in = stdin;
+
+               if ( ! xbt_automaton_parse_out )
+                       xbt_automaton_parse_out = stdout;
+
+               if ( ! YY_CURRENT_BUFFER ) {
+                       xbt_automaton_parse_ensure_buffer_stack ();
+                       YY_CURRENT_BUFFER_LVALUE =
+                               xbt_automaton_parse__create_buffer(xbt_automaton_parse_in,YY_BUF_SIZE );
+               }
+
+               xbt_automaton_parse__load_buffer_state( );
+               }
+
+       while ( 1 )             /* loops until end-of-file is reached */
+               {
+               yy_cp = (yy_c_buf_p);
+
+               /* Support of xbt_automaton_parse_text. */
+               *yy_cp = (yy_hold_char);
+
+               /* yy_bp points to the position in yy_ch_buf of the start of
+                * the current run.
+                */
+               yy_bp = yy_cp;
+
+               yy_current_state = (yy_start);
+yy_match:
+               do
+                       {
+                       register YY_CHAR yy_c = yy_ec[YY_SC_TO_UI(*yy_cp)];
+                       if ( yy_accept[yy_current_state] )
+                               {
+                               (yy_last_accepting_state) = yy_current_state;
+                               (yy_last_accepting_cpos) = yy_cp;
+                               }
+                       while ( yy_chk[yy_base[yy_current_state] + yy_c] != yy_current_state )
+                               {
+                               yy_current_state = (int) yy_def[yy_current_state];
+                               if ( yy_current_state >= 54 )
+                                       yy_c = yy_meta[(unsigned int) yy_c];
+                               }
+                       yy_current_state = yy_nxt[yy_base[yy_current_state] + (unsigned int) yy_c];
+                       ++yy_cp;
+                       }
+               while ( yy_base[yy_current_state] != 90 );
+
+yy_find_action:
+               yy_act = yy_accept[yy_current_state];
+               if ( yy_act == 0 )
+                       { /* have to back up */
+                       yy_cp = (yy_last_accepting_cpos);
+                       yy_current_state = (yy_last_accepting_state);
+                       yy_act = yy_accept[yy_current_state];
+                       }
+
+               YY_DO_BEFORE_ACTION;
+
+do_action:     /* This label is used only to access EOF actions. */
+
+               switch ( yy_act )
+       { /* beginning of action switch */
+                       case 0: /* must back up */
+                       /* undo the effects of YY_DO_BEFORE_ACTION */
+                       *yy_cp = (yy_hold_char);
+                       yy_cp = (yy_last_accepting_cpos);
+                       yy_current_state = (yy_last_accepting_state);
+                       goto yy_find_action;
+
+case 1:
+YY_RULE_SETUP
+#line 30 "parserPromela.lex"
+{ printf("%s", xbt_automaton_parse_text); return (NEVER); }
+       YY_BREAK
+case 2:
+YY_RULE_SETUP
+#line 31 "parserPromela.lex"
+{ printf("%s", xbt_automaton_parse_text); return (IF); }
+       YY_BREAK
+case 3:
+YY_RULE_SETUP
+#line 32 "parserPromela.lex"
+{ printf("%s", xbt_automaton_parse_text); 
+               return (FI); }
+       YY_BREAK
+case 4:
+YY_RULE_SETUP
+#line 34 "parserPromela.lex"
+{ printf("%s", xbt_automaton_parse_text); return (IMPLIES); }
+       YY_BREAK
+case 5:
+YY_RULE_SETUP
+#line 35 "parserPromela.lex"
+{ printf("%s", xbt_automaton_parse_text); return (GOTO); }
+       YY_BREAK
+case 6:
+YY_RULE_SETUP
+#line 36 "parserPromela.lex"
+{ printf("%s", xbt_automaton_parse_text); return (AND); }
+       YY_BREAK
+case 7:
+YY_RULE_SETUP
+#line 37 "parserPromela.lex"
+{ printf("%s", xbt_automaton_parse_text); return (OR); }
+       YY_BREAK
+case 8:
+YY_RULE_SETUP
+#line 38 "parserPromela.lex"
+{ printf("%s", xbt_automaton_parse_text); return (NOT); }
+       YY_BREAK
+case 9:
+YY_RULE_SETUP
+#line 39 "parserPromela.lex"
+{ printf("%s", xbt_automaton_parse_text); return (LEFT_PAR); }
+       YY_BREAK
+case 10:
+YY_RULE_SETUP
+#line 40 "parserPromela.lex"
+{ printf("%s", xbt_automaton_parse_text); return (RIGHT_PAR); }
+       YY_BREAK
+case 11:
+YY_RULE_SETUP
+#line 41 "parserPromela.lex"
+{ printf("%s", xbt_automaton_parse_text); return (CASE); }
+       YY_BREAK
+case 12:
+YY_RULE_SETUP
+#line 42 "parserPromela.lex"
+{ printf("%s", xbt_automaton_parse_text); return (COLON); }
+       YY_BREAK
+case 13:
+YY_RULE_SETUP
+#line 43 "parserPromela.lex"
+{ printf("%s", xbt_automaton_parse_text); return (SEMI_COLON); }
+       YY_BREAK
+case 14:
+YY_RULE_SETUP
+#line 44 "parserPromela.lex"
+{ printf("%s", xbt_automaton_parse_text); return (CASE_TRUE); }
+       YY_BREAK
+case 15:
+YY_RULE_SETUP
+#line 45 "parserPromela.lex"
+{ printf("%s", xbt_automaton_parse_text); return (LEFT_BRACE); }
+       YY_BREAK
+case 16:
+YY_RULE_SETUP
+#line 46 "parserPromela.lex"
+{ printf("%s", xbt_automaton_parse_text); return (RIGHT_BRACE); }
+       YY_BREAK
+case 17:
+/* rule 17 can match eol */
+YY_RULE_SETUP
+#line 49 "parserPromela.lex"
+{ printf(" ");}
+       YY_BREAK
+case 18:
+YY_RULE_SETUP
+#line 51 "parserPromela.lex"
+{ printf("%s",xbt_automaton_parse_text); }
+       YY_BREAK
+case 19:
+YY_RULE_SETUP
+#line 54 "parserPromela.lex"
+{ printf("%s",xbt_automaton_parse_text); 
+                            sscanf(xbt_automaton_parse_text,"%lf",&yylval.real); 
+                            return (LITT_REEL); }
+       YY_BREAK
+case 20:
+YY_RULE_SETUP
+#line 58 "parserPromela.lex"
+{ printf("%s",xbt_automaton_parse_text); 
+                            sscanf(xbt_automaton_parse_text,"%d",&yylval.integer); 
+                            return (LITT_ENT); }
+       YY_BREAK
+case 21:
+/* rule 21 can match eol */
+YY_RULE_SETUP
+#line 62 "parserPromela.lex"
+{ printf("%s",xbt_automaton_parse_text);  
+                            yylval.string=(char *)malloc(strlen(xbt_automaton_parse_text)+1);
+                            sscanf(xbt_automaton_parse_text,"%s",yylval.string); 
+                            return (LITT_CHAINE); }
+       YY_BREAK
+case 22:
+YY_RULE_SETUP
+#line 67 "parserPromela.lex"
+{ printf("%s",xbt_automaton_parse_text); 
+                           yylval.string=(char *)malloc(strlen(xbt_automaton_parse_text)+1);
+                           sscanf(xbt_automaton_parse_text,"%s",yylval.string);
+                           return (ID); }
+       YY_BREAK
+case 23:
+/* rule 23 can match eol */
+YY_RULE_SETUP
+#line 72 "parserPromela.lex"
+{ printf("\n"); }
+       YY_BREAK
+case 24:
+YY_RULE_SETUP
+#line 74 "parserPromela.lex"
+{ printf("caractère inconnu\n"); }
+       YY_BREAK
+case 25:
+YY_RULE_SETUP
+#line 76 "parserPromela.lex"
+ECHO;
+       YY_BREAK
+#line 945 "automaton_parse.yy.c"
+case YY_STATE_EOF(INITIAL):
+       yyterminate();
+
+       case YY_END_OF_BUFFER:
+               {
+               /* Amount of text matched not including the EOB char. */
+               int yy_amount_of_matched_text = (int) (yy_cp - (yytext_ptr)) - 1;
+
+               /* Undo the effects of YY_DO_BEFORE_ACTION. */
+               *yy_cp = (yy_hold_char);
+               YY_RESTORE_YY_MORE_OFFSET
+
+               if ( YY_CURRENT_BUFFER_LVALUE->yy_buffer_status == YY_BUFFER_NEW )
+                       {
+                       /* We're scanning a new file or input source.  It's
+                        * possible that this happened because the user
+                        * just pointed xbt_automaton_parse_in at a new source and called
+                        * xbt_automaton_parse_lex().  If so, then we have to assure
+                        * consistency between YY_CURRENT_BUFFER and our
+                        * globals.  Here is the right place to do so, because
+                        * this is the first action (other than possibly a
+                        * back-up) that will match for the new input source.
+                        */
+                       (yy_n_chars) = YY_CURRENT_BUFFER_LVALUE->yy_n_chars;
+                       YY_CURRENT_BUFFER_LVALUE->yy_input_file = xbt_automaton_parse_in;
+                       YY_CURRENT_BUFFER_LVALUE->yy_buffer_status = YY_BUFFER_NORMAL;
+                       }
+
+               /* Note that here we test for yy_c_buf_p "<=" to the position
+                * of the first EOB in the buffer, since yy_c_buf_p will
+                * already have been incremented past the NUL character
+                * (since all states make transitions on EOB to the
+                * end-of-buffer state).  Contrast this with the test
+                * in input().
+                */
+               if ( (yy_c_buf_p) <= &YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[(yy_n_chars)] )
+                       { /* This was really a NUL. */
+                       yy_state_type yy_next_state;
+
+                       (yy_c_buf_p) = (yytext_ptr) + yy_amount_of_matched_text;
+
+                       yy_current_state = yy_get_previous_state(  );
+
+                       /* Okay, we're now positioned to make the NUL
+                        * transition.  We couldn't have
+                        * yy_get_previous_state() go ahead and do it
+                        * for us because it doesn't know how to deal
+                        * with the possibility of jamming (and we don't
+                        * want to build jamming into it because then it
+                        * will run more slowly).
+                        */
+
+                       yy_next_state = yy_try_NUL_trans( yy_current_state );
+
+                       yy_bp = (yytext_ptr) + YY_MORE_ADJ;
+
+                       if ( yy_next_state )
+                               {
+                               /* Consume the NUL. */
+                               yy_cp = ++(yy_c_buf_p);
+                               yy_current_state = yy_next_state;
+                               goto yy_match;
+                               }
+
+                       else
+                               {
+                               yy_cp = (yy_c_buf_p);
+                               goto yy_find_action;
+                               }
+                       }
+
+               else switch ( yy_get_next_buffer(  ) )
+                       {
+                       case EOB_ACT_END_OF_FILE:
+                               {
+                               (yy_did_buffer_switch_on_eof) = 0;
+
+                               if ( xbt_automaton_parse_wrap( ) )
+                                       {
+                                       /* Note: because we've taken care in
+                                        * yy_get_next_buffer() to have set up
+                                        * xbt_automaton_parse_text, we can now set up
+                                        * yy_c_buf_p so that if some total
+                                        * hoser (like flex itself) wants to
+                                        * call the scanner after we return the
+                                        * YY_NULL, it'll still work - another
+                                        * YY_NULL will get returned.
+                                        */
+                                       (yy_c_buf_p) = (yytext_ptr) + YY_MORE_ADJ;
+
+                                       yy_act = YY_STATE_EOF(YY_START);
+                                       goto do_action;
+                                       }
+
+                               else
+                                       {
+                                       if ( ! (yy_did_buffer_switch_on_eof) )
+                                               YY_NEW_FILE;
+                                       }
+                               break;
+                               }
+
+                       case EOB_ACT_CONTINUE_SCAN:
+                               (yy_c_buf_p) =
+                                       (yytext_ptr) + yy_amount_of_matched_text;
+
+                               yy_current_state = yy_get_previous_state(  );
+
+                               yy_cp = (yy_c_buf_p);
+                               yy_bp = (yytext_ptr) + YY_MORE_ADJ;
+                               goto yy_match;
+
+                       case EOB_ACT_LAST_MATCH:
+                               (yy_c_buf_p) =
+                               &YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[(yy_n_chars)];
+
+                               yy_current_state = yy_get_previous_state(  );
+
+                               yy_cp = (yy_c_buf_p);
+                               yy_bp = (yytext_ptr) + YY_MORE_ADJ;
+                               goto yy_find_action;
+                       }
+               break;
+               }
+
+       default:
+               YY_FATAL_ERROR(
+                       "fatal flex scanner internal error--no action found" );
+       } /* end of action switch */
+               } /* end of scanning one token */
+} /* end of xbt_automaton_parse_lex */
+
+/* yy_get_next_buffer - try to read in a new buffer
+ *
+ * Returns a code representing an action:
+ *     EOB_ACT_LAST_MATCH -
+ *     EOB_ACT_CONTINUE_SCAN - continue scanning from current position
+ *     EOB_ACT_END_OF_FILE - end of file
+ */
+static int yy_get_next_buffer (void)
+{
+       register char *dest = YY_CURRENT_BUFFER_LVALUE->yy_ch_buf;
+       register char *source = (yytext_ptr);
+       register int number_to_move, i;
+       int ret_val;
+
+       if ( (yy_c_buf_p) > &YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[(yy_n_chars) + 1] )
+               YY_FATAL_ERROR(
+               "fatal flex scanner internal error--end of buffer missed" );
+
+       if ( YY_CURRENT_BUFFER_LVALUE->yy_fill_buffer == 0 )
+               { /* Don't try to fill the buffer, so this is an EOF. */
+               if ( (yy_c_buf_p) - (yytext_ptr) - YY_MORE_ADJ == 1 )
+                       {
+                       /* We matched a single character, the EOB, so
+                        * treat this as a final EOF.
+                        */
+                       return EOB_ACT_END_OF_FILE;
+                       }
+
+               else
+                       {
+                       /* We matched some text prior to the EOB, first
+                        * process it.
+                        */
+                       return EOB_ACT_LAST_MATCH;
+                       }
+               }
+
+       /* Try to read more data. */
+
+       /* First move last chars to start of buffer. */
+       number_to_move = (int) ((yy_c_buf_p) - (yytext_ptr)) - 1;
+
+       for ( i = 0; i < number_to_move; ++i )
+               *(dest++) = *(source++);
+
+       if ( YY_CURRENT_BUFFER_LVALUE->yy_buffer_status == YY_BUFFER_EOF_PENDING )
+               /* don't do the read, it's not guaranteed to return an EOF,
+                * just force an EOF
+                */
+               YY_CURRENT_BUFFER_LVALUE->yy_n_chars = (yy_n_chars) = 0;
+
+       else
+               {
+                       int num_to_read =
+                       YY_CURRENT_BUFFER_LVALUE->yy_buf_size - number_to_move - 1;
+
+               while ( num_to_read <= 0 )
+                       { /* Not enough room in the buffer - grow it. */
+
+                       /* just a shorter name for the current buffer */
+                       YY_BUFFER_STATE b = YY_CURRENT_BUFFER;
+
+                       int yy_c_buf_p_offset =
+                               (int) ((yy_c_buf_p) - b->yy_ch_buf);
+
+                       if ( b->yy_is_our_buffer )
+                               {
+                               int new_size = b->yy_buf_size * 2;
+
+                               if ( new_size <= 0 )
+                                       b->yy_buf_size += b->yy_buf_size / 8;
+                               else
+                                       b->yy_buf_size *= 2;
+
+                               b->yy_ch_buf = (char *)
+                                       /* Include room in for 2 EOB chars. */
+                                       xbt_automaton_parse_realloc((void *) b->yy_ch_buf,b->yy_buf_size + 2  );
+                               }
+                       else
+                               /* Can't grow it, we don't own it. */
+                               b->yy_ch_buf = 0;
+
+                       if ( ! b->yy_ch_buf )
+                               YY_FATAL_ERROR(
+                               "fatal error - scanner input buffer overflow" );
+
+                       (yy_c_buf_p) = &b->yy_ch_buf[yy_c_buf_p_offset];
+
+                       num_to_read = YY_CURRENT_BUFFER_LVALUE->yy_buf_size -
+                                               number_to_move - 1;
+
+                       }
+
+               if ( num_to_read > YY_READ_BUF_SIZE )
+                       num_to_read = YY_READ_BUF_SIZE;
+
+               /* Read in more data. */
+               YY_INPUT( (&YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[number_to_move]),
+                       (yy_n_chars), (size_t) num_to_read );
+
+               YY_CURRENT_BUFFER_LVALUE->yy_n_chars = (yy_n_chars);
+               }
+
+       if ( (yy_n_chars) == 0 )
+               {
+               if ( number_to_move == YY_MORE_ADJ )
+                       {
+                       ret_val = EOB_ACT_END_OF_FILE;
+                       xbt_automaton_parse_restart(xbt_automaton_parse_in  );
+                       }
+
+               else
+                       {
+                       ret_val = EOB_ACT_LAST_MATCH;
+                       YY_CURRENT_BUFFER_LVALUE->yy_buffer_status =
+                               YY_BUFFER_EOF_PENDING;
+                       }
+               }
+
+       else
+               ret_val = EOB_ACT_CONTINUE_SCAN;
+
+       if ((yy_size_t) ((yy_n_chars) + number_to_move) > YY_CURRENT_BUFFER_LVALUE->yy_buf_size) {
+               /* Extend the array by 50%, plus the number we really need. */
+               yy_size_t new_size = (yy_n_chars) + number_to_move + ((yy_n_chars) >> 1);
+               YY_CURRENT_BUFFER_LVALUE->yy_ch_buf = (char *) xbt_automaton_parse_realloc((void *) YY_CURRENT_BUFFER_LVALUE->yy_ch_buf,new_size  );
+               if ( ! YY_CURRENT_BUFFER_LVALUE->yy_ch_buf )
+                       YY_FATAL_ERROR( "out of dynamic memory in yy_get_next_buffer()" );
+       }
+
+       (yy_n_chars) += number_to_move;
+       YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[(yy_n_chars)] = YY_END_OF_BUFFER_CHAR;
+       YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[(yy_n_chars) + 1] = YY_END_OF_BUFFER_CHAR;
+
+       (yytext_ptr) = &YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[0];
+
+       return ret_val;
+}
+
+/* yy_get_previous_state - get the state just before the EOB char was reached */
+
+    static yy_state_type yy_get_previous_state (void)
+{
+       register yy_state_type yy_current_state;
+       register char *yy_cp;
+    
+       yy_current_state = (yy_start);
+
+       for ( yy_cp = (yytext_ptr) + YY_MORE_ADJ; yy_cp < (yy_c_buf_p); ++yy_cp )
+               {
+               register YY_CHAR yy_c = (*yy_cp ? yy_ec[YY_SC_TO_UI(*yy_cp)] : 1);
+               if ( yy_accept[yy_current_state] )
+                       {
+                       (yy_last_accepting_state) = yy_current_state;
+                       (yy_last_accepting_cpos) = yy_cp;
+                       }
+               while ( yy_chk[yy_base[yy_current_state] + yy_c] != yy_current_state )
+                       {
+                       yy_current_state = (int) yy_def[yy_current_state];
+                       if ( yy_current_state >= 54 )
+                               yy_c = yy_meta[(unsigned int) yy_c];
+                       }
+               yy_current_state = yy_nxt[yy_base[yy_current_state] + (unsigned int) yy_c];
+               }
+
+       return yy_current_state;
+}
+
+/* yy_try_NUL_trans - try to make a transition on the NUL character
+ *
+ * synopsis
+ *     next_state = yy_try_NUL_trans( current_state );
+ */
+    static yy_state_type yy_try_NUL_trans  (yy_state_type yy_current_state )
+{
+       register int yy_is_jam;
+       register char *yy_cp = (yy_c_buf_p);
+
+       register YY_CHAR yy_c = 1;
+       if ( yy_accept[yy_current_state] )
+               {
+               (yy_last_accepting_state) = yy_current_state;
+               (yy_last_accepting_cpos) = yy_cp;
+               }
+       while ( yy_chk[yy_base[yy_current_state] + yy_c] != yy_current_state )
+               {
+               yy_current_state = (int) yy_def[yy_current_state];
+               if ( yy_current_state >= 54 )
+                       yy_c = yy_meta[(unsigned int) yy_c];
+               }
+       yy_current_state = yy_nxt[yy_base[yy_current_state] + (unsigned int) yy_c];
+       yy_is_jam = (yy_current_state == 53);
+
+       return yy_is_jam ? 0 : yy_current_state;
+}
+
+    static void yyunput (int c, register char * yy_bp )
+{
+       register char *yy_cp;
+    
+    yy_cp = (yy_c_buf_p);
+
+       /* undo effects of setting up xbt_automaton_parse_text */
+       *yy_cp = (yy_hold_char);
+
+       if ( yy_cp < YY_CURRENT_BUFFER_LVALUE->yy_ch_buf + 2 )
+               { /* need to shift things up to make room */
+               /* +2 for EOB chars. */
+               register int number_to_move = (yy_n_chars) + 2;
+               register char *dest = &YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[
+                                       YY_CURRENT_BUFFER_LVALUE->yy_buf_size + 2];
+               register char *source =
+                               &YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[number_to_move];
+
+               while ( source > YY_CURRENT_BUFFER_LVALUE->yy_ch_buf )
+                       *--dest = *--source;
+
+               yy_cp += (int) (dest - source);
+               yy_bp += (int) (dest - source);
+               YY_CURRENT_BUFFER_LVALUE->yy_n_chars =
+                       (yy_n_chars) = YY_CURRENT_BUFFER_LVALUE->yy_buf_size;
+
+               if ( yy_cp < YY_CURRENT_BUFFER_LVALUE->yy_ch_buf + 2 )
+                       YY_FATAL_ERROR( "flex scanner push-back overflow" );
+               }
+
+       *--yy_cp = (char) c;
+
+       (yytext_ptr) = yy_bp;
+       (yy_hold_char) = *yy_cp;
+       (yy_c_buf_p) = yy_cp;
+}
+
+#ifndef YY_NO_INPUT
+#ifdef __cplusplus
+    static int yyinput (void)
+#else
+    static int input  (void)
+#endif
+
+{
+       int c;
+    
+       *(yy_c_buf_p) = (yy_hold_char);
+
+       if ( *(yy_c_buf_p) == YY_END_OF_BUFFER_CHAR )
+               {
+               /* yy_c_buf_p now points to the character we want to return.
+                * If this occurs *before* the EOB characters, then it's a
+                * valid NUL; if not, then we've hit the end of the buffer.
+                */
+               if ( (yy_c_buf_p) < &YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[(yy_n_chars)] )
+                       /* This was really a NUL. */
+                       *(yy_c_buf_p) = '\0';
+
+               else
+                       { /* need more input */
+                       int offset = (yy_c_buf_p) - (yytext_ptr);
+                       ++(yy_c_buf_p);
+
+                       switch ( yy_get_next_buffer(  ) )
+                               {
+                               case EOB_ACT_LAST_MATCH:
+                                       /* This happens because yy_g_n_b()
+                                        * sees that we've accumulated a
+                                        * token and flags that we need to
+                                        * try matching the token before
+                                        * proceeding.  But for input(),
+                                        * there's no matching to consider.
+                                        * So convert the EOB_ACT_LAST_MATCH
+                                        * to EOB_ACT_END_OF_FILE.
+                                        */
+
+                                       /* Reset buffer status. */
+                                       xbt_automaton_parse_restart(xbt_automaton_parse_in );
+
+                                       /*FALLTHROUGH*/
+
+                               case EOB_ACT_END_OF_FILE:
+                                       {
+                                       if ( xbt_automaton_parse_wrap( ) )
+                                               return EOF;
+
+                                       if ( ! (yy_did_buffer_switch_on_eof) )
+                                               YY_NEW_FILE;
+#ifdef __cplusplus
+                                       return yyinput();
+#else
+                                       return input();
+#endif
+                                       }
+
+                               case EOB_ACT_CONTINUE_SCAN:
+                                       (yy_c_buf_p) = (yytext_ptr) + offset;
+                                       break;
+                               }
+                       }
+               }
+
+       c = *(unsigned char *) (yy_c_buf_p);    /* cast for 8-bit char's */
+       *(yy_c_buf_p) = '\0';   /* preserve xbt_automaton_parse_text */
+       (yy_hold_char) = *++(yy_c_buf_p);
+
+       return c;
+}
+#endif /* ifndef YY_NO_INPUT */
+
+/** Immediately switch to a different input stream.
+ * @param input_file A readable stream.
+ * 
+ * @note This function does not reset the start condition to @c INITIAL .
+ */
+    void xbt_automaton_parse_restart  (FILE * input_file )
+{
+    
+       if ( ! YY_CURRENT_BUFFER ){
+        xbt_automaton_parse_ensure_buffer_stack ();
+               YY_CURRENT_BUFFER_LVALUE =
+            xbt_automaton_parse__create_buffer(xbt_automaton_parse_in,YY_BUF_SIZE );
+       }
+
+       xbt_automaton_parse__init_buffer(YY_CURRENT_BUFFER,input_file );
+       xbt_automaton_parse__load_buffer_state( );
+}
+
+/** Switch to a different input buffer.
+ * @param new_buffer The new input buffer.
+ * 
+ */
+    void xbt_automaton_parse__switch_to_buffer  (YY_BUFFER_STATE  new_buffer )
+{
+    
+       /* TODO. We should be able to replace this entire function body
+        * with
+        *              xbt_automaton_parse_pop_buffer_state();
+        *              xbt_automaton_parse_push_buffer_state(new_buffer);
+     */
+       xbt_automaton_parse_ensure_buffer_stack ();
+       if ( YY_CURRENT_BUFFER == new_buffer )
+               return;
+
+       if ( YY_CURRENT_BUFFER )
+               {
+               /* Flush out information for old buffer. */
+               *(yy_c_buf_p) = (yy_hold_char);
+               YY_CURRENT_BUFFER_LVALUE->yy_buf_pos = (yy_c_buf_p);
+               YY_CURRENT_BUFFER_LVALUE->yy_n_chars = (yy_n_chars);
+               }
+
+       YY_CURRENT_BUFFER_LVALUE = new_buffer;
+       xbt_automaton_parse__load_buffer_state( );
+
+       /* We don't actually know whether we did this switch during
+        * EOF (xbt_automaton_parse_wrap()) processing, but the only time this flag
+        * is looked at is after xbt_automaton_parse_wrap() is called, so it's safe
+        * to go ahead and always set it.
+        */
+       (yy_did_buffer_switch_on_eof) = 1;
+}
+
+static void xbt_automaton_parse__load_buffer_state  (void)
+{
+       (yy_n_chars) = YY_CURRENT_BUFFER_LVALUE->yy_n_chars;
+       (yytext_ptr) = (yy_c_buf_p) = YY_CURRENT_BUFFER_LVALUE->yy_buf_pos;
+       xbt_automaton_parse_in = YY_CURRENT_BUFFER_LVALUE->yy_input_file;
+       (yy_hold_char) = *(yy_c_buf_p);
+}
+
+/** Allocate and initialize an input buffer state.
+ * @param file A readable stream.
+ * @param size The character buffer size in bytes. When in doubt, use @c YY_BUF_SIZE.
+ * 
+ * @return the allocated buffer state.
+ */
+    YY_BUFFER_STATE xbt_automaton_parse__create_buffer  (FILE * file, int  size )
+{
+       YY_BUFFER_STATE b;
+    
+       b = (YY_BUFFER_STATE) xbt_automaton_parse_alloc(sizeof( struct yy_buffer_state )  );
+       if ( ! b )
+               YY_FATAL_ERROR( "out of dynamic memory in xbt_automaton_parse__create_buffer()" );
+
+       b->yy_buf_size = size;
+
+       /* yy_ch_buf has to be 2 characters longer than the size given because
+        * we need to put in 2 end-of-buffer characters.
+        */
+       b->yy_ch_buf = (char *) xbt_automaton_parse_alloc(b->yy_buf_size + 2  );
+       if ( ! b->yy_ch_buf )
+               YY_FATAL_ERROR( "out of dynamic memory in xbt_automaton_parse__create_buffer()" );
+
+       b->yy_is_our_buffer = 1;
+
+       xbt_automaton_parse__init_buffer(b,file );
+
+       return b;
+}
+
+/** Destroy the buffer.
+ * @param b a buffer created with xbt_automaton_parse__create_buffer()
+ * 
+ */
+    void xbt_automaton_parse__delete_buffer (YY_BUFFER_STATE  b )
+{
+    
+       if ( ! b )
+               return;
+
+       if ( b == YY_CURRENT_BUFFER ) /* Not sure if we should pop here. */
+               YY_CURRENT_BUFFER_LVALUE = (YY_BUFFER_STATE) 0;
+
+       if ( b->yy_is_our_buffer )
+               xbt_automaton_parse_free((void *) b->yy_ch_buf  );
+
+       xbt_automaton_parse_free((void *) b  );
+}
+
+#ifndef __cplusplus
+extern int isatty (int );
+#endif /* __cplusplus */
+    
+/* Initializes or reinitializes a buffer.
+ * This function is sometimes called more than once on the same buffer,
+ * such as during a xbt_automaton_parse_restart() or at EOF.
+ */
+    static void xbt_automaton_parse__init_buffer  (YY_BUFFER_STATE  b, FILE * file )
+
+{
+       int oerrno = errno;
+    
+       xbt_automaton_parse__flush_buffer(b );
+
+       b->yy_input_file = file;
+       b->yy_fill_buffer = 1;
+
+    /* If b is the current buffer, then xbt_automaton_parse__init_buffer was _probably_
+     * called from xbt_automaton_parse_restart() or through yy_get_next_buffer.
+     * In that case, we don't want to reset the lineno or column.
+     */
+    if (b != YY_CURRENT_BUFFER){
+        b->yy_bs_lineno = 1;
+        b->yy_bs_column = 0;
+    }
+
+        b->yy_is_interactive = file ? (isatty( fileno(file) ) > 0) : 0;
+    
+       errno = oerrno;
+}
+
+/** Discard all buffered characters. On the next scan, YY_INPUT will be called.
+ * @param b the buffer state to be flushed, usually @c YY_CURRENT_BUFFER.
+ * 
+ */
+    void xbt_automaton_parse__flush_buffer (YY_BUFFER_STATE  b )
+{
+       if ( ! b )
+               return;
+
+       b->yy_n_chars = 0;
+
+       /* We always need two end-of-buffer characters.  The first causes
+        * a transition to the end-of-buffer state.  The second causes
+        * a jam in that state.
+        */
+       b->yy_ch_buf[0] = YY_END_OF_BUFFER_CHAR;
+       b->yy_ch_buf[1] = YY_END_OF_BUFFER_CHAR;
+
+       b->yy_buf_pos = &b->yy_ch_buf[0];
+
+       b->yy_at_bol = 1;
+       b->yy_buffer_status = YY_BUFFER_NEW;
+
+       if ( b == YY_CURRENT_BUFFER )
+               xbt_automaton_parse__load_buffer_state( );
+}
+
+/** Pushes the new state onto the stack. The new state becomes
+ *  the current state. This function will allocate the stack
+ *  if necessary.
+ *  @param new_buffer The new state.
+ *  
+ */
+void xbt_automaton_parse_push_buffer_state (YY_BUFFER_STATE new_buffer )
+{
+       if (new_buffer == NULL)
+               return;
+
+       xbt_automaton_parse_ensure_buffer_stack();
+
+       /* This block is copied from xbt_automaton_parse__switch_to_buffer. */
+       if ( YY_CURRENT_BUFFER )
+               {
+               /* Flush out information for old buffer. */
+               *(yy_c_buf_p) = (yy_hold_char);
+               YY_CURRENT_BUFFER_LVALUE->yy_buf_pos = (yy_c_buf_p);
+               YY_CURRENT_BUFFER_LVALUE->yy_n_chars = (yy_n_chars);
+               }
+
+       /* Only push if top exists. Otherwise, replace top. */
+       if (YY_CURRENT_BUFFER)
+               (yy_buffer_stack_top)++;
+       YY_CURRENT_BUFFER_LVALUE = new_buffer;
+
+       /* copied from xbt_automaton_parse__switch_to_buffer. */
+       xbt_automaton_parse__load_buffer_state( );
+       (yy_did_buffer_switch_on_eof) = 1;
+}
+
+/** Removes and deletes the top of the stack, if present.
+ *  The next element becomes the new top.
+ *  
+ */
+void xbt_automaton_parse_pop_buffer_state (void)
+{
+       if (!YY_CURRENT_BUFFER)
+               return;
+
+       xbt_automaton_parse__delete_buffer(YY_CURRENT_BUFFER );
+       YY_CURRENT_BUFFER_LVALUE = NULL;
+       if ((yy_buffer_stack_top) > 0)
+               --(yy_buffer_stack_top);
+
+       if (YY_CURRENT_BUFFER) {
+               xbt_automaton_parse__load_buffer_state( );
+               (yy_did_buffer_switch_on_eof) = 1;
+       }
+}
+
+/* Allocates the stack if it does not exist.
+ *  Guarantees space for at least one push.
+ */
+static void xbt_automaton_parse_ensure_buffer_stack (void)
+{
+       int num_to_alloc;
+    
+       if (!(yy_buffer_stack)) {
+
+               /* First allocation is just for 2 elements, since we don't know if this
+                * scanner will even need a stack. We use 2 instead of 1 to avoid an
+                * immediate realloc on the next call.
+         */
+               num_to_alloc = 1;
+               (yy_buffer_stack) = (struct yy_buffer_state**)xbt_automaton_parse_alloc
+                                                               (num_to_alloc * sizeof(struct yy_buffer_state*)
+                                                               );
+               if ( ! (yy_buffer_stack) )
+                       YY_FATAL_ERROR( "out of dynamic memory in xbt_automaton_parse_ensure_buffer_stack()" );
+                                                                 
+               memset((yy_buffer_stack), 0, num_to_alloc * sizeof(struct yy_buffer_state*));
+                               
+               (yy_buffer_stack_max) = num_to_alloc;
+               (yy_buffer_stack_top) = 0;
+               return;
+       }
+
+       if ((yy_buffer_stack_top) >= ((yy_buffer_stack_max)) - 1){
+
+               /* Increase the buffer to prepare for a possible push. */
+               int grow_size = 8 /* arbitrary grow size */;
+
+               num_to_alloc = (yy_buffer_stack_max) + grow_size;
+               (yy_buffer_stack) = (struct yy_buffer_state**)xbt_automaton_parse_realloc
+                                                               ((yy_buffer_stack),
+                                                               num_to_alloc * sizeof(struct yy_buffer_state*)
+                                                               );
+               if ( ! (yy_buffer_stack) )
+                       YY_FATAL_ERROR( "out of dynamic memory in xbt_automaton_parse_ensure_buffer_stack()" );
+
+               /* zero only the new slots.*/
+               memset((yy_buffer_stack) + (yy_buffer_stack_max), 0, grow_size * sizeof(struct yy_buffer_state*));
+               (yy_buffer_stack_max) = num_to_alloc;
+       }
+}
+
+/** Setup the input buffer state to scan directly from a user-specified character buffer.
+ * @param base the character buffer
+ * @param size the size in bytes of the character buffer
+ * 
+ * @return the newly allocated buffer state object. 
+ */
+YY_BUFFER_STATE xbt_automaton_parse__scan_buffer  (char * base, yy_size_t  size )
+{
+       YY_BUFFER_STATE b;
+    
+       if ( size < 2 ||
+            base[size-2] != YY_END_OF_BUFFER_CHAR ||
+            base[size-1] != YY_END_OF_BUFFER_CHAR )
+               /* They forgot to leave room for the EOB's. */
+               return 0;
+
+       b = (YY_BUFFER_STATE) xbt_automaton_parse_alloc(sizeof( struct yy_buffer_state )  );
+       if ( ! b )
+               YY_FATAL_ERROR( "out of dynamic memory in xbt_automaton_parse__scan_buffer()" );
+
+       b->yy_buf_size = size - 2;      /* "- 2" to take care of EOB's */
+       b->yy_buf_pos = b->yy_ch_buf = base;
+       b->yy_is_our_buffer = 0;
+       b->yy_input_file = 0;
+       b->yy_n_chars = b->yy_buf_size;
+       b->yy_is_interactive = 0;
+       b->yy_at_bol = 1;
+       b->yy_fill_buffer = 0;
+       b->yy_buffer_status = YY_BUFFER_NEW;
+
+       xbt_automaton_parse__switch_to_buffer(b  );
+
+       return b;
+}
+
+/** Setup the input buffer state to scan a string. The next call to xbt_automaton_parse_lex() will
+ * scan from a @e copy of @a str.
+ * @param yystr a NUL-terminated string to scan
+ * 
+ * @return the newly allocated buffer state object.
+ * @note If you want to scan bytes that may contain NUL values, then use
+ *       xbt_automaton_parse__scan_bytes() instead.
+ */
+YY_BUFFER_STATE xbt_automaton_parse__scan_string (yyconst char * yystr )
+{
+    
+       return xbt_automaton_parse__scan_bytes(yystr,strlen(yystr) );
+}
+
+/** Setup the input buffer state to scan the given bytes. The next call to xbt_automaton_parse_lex() will
+ * scan from a @e copy of @a bytes.
+ * @param yybytes the byte buffer to scan
+ * @param _yybytes_len the number of bytes in the buffer pointed to by @a bytes.
+ * 
+ * @return the newly allocated buffer state object.
+ */
+YY_BUFFER_STATE xbt_automaton_parse__scan_bytes  (yyconst char * yybytes, int  _yybytes_len )
+{
+       YY_BUFFER_STATE b;
+       char *buf;
+       yy_size_t n;
+       int i;
+    
+       /* Get memory for full buffer, including space for trailing EOB's. */
+       n = _yybytes_len + 2;
+       buf = (char *) xbt_automaton_parse_alloc(n  );
+       if ( ! buf )
+               YY_FATAL_ERROR( "out of dynamic memory in xbt_automaton_parse__scan_bytes()" );
+
+       for ( i = 0; i < _yybytes_len; ++i )
+               buf[i] = yybytes[i];
+
+       buf[_yybytes_len] = buf[_yybytes_len+1] = YY_END_OF_BUFFER_CHAR;
+
+       b = xbt_automaton_parse__scan_buffer(buf,n );
+       if ( ! b )
+               YY_FATAL_ERROR( "bad buffer in xbt_automaton_parse__scan_bytes()" );
+
+       /* It's okay to grow etc. this buffer, and we should throw it
+        * away when we're done.
+        */
+       b->yy_is_our_buffer = 1;
+
+       return b;
+}
+
+#ifndef YY_EXIT_FAILURE
+#define YY_EXIT_FAILURE 2
+#endif
+
+static void yy_fatal_error (yyconst char* msg )
+{
+       (void) fprintf( stderr, "%s\n", msg );
+       exit( YY_EXIT_FAILURE );
+}
+
+/* Redefine yyless() so it works in section 3 code. */
+
+#undef yyless
+#define yyless(n) \
+       do \
+               { \
+               /* Undo effects of setting up xbt_automaton_parse_text. */ \
+        int yyless_macro_arg = (n); \
+        YY_LESS_LINENO(yyless_macro_arg);\
+               xbt_automaton_parse_text[xbt_automaton_parse_leng] = (yy_hold_char); \
+               (yy_c_buf_p) = xbt_automaton_parse_text + yyless_macro_arg; \
+               (yy_hold_char) = *(yy_c_buf_p); \
+               *(yy_c_buf_p) = '\0'; \
+               xbt_automaton_parse_leng = yyless_macro_arg; \
+               } \
+       while ( 0 )
+
+/* Accessor  methods (get/set functions) to struct members. */
+
+/** Get the current line number.
+ * 
+ */
+int xbt_automaton_parse_get_lineno  (void)
+{
+        
+    return xbt_automaton_parse_lineno;
+}
+
+/** Get the input stream.
+ * 
+ */
+FILE *xbt_automaton_parse_get_in  (void)
+{
+        return xbt_automaton_parse_in;
+}
+
+/** Get the output stream.
+ * 
+ */
+FILE *xbt_automaton_parse_get_out  (void)
+{
+        return xbt_automaton_parse_out;
+}
+
+/** Get the length of the current token.
+ * 
+ */
+int xbt_automaton_parse_get_leng  (void)
+{
+        return xbt_automaton_parse_leng;
+}
+
+/** Get the current token.
+ * 
+ */
+
+char *xbt_automaton_parse_get_text  (void)
+{
+        return xbt_automaton_parse_text;
+}
+
+/** Set the current line number.
+ * @param line_number
+ * 
+ */
+void xbt_automaton_parse_set_lineno (int  line_number )
+{
+    
+    xbt_automaton_parse_lineno = line_number;
+}
+
+/** Set the input stream. This does not discard the current
+ * input buffer.
+ * @param in_str A readable stream.
+ * 
+ * @see xbt_automaton_parse__switch_to_buffer
+ */
+void xbt_automaton_parse_set_in (FILE *  in_str )
+{
+        xbt_automaton_parse_in = in_str ;
+}
+
+void xbt_automaton_parse_set_out (FILE *  out_str )
+{
+        xbt_automaton_parse_out = out_str ;
+}
+
+int xbt_automaton_parse_get_debug  (void)
+{
+        return xbt_automaton_parse__flex_debug;
+}
+
+void xbt_automaton_parse_set_debug (int  bdebug )
+{
+        xbt_automaton_parse__flex_debug = bdebug ;
+}
+
+static int yy_init_globals (void)
+{
+        /* Initialization is the same as for the non-reentrant scanner.
+     * This function is called from xbt_automaton_parse_lex_destroy(), so don't allocate here.
+     */
+
+    (yy_buffer_stack) = 0;
+    (yy_buffer_stack_top) = 0;
+    (yy_buffer_stack_max) = 0;
+    (yy_c_buf_p) = (char *) 0;
+    (yy_init) = 0;
+    (yy_start) = 0;
+
+/* Defined in main.c */
+#ifdef YY_STDINIT
+    xbt_automaton_parse_in = stdin;
+    xbt_automaton_parse_out = stdout;
+#else
+    xbt_automaton_parse_in = (FILE *) 0;
+    xbt_automaton_parse_out = (FILE *) 0;
+#endif
+
+    /* For future reference: Set errno on error, since we are called by
+     * xbt_automaton_parse_lex_init()
+     */
+    return 0;
+}
+
+/* xbt_automaton_parse_lex_destroy is for both reentrant and non-reentrant scanners. */
+int xbt_automaton_parse_lex_destroy  (void)
+{
+    
+    /* Pop the buffer stack, destroying each element. */
+       while(YY_CURRENT_BUFFER){
+               xbt_automaton_parse__delete_buffer(YY_CURRENT_BUFFER  );
+               YY_CURRENT_BUFFER_LVALUE = NULL;
+               xbt_automaton_parse_pop_buffer_state();
+       }
+
+       /* Destroy the stack itself. */
+       xbt_automaton_parse_free((yy_buffer_stack) );
+       (yy_buffer_stack) = NULL;
+
+    /* Reset the globals. This is important in a non-reentrant scanner so the next time
+     * xbt_automaton_parse_lex() is called, initialization will occur. */
+    yy_init_globals( );
+
+    return 0;
+}
+
+/*
+ * Internal utility routines.
+ */
+
+#ifndef yytext_ptr
+static void yy_flex_strncpy (char* s1, yyconst char * s2, int n )
+{
+       register int i;
+       for ( i = 0; i < n; ++i )
+               s1[i] = s2[i];
+}
+#endif
+
+#ifdef YY_NEED_STRLEN
+static int yy_flex_strlen (yyconst char * s )
+{
+       register int n;
+       for ( n = 0; s[n]; ++n )
+               ;
+
+       return n;
+}
+#endif
+
+void *xbt_automaton_parse_alloc (yy_size_t  size )
+{
+       return (void *) malloc( size );
+}
+
+void *xbt_automaton_parse_realloc  (void * ptr, yy_size_t  size )
+{
+       /* The cast to (char *) in the following accommodates both
+        * implementations that use char* generic pointers, and those
+        * that use void* generic pointers.  It works with the latter
+        * because both ANSI C and C++ allow castless assignment from
+        * any pointer type to void*, and deal with argument conversions
+        * as though doing an assignment.
+        */
+       return (void *) realloc( (char *) ptr, size );
+}
+
+void xbt_automaton_parse_free (void * ptr )
+{
+       free( (char *) ptr );   /* see xbt_automaton_parse_realloc() for (char *) cast */
+}
+
+#define YYTABLES_NAME "yytables"
+
+#line 76 "parserPromela.lex"
+
+
+
+
+
index 97e650d..30d97c3 100644 (file)
@@ -7,6 +7,7 @@
 
 #include <simgrid_config.h> /* HAVE_MC ? */
 #include <xbt.h>
+#include "xbt/automaton.h"
 
 #ifndef SIMGRID_MODELCHECKER_H
 #define SIMGRID_MODELCHECKER_H
@@ -20,6 +21,7 @@ XBT_PUBLIC(void) MC_assert(int);
 XBT_PUBLIC(void) MC_assert_stateful(int);
 XBT_PUBLIC(int) MC_random(int min, int max);
 XBT_PUBLIC(void) MC_diff(void);
+XBT_PUBLIC(xbt_automaton_t) MC_create_automaton(const char *file);
 
 #else
 
index 56e7e6e..f140ed2 100644 (file)
@@ -1,11 +1,3 @@
-/*  xbt/automaton.h -- büchi automaton                                      */
-
-/* Copyright (c) 2011. The SimGrid Team.
- * All rights reserved.                                                     */
-
-/* This program is free software; you can redistribute it and/or modify it
- * under the terms of the license (GNU LGPL) which comes with this package. */
-
 #ifndef _XBT_AUTOMATON_H
 #define _XBT_AUTOMATON_H
 
@@ -36,9 +28,7 @@ typedef struct xbt_automaton {
 typedef struct xbt_automaton* xbt_automaton_t;
 
 typedef struct xbt_exp_label{
-  /* fixme: "or", "and", and "not" are reserved keywords in C++ */
-  /* enum{or=0, and=1, not=2, predicat=3, one=4} type; */
-  int type;
+  enum{or=0, and=1, not=2, predicat=3, one=4} type;
   union{
     struct{
       struct xbt_exp_label* left_exp;
index 7fb7d5a..c80c34d 100644 (file)
@@ -1,11 +1,3 @@
-/*  xbt/automatonparse_promela.h -- implementation automaton from promela file    */
-
-/* Copyright (c) 2011. The SimGrid Team.
- * All rights reserved.                                                     */
-
-/* This program is free software; you can redistribute it and/or modify it
- * under the terms of the license (GNU LGPL) which comes with this package. */
-
 #ifndef _XBT_AUTOMATONPARSE_PROMELA_H
 #define _XBT_AUTOMATONPARSE_PROMELA_H
 
index 884933a..247d959 100644 (file)
@@ -12,6 +12,7 @@
 #include "../simix/smx_private.h"
 #include "xbt/fifo.h"
 #include "mc_private.h"
+#include "xbt/automaton/automaton_create.h"
 
 XBT_LOG_NEW_CATEGORY(mc, "All MC categories");
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_global, mc,
@@ -607,3 +608,7 @@ void MC_diff(void){
   }
 
 }
+
+xbt_automaton_t MC_create_automaton(const char *file){
+  return xbt_create_automaton(file);
+}
diff --git a/src/xbt/automaton/automaton.c b/src/xbt/automaton/automaton.c
new file mode 100644 (file)
index 0000000..dffad32
--- /dev/null
@@ -0,0 +1,366 @@
+/* automaton - representation of büchi automaton */
+
+/* Copyright (c) 2011. The SimGrid Team.
+ * All rights reserved.                                                     */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+#include "xbt/automaton.h"
+
+xbt_automaton_t xbt_automaton_new_automaton(){
+  xbt_automaton_t automaton = NULL;
+  automaton = xbt_new0(struct xbt_automaton, 1);
+  automaton->states = xbt_dynar_new(sizeof(xbt_state_t), NULL);
+  automaton->transitions = xbt_dynar_new(sizeof(xbt_transition_t), NULL);
+  automaton->propositional_symbols = xbt_dynar_new(sizeof(xbt_propositional_symbol_t), NULL);
+  return automaton;
+}
+
+xbt_state_t xbt_automaton_new_state(xbt_automaton_t a, int type, char* id){
+  xbt_state_t state = NULL;
+  state = xbt_new0(struct xbt_state, 1);
+  state->type = type;
+  state->id = strdup(id);
+  state->in = xbt_dynar_new(sizeof(xbt_transition_t), NULL);
+  state->out = xbt_dynar_new(sizeof(xbt_transition_t), NULL); 
+  xbt_dynar_push(a->states, &state);
+  return state;
+}
+
+xbt_transition_t xbt_automaton_new_transition(xbt_automaton_t a, xbt_state_t src, xbt_state_t dst, xbt_exp_label_t label){
+  xbt_transition_t transition = NULL;
+  transition = xbt_new0(struct xbt_transition, 1);
+  if(src != NULL){
+    xbt_dynar_push(src->out, &transition);
+    transition->src = src;
+  }
+  if(dst != NULL){
+    xbt_dynar_push(dst->in, &transition);
+    transition->dst = dst;
+  }
+  transition->label = label;
+  xbt_dynar_push(a->transitions, &transition);
+  return transition;
+}
+
+xbt_exp_label_t xbt_automaton_new_label(int type, ...){
+  xbt_exp_label_t label = NULL;
+  label = xbt_new0(struct xbt_exp_label, 1);
+  label->type = type;
+
+  va_list ap;
+  va_start(ap, type);
+  switch(type){
+  case 0 : {
+    xbt_exp_label_t left = va_arg(ap, xbt_exp_label_t);
+    xbt_exp_label_t right = va_arg(ap, xbt_exp_label_t);
+    label->u.or_and.left_exp = left;
+    label->u.or_and.right_exp = right;
+    break;
+  }
+  case 1 : {
+    xbt_exp_label_t left = va_arg(ap, xbt_exp_label_t);
+    xbt_exp_label_t right = va_arg(ap, xbt_exp_label_t);
+    label->u.or_and.left_exp = left;
+    label->u.or_and.right_exp = right;
+    break;
+  }
+  case 2 : {
+    xbt_exp_label_t exp_not = va_arg(ap, xbt_exp_label_t);
+    label->u.exp_not = exp_not;
+    break;
+  }
+  case 3 :{
+    char* p = va_arg(ap, char*);
+    label->u.predicat = strdup(p);
+    break;
+  }
+  }
+  va_end(ap);
+  return label;
+}
+
+
+xbt_dynar_t xbt_automaton_get_states(xbt_automaton_t a){
+  return a->states;
+}
+
+xbt_dynar_t xbt_automaton_get_transitions(xbt_automaton_t a){
+  return a->transitions;
+}
+
+xbt_transition_t xbt_automaton_get_transition(xbt_automaton_t a, xbt_state_t src, xbt_state_t dst){
+  xbt_transition_t transition;
+  unsigned int cursor;
+  xbt_dynar_foreach(src->out, cursor, transition){
+    if((transition->src == src) && (transition->dst == dst))
+      return transition;
+  }
+  return NULL;
+}
+
+void xbt_automaton_free_automaton(xbt_automaton_t a, void_f_pvoid_t transition_free_function){
+  unsigned int cursor = 0;
+  xbt_state_t state = NULL;
+  xbt_transition_t transition = NULL;
+
+  xbt_dynar_foreach(a->states, cursor, state){
+    xbt_dynar_free(&(state->out));
+    xbt_dynar_free(&(state->in));
+  }
+
+  xbt_dynar_foreach(a->transitions, cursor, transition){
+    if(transition_free_function) 
+      (*transition_free_function) (transition->label);
+  }
+
+  xbt_dynar_foreach(a->states, cursor, state)
+    free(state);
+  xbt_dynar_free(&(a->states));
+
+  xbt_dynar_foreach(a->transitions, cursor, state)
+    free(transition);
+  xbt_dynar_free(&(a->transitions));
+
+  free(a);
+
+  return;
+}
+
+void xbt_automaton_free_state(xbt_automaton_t a, xbt_state_t s, void_f_pvoid_t transition_free_function){
+  unsigned long nbr;
+  unsigned long i;
+  unsigned int cursor = 0;
+  xbt_state_t state = NULL;
+  xbt_transition_t transition = NULL;
+
+  nbr = xbt_dynar_length(a->transitions);
+  for(i = 0; i <nbr; i++){
+    xbt_dynar_get_cpy(a->transitions, cursor, &transition);
+    if((transition->src == s) || (transition->dst == s)){
+      xbt_automaton_free_transition(a, transition, transition_free_function);
+    }else{
+      cursor++;
+    }
+  }
+
+  cursor = 0;
+  xbt_dynar_foreach(a->states, cursor, state)
+    if(state == s)
+      xbt_dynar_cursor_rm(a->states, &cursor);
+
+  xbt_dynar_free(&(s->in));
+  xbt_dynar_free(&(s->out));
+
+  free(s);
+
+  return;
+}
+
+void xbt_automaton_free_transition(xbt_automaton_t a, xbt_transition_t t, void_f_pvoid_t transition_free_function){
+  int index;
+  unsigned int cursor = 0;
+  xbt_transition_t transition = NULL;
+
+  if((transition_free_function) && (t->label))
+    (*transition_free_function) (t->label);
+
+  xbt_dynar_foreach(a->transitions, cursor, transition) {
+    if(transition == t){
+      index = __xbt_find_in_dynar(transition->dst->in, transition);
+      xbt_dynar_remove_at(transition->dst->in, index, NULL);
+      index = __xbt_find_in_dynar(transition->src->out, transition);
+      xbt_dynar_remove_at(transition->src->out, index, NULL);
+      xbt_dynar_cursor_rm(a->transitions, & cursor);
+      free(transition);
+      break;
+    }  
+  }
+} 
+
+xbt_state_t xbt_automaton_transition_get_source(xbt_transition_t t){
+  return t->src;
+}
+
+xbt_state_t xbt_automaton_transition_get_destination(xbt_transition_t t){
+  return t->dst;
+}
+
+void xbt_automaton_transition_set_source(xbt_transition_t t, xbt_state_t src){
+  t->src = src;
+  xbt_dynar_push(src->out,&t);
+}
+
+void xbt_automaton_transition_set_destination(xbt_transition_t t, xbt_state_t dst){
+  t->dst = dst;
+  xbt_dynar_push(dst->in,&t);
+}
+
+xbt_dynar_t xbt_automaton_state_get_out_transitions(xbt_state_t s){
+  return s->out;
+}
+
+xbt_dynar_t xbt_automaton_state_get_in_transitions(xbt_state_t s){
+  return s->in;
+}
+
+xbt_state_t xbt_automaton_state_exists(xbt_automaton_t a, char *id){
+  xbt_state_t state = NULL;
+  unsigned int cursor = 0;
+  xbt_dynar_foreach(a->states, cursor, state){
+   if(strcmp(state->id, id)==0)
+     return state;
+  }
+  return NULL;
+}
+
+void  xbt_automaton_display(xbt_automaton_t a){
+  unsigned int cursor = 0;
+  xbt_state_t state = NULL;
+
+  printf("\n\nEtat courant : %s\n", a->current_state->id);
+
+  printf("\nListe des états : %lu\n\n", xbt_dynar_length(a->states));
+  
+  xbt_dynar_foreach(a->states, cursor, state){
+    printf("ID : %s, type : %d\n", state->id, state->type);
+  }
+
+  cursor=0;
+  xbt_transition_t transition = NULL;
+  printf("\nListe des transitions : %lu\n\n", xbt_dynar_length(a->transitions));
+  
+  xbt_dynar_foreach(a->transitions, cursor, transition){
+    printf("label :");
+    xbt_automaton_display_exp(transition->label);
+    printf(", %s -> %s\n", transition->src->id, transition->dst->id);
+  }
+}
+
+void xbt_automaton_display_exp(xbt_exp_label_t label){
+
+  switch(label->type){
+  case 0 :
+    printf("(");
+    xbt_automaton_display_exp(label->u.or_and.left_exp);
+    printf(" || ");
+    xbt_automaton_display_exp(label->u.or_and.right_exp);
+    printf(")");
+    break;
+  case 1 : 
+    printf("(");
+    xbt_automaton_display_exp(label->u.or_and.left_exp);
+    printf(" && ");
+    xbt_automaton_display_exp(label->u.or_and.right_exp);
+    printf(")");
+    break;
+  case 2 : 
+    printf("(!");
+    xbt_automaton_display_exp(label->u.exp_not);
+    printf(")");
+    break;
+  case 3 :
+    printf("(%s)",label->u.predicat);
+    break;
+  case 4 :
+    printf("(1)");
+    break;
+  }
+
+}
+
+xbt_state_t xbt_automaton_get_current_state(xbt_automaton_t a){
+  return a->current_state;
+}
+
+xbt_propositional_symbol_t xbt_new_propositional_symbol(xbt_automaton_t a, const char* id, void* fct){
+  xbt_propositional_symbol_t prop_symb = NULL;
+  prop_symb = xbt_new0(struct xbt_propositional_symbol, 1);
+  prop_symb->pred = strdup(id);
+  prop_symb->function = fct;
+  xbt_dynar_push(a->propositional_symbols, &prop_symb);
+  return prop_symb;
+}
+
+int automaton_state_compare(xbt_state_t s1, xbt_state_t s2){
+
+  /* single id for each state, id and type sufficient for comparison*/
+
+  if(strcmp(s1->id, s2->id))
+    return 1;
+
+  if(s1->type != s2->type)
+    return 1;
+
+  return 0;
+
+}
+
+int automaton_transition_compare(const void *t1, const void *t2){
+
+  if(automaton_state_compare(((xbt_transition_t)t1)->src, ((xbt_transition_t)t2)->src))
+    return 1;
+  
+  if(automaton_state_compare(((xbt_transition_t)t1)->dst, ((xbt_transition_t)t2)->dst))
+    return 1;
+
+  if(automaton_label_transition_compare(((xbt_transition_t)t1)->label,((xbt_transition_t)t2)->label))
+    return 1;
+
+  return 0;
+  
+}
+
+int automaton_label_transition_compare(xbt_exp_label_t l1, xbt_exp_label_t l2){
+
+  if(l1->type != l2->type)
+    return 1;
+
+  switch(l1->type){
+
+  case 0 : // OR 
+  case 1 : // AND
+    if(automaton_label_transition_compare(l1->u.or_and.left_exp, l2->u.or_and.left_exp))
+      return 1;
+    else
+      return automaton_label_transition_compare(l1->u.or_and.right_exp, l2->u.or_and.right_exp);
+    break;
+
+  case 2 : // NOT
+    return automaton_label_transition_compare(l1->u.exp_not, l2->u.exp_not);
+    break;
+
+  case 3 : // predicat
+    return (strcmp(l1->u.predicat, l2->u.predicat));
+    break;
+
+  case 4 : // 1
+    return 0;
+    break;
+
+  default :
+    return -1;
+    break;
+
+  }
+
+}
+
+
+int propositional_symbols_compare_value(xbt_dynar_t s1, xbt_dynar_t s2){
+
+  int *iptr1, *iptr2;
+  unsigned int cursor;
+  unsigned int nb_elem = xbt_dynar_length(s1);
+
+  for(cursor=0;cursor<nb_elem;cursor++){
+    iptr1 = xbt_dynar_get_ptr(s1, cursor);
+    iptr2 = xbt_dynar_get_ptr(s2, cursor);
+    if(*iptr1 != *iptr2)
+      return 1;
+  } 
+
+  return 0;
+}
diff --git a/src/xbt/automaton/automaton_create.c b/src/xbt/automaton/automaton_create.c
new file mode 100644 (file)
index 0000000..0b2ed30
--- /dev/null
@@ -0,0 +1,12 @@
+#include "xbt/automatonparse_promela.h"
+#include "y.tab.c"
+#include "automaton_create.h"
+
+xbt_automaton_t xbt_create_automaton(const char *file){
+
+  init();
+  yyin = fopen(file, "r");
+  yyparse();
+  return automaton;
+
+}
diff --git a/src/xbt/automaton/automaton_create.h b/src/xbt/automaton/automaton_create.h
new file mode 100644 (file)
index 0000000..24d0ebe
--- /dev/null
@@ -0,0 +1,14 @@
+/*  xbt/automaton/automaton_create.h -- büchi automaton                                      */
+
+/* Copyright (c) 2011. The SimGrid Team.
+ * All rights reserved.                                                     */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+#ifndef _AUTOMATON_CREATE_H
+#define _AUTOMATON_CREATE_H
+
+xbt_automaton_t xbt_create_automaton(const char *file);
+
+#endif
diff --git a/src/xbt/automaton/automaton_parse.yy.c b/src/xbt/automaton/automaton_parse.yy.c
new file mode 100644 (file)
index 0000000..a7395b1
--- /dev/null
@@ -0,0 +1,1947 @@
+#line 2 "automaton_parse.yy.c"
+
+#line 4 "automaton_parse.yy.c"
+
+#define  YY_INT_ALIGNED short int
+
+/* A lexical scanner generated by flex */
+
+#define yy_create_buffer xbt_automaton_parse__create_buffer
+#define yy_delete_buffer xbt_automaton_parse__delete_buffer
+#define yy_flex_debug xbt_automaton_parse__flex_debug
+#define yy_init_buffer xbt_automaton_parse__init_buffer
+#define yy_flush_buffer xbt_automaton_parse__flush_buffer
+#define yy_load_buffer_state xbt_automaton_parse__load_buffer_state
+#define yy_switch_to_buffer xbt_automaton_parse__switch_to_buffer
+#define yyin xbt_automaton_parse_in
+#define yyleng xbt_automaton_parse_leng
+#define yylex xbt_automaton_parse_lex
+#define yylineno xbt_automaton_parse_lineno
+#define yyout xbt_automaton_parse_out
+#define yyrestart xbt_automaton_parse_restart
+#define yytext xbt_automaton_parse_text
+#define yywrap xbt_automaton_parse_wrap
+#define yyalloc xbt_automaton_parse_alloc
+#define yyrealloc xbt_automaton_parse_realloc
+#define yyfree xbt_automaton_parse_free
+
+#define FLEX_SCANNER
+#define YY_FLEX_MAJOR_VERSION 2
+#define YY_FLEX_MINOR_VERSION 5
+#define YY_FLEX_SUBMINOR_VERSION 35
+#if YY_FLEX_SUBMINOR_VERSION > 0
+#define FLEX_BETA
+#endif
+
+/* First, we deal with  platform-specific or compiler-specific issues. */
+
+/* begin standard C headers. */
+#include <stdio.h>
+#include <string.h>
+#include <errno.h>
+#include <stdlib.h>
+
+/* end standard C headers. */
+
+/* flex integer type definitions */
+
+#ifndef FLEXINT_H
+#define FLEXINT_H
+
+/* C99 systems have <inttypes.h>. Non-C99 systems may or may not. */
+
+#if defined (__STDC_VERSION__) && __STDC_VERSION__ >= 199901L
+
+/* C99 says to define __STDC_LIMIT_MACROS before including stdint.h,
+ * if you want the limit (max/min) macros for int types. 
+ */
+#ifndef __STDC_LIMIT_MACROS
+#define __STDC_LIMIT_MACROS 1
+#endif
+
+#include <inttypes.h>
+typedef int8_t flex_int8_t;
+typedef uint8_t flex_uint8_t;
+typedef int16_t flex_int16_t;
+typedef uint16_t flex_uint16_t;
+typedef int32_t flex_int32_t;
+typedef uint32_t flex_uint32_t;
+#else
+typedef signed char flex_int8_t;
+typedef short int flex_int16_t;
+typedef int flex_int32_t;
+typedef unsigned char flex_uint8_t; 
+typedef unsigned short int flex_uint16_t;
+typedef unsigned int flex_uint32_t;
+
+/* Limits of integral types. */
+#ifndef INT8_MIN
+#define INT8_MIN               (-128)
+#endif
+#ifndef INT16_MIN
+#define INT16_MIN              (-32767-1)
+#endif
+#ifndef INT32_MIN
+#define INT32_MIN              (-2147483647-1)
+#endif
+#ifndef INT8_MAX
+#define INT8_MAX               (127)
+#endif
+#ifndef INT16_MAX
+#define INT16_MAX              (32767)
+#endif
+#ifndef INT32_MAX
+#define INT32_MAX              (2147483647)
+#endif
+#ifndef UINT8_MAX
+#define UINT8_MAX              (255U)
+#endif
+#ifndef UINT16_MAX
+#define UINT16_MAX             (65535U)
+#endif
+#ifndef UINT32_MAX
+#define UINT32_MAX             (4294967295U)
+#endif
+
+#endif /* ! C99 */
+
+#endif /* ! FLEXINT_H */
+
+#ifdef __cplusplus
+
+/* The "const" storage-class-modifier is valid. */
+#define YY_USE_CONST
+
+#else  /* ! __cplusplus */
+
+/* C99 requires __STDC__ to be defined as 1. */
+#if defined (__STDC__)
+
+#define YY_USE_CONST
+
+#endif /* defined (__STDC__) */
+#endif /* ! __cplusplus */
+
+#ifdef YY_USE_CONST
+#define yyconst const
+#else
+#define yyconst
+#endif
+
+/* Returned upon end-of-file. */
+#define YY_NULL 0
+
+/* Promotes a possibly negative, possibly signed char to an unsigned
+ * integer for use as an array index.  If the signed char is negative,
+ * we want to instead treat it as an 8-bit unsigned char, hence the
+ * double cast.
+ */
+#define YY_SC_TO_UI(c) ((unsigned int) (unsigned char) c)
+
+/* Enter a start condition.  This macro really ought to take a parameter,
+ * but we do it the disgusting crufty way forced on us by the ()-less
+ * definition of BEGIN.
+ */
+#define BEGIN (yy_start) = 1 + 2 *
+
+/* Translate the current start state into a value that can be later handed
+ * to BEGIN to return to the state.  The YYSTATE alias is for lex
+ * compatibility.
+ */
+#define YY_START (((yy_start) - 1) / 2)
+#define YYSTATE YY_START
+
+/* Action number for EOF rule of a given start state. */
+#define YY_STATE_EOF(state) (YY_END_OF_BUFFER + state + 1)
+
+/* Special action meaning "start processing a new file". */
+#define YY_NEW_FILE xbt_automaton_parse_restart(xbt_automaton_parse_in  )
+
+#define YY_END_OF_BUFFER_CHAR 0
+
+/* Size of default input buffer. */
+#ifndef YY_BUF_SIZE
+#ifdef __ia64__
+/* On IA-64, the buffer size is 16k, not 8k.
+ * Moreover, YY_BUF_SIZE is 2*YY_READ_BUF_SIZE in the general case.
+ * Ditto for the __ia64__ case accordingly.
+ */
+#define YY_BUF_SIZE 32768
+#else
+#define YY_BUF_SIZE 16384
+#endif /* __ia64__ */
+#endif
+
+/* The state buf must be large enough to hold one state per character in the main buffer.
+ */
+#define YY_STATE_BUF_SIZE   ((YY_BUF_SIZE + 2) * sizeof(yy_state_type))
+
+#ifndef YY_TYPEDEF_YY_BUFFER_STATE
+#define YY_TYPEDEF_YY_BUFFER_STATE
+typedef struct yy_buffer_state *YY_BUFFER_STATE;
+#endif
+
+extern int xbt_automaton_parse_leng;
+
+extern FILE *xbt_automaton_parse_in, *xbt_automaton_parse_out;
+
+#define EOB_ACT_CONTINUE_SCAN 0
+#define EOB_ACT_END_OF_FILE 1
+#define EOB_ACT_LAST_MATCH 2
+
+    #define YY_LESS_LINENO(n)
+    
+/* Return all but the first "n" matched characters back to the input stream. */
+#define yyless(n) \
+       do \
+               { \
+               /* Undo effects of setting up xbt_automaton_parse_text. */ \
+        int yyless_macro_arg = (n); \
+        YY_LESS_LINENO(yyless_macro_arg);\
+               *yy_cp = (yy_hold_char); \
+               YY_RESTORE_YY_MORE_OFFSET \
+               (yy_c_buf_p) = yy_cp = yy_bp + yyless_macro_arg - YY_MORE_ADJ; \
+               YY_DO_BEFORE_ACTION; /* set up xbt_automaton_parse_text again */ \
+               } \
+       while ( 0 )
+
+#define unput(c) yyunput( c, (yytext_ptr)  )
+
+#ifndef YY_TYPEDEF_YY_SIZE_T
+#define YY_TYPEDEF_YY_SIZE_T
+typedef size_t yy_size_t;
+#endif
+
+#ifndef YY_STRUCT_YY_BUFFER_STATE
+#define YY_STRUCT_YY_BUFFER_STATE
+struct yy_buffer_state
+       {
+       FILE *yy_input_file;
+
+       char *yy_ch_buf;                /* input buffer */
+       char *yy_buf_pos;               /* current position in input buffer */
+
+       /* Size of input buffer in bytes, not including room for EOB
+        * characters.
+        */
+       yy_size_t yy_buf_size;
+
+       /* Number of characters read into yy_ch_buf, not including EOB
+        * characters.
+        */
+       int yy_n_chars;
+
+       /* Whether we "own" the buffer - i.e., we know we created it,
+        * and can realloc() it to grow it, and should free() it to
+        * delete it.
+        */
+       int yy_is_our_buffer;
+
+       /* Whether this is an "interactive" input source; if so, and
+        * if we're using stdio for input, then we want to use getc()
+        * instead of fread(), to make sure we stop fetching input after
+        * each newline.
+        */
+       int yy_is_interactive;
+
+       /* Whether we're considered to be at the beginning of a line.
+        * If so, '^' rules will be active on the next match, otherwise
+        * not.
+        */
+       int yy_at_bol;
+
+    int yy_bs_lineno; /**< The line count. */
+    int yy_bs_column; /**< The column count. */
+    
+       /* Whether to try to fill the input buffer when we reach the
+        * end of it.
+        */
+       int yy_fill_buffer;
+
+       int yy_buffer_status;
+
+#define YY_BUFFER_NEW 0
+#define YY_BUFFER_NORMAL 1
+       /* When an EOF's been seen but there's still some text to process
+        * then we mark the buffer as YY_EOF_PENDING, to indicate that we
+        * shouldn't try reading from the input source any more.  We might
+        * still have a bunch of tokens to match, though, because of
+        * possible backing-up.
+        *
+        * When we actually see the EOF, we change the status to "new"
+        * (via xbt_automaton_parse_restart()), so that the user can continue scanning by
+        * just pointing xbt_automaton_parse_in at a new input file.
+        */
+#define YY_BUFFER_EOF_PENDING 2
+
+       };
+#endif /* !YY_STRUCT_YY_BUFFER_STATE */
+
+/* Stack of input buffers. */
+static size_t yy_buffer_stack_top = 0; /**< index of top of stack. */
+static size_t yy_buffer_stack_max = 0; /**< capacity of stack. */
+static YY_BUFFER_STATE * yy_buffer_stack = 0; /**< Stack as an array. */
+
+/* We provide macros for accessing buffer states in case in the
+ * future we want to put the buffer states in a more general
+ * "scanner state".
+ *
+ * Returns the top of the stack, or NULL.
+ */
+#define YY_CURRENT_BUFFER ( (yy_buffer_stack) \
+                          ? (yy_buffer_stack)[(yy_buffer_stack_top)] \
+                          : NULL)
+
+/* Same as previous macro, but useful when we know that the buffer stack is not
+ * NULL or when we need an lvalue. For internal use only.
+ */
+#define YY_CURRENT_BUFFER_LVALUE (yy_buffer_stack)[(yy_buffer_stack_top)]
+
+/* yy_hold_char holds the character lost when xbt_automaton_parse_text is formed. */
+static char yy_hold_char;
+static int yy_n_chars;         /* number of characters read into yy_ch_buf */
+int xbt_automaton_parse_leng;
+
+/* Points to current character in buffer. */
+static char *yy_c_buf_p = (char *) 0;
+static int yy_init = 0;                /* whether we need to initialize */
+static int yy_start = 0;       /* start state number */
+
+/* Flag which is used to allow xbt_automaton_parse_wrap()'s to do buffer switches
+ * instead of setting up a fresh xbt_automaton_parse_in.  A bit of a hack ...
+ */
+static int yy_did_buffer_switch_on_eof;
+
+void xbt_automaton_parse_restart (FILE *input_file  );
+void xbt_automaton_parse__switch_to_buffer (YY_BUFFER_STATE new_buffer  );
+YY_BUFFER_STATE xbt_automaton_parse__create_buffer (FILE *file,int size  );
+void xbt_automaton_parse__delete_buffer (YY_BUFFER_STATE b  );
+void xbt_automaton_parse__flush_buffer (YY_BUFFER_STATE b  );
+void xbt_automaton_parse_push_buffer_state (YY_BUFFER_STATE new_buffer  );
+void xbt_automaton_parse_pop_buffer_state (void );
+
+static void xbt_automaton_parse_ensure_buffer_stack (void );
+static void xbt_automaton_parse__load_buffer_state (void );
+static void xbt_automaton_parse__init_buffer (YY_BUFFER_STATE b,FILE *file  );
+
+#define YY_FLUSH_BUFFER xbt_automaton_parse__flush_buffer(YY_CURRENT_BUFFER )
+
+YY_BUFFER_STATE xbt_automaton_parse__scan_buffer (char *base,yy_size_t size  );
+YY_BUFFER_STATE xbt_automaton_parse__scan_string (yyconst char *yy_str  );
+YY_BUFFER_STATE xbt_automaton_parse__scan_bytes (yyconst char *bytes,int len  );
+
+void *xbt_automaton_parse_alloc (yy_size_t  );
+void *xbt_automaton_parse_realloc (void *,yy_size_t  );
+void xbt_automaton_parse_free (void *  );
+
+#define yy_new_buffer xbt_automaton_parse__create_buffer
+
+#define yy_set_interactive(is_interactive) \
+       { \
+       if ( ! YY_CURRENT_BUFFER ){ \
+        xbt_automaton_parse_ensure_buffer_stack (); \
+               YY_CURRENT_BUFFER_LVALUE =    \
+            xbt_automaton_parse__create_buffer(xbt_automaton_parse_in,YY_BUF_SIZE ); \
+       } \
+       YY_CURRENT_BUFFER_LVALUE->yy_is_interactive = is_interactive; \
+       }
+
+#define yy_set_bol(at_bol) \
+       { \
+       if ( ! YY_CURRENT_BUFFER ){\
+        xbt_automaton_parse_ensure_buffer_stack (); \
+               YY_CURRENT_BUFFER_LVALUE =    \
+            xbt_automaton_parse__create_buffer(xbt_automaton_parse_in,YY_BUF_SIZE ); \
+       } \
+       YY_CURRENT_BUFFER_LVALUE->yy_at_bol = at_bol; \
+       }
+
+#define YY_AT_BOL() (YY_CURRENT_BUFFER_LVALUE->yy_at_bol)
+
+/* Begin user sect3 */
+
+#define xbt_automaton_parse_wrap(n) 1
+#define YY_SKIP_YYWRAP
+
+typedef unsigned char YY_CHAR;
+
+FILE *xbt_automaton_parse_in = (FILE *) 0, *xbt_automaton_parse_out = (FILE *) 0;
+
+typedef int yy_state_type;
+
+extern int xbt_automaton_parse_lineno;
+
+int xbt_automaton_parse_lineno = 1;
+
+extern char *xbt_automaton_parse_text;
+#define yytext_ptr xbt_automaton_parse_text
+
+static yy_state_type yy_get_previous_state (void );
+static yy_state_type yy_try_NUL_trans (yy_state_type current_state  );
+static int yy_get_next_buffer (void );
+static void yy_fatal_error (yyconst char msg[]  );
+
+/* Done after the current pattern has been matched and before the
+ * corresponding action - sets up xbt_automaton_parse_text.
+ */
+#define YY_DO_BEFORE_ACTION \
+       (yytext_ptr) = yy_bp; \
+       xbt_automaton_parse_leng = (size_t) (yy_cp - yy_bp); \
+       (yy_hold_char) = *yy_cp; \
+       *yy_cp = '\0'; \
+       (yy_c_buf_p) = yy_cp;
+
+#define YY_NUM_RULES 25
+#define YY_END_OF_BUFFER 26
+/* This struct is not used in this scanner,
+   but its presence is necessary. */
+struct yy_trans_info
+       {
+       flex_int32_t yy_verify;
+       flex_int32_t yy_nxt;
+       };
+static yyconst flex_int16_t yy_accept[54] =
+    {   0,
+        0,    0,   26,   24,   18,   23,    8,   24,   24,    9,
+       10,   24,   24,   20,   14,   12,   13,   22,   22,   22,
+       22,   22,   15,   24,   16,   18,    0,    0,   21,    0,
+        6,    4,    0,    0,   20,   11,   22,    3,   22,    2,
+       22,    7,    0,    0,    0,   19,   22,   22,   17,    5,
+       22,    1,    0
+    } ;
+
+static yyconst flex_int32_t yy_ec[256] =
+    {   0,
+        1,    1,    1,    1,    1,    1,    1,    1,    2,    3,
+        1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
+        1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
+        1,    4,    5,    6,    1,    1,    1,    7,    1,    8,
+        9,   10,    1,    1,   11,   12,   13,   14,   15,   14,
+       14,   14,   14,   14,   14,   14,   14,   16,   17,    1,
+        1,   18,    1,    1,   19,   19,   19,   19,   19,   19,
+       19,   19,   19,   19,   19,   19,   19,   19,   19,   19,
+       19,   19,   19,   19,   19,   19,   19,   19,   19,   19,
+        1,   20,    1,    1,   21,    1,   19,   19,   19,   19,
+
+       22,   23,   24,   19,   25,   19,   19,   19,   19,   26,
+       27,   19,   19,   28,   19,   29,   19,   30,   19,   19,
+       19,   19,   31,   32,   33,    1,    1,    1,    1,    1,
+        1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
+        1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
+        1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
+        1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
+        1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
+        1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
+        1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
+
+        1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
+        1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
+        1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
+        1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
+        1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
+        1,    1,    1,    1,    1
+    } ;
+
+static yyconst flex_int32_t yy_meta[34] =
+    {   0,
+        1,    1,    2,    2,    1,    2,    1,    1,    1,    1,
+        1,    1,    3,    4,    4,    1,    1,    1,    4,    2,
+        4,    4,    4,    4,    4,    4,    4,    4,    4,    4,
+        1,    1,    1
+    } ;
+
+static yyconst flex_int16_t yy_base[57] =
+    {   0,
+        0,    0,   89,   90,   32,   90,   90,   34,   81,   90,
+       90,   69,   76,   27,   31,   69,   90,    0,   59,   56,
+       58,   55,   90,   42,   90,   45,   47,    0,    0,    0,
+       90,   90,   52,   43,   49,   90,    0,    0,   44,    0,
+       42,   90,   56,   65,   52,   56,   25,   26,   90,    0,
+       16,    0,   90,   74,   31,   78
+    } ;
+
+static yyconst flex_int16_t yy_def[57] =
+    {   0,
+       53,    1,   53,   53,   53,   53,   53,   54,   53,   53,
+       53,   53,   53,   53,   53,   53,   53,   55,   55,   55,
+       55,   55,   53,   53,   53,   53,   54,   27,   27,   27,
+       53,   53,   56,   53,   53,   53,   55,   55,   55,   55,
+       55,   53,   56,   56,   53,   53,   55,   55,   53,   55,
+       55,   55,    0,   53,   53,   53
+    } ;
+
+static yyconst flex_int16_t yy_nxt[124] =
+    {   0,
+        4,    5,    6,    5,    7,    8,    9,   10,   11,    4,
+       12,    4,   13,   14,   15,   16,   17,    4,   18,    4,
+        4,   18,   19,   20,   21,   22,   18,   18,   18,   18,
+       23,   24,   25,   26,   37,   26,   27,   28,   34,   29,
+       35,   35,   34,   52,   35,   35,   26,   51,   26,   27,
+       28,   50,   29,   27,   44,   44,   46,   46,   44,   44,
+       34,   45,   35,   35,   49,   45,   27,   44,   44,   46,
+       46,   48,   47,   42,   45,   30,   41,   30,   43,   43,
+       40,   43,   39,   38,   36,   33,   32,   31,   53,    3,
+       53,   53,   53,   53,   53,   53,   53,   53,   53,   53,
+
+       53,   53,   53,   53,   53,   53,   53,   53,   53,   53,
+       53,   53,   53,   53,   53,   53,   53,   53,   53,   53,
+       53,   53,   53
+    } ;
+
+static yyconst flex_int16_t yy_chk[124] =
+    {   0,
+        1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
+        1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
+        1,    1,    1,    1,    1,    1,    1,    1,    1,    1,
+        1,    1,    1,    5,   55,    5,    8,    8,   14,    8,
+       14,   14,   15,   51,   15,   15,   26,   48,   26,   27,
+       27,   47,   27,    8,   33,   33,   34,   34,   43,   43,
+       35,   33,   35,   35,   45,   43,   27,   44,   44,   46,
+       46,   41,   39,   24,   44,   54,   22,   54,   56,   56,
+       21,   56,   20,   19,   16,   13,   12,    9,    3,   53,
+       53,   53,   53,   53,   53,   53,   53,   53,   53,   53,
+
+       53,   53,   53,   53,   53,   53,   53,   53,   53,   53,
+       53,   53,   53,   53,   53,   53,   53,   53,   53,   53,
+       53,   53,   53
+    } ;
+
+static yy_state_type yy_last_accepting_state;
+static char *yy_last_accepting_cpos;
+
+extern int xbt_automaton_parse__flex_debug;
+int xbt_automaton_parse__flex_debug = 0;
+
+/* The intent behind this definition is that it'll catch
+ * any uses of REJECT which flex missed.
+ */
+#define REJECT reject_used_but_not_detected
+#define yymore() yymore_used_but_not_detected
+#define YY_MORE_ADJ 0
+#define YY_RESTORE_YY_MORE_OFFSET
+char *xbt_automaton_parse_text;
+#line 1 "parserPromela.lex"
+#line 4 "parserPromela.lex"
+
+
+#include <stdio.h>
+#include "y.tab.h"
+  
+  extern YYSTYPE yylval;
+#line 533 "automaton_parse.yy.c"
+
+#define INITIAL 0
+
+#ifndef YY_NO_UNISTD_H
+/* Special case for "unistd.h", since it is non-ANSI. We include it way
+ * down here because we want the user's section 1 to have been scanned first.
+ * The user has a chance to override it with an option.
+ */
+#include <unistd.h>
+#endif
+
+#ifndef YY_EXTRA_TYPE
+#define YY_EXTRA_TYPE void *
+#endif
+
+static int yy_init_globals (void );
+
+/* Accessor methods to globals.
+   These are made visible to non-reentrant scanners for convenience. */
+
+int xbt_automaton_parse_lex_destroy (void );
+
+int xbt_automaton_parse_get_debug (void );
+
+void xbt_automaton_parse_set_debug (int debug_flag  );
+
+YY_EXTRA_TYPE xbt_automaton_parse_get_extra (void );
+
+void xbt_automaton_parse_set_extra (YY_EXTRA_TYPE user_defined  );
+
+FILE *xbt_automaton_parse_get_in (void );
+
+void xbt_automaton_parse_set_in  (FILE * in_str  );
+
+FILE *xbt_automaton_parse_get_out (void );
+
+void xbt_automaton_parse_set_out  (FILE * out_str  );
+
+int xbt_automaton_parse_get_leng (void );
+
+char *xbt_automaton_parse_get_text (void );
+
+int xbt_automaton_parse_get_lineno (void );
+
+void xbt_automaton_parse_set_lineno (int line_number  );
+
+/* Macros after this point can all be overridden by user definitions in
+ * section 1.
+ */
+
+#ifndef YY_SKIP_YYWRAP
+#ifdef __cplusplus
+extern "C" int xbt_automaton_parse_wrap (void );
+#else
+extern int xbt_automaton_parse_wrap (void );
+#endif
+#endif
+
+    static void yyunput (int c,char *buf_ptr  );
+    
+#ifndef yytext_ptr
+static void yy_flex_strncpy (char *,yyconst char *,int );
+#endif
+
+#ifdef YY_NEED_STRLEN
+static int yy_flex_strlen (yyconst char * );
+#endif
+
+#ifndef YY_NO_INPUT
+
+#ifdef __cplusplus
+static int yyinput (void );
+#else
+static int input (void );
+#endif
+
+#endif
+
+/* Amount of stuff to slurp up with each read. */
+#ifndef YY_READ_BUF_SIZE
+#ifdef __ia64__
+/* On IA-64, the buffer size is 16k, not 8k */
+#define YY_READ_BUF_SIZE 16384
+#else
+#define YY_READ_BUF_SIZE 8192
+#endif /* __ia64__ */
+#endif
+
+/* Copy whatever the last rule matched to the standard output. */
+#ifndef ECHO
+/* This used to be an fputs(), but since the string might contain NUL's,
+ * we now use fwrite().
+ */
+#define ECHO do { if (fwrite( xbt_automaton_parse_text, xbt_automaton_parse_leng, 1, xbt_automaton_parse_out )) {} } while (0)
+#endif
+
+/* Gets input and stuffs it into "buf".  number of characters read, or YY_NULL,
+ * is returned in "result".
+ */
+#ifndef YY_INPUT
+#define YY_INPUT(buf,result,max_size) \
+       if ( YY_CURRENT_BUFFER_LVALUE->yy_is_interactive ) \
+               { \
+               int c = '*'; \
+               size_t n; \
+               for ( n = 0; n < max_size && \
+                            (c = getc( xbt_automaton_parse_in )) != EOF && c != '\n'; ++n ) \
+                       buf[n] = (char) c; \
+               if ( c == '\n' ) \
+                       buf[n++] = (char) c; \
+               if ( c == EOF && ferror( xbt_automaton_parse_in ) ) \
+                       YY_FATAL_ERROR( "input in flex scanner failed" ); \
+               result = n; \
+               } \
+       else \
+               { \
+               errno=0; \
+               while ( (result = fread(buf, 1, max_size, xbt_automaton_parse_in))==0 && ferror(xbt_automaton_parse_in)) \
+                       { \
+                       if( errno != EINTR) \
+                               { \
+                               YY_FATAL_ERROR( "input in flex scanner failed" ); \
+                               break; \
+                               } \
+                       errno=0; \
+                       clearerr(xbt_automaton_parse_in); \
+                       } \
+               }\
+\
+
+#endif
+
+/* No semi-colon after return; correct usage is to write "yyterminate();" -
+ * we don't want an extra ';' after the "return" because that will cause
+ * some compilers to complain about unreachable statements.
+ */
+#ifndef yyterminate
+#define yyterminate() return YY_NULL
+#endif
+
+/* Number of entries by which start-condition stack grows. */
+#ifndef YY_START_STACK_INCR
+#define YY_START_STACK_INCR 25
+#endif
+
+/* Report a fatal error. */
+#ifndef YY_FATAL_ERROR
+#define YY_FATAL_ERROR(msg) yy_fatal_error( msg )
+#endif
+
+/* end tables serialization structures and prototypes */
+
+/* Default declaration of generated scanner - a define so the user can
+ * easily add parameters.
+ */
+#ifndef YY_DECL
+#define YY_DECL_IS_OURS 1
+
+extern int xbt_automaton_parse_lex (void);
+
+#define YY_DECL int xbt_automaton_parse_lex (void)
+#endif /* !YY_DECL */
+
+/* Code executed at the beginning of each rule, after xbt_automaton_parse_text and xbt_automaton_parse_leng
+ * have been set up.
+ */
+#ifndef YY_USER_ACTION
+#define YY_USER_ACTION
+#endif
+
+/* Code executed at the end of each rule. */
+#ifndef YY_BREAK
+#define YY_BREAK break;
+#endif
+
+#define YY_RULE_SETUP \
+       YY_USER_ACTION
+
+/** The main scanner function which does all the work.
+ */
+YY_DECL
+{
+       register yy_state_type yy_current_state;
+       register char *yy_cp, *yy_bp;
+       register int yy_act;
+    
+#line 28 "parserPromela.lex"
+
+
+#line 723 "automaton_parse.yy.c"
+
+       if ( !(yy_init) )
+               {
+               (yy_init) = 1;
+
+#ifdef YY_USER_INIT
+               YY_USER_INIT;
+#endif
+
+               if ( ! (yy_start) )
+                       (yy_start) = 1; /* first start state */
+
+               if ( ! xbt_automaton_parse_in )
+                       xbt_automaton_parse_in = stdin;
+
+               if ( ! xbt_automaton_parse_out )
+                       xbt_automaton_parse_out = stdout;
+
+               if ( ! YY_CURRENT_BUFFER ) {
+                       xbt_automaton_parse_ensure_buffer_stack ();
+                       YY_CURRENT_BUFFER_LVALUE =
+                               xbt_automaton_parse__create_buffer(xbt_automaton_parse_in,YY_BUF_SIZE );
+               }
+
+               xbt_automaton_parse__load_buffer_state( );
+               }
+
+       while ( 1 )             /* loops until end-of-file is reached */
+               {
+               yy_cp = (yy_c_buf_p);
+
+               /* Support of xbt_automaton_parse_text. */
+               *yy_cp = (yy_hold_char);
+
+               /* yy_bp points to the position in yy_ch_buf of the start of
+                * the current run.
+                */
+               yy_bp = yy_cp;
+
+               yy_current_state = (yy_start);
+yy_match:
+               do
+                       {
+                       register YY_CHAR yy_c = yy_ec[YY_SC_TO_UI(*yy_cp)];
+                       if ( yy_accept[yy_current_state] )
+                               {
+                               (yy_last_accepting_state) = yy_current_state;
+                               (yy_last_accepting_cpos) = yy_cp;
+                               }
+                       while ( yy_chk[yy_base[yy_current_state] + yy_c] != yy_current_state )
+                               {
+                               yy_current_state = (int) yy_def[yy_current_state];
+                               if ( yy_current_state >= 54 )
+                                       yy_c = yy_meta[(unsigned int) yy_c];
+                               }
+                       yy_current_state = yy_nxt[yy_base[yy_current_state] + (unsigned int) yy_c];
+                       ++yy_cp;
+                       }
+               while ( yy_base[yy_current_state] != 90 );
+
+yy_find_action:
+               yy_act = yy_accept[yy_current_state];
+               if ( yy_act == 0 )
+                       { /* have to back up */
+                       yy_cp = (yy_last_accepting_cpos);
+                       yy_current_state = (yy_last_accepting_state);
+                       yy_act = yy_accept[yy_current_state];
+                       }
+
+               YY_DO_BEFORE_ACTION;
+
+do_action:     /* This label is used only to access EOF actions. */
+
+               switch ( yy_act )
+       { /* beginning of action switch */
+                       case 0: /* must back up */
+                       /* undo the effects of YY_DO_BEFORE_ACTION */
+                       *yy_cp = (yy_hold_char);
+                       yy_cp = (yy_last_accepting_cpos);
+                       yy_current_state = (yy_last_accepting_state);
+                       goto yy_find_action;
+
+case 1:
+YY_RULE_SETUP
+#line 30 "parserPromela.lex"
+{ printf("%s", xbt_automaton_parse_text); return (NEVER); }
+       YY_BREAK
+case 2:
+YY_RULE_SETUP
+#line 31 "parserPromela.lex"
+{ printf("%s", xbt_automaton_parse_text); return (IF); }
+       YY_BREAK
+case 3:
+YY_RULE_SETUP
+#line 32 "parserPromela.lex"
+{ printf("%s", xbt_automaton_parse_text); 
+               return (FI); }
+       YY_BREAK
+case 4:
+YY_RULE_SETUP
+#line 34 "parserPromela.lex"
+{ printf("%s", xbt_automaton_parse_text); return (IMPLIES); }
+       YY_BREAK
+case 5:
+YY_RULE_SETUP
+#line 35 "parserPromela.lex"
+{ printf("%s", xbt_automaton_parse_text); return (GOTO); }
+       YY_BREAK
+case 6:
+YY_RULE_SETUP
+#line 36 "parserPromela.lex"
+{ printf("%s", xbt_automaton_parse_text); return (AND); }
+       YY_BREAK
+case 7:
+YY_RULE_SETUP
+#line 37 "parserPromela.lex"
+{ printf("%s", xbt_automaton_parse_text); return (OR); }
+       YY_BREAK
+case 8:
+YY_RULE_SETUP
+#line 38 "parserPromela.lex"
+{ printf("%s", xbt_automaton_parse_text); return (NOT); }
+       YY_BREAK
+case 9:
+YY_RULE_SETUP
+#line 39 "parserPromela.lex"
+{ printf("%s", xbt_automaton_parse_text); return (LEFT_PAR); }
+       YY_BREAK
+case 10:
+YY_RULE_SETUP
+#line 40 "parserPromela.lex"
+{ printf("%s", xbt_automaton_parse_text); return (RIGHT_PAR); }
+       YY_BREAK
+case 11:
+YY_RULE_SETUP
+#line 41 "parserPromela.lex"
+{ printf("%s", xbt_automaton_parse_text); return (CASE); }
+       YY_BREAK
+case 12:
+YY_RULE_SETUP
+#line 42 "parserPromela.lex"
+{ printf("%s", xbt_automaton_parse_text); return (COLON); }
+       YY_BREAK
+case 13:
+YY_RULE_SETUP
+#line 43 "parserPromela.lex"
+{ printf("%s", xbt_automaton_parse_text); return (SEMI_COLON); }
+       YY_BREAK
+case 14:
+YY_RULE_SETUP
+#line 44 "parserPromela.lex"
+{ printf("%s", xbt_automaton_parse_text); return (CASE_TRUE); }
+       YY_BREAK
+case 15:
+YY_RULE_SETUP
+#line 45 "parserPromela.lex"
+{ printf("%s", xbt_automaton_parse_text); return (LEFT_BRACE); }
+       YY_BREAK
+case 16:
+YY_RULE_SETUP
+#line 46 "parserPromela.lex"
+{ printf("%s", xbt_automaton_parse_text); return (RIGHT_BRACE); }
+       YY_BREAK
+case 17:
+/* rule 17 can match eol */
+YY_RULE_SETUP
+#line 49 "parserPromela.lex"
+{ printf(" ");}
+       YY_BREAK
+case 18:
+YY_RULE_SETUP
+#line 51 "parserPromela.lex"
+{ printf("%s",xbt_automaton_parse_text); }
+       YY_BREAK
+case 19:
+YY_RULE_SETUP
+#line 54 "parserPromela.lex"
+{ printf("%s",xbt_automaton_parse_text); 
+                            sscanf(xbt_automaton_parse_text,"%lf",&yylval.real); 
+                            return (LITT_REEL); }
+       YY_BREAK
+case 20:
+YY_RULE_SETUP
+#line 58 "parserPromela.lex"
+{ printf("%s",xbt_automaton_parse_text); 
+                            sscanf(xbt_automaton_parse_text,"%d",&yylval.integer); 
+                            return (LITT_ENT); }
+       YY_BREAK
+case 21:
+/* rule 21 can match eol */
+YY_RULE_SETUP
+#line 62 "parserPromela.lex"
+{ printf("%s",xbt_automaton_parse_text);  
+                            yylval.string=(char *)malloc(strlen(xbt_automaton_parse_text)+1);
+                            sscanf(xbt_automaton_parse_text,"%s",yylval.string); 
+                            return (LITT_CHAINE); }
+       YY_BREAK
+case 22:
+YY_RULE_SETUP
+#line 67 "parserPromela.lex"
+{ printf("%s",xbt_automaton_parse_text); 
+                           yylval.string=(char *)malloc(strlen(xbt_automaton_parse_text)+1);
+                           sscanf(xbt_automaton_parse_text,"%s",yylval.string);
+                           return (ID); }
+       YY_BREAK
+case 23:
+/* rule 23 can match eol */
+YY_RULE_SETUP
+#line 72 "parserPromela.lex"
+{ printf("\n"); }
+       YY_BREAK
+case 24:
+YY_RULE_SETUP
+#line 74 "parserPromela.lex"
+{ printf("caractère inconnu\n"); }
+       YY_BREAK
+case 25:
+YY_RULE_SETUP
+#line 76 "parserPromela.lex"
+ECHO;
+       YY_BREAK
+#line 945 "automaton_parse.yy.c"
+case YY_STATE_EOF(INITIAL):
+       yyterminate();
+
+       case YY_END_OF_BUFFER:
+               {
+               /* Amount of text matched not including the EOB char. */
+               int yy_amount_of_matched_text = (int) (yy_cp - (yytext_ptr)) - 1;
+
+               /* Undo the effects of YY_DO_BEFORE_ACTION. */
+               *yy_cp = (yy_hold_char);
+               YY_RESTORE_YY_MORE_OFFSET
+
+               if ( YY_CURRENT_BUFFER_LVALUE->yy_buffer_status == YY_BUFFER_NEW )
+                       {
+                       /* We're scanning a new file or input source.  It's
+                        * possible that this happened because the user
+                        * just pointed xbt_automaton_parse_in at a new source and called
+                        * xbt_automaton_parse_lex().  If so, then we have to assure
+                        * consistency between YY_CURRENT_BUFFER and our
+                        * globals.  Here is the right place to do so, because
+                        * this is the first action (other than possibly a
+                        * back-up) that will match for the new input source.
+                        */
+                       (yy_n_chars) = YY_CURRENT_BUFFER_LVALUE->yy_n_chars;
+                       YY_CURRENT_BUFFER_LVALUE->yy_input_file = xbt_automaton_parse_in;
+                       YY_CURRENT_BUFFER_LVALUE->yy_buffer_status = YY_BUFFER_NORMAL;
+                       }
+
+               /* Note that here we test for yy_c_buf_p "<=" to the position
+                * of the first EOB in the buffer, since yy_c_buf_p will
+                * already have been incremented past the NUL character
+                * (since all states make transitions on EOB to the
+                * end-of-buffer state).  Contrast this with the test
+                * in input().
+                */
+               if ( (yy_c_buf_p) <= &YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[(yy_n_chars)] )
+                       { /* This was really a NUL. */
+                       yy_state_type yy_next_state;
+
+                       (yy_c_buf_p) = (yytext_ptr) + yy_amount_of_matched_text;
+
+                       yy_current_state = yy_get_previous_state(  );
+
+                       /* Okay, we're now positioned to make the NUL
+                        * transition.  We couldn't have
+                        * yy_get_previous_state() go ahead and do it
+                        * for us because it doesn't know how to deal
+                        * with the possibility of jamming (and we don't
+                        * want to build jamming into it because then it
+                        * will run more slowly).
+                        */
+
+                       yy_next_state = yy_try_NUL_trans( yy_current_state );
+
+                       yy_bp = (yytext_ptr) + YY_MORE_ADJ;
+
+                       if ( yy_next_state )
+                               {
+                               /* Consume the NUL. */
+                               yy_cp = ++(yy_c_buf_p);
+                               yy_current_state = yy_next_state;
+                               goto yy_match;
+                               }
+
+                       else
+                               {
+                               yy_cp = (yy_c_buf_p);
+                               goto yy_find_action;
+                               }
+                       }
+
+               else switch ( yy_get_next_buffer(  ) )
+                       {
+                       case EOB_ACT_END_OF_FILE:
+                               {
+                               (yy_did_buffer_switch_on_eof) = 0;
+
+                               if ( xbt_automaton_parse_wrap( ) )
+                                       {
+                                       /* Note: because we've taken care in
+                                        * yy_get_next_buffer() to have set up
+                                        * xbt_automaton_parse_text, we can now set up
+                                        * yy_c_buf_p so that if some total
+                                        * hoser (like flex itself) wants to
+                                        * call the scanner after we return the
+                                        * YY_NULL, it'll still work - another
+                                        * YY_NULL will get returned.
+                                        */
+                                       (yy_c_buf_p) = (yytext_ptr) + YY_MORE_ADJ;
+
+                                       yy_act = YY_STATE_EOF(YY_START);
+                                       goto do_action;
+                                       }
+
+                               else
+                                       {
+                                       if ( ! (yy_did_buffer_switch_on_eof) )
+                                               YY_NEW_FILE;
+                                       }
+                               break;
+                               }
+
+                       case EOB_ACT_CONTINUE_SCAN:
+                               (yy_c_buf_p) =
+                                       (yytext_ptr) + yy_amount_of_matched_text;
+
+                               yy_current_state = yy_get_previous_state(  );
+
+                               yy_cp = (yy_c_buf_p);
+                               yy_bp = (yytext_ptr) + YY_MORE_ADJ;
+                               goto yy_match;
+
+                       case EOB_ACT_LAST_MATCH:
+                               (yy_c_buf_p) =
+                               &YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[(yy_n_chars)];
+
+                               yy_current_state = yy_get_previous_state(  );
+
+                               yy_cp = (yy_c_buf_p);
+                               yy_bp = (yytext_ptr) + YY_MORE_ADJ;
+                               goto yy_find_action;
+                       }
+               break;
+               }
+
+       default:
+               YY_FATAL_ERROR(
+                       "fatal flex scanner internal error--no action found" );
+       } /* end of action switch */
+               } /* end of scanning one token */
+} /* end of xbt_automaton_parse_lex */
+
+/* yy_get_next_buffer - try to read in a new buffer
+ *
+ * Returns a code representing an action:
+ *     EOB_ACT_LAST_MATCH -
+ *     EOB_ACT_CONTINUE_SCAN - continue scanning from current position
+ *     EOB_ACT_END_OF_FILE - end of file
+ */
+static int yy_get_next_buffer (void)
+{
+       register char *dest = YY_CURRENT_BUFFER_LVALUE->yy_ch_buf;
+       register char *source = (yytext_ptr);
+       register int number_to_move, i;
+       int ret_val;
+
+       if ( (yy_c_buf_p) > &YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[(yy_n_chars) + 1] )
+               YY_FATAL_ERROR(
+               "fatal flex scanner internal error--end of buffer missed" );
+
+       if ( YY_CURRENT_BUFFER_LVALUE->yy_fill_buffer == 0 )
+               { /* Don't try to fill the buffer, so this is an EOF. */
+               if ( (yy_c_buf_p) - (yytext_ptr) - YY_MORE_ADJ == 1 )
+                       {
+                       /* We matched a single character, the EOB, so
+                        * treat this as a final EOF.
+                        */
+                       return EOB_ACT_END_OF_FILE;
+                       }
+
+               else
+                       {
+                       /* We matched some text prior to the EOB, first
+                        * process it.
+                        */
+                       return EOB_ACT_LAST_MATCH;
+                       }
+               }
+
+       /* Try to read more data. */
+
+       /* First move last chars to start of buffer. */
+       number_to_move = (int) ((yy_c_buf_p) - (yytext_ptr)) - 1;
+
+       for ( i = 0; i < number_to_move; ++i )
+               *(dest++) = *(source++);
+
+       if ( YY_CURRENT_BUFFER_LVALUE->yy_buffer_status == YY_BUFFER_EOF_PENDING )
+               /* don't do the read, it's not guaranteed to return an EOF,
+                * just force an EOF
+                */
+               YY_CURRENT_BUFFER_LVALUE->yy_n_chars = (yy_n_chars) = 0;
+
+       else
+               {
+                       int num_to_read =
+                       YY_CURRENT_BUFFER_LVALUE->yy_buf_size - number_to_move - 1;
+
+               while ( num_to_read <= 0 )
+                       { /* Not enough room in the buffer - grow it. */
+
+                       /* just a shorter name for the current buffer */
+                       YY_BUFFER_STATE b = YY_CURRENT_BUFFER;
+
+                       int yy_c_buf_p_offset =
+                               (int) ((yy_c_buf_p) - b->yy_ch_buf);
+
+                       if ( b->yy_is_our_buffer )
+                               {
+                               int new_size = b->yy_buf_size * 2;
+
+                               if ( new_size <= 0 )
+                                       b->yy_buf_size += b->yy_buf_size / 8;
+                               else
+                                       b->yy_buf_size *= 2;
+
+                               b->yy_ch_buf = (char *)
+                                       /* Include room in for 2 EOB chars. */
+                                       xbt_automaton_parse_realloc((void *) b->yy_ch_buf,b->yy_buf_size + 2  );
+                               }
+                       else
+                               /* Can't grow it, we don't own it. */
+                               b->yy_ch_buf = 0;
+
+                       if ( ! b->yy_ch_buf )
+                               YY_FATAL_ERROR(
+                               "fatal error - scanner input buffer overflow" );
+
+                       (yy_c_buf_p) = &b->yy_ch_buf[yy_c_buf_p_offset];
+
+                       num_to_read = YY_CURRENT_BUFFER_LVALUE->yy_buf_size -
+                                               number_to_move - 1;
+
+                       }
+
+               if ( num_to_read > YY_READ_BUF_SIZE )
+                       num_to_read = YY_READ_BUF_SIZE;
+
+               /* Read in more data. */
+               YY_INPUT( (&YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[number_to_move]),
+                       (yy_n_chars), (size_t) num_to_read );
+
+               YY_CURRENT_BUFFER_LVALUE->yy_n_chars = (yy_n_chars);
+               }
+
+       if ( (yy_n_chars) == 0 )
+               {
+               if ( number_to_move == YY_MORE_ADJ )
+                       {
+                       ret_val = EOB_ACT_END_OF_FILE;
+                       xbt_automaton_parse_restart(xbt_automaton_parse_in  );
+                       }
+
+               else
+                       {
+                       ret_val = EOB_ACT_LAST_MATCH;
+                       YY_CURRENT_BUFFER_LVALUE->yy_buffer_status =
+                               YY_BUFFER_EOF_PENDING;
+                       }
+               }
+
+       else
+               ret_val = EOB_ACT_CONTINUE_SCAN;
+
+       if ((yy_size_t) ((yy_n_chars) + number_to_move) > YY_CURRENT_BUFFER_LVALUE->yy_buf_size) {
+               /* Extend the array by 50%, plus the number we really need. */
+               yy_size_t new_size = (yy_n_chars) + number_to_move + ((yy_n_chars) >> 1);
+               YY_CURRENT_BUFFER_LVALUE->yy_ch_buf = (char *) xbt_automaton_parse_realloc((void *) YY_CURRENT_BUFFER_LVALUE->yy_ch_buf,new_size  );
+               if ( ! YY_CURRENT_BUFFER_LVALUE->yy_ch_buf )
+                       YY_FATAL_ERROR( "out of dynamic memory in yy_get_next_buffer()" );
+       }
+
+       (yy_n_chars) += number_to_move;
+       YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[(yy_n_chars)] = YY_END_OF_BUFFER_CHAR;
+       YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[(yy_n_chars) + 1] = YY_END_OF_BUFFER_CHAR;
+
+       (yytext_ptr) = &YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[0];
+
+       return ret_val;
+}
+
+/* yy_get_previous_state - get the state just before the EOB char was reached */
+
+    static yy_state_type yy_get_previous_state (void)
+{
+       register yy_state_type yy_current_state;
+       register char *yy_cp;
+    
+       yy_current_state = (yy_start);
+
+       for ( yy_cp = (yytext_ptr) + YY_MORE_ADJ; yy_cp < (yy_c_buf_p); ++yy_cp )
+               {
+               register YY_CHAR yy_c = (*yy_cp ? yy_ec[YY_SC_TO_UI(*yy_cp)] : 1);
+               if ( yy_accept[yy_current_state] )
+                       {
+                       (yy_last_accepting_state) = yy_current_state;
+                       (yy_last_accepting_cpos) = yy_cp;
+                       }
+               while ( yy_chk[yy_base[yy_current_state] + yy_c] != yy_current_state )
+                       {
+                       yy_current_state = (int) yy_def[yy_current_state];
+                       if ( yy_current_state >= 54 )
+                               yy_c = yy_meta[(unsigned int) yy_c];
+                       }
+               yy_current_state = yy_nxt[yy_base[yy_current_state] + (unsigned int) yy_c];
+               }
+
+       return yy_current_state;
+}
+
+/* yy_try_NUL_trans - try to make a transition on the NUL character
+ *
+ * synopsis
+ *     next_state = yy_try_NUL_trans( current_state );
+ */
+    static yy_state_type yy_try_NUL_trans  (yy_state_type yy_current_state )
+{
+       register int yy_is_jam;
+       register char *yy_cp = (yy_c_buf_p);
+
+       register YY_CHAR yy_c = 1;
+       if ( yy_accept[yy_current_state] )
+               {
+               (yy_last_accepting_state) = yy_current_state;
+               (yy_last_accepting_cpos) = yy_cp;
+               }
+       while ( yy_chk[yy_base[yy_current_state] + yy_c] != yy_current_state )
+               {
+               yy_current_state = (int) yy_def[yy_current_state];
+               if ( yy_current_state >= 54 )
+                       yy_c = yy_meta[(unsigned int) yy_c];
+               }
+       yy_current_state = yy_nxt[yy_base[yy_current_state] + (unsigned int) yy_c];
+       yy_is_jam = (yy_current_state == 53);
+
+       return yy_is_jam ? 0 : yy_current_state;
+}
+
+    static void yyunput (int c, register char * yy_bp )
+{
+       register char *yy_cp;
+    
+    yy_cp = (yy_c_buf_p);
+
+       /* undo effects of setting up xbt_automaton_parse_text */
+       *yy_cp = (yy_hold_char);
+
+       if ( yy_cp < YY_CURRENT_BUFFER_LVALUE->yy_ch_buf + 2 )
+               { /* need to shift things up to make room */
+               /* +2 for EOB chars. */
+               register int number_to_move = (yy_n_chars) + 2;
+               register char *dest = &YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[
+                                       YY_CURRENT_BUFFER_LVALUE->yy_buf_size + 2];
+               register char *source =
+                               &YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[number_to_move];
+
+               while ( source > YY_CURRENT_BUFFER_LVALUE->yy_ch_buf )
+                       *--dest = *--source;
+
+               yy_cp += (int) (dest - source);
+               yy_bp += (int) (dest - source);
+               YY_CURRENT_BUFFER_LVALUE->yy_n_chars =
+                       (yy_n_chars) = YY_CURRENT_BUFFER_LVALUE->yy_buf_size;
+
+               if ( yy_cp < YY_CURRENT_BUFFER_LVALUE->yy_ch_buf + 2 )
+                       YY_FATAL_ERROR( "flex scanner push-back overflow" );
+               }
+
+       *--yy_cp = (char) c;
+
+       (yytext_ptr) = yy_bp;
+       (yy_hold_char) = *yy_cp;
+       (yy_c_buf_p) = yy_cp;
+}
+
+#ifndef YY_NO_INPUT
+#ifdef __cplusplus
+    static int yyinput (void)
+#else
+    static int input  (void)
+#endif
+
+{
+       int c;
+    
+       *(yy_c_buf_p) = (yy_hold_char);
+
+       if ( *(yy_c_buf_p) == YY_END_OF_BUFFER_CHAR )
+               {
+               /* yy_c_buf_p now points to the character we want to return.
+                * If this occurs *before* the EOB characters, then it's a
+                * valid NUL; if not, then we've hit the end of the buffer.
+                */
+               if ( (yy_c_buf_p) < &YY_CURRENT_BUFFER_LVALUE->yy_ch_buf[(yy_n_chars)] )
+                       /* This was really a NUL. */
+                       *(yy_c_buf_p) = '\0';
+
+               else
+                       { /* need more input */
+                       int offset = (yy_c_buf_p) - (yytext_ptr);
+                       ++(yy_c_buf_p);
+
+                       switch ( yy_get_next_buffer(  ) )
+                               {
+                               case EOB_ACT_LAST_MATCH:
+                                       /* This happens because yy_g_n_b()
+                                        * sees that we've accumulated a
+                                        * token and flags that we need to
+                                        * try matching the token before
+                                        * proceeding.  But for input(),
+                                        * there's no matching to consider.
+                                        * So convert the EOB_ACT_LAST_MATCH
+                                        * to EOB_ACT_END_OF_FILE.
+                                        */
+
+                                       /* Reset buffer status. */
+                                       xbt_automaton_parse_restart(xbt_automaton_parse_in );
+
+                                       /*FALLTHROUGH*/
+
+                               case EOB_ACT_END_OF_FILE:
+                                       {
+                                       if ( xbt_automaton_parse_wrap( ) )
+                                               return EOF;
+
+                                       if ( ! (yy_did_buffer_switch_on_eof) )
+                                               YY_NEW_FILE;
+#ifdef __cplusplus
+                                       return yyinput();
+#else
+                                       return input();
+#endif
+                                       }
+
+                               case EOB_ACT_CONTINUE_SCAN:
+                                       (yy_c_buf_p) = (yytext_ptr) + offset;
+                                       break;
+                               }
+                       }
+               }
+
+       c = *(unsigned char *) (yy_c_buf_p);    /* cast for 8-bit char's */
+       *(yy_c_buf_p) = '\0';   /* preserve xbt_automaton_parse_text */
+       (yy_hold_char) = *++(yy_c_buf_p);
+
+       return c;
+}
+#endif /* ifndef YY_NO_INPUT */
+
+/** Immediately switch to a different input stream.
+ * @param input_file A readable stream.
+ * 
+ * @note This function does not reset the start condition to @c INITIAL .
+ */
+    void xbt_automaton_parse_restart  (FILE * input_file )
+{
+    
+       if ( ! YY_CURRENT_BUFFER ){
+        xbt_automaton_parse_ensure_buffer_stack ();
+               YY_CURRENT_BUFFER_LVALUE =
+            xbt_automaton_parse__create_buffer(xbt_automaton_parse_in,YY_BUF_SIZE );
+       }
+
+       xbt_automaton_parse__init_buffer(YY_CURRENT_BUFFER,input_file );
+       xbt_automaton_parse__load_buffer_state( );
+}
+
+/** Switch to a different input buffer.
+ * @param new_buffer The new input buffer.
+ * 
+ */
+    void xbt_automaton_parse__switch_to_buffer  (YY_BUFFER_STATE  new_buffer )
+{
+    
+       /* TODO. We should be able to replace this entire function body
+        * with
+        *              xbt_automaton_parse_pop_buffer_state();
+        *              xbt_automaton_parse_push_buffer_state(new_buffer);
+     */
+       xbt_automaton_parse_ensure_buffer_stack ();
+       if ( YY_CURRENT_BUFFER == new_buffer )
+               return;
+
+       if ( YY_CURRENT_BUFFER )
+               {
+               /* Flush out information for old buffer. */
+               *(yy_c_buf_p) = (yy_hold_char);
+               YY_CURRENT_BUFFER_LVALUE->yy_buf_pos = (yy_c_buf_p);
+               YY_CURRENT_BUFFER_LVALUE->yy_n_chars = (yy_n_chars);
+               }
+
+       YY_CURRENT_BUFFER_LVALUE = new_buffer;
+       xbt_automaton_parse__load_buffer_state( );
+
+       /* We don't actually know whether we did this switch during
+        * EOF (xbt_automaton_parse_wrap()) processing, but the only time this flag
+        * is looked at is after xbt_automaton_parse_wrap() is called, so it's safe
+        * to go ahead and always set it.
+        */
+       (yy_did_buffer_switch_on_eof) = 1;
+}
+
+static void xbt_automaton_parse__load_buffer_state  (void)
+{
+       (yy_n_chars) = YY_CURRENT_BUFFER_LVALUE->yy_n_chars;
+       (yytext_ptr) = (yy_c_buf_p) = YY_CURRENT_BUFFER_LVALUE->yy_buf_pos;
+       xbt_automaton_parse_in = YY_CURRENT_BUFFER_LVALUE->yy_input_file;
+       (yy_hold_char) = *(yy_c_buf_p);
+}
+
+/** Allocate and initialize an input buffer state.
+ * @param file A readable stream.
+ * @param size The character buffer size in bytes. When in doubt, use @c YY_BUF_SIZE.
+ * 
+ * @return the allocated buffer state.
+ */
+    YY_BUFFER_STATE xbt_automaton_parse__create_buffer  (FILE * file, int  size )
+{
+       YY_BUFFER_STATE b;
+    
+       b = (YY_BUFFER_STATE) xbt_automaton_parse_alloc(sizeof( struct yy_buffer_state )  );
+       if ( ! b )
+               YY_FATAL_ERROR( "out of dynamic memory in xbt_automaton_parse__create_buffer()" );
+
+       b->yy_buf_size = size;
+
+       /* yy_ch_buf has to be 2 characters longer than the size given because
+        * we need to put in 2 end-of-buffer characters.
+        */
+       b->yy_ch_buf = (char *) xbt_automaton_parse_alloc(b->yy_buf_size + 2  );
+       if ( ! b->yy_ch_buf )
+               YY_FATAL_ERROR( "out of dynamic memory in xbt_automaton_parse__create_buffer()" );
+
+       b->yy_is_our_buffer = 1;
+
+       xbt_automaton_parse__init_buffer(b,file );
+
+       return b;
+}
+
+/** Destroy the buffer.
+ * @param b a buffer created with xbt_automaton_parse__create_buffer()
+ * 
+ */
+    void xbt_automaton_parse__delete_buffer (YY_BUFFER_STATE  b )
+{
+    
+       if ( ! b )
+               return;
+
+       if ( b == YY_CURRENT_BUFFER ) /* Not sure if we should pop here. */
+               YY_CURRENT_BUFFER_LVALUE = (YY_BUFFER_STATE) 0;
+
+       if ( b->yy_is_our_buffer )
+               xbt_automaton_parse_free((void *) b->yy_ch_buf  );
+
+       xbt_automaton_parse_free((void *) b  );
+}
+
+#ifndef __cplusplus
+extern int isatty (int );
+#endif /* __cplusplus */
+    
+/* Initializes or reinitializes a buffer.
+ * This function is sometimes called more than once on the same buffer,
+ * such as during a xbt_automaton_parse_restart() or at EOF.
+ */
+    static void xbt_automaton_parse__init_buffer  (YY_BUFFER_STATE  b, FILE * file )
+
+{
+       int oerrno = errno;
+    
+       xbt_automaton_parse__flush_buffer(b );
+
+       b->yy_input_file = file;
+       b->yy_fill_buffer = 1;
+
+    /* If b is the current buffer, then xbt_automaton_parse__init_buffer was _probably_
+     * called from xbt_automaton_parse_restart() or through yy_get_next_buffer.
+     * In that case, we don't want to reset the lineno or column.
+     */
+    if (b != YY_CURRENT_BUFFER){
+        b->yy_bs_lineno = 1;
+        b->yy_bs_column = 0;
+    }
+
+        b->yy_is_interactive = file ? (isatty( fileno(file) ) > 0) : 0;
+    
+       errno = oerrno;
+}
+
+/** Discard all buffered characters. On the next scan, YY_INPUT will be called.
+ * @param b the buffer state to be flushed, usually @c YY_CURRENT_BUFFER.
+ * 
+ */
+    void xbt_automaton_parse__flush_buffer (YY_BUFFER_STATE  b )
+{
+       if ( ! b )
+               return;
+
+       b->yy_n_chars = 0;
+
+       /* We always need two end-of-buffer characters.  The first causes
+        * a transition to the end-of-buffer state.  The second causes
+        * a jam in that state.
+        */
+       b->yy_ch_buf[0] = YY_END_OF_BUFFER_CHAR;
+       b->yy_ch_buf[1] = YY_END_OF_BUFFER_CHAR;
+
+       b->yy_buf_pos = &b->yy_ch_buf[0];
+
+       b->yy_at_bol = 1;
+       b->yy_buffer_status = YY_BUFFER_NEW;
+
+       if ( b == YY_CURRENT_BUFFER )
+               xbt_automaton_parse__load_buffer_state( );
+}
+
+/** Pushes the new state onto the stack. The new state becomes
+ *  the current state. This function will allocate the stack
+ *  if necessary.
+ *  @param new_buffer The new state.
+ *  
+ */
+void xbt_automaton_parse_push_buffer_state (YY_BUFFER_STATE new_buffer )
+{
+       if (new_buffer == NULL)
+               return;
+
+       xbt_automaton_parse_ensure_buffer_stack();
+
+       /* This block is copied from xbt_automaton_parse__switch_to_buffer. */
+       if ( YY_CURRENT_BUFFER )
+               {
+               /* Flush out information for old buffer. */
+               *(yy_c_buf_p) = (yy_hold_char);
+               YY_CURRENT_BUFFER_LVALUE->yy_buf_pos = (yy_c_buf_p);
+               YY_CURRENT_BUFFER_LVALUE->yy_n_chars = (yy_n_chars);
+               }
+
+       /* Only push if top exists. Otherwise, replace top. */
+       if (YY_CURRENT_BUFFER)
+               (yy_buffer_stack_top)++;
+       YY_CURRENT_BUFFER_LVALUE = new_buffer;
+
+       /* copied from xbt_automaton_parse__switch_to_buffer. */
+       xbt_automaton_parse__load_buffer_state( );
+       (yy_did_buffer_switch_on_eof) = 1;
+}
+
+/** Removes and deletes the top of the stack, if present.
+ *  The next element becomes the new top.
+ *  
+ */
+void xbt_automaton_parse_pop_buffer_state (void)
+{
+       if (!YY_CURRENT_BUFFER)
+               return;
+
+       xbt_automaton_parse__delete_buffer(YY_CURRENT_BUFFER );
+       YY_CURRENT_BUFFER_LVALUE = NULL;
+       if ((yy_buffer_stack_top) > 0)
+               --(yy_buffer_stack_top);
+
+       if (YY_CURRENT_BUFFER) {
+               xbt_automaton_parse__load_buffer_state( );
+               (yy_did_buffer_switch_on_eof) = 1;
+       }
+}
+
+/* Allocates the stack if it does not exist.
+ *  Guarantees space for at least one push.
+ */
+static void xbt_automaton_parse_ensure_buffer_stack (void)
+{
+       int num_to_alloc;
+    
+       if (!(yy_buffer_stack)) {
+
+               /* First allocation is just for 2 elements, since we don't know if this
+                * scanner will even need a stack. We use 2 instead of 1 to avoid an
+                * immediate realloc on the next call.
+         */
+               num_to_alloc = 1;
+               (yy_buffer_stack) = (struct yy_buffer_state**)xbt_automaton_parse_alloc
+                                                               (num_to_alloc * sizeof(struct yy_buffer_state*)
+                                                               );
+               if ( ! (yy_buffer_stack) )
+                       YY_FATAL_ERROR( "out of dynamic memory in xbt_automaton_parse_ensure_buffer_stack()" );
+                                                                 
+               memset((yy_buffer_stack), 0, num_to_alloc * sizeof(struct yy_buffer_state*));
+                               
+               (yy_buffer_stack_max) = num_to_alloc;
+               (yy_buffer_stack_top) = 0;
+               return;
+       }
+
+       if ((yy_buffer_stack_top) >= ((yy_buffer_stack_max)) - 1){
+
+               /* Increase the buffer to prepare for a possible push. */
+               int grow_size = 8 /* arbitrary grow size */;
+
+               num_to_alloc = (yy_buffer_stack_max) + grow_size;
+               (yy_buffer_stack) = (struct yy_buffer_state**)xbt_automaton_parse_realloc
+                                                               ((yy_buffer_stack),
+                                                               num_to_alloc * sizeof(struct yy_buffer_state*)
+                                                               );
+               if ( ! (yy_buffer_stack) )
+                       YY_FATAL_ERROR( "out of dynamic memory in xbt_automaton_parse_ensure_buffer_stack()" );
+
+               /* zero only the new slots.*/
+               memset((yy_buffer_stack) + (yy_buffer_stack_max), 0, grow_size * sizeof(struct yy_buffer_state*));
+               (yy_buffer_stack_max) = num_to_alloc;
+       }
+}
+
+/** Setup the input buffer state to scan directly from a user-specified character buffer.
+ * @param base the character buffer
+ * @param size the size in bytes of the character buffer
+ * 
+ * @return the newly allocated buffer state object. 
+ */
+YY_BUFFER_STATE xbt_automaton_parse__scan_buffer  (char * base, yy_size_t  size )
+{
+       YY_BUFFER_STATE b;
+    
+       if ( size < 2 ||
+            base[size-2] != YY_END_OF_BUFFER_CHAR ||
+            base[size-1] != YY_END_OF_BUFFER_CHAR )
+               /* They forgot to leave room for the EOB's. */
+               return 0;
+
+       b = (YY_BUFFER_STATE) xbt_automaton_parse_alloc(sizeof( struct yy_buffer_state )  );
+       if ( ! b )
+               YY_FATAL_ERROR( "out of dynamic memory in xbt_automaton_parse__scan_buffer()" );
+
+       b->yy_buf_size = size - 2;      /* "- 2" to take care of EOB's */
+       b->yy_buf_pos = b->yy_ch_buf = base;
+       b->yy_is_our_buffer = 0;
+       b->yy_input_file = 0;
+       b->yy_n_chars = b->yy_buf_size;
+       b->yy_is_interactive = 0;
+       b->yy_at_bol = 1;
+       b->yy_fill_buffer = 0;
+       b->yy_buffer_status = YY_BUFFER_NEW;
+
+       xbt_automaton_parse__switch_to_buffer(b  );
+
+       return b;
+}
+
+/** Setup the input buffer state to scan a string. The next call to xbt_automaton_parse_lex() will
+ * scan from a @e copy of @a str.
+ * @param yystr a NUL-terminated string to scan
+ * 
+ * @return the newly allocated buffer state object.
+ * @note If you want to scan bytes that may contain NUL values, then use
+ *       xbt_automaton_parse__scan_bytes() instead.
+ */
+YY_BUFFER_STATE xbt_automaton_parse__scan_string (yyconst char * yystr )
+{
+    
+       return xbt_automaton_parse__scan_bytes(yystr,strlen(yystr) );
+}
+
+/** Setup the input buffer state to scan the given bytes. The next call to xbt_automaton_parse_lex() will
+ * scan from a @e copy of @a bytes.
+ * @param yybytes the byte buffer to scan
+ * @param _yybytes_len the number of bytes in the buffer pointed to by @a bytes.
+ * 
+ * @return the newly allocated buffer state object.
+ */
+YY_BUFFER_STATE xbt_automaton_parse__scan_bytes  (yyconst char * yybytes, int  _yybytes_len )
+{
+       YY_BUFFER_STATE b;
+       char *buf;
+       yy_size_t n;
+       int i;
+    
+       /* Get memory for full buffer, including space for trailing EOB's. */
+       n = _yybytes_len + 2;
+       buf = (char *) xbt_automaton_parse_alloc(n  );
+       if ( ! buf )
+               YY_FATAL_ERROR( "out of dynamic memory in xbt_automaton_parse__scan_bytes()" );
+
+       for ( i = 0; i < _yybytes_len; ++i )
+               buf[i] = yybytes[i];
+
+       buf[_yybytes_len] = buf[_yybytes_len+1] = YY_END_OF_BUFFER_CHAR;
+
+       b = xbt_automaton_parse__scan_buffer(buf,n );
+       if ( ! b )
+               YY_FATAL_ERROR( "bad buffer in xbt_automaton_parse__scan_bytes()" );
+
+       /* It's okay to grow etc. this buffer, and we should throw it
+        * away when we're done.
+        */
+       b->yy_is_our_buffer = 1;
+
+       return b;
+}
+
+#ifndef YY_EXIT_FAILURE
+#define YY_EXIT_FAILURE 2
+#endif
+
+static void yy_fatal_error (yyconst char* msg )
+{
+       (void) fprintf( stderr, "%s\n", msg );
+       exit( YY_EXIT_FAILURE );
+}
+
+/* Redefine yyless() so it works in section 3 code. */
+
+#undef yyless
+#define yyless(n) \
+       do \
+               { \
+               /* Undo effects of setting up xbt_automaton_parse_text. */ \
+        int yyless_macro_arg = (n); \
+        YY_LESS_LINENO(yyless_macro_arg);\
+               xbt_automaton_parse_text[xbt_automaton_parse_leng] = (yy_hold_char); \
+               (yy_c_buf_p) = xbt_automaton_parse_text + yyless_macro_arg; \
+               (yy_hold_char) = *(yy_c_buf_p); \
+               *(yy_c_buf_p) = '\0'; \
+               xbt_automaton_parse_leng = yyless_macro_arg; \
+               } \
+       while ( 0 )
+
+/* Accessor  methods (get/set functions) to struct members. */
+
+/** Get the current line number.
+ * 
+ */
+int xbt_automaton_parse_get_lineno  (void)
+{
+        
+    return xbt_automaton_parse_lineno;
+}
+
+/** Get the input stream.
+ * 
+ */
+FILE *xbt_automaton_parse_get_in  (void)
+{
+        return xbt_automaton_parse_in;
+}
+
+/** Get the output stream.
+ * 
+ */
+FILE *xbt_automaton_parse_get_out  (void)
+{
+        return xbt_automaton_parse_out;
+}
+
+/** Get the length of the current token.
+ * 
+ */
+int xbt_automaton_parse_get_leng  (void)
+{
+        return xbt_automaton_parse_leng;
+}
+
+/** Get the current token.
+ * 
+ */
+
+char *xbt_automaton_parse_get_text  (void)
+{
+        return xbt_automaton_parse_text;
+}
+
+/** Set the current line number.
+ * @param line_number
+ * 
+ */
+void xbt_automaton_parse_set_lineno (int  line_number )
+{
+    
+    xbt_automaton_parse_lineno = line_number;
+}
+
+/** Set the input stream. This does not discard the current
+ * input buffer.
+ * @param in_str A readable stream.
+ * 
+ * @see xbt_automaton_parse__switch_to_buffer
+ */
+void xbt_automaton_parse_set_in (FILE *  in_str )
+{
+        xbt_automaton_parse_in = in_str ;
+}
+
+void xbt_automaton_parse_set_out (FILE *  out_str )
+{
+        xbt_automaton_parse_out = out_str ;
+}
+
+int xbt_automaton_parse_get_debug  (void)
+{
+        return xbt_automaton_parse__flex_debug;
+}
+
+void xbt_automaton_parse_set_debug (int  bdebug )
+{
+        xbt_automaton_parse__flex_debug = bdebug ;
+}
+
+static int yy_init_globals (void)
+{
+        /* Initialization is the same as for the non-reentrant scanner.
+     * This function is called from xbt_automaton_parse_lex_destroy(), so don't allocate here.
+     */
+
+    (yy_buffer_stack) = 0;
+    (yy_buffer_stack_top) = 0;
+    (yy_buffer_stack_max) = 0;
+    (yy_c_buf_p) = (char *) 0;
+    (yy_init) = 0;
+    (yy_start) = 0;
+
+/* Defined in main.c */
+#ifdef YY_STDINIT
+    xbt_automaton_parse_in = stdin;
+    xbt_automaton_parse_out = stdout;
+#else
+    xbt_automaton_parse_in = (FILE *) 0;
+    xbt_automaton_parse_out = (FILE *) 0;
+#endif
+
+    /* For future reference: Set errno on error, since we are called by
+     * xbt_automaton_parse_lex_init()
+     */
+    return 0;
+}
+
+/* xbt_automaton_parse_lex_destroy is for both reentrant and non-reentrant scanners. */
+int xbt_automaton_parse_lex_destroy  (void)
+{
+    
+    /* Pop the buffer stack, destroying each element. */
+       while(YY_CURRENT_BUFFER){
+               xbt_automaton_parse__delete_buffer(YY_CURRENT_BUFFER  );
+               YY_CURRENT_BUFFER_LVALUE = NULL;
+               xbt_automaton_parse_pop_buffer_state();
+       }
+
+       /* Destroy the stack itself. */
+       xbt_automaton_parse_free((yy_buffer_stack) );
+       (yy_buffer_stack) = NULL;
+
+    /* Reset the globals. This is important in a non-reentrant scanner so the next time
+     * xbt_automaton_parse_lex() is called, initialization will occur. */
+    yy_init_globals( );
+
+    return 0;
+}
+
+/*
+ * Internal utility routines.
+ */
+
+#ifndef yytext_ptr
+static void yy_flex_strncpy (char* s1, yyconst char * s2, int n )
+{
+       register int i;
+       for ( i = 0; i < n; ++i )
+               s1[i] = s2[i];
+}
+#endif
+
+#ifdef YY_NEED_STRLEN
+static int yy_flex_strlen (yyconst char * s )
+{
+       register int n;
+       for ( n = 0; s[n]; ++n )
+               ;
+
+       return n;
+}
+#endif
+
+void *xbt_automaton_parse_alloc (yy_size_t  size )
+{
+       return (void *) malloc( size );
+}
+
+void *xbt_automaton_parse_realloc  (void * ptr, yy_size_t  size )
+{
+       /* The cast to (char *) in the following accommodates both
+        * implementations that use char* generic pointers, and those
+        * that use void* generic pointers.  It works with the latter
+        * because both ANSI C and C++ allow castless assignment from
+        * any pointer type to void*, and deal with argument conversions
+        * as though doing an assignment.
+        */
+       return (void *) realloc( (char *) ptr, size );
+}
+
+void xbt_automaton_parse_free (void * ptr )
+{
+       free( (char *) ptr );   /* see xbt_automaton_parse_realloc() for (char *) cast */
+}
+
+#define YYTABLES_NAME "yytables"
+
+#line 76 "parserPromela.lex"
+
+
+
+
+
diff --git a/src/xbt/automaton/automatonparse_promela.c b/src/xbt/automaton/automatonparse_promela.c
new file mode 100644 (file)
index 0000000..bfd39e1
--- /dev/null
@@ -0,0 +1,101 @@
+/* methods for implementation of automaton from promela description */
+
+/* Copyright (c) 2011. The SimGrid Team.
+ * All rights reserved.                                                     */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+#include "xbt/automatonparse_promela.h"
+
+xbt_automaton_t automaton;
+char* state_id_src;
+
+void init(){
+  automaton = xbt_automaton_new_automaton();
+}
+
+void new_state(char* id, int src){
+
+  char* id_state = strdup(id);
+  char* first_part = strtok(id,"_");
+  int type = 0 ; // -1=état initial, 0=état intermédiaire, 1=état final
+
+  if(strcmp(first_part,"accept")==0){
+    type = 1;
+  }else{
+    char* second_part = strtok(NULL,"_");
+    if(strcmp(second_part,"init")==0){
+      type = -1;
+    }
+  }
+
+  xbt_state_t state = NULL;
+  state = xbt_automaton_state_exists(automaton, id_state);
+  if(state == NULL){
+    state = xbt_automaton_new_state(automaton, type, id_state);
+  }
+
+  if(type==-1)
+    automaton->current_state = state;
+
+  if(src)
+    state_id_src = strdup(id_state);
+    
+}
+
+void new_transition(char* id, xbt_exp_label_t label){
+
+  char* id_state = strdup(id);
+  xbt_state_t state_dst = NULL;
+  new_state(id, 0);
+  state_dst = xbt_automaton_state_exists(automaton, id_state);
+  xbt_state_t state_src = xbt_automaton_state_exists(automaton, state_id_src); 
+  
+  //xbt_transition_t trans = NULL;
+  xbt_automaton_new_transition(automaton, state_src, state_dst, label);
+
+}
+
+xbt_exp_label_t new_label(int type, ...){
+  xbt_exp_label_t label = NULL;
+  va_list ap;
+  va_start(ap,type);
+  switch(type){
+  case 0 : {
+    xbt_exp_label_t left = va_arg(ap, xbt_exp_label_t);
+    xbt_exp_label_t right = va_arg(ap, xbt_exp_label_t);
+    label = xbt_automaton_new_label(type, left, right);
+    break;
+  }
+  case 1 : {
+    xbt_exp_label_t left = va_arg(ap, xbt_exp_label_t);
+    xbt_exp_label_t right = va_arg(ap, xbt_exp_label_t);
+    label = xbt_automaton_new_label(type, left, right);
+    break;
+  }
+  case 2 : {
+    xbt_exp_label_t exp_not = va_arg(ap, xbt_exp_label_t);
+    label = xbt_automaton_new_label(type, exp_not);
+    break;
+  }
+  case 3 : {
+    char* p = va_arg(ap, char*);
+    label = xbt_automaton_new_label(type, p);
+    break;
+  }
+  case 4 : {
+    label = xbt_automaton_new_label(type);
+    break;
+  }
+  }
+  va_end(ap);
+  return label;
+}
+
+xbt_automaton_t get_automaton(){
+  return automaton;
+}
+
+
+
diff --git a/src/xbt/automaton/parserPromela.lex b/src/xbt/automaton/parserPromela.lex
new file mode 100644 (file)
index 0000000..f4c9132
--- /dev/null
@@ -0,0 +1,78 @@
+%option noyywrap
+
+%{
+
+
+#include <stdio.h>
+#include "y.tab.h"
+  
+  extern YYSTYPE yylval;
+%}
+
+blancs       [ \t]+
+espace       [ ]+
+nouv_ligne   [ \n]
+
+chiffre      [0-9]
+entier       {chiffre}+
+reel         {entier}("."{entier})
+caractere    [a-zA-Z0-9_]
+
+numl         \n
+
+chaine       \"({caractere}*|\n|\\|\"|{espace}*)*\"
+
+commentaire  "/*"([^\*\/]*{nouv_ligne}*[^\*\/]*)*"*/"
+
+%%
+
+"never"      { printf("%s", yytext); return (NEVER); }
+"if"         { printf("%s", yytext); return (IF); }
+"fi"         { printf("%s", yytext); 
+               return (FI); }
+"->"         { printf("%s", yytext); return (IMPLIES); }
+"goto"       { printf("%s", yytext); return (GOTO); }
+"&&"         { printf("%s", yytext); return (AND); }
+"||"         { printf("%s", yytext); return (OR); }
+"!"          { printf("%s", yytext); return (NOT); }
+"("          { printf("%s", yytext); return (LEFT_PAR); }
+")"          { printf("%s", yytext); return (RIGHT_PAR); }
+"::"         { printf("%s", yytext); return (CASE); }
+":"          { printf("%s", yytext); return (COLON); }
+";"          { printf("%s", yytext); return (SEMI_COLON); }
+"1"          { printf("%s", yytext); return (CASE_TRUE); }
+"{"          { printf("%s", yytext); return (LEFT_BRACE); }
+"}"          { printf("%s", yytext); return (RIGHT_BRACE); }
+
+
+{commentaire}             { printf(" ");}
+
+{blancs}                  { printf("%s",yytext); }
+
+
+{reel}                    { printf("%s",yytext); 
+                            sscanf(yytext,"%lf",&yylval.real); 
+                            return (LITT_REEL); }
+
+{entier}                  { printf("%s",yytext); 
+                            sscanf(yytext,"%d",&yylval.integer); 
+                            return (LITT_ENT); }
+
+{chaine}                  { printf("%s",yytext);  
+                            yylval.string=(char *)malloc(strlen(yytext)+1);
+                            sscanf(yytext,"%s",yylval.string); 
+                            return (LITT_CHAINE); }
+
+[a-zA-Z]{caractere}*      { printf("%s",yytext); 
+                           yylval.string=(char *)malloc(strlen(yytext)+1);
+                           sscanf(yytext,"%s",yylval.string);
+                           return (ID); }
+                  
+{numl}                    { printf("\n"); }
+
+.                         { printf("caractère inconnu\n"); }
+
+%%
+
+
diff --git a/src/xbt/automaton/parserPromela.yacc b/src/xbt/automaton/parserPromela.yacc
new file mode 100644 (file)
index 0000000..36fd2c0
--- /dev/null
@@ -0,0 +1,78 @@
+%{
+
+  //#include "../../../include/xbt/automatonparse_promela.h"
+  //#include "../../../include/xbt/automaton.h"
+#include "automaton_parse.yy.c"
+#include <xbt/automaton.h>
+#include <xbt/automatonparse_promela.h>
+
+void yyerror(const char *s);
+
+%}
+
+%union{
+  double real;
+  int integer;
+  char* string;
+  xbt_exp_label_t label;
+}
+
+%token NEVER
+%token IF
+%token FI
+%token IMPLIES
+%token GOTO
+%token AND
+%token OR
+%token NOT
+%token LEFT_PAR
+%token RIGHT_PAR
+%token CASE
+%token COLON
+%token SEMI_COLON
+%token CASE_TRUE
+%token LEFT_BRACE
+%token RIGHT_BRACE
+%token <integer> LITT_ENT
+%token <string> LITT_CHAINE
+%token <real> LITT_REEL
+%token <string> ID
+
+%type <label> exp;
+
+%start automaton
+
+%left AND OR
+%nonassoc NOT
+
+%%
+
+automaton : NEVER LEFT_BRACE stateseq RIGHT_BRACE 
+          ;
+
+stateseq : 
+         | ID COLON { new_state($1, 1);} IF option FI SEMI_COLON stateseq 
+         ;
+
+option :
+       | CASE exp IMPLIES GOTO ID option { new_transition($5, $2);}
+       ;
+
+exp : LEFT_PAR exp RIGHT_PAR { $$ = $2; }
+    | exp OR exp { $$ = new_label(0, $1, $3); }
+    | exp AND exp { $$ = new_label(1, $1, $3); }
+    | NOT exp { $$ = new_label(2, $2); }
+    | CASE_TRUE { $$ = new_label(4); }
+    | ID { $$ = new_label(3, $1); }
+    ;
+%%
+
+
+
+void yyerror(const char *s){
+  fprintf (stderr, "%s\n", s);
+}
+
+
+
diff --git a/src/xbt/automaton/y.tab.c b/src/xbt/automaton/y.tab.c
new file mode 100644 (file)
index 0000000..f5b9049
--- /dev/null
@@ -0,0 +1,1719 @@
+/* A Bison parser, made by GNU Bison 2.5.  */
+
+/* Bison implementation for Yacc-like parsers in C
+   
+      Copyright (C) 1984, 1989-1990, 2000-2011 Free Software Foundation, Inc.
+   
+   This program 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 3 of the License, or
+   (at your option) any later version.
+   
+   This program 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, see <http://www.gnu.org/licenses/>.  */
+
+/* As a special exception, you may create a larger work that contains
+   part or all of the Bison parser skeleton and distribute that work
+   under terms of your choice, so long as that work isn't itself a
+   parser generator using the skeleton or a modified version thereof
+   as a parser skeleton.  Alternatively, if you modify or redistribute
+   the parser skeleton itself, you may (at your option) remove this
+   special exception, which will cause the skeleton and the resulting
+   Bison output files to be licensed under the GNU General Public
+   License without this special exception.
+   
+   This special exception was added by the Free Software Foundation in
+   version 2.2 of Bison.  */
+
+/* C LALR(1) parser skeleton written by Richard Stallman, by
+   simplifying the original so-called "semantic" parser.  */
+
+/* All symbols defined below should begin with yy or YY, to avoid
+   infringing on user name space.  This should be done even for local
+   variables, as they might otherwise be expanded by user macros.
+   There are some unavoidable exceptions within include files to
+   define necessary library symbols; they are noted "INFRINGES ON
+   USER NAME SPACE" below.  */
+
+/* Identify Bison output.  */
+#define YYBISON 1
+
+/* Bison version.  */
+#define YYBISON_VERSION "2.5"
+
+/* Skeleton name.  */
+#define YYSKELETON_NAME "yacc.c"
+
+/* Pure parsers.  */
+#define YYPURE 0
+
+/* Push parsers.  */
+#define YYPUSH 0
+
+/* Pull parsers.  */
+#define YYPULL 1
+
+/* Using locations.  */
+#define YYLSP_NEEDED 0
+
+
+
+/* Copy the first part of user declarations.  */
+
+/* Line 268 of yacc.c  */
+#line 1 "parserPromela.yacc"
+
+
+  //#include "../../../include/xbt/automatonparse_promela.h"
+  //#include "../../../include/xbt/automaton.h"
+#include "automaton_parse.yy.c"
+#include <xbt/automaton.h>
+#include <xbt/automatonparse_promela.h>
+
+void yyerror(const char *s);
+
+
+
+/* Line 268 of yacc.c  */
+#line 84 "y.tab.c"
+
+/* Enabling traces.  */
+#ifndef YYDEBUG
+# define YYDEBUG 0
+#endif
+
+/* Enabling verbose error messages.  */
+#ifdef YYERROR_VERBOSE
+# undef YYERROR_VERBOSE
+# define YYERROR_VERBOSE 1
+#else
+# define YYERROR_VERBOSE 0
+#endif
+
+/* Enabling the token table.  */
+#ifndef YYTOKEN_TABLE
+# define YYTOKEN_TABLE 0
+#endif
+
+
+/* Tokens.  */
+#ifndef YYTOKENTYPE
+# define YYTOKENTYPE
+   /* Put the tokens into the symbol table, so that GDB and other debuggers
+      know about them.  */
+   enum yytokentype {
+     NEVER = 258,
+     IF = 259,
+     FI = 260,
+     IMPLIES = 261,
+     GOTO = 262,
+     AND = 263,
+     OR = 264,
+     NOT = 265,
+     LEFT_PAR = 266,
+     RIGHT_PAR = 267,
+     CASE = 268,
+     COLON = 269,
+     SEMI_COLON = 270,
+     CASE_TRUE = 271,
+     LEFT_BRACE = 272,
+     RIGHT_BRACE = 273,
+     LITT_ENT = 274,
+     LITT_CHAINE = 275,
+     LITT_REEL = 276,
+     ID = 277
+   };
+#endif
+/* Tokens.  */
+#define NEVER 258
+#define IF 259
+#define FI 260
+#define IMPLIES 261
+#define GOTO 262
+#define AND 263
+#define OR 264
+#define NOT 265
+#define LEFT_PAR 266
+#define RIGHT_PAR 267
+#define CASE 268
+#define COLON 269
+#define SEMI_COLON 270
+#define CASE_TRUE 271
+#define LEFT_BRACE 272
+#define RIGHT_BRACE 273
+#define LITT_ENT 274
+#define LITT_CHAINE 275
+#define LITT_REEL 276
+#define ID 277
+
+
+
+
+#if ! defined YYSTYPE && ! defined YYSTYPE_IS_DECLARED
+typedef union YYSTYPE
+{
+
+/* Line 293 of yacc.c  */
+#line 13 "parserPromela.yacc"
+
+  double real;
+  int integer;
+  char* string;
+  xbt_exp_label_t label;
+
+
+
+/* Line 293 of yacc.c  */
+#line 173 "y.tab.c"
+} YYSTYPE;
+# define YYSTYPE_IS_TRIVIAL 1
+# define yystype YYSTYPE /* obsolescent; will be withdrawn */
+# define YYSTYPE_IS_DECLARED 1
+#endif
+
+
+/* Copy the second part of user declarations.  */
+
+
+/* Line 343 of yacc.c  */
+#line 185 "y.tab.c"
+
+#ifdef short
+# undef short
+#endif
+
+#ifdef YYTYPE_UINT8
+typedef YYTYPE_UINT8 yytype_uint8;
+#else
+typedef unsigned char yytype_uint8;
+#endif
+
+#ifdef YYTYPE_INT8
+typedef YYTYPE_INT8 yytype_int8;
+#elif (defined __STDC__ || defined __C99__FUNC__ \
+     || defined __cplusplus || defined _MSC_VER)
+typedef signed char yytype_int8;
+#else
+typedef short int yytype_int8;
+#endif
+
+#ifdef YYTYPE_UINT16
+typedef YYTYPE_UINT16 yytype_uint16;
+#else
+typedef unsigned short int yytype_uint16;
+#endif
+
+#ifdef YYTYPE_INT16
+typedef YYTYPE_INT16 yytype_int16;
+#else
+typedef short int yytype_int16;
+#endif
+
+#ifndef YYSIZE_T
+# ifdef __SIZE_TYPE__
+#  define YYSIZE_T __SIZE_TYPE__
+# elif defined size_t
+#  define YYSIZE_T size_t
+# elif ! defined YYSIZE_T && (defined __STDC__ || defined __C99__FUNC__ \
+     || defined __cplusplus || defined _MSC_VER)
+#  include <stddef.h> /* INFRINGES ON USER NAME SPACE */
+#  define YYSIZE_T size_t
+# else
+#  define YYSIZE_T unsigned int
+# endif
+#endif
+
+#define YYSIZE_MAXIMUM ((YYSIZE_T) -1)
+
+#ifndef YY_
+# if defined YYENABLE_NLS && YYENABLE_NLS
+#  if ENABLE_NLS
+#   include <libintl.h> /* INFRINGES ON USER NAME SPACE */
+#   define YY_(msgid) dgettext ("bison-runtime", msgid)
+#  endif
+# endif
+# ifndef YY_
+#  define YY_(msgid) msgid
+# endif
+#endif
+
+/* Suppress unused-variable warnings by "using" E.  */
+#if ! defined lint || defined __GNUC__
+# define YYUSE(e) ((void) (e))
+#else
+# define YYUSE(e) /* empty */
+#endif
+
+/* Identity function, used to suppress warnings about constant conditions.  */
+#ifndef lint
+# define YYID(n) (n)
+#else
+#if (defined __STDC__ || defined __C99__FUNC__ \
+     || defined __cplusplus || defined _MSC_VER)
+static int
+YYID (int yyi)
+#else
+static int
+YYID (yyi)
+    int yyi;
+#endif
+{
+  return yyi;
+}
+#endif
+
+#if ! defined yyoverflow || YYERROR_VERBOSE
+
+/* The parser invokes alloca or malloc; define the necessary symbols.  */
+
+# ifdef YYSTACK_USE_ALLOCA
+#  if YYSTACK_USE_ALLOCA
+#   ifdef __GNUC__
+#    define YYSTACK_ALLOC __builtin_alloca
+#   elif defined __BUILTIN_VA_ARG_INCR
+#    include <alloca.h> /* INFRINGES ON USER NAME SPACE */
+#   elif defined _AIX
+#    define YYSTACK_ALLOC __alloca
+#   elif defined _MSC_VER
+#    include <malloc.h> /* INFRINGES ON USER NAME SPACE */
+#    define alloca _alloca
+#   else
+#    define YYSTACK_ALLOC alloca
+#    if ! defined _ALLOCA_H && ! defined EXIT_SUCCESS && (defined __STDC__ || defined __C99__FUNC__ \
+     || defined __cplusplus || defined _MSC_VER)
+#     include <stdlib.h> /* INFRINGES ON USER NAME SPACE */
+#     ifndef EXIT_SUCCESS
+#      define EXIT_SUCCESS 0
+#     endif
+#    endif
+#   endif
+#  endif
+# endif
+
+# ifdef YYSTACK_ALLOC
+   /* Pacify GCC's `empty if-body' warning.  */
+#  define YYSTACK_FREE(Ptr) do { /* empty */; } while (YYID (0))
+#  ifndef YYSTACK_ALLOC_MAXIMUM
+    /* The OS might guarantee only one guard page at the bottom of the stack,
+       and a page size can be as small as 4096 bytes.  So we cannot safely
+       invoke alloca (N) if N exceeds 4096.  Use a slightly smaller number
+       to allow for a few compiler-allocated temporary stack slots.  */
+#   define YYSTACK_ALLOC_MAXIMUM 4032 /* reasonable circa 2006 */
+#  endif
+# else
+#  define YYSTACK_ALLOC YYMALLOC
+#  define YYSTACK_FREE YYFREE
+#  ifndef YYSTACK_ALLOC_MAXIMUM
+#   define YYSTACK_ALLOC_MAXIMUM YYSIZE_MAXIMUM
+#  endif
+#  if (defined __cplusplus && ! defined EXIT_SUCCESS \
+       && ! ((defined YYMALLOC || defined malloc) \
+            && (defined YYFREE || defined free)))
+#   include <stdlib.h> /* INFRINGES ON USER NAME SPACE */
+#   ifndef EXIT_SUCCESS
+#    define EXIT_SUCCESS 0
+#   endif
+#  endif
+#  ifndef YYMALLOC
+#   define YYMALLOC malloc
+#   if ! defined malloc && ! defined EXIT_SUCCESS && (defined __STDC__ || defined __C99__FUNC__ \
+     || defined __cplusplus || defined _MSC_VER)
+void *malloc (YYSIZE_T); /* INFRINGES ON USER NAME SPACE */
+#   endif
+#  endif
+#  ifndef YYFREE
+#   define YYFREE free
+#   if ! defined free && ! defined EXIT_SUCCESS && (defined __STDC__ || defined __C99__FUNC__ \
+     || defined __cplusplus || defined _MSC_VER)
+void free (void *); /* INFRINGES ON USER NAME SPACE */
+#   endif
+#  endif
+# endif
+#endif /* ! defined yyoverflow || YYERROR_VERBOSE */
+
+
+#if (! defined yyoverflow \
+     && (! defined __cplusplus \
+        || (defined YYSTYPE_IS_TRIVIAL && YYSTYPE_IS_TRIVIAL)))
+
+/* A type that is properly aligned for any stack member.  */
+union yyalloc
+{
+  yytype_int16 yyss_alloc;
+  YYSTYPE yyvs_alloc;
+};
+
+/* The size of the maximum gap between one aligned stack and the next.  */
+# define YYSTACK_GAP_MAXIMUM (sizeof (union yyalloc) - 1)
+
+/* The size of an array large to enough to hold all stacks, each with
+   N elements.  */
+# define YYSTACK_BYTES(N) \
+     ((N) * (sizeof (yytype_int16) + sizeof (YYSTYPE)) \
+      + YYSTACK_GAP_MAXIMUM)
+
+# define YYCOPY_NEEDED 1
+
+/* Relocate STACK from its old location to the new one.  The
+   local variables YYSIZE and YYSTACKSIZE give the old and new number of
+   elements in the stack, and YYPTR gives the new location of the
+   stack.  Advance YYPTR to a properly aligned location for the next
+   stack.  */
+# define YYSTACK_RELOCATE(Stack_alloc, Stack)                          \
+    do                                                                 \
+      {                                                                        \
+       YYSIZE_T yynewbytes;                                            \
+       YYCOPY (&yyptr->Stack_alloc, Stack, yysize);                    \
+       Stack = &yyptr->Stack_alloc;                                    \
+       yynewbytes = yystacksize * sizeof (*Stack) + YYSTACK_GAP_MAXIMUM; \
+       yyptr += yynewbytes / sizeof (*yyptr);                          \
+      }                                                                        \
+    while (YYID (0))
+
+#endif
+
+#if defined YYCOPY_NEEDED && YYCOPY_NEEDED
+/* Copy COUNT objects from FROM to TO.  The source and destination do
+   not overlap.  */
+# ifndef YYCOPY
+#  if defined __GNUC__ && 1 < __GNUC__
+#   define YYCOPY(To, From, Count) \
+      __builtin_memcpy (To, From, (Count) * sizeof (*(From)))
+#  else
+#   define YYCOPY(To, From, Count)             \
+      do                                       \
+       {                                       \
+         YYSIZE_T yyi;                         \
+         for (yyi = 0; yyi < (Count); yyi++)   \
+           (To)[yyi] = (From)[yyi];            \
+       }                                       \
+      while (YYID (0))
+#  endif
+# endif
+#endif /* !YYCOPY_NEEDED */
+
+/* YYFINAL -- State number of the termination state.  */
+#define YYFINAL  4
+/* YYLAST -- Last index in YYTABLE.  */
+#define YYLAST   28
+
+/* YYNTOKENS -- Number of terminals.  */
+#define YYNTOKENS  23
+/* YYNNTS -- Number of nonterminals.  */
+#define YYNNTS  6
+/* YYNRULES -- Number of rules.  */
+#define YYNRULES  13
+/* YYNRULES -- Number of states.  */
+#define YYNSTATES  32
+
+/* YYTRANSLATE(YYLEX) -- Bison symbol number corresponding to YYLEX.  */
+#define YYUNDEFTOK  2
+#define YYMAXUTOK   277
+
+#define YYTRANSLATE(YYX)                                               \
+  ((unsigned int) (YYX) <= YYMAXUTOK ? yytranslate[YYX] : YYUNDEFTOK)
+
+/* YYTRANSLATE[YYLEX] -- Bison symbol number corresponding to YYLEX.  */
+static const yytype_uint8 yytranslate[] =
+{
+       0,     2,     2,     2,     2,     2,     2,     2,     2,     2,
+       2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
+       2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
+       2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
+       2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
+       2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
+       2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
+       2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
+       2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
+       2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
+       2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
+       2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
+       2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
+       2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
+       2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
+       2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
+       2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
+       2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
+       2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
+       2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
+       2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
+       2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
+       2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
+       2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
+       2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
+       2,     2,     2,     2,     2,     2,     1,     2,     3,     4,
+       5,     6,     7,     8,     9,    10,    11,    12,    13,    14,
+      15,    16,    17,    18,    19,    20,    21,    22
+};
+
+#if YYDEBUG
+/* YYPRHS[YYN] -- Index of the first RHS symbol of rule number YYN in
+   YYRHS.  */
+static const yytype_uint8 yyprhs[] =
+{
+       0,     0,     3,     8,     9,    10,    19,    20,    27,    31,
+      35,    39,    42,    44
+};
+
+/* YYRHS -- A `-1'-separated list of the rules' RHS.  */
+static const yytype_int8 yyrhs[] =
+{
+      24,     0,    -1,     3,    17,    25,    18,    -1,    -1,    -1,
+      22,    14,    26,     4,    27,     5,    15,    25,    -1,    -1,
+      13,    28,     6,     7,    22,    27,    -1,    11,    28,    12,
+      -1,    28,     9,    28,    -1,    28,     8,    28,    -1,    10,
+      28,    -1,    16,    -1,    22,    -1
+};
+
+/* YYRLINE[YYN] -- source line where rule number YYN was defined.  */
+static const yytype_uint8 yyrline[] =
+{
+       0,    50,    50,    53,    54,    54,    57,    58,    61,    62,
+      63,    64,    65,    66
+};
+#endif
+
+#if YYDEBUG || YYERROR_VERBOSE || YYTOKEN_TABLE
+/* YYTNAME[SYMBOL-NUM] -- String name of the symbol SYMBOL-NUM.
+   First, the terminals, then, starting at YYNTOKENS, nonterminals.  */
+static const char *const yytname[] =
+{
+  "$end", "error", "$undefined", "NEVER", "IF", "FI", "IMPLIES", "GOTO",
+  "AND", "OR", "NOT", "LEFT_PAR", "RIGHT_PAR", "CASE", "COLON",
+  "SEMI_COLON", "CASE_TRUE", "LEFT_BRACE", "RIGHT_BRACE", "LITT_ENT",
+  "LITT_CHAINE", "LITT_REEL", "ID", "$accept", "automaton", "stateseq",
+  "$@1", "option", "exp", 0
+};
+#endif
+
+# ifdef YYPRINT
+/* YYTOKNUM[YYLEX-NUM] -- Internal token number corresponding to
+   token YYLEX-NUM.  */
+static const yytype_uint16 yytoknum[] =
+{
+       0,   256,   257,   258,   259,   260,   261,   262,   263,   264,
+     265,   266,   267,   268,   269,   270,   271,   272,   273,   274,
+     275,   276,   277
+};
+# endif
+
+/* YYR1[YYN] -- Symbol number of symbol that rule YYN derives.  */
+static const yytype_uint8 yyr1[] =
+{
+       0,    23,    24,    25,    26,    25,    27,    27,    28,    28,
+      28,    28,    28,    28
+};
+
+/* YYR2[YYN] -- Number of symbols composing right hand side of rule YYN.  */
+static const yytype_uint8 yyr2[] =
+{
+       0,     2,     4,     0,     0,     8,     0,     6,     3,     3,
+       3,     2,     1,     1
+};
+
+/* YYDEFACT[STATE-NAME] -- Default reduction number in state STATE-NUM.
+   Performed when YYTABLE doesn't specify something else to do.  Zero
+   means the default is an error.  */
+static const yytype_uint8 yydefact[] =
+{
+       0,     0,     0,     3,     1,     0,     0,     4,     2,     0,
+       6,     0,     0,     0,     0,    12,    13,     0,     0,    11,
+       0,     0,     0,     0,     3,     8,     0,    10,     9,     5,
+       6,     7
+};
+
+/* YYDEFGOTO[NTERM-NUM].  */
+static const yytype_int8 yydefgoto[] =
+{
+      -1,     2,     6,     9,    12,    17
+};
+
+/* YYPACT[STATE-NUM] -- Index in YYTABLE of the portion describing
+   STATE-NUM.  */
+#define YYPACT_NINF -16
+static const yytype_int8 yypact[] =
+{
+       0,   -15,    10,   -13,   -16,     2,     1,   -16,   -16,    16,
+       8,   -10,    17,   -10,   -10,   -16,   -16,     9,    11,   -16,
+      -1,    18,   -10,   -10,   -13,   -16,     5,   -16,   -16,   -16,
+       8,   -16
+};
+
+/* YYPGOTO[NTERM-NUM].  */
+static const yytype_int8 yypgoto[] =
+{
+     -16,   -16,     4,   -16,    -7,    -9
+};
+
+/* YYTABLE[YYPACT[STATE-NUM]].  What to do in state STATE-NUM.  If
+   positive, shift that token.  If negative, reduce the rule which
+   number is the opposite.  If YYTABLE_NINF, syntax error.  */
+#define YYTABLE_NINF -1
+static const yytype_uint8 yytable[] =
+{
+      13,    14,     3,     1,    19,    20,    15,    22,    23,     5,
+       4,    25,    16,    27,    28,    21,     7,    22,    23,     8,
+      10,    11,    18,    31,     0,    26,    24,    30,    29
+};
+
+#define yypact_value_is_default(yystate) \
+  ((yystate) == (-16))
+
+#define yytable_value_is_error(yytable_value) \
+  YYID (0)
+
+static const yytype_int8 yycheck[] =
+{
+      10,    11,    17,     3,    13,    14,    16,     8,     9,    22,
+       0,    12,    22,    22,    23,     6,    14,     8,     9,    18,
+       4,    13,     5,    30,    -1,     7,    15,    22,    24
+};
+
+/* YYSTOS[STATE-NUM] -- The (internal number of the) accessing
+   symbol of state STATE-NUM.  */
+static const yytype_uint8 yystos[] =
+{
+       0,     3,    24,    17,     0,    22,    25,    14,    18,    26,
+       4,    13,    27,    10,    11,    16,    22,    28,     5,    28,
+      28,     6,     8,     9,    15,    12,     7,    28,    28,    25,
+      22,    27
+};
+
+#define yyerrok                (yyerrstatus = 0)
+#define yyclearin      (yychar = YYEMPTY)
+#define YYEMPTY                (-2)
+#define YYEOF          0
+
+#define YYACCEPT       goto yyacceptlab
+#define YYABORT                goto yyabortlab
+#define YYERROR                goto yyerrorlab
+
+
+/* Like YYERROR except do call yyerror.  This remains here temporarily
+   to ease the transition to the new meaning of YYERROR, for GCC.
+   Once GCC version 2 has supplanted version 1, this can go.  However,
+   YYFAIL appears to be in use.  Nevertheless, it is formally deprecated
+   in Bison 2.4.2's NEWS entry, where a plan to phase it out is
+   discussed.  */
+
+#define YYFAIL         goto yyerrlab
+#if defined YYFAIL
+  /* This is here to suppress warnings from the GCC cpp's
+     -Wunused-macros.  Normally we don't worry about that warning, but
+     some users do, and we want to make it easy for users to remove
+     YYFAIL uses, which will produce warnings from Bison 2.5.  */
+#endif
+
+#define YYRECOVERING()  (!!yyerrstatus)
+
+#define YYBACKUP(Token, Value)                                 \
+do                                                             \
+  if (yychar == YYEMPTY && yylen == 1)                         \
+    {                                                          \
+      yychar = (Token);                                                \
+      yylval = (Value);                                                \
+      YYPOPSTACK (1);                                          \
+      goto yybackup;                                           \
+    }                                                          \
+  else                                                         \
+    {                                                          \
+      yyerror (YY_("syntax error: cannot back up")); \
+      YYERROR;                                                 \
+    }                                                          \
+while (YYID (0))
+
+
+#define YYTERROR       1
+#define YYERRCODE      256
+
+
+/* YYLLOC_DEFAULT -- Set CURRENT to span from RHS[1] to RHS[N].
+   If N is 0, then set CURRENT to the empty location which ends
+   the previous symbol: RHS[0] (always defined).  */
+
+#define YYRHSLOC(Rhs, K) ((Rhs)[K])
+#ifndef YYLLOC_DEFAULT
+# define YYLLOC_DEFAULT(Current, Rhs, N)                               \
+    do                                                                 \
+      if (YYID (N))                                                    \
+       {                                                               \
+         (Current).first_line   = YYRHSLOC (Rhs, 1).first_line;        \
+         (Current).first_column = YYRHSLOC (Rhs, 1).first_column;      \
+         (Current).last_line    = YYRHSLOC (Rhs, N).last_line;         \
+         (Current).last_column  = YYRHSLOC (Rhs, N).last_column;       \
+       }                                                               \
+      else                                                             \
+       {                                                               \
+         (Current).first_line   = (Current).last_line   =              \
+           YYRHSLOC (Rhs, 0).last_line;                                \
+         (Current).first_column = (Current).last_column =              \
+           YYRHSLOC (Rhs, 0).last_column;                              \
+       }                                                               \
+    while (YYID (0))
+#endif
+
+
+/* This macro is provided for backward compatibility. */
+
+#ifndef YY_LOCATION_PRINT
+# define YY_LOCATION_PRINT(File, Loc) ((void) 0)
+#endif
+
+
+/* YYLEX -- calling `yylex' with the right arguments.  */
+
+#ifdef YYLEX_PARAM
+# define YYLEX yylex (YYLEX_PARAM)
+#else
+# define YYLEX yylex ()
+#endif
+
+/* Enable debugging if requested.  */
+#if YYDEBUG
+
+# ifndef YYFPRINTF
+#  include <stdio.h> /* INFRINGES ON USER NAME SPACE */
+#  define YYFPRINTF fprintf
+# endif
+
+# define YYDPRINTF(Args)                       \
+do {                                           \
+  if (yydebug)                                 \
+    YYFPRINTF Args;                            \
+} while (YYID (0))
+
+# define YY_SYMBOL_PRINT(Title, Type, Value, Location)                   \
+do {                                                                     \
+  if (yydebug)                                                           \
+    {                                                                    \
+      YYFPRINTF (stderr, "%s ", Title);                                          \
+      yy_symbol_print (stderr,                                           \
+                 Type, Value); \
+      YYFPRINTF (stderr, "\n");                                                  \
+    }                                                                    \
+} while (YYID (0))
+
+
+/*--------------------------------.
+| Print this symbol on YYOUTPUT.  |
+`--------------------------------*/
+
+/*ARGSUSED*/
+#if (defined __STDC__ || defined __C99__FUNC__ \
+     || defined __cplusplus || defined _MSC_VER)
+static void
+yy_symbol_value_print (FILE *yyoutput, int yytype, YYSTYPE const * const yyvaluep)
+#else
+static void
+yy_symbol_value_print (yyoutput, yytype, yyvaluep)
+    FILE *yyoutput;
+    int yytype;
+    YYSTYPE const * const yyvaluep;
+#endif
+{
+  if (!yyvaluep)
+    return;
+# ifdef YYPRINT
+  if (yytype < YYNTOKENS)
+    YYPRINT (yyoutput, yytoknum[yytype], *yyvaluep);
+# else
+  YYUSE (yyoutput);
+# endif
+  switch (yytype)
+    {
+      default:
+       break;
+    }
+}
+
+
+/*--------------------------------.
+| Print this symbol on YYOUTPUT.  |
+`--------------------------------*/
+
+#if (defined __STDC__ || defined __C99__FUNC__ \
+     || defined __cplusplus || defined _MSC_VER)
+static void
+yy_symbol_print (FILE *yyoutput, int yytype, YYSTYPE const * const yyvaluep)
+#else
+static void
+yy_symbol_print (yyoutput, yytype, yyvaluep)
+    FILE *yyoutput;
+    int yytype;
+    YYSTYPE const * const yyvaluep;
+#endif
+{
+  if (yytype < YYNTOKENS)
+    YYFPRINTF (yyoutput, "token %s (", yytname[yytype]);
+  else
+    YYFPRINTF (yyoutput, "nterm %s (", yytname[yytype]);
+
+  yy_symbol_value_print (yyoutput, yytype, yyvaluep);
+  YYFPRINTF (yyoutput, ")");
+}
+
+/*------------------------------------------------------------------.
+| yy_stack_print -- Print the state stack from its BOTTOM up to its |
+| TOP (included).                                                   |
+`------------------------------------------------------------------*/
+
+#if (defined __STDC__ || defined __C99__FUNC__ \
+     || defined __cplusplus || defined _MSC_VER)
+static void
+yy_stack_print (yytype_int16 *yybottom, yytype_int16 *yytop)
+#else
+static void
+yy_stack_print (yybottom, yytop)
+    yytype_int16 *yybottom;
+    yytype_int16 *yytop;
+#endif
+{
+  YYFPRINTF (stderr, "Stack now");
+  for (; yybottom <= yytop; yybottom++)
+    {
+      int yybot = *yybottom;
+      YYFPRINTF (stderr, " %d", yybot);
+    }
+  YYFPRINTF (stderr, "\n");
+}
+
+# define YY_STACK_PRINT(Bottom, Top)                           \
+do {                                                           \
+  if (yydebug)                                                 \
+    yy_stack_print ((Bottom), (Top));                          \
+} while (YYID (0))
+
+
+/*------------------------------------------------.
+| Report that the YYRULE is going to be reduced.  |
+`------------------------------------------------*/
+
+#if (defined __STDC__ || defined __C99__FUNC__ \
+     || defined __cplusplus || defined _MSC_VER)
+static void
+yy_reduce_print (YYSTYPE *yyvsp, int yyrule)
+#else
+static void
+yy_reduce_print (yyvsp, yyrule)
+    YYSTYPE *yyvsp;
+    int yyrule;
+#endif
+{
+  int yynrhs = yyr2[yyrule];
+  int yyi;
+  unsigned long int yylno = yyrline[yyrule];
+  YYFPRINTF (stderr, "Reducing stack by rule %d (line %lu):\n",
+            yyrule - 1, yylno);
+  /* The symbols being reduced.  */
+  for (yyi = 0; yyi < yynrhs; yyi++)
+    {
+      YYFPRINTF (stderr, "   $%d = ", yyi + 1);
+      yy_symbol_print (stderr, yyrhs[yyprhs[yyrule] + yyi],
+                      &(yyvsp[(yyi + 1) - (yynrhs)])
+                                      );
+      YYFPRINTF (stderr, "\n");
+    }
+}
+
+# define YY_REDUCE_PRINT(Rule)         \
+do {                                   \
+  if (yydebug)                         \
+    yy_reduce_print (yyvsp, Rule); \
+} while (YYID (0))
+
+/* Nonzero means print parse trace.  It is left uninitialized so that
+   multiple parsers can coexist.  */
+int yydebug;
+#else /* !YYDEBUG */
+# define YYDPRINTF(Args)
+# define YY_SYMBOL_PRINT(Title, Type, Value, Location)
+# define YY_STACK_PRINT(Bottom, Top)
+# define YY_REDUCE_PRINT(Rule)
+#endif /* !YYDEBUG */
+
+
+/* YYINITDEPTH -- initial size of the parser's stacks.  */
+#ifndef        YYINITDEPTH
+# define YYINITDEPTH 200
+#endif
+
+/* YYMAXDEPTH -- maximum size the stacks can grow to (effective only
+   if the built-in stack extension method is used).
+
+   Do not make this value too large; the results are undefined if
+   YYSTACK_ALLOC_MAXIMUM < YYSTACK_BYTES (YYMAXDEPTH)
+   evaluated with infinite-precision integer arithmetic.  */
+
+#ifndef YYMAXDEPTH
+# define YYMAXDEPTH 10000
+#endif
+
+
+#if YYERROR_VERBOSE
+
+# ifndef yystrlen
+#  if defined __GLIBC__ && defined _STRING_H
+#   define yystrlen strlen
+#  else
+/* Return the length of YYSTR.  */
+#if (defined __STDC__ || defined __C99__FUNC__ \
+     || defined __cplusplus || defined _MSC_VER)
+static YYSIZE_T
+yystrlen (const char *yystr)
+#else
+static YYSIZE_T
+yystrlen (yystr)
+    const char *yystr;
+#endif
+{
+  YYSIZE_T yylen;
+  for (yylen = 0; yystr[yylen]; yylen++)
+    continue;
+  return yylen;
+}
+#  endif
+# endif
+
+# ifndef yystpcpy
+#  if defined __GLIBC__ && defined _STRING_H && defined _GNU_SOURCE
+#   define yystpcpy stpcpy
+#  else
+/* Copy YYSRC to YYDEST, returning the address of the terminating '\0' in
+   YYDEST.  */
+#if (defined __STDC__ || defined __C99__FUNC__ \
+     || defined __cplusplus || defined _MSC_VER)
+static char *
+yystpcpy (char *yydest, const char *yysrc)
+#else
+static char *
+yystpcpy (yydest, yysrc)
+    char *yydest;
+    const char *yysrc;
+#endif
+{
+  char *yyd = yydest;
+  const char *yys = yysrc;
+
+  while ((*yyd++ = *yys++) != '\0')
+    continue;
+
+  return yyd - 1;
+}
+#  endif
+# endif
+
+# ifndef yytnamerr
+/* Copy to YYRES the contents of YYSTR after stripping away unnecessary
+   quotes and backslashes, so that it's suitable for yyerror.  The
+   heuristic is that double-quoting is unnecessary unless the string
+   contains an apostrophe, a comma, or backslash (other than
+   backslash-backslash).  YYSTR is taken from yytname.  If YYRES is
+   null, do not copy; instead, return the length of what the result
+   would have been.  */
+static YYSIZE_T
+yytnamerr (char *yyres, const char *yystr)
+{
+  if (*yystr == '"')
+    {
+      YYSIZE_T yyn = 0;
+      char const *yyp = yystr;
+
+      for (;;)
+       switch (*++yyp)
+         {
+         case '\'':
+         case ',':
+           goto do_not_strip_quotes;
+
+         case '\\':
+           if (*++yyp != '\\')
+             goto do_not_strip_quotes;
+           /* Fall through.  */
+         default:
+           if (yyres)
+             yyres[yyn] = *yyp;
+           yyn++;
+           break;
+
+         case '"':
+           if (yyres)
+             yyres[yyn] = '\0';
+           return yyn;
+         }
+    do_not_strip_quotes: ;
+    }
+
+  if (! yyres)
+    return yystrlen (yystr);
+
+  return yystpcpy (yyres, yystr) - yyres;
+}
+# endif
+
+/* Copy into *YYMSG, which is of size *YYMSG_ALLOC, an error message
+   about the unexpected token YYTOKEN for the state stack whose top is
+   YYSSP.
+
+   Return 0 if *YYMSG was successfully written.  Return 1 if *YYMSG is
+   not large enough to hold the message.  In that case, also set
+   *YYMSG_ALLOC to the required number of bytes.  Return 2 if the
+   required number of bytes is too large to store.  */
+static int
+yysyntax_error (YYSIZE_T *yymsg_alloc, char **yymsg,
+                yytype_int16 *yyssp, int yytoken)
+{
+  YYSIZE_T yysize0 = yytnamerr (0, yytname[yytoken]);
+  YYSIZE_T yysize = yysize0;
+  YYSIZE_T yysize1;
+  enum { YYERROR_VERBOSE_ARGS_MAXIMUM = 5 };
+  /* Internationalized format string. */
+  const char *yyformat = 0;
+  /* Arguments of yyformat. */
+  char const *yyarg[YYERROR_VERBOSE_ARGS_MAXIMUM];
+  /* Number of reported tokens (one for the "unexpected", one per
+     "expected"). */
+  int yycount = 0;
+
+  /* There are many possibilities here to consider:
+     - Assume YYFAIL is not used.  It's too flawed to consider.  See
+       <http://lists.gnu.org/archive/html/bison-patches/2009-12/msg00024.html>
+       for details.  YYERROR is fine as it does not invoke this
+       function.
+     - If this state is a consistent state with a default action, then
+       the only way this function was invoked is if the default action
+       is an error action.  In that case, don't check for expected
+       tokens because there are none.
+     - The only way there can be no lookahead present (in yychar) is if
+       this state is a consistent state with a default action.  Thus,
+       detecting the absence of a lookahead is sufficient to determine
+       that there is no unexpected or expected token to report.  In that
+       case, just report a simple "syntax error".
+     - Don't assume there isn't a lookahead just because this state is a
+       consistent state with a default action.  There might have been a
+       previous inconsistent state, consistent state with a non-default
+       action, or user semantic action that manipulated yychar.
+     - Of course, the expected token list depends on states to have
+       correct lookahead information, and it depends on the parser not
+       to perform extra reductions after fetching a lookahead from the
+       scanner and before detecting a syntax error.  Thus, state merging
+       (from LALR or IELR) and default reductions corrupt the expected
+       token list.  However, the list is correct for canonical LR with
+       one exception: it will still contain any token that will not be
+       accepted due to an error action in a later state.
+  */
+  if (yytoken != YYEMPTY)
+    {
+      int yyn = yypact[*yyssp];
+      yyarg[yycount++] = yytname[yytoken];
+      if (!yypact_value_is_default (yyn))
+        {
+          /* Start YYX at -YYN if negative to avoid negative indexes in
+             YYCHECK.  In other words, skip the first -YYN actions for
+             this state because they are default actions.  */
+          int yyxbegin = yyn < 0 ? -yyn : 0;
+          /* Stay within bounds of both yycheck and yytname.  */
+          int yychecklim = YYLAST - yyn + 1;
+          int yyxend = yychecklim < YYNTOKENS ? yychecklim : YYNTOKENS;
+          int yyx;
+
+          for (yyx = yyxbegin; yyx < yyxend; ++yyx)
+            if (yycheck[yyx + yyn] == yyx && yyx != YYTERROR
+                && !yytable_value_is_error (yytable[yyx + yyn]))
+              {
+                if (yycount == YYERROR_VERBOSE_ARGS_MAXIMUM)
+                  {
+                    yycount = 1;
+                    yysize = yysize0;
+                    break;
+                  }
+                yyarg[yycount++] = yytname[yyx];
+                yysize1 = yysize + yytnamerr (0, yytname[yyx]);
+                if (! (yysize <= yysize1
+                       && yysize1 <= YYSTACK_ALLOC_MAXIMUM))
+                  return 2;
+                yysize = yysize1;
+              }
+        }
+    }
+
+  switch (yycount)
+    {
+# define YYCASE_(N, S)                      \
+      case N:                               \
+        yyformat = S;                       \
+      break
+      YYCASE_(0, YY_("syntax error"));
+      YYCASE_(1, YY_("syntax error, unexpected %s"));
+      YYCASE_(2, YY_("syntax error, unexpected %s, expecting %s"));
+      YYCASE_(3, YY_("syntax error, unexpected %s, expecting %s or %s"));
+      YYCASE_(4, YY_("syntax error, unexpected %s, expecting %s or %s or %s"));
+      YYCASE_(5, YY_("syntax error, unexpected %s, expecting %s or %s or %s or %s"));
+# undef YYCASE_
+    }
+
+  yysize1 = yysize + yystrlen (yyformat);
+  if (! (yysize <= yysize1 && yysize1 <= YYSTACK_ALLOC_MAXIMUM))
+    return 2;
+  yysize = yysize1;
+
+  if (*yymsg_alloc < yysize)
+    {
+      *yymsg_alloc = 2 * yysize;
+      if (! (yysize <= *yymsg_alloc
+             && *yymsg_alloc <= YYSTACK_ALLOC_MAXIMUM))
+        *yymsg_alloc = YYSTACK_ALLOC_MAXIMUM;
+      return 1;
+    }
+
+  /* Avoid sprintf, as that infringes on the user's name space.
+     Don't have undefined behavior even if the translation
+     produced a string with the wrong number of "%s"s.  */
+  {
+    char *yyp = *yymsg;
+    int yyi = 0;
+    while ((*yyp = *yyformat) != '\0')
+      if (*yyp == '%' && yyformat[1] == 's' && yyi < yycount)
+        {
+          yyp += yytnamerr (yyp, yyarg[yyi++]);
+          yyformat += 2;
+        }
+      else
+        {
+          yyp++;
+          yyformat++;
+        }
+  }
+  return 0;
+}
+#endif /* YYERROR_VERBOSE */
+
+/*-----------------------------------------------.
+| Release the memory associated to this symbol.  |
+`-----------------------------------------------*/
+
+/*ARGSUSED*/
+#if (defined __STDC__ || defined __C99__FUNC__ \
+     || defined __cplusplus || defined _MSC_VER)
+static void
+yydestruct (const char *yymsg, int yytype, YYSTYPE *yyvaluep)
+#else
+static void
+yydestruct (yymsg, yytype, yyvaluep)
+    const char *yymsg;
+    int yytype;
+    YYSTYPE *yyvaluep;
+#endif
+{
+  YYUSE (yyvaluep);
+
+  if (!yymsg)
+    yymsg = "Deleting";
+  YY_SYMBOL_PRINT (yymsg, yytype, yyvaluep, yylocationp);
+
+  switch (yytype)
+    {
+
+      default:
+       break;
+    }
+}
+
+
+/* Prevent warnings from -Wmissing-prototypes.  */
+#ifdef YYPARSE_PARAM
+#if defined __STDC__ || defined __cplusplus
+int yyparse (void *YYPARSE_PARAM);
+#else
+int yyparse ();
+#endif
+#else /* ! YYPARSE_PARAM */
+#if defined __STDC__ || defined __cplusplus
+int yyparse (void);
+#else
+int yyparse ();
+#endif
+#endif /* ! YYPARSE_PARAM */
+
+
+/* The lookahead symbol.  */
+int yychar;
+
+/* The semantic value of the lookahead symbol.  */
+YYSTYPE yylval;
+
+/* Number of syntax errors so far.  */
+int yynerrs;
+
+
+/*----------.
+| yyparse.  |
+`----------*/
+
+#ifdef YYPARSE_PARAM
+#if (defined __STDC__ || defined __C99__FUNC__ \
+     || defined __cplusplus || defined _MSC_VER)
+int
+yyparse (void *YYPARSE_PARAM)
+#else
+int
+yyparse (YYPARSE_PARAM)
+    void *YYPARSE_PARAM;
+#endif
+#else /* ! YYPARSE_PARAM */
+#if (defined __STDC__ || defined __C99__FUNC__ \
+     || defined __cplusplus || defined _MSC_VER)
+int
+yyparse (void)
+#else
+int
+yyparse ()
+
+#endif
+#endif
+{
+    int yystate;
+    /* Number of tokens to shift before error messages enabled.  */
+    int yyerrstatus;
+
+    /* The stacks and their tools:
+       `yyss': related to states.
+       `yyvs': related to semantic values.
+
+       Refer to the stacks thru separate pointers, to allow yyoverflow
+       to reallocate them elsewhere.  */
+
+    /* The state stack.  */
+    yytype_int16 yyssa[YYINITDEPTH];
+    yytype_int16 *yyss;
+    yytype_int16 *yyssp;
+
+    /* The semantic value stack.  */
+    YYSTYPE yyvsa[YYINITDEPTH];
+    YYSTYPE *yyvs;
+    YYSTYPE *yyvsp;
+
+    YYSIZE_T yystacksize;
+
+  int yyn;
+  int yyresult;
+  /* Lookahead token as an internal (translated) token number.  */
+  int yytoken;
+  /* The variables used to return semantic value and location from the
+     action routines.  */
+  YYSTYPE yyval;
+
+#if YYERROR_VERBOSE
+  /* Buffer for error messages, and its allocated size.  */
+  char yymsgbuf[128];
+  char *yymsg = yymsgbuf;
+  YYSIZE_T yymsg_alloc = sizeof yymsgbuf;
+#endif
+
+#define YYPOPSTACK(N)   (yyvsp -= (N), yyssp -= (N))
+
+  /* The number of symbols on the RHS of the reduced rule.
+     Keep to zero when no symbol should be popped.  */
+  int yylen = 0;
+
+  yytoken = 0;
+  yyss = yyssa;
+  yyvs = yyvsa;
+  yystacksize = YYINITDEPTH;
+
+  YYDPRINTF ((stderr, "Starting parse\n"));
+
+  yystate = 0;
+  yyerrstatus = 0;
+  yynerrs = 0;
+  yychar = YYEMPTY; /* Cause a token to be read.  */
+
+  /* Initialize stack pointers.
+     Waste one element of value and location stack
+     so that they stay on the same level as the state stack.
+     The wasted elements are never initialized.  */
+  yyssp = yyss;
+  yyvsp = yyvs;
+
+  goto yysetstate;
+
+/*------------------------------------------------------------.
+| yynewstate -- Push a new state, which is found in yystate.  |
+`------------------------------------------------------------*/
+ yynewstate:
+  /* In all cases, when you get here, the value and location stacks
+     have just been pushed.  So pushing a state here evens the stacks.  */
+  yyssp++;
+
+ yysetstate:
+  *yyssp = yystate;
+
+  if (yyss + yystacksize - 1 <= yyssp)
+    {
+      /* Get the current used size of the three stacks, in elements.  */
+      YYSIZE_T yysize = yyssp - yyss + 1;
+
+#ifdef yyoverflow
+      {
+       /* Give user a chance to reallocate the stack.  Use copies of
+          these so that the &'s don't force the real ones into
+          memory.  */
+       YYSTYPE *yyvs1 = yyvs;
+       yytype_int16 *yyss1 = yyss;
+
+       /* Each stack pointer address is followed by the size of the
+          data in use in that stack, in bytes.  This used to be a
+          conditional around just the two extra args, but that might
+          be undefined if yyoverflow is a macro.  */
+       yyoverflow (YY_("memory exhausted"),
+                   &yyss1, yysize * sizeof (*yyssp),
+                   &yyvs1, yysize * sizeof (*yyvsp),
+                   &yystacksize);
+
+       yyss = yyss1;
+       yyvs = yyvs1;
+      }
+#else /* no yyoverflow */
+# ifndef YYSTACK_RELOCATE
+      goto yyexhaustedlab;
+# else
+      /* Extend the stack our own way.  */
+      if (YYMAXDEPTH <= yystacksize)
+       goto yyexhaustedlab;
+      yystacksize *= 2;
+      if (YYMAXDEPTH < yystacksize)
+       yystacksize = YYMAXDEPTH;
+
+      {
+       yytype_int16 *yyss1 = yyss;
+       union yyalloc *yyptr =
+         (union yyalloc *) YYSTACK_ALLOC (YYSTACK_BYTES (yystacksize));
+       if (! yyptr)
+         goto yyexhaustedlab;
+       YYSTACK_RELOCATE (yyss_alloc, yyss);
+       YYSTACK_RELOCATE (yyvs_alloc, yyvs);
+#  undef YYSTACK_RELOCATE
+       if (yyss1 != yyssa)
+         YYSTACK_FREE (yyss1);
+      }
+# endif
+#endif /* no yyoverflow */
+
+      yyssp = yyss + yysize - 1;
+      yyvsp = yyvs + yysize - 1;
+
+      YYDPRINTF ((stderr, "Stack size increased to %lu\n",
+                 (unsigned long int) yystacksize));
+
+      if (yyss + yystacksize - 1 <= yyssp)
+       YYABORT;
+    }
+
+  YYDPRINTF ((stderr, "Entering state %d\n", yystate));
+
+  if (yystate == YYFINAL)
+    YYACCEPT;
+
+  goto yybackup;
+
+/*-----------.
+| yybackup.  |
+`-----------*/
+yybackup:
+
+  /* Do appropriate processing given the current state.  Read a
+     lookahead token if we need one and don't already have one.  */
+
+  /* First try to decide what to do without reference to lookahead token.  */
+  yyn = yypact[yystate];
+  if (yypact_value_is_default (yyn))
+    goto yydefault;
+
+  /* Not known => get a lookahead token if don't already have one.  */
+
+  /* YYCHAR is either YYEMPTY or YYEOF or a valid lookahead symbol.  */
+  if (yychar == YYEMPTY)
+    {
+      YYDPRINTF ((stderr, "Reading a token: "));
+      yychar = YYLEX;
+    }
+
+  if (yychar <= YYEOF)
+    {
+      yychar = yytoken = YYEOF;
+      YYDPRINTF ((stderr, "Now at end of input.\n"));
+    }
+  else
+    {
+      yytoken = YYTRANSLATE (yychar);
+      YY_SYMBOL_PRINT ("Next token is", yytoken, &yylval, &yylloc);
+    }
+
+  /* If the proper action on seeing token YYTOKEN is to reduce or to
+     detect an error, take that action.  */
+  yyn += yytoken;
+  if (yyn < 0 || YYLAST < yyn || yycheck[yyn] != yytoken)
+    goto yydefault;
+  yyn = yytable[yyn];
+  if (yyn <= 0)
+    {
+      if (yytable_value_is_error (yyn))
+        goto yyerrlab;
+      yyn = -yyn;
+      goto yyreduce;
+    }
+
+  /* Count tokens shifted since error; after three, turn off error
+     status.  */
+  if (yyerrstatus)
+    yyerrstatus--;
+
+  /* Shift the lookahead token.  */
+  YY_SYMBOL_PRINT ("Shifting", yytoken, &yylval, &yylloc);
+
+  /* Discard the shifted token.  */
+  yychar = YYEMPTY;
+
+  yystate = yyn;
+  *++yyvsp = yylval;
+
+  goto yynewstate;
+
+
+/*-----------------------------------------------------------.
+| yydefault -- do the default action for the current state.  |
+`-----------------------------------------------------------*/
+yydefault:
+  yyn = yydefact[yystate];
+  if (yyn == 0)
+    goto yyerrlab;
+  goto yyreduce;
+
+
+/*-----------------------------.
+| yyreduce -- Do a reduction.  |
+`-----------------------------*/
+yyreduce:
+  /* yyn is the number of a rule to reduce with.  */
+  yylen = yyr2[yyn];
+
+  /* If YYLEN is nonzero, implement the default value of the action:
+     `$$ = $1'.
+
+     Otherwise, the following line sets YYVAL to garbage.
+     This behavior is undocumented and Bison
+     users should not rely upon it.  Assigning to YYVAL
+     unconditionally makes the parser a bit smaller, and it avoids a
+     GCC warning that YYVAL may be used uninitialized.  */
+  yyval = yyvsp[1-yylen];
+
+
+  YY_REDUCE_PRINT (yyn);
+  switch (yyn)
+    {
+        case 4:
+
+/* Line 1806 of yacc.c  */
+#line 54 "parserPromela.yacc"
+    { new_state((yyvsp[(1) - (2)].string), 1);}
+    break;
+
+  case 7:
+
+/* Line 1806 of yacc.c  */
+#line 58 "parserPromela.yacc"
+    { new_transition((yyvsp[(5) - (6)].string), (yyvsp[(2) - (6)].label));}
+    break;
+
+  case 8:
+
+/* Line 1806 of yacc.c  */
+#line 61 "parserPromela.yacc"
+    { (yyval.label) = (yyvsp[(2) - (3)].label); }
+    break;
+
+  case 9:
+
+/* Line 1806 of yacc.c  */
+#line 62 "parserPromela.yacc"
+    { (yyval.label) = new_label(0, (yyvsp[(1) - (3)].label), (yyvsp[(3) - (3)].label)); }
+    break;
+
+  case 10:
+
+/* Line 1806 of yacc.c  */
+#line 63 "parserPromela.yacc"
+    { (yyval.label) = new_label(1, (yyvsp[(1) - (3)].label), (yyvsp[(3) - (3)].label)); }
+    break;
+
+  case 11:
+
+/* Line 1806 of yacc.c  */
+#line 64 "parserPromela.yacc"
+    { (yyval.label) = new_label(2, (yyvsp[(2) - (2)].label)); }
+    break;
+
+  case 12:
+
+/* Line 1806 of yacc.c  */
+#line 65 "parserPromela.yacc"
+    { (yyval.label) = new_label(4); }
+    break;
+
+  case 13:
+
+/* Line 1806 of yacc.c  */
+#line 66 "parserPromela.yacc"
+    { (yyval.label) = new_label(3, (yyvsp[(1) - (1)].string)); }
+    break;
+
+
+
+/* Line 1806 of yacc.c  */
+#line 1478 "y.tab.c"
+      default: break;
+    }
+  /* User semantic actions sometimes alter yychar, and that requires
+     that yytoken be updated with the new translation.  We take the
+     approach of translating immediately before every use of yytoken.
+     One alternative is translating here after every semantic action,
+     but that translation would be missed if the semantic action invokes
+     YYABORT, YYACCEPT, or YYERROR immediately after altering yychar or
+     if it invokes YYBACKUP.  In the case of YYABORT or YYACCEPT, an
+     incorrect destructor might then be invoked immediately.  In the
+     case of YYERROR or YYBACKUP, subsequent parser actions might lead
+     to an incorrect destructor call or verbose syntax error message
+     before the lookahead is translated.  */
+  YY_SYMBOL_PRINT ("-> $$ =", yyr1[yyn], &yyval, &yyloc);
+
+  YYPOPSTACK (yylen);
+  yylen = 0;
+  YY_STACK_PRINT (yyss, yyssp);
+
+  *++yyvsp = yyval;
+
+  /* Now `shift' the result of the reduction.  Determine what state
+     that goes to, based on the state we popped back to and the rule
+     number reduced by.  */
+
+  yyn = yyr1[yyn];
+
+  yystate = yypgoto[yyn - YYNTOKENS] + *yyssp;
+  if (0 <= yystate && yystate <= YYLAST && yycheck[yystate] == *yyssp)
+    yystate = yytable[yystate];
+  else
+    yystate = yydefgoto[yyn - YYNTOKENS];
+
+  goto yynewstate;
+
+
+/*------------------------------------.
+| yyerrlab -- here on detecting error |
+`------------------------------------*/
+yyerrlab:
+  /* Make sure we have latest lookahead translation.  See comments at
+     user semantic actions for why this is necessary.  */
+  yytoken = yychar == YYEMPTY ? YYEMPTY : YYTRANSLATE (yychar);
+
+  /* If not already recovering from an error, report this error.  */
+  if (!yyerrstatus)
+    {
+      ++yynerrs;
+#if ! YYERROR_VERBOSE
+      yyerror (YY_("syntax error"));
+#else
+# define YYSYNTAX_ERROR yysyntax_error (&yymsg_alloc, &yymsg, \
+                                        yyssp, yytoken)
+      {
+        char const *yymsgp = YY_("syntax error");
+        int yysyntax_error_status;
+        yysyntax_error_status = YYSYNTAX_ERROR;
+        if (yysyntax_error_status == 0)
+          yymsgp = yymsg;
+        else if (yysyntax_error_status == 1)
+          {
+            if (yymsg != yymsgbuf)
+              YYSTACK_FREE (yymsg);
+            yymsg = (char *) YYSTACK_ALLOC (yymsg_alloc);
+            if (!yymsg)
+              {
+                yymsg = yymsgbuf;
+                yymsg_alloc = sizeof yymsgbuf;
+                yysyntax_error_status = 2;
+              }
+            else
+              {
+                yysyntax_error_status = YYSYNTAX_ERROR;
+                yymsgp = yymsg;
+              }
+          }
+        yyerror (yymsgp);
+        if (yysyntax_error_status == 2)
+          goto yyexhaustedlab;
+      }
+# undef YYSYNTAX_ERROR
+#endif
+    }
+
+
+
+  if (yyerrstatus == 3)
+    {
+      /* If just tried and failed to reuse lookahead token after an
+        error, discard it.  */
+
+      if (yychar <= YYEOF)
+       {
+         /* Return failure if at end of input.  */
+         if (yychar == YYEOF)
+           YYABORT;
+       }
+      else
+       {
+         yydestruct ("Error: discarding",
+                     yytoken, &yylval);
+         yychar = YYEMPTY;
+       }
+    }
+
+  /* Else will try to reuse lookahead token after shifting the error
+     token.  */
+  goto yyerrlab1;
+
+
+/*---------------------------------------------------.
+| yyerrorlab -- error raised explicitly by YYERROR.  |
+`---------------------------------------------------*/
+yyerrorlab:
+
+  /* Pacify compilers like GCC when the user code never invokes
+     YYERROR and the label yyerrorlab therefore never appears in user
+     code.  */
+  if (/*CONSTCOND*/ 0)
+     goto yyerrorlab;
+
+  /* Do not reclaim the symbols of the rule which action triggered
+     this YYERROR.  */
+  YYPOPSTACK (yylen);
+  yylen = 0;
+  YY_STACK_PRINT (yyss, yyssp);
+  yystate = *yyssp;
+  goto yyerrlab1;
+
+
+/*-------------------------------------------------------------.
+| yyerrlab1 -- common code for both syntax error and YYERROR.  |
+`-------------------------------------------------------------*/
+yyerrlab1:
+  yyerrstatus = 3;     /* Each real token shifted decrements this.  */
+
+  for (;;)
+    {
+      yyn = yypact[yystate];
+      if (!yypact_value_is_default (yyn))
+       {
+         yyn += YYTERROR;
+         if (0 <= yyn && yyn <= YYLAST && yycheck[yyn] == YYTERROR)
+           {
+             yyn = yytable[yyn];
+             if (0 < yyn)
+               break;
+           }
+       }
+
+      /* Pop the current state because it cannot handle the error token.  */
+      if (yyssp == yyss)
+       YYABORT;
+
+
+      yydestruct ("Error: popping",
+                 yystos[yystate], yyvsp);
+      YYPOPSTACK (1);
+      yystate = *yyssp;
+      YY_STACK_PRINT (yyss, yyssp);
+    }
+
+  *++yyvsp = yylval;
+
+
+  /* Shift the error token.  */
+  YY_SYMBOL_PRINT ("Shifting", yystos[yyn], yyvsp, yylsp);
+
+  yystate = yyn;
+  goto yynewstate;
+
+
+/*-------------------------------------.
+| yyacceptlab -- YYACCEPT comes here.  |
+`-------------------------------------*/
+yyacceptlab:
+  yyresult = 0;
+  goto yyreturn;
+
+/*-----------------------------------.
+| yyabortlab -- YYABORT comes here.  |
+`-----------------------------------*/
+yyabortlab:
+  yyresult = 1;
+  goto yyreturn;
+
+#if !defined(yyoverflow) || YYERROR_VERBOSE
+/*-------------------------------------------------.
+| yyexhaustedlab -- memory exhaustion comes here.  |
+`-------------------------------------------------*/
+yyexhaustedlab:
+  yyerror (YY_("memory exhausted"));
+  yyresult = 2;
+  /* Fall through.  */
+#endif
+
+yyreturn:
+  if (yychar != YYEMPTY)
+    {
+      /* Make sure we have latest lookahead translation.  See comments at
+         user semantic actions for why this is necessary.  */
+      yytoken = YYTRANSLATE (yychar);
+      yydestruct ("Cleanup: discarding lookahead",
+                  yytoken, &yylval);
+    }
+  /* Do not reclaim the symbols of the rule which action triggered
+     this YYABORT or YYACCEPT.  */
+  YYPOPSTACK (yylen);
+  YY_STACK_PRINT (yyss, yyssp);
+  while (yyssp != yyss)
+    {
+      yydestruct ("Cleanup: popping",
+                 yystos[*yyssp], yyvsp);
+      YYPOPSTACK (1);
+    }
+#ifndef yyoverflow
+  if (yyss != yyssa)
+    YYSTACK_FREE (yyss);
+#endif
+#if YYERROR_VERBOSE
+  if (yymsg != yymsgbuf)
+    YYSTACK_FREE (yymsg);
+#endif
+  /* Make sure YYID is used.  */
+  return YYID (yyresult);
+}
+
+
+
+/* Line 2067 of yacc.c  */
+#line 69 "parserPromela.yacc"
+
+
+
+
+void yyerror(const char *s){
+  fprintf (stderr, "%s\n", s);
+}
+
+
+
+
diff --git a/src/xbt/automaton/y.tab.h b/src/xbt/automaton/y.tab.h
new file mode 100644 (file)
index 0000000..ad611d5
--- /dev/null
@@ -0,0 +1,111 @@
+/* A Bison parser, made by GNU Bison 2.5.  */
+
+/* Bison interface for Yacc-like parsers in C
+   
+      Copyright (C) 1984, 1989-1990, 2000-2011 Free Software Foundation, Inc.
+   
+   This program 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 3 of the License, or
+   (at your option) any later version.
+   
+   This program 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, see <http://www.gnu.org/licenses/>.  */
+
+/* As a special exception, you may create a larger work that contains
+   part or all of the Bison parser skeleton and distribute that work
+   under terms of your choice, so long as that work isn't itself a
+   parser generator using the skeleton or a modified version thereof
+   as a parser skeleton.  Alternatively, if you modify or redistribute
+   the parser skeleton itself, you may (at your option) remove this
+   special exception, which will cause the skeleton and the resulting
+   Bison output files to be licensed under the GNU General Public
+   License without this special exception.
+   
+   This special exception was added by the Free Software Foundation in
+   version 2.2 of Bison.  */
+
+
+/* Tokens.  */
+#ifndef YYTOKENTYPE
+# define YYTOKENTYPE
+   /* Put the tokens into the symbol table, so that GDB and other debuggers
+      know about them.  */
+   enum yytokentype {
+     NEVER = 258,
+     IF = 259,
+     FI = 260,
+     IMPLIES = 261,
+     GOTO = 262,
+     AND = 263,
+     OR = 264,
+     NOT = 265,
+     LEFT_PAR = 266,
+     RIGHT_PAR = 267,
+     CASE = 268,
+     COLON = 269,
+     SEMI_COLON = 270,
+     CASE_TRUE = 271,
+     LEFT_BRACE = 272,
+     RIGHT_BRACE = 273,
+     LITT_ENT = 274,
+     LITT_CHAINE = 275,
+     LITT_REEL = 276,
+     ID = 277
+   };
+#endif
+/* Tokens.  */
+#define NEVER 258
+#define IF 259
+#define FI 260
+#define IMPLIES 261
+#define GOTO 262
+#define AND 263
+#define OR 264
+#define NOT 265
+#define LEFT_PAR 266
+#define RIGHT_PAR 267
+#define CASE 268
+#define COLON 269
+#define SEMI_COLON 270
+#define CASE_TRUE 271
+#define LEFT_BRACE 272
+#define RIGHT_BRACE 273
+#define LITT_ENT 274
+#define LITT_CHAINE 275
+#define LITT_REEL 276
+#define ID 277
+
+
+
+
+#if ! defined YYSTYPE && ! defined YYSTYPE_IS_DECLARED
+typedef union YYSTYPE
+{
+
+/* Line 2068 of yacc.c  */
+#line 13 "parserPromela.yacc"
+
+  double real;
+  int integer;
+  char* string;
+  xbt_exp_label_t label;
+
+
+
+/* Line 2068 of yacc.c  */
+#line 103 "y.tab.h"
+} YYSTYPE;
+# define YYSTYPE_IS_TRIVIAL 1
+# define yystype YYSTYPE /* obsolescent; will be withdrawn */
+# define YYSTYPE_IS_DECLARED 1
+#endif
+
+extern YYSTYPE yylval;
+
+