Clean sources for mc and reedit some files

diff --git a/buildtools/Cmake/DefinePackages.cmake b/buildtools/Cmake/DefinePackages.cmake
index bf142df..7fee383 100644 (file)
--- a/buildtools/Cmake/DefinePackages.cmake
+++ b/buildtools/Cmake/DefinePackages.cmake
@@ -31,6 +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/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/surf/maxmin_private.h
        src/surf/trace_mgr_private.h
        src/surf/surf_private.h
        src/surf/maxmin_private.h
        src/surf/trace_mgr_private.h
        src/surf/surf_private.h


@@ -84,7 +87,6 @@ set(EXTRA_DIST
        src/smpi/README
        src/mk_supernovae.pl
        
        src/smpi/README
        src/mk_supernovae.pl
        

-

        tools/gras/gras_stub_generator.h
        tools/tesh/run_context.h  
        tools/tesh/tesh.h
        tools/gras/gras_stub_generator.h
        tools/tesh/run_context.h  
        tools/tesh/tesh.h


@@ -169,7 +171,6 @@ set(XBT_SRC
        src/xbt/parmap.c
        src/xbt/xbt_replay.c
        src/xbt/lib.c
        src/xbt/parmap.c
        src/xbt/xbt_replay.c
        src/xbt/lib.c

-       src/xbt/automaton/automaton.c

        src/xbt/automaton/automatonparse_promela.c
        src/xbt/automaton/automaton.c
        src/xbt/automaton/automaton_create.c
        src/xbt/automaton/automatonparse_promela.c
        src/xbt/automaton/automaton.c
        src/xbt/automaton/automaton_create.c


@@ -872,6 +873,9 @@ examples/platforms/syscoord/median_p2psim.xml
 
 set(generated_src_files
 src/xbt/datadesc/ddt_parse.yy.c
 
 set(generated_src_files
 src/xbt/datadesc/ddt_parse.yy.c

+src/xbt/automaton/y.tab.c
+src/xbt/automaton/y.tab.h
+src/xbt/automaton/automaton_parse.yy.c

 )
 
 foreach(file ${generated_src_files})
 )
 
 foreach(file ${generated_src_files})

diff --git a/examples/msg/mc/CMakeLists.txt b/examples/msg/mc/CMakeLists.txt
index 2b05f76..adb5af4 100644 (file)
--- a/examples/msg/mc/CMakeLists.txt
+++ b/examples/msg/mc/CMakeLists.txt
@@ -7,15 +7,15 @@ add_executable(centralized centralized_mutex.c)
 add_executable(bugged1     bugged1.c)
 add_executable(bugged1_stateful bugged1_stateful.c)
 add_executable(bugged2_stateful bugged2_stateful.c)
 add_executable(bugged1     bugged1.c)
 add_executable(bugged1_stateful bugged1_stateful.c)
 add_executable(bugged2_stateful bugged2_stateful.c)

-add_executable(bugged2     bugged2.c)
+add_executable(bugged2      bugged2.c)

 add_executable(bugged3    bugged3.c)
 add_executable(random_test random_test.c)
 add_executable(bugged3    bugged3.c)
 add_executable(random_test random_test.c)

-add_executable(bugged1_for_liveness automaton.c automatonparse_promela.c bugged1_for_liveness.c)
-add_executable(bugged1_while_liveness automaton.c automatonparse_promela.c bugged1_while_liveness.c)
-add_executable(bugged2_liveness automaton.c automatonparse_promela.c bugged2_liveness.c)
-add_executable(centralized_liveness automaton.c automatonparse_promela.c centralized_liveness.c)
-add_executable(centralized_liveness_deadlock automaton.c automatonparse_promela.c centralized_liveness_deadlock.c)
-add_executable(test_snapshot automaton.c automatonparse_promela.c test_snapshot.c)
+add_executable(bugged1_for_liveness bugged1_for_liveness.c)
+add_executable(bugged1_while_liveness bugged1_while_liveness.c)
+add_executable(bugged2_liveness bugged2_liveness.c)
+add_executable(centralized_liveness centralized_liveness.c)
+add_executable(centralized_liveness_deadlock centralized_liveness_deadlock.c)
+add_executable(test_snapshot test_snapshot.c)

 
 target_link_libraries(centralized simgrid m )
 target_link_libraries(bugged1     simgrid m )
 
 target_link_libraries(centralized simgrid m )
 target_link_libraries(bugged1     simgrid m )


@@ -54,8 +54,6 @@ set(xml_files
 )
 set(examples_src
   ${examples_src}
 )
 set(examples_src
   ${examples_src}

-  ${CMAKE_CURRENT_SOURCE_DIR}/automaton.c
-  ${CMAKE_CURRENT_SOURCE_DIR}/automatonparse_promela.c

   ${CMAKE_CURRENT_SOURCE_DIR}/bugged1.c
   ${CMAKE_CURRENT_SOURCE_DIR}/bugged1_for_liveness.c
   ${CMAKE_CURRENT_SOURCE_DIR}/bugged1_stateful.c
   ${CMAKE_CURRENT_SOURCE_DIR}/bugged1.c
   ${CMAKE_CURRENT_SOURCE_DIR}/bugged1_for_liveness.c
   ${CMAKE_CURRENT_SOURCE_DIR}/bugged1_stateful.c


@@ -67,15 +65,12 @@ set(examples_src
   ${CMAKE_CURRENT_SOURCE_DIR}/centralized_liveness.c
   ${CMAKE_CURRENT_SOURCE_DIR}/centralized_liveness_deadlock.c
   ${CMAKE_CURRENT_SOURCE_DIR}/centralized_mutex.c
   ${CMAKE_CURRENT_SOURCE_DIR}/centralized_liveness.c
   ${CMAKE_CURRENT_SOURCE_DIR}/centralized_liveness_deadlock.c
   ${CMAKE_CURRENT_SOURCE_DIR}/centralized_mutex.c

-  ${CMAKE_CURRENT_SOURCE_DIR}/lex.yy.c

   ${CMAKE_CURRENT_SOURCE_DIR}/random_test.c
   ${CMAKE_CURRENT_SOURCE_DIR}/test_snapshot.c
   ${CMAKE_CURRENT_SOURCE_DIR}/random_test.c
   ${CMAKE_CURRENT_SOURCE_DIR}/test_snapshot.c

-  ${CMAKE_CURRENT_SOURCE_DIR}/y.tab.c

   ${CMAKE_CURRENT_SOURCE_DIR}/bugged1_liveness.h
   ${CMAKE_CURRENT_SOURCE_DIR}/bugged2_liveness.h
   ${CMAKE_CURRENT_SOURCE_DIR}/centralized_liveness.h
   ${CMAKE_CURRENT_SOURCE_DIR}/test_snapshot.h
   ${CMAKE_CURRENT_SOURCE_DIR}/bugged1_liveness.h
   ${CMAKE_CURRENT_SOURCE_DIR}/bugged2_liveness.h
   ${CMAKE_CURRENT_SOURCE_DIR}/centralized_liveness.h
   ${CMAKE_CURRENT_SOURCE_DIR}/test_snapshot.h

-  ${CMAKE_CURRENT_SOURCE_DIR}/y.tab.h

   PARENT_SCOPE
 )
 set(bin_files
   PARENT_SCOPE
 )
 set(bin_files

diff --git a/src/xbt/automaton/parserPromela.yacc b/src/xbt/automaton/parserPromela.yacc
index 36fd2c0..6c6ae1f 100644 (file)
--- a/src/xbt/automaton/parserPromela.yacc
+++ b/src/xbt/automaton/parserPromela.yacc
@@ -1,7 +1,5 @@
 %{
 
 %{
 

-  //#include "../../../include/xbt/automatonparse_promela.h"
-  //#include "../../../include/xbt/automaton.h"

 #include "automaton_parse.yy.c"
 #include <xbt/automaton.h>
 #include <xbt/automatonparse_promela.h>
 #include "automaton_parse.yy.c"
 #include <xbt/automaton.h>
 #include <xbt/automatonparse_promela.h>

diff --git a/src/xbt/automaton/y.tab.c b/src/xbt/automaton/y.tab.c
index f5b9049..c8811de 100644 (file)
--- a/src/xbt/automaton/y.tab.c
+++ b/src/xbt/automaton/y.tab.c
@@ -69,8 +69,6 @@
 #line 1 "parserPromela.yacc"
 
 
 #line 1 "parserPromela.yacc"
 
 

-  //#include "../../../include/xbt/automatonparse_promela.h"
-  //#include "../../../include/xbt/automaton.h"

 #include "automaton_parse.yy.c"
 #include <xbt/automaton.h>
 #include <xbt/automatonparse_promela.h>
 #include "automaton_parse.yy.c"
 #include <xbt/automaton.h>
 #include <xbt/automatonparse_promela.h>


@@ -80,7 +78,7 @@ void yyerror(const char *s);
 
 
 /* Line 268 of yacc.c  */
 
 
 /* Line 268 of yacc.c  */

-#line 84 "y.tab.c"
+#line 82 "y.tab.c"

 
 /* Enabling traces.  */
 #ifndef YYDEBUG
 
 /* Enabling traces.  */
 #ifndef YYDEBUG


@@ -159,7 +157,7 @@ typedef union YYSTYPE
 {
 
 /* Line 293 of yacc.c  */
 {
 
 /* Line 293 of yacc.c  */

-#line 13 "parserPromela.yacc"
+#line 11 "parserPromela.yacc"

 
   double real;
   int integer;
 
   double real;
   int integer;


@@ -169,7 +167,7 @@ typedef union YYSTYPE
 
 
 /* Line 293 of yacc.c  */
 
 
 /* Line 293 of yacc.c  */

-#line 173 "y.tab.c"
+#line 171 "y.tab.c"

 } YYSTYPE;
 # define YYSTYPE_IS_TRIVIAL 1
 # define yystype YYSTYPE /* obsolescent; will be withdrawn */
 } YYSTYPE;
 # define YYSTYPE_IS_TRIVIAL 1
 # define yystype YYSTYPE /* obsolescent; will be withdrawn */


@@ -181,7 +179,7 @@ typedef union YYSTYPE
 
 
 /* Line 343 of yacc.c  */
 
 
 /* Line 343 of yacc.c  */

-#line 185 "y.tab.c"
+#line 183 "y.tab.c"

 
 #ifdef short
 # undef short
 
 #ifdef short
 # undef short


@@ -473,8 +471,8 @@ static const yytype_int8 yyrhs[] =
 /* YYRLINE[YYN] -- source line where rule number YYN was defined.  */
 static const yytype_uint8 yyrline[] =
 {
 /* YYRLINE[YYN] -- source line where rule number YYN was defined.  */
 static const yytype_uint8 yyrline[] =
 {

-       0,    50,    50,    53,    54,    54,    57,    58,    61,    62,
-      63,    64,    65,    66
+       0,    48,    48,    51,    52,    52,    55,    56,    59,    60,
+      61,    62,    63,    64

 };
 #endif
 
 };
 #endif
 


@@ -1418,63 +1416,63 @@ yyreduce:
         case 4:
 
 /* Line 1806 of yacc.c  */
         case 4:
 
 /* Line 1806 of yacc.c  */

-#line 54 "parserPromela.yacc"
+#line 52 "parserPromela.yacc"

     { new_state((yyvsp[(1) - (2)].string), 1);}
     break;
 
   case 7:
 
 /* Line 1806 of yacc.c  */
     { new_state((yyvsp[(1) - (2)].string), 1);}
     break;
 
   case 7:
 
 /* Line 1806 of yacc.c  */

-#line 58 "parserPromela.yacc"
+#line 56 "parserPromela.yacc"

     { new_transition((yyvsp[(5) - (6)].string), (yyvsp[(2) - (6)].label));}
     break;
 
   case 8:
 
 /* Line 1806 of yacc.c  */
     { new_transition((yyvsp[(5) - (6)].string), (yyvsp[(2) - (6)].label));}
     break;
 
   case 8:
 
 /* Line 1806 of yacc.c  */

-#line 61 "parserPromela.yacc"
+#line 59 "parserPromela.yacc"

     { (yyval.label) = (yyvsp[(2) - (3)].label); }
     break;
 
   case 9:
 
 /* Line 1806 of yacc.c  */
     { (yyval.label) = (yyvsp[(2) - (3)].label); }
     break;
 
   case 9:
 
 /* Line 1806 of yacc.c  */

-#line 62 "parserPromela.yacc"
+#line 60 "parserPromela.yacc"

     { (yyval.label) = new_label(0, (yyvsp[(1) - (3)].label), (yyvsp[(3) - (3)].label)); }
     break;
 
   case 10:
 
 /* Line 1806 of yacc.c  */
     { (yyval.label) = new_label(0, (yyvsp[(1) - (3)].label), (yyvsp[(3) - (3)].label)); }
     break;
 
   case 10:
 
 /* Line 1806 of yacc.c  */

-#line 63 "parserPromela.yacc"
+#line 61 "parserPromela.yacc"

     { (yyval.label) = new_label(1, (yyvsp[(1) - (3)].label), (yyvsp[(3) - (3)].label)); }
     break;
 
   case 11:
 
 /* Line 1806 of yacc.c  */
     { (yyval.label) = new_label(1, (yyvsp[(1) - (3)].label), (yyvsp[(3) - (3)].label)); }
     break;
 
   case 11:
 
 /* Line 1806 of yacc.c  */

-#line 64 "parserPromela.yacc"
+#line 62 "parserPromela.yacc"

     { (yyval.label) = new_label(2, (yyvsp[(2) - (2)].label)); }
     break;
 
   case 12:
 
 /* Line 1806 of yacc.c  */
     { (yyval.label) = new_label(2, (yyvsp[(2) - (2)].label)); }
     break;
 
   case 12:
 
 /* Line 1806 of yacc.c  */

-#line 65 "parserPromela.yacc"
+#line 63 "parserPromela.yacc"

     { (yyval.label) = new_label(4); }
     break;
 
   case 13:
 
 /* Line 1806 of yacc.c  */
     { (yyval.label) = new_label(4); }
     break;
 
   case 13:
 
 /* Line 1806 of yacc.c  */

-#line 66 "parserPromela.yacc"
+#line 64 "parserPromela.yacc"

     { (yyval.label) = new_label(3, (yyvsp[(1) - (1)].string)); }
     break;
 
 
 
 /* Line 1806 of yacc.c  */
     { (yyval.label) = new_label(3, (yyvsp[(1) - (1)].string)); }
     break;
 
 
 
 /* Line 1806 of yacc.c  */

-#line 1478 "y.tab.c"
+#line 1476 "y.tab.c"

       default: break;
     }
   /* User semantic actions sometimes alter yychar, and that requires
       default: break;
     }
   /* User semantic actions sometimes alter yychar, and that requires


@@ -1705,7 +1703,7 @@ yyreturn:
 
 
 /* Line 2067 of yacc.c  */
 
 
 /* Line 2067 of yacc.c  */

-#line 69 "parserPromela.yacc"
+#line 67 "parserPromela.yacc"

 
 
 
 
 
 

diff --git a/src/xbt/automaton/y.tab.h b/src/xbt/automaton/y.tab.h
index ad611d5..fdf2faf 100644 (file)
--- a/src/xbt/automaton/y.tab.h
+++ b/src/xbt/automaton/y.tab.h
@@ -89,7 +89,7 @@ typedef union YYSTYPE
 {
 
 /* Line 2068 of yacc.c  */
 {
 
 /* Line 2068 of yacc.c  */

-#line 13 "parserPromela.yacc"
+#line 11 "parserPromela.yacc"

 
   double real;
   int integer;
 
   double real;
   int integer;