Token Ring

Invariant:

(This invariant is for 4 processes)
(x0==x1)&&(x1==x2)&&(x2==x3) || (x0==x1+1)&&(x1==x2)&&(x2==x3) || (x0=x1)&&(x1==x2+1)&&(x2==x3) ||  (x0==x1)&&(x1==x2)&&(x2==x3+1)



Synthesized programs
Case 1: N=4, L=3, sch={0,1,2,3}

P0
 {x0}{0} : x0{1,2} x3{2}
 {x0}{1} : x0{0,2} x3{0}
 {x0}{2} : x0{0,1} x3{1}
 
P1 
 {x1}{0} : x0{0} x1{1,2}
 {x1}{1} : x0{1} x1{0,2}
 {x1}{2} : x0{2} x1{0,1}
 
P2 
 {x2}{0} : x1{0} x2{1,2}
 {x2}{1} : x1{1} x2{0,2}
 {x2}{2} : x1{2} x2{0,1}
 
P3 
 {x3}{0} : x2{0} x3{2}
 {x3}{1} : x2{1} x3{0}
 {x3}{2} : x2{2} x3{1}



Case 2: N=4, L=3, sch={1,2,3,0}

 {x0}{0} : x0{2} x3{2}
 {x0}{1} : x0{0} x3{0}
 {x0}{2} : x0{1} x3{1}
 
 {x1}{0} : x0{0} x1{1,2}
 {x1}{1} : x0{1} x1{0,2}
 {x1}{2} : x0{2} x1{0,1}
 
 {x2}{0} : x1{0} x2{1,2}
 {x2}{1} : x1{1} x2{0,2}
 {x2}{2} : x1{2} x2{0,1}
 
 {x3}{0} : x2{0} x3{1,2}
 {x3}{1} : x2{1} x3{0,2}
 {x3}{2} : x2{2} x3{0,1}



Case 3: N=4, L=4, sch={0,1,2,3}

 {x0}{0} : x3{0,3} (x0{3} + x0{2} x3{0,1,2})
 {x0}{1} : x3{0,1} (x0{0} + x0{3} x3{1,2,3})
 {x0}{2} : x3{1,2} (x0{1} + x0{0} x3{0,2,3})
 {x0}{3} : x3{2,3} (x0{2} + x0{1} x3{0,1,3})
 
 {x1}{0} : x1{2,3} (x0{0} + x0{1} x1{0,1,2})
 {x1}{1} : x1{0,3} (x0{1} + x0{2} x1{1,2,3})
 {x1}{2} : x1{0,1} (x0{2} + x0{3} x1{0,2,3})
 {x1}{3} : x1{1,2} (x0{3} + x0{0} x1{0,1,3})
 
 {x2}{0} : x2{2,3} (x1{0} + x1{1} x2{0,1,2})
 {x2}{1} : x2{0,3} (x1{1} + x1{2} x2{1,2,3})
 {x2}{2} : x2{0,1} (x1{2} + x1{3} x2{0,2,3})
 {x2}{3} : x2{1,2} (x1{3} + x1{0} x2{0,1,3})
 
 {x3}{0} : x2{0} x3{3}
 {x3}{1} : x2{1} x3{0}
 {x3}{2} : x2{2} x3{1}
 {x3}{3} : x2{3} x3{2}




Case 4: N=4, L=4, sch={1,2,3,0}

 {x0}{0} : x0{3} x3{3}
 {x0}{1} : x0{0} x3{0}
 {x0}{2} : x0{1} x3{1}
 {x0}{3} : x0{2} x3{2}
 
 {x1}{0} : x1{2,3} (x0{1} + x0{0} x1{0,1,3})
 {x1}{1} : x1{0,3} (x0{2} + x0{1} x1{0,1,2})
 {x1}{2} : x1{0,1} (x0{3} + x0{2} x1{1,2,3})
 {x1}{3} : x1{1,2} (x0{0} + x0{3} x1{0,2,3})
 
 {x2}{0} : x2{2,3} (x1{0} + x1{1} x2{0,1,2})
 {x2}{1} : x2{0,3} (x1{1} + x1{2} x2{1,2,3})
 {x2}{2} : x2{0,1} (x1{2} + x1{3} x2{0,2,3})
 {x2}{3} : x2{1,2} (x1{3} + x1{0} x2{0,1,3})
 
 {x3}{0} : x3{2,3} (x2{0} + x2{1} x3{0,1,2})
 {x3}{1} : x3{0,3} (x2{1} + x2{2} x3{1,2,3})
 {x3}{2} : x3{0,1} (x2{2} + x2{3} x3{0,2,3})
 {x3}{3} : x3{1,2} (x2{3} + x2{0} x3{0,1,3})




