Matching on a ring:

L=3
m(i) corresponds to the variable of process (i)

m(i) takes three values {0,1,2} where:

0='self'
1='left'
2='right'


Invariant:

for all (i) (m(i)==0 --> (m(i+1)== 2 && m(i-1)==1)) && (m(i)==1 --> m(i-1)==2) && (m(i)==2 --> m(i+1)==1)


Synthesized programs

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


P0 
 {m0}{0} : m0{1,2} m1{2} m5{1}
 {m0}{1} : m0{0,2} m5{0,2} (m0{0,1} (m1{0} + m5{1,2}) + m1{0,2} (m0{1,2} m1{1,2} + m5{1,2}))
 {m0}{2} : m0{0,1} m1{0,1} (m0{0,2} (m1{1,2} + m5{0}) + m5{0,1} (m1{1,2} + m0{1,2}m5{1,2}))
 
P1 
 {m1}{0} : m0{1} m1{1,2} m2{2}
 {m1}{1} : m1{0,2} (m0{2} (m1{0,1} + m2{0}) + m0{0} m2{2})
 {m1}{2} : m1{0,1} m2{0,1} (m0{1,2} (m0{0,1} m1{1,2} + m2{1,2}) + m0{0} m1{0,2})
 
P2 
 {m2}{0} : m1{1} m2{1,2} m3{2}
 {m2}{1} : m2{0,2} (m1{2} (m2{0,1} + m3{0}) + m1{0} m3{2})
 {m2}{2} : m2{0,1} m3{0,1} (m1{0} m2{0,2} + m1{1,2} m3{1,2})
 
P3 
 {m3}{0} : m2{1} m3{1,2} m4{2}
 {m3}{1} : m3{0,2} (m2{2} (m3{0,1} + m4{0}) + m2{0} m4{2})
 {m3}{2} : m3{0,1} m4{0,1} (m2{0} m3{0,2} + m2{1,2} m4{1,2})
 
P4 
 {m4}{0} : m3{1} m4{1,2} m5{2}
 {m4}{1} : m4{0,2} (m3{2} (m4{0,1} + m5{0}) + m3{0} m5{2})
 {m4}{2} : m4{0,1} m5{0,1} (m3{0} m4{0,2} + m3{1,2} m5{1,2})
 
P5 
 {m5}{0} : m0{2} m4{1} m5{1,2}
 {m5}{1} : m5{0,2} (m0{2} m4{0} + m4{2} m5{0,1})
 {m5}{2} : m0{0,1} m5{0} (m0{1,2} + m4{1})



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

 {m0}{0} : m0{1,2} m1{2} m5{1}
 {m0}{1} : m0{0,2} (m1{0} m5{2} + m1{2} m5{0} + m0{0,1} m5{2})
 {m0}{2} : m0{0,1} m1{0,1} (m1{1,2} m5{1,2} + m0{0,2} m5{0})
 
 {m1}{0} : m0{1} m1{1,2} m2{2}
 {m1}{1} : m1{0,2} (m0{2} (m1{0,1} + m2{0}) + m0{0} m2{2})
 {m1}{2} : m1{0,1} m2{0,1} (m0{0} m1{0,2} + m0{1,2} m2{1,2})
 
 {m2}{0} : m1{1} m2{1,2} m3{2}
 {m2}{1} : m2{0,2} (m1{2} m2{0,1} + m1{0} m3{2})
 {m2}{2} : m2{0} m3{0,1} (m1{1} + m3{1,2})
 
 {m3}{0} : m2{1} m3{1,2} m4{2}
 {m3}{1} : m2{0,2} m3{0,2} (m2{1,2} (m3{0,1} + m4{0,2}) + m3{1,2} m4{2} + m3{0,1}m4{0})
 {m3}{2} : m3{0,1} m4{0,1} (m2{0,1} (m2{1,2} m3{1,2} + m2{0,2} m3{0,2} + m4{1,2}) + m3{0,2} m4{1,2})
 
 {m4}{0} : m3{1} m4{1,2} m5{2}
 {m4}{1} : m4{0,2} (m3{2} (m4{0,1} + m5{0}) + m3{0} m5{2})
 {m4}{2} : m4{0,1} m5{0,1} (m3{1,2} (m3{0,1} m4{1,2} + m5{1,2}) + m3{0} m4{0,2})
 
 {m5}{0} : m0{2} m4{1} m5{1,2}
 {m5}{1} : m5{0,2} (m0{0} m4{2} + m0{2} m4{0} + m4{2} m5{0,1})
 {m5}{2} : m0{0,1} m5{0,1} (m0{1,2} m4{1,2} + m4{0} m5{0,2})
 

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

 {m0}{0} : m0{1,2} m1{2} m7{0,1} (m0{0,2} + m7{1,2})
 {m0}{1} : m0{0,2} m7{0,2} (m0{0,1} (m1{0} + m7{1,2}) + m1{0,2} (m0{1,2} m1{1,2} +  m7{1,2}))
 {m0}{2} : m0{0,1} m1{0,1} (m1{1,2} + m0{0,2} m7{0})
 
 {m1}{0} : m0{1} m1{1,2} m2{2}
 {m1}{1} : m0{0,2} m1{0,2} (m0{1,2} (m1{0,1} + m2{0,2}) + m2{0,2} (m1{0,1} +  m2{1,2}))
 {m1}{2} : m1{0,1} (m0{0} m1{0,2} + m0{1,2} m2{1})

 {m2}{0} : m1{1} m2{1,2} m3{2}
 {m2}{1} : m1{0,2} m2{0,2} (m1{1,2} (m2{0,1} + m3{0,2}) + m3{0,2} (m2{0,1} + m3{1,2}))
 {m2}{2} : m2{0,1} (m1{0} m2{0,2} + m1{1,2} m3{1})
 
 {m3}{0} : m2{1} m3{1,2} m4{2}
 {m3}{1} : m3{0,2} (m2{0,2} (m2{1,2} (m3{0,1} + m4{0,2}) + m4{2}) + m3{0,1} m4{0})
 {m3}{2} : m3{0,1} (m2{0} m3{0,2} + m2{1,2} m4{1})
 
 {m4}{0} : m3{1} m4{1,2} m5{2}
 {m4}{1} : m3{0,2} m4{0,2} (m3{1,2} (m4{0,1} + m5{0,2}) + m4{1,2} m5{2})
 {m4}{2} : m4{0,1} m5{1} (m3{1,2} + m4{0,2})
 
 {m5}{0} : m4{1} m5{1,2} m6{2}
 {m5}{1} : m4{0,2} m5{0,2} (m4{1,2} (m5{0,1} + m6{0,2}) + m6{0,2} (m5{0,1} + m6{1,2}))
 {m5}{2} : m5{0,1} (m4{0} m5{0,2} + m4{1,2} m6{1})
 
 {m6}{0} : m5{1} m6{1,2} m7{2}
 {m6}{1} : m5{0,2} m6{0,2} (m5{1,2} (m6{0,1} + m7{0,2}) + m7{0,2} (m6{0,1} + m7{1,2}))
 {m6}{2} : m6{0,1} (m5{0} m6{0,2} + m5{1,2} m7{1})
 
 {m7}{0} : m0{2} m6{1} m7{1,2}
 {m7}{1} : m6{0,2} m7{0,2} (m0{0,2} (m0{1,2} + m7{0,1}) + m6{1,2} m7{0,1})
 {m7}{2} : m7{0,1} (m0{0,1} (m0{1,2} m6{1,2} + m6{0,1} m7{0,2}) + m6{0} m7{0,2})