#define incmod3(x) ((x+1)%3)
#define decmod3(x) ((x+2)%3)
#define invlocal(x,y,z,t) ((x==y && y==z ) || (turn==t)&&((x==y && y==incmod3(z)) || (x==incmod3(y) && y==z)))
#define invariant invlocal(x1,x2,x3,0) && invlocal(x4,x5,x6,1) && invlocal(x7,x8,x9,2)
#define nofaults counter>29

int x1,x2,x3,x4,x5,x6,x7,x8,x9;
int turn;
int counter;


proctype P1(){
  do
    ::d_step{x1==x3 && turn==0 && x1==x7 -> x1=incmod3(x3)}
    ::d_step{x1==x3 && turn==0 && x1!=x7  -> turn=1} 
  od
}
proctype P4(){
do
    ::d_step{x4==x6 && turn==1 && x4!=x1 -> x4=incmod3(x6)}
    ::d_step{x4==x6 && turn==1 && x4==x1  -> turn=2} 
 od
}

proctype P7(){
do
    ::d_step{x7==x9 && turn==2 && x7!=x4 -> x7=incmod3(x9)}
    ::d_step{x7==x9 && turn==2 && x7==x4  -> turn=0} 
 od
}


proctype P2(){
  do
    ::d_step{x2==incmod3(x1)->x2=decmod3(x1)}
    ::d_step{x1==incmod3(x2)->x2=x1}
  od
}

proctype P5(){
do
    ::d_step{x5==incmod3(x4)->x5=decmod3(x4)}
    ::d_step{x4==incmod3(x5)->x5=x4}
  od
}

proctype P8(){
do
    ::d_step{x8==incmod3(x7)->x8=decmod3(x7)}
    ::d_step{x7==incmod3(x8)->x8=x7}
  od
}

proctype P3(){
  do
    ::d_step{x3!=x2->x3=x2}
  od
}

proctype P6(){
  do
   ::d_step{x6!=x5->x6=x5}
od
}

proctype P9(){
do
   ::d_step{x9!=x8->x9=x8}
od  
}

proctype Fault()
{
  
  counter=0;
  do
    ::(counter<30)->d_step{x1=0; counter++;}
    ::(counter<30)->d_step{x1=1; counter++;}
    ::(counter<30)->d_step{x1=2; counter++;}  
    ::(counter<30)->d_step{x2=0; counter++;}
    ::(counter<30)->d_step{x2=1; counter++;}
    ::(counter<30)->d_step{x2=2; counter++;}
    ::(counter<30)->d_step{x3=0; counter++;}
    ::(counter<30)->d_step{x3=1; counter++;}
    ::(counter<30)->d_step{x3=2; counter++;}
    ::(counter<30)->d_step{x4=0; counter++;}
    ::(counter<30)->d_step{x4=1; counter++;}
    ::(counter<30)->d_step{x4=2; counter++;}  
    ::(counter<30)->d_step{x5=0; counter++;}
    ::(counter<30)->d_step{x5=1; counter++;}
    ::(counter<30)->d_step{x5=2; counter++;}
    ::(counter<30)->d_step{x6=0; counter++;}
    ::(counter<30)->d_step{x6=1; counter++;}
    ::(counter<30)->d_step{x6=2; counter++;}
    ::(counter<30)->d_step{x7=0; counter++;}
    ::(counter<30)->d_step{x7=1; counter++;}
    ::(counter<30)->d_step{x7=2; counter++;}  
    ::(counter<30)->d_step{x8=0; counter++;}
    ::(counter<30)->d_step{x8=1; counter++;}
    ::(counter<30)->d_step{x8=2; counter++;}
    ::(counter<30)->d_step{x9=0; counter++;}
    ::(counter<30)->d_step{x9=1; counter++;}
    ::(counter<30)->d_step{x9=2; counter++;}
     ::(counter<30)->d_step{turn=0;counter++;}
    ::(counter<30)->d_step{turn=1;counter++;}
    ::(counter<30)->d_step{turn=2;counter++;}
od
}

init
{
  
  /*Initialize*/
  x1=0; x2=0; x3=0;
  
  run P1();
  run P2();
  run P3();
  run P4();
  run P5();
  run P6();
  run P7();
  run P8();
  run P9();
  run Fault();

}