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/deploy_electric_fence.xml
-include examples/deprecated/msg/mc/electric_fence.c
-include examples/deprecated/msg/mc/platform.xml
include examples/deprecated/msg/mc/promela_bugged1_liveness
include examples/deprecated/msg/mc/promela_bugged2_liveness
include examples/deprecated/msg/synchro-semaphore/synchro-semaphore.c
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-electric-fence/platform.xml
+include examples/s4u/mc-electric-fence/s4u-mc-electric-fence.cpp
+include examples/s4u/mc-electric-fence/s4u-mc-electric-fence.tesh
include examples/s4u/mc-failing-assert/s4u-mc-failing-assert.cpp
include examples/s4u/mc-failing-assert/s4u-mc-failing-assert.tesh
include examples/s4u/network-ns3/3hosts_2links_d.xml
-foreach (x bugged1 bugged2 bugged3 centralized_mutex electric_fence bugged1_liveness bugged2_liveness)
+foreach (x bugged1 bugged2 bugged3 centralized_mutex bugged1_liveness bugged2_liveness)
if(SIMGRID_HAVE_MC AND SIMGRID_HAVE_MSG)
add_executable (${x} EXCLUDE_FROM_ALL ${x}.c)
target_link_libraries(${x} simgrid)
${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
- ${CMAKE_CURRENT_SOURCE_DIR}/platform.xml PARENT_SCOPE)
+set(xml_files ${xml_files} ${CMAKE_CURRENT_SOURCE_DIR}/deploy_bugged1_liveness_visited.xml 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
+++ /dev/null
-<?xml version='1.0'?>
-<!DOCTYPE platform SYSTEM "https://simgrid.org/simgrid.dtd">
-<platform version="4.1">
- <actor host="HostA" function="server">
- <argument value="0"/>
- </actor>
- <actor host="HostB" function="client">
- <argument value="1"/>
- </actor>
- <actor host="HostC" function="client">
- <argument value="2"/>
- </actor>
-</platform>
+++ /dev/null
-/* Copyright (c) 2013-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. */
-
-/******************** Non-deterministic message ordering *********************/
-/* This example implements one process which receives messages from two other */
-/* processes. There is no bug on it, it is just provided to test the soundness*/
-/* of the state space reduction with DPOR, if the maximum depth (defined with */
-/* --cfg=model-check/max-depth:) is reached. */
-/******************************************************************************/
-
-#include <simgrid/msg.h>
-#include <simgrid/modelchecker.h>
-
-#define N 2
-
-XBT_LOG_NEW_DEFAULT_CATEGORY(electric_fence, "Example to check the soundness of DPOR");
-
-static int server(XBT_ATTRIB_UNUSED int argc, XBT_ATTRIB_UNUSED char* argv[])
-{
- msg_task_t task1 = NULL;
- msg_task_t task2 = NULL;
-
- msg_comm_t comm_received1 = MSG_task_irecv(&task1, "mymailbox");
- msg_comm_t comm_received2 = MSG_task_irecv(&task2, "mymailbox");
-
- MSG_comm_wait(comm_received1, -1);
- MSG_comm_wait(comm_received2, -1);
-
- XBT_INFO("OK");
- return 0;
-}
-
-static int client(int argc, char *argv[])
-{
- xbt_assert(argc == 2);
- msg_task_t task = MSG_task_create(argv[1], 0, 10000, NULL);
-
- MSG_task_send(task, "mymailbox");
-
- XBT_INFO("Sent!");
- return 0;
-}
-
-int main(int argc, char *argv[])
-{
- MSG_init(&argc, argv);
-
- MSG_create_environment("platform.xml");
-
- MSG_function_register("server", server);
- MSG_function_register("client", client);
- MSG_launch_application("deploy_electric_fence.xml");
-
- MSG_main();
- return 0;
-}
set(_${example}_factories "ucontext;raw;boost")
endforeach()
+set(_mc-electric-fence_disable 1)
+
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-failing-assert
+ 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
${CMAKE_CURRENT_SOURCE_DIR}/dht-kademlia/s4u-dht-kademlia_d.xml
${CMAKE_CURRENT_SOURCE_DIR}/energy-boot/platform_boot.xml
${CMAKE_CURRENT_SOURCE_DIR}/io-file-remote/s4u-io-file-remote_d.xml
+ ${CMAKE_CURRENT_SOURCE_DIR}/mc-electric-fence/platform.xml
${CMAKE_CURRENT_SOURCE_DIR}/platform-properties/s4u-platform-properties_d.xml
${CMAKE_CURRENT_SOURCE_DIR}/platform-failures/s4u-platform-failures_d.xml
${CMAKE_CURRENT_SOURCE_DIR}/replay-comm/s4u-replay-comm-split_d.xml
<host id="HostA" speed="137.333Mf"/>
<host id="HostB" speed="98.095Mf"/>
<host id="HostC" speed="98.095Mf"/>
- <host id="HostD" speed="98.095Mf"/>
<link id="1" bandwidth="3.430125MBps" latency="536.941us"/>
<link id="2" bandwidth="3.430125MBps" latency="536.941us"/>
- <link id="3" bandwidth="3.430125MBps" latency="536.941us"/>
<route src="HostA" dst="HostB">
<link_ctn id="1"/>
</route>
<route src="HostA" dst="HostC">
<link_ctn id="2"/>
</route>
- <route src="HostA" dst="HostD">
- <link_ctn id="3"/>
- </route>
</zone>
</platform>
--- /dev/null
+/* Copyright (c) 2013-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. */
+
+/******************** Non-deterministic message ordering *********************/
+/* This example implements one process which receives messages from two other */
+/* processes. There is no bug on it, it is just provided to test the soundness*/
+/* of the state space reduction with DPOR, if the maximum depth (defined with */
+/* --cfg=model-check/max-depth:) is reached. */
+/******************************************************************************/
+
+#include <simgrid/modelchecker.h>
+#include <simgrid/s4u.hpp>
+
+#define N 2
+
+XBT_LOG_NEW_DEFAULT_CATEGORY(electric_fence, "Example to check the soundness of DPOR");
+
+static void server()
+{
+ void* data1 = nullptr;
+ void* data2 = nullptr;
+ simgrid::s4u::CommPtr comm_received1 = simgrid::s4u::Mailbox::by_name("mymailbox")->get_async(&data1);
+ simgrid::s4u::CommPtr comm_received2 = simgrid::s4u::Mailbox::by_name("mymailbox")->get_async(&data2);
+
+ comm_received1->wait();
+ comm_received2->wait();
+
+ XBT_INFO("OK");
+ delete static_cast<int*>(data1);
+ delete static_cast<int*>(data2);
+}
+
+static void client(int id)
+{
+ int* payload = new int();
+ *payload = id;
+ simgrid::s4u::Mailbox::by_name("mymailbox")->put(payload, 10000);
+ XBT_INFO("Sent!");
+}
+
+int main(int argc, char* argv[])
+{
+ simgrid::s4u::Engine e(&argc, argv);
+
+ e.load_platform("platform.xml");
+
+ simgrid::s4u::Actor::create("server", simgrid::s4u::Host::by_name("HostA"), server);
+ simgrid::s4u::Actor::create("client", simgrid::s4u::Host::by_name("HostB"), client, 1);
+ simgrid::s4u::Actor::create("client", simgrid::s4u::Host::by_name("HostC"), client, 2);
+
+ e.run();
+ return 0;
+}