+ // 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.