Added peer2peer example.

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

prism-examples/peer2peer/.autopp

@@ -0,0 +1,10 @@
+#!/bin/csh
+
+foreach N (4 5)
+  foreach K (4 5 6 7 8)
+	echo "Generating for N=$N, K=$K"
+    prismpp .peer2peerN_K.sm.pp $N $K  >! peer2peer"$N"_"$K".sm
+	unix2dos peer2peer"$N"_"$K".sm
+  end
+end
+

prism-examples/peer2peer/.peer2peerN_K.sm.pp

@@ -0,0 +1,53 @@
+// Simple peer-to-peer file distribution protocol based on BitTorrent
+// gxn/dxp Jan 2006
+
+ctmc
+
+#const N#
+#const K#
+// N=#N# clients, K=#K# blocks to be downloaded
+// Actually there are N+1=#N+1# clients, one of which has all blocks initially
+
+// Rate of block download for a single source
+const double mu=2;
+
+// Rate of download of block i:
+// A client can download from the single client which starts with all blocks
+// or from anyone that has subsequently downloaded it.
+// Total number of concurrent downloads for each block is 4.
+#for j=1:K#
+formula rate#j#=mu*(1+min(3,#+ i=1:N#b#i##j##end#));
+#end#
+
+// client 1
+module client1
+	
+	// bij - has client i downloaded block j yet?
+	#for j=1:K#
+	b1#j# : [0..1];
+	#end#
+	
+	// Downloading of each block (see rate computations above)
+	#for j=1:K#
+	[] b1#j#=0 -> rate#j# : (b1#j#'=1);
+	#end#
+	
+endmodule
+
+// construct remaining clients through renaming
+#for i=2:N#
+module client#i#=client1[b11=b#i#1#for j=2:K#,b1#j#=b#i##j##end#,b#i#1=b11#for j=2:K#,b#i##j#=b1#j##end#] endmodule
+#end#
+
+// labels
+#for i=1:N#
+label "done#i#" = #+ j=1:K#b#i##j##end# = #K#; // client #i# has received all blocks
+#end#
+label "done" = #+ i=1:N#(#+ j=1:K#b#i##j##end#)#end# = #N*K#; // all clients have received all blocks
+
+// reward: fraction of blocks received
+rewards "frac_rec"
+#for i=1:N#
+	true : ((#+ j=1:K#b#i##j##end#)/#K#)/#N#;
+#end#
+endrewards

prism-examples/peer2peer/README

@@ -0,0 +1,6 @@
+This case study models a very simple peer-to-peer protocol, loosely based on BitTorrent.
+
+For more information, see: http://www.prismmodelchecker.org/casestudies/peer2peer.php
+
+=====================================================================================
+

prism-examples/peer2peer/auto

@@ -0,0 +1,9 @@
+#!/bin/csh
+
+foreach N (4 5)
+  foreach K (4 5 6 7 8)
+    prism peer2peer"$N"_"$K".sm peer2peer.csl -fixdl -const T=0:0.01:1.5
+  end
+end
+
+

prism-examples/peer2peer/peer2peer.csl

@@ -0,0 +1,8 @@
+const double T; // time bound
+
+// probability that all clients have received all blocks by time T
+P=? [ true U<=T  "done"  ]
+
+// expected fraction of blocks received by time T
+R=? [ I=T ]
+

prism-examples/peer2peer/peer2peer4_4.sm

@@ -0,0 +1,56 @@
+// Simple peer-to-peer file distribution protocol based on BitTorrent
+// gxn/dxp Jan 2006
+
+ctmc
+
+// N=4 clients, K=4 blocks to be downloaded
+// Actually there are N+1=5 clients, one of which has all blocks initially
+
+// Rate of block download for a single source
+const double mu=2;
+
+// Rate of download of block i:
+// A client can download from the single client which starts with all blocks
+// or from anyone that has subsequently downloaded it.
+// Total number of concurrent downloads for each block is 4.
+formula rate1=mu*(1+min(3,b11+b21+b31+b41));
+formula rate2=mu*(1+min(3,b12+b22+b32+b42));
+formula rate3=mu*(1+min(3,b13+b23+b33+b43));
+formula rate4=mu*(1+min(3,b14+b24+b34+b44));
+
+// client 1
+module client1
+	
+	// bij - has client i downloaded block j yet?
+	b11 : [0..1];
+	b12 : [0..1];
+	b13 : [0..1];
+	b14 : [0..1];
+	
+	// Downloading of each block (see rate computations above)
+	[] b11=0 -> rate1 : (b11'=1);
+	[] b12=0 -> rate2 : (b12'=1);
+	[] b13=0 -> rate3 : (b13'=1);
+	[] b14=0 -> rate4 : (b14'=1);
+	
+endmodule
+
+// construct remaining clients through renaming
+module client2=client1[b11=b21,b12=b22,b13=b23,b14=b24,b21=b11,b22=b12,b23=b13,b24=b14] endmodule
+module client3=client1[b11=b31,b12=b32,b13=b33,b14=b34,b31=b11,b32=b12,b33=b13,b34=b14] endmodule
+module client4=client1[b11=b41,b12=b42,b13=b43,b14=b44,b41=b11,b42=b12,b43=b13,b44=b14] endmodule
+
+// labels
+label "done1" = b11+b12+b13+b14 = 4; // client 1 has received all blocks
+label "done2" = b21+b22+b23+b24 = 4; // client 2 has received all blocks
+label "done3" = b31+b32+b33+b34 = 4; // client 3 has received all blocks
+label "done4" = b41+b42+b43+b44 = 4; // client 4 has received all blocks
+label "done" = (b11+b12+b13+b14)+(b21+b22+b23+b24)+(b31+b32+b33+b34)+(b41+b42+b43+b44) = 16; // all clients have received all blocks
+
+// reward: fraction of blocks received
+rewards "frac_rec"
+	true : ((b11+b12+b13+b14)/4)/4;
+	true : ((b21+b22+b23+b24)/4)/4;
+	true : ((b31+b32+b33+b34)/4)/4;
+	true : ((b41+b42+b43+b44)/4)/4;
+endrewards

prism-examples/peer2peer/peer2peer4_5.sm

@@ -0,0 +1,59 @@
+// Simple peer-to-peer file distribution protocol based on BitTorrent
+// gxn/dxp Jan 2006
+
+ctmc
+
+// N=4 clients, K=5 blocks to be downloaded
+// Actually there are N+1=5 clients, one of which has all blocks initially
+
+// Rate of block download for a single source
+const double mu=2;
+
+// Rate of download of block i:
+// A client can download from the single client which starts with all blocks
+// or from anyone that has subsequently downloaded it.
+// Total number of concurrent downloads for each block is 4.
+formula rate1=mu*(1+min(3,b11+b21+b31+b41));
+formula rate2=mu*(1+min(3,b12+b22+b32+b42));
+formula rate3=mu*(1+min(3,b13+b23+b33+b43));
+formula rate4=mu*(1+min(3,b14+b24+b34+b44));
+formula rate5=mu*(1+min(3,b15+b25+b35+b45));
+
+// client 1
+module client1
+	
+	// bij - has client i downloaded block j yet?
+	b11 : [0..1];
+	b12 : [0..1];
+	b13 : [0..1];
+	b14 : [0..1];
+	b15 : [0..1];
+	
+	// Downloading of each block (see rate computations above)
+	[] b11=0 -> rate1 : (b11'=1);
+	[] b12=0 -> rate2 : (b12'=1);
+	[] b13=0 -> rate3 : (b13'=1);
+	[] b14=0 -> rate4 : (b14'=1);
+	[] b15=0 -> rate5 : (b15'=1);
+	
+endmodule
+
+// construct remaining clients through renaming
+module client2=client1[b11=b21,b12=b22,b13=b23,b14=b24,b15=b25,b21=b11,b22=b12,b23=b13,b24=b14,b25=b15] endmodule
+module client3=client1[b11=b31,b12=b32,b13=b33,b14=b34,b15=b35,b31=b11,b32=b12,b33=b13,b34=b14,b35=b15] endmodule
+module client4=client1[b11=b41,b12=b42,b13=b43,b14=b44,b15=b45,b41=b11,b42=b12,b43=b13,b44=b14,b45=b15] endmodule
+
+// labels
+label "done1" = b11+b12+b13+b14+b15 = 5; // client 1 has received all blocks
+label "done2" = b21+b22+b23+b24+b25 = 5; // client 2 has received all blocks
+label "done3" = b31+b32+b33+b34+b35 = 5; // client 3 has received all blocks
+label "done4" = b41+b42+b43+b44+b45 = 5; // client 4 has received all blocks
+label "done" = (b11+b12+b13+b14+b15)+(b21+b22+b23+b24+b25)+(b31+b32+b33+b34+b35)+(b41+b42+b43+b44+b45) = 20; // all clients have received all blocks
+
+// reward: fraction of blocks received
+rewards "frac_rec"
+	true : ((b11+b12+b13+b14+b15)/5)/4;
+	true : ((b21+b22+b23+b24+b25)/5)/4;
+	true : ((b31+b32+b33+b34+b35)/5)/4;
+	true : ((b41+b42+b43+b44+b45)/5)/4;
+endrewards

prism-examples/peer2peer/peer2peer4_6.sm

@@ -0,0 +1,62 @@
+// Simple peer-to-peer file distribution protocol based on BitTorrent
+// gxn/dxp Jan 2006
+
+ctmc
+
+// N=4 clients, K=6 blocks to be downloaded
+// Actually there are N+1=5 clients, one of which has all blocks initially
+
+// Rate of block download for a single source
+const double mu=2;
+
+// Rate of download of block i:
+// A client can download from the single client which starts with all blocks
+// or from anyone that has subsequently downloaded it.
+// Total number of concurrent downloads for each block is 4.
+formula rate1=mu*(1+min(3,b11+b21+b31+b41));
+formula rate2=mu*(1+min(3,b12+b22+b32+b42));
+formula rate3=mu*(1+min(3,b13+b23+b33+b43));
+formula rate4=mu*(1+min(3,b14+b24+b34+b44));
+formula rate5=mu*(1+min(3,b15+b25+b35+b45));
+formula rate6=mu*(1+min(3,b16+b26+b36+b46));
+
+// client 1
+module client1
+	
+	// bij - has client i downloaded block j yet?
+	b11 : [0..1];
+	b12 : [0..1];
+	b13 : [0..1];
+	b14 : [0..1];
+	b15 : [0..1];
+	b16 : [0..1];
+	
+	// Downloading of each block (see rate computations above)
+	[] b11=0 -> rate1 : (b11'=1);
+	[] b12=0 -> rate2 : (b12'=1);
+	[] b13=0 -> rate3 : (b13'=1);
+	[] b14=0 -> rate4 : (b14'=1);
+	[] b15=0 -> rate5 : (b15'=1);
+	[] b16=0 -> rate6 : (b16'=1);
+	
+endmodule
+
+// construct remaining clients through renaming
+module client2=client1[b11=b21,b12=b22,b13=b23,b14=b24,b15=b25,b16=b26,b21=b11,b22=b12,b23=b13,b24=b14,b25=b15,b26=b16] endmodule
+module client3=client1[b11=b31,b12=b32,b13=b33,b14=b34,b15=b35,b16=b36,b31=b11,b32=b12,b33=b13,b34=b14,b35=b15,b36=b16] endmodule
+module client4=client1[b11=b41,b12=b42,b13=b43,b14=b44,b15=b45,b16=b46,b41=b11,b42=b12,b43=b13,b44=b14,b45=b15,b46=b16] endmodule
+
+// labels
+label "done1" = b11+b12+b13+b14+b15+b16 = 6; // client 1 has received all blocks
+label "done2" = b21+b22+b23+b24+b25+b26 = 6; // client 2 has received all blocks
+label "done3" = b31+b32+b33+b34+b35+b36 = 6; // client 3 has received all blocks
+label "done4" = b41+b42+b43+b44+b45+b46 = 6; // client 4 has received all blocks
+label "done" = (b11+b12+b13+b14+b15+b16)+(b21+b22+b23+b24+b25+b26)+(b31+b32+b33+b34+b35+b36)+(b41+b42+b43+b44+b45+b46) = 24; // all clients have received all blocks
+
+// reward: fraction of blocks received
+rewards "frac_rec"
+	true : ((b11+b12+b13+b14+b15+b16)/6)/4;
+	true : ((b21+b22+b23+b24+b25+b26)/6)/4;
+	true : ((b31+b32+b33+b34+b35+b36)/6)/4;
+	true : ((b41+b42+b43+b44+b45+b46)/6)/4;
+endrewards

prism-examples/peer2peer/peer2peer4_7.sm

@@ -0,0 +1,65 @@
+// Simple peer-to-peer file distribution protocol based on BitTorrent
+// gxn/dxp Jan 2006
+
+ctmc
+
+// N=4 clients, K=7 blocks to be downloaded
+// Actually there are N+1=5 clients, one of which has all blocks initially
+
+// Rate of block download for a single source
+const double mu=2;
+
+// Rate of download of block i:
+// A client can download from the single client which starts with all blocks
+// or from anyone that has subsequently downloaded it.
+// Total number of concurrent downloads for each block is 4.
+formula rate1=mu*(1+min(3,b11+b21+b31+b41));
+formula rate2=mu*(1+min(3,b12+b22+b32+b42));
+formula rate3=mu*(1+min(3,b13+b23+b33+b43));
+formula rate4=mu*(1+min(3,b14+b24+b34+b44));
+formula rate5=mu*(1+min(3,b15+b25+b35+b45));
+formula rate6=mu*(1+min(3,b16+b26+b36+b46));
+formula rate7=mu*(1+min(3,b17+b27+b37+b47));
+
+// client 1
+module client1
+	
+	// bij - has client i downloaded block j yet?
+	b11 : [0..1];
+	b12 : [0..1];
+	b13 : [0..1];
+	b14 : [0..1];
+	b15 : [0..1];
+	b16 : [0..1];
+	b17 : [0..1];
+	
+	// Downloading of each block (see rate computations above)
+	[] b11=0 -> rate1 : (b11'=1);
+	[] b12=0 -> rate2 : (b12'=1);
+	[] b13=0 -> rate3 : (b13'=1);
+	[] b14=0 -> rate4 : (b14'=1);
+	[] b15=0 -> rate5 : (b15'=1);
+	[] b16=0 -> rate6 : (b16'=1);
+	[] b17=0 -> rate7 : (b17'=1);
+	
+endmodule
+
+// construct remaining clients through renaming
+module client2=client1[b11=b21,b12=b22,b13=b23,b14=b24,b15=b25,b16=b26,b17=b27,b21=b11,b22=b12,b23=b13,b24=b14,b25=b15,b26=b16,b27=b17] endmodule
+module client3=client1[b11=b31,b12=b32,b13=b33,b14=b34,b15=b35,b16=b36,b17=b37,b31=b11,b32=b12,b33=b13,b34=b14,b35=b15,b36=b16,b37=b17] endmodule
+module client4=client1[b11=b41,b12=b42,b13=b43,b14=b44,b15=b45,b16=b46,b17=b47,b41=b11,b42=b12,b43=b13,b44=b14,b45=b15,b46=b16,b47=b17] endmodule
+
+// labels
+label "done1" = b11+b12+b13+b14+b15+b16+b17 = 7; // client 1 has received all blocks
+label "done2" = b21+b22+b23+b24+b25+b26+b27 = 7; // client 2 has received all blocks
+label "done3" = b31+b32+b33+b34+b35+b36+b37 = 7; // client 3 has received all blocks
+label "done4" = b41+b42+b43+b44+b45+b46+b47 = 7; // client 4 has received all blocks
+label "done" = (b11+b12+b13+b14+b15+b16+b17)+(b21+b22+b23+b24+b25+b26+b27)+(b31+b32+b33+b34+b35+b36+b37)+(b41+b42+b43+b44+b45+b46+b47) = 28; // all clients have received all blocks
+
+// reward: fraction of blocks received
+rewards "frac_rec"
+	true : ((b11+b12+b13+b14+b15+b16+b17)/7)/4;
+	true : ((b21+b22+b23+b24+b25+b26+b27)/7)/4;
+	true : ((b31+b32+b33+b34+b35+b36+b37)/7)/4;
+	true : ((b41+b42+b43+b44+b45+b46+b47)/7)/4;
+endrewards

prism-examples/peer2peer/peer2peer4_8.sm

@@ -0,0 +1,68 @@
+// Simple peer-to-peer file distribution protocol based on BitTorrent
+// gxn/dxp Jan 2006
+
+ctmc
+
+// N=4 clients, K=8 blocks to be downloaded
+// Actually there are N+1=5 clients, one of which has all blocks initially
+
+// Rate of block download for a single source
+const double mu=2;
+
+// Rate of download of block i:
+// A client can download from the single client which starts with all blocks
+// or from anyone that has subsequently downloaded it.
+// Total number of concurrent downloads for each block is 4.
+formula rate1=mu*(1+min(3,b11+b21+b31+b41));
+formula rate2=mu*(1+min(3,b12+b22+b32+b42));
+formula rate3=mu*(1+min(3,b13+b23+b33+b43));
+formula rate4=mu*(1+min(3,b14+b24+b34+b44));
+formula rate5=mu*(1+min(3,b15+b25+b35+b45));
+formula rate6=mu*(1+min(3,b16+b26+b36+b46));
+formula rate7=mu*(1+min(3,b17+b27+b37+b47));
+formula rate8=mu*(1+min(3,b18+b28+b38+b48));
+
+// client 1
+module client1
+	
+	// bij - has client i downloaded block j yet?
+	b11 : [0..1];
+	b12 : [0..1];
+	b13 : [0..1];
+	b14 : [0..1];
+	b15 : [0..1];
+	b16 : [0..1];
+	b17 : [0..1];
+	b18 : [0..1];
+	
+	// Downloading of each block (see rate computations above)
+	[] b11=0 -> rate1 : (b11'=1);
+	[] b12=0 -> rate2 : (b12'=1);
+	[] b13=0 -> rate3 : (b13'=1);
+	[] b14=0 -> rate4 : (b14'=1);
+	[] b15=0 -> rate5 : (b15'=1);
+	[] b16=0 -> rate6 : (b16'=1);
+	[] b17=0 -> rate7 : (b17'=1);
+	[] b18=0 -> rate8 : (b18'=1);
+	
+endmodule
+
+// construct remaining clients through renaming
+module client2=client1[b11=b21,b12=b22,b13=b23,b14=b24,b15=b25,b16=b26,b17=b27,b18=b28,b21=b11,b22=b12,b23=b13,b24=b14,b25=b15,b26=b16,b27=b17,b28=b18] endmodule
+module client3=client1[b11=b31,b12=b32,b13=b33,b14=b34,b15=b35,b16=b36,b17=b37,b18=b38,b31=b11,b32=b12,b33=b13,b34=b14,b35=b15,b36=b16,b37=b17,b38=b18] endmodule
+module client4=client1[b11=b41,b12=b42,b13=b43,b14=b44,b15=b45,b16=b46,b17=b47,b18=b48,b41=b11,b42=b12,b43=b13,b44=b14,b45=b15,b46=b16,b47=b17,b48=b18] endmodule
+
+// labels
+label "done1" = b11+b12+b13+b14+b15+b16+b17+b18 = 8; // client 1 has received all blocks
+label "done2" = b21+b22+b23+b24+b25+b26+b27+b28 = 8; // client 2 has received all blocks
+label "done3" = b31+b32+b33+b34+b35+b36+b37+b38 = 8; // client 3 has received all blocks
+label "done4" = b41+b42+b43+b44+b45+b46+b47+b48 = 8; // client 4 has received all blocks
+label "done" = (b11+b12+b13+b14+b15+b16+b17+b18)+(b21+b22+b23+b24+b25+b26+b27+b28)+(b31+b32+b33+b34+b35+b36+b37+b38)+(b41+b42+b43+b44+b45+b46+b47+b48) = 32; // all clients have received all blocks
+
+// reward: fraction of blocks received
+rewards "frac_rec"
+	true : ((b11+b12+b13+b14+b15+b16+b17+b18)/8)/4;
+	true : ((b21+b22+b23+b24+b25+b26+b27+b28)/8)/4;
+	true : ((b31+b32+b33+b34+b35+b36+b37+b38)/8)/4;
+	true : ((b41+b42+b43+b44+b45+b46+b47+b48)/8)/4;
+endrewards

prism-examples/peer2peer/peer2peer5_4.sm

@@ -0,0 +1,59 @@
+// Simple peer-to-peer file distribution protocol based on BitTorrent
+// gxn/dxp Jan 2006
+
+ctmc
+
+// N=5 clients, K=4 blocks to be downloaded
+// Actually there are N+1=6 clients, one of which has all blocks initially
+
+// Rate of block download for a single source
+const double mu=2;
+
+// Rate of download of block i:
+// A client can download from the single client which starts with all blocks
+// or from anyone that has subsequently downloaded it.
+// Total number of concurrent downloads for each block is 4.
+formula rate1=mu*(1+min(3,b11+b21+b31+b41+b51));
+formula rate2=mu*(1+min(3,b12+b22+b32+b42+b52));
+formula rate3=mu*(1+min(3,b13+b23+b33+b43+b53));
+formula rate4=mu*(1+min(3,b14+b24+b34+b44+b54));
+
+// client 1
+module client1
+	
+	// bij - has client i downloaded block j yet?
+	b11 : [0..1];
+	b12 : [0..1];
+	b13 : [0..1];
+	b14 : [0..1];
+	
+	// Downloading of each block (see rate computations above)
+	[] b11=0 -> rate1 : (b11'=1);
+	[] b12=0 -> rate2 : (b12'=1);
+	[] b13=0 -> rate3 : (b13'=1);
+	[] b14=0 -> rate4 : (b14'=1);
+	
+endmodule
+
+// construct remaining clients through renaming
+module client2=client1[b11=b21,b12=b22,b13=b23,b14=b24,b21=b11,b22=b12,b23=b13,b24=b14] endmodule
+module client3=client1[b11=b31,b12=b32,b13=b33,b14=b34,b31=b11,b32=b12,b33=b13,b34=b14] endmodule
+module client4=client1[b11=b41,b12=b42,b13=b43,b14=b44,b41=b11,b42=b12,b43=b13,b44=b14] endmodule
+module client5=client1[b11=b51,b12=b52,b13=b53,b14=b54,b51=b11,b52=b12,b53=b13,b54=b14] endmodule
+
+// labels
+label "done1" = b11+b12+b13+b14 = 4; // client 1 has received all blocks
+label "done2" = b21+b22+b23+b24 = 4; // client 2 has received all blocks
+label "done3" = b31+b32+b33+b34 = 4; // client 3 has received all blocks
+label "done4" = b41+b42+b43+b44 = 4; // client 4 has received all blocks
+label "done5" = b51+b52+b53+b54 = 4; // client 5 has received all blocks
+label "done" = (b11+b12+b13+b14)+(b21+b22+b23+b24)+(b31+b32+b33+b34)+(b41+b42+b43+b44)+(b51+b52+b53+b54) = 20; // all clients have received all blocks
+
+// reward: fraction of blocks received
+rewards "frac_rec"
+	true : ((b11+b12+b13+b14)/4)/5;
+	true : ((b21+b22+b23+b24)/4)/5;
+	true : ((b31+b32+b33+b34)/4)/5;
+	true : ((b41+b42+b43+b44)/4)/5;
+	true : ((b51+b52+b53+b54)/4)/5;
+endrewards

prism-examples/peer2peer/peer2peer5_5.sm

@@ -0,0 +1,62 @@
+// Simple peer-to-peer file distribution protocol based on BitTorrent
+// gxn/dxp Jan 2006
+
+ctmc
+
+// N=5 clients, K=5 blocks to be downloaded
+// Actually there are N+1=6 clients, one of which has all blocks initially
+
+// Rate of block download for a single source
+const double mu=2;
+
+// Rate of download of block i:
+// A client can download from the single client which starts with all blocks
+// or from anyone that has subsequently downloaded it.
+// Total number of concurrent downloads for each block is 4.
+formula rate1=mu*(1+min(3,b11+b21+b31+b41+b51));
+formula rate2=mu*(1+min(3,b12+b22+b32+b42+b52));
+formula rate3=mu*(1+min(3,b13+b23+b33+b43+b53));
+formula rate4=mu*(1+min(3,b14+b24+b34+b44+b54));
+formula rate5=mu*(1+min(3,b15+b25+b35+b45+b55));
+
+// client 1
+module client1
+	
+	// bij - has client i downloaded block j yet?
+	b11 : [0..1];
+	b12 : [0..1];
+	b13 : [0..1];
+	b14 : [0..1];
+	b15 : [0..1];
+	
+	// Downloading of each block (see rate computations above)
+	[] b11=0 -> rate1 : (b11'=1);
+	[] b12=0 -> rate2 : (b12'=1);
+	[] b13=0 -> rate3 : (b13'=1);
+	[] b14=0 -> rate4 : (b14'=1);
+	[] b15=0 -> rate5 : (b15'=1);
+	
+endmodule
+
+// construct remaining clients through renaming
+module client2=client1[b11=b21,b12=b22,b13=b23,b14=b24,b15=b25,b21=b11,b22=b12,b23=b13,b24=b14,b25=b15] endmodule
+module client3=client1[b11=b31,b12=b32,b13=b33,b14=b34,b15=b35,b31=b11,b32=b12,b33=b13,b34=b14,b35=b15] endmodule
+module client4=client1[b11=b41,b12=b42,b13=b43,b14=b44,b15=b45,b41=b11,b42=b12,b43=b13,b44=b14,b45=b15] endmodule
+module client5=client1[b11=b51,b12=b52,b13=b53,b14=b54,b15=b55,b51=b11,b52=b12,b53=b13,b54=b14,b55=b15] endmodule
+
+// labels
+label "done1" = b11+b12+b13+b14+b15 = 5; // client 1 has received all blocks
+label "done2" = b21+b22+b23+b24+b25 = 5; // client 2 has received all blocks
+label "done3" = b31+b32+b33+b34+b35 = 5; // client 3 has received all blocks
+label "done4" = b41+b42+b43+b44+b45 = 5; // client 4 has received all blocks
+label "done5" = b51+b52+b53+b54+b55 = 5; // client 5 has received all blocks
+label "done" = (b11+b12+b13+b14+b15)+(b21+b22+b23+b24+b25)+(b31+b32+b33+b34+b35)+(b41+b42+b43+b44+b45)+(b51+b52+b53+b54+b55) = 25; // all clients have received all blocks
+
+// reward: fraction of blocks received
+rewards "frac_rec"
+	true : ((b11+b12+b13+b14+b15)/5)/5;
+	true : ((b21+b22+b23+b24+b25)/5)/5;
+	true : ((b31+b32+b33+b34+b35)/5)/5;
+	true : ((b41+b42+b43+b44+b45)/5)/5;
+	true : ((b51+b52+b53+b54+b55)/5)/5;
+endrewards

prism-examples/peer2peer/peer2peer5_6.sm

@@ -0,0 +1,65 @@
+// Simple peer-to-peer file distribution protocol based on BitTorrent
+// gxn/dxp Jan 2006
+
+ctmc
+
+// N=5 clients, K=6 blocks to be downloaded
+// Actually there are N+1=6 clients, one of which has all blocks initially
+
+// Rate of block download for a single source
+const double mu=2;
+
+// Rate of download of block i:
+// A client can download from the single client which starts with all blocks
+// or from anyone that has subsequently downloaded it.
+// Total number of concurrent downloads for each block is 4.
+formula rate1=mu*(1+min(3,b11+b21+b31+b41+b51));
+formula rate2=mu*(1+min(3,b12+b22+b32+b42+b52));
+formula rate3=mu*(1+min(3,b13+b23+b33+b43+b53));
+formula rate4=mu*(1+min(3,b14+b24+b34+b44+b54));
+formula rate5=mu*(1+min(3,b15+b25+b35+b45+b55));
+formula rate6=mu*(1+min(3,b16+b26+b36+b46+b56));
+
+// client 1
+module client1
+	
+	// bij - has client i downloaded block j yet?
+	b11 : [0..1];
+	b12 : [0..1];
+	b13 : [0..1];
+	b14 : [0..1];
+	b15 : [0..1];
+	b16 : [0..1];
+	
+	// Downloading of each block (see rate computations above)
+	[] b11=0 -> rate1 : (b11'=1);
+	[] b12=0 -> rate2 : (b12'=1);
+	[] b13=0 -> rate3 : (b13'=1);
+	[] b14=0 -> rate4 : (b14'=1);
+	[] b15=0 -> rate5 : (b15'=1);
+	[] b16=0 -> rate6 : (b16'=1);
+	
+endmodule
+
+// construct remaining clients through renaming
+module client2=client1[b11=b21,b12=b22,b13=b23,b14=b24,b15=b25,b16=b26,b21=b11,b22=b12,b23=b13,b24=b14,b25=b15,b26=b16] endmodule
+module client3=client1[b11=b31,b12=b32,b13=b33,b14=b34,b15=b35,b16=b36,b31=b11,b32=b12,b33=b13,b34=b14,b35=b15,b36=b16] endmodule
+module client4=client1[b11=b41,b12=b42,b13=b43,b14=b44,b15=b45,b16=b46,b41=b11,b42=b12,b43=b13,b44=b14,b45=b15,b46=b16] endmodule
+module client5=client1[b11=b51,b12=b52,b13=b53,b14=b54,b15=b55,b16=b56,b51=b11,b52=b12,b53=b13,b54=b14,b55=b15,b56=b16] endmodule
+
+// labels
+label "done1" = b11+b12+b13+b14+b15+b16 = 6; // client 1 has received all blocks
+label "done2" = b21+b22+b23+b24+b25+b26 = 6; // client 2 has received all blocks
+label "done3" = b31+b32+b33+b34+b35+b36 = 6; // client 3 has received all blocks
+label "done4" = b41+b42+b43+b44+b45+b46 = 6; // client 4 has received all blocks
+label "done5" = b51+b52+b53+b54+b55+b56 = 6; // client 5 has received all blocks
+label "done" = (b11+b12+b13+b14+b15+b16)+(b21+b22+b23+b24+b25+b26)+(b31+b32+b33+b34+b35+b36)+(b41+b42+b43+b44+b45+b46)+(b51+b52+b53+b54+b55+b56) = 30; // all clients have received all blocks
+
+// reward: fraction of blocks received
+rewards "frac_rec"
+	true : ((b11+b12+b13+b14+b15+b16)/6)/5;
+	true : ((b21+b22+b23+b24+b25+b26)/6)/5;
+	true : ((b31+b32+b33+b34+b35+b36)/6)/5;
+	true : ((b41+b42+b43+b44+b45+b46)/6)/5;
+	true : ((b51+b52+b53+b54+b55+b56)/6)/5;
+endrewards

prism-examples/peer2peer/peer2peer5_7.sm

@@ -0,0 +1,68 @@
+// Simple peer-to-peer file distribution protocol based on BitTorrent
+// gxn/dxp Jan 2006
+
+ctmc
+
+// N=5 clients, K=7 blocks to be downloaded
+// Actually there are N+1=6 clients, one of which has all blocks initially
+
+// Rate of block download for a single source
+const double mu=2;
+
+// Rate of download of block i:
+// A client can download from the single client which starts with all blocks
+// or from anyone that has subsequently downloaded it.
+// Total number of concurrent downloads for each block is 4.
+formula rate1=mu*(1+min(3,b11+b21+b31+b41+b51));
+formula rate2=mu*(1+min(3,b12+b22+b32+b42+b52));
+formula rate3=mu*(1+min(3,b13+b23+b33+b43+b53));
+formula rate4=mu*(1+min(3,b14+b24+b34+b44+b54));
+formula rate5=mu*(1+min(3,b15+b25+b35+b45+b55));
+formula rate6=mu*(1+min(3,b16+b26+b36+b46+b56));
+formula rate7=mu*(1+min(3,b17+b27+b37+b47+b57));
+
+// client 1
+module client1
+	
+	// bij - has client i downloaded block j yet?
+	b11 : [0..1];
+	b12 : [0..1];
+	b13 : [0..1];
+	b14 : [0..1];
+	b15 : [0..1];
+	b16 : [0..1];
+	b17 : [0..1];
+	
+	// Downloading of each block (see rate computations above)
+	[] b11=0 -> rate1 : (b11'=1);
+	[] b12=0 -> rate2 : (b12'=1);
+	[] b13=0 -> rate3 : (b13'=1);
+	[] b14=0 -> rate4 : (b14'=1);
+	[] b15=0 -> rate5 : (b15'=1);
+	[] b16=0 -> rate6 : (b16'=1);
+	[] b17=0 -> rate7 : (b17'=1);
+	
+endmodule
+
+// construct remaining clients through renaming
+module client2=client1[b11=b21,b12=b22,b13=b23,b14=b24,b15=b25,b16=b26,b17=b27,b21=b11,b22=b12,b23=b13,b24=b14,b25=b15,b26=b16,b27=b17] endmodule
+module client3=client1[b11=b31,b12=b32,b13=b33,b14=b34,b15=b35,b16=b36,b17=b37,b31=b11,b32=b12,b33=b13,b34=b14,b35=b15,b36=b16,b37=b17] endmodule
+module client4=client1[b11=b41,b12=b42,b13=b43,b14=b44,b15=b45,b16=b46,b17=b47,b41=b11,b42=b12,b43=b13,b44=b14,b45=b15,b46=b16,b47=b17] endmodule
+module client5=client1[b11=b51,b12=b52,b13=b53,b14=b54,b15=b55,b16=b56,b17=b57,b51=b11,b52=b12,b53=b13,b54=b14,b55=b15,b56=b16,b57=b17] endmodule
+
+// labels
+label "done1" = b11+b12+b13+b14+b15+b16+b17 = 7; // client 1 has received all blocks
+label "done2" = b21+b22+b23+b24+b25+b26+b27 = 7; // client 2 has received all blocks
+label "done3" = b31+b32+b33+b34+b35+b36+b37 = 7; // client 3 has received all blocks
+label "done4" = b41+b42+b43+b44+b45+b46+b47 = 7; // client 4 has received all blocks
+label "done5" = b51+b52+b53+b54+b55+b56+b57 = 7; // client 5 has received all blocks
+label "done" = (b11+b12+b13+b14+b15+b16+b17)+(b21+b22+b23+b24+b25+b26+b27)+(b31+b32+b33+b34+b35+b36+b37)+(b41+b42+b43+b44+b45+b46+b47)+(b51+b52+b53+b54+b55+b56+b57) = 35; // all clients have received all blocks
+
+// reward: fraction of blocks received
+rewards "frac_rec"
+	true : ((b11+b12+b13+b14+b15+b16+b17)/7)/5;
+	true : ((b21+b22+b23+b24+b25+b26+b27)/7)/5;
+	true : ((b31+b32+b33+b34+b35+b36+b37)/7)/5;
+	true : ((b41+b42+b43+b44+b45+b46+b47)/7)/5;
+	true : ((b51+b52+b53+b54+b55+b56+b57)/7)/5;
+endrewards

prism-examples/peer2peer/peer2peer5_8.sm

@@ -0,0 +1,71 @@
+// Simple peer-to-peer file distribution protocol based on BitTorrent
+// gxn/dxp Jan 2006
+
+ctmc
+
+// N=5 clients, K=8 blocks to be downloaded
+// Actually there are N+1=6 clients, one of which has all blocks initially
+
+// Rate of block download for a single source
+const double mu=2;
+
+// Rate of download of block i:
+// A client can download from the single client which starts with all blocks
+// or from anyone that has subsequently downloaded it.
+// Total number of concurrent downloads for each block is 4.
+formula rate1=mu*(1+min(3,b11+b21+b31+b41+b51));
+formula rate2=mu*(1+min(3,b12+b22+b32+b42+b52));
+formula rate3=mu*(1+min(3,b13+b23+b33+b43+b53));
+formula rate4=mu*(1+min(3,b14+b24+b34+b44+b54));
+formula rate5=mu*(1+min(3,b15+b25+b35+b45+b55));
+formula rate6=mu*(1+min(3,b16+b26+b36+b46+b56));
+formula rate7=mu*(1+min(3,b17+b27+b37+b47+b57));
+formula rate8=mu*(1+min(3,b18+b28+b38+b48+b58));
+
+// client 1
+module client1
+	
+	// bij - has client i downloaded block j yet?
+	b11 : [0..1];
+	b12 : [0..1];
+	b13 : [0..1];
+	b14 : [0..1];
+	b15 : [0..1];
+	b16 : [0..1];
+	b17 : [0..1];
+	b18 : [0..1];
+	
+	// Downloading of each block (see rate computations above)
+	[] b11=0 -> rate1 : (b11'=1);
+	[] b12=0 -> rate2 : (b12'=1);
+	[] b13=0 -> rate3 : (b13'=1);
+	[] b14=0 -> rate4 : (b14'=1);
+	[] b15=0 -> rate5 : (b15'=1);
+	[] b16=0 -> rate6 : (b16'=1);
+	[] b17=0 -> rate7 : (b17'=1);
+	[] b18=0 -> rate8 : (b18'=1);
+	
+endmodule
+
+// construct remaining clients through renaming
+module client2=client1[b11=b21,b12=b22,b13=b23,b14=b24,b15=b25,b16=b26,b17=b27,b18=b28,b21=b11,b22=b12,b23=b13,b24=b14,b25=b15,b26=b16,b27=b17,b28=b18] endmodule
+module client3=client1[b11=b31,b12=b32,b13=b33,b14=b34,b15=b35,b16=b36,b17=b37,b18=b38,b31=b11,b32=b12,b33=b13,b34=b14,b35=b15,b36=b16,b37=b17,b38=b18] endmodule
+module client4=client1[b11=b41,b12=b42,b13=b43,b14=b44,b15=b45,b16=b46,b17=b47,b18=b48,b41=b11,b42=b12,b43=b13,b44=b14,b45=b15,b46=b16,b47=b17,b48=b18] endmodule
+module client5=client1[b11=b51,b12=b52,b13=b53,b14=b54,b15=b55,b16=b56,b17=b57,b18=b58,b51=b11,b52=b12,b53=b13,b54=b14,b55=b15,b56=b16,b57=b17,b58=b18] endmodule
+
+// labels
+label "done1" = b11+b12+b13+b14+b15+b16+b17+b18 = 8; // client 1 has received all blocks
+label "done2" = b21+b22+b23+b24+b25+b26+b27+b28 = 8; // client 2 has received all blocks
+label "done3" = b31+b32+b33+b34+b35+b36+b37+b38 = 8; // client 3 has received all blocks
+label "done4" = b41+b42+b43+b44+b45+b46+b47+b48 = 8; // client 4 has received all blocks
+label "done5" = b51+b52+b53+b54+b55+b56+b57+b58 = 8; // client 5 has received all blocks
+label "done" = (b11+b12+b13+b14+b15+b16+b17+b18)+(b21+b22+b23+b24+b25+b26+b27+b28)+(b31+b32+b33+b34+b35+b36+b37+b38)+(b41+b42+b43+b44+b45+b46+b47+b48)+(b51+b52+b53+b54+b55+b56+b57+b58) = 40; // all clients have received all blocks
+
+// reward: fraction of blocks received
+rewards "frac_rec"
+	true : ((b11+b12+b13+b14+b15+b16+b17+b18)/8)/5;
+	true : ((b21+b22+b23+b24+b25+b26+b27+b28)/8)/5;
+	true : ((b31+b32+b33+b34+b35+b36+b37+b38)/8)/5;
+	true : ((b41+b42+b43+b44+b45+b46+b47+b48)/8)/5;
+	true : ((b51+b52+b53+b54+b55+b56+b57+b58)/8)/5;
+endrewards