From 5545eba87d69beaf0c523f73195d0c00a9c3a72f Mon Sep 17 00:00:00 2001 From: Gethin Norman Date: Fri, 5 Dec 2008 16:42:18 +0000 Subject: [PATCH] updated rabin example git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@872 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism-examples/rabin/.autopp | 2 +- prism-examples/rabin/.rabinN.nm.pp | 46 +++++--- prism-examples/rabin/README | 4 - prism-examples/rabin/auto | 16 +-- prism-examples/rabin/modified/.autopp | 7 -- .../rabin/modified/.mod_rabinN.nm.pp | 89 --------------- prism-examples/rabin/modified/mod_rabin.pctl | 23 ---- prism-examples/rabin/modified/mod_rabin10.nm | 101 ------------------ prism-examples/rabin/modified/mod_rabin3.nm | 92 ---------------- prism-examples/rabin/modified/mod_rabin4.nm | 93 ---------------- prism-examples/rabin/modified/mod_rabin5.nm | 95 ---------------- prism-examples/rabin/modified/mod_rabin6.nm | 96 ----------------- prism-examples/rabin/modified/mod_rabin8.nm | 98 ----------------- prism-examples/rabin/rabin.pctl | 28 ++++- prism-examples/rabin/rabin10.nm | 71 +++++++----- prism-examples/rabin/rabin12.nm | 84 --------------- prism-examples/rabin/rabin3.nm | 53 ++++++--- prism-examples/rabin/rabin4.nm | 55 +++++++--- prism-examples/rabin/rabin5.nm | 59 ++++++---- prism-examples/rabin/rabin6.nm | 61 +++++++---- .../{modified/mod_rabin7.nm => rabin7.nm} | 14 +-- prism-examples/rabin/rabin8.nm | 65 +++++++---- .../{modified/mod_rabin9.nm => rabin9.nm} | 14 +-- 23 files changed, 327 insertions(+), 939 deletions(-) delete mode 100755 prism-examples/rabin/modified/.autopp delete mode 100644 prism-examples/rabin/modified/.mod_rabinN.nm.pp delete mode 100644 prism-examples/rabin/modified/mod_rabin.pctl delete mode 100644 prism-examples/rabin/modified/mod_rabin10.nm delete mode 100644 prism-examples/rabin/modified/mod_rabin3.nm delete mode 100644 prism-examples/rabin/modified/mod_rabin4.nm delete mode 100644 prism-examples/rabin/modified/mod_rabin5.nm delete mode 100644 prism-examples/rabin/modified/mod_rabin6.nm delete mode 100644 prism-examples/rabin/modified/mod_rabin8.nm delete mode 100644 prism-examples/rabin/rabin12.nm rename prism-examples/rabin/{modified/mod_rabin7.nm => rabin7.nm} (82%) rename prism-examples/rabin/{modified/mod_rabin9.nm => rabin9.nm} (83%) diff --git a/prism-examples/rabin/.autopp b/prism-examples/rabin/.autopp index b46e45ca..7d9139cd 100755 --- a/prism-examples/rabin/.autopp +++ b/prism-examples/rabin/.autopp @@ -1,6 +1,6 @@ #!/bin/csh -foreach N ( 3 4 5 6 8 10 12 ) +foreach N ( 3 4 5 6 7 8 9 10 ) echo "Generating for N=$N" prismpp .rabinN.nm.pp $N >! rabin$N.nm unix2dos rabin$N.nm diff --git a/prism-examples/rabin/.rabinN.nm.pp b/prism-examples/rabin/.rabinN.nm.pp index 0341e44c..7b69712d 100644 --- a/prism-examples/rabin/.rabinN.nm.pp +++ b/prism-examples/rabin/.rabinN.nm.pp @@ -2,7 +2,18 @@ #const K=4+func(ceil,func(log,N,2))# // N-processor mutual exclusion [Rab82] // with global variables to remove sychronization -// gxn/dxp 02/02/00 +// gxn/dxp 03/12/08 + +// version to verify a variant of the bounded waiting property +// namely the probability a process entries the critical section given it tries +// to acheive this we have split the drawing phase into two steps, so we know +// a process will draw before it actual makes the probabilistic choice +// we have however kept the two steps atomic(no other process can move one +// the first step has been made) since otherwise the adversary can prevent the +// process from actually trying in the current round by never shcedling it again + +// note we have removed the self loops to eliminate the need for fairness constraints + mdp @@ -27,37 +38,43 @@ global r : [1..2]; // current draw: bi // current round: ri -// atomic formula for process 1 drawing +// formula for process 1 drawing formula draw = p1=1 & (b (p1'=0); + // [] go & p1=0 -> (p1'=0); // enter trying - [] p1=0 -> (p1'=1); + [] go & p1=0 -> (p1'=1); // make a draw - [] draw ->#+ i=1:K-1# #1/func(floor,func(pow,2,i))# : (b1'=#i#) & (r1'=r) & (b'=max(b,#i#)) - #end#+ #1/func(floor,func(pow,2,K-1))# : (b1'=#K#) & (r1'=r) & (b'=max(b,#K#)); + [] go & draw & draw1=0 -> (draw1'=1); + [] draw1=1 ->#+ i=1:K-1# #1/func(floor,func(pow,2,i))# : (b1'=#i#) & (r1'=r) & (b'=max(b,#i#)) & (draw1'=0) + #end#+ #1/func(floor,func(pow,2,K-1))# : (b1'=#K#) & (r1'=r) & (b'=max(b,#K#)) & (draw1'=0); // enter critical section and randomly set r to 1 or 2 - [] p1=1 & b=b1 & r=r1 & c=0 -> 0.5 : (r'=1) & (c'=1) & (b'=0) & (b1'=0) & (r1'=0) & (p1'=2) + [] go & p1=1 & b=b1 & r=r1 & c=0 -> 0.5 : (r'=1) & (c'=1) & (b'=0) & (b1'=0) & (r1'=0) & (p1'=2) + 0.5 : (r'=2) & (c'=1) & (b'=0) & (b1'=0) & (r1'=0) & (p1'=2); // loop when trying and cannot make a draw or enter critical section - [] p1=1 & r1=r & b1<=b & ((c=0 & b1!=b) | c=1) -> (p1'=p1); + // [] go & p1=1 & r1=r & b1<=b & ((c=0 & b1!=b) | c=1) -> (p1'=p1); // leave crictical section - [] p1=2 -> (p1'=0) & (c'=0); + [] go & p1=2 -> (p1'=0) & (c'=0); // stay in critical section - [] p1=2 -> (p1'=2); + // [] go & p1=2 -> (p1'=2); endmodule // construct further modules through renaming #for i=2:N# -module process#i# = process1 [p1=p#i#, b1=b#i#, r1=r#i#] endmodule #end# +module process#i# = process1 [p1=p#i#, b1=b#i#, r1=r#i#, draw1=draw#i#, draw#i#=draw1 ] endmodule #end# // formulas/labels for use in properties: @@ -68,4 +85,7 @@ formula num_procs_in_crit = #+ i=1:N#(p#i#=2?1:0)#end#; label "one_trying" = #| i=1:N#p#i#=1#end#; // one of the processes is in the critical section -label "one_critical" = #| i=1:N#p#i#=2#end#; +label "one_critical" = #| i=1:N#p#i#=2#end#; + +// maximum value of the bi's +formula maxb = max(b1#for i=2:N#,b#i##end#); diff --git a/prism-examples/rabin/README b/prism-examples/rabin/README index 0afe26c4..852d8ce2 100644 --- a/prism-examples/rabin/README +++ b/prism-examples/rabin/README @@ -1,10 +1,6 @@ This case study is based on Rabin's solution to the well known mutual exclusion problem [Rab82]. For more information, see: http://www.prismmodelchecker.org/casestudies/rabin.php - -In the subdirectory "modified" there is a modified version of the protocol used for -verifying, given a process tries in the current round, the probability it -enters in the current round ===================================================================================== diff --git a/prism-examples/rabin/auto b/prism-examples/rabin/auto index 59425264..be876ff3 100755 --- a/prism-examples/rabin/auto +++ b/prism-examples/rabin/auto @@ -1,9 +1,11 @@ #!/bin/csh -prism rabin3.nm rabin.pctl -fair -prism rabin4.nm rabin.pctl -fair -prism rabin5.nm rabin.pctl -fair -prism rabin6.nm rabin.pctl -fair -prism rabin8.nm rabin.pctl -fair -#prism rabin10.nm rabin.pctl -fair -#prism rabin12.nm rabin.pctl -fair +prism rabin3.nm rabin.pctl -m +prism rabin4.nm rabin.pctl -m +prism rabin5.nm rabin.pctl -m +prism rabin6.nm rabin.pctl -m +prism rabin7.nm rabin.pctl -m +prism rabin8.nm rabin.pctl -m +#prism rabin9.nm rabin.pctl -m +#prism rabin10.nm rabin.pctl -m + diff --git a/prism-examples/rabin/modified/.autopp b/prism-examples/rabin/modified/.autopp deleted file mode 100755 index a130c69e..00000000 --- a/prism-examples/rabin/modified/.autopp +++ /dev/null @@ -1,7 +0,0 @@ -#!/bin/csh - -foreach N ( 3 4 5 6 7 8 9 10 ) - echo "Generating for N=$N" - prismpp .mod_rabinN.nm.pp $N >! mod_rabin$N.nm - unix2dos mod_rabin$N.nm -end diff --git a/prism-examples/rabin/modified/.mod_rabinN.nm.pp b/prism-examples/rabin/modified/.mod_rabinN.nm.pp deleted file mode 100644 index 96129a6b..00000000 --- a/prism-examples/rabin/modified/.mod_rabinN.nm.pp +++ /dev/null @@ -1,89 +0,0 @@ -#const N# -#const K=4+func(ceil,func(log,N,2))# -// N-processor mutual exclusion [Rab82] -// with global variables to remove sychronization -// gxn/dxp 03/12/08 - -// modified version to verify a variant of the bounded waiting property -// namely the probability a process entries the critical sectiongiven it tries - -// note we have removed the self loops to allow the fairness constraints -// to be ignored during verification - -// split the drawing phase into two steps but is still atomic as no -// other process can move one the first step has been made - -mdp - -// size of shared counter -const int K = #K#; // 4+ceil(log_2 N) - -// global variables (all modules can read and write) -// c=0 critical section free -// c=1 critical section not free -// b current highest draw -// r current round - -global c : [0..1]; -global b : [0..K]; -global r : [1..2]; - -// local variables: process i -// state: pi -// 0 remainder -// 1 trying -// 2 critical section -// current draw: bi -// current round: ri - -// formula for process 1 drawing -formula draw = p1=1 & (b (p1'=0); - // enter trying - [] go & p1=0 -> (p1'=1); - // make a draw - [] go & draw & draw1=0 -> (draw1'=1); - [] draw1=1 ->#+ i=1:K-1# #1/func(floor,func(pow,2,i))# : (b1'=#i#) & (r1'=r) & (b'=max(b,#i#)) & (draw1'=0) - #end#+ #1/func(floor,func(pow,2,K-1))# : (b1'=#K#) & (r1'=r) & (b'=max(b,#K#)) & (draw1'=0); - // enter critical section and randomly set r to 1 or 2 - [] go & p1=1 & b=b1 & r=r1 & c=0 -> 0.5 : (r'=1) & (c'=1) & (b'=0) & (b1'=0) & (r1'=0) & (p1'=2) - + 0.5 : (r'=2) & (c'=1) & (b'=0) & (b1'=0) & (r1'=0) & (p1'=2); - // loop when trying and cannot make a draw or enter critical section - // [] go & p1=1 & r1=r & b1<=b & ((c=0 & b1!=b) | c=1) -> (p1'=p1); - // leave crictical section - [] go & p1=2 -> (p1'=0) & (c'=0); - // stay in critical section - // [] go & p1=2 -> (p1'=2); - -endmodule - -// construct further modules through renaming -#for i=2:N# -module process#i# = process1 [p1=p#i#, b1=b#i#, r1=r#i#, draw1=draw#i#, draw#i#=draw1 ] endmodule #end# - -// formulas/labels for use in properties: - -// number of processes in critical section -formula num_procs_in_crit = #+ i=1:N#(p#i#=2?1:0)#end#; - -// one of the processes is trying -label "one_trying" = #| i=1:N#p#i#=1#end#; - -// one of the processes is in the critical section -label "one_critical" = #| i=1:N#p#i#=2#end#; - -// maximum value of the bi's -formula maxb = max(b1#for i=2:N#,b#i##end#); diff --git a/prism-examples/rabin/modified/mod_rabin.pctl b/prism-examples/rabin/modified/mod_rabin.pctl deleted file mode 100644 index 673e674e..00000000 --- a/prism-examples/rabin/modified/mod_rabin.pctl +++ /dev/null @@ -1,23 +0,0 @@ -// mention that Rabin property is not well defined (see Saias thesis) - -// minimum probability process enters the criticial section -// only interested in the probability in states for which -// - process is going to make a draw (draw1=1) -// - no process is in the critical section (otherwise probability is clearly 0 -// and we take the minimum value over this set of states -Pmin=?[ !"one_critical" U (p1=2) {draw1=1 & !"one_critical"}{min} ] - -// probability above is zero which is due to the fact that the adversary can use the values -// of the state variables of the other processes -// this does not quite disprove Rabin's bounded waiting property as one is starting -// from the state the process decides to enter the round and one doesnot take into account -// the probability of reaching this state (this does have an influence as the results -// for the properties below show that to get the probability 0 one of the other processes -//must have already randomly picked a high value for its bi) - -// to demonstrate this fact we restrict attention to states where these values -// are restricted,i.e. where the values of the bi variables are bounded Pmin=?[ !"one_critical" U (p1=2) {draw1=1 & !"one_critical" & maxb<6}{min} ] Pmin=?[ !"one_critical" U (p1=2) {draw1=1 & !"one_critical" & maxb<5}{min} ] Pmin=?[ !"one_critical" U (p1=2) {draw1=1 & !"one_critical" & maxb<4}{min} ] Pmin=?[ !"one_critical" U (p1=2) {draw1=1 & !"one_critical" & maxb<3}{min} ] Pmin=?[ !"one_critical" U (p1=2) {draw1=1 & !"one_critical" & maxb<2}{min} ] Pmin=?[ !"one_critical" U (p1=2) {draw1=1 & !"one_critical" & maxb<1}{min} ] -// liveness (eventially a process enters its critical section -// since we have removed the loops this holds with probability 1 even without fairness -Pmin=?[F p1=2 | p2=2 | p3=2 ] - diff --git a/prism-examples/rabin/modified/mod_rabin10.nm b/prism-examples/rabin/modified/mod_rabin10.nm deleted file mode 100644 index 55411331..00000000 --- a/prism-examples/rabin/modified/mod_rabin10.nm +++ /dev/null @@ -1,101 +0,0 @@ -// N-processor mutual exclusion [Rab82] -// with global variables to remove sychronization -// gxn/dxp 03/12/08 - -// modified version to verify a variant of the bounded waiting property -// namely the probability a process entries the critical sectiongiven it tries - -// note we have removed the self loops to allow the fairness constraints -// to be ignored during verification - -// split the drawing phase into two steps but is still atomic as no -// other process can move one the first step has been made - -mdp - -// size of shared counter -const int K = 8; // 4+ceil(log_2 N) - -// global variables (all modules can read and write) -// c=0 critical section free -// c=1 critical section not free -// b current highest draw -// r current round - -global c : [0..1]; -global b : [0..K]; -global r : [1..2]; - -// local variables: process i -// state: pi -// 0 remainder -// 1 trying -// 2 critical section -// current draw: bi -// current round: ri - -// formula for process 1 drawing -formula draw = p1=1 & (b (p1'=0); - // enter trying - [] go & p1=0 -> (p1'=1); - // make a draw - [] go & draw & draw1=0 -> (draw1'=1); - [] draw1=1 -> 0.5 : (b1'=1) & (r1'=r) & (b'=max(b,1)) & (draw1'=0) - + 0.25 : (b1'=2) & (r1'=r) & (b'=max(b,2)) & (draw1'=0) - + 0.125 : (b1'=3) & (r1'=r) & (b'=max(b,3)) & (draw1'=0) - + 0.0625 : (b1'=4) & (r1'=r) & (b'=max(b,4)) & (draw1'=0) - + 0.03125 : (b1'=5) & (r1'=r) & (b'=max(b,5)) & (draw1'=0) - + 0.015625 : (b1'=6) & (r1'=r) & (b'=max(b,6)) & (draw1'=0) - + 0.0078125 : (b1'=7) & (r1'=r) & (b'=max(b,7)) & (draw1'=0) - + 0.0078125 : (b1'=8) & (r1'=r) & (b'=max(b,8)) & (draw1'=0); - // enter critical section and randomly set r to 1 or 2 - [] go & p1=1 & b=b1 & r=r1 & c=0 -> 0.5 : (r'=1) & (c'=1) & (b'=0) & (b1'=0) & (r1'=0) & (p1'=2) - + 0.5 : (r'=2) & (c'=1) & (b'=0) & (b1'=0) & (r1'=0) & (p1'=2); - // loop when trying and cannot make a draw or enter critical section - // [] go & p1=1 & r1=r & b1<=b & ((c=0 & b1!=b) | c=1) -> (p1'=p1); - // leave crictical section - [] go & p1=2 -> (p1'=0) & (c'=0); - // stay in critical section - // [] go & p1=2 -> (p1'=2); - -endmodule - -// construct further modules through renaming -module process2 = process1 [p1=p2, b1=b2, r1=r2, draw1=draw2, draw2=draw1 ] endmodule -module process3 = process1 [p1=p3, b1=b3, r1=r3, draw1=draw3, draw3=draw1 ] endmodule -module process4 = process1 [p1=p4, b1=b4, r1=r4, draw1=draw4, draw4=draw1 ] endmodule -module process5 = process1 [p1=p5, b1=b5, r1=r5, draw1=draw5, draw5=draw1 ] endmodule -module process6 = process1 [p1=p6, b1=b6, r1=r6, draw1=draw6, draw6=draw1 ] endmodule -module process7 = process1 [p1=p7, b1=b7, r1=r7, draw1=draw7, draw7=draw1 ] endmodule -module process8 = process1 [p1=p8, b1=b8, r1=r8, draw1=draw8, draw8=draw1 ] endmodule -module process9 = process1 [p1=p9, b1=b9, r1=r9, draw1=draw9, draw9=draw1 ] endmodule -module process10 = process1 [p1=p10, b1=b10, r1=r10, draw1=draw10, draw10=draw1 ] endmodule - -// formulas/labels for use in properties: - -// number of processes in critical section -formula num_procs_in_crit = (p1=2?1:0)+(p2=2?1:0)+(p3=2?1:0)+(p4=2?1:0)+(p5=2?1:0)+(p6=2?1:0)+(p7=2?1:0)+(p8=2?1:0)+(p9=2?1:0)+(p10=2?1:0); - -// one of the processes is trying -label "one_trying" = p1=1|p2=1|p3=1|p4=1|p5=1|p6=1|p7=1|p8=1|p9=1|p10=1; - -// one of the processes is in the critical section -label "one_critical" = p1=2|p2=2|p3=2|p4=2|p5=2|p6=2|p7=2|p8=2|p9=2|p10=2; - -// maximum value of the bi's -formula maxb = max(b1,b2,b3,b4,b5,b6,b7,b8,b9,b10); - diff --git a/prism-examples/rabin/modified/mod_rabin3.nm b/prism-examples/rabin/modified/mod_rabin3.nm deleted file mode 100644 index a40cb8da..00000000 --- a/prism-examples/rabin/modified/mod_rabin3.nm +++ /dev/null @@ -1,92 +0,0 @@ -// N-processor mutual exclusion [Rab82] -// with global variables to remove sychronization -// gxn/dxp 03/12/08 - -// modified version to verify a variant of the bounded waiting property -// namely the probability a process entries the critical sectiongiven it tries - -// note we have removed the self loops to allow the fairness constraints -// to be ignored during verification - -// split the drawing phase into two steps but is still atomic as no -// other process can move one the first step has been made - -mdp - -// size of shared counter -const int K = 6; // 4+ceil(log_2 N) - -// global variables (all modules can read and write) -// c=0 critical section free -// c=1 critical section not free -// b current highest draw -// r current round - -global c : [0..1]; -global b : [0..K]; -global r : [1..2]; - -// local variables: process i -// state: pi -// 0 remainder -// 1 trying -// 2 critical section -// current draw: bi -// current round: ri - -// formula for process 1 drawing -formula draw = p1=1 & (b (p1'=0); - // enter trying - [] go & p1=0 -> (p1'=1); - // make a draw - [] go & draw & draw1=0 -> (draw1'=1); - [] draw1=1 -> 0.5 : (b1'=1) & (r1'=r) & (b'=max(b,1)) & (draw1'=0) - + 0.25 : (b1'=2) & (r1'=r) & (b'=max(b,2)) & (draw1'=0) - + 0.125 : (b1'=3) & (r1'=r) & (b'=max(b,3)) & (draw1'=0) - + 0.0625 : (b1'=4) & (r1'=r) & (b'=max(b,4)) & (draw1'=0) - + 0.03125 : (b1'=5) & (r1'=r) & (b'=max(b,5)) & (draw1'=0) - + 0.03125 : (b1'=6) & (r1'=r) & (b'=max(b,6)) & (draw1'=0); - // enter critical section and randomly set r to 1 or 2 - [] go & p1=1 & b=b1 & r=r1 & c=0 -> 0.5 : (r'=1) & (c'=1) & (b'=0) & (b1'=0) & (r1'=0) & (p1'=2) - + 0.5 : (r'=2) & (c'=1) & (b'=0) & (b1'=0) & (r1'=0) & (p1'=2); - // loop when trying and cannot make a draw or enter critical section - // [] go & p1=1 & r1=r & b1<=b & ((c=0 & b1!=b) | c=1) -> (p1'=p1); - // leave crictical section - [] go & p1=2 -> (p1'=0) & (c'=0); - // stay in critical section - // [] go & p1=2 -> (p1'=2); - -endmodule - -// construct further modules through renaming -module process2 = process1 [p1=p2, b1=b2, r1=r2, draw1=draw2, draw2=draw1 ] endmodule -module process3 = process1 [p1=p3, b1=b3, r1=r3, draw1=draw3, draw3=draw1 ] endmodule - -// formulas/labels for use in properties: - -// number of processes in critical section -formula num_procs_in_crit = (p1=2?1:0)+(p2=2?1:0)+(p3=2?1:0); - -// one of the processes is trying -label "one_trying" = p1=1|p2=1|p3=1; - -// one of the processes is in the critical section -label "one_critical" = p1=2|p2=2|p3=2; - -// maximum value of the bi's -formula maxb = max(b1,b2,b3); - diff --git a/prism-examples/rabin/modified/mod_rabin4.nm b/prism-examples/rabin/modified/mod_rabin4.nm deleted file mode 100644 index 1993bd83..00000000 --- a/prism-examples/rabin/modified/mod_rabin4.nm +++ /dev/null @@ -1,93 +0,0 @@ -// N-processor mutual exclusion [Rab82] -// with global variables to remove sychronization -// gxn/dxp 03/12/08 - -// modified version to verify a variant of the bounded waiting property -// namely the probability a process entries the critical sectiongiven it tries - -// note we have removed the self loops to allow the fairness constraints -// to be ignored during verification - -// split the drawing phase into two steps but is still atomic as no -// other process can move one the first step has been made - -mdp - -// size of shared counter -const int K = 6; // 4+ceil(log_2 N) - -// global variables (all modules can read and write) -// c=0 critical section free -// c=1 critical section not free -// b current highest draw -// r current round - -global c : [0..1]; -global b : [0..K]; -global r : [1..2]; - -// local variables: process i -// state: pi -// 0 remainder -// 1 trying -// 2 critical section -// current draw: bi -// current round: ri - -// formula for process 1 drawing -formula draw = p1=1 & (b (p1'=0); - // enter trying - [] go & p1=0 -> (p1'=1); - // make a draw - [] go & draw & draw1=0 -> (draw1'=1); - [] draw1=1 -> 0.5 : (b1'=1) & (r1'=r) & (b'=max(b,1)) & (draw1'=0) - + 0.25 : (b1'=2) & (r1'=r) & (b'=max(b,2)) & (draw1'=0) - + 0.125 : (b1'=3) & (r1'=r) & (b'=max(b,3)) & (draw1'=0) - + 0.0625 : (b1'=4) & (r1'=r) & (b'=max(b,4)) & (draw1'=0) - + 0.03125 : (b1'=5) & (r1'=r) & (b'=max(b,5)) & (draw1'=0) - + 0.03125 : (b1'=6) & (r1'=r) & (b'=max(b,6)) & (draw1'=0); - // enter critical section and randomly set r to 1 or 2 - [] go & p1=1 & b=b1 & r=r1 & c=0 -> 0.5 : (r'=1) & (c'=1) & (b'=0) & (b1'=0) & (r1'=0) & (p1'=2) - + 0.5 : (r'=2) & (c'=1) & (b'=0) & (b1'=0) & (r1'=0) & (p1'=2); - // loop when trying and cannot make a draw or enter critical section - // [] go & p1=1 & r1=r & b1<=b & ((c=0 & b1!=b) | c=1) -> (p1'=p1); - // leave crictical section - [] go & p1=2 -> (p1'=0) & (c'=0); - // stay in critical section - // [] go & p1=2 -> (p1'=2); - -endmodule - -// construct further modules through renaming -module process2 = process1 [p1=p2, b1=b2, r1=r2, draw1=draw2, draw2=draw1 ] endmodule -module process3 = process1 [p1=p3, b1=b3, r1=r3, draw1=draw3, draw3=draw1 ] endmodule -module process4 = process1 [p1=p4, b1=b4, r1=r4, draw1=draw4, draw4=draw1 ] endmodule - -// formulas/labels for use in properties: - -// number of processes in critical section -formula num_procs_in_crit = (p1=2?1:0)+(p2=2?1:0)+(p3=2?1:0)+(p4=2?1:0); - -// one of the processes is trying -label "one_trying" = p1=1|p2=1|p3=1|p4=1; - -// one of the processes is in the critical section -label "one_critical" = p1=2|p2=2|p3=2|p4=2; - -// maximum value of the bi's -formula maxb = max(b1,b2,b3,b4); - diff --git a/prism-examples/rabin/modified/mod_rabin5.nm b/prism-examples/rabin/modified/mod_rabin5.nm deleted file mode 100644 index ff0c8462..00000000 --- a/prism-examples/rabin/modified/mod_rabin5.nm +++ /dev/null @@ -1,95 +0,0 @@ -// N-processor mutual exclusion [Rab82] -// with global variables to remove sychronization -// gxn/dxp 03/12/08 - -// modified version to verify a variant of the bounded waiting property -// namely the probability a process entries the critical sectiongiven it tries - -// note we have removed the self loops to allow the fairness constraints -// to be ignored during verification - -// split the drawing phase into two steps but is still atomic as no -// other process can move one the first step has been made - -mdp - -// size of shared counter -const int K = 7; // 4+ceil(log_2 N) - -// global variables (all modules can read and write) -// c=0 critical section free -// c=1 critical section not free -// b current highest draw -// r current round - -global c : [0..1]; -global b : [0..K]; -global r : [1..2]; - -// local variables: process i -// state: pi -// 0 remainder -// 1 trying -// 2 critical section -// current draw: bi -// current round: ri - -// formula for process 1 drawing -formula draw = p1=1 & (b (p1'=0); - // enter trying - [] go & p1=0 -> (p1'=1); - // make a draw - [] go & draw & draw1=0 -> (draw1'=1); - [] draw1=1 -> 0.5 : (b1'=1) & (r1'=r) & (b'=max(b,1)) & (draw1'=0) - + 0.25 : (b1'=2) & (r1'=r) & (b'=max(b,2)) & (draw1'=0) - + 0.125 : (b1'=3) & (r1'=r) & (b'=max(b,3)) & (draw1'=0) - + 0.0625 : (b1'=4) & (r1'=r) & (b'=max(b,4)) & (draw1'=0) - + 0.03125 : (b1'=5) & (r1'=r) & (b'=max(b,5)) & (draw1'=0) - + 0.015625 : (b1'=6) & (r1'=r) & (b'=max(b,6)) & (draw1'=0) - + 0.015625 : (b1'=7) & (r1'=r) & (b'=max(b,7)) & (draw1'=0); - // enter critical section and randomly set r to 1 or 2 - [] go & p1=1 & b=b1 & r=r1 & c=0 -> 0.5 : (r'=1) & (c'=1) & (b'=0) & (b1'=0) & (r1'=0) & (p1'=2) - + 0.5 : (r'=2) & (c'=1) & (b'=0) & (b1'=0) & (r1'=0) & (p1'=2); - // loop when trying and cannot make a draw or enter critical section - // [] go & p1=1 & r1=r & b1<=b & ((c=0 & b1!=b) | c=1) -> (p1'=p1); - // leave crictical section - [] go & p1=2 -> (p1'=0) & (c'=0); - // stay in critical section - // [] go & p1=2 -> (p1'=2); - -endmodule - -// construct further modules through renaming -module process2 = process1 [p1=p2, b1=b2, r1=r2, draw1=draw2, draw2=draw1 ] endmodule -module process3 = process1 [p1=p3, b1=b3, r1=r3, draw1=draw3, draw3=draw1 ] endmodule -module process4 = process1 [p1=p4, b1=b4, r1=r4, draw1=draw4, draw4=draw1 ] endmodule -module process5 = process1 [p1=p5, b1=b5, r1=r5, draw1=draw5, draw5=draw1 ] endmodule - -// formulas/labels for use in properties: - -// number of processes in critical section -formula num_procs_in_crit = (p1=2?1:0)+(p2=2?1:0)+(p3=2?1:0)+(p4=2?1:0)+(p5=2?1:0); - -// one of the processes is trying -label "one_trying" = p1=1|p2=1|p3=1|p4=1|p5=1; - -// one of the processes is in the critical section -label "one_critical" = p1=2|p2=2|p3=2|p4=2|p5=2; - -// maximum value of the bi's -formula maxb = max(b1,b2,b3,b4,b5); - diff --git a/prism-examples/rabin/modified/mod_rabin6.nm b/prism-examples/rabin/modified/mod_rabin6.nm deleted file mode 100644 index dfe917f8..00000000 --- a/prism-examples/rabin/modified/mod_rabin6.nm +++ /dev/null @@ -1,96 +0,0 @@ -// N-processor mutual exclusion [Rab82] -// with global variables to remove sychronization -// gxn/dxp 03/12/08 - -// modified version to verify a variant of the bounded waiting property -// namely the probability a process entries the critical sectiongiven it tries - -// note we have removed the self loops to allow the fairness constraints -// to be ignored during verification - -// split the drawing phase into two steps but is still atomic as no -// other process can move one the first step has been made - -mdp - -// size of shared counter -const int K = 7; // 4+ceil(log_2 N) - -// global variables (all modules can read and write) -// c=0 critical section free -// c=1 critical section not free -// b current highest draw -// r current round - -global c : [0..1]; -global b : [0..K]; -global r : [1..2]; - -// local variables: process i -// state: pi -// 0 remainder -// 1 trying -// 2 critical section -// current draw: bi -// current round: ri - -// formula for process 1 drawing -formula draw = p1=1 & (b (p1'=0); - // enter trying - [] go & p1=0 -> (p1'=1); - // make a draw - [] go & draw & draw1=0 -> (draw1'=1); - [] draw1=1 -> 0.5 : (b1'=1) & (r1'=r) & (b'=max(b,1)) & (draw1'=0) - + 0.25 : (b1'=2) & (r1'=r) & (b'=max(b,2)) & (draw1'=0) - + 0.125 : (b1'=3) & (r1'=r) & (b'=max(b,3)) & (draw1'=0) - + 0.0625 : (b1'=4) & (r1'=r) & (b'=max(b,4)) & (draw1'=0) - + 0.03125 : (b1'=5) & (r1'=r) & (b'=max(b,5)) & (draw1'=0) - + 0.015625 : (b1'=6) & (r1'=r) & (b'=max(b,6)) & (draw1'=0) - + 0.015625 : (b1'=7) & (r1'=r) & (b'=max(b,7)) & (draw1'=0); - // enter critical section and randomly set r to 1 or 2 - [] go & p1=1 & b=b1 & r=r1 & c=0 -> 0.5 : (r'=1) & (c'=1) & (b'=0) & (b1'=0) & (r1'=0) & (p1'=2) - + 0.5 : (r'=2) & (c'=1) & (b'=0) & (b1'=0) & (r1'=0) & (p1'=2); - // loop when trying and cannot make a draw or enter critical section - // [] go & p1=1 & r1=r & b1<=b & ((c=0 & b1!=b) | c=1) -> (p1'=p1); - // leave crictical section - [] go & p1=2 -> (p1'=0) & (c'=0); - // stay in critical section - // [] go & p1=2 -> (p1'=2); - -endmodule - -// construct further modules through renaming -module process2 = process1 [p1=p2, b1=b2, r1=r2, draw1=draw2, draw2=draw1 ] endmodule -module process3 = process1 [p1=p3, b1=b3, r1=r3, draw1=draw3, draw3=draw1 ] endmodule -module process4 = process1 [p1=p4, b1=b4, r1=r4, draw1=draw4, draw4=draw1 ] endmodule -module process5 = process1 [p1=p5, b1=b5, r1=r5, draw1=draw5, draw5=draw1 ] endmodule -module process6 = process1 [p1=p6, b1=b6, r1=r6, draw1=draw6, draw6=draw1 ] endmodule - -// formulas/labels for use in properties: - -// number of processes in critical section -formula num_procs_in_crit = (p1=2?1:0)+(p2=2?1:0)+(p3=2?1:0)+(p4=2?1:0)+(p5=2?1:0)+(p6=2?1:0); - -// one of the processes is trying -label "one_trying" = p1=1|p2=1|p3=1|p4=1|p5=1|p6=1; - -// one of the processes is in the critical section -label "one_critical" = p1=2|p2=2|p3=2|p4=2|p5=2|p6=2; - -// maximum value of the bi's -formula maxb = max(b1,b2,b3,b4,b5,b6); - diff --git a/prism-examples/rabin/modified/mod_rabin8.nm b/prism-examples/rabin/modified/mod_rabin8.nm deleted file mode 100644 index 624c1d6f..00000000 --- a/prism-examples/rabin/modified/mod_rabin8.nm +++ /dev/null @@ -1,98 +0,0 @@ -// N-processor mutual exclusion [Rab82] -// with global variables to remove sychronization -// gxn/dxp 03/12/08 - -// modified version to verify a variant of the bounded waiting property -// namely the probability a process entries the critical sectiongiven it tries - -// note we have removed the self loops to allow the fairness constraints -// to be ignored during verification - -// split the drawing phase into two steps but is still atomic as no -// other process can move one the first step has been made - -mdp - -// size of shared counter -const int K = 7; // 4+ceil(log_2 N) - -// global variables (all modules can read and write) -// c=0 critical section free -// c=1 critical section not free -// b current highest draw -// r current round - -global c : [0..1]; -global b : [0..K]; -global r : [1..2]; - -// local variables: process i -// state: pi -// 0 remainder -// 1 trying -// 2 critical section -// current draw: bi -// current round: ri - -// formula for process 1 drawing -formula draw = p1=1 & (b (p1'=0); - // enter trying - [] go & p1=0 -> (p1'=1); - // make a draw - [] go & draw & draw1=0 -> (draw1'=1); - [] draw1=1 -> 0.5 : (b1'=1) & (r1'=r) & (b'=max(b,1)) & (draw1'=0) - + 0.25 : (b1'=2) & (r1'=r) & (b'=max(b,2)) & (draw1'=0) - + 0.125 : (b1'=3) & (r1'=r) & (b'=max(b,3)) & (draw1'=0) - + 0.0625 : (b1'=4) & (r1'=r) & (b'=max(b,4)) & (draw1'=0) - + 0.03125 : (b1'=5) & (r1'=r) & (b'=max(b,5)) & (draw1'=0) - + 0.015625 : (b1'=6) & (r1'=r) & (b'=max(b,6)) & (draw1'=0) - + 0.015625 : (b1'=7) & (r1'=r) & (b'=max(b,7)) & (draw1'=0); - // enter critical section and randomly set r to 1 or 2 - [] go & p1=1 & b=b1 & r=r1 & c=0 -> 0.5 : (r'=1) & (c'=1) & (b'=0) & (b1'=0) & (r1'=0) & (p1'=2) - + 0.5 : (r'=2) & (c'=1) & (b'=0) & (b1'=0) & (r1'=0) & (p1'=2); - // loop when trying and cannot make a draw or enter critical section - // [] go & p1=1 & r1=r & b1<=b & ((c=0 & b1!=b) | c=1) -> (p1'=p1); - // leave crictical section - [] go & p1=2 -> (p1'=0) & (c'=0); - // stay in critical section - // [] go & p1=2 -> (p1'=2); - -endmodule - -// construct further modules through renaming -module process2 = process1 [p1=p2, b1=b2, r1=r2, draw1=draw2, draw2=draw1 ] endmodule -module process3 = process1 [p1=p3, b1=b3, r1=r3, draw1=draw3, draw3=draw1 ] endmodule -module process4 = process1 [p1=p4, b1=b4, r1=r4, draw1=draw4, draw4=draw1 ] endmodule -module process5 = process1 [p1=p5, b1=b5, r1=r5, draw1=draw5, draw5=draw1 ] endmodule -module process6 = process1 [p1=p6, b1=b6, r1=r6, draw1=draw6, draw6=draw1 ] endmodule -module process7 = process1 [p1=p7, b1=b7, r1=r7, draw1=draw7, draw7=draw1 ] endmodule -module process8 = process1 [p1=p8, b1=b8, r1=r8, draw1=draw8, draw8=draw1 ] endmodule - -// formulas/labels for use in properties: - -// number of processes in critical section -formula num_procs_in_crit = (p1=2?1:0)+(p2=2?1:0)+(p3=2?1:0)+(p4=2?1:0)+(p5=2?1:0)+(p6=2?1:0)+(p7=2?1:0)+(p8=2?1:0); - -// one of the processes is trying -label "one_trying" = p1=1|p2=1|p3=1|p4=1|p5=1|p6=1|p7=1|p8=1; - -// one of the processes is in the critical section -label "one_critical" = p1=2|p2=2|p3=2|p4=2|p5=2|p6=2|p7=2|p8=2; - -// maximum value of the bi's -formula maxb = max(b1,b2,b3,b4,b5,b6,b7,b8); - diff --git a/prism-examples/rabin/rabin.pctl b/prism-examples/rabin/rabin.pctl index 14724378..673e674e 100644 --- a/prism-examples/rabin/rabin.pctl +++ b/prism-examples/rabin/rabin.pctl @@ -1,5 +1,23 @@ -// Mutual exclusion: at any time t there is at most one process in its critical section phase -num_procs_in_crit <= 1 - -// Liveness: if a process is trying, then eventually a process enters the critical section -"one_trying" => P>=1 [ F "one_critical" ] +// mention that Rabin property is not well defined (see Saias thesis) + +// minimum probability process enters the criticial section +// only interested in the probability in states for which +// - process is going to make a draw (draw1=1) +// - no process is in the critical section (otherwise probability is clearly 0 +// and we take the minimum value over this set of states +Pmin=?[ !"one_critical" U (p1=2) {draw1=1 & !"one_critical"}{min} ] + +// probability above is zero which is due to the fact that the adversary can use the values +// of the state variables of the other processes +// this does not quite disprove Rabin's bounded waiting property as one is starting +// from the state the process decides to enter the round and one doesnot take into account +// the probability of reaching this state (this does have an influence as the results +// for the properties below show that to get the probability 0 one of the other processes +//must have already randomly picked a high value for its bi) + +// to demonstrate this fact we restrict attention to states where these values +// are restricted,i.e. where the values of the bi variables are bounded Pmin=?[ !"one_critical" U (p1=2) {draw1=1 & !"one_critical" & maxb<6}{min} ] Pmin=?[ !"one_critical" U (p1=2) {draw1=1 & !"one_critical" & maxb<5}{min} ] Pmin=?[ !"one_critical" U (p1=2) {draw1=1 & !"one_critical" & maxb<4}{min} ] Pmin=?[ !"one_critical" U (p1=2) {draw1=1 & !"one_critical" & maxb<3}{min} ] Pmin=?[ !"one_critical" U (p1=2) {draw1=1 & !"one_critical" & maxb<2}{min} ] Pmin=?[ !"one_critical" U (p1=2) {draw1=1 & !"one_critical" & maxb<1}{min} ] +// liveness (eventially a process enters its critical section +// since we have removed the loops this holds with probability 1 even without fairness +Pmin=?[F p1=2 | p2=2 | p3=2 ] + diff --git a/prism-examples/rabin/rabin10.nm b/prism-examples/rabin/rabin10.nm index 1e7714cf..3527e331 100644 --- a/prism-examples/rabin/rabin10.nm +++ b/prism-examples/rabin/rabin10.nm @@ -1,6 +1,17 @@ // N-processor mutual exclusion [Rab82] // with global variables to remove sychronization -// gxn/dxp 02/02/00 +// gxn/dxp 03/12/08 + +// version to verify a variant of the bounded waiting property +// namely the probability a process entries the critical section given it tries +// to acheive this we have split the drawing phase into two steps, so we know +// a process will draw before it actual makes the probabilistic choice +// we have however kept the two steps atomic(no other process can move one +// the first step has been made) since otherwise the adversary can prevent the +// process from actually trying in the current round by never shcedling it again + +// note we have removed the self loops to eliminate the need for fairness constraints + mdp @@ -25,50 +36,56 @@ global r : [1..2]; // current draw: bi // current round: ri -// atomic formula for process 1 drawing +// formula for process 1 drawing formula draw = p1=1 & (b (p1'=0); + // [] go & p1=0 -> (p1'=0); // enter trying - [] p1=0 -> (p1'=1); + [] go & p1=0 -> (p1'=1); // make a draw - [] draw -> 0.5 : (b1'=1) & (r1'=r) & (b'=max(b,1)) - + 0.25 : (b1'=2) & (r1'=r) & (b'=max(b,2)) - + 0.125 : (b1'=3) & (r1'=r) & (b'=max(b,3)) - + 0.0625 : (b1'=4) & (r1'=r) & (b'=max(b,4)) - + 0.03125 : (b1'=5) & (r1'=r) & (b'=max(b,5)) - + 0.015625 : (b1'=6) & (r1'=r) & (b'=max(b,6)) - + 0.0078125 : (b1'=7) & (r1'=r) & (b'=max(b,7)) - + 0.0078125 : (b1'=8) & (r1'=r) & (b'=max(b,8)); + [] go & draw & draw1=0 -> (draw1'=1); + [] draw1=1 -> 0.5 : (b1'=1) & (r1'=r) & (b'=max(b,1)) & (draw1'=0) + + 0.25 : (b1'=2) & (r1'=r) & (b'=max(b,2)) & (draw1'=0) + + 0.125 : (b1'=3) & (r1'=r) & (b'=max(b,3)) & (draw1'=0) + + 0.0625 : (b1'=4) & (r1'=r) & (b'=max(b,4)) & (draw1'=0) + + 0.03125 : (b1'=5) & (r1'=r) & (b'=max(b,5)) & (draw1'=0) + + 0.015625 : (b1'=6) & (r1'=r) & (b'=max(b,6)) & (draw1'=0) + + 0.0078125 : (b1'=7) & (r1'=r) & (b'=max(b,7)) & (draw1'=0) + + 0.0078125 : (b1'=8) & (r1'=r) & (b'=max(b,8)) & (draw1'=0); // enter critical section and randomly set r to 1 or 2 - [] p1=1 & b=b1 & r=r1 & c=0 -> 0.5 : (r'=1) & (c'=1) & (b'=0) & (b1'=0) & (r1'=0) & (p1'=2) + [] go & p1=1 & b=b1 & r=r1 & c=0 -> 0.5 : (r'=1) & (c'=1) & (b'=0) & (b1'=0) & (r1'=0) & (p1'=2) + 0.5 : (r'=2) & (c'=1) & (b'=0) & (b1'=0) & (r1'=0) & (p1'=2); // loop when trying and cannot make a draw or enter critical section - [] p1=1 & r1=r & b1<=b & ((c=0 & b1!=b) | c=1) -> (p1'=p1); + // [] go & p1=1 & r1=r & b1<=b & ((c=0 & b1!=b) | c=1) -> (p1'=p1); // leave crictical section - [] p1=2 -> (p1'=0) & (c'=0); + [] go & p1=2 -> (p1'=0) & (c'=0); // stay in critical section - [] p1=2 -> (p1'=2); + // [] go & p1=2 -> (p1'=2); endmodule // construct further modules through renaming -module process2 = process1 [p1=p2, b1=b2, r1=r2] endmodule -module process3 = process1 [p1=p3, b1=b3, r1=r3] endmodule -module process4 = process1 [p1=p4, b1=b4, r1=r4] endmodule -module process5 = process1 [p1=p5, b1=b5, r1=r5] endmodule -module process6 = process1 [p1=p6, b1=b6, r1=r6] endmodule -module process7 = process1 [p1=p7, b1=b7, r1=r7] endmodule -module process8 = process1 [p1=p8, b1=b8, r1=r8] endmodule -module process9 = process1 [p1=p9, b1=b9, r1=r9] endmodule -module process10 = process1 [p1=p10, b1=b10, r1=r10] endmodule +module process2 = process1 [p1=p2, b1=b2, r1=r2, draw1=draw2, draw2=draw1 ] endmodule +module process3 = process1 [p1=p3, b1=b3, r1=r3, draw1=draw3, draw3=draw1 ] endmodule +module process4 = process1 [p1=p4, b1=b4, r1=r4, draw1=draw4, draw4=draw1 ] endmodule +module process5 = process1 [p1=p5, b1=b5, r1=r5, draw1=draw5, draw5=draw1 ] endmodule +module process6 = process1 [p1=p6, b1=b6, r1=r6, draw1=draw6, draw6=draw1 ] endmodule +module process7 = process1 [p1=p7, b1=b7, r1=r7, draw1=draw7, draw7=draw1 ] endmodule +module process8 = process1 [p1=p8, b1=b8, r1=r8, draw1=draw8, draw8=draw1 ] endmodule +module process9 = process1 [p1=p9, b1=b9, r1=r9, draw1=draw9, draw9=draw1 ] endmodule +module process10 = process1 [p1=p10, b1=b10, r1=r10, draw1=draw10, draw10=draw1 ] endmodule // formulas/labels for use in properties: @@ -80,3 +97,7 @@ label "one_trying" = p1=1|p2=1|p3=1|p4=1|p5=1|p6=1|p7=1|p8=1|p9=1|p10=1; // one of the processes is in the critical section label "one_critical" = p1=2|p2=2|p3=2|p4=2|p5=2|p6=2|p7=2|p8=2|p9=2|p10=2; + +// maximum value of the bi's +formula maxb = max(b1,b2,b3,b4,b5,b6,b7,b8,b9,b10); + diff --git a/prism-examples/rabin/rabin12.nm b/prism-examples/rabin/rabin12.nm deleted file mode 100644 index d535dbc7..00000000 --- a/prism-examples/rabin/rabin12.nm +++ /dev/null @@ -1,84 +0,0 @@ -// N-processor mutual exclusion [Rab82] -// with global variables to remove sychronization -// gxn/dxp 02/02/00 - -mdp - -// size of shared counter -const int K = 8; // 4+ceil(log_2 N) - -// global variables (all modules can read and write) -// c=0 critical section free -// c=1 critical section not free -// b current highest draw -// r current round - -global c : [0..1]; -global b : [0..K]; -global r : [1..2]; - -// local variables: process i -// state: pi -// 0 remainder -// 1 trying -// 2 critical section -// current draw: bi -// current round: ri - -// atomic formula for process 1 drawing -formula draw = p1=1 & (b (p1'=0); - // enter trying - [] p1=0 -> (p1'=1); - // make a draw - [] draw -> 0.5 : (b1'=1) & (r1'=r) & (b'=max(b,1)) - + 0.25 : (b1'=2) & (r1'=r) & (b'=max(b,2)) - + 0.125 : (b1'=3) & (r1'=r) & (b'=max(b,3)) - + 0.0625 : (b1'=4) & (r1'=r) & (b'=max(b,4)) - + 0.03125 : (b1'=5) & (r1'=r) & (b'=max(b,5)) - + 0.015625 : (b1'=6) & (r1'=r) & (b'=max(b,6)) - + 0.0078125 : (b1'=7) & (r1'=r) & (b'=max(b,7)) - + 0.0078125 : (b1'=8) & (r1'=r) & (b'=max(b,8)); - // enter critical section and randomly set r to 1 or 2 - [] p1=1 & b=b1 & r=r1 & c=0 -> 0.5 : (r'=1) & (c'=1) & (b'=0) & (b1'=0) & (r1'=0) & (p1'=2) - + 0.5 : (r'=2) & (c'=1) & (b'=0) & (b1'=0) & (r1'=0) & (p1'=2); - // loop when trying and cannot make a draw or enter critical section - [] p1=1 & r1=r & b1<=b & ((c=0 & b1!=b) | c=1) -> (p1'=p1); - // leave crictical section - [] p1=2 -> (p1'=0) & (c'=0); - // stay in critical section - [] p1=2 -> (p1'=2); - -endmodule - -// construct further modules through renaming -module process2 = process1 [p1=p2, b1=b2, r1=r2] endmodule -module process3 = process1 [p1=p3, b1=b3, r1=r3] endmodule -module process4 = process1 [p1=p4, b1=b4, r1=r4] endmodule -module process5 = process1 [p1=p5, b1=b5, r1=r5] endmodule -module process6 = process1 [p1=p6, b1=b6, r1=r6] endmodule -module process7 = process1 [p1=p7, b1=b7, r1=r7] endmodule -module process8 = process1 [p1=p8, b1=b8, r1=r8] endmodule -module process9 = process1 [p1=p9, b1=b9, r1=r9] endmodule -module process10 = process1 [p1=p10, b1=b10, r1=r10] endmodule -module process11 = process1 [p1=p11, b1=b11, r1=r11] endmodule -module process12 = process1 [p1=p12, b1=b12, r1=r12] endmodule - -// formulas/labels for use in properties: - -// number of processes in critical section -formula num_procs_in_crit = (p1=2?1:0)+(p2=2?1:0)+(p3=2?1:0)+(p4=2?1:0)+(p5=2?1:0)+(p6=2?1:0)+(p7=2?1:0)+(p8=2?1:0)+(p9=2?1:0)+(p10=2?1:0)+(p11=2?1:0)+(p12=2?1:0); - -// one of the processes is trying -label "one_trying" = p1=1|p2=1|p3=1|p4=1|p5=1|p6=1|p7=1|p8=1|p9=1|p10=1|p11=1|p12=1; - -// one of the processes is in the critical section -label "one_critical" = p1=2|p2=2|p3=2|p4=2|p5=2|p6=2|p7=2|p8=2|p9=2|p10=2|p11=2|p12=2; diff --git a/prism-examples/rabin/rabin3.nm b/prism-examples/rabin/rabin3.nm index b0d042b0..a29698c0 100644 --- a/prism-examples/rabin/rabin3.nm +++ b/prism-examples/rabin/rabin3.nm @@ -1,6 +1,17 @@ // N-processor mutual exclusion [Rab82] // with global variables to remove sychronization -// gxn/dxp 02/02/00 +// gxn/dxp 03/12/08 + +// version to verify a variant of the bounded waiting property +// namely the probability a process entries the critical section given it tries +// to acheive this we have split the drawing phase into two steps, so we know +// a process will draw before it actual makes the probabilistic choice +// we have however kept the two steps atomic(no other process can move one +// the first step has been made) since otherwise the adversary can prevent the +// process from actually trying in the current round by never shcedling it again + +// note we have removed the self loops to eliminate the need for fairness constraints + mdp @@ -25,41 +36,47 @@ global r : [1..2]; // current draw: bi // current round: ri -// atomic formula for process 1 drawing +// formula for process 1 drawing formula draw = p1=1 & (b (p1'=0); + // [] go & p1=0 -> (p1'=0); // enter trying - [] p1=0 -> (p1'=1); + [] go & p1=0 -> (p1'=1); // make a draw - [] draw -> 0.5 : (b1'=1) & (r1'=r) & (b'=max(b,1)) - + 0.25 : (b1'=2) & (r1'=r) & (b'=max(b,2)) - + 0.125 : (b1'=3) & (r1'=r) & (b'=max(b,3)) - + 0.0625 : (b1'=4) & (r1'=r) & (b'=max(b,4)) - + 0.03125 : (b1'=5) & (r1'=r) & (b'=max(b,5)) - + 0.03125 : (b1'=6) & (r1'=r) & (b'=max(b,6)); + [] go & draw & draw1=0 -> (draw1'=1); + [] draw1=1 -> 0.5 : (b1'=1) & (r1'=r) & (b'=max(b,1)) & (draw1'=0) + + 0.25 : (b1'=2) & (r1'=r) & (b'=max(b,2)) & (draw1'=0) + + 0.125 : (b1'=3) & (r1'=r) & (b'=max(b,3)) & (draw1'=0) + + 0.0625 : (b1'=4) & (r1'=r) & (b'=max(b,4)) & (draw1'=0) + + 0.03125 : (b1'=5) & (r1'=r) & (b'=max(b,5)) & (draw1'=0) + + 0.03125 : (b1'=6) & (r1'=r) & (b'=max(b,6)) & (draw1'=0); // enter critical section and randomly set r to 1 or 2 - [] p1=1 & b=b1 & r=r1 & c=0 -> 0.5 : (r'=1) & (c'=1) & (b'=0) & (b1'=0) & (r1'=0) & (p1'=2) + [] go & p1=1 & b=b1 & r=r1 & c=0 -> 0.5 : (r'=1) & (c'=1) & (b'=0) & (b1'=0) & (r1'=0) & (p1'=2) + 0.5 : (r'=2) & (c'=1) & (b'=0) & (b1'=0) & (r1'=0) & (p1'=2); // loop when trying and cannot make a draw or enter critical section - [] p1=1 & r1=r & b1<=b & ((c=0 & b1!=b) | c=1) -> (p1'=p1); + // [] go & p1=1 & r1=r & b1<=b & ((c=0 & b1!=b) | c=1) -> (p1'=p1); // leave crictical section - [] p1=2 -> (p1'=0) & (c'=0); + [] go & p1=2 -> (p1'=0) & (c'=0); // stay in critical section - [] p1=2 -> (p1'=2); + // [] go & p1=2 -> (p1'=2); endmodule // construct further modules through renaming -module process2 = process1 [p1=p2, b1=b2, r1=r2] endmodule -module process3 = process1 [p1=p3, b1=b3, r1=r3] endmodule +module process2 = process1 [p1=p2, b1=b2, r1=r2, draw1=draw2, draw2=draw1 ] endmodule +module process3 = process1 [p1=p3, b1=b3, r1=r3, draw1=draw3, draw3=draw1 ] endmodule // formulas/labels for use in properties: @@ -71,3 +88,7 @@ label "one_trying" = p1=1|p2=1|p3=1; // one of the processes is in the critical section label "one_critical" = p1=2|p2=2|p3=2; + +// maximum value of the bi's +formula maxb = max(b1,b2,b3); + diff --git a/prism-examples/rabin/rabin4.nm b/prism-examples/rabin/rabin4.nm index 58a23194..f4b3c416 100644 --- a/prism-examples/rabin/rabin4.nm +++ b/prism-examples/rabin/rabin4.nm @@ -1,6 +1,17 @@ // N-processor mutual exclusion [Rab82] // with global variables to remove sychronization -// gxn/dxp 02/02/00 +// gxn/dxp 03/12/08 + +// version to verify a variant of the bounded waiting property +// namely the probability a process entries the critical section given it tries +// to acheive this we have split the drawing phase into two steps, so we know +// a process will draw before it actual makes the probabilistic choice +// we have however kept the two steps atomic(no other process can move one +// the first step has been made) since otherwise the adversary can prevent the +// process from actually trying in the current round by never shcedling it again + +// note we have removed the self loops to eliminate the need for fairness constraints + mdp @@ -25,42 +36,48 @@ global r : [1..2]; // current draw: bi // current round: ri -// atomic formula for process 1 drawing +// formula for process 1 drawing formula draw = p1=1 & (b (p1'=0); + // [] go & p1=0 -> (p1'=0); // enter trying - [] p1=0 -> (p1'=1); + [] go & p1=0 -> (p1'=1); // make a draw - [] draw -> 0.5 : (b1'=1) & (r1'=r) & (b'=max(b,1)) - + 0.25 : (b1'=2) & (r1'=r) & (b'=max(b,2)) - + 0.125 : (b1'=3) & (r1'=r) & (b'=max(b,3)) - + 0.0625 : (b1'=4) & (r1'=r) & (b'=max(b,4)) - + 0.03125 : (b1'=5) & (r1'=r) & (b'=max(b,5)) - + 0.03125 : (b1'=6) & (r1'=r) & (b'=max(b,6)); + [] go & draw & draw1=0 -> (draw1'=1); + [] draw1=1 -> 0.5 : (b1'=1) & (r1'=r) & (b'=max(b,1)) & (draw1'=0) + + 0.25 : (b1'=2) & (r1'=r) & (b'=max(b,2)) & (draw1'=0) + + 0.125 : (b1'=3) & (r1'=r) & (b'=max(b,3)) & (draw1'=0) + + 0.0625 : (b1'=4) & (r1'=r) & (b'=max(b,4)) & (draw1'=0) + + 0.03125 : (b1'=5) & (r1'=r) & (b'=max(b,5)) & (draw1'=0) + + 0.03125 : (b1'=6) & (r1'=r) & (b'=max(b,6)) & (draw1'=0); // enter critical section and randomly set r to 1 or 2 - [] p1=1 & b=b1 & r=r1 & c=0 -> 0.5 : (r'=1) & (c'=1) & (b'=0) & (b1'=0) & (r1'=0) & (p1'=2) + [] go & p1=1 & b=b1 & r=r1 & c=0 -> 0.5 : (r'=1) & (c'=1) & (b'=0) & (b1'=0) & (r1'=0) & (p1'=2) + 0.5 : (r'=2) & (c'=1) & (b'=0) & (b1'=0) & (r1'=0) & (p1'=2); // loop when trying and cannot make a draw or enter critical section - [] p1=1 & r1=r & b1<=b & ((c=0 & b1!=b) | c=1) -> (p1'=p1); + // [] go & p1=1 & r1=r & b1<=b & ((c=0 & b1!=b) | c=1) -> (p1'=p1); // leave crictical section - [] p1=2 -> (p1'=0) & (c'=0); + [] go & p1=2 -> (p1'=0) & (c'=0); // stay in critical section - [] p1=2 -> (p1'=2); + // [] go & p1=2 -> (p1'=2); endmodule // construct further modules through renaming -module process2 = process1 [p1=p2, b1=b2, r1=r2] endmodule -module process3 = process1 [p1=p3, b1=b3, r1=r3] endmodule -module process4 = process1 [p1=p4, b1=b4, r1=r4] endmodule +module process2 = process1 [p1=p2, b1=b2, r1=r2, draw1=draw2, draw2=draw1 ] endmodule +module process3 = process1 [p1=p3, b1=b3, r1=r3, draw1=draw3, draw3=draw1 ] endmodule +module process4 = process1 [p1=p4, b1=b4, r1=r4, draw1=draw4, draw4=draw1 ] endmodule // formulas/labels for use in properties: @@ -72,3 +89,7 @@ label "one_trying" = p1=1|p2=1|p3=1|p4=1; // one of the processes is in the critical section label "one_critical" = p1=2|p2=2|p3=2|p4=2; + +// maximum value of the bi's +formula maxb = max(b1,b2,b3,b4); + diff --git a/prism-examples/rabin/rabin5.nm b/prism-examples/rabin/rabin5.nm index e3fb1a7e..e227b243 100644 --- a/prism-examples/rabin/rabin5.nm +++ b/prism-examples/rabin/rabin5.nm @@ -1,6 +1,17 @@ // N-processor mutual exclusion [Rab82] // with global variables to remove sychronization -// gxn/dxp 02/02/00 +// gxn/dxp 03/12/08 + +// version to verify a variant of the bounded waiting property +// namely the probability a process entries the critical section given it tries +// to acheive this we have split the drawing phase into two steps, so we know +// a process will draw before it actual makes the probabilistic choice +// we have however kept the two steps atomic(no other process can move one +// the first step has been made) since otherwise the adversary can prevent the +// process from actually trying in the current round by never shcedling it again + +// note we have removed the self loops to eliminate the need for fairness constraints + mdp @@ -25,44 +36,50 @@ global r : [1..2]; // current draw: bi // current round: ri -// atomic formula for process 1 drawing +// formula for process 1 drawing formula draw = p1=1 & (b (p1'=0); + // [] go & p1=0 -> (p1'=0); // enter trying - [] p1=0 -> (p1'=1); + [] go & p1=0 -> (p1'=1); // make a draw - [] draw -> 0.5 : (b1'=1) & (r1'=r) & (b'=max(b,1)) - + 0.25 : (b1'=2) & (r1'=r) & (b'=max(b,2)) - + 0.125 : (b1'=3) & (r1'=r) & (b'=max(b,3)) - + 0.0625 : (b1'=4) & (r1'=r) & (b'=max(b,4)) - + 0.03125 : (b1'=5) & (r1'=r) & (b'=max(b,5)) - + 0.015625 : (b1'=6) & (r1'=r) & (b'=max(b,6)) - + 0.015625 : (b1'=7) & (r1'=r) & (b'=max(b,7)); + [] go & draw & draw1=0 -> (draw1'=1); + [] draw1=1 -> 0.5 : (b1'=1) & (r1'=r) & (b'=max(b,1)) & (draw1'=0) + + 0.25 : (b1'=2) & (r1'=r) & (b'=max(b,2)) & (draw1'=0) + + 0.125 : (b1'=3) & (r1'=r) & (b'=max(b,3)) & (draw1'=0) + + 0.0625 : (b1'=4) & (r1'=r) & (b'=max(b,4)) & (draw1'=0) + + 0.03125 : (b1'=5) & (r1'=r) & (b'=max(b,5)) & (draw1'=0) + + 0.015625 : (b1'=6) & (r1'=r) & (b'=max(b,6)) & (draw1'=0) + + 0.015625 : (b1'=7) & (r1'=r) & (b'=max(b,7)) & (draw1'=0); // enter critical section and randomly set r to 1 or 2 - [] p1=1 & b=b1 & r=r1 & c=0 -> 0.5 : (r'=1) & (c'=1) & (b'=0) & (b1'=0) & (r1'=0) & (p1'=2) + [] go & p1=1 & b=b1 & r=r1 & c=0 -> 0.5 : (r'=1) & (c'=1) & (b'=0) & (b1'=0) & (r1'=0) & (p1'=2) + 0.5 : (r'=2) & (c'=1) & (b'=0) & (b1'=0) & (r1'=0) & (p1'=2); // loop when trying and cannot make a draw or enter critical section - [] p1=1 & r1=r & b1<=b & ((c=0 & b1!=b) | c=1) -> (p1'=p1); + // [] go & p1=1 & r1=r & b1<=b & ((c=0 & b1!=b) | c=1) -> (p1'=p1); // leave crictical section - [] p1=2 -> (p1'=0) & (c'=0); + [] go & p1=2 -> (p1'=0) & (c'=0); // stay in critical section - [] p1=2 -> (p1'=2); + // [] go & p1=2 -> (p1'=2); endmodule // construct further modules through renaming -module process2 = process1 [p1=p2, b1=b2, r1=r2] endmodule -module process3 = process1 [p1=p3, b1=b3, r1=r3] endmodule -module process4 = process1 [p1=p4, b1=b4, r1=r4] endmodule -module process5 = process1 [p1=p5, b1=b5, r1=r5] endmodule +module process2 = process1 [p1=p2, b1=b2, r1=r2, draw1=draw2, draw2=draw1 ] endmodule +module process3 = process1 [p1=p3, b1=b3, r1=r3, draw1=draw3, draw3=draw1 ] endmodule +module process4 = process1 [p1=p4, b1=b4, r1=r4, draw1=draw4, draw4=draw1 ] endmodule +module process5 = process1 [p1=p5, b1=b5, r1=r5, draw1=draw5, draw5=draw1 ] endmodule // formulas/labels for use in properties: @@ -74,3 +91,7 @@ label "one_trying" = p1=1|p2=1|p3=1|p4=1|p5=1; // one of the processes is in the critical section label "one_critical" = p1=2|p2=2|p3=2|p4=2|p5=2; + +// maximum value of the bi's +formula maxb = max(b1,b2,b3,b4,b5); + diff --git a/prism-examples/rabin/rabin6.nm b/prism-examples/rabin/rabin6.nm index c17d6905..33c9118b 100644 --- a/prism-examples/rabin/rabin6.nm +++ b/prism-examples/rabin/rabin6.nm @@ -1,6 +1,17 @@ // N-processor mutual exclusion [Rab82] // with global variables to remove sychronization -// gxn/dxp 02/02/00 +// gxn/dxp 03/12/08 + +// version to verify a variant of the bounded waiting property +// namely the probability a process entries the critical section given it tries +// to acheive this we have split the drawing phase into two steps, so we know +// a process will draw before it actual makes the probabilistic choice +// we have however kept the two steps atomic(no other process can move one +// the first step has been made) since otherwise the adversary can prevent the +// process from actually trying in the current round by never shcedling it again + +// note we have removed the self loops to eliminate the need for fairness constraints + mdp @@ -25,45 +36,51 @@ global r : [1..2]; // current draw: bi // current round: ri -// atomic formula for process 1 drawing +// formula for process 1 drawing formula draw = p1=1 & (b (p1'=0); + // [] go & p1=0 -> (p1'=0); // enter trying - [] p1=0 -> (p1'=1); + [] go & p1=0 -> (p1'=1); // make a draw - [] draw -> 0.5 : (b1'=1) & (r1'=r) & (b'=max(b,1)) - + 0.25 : (b1'=2) & (r1'=r) & (b'=max(b,2)) - + 0.125 : (b1'=3) & (r1'=r) & (b'=max(b,3)) - + 0.0625 : (b1'=4) & (r1'=r) & (b'=max(b,4)) - + 0.03125 : (b1'=5) & (r1'=r) & (b'=max(b,5)) - + 0.015625 : (b1'=6) & (r1'=r) & (b'=max(b,6)) - + 0.015625 : (b1'=7) & (r1'=r) & (b'=max(b,7)); + [] go & draw & draw1=0 -> (draw1'=1); + [] draw1=1 -> 0.5 : (b1'=1) & (r1'=r) & (b'=max(b,1)) & (draw1'=0) + + 0.25 : (b1'=2) & (r1'=r) & (b'=max(b,2)) & (draw1'=0) + + 0.125 : (b1'=3) & (r1'=r) & (b'=max(b,3)) & (draw1'=0) + + 0.0625 : (b1'=4) & (r1'=r) & (b'=max(b,4)) & (draw1'=0) + + 0.03125 : (b1'=5) & (r1'=r) & (b'=max(b,5)) & (draw1'=0) + + 0.015625 : (b1'=6) & (r1'=r) & (b'=max(b,6)) & (draw1'=0) + + 0.015625 : (b1'=7) & (r1'=r) & (b'=max(b,7)) & (draw1'=0); // enter critical section and randomly set r to 1 or 2 - [] p1=1 & b=b1 & r=r1 & c=0 -> 0.5 : (r'=1) & (c'=1) & (b'=0) & (b1'=0) & (r1'=0) & (p1'=2) + [] go & p1=1 & b=b1 & r=r1 & c=0 -> 0.5 : (r'=1) & (c'=1) & (b'=0) & (b1'=0) & (r1'=0) & (p1'=2) + 0.5 : (r'=2) & (c'=1) & (b'=0) & (b1'=0) & (r1'=0) & (p1'=2); // loop when trying and cannot make a draw or enter critical section - [] p1=1 & r1=r & b1<=b & ((c=0 & b1!=b) | c=1) -> (p1'=p1); + // [] go & p1=1 & r1=r & b1<=b & ((c=0 & b1!=b) | c=1) -> (p1'=p1); // leave crictical section - [] p1=2 -> (p1'=0) & (c'=0); + [] go & p1=2 -> (p1'=0) & (c'=0); // stay in critical section - [] p1=2 -> (p1'=2); + // [] go & p1=2 -> (p1'=2); endmodule // construct further modules through renaming -module process2 = process1 [p1=p2, b1=b2, r1=r2] endmodule -module process3 = process1 [p1=p3, b1=b3, r1=r3] endmodule -module process4 = process1 [p1=p4, b1=b4, r1=r4] endmodule -module process5 = process1 [p1=p5, b1=b5, r1=r5] endmodule -module process6 = process1 [p1=p6, b1=b6, r1=r6] endmodule +module process2 = process1 [p1=p2, b1=b2, r1=r2, draw1=draw2, draw2=draw1 ] endmodule +module process3 = process1 [p1=p3, b1=b3, r1=r3, draw1=draw3, draw3=draw1 ] endmodule +module process4 = process1 [p1=p4, b1=b4, r1=r4, draw1=draw4, draw4=draw1 ] endmodule +module process5 = process1 [p1=p5, b1=b5, r1=r5, draw1=draw5, draw5=draw1 ] endmodule +module process6 = process1 [p1=p6, b1=b6, r1=r6, draw1=draw6, draw6=draw1 ] endmodule // formulas/labels for use in properties: @@ -75,3 +92,7 @@ label "one_trying" = p1=1|p2=1|p3=1|p4=1|p5=1|p6=1; // one of the processes is in the critical section label "one_critical" = p1=2|p2=2|p3=2|p4=2|p5=2|p6=2; + +// maximum value of the bi's +formula maxb = max(b1,b2,b3,b4,b5,b6); + diff --git a/prism-examples/rabin/modified/mod_rabin7.nm b/prism-examples/rabin/rabin7.nm similarity index 82% rename from prism-examples/rabin/modified/mod_rabin7.nm rename to prism-examples/rabin/rabin7.nm index 6d975466..50dc5e43 100644 --- a/prism-examples/rabin/modified/mod_rabin7.nm +++ b/prism-examples/rabin/rabin7.nm @@ -2,14 +2,16 @@ // with global variables to remove sychronization // gxn/dxp 03/12/08 -// modified version to verify a variant of the bounded waiting property -// namely the probability a process entries the critical sectiongiven it tries +// version to verify a variant of the bounded waiting property +// namely the probability a process entries the critical section given it tries +// to acheive this we have split the drawing phase into two steps, so we know +// a process will draw before it actual makes the probabilistic choice +// we have however kept the two steps atomic(no other process can move one +// the first step has been made) since otherwise the adversary can prevent the +// process from actually trying in the current round by never shcedling it again -// note we have removed the self loops to allow the fairness constraints -// to be ignored during verification +// note we have removed the self loops to eliminate the need for fairness constraints -// split the drawing phase into two steps but is still atomic as no -// other process can move one the first step has been made mdp diff --git a/prism-examples/rabin/rabin8.nm b/prism-examples/rabin/rabin8.nm index 30de7c7e..69c7070c 100644 --- a/prism-examples/rabin/rabin8.nm +++ b/prism-examples/rabin/rabin8.nm @@ -1,6 +1,17 @@ // N-processor mutual exclusion [Rab82] // with global variables to remove sychronization -// gxn/dxp 02/02/00 +// gxn/dxp 03/12/08 + +// version to verify a variant of the bounded waiting property +// namely the probability a process entries the critical section given it tries +// to acheive this we have split the drawing phase into two steps, so we know +// a process will draw before it actual makes the probabilistic choice +// we have however kept the two steps atomic(no other process can move one +// the first step has been made) since otherwise the adversary can prevent the +// process from actually trying in the current round by never shcedling it again + +// note we have removed the self loops to eliminate the need for fairness constraints + mdp @@ -25,47 +36,53 @@ global r : [1..2]; // current draw: bi // current round: ri -// atomic formula for process 1 drawing +// formula for process 1 drawing formula draw = p1=1 & (b (p1'=0); + // [] go & p1=0 -> (p1'=0); // enter trying - [] p1=0 -> (p1'=1); + [] go & p1=0 -> (p1'=1); // make a draw - [] draw -> 0.5 : (b1'=1) & (r1'=r) & (b'=max(b,1)) - + 0.25 : (b1'=2) & (r1'=r) & (b'=max(b,2)) - + 0.125 : (b1'=3) & (r1'=r) & (b'=max(b,3)) - + 0.0625 : (b1'=4) & (r1'=r) & (b'=max(b,4)) - + 0.03125 : (b1'=5) & (r1'=r) & (b'=max(b,5)) - + 0.015625 : (b1'=6) & (r1'=r) & (b'=max(b,6)) - + 0.015625 : (b1'=7) & (r1'=r) & (b'=max(b,7)); + [] go & draw & draw1=0 -> (draw1'=1); + [] draw1=1 -> 0.5 : (b1'=1) & (r1'=r) & (b'=max(b,1)) & (draw1'=0) + + 0.25 : (b1'=2) & (r1'=r) & (b'=max(b,2)) & (draw1'=0) + + 0.125 : (b1'=3) & (r1'=r) & (b'=max(b,3)) & (draw1'=0) + + 0.0625 : (b1'=4) & (r1'=r) & (b'=max(b,4)) & (draw1'=0) + + 0.03125 : (b1'=5) & (r1'=r) & (b'=max(b,5)) & (draw1'=0) + + 0.015625 : (b1'=6) & (r1'=r) & (b'=max(b,6)) & (draw1'=0) + + 0.015625 : (b1'=7) & (r1'=r) & (b'=max(b,7)) & (draw1'=0); // enter critical section and randomly set r to 1 or 2 - [] p1=1 & b=b1 & r=r1 & c=0 -> 0.5 : (r'=1) & (c'=1) & (b'=0) & (b1'=0) & (r1'=0) & (p1'=2) + [] go & p1=1 & b=b1 & r=r1 & c=0 -> 0.5 : (r'=1) & (c'=1) & (b'=0) & (b1'=0) & (r1'=0) & (p1'=2) + 0.5 : (r'=2) & (c'=1) & (b'=0) & (b1'=0) & (r1'=0) & (p1'=2); // loop when trying and cannot make a draw or enter critical section - [] p1=1 & r1=r & b1<=b & ((c=0 & b1!=b) | c=1) -> (p1'=p1); + // [] go & p1=1 & r1=r & b1<=b & ((c=0 & b1!=b) | c=1) -> (p1'=p1); // leave crictical section - [] p1=2 -> (p1'=0) & (c'=0); + [] go & p1=2 -> (p1'=0) & (c'=0); // stay in critical section - [] p1=2 -> (p1'=2); + // [] go & p1=2 -> (p1'=2); endmodule // construct further modules through renaming -module process2 = process1 [p1=p2, b1=b2, r1=r2] endmodule -module process3 = process1 [p1=p3, b1=b3, r1=r3] endmodule -module process4 = process1 [p1=p4, b1=b4, r1=r4] endmodule -module process5 = process1 [p1=p5, b1=b5, r1=r5] endmodule -module process6 = process1 [p1=p6, b1=b6, r1=r6] endmodule -module process7 = process1 [p1=p7, b1=b7, r1=r7] endmodule -module process8 = process1 [p1=p8, b1=b8, r1=r8] endmodule +module process2 = process1 [p1=p2, b1=b2, r1=r2, draw1=draw2, draw2=draw1 ] endmodule +module process3 = process1 [p1=p3, b1=b3, r1=r3, draw1=draw3, draw3=draw1 ] endmodule +module process4 = process1 [p1=p4, b1=b4, r1=r4, draw1=draw4, draw4=draw1 ] endmodule +module process5 = process1 [p1=p5, b1=b5, r1=r5, draw1=draw5, draw5=draw1 ] endmodule +module process6 = process1 [p1=p6, b1=b6, r1=r6, draw1=draw6, draw6=draw1 ] endmodule +module process7 = process1 [p1=p7, b1=b7, r1=r7, draw1=draw7, draw7=draw1 ] endmodule +module process8 = process1 [p1=p8, b1=b8, r1=r8, draw1=draw8, draw8=draw1 ] endmodule // formulas/labels for use in properties: @@ -77,3 +94,7 @@ label "one_trying" = p1=1|p2=1|p3=1|p4=1|p5=1|p6=1|p7=1|p8=1; // one of the processes is in the critical section label "one_critical" = p1=2|p2=2|p3=2|p4=2|p5=2|p6=2|p7=2|p8=2; + +// maximum value of the bi's +formula maxb = max(b1,b2,b3,b4,b5,b6,b7,b8); + diff --git a/prism-examples/rabin/modified/mod_rabin9.nm b/prism-examples/rabin/rabin9.nm similarity index 83% rename from prism-examples/rabin/modified/mod_rabin9.nm rename to prism-examples/rabin/rabin9.nm index 7bd58f09..fdb67853 100644 --- a/prism-examples/rabin/modified/mod_rabin9.nm +++ b/prism-examples/rabin/rabin9.nm @@ -2,14 +2,16 @@ // with global variables to remove sychronization // gxn/dxp 03/12/08 -// modified version to verify a variant of the bounded waiting property -// namely the probability a process entries the critical sectiongiven it tries +// version to verify a variant of the bounded waiting property +// namely the probability a process entries the critical section given it tries +// to acheive this we have split the drawing phase into two steps, so we know +// a process will draw before it actual makes the probabilistic choice +// we have however kept the two steps atomic(no other process can move one +// the first step has been made) since otherwise the adversary can prevent the +// process from actually trying in the current round by never shcedling it again -// note we have removed the self loops to allow the fairness constraints -// to be ignored during verification +// note we have removed the self loops to eliminate the need for fairness constraints -// split the drawing phase into two steps but is still atomic as no -// other process can move one the first step has been made mdp