Case 5: N=5, L=4, sch={0,1,2,3,4}

 {x0}{0} : x4{0,3} (x0{2} + x0{3} x4{1,2,3})
 {x0}{1} : x4{0,1} (x0{3} + x0{0} x4{0,2,3})
 {x0}{2} : x4{1,2} (x0{0} + x0{1} x4{0,1,3})
 {x0}{3} : x4{2,3} (x0{1} + x0{2} x4{0,1,2})
 
 {x1}{0} : x1{2,3} (x0{0} + x0{1} x1{0,1,2})
 {x1}{1} : x1{0,3} (x0{1} + x0{2} x1{1,2,3})
 {x1}{2} : x1{0,1} (x0{2} + x0{3} x1{0,2,3})
 {x1}{3} : x1{1,2} (x0{3} + x0{0} x1{0,1,3})
 
 {x2}{0} : x2{2,3} (x1{0} + x1{1} x2{0,1,2})
 {x2}{1} : x2{0,3} (x1{1} + x1{2} x2{1,2,3})
 {x2}{2} : x2{0,1} (x1{2} + x1{3} x2{0,2,3})
 {x2}{3} : x2{1,2} (x1{3} + x1{0} x2{0,1,3})
 
 {x3}{0} : x3{2,3} (x2{0} + x2{1} x3{0,1,2})
 {x3}{1} : x3{0,3} (x2{1} + x2{2} x3{1,2,3})
 {x3}{2} : x3{0,1} (x2{2} + x2{3} x3{0,2,3})
 {x3}{3} : x3{1,2} (x2{3} + x2{0} x3{0,1,3})
 
 {x4}{0} : x3{0} x4{3}
 {x4}{1} : x3{1} x4{0}
 {x4}{2} : x3{2} x4{1}
 {x4}{3} : x3{3} x4{2}





Case 6: N=5, L=4, sch{1,2,3,4,0}


 {x0}{0} : x0{3} x4{3}
 {x0}{1} : x0{0} x4{0}
 {x0}{2} : x0{1} x4{1}
 {x0}{3} : x0{2} x4{2}
 
 {x1}{0} : x1{2,3} (x0{0} + x0{1} x1{0,1,2})
 {x1}{1} : x1{0,3} (x0{1} + x0{2} x1{1,2,3})
 {x1}{2} : x1{0,1} (x0{2} + x0{3} x1{0,2,3})
 {x1}{3} : x1{1,2} (x0{3} + x0{0} x1{0,1,3})
 
 {x2}{0} : x2{2,3} (x1{0} + x1{1} x2{0,1,2})
 {x2}{1} : x2{0,3} (x1{1} + x1{2} x2{1,2,3})
 {x2}{2} : x2{0,1} (x1{2} + x1{3} x2{0,2,3})
 {x2}{3} : x2{1,2} (x1{3} + x1{0} x2{0,1,3})
 
 {x3}{0} : x3{2,3} (x2{0} + x2{1} x3{0,1,2})
 {x3}{1} : x3{0,3} (x2{1} + x2{2} x3{1,2,3})
 {x3}{2} : x3{0,1} (x2{2} + x2{3} x3{0,2,3})
 {x3}{3} : x3{1,2} (x2{3} + x2{0} x3{0,1,3})
 
 {x4}{0} : x4{2,3} (x3{0} + x3{1} x4{0,1,2})
 {x4}{1} : x4{0,3} (x3{1} + x3{2} x4{1,2,3})
 {x4}{2} : x4{0,1} (x3{2} + x3{3} x4{0,2,3})
 {x4}{3} : x4{1,2} (x3{3} + x3{0} x4{0,1,3})