Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
model-checker : remove unused files in examples/ms/mc
authorMarion Guthmuller <marion.guthmuller@loria.fr>
Fri, 15 Jun 2012 07:32:52 +0000 (09:32 +0200)
committerMarion Guthmuller <marion.guthmuller@loria.fr>
Fri, 15 Jun 2012 08:06:13 +0000 (10:06 +0200)
examples/msg/mc/automaton.c [deleted file]
examples/msg/mc/automaton_parse.yy.c [deleted file]
examples/msg/mc/automatonparse_promela.c [deleted file]
examples/msg/mc/y.output [deleted file]
examples/msg/mc/y.tab.c [deleted file]
examples/msg/mc/y.tab.h [deleted file]

diff --git a/examples/msg/mc/automaton.c b/examples/msg/mc/automaton.c
deleted file mode 100644 (file)
index 8f189a8..0000000
+++ /dev/null
@@ -1,358 +0,0 @@
-#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/examples/msg/mc/automaton_parse.yy.c b/examples/msg/mc/automaton_parse.yy.c
deleted file mode 100644 (file)
index a7395b1..0000000
+++ /dev/null
@@ -1,1947 +0,0 @@
-#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/examples/msg/mc/automatonparse_promela.c b/examples/msg/mc/automatonparse_promela.c
deleted file mode 100644 (file)
index 128a874..0000000
+++ /dev/null
@@ -1,93 +0,0 @@
-#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/examples/msg/mc/y.output b/examples/msg/mc/y.output
deleted file mode 100644 (file)
index 7bef6cd..0000000
+++ /dev/null
@@ -1,353 +0,0 @@
-Terminals unused in grammar
-
-   LITT_ENT
-   LITT_CHAINE
-   LITT_REEL
-
-
-Grammaire
-
-    0 $accept: automaton $end
-
-    1 automaton: NEVER LEFT_BRACE stateseq RIGHT_BRACE
-
-    2 stateseq: /* vide */
-
-    3 $@1: /* vide */
-
-    4 stateseq: ID COLON $@1 IF option FI SEMI_COLON stateseq
-
-    5 option: /* vide */
-    6       | CASE exp IMPLIES GOTO ID option
-
-    7 exp: LEFT_PAR exp RIGHT_PAR
-    8    | exp OR exp
-    9    | exp AND exp
-   10    | NOT exp
-   11    | CASE_TRUE
-   12    | ID
-
-
-Terminaux, suivis des règles où ils apparaissent
-
-$end (0) 0
-error (256)
-NEVER (258) 1
-IF (259) 4
-FI (260) 4
-IMPLIES (261) 6
-GOTO (262) 6
-AND (263) 9
-OR (264) 8
-NOT (265) 10
-LEFT_PAR (266) 7
-RIGHT_PAR (267) 7
-CASE (268) 6
-COLON (269) 4
-SEMI_COLON (270) 4
-CASE_TRUE (271) 11
-LEFT_BRACE (272) 1
-RIGHT_BRACE (273) 1
-LITT_ENT (274)
-LITT_CHAINE (275)
-LITT_REEL (276)
-ID (277) 4 6 12
-
-
-Non-terminaux, suivis des règles où ils apparaissent
-
-$accept (23)
-    à gauche: 0
-automaton (24)
-    à gauche: 1, à droite: 0
-stateseq (25)
-    à gauche: 2 4, à droite: 1 4
-$@1 (26)
-    à gauche: 3, à droite: 4
-option (27)
-    à gauche: 5 6, à droite: 4 6
-exp (28)
-    à gauche: 7 8 9 10 11 12, à droite: 6 7 8 9 10
-
-
-état 0
-
-    0 $accept: . automaton $end
-
-    NEVER  décalage et aller à l'état 1
-
-    automaton  aller à l'état 2
-
-
-état 1
-
-    1 automaton: NEVER . LEFT_BRACE stateseq RIGHT_BRACE
-
-    LEFT_BRACE  décalage et aller à l'état 3
-
-
-état 2
-
-    0 $accept: automaton . $end
-
-    $end  décalage et aller à l'état 4
-
-
-état 3
-
-    1 automaton: NEVER LEFT_BRACE . stateseq RIGHT_BRACE
-
-    ID  décalage et aller à l'état 5
-
-    $défaut  réduction par utilisation de la règle 2 (stateseq)
-
-    stateseq  aller à l'état 6
-
-
-état 4
-
-    0 $accept: automaton $end .
-
-    $défaut  accepter
-
-
-état 5
-
-    4 stateseq: ID . COLON $@1 IF option FI SEMI_COLON stateseq
-
-    COLON  décalage et aller à l'état 7
-
-
-état 6
-
-    1 automaton: NEVER LEFT_BRACE stateseq . RIGHT_BRACE
-
-    RIGHT_BRACE  décalage et aller à l'état 8
-
-
-état 7
-
-    4 stateseq: ID COLON . $@1 IF option FI SEMI_COLON stateseq
-
-    $défaut  réduction par utilisation de la règle 3 ($@1)
-
-    $@1  aller à l'état 9
-
-
-état 8
-
-    1 automaton: NEVER LEFT_BRACE stateseq RIGHT_BRACE .
-
-    $défaut  réduction par utilisation de la règle 1 (automaton)
-
-
-état 9
-
-    4 stateseq: ID COLON $@1 . IF option FI SEMI_COLON stateseq
-
-    IF  décalage et aller à l'état 10
-
-
-état 10
-
-    4 stateseq: ID COLON $@1 IF . option FI SEMI_COLON stateseq
-
-    CASE  décalage et aller à l'état 11
-
-    $défaut  réduction par utilisation de la règle 5 (option)
-
-    option  aller à l'état 12
-
-
-état 11
-
-    6 option: CASE . exp IMPLIES GOTO ID option
-
-    NOT        décalage et aller à l'état 13
-    LEFT_PAR   décalage et aller à l'état 14
-    CASE_TRUE  décalage et aller à l'état 15
-    ID         décalage et aller à l'état 16
-
-    exp  aller à l'état 17
-
-
-état 12
-
-    4 stateseq: ID COLON $@1 IF option . FI SEMI_COLON stateseq
-
-    FI  décalage et aller à l'état 18
-
-
-état 13
-
-   10 exp: NOT . exp
-
-    NOT        décalage et aller à l'état 13
-    LEFT_PAR   décalage et aller à l'état 14
-    CASE_TRUE  décalage et aller à l'état 15
-    ID         décalage et aller à l'état 16
-
-    exp  aller à l'état 19
-
-
-état 14
-
-    7 exp: LEFT_PAR . exp RIGHT_PAR
-
-    NOT        décalage et aller à l'état 13
-    LEFT_PAR   décalage et aller à l'état 14
-    CASE_TRUE  décalage et aller à l'état 15
-    ID         décalage et aller à l'état 16
-
-    exp  aller à l'état 20
-
-
-état 15
-
-   11 exp: CASE_TRUE .
-
-    $défaut  réduction par utilisation de la règle 11 (exp)
-
-
-état 16
-
-   12 exp: ID .
-
-    $défaut  réduction par utilisation de la règle 12 (exp)
-
-
-état 17
-
-    6 option: CASE exp . IMPLIES GOTO ID option
-    8 exp: exp . OR exp
-    9    | exp . AND exp
-
-    IMPLIES  décalage et aller à l'état 21
-    AND      décalage et aller à l'état 22
-    OR       décalage et aller à l'état 23
-
-
-état 18
-
-    4 stateseq: ID COLON $@1 IF option FI . SEMI_COLON stateseq
-
-    SEMI_COLON  décalage et aller à l'état 24
-
-
-état 19
-
-    8 exp: exp . OR exp
-    9    | exp . AND exp
-   10    | NOT exp .
-
-    $défaut  réduction par utilisation de la règle 10 (exp)
-
-
-état 20
-
-    7 exp: LEFT_PAR exp . RIGHT_PAR
-    8    | exp . OR exp
-    9    | exp . AND exp
-
-    AND        décalage et aller à l'état 22
-    OR         décalage et aller à l'état 23
-    RIGHT_PAR  décalage et aller à l'état 25
-
-
-état 21
-
-    6 option: CASE exp IMPLIES . GOTO ID option
-
-    GOTO  décalage et aller à l'état 26
-
-
-état 22
-
-    9 exp: exp AND . exp
-
-    NOT        décalage et aller à l'état 13
-    LEFT_PAR   décalage et aller à l'état 14
-    CASE_TRUE  décalage et aller à l'état 15
-    ID         décalage et aller à l'état 16
-
-    exp  aller à l'état 27
-
-
-état 23
-
-    8 exp: exp OR . exp
-
-    NOT        décalage et aller à l'état 13
-    LEFT_PAR   décalage et aller à l'état 14
-    CASE_TRUE  décalage et aller à l'état 15
-    ID         décalage et aller à l'état 16
-
-    exp  aller à l'état 28
-
-
-état 24
-
-    4 stateseq: ID COLON $@1 IF option FI SEMI_COLON . stateseq
-
-    ID  décalage et aller à l'état 5
-
-    $défaut  réduction par utilisation de la règle 2 (stateseq)
-
-    stateseq  aller à l'état 29
-
-
-état 25
-
-    7 exp: LEFT_PAR exp RIGHT_PAR .
-
-    $défaut  réduction par utilisation de la règle 7 (exp)
-
-
-état 26
-
-    6 option: CASE exp IMPLIES GOTO . ID option
-
-    ID  décalage et aller à l'état 30
-
-
-état 27
-
-    8 exp: exp . OR exp
-    9    | exp . AND exp
-    9    | exp AND exp .
-
-    $défaut  réduction par utilisation de la règle 9 (exp)
-
-
-état 28
-
-    8 exp: exp . OR exp
-    8    | exp OR exp .
-    9    | exp . AND exp
-
-    $défaut  réduction par utilisation de la règle 8 (exp)
-
-
-état 29
-
-    4 stateseq: ID COLON $@1 IF option FI SEMI_COLON stateseq .
-
-    $défaut  réduction par utilisation de la règle 4 (stateseq)
-
-
-état 30
-
-    6 option: CASE exp IMPLIES GOTO ID . option
-
-    CASE  décalage et aller à l'état 11
-
-    $défaut  réduction par utilisation de la règle 5 (option)
-
-    option  aller à l'état 31
-
-
-état 31
-
-    6 option: CASE exp IMPLIES GOTO ID option .
-
-    $défaut  réduction par utilisation de la règle 6 (option)
diff --git a/examples/msg/mc/y.tab.c b/examples/msg/mc/y.tab.c
deleted file mode 100644 (file)
index d2cd6cb..0000000
+++ /dev/null
@@ -1,1668 +0,0 @@
-
-/* A Bison parser, made by GNU Bison 2.4.1.  */
-
-/* Skeleton implementation for Bison's Yacc-like parsers in C
-   
-      Copyright (C) 1984, 1989, 1990, 2000, 2001, 2002, 2003, 2004, 2005, 2006
-   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.4.1"
-
-/* 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 189 of yacc.c  */
-#line 1 "parserPromela.yacc"
-
-
-#include "automaton.h"
-#include "automatonparse_promela.h"
-#include "lex.yy.c"
-
-void yyerror(const char *s);
-
-
-
-/* Line 189 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 214 of yacc.c  */
-#line 11 "parserPromela.yacc"
-
-  double real;
-  int integer;
-  char* string;
-  xbt_exp_label_t label;
-
-
-
-/* Line 214 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 264 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 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 _STDLIB_H && (defined __STDC__ || defined __C99__FUNC__ \
-     || defined __cplusplus || defined _MSC_VER)
-#     include <stdlib.h> /* INFRINGES ON USER NAME SPACE */
-#     ifndef _STDLIB_H
-#      define _STDLIB_H 1
-#     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 _STDLIB_H \
-       && ! ((defined YYMALLOC || defined malloc) \
-            && (defined YYFREE || defined free)))
-#   include <stdlib.h> /* INFRINGES ON USER NAME SPACE */
-#   ifndef _STDLIB_H
-#    define _STDLIB_H 1
-#   endif
-#  endif
-#  ifndef YYMALLOC
-#   define YYMALLOC malloc
-#   if ! defined malloc && ! defined _STDLIB_H && (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 _STDLIB_H && (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)
-
-/* 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
-
-/* 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
-
-/* 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,    48,    48,    51,    52,    52,    55,    56,    59,    60,
-      61,    62,    63,    64
-};
-#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 rule to reduce with in state
-   STATE-NUM 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 zero, do what YYDEFACT says.
-   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
-};
-
-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.  */
-
-#define YYFAIL         goto yyerrlab
-
-#define YYRECOVERING()  (!!yyerrstatus)
-
-#define YYBACKUP(Token, Value)                                 \
-do                                                             \
-  if (yychar == YYEMPTY && yylen == 1)                         \
-    {                                                          \
-      yychar = (Token);                                                \
-      yylval = (Value);                                                \
-      yytoken = YYTRANSLATE (yychar);                          \
-      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
-
-
-/* YY_LOCATION_PRINT -- Print the location on the stream.
-   This macro was not mandated originally: define only if we know
-   we won't break user code: when these are the locations we know.  */
-
-#ifndef YY_LOCATION_PRINT
-# if YYLTYPE_IS_TRIVIAL
-#  define YY_LOCATION_PRINT(File, Loc)                 \
-     fprintf (File, "%d.%d-%d.%d",                     \
-             (Loc).first_line, (Loc).first_column,     \
-             (Loc).last_line,  (Loc).last_column)
-# else
-#  define YY_LOCATION_PRINT(File, Loc) ((void) 0)
-# endif
-#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
-
-\f
-
-#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 YYRESULT an error message about the unexpected token
-   YYCHAR while in state YYSTATE.  Return the number of bytes copied,
-   including the terminating null byte.  If YYRESULT is null, do not
-   copy anything; just return the number of bytes that would be
-   copied.  As a special case, return 0 if an ordinary "syntax error"
-   message will do.  Return YYSIZE_MAXIMUM if overflow occurs during
-   size calculation.  */
-static YYSIZE_T
-yysyntax_error (char *yyresult, int yystate, int yychar)
-{
-  int yyn = yypact[yystate];
-
-  if (! (YYPACT_NINF < yyn && yyn <= YYLAST))
-    return 0;
-  else
-    {
-      int yytype = YYTRANSLATE (yychar);
-      YYSIZE_T yysize0 = yytnamerr (0, yytname[yytype]);
-      YYSIZE_T yysize = yysize0;
-      YYSIZE_T yysize1;
-      int yysize_overflow = 0;
-      enum { YYERROR_VERBOSE_ARGS_MAXIMUM = 5 };
-      char const *yyarg[YYERROR_VERBOSE_ARGS_MAXIMUM];
-      int yyx;
-
-# if 0
-      /* This is so xgettext sees the translatable formats that are
-        constructed on the fly.  */
-      YY_("syntax error, unexpected %s");
-      YY_("syntax error, unexpected %s, expecting %s");
-      YY_("syntax error, unexpected %s, expecting %s or %s");
-      YY_("syntax error, unexpected %s, expecting %s or %s or %s");
-      YY_("syntax error, unexpected %s, expecting %s or %s or %s or %s");
-# endif
-      char *yyfmt;
-      char const *yyf;
-      static char const yyunexpected[] = "syntax error, unexpected %s";
-      static char const yyexpecting[] = ", expecting %s";
-      static char const yyor[] = " or %s";
-      char yyformat[sizeof yyunexpected
-                   + sizeof yyexpecting - 1
-                   + ((YYERROR_VERBOSE_ARGS_MAXIMUM - 2)
-                      * (sizeof yyor - 1))];
-      char const *yyprefix = yyexpecting;
-
-      /* Start YYX at -YYN if negative to avoid negative indexes in
-        YYCHECK.  */
-      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 yycount = 1;
-
-      yyarg[0] = yytname[yytype];
-      yyfmt = yystpcpy (yyformat, yyunexpected);
-
-      for (yyx = yyxbegin; yyx < yyxend; ++yyx)
-       if (yycheck[yyx + yyn] == yyx && yyx != YYTERROR)
-         {
-           if (yycount == YYERROR_VERBOSE_ARGS_MAXIMUM)
-             {
-               yycount = 1;
-               yysize = yysize0;
-               yyformat[sizeof yyunexpected - 1] = '\0';
-               break;
-             }
-           yyarg[yycount++] = yytname[yyx];
-           yysize1 = yysize + yytnamerr (0, yytname[yyx]);
-           yysize_overflow |= (yysize1 < yysize);
-           yysize = yysize1;
-           yyfmt = yystpcpy (yyfmt, yyprefix);
-           yyprefix = yyor;
-         }
-
-      yyf = YY_(yyformat);
-      yysize1 = yysize + yystrlen (yyf);
-      yysize_overflow |= (yysize1 < yysize);
-      yysize = yysize1;
-
-      if (yysize_overflow)
-       return YYSIZE_MAXIMUM;
-
-      if (yyresult)
-       {
-         /* 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 = yyresult;
-         int yyi = 0;
-         while ((*yyp = *yyf) != '\0')
-           {
-             if (*yyp == '%' && yyf[1] == 's' && yyi < yycount)
-               {
-                 yyp += yytnamerr (yyp, yyarg[yyi++]);
-                 yyf += 2;
-               }
-             else
-               {
-                 yyp++;
-                 yyf++;
-               }
-           }
-       }
-      return yysize;
-    }
-}
-#endif /* YYERROR_VERBOSE */
-\f
-
-/*-----------------------------------------------.
-| 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 or yypush_parse.  |
-`-------------------------*/
-
-#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 (yyn == YYPACT_NINF)
-    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 (yyn == 0 || yyn == YYTABLE_NINF)
-       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 1455 of yacc.c  */
-#line 52 "parserPromela.yacc"
-    { new_state((yyvsp[(1) - (2)].string), 1);}
-    break;
-
-  case 7:
-
-/* Line 1455 of yacc.c  */
-#line 56 "parserPromela.yacc"
-    { new_transition((yyvsp[(5) - (6)].string), (yyvsp[(2) - (6)].label));}
-    break;
-
-  case 8:
-
-/* Line 1455 of yacc.c  */
-#line 59 "parserPromela.yacc"
-    { (yyval.label) = (yyvsp[(2) - (3)].label); }
-    break;
-
-  case 9:
-
-/* Line 1455 of yacc.c  */
-#line 60 "parserPromela.yacc"
-    { (yyval.label) = new_label(0, (yyvsp[(1) - (3)].label), (yyvsp[(3) - (3)].label)); }
-    break;
-
-  case 10:
-
-/* Line 1455 of yacc.c  */
-#line 61 "parserPromela.yacc"
-    { (yyval.label) = new_label(1, (yyvsp[(1) - (3)].label), (yyvsp[(3) - (3)].label)); }
-    break;
-
-  case 11:
-
-/* Line 1455 of yacc.c  */
-#line 62 "parserPromela.yacc"
-    { (yyval.label) = new_label(2, (yyvsp[(2) - (2)].label)); }
-    break;
-
-  case 12:
-
-/* Line 1455 of yacc.c  */
-#line 63 "parserPromela.yacc"
-    { (yyval.label) = new_label(4); }
-    break;
-
-  case 13:
-
-/* Line 1455 of yacc.c  */
-#line 64 "parserPromela.yacc"
-    { (yyval.label) = new_label(3, (yyvsp[(1) - (1)].string)); }
-    break;
-
-
-
-/* Line 1455 of yacc.c  */
-#line 1446 "y.tab.c"
-      default: break;
-    }
-  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:
-  /* If not already recovering from an error, report this error.  */
-  if (!yyerrstatus)
-    {
-      ++yynerrs;
-#if ! YYERROR_VERBOSE
-      yyerror (YY_("syntax error"));
-#else
-      {
-       YYSIZE_T yysize = yysyntax_error (0, yystate, yychar);
-       if (yymsg_alloc < yysize && yymsg_alloc < YYSTACK_ALLOC_MAXIMUM)
-         {
-           YYSIZE_T yyalloc = 2 * yysize;
-           if (! (yysize <= yyalloc && yyalloc <= YYSTACK_ALLOC_MAXIMUM))
-             yyalloc = YYSTACK_ALLOC_MAXIMUM;
-           if (yymsg != yymsgbuf)
-             YYSTACK_FREE (yymsg);
-           yymsg = (char *) YYSTACK_ALLOC (yyalloc);
-           if (yymsg)
-             yymsg_alloc = yyalloc;
-           else
-             {
-               yymsg = yymsgbuf;
-               yymsg_alloc = sizeof yymsgbuf;
-             }
-         }
-
-       if (0 < yysize && yysize <= yymsg_alloc)
-         {
-           (void) yysyntax_error (yymsg, yystate, yychar);
-           yyerror (yymsg);
-         }
-       else
-         {
-           yyerror (YY_("syntax error"));
-           if (yysize != 0)
-             goto yyexhaustedlab;
-         }
-      }
-#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 (yyn != YYPACT_NINF)
-       {
-         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)
-     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 1675 of yacc.c  */
-#line 67 "parserPromela.yacc"
-
-
-
-
-void yyerror(const char *s){
-  fprintf (stderr, "%s\n", s);
-}
-
-
-
-
diff --git a/examples/msg/mc/y.tab.h b/examples/msg/mc/y.tab.h
deleted file mode 100644 (file)
index 22bb813..0000000
+++ /dev/null
@@ -1,113 +0,0 @@
-
-/* A Bison parser, made by GNU Bison 2.4.1.  */
-
-/* Skeleton interface for Bison's Yacc-like parsers in C
-   
-      Copyright (C) 1984, 1989, 1990, 2000, 2001, 2002, 2003, 2004, 2005, 2006
-   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 1676 of yacc.c  */
-#line 11 "parserPromela.yacc"
-
-  double real;
-  int integer;
-  char* string;
-  xbt_exp_label_t label;
-
-
-
-/* Line 1676 of yacc.c  */
-#line 105 "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;
-
-