+/***************** 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"
