From: Martin Quinson <martin.quinson@loria.fr>
Date: Mon, 4 Apr 2016 17:01:00 +0000 (+0200)
Subject: Merge branch 'master' of scm.gforge.inria.fr:/gitroot/simgrid/simgrid
X-Git-Tag: v3_13~180^2~7
X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/d4f9d0cf42605d96b91088c02ddfbf2411f89de1?hp=9f646472eb2d52b33a9be7450259564ac890ea99

Merge branch 'master' of scm.gforge.inria.fr:/gitroot/simgrid/simgrid
---

diff --git a/examples/msg/cloud/bound.c b/examples/msg/cloud/bound.c
index ffb7387505..aef36265ba 100644
--- a/examples/msg/cloud/bound.c
+++ b/examples/msg/cloud/bound.c
@@ -4,22 +4,13 @@
 /* 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. */
 
-#include <stdio.h>
-#include "simgrid/msg.h"        /* Yeah! If you want to use msg, you need to include simgrid/msg.h */
-#include "xbt/sysdep.h"         /* calloc, printf */
+#include "simgrid/msg.h"
 
-/* Create a log channel to have nice outputs. */
-#include "xbt/log.h"
-#include "xbt/asserts.h"
-XBT_LOG_NEW_DEFAULT_CATEGORY(msg_test,
-                             "Messages specific for this msg example");
+XBT_LOG_NEW_DEFAULT_CATEGORY(msg_test, "Messages specific for this msg example");
 
 /** @addtogroup MSG_examples
  *
- * - <b>priority/priority.c</b>: Demonstrates the use of @ref
- *   MSG_task_set_bound to change the computation priority of a
- *   given task.
- *
+ * - <b>cloud/bound.c</b>: Demonstrates the use of @ref MSG_task_set_bound
  */
 
 static int worker_main(int argc, char *argv[])
@@ -28,24 +19,22 @@ static int worker_main(int argc, char *argv[])
   int use_bound = xbt_str_parse_int(argv[2], "Second parameter (use_bound) should be 0 or 1 but is: %s");
   double bound = xbt_str_parse_double(argv[3], "Invalid bound: %s");
 
-  {
-    double clock_sta = MSG_get_clock();
-
-    msg_task_t task = MSG_task_create("Task", computation_amount, 0, NULL);
-    if (use_bound)
-      MSG_task_set_bound(task, bound);
-    MSG_task_execute(task);
-    MSG_task_destroy(task);
-
-    double clock_end = MSG_get_clock();
-    double duration = clock_end - clock_sta;
-    double flops_per_sec = computation_amount / duration;
-
-    if (use_bound)
-      XBT_INFO("bound to %f => duration %f (%f flops/s)", bound, duration, flops_per_sec);
-    else
-      XBT_INFO("not bound => duration %f (%f flops/s)", duration, flops_per_sec);
-  }
+  double clock_sta = MSG_get_clock();
+
+  msg_task_t task = MSG_task_create("Task", computation_amount, 0, NULL);
+  if (use_bound)
+     MSG_task_set_bound(task, bound);
+  MSG_task_execute(task);
+  MSG_task_destroy(task);
+
+  double clock_end = MSG_get_clock();
+  double duration = clock_end - clock_sta;
+  double flops_per_sec = computation_amount / duration;
+
+  if (use_bound)
+    XBT_INFO("bound to %f => duration %f (%f flops/s)", bound, duration, flops_per_sec);
+  else
+    XBT_INFO("not bound => duration %f (%f flops/s)", duration, flops_per_sec);
 
   return 0;
 }
@@ -62,13 +51,10 @@ static void launch_worker(msg_host_t host, const char *pr_name, double computati
   MSG_process_create_with_arguments(pr_name, worker_main, NULL, host, 4, argv);
 }
 
-
-
 static int worker_busy_loop_main(int argc, char *argv[])
 {
   msg_task_t *task = MSG_process_get_data(MSG_process_self());
-  for (;;)
-    MSG_task_execute(*task);
+  MSG_task_execute(*task);
 
   return 0;
 }
@@ -88,9 +74,8 @@ static void test_dynamic_change(void)
 
   msg_task_t task0 = MSG_task_create("Task0", DOUBLE_MAX, 0, NULL);
   msg_task_t task1 = MSG_task_create("Task1", DOUBLE_MAX, 0, NULL);
-  msg_process_t pr0 = MSG_process_create("worker0", worker_busy_loop_main, &task0, vm0);
-  msg_process_t pr1 = MSG_process_create("worker1", worker_busy_loop_main, &task1, vm1);
-
+  MSG_process_create("worker0", worker_busy_loop_main, &task0, vm0);
+  MSG_process_create("worker1", worker_busy_loop_main, &task1, vm1);
 
   double task0_remain_prev = MSG_task_get_flops_amount(task0);
   double task1_remain_prev = MSG_task_get_flops_amount(task1);
@@ -117,16 +102,12 @@ static void test_dynamic_change(void)
       task1_remain_prev = task1_remain_now;
     }
   }
+  MSG_process_sleep(2000); // let the tasks end
 
-  MSG_process_kill(pr0);
-  MSG_process_kill(pr1);
-  
   MSG_vm_destroy(vm0);
   MSG_vm_destroy(vm1);
 }
 
-
-
 static void test_one_task(msg_host_t hostA)
 {
   const double cpu_speed = MSG_host_get_speed(hostA);
@@ -135,43 +116,32 @@ static void test_one_task(msg_host_t hostA)
 
   XBT_INFO("### Test: with/without MSG_task_set_bound");
 
-  {
-    XBT_INFO("### Test: no bound for Task1@%s", hostA_name);
-    launch_worker(hostA, "worker0", computation_amount, 0, 0);
-  }
+  XBT_INFO("### Test: no bound for Task1@%s", hostA_name);
+  launch_worker(hostA, "worker0", computation_amount, 0, 0);
 
   MSG_process_sleep(1000);
 
-  {
-    XBT_INFO("### Test: 50%% for Task1@%s", hostA_name);
-    launch_worker(hostA, "worker0", computation_amount, 1, cpu_speed / 2);
-  }
+  XBT_INFO("### Test: 50%% for Task1@%s", hostA_name);
+  launch_worker(hostA, "worker0", computation_amount, 1, cpu_speed / 2);
 
   MSG_process_sleep(1000);
 
-  {
-    XBT_INFO("### Test: 33%% for Task1@%s", hostA_name);
-    launch_worker(hostA, "worker0", computation_amount, 1, cpu_speed / 3);
-  }
+  XBT_INFO("### Test: 33%% for Task1@%s", hostA_name);
+  launch_worker(hostA, "worker0", computation_amount, 1, cpu_speed / 3);
 
   MSG_process_sleep(1000);
 
-  {
-    XBT_INFO("### Test: zero for Task1@%s (i.e., unlimited)", hostA_name);
-    launch_worker(hostA, "worker0", computation_amount, 1, 0);
-  }
+  XBT_INFO("### Test: zero for Task1@%s (i.e., unlimited)", hostA_name);
+  launch_worker(hostA, "worker0", computation_amount, 1, 0);
 
   MSG_process_sleep(1000);
 
-  {
-    XBT_INFO("### Test: 200%% for Task1@%s (i.e., meaningless)", hostA_name);
-    launch_worker(hostA, "worker0", computation_amount, 1, cpu_speed * 2);
-  }
+  XBT_INFO("### Test: 200%% for Task1@%s (i.e., meaningless)", hostA_name);
+  launch_worker(hostA, "worker0", computation_amount, 1, cpu_speed * 2);
 
   MSG_process_sleep(1000);
 }
 
-
 static void test_two_tasks(msg_host_t hostA, msg_host_t hostB)
 {
   const double cpu_speed = MSG_host_get_speed(hostA);
@@ -180,59 +150,45 @@ static void test_two_tasks(msg_host_t hostA, msg_host_t hostB)
   const char *hostA_name = MSG_host_get_name(hostA);
   const char *hostB_name = MSG_host_get_name(hostB);
 
-  {
-    XBT_INFO("### Test: no bound for Task1@%s, no bound for Task2@%s", hostA_name, hostB_name);
-    launch_worker(hostA, "worker0", computation_amount, 0, 0);
-    launch_worker(hostB, "worker1", computation_amount, 0, 0);
-  }
+  XBT_INFO("### Test: no bound for Task1@%s, no bound for Task2@%s", hostA_name, hostB_name);
+  launch_worker(hostA, "worker0", computation_amount, 0, 0);
+  launch_worker(hostB, "worker1", computation_amount, 0, 0);
 
   MSG_process_sleep(1000);
 
-  {
-    XBT_INFO("### Test: 0 for Task1@%s, 0 for Task2@%s (i.e., unlimited)", hostA_name, hostB_name);
-    launch_worker(hostA, "worker0", computation_amount, 1, 0);
-    launch_worker(hostB, "worker1", computation_amount, 1, 0);
-  }
+  XBT_INFO("### Test: 0 for Task1@%s, 0 for Task2@%s (i.e., unlimited)", hostA_name, hostB_name);
+  launch_worker(hostA, "worker0", computation_amount, 1, 0);
+  launch_worker(hostB, "worker1", computation_amount, 1, 0);
 
   MSG_process_sleep(1000);
 
-  {
-    XBT_INFO("### Test: 50%% for Task1@%s, 50%% for Task2@%s", hostA_name, hostB_name);
-    launch_worker(hostA, "worker0", computation_amount, 1, cpu_speed / 2);
-    launch_worker(hostB, "worker1", computation_amount, 1, cpu_speed / 2);
-  }
+  XBT_INFO("### Test: 50%% for Task1@%s, 50%% for Task2@%s", hostA_name, hostB_name);
+  launch_worker(hostA, "worker0", computation_amount, 1, cpu_speed / 2);
+  launch_worker(hostB, "worker1", computation_amount, 1, cpu_speed / 2);
 
   MSG_process_sleep(1000);
 
-  {
-    XBT_INFO("### Test: 25%% for Task1@%s, 25%% for Task2@%s", hostA_name, hostB_name);
-    launch_worker(hostA, "worker0", computation_amount, 1, cpu_speed / 4);
-    launch_worker(hostB, "worker1", computation_amount, 1, cpu_speed / 4);
-  }
+  XBT_INFO("### Test: 25%% for Task1@%s, 25%% for Task2@%s", hostA_name, hostB_name);
+  launch_worker(hostA, "worker0", computation_amount, 1, cpu_speed / 4);
+  launch_worker(hostB, "worker1", computation_amount, 1, cpu_speed / 4);
 
   MSG_process_sleep(1000);
 
-  {
-    XBT_INFO("### Test: 75%% for Task1@%s, 100%% for Task2@%s", hostA_name, hostB_name);
-    launch_worker(hostA, "worker0", computation_amount, 1, cpu_speed * 0.75);
-    launch_worker(hostB, "worker1", computation_amount, 1, cpu_speed);
-  }
+  XBT_INFO("### Test: 75%% for Task1@%s, 100%% for Task2@%s", hostA_name, hostB_name);
+  launch_worker(hostA, "worker0", computation_amount, 1, cpu_speed * 0.75);
+  launch_worker(hostB, "worker1", computation_amount, 1, cpu_speed);
 
   MSG_process_sleep(1000);
 
-  {
-    XBT_INFO("### Test: no bound for Task1@%s, 25%% for Task2@%s", hostA_name, hostB_name);
-    launch_worker(hostA, "worker0", computation_amount, 0, 0);
-    launch_worker(hostB, "worker1", computation_amount, 1, cpu_speed / 4);
-  }
+  XBT_INFO("### Test: no bound for Task1@%s, 25%% for Task2@%s", hostA_name, hostB_name);
+  launch_worker(hostA, "worker0", computation_amount, 0, 0);
+  launch_worker(hostB, "worker1", computation_amount, 1, cpu_speed / 4);
 
   MSG_process_sleep(1000);
 
-  {
-    XBT_INFO("### Test: 75%% for Task1@%s, 25%% for Task2@%s", hostA_name, hostB_name);
-    launch_worker(hostA, "worker0", computation_amount, 1, cpu_speed * 0.75);
-    launch_worker(hostB, "worker1", computation_amount, 1, cpu_speed / 4);
-  }
+  XBT_INFO("### Test: 75%% for Task1@%s, 25%% for Task2@%s", hostA_name, hostB_name);
+  launch_worker(hostA, "worker0", computation_amount, 1, cpu_speed * 0.75);
+  launch_worker(hostB, "worker1", computation_amount, 1, cpu_speed / 4);
 
   MSG_process_sleep(1000);
 }
