dc45444e |
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 | } |