diff --git a/prism-examples/leader/asynchronous/.autopp b/prism-examples/leader/asynchronous/.autopp index dd396d4e..27f12a87 100755 --- a/prism-examples/leader/asynchronous/.autopp +++ b/prism-examples/leader/asynchronous/.autopp @@ -2,6 +2,6 @@ foreach N ( 3 4 5 6 7 8 9 10 ) echo "Generating for N=$N" - prismpp .leaderN.nm.pp $N >! leader_"$N".nm + prismpp .leaderN.nm.pp $N >! leader"$N".nm unix2dos leader"$N".nm end diff --git a/prism-examples/leader/asynchronous/leader10.nm b/prism-examples/leader/asynchronous/leader10.nm index 59361e4f..f4438fd9 100644 --- a/prism-examples/leader/asynchronous/leader10.nm +++ b/prism-examples/leader/asynchronous/leader10.nm @@ -1,15 +1,16 @@ // asynchronous leader election -// 10 processes +// 4 processes // gxn/dxp 29/01/01 mdp -const N=10; // number of processes +const N= 10; // number of processes +//---------------------------------------------------------------------------------------------------------------------------- module process1 // COUNTER - c1 : [0..N-1]; + c1 : [0..10-1]; // STATES s1 : [0..4]; @@ -27,7 +28,6 @@ module process1 // not received anything // received choice // received counter - sent1 : [0..2]; // not send anything // sent choice @@ -69,27 +69,35 @@ module process1 [p101] (s1=3) & (receive1=0) -> (p1'=p10) & (receive1'=1); // receive counter [c101] (s1=3) & (receive1=1) & (c10 (c1'=c10+1) & (receive1'=2); - + // done [done] (s1=4) -> (s1'=s1); // add loop for processes who are inactive [done] (s1=3) -> (s1'=s1); - + endmodule -module process2= process1[s1=s2 ,p1=p2 ,c1=c2 ,sent1=sent2 ,receive1=receive2 ,p12=p23 ,p101=p12 ,c12=c23 ,c101=c12 ,p10=p1,c10=c1] endmodule -module process3= process1[s1=s3 ,p1=p3 ,c1=c3 ,sent1=sent3 ,receive1=receive3 ,p12=p34 ,p101=p23 ,c12=c34 ,c101=c23 ,p10=p2,c10=c2] endmodule -module process4= process1[s1=s4 ,p1=p4 ,c1=c4 ,sent1=sent4 ,receive1=receive4 ,p12=p45 ,p101=p34 ,c12=c45 ,c101=c34 ,p10=p3,c10=c3] endmodule -module process5= process1[s1=s5 ,p1=p5 ,c1=c5 ,sent1=sent5 ,receive1=receive5 ,p12=p56 ,p101=p45 ,c12=c56 ,c101=c45 ,p10=p4,c10=c4] endmodule -module process6= process1[s1=s6 ,p1=p6 ,c1=c6 ,sent1=sent6 ,receive1=receive6 ,p12=p67 ,p101=p56 ,c12=c67 ,c101=c56 ,p10=p5,c10=c5] endmodule -module process7= process1[s1=s7 ,p1=p7 ,c1=c7 ,sent1=sent7 ,receive1=receive7 ,p12=p78 ,p101=p67 ,c12=c78 ,c101=c67 ,p10=p6,c10=c6] endmodule -module process8= process1[s1=s8 ,p1=p8 ,c1=c8 ,sent1=sent8 ,receive1=receive8 ,p12=p89 ,p101=p78 ,c12=c89 ,c101=c78 ,p10=p7,c10=c7] endmodule -module process9= process1[s1=s9 ,p1=p9 ,c1=c9 ,sent1=sent9 ,receive1=receive9 ,p12=p910,p101=p89 ,c12=c910,c101=c89 ,p10=p7,c10=c8] endmodule -module process10=process1[s1=s10,p1=p10,c1=c10,sent1=sent10,receive1=receive10,p12=p101,p101=p910,c12=c101,c101=c910,p10=p7,c10=c9] endmodule +//---------------------------------------------------------------------------------------------------------------------------- + +// construct further stations through renaming +module process2=process1[s1=s2,p1=p2,c1=c2,sent1=sent2,receive1=receive2,p12=p23,p101=p12,c12=c23,c101=c12,p10=p1,c10=c1] endmodule +module process3=process1[s1=s3,p1=p3,c1=c3,sent1=sent3,receive1=receive3,p12=p34,p101=p23,c12=c34,c101=c23,p10=p2,c10=c2] endmodule +module process4=process1[s1=s4,p1=p4,c1=c4,sent1=sent4,receive1=receive4,p12=p45,p101=p34,c12=c45,c101=c34,p10=p3,c10=c3] endmodule +module process5=process1[s1=s5,p1=p5,c1=c5,sent1=sent5,receive1=receive5,p12=p56,p101=p45,c12=c56,c101=c45,p10=p4,c10=c4] endmodule +module process6=process1[s1=s6,p1=p6,c1=c6,sent1=sent6,receive1=receive6,p12=p67,p101=p56,c12=c67,c101=c56,p10=p5,c10=c5] endmodule +module process7=process1[s1=s7,p1=p7,c1=c7,sent1=sent7,receive1=receive7,p12=p78,p101=p67,c12=c78,c101=c67,p10=p6,c10=c6] endmodule +module process8=process1[s1=s8,p1=p8,c1=c8,sent1=sent8,receive1=receive8,p12=p89,p101=p78,c12=c89,c101=c78,p10=p7,c10=c7] endmodule +module process9=process1[s1=s9,p1=p9,c1=c9,sent1=sent9,receive1=receive9,p12=p910,p101=p89,c12=c910,c101=c89,p10=p8,c10=c8] endmodule +module process10=process1[s1=s10,p1=p10,c1=c10,sent1=sent10,receive1=receive10,p12=p101,p101=p910,c12=c101,c101=c910,p10=p9,c10=c9] endmodule + +//---------------------------------------------------------------------------------------------------------------------------- // reward - expected number of rounds (equals the number of times a process receives a counter) rewards - [c12] true : 1; - endrewards + +//---------------------------------------------------------------------------------------------------------------------------- +formula leaders = (s1=4?1:0)+(s2=4?1:0)+(s3=4?1:0)+(s4=4?1:0)+(s5=4?1:0)+(s6=4?1:0)+(s7=4?1:0)+(s8=4?1:0)+(s9=4?1:0)+(s10=4?1:0); +label "elected" = s1=4|s2=4|s3=4|s4=4|s5=4|s6=4|s7=4|s8=4|s9=4|s10=4; + diff --git a/prism-examples/leader/asynchronous/leader3.nm b/prism-examples/leader/asynchronous/leader3.nm index bdbba975..25a3ec89 100644 --- a/prism-examples/leader/asynchronous/leader3.nm +++ b/prism-examples/leader/asynchronous/leader3.nm @@ -1,15 +1,16 @@ -// asynchronous leader election [Itai & Rodeh 1981] -// 3 processes +// asynchronous leader election +// 4 processes // gxn/dxp 29/01/01 mdp -const N=3; // number of processes +const N= 3; // number of processes +//---------------------------------------------------------------------------------------------------------------------------- module process1 // COUNTER - c1 : [0..N-1]; + c1 : [0..3-1]; // STATES s1 : [0..4]; @@ -27,7 +28,6 @@ module process1 // not received anything // received choice // received counter - sent1 : [0..2]; // not send anything // sent choice @@ -69,7 +69,7 @@ module process1 [p31] (s1=3) & (receive1=0) -> (p1'=p3) & (receive1'=1); // receive counter [c31] (s1=3) & (receive1=1) & (c3 (c1'=c3+1) & (receive1'=2); - + // done [done] (s1=4) -> (s1'=s1); // add loop for processes who are inactive @@ -77,13 +77,20 @@ module process1 endmodule +//---------------------------------------------------------------------------------------------------------------------------- + +// construct further stations through renaming module process2=process1[s1=s2,p1=p2,c1=c2,sent1=sent2,receive1=receive2,p12=p23,p31=p12,c12=c23,c31=c12,p3=p1,c3=c1] endmodule module process3=process1[s1=s3,p1=p3,c1=c3,sent1=sent3,receive1=receive3,p12=p31,p31=p23,c12=c31,c31=c23,p3=p2,c3=c2] endmodule +//---------------------------------------------------------------------------------------------------------------------------- + // reward - expected number of rounds (equals the number of times a process receives a counter) rewards - [c12] true : 1; - endrewards +//---------------------------------------------------------------------------------------------------------------------------- +formula leaders = (s1=4?1:0)+(s2=4?1:0)+(s3=4?1:0); +label "elected" = s1=4|s2=4|s3=4; + diff --git a/prism-examples/leader/asynchronous/leader4.nm b/prism-examples/leader/asynchronous/leader4.nm index 7e9d3bd3..81ade2ea 100644 --- a/prism-examples/leader/asynchronous/leader4.nm +++ b/prism-examples/leader/asynchronous/leader4.nm @@ -4,12 +4,13 @@ mdp -const N=4; // number of processes +const N= 4; // number of processes +//---------------------------------------------------------------------------------------------------------------------------- module process1 // COUNTER - c1 : [0..N-1]; + c1 : [0..4-1]; // STATES s1 : [0..4]; @@ -76,13 +77,21 @@ module process1 endmodule +//---------------------------------------------------------------------------------------------------------------------------- + +// construct further stations through renaming module process2=process1[s1=s2,p1=p2,c1=c2,sent1=sent2,receive1=receive2,p12=p23,p41=p12,c12=c23,c41=c12,p4=p1,c4=c1] endmodule module process3=process1[s1=s3,p1=p3,c1=c3,sent1=sent3,receive1=receive3,p12=p34,p41=p23,c12=c34,c41=c23,p4=p2,c4=c2] endmodule module process4=process1[s1=s4,p1=p4,c1=c4,sent1=sent4,receive1=receive4,p12=p41,p41=p34,c12=c41,c41=c34,p4=p3,c4=c3] endmodule +//---------------------------------------------------------------------------------------------------------------------------- + // reward - expected number of rounds (equals the number of times a process receives a counter) rewards - [c12] true : 1; - endrewards + +//---------------------------------------------------------------------------------------------------------------------------- +formula leaders = (s1=4?1:0)+(s2=4?1:0)+(s3=4?1:0)+(s4=4?1:0); +label "elected" = s1=4|s2=4|s3=4|s4=4; + diff --git a/prism-examples/leader/asynchronous/leader5.nm b/prism-examples/leader/asynchronous/leader5.nm index 898b7774..558bab56 100644 --- a/prism-examples/leader/asynchronous/leader5.nm +++ b/prism-examples/leader/asynchronous/leader5.nm @@ -1,15 +1,16 @@ // asynchronous leader election -// 5 processes +// 4 processes // gxn/dxp 29/01/01 mdp -const N=5; // number of processes +const N= 5; // number of processes +//---------------------------------------------------------------------------------------------------------------------------- module process1 // COUNTER - c1 : [0..N-1]; + c1 : [0..5-1]; // STATES s1 : [0..4]; @@ -27,7 +28,6 @@ module process1 // not received anything // received choice // received counter - sent1 : [0..2]; // not send anything // sent choice @@ -69,7 +69,7 @@ module process1 [p51] (s1=3) & (receive1=0) -> (p1'=p5) & (receive1'=1); // receive counter [c51] (s1=3) & (receive1=1) & (c5 (c1'=c5+1) & (receive1'=2); - + // done [done] (s1=4) -> (s1'=s1); // add loop for processes who are inactive @@ -77,14 +77,22 @@ module process1 endmodule +//---------------------------------------------------------------------------------------------------------------------------- + +// construct further stations through renaming module process2=process1[s1=s2,p1=p2,c1=c2,sent1=sent2,receive1=receive2,p12=p23,p51=p12,c12=c23,c51=c12,p5=p1,c5=c1] endmodule module process3=process1[s1=s3,p1=p3,c1=c3,sent1=sent3,receive1=receive3,p12=p34,p51=p23,c12=c34,c51=c23,p5=p2,c5=c2] endmodule module process4=process1[s1=s4,p1=p4,c1=c4,sent1=sent4,receive1=receive4,p12=p45,p51=p34,c12=c45,c51=c34,p5=p3,c5=c3] endmodule module process5=process1[s1=s5,p1=p5,c1=c5,sent1=sent5,receive1=receive5,p12=p51,p51=p45,c12=c51,c51=c45,p5=p4,c5=c4] endmodule +//---------------------------------------------------------------------------------------------------------------------------- + // reward - expected number of rounds (equals the number of times a process receives a counter) rewards - [c12] true : 1; - endrewards + +//---------------------------------------------------------------------------------------------------------------------------- +formula leaders = (s1=4?1:0)+(s2=4?1:0)+(s3=4?1:0)+(s4=4?1:0)+(s5=4?1:0); +label "elected" = s1=4|s2=4|s3=4|s4=4|s5=4; + diff --git a/prism-examples/leader/asynchronous/leader6.nm b/prism-examples/leader/asynchronous/leader6.nm index b122abe9..84b3283a 100644 --- a/prism-examples/leader/asynchronous/leader6.nm +++ b/prism-examples/leader/asynchronous/leader6.nm @@ -1,15 +1,16 @@ // asynchronous leader election -// 6 processes +// 4 processes // gxn/dxp 29/01/01 mdp -const N=6; // number of processes +const N= 6; // number of processes +//---------------------------------------------------------------------------------------------------------------------------- module process1 // COUNTER - c1 : [0..N-1]; + c1 : [0..6-1]; // STATES s1 : [0..4]; @@ -27,7 +28,6 @@ module process1 // not received anything // received choice // received counter - sent1 : [0..2]; // not send anything // sent choice @@ -69,23 +69,31 @@ module process1 [p61] (s1=3) & (receive1=0) -> (p1'=p6) & (receive1'=1); // receive counter [c61] (s1=3) & (receive1=1) & (c6 (c1'=c6+1) & (receive1'=2); - + // done [done] (s1=4) -> (s1'=s1); // add loop for processes who are inactive [done] (s1=3) -> (s1'=s1); - + endmodule +//---------------------------------------------------------------------------------------------------------------------------- + +// construct further stations through renaming module process2=process1[s1=s2,p1=p2,c1=c2,sent1=sent2,receive1=receive2,p12=p23,p61=p12,c12=c23,c61=c12,p6=p1,c6=c1] endmodule module process3=process1[s1=s3,p1=p3,c1=c3,sent1=sent3,receive1=receive3,p12=p34,p61=p23,c12=c34,c61=c23,p6=p2,c6=c2] endmodule module process4=process1[s1=s4,p1=p4,c1=c4,sent1=sent4,receive1=receive4,p12=p45,p61=p34,c12=c45,c61=c34,p6=p3,c6=c3] endmodule module process5=process1[s1=s5,p1=p5,c1=c5,sent1=sent5,receive1=receive5,p12=p56,p61=p45,c12=c56,c61=c45,p6=p4,c6=c4] endmodule module process6=process1[s1=s6,p1=p6,c1=c6,sent1=sent6,receive1=receive6,p12=p61,p61=p56,c12=c61,c61=c56,p6=p5,c6=c5] endmodule +//---------------------------------------------------------------------------------------------------------------------------- + // reward - expected number of rounds (equals the number of times a process receives a counter) rewards - [c12] true : 1; - endrewards + +//---------------------------------------------------------------------------------------------------------------------------- +formula leaders = (s1=4?1:0)+(s2=4?1:0)+(s3=4?1:0)+(s4=4?1:0)+(s5=4?1:0)+(s6=4?1:0); +label "elected" = s1=4|s2=4|s3=4|s4=4|s5=4|s6=4; + diff --git a/prism-examples/leader/asynchronous/leader7.nm b/prism-examples/leader/asynchronous/leader7.nm index 74fb9fe7..fd1a84be 100644 --- a/prism-examples/leader/asynchronous/leader7.nm +++ b/prism-examples/leader/asynchronous/leader7.nm @@ -1,15 +1,16 @@ // asynchronous leader election -// 7 processes +// 4 processes // gxn/dxp 29/01/01 mdp -const N=7; // number of processes +const N= 7; // number of processes +//---------------------------------------------------------------------------------------------------------------------------- module process1 // COUNTER - c1 : [0..N-1]; + c1 : [0..7-1]; // STATES s1 : [0..4]; @@ -27,7 +28,6 @@ module process1 // not received anything // received choice // received counter - sent1 : [0..2]; // not send anything // sent choice @@ -69,14 +69,17 @@ module process1 [p71] (s1=3) & (receive1=0) -> (p1'=p7) & (receive1'=1); // receive counter [c71] (s1=3) & (receive1=1) & (c7 (c1'=c7+1) & (receive1'=2); - + // done [done] (s1=4) -> (s1'=s1); // add loop for processes who are inactive [done] (s1=3) -> (s1'=s1); - + endmodule +//---------------------------------------------------------------------------------------------------------------------------- + +// construct further stations through renaming module process2=process1[s1=s2,p1=p2,c1=c2,sent1=sent2,receive1=receive2,p12=p23,p71=p12,c12=c23,c71=c12,p7=p1,c7=c1] endmodule module process3=process1[s1=s3,p1=p3,c1=c3,sent1=sent3,receive1=receive3,p12=p34,p71=p23,c12=c34,c71=c23,p7=p2,c7=c2] endmodule module process4=process1[s1=s4,p1=p4,c1=c4,sent1=sent4,receive1=receive4,p12=p45,p71=p34,c12=c45,c71=c34,p7=p3,c7=c3] endmodule @@ -84,9 +87,14 @@ module process5=process1[s1=s5,p1=p5,c1=c5,sent1=sent5,receive1=receive5,p12=p56 module process6=process1[s1=s6,p1=p6,c1=c6,sent1=sent6,receive1=receive6,p12=p67,p71=p56,c12=c67,c71=c56,p7=p5,c7=c5] endmodule module process7=process1[s1=s7,p1=p7,c1=c7,sent1=sent7,receive1=receive7,p12=p71,p71=p67,c12=c71,c71=c67,p7=p6,c7=c6] endmodule +//---------------------------------------------------------------------------------------------------------------------------- + // reward - expected number of rounds (equals the number of times a process receives a counter) rewards - [c12] true : 1; - endrewards + +//---------------------------------------------------------------------------------------------------------------------------- +formula leaders = (s1=4?1:0)+(s2=4?1:0)+(s3=4?1:0)+(s4=4?1:0)+(s5=4?1:0)+(s6=4?1:0)+(s7=4?1:0); +label "elected" = s1=4|s2=4|s3=4|s4=4|s5=4|s6=4|s7=4; + diff --git a/prism-examples/leader/asynchronous/leader8.nm b/prism-examples/leader/asynchronous/leader8.nm index 8e54eab1..68b684cf 100644 --- a/prism-examples/leader/asynchronous/leader8.nm +++ b/prism-examples/leader/asynchronous/leader8.nm @@ -1,15 +1,16 @@ // asynchronous leader election -// 8 processes +// 4 processes // gxn/dxp 29/01/01 mdp -const N=8; // number of processes +const N= 8; // number of processes +//---------------------------------------------------------------------------------------------------------------------------- module process1 // COUNTER - c1 : [0..N-1]; + c1 : [0..8-1]; // STATES s1 : [0..4]; @@ -27,7 +28,6 @@ module process1 // not received anything // received choice // received counter - sent1 : [0..2]; // not send anything // sent choice @@ -69,14 +69,17 @@ module process1 [p81] (s1=3) & (receive1=0) -> (p1'=p8) & (receive1'=1); // receive counter [c81] (s1=3) & (receive1=1) & (c8 (c1'=c8+1) & (receive1'=2); - + // done [done] (s1=4) -> (s1'=s1); // add loop for processes who are inactive [done] (s1=3) -> (s1'=s1); - + endmodule +//---------------------------------------------------------------------------------------------------------------------------- + +// construct further stations through renaming module process2=process1[s1=s2,p1=p2,c1=c2,sent1=sent2,receive1=receive2,p12=p23,p81=p12,c12=c23,c81=c12,p8=p1,c8=c1] endmodule module process3=process1[s1=s3,p1=p3,c1=c3,sent1=sent3,receive1=receive3,p12=p34,p81=p23,c12=c34,c81=c23,p8=p2,c8=c2] endmodule module process4=process1[s1=s4,p1=p4,c1=c4,sent1=sent4,receive1=receive4,p12=p45,p81=p34,c12=c45,c81=c34,p8=p3,c8=c3] endmodule @@ -85,9 +88,14 @@ module process6=process1[s1=s6,p1=p6,c1=c6,sent1=sent6,receive1=receive6,p12=p67 module process7=process1[s1=s7,p1=p7,c1=c7,sent1=sent7,receive1=receive7,p12=p78,p81=p67,c12=c78,c81=c67,p8=p6,c8=c6] endmodule module process8=process1[s1=s8,p1=p8,c1=c8,sent1=sent8,receive1=receive8,p12=p81,p81=p78,c12=c81,c81=c78,p8=p7,c8=c7] endmodule +//---------------------------------------------------------------------------------------------------------------------------- + // reward - expected number of rounds (equals the number of times a process receives a counter) rewards - [c12] true : 1; - endrewards + +//---------------------------------------------------------------------------------------------------------------------------- +formula leaders = (s1=4?1:0)+(s2=4?1:0)+(s3=4?1:0)+(s4=4?1:0)+(s5=4?1:0)+(s6=4?1:0)+(s7=4?1:0)+(s8=4?1:0); +label "elected" = s1=4|s2=4|s3=4|s4=4|s5=4|s6=4|s7=4|s8=4; + diff --git a/prism-examples/leader/asynchronous/leader9.nm b/prism-examples/leader/asynchronous/leader9.nm index 5e97366e..3a7d4f56 100644 --- a/prism-examples/leader/asynchronous/leader9.nm +++ b/prism-examples/leader/asynchronous/leader9.nm @@ -1,15 +1,16 @@ // asynchronous leader election -// 9 processes +// 4 processes // gxn/dxp 29/01/01 mdp -const N=9; // number of processes +const N= 9; // number of processes +//---------------------------------------------------------------------------------------------------------------------------- module process1 // COUNTER - c1 : [0..N-1]; + c1 : [0..9-1]; // STATES s1 : [0..4]; @@ -27,7 +28,6 @@ module process1 // not received anything // received choice // received counter - sent1 : [0..2]; // not send anything // sent choice @@ -69,26 +69,34 @@ module process1 [p91] (s1=3) & (receive1=0) -> (p1'=p9) & (receive1'=1); // receive counter [c91] (s1=3) & (receive1=1) & (c9 (c1'=c9+1) & (receive1'=2); - + // done [done] (s1=4) -> (s1'=s1); // add loop for processes who are inactive [done] (s1=3) -> (s1'=s1); - + endmodule +//---------------------------------------------------------------------------------------------------------------------------- + +// construct further stations through renaming module process2=process1[s1=s2,p1=p2,c1=c2,sent1=sent2,receive1=receive2,p12=p23,p91=p12,c12=c23,c91=c12,p9=p1,c9=c1] endmodule module process3=process1[s1=s3,p1=p3,c1=c3,sent1=sent3,receive1=receive3,p12=p34,p91=p23,c12=c34,c91=c23,p9=p2,c9=c2] endmodule module process4=process1[s1=s4,p1=p4,c1=c4,sent1=sent4,receive1=receive4,p12=p45,p91=p34,c12=c45,c91=c34,p9=p3,c9=c3] endmodule module process5=process1[s1=s5,p1=p5,c1=c5,sent1=sent5,receive1=receive5,p12=p56,p91=p45,c12=c56,c91=c45,p9=p4,c9=c4] endmodule module process6=process1[s1=s6,p1=p6,c1=c6,sent1=sent6,receive1=receive6,p12=p67,p91=p56,c12=c67,c91=c56,p9=p5,c9=c5] endmodule -module process7=process1[s1=s7,p1=p7,c1=c7,sent1=sent7,receive1=receive7,p12=p79,p91=p67,c12=c79,c91=c67,p9=p6,c9=c6] endmodule +module process7=process1[s1=s7,p1=p7,c1=c7,sent1=sent7,receive1=receive7,p12=p78,p91=p67,c12=c78,c91=c67,p9=p6,c9=c6] endmodule module process8=process1[s1=s8,p1=p8,c1=c8,sent1=sent8,receive1=receive8,p12=p89,p91=p78,c12=c89,c91=c78,p9=p7,c9=c7] endmodule module process9=process1[s1=s9,p1=p9,c1=c9,sent1=sent9,receive1=receive9,p12=p91,p91=p89,c12=c91,c91=c89,p9=p8,c9=c8] endmodule -// reward - expected number of rounds (equals the number of times a single process receives a counter) +//---------------------------------------------------------------------------------------------------------------------------- + +// reward - expected number of rounds (equals the number of times a process receives a counter) rewards - [c12] true : 1; - endrewards + +//---------------------------------------------------------------------------------------------------------------------------- +formula leaders = (s1=4?1:0)+(s2=4?1:0)+(s3=4?1:0)+(s4=4?1:0)+(s5=4?1:0)+(s6=4?1:0)+(s7=4?1:0)+(s8=4?1:0)+(s9=4?1:0); +label "elected" = s1=4|s2=4|s3=4|s4=4|s5=4|s6=4|s7=4|s8=4|s9=4; +