From: Marion Guthmuller <marion.guthmuller@loria.fr>
Date: Mon, 9 Jan 2012 20:59:31 +0000 (+0100)
Subject: model-checker : add comments for the example bugged2_liveness
X-Git-Tag: exp_20120216~133^2~9
X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/e716b5b6eb47bcdd09c22747a617a7f68e65a645?ds=sidebyside

model-checker : add comments for the example bugged2_liveness
---

diff --git a/examples/msg/mc/bugged2_liveness.c b/examples/msg/mc/bugged2_liveness.c
index 3f544cccee..4ab7ab2514 100644
--- a/examples/msg/mc/bugged2_liveness.c
+++ b/examples/msg/mc/bugged2_liveness.c
@@ -1,3 +1,12 @@
+/***************** Producer/Consumer Algorithm *************************/
+/* This example implements a producer/consumer algorithm.              */
+/* If consumer work before producer, message is empty                  */
+/* LTL property checked : GF((pready U produce) -> (cready U consume)) */
+/* (pready = producer got CS, produce=message pushed in the buffer)    */
+/* (cready = consumer got CS, consume=message display by consumer)     */
+/***********************************************************************/
+
+
 #include "msg/msg.h"
 #include "mc/mc.h"
 #include "xbt/automaton.h"