@@ -243,109 +199,90 @@ static int master_main(int argc, char *argv[])
   msg_host_t pm0 = xbt_dynar_get_as(hosts_dynar, 0, msg_host_t);
   msg_host_t pm1 = xbt_dynar_get_as(hosts_dynar, 0, msg_host_t);
 
+  XBT_INFO("# 1. Put a single task on a PM. ");
+  test_one_task(pm0);
+  XBT_INFO(" ");
 
-  {
-    XBT_INFO("# 1. Put a single task on a PM. ");
-    test_one_task(pm0);
-    XBT_INFO(" ");
+  XBT_INFO("# 2. Put two tasks on a PM.");
+  test_two_tasks(pm0, pm0);
+  XBT_INFO(" ");
 
+  msg_host_t vm0 = MSG_vm_create_core(pm0, "VM0");
+  MSG_vm_start(vm0);
 
-    XBT_INFO("# 2. Put two tasks on a PM.");
-    test_two_tasks(pm0, pm0);
-    XBT_INFO(" ");
-  }
-
-
-  {
-    msg_host_t vm0 = MSG_vm_create_core(pm0, "VM0");
-    MSG_vm_start(vm0);
-
-    XBT_INFO("# 3. Put a single task on a VM. ");
-    test_one_task(vm0);
-    XBT_INFO(" ");
-
-    XBT_INFO("# 4. Put two tasks on a VM.");
-    test_two_tasks(vm0, vm0);
-    XBT_INFO(" ");
-
-
-    MSG_vm_destroy(vm0);
-  }
-
-
-  {
-    msg_host_t vm0 = MSG_vm_create_core(pm0, "VM0");
-    MSG_vm_start(vm0);
-
-    XBT_INFO("# 6. Put a task on a PM and a task on a VM.");
-    test_two_tasks(pm0, vm0);
-    XBT_INFO(" ");
+  XBT_INFO("# 3. Put a single task on a VM. ");
+  test_one_task(vm0);
+  XBT_INFO(" ");
 
+  XBT_INFO("# 4. Put two tasks on a VM.");
+  test_two_tasks(vm0, vm0);
+  XBT_INFO(" ");
 
-    MSG_vm_destroy(vm0);
-  }
+  MSG_vm_destroy(vm0);
 
+  vm0 = MSG_vm_create_core(pm0, "VM0");
+  MSG_vm_start(vm0);
 
-  {
-    msg_host_t vm0 = MSG_vm_create_core(pm0, "VM0");
-    const double cpu_speed = MSG_host_get_speed(pm0);
-    MSG_vm_set_bound(vm0, cpu_speed / 10);
-    MSG_vm_start(vm0);
+  XBT_INFO("# 6. Put a task on a PM and a task on a VM.");
+  test_two_tasks(pm0, vm0);
+  XBT_INFO(" ");
 
-    XBT_INFO("# 7. Put a single task on the VM capped by 10%%.");
-    test_one_task(vm0);
-    XBT_INFO(" ");
+  MSG_vm_destroy(vm0);
 
-    XBT_INFO("# 8. Put two tasks on the VM capped by 10%%.");
-    test_two_tasks(vm0, vm0);
-    XBT_INFO(" ");
+  vm0 = MSG_vm_create_core(pm0, "VM0");
+  double cpu_speed = MSG_host_get_speed(pm0);
+  MSG_vm_set_bound(vm0, cpu_speed / 10);
+  MSG_vm_start(vm0);
 
-    XBT_INFO("# 9. Put a task on a PM and a task on the VM capped by 10%%.");
-    test_two_tasks(pm0, vm0);
-    XBT_INFO(" ");
+  XBT_INFO("# 7. Put a single task on the VM capped by 10%%.");
+  test_one_task(vm0);
+  XBT_INFO(" ");
 
-    MSG_vm_destroy(vm0);
-  }
+  XBT_INFO("# 8. Put two tasks on the VM capped by 10%%.");
+  test_two_tasks(vm0, vm0);
+  XBT_INFO(" ");
 
+  XBT_INFO("# 9. Put a task on a PM and a task on the VM capped by 10%%.");
+  test_two_tasks(pm0, vm0);
+  XBT_INFO(" ");
 
-  {
-    msg_host_t vm0 = MSG_vm_create_core(pm0, "VM0");
+  MSG_vm_destroy(vm0);
 
-    s_vm_params_t params;
-    memset(&params, 0, sizeof(params));
-    params.ramsize = 1L * 1000 * 1000 * 1000; // 1Gbytes
-    MSG_host_set_params(vm0, &params);
-    MSG_vm_start(vm0);
+  vm0 = MSG_vm_create_core(pm0, "VM0");
 
-    const double cpu_speed = MSG_host_get_speed(pm0);
-    MSG_vm_start(vm0);
+  s_vm_params_t params;
+  memset(&params, 0, sizeof(params));
+  params.ramsize = 1L * 1000 * 1000 * 1000; // 1Gbytes
+  MSG_host_set_params(vm0, &params);
+  MSG_vm_start(vm0);
 
-    XBT_INFO("# 10. Test migration");
-    const double computation_amount = cpu_speed * 10;
+  cpu_speed = MSG_host_get_speed(pm0);
+  MSG_vm_start(vm0);
 
-    XBT_INFO("# 10. (a) Put a task on a VM without any bound.");
-    launch_worker(vm0, "worker0", computation_amount, 0, 0);
-    MSG_process_sleep(1000);
-    XBT_INFO(" ");
+  XBT_INFO("# 10. Test migration");
+  const double computation_amount = cpu_speed * 10;
 
-    XBT_INFO("# 10. (b) set 10%% bound to the VM, and then put a task on the VM.");
-    MSG_vm_set_bound(vm0, cpu_speed / 10);
-    launch_worker(vm0, "worker0", computation_amount, 0, 0);
-    MSG_process_sleep(1000);
-    XBT_INFO(" ");
+  XBT_INFO("# 10. (a) Put a task on a VM without any bound.");
+  launch_worker(vm0, "worker0", computation_amount, 0, 0);
+  MSG_process_sleep(1000);
+  XBT_INFO(" ");
 
-    XBT_INFO("# 10. (c) migrate");
-    MSG_vm_migrate(vm0, pm1);
-    XBT_INFO(" ");
+  XBT_INFO("# 10. (b) set 10%% bound to the VM, and then put a task on the VM.");
+  MSG_vm_set_bound(vm0, cpu_speed / 10);
+  launch_worker(vm0, "worker0", computation_amount, 0, 0);
+  MSG_process_sleep(1000);
+  XBT_INFO(" ");
 
-    XBT_INFO("# 10. (d) Put a task again on the VM.");
-    launch_worker(vm0, "worker0", computation_amount, 0, 0);
-    MSG_process_sleep(1000);
-    XBT_INFO(" ");
+  XBT_INFO("# 10. (c) migrate");
+  MSG_vm_migrate(vm0, pm1);
+  XBT_INFO(" ");
 
-    MSG_vm_destroy(vm0);
-  }
+  XBT_INFO("# 10. (d) Put a task again on the VM.");
+  launch_worker(vm0, "worker0", computation_amount, 0, 0);
+  MSG_process_sleep(1000);
+  XBT_INFO(" ");
 
+  MSG_vm_destroy(vm0);
 
   XBT_INFO("# 11. Change a bound dynamically.");
   test_dynamic_change();
@@ -369,10 +306,7 @@ int main(int argc, char *argv[])
   MSG_init(&argc, argv);
 
   /* load the platform file */
-  if (argc != 2) {
-    printf("Usage: %s example/msg/cloud/simple_plat.xml\n", argv[0]);
-    return 1;
-  }
+  xbt_assert(argc == 2, "Usage: %s platform_file\n\tExample: %s ../platforms/small_platform.xml\n", argv[0], argv[0]);
 
   MSG_create_environment(argv[1]);
 
@@ -383,6 +317,5 @@ int main(int argc, char *argv[])
   int res = MSG_main();
   XBT_INFO("Bye (simulation time %g)", MSG_get_clock());
 
-
   return !(res == MSG_OK);
 }
diff --git a/examples/msg/exception/exception.c b/examples/msg/exception/exception.c
index 56b06f7862..e505e7595b 100644
--- a/examples/msg/exception/exception.c
+++ b/examples/msg/exception/exception.c
@@ -108,11 +108,10 @@ int main(int argc, char *argv[]) {
   msg_error_t res = MSG_OK;
 
   MSG_init(&argc, argv);
-  xbt_assert(argc > 2, "Usage: %s platform_file\n\tExample: %s msg_platform.xml\n", argv[0], argv[0]);
+  xbt_assert(argc == 2, "Usage: %s platform_file\n\tExample: %s msg_platform.xml\n", argv[0], argv[0]);
 
   MSG_create_environment(argv[1]);
   MSG_process_create("terrorist", terrorist, NULL, MSG_get_host_by_name("Jacquelin"));
-  MSG_launch_application(argv[2]);
 
   // Launch the simulation
   res = MSG_main();
diff --git a/examples/msg/exception/exception.tesh b/examples/msg/exception/exception.tesh
index db3b7a7754..4dff602278 100644
--- a/examples/msg/exception/exception.tesh
+++ b/examples/msg/exception/exception.tesh
@@ -18,13 +18,15 @@ $ $SG_TEST_EXENV exception/exception ${srcdir:=.}/../platforms/platform.xml "--l
 > [  3.000000] (2:victim@Jacquelin) The received exception resumed my suspension. Good. Here is it:  ----------------------->8----
 > ** SimGrid: UNCAUGHT EXCEPTION received on exception/exception(2): category: action canceled; value: 0
 > ** Canceled
-> ** Thrown by () on process 0
+> ** Thrown by maestro() on process 0
 > [  0.000000] (0:maestro@) Configuration change: Set 'exception/cutpath' to '1'
 > [  3.000000] (2:victim@Jacquelin) Canceled
 >
-> **   In SIMIX_execution_finish() at smx_host.c
-> **   In SIMIX_run() at smx_global.c
-> **   In MSG_main() at msg_global.c
+> **   In SIMIX_execution_finish() at smx_host.cpp
+> **   In SIMIX_post_host_execute() at smx_host.cpp
+> **   In SIMIX_run() at src/simix/smx_global.cpp:482 (discriminator smx_global.cpp:482 (discriminator 1)
+> **   In SIMIX_simcall_exit() at popping.cpp
+> **   In MSG_main() at msg_global.cpp
 > **   In main() at exception.c
 > [  3.000000] (2:victim@Jacquelin) (end of the second exception) ----8<------------------------
 > [  3.000000] (2:victim@Jacquelin) Let's sleep for 10 seconds.
diff --git a/examples/msg/mc/bugged1_liveness.c b/examples/msg/mc/bugged1_liveness.c
index 04945213c5..949020bd2f 100644
--- a/examples/msg/mc/bugged1_liveness.c
+++ b/examples/msg/mc/bugged1_liveness.c
@@ -18,7 +18,6 @@
 
 #include "simgrid/msg.h"
 #include "mc/mc.h"
-#include "xbt/automaton.h"
 #include "bugged1_liveness.h"
 
 XBT_LOG_NEW_DEFAULT_CATEGORY(bugged1_liveness, "my log messages");
diff --git a/examples/msg/mc/bugged2_liveness.c b/examples/msg/mc/bugged2_liveness.c
index da785bb23f..b82e3ac05c 100644
--- a/examples/msg/mc/bugged2_liveness.c
+++ b/examples/msg/mc/bugged2_liveness.c
@@ -12,7 +12,6 @@
 
 #include "simgrid/msg.h"
 #include "mc/mc.h"
-#include "xbt/automaton.h"
 #include "bugged2_liveness.h"
 
 XBT_LOG_NEW_DEFAULT_CATEGORY(bugged3, "my log messages");
diff --git a/include/simgrid/modelchecker.h b/include/simgrid/modelchecker.h
index a401b7a5fe..0579ca6e2a 100644
--- a/include/simgrid/modelchecker.h
+++ b/include/simgrid/modelchecker.h
@@ -20,7 +20,6 @@
 #include <simgrid_config.h> /* HAVE_MC ? */
 
 #include <xbt/base.h>
-#include <xbt/automaton.h>
 
 SG_BEGIN_DECL()
 
diff --git a/src/mc/Checker.hpp b/src/mc/Checker.hpp
index af861cd455..625967887e 100644
--- a/src/mc/Checker.hpp
+++ b/src/mc/Checker.hpp
@@ -53,6 +53,8 @@ protected:
 };
 
 XBT_PUBLIC() Checker* createLivenessChecker(Session& session);
+XBT_PUBLIC() Checker* createSafetyChecker(Session& session);
+XBT_PUBLIC() Checker* createCommunicationDeterminismChecker(Session& session);
 
 }
 }
