verif/md/model_03_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)