#define incmod(x) ((x+1)%4)
#define decmod(x) ((x+3)%4)
#define inc2mod(x) ((x+2)%4)
#define invariant ((x1==x2 && x2==x3 && x3==x4 ) || (x1==incmod(x2) && x2==x3 && x3==x4 ) || (x1==x2 && x2==incmod(x3) && x3==x4 ) || (x1==x2 && x2==x3 && x3==incmod(x4) )) 
#define nofaults counter>29

int x1,x2,x3,x4;
int counter;


proctype P1(){
  do
    ::d_step{ (x1!=incmod(x4) && x1!=inc2mod(x4))->x1=incmod(x4)}
    ::d_step{(x1==inc2mod(x4))->x1=x4}
  od
}

proctype P2(){

  do
    ::d_step{(x1==incmod(x2))->x2=x1}    
  od
}

proctype P3(){

  do
    ::d_step{(x3!=x2) && (x3!=decmod(x2))->x3=decmod(x2)}
    ::d_step{(x3== decmod(x2))-> x3=x2}
  od

}

proctype P4(){
  do
    ::d_step{(x3!=x4) && (x3!=decmod(x4))->x4=x3}
    ::d_step{(x3== decmod(x4))-> x4=decmod(x3)}
  od

}




proctype Fault()
{
  
  counter=0;
  do
    ::(counter<5)->d_step{x1=0; counter++;}
    ::(counter<8)->d_step{x1=1; counter++;}
    ::(counter<12)->d_step{x1=2; counter++;}  
    ::(counter<2)->d_step{x2=0; counter++;}
    ::(counter<25)->d_step{x2=1; counter++;}
    ::(counter<10)->d_step{x2=2; counter++;}
    ::(counter<30)->d_step{x3=0; counter++;}
    ::(counter<1)->d_step{x3=1; counter++;}
    ::(counter<22)->d_step{x3=2; counter++;}
  od
}

init
{
  
  /*Initialize*/
  x1=0; x2=0; x3=0;x4=0;
  
  run P1();
  run P2();
  run P3();
  run P4();
  run Fault();

}