1	#define N 10
2	
3	byte x=0;
4	byte y=0;
5	byte z=0;
6	
7	active proctype P_X(){
8		do
9			:: x==y && x == z && x < N->
10			x=x+1
11		od;
12	}
13	active proctype P_Y(){	
14		do
15			:: x>y && y < N->
16			y=y+1
17		od;
18	}
19	
20	active proctype P_Z(){	
21		do
22			:: y>z && z < N->
23			z=z+1
24		od;
25	}