A
lgorithmique
N
umérique
D
istribuée
Public GIT Repository
projects
/
simgrid.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
Make it clear that MC is supposed to detect a counter-example in chord.
[simgrid.git]
/
examples
/
msg
/
chord
/
chord.c
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);
}