diff --git a/src/mc/CommunicationDeterminismChecker.cpp b/src/mc/CommunicationDeterminismChecker.cpp
index b30b312d48..a817ff97a1 100644
--- a/src/mc/CommunicationDeterminismChecker.cpp
+++ b/src/mc/CommunicationDeterminismChecker.cpp
@@ -8,7 +8,6 @@
 
 #include <xbt/dynar.h>
 #include <xbt/dynar.hpp>
-#include <xbt/fifo.h>
 #include <xbt/log.h>
 #include <xbt/sysdep.h>
 
@@ -22,6 +21,7 @@
 #include "src/mc/Client.hpp"
 #include "src/mc/CommunicationDeterminismChecker.hpp"
 #include "src/mc/mc_exit.h"
+#include "src/mc/VisitedState.hpp"
 
 using simgrid::mc::remote;
 
@@ -315,50 +315,39 @@ CommunicationDeterminismChecker::~CommunicationDeterminismChecker()
 RecordTrace CommunicationDeterminismChecker::getRecordTrace() // override
 {
   RecordTrace res;
-
-  xbt_fifo_item_t start = xbt_fifo_get_last_item(mc_stack);
-  for (xbt_fifo_item_t item = start; item; item = xbt_fifo_get_prev_item(item)) {
-
-    // Find (pid, value):
-    simgrid::mc::State* state = (simgrid::mc::State*) xbt_fifo_get_item_content(item);
+  for (auto const& state : stack_) {
     int value = 0;
-    smx_simcall_t saved_req = MC_state_get_executed_request(state, &value);
+    smx_simcall_t saved_req = MC_state_get_executed_request(state.get(), &value);
     const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req);
     const int pid = issuer->pid;
-
     res.push_back(RecordTraceElement(pid, value));
   }
-
   return res;
 }
 
 // TODO, deduplicate with SafetyChecker
 std::vector<std::string> CommunicationDeterminismChecker::getTextualTrace() // override
 {
-  std::vector<std::string> res;
-  for (xbt_fifo_item_t item = xbt_fifo_get_last_item(mc_stack);
-       item; item = xbt_fifo_get_prev_item(item)) {
-    simgrid::mc::State* state = (simgrid::mc::State*)xbt_fifo_get_item_content(item);
+  std::vector<std::string> trace;
+  for (auto const& state : stack_) {
     int value;
-    smx_simcall_t req = MC_state_get_executed_request(state, &value);
+    smx_simcall_t req = MC_state_get_executed_request(state.get(), &value);
     if (req) {
       char* req_str = simgrid::mc::request_to_string(
         req, value, simgrid::mc::RequestType::executed);
-      res.push_back(req_str);
+      trace.push_back(req_str);
       xbt_free(req_str);
     }
   }
-  return res;
+  return trace;
 }
 
 void CommunicationDeterminismChecker::prepare()
 {
-  simgrid::mc::State* initial_state = nullptr;
+
   int i;
   const int maxpid = MC_smx_get_maxpid();
 
-  simgrid::mc::visited_states.clear();
-
   // Create initial_communications_pattern elements:
   initial_communications_pattern = xbt_dynar_new(sizeof(mc_list_comm_pattern_t), MC_list_comm_pattern_free_voidp);
   for (i=0; i < maxpid; i++){
@@ -375,7 +364,8 @@ void CommunicationDeterminismChecker::prepare()
     xbt_dynar_insert_at(incomplete_communications_pattern, i, &process_pattern);
   }
 
-  initial_state = MC_state_new();
+  std::unique_ptr<simgrid::mc::State> initial_state =
+    std::unique_ptr<simgrid::mc::State>(MC_state_new());
 
   XBT_DEBUG("********* Start communication determinism verification *********");
 
@@ -385,9 +375,9 @@ void CommunicationDeterminismChecker::prepare()
   /* Get an enabled process and insert it in the interleave set of the initial state */
   for (auto& p : mc_model_checker->process().simix_processes())
     if (simgrid::mc::process_is_enabled(&p.copy))
-      MC_state_interleave_process(initial_state, &p.copy);
+      MC_state_interleave_process(initial_state.get(), &p.copy);
 
-  xbt_fifo_unshift(mc_stack, initial_state);
+  stack_.push_back(std::move(initial_state));
 }
 
 static inline
@@ -411,23 +401,21 @@ int CommunicationDeterminismChecker::main(void)
   int value;
   std::unique_ptr<simgrid::mc::VisitedState> visited_state = nullptr;
   smx_simcall_t req = nullptr;
-  simgrid::mc::State* state = nullptr;
-  simgrid::mc::State* next_state = nullptr;
 
-  while (xbt_fifo_size(mc_stack) > 0) {
+  while (!stack_.empty()) {
 
     /* Get current state */
-    state = (simgrid::mc::State*) xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
+    simgrid::mc::State* state = stack_.back().get();
 
     XBT_DEBUG("**************************************************");
-    XBT_DEBUG("Exploration depth = %d (state = %d, interleaved processes = %d)",
-              xbt_fifo_size(mc_stack), state->num,
+    XBT_DEBUG("Exploration depth = %zi (state = %d, interleaved processes = %d)",
+              stack_.size(), state->num,
               MC_state_interleave_size(state));
 
     /* Update statistics */
     mc_stats->visited_states++;
 
-    if ((xbt_fifo_size(mc_stack) <= _sg_mc_max_depth)
+    if (stack_.size() <= (std::size_t) _sg_mc_max_depth
         && (req = MC_state_get_request(state, &value))
         && (visited_state == nullptr)) {
 
@@ -458,7 +446,8 @@ int CommunicationDeterminismChecker::main(void)
       mc_model_checker->wait_for_requests();
 
       /* Create the new expanded state */
-      next_state = MC_state_new();
+      std::unique_ptr<simgrid::mc::State> next_state =
+        std::unique_ptr<simgrid::mc::State>(MC_state_new());
 
       /* If comm determinism verification, we cannot stop the exploration if
          some communications are not finished (at least, data are transfered).
@@ -467,12 +456,13 @@ int CommunicationDeterminismChecker::main(void)
       bool compare_snapshots = all_communications_are_finished()
         && initial_global_state->initial_communications_pattern_done;
 
-      if (_sg_mc_visited == 0 || (visited_state = simgrid::mc::is_visited_state(next_state, compare_snapshots)) == nullptr) {
+      if (_sg_mc_visited == 0
+          || (visited_state = visitedStates_.addVisitedState(next_state.get(), compare_snapshots)) == nullptr) {
 
         /* Get enabled processes and insert them in the interleave set of the next state */
         for (auto& p : mc_model_checker->process().simix_processes())
           if (simgrid::mc::process_is_enabled(&p.copy))
-            MC_state_interleave_process(next_state, &p.copy);
+            MC_state_interleave_process(next_state.get(), &p.copy);
 
         if (dot_output != nullptr)
           fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num,  next_state->num, req_str);
@@ -481,27 +471,28 @@ int CommunicationDeterminismChecker::main(void)
         fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
           state->num, visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str);
 
-      xbt_fifo_unshift(mc_stack, next_state);
+      stack_.push_back(std::move(next_state));
 
       if (dot_output != nullptr)
         xbt_free(req_str);
 
     } else {
 
-      if (xbt_fifo_size(mc_stack) > _sg_mc_max_depth)
+      if (stack_.size() > (std::size_t) _sg_mc_max_depth)
         XBT_WARN("/!\\ Max depth reached ! /!\\ ");
       else if (visited_state != nullptr)
         XBT_DEBUG("State already visited (equal to state %d), exploration stopped on this path.", visited_state->other_num == -1 ? visited_state->num : visited_state->other_num);
       else
-        XBT_DEBUG("There are no more processes to interleave. (depth %d)", xbt_fifo_size(mc_stack));
+        XBT_DEBUG("There are no more processes to interleave. (depth %zi)",
+          stack_.size());
 
       if (!initial_global_state->initial_communications_pattern_done)
         initial_global_state->initial_communications_pattern_done = 1;
 
       /* Trash the current state, no longer needed */
-      xbt_fifo_shift(mc_stack);
-      MC_state_delete(state, !state->in_visited_states ? 1 : 0);
-      XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
+      XBT_DEBUG("Delete state %d at depth %zi",
+        state->num, stack_.size());
+      stack_.pop_back();
 
       visited_state = nullptr;
 
@@ -511,22 +502,27 @@ int CommunicationDeterminismChecker::main(void)
         return SIMGRID_MC_EXIT_DEADLOCK;
       }
 
-      while ((state = (simgrid::mc::State*) xbt_fifo_shift(mc_stack)) != nullptr)
-        if (MC_state_interleave_size(state) && xbt_fifo_size(mc_stack) < _sg_mc_max_depth) {
+      while (!stack_.empty()) {
+        std::unique_ptr<simgrid::mc::State> state = std::move(stack_.back());
+        stack_.pop_back();
+        if (MC_state_interleave_size(state.get())
+            && stack_.size() < (std::size_t) _sg_mc_max_depth) {
           /* We found a back-tracking point, let's loop */
-          XBT_DEBUG("Back-tracking to state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
-          xbt_fifo_unshift(mc_stack, state);
+          XBT_DEBUG("Back-tracking to state %d at depth %zi",
+            state->num, stack_.size() + 1);
+          stack_.push_back(std::move(state));
 
-          MC_replay(mc_stack);
+          simgrid::mc::replay(stack_);
 
-          XBT_DEBUG("Back-tracking to state %d at depth %d done", state->num, xbt_fifo_size(mc_stack));
+          XBT_DEBUG("Back-tracking to state %d at depth %zi done",
+            stack_.back()->num, stack_.size());
 
           break;
         } else {
-          XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
-          MC_state_delete(state, !state->in_visited_states ? 1 : 0);
+          XBT_DEBUG("Delete state %d at depth %zi",
+            state->num, stack_.size() + 1);
         }
-
+      }
     }
   }
 
@@ -543,9 +539,6 @@ int CommunicationDeterminismChecker::run()
     // This will move somehwere else:
     simgrid::mc::Client::get()->handleMessages();
 
-  /* Create exploration stack */
-  mc_stack = xbt_fifo_new();
-
   this->prepare();
 
   initial_global_state = std::unique_ptr<s_mc_global_t>(new s_mc_global_t());
@@ -561,5 +554,10 @@ int CommunicationDeterminismChecker::run()
   return res;
 }
 
+Checker* createCommunicationDeterminismChecker(Session& session)
+{
+  return new CommunicationDeterminismChecker(session);
+}
+
 }
 }
