verif/nico-md-merge/no_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 []((buffer_large_enough) -> (!have_events_lost))