#define incmod3(x) ((x+1)%3)
#define decmod3(x) ((x+2)%3)
#define implies(s1,s2) (!(s1) || (s2))

#define right 2
#define left 1
#define self 0

#define invariant implies(x1==left, x7==right) && implies(x1==right,x2==left)&& implies(x1==self, (x7 ==left) && (x2==right)) && implies(x2==left, x1==right) && implies(x2==right,x3==left)&& implies(x2==self, (x1 ==left) && (x3==right)) && implies(x3==left, x2==right) && implies(x3==right,x4==left)&& implies(x3==self, (x2 ==left) && (x4==right)) && implies(x4==left, x3==right) && implies(x4==right,x5==left)&& implies(x4==self, (x3 ==left) && (x5==right)) && implies(x5==left, x4==right) && implies(x5==right,x6==left)&& implies(x5==self, (x4 ==left) && (x6==right)) && implies(x6==left, x5==right) && implies(x6==right,x7==left)&& implies(x6==self, (x5 ==left) && (x7==right)) && implies(x7==left, x6==right) && implies(x7==right,x1==left)&& implies(x7==self, (x6 ==left) && (x1==right))

#define nofaults counter>29

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


proctype P1(){
  do
    ::d_step{x1!=self && x7==left && x2==right   ->x1=self}
    ::d_step{((x1==self)&&(x7==right || x2==self)) || (x7==self && x1!=left && x2==right) || (x7==right && x1==right && x2!=left)  ->x1=left}
    ::d_step{((x1==self)&&(x7==self || x2==left))   ||  (x7==left && x1!=right && x2==self) || (x7!=right  && x1==left   && x2==left)  ->x1=right}
  od
}

proctype P2(){
  do
    ::d_step{x2!=self && x1==left && x3==right   ->x2=self}
    ::d_step{((x2==self)&&(x1==right || x3==self)) || (x1==self && x2!=left && x3==right) || (x1==right && x2==right && x3!=left)  ->x2=left}
    ::d_step{((x2==self)&&(x1==self || x3==left))   ||  (x1==left && x2!=right && x3==self) || (x1!=right  && x2==left   && x3==left)  ->x2=right}

  od
}

proctype P3(){
  do
    ::d_step{x3!=self && x2==left && x4==right   ->x3=self}
    ::d_step{((x3==self)&&(x2==right || x4==self)) || (x2==self && x3!=left && x4==right) || (x2==right && x3==right && x4!=left)  ->x3=left}
    ::d_step{((x3==self)&&(x2==self || x4==left))   ||  (x2==left && x3!=right && x4==self) || (x2!=right  && x3==left   && x4==left)  ->x3=right}



  od
}


proctype P4(){
  do
    ::d_step{x4!=self && x3==left && x5==right   ->x4=self}
    ::d_step{((x4==self)&&(x3==right || x5==self)) || (x3==self && x4!=left && x5==right) || (x3==right && x4==right && x5!=left)  ->x4=left}
    ::d_step{((x4==self)&&(x3==self || x5==left))   ||  (x3==left && x4!=right && x5==self) || (x3!=right  && x4==left   && x5==left)  ->x4=right}

 od
}

proctype P5(){
 do
    ::d_step{x5!=self && x4==left && x6==right   ->x5=self}
    ::d_step{((x5==self)&&(x4==right || x6==self)) || (x4==self && x5!=left && x6==right) || (x4==right && x5==right && x6!=left)  ->x5=left}
    ::d_step{((x5==self)&&(x4==self || x6==left))   ||  (x4==left && x5!=right && x6==self) || (x4!=right  && x5==left   && x6==left)  ->x5=right}
 od
}

proctype P6(){
 do
    ::d_step{x6!=self && x5==left && x7==right   ->x6=self}
    ::d_step{((x6==self)&&(x5==right || x7==self)) || (x5==self && x6!=left && x7==right) || (x5==right && x6==right && x7!=left)  ->x6=left}
    ::d_step{((x6==self)&&(x5==self || x7==left))   ||  (x5==left && x6!=right && x7==self) || (x5!=right  && x6==left   && x7==left)  ->x6=right}
 od
}

proctype P7(){
 do
    ::d_step{x7!=self && x6==left && x1==right   ->x7=self}
    ::d_step{((x7==self)&&(x6==right || x1==self)) || (x6==self && x7!=left && x1==right) || (x6==right && x7==right && x1!=left)  ->x7=left}
    ::d_step{((x7==self)&&(x6==self || x1==left))   ||  (x6==left && x7!=right && x1==self) || (x6!=right  && x7==left   && x1==left)  ->x7=right}
 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++;}
    
    



  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();

}