verif/nico-md-merge/events_lost.ltl

   1 // If we have less writers than the buffer space available, we should
   2 // not loose events.
   3 // assert(NUMPROCS + NUMSWITCH > BUFSIZE || events_lost == 0);
   4
   5 []((have_events_lost) -> (!buffer_large_enough))