verif/md/model_03_no_events_lost.spin.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))