#define N 10

byte x=0;
byte y=0;
byte z=0;

active proctype P_X(){
	do
		:: x==y && x == z && x < N->
		x=x+1
	od;
}
active proctype P_Y(){	
	do
		:: x>y && y < N->
		y=y+1
	od;
}

active proctype P_Z(){	
	do
		:: y>z && z < N->
		z=z+1
	od;
}