Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
Various cleanups to the model-checking user interface
authorMartin Quinson <martin.quinson@loria.fr>
Thu, 21 Jun 2012 13:26:06 +0000 (15:26 +0200)
committerMartin Quinson <martin.quinson@loria.fr>
Thu, 21 Jun 2012 13:29:33 +0000 (15:29 +0200)
- hide the automaton used to represent the property within MC
- move from yacc to bison so that I can choose the output name
- Hide a bunch of private functions used to parse the automaton from
  file
(more to come)

Hopefully, I didn't break too much stuff on my way

27 files changed:
buildtools/Cmake/DefinePackages.cmake
buildtools/Cmake/MaintainerMode.cmake
buildtools/Cmake/MakeLib.cmake
examples/msg/mc/bugged1_for_liveness.c
examples/msg/mc/bugged1_while_liveness.c
examples/msg/mc/bugged2_liveness.c
examples/msg/mc/centralized_liveness.c
examples/msg/mc/centralized_liveness_deadlock.c
examples/msg/mc/test_snapshot.c
include/msg/msg.h
include/simgrid/modelchecker.h
include/xbt/automaton.h
include/xbt/automatonparse_promela.h [deleted file]
src/include/mc/mc.h
src/mc/mc_global.c
src/mc/mc_liveness.c
src/mc/mc_private.h
src/msg/msg_global.c
src/xbt/automaton/automaton.c
src/xbt/automaton/automaton_create.c [deleted file]
src/xbt/automaton/automaton_create.h [deleted file]
src/xbt/automaton/automaton_lexer.yy.c [moved from src/xbt/automaton/automaton_parse.yy.c with 75% similarity]
src/xbt/automaton/automatonparse_promela.c
src/xbt/automaton/parserPromela.lex
src/xbt/automaton/parserPromela.tab.cacc [moved from src/xbt/automaton/y.tab.c with 98% similarity]
src/xbt/automaton/parserPromela.tab.hacc [moved from src/xbt/automaton/y.tab.h with 83% similarity]
src/xbt/automaton/parserPromela.yacc

