From: Frederic Suter <frederic.suter@cc.in2p3.fr>
Date: Thu, 2 Apr 2020 10:19:08 +0000 (+0200)
Subject: add a tesh for bugged2-liveness
X-Git-Tag: v3.26~666
X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/08d235d6203bef6455f1b840159a52bbb2485536

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 080654d4e4..2d70929cd0 100644
--- 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/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
diff --git a/examples/deprecated/msg/mc/CMakeLists.txt b/examples/deprecated/msg/mc/CMakeLists.txt
index fc6e6d3988..cdcfa63041 100644
--- 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(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)
- 
\ 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
index 0000000000..16d8b151ab
--- /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 2926b46819..80fa412e36 100644
--- 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);
 
-  MSG_create_environment("../msg_platform.xml");
+  MSG_create_environment(argv[1]);
   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;