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