#define rwoff1 (write_off - read_off >= 0)
#define rwoff2 (write_off - read_off < HALF_UCHAR)

#define wcsum1 (write_off - _commit_sum >= 0)
#define wcsum2 (write_off - _commit_sum < HALF_UCHAR)

#define buffer_large_enough (NUMPROCS + NUMSWITCH <= BUFSIZE)
#define have_events_lost (events_lost != 0)
never {    /* !( buffer_large_enough -> ([](!have_events_lost))) */
T0_init:
	if
	:: ((buffer_large_enough) && (have_events_lost)) -> goto accept_all
	:: ((buffer_large_enough)) -> goto T0_S3
	fi;
T0_S3:
	if
	:: ((have_events_lost)) -> goto accept_all
	:: (1) -> goto T0_S3
	fi;
accept_all:
	skip
}