Dining cryptographers example.

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

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

@@ -0,0 +1,5 @@
+#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

@@ -0,0 +1,11 @@
+#!/bin/csh
+
+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

@@ -0,0 +1,6 @@
+#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

@@ -0,0 +1,48 @@
+#const N#
+// model of dining cryptographers
+// gxn/dxp 15/11/06
+
+mdp
+
+// constants used in renaming (identities of cryptographers)
+#for i=1:N#
+const int p#i# = #i#;
+#end#
+
+// global variable which decides who pays
+// (0 - master pays, i=1..N - cryptographer i pays)
+global pay : [0..#N#];
+
+// module for first cryptographer
+module crypt1
+	
+	coin1 : [0..2]; // value of its coin
+	s1 : [0..1]; // its status (0 = not done, 1 = done)
+	agree1 : [0..1]; // what it states (0 = disagree, 1 = agree)
+	
+	// flip coin
+	[] coin1=0 -> 0.5 : (coin1'=1) + 0.5 : (coin1'=2);
+	
+	// make statement (once relevant coins have been flipped)
+	// agree (coins the same and does not pay)
+	[] s1=0 & coin1>0 & coin2>0 & coin1=coin2    & (pay!=p1) -> (s1'=1) & (agree1'=1);
+	// disagree (coins different and does not pay)
+	[] s1=0 & coin1>0 & coin2>0 & !(coin1=coin2) & (pay!=p1) -> (s1'=1);
+	// disagree (coins the same and pays)
+	[] s1=0 & coin1>0 & coin2>0 & coin1=coin2    & (pay=p1)  -> (s1'=1);
+	// agree (coins different and pays)
+	[] s1=0 & coin1>0 & coin2>0 & !(coin1=coin2) & (pay=p1)  -> (s1'=1) & (agree1'=1);
+	
+	// synchronising loop when finished to avoid deadlock
+	[done] s1=1 -> true;
+
+endmodule
+
+// construct further cryptographers with renaming
+#for i=2:N#
+module crypt#i# = crypt1 [ coin1=coin#i#, s1=s#i#, agree1=agree#i#, p1=p#i#, coin2=coin#func(mod,i,N)+1# ] endmodule
+#end#
+
+// 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

prism-examples/dining_crypt/README

@@ -0,0 +1,10 @@
+This case study is based on the well known dining cryptographers problem [Cha88].
+
+For more information, see: http://www.prismmodelchecker.org/casestudies/dining_crypt.php
+
+=====================================================================================
+
+[Cha88]
+D. Chaum
+The Dining Cryptographers Problem: Unconditional Sender and Recipient Untraceability
+Journal of Cryptology, vol. 1, pp 65-75, 1988

prism-examples/dining_crypt/anonymity10.pctl

@@ -0,0 +1,4 @@
+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

@@ -0,0 +1,4 @@
+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

@@ -0,0 +1,4 @@
+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

@@ -0,0 +1,4 @@
+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

@@ -0,0 +1,4 @@
+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

@@ -0,0 +1,4 @@
+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

@@ -0,0 +1,4 @@
+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

@@ -0,0 +1,4 @@
+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

@@ -0,0 +1,4 @@
+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

@@ -0,0 +1,21 @@
+#!/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  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-examples/dining_crypt/correctness10.pctl

@@ -0,0 +1,5 @@
+// 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

@@ -0,0 +1,5 @@
+// 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

@@ -0,0 +1,5 @@
+// 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

@@ -0,0 +1,5 @@
+// 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

@@ -0,0 +1,5 @@
+// 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

@@ -0,0 +1,5 @@
+// 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

@@ -0,0 +1,5 @@
+// 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

@@ -0,0 +1,5 @@
+// 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

@@ -0,0 +1,5 @@
+// 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

@@ -0,0 +1,60 @@
+// model of dining cryptographers
+// gxn/dxp 15/11/06
+
+mdp
+
+// constants used in renaming (identities of cryptographers)
+const int p1 = 1;
+const int p2 = 2;
+const int p3 = 3;
+const int p4 = 4;
+const int p5 = 5;
+const int p6 = 6;
+const int p7 = 7;
+const int p8 = 8;
+const int p9 = 9;
+const int p10 = 10;
+
+// global variable which decides who pays
+// (0 - master pays, i=1..N - cryptographer i pays)
+global pay : [0..10];
+
+// module for first cryptographer
+module crypt1
+	
+	coin1 : [0..2]; // value of its coin
+	s1 : [0..1]; // its status (0 = not done, 1 = done)
+	agree1 : [0..1]; // what it states (0 = disagree, 1 = agree)
+	
+	// flip coin
+	[] coin1=0 -> 0.5 : (coin1'=1) + 0.5 : (coin1'=2);
+	
+	// make statement (once relevant coins have been flipped)
+	// agree (coins the same and does not pay)
+	[] s1=0 & coin1>0 & coin2>0 & coin1=coin2    & (pay!=p1) -> (s1'=1) & (agree1'=1);
+	// disagree (coins different and does not pay)
+	[] s1=0 & coin1>0 & coin2>0 & !(coin1=coin2) & (pay!=p1) -> (s1'=1);
+	// disagree (coins the same and pays)
+	[] s1=0 & coin1>0 & coin2>0 & coin1=coin2    & (pay=p1)  -> (s1'=1);
+	// agree (coins different and pays)
+	[] s1=0 & coin1>0 & coin2>0 & !(coin1=coin2) & (pay=p1)  -> (s1'=1) & (agree1'=1);
+	
+	// synchronising loop when finished to avoid deadlock
+	[done] s1=1 -> true;
+
+endmodule
+
+// construct further cryptographers with renaming
+module crypt2 = crypt1 [ coin1=coin2, s1=s2, agree1=agree2, p1=p2, coin2=coin3 ] endmodule
+module crypt3 = crypt1 [ coin1=coin3, s1=s3, agree1=agree3, p1=p3, coin2=coin4 ] endmodule
+module crypt4 = crypt1 [ coin1=coin4, s1=s4, agree1=agree4, p1=p4, coin2=coin5 ] endmodule
+module crypt5 = crypt1 [ coin1=coin5, s1=s5, agree1=agree5, p1=p5, coin2=coin6 ] endmodule
+module crypt6 = crypt1 [ coin1=coin6, s1=s6, agree1=agree6, p1=p6, coin2=coin7 ] endmodule
+module crypt7 = crypt1 [ coin1=coin7, s1=s7, agree1=agree7, p1=p7, coin2=coin8 ] endmodule
+module crypt8 = crypt1 [ coin1=coin8, s1=s8, agree1=agree8, p1=p8, coin2=coin9 ] endmodule
+module crypt9 = crypt1 [ coin1=coin9, s1=s9, agree1=agree9, p1=p9, coin2=coin10 ] endmodule
+module crypt10 = crypt1 [ coin1=coin10, s1=s10, agree1=agree10, p1=p10, coin2=coin1 ] endmodule
+
+// 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

prism-examples/dining_crypt/dining_crypt15.nm

@@ -0,0 +1,70 @@
+// model of dining cryptographers
+// gxn/dxp 15/11/06
+
+mdp
+
+// constants used in renaming (identities of cryptographers)
+const int p1 = 1;
+const int p2 = 2;
+const int p3 = 3;
+const int p4 = 4;
+const int p5 = 5;
+const int p6 = 6;
+const int p7 = 7;
+const int p8 = 8;
+const int p9 = 9;
+const int p10 = 10;
+const int p11 = 11;
+const int p12 = 12;
+const int p13 = 13;
+const int p14 = 14;
+const int p15 = 15;
+
+// global variable which decides who pays
+// (0 - master pays, i=1..N - cryptographer i pays)
+global pay : [0..15];
+
+// module for first cryptographer
+module crypt1
+	
+	coin1 : [0..2]; // value of its coin
+	s1 : [0..1]; // its status (0 = not done, 1 = done)
+	agree1 : [0..1]; // what it states (0 = disagree, 1 = agree)
+	
+	// flip coin
+	[] coin1=0 -> 0.5 : (coin1'=1) + 0.5 : (coin1'=2);
+	
+	// make statement (once relevant coins have been flipped)
+	// agree (coins the same and does not pay)
+	[] s1=0 & coin1>0 & coin2>0 & coin1=coin2    & (pay!=p1) -> (s1'=1) & (agree1'=1);
+	// disagree (coins different and does not pay)
+	[] s1=0 & coin1>0 & coin2>0 & !(coin1=coin2) & (pay!=p1) -> (s1'=1);
+	// disagree (coins the same and pays)
+	[] s1=0 & coin1>0 & coin2>0 & coin1=coin2    & (pay=p1)  -> (s1'=1);
+	// agree (coins different and pays)
+	[] s1=0 & coin1>0 & coin2>0 & !(coin1=coin2) & (pay=p1)  -> (s1'=1) & (agree1'=1);
+	
+	// synchronising loop when finished to avoid deadlock
+	[done] s1=1 -> true;
+
+endmodule
+
+// construct further cryptographers with renaming
+module crypt2 = crypt1 [ coin1=coin2, s1=s2, agree1=agree2, p1=p2, coin2=coin3 ] endmodule
+module crypt3 = crypt1 [ coin1=coin3, s1=s3, agree1=agree3, p1=p3, coin2=coin4 ] endmodule
+module crypt4 = crypt1 [ coin1=coin4, s1=s4, agree1=agree4, p1=p4, coin2=coin5 ] endmodule
+module crypt5 = crypt1 [ coin1=coin5, s1=s5, agree1=agree5, p1=p5, coin2=coin6 ] endmodule
+module crypt6 = crypt1 [ coin1=coin6, s1=s6, agree1=agree6, p1=p6, coin2=coin7 ] endmodule
+module crypt7 = crypt1 [ coin1=coin7, s1=s7, agree1=agree7, p1=p7, coin2=coin8 ] endmodule
+module crypt8 = crypt1 [ coin1=coin8, s1=s8, agree1=agree8, p1=p8, coin2=coin9 ] endmodule
+module crypt9 = crypt1 [ coin1=coin9, s1=s9, agree1=agree9, p1=p9, coin2=coin10 ] endmodule
+module crypt10 = crypt1 [ coin1=coin10, s1=s10, agree1=agree10, p1=p10, coin2=coin11 ] endmodule
+module crypt11 = crypt1 [ coin1=coin11, s1=s11, agree1=agree11, p1=p11, coin2=coin12 ] endmodule
+module crypt12 = crypt1 [ coin1=coin12, s1=s12, agree1=agree12, p1=p12, coin2=coin13 ] endmodule
+module crypt13 = crypt1 [ coin1=coin13, s1=s13, agree1=agree13, p1=p13, coin2=coin14 ] endmodule
+module crypt14 = crypt1 [ coin1=coin14, s1=s14, agree1=agree14, p1=p14, coin2=coin15 ] endmodule
+module crypt15 = crypt1 [ coin1=coin15, s1=s15, agree1=agree15, p1=p15, coin2=coin1 ] endmodule
+
+// 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

prism-examples/dining_crypt/dining_crypt3.nm

@@ -0,0 +1,46 @@
+// model of dining cryptographers
+// gxn/dxp 15/11/06
+
+mdp
+
+// constants used in renaming (identities of cryptographers)
+const int p1 = 1;
+const int p2 = 2;
+const int p3 = 3;
+
+// global variable which decides who pays
+// (0 - master pays, i=1..N - cryptographer i pays)
+global pay : [0..3];
+
+// module for first cryptographer
+module crypt1
+	
+	coin1 : [0..2]; // value of its coin
+	s1 : [0..1]; // its status (0 = not done, 1 = done)
+	agree1 : [0..1]; // what it states (0 = disagree, 1 = agree)
+	
+	// flip coin
+	[] coin1=0 -> 0.5 : (coin1'=1) + 0.5 : (coin1'=2);
+	
+	// make statement (once relevant coins have been flipped)
+	// agree (coins the same and does not pay)
+	[] s1=0 & coin1>0 & coin2>0 & coin1=coin2    & (pay!=p1) -> (s1'=1) & (agree1'=1);
+	// disagree (coins different and does not pay)
+	[] s1=0 & coin1>0 & coin2>0 & !(coin1=coin2) & (pay!=p1) -> (s1'=1);
+	// disagree (coins the same and pays)
+	[] s1=0 & coin1>0 & coin2>0 & coin1=coin2    & (pay=p1)  -> (s1'=1);
+	// agree (coins different and pays)
+	[] s1=0 & coin1>0 & coin2>0 & !(coin1=coin2) & (pay=p1)  -> (s1'=1) & (agree1'=1);
+	
+	// synchronising loop when finished to avoid deadlock
+	[done] s1=1 -> true;
+
+endmodule
+
+// construct further cryptographers with renaming
+module crypt2 = crypt1 [ coin1=coin2, s1=s2, agree1=agree2, p1=p2, coin2=coin3 ] endmodule
+module crypt3 = crypt1 [ coin1=coin3, s1=s3, agree1=agree3, p1=p3, coin2=coin1 ] endmodule
+
+// 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

prism-examples/dining_crypt/dining_crypt4.nm

@@ -0,0 +1,48 @@
+// model of dining cryptographers
+// gxn/dxp 15/11/06
+
+mdp
+
+// constants used in renaming (identities of cryptographers)
+const int p1 = 1;
+const int p2 = 2;
+const int p3 = 3;
+const int p4 = 4;
+
+// global variable which decides who pays
+// (0 - master pays, i=1..N - cryptographer i pays)
+global pay : [0..4];
+
+// module for first cryptographer
+module crypt1
+	
+	coin1 : [0..2]; // value of its coin
+	s1 : [0..1]; // its status (0 = not done, 1 = done)
+	agree1 : [0..1]; // what it states (0 = disagree, 1 = agree)
+	
+	// flip coin
+	[] coin1=0 -> 0.5 : (coin1'=1) + 0.5 : (coin1'=2);
+	
+	// make statement (once relevant coins have been flipped)
+	// agree (coins the same and does not pay)
+	[] s1=0 & coin1>0 & coin2>0 & coin1=coin2    & (pay!=p1) -> (s1'=1) & (agree1'=1);
+	// disagree (coins different and does not pay)
+	[] s1=0 & coin1>0 & coin2>0 & !(coin1=coin2) & (pay!=p1) -> (s1'=1);
+	// disagree (coins the same and pays)
+	[] s1=0 & coin1>0 & coin2>0 & coin1=coin2    & (pay=p1)  -> (s1'=1);
+	// agree (coins different and pays)
+	[] s1=0 & coin1>0 & coin2>0 & !(coin1=coin2) & (pay=p1)  -> (s1'=1) & (agree1'=1);
+	
+	// synchronising loop when finished to avoid deadlock
+	[done] s1=1 -> true;
+
+endmodule
+
+// construct further cryptographers with renaming
+module crypt2 = crypt1 [ coin1=coin2, s1=s2, agree1=agree2, p1=p2, coin2=coin3 ] endmodule
+module crypt3 = crypt1 [ coin1=coin3, s1=s3, agree1=agree3, p1=p3, coin2=coin4 ] endmodule
+module crypt4 = crypt1 [ coin1=coin4, s1=s4, agree1=agree4, p1=p4, coin2=coin1 ] endmodule
+
+// 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

prism-examples/dining_crypt/dining_crypt5.nm

@@ -0,0 +1,50 @@
+// model of dining cryptographers
+// gxn/dxp 15/11/06
+
+mdp
+
+// constants used in renaming (identities of cryptographers)
+const int p1 = 1;
+const int p2 = 2;
+const int p3 = 3;
+const int p4 = 4;
+const int p5 = 5;
+
+// global variable which decides who pays
+// (0 - master pays, i=1..N - cryptographer i pays)
+global pay : [0..5];
+
+// module for first cryptographer
+module crypt1
+	
+	coin1 : [0..2]; // value of its coin
+	s1 : [0..1]; // its status (0 = not done, 1 = done)
+	agree1 : [0..1]; // what it states (0 = disagree, 1 = agree)
+	
+	// flip coin
+	[] coin1=0 -> 0.5 : (coin1'=1) + 0.5 : (coin1'=2);
+	
+	// make statement (once relevant coins have been flipped)
+	// agree (coins the same and does not pay)
+	[] s1=0 & coin1>0 & coin2>0 & coin1=coin2    & (pay!=p1) -> (s1'=1) & (agree1'=1);
+	// disagree (coins different and does not pay)
+	[] s1=0 & coin1>0 & coin2>0 & !(coin1=coin2) & (pay!=p1) -> (s1'=1);
+	// disagree (coins the same and pays)
+	[] s1=0 & coin1>0 & coin2>0 & coin1=coin2    & (pay=p1)  -> (s1'=1);
+	// agree (coins different and pays)
+	[] s1=0 & coin1>0 & coin2>0 & !(coin1=coin2) & (pay=p1)  -> (s1'=1) & (agree1'=1);
+	
+	// synchronising loop when finished to avoid deadlock
+	[done] s1=1 -> true;
+
+endmodule
+
+// construct further cryptographers with renaming
+module crypt2 = crypt1 [ coin1=coin2, s1=s2, agree1=agree2, p1=p2, coin2=coin3 ] endmodule
+module crypt3 = crypt1 [ coin1=coin3, s1=s3, agree1=agree3, p1=p3, coin2=coin4 ] endmodule
+module crypt4 = crypt1 [ coin1=coin4, s1=s4, agree1=agree4, p1=p4, coin2=coin5 ] endmodule
+module crypt5 = crypt1 [ coin1=coin5, s1=s5, agree1=agree5, p1=p5, coin2=coin1 ] endmodule
+
+// 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

prism-examples/dining_crypt/dining_crypt6.nm

@@ -0,0 +1,52 @@
+// model of dining cryptographers
+// gxn/dxp 15/11/06
+
+mdp
+
+// constants used in renaming (identities of cryptographers)
+const int p1 = 1;
+const int p2 = 2;
+const int p3 = 3;
+const int p4 = 4;
+const int p5 = 5;
+const int p6 = 6;
+
+// global variable which decides who pays
+// (0 - master pays, i=1..N - cryptographer i pays)
+global pay : [0..6];
+
+// module for first cryptographer
+module crypt1
+	
+	coin1 : [0..2]; // value of its coin
+	s1 : [0..1]; // its status (0 = not done, 1 = done)
+	agree1 : [0..1]; // what it states (0 = disagree, 1 = agree)
+	
+	// flip coin
+	[] coin1=0 -> 0.5 : (coin1'=1) + 0.5 : (coin1'=2);
+	
+	// make statement (once relevant coins have been flipped)
+	// agree (coins the same and does not pay)
+	[] s1=0 & coin1>0 & coin2>0 & coin1=coin2    & (pay!=p1) -> (s1'=1) & (agree1'=1);
+	// disagree (coins different and does not pay)
+	[] s1=0 & coin1>0 & coin2>0 & !(coin1=coin2) & (pay!=p1) -> (s1'=1);
+	// disagree (coins the same and pays)
+	[] s1=0 & coin1>0 & coin2>0 & coin1=coin2    & (pay=p1)  -> (s1'=1);
+	// agree (coins different and pays)
+	[] s1=0 & coin1>0 & coin2>0 & !(coin1=coin2) & (pay=p1)  -> (s1'=1) & (agree1'=1);
+	
+	// synchronising loop when finished to avoid deadlock
+	[done] s1=1 -> true;
+
+endmodule
+
+// construct further cryptographers with renaming
+module crypt2 = crypt1 [ coin1=coin2, s1=s2, agree1=agree2, p1=p2, coin2=coin3 ] endmodule
+module crypt3 = crypt1 [ coin1=coin3, s1=s3, agree1=agree3, p1=p3, coin2=coin4 ] endmodule
+module crypt4 = crypt1 [ coin1=coin4, s1=s4, agree1=agree4, p1=p4, coin2=coin5 ] endmodule
+module crypt5 = crypt1 [ coin1=coin5, s1=s5, agree1=agree5, p1=p5, coin2=coin6 ] endmodule
+module crypt6 = crypt1 [ coin1=coin6, s1=s6, agree1=agree6, p1=p6, coin2=coin1 ] endmodule
+
+// 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

prism-examples/dining_crypt/dining_crypt7.nm

@@ -0,0 +1,54 @@
+// model of dining cryptographers
+// gxn/dxp 15/11/06
+
+mdp
+
+// constants used in renaming (identities of cryptographers)
+const int p1 = 1;
+const int p2 = 2;
+const int p3 = 3;
+const int p4 = 4;
+const int p5 = 5;
+const int p6 = 6;
+const int p7 = 7;
+
+// global variable which decides who pays
+// (0 - master pays, i=1..N - cryptographer i pays)
+global pay : [0..7];
+
+// module for first cryptographer
+module crypt1
+	
+	coin1 : [0..2]; // value of its coin
+	s1 : [0..1]; // its status (0 = not done, 1 = done)
+	agree1 : [0..1]; // what it states (0 = disagree, 1 = agree)
+	
+	// flip coin
+	[] coin1=0 -> 0.5 : (coin1'=1) + 0.5 : (coin1'=2);
+	
+	// make statement (once relevant coins have been flipped)
+	// agree (coins the same and does not pay)
+	[] s1=0 & coin1>0 & coin2>0 & coin1=coin2    & (pay!=p1) -> (s1'=1) & (agree1'=1);
+	// disagree (coins different and does not pay)
+	[] s1=0 & coin1>0 & coin2>0 & !(coin1=coin2) & (pay!=p1) -> (s1'=1);
+	// disagree (coins the same and pays)
+	[] s1=0 & coin1>0 & coin2>0 & coin1=coin2    & (pay=p1)  -> (s1'=1);
+	// agree (coins different and pays)
+	[] s1=0 & coin1>0 & coin2>0 & !(coin1=coin2) & (pay=p1)  -> (s1'=1) & (agree1'=1);
+	
+	// synchronising loop when finished to avoid deadlock
+	[done] s1=1 -> true;
+
+endmodule
+
+// construct further cryptographers with renaming
+module crypt2 = crypt1 [ coin1=coin2, s1=s2, agree1=agree2, p1=p2, coin2=coin3 ] endmodule
+module crypt3 = crypt1 [ coin1=coin3, s1=s3, agree1=agree3, p1=p3, coin2=coin4 ] endmodule
+module crypt4 = crypt1 [ coin1=coin4, s1=s4, agree1=agree4, p1=p4, coin2=coin5 ] endmodule
+module crypt5 = crypt1 [ coin1=coin5, s1=s5, agree1=agree5, p1=p5, coin2=coin6 ] endmodule
+module crypt6 = crypt1 [ coin1=coin6, s1=s6, agree1=agree6, p1=p6, coin2=coin7 ] endmodule
+module crypt7 = crypt1 [ coin1=coin7, s1=s7, agree1=agree7, p1=p7, coin2=coin1 ] endmodule
+
+// 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

prism-examples/dining_crypt/dining_crypt8.nm

@@ -0,0 +1,56 @@
+// model of dining cryptographers
+// gxn/dxp 15/11/06
+
+mdp
+
+// constants used in renaming (identities of cryptographers)
+const int p1 = 1;
+const int p2 = 2;
+const int p3 = 3;
+const int p4 = 4;
+const int p5 = 5;
+const int p6 = 6;
+const int p7 = 7;
+const int p8 = 8;
+
+// global variable which decides who pays
+// (0 - master pays, i=1..N - cryptographer i pays)
+global pay : [0..8];
+
+// module for first cryptographer
+module crypt1
+	
+	coin1 : [0..2]; // value of its coin
+	s1 : [0..1]; // its status (0 = not done, 1 = done)
+	agree1 : [0..1]; // what it states (0 = disagree, 1 = agree)
+	
+	// flip coin
+	[] coin1=0 -> 0.5 : (coin1'=1) + 0.5 : (coin1'=2);
+	
+	// make statement (once relevant coins have been flipped)
+	// agree (coins the same and does not pay)
+	[] s1=0 & coin1>0 & coin2>0 & coin1=coin2    & (pay!=p1) -> (s1'=1) & (agree1'=1);
+	// disagree (coins different and does not pay)
+	[] s1=0 & coin1>0 & coin2>0 & !(coin1=coin2) & (pay!=p1) -> (s1'=1);
+	// disagree (coins the same and pays)
+	[] s1=0 & coin1>0 & coin2>0 & coin1=coin2    & (pay=p1)  -> (s1'=1);
+	// agree (coins different and pays)
+	[] s1=0 & coin1>0 & coin2>0 & !(coin1=coin2) & (pay=p1)  -> (s1'=1) & (agree1'=1);
+	
+	// synchronising loop when finished to avoid deadlock
+	[done] s1=1 -> true;
+
+endmodule
+
+// construct further cryptographers with renaming
+module crypt2 = crypt1 [ coin1=coin2, s1=s2, agree1=agree2, p1=p2, coin2=coin3 ] endmodule
+module crypt3 = crypt1 [ coin1=coin3, s1=s3, agree1=agree3, p1=p3, coin2=coin4 ] endmodule
+module crypt4 = crypt1 [ coin1=coin4, s1=s4, agree1=agree4, p1=p4, coin2=coin5 ] endmodule
+module crypt5 = crypt1 [ coin1=coin5, s1=s5, agree1=agree5, p1=p5, coin2=coin6 ] endmodule
+module crypt6 = crypt1 [ coin1=coin6, s1=s6, agree1=agree6, p1=p6, coin2=coin7 ] endmodule
+module crypt7 = crypt1 [ coin1=coin7, s1=s7, agree1=agree7, p1=p7, coin2=coin8 ] endmodule
+module crypt8 = crypt1 [ coin1=coin8, s1=s8, agree1=agree8, p1=p8, coin2=coin1 ] endmodule
+
+// 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

prism-examples/dining_crypt/dining_crypt9.nm

@@ -0,0 +1,58 @@
+// model of dining cryptographers
+// gxn/dxp 15/11/06
+
+mdp
+
+// constants used in renaming (identities of cryptographers)
+const int p1 = 1;
+const int p2 = 2;
+const int p3 = 3;
+const int p4 = 4;
+const int p5 = 5;
+const int p6 = 6;
+const int p7 = 7;
+const int p8 = 8;
+const int p9 = 9;
+
+// global variable which decides who pays
+// (0 - master pays, i=1..N - cryptographer i pays)
+global pay : [0..9];
+
+// module for first cryptographer
+module crypt1
+	
+	coin1 : [0..2]; // value of its coin
+	s1 : [0..1]; // its status (0 = not done, 1 = done)
+	agree1 : [0..1]; // what it states (0 = disagree, 1 = agree)
+	
+	// flip coin
+	[] coin1=0 -> 0.5 : (coin1'=1) + 0.5 : (coin1'=2);
+	
+	// make statement (once relevant coins have been flipped)
+	// agree (coins the same and does not pay)
+	[] s1=0 & coin1>0 & coin2>0 & coin1=coin2    & (pay!=p1) -> (s1'=1) & (agree1'=1);
+	// disagree (coins different and does not pay)
+	[] s1=0 & coin1>0 & coin2>0 & !(coin1=coin2) & (pay!=p1) -> (s1'=1);
+	// disagree (coins the same and pays)
+	[] s1=0 & coin1>0 & coin2>0 & coin1=coin2    & (pay=p1)  -> (s1'=1);
+	// agree (coins different and pays)
+	[] s1=0 & coin1>0 & coin2>0 & !(coin1=coin2) & (pay=p1)  -> (s1'=1) & (agree1'=1);
+	
+	// synchronising loop when finished to avoid deadlock
+	[done] s1=1 -> true;
+
+endmodule
+
+// construct further cryptographers with renaming
+module crypt2 = crypt1 [ coin1=coin2, s1=s2, agree1=agree2, p1=p2, coin2=coin3 ] endmodule
+module crypt3 = crypt1 [ coin1=coin3, s1=s3, agree1=agree3, p1=p3, coin2=coin4 ] endmodule
+module crypt4 = crypt1 [ coin1=coin4, s1=s4, agree1=agree4, p1=p4, coin2=coin5 ] endmodule
+module crypt5 = crypt1 [ coin1=coin5, s1=s5, agree1=agree5, p1=p5, coin2=coin6 ] endmodule
+module crypt6 = crypt1 [ coin1=coin6, s1=s6, agree1=agree6, p1=p6, coin2=coin7 ] endmodule
+module crypt7 = crypt1 [ coin1=coin7, s1=s7, agree1=agree7, p1=p7, coin2=coin8 ] endmodule
+module crypt8 = crypt1 [ coin1=coin8, s1=s8, agree1=agree8, p1=p8, coin2=coin9 ] endmodule
+module crypt9 = crypt1 [ coin1=coin9, s1=s9, agree1=agree9, p1=p9, coin2=coin1 ] endmodule
+
+// 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