X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/a941e1f7d2bca6b2e3ef7f83b954d26f990cd9a6..1817e908617a7ac2fd9cd68dc222117c368477a1:/examples/msg/mc/bugged2_liveness.c

diff --git a/examples/msg/mc/bugged2_liveness.c b/examples/msg/mc/bugged2_liveness.c
index 4ab7ab2514..305771fbdc 100644
--- a/examples/msg/mc/bugged2_liveness.c
+++ b/examples/msg/mc/bugged2_liveness.c
@@ -1,9 +1,6 @@
 /***************** 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)     */
 /***********************************************************************/