[lttv.git] / trunk / verif / nico-md-merge / no_events_lost.ltl

// If we have less writers than the buffer space available, we should
// not loose events.
// assert(NUMPROCS + NUMSWITCH > BUFSIZE || events_lost == 0);

[]((buffer_large_enough) -> (!have_events_lost))
Commit	Line	Data
dc45444e	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))