From 0ff36f645a2645b6fcc757c72ca30b8533564358 Mon Sep 17 00:00:00 2001 From: Martin Quinson Date: Thu, 5 Jul 2012 21:33:19 +0200 Subject: [PATCH] be more verbose on explaining the expected result of the model-checker --- examples/msg/chord/chord.c | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/examples/msg/chord/chord.c b/examples/msg/chord/chord.c index f2c07baea2..129c79aead 100644 --- a/examples/msg/chord/chord.c +++ b/examples/msg/chord/chord.c @@ -637,7 +637,13 @@ static int remote_find_successor(node_t node, int ask_to, int id) task_data_t ans_data = MSG_task_get_data(task_received); if (MC_IS_ENABLED) { - // the model-checker is expected to find a counter-example here + // the model-checker is expected to find a counter-example here. + // + // As you can see in the test right below, task_received is not always equal to task_sent + // (as messages from differing round can interleave). But the previous version of this code + // wrongly assumed that, leading to problems. But this only occured on large platforms, + // leading to hardly usable traces. So we used the model-checker to track down the issue, + // and we came down to this test, that explained the bug in a snap. MC_assert(task_received == task_sent); } -- 2.20.1