\ No newline at end of file
diff --git a/src/mc/CommunicationDeterminismChecker.hpp b/src/mc/CommunicationDeterminismChecker.hpp
index e04657c56e..bd30d0435e 100644
--- a/src/mc/CommunicationDeterminismChecker.hpp
+++ b/src/mc/CommunicationDeterminismChecker.hpp
@@ -4,8 +4,14 @@
 /* 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. */
 
+#include <list>
+#include <memory>
+#include <string>
+#include <vector>
+
 #include "src/mc/mc_forward.hpp"
 #include "src/mc/Checker.hpp"
+#include "src/mc/VisitedState.hpp"
 
 #ifndef SIMGRID_MC_COMMUNICATION_DETERMINISM_CHECKER_HPP
 #define SIMGRID_MC_COMMUNICATION_DETERMINISM_CHECKER_HPP
@@ -13,7 +19,7 @@
 namespace simgrid {
 namespace mc {
 
-class CommunicationDeterminismChecker : public Checker {
+class XBT_PRIVATE CommunicationDeterminismChecker : public Checker {
 public:
   CommunicationDeterminismChecker(Session& session);
   ~CommunicationDeterminismChecker();
@@ -23,6 +29,10 @@ public:
 private:
   void prepare();
   int main();
+private:
+  /** Stack representing the position in the exploration graph */
+  std::list<std::unique_ptr<simgrid::mc::State>> stack_;
+  simgrid::mc::VisitedStates visitedStates_;
 };
 
 #endif
diff --git a/src/mc/LivenessChecker.cpp b/src/mc/LivenessChecker.cpp
index abf36efed1..e41d3f54fd 100644
--- a/src/mc/LivenessChecker.cpp
+++ b/src/mc/LivenessChecker.cpp
@@ -40,7 +40,8 @@ namespace mc {
 
 VisitedPair::VisitedPair(
   int pair_num, xbt_automaton_state_t automaton_state,
-  std::vector<int> const& atomic_propositions, std::shared_ptr<simgrid::mc::State> graph_state)
+  std::shared_ptr<const std::vector<int>> atomic_propositions,
+  std::shared_ptr<simgrid::mc::State> graph_state)
 {
   simgrid::mc::Process* process = &(mc_model_checker->process());
 
@@ -56,7 +57,7 @@ VisitedPair::VisitedPair(
   this->automaton_state = automaton_state;
   this->num = pair_num;
   this->other_num = -1;
-  this->atomic_propositions = atomic_propositions;
+  this->atomic_propositions = std::move(atomic_propositions);
 }
 
 VisitedPair::~VisitedPair()
@@ -96,14 +97,14 @@ Pair::Pair() : num(++mc_stats->expanded_pairs)
 
 Pair::~Pair() {}
 
-std::vector<int> LivenessChecker::getPropositionValues()
+std::shared_ptr<const std::vector<int>> LivenessChecker::getPropositionValues()
 {
   std::vector<int> values;
   unsigned int cursor = 0;
   xbt_automaton_propositional_symbol_t ps = nullptr;
   xbt_dynar_foreach(simgrid::mc::property_automaton->propositional_symbols, cursor, ps)
     values.push_back(xbt_automaton_propositional_symbol_evaluate(ps));
-  return values;
+  return std::make_shared<const std::vector<int>>(std::move(values));
 }
 
 int LivenessChecker::compare(simgrid::mc::VisitedPair* state1, simgrid::mc::VisitedPair* state2)
@@ -128,7 +129,7 @@ std::shared_ptr<VisitedPair> LivenessChecker::insertAcceptancePair(simgrid::mc::
     std::shared_ptr<simgrid::mc::VisitedPair> const& pair_test = *i;
     if (xbt_automaton_state_compare(
           pair_test->automaton_state, new_pair->automaton_state) != 0
-        || pair_test->atomic_propositions != new_pair->atomic_propositions
+        || *(pair_test->atomic_propositions) != *(new_pair->atomic_propositions)
         || this->compare(pair_test.get(), new_pair.get()) != 0)
       continue;
     XBT_INFO("Pair %d already reached (equal to pair %d) !",
@@ -160,13 +161,15 @@ void LivenessChecker::prepare(void)
   initial_global_state->snapshot = simgrid::mc::take_snapshot(0);
   initial_global_state->prev_pair = 0;
 
+  std::shared_ptr<const std::vector<int>> propos = this->getPropositionValues();
+
   // For each initial state of the property automaton, push a
   // (application_state, automaton_state) pair to the exploration stack:
   unsigned int cursor = 0;
   xbt_automaton_state_t automaton_state;
   xbt_dynar_foreach(simgrid::mc::property_automaton->states, cursor, automaton_state)
     if (automaton_state->type == -1)
-      explorationStack_.push_back(this->newPair(nullptr, automaton_state));
+      explorationStack_.push_back(this->newPair(nullptr, automaton_state, propos));
 }
 
 
@@ -251,7 +254,7 @@ int LivenessChecker::insertVisitedPair(std::shared_ptr<VisitedPair> visited_pair
     VisitedPair* pair_test = i->get();
     if (xbt_automaton_state_compare(
           pair_test->automaton_state, visited_pair->automaton_state) != 0
-        || pair_test->atomic_propositions != visited_pair->atomic_propositions
+        || *(pair_test->atomic_propositions) != *(visited_pair->atomic_propositions)
         || this->compare(pair_test, visited_pair.get()) != 0)
         continue;
     if (pair_test->other_num == -1)
@@ -411,16 +414,16 @@ int LivenessChecker::main(void)
     current_pair->exploration_started = true;
 
     /* Get values of atomic propositions (variables used in the property formula) */
-    std::vector<int> prop_values = this->getPropositionValues();
+    std::shared_ptr<const std::vector<int>> prop_values = this->getPropositionValues();
 
     // For each enabled transition in the property automaton, push a
     // (application_state, automaton_state) pair to the exploration stack:
     int cursor = xbt_dynar_length(current_pair->automaton_state->out) - 1;
     while (cursor >= 0) {
       xbt_automaton_transition_t transition_succ = (xbt_automaton_transition_t)xbt_dynar_get_as(current_pair->automaton_state->out, cursor, xbt_automaton_transition_t);
-      if (evaluate_label(transition_succ->label, prop_values))
+      if (evaluate_label(transition_succ->label, *prop_values))
           explorationStack_.push_back(this->newPair(
-            current_pair.get(), transition_succ->dst));
+            current_pair.get(), transition_succ->dst, prop_values));
        cursor--;
      }
 
@@ -431,12 +434,12 @@ int LivenessChecker::main(void)
   return SIMGRID_MC_EXIT_SUCCESS;
 }
 
-std::shared_ptr<Pair> LivenessChecker::newPair(Pair* current_pair, xbt_automaton_state_t state)
+std::shared_ptr<Pair> LivenessChecker::newPair(Pair* current_pair, xbt_automaton_state_t state, std::shared_ptr<const std::vector<int>> propositions)
 {
   std::shared_ptr<Pair> next_pair = std::make_shared<Pair>();
   next_pair->automaton_state = state;
   next_pair->graph_state = std::shared_ptr<simgrid::mc::State>(MC_state_new());
-  next_pair->atomic_propositions = this->getPropositionValues();
+  next_pair->atomic_propositions = std::move(propositions);
   if (current_pair)
     next_pair->depth = current_pair->depth + 1;
   else
diff --git a/src/mc/LivenessChecker.hpp b/src/mc/LivenessChecker.hpp
index f12c0b3be1..18c32a0372 100644
--- a/src/mc/LivenessChecker.hpp
+++ b/src/mc/LivenessChecker.hpp
@@ -34,7 +34,7 @@ struct XBT_PRIVATE Pair {
   bool search_cycle = false;
   std::shared_ptr<simgrid::mc::State> graph_state = nullptr; /* System state included */
   xbt_automaton_state_t automaton_state = nullptr;
-  std::vector<int> atomic_propositions;
+  std::shared_ptr<const std::vector<int>> atomic_propositions;
   int requests = 0;
   int depth = 0;
   bool exploration_started = false;
@@ -51,13 +51,13 @@ struct XBT_PRIVATE VisitedPair {
   int other_num = 0; /* Dot output for */
   std::shared_ptr<simgrid::mc::State> graph_state = nullptr; /* System state included */
   xbt_automaton_state_t automaton_state = nullptr;
-  std::vector<int> atomic_propositions;
+  std::shared_ptr<const std::vector<int>> atomic_propositions;
   std::size_t heap_bytes_used = 0;
   int nb_processes = 0;
 
   VisitedPair(
     int pair_num, xbt_automaton_state_t automaton_state,
-    std::vector<int> const& atomic_propositions,
+    std::shared_ptr<const std::vector<int>> atomic_propositions,
     std::shared_ptr<simgrid::mc::State> graph_state);
   ~VisitedPair();
 };
@@ -73,7 +73,7 @@ private:
   int main();
   void prepare();
   int compare(simgrid::mc::VisitedPair* state1, simgrid::mc::VisitedPair* state2);
-  std::vector<int> getPropositionValues();
+  std::shared_ptr<const std::vector<int>> getPropositionValues();
   std::shared_ptr<VisitedPair> insertAcceptancePair(simgrid::mc::Pair* pair);
   int insertVisitedPair(std::shared_ptr<VisitedPair> visited_pair, simgrid::mc::Pair* pair);
   void showAcceptanceCycle(std::size_t depth);
@@ -81,7 +81,7 @@ private:
   void removeAcceptancePair(int pair_num);
   void purgeVisitedPairs();
   void backtrack();
-  std::shared_ptr<Pair> newPair(Pair* pair, xbt_automaton_state_t state);
+  std::shared_ptr<Pair> newPair(Pair* pair, xbt_automaton_state_t state, std::shared_ptr<const std::vector<int>> propositions);
 public:
   // A stack of (application_state, automaton_state) pairs for DFS exploration:
   std::list<std::shared_ptr<Pair>> explorationStack_;
diff --git a/src/mc/SafetyChecker.cpp b/src/mc/SafetyChecker.cpp
index 9848af70fd..0a05e4a8e7 100644
--- a/src/mc/SafetyChecker.cpp
+++ b/src/mc/SafetyChecker.cpp
@@ -5,13 +5,11 @@
  * under the terms of the license (GNU LGPL) which comes with this package. */
 
 #include <cassert>
-
 #include <cstdio>
 
+#include <list>
+
 #include <xbt/log.h>
-#include <xbt/dynar.h>
-#include <xbt/dynar.hpp>
-#include <xbt/fifo.h>
 #include <xbt/sysdep.h>
 
 #include "src/mc/mc_state.h"
@@ -24,12 +22,12 @@
 #include "src/mc/mc_exit.h"
 #include "src/mc/Checker.hpp"
 #include "src/mc/SafetyChecker.hpp"
+#include "src/mc/VisitedState.hpp"
 
 #include "src/xbt/mmalloc/mmprivate.h"
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_safety, mc,
                                 "Logging specific to MC safety verification ");
-
 namespace simgrid {
 namespace mc {
 
@@ -53,48 +51,36 @@ static int snapshot_compare(simgrid::mc::State* state1, simgrid::mc::State* stat
   return snapshot_compare(num1, s1, num2, s2);
 }
 
-static int is_exploration_stack_state(simgrid::mc::State* current_state){
-
-  xbt_fifo_item_t item;
-  simgrid::mc::State* stack_state;
-  for(item = xbt_fifo_get_first_item(mc_stack); item != nullptr; item = xbt_fifo_get_next_item(item)) {
-    stack_state = (simgrid::mc::State*) xbt_fifo_get_item_content(item);
-    if(snapshot_compare(stack_state, current_state) == 0){
-      XBT_INFO("Non-progressive cycle : state %d -> state %d", stack_state->num, current_state->num);
-      return 1;
+bool SafetyChecker::checkNonDeterminism(simgrid::mc::State* current_state)
+{
+  for (auto i = stack_.rbegin(); i != stack_.rend(); ++i)
+    if (snapshot_compare(i->get(), current_state) == 0){
+      XBT_INFO("Non-progressive cycle : state %d -> state %d",
+        (*i)->num, current_state->num);
+      return true;
     }
-  }
-  return 0;
+  return false;
 }
 
 RecordTrace SafetyChecker::getRecordTrace() // override
 {
   RecordTrace res;
-
-  xbt_fifo_item_t start = xbt_fifo_get_last_item(mc_stack);
-  for (xbt_fifo_item_t item = start; item; item = xbt_fifo_get_prev_item(item)) {
-
-    // Find (pid, value):
-    simgrid::mc::State* state = (simgrid::mc::State*) xbt_fifo_get_item_content(item);
+  for (auto const& state : stack_) {
     int value = 0;
-    smx_simcall_t saved_req = MC_state_get_executed_request(state, &value);
+    smx_simcall_t saved_req = MC_state_get_executed_request(state.get(), &value);
     const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req);
     const int pid = issuer->pid;
-
     res.push_back(RecordTraceElement(pid, value));
   }
-
   return res;
 }
 
 std::vector<std::string> SafetyChecker::getTextualTrace() // override
 {
   std::vector<std::string> trace;
-  for (xbt_fifo_item_t item = xbt_fifo_get_last_item(mc_stack);
-       item; item = xbt_fifo_get_prev_item(item)) {
-    simgrid::mc::State* state = (simgrid::mc::State*)xbt_fifo_get_item_content(item);
+  for (auto const& state : stack_) {
     int value;
-    smx_simcall_t req = MC_state_get_executed_request(state, &value);
+    smx_simcall_t req = MC_state_get_executed_request(state.get(), &value);
     if (req) {
       char* req_str = simgrid::mc::request_to_string(
         req, value, simgrid::mc::RequestType::executed);
@@ -109,35 +95,30 @@ int SafetyChecker::run()
 {
   this->init();
 
-  char *req_str = nullptr;
   int value;
   smx_simcall_t req = nullptr;
-  simgrid::mc::State* state = nullptr;
-  simgrid::mc::State* prev_state = nullptr;
-  simgrid::mc::State* next_state = nullptr;
-  xbt_fifo_item_t item = nullptr;
   std::unique_ptr<simgrid::mc::VisitedState> visited_state = nullptr;
 
-  while (xbt_fifo_size(mc_stack) > 0) {
+  while (!stack_.empty()) {
 
     /* Get current state */
-    state = (simgrid::mc::State*)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
+    simgrid::mc::State* state = stack_.back().get();
 
     XBT_DEBUG("**************************************************");
-    XBT_DEBUG
-        ("Exploration depth=%d (state=%p, num %d)(%u interleave, user_max_depth %d)",
-         xbt_fifo_size(mc_stack), state, state->num,
-         MC_state_interleave_size(state), user_max_depth_reached);
+    XBT_DEBUG(
+      "Exploration depth=%zi (state=%p, num %d)(%u interleave, user_max_depth %d)",
+      stack_.size(), state, state->num,
+      MC_state_interleave_size(state), user_max_depth_reached);
 
     /* Update statistics */
     mc_stats->visited_states++;
 
     /* If there are processes to interleave and the maximum depth has not been reached
        then perform one step of the exploration algorithm */
-    if (xbt_fifo_size(mc_stack) <= _sg_mc_max_depth && !user_max_depth_reached
+    if (stack_.size() <= (std::size_t) _sg_mc_max_depth && !user_max_depth_reached
         && (req = MC_state_get_request(state, &value)) && visited_state == nullptr) {
 
-      req_str = simgrid::mc::request_to_string(req, value, simgrid::mc::RequestType::simix);
+      char* req_str = simgrid::mc::request_to_string(req, value, simgrid::mc::RequestType::simix);
       XBT_DEBUG("Execute: %s", req_str);
       xbt_free(req_str);
 
@@ -155,19 +136,21 @@ int SafetyChecker::run()
       mc_model_checker->wait_for_requests();
 
       /* Create the new expanded state */
-      next_state = MC_state_new();
+      std::unique_ptr<simgrid::mc::State> next_state =
+        std::unique_ptr<simgrid::mc::State>(MC_state_new());
 
-      if(_sg_mc_termination && is_exploration_stack_state(next_state)){
+      if (_sg_mc_termination && this->checkNonDeterminism(next_state.get())){
           MC_show_non_termination();
           return SIMGRID_MC_EXIT_NON_TERMINATION;
       }
 
-      if (_sg_mc_visited == 0 || (visited_state = simgrid::mc::is_visited_state(next_state, true)) == nullptr) {
+      if (_sg_mc_visited == 0
+          || (visited_state = visitedStates_.addVisitedState(next_state.get(), true)) == nullptr) {
 
         /* Get an enabled process and insert it in the interleave set of the next state */
         for (auto& p : mc_model_checker->process().simix_processes())
           if (simgrid::mc::process_is_enabled(&p.copy)) {
-            MC_state_interleave_process(next_state, &p.copy);
+            MC_state_interleave_process(next_state.get(), &p.copy);
             if (reductionMode_ != simgrid::mc::ReductionMode::none)
               break;
           }
@@ -178,8 +161,7 @@ int SafetyChecker::run()
       } else if (dot_output != nullptr)
         std::fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str);
 
-
-      xbt_fifo_unshift(mc_stack, next_state);
+      stack_.push_back(std::move(next_state));
 
       if (dot_output != nullptr)
         xbt_free(req_str);
@@ -189,7 +171,9 @@ int SafetyChecker::run()
       /* The interleave set is empty or the maximum depth is reached, let's back-track */
     } else {
 
-      if ((xbt_fifo_size(mc_stack) > _sg_mc_max_depth) || user_max_depth_reached || visited_state != nullptr) {
+      if (stack_.size() > (std::size_t) _sg_mc_max_depth
+          || user_max_depth_reached
+          || visited_state != nullptr) {
 
         if (user_max_depth_reached && visited_state == nullptr)
           XBT_DEBUG("User max depth reached !");
@@ -199,12 +183,12 @@ int SafetyChecker::run()
           XBT_DEBUG("State already visited (equal to state %d), exploration stopped on this path.", visited_state->other_num == -1 ? visited_state->num : visited_state->other_num);
 
       } else
-        XBT_DEBUG("There are no more processes to interleave. (depth %d)", xbt_fifo_size(mc_stack) + 1);
+        XBT_DEBUG("There are no more processes to interleave. (depth %zi)",
+          stack_.size() + 1);
 
       /* Trash the current state, no longer needed */
-      xbt_fifo_shift(mc_stack);
-      XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
-      MC_state_delete(state, !state->in_visited_states ? 1 : 0);
+      XBT_DEBUG("Delete state %d at depth %zi", state->num, stack_.size());
+      stack_.pop_back();
 
       visited_state = nullptr;
 
@@ -221,23 +205,26 @@ int SafetyChecker::run()
          executed before it. If it does then add it to the interleave set of the
          state that executed that previous request. */
 
-      while ((state = (simgrid::mc::State*) xbt_fifo_shift(mc_stack))) {
+      while (!stack_.empty()) {
+        std::unique_ptr<simgrid::mc::State> state = std::move(stack_.back());
+        stack_.pop_back();
         if (reductionMode_ == simgrid::mc::ReductionMode::dpor) {
-          req = MC_state_get_internal_request(state);
+          req = MC_state_get_internal_request(state.get());
           if (req->call == SIMCALL_MUTEX_LOCK || req->call == SIMCALL_MUTEX_TRYLOCK)
             xbt_die("Mutex is currently not supported with DPOR, "
               "use --cfg=model-check/reduction:none");
           const smx_process_t issuer = MC_smx_simcall_get_issuer(req);
-          xbt_fifo_foreach(mc_stack, item, prev_state, simgrid::mc::State*) {
+          for (auto i = stack_.rbegin(); i != stack_.rend(); ++i) {
+            simgrid::mc::State* prev_state = i->get();
             if (reductionMode_ != simgrid::mc::ReductionMode::none
                 && simgrid::mc::request_depend(req, MC_state_get_internal_request(prev_state))) {
               if (XBT_LOG_ISENABLED(mc_safety, xbt_log_priority_debug)) {
                 XBT_DEBUG("Dependent Transitions:");
                 smx_simcall_t prev_req = MC_state_get_executed_request(prev_state, &value);
-                req_str = simgrid::mc::request_to_string(prev_req, value, simgrid::mc::RequestType::internal);
+                char* req_str = simgrid::mc::request_to_string(prev_req, value, simgrid::mc::RequestType::internal);
                 XBT_DEBUG("%s (state=%d)", req_str, prev_state->num);
                 xbt_free(req_str);
-                prev_req = MC_state_get_executed_request(state, &value);
+                prev_req = MC_state_get_executed_request(state.get(), &value);
                 req_str = simgrid::mc::request_to_string(prev_req, value, simgrid::mc::RequestType::executed);
                 XBT_DEBUG("%s (state=%d)", req_str, state->num);
                 xbt_free(req_str);
@@ -268,16 +255,19 @@ int SafetyChecker::run()
           }
         }
 
-        if (MC_state_interleave_size(state) && xbt_fifo_size(mc_stack) < _sg_mc_max_depth) {
+        if (MC_state_interleave_size(state.get())
+            && stack_.size() < (std::size_t) _sg_mc_max_depth) {
           /* We found a back-tracking point, let's loop */
-          XBT_DEBUG("Back-tracking to state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
-          xbt_fifo_unshift(mc_stack, state);
-          MC_replay(mc_stack);
-          XBT_DEBUG("Back-tracking to state %d at depth %d done", state->num, xbt_fifo_size(mc_stack));
+          XBT_DEBUG("Back-tracking to state %d at depth %zi",
+            state->num, stack_.size() + 1);
+          stack_.push_back(std::move(state));
+          simgrid::mc::replay(stack_);
+          XBT_DEBUG("Back-tracking to state %d at depth %zi done",
+            stack_.back()->num, stack_.size());
           break;
         } else {
-          XBT_DEBUG("Delete state %d at depth %d", state->num, xbt_fifo_size(mc_stack) + 1);
-          MC_state_delete(state, !state->in_visited_states ? 1 : 0);
+          XBT_DEBUG("Delete state %d at depth %zi",
+            state->num, stack_.size() + 1);
         }
       }
     }
@@ -305,12 +295,8 @@ void SafetyChecker::init()
 
   XBT_DEBUG("Starting the safety algorithm");
 
-  /* Create exploration stack */
-  mc_stack = xbt_fifo_new();
-
-  simgrid::mc::visited_states.clear();
-
-  simgrid::mc::State* initial_state = MC_state_new();
+  std::unique_ptr<simgrid::mc::State> initial_state =
+    std::unique_ptr<simgrid::mc::State>(MC_state_new());
 
   XBT_DEBUG("**************************************************");
   XBT_DEBUG("Initial state");
@@ -321,12 +307,12 @@ void SafetyChecker::init()
   /* Get an enabled process and insert it in the interleave set of the initial state */
   for (auto& p : mc_model_checker->process().simix_processes())
     if (simgrid::mc::process_is_enabled(&p.copy)) {
-      MC_state_interleave_process(initial_state, &p.copy);
+      MC_state_interleave_process(initial_state.get(), &p.copy);
       if (reductionMode_ != simgrid::mc::ReductionMode::none)
         break;
     }
 
-  xbt_fifo_unshift(mc_stack, initial_state);
+  stack_.push_back(std::move(initial_state));
 
   /* Save the initial state */
   initial_global_state = std::unique_ptr<s_mc_global_t>(new s_mc_global_t());
@@ -340,6 +326,11 @@ SafetyChecker::SafetyChecker(Session& session) : Checker(session)
 SafetyChecker::~SafetyChecker()
 {
 }
+
+Checker* createSafetyChecker(Session& session)
+{
+  return new SafetyChecker(session);
+}
   
 }
 }
diff --git a/src/mc/SafetyChecker.hpp b/src/mc/SafetyChecker.hpp
index 48edb7b23e..9694a93d3a 100644
--- a/src/mc/SafetyChecker.hpp
+++ b/src/mc/SafetyChecker.hpp
@@ -7,13 +7,19 @@
 #ifndef SIMGRID_MC_SAFETY_CHECKER_HPP
 #define SIMGRID_MC_SAFETY_CHECKER_HPP
 
+#include <list>
+#include <memory>
+#include <string>
+#include <vector>
+
 #include "src/mc/mc_forward.hpp"
 #include "src/mc/Checker.hpp"
+#include "src/mc/VisitedState.hpp"
 
 namespace simgrid {
 namespace mc {
 
-class SafetyChecker : public Checker {
+class XBT_PRIVATE SafetyChecker : public Checker {
   simgrid::mc::ReductionMode reductionMode_ = simgrid::mc::ReductionMode::unset;
 public:
   SafetyChecker(Session& session);
@@ -24,6 +30,11 @@ public:
 private:
   // Temp
   void init();
+  bool checkNonDeterminism(simgrid::mc::State* current_state);
+private:
+  /** Stack representing the position in the exploration graph */
+  std::list<std::unique_ptr<simgrid::mc::State>> stack_;
+  simgrid::mc::VisitedStates visitedStates_;
 };
 
 }
diff --git a/src/mc/mc_visited.cpp b/src/mc/VisitedState.cpp
similarity index 55%
rename from src/mc/mc_visited.cpp
rename to src/mc/VisitedState.cpp
index fbdd510678..4399f82493 100644
--- a/src/mc/mc_visited.cpp
+++ b/src/mc/VisitedState.cpp
@@ -10,7 +10,6 @@
 #include <memory>
 #include <algorithm>
 
-#include <xbt/automaton.h>
 #include <xbt/log.h>
 #include <xbt/sysdep.h>
 #include <xbt/dynar.h>
@@ -22,14 +21,22 @@
 #include "src/mc/mc_private.h"
 #include "src/mc/Process.hpp"
 #include "src/mc/mc_smx.h"
+#include "src/mc/VisitedState.hpp"
 
-XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_visited, mc,
+XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_VisitedState, mc,
                                 "Logging specific to state equaity detection mechanisms");
 
 namespace simgrid {
 namespace mc {
 
-std::vector<std::unique_ptr<simgrid::mc::VisitedState>> visited_states;
+static int snapshot_compare(simgrid::mc::VisitedState* state1, simgrid::mc::VisitedState* state2)
+{
+  simgrid::mc::Snapshot* s1 = state1->system_state.get();
+  simgrid::mc::Snapshot* s2 = state2->system_state.get();
+  int num1 = state1->num;
+  int num2 = state2->num;
+  return snapshot_compare(num1, s1, num2, s2);
+}
 
 /**
  * \brief Save the current state
@@ -54,37 +61,26 @@ VisitedState::~VisitedState()
 {
 }
 
-static void prune_visited_states()
+void VisitedStates::prune()
 {
-  while (visited_states.size() > (std::size_t) _sg_mc_visited) {
+  while (states_.size() > (std::size_t) _sg_mc_visited) {
     XBT_DEBUG("Try to remove visited state (maximum number of stored states reached)");
-    auto min_element = std::min_element(visited_states.begin(), visited_states.end(),
+    auto min_element = std::min_element(states_.begin(), states_.end(),
       [](std::unique_ptr<simgrid::mc::VisitedState>& a, std::unique_ptr<simgrid::mc::VisitedState>& b) {
         return a->num < b->num;
       });
-    xbt_assert(min_element != visited_states.end());
+    xbt_assert(min_element != states_.end());
     // and drop it:
-    visited_states.erase(min_element);
+    states_.erase(min_element);
     XBT_DEBUG("Remove visited state (maximum number of stored states reached)");
   }
 }
 
-static int snapshot_compare(simgrid::mc::VisitedState* state1, simgrid::mc::VisitedState* state2)
-{
-  simgrid::mc::Snapshot* s1 = state1->system_state.get();
-  simgrid::mc::Snapshot* s2 = state2->system_state.get();
-  int num1 = state1->num;
-  int num2 = state2->num;
-  return snapshot_compare(num1, s1, num2, s2);
-}
-
 /**
  * \brief Checks whether a given state has already been visited by the algorithm.
  */
-std::unique_ptr<simgrid::mc::VisitedState> is_visited_state(simgrid::mc::State* graph_state, bool compare_snpashots)
+std::unique_ptr<simgrid::mc::VisitedState> VisitedStates::addVisitedState(simgrid::mc::State* graph_state, bool compare_snpashots)
 {
-
-
   std::unique_ptr<simgrid::mc::VisitedState> new_state =
     std::unique_ptr<simgrid::mc::VisitedState>(new VisitedState());
   graph_state->system_state = new_state->system_state;
@@ -92,47 +88,45 @@ std::unique_ptr<simgrid::mc::VisitedState> is_visited_state(simgrid::mc::State*
   XBT_DEBUG("Snapshot %p of visited state %d (exploration stack state %d)",
     new_state->system_state.get(), new_state->num, graph_state->num);
 
-  auto range = std::equal_range(visited_states.begin(), visited_states.end(),
+  auto range = std::equal_range(states_.begin(), states_.end(),
     new_state.get(), simgrid::mc::DerefAndCompareByNbProcessesAndUsedHeap());
 
-      if (compare_snpashots) {
-
-        for (auto i = range.first; i != range.second; ++i) {
-          auto& visited_state = *i;
-          if (snapshot_compare(visited_state.get(), new_state.get()) == 0) {
-            // The state has been visited:
-
-            std::unique_ptr<simgrid::mc::VisitedState> old_state =
-              std::move(visited_state);
-
-            if (old_state->other_num == -1)
-              new_state->other_num = old_state->num;
-            else
-              new_state->other_num = old_state->other_num;
-
-            if (dot_output == nullptr)
-              XBT_DEBUG("State %d already visited ! (equal to state %d)",
-                new_state->num, old_state->num);
-            else
-              XBT_DEBUG(
-                "State %d already visited ! (equal to state %d (state %d in dot_output))",
-                new_state->num, old_state->num, new_state->other_num);
-
-            /* Replace the old state with the new one (with a bigger num)
-               (when the max number of visited states is reached,  the oldest
-               one is removed according to its number (= with the min number) */
-            XBT_DEBUG("Replace visited state %d with the new visited state %d",
-              old_state->num, new_state->num);
-
-            visited_state = std::move(new_state);
-            return std::move(old_state);
-          }
-        }
+  if (compare_snpashots)
+    for (auto i = range.first; i != range.second; ++i) {
+      auto& visited_state = *i;
+      if (snapshot_compare(visited_state.get(), new_state.get()) == 0) {
+        // The state has been visited:
+
+        std::unique_ptr<simgrid::mc::VisitedState> old_state =
+          std::move(visited_state);
+
+        if (old_state->other_num == -1)
+          new_state->other_num = old_state->num;
+        else
+          new_state->other_num = old_state->other_num;
+
+        if (dot_output == nullptr)
+          XBT_DEBUG("State %d already visited ! (equal to state %d)",
+            new_state->num, old_state->num);
+        else
+          XBT_DEBUG(
+            "State %d already visited ! (equal to state %d (state %d in dot_output))",
+            new_state->num, old_state->num, new_state->other_num);
+
+        /* Replace the old state with the new one (with a bigger num)
+           (when the max number of visited states is reached,  the oldest
+           one is removed according to its number (= with the min number) */
+        XBT_DEBUG("Replace visited state %d with the new visited state %d",
+          old_state->num, new_state->num);
+
+        visited_state = std::move(new_state);
+        return std::move(old_state);
       }
+    }
 
-  XBT_DEBUG("Insert new visited state %d (total : %lu)", new_state->num, (unsigned long) visited_states.size());
-  visited_states.insert(range.first, std::move(new_state));
-  prune_visited_states();
+  XBT_DEBUG("Insert new visited state %d (total : %lu)", new_state->num, (unsigned long) states_.size());
+  states_.insert(range.first, std::move(new_state));
+  this->prune();
   return nullptr;
 }
 
diff --git a/src/mc/VisitedState.hpp b/src/mc/VisitedState.hpp
new file mode 100644
index 0000000000..364c8bfa52
--- /dev/null
+++ b/src/mc/VisitedState.hpp
@@ -0,0 +1,42 @@
+/* Copyright (c) 2007-2016. 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. */
+
+#ifndef SIMGRID_MC_VISITED_STATE_HPP
+#define SIMGRID_MC_VISITED_STATE_HPP
+
+#include <cstddef>
+
+#include <memory>
+
+#include "src/mc/mc_snapshot.h"
+
+namespace simgrid {
+namespace mc {
+
+struct XBT_PRIVATE VisitedState {
+  std::shared_ptr<simgrid::mc::Snapshot> system_state = nullptr;
+  std::size_t heap_bytes_used = 0;
+  int nb_processes = 0;
+  int num = 0;
+  int other_num = 0; // dot_output for
+
+  VisitedState();
+  ~VisitedState();
+};
+
+class XBT_PRIVATE VisitedStates {
+  std::vector<std::unique_ptr<simgrid::mc::VisitedState>> states_;
+public:
+  void clear() { states_.clear(); }
+  std::unique_ptr<simgrid::mc::VisitedState> addVisitedState(simgrid::mc::State* graph_state, bool compare_snpashots);
+private:
+  void prune();
+};
+
+}
+}
+
+#endif
diff --git a/src/mc/mc_global.cpp b/src/mc/mc_global.cpp
index 6e9b7b6683..cf23f62827 100644
--- a/src/mc/mc_global.cpp
+++ b/src/mc/mc_global.cpp
@@ -61,7 +61,6 @@ simgrid::mc::State* mc_current_state = nullptr;
 char mc_replay_mode = false;
 
 mc_stats_t mc_stats = nullptr;
-xbt_fifo_t mc_stack = nullptr;
 
 /* Liveness */
 
@@ -110,27 +109,23 @@ void MC_run()
   simgrid::mc::processes_time.clear();
 }
 
+namespace simgrid {
+namespace mc {
+
 /**
  * \brief Re-executes from the state at position start all the transitions indicated by
  *        a given model-checker stack.
  * \param stack The stack with the transitions to execute.
  * \param start Start index to begin the re-execution.
  */
-void MC_replay(xbt_fifo_t stack)
+void replay(std::list<std::unique_ptr<simgrid::mc::State>> const& stack)
 {
-  int value, count = 1;
-  char *req_str;
-  smx_simcall_t req = nullptr, saved_req = NULL;
-  xbt_fifo_item_t item, start_item;
-  simgrid::mc::State* state;
-  
   XBT_DEBUG("**** Begin Replay ****");
 
   /* Intermediate backtracking */
   if(_sg_mc_checkpoint > 0 || _sg_mc_termination || _sg_mc_visited > 0) {
-    start_item = xbt_fifo_get_first_item(stack);
-    state = (simgrid::mc::State*)xbt_fifo_get_item_content(start_item);
-    if(state->system_state){
+    simgrid::mc::State* state = stack.back().get();
+    if (state->system_state) {
       simgrid::mc::restore_snapshot(state->system_state);
       if(_sg_mc_comms_determinism || _sg_mc_send_determinism) 
         MC_restore_communications_pattern(state);
@@ -144,8 +139,6 @@ void MC_replay(xbt_fifo_t stack)
   /* At the moment of taking the snapshot the raw heap was set, so restoring
    * it will set it back again, we have to unset it to continue  */
 
-  start_item = xbt_fifo_get_last_item(stack);
-
   if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
     // int n = xbt_dynar_length(incomplete_communications_pattern);
     unsigned n = MC_smx_get_maxpid();
@@ -157,25 +150,27 @@ void MC_replay(xbt_fifo_t stack)
     }
   }
 
+  int count = 1;
+
   /* Traverse the stack from the state at position start and re-execute the transitions */
-  for (item = start_item;
-       item != xbt_fifo_get_first_item(stack);
-       item = xbt_fifo_get_prev_item(item)) {
+  for (std::unique_ptr<simgrid::mc::State> const& state : stack) {
+    if (state == stack.back())
+      break;
 
-    state = (simgrid::mc::State*) xbt_fifo_get_item_content(item);
-    saved_req = MC_state_get_executed_request(state, &value);
+    int value;
+    smx_simcall_t saved_req = MC_state_get_executed_request(state.get(), &value);
     
     if (saved_req) {
       /* because we got a copy of the executed request, we have to fetch the  
          real one, pointed by the request field of the issuer process */
 
       const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req);
-      req = &issuer->simcall;
+      smx_simcall_t req = &issuer->simcall;
 
       /* Debug information */
       if (XBT_LOG_ISENABLED(mc_global, xbt_log_priority_debug)) {
-        req_str = simgrid::mc::request_to_string(req, value, simgrid::mc::RequestType::simix);
-        XBT_DEBUG("Replay: %s (%p)", req_str, state);
+        char* req_str = simgrid::mc::request_to_string(req, value, simgrid::mc::RequestType::simix);
+        XBT_DEBUG("Replay: %s (%p)", req_str, state.get());
         xbt_free(req_str);
       }
 
@@ -203,6 +198,9 @@ void MC_replay(xbt_fifo_t stack)
   XBT_DEBUG("**** End Replay ****");
 }
 
+}
+}
+
 void MC_show_deadlock(void)
 {
   XBT_INFO("**************************");
diff --git a/src/mc/mc_private.h b/src/mc/mc_private.h
index 28c1533afb..064926f0a8 100644
--- a/src/mc/mc_private.h
+++ b/src/mc/mc_private.h
@@ -22,6 +22,7 @@
 #include <xbt/fifo.h>
 #include <xbt/config.h>
 #include <xbt/base.h>
+#include <xbt/automaton.h>
 
 #include "mc/mc.h"
 #include "mc/datatypes.h"
@@ -64,16 +65,8 @@ XBT_PRIVATE extern FILE *dot_output;
 
 XBT_PRIVATE extern int user_max_depth_reached;
 
-XBT_PRIVATE void MC_replay(xbt_fifo_t stack);
 XBT_PRIVATE void MC_show_deadlock(void);
 
-/** Stack (of `simgrid::mc::State*`) representing the current position of the
- *  the MC in the exploration graph
- *
- *  It is managed by its head (`xbt_fifo_shift` and `xbt_fifo_unshift`).
- */
-XBT_PRIVATE extern xbt_fifo_t mc_stack;
-
 /****************************** Statistics ************************************/
 
 typedef struct mc_stats {
diff --git a/src/mc/mc_safety.h b/src/mc/mc_safety.h
index 60c177f1f9..b1cd987846 100644
--- a/src/mc/mc_safety.h
+++ b/src/mc/mc_safety.h
@@ -31,20 +31,6 @@ enum class ReductionMode {
 
 extern XBT_PRIVATE simgrid::mc::ReductionMode reduction_mode;
 
-struct XBT_PRIVATE VisitedState {
-  std::shared_ptr<simgrid::mc::Snapshot> system_state = nullptr;
-  size_t heap_bytes_used = 0;
-  int nb_processes = 0;
-  int num = 0;
-  int other_num = 0; // dot_output for
-
-  VisitedState();
-  ~VisitedState();
-};
-
-extern XBT_PRIVATE std::vector<std::unique_ptr<simgrid::mc::VisitedState>> visited_states;
-XBT_PRIVATE std::unique_ptr<simgrid::mc::VisitedState> is_visited_state(simgrid::mc::State* graph_state, bool compare_snpashots);
-
 }
 }
 
diff --git a/src/mc/mc_state.h b/src/mc/mc_state.h
index 8fcbde486b..94c72013d6 100644
--- a/src/mc/mc_state.h
+++ b/src/mc/mc_state.h
@@ -7,6 +7,7 @@
 #ifndef SIMGRID_MC_STATE_H
 #define SIMGRID_MC_STATE_H
 
+#include <list>
 #include <memory>
 
 #include <xbt/base.h>
@@ -61,6 +62,8 @@ struct XBT_PRIVATE State {
   ~State();
 };
 
+XBT_PRIVATE void replay(std::list<std::unique_ptr<simgrid::mc::State>> const& stack);
+
 }
 }
 
diff --git a/src/mc/simgrid_mc.cpp b/src/mc/simgrid_mc.cpp
index 984ca974c6..9f85d7a164 100644
--- a/src/mc/simgrid_mc.cpp
+++ b/src/mc/simgrid_mc.cpp
@@ -27,8 +27,6 @@
 #include "src/mc/mc_exit.h"
 #include "src/mc/Session.hpp"
 #include "src/mc/Checker.hpp"
-#include "src/mc/CommunicationDeterminismChecker.hpp"
-#include "src/mc/SafetyChecker.hpp"
 
 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_main, mc, "Entry point for simgrid-mc");
 
@@ -46,10 +44,10 @@ std::unique_ptr<simgrid::mc::Checker> createChecker(simgrid::mc::Session& sessio
 {
   if (_sg_mc_comms_determinism || _sg_mc_send_determinism)
     return std::unique_ptr<simgrid::mc::Checker>(
-      new simgrid::mc::CommunicationDeterminismChecker(session));
+      simgrid::mc::createCommunicationDeterminismChecker(session));
   else if (!_sg_mc_property_file || _sg_mc_property_file[0] == '\0')
     return std::unique_ptr<simgrid::mc::Checker>(
-      new simgrid::mc::SafetyChecker(session));
+      simgrid::mc::createSafetyChecker(session));
   else
     return std::unique_ptr<simgrid::mc::Checker>(
       simgrid::mc::createLivenessChecker(session));
diff --git a/src/xbt/log.c b/src/xbt/log.c
index ae4b051d65..f76b348a16 100644
--- a/src/xbt/log.c
+++ b/src/xbt/log.c
@@ -629,7 +629,7 @@ static void xbt_log_connect_categories(void)
   XBT_LOG_CONNECT(mc_page_snapshot);
   XBT_LOG_CONNECT(mc_request);
   XBT_LOG_CONNECT(mc_safety);
-  XBT_LOG_CONNECT(mc_visited);
+  XBT_LOG_CONNECT(mc_VisitedState);
   XBT_LOG_CONNECT(mc_client);
   XBT_LOG_CONNECT(mc_client_api);
   XBT_LOG_CONNECT(mc_comm_pattern);
diff --git a/teshsuite/simdag/basic-parsing-test/basic-parsing-test-bypass.tesh b/teshsuite/simdag/basic-parsing-test/basic-parsing-test-bypass.tesh
index 59a164e371..2ae691c1b6 100644
--- a/teshsuite/simdag/basic-parsing-test/basic-parsing-test-bypass.tesh
+++ b/teshsuite/simdag/basic-parsing-test/basic-parsing-test-bypass.tesh
@@ -61,7 +61,7 @@ $ ${bindir:=.}/basic-parsing-test ${srcdir:=.}/examples/platforms/bypassASroute.
 >   Route latency = 0.000100, route bandwidth = 125000000.000000
 
 p Testing a bypass route
-
+! output sort
 $ ${bindir:=.}/basic-parsing-test ${srcdir:=.}/examples/platforms/bypassRoute.xml FULL_LINK
 > [0.000000] [xbt_cfg/INFO] Switching to the L07 model to handle parallel tasks.
 > Workstation number: 4, link number: 10
@@ -153,4 +153,4 @@ $ ${bindir:=.}/basic-parsing-test ${srcdir:=.}/examples/platforms/bypassRoute.xm
 > Route between AS_1_host1 and AS_1_host1
 >   Route size 1
 >   Link __loopback__: latency = 0.000015, bandwidth = 498000000.000000
->   Route latency = 0.000015, route bandwidth = 498000000.000000
\ No newline at end of file
+>   Route latency = 0.000015, route bandwidth = 498000000.000000
diff --git a/teshsuite/simdag/basic-parsing-test/basic-parsing-test-sym-full.tesh b/teshsuite/simdag/basic-parsing-test/basic-parsing-test-sym-full.tesh
index f243b280ea..dffd43cf58 100644
--- a/teshsuite/simdag/basic-parsing-test/basic-parsing-test-sym-full.tesh
+++ b/teshsuite/simdag/basic-parsing-test/basic-parsing-test-sym-full.tesh
@@ -155,6 +155,7 @@ $ ${bindir:=.}/basic-parsing-test ../platforms/one_cluster_fullduplex.xml FULL_L
 >   Link bob_cluster_link_6_DOWN: latency = 0.000050, bandwidth = 125000000.000000
 >   Route latency = 0.000600, route bandwidth = 125000000.000000
 
+! output sort
 $ ${bindir:=.}/basic-parsing-test ../platforms/two_clusters.xml FULL_LINK "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n"
 > [  0.000000] (0:maestro@) Switching to the L07 model to handle parallel tasks.
 > Workstation number: 4, link number: 12
@@ -271,6 +272,7 @@ $ ${bindir:=.}/basic-parsing-test ../platforms/two_clusters.xml FULL_LINK "--log
 >   Link alice_cluster_link_1_DOWN: latency = 0.000050, bandwidth = 125000000.000000
 >   Route latency = 0.000600, route bandwidth = 125000000.000000
 
+! output sort
 $ ${bindir:=.}/basic-parsing-test ../platforms/two_hosts_one_link.xml FULL_LINK "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n"
 > [  0.000000] (0:maestro@) Switching to the L07 model to handle parallel tasks.
 > Workstation number: 2, link number: 2
@@ -291,6 +293,7 @@ $ ${bindir:=.}/basic-parsing-test ../platforms/two_hosts_one_link.xml FULL_LINK
 >   Link __loopback__: latency = 0.000015, bandwidth = 498000000.000000
 >   Route latency = 0.000015, route bandwidth = 498000000.000000
 
+! output sort
 $ ${bindir:=.}/basic-parsing-test ../platforms/two_hosts_one_link_fullduplex.xml FULL_LINK "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n"
 > [  0.000000] (0:maestro@) Switching to the L07 model to handle parallel tasks.
 > Workstation number: 2, link number: 3
@@ -311,6 +314,7 @@ $ ${bindir:=.}/basic-parsing-test ../platforms/two_hosts_one_link_fullduplex.xml
 >   Link __loopback__: latency = 0.000015, bandwidth = 498000000.000000
 >   Route latency = 0.000015, route bandwidth = 498000000.000000
 
+! output sort
 $ ${bindir:=.}/basic-parsing-test ../platforms/Dijkstra.xml FULL_LINK "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n"
 > [  0.000000] (0:maestro@) Switching to the L07 model to handle parallel tasks.
 > Workstation number: 2, link number: 6
@@ -333,6 +337,7 @@ $ ${bindir:=.}/basic-parsing-test ../platforms/Dijkstra.xml FULL_LINK "--log=roo
 >   Link __loopback__: latency = 0.000015, bandwidth = 498000000.000000
 >   Route latency = 0.000015, route bandwidth = 498000000.000000
 
+! output sort
 $ ${bindir:=.}/basic-parsing-test ../platforms/four_hosts_floyd.xml FULL_LINK
 > [0.000000] [xbt_cfg/INFO] Switching to the L07 model to handle parallel tasks.
 > Workstation number: 4, link number: 5
diff --git a/teshsuite/simdag/basic-parsing-test/basic-parsing-test.tesh b/teshsuite/simdag/basic-parsing-test/basic-parsing-test.tesh
index 9f02fe29ff..ee27b68deb 100644
--- a/teshsuite/simdag/basic-parsing-test/basic-parsing-test.tesh
+++ b/teshsuite/simdag/basic-parsing-test/basic-parsing-test.tesh
@@ -4,30 +4,37 @@ $ ${bindir:=.}/basic-parsing-test ../platforms/one_cluster.xml "--log=root.fmt:[
 > [  0.000000] (0:maestro@) Switching to the L07 model to handle parallel tasks.
 > Workstation number: 5, link number: 12
 
+! output sort
 $ ${bindir:=.}/basic-parsing-test ../platforms/host_attributes.xml "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n"
 > [  0.000000] (0:maestro@) Switching to the L07 model to handle parallel tasks.
 > Workstation number: 5, link number: 1
 
+! output sort
 $ ${bindir:=.}/basic-parsing-test ../platforms/link_attributes.xml "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n"
 > [  0.000000] (0:maestro@) Switching to the L07 model to handle parallel tasks.
 > Workstation number: 1, link number: 5
 
+! output sort
 $ ${bindir:=.}/basic-parsing-test ../platforms/three_hosts_non_symmetric_route.xml "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n"
 > [  0.000000] (0:maestro@) Switching to the L07 model to handle parallel tasks.
 > Workstation number: 3, link number: 4
 
+! output sort
 $ ${bindir:=.}/basic-parsing-test ../platforms/two_clusters.xml "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n"
 > [  0.000000] (0:maestro@) Switching to the L07 model to handle parallel tasks.
 > Workstation number: 4, link number: 12
 
+! output sort
 $ ${bindir:=.}/basic-parsing-test ../platforms/two_hosts_multi_hop.xml "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n"
 > [  0.000000] (0:maestro@) Switching to the L07 model to handle parallel tasks.
 > Workstation number: 2, link number: 4
 
+! output sort
 $ ${bindir:=.}/basic-parsing-test ../platforms/two_hosts_one_link.xml "--log=root.fmt:[%10.6r]%e(%i:%P@%h)%e%m%n"
 > [  0.000000] (0:maestro@) Switching to the L07 model to handle parallel tasks.
 > Workstation number: 2, link number: 2
 
+! output sort
 $ ${bindir:=.}/basic-parsing-test ../platforms/four_hosts_floyd.xml
 > [0.000000] [xbt_cfg/INFO] Switching to the L07 model to handle parallel tasks.
 > Workstation number: 4, link number: 5
diff --git a/teshsuite/simdag/flatifier/flatifier.tesh b/teshsuite/simdag/flatifier/flatifier.tesh
index 656bd27e1b..0f78b05046 100644
--- a/teshsuite/simdag/flatifier/flatifier.tesh
+++ b/teshsuite/simdag/flatifier/flatifier.tesh
@@ -1,5 +1,5 @@
 #! ./tesh
-
+! output sort
 $ ${bindir:=.}/flatifier$EXEEXT ../platforms/one_cluster.xml "--log=root.fmt:[%10.6r]%e[%i:%P@%h]%e%m%n"
 > [  0.000000] [0:maestro@] Switching to the L07 model to handle parallel tasks.
 > <?xml version='1.0'?>
@@ -135,6 +135,7 @@ $ ${bindir:=.}/flatifier$EXEEXT ../platforms/one_cluster.xml "--log=root.fmt:[%1
 > </AS>
 > </platform>
 
+! output sort
 $ ${bindir:=.}/flatifier$EXEEXT ../platforms/one_cluster_multicore.xml "--log=root.fmt:[%10.6r]%e[%i:%P@%h]%e%m%n"
 > [  0.000000] [0:maestro@] Switching to the L07 model to handle parallel tasks.
 > <?xml version='1.0'?>
@@ -269,6 +270,7 @@ $ ${bindir:=.}/flatifier$EXEEXT ../platforms/one_cluster_multicore.xml "--log=ro
 > </AS>
 > </platform>
 
+! output sort
 $ ${bindir:=.}/flatifier$EXEEXT ../platforms/host_attributes.xml "--log=root.fmt:[%10.6r]%e[%i:%P@%h]%e%m%n"
 > [  0.000000] [0:maestro@] Switching to the L07 model to handle parallel tasks.
 > <?xml version='1.0'?>
@@ -303,6 +305,7 @@ $ ${bindir:=.}/flatifier$EXEEXT ../platforms/host_attributes.xml "--log=root.fmt
 > </AS>
 > </platform>
 
+! output sort
 $ ${bindir:=.}/flatifier$EXEEXT ../platforms/link_attributes.xml "--log=root.fmt:[%10.6r]%e[%i:%P@%h]%e%m%n"
 > [  0.000000] [0:maestro@] Switching to the L07 model to handle parallel tasks.
 > <?xml version='1.0'?>
@@ -321,6 +324,7 @@ $ ${bindir:=.}/flatifier$EXEEXT ../platforms/link_attributes.xml "--log=root.fmt
 > </AS>
 > </platform>
 
+! output sort
 $ ${bindir:=.}/flatifier$EXEEXT ../platforms/three_hosts_non_symmetric_route.xml "--log=root.fmt:[%10.6r]%e[%i:%P@%h]%e%m%n"
 > [  0.000000] [0:maestro@] Switching to the L07 model to handle parallel tasks.
 > <?xml version='1.0'?>
@@ -364,6 +368,7 @@ $ ${bindir:=.}/flatifier$EXEEXT ../platforms/three_hosts_non_symmetric_route.xml
 > </AS>
 > </platform>
 
+! output sort
 $ ${bindir:=.}/flatifier$EXEEXT ../platforms/two_clusters.xml "--log=root.fmt:[%10.6r]%e[%i:%P@%h]%e%m%n"
 > [  0.000000] [0:maestro@] Switching to the L07 model to handle parallel tasks.
 > <?xml version='1.0'?>
@@ -499,6 +504,7 @@ $ ${bindir:=.}/flatifier$EXEEXT ../platforms/two_clusters.xml "--log=root.fmt:[%
 > </AS>
 > </platform>
 
+! output sort
 $ ${bindir:=.}/flatifier$EXEEXT ../platforms/two_hosts_multi_hop.xml "--log=root.fmt:[%10.6r]%e[%i:%P@%h]%e%m%n"
 > [  0.000000] [0:maestro@] Switching to the L07 model to handle parallel tasks.
 > <?xml version='1.0'?>
@@ -526,6 +532,7 @@ $ ${bindir:=.}/flatifier$EXEEXT ../platforms/two_hosts_multi_hop.xml "--log=root
 > </AS>
 > </platform>
 
+! output sort
 $ ${bindir:=.}/flatifier$EXEEXT ../platforms/two_hosts_one_link.xml "--log=root.fmt:[%10.6r]%e[%i:%P@%h]%e%m%n"
 > [  0.000000] [0:maestro@] Switching to the L07 model to handle parallel tasks.
 > <?xml version='1.0'?>
@@ -551,6 +558,7 @@ $ ${bindir:=.}/flatifier$EXEEXT ../platforms/two_hosts_one_link.xml "--log=root.
 > </AS>
 > </platform>
 
+! output sort
 $ ${bindir:=.}/flatifier$EXEEXT ${srcdir:=.}/examples/platforms/bypassASroute.xml "--log=root.fmt:[%10.6r]%e[%i:%P@%h]%e%m%n"
 > [  0.000000] [0:maestro@] Switching to the L07 model to handle parallel tasks.
 > <?xml version='1.0'?>
@@ -685,7 +693,7 @@ $ ${bindir:=.}/flatifier$EXEEXT ${srcdir:=.}/examples/platforms/bypassASroute.xm
 > </AS>
 > </platform>
 
-
+! output sort
 $ ${bindir:=.}/flatifier$EXEEXT ${srcdir:=.}/examples/platforms/torus_cluster.xml "--log=root.fmt:[%10.6r]%e[%i:%P@%h]%e%m%n"
 > [  0.000000] [0:maestro@] Switching to the L07 model to handle parallel tasks.
 > <?xml version='1.0'?>
diff --git a/teshsuite/simdag/is-router/is-router.tesh b/teshsuite/simdag/is-router/is-router.tesh
index 4e1eaeac0b..997996f77a 100644
--- a/teshsuite/simdag/is-router/is-router.tesh
+++ b/teshsuite/simdag/is-router/is-router.tesh
@@ -1,5 +1,5 @@
 #! ./tesh
-
+! output sort
 $ ${bindir:=.}/is-router ../platforms/test_of_is_router.xml "--log=root.fmt:[%10.6r]%e[%i:%P@%h]%e%m%n"
 > [  0.000000] [0:maestro@] Switching to the L07 model to handle parallel tasks.
 > Host number: 10, link number: 1, elmts number: 21
diff --git a/tools/cmake/DefinePackages.cmake b/tools/cmake/DefinePackages.cmake
index 05a1e898a0..a2ed64bac2 100644
--- a/tools/cmake/DefinePackages.cmake
+++ b/tools/cmake/DefinePackages.cmake
@@ -609,7 +609,8 @@ set(MC_SRC
   src/mc/mc_safety.h
   src/mc/mc_state.h
   src/mc/mc_state.cpp
-  src/mc/mc_visited.cpp
+  src/mc/VisitedState.cpp
+  src/mc/VisitedState.hpp
   src/mc/mc_client_api.cpp
   src/mc/mc_protocol.h
   src/mc/mc_protocol.cpp