#define incmod(x) ((x+1)%7)
#define decmod(x) ((x+6)%7)
#define invariant ((x1==x2 && x2==x3 && x3==x4 && x4==x5  && x5==x6 && x6==x7) || (x1==incmod(x2) && x2==x3 && x3==x4 && x4==x5 && x5==x6 && x6==x7) || (x1==x2 && x2==incmod(x3) && x3==x4 && x4==x5 && x5==x6 && x6==x7) || (x1==x2 && x2==x3 && x3==incmod(x4) && x4==x5 && x5==x6 && x6==x7)  || (x1==x2 && x2==x3 &&  x3==x4 && x4==incmod(x5) && x5==x6 && x6==x7) || (x1==x2 && x2==x3 &&  x3==x4 && x4==x5 && x5==incmod(x6) && x6==x7) || (x1==x2 && x2==x3 &&  x3==x4 && x4==x5 && x5==x6 && x6==incmod(x7))) 
#define nofaults counter>29

int x1,x2,x3,x4,x5,x6,x7;
int counter;


proctype P1(){
  do
    ::d_step{ (x1==x7)->x1=incmod(x7)}
    ::d_step{((x1!=x7) && (x1!=incmod(x7)))->x1=x7}
  od
}
proctype P2(){
  do
    ::d_step{(x1!=x2) && (x1!=decmod(x2)) ->x2=x1}
    ::d_step{(x1==decmod(x2))->x2=decmod(x1)}
  od
}

proctype P3(){

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

}

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

}


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

}


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

}



proctype P7(){
  do
    ::d_step{(x6==incmod(x7))->x7=x6}
  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;x5=0;x6=0;x7=0;
  
  run P1();
  run P2();
  run P3();
  run P4();
  run P5();
  run P6();
  run P7();
  run Fault();

}