// artifical constrain byte choosing[2]; byte number[2]; process P_0 { byte j, max; state NCS, choose, for_loop, wait, CS; init NCS; trans NCS -> choose { effect choosing[0] = 1, j=0, max=0; }, choose -> choose { guard j<2 and number[j]>max; effect max = number[j], j = j +1;}, choose -> choose { guard j<2 and number[j]<=max; effect j = j+1;}, choose -> for_loop { guard j == 2 and max < 9; effect number[0] = max + 1, j = 0, choosing[0] = 0; }, for_loop -> wait { guard j<2 and choosing[j]==0; }, wait -> for_loop { guard number[j] == 0 or (number[j] > number[0]) or (number[j] == number[0] and 0 <= j); effect j= j+1;}, for_loop -> CS {guard j==2; }, CS -> NCS { effect number[0]=0;}; } process P_1 { byte j, max; state NCS, choose, for_loop, wait, CS; init NCS; trans NCS -> choose { effect choosing[1] = 1, j=0, max=0; }, choose -> choose { guard j<2 and number[j]>max; effect max = number[j], j = j +1;}, choose -> choose { guard j<2 and number[j]<=max; effect j = j+1;}, choose -> for_loop { guard j == 2 and max < 9; effect number[1] = max + 1, j = 0, choosing[1] = 0; }, for_loop -> wait { guard j<2 and choosing[j]==0; }, wait -> for_loop { guard number[j] == 0 or (number[j] > number[1]) or (number[j] == number[1] and 1 <= j); effect j= j+1;}, for_loop -> CS {guard j==2; }, CS -> NCS { effect number[1]=0;}; } system async;