3-coloring of a ring

Invariant:

for all (0<=i<N) (c(i)!=c(i+1))

//(recall that addition and subtraction of indices is modulo N)




Synthesized programs:


N=10, sch={1,2,3,4,5,6,7,8,9,0}




P0 //This process does nothing
 {c0}{0} : Constant 0 
 {c0}{1} : Constant 0
 {c0}{2} : Constant 0

P1 
 {c1}{0} : c0{1,2} c1{1,2} c2{1,2} (c0{0,2} c1{0,2} + c0{0,1} c2{0,2} + c1{0,1} c2{0,1})
 {c1}{1} : c0{0,2} c1{0,2} c2{0,2} (c0{1,2} c1{1,2} + c0{0,1} c2{1,2} + c1{0,1} c2{0,1})
 {c1}{2} : c0{0,1} c1{0,1} c2{0,1} (c0{1,2} c1{1,2} + c0{0,2} c2{1,2} + c1{0,2} c2{0,2})

P2 
 {c2}{0} : c1{1} c2{2} c3{2} + c1{2} c2{1} c3{1}
 {c2}{1} : c1{0} c2{2} c3{2} + c1{2} c2{0} c3{0}
 {c2}{2} : c1{0} c2{1} c3{1} + c1{1} c2{0} c3{0}

P3 
 {c3}{0} : c2{1} c3{2} c4{2} + c2{2} c3{1} c4{1}
 {c3}{1} : c2{0} c3{2} c4{2} + c2{2} c3{0} c4{0}
 {c3}{2} : c2{0} c3{1} c4{1} + c2{1} c3{0} c4{0}

P4 
 {c4}{0} : c3{1} c4{2} c5{2} + c3{2} c4{1} c5{1}
 {c4}{1} : c3{0} c4{2} c5{2} + c3{2} c4{0} c5{0}
 {c4}{2} : c3{0} c4{1} c5{1} + c3{1} c4{0} c5{0}

P5 
 {c5}{0} : c4{1} c5{2} c6{2} + c4{2} c5{1} c6{1}
 {c5}{1} : c4{0} c5{2} c6{2} + c4{2} c5{0} c6{0}
 {c5}{2} : c4{0} c5{1} c6{1} + c4{1} c5{0} c6{0}

P6 
 {c6}{0} : c5{1} c6{2} c7{2} + c5{2} c6{1} c7{1}
 {c6}{1} : c5{0} c6{2} c7{2} + c5{2} c6{0} c7{0}
 {c6}{2} : c5{0} c6{1} c7{1} + c5{1} c6{0} c7{0}
 
P7
 {c7}{0} : c6{1} c7{2} c8{2} + c6{2} c7{1} c8{1}
 {c7}{1} : c6{0} c7{2} c8{2} + c6{2} c7{0} c8{0}
 {c7}{2} : c6{0} c7{1} c8{1} + c6{1} c7{0} c8{0}

P8 
 {c8}{0} : c7{1} c8{2} c9{2} + c7{2} c8{1} c9{1}
 {c8}{1} : c7{0} c8{2} c9{2} + c7{2} c8{0} c9{0}
 {c8}{2} : c7{0} c8{1} c9{1} + c7{1} c8{0} c9{0}
 
P9
 {c9}{0} : c0{2} c8{1} c9{2} + c0{1} c8{2} c9{1}
 {c9}{1} : c0{2} c8{0} c9{2} + c0{0} c8{2} c9{0}
 {c9}{2} : c0{1} c8{0} c9{1} + c0{0} c8{1} c9{0}