Tidied up dining cryptographers example.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@498 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism-examples/dining_crypt/.anonymityN.pctl.pp

@@ -1,5 +0,0 @@
-#const N#
-const int k;
-
-Pmin=? [ F (#& j=1:N#s#j#=1#end#) & (#+ j=1:N# #func(floor,func(pow,2,N-j))#*agree#j# #end# = k) {"init"&pay>0}{min} ]
-Pmax=? [ F (#& j=1:N#s#j#=1#end#) & (#+ j=1:N# #func(floor,func(pow,2,N-j))#*agree#j# #end# = k) {"init"&pay>0}{max} ]

prism-examples/dining_crypt/.autopp

@@ -4,8 +4,4 @@ foreach N ( 3 4 5 6 7 8 9 10 15 )
 	echo "Generating for N=$N"
 	prismpp .dining_cryptN.nm.pp $N >! dining_crypt$N.nm
 	unix2dos dining_crypt$N.nm
-	prismpp .correctnessN.pctl.pp $N >! correctness$N.pctl
-	unix2dos correctness$N.pctl
-	prismpp .anonymityN.pctl.pp $N >! anonymity$N.pctl
-	unix2dos anonymity$N.pctl
 end

prism-examples/dining_crypt/.correctnessN.pctl.pp

@@ -1,6 +0,0 @@
-#const N#
-// Correctness for the case where the master pays
-(pay=0) => P>=1 [ F (#& j=1:N#s#j#=1#end#) & func(mod,(#+ j=1:N#agree#j##end#),2)=#func(mod,N,2)# ]
-
-// Correctness for the case where a cryptographer pays
-(pay>0) => P>=1 [ F (#& j=1:N#s#j#=1#end#) & func(mod,(#+ j=1:N#agree#j##end#),2)=#func(mod,N+1,2)# ]

prism-examples/dining_crypt/.dining_cryptN.nm.pp

@@ -4,6 +4,9 @@
 
 mdp
 
+// number of cryptographers
+const int N = #N#;
+
 // constants used in renaming (identities of cryptographers)
 #for i=1:N#
 const int p#i# = #i#;
@@ -11,7 +14,7 @@ const int p#i# = #i#;
 
 // global variable which decides who pays
 // (0 - master pays, i=1..N - cryptographer i pays)
-global pay : [0..#N#];
+global pay : [0..N];
 
 // module for first cryptographer
 module crypt1
@@ -46,3 +49,17 @@ module crypt#i# = crypt1 [ coin1=coin#i#, s1=s#i#, agree1=agree#i#, p1=p#i#, coi
 // set of initial states
 // (cryptographers in their initial state, "pay" can be anything)
 init #& i=1:N# coin#i#=0&s#i#=0&agree#i#=0 #end# endinit
+
+// unique integer representing outcome
+formula outcome = #+ j=1:N# #func(floor,func(pow,2,N-j))#*agree#j# #end#;
+
+// parity of number of "agree"s (0 = even, 1 = odd)
+formula parity = func(mod, #+ j=1:N#agree#j##end#, 2);
+
+// label denoting states where protocol has finished
+label "done" = #& i=1:N#s#i#=1#end#;
+// label denoting states where number of "agree"s is even
+label "even" = func(mod,(#+ i=1:N#agree#i##end#),2)=0;
+// label denoting states where number of "agree"s is even
+label "odd" = func(mod,(#+ i=1:N#agree#i##end#),2)=1;
+

prism-examples/dining_crypt/anonymity.pctl

@@ -0,0 +1,7 @@
+const int k;
+
+// Anonymity - check for k=0..2^N - both min/max should be the same and equal to 1/2^(N-1) or 0
+// (depending on the parity of the number of bits in the binary representation of outcome)
+Pmin=? [ F "done" & outcome = k {"init"&pay>0}{min} ]
+Pmax=? [ F "done" & outcome = k {"init"&pay>0}{max} ]
+

prism-examples/dining_crypt/anonymity10.pctl

@@ -1,4 +0,0 @@
-const int k;
-
-Pmin=? [ F (s1=1&s2=1&s3=1&s4=1&s5=1&s6=1&s7=1&s8=1&s9=1&s10=1) & ( 512*agree1 + 256*agree2 + 128*agree3 + 64*agree4 + 32*agree5 + 16*agree6 + 8*agree7 + 4*agree8 + 2*agree9 + 1*agree10  = k) {"init"&pay>0}{min} ]
-Pmax=? [ F (s1=1&s2=1&s3=1&s4=1&s5=1&s6=1&s7=1&s8=1&s9=1&s10=1) & ( 512*agree1 + 256*agree2 + 128*agree3 + 64*agree4 + 32*agree5 + 16*agree6 + 8*agree7 + 4*agree8 + 2*agree9 + 1*agree10  = k) {"init"&pay>0}{max} ]

prism-examples/dining_crypt/anonymity15.pctl

@@ -1,4 +0,0 @@
-const int k;
-
-Pmin=? [ F (s1=1&s2=1&s3=1&s4=1&s5=1&s6=1&s7=1&s8=1&s9=1&s10=1&s11=1&s12=1&s13=1&s14=1&s15=1) & ( 16384*agree1 + 8192*agree2 + 4096*agree3 + 2048*agree4 + 1024*agree5 + 512*agree6 + 256*agree7 + 128*agree8 + 64*agree9 + 32*agree10 + 16*agree11 + 8*agree12 + 4*agree13 + 2*agree14 + 1*agree15  = k) {"init"&pay>0}{min} ]
-Pmax=? [ F (s1=1&s2=1&s3=1&s4=1&s5=1&s6=1&s7=1&s8=1&s9=1&s10=1&s11=1&s12=1&s13=1&s14=1&s15=1) & ( 16384*agree1 + 8192*agree2 + 4096*agree3 + 2048*agree4 + 1024*agree5 + 512*agree6 + 256*agree7 + 128*agree8 + 64*agree9 + 32*agree10 + 16*agree11 + 8*agree12 + 4*agree13 + 2*agree14 + 1*agree15  = k) {"init"&pay>0}{max} ]

prism-examples/dining_crypt/anonymity3.pctl

@@ -1,4 +0,0 @@
-const int k;
-
-Pmin=? [ F (s1=1&s2=1&s3=1) & ( 4*agree1 + 2*agree2 + 1*agree3  = k) {"init"&pay>0}{min} ]
-Pmax=? [ F (s1=1&s2=1&s3=1) & ( 4*agree1 + 2*agree2 + 1*agree3  = k) {"init"&pay>0}{max} ]

prism-examples/dining_crypt/anonymity4.pctl

@@ -1,4 +0,0 @@
-const int k;
-
-Pmin=? [ F (s1=1&s2=1&s3=1&s4=1) & ( 8*agree1 + 4*agree2 + 2*agree3 + 1*agree4  = k) {"init"&pay>0}{min} ]
-Pmax=? [ F (s1=1&s2=1&s3=1&s4=1) & ( 8*agree1 + 4*agree2 + 2*agree3 + 1*agree4  = k) {"init"&pay>0}{max} ]

prism-examples/dining_crypt/anonymity5.pctl

@@ -1,4 +0,0 @@
-const int k;
-
-Pmin=? [ F (s1=1&s2=1&s3=1&s4=1&s5=1) & ( 16*agree1 + 8*agree2 + 4*agree3 + 2*agree4 + 1*agree5  = k) {"init"&pay>0}{min} ]
-Pmax=? [ F (s1=1&s2=1&s3=1&s4=1&s5=1) & ( 16*agree1 + 8*agree2 + 4*agree3 + 2*agree4 + 1*agree5  = k) {"init"&pay>0}{max} ]

prism-examples/dining_crypt/anonymity6.pctl

@@ -1,4 +0,0 @@
-const int k;
-
-Pmin=? [ F (s1=1&s2=1&s3=1&s4=1&s5=1&s6=1) & ( 32*agree1 + 16*agree2 + 8*agree3 + 4*agree4 + 2*agree5 + 1*agree6  = k) {"init"&pay>0}{min} ]
-Pmax=? [ F (s1=1&s2=1&s3=1&s4=1&s5=1&s6=1) & ( 32*agree1 + 16*agree2 + 8*agree3 + 4*agree4 + 2*agree5 + 1*agree6  = k) {"init"&pay>0}{max} ]

prism-examples/dining_crypt/anonymity7.pctl

@@ -1,4 +0,0 @@
-const int k;
-
-Pmin=? [ F (s1=1&s2=1&s3=1&s4=1&s5=1&s6=1&s7=1) & ( 64*agree1 + 32*agree2 + 16*agree3 + 8*agree4 + 4*agree5 + 2*agree6 + 1*agree7  = k) {"init"&pay>0}{min} ]
-Pmax=? [ F (s1=1&s2=1&s3=1&s4=1&s5=1&s6=1&s7=1) & ( 64*agree1 + 32*agree2 + 16*agree3 + 8*agree4 + 4*agree5 + 2*agree6 + 1*agree7  = k) {"init"&pay>0}{max} ]

prism-examples/dining_crypt/anonymity8.pctl

@@ -1,4 +0,0 @@
-const int k;
-
-Pmin=? [ F (s1=1&s2=1&s3=1&s4=1&s5=1&s6=1&s7=1&s8=1) & ( 128*agree1 + 64*agree2 + 32*agree3 + 16*agree4 + 8*agree5 + 4*agree6 + 2*agree7 + 1*agree8  = k) {"init"&pay>0}{min} ]
-Pmax=? [ F (s1=1&s2=1&s3=1&s4=1&s5=1&s6=1&s7=1&s8=1) & ( 128*agree1 + 64*agree2 + 32*agree3 + 16*agree4 + 8*agree5 + 4*agree6 + 2*agree7 + 1*agree8  = k) {"init"&pay>0}{max} ]

prism-examples/dining_crypt/anonymity9.pctl

@@ -1,4 +0,0 @@
-const int k;
-
-Pmin=? [ F (s1=1&s2=1&s3=1&s4=1&s5=1&s6=1&s7=1&s8=1&s9=1) & ( 256*agree1 + 128*agree2 + 64*agree3 + 32*agree4 + 16*agree5 + 8*agree6 + 4*agree7 + 2*agree8 + 1*agree9  = k) {"init"&pay>0}{min} ]
-Pmax=? [ F (s1=1&s2=1&s3=1&s4=1&s5=1&s6=1&s7=1&s8=1&s9=1) & ( 256*agree1 + 128*agree2 + 64*agree3 + 32*agree4 + 16*agree5 + 8*agree6 + 4*agree7 + 2*agree8 + 1*agree9  = k) {"init"&pay>0}{max} ]

prism-examples/dining_crypt/auto

@@ -1,21 +1,22 @@
 #!/bin/csh
 
-prism dining_crypt3.nm  correctness3.pctl
-prism dining_crypt4.nm  correctness4.pctl
-prism dining_crypt5.nm  correctness5.pctl
-prism dining_crypt6.nm  correctness6.pctl
-prism dining_crypt7.nm  correctness7.pctl
-prism dining_crypt8.nm  correctness8.pctl
-prism dining_crypt9.nm  correctness9.pctl
-prism dining_crypt10.nm correctness10.pctl
-prism dining_crypt15.nm correctness15.pctl
+prism dining_crypt3.nm  correctness.pctl
+prism dining_crypt4.nm  correctness.pctl
+prism dining_crypt5.nm  correctness.pctl
+prism dining_crypt6.nm  correctness.pctl
+prism dining_crypt7.nm  correctness.pctl
+prism dining_crypt8.nm  correctness.pctl
+prism dining_crypt9.nm  correctness.pctl
+prism dining_crypt10.nm correctness.pctl
+prism dining_crypt15.nm correctness.pctl
 
-prism dining_crypt3.nm  anonymity3.pctl  -const k=0 -m -nopre
-prism dining_crypt4.nm  anonymity4.pctl  -const k=1 -m -nopre
-prism dining_crypt5.nm  anonymity5.pctl  -const k=0 -m -nopre
-prism dining_crypt6.nm  anonymity6.pctl  -const k=1 -m -nopre
-prism dining_crypt7.nm  anonymity7.pctl  -const k=0 -m -nopre
-prism dining_crypt8.nm  anonymity8.pctl  -const k=1 -m -nopre
-prism dining_crypt9.nm  anonymity9.pctl  -const k=0 -m -nopre
-prism dining_crypt10.nm anonymity10.pctl -const k=1 -m -nopre
-prism dining_crypt15.nm anonymity15.pctl -const k=0 -m -nopre
+prism dining_crypt3.nm  anonymity.pctl -const k=0:7 -m -nopre -exportresults stdout
+prism dining_crypt4.nm  anonymity.pctl -const k=0:15 -m -nopre -exportresults stdout
+
+prism dining_crypt5.nm  anonymity.pctl -const k=0 -m -nopre
+prism dining_crypt6.nm  anonymity.pctl -const k=1 -m -nopre
+prism dining_crypt7.nm  anonymity.pctl -const k=0 -m -nopre
+prism dining_crypt8.nm  anonymity.pctl -const k=1 -m -nopre
+prism dining_crypt9.nm  anonymity.pctl -const k=0 -m -nopre
+prism dining_crypt10.nm anonymity.pctl -const k=1 -m -nopre
+prism dining_crypt15.nm anonymity.pctl -const k=0 -m -nopre

prism-examples/dining_crypt/correctness.pctl

@@ -0,0 +1,7 @@
+// Correctness for the case where the master pays
+// (final parity of number of number of "agrees"s matches that of N)
+(pay=0) => P>=1 [ F "done" & parity=func(mod, N, 2) ]
+
+// Correctness for the case where a cryptographer pays
+// (final parity of number of number of "agrees"s does not match that of N)
+(pay>0) => P>=1 [ F "done" & parity!=func(mod, N, 2) ]

prism-examples/dining_crypt/correctness10.pctl

@@ -1,5 +0,0 @@
-// Correctness for the case where the master pays
-(pay=0) => P>=1 [ F (s1=1&s2=1&s3=1&s4=1&s5=1&s6=1&s7=1&s8=1&s9=1&s10=1) & func(mod,(agree1+agree2+agree3+agree4+agree5+agree6+agree7+agree8+agree9+agree10),2)=0 ]
-
-// Correctness for the case where a cryptographer pays
-(pay>0) => P>=1 [ F (s1=1&s2=1&s3=1&s4=1&s5=1&s6=1&s7=1&s8=1&s9=1&s10=1) & func(mod,(agree1+agree2+agree3+agree4+agree5+agree6+agree7+agree8+agree9+agree10),2)=1 ]

prism-examples/dining_crypt/correctness15.pctl

@@ -1,5 +0,0 @@
-// Correctness for the case where the master pays
-(pay=0) => P>=1 [ F (s1=1&s2=1&s3=1&s4=1&s5=1&s6=1&s7=1&s8=1&s9=1&s10=1&s11=1&s12=1&s13=1&s14=1&s15=1) & func(mod,(agree1+agree2+agree3+agree4+agree5+agree6+agree7+agree8+agree9+agree10+agree11+agree12+agree13+agree14+agree15),2)=1 ]
-
-// Correctness for the case where a cryptographer pays
-(pay>0) => P>=1 [ F (s1=1&s2=1&s3=1&s4=1&s5=1&s6=1&s7=1&s8=1&s9=1&s10=1&s11=1&s12=1&s13=1&s14=1&s15=1) & func(mod,(agree1+agree2+agree3+agree4+agree5+agree6+agree7+agree8+agree9+agree10+agree11+agree12+agree13+agree14+agree15),2)=0 ]

prism-examples/dining_crypt/correctness3.pctl

@@ -1,5 +0,0 @@
-// Correctness for the case where the master pays
-(pay=0) => P>=1 [ F (s1=1&s2=1&s3=1) & func(mod,(agree1+agree2+agree3),2)=1 ]
-
-// Correctness for the case where a cryptographer pays
-(pay>0) => P>=1 [ F (s1=1&s2=1&s3=1) & func(mod,(agree1+agree2+agree3),2)=0 ]

prism-examples/dining_crypt/correctness4.pctl

@@ -1,5 +0,0 @@
-// Correctness for the case where the master pays
-(pay=0) => P>=1 [ F (s1=1&s2=1&s3=1&s4=1) & func(mod,(agree1+agree2+agree3+agree4),2)=0 ]
-
-// Correctness for the case where a cryptographer pays
-(pay>0) => P>=1 [ F (s1=1&s2=1&s3=1&s4=1) & func(mod,(agree1+agree2+agree3+agree4),2)=1 ]

prism-examples/dining_crypt/correctness5.pctl

@@ -1,5 +0,0 @@
-// Correctness for the case where the master pays
-(pay=0) => P>=1 [ F (s1=1&s2=1&s3=1&s4=1&s5=1) & func(mod,(agree1+agree2+agree3+agree4+agree5),2)=1 ]
-
-// Correctness for the case where a cryptographer pays
-(pay>0) => P>=1 [ F (s1=1&s2=1&s3=1&s4=1&s5=1) & func(mod,(agree1+agree2+agree3+agree4+agree5),2)=0 ]

prism-examples/dining_crypt/correctness6.pctl

@@ -1,5 +0,0 @@
-// Correctness for the case where the master pays
-(pay=0) => P>=1 [ F (s1=1&s2=1&s3=1&s4=1&s5=1&s6=1) & func(mod,(agree1+agree2+agree3+agree4+agree5+agree6),2)=0 ]
-
-// Correctness for the case where a cryptographer pays
-(pay>0) => P>=1 [ F (s1=1&s2=1&s3=1&s4=1&s5=1&s6=1) & func(mod,(agree1+agree2+agree3+agree4+agree5+agree6),2)=1 ]

prism-examples/dining_crypt/correctness7.pctl

@@ -1,5 +0,0 @@
-// Correctness for the case where the master pays
-(pay=0) => P>=1 [ F (s1=1&s2=1&s3=1&s4=1&s5=1&s6=1&s7=1) & func(mod,(agree1+agree2+agree3+agree4+agree5+agree6+agree7),2)=1 ]
-
-// Correctness for the case where a cryptographer pays
-(pay>0) => P>=1 [ F (s1=1&s2=1&s3=1&s4=1&s5=1&s6=1&s7=1) & func(mod,(agree1+agree2+agree3+agree4+agree5+agree6+agree7),2)=0 ]

prism-examples/dining_crypt/correctness8.pctl

@@ -1,5 +0,0 @@
-// Correctness for the case where the master pays
-(pay=0) => P>=1 [ F (s1=1&s2=1&s3=1&s4=1&s5=1&s6=1&s7=1&s8=1) & func(mod,(agree1+agree2+agree3+agree4+agree5+agree6+agree7+agree8),2)=0 ]
-
-// Correctness for the case where a cryptographer pays
-(pay>0) => P>=1 [ F (s1=1&s2=1&s3=1&s4=1&s5=1&s6=1&s7=1&s8=1) & func(mod,(agree1+agree2+agree3+agree4+agree5+agree6+agree7+agree8),2)=1 ]

prism-examples/dining_crypt/correctness9.pctl

@@ -1,5 +0,0 @@
-// Correctness for the case where the master pays
-(pay=0) => P>=1 [ F (s1=1&s2=1&s3=1&s4=1&s5=1&s6=1&s7=1&s8=1&s9=1) & func(mod,(agree1+agree2+agree3+agree4+agree5+agree6+agree7+agree8+agree9),2)=1 ]
-
-// Correctness for the case where a cryptographer pays
-(pay>0) => P>=1 [ F (s1=1&s2=1&s3=1&s4=1&s5=1&s6=1&s7=1&s8=1&s9=1) & func(mod,(agree1+agree2+agree3+agree4+agree5+agree6+agree7+agree8+agree9),2)=0 ]

prism-examples/dining_crypt/dining_crypt10.nm

@@ -3,6 +3,9 @@
 
 mdp
 
+// number of cryptographers
+const int N = 10;
+
 // constants used in renaming (identities of cryptographers)
 const int p1 = 1;
 const int p2 = 2;
@@ -17,7 +20,7 @@ const int p10 = 10;
 
 // global variable which decides who pays
 // (0 - master pays, i=1..N - cryptographer i pays)
-global pay : [0..10];
+global pay : [0..N];
 
 // module for first cryptographer
 module crypt1
@@ -58,3 +61,17 @@ module crypt10 = crypt1 [ coin1=coin10, s1=s10, agree1=agree10, p1=p10, coin2=co
 // set of initial states
 // (cryptographers in their initial state, "pay" can be anything)
 init  coin1=0&s1=0&agree1=0 & coin2=0&s2=0&agree2=0 & coin3=0&s3=0&agree3=0 & coin4=0&s4=0&agree4=0 & coin5=0&s5=0&agree5=0 & coin6=0&s6=0&agree6=0 & coin7=0&s7=0&agree7=0 & coin8=0&s8=0&agree8=0 & coin9=0&s9=0&agree9=0 & coin10=0&s10=0&agree10=0  endinit
+
+// unique integer representing outcome
+formula outcome =  512*agree1 + 256*agree2 + 128*agree3 + 64*agree4 + 32*agree5 + 16*agree6 + 8*agree7 + 4*agree8 + 2*agree9 + 1*agree10 ;
+
+// parity of number of "agree"s (0 = even, 1 = odd)
+formula parity = func(mod, agree1+agree2+agree3+agree4+agree5+agree6+agree7+agree8+agree9+agree10, 2);
+
+// label denoting states where protocol has finished
+label "done" = s1=1&s2=1&s3=1&s4=1&s5=1&s6=1&s7=1&s8=1&s9=1&s10=1;
+// label denoting states where number of "agree"s is even
+label "even" = func(mod,(agree1+agree2+agree3+agree4+agree5+agree6+agree7+agree8+agree9+agree10),2)=0;
+// label denoting states where number of "agree"s is even
+label "odd" = func(mod,(agree1+agree2+agree3+agree4+agree5+agree6+agree7+agree8+agree9+agree10),2)=1;
+

prism-examples/dining_crypt/dining_crypt15.nm

@@ -3,6 +3,9 @@
 
 mdp
 
+// number of cryptographers
+const int N = 15;
+
 // constants used in renaming (identities of cryptographers)
 const int p1 = 1;
 const int p2 = 2;
@@ -22,7 +25,7 @@ const int p15 = 15;
 
 // global variable which decides who pays
 // (0 - master pays, i=1..N - cryptographer i pays)
-global pay : [0..15];
+global pay : [0..N];
 
 // module for first cryptographer
 module crypt1
@@ -68,3 +71,17 @@ module crypt15 = crypt1 [ coin1=coin15, s1=s15, agree1=agree15, p1=p15, coin2=co
 // set of initial states
 // (cryptographers in their initial state, "pay" can be anything)
 init  coin1=0&s1=0&agree1=0 & coin2=0&s2=0&agree2=0 & coin3=0&s3=0&agree3=0 & coin4=0&s4=0&agree4=0 & coin5=0&s5=0&agree5=0 & coin6=0&s6=0&agree6=0 & coin7=0&s7=0&agree7=0 & coin8=0&s8=0&agree8=0 & coin9=0&s9=0&agree9=0 & coin10=0&s10=0&agree10=0 & coin11=0&s11=0&agree11=0 & coin12=0&s12=0&agree12=0 & coin13=0&s13=0&agree13=0 & coin14=0&s14=0&agree14=0 & coin15=0&s15=0&agree15=0  endinit
+
+// unique integer representing outcome
+formula outcome =  16384*agree1 + 8192*agree2 + 4096*agree3 + 2048*agree4 + 1024*agree5 + 512*agree6 + 256*agree7 + 128*agree8 + 64*agree9 + 32*agree10 + 16*agree11 + 8*agree12 + 4*agree13 + 2*agree14 + 1*agree15 ;
+
+// parity of number of "agree"s (0 = even, 1 = odd)
+formula parity = func(mod, agree1+agree2+agree3+agree4+agree5+agree6+agree7+agree8+agree9+agree10+agree11+agree12+agree13+agree14+agree15, 2);
+
+// label denoting states where protocol has finished
+label "done" = s1=1&s2=1&s3=1&s4=1&s5=1&s6=1&s7=1&s8=1&s9=1&s10=1&s11=1&s12=1&s13=1&s14=1&s15=1;
+// label denoting states where number of "agree"s is even
+label "even" = func(mod,(agree1+agree2+agree3+agree4+agree5+agree6+agree7+agree8+agree9+agree10+agree11+agree12+agree13+agree14+agree15),2)=0;
+// label denoting states where number of "agree"s is even
+label "odd" = func(mod,(agree1+agree2+agree3+agree4+agree5+agree6+agree7+agree8+agree9+agree10+agree11+agree12+agree13+agree14+agree15),2)=1;
+

prism-examples/dining_crypt/dining_crypt3.nm

@@ -3,6 +3,9 @@
 
 mdp
 
+// number of cryptographers
+const int N = 3;
+
 // constants used in renaming (identities of cryptographers)
 const int p1 = 1;
 const int p2 = 2;
@@ -10,7 +13,7 @@ const int p3 = 3;
 
 // global variable which decides who pays
 // (0 - master pays, i=1..N - cryptographer i pays)
-global pay : [0..3];
+global pay : [0..N];
 
 // module for first cryptographer
 module crypt1
@@ -44,3 +47,17 @@ module crypt3 = crypt1 [ coin1=coin3, s1=s3, agree1=agree3, p1=p3, coin2=coin1 ]
 // set of initial states
 // (cryptographers in their initial state, "pay" can be anything)
 init  coin1=0&s1=0&agree1=0 & coin2=0&s2=0&agree2=0 & coin3=0&s3=0&agree3=0  endinit
+
+// unique integer representing outcome
+formula outcome =  4*agree1 + 2*agree2 + 1*agree3 ;
+
+// parity of number of "agree"s (0 = even, 1 = odd)
+formula parity = func(mod, agree1+agree2+agree3, 2);
+
+// label denoting states where protocol has finished
+label "done" = s1=1&s2=1&s3=1;
+// label denoting states where number of "agree"s is even
+label "even" = func(mod,(agree1+agree2+agree3),2)=0;
+// label denoting states where number of "agree"s is even
+label "odd" = func(mod,(agree1+agree2+agree3),2)=1;
+

prism-examples/dining_crypt/dining_crypt4.nm

@@ -3,6 +3,9 @@
 
 mdp
 
+// number of cryptographers
+const int N = 4;
+
 // constants used in renaming (identities of cryptographers)
 const int p1 = 1;
 const int p2 = 2;
@@ -11,7 +14,7 @@ const int p4 = 4;
 
 // global variable which decides who pays
 // (0 - master pays, i=1..N - cryptographer i pays)
-global pay : [0..4];
+global pay : [0..N];
 
 // module for first cryptographer
 module crypt1
@@ -46,3 +49,17 @@ module crypt4 = crypt1 [ coin1=coin4, s1=s4, agree1=agree4, p1=p4, coin2=coin1 ]
 // set of initial states
 // (cryptographers in their initial state, "pay" can be anything)
 init  coin1=0&s1=0&agree1=0 & coin2=0&s2=0&agree2=0 & coin3=0&s3=0&agree3=0 & coin4=0&s4=0&agree4=0  endinit
+
+// unique integer representing outcome
+formula outcome =  8*agree1 + 4*agree2 + 2*agree3 + 1*agree4 ;
+
+// parity of number of "agree"s (0 = even, 1 = odd)
+formula parity = func(mod, agree1+agree2+agree3+agree4, 2);
+
+// label denoting states where protocol has finished
+label "done" = s1=1&s2=1&s3=1&s4=1;
+// label denoting states where number of "agree"s is even
+label "even" = func(mod,(agree1+agree2+agree3+agree4),2)=0;
+// label denoting states where number of "agree"s is even
+label "odd" = func(mod,(agree1+agree2+agree3+agree4),2)=1;
+

prism-examples/dining_crypt/dining_crypt5.nm

@@ -3,6 +3,9 @@
 
 mdp
 
+// number of cryptographers
+const int N = 5;
+
 // constants used in renaming (identities of cryptographers)
 const int p1 = 1;
 const int p2 = 2;
@@ -12,7 +15,7 @@ const int p5 = 5;
 
 // global variable which decides who pays
 // (0 - master pays, i=1..N - cryptographer i pays)
-global pay : [0..5];
+global pay : [0..N];
 
 // module for first cryptographer
 module crypt1
@@ -48,3 +51,17 @@ module crypt5 = crypt1 [ coin1=coin5, s1=s5, agree1=agree5, p1=p5, coin2=coin1 ]
 // set of initial states
 // (cryptographers in their initial state, "pay" can be anything)
 init  coin1=0&s1=0&agree1=0 & coin2=0&s2=0&agree2=0 & coin3=0&s3=0&agree3=0 & coin4=0&s4=0&agree4=0 & coin5=0&s5=0&agree5=0  endinit
+
+// unique integer representing outcome
+formula outcome =  16*agree1 + 8*agree2 + 4*agree3 + 2*agree4 + 1*agree5 ;
+
+// parity of number of "agree"s (0 = even, 1 = odd)
+formula parity = func(mod, agree1+agree2+agree3+agree4+agree5, 2);
+
+// label denoting states where protocol has finished
+label "done" = s1=1&s2=1&s3=1&s4=1&s5=1;
+// label denoting states where number of "agree"s is even
+label "even" = func(mod,(agree1+agree2+agree3+agree4+agree5),2)=0;
+// label denoting states where number of "agree"s is even
+label "odd" = func(mod,(agree1+agree2+agree3+agree4+agree5),2)=1;
+

prism-examples/dining_crypt/dining_crypt6.nm

@@ -3,6 +3,9 @@
 
 mdp
 
+// number of cryptographers
+const int N = 6;
+
 // constants used in renaming (identities of cryptographers)
 const int p1 = 1;
 const int p2 = 2;
@@ -13,7 +16,7 @@ const int p6 = 6;
 
 // global variable which decides who pays
 // (0 - master pays, i=1..N - cryptographer i pays)
-global pay : [0..6];
+global pay : [0..N];
 
 // module for first cryptographer
 module crypt1
@@ -50,3 +53,17 @@ module crypt6 = crypt1 [ coin1=coin6, s1=s6, agree1=agree6, p1=p6, coin2=coin1 ]
 // set of initial states
 // (cryptographers in their initial state, "pay" can be anything)
 init  coin1=0&s1=0&agree1=0 & coin2=0&s2=0&agree2=0 & coin3=0&s3=0&agree3=0 & coin4=0&s4=0&agree4=0 & coin5=0&s5=0&agree5=0 & coin6=0&s6=0&agree6=0  endinit
+
+// unique integer representing outcome
+formula outcome =  32*agree1 + 16*agree2 + 8*agree3 + 4*agree4 + 2*agree5 + 1*agree6 ;
+
+// parity of number of "agree"s (0 = even, 1 = odd)
+formula parity = func(mod, agree1+agree2+agree3+agree4+agree5+agree6, 2);
+
+// label denoting states where protocol has finished
+label "done" = s1=1&s2=1&s3=1&s4=1&s5=1&s6=1;
+// label denoting states where number of "agree"s is even
+label "even" = func(mod,(agree1+agree2+agree3+agree4+agree5+agree6),2)=0;
+// label denoting states where number of "agree"s is even
+label "odd" = func(mod,(agree1+agree2+agree3+agree4+agree5+agree6),2)=1;
+

prism-examples/dining_crypt/dining_crypt7.nm

@@ -3,6 +3,9 @@
 
 mdp
 
+// number of cryptographers
+const int N = 7;
+
 // constants used in renaming (identities of cryptographers)
 const int p1 = 1;
 const int p2 = 2;
@@ -14,7 +17,7 @@ const int p7 = 7;
 
 // global variable which decides who pays
 // (0 - master pays, i=1..N - cryptographer i pays)
-global pay : [0..7];
+global pay : [0..N];
 
 // module for first cryptographer
 module crypt1
@@ -52,3 +55,17 @@ module crypt7 = crypt1 [ coin1=coin7, s1=s7, agree1=agree7, p1=p7, coin2=coin1 ]
 // set of initial states
 // (cryptographers in their initial state, "pay" can be anything)
 init  coin1=0&s1=0&agree1=0 & coin2=0&s2=0&agree2=0 & coin3=0&s3=0&agree3=0 & coin4=0&s4=0&agree4=0 & coin5=0&s5=0&agree5=0 & coin6=0&s6=0&agree6=0 & coin7=0&s7=0&agree7=0  endinit
+
+// unique integer representing outcome
+formula outcome =  64*agree1 + 32*agree2 + 16*agree3 + 8*agree4 + 4*agree5 + 2*agree6 + 1*agree7 ;
+
+// parity of number of "agree"s (0 = even, 1 = odd)
+formula parity = func(mod, agree1+agree2+agree3+agree4+agree5+agree6+agree7, 2);
+
+// label denoting states where protocol has finished
+label "done" = s1=1&s2=1&s3=1&s4=1&s5=1&s6=1&s7=1;
+// label denoting states where number of "agree"s is even
+label "even" = func(mod,(agree1+agree2+agree3+agree4+agree5+agree6+agree7),2)=0;
+// label denoting states where number of "agree"s is even
+label "odd" = func(mod,(agree1+agree2+agree3+agree4+agree5+agree6+agree7),2)=1;
+

prism-examples/dining_crypt/dining_crypt8.nm

@@ -3,6 +3,9 @@
 
 mdp
 
+// number of cryptographers
+const int N = 8;
+
 // constants used in renaming (identities of cryptographers)
 const int p1 = 1;
 const int p2 = 2;
@@ -15,7 +18,7 @@ const int p8 = 8;
 
 // global variable which decides who pays
 // (0 - master pays, i=1..N - cryptographer i pays)
-global pay : [0..8];
+global pay : [0..N];
 
 // module for first cryptographer
 module crypt1
@@ -54,3 +57,17 @@ module crypt8 = crypt1 [ coin1=coin8, s1=s8, agree1=agree8, p1=p8, coin2=coin1 ]
 // set of initial states
 // (cryptographers in their initial state, "pay" can be anything)
 init  coin1=0&s1=0&agree1=0 & coin2=0&s2=0&agree2=0 & coin3=0&s3=0&agree3=0 & coin4=0&s4=0&agree4=0 & coin5=0&s5=0&agree5=0 & coin6=0&s6=0&agree6=0 & coin7=0&s7=0&agree7=0 & coin8=0&s8=0&agree8=0  endinit
+
+// unique integer representing outcome
+formula outcome =  128*agree1 + 64*agree2 + 32*agree3 + 16*agree4 + 8*agree5 + 4*agree6 + 2*agree7 + 1*agree8 ;
+
+// parity of number of "agree"s (0 = even, 1 = odd)
+formula parity = func(mod, agree1+agree2+agree3+agree4+agree5+agree6+agree7+agree8, 2);
+
+// label denoting states where protocol has finished
+label "done" = s1=1&s2=1&s3=1&s4=1&s5=1&s6=1&s7=1&s8=1;
+// label denoting states where number of "agree"s is even
+label "even" = func(mod,(agree1+agree2+agree3+agree4+agree5+agree6+agree7+agree8),2)=0;
+// label denoting states where number of "agree"s is even
+label "odd" = func(mod,(agree1+agree2+agree3+agree4+agree5+agree6+agree7+agree8),2)=1;
+

prism-examples/dining_crypt/dining_crypt9.nm

@@ -3,6 +3,9 @@
 
 mdp
 
+// number of cryptographers
+const int N = 9;
+
 // constants used in renaming (identities of cryptographers)
 const int p1 = 1;
 const int p2 = 2;
@@ -16,7 +19,7 @@ const int p9 = 9;
 
 // global variable which decides who pays
 // (0 - master pays, i=1..N - cryptographer i pays)
-global pay : [0..9];
+global pay : [0..N];
 
 // module for first cryptographer
 module crypt1
@@ -56,3 +59,17 @@ module crypt9 = crypt1 [ coin1=coin9, s1=s9, agree1=agree9, p1=p9, coin2=coin1 ]
 // set of initial states
 // (cryptographers in their initial state, "pay" can be anything)
 init  coin1=0&s1=0&agree1=0 & coin2=0&s2=0&agree2=0 & coin3=0&s3=0&agree3=0 & coin4=0&s4=0&agree4=0 & coin5=0&s5=0&agree5=0 & coin6=0&s6=0&agree6=0 & coin7=0&s7=0&agree7=0 & coin8=0&s8=0&agree8=0 & coin9=0&s9=0&agree9=0  endinit
+
+// unique integer representing outcome
+formula outcome =  256*agree1 + 128*agree2 + 64*agree3 + 32*agree4 + 16*agree5 + 8*agree6 + 4*agree7 + 2*agree8 + 1*agree9 ;
+
+// parity of number of "agree"s (0 = even, 1 = odd)
+formula parity = func(mod, agree1+agree2+agree3+agree4+agree5+agree6+agree7+agree8+agree9, 2);
+
+// label denoting states where protocol has finished
+label "done" = s1=1&s2=1&s3=1&s4=1&s5=1&s6=1&s7=1&s8=1&s9=1;
+// label denoting states where number of "agree"s is even
+label "even" = func(mod,(agree1+agree2+agree3+agree4+agree5+agree6+agree7+agree8+agree9),2)=0;
+// label denoting states where number of "agree"s is even
+label "odd" = func(mod,(agree1+agree2+agree3+agree4+agree5+agree6+agree7+agree8+agree9),2)=1;
+