0b55f123 |
1 | #define NUMPROCS 2 |
2 | |
3 | byte counter = 0; |
4 | byte progress[NUMPROCS]; |
5 | |
6 | proctype incrementer(byte me) |
7 | { |
8 | int temp; |
9 | |
10 | temp = counter; |
11 | counter = temp + 1; |
12 | progress[me] = 1; |
13 | } |
14 | |
15 | init { |
16 | int i = 0; |
17 | int sum = 0; |
18 | |
19 | atomic { |
20 | i = 0; |
21 | do |
22 | :: i < NUMPROCS -> |
23 | progress[i] = 0; |
24 | run incrementer(i); |
25 | i++ |
26 | :: i >= NUMPROCS -> break |
27 | od; |
28 | } |
29 | atomic { |
30 | i = 0; |
31 | sum = 0; |
32 | do |
33 | :: i < NUMPROCS -> |
34 | sum = sum + progress[i]; |
35 | i++ |
36 | :: i >= NUMPROCS -> break |
37 | od; |
38 | assert(sum < NUMPROCS || counter == NUMPROCS) |
39 | } |
40 | } |