From 3d28e83ea2a5f93c7654087eb70ab2e873553628 Mon Sep 17 00:00:00 2001
From: Marion Guthmuller <marion.guthmuller@loria.fr>
Date: Wed, 13 Jun 2012 11:47:33 +0200
Subject: [PATCH] model-checker : test unit for snapshot comparison

---
 src/mc/mc_liveness.c | 28 ++++++++++++++++++++++++++++
 1 file changed, 28 insertions(+)

diff --git a/src/mc/mc_liveness.c b/src/mc/mc_liveness.c
index 1ad236eabb..38dc7bd64c 100644
--- a/src/mc/mc_liveness.c
+++ b/src/mc/mc_liveness.c
@@ -1280,3 +1280,31 @@ void MC_ddfs(int search_cycle){
   
 
 }
+
+
+#ifdef SIMGRID_TEST
+
+XBT_TEST_SUITE("mc_liveness", "Model checking liveness properties");
+XBT_LOG_EXTERNAL_DEFAULT_CATEGORY(mc_liveness);
+
+XBT_TEST_UNIT("snapshots_comparison", test_compare_snapshot, "Comparison of snapshots")
+{
+
+  MC_SET_RAW_MEM;
+
+  /* Save first snapshot */
+  mc_snapshot_t snapshot1 = xbt_new0(s_mc_snapshot_t, 1);
+  MC_take_snapshot_liveness(snapshot1);
+
+  /* Save second snapshot */
+  mc_snapshot_t snapshot2 = xbt_new0(s_mc_snapshot_t, 1);
+  MC_take_snapshot_liveness(snapshot2);
+
+  MC_UNSET_RAW_MEM;
+
+  xbt_test_assert(snapshot_compare(snapshot1, snapshot2, std_heap, raw_heap) == 0, "Different consecutive snapshot");
+  
+
+}
+
+#endif
-- 
2.20.1