${CMAKE_HOME_DIRECTORY}/examples/s4u/${example}/s4u-${example}.tesh)
endforeach()
+
+# Model-checking examples: with only one source and tested with all factories but thread
+######################################################################
+
+foreach (example mc-failing-assert)
+ if(SIMGRID_HAVE_MC)
+ add_executable (s4u-${example} EXCLUDE_FROM_ALL ${example}/s4u-${example}.cpp)
+ add_dependencies (tests s4u-${example})
+ target_link_libraries(s4u-${example} simgrid)
+ set_target_properties(s4u-${example} PROPERTIES RUNTIME_OUTPUT_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR}/${example})
+
+
+ ADD_TESH_FACTORIES(s4u-${example} "ucontext;raw;boost"
+ --setenv bindir=${CMAKE_CURRENT_BINARY_DIR}/${example}
+ --setenv platfdir=${CMAKE_HOME_DIRECTORY}/examples/platforms
+ --cd ${CMAKE_CURRENT_SOURCE_DIR}/${example}
+ ${CMAKE_HOME_DIRECTORY}/examples/s4u/${example}/s4u-${example}.tesh)
+ endif()
+
+ set(tesh_files ${tesh_files} ${CMAKE_CURRENT_SOURCE_DIR}/${example}/s4u-${example}.tesh)
+ set(examples_src ${examples_src} ${CMAKE_CURRENT_SOURCE_DIR}/${example}/s4u-${example}.cpp)
+endforeach()
+
+
# Multi-files examples
######################
.. TODO:: document here the examples about plugins
+=======================
+Model-Checking Examples
+=======================
+
+The model-checker can be used to exhaustively search for issues in the
+tested application. It must be activated at compile time, but this
+mode is rather experimental in SimGrid (as of v3.22). You should not
+enable it unless you really want to formally verify your applications:
+SimGrid is slower and maybe less robust when MC is enabled.
+
+ - **Failed assert**
+ In this example, two actors send some data to a central server,
+ which asserts that the messages are always received in the same order.
+ This is obviously wrong, and the model-checker correctly finds a
+ counter-example to that assertion.
+ |br| `examples/s4u/mc-failed-assert/s4u-mc-failed-assert.cpp <https://framagit.org/simgrid/simgrid/tree/master/examples/s4u/mc-failed-assert/s4u-mc-failed-assert.cpp>`_
+
.. |br| raw:: html
<br />
--- /dev/null
+/* Copyright (c) 2010-2019. 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 *********************/
+/* Server assumes a fixed order in the reception of messages from its clients */
+/* which is incorrect because the message ordering is non-deterministic */
+/******************************************************************************/
+
+#include <simgrid/modelchecker.h>
+#include <simgrid/s4u.hpp>
+
+XBT_LOG_NEW_DEFAULT_CATEGORY(mc_assert_example, "Logging channel used in this example");
+
+static int server(int worker_amount)
+{
+ int value_got = -1;
+ simgrid::s4u::Mailbox* mb = simgrid::s4u::Mailbox::by_name("server");
+ for (int count = 0; count < worker_amount; count++) {
+ int* msg = static_cast<int*>(mb->get());
+ value_got = *msg;
+ free(msg);
+ }
+ /*
+ * We assert here that the last message we got (which overwrite any previously received message) is the one from the
+ * last worker This will obviously fail when the messages are received out of order.
+ */
+ MC_assert(value_got == 2);
+
+ XBT_INFO("OK");
+ return 0;
+}
+
+static int client(int rank)
+{
+ /* I just send my rank onto the mailbox. It must be passed as a stable memory block (thus the new) so that that
+ * memory survives even after the end of the client */
+
+ simgrid::s4u::Mailbox* mailbox = simgrid::s4u::Mailbox::by_name("server");
+ mailbox->put(new int(rank), 1 /* communication cost is not really relevant in MC mode */);
+
+ XBT_INFO("Sent!");
+ return 0;
+}
+
+int main(int argc, char* argv[])
+{
+ simgrid::s4u::Engine e(&argc, argv);
+ xbt_assert(argc > 1, "Usage: %s platform_file\n", argv[0]);
+
+ e.load_platform(argv[1]);
+ auto hosts = e.get_all_hosts();
+ xbt_assert(hosts.size() >= 3, "This example requires at least 3 hosts");
+
+ simgrid::s4u::Actor::create("server", hosts[0], &server, 2);
+ simgrid::s4u::Actor::create("client1", hosts[1], &client, 1);
+ simgrid::s4u::Actor::create("client2", hosts[2], &client, 2);
+
+ e.run();
+ return 0;
+}
--- /dev/null
+#!/usr/bin/env tesh
+
+! expect return 1
+! timeout 20
+$ ${bindir:=.}/../../../bin/simgrid-mc ${bindir:=.}/s4u-mc-failing-assert ${platfdir}/small_platform.xml "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n" --log=xbt_cfg.thresh:warning
+> [ 0.000000] (0:maestro@) Check a safety property. Reduction is: dpor.
+> [ 0.000000] (2:client1@Bourassa) Sent!
+> [ 0.000000] (1:server@Boivin) OK
+> [ 0.000000] (3:client2@Fafard) Sent!
+> [ 0.000000] (2:client1@Bourassa) Sent!
+> [ 0.000000] (2:client1@Bourassa) Sent!
+> [ 0.000000] (1:server@Boivin) OK
+> [ 0.000000] (3:client2@Fafard) Sent!
+> [ 0.000000] (2:client1@Bourassa) Sent!
+> [ 0.000000] (0:maestro@) **************************
+> [ 0.000000] (0:maestro@) *** PROPERTY NOT VALID ***
+> [ 0.000000] (0:maestro@) **************************
+> [ 0.000000] (0:maestro@) Counter-example execution trace:
+> [ 0.000000] (0:maestro@) [(1)Boivin (server)] iRecv(dst=(1)Boivin (server), buff=(verbose only), size=(verbose only))
+> [ 0.000000] (0:maestro@) [(3)Fafard (client2)] iSend(src=(3)Fafard (client2), buff=(verbose only), size=(verbose only))
+> [ 0.000000] (0:maestro@) [(1)Boivin (server)] Wait(comm=(verbose only) [(3)Fafard (client2)-> (1)Boivin (server)])
+> [ 0.000000] (0:maestro@) [(1)Boivin (server)] iRecv(dst=(1)Boivin (server), buff=(verbose only), size=(verbose only))
+> [ 0.000000] (0:maestro@) [(2)Bourassa (client1)] iSend(src=(2)Bourassa (client1), buff=(verbose only), size=(verbose only))
+> [ 0.000000] (0:maestro@) [(1)Boivin (server)] Wait(comm=(verbose only) [(2)Bourassa (client1)-> (1)Boivin (server)])
+> [ 0.000000] (0:maestro@) Expanded states = 18
+> [ 0.000000] (0:maestro@) Visited states = 36
+> [ 0.000000] (0:maestro@) Executed transitions = 32
