#define incmod3(x) ((x+1)%3) #define decmod3(x) ((x+2)%3) #define implies(s1,s2) (!(s1) || (s2)) #define invariant implies(x1==left, x5==right) && implies(x1==right,x2==left)&& implies(x1==self, (x5 ==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,x1==left)&& implies(x5==self, (x4 ==left) && (x1==right)) #define nofaults counter>29 #define right 2 #define left 1 #define self 0 int x1,x2,x3,x4,x5; int counter; proctype P1(){ do ::d_step{x1!=self && x5==left && x2==right ->x1=self} ::d_step{x1!=left && x5==right && (x1!=right || x2!=self) -> x1=left} ::d_step{x1!=right && x2==left && (x1!=left || x5==left)->x1=right} od } proctype P2(){ do ::d_step{x2!=self && x1==left && x3==right -> x2=self} ::d_step{x2!=left && x1!=left && (x1!=self || (x2!=right && x3==self))-> x2=left} ::d_step{x2!=right && x3!=right &&( (x1!=right && ((x1!=left && x2!=left) || x3!=self)) || (x2!=left && x3!=self))->x2=right} od } proctype P3(){ do ::d_step{x3!=self && x2==left && x4==right ->x3=self} ::d_step{x3!=left && x2!=left &&( (x2!=self && (x3!=right || x4!=left)) || (x3!=self && x4==right) || (x3!=right && x4==self))-> x3=left} ::d_step{x3!=right && ((x2==self && x3!=left) || (x2==left && x4==left) || (x3!=left && x4==left))->x3=right} od } proctype P4(){ do ::d_step{x4!=self && x3==left && x5==right ->x4=self} ::d_step{x4!=left && x3!=left &&((x3!=self &&(x4!=right || x5==right))||(x4!=right && x5==self) )->x4=left} ::d_step{x4!=right &&((x4!=left && x3==self) || (x3!=self && x5==left))->x4=right} od } proctype P5(){ do ::d_step{x5!=self && x4==left && x1==right->x5=self} ::d_step{x5!=left && (x4==right ||(x5!=right && x1==self))->x5=left} ::d_step{x5!=right &&((x1==left && (x4==left || x5!=left)) || (x4==self && x5!=left))->x5=right} 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; run P1(); run P2(); run P3(); run P4(); run P5(); run Fault(); }