From: Martin Quinson Date: Thu, 21 Jun 2012 13:26:06 +0000 (+0200) Subject: Various cleanups to the model-checking user interface X-Git-Tag: v3_8~522 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/984b8e1616cfd626c6244a34ccd42ee0b1e89bcd Various cleanups to the model-checking user interface - 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 --- diff --git a/buildtools/Cmake/DefinePackages.cmake b/buildtools/Cmake/DefinePackages.cmake index 592ddb853d..ace4e254bc 100644 --- a/buildtools/Cmake/DefinePackages.cmake +++ b/buildtools/Cmake/DefinePackages.cmake @@ -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 diff --git a/buildtools/Cmake/MaintainerMode.cmake b/buildtools/Cmake/MaintainerMode.cmake index c1e45d4d90..64e6aa367a 100644 --- a/buildtools/Cmake/MaintainerMode.cmake +++ b/buildtools/Cmake/MaintainerMode.cmake @@ -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) diff --git a/buildtools/Cmake/MakeLib.cmake b/buildtools/Cmake/MakeLib.cmake index 6d373a1c5b..52d66f376c 100644 --- a/buildtools/Cmake/MakeLib.cmake +++ b/buildtools/Cmake/MakeLib.cmake @@ -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 diff --git a/examples/msg/mc/bugged1_for_liveness.c b/examples/msg/mc/bugged1_for_liveness.c index 784e667a5d..b1f2112af6 100644 --- a/examples/msg/mc/bugged1_for_liveness.c +++ b/examples/msg/mc/bugged1_for_liveness.c @@ -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; } diff --git a/examples/msg/mc/bugged1_while_liveness.c b/examples/msg/mc/bugged1_while_liveness.c index 8d2bdb24ac..b8da0a149a 100644 --- a/examples/msg/mc/bugged1_while_liveness.c +++ b/examples/msg/mc/bugged1_while_liveness.c @@ -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; } diff --git a/examples/msg/mc/bugged2_liveness.c b/examples/msg/mc/bugged2_liveness.c index 25a35ca482..3209cff42b 100644 --- a/examples/msg/mc/bugged2_liveness.c +++ b/examples/msg/mc/bugged2_liveness.c @@ -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; diff --git a/examples/msg/mc/centralized_liveness.c b/examples/msg/mc/centralized_liveness.c index c78c2673cf..b031038971 100644 --- a/examples/msg/mc/centralized_liveness.c +++ b/examples/msg/mc/centralized_liveness.c @@ -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; diff --git a/examples/msg/mc/centralized_liveness_deadlock.c b/examples/msg/mc/centralized_liveness_deadlock.c index 3c02d517a2..6d1e175fcf 100644 --- a/examples/msg/mc/centralized_liveness_deadlock.c +++ b/examples/msg/mc/centralized_liveness_deadlock.c @@ -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; diff --git a/examples/msg/mc/test_snapshot.c b/examples/msg/mc/test_snapshot.c index 77260db0bc..59c7fc6495 100644 --- a/examples/msg/mc/test_snapshot.c +++ b/examples/msg/mc/test_snapshot.c @@ -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 @@ -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; } diff --git a/include/msg/msg.h b/include/msg/msg.h index 4a37ef4db5..da0fca17c2 100644 --- a/include/msg/msg.h +++ b/include/msg/msg.h @@ -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); diff --git a/include/simgrid/modelchecker.h b/include/simgrid/modelchecker.h index 2752cbd1ff..da83b88a29 100644 --- a/include/simgrid/modelchecker.h +++ b/include/simgrid/modelchecker.h @@ -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 diff --git a/include/xbt/automaton.h b/include/xbt/automaton.h index f140ed2e82..49df4630c0 100644 --- a/include/xbt/automaton.h +++ b/include/xbt/automaton.h @@ -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 index d461474458..0000000000 --- a/include/xbt/automatonparse_promela.h +++ /dev/null @@ -1,26 +0,0 @@ -#ifndef _XBT_AUTOMATONPARSE_PROMELA_H -#define _XBT_AUTOMATONPARSE_PROMELA_H - -#include -#include -#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 diff --git a/src/include/mc/mc.h b/src/include/mc/mc.h index cf0bab680a..52c568de92 100644 --- a/src/include/mc/mc.h +++ b/src/include/mc/mc.h @@ -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); diff --git a/src/mc/mc_global.c b/src/mc/mc_global.c index 211f26bbd1..f62e2f7230 100644 --- a/src/mc/mc_global.c +++ b/src/mc/mc_global.c @@ -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; } diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c index a49dbfbedc..08a6d5429c 100644 --- a/src/mc/mc_liveness.c +++ b/src/mc/mc_liveness.c @@ -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); diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h index 9a0ee71e1f..77d842da75 100644 --- a/src/mc/mc_private.h +++ b/src/mc/mc_private.h @@ -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; diff --git a/src/msg/msg_global.c b/src/msg/msg_global.c index 879461fd2e..681bdef8b9 100644 --- a/src/msg/msg_global.c +++ b/src/msg/msg_global.c @@ -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(); diff --git a/src/xbt/automaton/automaton.c b/src/xbt/automaton/automaton.c index dffad324b2..97c397cfc1 100644 --- a/src/xbt/automaton/automaton.c +++ b/src/xbt/automaton/automaton.c @@ -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 index 0b2ed306c9..0000000000 --- a/src/xbt/automaton/automaton_create.c +++ /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 index 24d0ebeedc..0000000000 --- a/src/xbt/automaton/automaton_create.h +++ /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 diff --git a/src/xbt/automaton/automaton_parse.yy.c b/src/xbt/automaton/automaton_lexer.yy.c similarity index 75% rename from src/xbt/automaton/automaton_parse.yy.c rename to src/xbt/automaton/automaton_lexer.yy.c index a7395b169d..5a5d379b14 100644 --- a/src/xbt/automaton/automaton_parse.yy.c +++ b/src/xbt/automaton/automaton_lexer.yy.c @@ -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 -#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" diff --git a/src/xbt/automaton/automatonparse_promela.c b/src/xbt/automaton/automatonparse_promela.c index beb79a685f..9736dd122e 100644 --- a/src/xbt/automaton/automatonparse_promela.c +++ b/src/xbt/automaton/automatonparse_promela.c @@ -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(); +} diff --git a/src/xbt/automaton/parserPromela.lex b/src/xbt/automaton/parserPromela.lex index f4c913280e..921940f07d 100644 --- a/src/xbt/automaton/parserPromela.lex +++ b/src/xbt/automaton/parserPromela.lex @@ -4,7 +4,7 @@ #include -#include "y.tab.h" +#include "parserPromela.tab.hacc" extern YYSTYPE yylval; diff --git a/src/xbt/automaton/y.tab.c b/src/xbt/automaton/parserPromela.tab.cacc similarity index 98% rename from src/xbt/automaton/y.tab.c rename to src/xbt/automaton/parserPromela.tab.cacc index c8811dea94..b09c6349a0 100644 --- a/src/xbt/automaton/y.tab.c +++ b/src/xbt/automaton/parserPromela.tab.cacc @@ -61,6 +61,14 @@ /* 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. */ @@ -69,16 +77,15 @@ #line 1 "parserPromela.yacc" -#include "automaton_parse.yy.c" +#include "automaton_lexer.yy.c" #include -#include 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" diff --git a/src/xbt/automaton/y.tab.h b/src/xbt/automaton/parserPromela.tab.hacc similarity index 83% rename from src/xbt/automaton/y.tab.h rename to src/xbt/automaton/parserPromela.tab.hacc index fdf2faffa2..51a4ae6cfb 100644 --- a/src/xbt/automaton/y.tab.h +++ b/src/xbt/automaton/parserPromela.tab.hacc @@ -59,28 +59,6 @@ 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; diff --git a/src/xbt/automaton/parserPromela.yacc b/src/xbt/automaton/parserPromela.yacc index 6c6ae1f18f..f88ac53087 100644 --- a/src/xbt/automaton/parserPromela.yacc +++ b/src/xbt/automaton/parserPromela.yacc @@ -1,8 +1,7 @@ %{ -#include "automaton_parse.yy.c" +#include "automaton_lexer.yy.c" #include -#include void yyerror(const char *s);