add a tesh for bugged2-liveness

Do not test it because it never ends, but at least now if one wants to
do something clever with this test, one can ;)

diff --git a/MANIFEST.in b/MANIFEST.in
index 080654d..2d70929 100644 (file)
--- a/MANIFEST.in
+++ b/MANIFEST.in
@@ -256,6 +256,7 @@ include examples/deprecated/java/trace/pingpong/Sender.java
 include examples/deprecated/java/trace/pingpong/trace-pingpong.tesh
 include examples/deprecated/msg/README.doc
 include examples/deprecated/msg/mc/bugged2_liveness.c
 include examples/deprecated/java/trace/pingpong/trace-pingpong.tesh
 include examples/deprecated/msg/README.doc
 include examples/deprecated/msg/mc/bugged2_liveness.c

+include examples/deprecated/msg/mc/bugged2_liveness.tesh

 include examples/deprecated/msg/mc/centralized_mutex.c
 include examples/deprecated/msg/mc/centralized_mutex.tesh
 include examples/deprecated/msg/mc/deploy_bugged2_liveness.xml
 include examples/deprecated/msg/mc/centralized_mutex.c
 include examples/deprecated/msg/mc/centralized_mutex.tesh
 include examples/deprecated/msg/mc/deploy_bugged2_liveness.xml

diff --git a/examples/deprecated/msg/mc/CMakeLists.txt b/examples/deprecated/msg/mc/CMakeLists.txt
index fc6e6d3..cdcfa63 100644 (file)
--- a/examples/deprecated/msg/mc/CMakeLists.txt
+++ b/examples/deprecated/msg/mc/CMakeLists.txt
@@ -8,8 +8,17 @@ foreach (x centralized_mutex bugged2_liveness)
   set(xml_files     ${xml_files}    ${CMAKE_CURRENT_SOURCE_DIR}/deploy_${x}.xml)
 endforeach()
 
   set(xml_files     ${xml_files}    ${CMAKE_CURRENT_SOURCE_DIR}/deploy_${x}.xml)
 endforeach()
 

-set(tesh_files   ${tesh_files}    ${CMAKE_CURRENT_SOURCE_DIR}/centralized_mutex.tesh                PARENT_SCOPE)
+set(tesh_files   ${tesh_files}    ${CMAKE_CURRENT_SOURCE_DIR}/bugged2_liveness.tesh
+                                  ${CMAKE_CURRENT_SOURCE_DIR}/centralized_mutex.tesh                PARENT_SCOPE)

 set(xml_files    ${xml_files}                                                                       PARENT_SCOPE)
 set(examples_src ${examples_src}                                                                    PARENT_SCOPE)
 set(bin_files    ${bin_files}     ${CMAKE_CURRENT_SOURCE_DIR}/promela_bugged2_liveness              PARENT_SCOPE)
 set(xml_files    ${xml_files}                                                                       PARENT_SCOPE)
 set(examples_src ${examples_src}                                                                    PARENT_SCOPE)
 set(bin_files    ${bin_files}     ${CMAKE_CURRENT_SOURCE_DIR}/promela_bugged2_liveness              PARENT_SCOPE)

- 
\ No newline at end of file
+
+#if(SIMGRID_HAVE_MC)
+#  IF(HAVE_UCONTEXT_CONTEXTS AND SIMGRID_PROCESSOR_x86_64) # liveness model-checking works only on 64bits (for now ...)
+#    ADD_TESH(mc-bugged2-liveness-ucontext     --setenv bindir=${CMAKE_CURRENT_BINARY_DIR}
+#                                              --setenv platfdir=${CMAKE_HOME_DIRECTORY}/examples/platforms 
+#                                              --cd ${CMAKE_HOME_DIRECTORY}/examples/deprecated/msg/mc
+#                                              bugged2-liveness.tesh)
+#  ENDIF()
+#ENDIF()
\ No newline at end of file

diff --git a/examples/deprecated/msg/mc/bugged2-liveness.tesh b/examples/deprecated/msg/mc/bugged2-liveness.tesh
new file mode 100644 (file)
index 0000000..16d8b15
--- /dev/null
+++ b/examples/deprecated/msg/mc/bugged2-liveness.tesh
@@ -0,0 +1,6 @@
+#!/usr/bin/env tesh
+
+! expect return 2
+! timeout 20
+! output ignore
+$ ${bindir:=.}/../../../../bin/simgrid-mc ${bindir:=.}/bugged2_liveness ${platfdir:=.}/small_platform.xml ${srcdir:=.}/deploy_bugged2_liveness.xml --log=xbt_cfg.thresh:warning "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --cfg=contexts/factory:ucontext --cfg=contexts/stack-size:256 --cfg=model-check/property:promela_bugged2_liveness

diff --git a/examples/deprecated/msg/mc/bugged2_liveness.c b/examples/deprecated/msg/mc/bugged2_liveness.c
index 2926b46..80fa412 100644 (file)
--- a/examples/deprecated/msg/mc/bugged2_liveness.c
+++ b/examples/deprecated/msg/mc/bugged2_liveness.c
@@ -84,10 +84,10 @@ int main(int argc, char *argv[])
 
   MC_automaton_new_propositional_symbol_pointer("cs", &cs);
 
 
   MC_automaton_new_propositional_symbol_pointer("cs", &cs);
 

-  MSG_create_environment("../msg_platform.xml");
+  MSG_create_environment(argv[1]);

   MSG_function_register("coordinator", coordinator);
   MSG_function_register("client", client);
   MSG_function_register("coordinator", coordinator);
   MSG_function_register("client", client);

-  MSG_launch_application("deploy_bugged2_liveness.xml");
+  MSG_launch_application(argv[2]);

   MSG_main();
 
   return 0;
   MSG_main();
 
   return 0;