Make it clear that MC is supposed to detect a counter-example in chord.

diff --git a/examples/msg/chord/chord.c b/examples/msg/chord/chord.c
index e0787cb..f2c07ba 100644 (file)
--- 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) {
         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);
         }
 
           MC_assert(task_received == task_sent);
         }