From 392f009f7db6b4fae2a0f36a0452178d7be7b5f2 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Christophe=20Thi=C3=A9ry?= Date: Thu, 5 Jul 2012 17:14:55 +0200 Subject: [PATCH] Make it clear that MC is supposed to detect a counter-example in chord. --- examples/msg/chord/chord.c | 1 + 1 file changed, 1 insertion(+) diff --git a/examples/msg/chord/chord.c b/examples/msg/chord/chord.c index e0787cb21d..f2c07baea2 100644 --- a/examples/msg/chord/chord.c +++ b/examples/msg/chord/chord.c @@ -637,6 +637,7 @@ 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 MC_assert(task_received == task_sent); } -- 2.20.1