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
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
--- /dev/null
+#!/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
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;