model-checker : bugged2_liveness with promela of LTL properties checked

[simgrid.git] / examples / msg / mc / bugged2_liveness.c

diff --git a/examples/msg/mc/bugged2_liveness.c b/examples/msg/mc/bugged2_liveness.c
index 3f544cc..305771f 100644 (file)
--- a/examples/msg/mc/bugged2_liveness.c
+++ b/examples/msg/mc/bugged2_liveness.c
@@ -1,3 +1,9 @@
+/***************** Producer/Consumer Algorithm *************************/
+/* This example implements a producer/consumer algorithm.              */
+/* If consumer work before producer, message is empty                  */
+/***********************************************************************/
+
+
 #include "msg/msg.h"
 #include "mc/mc.h"
 #include "xbt/automaton.h"