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/bugged1_liveness.c
-include examples/deprecated/msg/mc/bugged1_liveness.tesh
-include examples/deprecated/msg/mc/bugged1_liveness_stack_cleaner
-include examples/deprecated/msg/mc/bugged1_liveness_visited.tesh
include examples/deprecated/msg/mc/bugged2_liveness.c
include examples/deprecated/msg/mc/bugged3.c
include examples/deprecated/msg/mc/centralized_mutex.c
include examples/deprecated/msg/mc/centralized_mutex.tesh
-include examples/deprecated/msg/mc/deploy_bugged1_liveness.xml
-include examples/deprecated/msg/mc/deploy_bugged1_liveness_visited.xml
include examples/deprecated/msg/mc/deploy_bugged2_liveness.xml
include examples/deprecated/msg/mc/deploy_bugged3.xml
include examples/deprecated/msg/mc/deploy_centralized_mutex.xml
-include examples/deprecated/msg/mc/promela_bugged1_liveness
include examples/deprecated/msg/mc/promela_bugged2_liveness
include examples/deprecated/msg/trace-categories/trace-categories.c
include examples/deprecated/msg/trace-categories/trace-categories.tesh
include examples/s4u/io-file-system/s4u-io-file-system.tesh
include examples/s4u/maestro-set/s4u-maestro-set.cpp
include examples/s4u/maestro-set/s4u-maestro-set.tesh
+include examples/s4u/mc-bugged1-liveness/promela_bugged1_liveness
+include examples/s4u/mc-bugged1-liveness/s4u-mc-bugged1-liveness-stack-cleaner
+include examples/s4u/mc-bugged1-liveness/s4u-mc-bugged1-liveness-visited.tesh
+include examples/s4u/mc-bugged1-liveness/s4u-mc-bugged1-liveness.cpp
+include examples/s4u/mc-bugged1-liveness/s4u-mc-bugged1-liveness.tesh
include examples/s4u/mc-bugged1/s4u-mc-bugged1.cpp
include examples/s4u/mc-bugged1/s4u-mc-bugged1.tesh
include examples/s4u/mc-bugged2/s4u-mc-bugged2.cpp
-foreach (x bugged3 centralized_mutex bugged1_liveness bugged2_liveness)
+foreach (x bugged3 centralized_mutex bugged2_liveness)
if(SIMGRID_HAVE_MC AND SIMGRID_HAVE_MSG)
add_executable (${x} EXCLUDE_FROM_ALL ${x}.c)
target_link_libraries(${x} simgrid)
set(xml_files ${xml_files} ${CMAKE_CURRENT_SOURCE_DIR}/deploy_${x}.xml)
endforeach()
-if(SIMGRID_HAVE_MC AND SIMGRID_HAVE_MSG)
- if(HAVE_C_STACK_CLEANER)
- add_executable (bugged1_liveness_cleaner_on EXCLUDE_FROM_ALL bugged1_liveness.c)
- target_link_libraries(bugged1_liveness_cleaner_on simgrid)
- set_target_properties(bugged1_liveness_cleaner_on PROPERTIES COMPILE_FLAGS "-DGARBAGE_STACK -fstack-cleaner")
- add_dependencies(tests bugged1_liveness_cleaner_on)
-
- add_executable (bugged1_liveness_cleaner_off EXCLUDE_FROM_ALL bugged1_liveness.c)
- target_link_libraries(bugged1_liveness_cleaner_off simgrid)
- set_target_properties(bugged1_liveness_cleaner_off PROPERTIES COMPILE_FLAGS "-DGARBAGE_STACK -fno-stack-cleaner")
- add_dependencies(tests bugged1_liveness_cleaner_off)
- endif()
-
- IF(HAVE_UCONTEXT_CONTEXTS AND SIMGRID_PROCESSOR_x86_64) # liveness model-checking works only on 64bits (for now ...)
- ADD_TESH(mc-bugged1-liveness-ucontext --setenv bindir=${CMAKE_BINARY_DIR}/examples/deprecated/msg/mc
- --setenv platfdir=${CMAKE_HOME_DIRECTORY}/examples/platforms
- --cd ${CMAKE_HOME_DIRECTORY}/examples/deprecated/msg/mc bugged1_liveness.tesh)
- ADD_TESH(mc-bugged1-liveness-visited-ucontext --setenv bindir=${CMAKE_BINARY_DIR}/examples/deprecated/msg/mc
- --setenv platfdir=${CMAKE_HOME_DIRECTORY}/examples/platforms
- --cd ${CMAKE_HOME_DIRECTORY}/examples/deprecated/msg/mc bugged1_liveness_visited.tesh)
- IF(HAVE_C_STACK_CLEANER)
- # This test checks if the stack cleaner is making a difference:
- ADD_TEST(mc-bugged1-liveness-stack-cleaner ${CMAKE_HOME_DIRECTORY}/examples/deprecated/msg/mc/bugged1_liveness_stack_cleaner ${CMAKE_HOME_DIRECTORY}/examples/deprecated/msg/mc/ ${CMAKE_BINARY_DIR}/examples/deprecated/msg/mc/)
- ENDIF()
- ENDIF()
-
- if (enable_coverage)
- SET_TESTS_PROPERTIES(mc-bugged1-liveness-visited-ucontext PROPERTIES RUN_SERIAL "TRUE")
- endif()
-endif()
-
-set(tesh_files ${tesh_files} ${CMAKE_CURRENT_SOURCE_DIR}/bugged1_liveness.tesh
- ${CMAKE_CURRENT_SOURCE_DIR}/bugged1_liveness_visited.tesh
- ${CMAKE_CURRENT_SOURCE_DIR}/centralized_mutex.tesh PARENT_SCOPE)
-set(xml_files ${xml_files} ${CMAKE_CURRENT_SOURCE_DIR}/deploy_bugged1_liveness_visited.xml PARENT_SCOPE)
+set(tesh_files ${tesh_files} ${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_bugged1_liveness
- ${CMAKE_CURRENT_SOURCE_DIR}/promela_bugged2_liveness
- ${CMAKE_CURRENT_SOURCE_DIR}/bugged1_liveness_stack_cleaner PARENT_SCOPE)
+set(bin_files ${bin_files} ${CMAKE_CURRENT_SOURCE_DIR}/promela_bugged2_liveness PARENT_SCOPE)
+++ /dev/null
-/* Copyright (c) 2012-2020. 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. */
-
-/***************** Centralized Mutual Exclusion Algorithm *******************/
-/* This example implements a centralized mutual exclusion algorithm. */
-/* Bug : CS requests of client 1 not satisfied */
-/* LTL property checked : G(r->F(cs)); (r=request of CS, cs=CS ok) */
-/****************************************************************************/
-
-#ifdef GARBAGE_STACK
-#include <sys/stat.h>
-#include <fcntl.h>
-#include <unistd.h>
-#endif
-
-#include <simgrid/modelchecker.h>
-#include <simgrid/msg.h>
-#include <xbt/dynar.h>
-
-XBT_LOG_NEW_DEFAULT_CATEGORY(bugged1_liveness, "my log messages");
-
-int r=0;
-int cs=0;
-
-#ifdef GARBAGE_STACK
-/** Do not use a clean stack */
-static void garbage_stack(void) {
- const size_t size = 256;
- int fd = open("/dev/urandom", O_RDONLY);
- char foo[size];
- read(fd, foo, size);
- close(fd);
-}
-#endif
-
-static int coordinator(XBT_ATTRIB_UNUSED int argc, XBT_ATTRIB_UNUSED char* argv[])
-{
- int CS_used = 0;
- msg_task_t task = NULL;
- msg_task_t answer = NULL;
- xbt_dynar_t requests = xbt_dynar_new(sizeof(char *), NULL);
- char *req;
-
- while(1){
- MSG_task_receive(&task, "coordinator");
- const char *kind = MSG_task_get_name(task);
- if (!strcmp(kind, "request")) {
- req = MSG_task_get_data(task);
- if (CS_used) {
- XBT_INFO("CS already used. Queue the request.");
- xbt_dynar_push(requests, &req);
- } else {
- if(strcmp(req, "1") != 0){
- XBT_INFO("CS idle. Grant immediatly");
- answer = MSG_task_create("grant", 0, 1000, NULL);
- MSG_task_send(answer, req);
- CS_used = 1;
- answer = NULL;
- }
- }
- } else {
- if (!xbt_dynar_is_empty(requests)) {
- XBT_INFO("CS release. Grant to queued requests (queue size: %lu)", xbt_dynar_length(requests));
- xbt_dynar_shift(requests, &req);
- if(strcmp(req, "1") != 0){
- MSG_task_send(MSG_task_create("grant", 0, 1000, NULL), req);
- }else{
- xbt_dynar_push(requests, &req);
- CS_used = 0;
- }
- }else{
- XBT_INFO("CS release. resource now idle");
- CS_used = 0;
- }
- }
- MSG_task_destroy(task);
- task = NULL;
- kind = NULL;
- req = NULL;
- }
- return 0;
-}
-
-static int client(int argc, char *argv[])
-{
- xbt_assert(argc == 2);
- int my_pid = MSG_process_get_PID(MSG_process_self());
-
- char *my_mailbox = xbt_strdup(argv[1]);
- msg_task_t grant = NULL;
- msg_task_t release = NULL;
-
- while(1){
- XBT_INFO("Ask the request");
- MSG_task_send(MSG_task_create("request", 0, 1000, my_mailbox), "coordinator");
-
- if(strcmp(my_mailbox, "1") == 0){
- r = 1;
- cs = 0;
- XBT_INFO("Propositions changed : r=1, cs=0");
- }
-
- MSG_task_receive(&grant, my_mailbox);
- const char *kind = MSG_task_get_name(grant);
-
- if((strcmp(my_mailbox, "1") == 0) && (strcmp("grant", kind) == 0)){
- cs = 1;
- r = 0;
- XBT_INFO("Propositions changed : r=0, cs=1");
- }
-
- MSG_task_destroy(grant);
- grant = NULL;
- kind = NULL;
-
- XBT_INFO("%s got the answer. Sleep a bit and release it", argv[1]);
-
- MSG_process_sleep(1);
-
- release = MSG_task_create("release", 0, 1000, NULL);
- MSG_task_send(release, "coordinator");
-
- release = NULL;
-
- MSG_process_sleep(my_pid);
-
- if(strcmp(my_mailbox, "1") == 0){
- cs=0;
- r=0;
- XBT_INFO("Propositions changed : r=0, cs=0");
- }
-
- }
- return 0;
-}
-
-static int raw_client(int argc, char *argv[])
-{
-#ifdef GARBAGE_STACK
- // At this point the stack of the callee (client) is probably filled with
- // zeros and uninitialized variables will contain 0. This call will place
- // random byes in the stack of the callee:
- garbage_stack();
-#endif
- return client(argc, argv);
-}
-
-int main(int argc, char *argv[])
-{
- MSG_init(&argc, argv);
-
- MC_automaton_new_propositional_symbol_pointer("r", &r);
- MC_automaton_new_propositional_symbol_pointer("cs", &cs);
-
- MSG_create_environment(argv[1]);
-
- MSG_function_register("coordinator", coordinator);
- MSG_function_register("client", raw_client);
- MSG_launch_application(argv[2]);
-
- MSG_main();
-
- return 0;
-}
#!/usr/bin/env tesh
-$ ${bindir:=.}/centralized_mutex ${platfdir:=.}/model_checker_platform.xml
+$ ${bindir:=.}/centralized_mutex ${platfdir:=.}/small_platform.xml
+++ /dev/null
-<?xml version='1.0'?>
-<!DOCTYPE platform SYSTEM "https://simgrid.org/simgrid.dtd">
-<platform version="4.1">
- <actor host="Tremblay" function="coordinator" />
- <actor host="Boivin" function="client" >
- <argument value="1"/>
- </actor>
- <actor host="Fafard" function="client" >
- <argument value="2"/>
- </actor>
-</platform>
+++ /dev/null
-<?xml version='1.0'?>
-<!DOCTYPE platform SYSTEM "https://simgrid.org/simgrid.dtd">
-<platform version="4.1">
- <actor host="Tremblay" function="coordinator" />
- <actor host="Boivin" function="client" >
- <argument value="2"/>
- </actor>
- <actor host="Fafard" function="client" >
- <argument value="1"/>
- </actor>
-</platform>
set(_${example}_factories "ucontext;raw;boost")
endforeach()
+if(SIMGRID_HAVE_MC)
+ set(_mc-bugged1-liveness_disable 1)
+ if(HAVE_C_STACK_CLEANER)
+ add_executable (s4u-mc-bugged1-liveness-cleaner-on EXCLUDE_FROM_ALL s4u-mc-bugged1-liveness/s4u-mc-bugged1-liveness.cpp)
+ target_link_libraries(s4u-mc-bugged1-liveness-cleaner-on simgrid)
+ set_target_properties(s4u-mc-bugged1-liveness-cleaner-on PROPERTIES COMPILE_FLAGS "-DGARBAGE_STACK -fstack-cleaner")
+ add_dependencies(tests s4u-mc-bugged1-liveness-cleaner-on)
+
+ add_executable (s4u-mc-bugged1-liveness-cleaner-off EXCLUDE_FROM_ALL s4u-mc-bugged1-liveness/s4u-mc-bugged1-liveness.cpp)
+ target_link_libraries(s4u-mc-bugged1-liveness-cleaner-off simgrid)
+ set_target_properties(s4u-mc-bugged1-liveness-cleaner-off PROPERTIES COMPILE_FLAGS "-DGARBAGE_STACK -fno-stack-cleaner")
+ add_dependencies(tests s4u-mc-bugged1-liveness-cleaner-off)
+ endif()
+
+endif()
+
if(SIMGRID_HAVE_NS3)
add_executable (s4u-network-ns3 EXCLUDE_FROM_ALL network-ns3/s4u-network-ns3.cpp)
target_link_libraries(s4u-network-ns3 simgrid)
engine-filtering
exec-async exec-basic exec-dvfs exec-ptask exec-remote exec-waitany exec-waitfor exec-dependent
maestro-set
- mc-bugged1 mc-bugged2 mc-electric-fence mc-failing-assert
+ mc-bugged1 mc-bugged1-liveness mc-bugged2 mc-electric-fence mc-failing-assert
io-async io-file-system io-file-remote io-disk-raw io-dependent
platform-failures platform-profile platform-properties
plugin-hostload
endforeach()
set(tesh_files ${tesh_files} ${CMAKE_CURRENT_SOURCE_DIR}/app-masterworkers/s4u-app-masterworkers.tesh)
-
+# Model-checking liveness
+if(SIMGRID_HAVE_MC)
+ IF(HAVE_UCONTEXT_CONTEXTS AND SIMGRID_PROCESSOR_x86_64) # liveness model-checking works only on 64bits (for now ...)
+ ADD_TESH(s4u-mc-bugged1-liveness-ucontext --setenv bindir=${CMAKE_BINARY_DIR}/examples/s4u/mc-bugged1-liveness
+ --setenv platfdir=${CMAKE_HOME_DIRECTORY}/examples/platforms
+ --cd ${CMAKE_HOME_DIRECTORY}/examples/s4u/mc-bugged1-liveness/ s4u-mc-bugged1-liveness.tesh)
+ ADD_TESH(s4u-mc-bugged1-liveness-visited-ucontext --setenv bindir=${CMAKE_BINARY_DIR}/examples/s4u/mc-bugged1-liveness
+ --setenv platfdir=${CMAKE_HOME_DIRECTORY}/examples/platforms
+ --cd ${CMAKE_HOME_DIRECTORY}/examples/s4u/mc-bugged1-liveness/ s4u-mc-bugged1-liveness-visited.tesh)
+ IF(HAVE_C_STACK_CLEANER)
+ # This test checks if the stack cleaner is making a difference:
+ ADD_TEST(s4u-mc-bugged1-liveness-stack-cleaner ${CMAKE_HOME_DIRECTORY}/examples/s4u/mc-bugged1-liveness/s4u-mc-bugged1-liveness-stack-cleaner
+ ${CMAKE_HOME_DIRECTORY}/examples/s4u/mc-bugged1-liveness/
+ ${CMAKE_BINARY_DIR}/examples/s4u/mc-bugged1-liveness/)
+ ENDIF()
+ ENDIF()
+
+ if (enable_coverage)
+ SET_TESTS_PROPERTIES(mc-bugged1-liveness-visited-ucontext PROPERTIES RUN_SERIAL "TRUE")
+ endif()
+ENDIF()
# The tests the parallel variant of of DHTs
set(examples_src ${examples_src} ${CMAKE_CURRENT_SOURCE_DIR}/network-ns3/s4u-network-ns3.cpp PARENT_SCOPE)
set(tesh_files ${tesh_files} ${CMAKE_CURRENT_SOURCE_DIR}/app-pingpong/simix-breakpoint.tesh
+ ${CMAKE_CURRENT_SOURCE_DIR}/mc-bugged1-liveness/s4u-mc-bugged1-liveness-visited.tesh
${CMAKE_CURRENT_SOURCE_DIR}/network-ns3/s4u-network-ns3.tesh PARENT_SCOPE)
set(xml_files ${xml_files} ${CMAKE_CURRENT_SOURCE_DIR}/actor-create/s4u-actor-create_d.xml
${CMAKE_CURRENT_SOURCE_DIR}/actor-lifetime/s4u-actor-lifetime_d.xml
${CMAKE_CURRENT_SOURCE_DIR}/network-ns3/dogbone_d.xml
${CMAKE_CURRENT_SOURCE_DIR}/network-ns3/onelink_d.xml
${CMAKE_CURRENT_SOURCE_DIR}/network-ns3/one_cluster_d.xml PARENT_SCOPE)
-set(bin_files ${bin_files} ${CMAKE_CURRENT_SOURCE_DIR}/dht-kademlia/generate.py PARENT_SCOPE)
+set(bin_files ${bin_files} ${CMAKE_CURRENT_SOURCE_DIR}/dht-kademlia/generate.py
+ ${CMAKE_CURRENT_SOURCE_DIR}/mc-bugged1-liveness/s4u-mc-bugged1-liveness-stack-cleaner
+ ${CMAKE_CURRENT_SOURCE_DIR}/mc-bugged1-liveness/promela_bugged1_liveness PARENT_SCOPE)
set(txt_files ${txt_files} ${CMAKE_CURRENT_SOURCE_DIR}/replay-comm/s4u-replay-comm-split-p0.txt
${CMAKE_CURRENT_SOURCE_DIR}/replay-comm/s4u-replay-comm-split-p1.txt
${CMAKE_CURRENT_SOURCE_DIR}/replay-comm/s4u-replay-comm.txt
! expect return 2
! timeout 30
! output ignore
-$ ${bindir:=.}/../../../../bin/simgrid-mc ${bindir:=.}/bugged1_liveness ${platfdir:=.}/small_platform.xml ${srcdir:=.}/deploy_bugged1_liveness_visited.xml --log=xbt_cfg.thresh:warning "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --cfg=contexts/factory:ucontext --cfg=model-check/visited:100 --cfg=contexts/stack-size:256 --cfg=model-check/property:promela_bugged1_liveness
+$ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/s4u-mc-bugged1-liveness ${platfdir:=.}/small_platform.xml 1 --log=xbt_cfg.thresh:warning "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --cfg=contexts/factory:ucontext --cfg=model-check/visited:100 --cfg=contexts/stack-size:256 --cfg=model-check/property:promela_bugged1_liveness
> [ 0.000000] (0:maestro@) Check the liveness property promela_bugged1_liveness
> [ 0.000000] (2:client@Boivin) Ask the request
> [ 0.000000] (3:client@Fafard) Ask the request
--- /dev/null
+/* Copyright (c) 2012-2020. 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. */
+
+/***************** Centralized Mutual Exclusion Algorithm *******************/
+/* This example implements a centralized mutual exclusion algorithm. */
+/* Bug : CS requests of client 1 not satisfied */
+/* LTL property checked : G(r->F(cs)); (r=request of CS, cs=CS ok) */
+/****************************************************************************/
+
+#ifdef GARBAGE_STACK
+#include <fcntl.h>
+#include <sys/stat.h>
+#include <unistd.h>
+#endif
+
+#include <simgrid/modelchecker.h>
+#include <simgrid/s4u.hpp>
+#include <xbt/dynar.h>
+
+XBT_LOG_NEW_DEFAULT_CATEGORY(bugged1_liveness, "my log messages");
+
+class Message {
+public:
+ enum class Kind { GRANT, REQUEST, RELEASE };
+ Kind kind = Kind::GRANT;
+ simgrid::s4u::Mailbox* return_mailbox = nullptr;
+ explicit Message(Message::Kind kind, simgrid::s4u::Mailbox* mbox) : kind(kind), return_mailbox(mbox) {}
+};
+
+int r = 0;
+int cs = 0;
+
+#ifdef GARBAGE_STACK
+/** Do not use a clean stack */
+static void garbage_stack(void)
+{
+ const size_t size = 256;
+ int fd = open("/dev/urandom", O_RDONLY);
+ char foo[size];
+ read(fd, foo, size);
+ close(fd);
+}
+#endif
+
+static void coordinator()
+{
+ int CS_used = 0;
+ Message* m = nullptr;
+ std::queue<simgrid::s4u::Mailbox*> requests;
+
+ simgrid::s4u::Mailbox* mbox = simgrid::s4u::Mailbox::by_name("coordinator");
+
+ while (1) {
+ m = static_cast<Message*>(mbox->get());
+ if (m->kind == Message::Kind::REQUEST) {
+ if (CS_used) {
+ XBT_INFO("CS already used. Queue the request.");
+ requests.push(m->return_mailbox);
+ } else {
+ if (m->return_mailbox->get_name() != "1") {
+ XBT_INFO("CS idle. Grant immediatly");
+ m->return_mailbox->put(new Message(Message::Kind::GRANT, mbox), 1000);
+ CS_used = 1;
+ }
+ }
+ } else {
+ if (not requests.empty()) {
+ XBT_INFO("CS release. Grant to queued requests (queue size: %zu)", requests.size());
+ simgrid::s4u::Mailbox* req = requests.front();
+ requests.pop();
+ if (req->get_name() != "1") {
+ req->put(new Message(Message::Kind::GRANT, mbox), 1000);
+ } else {
+ requests.push(req);
+ CS_used = 0;
+ }
+ } else {
+ XBT_INFO("CS release. resource now idle");
+ CS_used = 0;
+ }
+ }
+ delete m;
+ }
+}
+
+static void client(int id)
+{
+ int my_pid = simgrid::s4u::this_actor::get_pid();
+
+ simgrid::s4u::Mailbox* my_mailbox = simgrid::s4u::Mailbox::by_name(std::to_string(id));
+
+ while (1) {
+ XBT_INFO("Ask the request");
+ simgrid::s4u::Mailbox::by_name("coordinator")->put(new Message(Message::Kind::REQUEST, my_mailbox), 1000);
+
+ if (id == 1) {
+ r = 1;
+ cs = 0;
+ XBT_INFO("Propositions changed : r=1, cs=0");
+ }
+
+ Message* grant = static_cast<Message*>(my_mailbox->get());
+
+ if ((id == 1) && (grant->kind == Message::Kind::GRANT)) {
+ cs = 1;
+ r = 0;
+ XBT_INFO("Propositions changed : r=0, cs=1");
+ }
+
+ delete grant;
+
+ XBT_INFO("%d got the answer. Sleep a bit and release it", id);
+
+ simgrid::s4u::this_actor::sleep_for(1);
+
+ simgrid::s4u::Mailbox::by_name("coordinator")->put(new Message(Message::Kind::RELEASE, my_mailbox), 1000);
+
+ simgrid::s4u::this_actor::sleep_for(my_pid);
+
+ if (id == 1) {
+ cs = 0;
+ r = 0;
+ XBT_INFO("Propositions changed : r=0, cs=0");
+ }
+ }
+}
+
+static void raw_client(int id)
+{
+#ifdef GARBAGE_STACK
+ // At this point the stack of the callee (client) is probably filled with
+ // zeros and uninitialized variables will contain 0. This call will place
+ // random byes in the stack of the callee:
+ garbage_stack();
+#endif
+ client(id);
+}
+
+int main(int argc, char* argv[])
+{
+ simgrid::s4u::Engine e(&argc, argv);
+
+ MC_automaton_new_propositional_symbol_pointer("r", &r);
+ MC_automaton_new_propositional_symbol_pointer("cs", &cs);
+
+ e.load_platform(argv[1]);
+
+ simgrid::s4u::Actor::create("coordinator", simgrid::s4u::Host::by_name("Tremblay"), coordinator);
+ if (std::stod(argv[2]) == 0) {
+ simgrid::s4u::Actor::create("client", simgrid::s4u::Host::by_name("Boivin"), raw_client, 1);
+ simgrid::s4u::Actor::create("client", simgrid::s4u::Host::by_name("Fafard"), raw_client, 2);
+ } else { // "Visited" case
+ simgrid::s4u::Actor::create("client", simgrid::s4u::Host::by_name("Boivin"), raw_client, 2);
+ simgrid::s4u::Actor::create("client", simgrid::s4u::Host::by_name("Fafard"), raw_client, 1);
+ }
+ e.run();
+
+ return 0;
+}
! expect return 2
! timeout 20
! output ignore
-$ ${bindir:=.}/../../../../bin/simgrid-mc ${bindir:=.}/bugged1_liveness ${platfdir:=.}/small_platform.xml ${srcdir:=.}/deploy_bugged1_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_bugged1_liveness
+$ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/s4u-mc-bugged1-liveness ${platfdir:=.}/small_platform.xml 0 --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_bugged1_liveness
> [ 0.000000] (0:maestro@) Check the liveness property promela_bugged1_liveness
> [ 0.000000] (2:client@Boivin) Ask the request
> [ 0.000000] (3:client@Fafard) Ask the request