index 592ddb8..ace4e25 100644 (file)
@@ -31,9 +31,9 @@ set(EXTRA_DIST
   src/xbt/mmalloc/test/mmalloc_test.c
   src/xbt/datadesc/ddt_parse.yy.l
   src/xbt/datadesc/ddt_parse.yy.h
-  src/xbt/automaton/y.tab.c
-  src/xbt/automaton/y.tab.h
-  src/xbt/automaton/automaton_parse.yy.c
+  src/xbt/automaton/parserPromela.tab.cacc
+  src/xbt/automaton/parserPromela.tab.hacc
+  src/xbt/automaton/automaton_lexer.yy.c
   src/xbt/automaton/parserPromela.lex
   src/xbt/automaton/parserPromela.yacc
   src/surf/maxmin_private.h
@@ -175,8 +175,6 @@ set(XBT_SRC
   src/xbt/lib.c
   src/xbt/automaton/automatonparse_promela.c
   src/xbt/automaton/automaton.c
-  src/xbt/automaton/automaton_create.c
-  src/xbt/automaton/automaton_create.h
   src/xbt/datadesc/ddt_create.c
   src/xbt/datadesc/ddt_convert.c
   src/xbt/datadesc/ddt_exchange.c
index c1e45d4..64e6aa3 100644 (file)
@@ -2,27 +2,26 @@ if(enable_maintainer_mode AND NOT WIN32)
 find_program(FLEX_EXE NAMES flex)
 find_program(FLEXML_EXE NAMES flexml)
 find_program(SED_EXE NAMES sed)
-find_program(YACC_EXE NAMES yacc)
+find_program(BISON_EXE NAMES bison)
 find_program(LEX_EXE NAMES lex)
 
-mark_as_advanced(YACC_EXE)
+mark_as_advanced(BISON_EXE)
 mark_as_advanced(LEX_EXE)
 
-if(YACC_EXE AND LEX_EXE)
+if(BISON_EXE AND LEX_EXE)
   add_custom_target(automaton_generated_src ALL
   DEPENDS ${CMAKE_HOME_DIRECTORY}/src/xbt/automaton/parserPromela.lex
           ${CMAKE_HOME_DIRECTORY}/src/xbt/automaton/parserPromela.yacc
-  COMMENT "Generated automaton source files"
-  COMMAND ${YACC_EXE} -d parserPromela.yacc
-  COMMAND ${LEX_EXE} --prefix=xbt_automaton_parse_ --outfile=automaton_parse.yy.c parserPromela.lex
-  COMMAND ${CMAKE_COMMAND} -E remove y.output
+  COMMENT "Generating automaton source files"
+  COMMAND ${BISON_EXE} --name-prefix=xbt_automaton_parser_ -d parserPromela.yacc
+  COMMAND ${LEX_EXE} --prefix=xbt_automaton_parser_ --outfile=automaton_lexer.yy.c parserPromela.lex
   WORKING_DIRECTORY ${CMAKE_HOME_DIRECTORY}/src/xbt/automaton/
   )
 
   SET_DIRECTORY_PROPERTIES(PROPERTIES ADDITIONAL_MAKE_CLEAN_FILES
-  "${CMAKE_HOME_DIRECTORY}/src/xbt/automaton/y.tab.c;${CMAKE_HOME_DIRECTORY}/src/xbt/automaton/y.tab.h;${CMAKE_HOME_DIRECTORY}/src/xbt/automaton/automaton_parse.yy.c"
+  "${CMAKE_HOME_DIRECTORY}/src/xbt/automaton/parserPromela.tab.cacc;${CMAKE_HOME_DIRECTORY}/src/xbt/automaton/parserPromela.tab.hacc;${CMAKE_HOME_DIRECTORY}/src/xbt/automaton/automaton_parse.yy.c"
   )
-endif(YACC_EXE AND LEX_EXE)
+endif(BISON_EXE AND LEX_EXE)
 
 IF(FLEX_EXE)
        set(HAVE_FLEX 1)
index 6d373a1..52d66f3 100644 (file)
@@ -154,6 +154,6 @@ endif(enable_lib_static)
 
 # Dependencies from maintainer mode
 ###################################
-if(enable_maintainer_mode AND YACC_EXE AND LEX_EXE)
+if(enable_maintainer_mode AND BISON_EXE AND LEX_EXE)
   add_dependencies(simgrid automaton_generated_src)
-endif(enable_maintainer_mode AND YACC_EXE AND LEX_EXE)
\ No newline at end of file
+endif(enable_maintainer_mode AND BISON_EXE AND LEX_EXE)
\ No newline at end of file
index 784e667..b1f2112 100644 (file)
@@ -128,16 +128,16 @@ int client(int argc, char *argv[])
 
 int main(int argc, char *argv[])
 {
-  xbt_automaton_t a = MC_create_automaton("promela1_bugged1_liveness");
-  xbt_new_propositional_symbol(a,"r", &predR); 
-  xbt_new_propositional_symbol(a,"cs", &predCS); 
+  MC_automaton_load("promela1_bugged1_liveness");
+  MC_automaton_new_propositional_symbol("r", &predR);
+  MC_automaton_new_propositional_symbol("cs", &predCS);
   
   MSG_init(&argc, argv);
   MSG_create_environment("../msg_platform.xml");
   MSG_function_register("coordinator", coordinator);
   MSG_function_register("client", client);
   MSG_launch_application("deploy_bugged1_liveness.xml");
-  MSG_main_liveness(a);
+  MSG_main_liveness();
 
   return 0;
 }
index 8d2bdb2..b8da0a1 100644 (file)
@@ -119,16 +119,16 @@ int client(int argc, char *argv[])
 int main(int argc, char *argv[])
 {
 
-  xbt_automaton_t a = MC_create_automaton("promela1_bugged1_liveness");
-  xbt_new_propositional_symbol(a,"r", &predR); 
-  xbt_new_propositional_symbol(a,"cs", &predCS); 
+  MC_automaton_load("promela1_bugged1_liveness");
+  MC_automaton_new_propositional_symbol("r", &predR);
+  MC_automaton_new_propositional_symbol("cs", &predCS);
   
   MSG_init(&argc, argv);
   MSG_create_environment("../msg_platform.xml");
   MSG_function_register("coordinator", coordinator);
   MSG_function_register("client", client);
   MSG_launch_application("deploy_bugged1_liveness.xml");
-  MSG_main_liveness(a);
+  MSG_main_liveness();
 
   return 0;
 }
index 25a35ca..3209cff 100644 (file)
@@ -172,11 +172,11 @@ int main(int argc, char *argv[])
   buffer = malloc(8*sizeof(char));
   buffer[0]='\0';
 
-  xbt_automaton_t a = MC_create_automaton("promela2_bugged2_liveness");
-  xbt_new_propositional_symbol(a,"pready", &predPready); 
-  xbt_new_propositional_symbol(a,"cready", &predCready); 
-  xbt_new_propositional_symbol(a,"consume", &predConsume);
-  xbt_new_propositional_symbol(a,"produce", &predProduce); 
+  MC_automaton_load("promela2_bugged2_liveness");
+  MC_automaton_new_propositional_symbol("pready", &predPready);
+  MC_automaton_new_propositional_symbol("cready", &predCready);
+  MC_automaton_new_propositional_symbol("consume", &predConsume);
+  MC_automaton_new_propositional_symbol("produce", &predProduce);
   
   MSG_init(&argc, argv);
   MSG_create_environment("../msg_platform.xml");
@@ -184,7 +184,7 @@ int main(int argc, char *argv[])
   MSG_function_register("consumer", consumer);
   MSG_function_register("producer", producer);
   MSG_launch_application("deploy_bugged2_liveness.xml");
-  MSG_main_liveness(a);
+  MSG_main_liveness();
 
   return 0;
 
index c78c267..b031038 100644 (file)
@@ -99,15 +99,15 @@ int client(int argc, char *argv[])
 int main(int argc, char *argv[])
 {
   
-  xbt_automaton_t a = MC_create_automaton("promela_centralized_liveness");
-  xbt_new_propositional_symbol(a,"cs", &predCS); 
+  MC_automaton_load("promela_centralized_liveness");
+  MC_automaton_new_propositional_symbol("cs", &predCS);
   
   MSG_init(&argc, argv);
   MSG_create_environment("../msg_platform.xml");
   MSG_function_register("coordinator", coordinator);
   MSG_function_register("client", client);
   MSG_launch_application("deploy_centralized_liveness.xml");
-  MSG_main_liveness(a);
+  MSG_main_liveness();
 
   return 0;
 
index 3c02d51..6d1e175 100644 (file)
@@ -96,15 +96,15 @@ int client(int argc, char *argv[])
 int main(int argc, char *argv[])
 {
 
-  xbt_automaton_t a = MC_create_automaton("promela_centralized_liveness");
-  xbt_new_propositional_symbol(a,"cs", &predCS); 
+  MC_automaton_load("promela_centralized_liveness");
+  MC_automaton_new_propositional_symbol("cs", &predCS);
   
   MSG_init(&argc, argv);
   MSG_create_environment("../msg_platform.xml");
   MSG_function_register("coordinator", coordinator);
   MSG_function_register("client", client);
   MSG_launch_application("deploy_centralized_liveness.xml");
-  MSG_main_liveness(a);
+  MSG_main_liveness();
 
   return 0;
 
index 77260db..59c7fc6 100644 (file)
@@ -1,7 +1,6 @@
 #include "msg/msg.h"
 #include "mc/mc.h"
 #include "xbt/automaton.h"
-#include "xbt/automatonparse_promela.h"
 #include "test_snapshot.h"
 //#include "y.tab.c"
 #include <stdlib.h>
@@ -130,18 +129,16 @@ int main(int argc, char *argv[])
   xbt_dynar_push(d1, &c1);
   xbt_dynar_push(d1, &c1);
 
-  init();
-  yyparse();
-  automaton = get_automaton();
-  xbt_new_propositional_symbol(automaton,"r", &predR); 
-  xbt_new_propositional_symbol(automaton,"cs", &predCS); 
+  MC_automaton_load("promela_test_snapshot");
+  MC_automaton_new_propositional_symbol("r", &predR);
+  MC_automaton_new_propositional_symbol("cs", &predCS);
   
   MSG_init(&argc, argv);
   MSG_create_environment("../msg_platform.xml");
   MSG_function_register("coordinator", coordinator);
   MSG_function_register("client", client);
   MSG_launch_application("deploy_test_snapshot.xml");
-  MSG_main_liveness(automaton);
+  MSG_main_liveness();
 
   return 0;
 }
index 4a37ef4..da0fca1 100644 (file)
@@ -9,7 +9,6 @@
 #include "xbt.h"
 
 #include "msg/datatypes.h"
-#include "xbt/automaton.h"
 
 #include "simgrid/simix.h"
 
@@ -58,7 +57,7 @@ XBT_PUBLIC(void) MSG_config(const char *name, ...);
 
 XBT_PUBLIC(void) MSG_init_nocheck(int *argc, char **argv);
 XBT_PUBLIC(MSG_error_t) MSG_main(void);
-XBT_PUBLIC(MSG_error_t) MSG_main_liveness(xbt_automaton_t a);
+XBT_PUBLIC(MSG_error_t) MSG_main_liveness(void);
 XBT_PUBLIC(MSG_error_t) MSG_clean(void);
 XBT_PUBLIC(void) MSG_function_register(const char *name,
                                        xbt_main_func_t code);
index 2752cbd..da83b88 100644 (file)
@@ -20,7 +20,9 @@ extern int _surf_do_model_check;
 XBT_PUBLIC(void) MC_assert(int);
 XBT_PUBLIC(int) MC_random(int min, int max);
 XBT_PUBLIC(void) MC_diff(void);
-XBT_PUBLIC(xbt_automaton_t) MC_create_automaton(const char *file);
+XBT_PUBLIC(void) MC_automaton_load(const char *file);
+XBT_PUBLIC(void) MC_automaton_new_propositional_symbol(const char* id, void* fct);
+
 
 #else
 
index f140ed2..49df463 100644 (file)
@@ -59,7 +59,8 @@ typedef struct xbt_propositional_symbol{
 typedef struct xbt_propositional_symbol* xbt_propositional_symbol_t;
 
 
-XBT_PUBLIC(xbt_automaton_t) xbt_automaton_new_automaton(void);
+XBT_PUBLIC(xbt_automaton_t) xbt_automaton_new(void);
+XBT_PUBLIC(void) xbt_automaton_load(xbt_automaton_t automaton, const char *file);
 
 XBT_PUBLIC(xbt_state_t) xbt_automaton_new_state(xbt_automaton_t a, int type, char* id);
 
diff --git a/include/xbt/automatonparse_promela.h b/include/xbt/automatonparse_promela.h
deleted file mode 100644 (file)
index d461474..0000000
+++ /dev/null
@@ -1,26 +0,0 @@
-#ifndef _XBT_AUTOMATONPARSE_PROMELA_H
-#define _XBT_AUTOMATONPARSE_PROMELA_H
-
-#include <stdlib.h>
-#include <string.h>
-#include "xbt/automaton.h"
-
-SG_BEGIN_DECL()
-
-XBT_PUBLIC_DATA(xbt_automaton_t) automaton;
-
-XBT_PUBLIC(void) init(void);
-
-XBT_PUBLIC(void) new_state(char* id, int src);
-
-XBT_PUBLIC(void) new_transition(char* id, xbt_exp_label_t label);
-
-XBT_PUBLIC(xbt_exp_label_t) new_label(int type, ...);
-
-XBT_PUBLIC(xbt_automaton_t) get_automaton(void);
-          
-XBT_PUBLIC(void) display_automaton(void);
-
-SG_END_DECL()
-
-#endif
index cf0bab6..52c568d 100644 (file)
@@ -24,7 +24,7 @@ XBT_PUBLIC(void) MC_init_safety(void);
 XBT_PUBLIC(void) MC_exit(void);
 XBT_PUBLIC(void) MC_exit_liveness(void);
 XBT_PUBLIC(void) MC_modelcheck(void);
-XBT_PUBLIC(void) MC_modelcheck_liveness(xbt_automaton_t a);
+XBT_PUBLIC(void) MC_modelcheck_liveness(void);
 XBT_PUBLIC(void) MC_process_clock_add(smx_process_t, double);
 XBT_PUBLIC(double) MC_process_clock_get(smx_process_t);
 
index 211f26b..f62e2f7 100644 (file)
@@ -12,7 +12,7 @@
 #include "../simix/smx_private.h"
 #include "xbt/fifo.h"
 #include "mc_private.h"
-#include "xbt/automaton/automaton_create.h"
+#include "xbt/automaton.h"
 
 XBT_LOG_NEW_CATEGORY(mc, "All MC categories");
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_global, mc,
@@ -36,9 +36,8 @@ mc_stats_pair_t mc_stats_pair = NULL;
 xbt_fifo_t mc_stack_liveness = NULL;
 mc_snapshot_t initial_snapshot_liveness = NULL;
 
-xbt_automaton_t automaton;
+xbt_automaton_t _mc_property_automaton = NULL;
 
-static void MC_init_liveness(xbt_automaton_t a);
 static void MC_assert_pair(int prop);
 
 
@@ -78,8 +77,16 @@ void MC_init_safety(void)
 }
 
 
-static void MC_init_liveness(xbt_automaton_t a){
 
+void MC_modelcheck(void)
+{
+  MC_init_safety();
+  MC_dpor();
+  MC_exit();
+}
+
+void MC_modelcheck_liveness(){
+  /* init stuff */
   XBT_DEBUG("Start init mc");
   
   mc_time = xbt_new0(double, simix_process_maxpid);
@@ -99,30 +106,10 @@ static void MC_init_liveness(xbt_automaton_t a){
 
   MC_UNSET_RAW_MEM;
 
-  automaton = a;
 
   MC_ddfs_init();
 
-  
-}
-
-
-void MC_modelcheck(void)
-{
-  MC_init_safety();
-  MC_dpor();
-  MC_exit();
-}
-
-
-
-void MC_modelcheck_liveness(xbt_automaton_t a){
-  MC_init_liveness(a);
-  MC_exit_liveness();
-}
-
-void MC_exit_liveness(void)
-{
+  /* We're done */
   MC_print_statistics_pairs(mc_stats_pair);
   //xbt_free(mc_time);
   //MC_memory_exit();
@@ -531,9 +518,17 @@ void MC_diff(void){
 
 }
 
-xbt_automaton_t MC_create_automaton(const char *file){
+void MC_automaton_load(const char *file){
+  MC_SET_RAW_MEM;
+  if (_mc_property_automaton == NULL)
+    _mc_property_automaton = xbt_automaton_new();
+  xbt_automaton_load(_mc_property_automaton,file);
+  MC_UNSET_RAW_MEM;
+}
+void MC_automaton_new_propositional_symbol(const char* id, void* fct) {
   MC_SET_RAW_MEM;
-  xbt_automaton_t a = xbt_create_automaton(file);
+  if (_mc_property_automaton == NULL)
+    _mc_property_automaton = xbt_automaton_new();
+  xbt_new_propositional_symbol(_mc_property_automaton,id,fct);
   MC_UNSET_RAW_MEM;
-  return a;
 }
index a49dbfb..08a6d54 100644 (file)
@@ -156,7 +156,7 @@ int reached(xbt_state_t st){
     /* Get values of propositional symbols */
     unsigned int cursor = 0;
     xbt_propositional_symbol_t ps = NULL;
-    xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){
+    xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
       f = (int_f_void_t)ps->function;
       res = (*f)();
       xbt_dynar_push_as(prop_ato, int, res);
@@ -384,7 +384,7 @@ void set_pair_reached(xbt_state_t st){
   int res;
   int_f_void_t f;
 
-  xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){
+  xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
     f = (int_f_void_t)ps->function;
     res = (*f)();
     xbt_dynar_push_as(pair->prop_ato, int, res);
@@ -449,7 +449,7 @@ int reached_hash(xbt_state_t st){
     int res;
     int_f_void_t f;
 
-    xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){
+    xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
       f = (int_f_void_t)ps->function;
       res = (*f)();
       xbt_dynar_push_as(prop_ato, int, res);
@@ -523,7 +523,7 @@ void set_pair_reached_hash(xbt_state_t st){
   int res;
   int_f_void_t f;
 
-  xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){
+  xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
     f = (int_f_void_t)ps->function;
     res = (*f)();
     xbt_dynar_push_as(pair->prop_ato, int, res);
@@ -560,7 +560,7 @@ int visited(xbt_state_t st, int sc){
     int res;
     int_f_void_t f;
 
-    xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){
+    xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
       f = (int_f_void_t)ps->function;
       res = (*f)();
       xbt_dynar_push_as(prop_ato, int, res);
@@ -635,7 +635,7 @@ int visited_hash(xbt_state_t st, int sc){
     int res;
     int_f_void_t f;
 
-    xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){
+    xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
       f = (int_f_void_t)ps->function;
       res = (*f)();
       xbt_dynar_push_as(prop_ato, int, res);
@@ -713,7 +713,7 @@ void set_pair_visited_hash(xbt_state_t st, int sc){
   int res;
   int_f_void_t f;
 
-  xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){
+  xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
     f = (int_f_void_t)ps->function;
     res = (*f)();
     xbt_dynar_push_as(pair->prop_ato, int, res);
@@ -747,7 +747,7 @@ void set_pair_visited(xbt_state_t st, int sc){
   int res;
   int_f_void_t f;
 
-  xbt_dynar_foreach(automaton->propositional_symbols, cursor, ps){
+  xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
     f = (int_f_void_t)ps->function;
     res = (*f)();
     xbt_dynar_push_as(pair->prop_ato, int, res);
@@ -789,7 +789,7 @@ int MC_automaton_evaluate_label(xbt_exp_label_t l){
     unsigned int cursor = 0;
     xbt_propositional_symbol_t p = NULL;
     int_f_void_t f;
-    xbt_dynar_foreach(automaton->propositional_symbols, cursor, p){
+    xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, p){
       if(strcmp(p->pred, l->u.predicat) == 0){
         f = (int_f_void_t)p->function;
         return (*f)();
@@ -861,7 +861,7 @@ void MC_ddfs_init(void){
   unsigned int cursor = 0;
   xbt_state_t state;
 
-  xbt_dynar_foreach(automaton->states, cursor, state){
+  xbt_dynar_foreach(_mc_property_automaton->states, cursor, state){
     if(state->type == -1){
       
       MC_SET_RAW_MEM;
@@ -914,7 +914,7 @@ void MC_ddfs(int search_cycle){
   current_pair = (mc_pair_stateless_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness));
 
   /* Update current state in buchi automaton */
-  automaton->current_state = current_pair->automaton_state;
+  _mc_property_automaton->current_state = current_pair->automaton_state;
 
  
   XBT_INFO("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness), search_cycle);
index 9a0ee71..77d842d 100644 (file)
@@ -192,7 +192,7 @@ void MC_init_safety(void);
 /********************************** Double-DFS for liveness property**************************************/
 
 extern mc_snapshot_t initial_snapshot_liveness;
-extern xbt_automaton_t automaton;
+extern xbt_automaton_t _mc_property_automaton;
 
 typedef struct s_mc_pair{
   mc_snapshot_t system_state;
index 879461f..681bdef 100644 (file)
@@ -118,14 +118,14 @@ MSG_error_t MSG_main(void)
 }
 
 
-MSG_error_t MSG_main_liveness(xbt_automaton_t a)
+MSG_error_t MSG_main_liveness()
 {
   /* Clean IO before the run */
   fflush(stdout);
   fflush(stderr);
 
   if (MC_IS_ENABLED) {
-    MC_modelcheck_liveness(a);
+    MC_modelcheck_liveness();
   }
   else {
     SIMIX_run();
index dffad32..97c397c 100644 (file)
@@ -8,7 +8,7 @@
 
 #include "xbt/automaton.h"
 
-xbt_automaton_t xbt_automaton_new_automaton(){
+xbt_automaton_t xbt_automaton_new(){
   xbt_automaton_t automaton = NULL;
   automaton = xbt_new0(struct xbt_automaton, 1);
   automaton->states = xbt_dynar_new(sizeof(xbt_state_t), NULL);
diff --git a/src/xbt/automaton/automaton_create.c b/src/xbt/automaton/automaton_create.c
deleted file mode 100644 (file)
index 0b2ed30..0000000
+++ /dev/null
@@ -1,12 +0,0 @@
-#include "xbt/automatonparse_promela.h"
-#include "y.tab.c"
-#include "automaton_create.h"
-
-xbt_automaton_t xbt_create_automaton(const char *file){
-
-  init();
-  yyin = fopen(file, "r");
-  yyparse();
-  return automaton;
-
-}
diff --git a/src/xbt/automaton/automaton_create.h b/src/xbt/automaton/automaton_create.h
deleted file mode 100644 (file)
index 24d0ebe..0000000
+++ /dev/null
@@ -1,14 +0,0 @@
-/*  xbt/automaton/automaton_create.h -- büchi automaton                                      */
-
-/* Copyright (c) 2011. The SimGrid Team.
- * All rights reserved.                                                     */
-
-/* This program is free software; you can redistribute it and/or modify it
- * under the terms of the license (GNU LGPL) which comes with this package. */
-
-#ifndef _AUTOMATON_CREATE_H
-#define _AUTOMATON_CREATE_H
-
-xbt_automaton_t xbt_create_automaton(const char *file);
-
-#endif
similarity index 75%
rename from src/xbt/automaton/automaton_parse.yy.c
rename to src/xbt/automaton/automaton_lexer.yy.c
index a7395b1..5a5d379 100644 (file)
@@ -1,29 +1,29 @@
-#line 2 "automaton_parse.yy.c"
+#line 2 "automaton_lexer.yy.c"
 
-#line 4 "automaton_parse.yy.c"
+#line 4 "automaton_lexer.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 yy_create_buffer xbt_automaton_parser__create_buffer
+#define yy_delete_buffer xbt_automaton_parser__delete_buffer
+#define yy_flex_debug xbt_automaton_parser__flex_debug
+#define yy_init_buffer xbt_automaton_parser__init_buffer
+#define yy_flush_buffer xbt_automaton_parser__flush_buffer
+#define yy_load_buffer_state xbt_automaton_parser__load_buffer_state
+#define yy_switch_to_buffer xbt_automaton_parser__switch_to_buffer
+#define yyin xbt_automaton_parser_in
+#define yyleng xbt_automaton_parser_leng
+#define yylex xbt_automaton_parser_lex
+#define yylineno xbt_automaton_parser_lineno
+#define yyout xbt_automaton_parser_out
+#define yyrestart xbt_automaton_parser_restart
+#define yytext xbt_automaton_parser_text
+#define yywrap xbt_automaton_parser_wrap
+#define yyalloc xbt_automaton_parser_alloc
+#define yyrealloc xbt_automaton_parser_realloc
+#define yyfree xbt_automaton_parser_free
 
 #define FLEX_SCANNER
 #define YY_FLEX_MAJOR_VERSION 2
@@ -155,7 +155,7 @@ typedef unsigned int flex_uint32_t;
 #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_NEW_FILE xbt_automaton_parser_restart(xbt_automaton_parser_in  )
 
 #define YY_END_OF_BUFFER_CHAR 0
 
@@ -181,9 +181,9 @@ typedef unsigned int flex_uint32_t;
 typedef struct yy_buffer_state *YY_BUFFER_STATE;
 #endif
 
-extern int xbt_automaton_parse_leng;
+extern int xbt_automaton_parser_leng;
 
-extern FILE *xbt_automaton_parse_in, *xbt_automaton_parse_out;
+extern FILE *xbt_automaton_parser_in, *xbt_automaton_parser_out;
 
 #define EOB_ACT_CONTINUE_SCAN 0
 #define EOB_ACT_END_OF_FILE 1
@@ -195,13 +195,13 @@ extern FILE *xbt_automaton_parse_in, *xbt_automaton_parse_out;
 #define yyless(n) \
        do \
                { \
-               /* Undo effects of setting up xbt_automaton_parse_text. */ \
+               /* Undo effects of setting up xbt_automaton_parser_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 */ \
+               YY_DO_BEFORE_ACTION; /* set up xbt_automaton_parser_text again */ \
                } \
        while ( 0 )
 
@@ -269,8 +269,8 @@ struct yy_buffer_state
         * 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.
+        * (via xbt_automaton_parser_restart()), so that the user can continue scanning by
+        * just pointing xbt_automaton_parser_in at a new input file.
         */
 #define YY_BUFFER_EOF_PENDING 2
 
@@ -297,51 +297,51 @@ static YY_BUFFER_STATE * yy_buffer_stack = 0; /**< Stack as an array. */
  */
 #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. */
+/* yy_hold_char holds the character lost when xbt_automaton_parser_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;
+int xbt_automaton_parser_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 ...
+/* Flag which is used to allow xbt_automaton_parser_wrap()'s to do buffer switches
+ * instead of setting up a fresh xbt_automaton_parser_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 );
+void xbt_automaton_parser_restart (FILE *input_file  );
+void xbt_automaton_parser__switch_to_buffer (YY_BUFFER_STATE new_buffer  );
+YY_BUFFER_STATE xbt_automaton_parser__create_buffer (FILE *file,int size  );
+void xbt_automaton_parser__delete_buffer (YY_BUFFER_STATE b  );
+void xbt_automaton_parser__flush_buffer (YY_BUFFER_STATE b  );
+void xbt_automaton_parser_push_buffer_state (YY_BUFFER_STATE new_buffer  );
+void xbt_automaton_parser_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  );
+static void xbt_automaton_parser_ensure_buffer_stack (void );
+static void xbt_automaton_parser__load_buffer_state (void );
+static void xbt_automaton_parser__init_buffer (YY_BUFFER_STATE b,FILE *file  );
 
-#define YY_FLUSH_BUFFER xbt_automaton_parse__flush_buffer(YY_CURRENT_BUFFER )
+#define YY_FLUSH_BUFFER xbt_automaton_parser__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  );
+YY_BUFFER_STATE xbt_automaton_parser__scan_buffer (char *base,yy_size_t size  );
+YY_BUFFER_STATE xbt_automaton_parser__scan_string (yyconst char *yy_str  );
+YY_BUFFER_STATE xbt_automaton_parser__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 *  );
+void *xbt_automaton_parser_alloc (yy_size_t  );
+void *xbt_automaton_parser_realloc (void *,yy_size_t  );
+void xbt_automaton_parser_free (void *  );
 
-#define yy_new_buffer xbt_automaton_parse__create_buffer
+#define yy_new_buffer xbt_automaton_parser__create_buffer
 
 #define yy_set_interactive(is_interactive) \
        { \
        if ( ! YY_CURRENT_BUFFER ){ \
-        xbt_automaton_parse_ensure_buffer_stack (); \
+        xbt_automaton_parser_ensure_buffer_stack (); \
                YY_CURRENT_BUFFER_LVALUE =    \
-            xbt_automaton_parse__create_buffer(xbt_automaton_parse_in,YY_BUF_SIZE ); \
+            xbt_automaton_parser__create_buffer(xbt_automaton_parser_in,YY_BUF_SIZE ); \
        } \
        YY_CURRENT_BUFFER_LVALUE->yy_is_interactive = is_interactive; \
        }
@@ -349,9 +349,9 @@ void xbt_automaton_parse_free (void *  );
 #define yy_set_bol(at_bol) \
        { \
        if ( ! YY_CURRENT_BUFFER ){\
-        xbt_automaton_parse_ensure_buffer_stack (); \
+        xbt_automaton_parser_ensure_buffer_stack (); \
                YY_CURRENT_BUFFER_LVALUE =    \
-            xbt_automaton_parse__create_buffer(xbt_automaton_parse_in,YY_BUF_SIZE ); \
+            xbt_automaton_parser__create_buffer(xbt_automaton_parser_in,YY_BUF_SIZE ); \
        } \
        YY_CURRENT_BUFFER_LVALUE->yy_at_bol = at_bol; \
        }
@@ -360,21 +360,21 @@ void xbt_automaton_parse_free (void *  );
 
 /* Begin user sect3 */
 
-#define xbt_automaton_parse_wrap(n) 1
+#define xbt_automaton_parser_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;
+FILE *xbt_automaton_parser_in = (FILE *) 0, *xbt_automaton_parser_out = (FILE *) 0;
 
 typedef int yy_state_type;
 
-extern int xbt_automaton_parse_lineno;
+extern int xbt_automaton_parser_lineno;
 
-int xbt_automaton_parse_lineno = 1;
+int xbt_automaton_parser_lineno = 1;
 
-extern char *xbt_automaton_parse_text;
-#define yytext_ptr xbt_automaton_parse_text
+extern char *xbt_automaton_parser_text;
+#define yytext_ptr xbt_automaton_parser_text
 
 static yy_state_type yy_get_previous_state (void );
 static yy_state_type yy_try_NUL_trans (yy_state_type current_state  );
@@ -382,11 +382,11 @@ 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.
+ * corresponding action - sets up xbt_automaton_parser_text.
  */
 #define YY_DO_BEFORE_ACTION \
        (yytext_ptr) = yy_bp; \
-       xbt_automaton_parse_leng = (size_t) (yy_cp - yy_bp); \
+       xbt_automaton_parser_leng = (size_t) (yy_cp - yy_bp); \
        (yy_hold_char) = *yy_cp; \
        *yy_cp = '\0'; \
        (yy_c_buf_p) = yy_cp;
@@ -509,8 +509,8 @@ static yyconst flex_int16_t yy_chk[124] =
 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;
+extern int xbt_automaton_parser__flex_debug;
+int xbt_automaton_parser__flex_debug = 0;
 
 /* The intent behind this definition is that it'll catch
  * any uses of REJECT which flex missed.
@@ -519,17 +519,17 @@ int xbt_automaton_parse__flex_debug = 0;
 #define yymore() yymore_used_but_not_detected
 #define YY_MORE_ADJ 0
 #define YY_RESTORE_YY_MORE_OFFSET
-char *xbt_automaton_parse_text;
+char *xbt_automaton_parser_text;
 #line 1 "parserPromela.lex"
 #line 4 "parserPromela.lex"
 
 
 #include <stdio.h>
-#include "y.tab.h"
+#include "parserPromela.tab.hacc"
   
   extern YYSTYPE yylval;
  
-#line 533 "automaton_parse.yy.c"
+#line 533 "automaton_lexer.yy.c"
 
 #define INITIAL 0
 
@@ -550,31 +550,31 @@ 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_parser_lex_destroy (void );
 
-int xbt_automaton_parse_get_debug (void );
+int xbt_automaton_parser_get_debug (void );
 
-void xbt_automaton_parse_set_debug (int debug_flag  );
+void xbt_automaton_parser_set_debug (int debug_flag  );
 
-YY_EXTRA_TYPE xbt_automaton_parse_get_extra (void );
+YY_EXTRA_TYPE xbt_automaton_parser_get_extra (void );
 
-void xbt_automaton_parse_set_extra (YY_EXTRA_TYPE user_defined  );
+void xbt_automaton_parser_set_extra (YY_EXTRA_TYPE user_defined  );
 
-FILE *xbt_automaton_parse_get_in (void );
+FILE *xbt_automaton_parser_get_in (void );
 
-void xbt_automaton_parse_set_in  (FILE * in_str  );
+void xbt_automaton_parser_set_in  (FILE * in_str  );
 
-FILE *xbt_automaton_parse_get_out (void );
+FILE *xbt_automaton_parser_get_out (void );
 
-void xbt_automaton_parse_set_out  (FILE * out_str  );
+void xbt_automaton_parser_set_out  (FILE * out_str  );
 
-int xbt_automaton_parse_get_leng (void );
+int xbt_automaton_parser_get_leng (void );
 
-char *xbt_automaton_parse_get_text (void );
+char *xbt_automaton_parser_get_text (void );
 
-int xbt_automaton_parse_get_lineno (void );
+int xbt_automaton_parser_get_lineno (void );
 
-void xbt_automaton_parse_set_lineno (int line_number  );
+void xbt_automaton_parser_set_lineno (int line_number  );
 
 /* Macros after this point can all be overridden by user definitions in
  * section 1.
@@ -582,9 +582,9 @@ void xbt_automaton_parse_set_lineno (int line_number  );
 
 #ifndef YY_SKIP_YYWRAP
 #ifdef __cplusplus
-extern "C" int xbt_automaton_parse_wrap (void );
+extern "C" int xbt_automaton_parser_wrap (void );
 #else
-extern int xbt_automaton_parse_wrap (void );
+extern int xbt_automaton_parser_wrap (void );
 #endif
 #endif
 
@@ -623,7 +623,7 @@ static int input (void );
 /* 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)
+#define ECHO do { if (fwrite( xbt_automaton_parser_text, xbt_automaton_parser_leng, 1, xbt_automaton_parser_out )) {} } while (0)
 #endif
 
 /* Gets input and stuffs it into "buf".  number of characters read, or YY_NULL,
@@ -636,18 +636,18 @@ static int input (void );
                int c = '*'; \
                size_t n; \
                for ( n = 0; n < max_size && \
-                            (c = getc( xbt_automaton_parse_in )) != EOF && c != '\n'; ++n ) \
+                            (c = getc( xbt_automaton_parser_in )) != EOF && c != '\n'; ++n ) \
                        buf[n] = (char) c; \
                if ( c == '\n' ) \
                        buf[n++] = (char) c; \
-               if ( c == EOF && ferror( xbt_automaton_parse_in ) ) \
+               if ( c == EOF && ferror( xbt_automaton_parser_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)) \
+               while ( (result = fread(buf, 1, max_size, xbt_automaton_parser_in))==0 && ferror(xbt_automaton_parser_in)) \
                        { \
                        if( errno != EINTR) \
                                { \
@@ -655,7 +655,7 @@ static int input (void );
                                break; \
                                } \
                        errno=0; \
-                       clearerr(xbt_automaton_parse_in); \
+                       clearerr(xbt_automaton_parser_in); \
                        } \
                }\
 \
@@ -688,12 +688,12 @@ static int input (void );
 #ifndef YY_DECL
 #define YY_DECL_IS_OURS 1
 
-extern int xbt_automaton_parse_lex (void);
+extern int xbt_automaton_parser_lex (void);
 
-#define YY_DECL int xbt_automaton_parse_lex (void)
+#define YY_DECL int xbt_automaton_parser_lex (void)
 #endif /* !YY_DECL */
 
-/* Code executed at the beginning of each rule, after xbt_automaton_parse_text and xbt_automaton_parse_leng
+/* Code executed at the beginning of each rule, after xbt_automaton_parser_text and xbt_automaton_parser_leng
  * have been set up.
  */
 #ifndef YY_USER_ACTION
@@ -719,7 +719,7 @@ YY_DECL
 #line 28 "parserPromela.lex"
 
 
-#line 723 "automaton_parse.yy.c"
+#line 723 "automaton_lexer.yy.c"
 
        if ( !(yy_init) )
                {
@@ -732,26 +732,26 @@ YY_DECL
                if ( ! (yy_start) )
                        (yy_start) = 1; /* first start state */
 
-               if ( ! xbt_automaton_parse_in )
-                       xbt_automaton_parse_in = stdin;
+               if ( ! xbt_automaton_parser_in )
+                       xbt_automaton_parser_in = stdin;
 
-               if ( ! xbt_automaton_parse_out )
-                       xbt_automaton_parse_out = stdout;
+               if ( ! xbt_automaton_parser_out )
+                       xbt_automaton_parser_out = stdout;
 
                if ( ! YY_CURRENT_BUFFER ) {
-                       xbt_automaton_parse_ensure_buffer_stack ();
+                       xbt_automaton_parser_ensure_buffer_stack ();
                        YY_CURRENT_BUFFER_LVALUE =
-                               xbt_automaton_parse__create_buffer(xbt_automaton_parse_in,YY_BUF_SIZE );
+                               xbt_automaton_parser__create_buffer(xbt_automaton_parser_in,YY_BUF_SIZE );
                }
 
-               xbt_automaton_parse__load_buffer_state( );
+               xbt_automaton_parser__load_buffer_state( );
                }
 
        while ( 1 )             /* loops until end-of-file is reached */
                {
                yy_cp = (yy_c_buf_p);
 
-               /* Support of xbt_automaton_parse_text. */
+               /* Support of xbt_automaton_parser_text. */
                *yy_cp = (yy_hold_char);
 
                /* yy_bp points to the position in yy_ch_buf of the start of
@@ -805,83 +805,83 @@ do_action:        /* This label is used only to access EOF actions. */
 case 1:
 YY_RULE_SETUP
 #line 30 "parserPromela.lex"
-{ printf("%s", xbt_automaton_parse_text); return (NEVER); }
+{ printf("%s", xbt_automaton_parser_text); return (NEVER); }
        YY_BREAK
 case 2:
 YY_RULE_SETUP
 #line 31 "parserPromela.lex"
-{ printf("%s", xbt_automaton_parse_text); return (IF); }
+{ printf("%s", xbt_automaton_parser_text); return (IF); }
        YY_BREAK
 case 3:
 YY_RULE_SETUP
 #line 32 "parserPromela.lex"
-{ printf("%s", xbt_automaton_parse_text); 
+{ printf("%s", xbt_automaton_parser_text); 
                return (FI); }
        YY_BREAK
 case 4:
 YY_RULE_SETUP
 #line 34 "parserPromela.lex"
-{ printf("%s", xbt_automaton_parse_text); return (IMPLIES); }
+{ printf("%s", xbt_automaton_parser_text); return (IMPLIES); }
        YY_BREAK
 case 5:
 YY_RULE_SETUP
 #line 35 "parserPromela.lex"
-{ printf("%s", xbt_automaton_parse_text); return (GOTO); }
+{ printf("%s", xbt_automaton_parser_text); return (GOTO); }
        YY_BREAK
 case 6:
 YY_RULE_SETUP
 #line 36 "parserPromela.lex"
-{ printf("%s", xbt_automaton_parse_text); return (AND); }
+{ printf("%s", xbt_automaton_parser_text); return (AND); }
        YY_BREAK
 case 7:
 YY_RULE_SETUP
 #line 37 "parserPromela.lex"
-{ printf("%s", xbt_automaton_parse_text); return (OR); }
+{ printf("%s", xbt_automaton_parser_text); return (OR); }
        YY_BREAK
 case 8:
 YY_RULE_SETUP
 #line 38 "parserPromela.lex"
-{ printf("%s", xbt_automaton_parse_text); return (NOT); }
+{ printf("%s", xbt_automaton_parser_text); return (NOT); }
        YY_BREAK
 case 9:
 YY_RULE_SETUP
 #line 39 "parserPromela.lex"
-{ printf("%s", xbt_automaton_parse_text); return (LEFT_PAR); }
+{ printf("%s", xbt_automaton_parser_text); return (LEFT_PAR); }
        YY_BREAK
 case 10:
 YY_RULE_SETUP
 #line 40 "parserPromela.lex"
-{ printf("%s", xbt_automaton_parse_text); return (RIGHT_PAR); }
+{ printf("%s", xbt_automaton_parser_text); return (RIGHT_PAR); }
        YY_BREAK
 case 11:
 YY_RULE_SETUP
 #line 41 "parserPromela.lex"
-{ printf("%s", xbt_automaton_parse_text); return (CASE); }
+{ printf("%s", xbt_automaton_parser_text); return (CASE); }
        YY_BREAK
 case 12:
 YY_RULE_SETUP
 #line 42 "parserPromela.lex"
-{ printf("%s", xbt_automaton_parse_text); return (COLON); }
+{ printf("%s", xbt_automaton_parser_text); return (COLON); }
        YY_BREAK
 case 13:
 YY_RULE_SETUP
 #line 43 "parserPromela.lex"
-{ printf("%s", xbt_automaton_parse_text); return (SEMI_COLON); }
+{ printf("%s", xbt_automaton_parser_text); return (SEMI_COLON); }
        YY_BREAK
 case 14:
 YY_RULE_SETUP
 #line 44 "parserPromela.lex"
-{ printf("%s", xbt_automaton_parse_text); return (CASE_TRUE); }
+{ printf("%s", xbt_automaton_parser_text); return (CASE_TRUE); }
        YY_BREAK
 case 15:
 YY_RULE_SETUP
 #line 45 "parserPromela.lex"
-{ printf("%s", xbt_automaton_parse_text); return (LEFT_BRACE); }
+{ printf("%s", xbt_automaton_parser_text); return (LEFT_BRACE); }
        YY_BREAK
 case 16:
 YY_RULE_SETUP
 #line 46 "parserPromela.lex"
-{ printf("%s", xbt_automaton_parse_text); return (RIGHT_BRACE); }
+{ printf("%s", xbt_automaton_parser_text); return (RIGHT_BRACE); }
        YY_BREAK
 case 17:
 /* rule 17 can match eol */
@@ -892,37 +892,37 @@ YY_RULE_SETUP
 case 18:
 YY_RULE_SETUP
 #line 51 "parserPromela.lex"
-{ printf("%s",xbt_automaton_parse_text); }
+{ printf("%s",xbt_automaton_parser_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); 
+{ printf("%s",xbt_automaton_parser_text); 
+                            sscanf(xbt_automaton_parser_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); 
+{ printf("%s",xbt_automaton_parser_text); 
+                            sscanf(xbt_automaton_parser_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); 
+{ printf("%s",xbt_automaton_parser_text);  
+                            yylval.string=(char *)malloc(strlen(xbt_automaton_parser_text)+1);
+                            sscanf(xbt_automaton_parser_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);
+{ printf("%s",xbt_automaton_parser_text); 
+                           yylval.string=(char *)malloc(strlen(xbt_automaton_parser_text)+1);
+                           sscanf(xbt_automaton_parser_text,"%s",yylval.string);
                            return (ID); }
        YY_BREAK
 case 23:
@@ -941,7 +941,7 @@ YY_RULE_SETUP
 #line 76 "parserPromela.lex"
 ECHO;
        YY_BREAK
-#line 945 "automaton_parse.yy.c"
+#line 945 "automaton_lexer.yy.c"
 case YY_STATE_EOF(INITIAL):
        yyterminate();
 
@@ -958,15 +958,15 @@ case YY_STATE_EOF(INITIAL):
                        {
                        /* 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
+                        * just pointed xbt_automaton_parser_in at a new source and called
+                        * xbt_automaton_parser_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_input_file = xbt_automaton_parser_in;
                        YY_CURRENT_BUFFER_LVALUE->yy_buffer_status = YY_BUFFER_NORMAL;
                        }
 
@@ -1019,11 +1019,11 @@ case YY_STATE_EOF(INITIAL):
                                {
                                (yy_did_buffer_switch_on_eof) = 0;
 
-                               if ( xbt_automaton_parse_wrap( ) )
+                               if ( xbt_automaton_parser_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
+                                        * xbt_automaton_parser_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
@@ -1072,7 +1072,7 @@ case YY_STATE_EOF(INITIAL):
                        "fatal flex scanner internal error--no action found" );
        } /* end of action switch */
                } /* end of scanning one token */
-} /* end of xbt_automaton_parse_lex */
+} /* end of xbt_automaton_parser_lex */
 
 /* yy_get_next_buffer - try to read in a new buffer
  *
@@ -1150,7 +1150,7 @@ static int yy_get_next_buffer (void)
 
                                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  );
+                                       xbt_automaton_parser_realloc((void *) b->yy_ch_buf,b->yy_buf_size + 2  );
                                }
                        else
                                /* Can't grow it, we don't own it. */
@@ -1182,7 +1182,7 @@ static int yy_get_next_buffer (void)
                if ( number_to_move == YY_MORE_ADJ )
                        {
                        ret_val = EOB_ACT_END_OF_FILE;
-                       xbt_automaton_parse_restart(xbt_automaton_parse_in  );
+                       xbt_automaton_parser_restart(xbt_automaton_parser_in  );
                        }
 
                else
@@ -1199,7 +1199,7 @@ static int yy_get_next_buffer (void)
        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  );
+               YY_CURRENT_BUFFER_LVALUE->yy_ch_buf = (char *) xbt_automaton_parser_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()" );
        }
@@ -1276,7 +1276,7 @@ static int yy_get_next_buffer (void)
     
     yy_cp = (yy_c_buf_p);
 
-       /* undo effects of setting up xbt_automaton_parse_text */
+       /* undo effects of setting up xbt_automaton_parser_text */
        *yy_cp = (yy_hold_char);
 
        if ( yy_cp < YY_CURRENT_BUFFER_LVALUE->yy_ch_buf + 2 )
@@ -1348,13 +1348,13 @@ static int yy_get_next_buffer (void)
                                         */
 
                                        /* Reset buffer status. */
-                                       xbt_automaton_parse_restart(xbt_automaton_parse_in );
+                                       xbt_automaton_parser_restart(xbt_automaton_parser_in );
 
                                        /*FALLTHROUGH*/
 
                                case EOB_ACT_END_OF_FILE:
                                        {
-                                       if ( xbt_automaton_parse_wrap( ) )
+                                       if ( xbt_automaton_parser_wrap( ) )
                                                return EOF;
 
                                        if ( ! (yy_did_buffer_switch_on_eof) )
@@ -1374,7 +1374,7 @@ static int yy_get_next_buffer (void)
                }
 
        c = *(unsigned char *) (yy_c_buf_p);    /* cast for 8-bit char's */
-       *(yy_c_buf_p) = '\0';   /* preserve xbt_automaton_parse_text */
+       *(yy_c_buf_p) = '\0';   /* preserve xbt_automaton_parser_text */
        (yy_hold_char) = *++(yy_c_buf_p);
 
        return c;
@@ -1386,32 +1386,32 @@ static int yy_get_next_buffer (void)
  * 
  * @note This function does not reset the start condition to @c INITIAL .
  */
-    void xbt_automaton_parse_restart  (FILE * input_file )
+    void xbt_automaton_parser_restart  (FILE * input_file )
 {
     
        if ( ! YY_CURRENT_BUFFER ){
-        xbt_automaton_parse_ensure_buffer_stack ();
+        xbt_automaton_parser_ensure_buffer_stack ();
                YY_CURRENT_BUFFER_LVALUE =
-            xbt_automaton_parse__create_buffer(xbt_automaton_parse_in,YY_BUF_SIZE );
+            xbt_automaton_parser__create_buffer(xbt_automaton_parser_in,YY_BUF_SIZE );
        }
 
-       xbt_automaton_parse__init_buffer(YY_CURRENT_BUFFER,input_file );
-       xbt_automaton_parse__load_buffer_state( );
+       xbt_automaton_parser__init_buffer(YY_CURRENT_BUFFER,input_file );
+       xbt_automaton_parser__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 )
+    void xbt_automaton_parser__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_parser_pop_buffer_state();
+        *              xbt_automaton_parser_push_buffer_state(new_buffer);
      */
-       xbt_automaton_parse_ensure_buffer_stack ();
+       xbt_automaton_parser_ensure_buffer_stack ();
        if ( YY_CURRENT_BUFFER == new_buffer )
                return;
 
@@ -1424,21 +1424,21 @@ static int yy_get_next_buffer (void)
                }
 
        YY_CURRENT_BUFFER_LVALUE = new_buffer;
-       xbt_automaton_parse__load_buffer_state( );
+       xbt_automaton_parser__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
+        * EOF (xbt_automaton_parser_wrap()) processing, but the only time this flag
+        * is looked at is after xbt_automaton_parser_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)
+static void xbt_automaton_parser__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;
+       xbt_automaton_parser_in = YY_CURRENT_BUFFER_LVALUE->yy_input_file;
        (yy_hold_char) = *(yy_c_buf_p);
 }
 
@@ -1448,35 +1448,35 @@ static void xbt_automaton_parse__load_buffer_state  (void)
  * 
  * @return the allocated buffer state.
  */
-    YY_BUFFER_STATE xbt_automaton_parse__create_buffer  (FILE * file, int  size )
+    YY_BUFFER_STATE xbt_automaton_parser__create_buffer  (FILE * file, int  size )
 {
        YY_BUFFER_STATE b;
     
-       b = (YY_BUFFER_STATE) xbt_automaton_parse_alloc(sizeof( struct yy_buffer_state )  );
+       b = (YY_BUFFER_STATE) xbt_automaton_parser_alloc(sizeof( struct yy_buffer_state )  );
        if ( ! b )
-               YY_FATAL_ERROR( "out of dynamic memory in xbt_automaton_parse__create_buffer()" );
+               YY_FATAL_ERROR( "out of dynamic memory in xbt_automaton_parser__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  );
+       b->yy_ch_buf = (char *) xbt_automaton_parser_alloc(b->yy_buf_size + 2  );
        if ( ! b->yy_ch_buf )
-               YY_FATAL_ERROR( "out of dynamic memory in xbt_automaton_parse__create_buffer()" );
+               YY_FATAL_ERROR( "out of dynamic memory in xbt_automaton_parser__create_buffer()" );
 
        b->yy_is_our_buffer = 1;
 
-       xbt_automaton_parse__init_buffer(b,file );
+       xbt_automaton_parser__init_buffer(b,file );
 
        return b;
 }
 
 /** Destroy the buffer.
- * @param b a buffer created with xbt_automaton_parse__create_buffer()
+ * @param b a buffer created with xbt_automaton_parser__create_buffer()
  * 
  */
-    void xbt_automaton_parse__delete_buffer (YY_BUFFER_STATE  b )
+    void xbt_automaton_parser__delete_buffer (YY_BUFFER_STATE  b )
 {
     
        if ( ! b )
@@ -1486,9 +1486,9 @@ static void xbt_automaton_parse__load_buffer_state  (void)
                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_parser_free((void *) b->yy_ch_buf  );
 
-       xbt_automaton_parse_free((void *) b  );
+       xbt_automaton_parser_free((void *) b  );
 }
 
 #ifndef __cplusplus
@@ -1497,20 +1497,20 @@ extern int isatty (int );
     
 /* 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.
+ * such as during a xbt_automaton_parser_restart() or at EOF.
  */
-    static void xbt_automaton_parse__init_buffer  (YY_BUFFER_STATE  b, FILE * file )
+    static void xbt_automaton_parser__init_buffer  (YY_BUFFER_STATE  b, FILE * file )
 
 {
        int oerrno = errno;
     
-       xbt_automaton_parse__flush_buffer(b );
+       xbt_automaton_parser__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.
+    /* If b is the current buffer, then xbt_automaton_parser__init_buffer was _probably_
+     * called from xbt_automaton_parser_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){
@@ -1527,7 +1527,7 @@ extern int isatty (int );
  * @param b the buffer state to be flushed, usually @c YY_CURRENT_BUFFER.
  * 
  */
-    void xbt_automaton_parse__flush_buffer (YY_BUFFER_STATE  b )
+    void xbt_automaton_parser__flush_buffer (YY_BUFFER_STATE  b )
 {
        if ( ! b )
                return;
@@ -1547,7 +1547,7 @@ extern int isatty (int );
        b->yy_buffer_status = YY_BUFFER_NEW;
 
        if ( b == YY_CURRENT_BUFFER )
-               xbt_automaton_parse__load_buffer_state( );
+               xbt_automaton_parser__load_buffer_state( );
 }
 
 /** Pushes the new state onto the stack. The new state becomes
@@ -1556,14 +1556,14 @@ extern int isatty (int );
  *  @param new_buffer The new state.
  *  
  */
-void xbt_automaton_parse_push_buffer_state (YY_BUFFER_STATE new_buffer )
+void xbt_automaton_parser_push_buffer_state (YY_BUFFER_STATE new_buffer )
 {
        if (new_buffer == NULL)
                return;
 
-       xbt_automaton_parse_ensure_buffer_stack();
+       xbt_automaton_parser_ensure_buffer_stack();
 
-       /* This block is copied from xbt_automaton_parse__switch_to_buffer. */
+       /* This block is copied from xbt_automaton_parser__switch_to_buffer. */
        if ( YY_CURRENT_BUFFER )
                {
                /* Flush out information for old buffer. */
@@ -1577,8 +1577,8 @@ void xbt_automaton_parse_push_buffer_state (YY_BUFFER_STATE new_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( );
+       /* copied from xbt_automaton_parser__switch_to_buffer. */
+       xbt_automaton_parser__load_buffer_state( );
        (yy_did_buffer_switch_on_eof) = 1;
 }
 
@@ -1586,18 +1586,18 @@ void xbt_automaton_parse_push_buffer_state (YY_BUFFER_STATE new_buffer )
  *  The next element becomes the new top.
  *  
  */
-void xbt_automaton_parse_pop_buffer_state (void)
+void xbt_automaton_parser_pop_buffer_state (void)
 {
        if (!YY_CURRENT_BUFFER)
                return;
 
-       xbt_automaton_parse__delete_buffer(YY_CURRENT_BUFFER );
+       xbt_automaton_parser__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( );
+               xbt_automaton_parser__load_buffer_state( );
                (yy_did_buffer_switch_on_eof) = 1;
        }
 }
@@ -1605,7 +1605,7 @@ void xbt_automaton_parse_pop_buffer_state (void)
 /* Allocates the stack if it does not exist.
  *  Guarantees space for at least one push.
  */
-static void xbt_automaton_parse_ensure_buffer_stack (void)
+static void xbt_automaton_parser_ensure_buffer_stack (void)
 {
        int num_to_alloc;
     
@@ -1616,11 +1616,11 @@ static void xbt_automaton_parse_ensure_buffer_stack (void)
                 * immediate realloc on the next call.
          */
                num_to_alloc = 1;
-               (yy_buffer_stack) = (struct yy_buffer_state**)xbt_automaton_parse_alloc
+               (yy_buffer_stack) = (struct yy_buffer_state**)xbt_automaton_parser_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()" );
+                       YY_FATAL_ERROR( "out of dynamic memory in xbt_automaton_parser_ensure_buffer_stack()" );
                                                                  
                memset((yy_buffer_stack), 0, num_to_alloc * sizeof(struct yy_buffer_state*));
                                
@@ -1635,12 +1635,12 @@ static void xbt_automaton_parse_ensure_buffer_stack (void)
                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) = (struct yy_buffer_state**)xbt_automaton_parser_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()" );
+                       YY_FATAL_ERROR( "out of dynamic memory in xbt_automaton_parser_ensure_buffer_stack()" );
 
                /* zero only the new slots.*/
                memset((yy_buffer_stack) + (yy_buffer_stack_max), 0, grow_size * sizeof(struct yy_buffer_state*));
@@ -1654,7 +1654,7 @@ static void xbt_automaton_parse_ensure_buffer_stack (void)
  * 
  * @return the newly allocated buffer state object. 
  */
-YY_BUFFER_STATE xbt_automaton_parse__scan_buffer  (char * base, yy_size_t  size )
+YY_BUFFER_STATE xbt_automaton_parser__scan_buffer  (char * base, yy_size_t  size )
 {
        YY_BUFFER_STATE b;
     
@@ -1664,9 +1664,9 @@ YY_BUFFER_STATE xbt_automaton_parse__scan_buffer  (char * base, yy_size_t  size
                /* They forgot to leave room for the EOB's. */
                return 0;
 
-       b = (YY_BUFFER_STATE) xbt_automaton_parse_alloc(sizeof( struct yy_buffer_state )  );
+       b = (YY_BUFFER_STATE) xbt_automaton_parser_alloc(sizeof( struct yy_buffer_state )  );
        if ( ! b )
-               YY_FATAL_ERROR( "out of dynamic memory in xbt_automaton_parse__scan_buffer()" );
+               YY_FATAL_ERROR( "out of dynamic memory in xbt_automaton_parser__scan_buffer()" );
 
        b->yy_buf_size = size - 2;      /* "- 2" to take care of EOB's */
        b->yy_buf_pos = b->yy_ch_buf = base;
@@ -1678,33 +1678,33 @@ YY_BUFFER_STATE xbt_automaton_parse__scan_buffer  (char * base, yy_size_t  size
        b->yy_fill_buffer = 0;
        b->yy_buffer_status = YY_BUFFER_NEW;
 
-       xbt_automaton_parse__switch_to_buffer(b  );
+       xbt_automaton_parser__switch_to_buffer(b  );
 
        return b;
 }
 
-/** Setup the input buffer state to scan a string. The next call to xbt_automaton_parse_lex() will
+/** Setup the input buffer state to scan a string. The next call to xbt_automaton_parser_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.
+ *       xbt_automaton_parser__scan_bytes() instead.
  */
-YY_BUFFER_STATE xbt_automaton_parse__scan_string (yyconst char * yystr )
+YY_BUFFER_STATE xbt_automaton_parser__scan_string (yyconst char * yystr )
 {
     
-       return xbt_automaton_parse__scan_bytes(yystr,strlen(yystr) );
+       return xbt_automaton_parser__scan_bytes(yystr,strlen(yystr) );
 }
 
-/** Setup the input buffer state to scan the given bytes. The next call to xbt_automaton_parse_lex() will
+/** Setup the input buffer state to scan the given bytes. The next call to xbt_automaton_parser_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 xbt_automaton_parser__scan_bytes  (yyconst char * yybytes, int  _yybytes_len )
 {
        YY_BUFFER_STATE b;
        char *buf;
@@ -1713,18 +1713,18 @@ YY_BUFFER_STATE xbt_automaton_parse__scan_bytes  (yyconst char * yybytes, int  _
     
        /* Get memory for full buffer, including space for trailing EOB's. */
        n = _yybytes_len + 2;
-       buf = (char *) xbt_automaton_parse_alloc(n  );
+       buf = (char *) xbt_automaton_parser_alloc(n  );
        if ( ! buf )
-               YY_FATAL_ERROR( "out of dynamic memory in xbt_automaton_parse__scan_bytes()" );
+               YY_FATAL_ERROR( "out of dynamic memory in xbt_automaton_parser__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 );
+       b = xbt_automaton_parser__scan_buffer(buf,n );
        if ( ! b )
-               YY_FATAL_ERROR( "bad buffer in xbt_automaton_parse__scan_bytes()" );
+               YY_FATAL_ERROR( "bad buffer in xbt_automaton_parser__scan_bytes()" );
 
        /* It's okay to grow etc. this buffer, and we should throw it
         * away when we're done.
@@ -1750,14 +1750,14 @@ static void yy_fatal_error (yyconst char* msg )
 #define yyless(n) \
        do \
                { \
-               /* Undo effects of setting up xbt_automaton_parse_text. */ \
+               /* Undo effects of setting up xbt_automaton_parser_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; \
+               xbt_automaton_parser_text[xbt_automaton_parser_leng] = (yy_hold_char); \
+               (yy_c_buf_p) = xbt_automaton_parser_text + yyless_macro_arg; \
                (yy_hold_char) = *(yy_c_buf_p); \
                *(yy_c_buf_p) = '\0'; \
-               xbt_automaton_parse_leng = yyless_macro_arg; \
+               xbt_automaton_parser_leng = yyless_macro_arg; \
                } \
        while ( 0 )
 
@@ -1766,85 +1766,85 @@ static void yy_fatal_error (yyconst char* msg )
 /** Get the current line number.
  * 
  */
-int xbt_automaton_parse_get_lineno  (void)
+int xbt_automaton_parser_get_lineno  (void)
 {
         
-    return xbt_automaton_parse_lineno;
+    return xbt_automaton_parser_lineno;
 }
 
 /** Get the input stream.
  * 
  */
-FILE *xbt_automaton_parse_get_in  (void)
+FILE *xbt_automaton_parser_get_in  (void)
 {
-        return xbt_automaton_parse_in;
+        return xbt_automaton_parser_in;
 }
 
 /** Get the output stream.
  * 
  */
-FILE *xbt_automaton_parse_get_out  (void)
+FILE *xbt_automaton_parser_get_out  (void)
 {
-        return xbt_automaton_parse_out;
+        return xbt_automaton_parser_out;
 }
 
 /** Get the length of the current token.
  * 
  */
-int xbt_automaton_parse_get_leng  (void)
+int xbt_automaton_parser_get_leng  (void)
 {
-        return xbt_automaton_parse_leng;
+        return xbt_automaton_parser_leng;
 }
 
 /** Get the current token.
  * 
  */
 
-char *xbt_automaton_parse_get_text  (void)
+char *xbt_automaton_parser_get_text  (void)
 {
-        return xbt_automaton_parse_text;
+        return xbt_automaton_parser_text;
 }
 
 /** Set the current line number.
  * @param line_number
  * 
  */
-void xbt_automaton_parse_set_lineno (int  line_number )
+void xbt_automaton_parser_set_lineno (int  line_number )
 {
     
-    xbt_automaton_parse_lineno = line_number;
+    xbt_automaton_parser_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
+ * @see xbt_automaton_parser__switch_to_buffer
  */
-void xbt_automaton_parse_set_in (FILE *  in_str )
+void xbt_automaton_parser_set_in (FILE *  in_str )
 {
-        xbt_automaton_parse_in = in_str ;
+        xbt_automaton_parser_in = in_str ;
 }
 
-void xbt_automaton_parse_set_out (FILE *  out_str )
+void xbt_automaton_parser_set_out (FILE *  out_str )
 {
-        xbt_automaton_parse_out = out_str ;
+        xbt_automaton_parser_out = out_str ;
 }
 
-int xbt_automaton_parse_get_debug  (void)
+int xbt_automaton_parser_get_debug  (void)
 {
-        return xbt_automaton_parse__flex_debug;
+        return xbt_automaton_parser__flex_debug;
 }
 
-void xbt_automaton_parse_set_debug (int  bdebug )
+void xbt_automaton_parser_set_debug (int  bdebug )
 {
-        xbt_automaton_parse__flex_debug = bdebug ;
+        xbt_automaton_parser__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.
+     * This function is called from xbt_automaton_parser_lex_destroy(), so don't allocate here.
      */
 
     (yy_buffer_stack) = 0;
@@ -1856,36 +1856,36 @@ static int yy_init_globals (void)
 
 /* Defined in main.c */
 #ifdef YY_STDINIT
-    xbt_automaton_parse_in = stdin;
-    xbt_automaton_parse_out = stdout;
+    xbt_automaton_parser_in = stdin;
+    xbt_automaton_parser_out = stdout;
 #else
-    xbt_automaton_parse_in = (FILE *) 0;
-    xbt_automaton_parse_out = (FILE *) 0;
+    xbt_automaton_parser_in = (FILE *) 0;
+    xbt_automaton_parser_out = (FILE *) 0;
 #endif
 
     /* For future reference: Set errno on error, since we are called by
-     * xbt_automaton_parse_lex_init()
+     * xbt_automaton_parser_lex_init()
      */
     return 0;
 }
 
-/* xbt_automaton_parse_lex_destroy is for both reentrant and non-reentrant scanners. */
-int xbt_automaton_parse_lex_destroy  (void)
+/* xbt_automaton_parser_lex_destroy is for both reentrant and non-reentrant scanners. */
+int xbt_automaton_parser_lex_destroy  (void)
 {
     
     /* Pop the buffer stack, destroying each element. */
        while(YY_CURRENT_BUFFER){
-               xbt_automaton_parse__delete_buffer(YY_CURRENT_BUFFER  );
+               xbt_automaton_parser__delete_buffer(YY_CURRENT_BUFFER  );
                YY_CURRENT_BUFFER_LVALUE = NULL;
-               xbt_automaton_parse_pop_buffer_state();
+               xbt_automaton_parser_pop_buffer_state();
        }
 
        /* Destroy the stack itself. */
-       xbt_automaton_parse_free((yy_buffer_stack) );
+       xbt_automaton_parser_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. */
+     * xbt_automaton_parser_lex() is called, initialization will occur. */
     yy_init_globals( );
 
     return 0;
@@ -1915,12 +1915,12 @@ static int yy_flex_strlen (yyconst char * s )
 }
 #endif
 
-void *xbt_automaton_parse_alloc (yy_size_t  size )
+void *xbt_automaton_parser_alloc (yy_size_t  size )
 {
        return (void *) malloc( size );
 }
 
-void *xbt_automaton_parse_realloc  (void * ptr, yy_size_t  size )
+void *xbt_automaton_parser_realloc  (void * ptr, yy_size_t  size )
 {
        /* The cast to (char *) in the following accommodates both
         * implementations that use char* generic pointers, and those
@@ -1932,9 +1932,9 @@ void *xbt_automaton_parse_realloc  (void * ptr, yy_size_t  size )
        return (void *) realloc( (char *) ptr, size );
 }
 
-void xbt_automaton_parse_free (void * ptr )
+void xbt_automaton_parser_free (void * ptr )
 {
-       free( (char *) ptr );   /* see xbt_automaton_parse_realloc() for (char *) cast */
+       free( (char *) ptr );   /* see xbt_automaton_parser_realloc() for (char *) cast */
 }
 
 #define YYTABLES_NAME "yytables"
index beb79a6..9736dd1 100644 (file)
@@ -5,16 +5,12 @@
 /* This program is free software; you can redistribute it and/or modify it
  * under the terms of the license (GNU LGPL) which comes with this package. */
 
-#include "xbt/automatonparse_promela.h"
+#include "xbt/automaton.h"
 
-xbt_automaton_t automaton;
+static xbt_automaton_t parsed_automaton;
 char* state_id_src;
 
-void init(){
-  automaton = xbt_automaton_new_automaton();
-}
-
-void new_state(char* id, int src){
+static void new_state(char* id, int src){
 
   char* id_state = strdup(id);
   char* first_part = strtok(id,"_");
@@ -30,33 +26,33 @@ void new_state(char* id, int src){
   }
 
   xbt_state_t state = NULL;
-  state = xbt_automaton_state_exists(automaton, id_state);
+  state = xbt_automaton_state_exists(parsed_automaton, id_state);
   if(state == NULL){
-    state = xbt_automaton_new_state(automaton, type, id_state);
+    state = xbt_automaton_new_state(parsed_automaton, type, id_state);
   }
 
   if(type==-1)
-    automaton->current_state = state;
+    parsed_automaton->current_state = state;
 
   if(src)
     state_id_src = strdup(id_state);
     
 }
 
-void new_transition(char* id, xbt_exp_label_t label){
+static 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); 
+  state_dst = xbt_automaton_state_exists(parsed_automaton, id_state);
+  xbt_state_t state_src = xbt_automaton_state_exists(parsed_automaton, state_id_src);
   
   //xbt_transition_t trans = NULL;
-  xbt_automaton_new_transition(automaton, state_src, state_dst, label);
+  xbt_automaton_new_transition(parsed_automaton, state_src, state_dst, label);
 
 }
 
-xbt_exp_label_t new_label(int type, ...){
+static xbt_exp_label_t new_label(int type, ...){
   xbt_exp_label_t label = NULL;
   va_list ap;
   va_start(ap,type);
@@ -92,9 +88,11 @@ xbt_exp_label_t new_label(int type, ...){
   return label;
 }
 
-xbt_automaton_t get_automaton(){
-  return automaton;
-}
-
 
+#include "parserPromela.tab.cacc"
 
+void xbt_automaton_load(xbt_automaton_t a, const char *file){
+  parsed_automaton = a;
+  yyin = fopen(file, "r");
+  yyparse();
+}
index f4c9132..921940f 100644 (file)
@@ -4,7 +4,7 @@
 
 
 #include <stdio.h>
-#include "y.tab.h"
+#include "parserPromela.tab.hacc"
   
   extern YYSTYPE yylval;
  
similarity index 98%
rename from src/xbt/automaton/y.tab.c
rename to src/xbt/automaton/parserPromela.tab.cacc
index c8811de..b09c634 100644 (file)
 /* Using locations.  */
 #define YYLSP_NEEDED 0
 
+/* Substitute the variable and function names.  */
+#define yyparse         xbt_automaton_parser_parse
+#define yylex           xbt_automaton_parser_lex
+#define yyerror         xbt_automaton_parser_error
+#define yylval          xbt_automaton_parser_lval
+#define yychar          xbt_automaton_parser_char
+#define yydebug         xbt_automaton_parser_debug
+#define yynerrs         xbt_automaton_parser_nerrs
 
 
 /* Copy the first part of user declarations.  */
 #line 1 "parserPromela.yacc"
 
 
-#include "automaton_parse.yy.c"
+#include "automaton_lexer.yy.c"
 #include <xbt/automaton.h>
-#include <xbt/automatonparse_promela.h>
 
 void yyerror(const char *s);
 
 
 
 /* Line 268 of yacc.c  */
-#line 82 "y.tab.c"
+#line 89 "parserPromela.tab.cacc"
 
 /* Enabling traces.  */
 #ifndef YYDEBUG
@@ -127,28 +134,6 @@ void yyerror(const char *s);
      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
-
 
 
 
@@ -157,7 +142,7 @@ typedef union YYSTYPE
 {
 
 /* Line 293 of yacc.c  */
-#line 11 "parserPromela.yacc"
+#line 10 "parserPromela.yacc"
 
   double real;
   int integer;
@@ -167,7 +152,7 @@ typedef union YYSTYPE
 
 
 /* Line 293 of yacc.c  */
-#line 171 "y.tab.c"
+#line 156 "parserPromela.tab.cacc"
 } YYSTYPE;
 # define YYSTYPE_IS_TRIVIAL 1
 # define yystype YYSTYPE /* obsolescent; will be withdrawn */
@@ -179,7 +164,7 @@ typedef union YYSTYPE
 
 
 /* Line 343 of yacc.c  */
-#line 183 "y.tab.c"
+#line 168 "parserPromela.tab.cacc"
 
 #ifdef short
 # undef short
@@ -471,8 +456,8 @@ static const yytype_int8 yyrhs[] =
 /* 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
+       0,    47,    47,    50,    51,    51,    54,    55,    58,    59,
+      60,    61,    62,    63
 };
 #endif
 
@@ -1416,63 +1401,63 @@ yyreduce:
         case 4:
 
 /* Line 1806 of yacc.c  */
-#line 52 "parserPromela.yacc"
+#line 51 "parserPromela.yacc"
     { new_state((yyvsp[(1) - (2)].string), 1);}
     break;
 
   case 7:
 
 /* Line 1806 of yacc.c  */
-#line 56 "parserPromela.yacc"
+#line 55 "parserPromela.yacc"
     { new_transition((yyvsp[(5) - (6)].string), (yyvsp[(2) - (6)].label));}
     break;
 
   case 8:
 
 /* Line 1806 of yacc.c  */
-#line 59 "parserPromela.yacc"
+#line 58 "parserPromela.yacc"
     { (yyval.label) = (yyvsp[(2) - (3)].label); }
     break;
 
   case 9:
 
 /* Line 1806 of yacc.c  */
-#line 60 "parserPromela.yacc"
+#line 59 "parserPromela.yacc"
     { (yyval.label) = new_label(0, (yyvsp[(1) - (3)].label), (yyvsp[(3) - (3)].label)); }
     break;
 
   case 10:
 
 /* Line 1806 of yacc.c  */
-#line 61 "parserPromela.yacc"
+#line 60 "parserPromela.yacc"
     { (yyval.label) = new_label(1, (yyvsp[(1) - (3)].label), (yyvsp[(3) - (3)].label)); }
     break;
 
   case 11:
 
 /* Line 1806 of yacc.c  */
-#line 62 "parserPromela.yacc"
+#line 61 "parserPromela.yacc"
     { (yyval.label) = new_label(2, (yyvsp[(2) - (2)].label)); }
     break;
 
   case 12:
 
 /* Line 1806 of yacc.c  */
-#line 63 "parserPromela.yacc"
+#line 62 "parserPromela.yacc"
     { (yyval.label) = new_label(4); }
     break;
 
   case 13:
 
 /* Line 1806 of yacc.c  */
-#line 64 "parserPromela.yacc"
+#line 63 "parserPromela.yacc"
     { (yyval.label) = new_label(3, (yyvsp[(1) - (1)].string)); }
     break;
 
 
 
 /* Line 1806 of yacc.c  */
-#line 1476 "y.tab.c"
+#line 1461 "parserPromela.tab.cacc"
       default: break;
     }
   /* User semantic actions sometimes alter yychar, and that requires
@@ -1703,7 +1688,7 @@ yyreturn:
 
 
 /* Line 2067 of yacc.c  */
-#line 67 "parserPromela.yacc"
+#line 66 "parserPromela.yacc"
 
 
 
similarity index 83%
rename from src/xbt/automaton/y.tab.h
rename to src/xbt/automaton/parserPromela.tab.hacc
index fdf2faf..51a4ae6 100644 (file)
      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
-
 
 
 
@@ -89,7 +67,7 @@ typedef union YYSTYPE
 {
 
 /* Line 2068 of yacc.c  */
-#line 11 "parserPromela.yacc"
+#line 10 "parserPromela.yacc"
 
   double real;
   int integer;
@@ -99,13 +77,13 @@ typedef union YYSTYPE
 
 
 /* Line 2068 of yacc.c  */
-#line 103 "y.tab.h"
+#line 81 "parserPromela.tab.hacc"
 } YYSTYPE;
 # define YYSTYPE_IS_TRIVIAL 1
 # define yystype YYSTYPE /* obsolescent; will be withdrawn */
 # define YYSTYPE_IS_DECLARED 1
 #endif
 
-extern YYSTYPE yylval;
+extern YYSTYPE xbt_automaton_parser_lval;
 
 
index 6c6ae1f..f88ac53 100644 (file)
@@ -1,8 +1,7 @@
 %{
 
-#include "automaton_parse.yy.c"
+#include "automaton_lexer.yy.c"
 #include <xbt/automaton.h>
-#include <xbt/automatonparse_promela.h>
 
 void yyerror(const char *s);