| 1 | #define rwoff1 (write_off - read_off >= 0) |
| 2 | #define rwoff2 (write_off - read_off < HALF_UCHAR) |
| 3 | |
| 4 | #define wcsum1 (write_off - _commit_sum >= 0) |
| 5 | #define wcsum2 (write_off - _commit_sum < HALF_UCHAR) |
| 6 | |
| 7 | #define buffer_large_enough (NUMPROCS + NUMSWITCH <= BUFSIZE) |
| 8 | #define have_events_lost (events_lost != 0) |
| 9 | never { /* !( buffer_large_enough -> ([](!have_events_lost))) */ |
| 10 | T0_init: |
| 11 | if |
| 12 | :: ((buffer_large_enough) && (have_events_lost)) -> goto accept_all |
| 13 | :: ((buffer_large_enough)) -> goto T0_S3 |
| 14 | fi; |
| 15 | T0_S3: |
| 16 | if |
| 17 | :: ((have_events_lost)) -> goto accept_all |
| 18 | :: (1) -> goto T0_S3 |
| 19 | fi; |
| 20 | accept_all: |
| 21 | skip |
| 22 | } |