diff --git a/prism-examples/rabin/README b/prism-examples/rabin/README index 209d7695..0afe26c4 100644 --- a/prism-examples/rabin/README +++ b/prism-examples/rabin/README @@ -1,6 +1,10 @@ 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 +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/modified/.autopp b/prism-examples/rabin/modified/.autopp new file mode 100755 index 00000000..ca9b6c18 --- /dev/null +++ b/prism-examples/rabin/modified/.autopp @@ -0,0 +1,7 @@ +#!/bin/csh + +foreach N ( 3 4 5 6 7 8) + 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 new file mode 100644 index 00000000..49c79f24 --- /dev/null +++ b/prism-examples/rabin/modified/.mod_rabinN.nm.pp @@ -0,0 +1,89 @@ +#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/.rabinN.nm.pp b/prism-examples/rabin/modified/.rabinN.nm.pp new file mode 100644 index 00000000..0341e44c --- /dev/null +++ b/prism-examples/rabin/modified/.rabinN.nm.pp @@ -0,0 +1,71 @@ +#const N# +#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 + +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 + +// atomic formula for process 1 drawing +formula draw = p1=1 & (b (p1'=0); + // enter trying + [] 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#)); + // 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 +#for i=2:N# +module process#i# = process1 [p1=p#i#, b1=b#i#, r1=r#i#] 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#; diff --git a/prism-examples/rabin/modified/mod_rabin.pctl b/prism-examples/rabin/modified/mod_rabin.pctl new file mode 100644 index 00000000..c5137232 --- /dev/null +++ b/prism-examples/rabin/modified/mod_rabin.pctl @@ -0,0 +1,15 @@ +//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 +// 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_rabin3.nm b/prism-examples/rabin/modified/mod_rabin3.nm new file mode 100644 index 00000000..d5eaed51 --- /dev/null +++ b/prism-examples/rabin/modified/mod_rabin3.nm @@ -0,0 +1,92 @@ +// 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 new file mode 100644 index 00000000..61fc7402 --- /dev/null +++ b/prism-examples/rabin/modified/mod_rabin4.nm @@ -0,0 +1,93 @@ +// 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 new file mode 100644 index 00000000..03ec85c4 --- /dev/null +++ b/prism-examples/rabin/modified/mod_rabin5.nm @@ -0,0 +1,95 @@ +// 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 new file mode 100644 index 00000000..a13c2607 --- /dev/null +++ b/prism-examples/rabin/modified/mod_rabin6.nm @@ -0,0 +1,96 @@ +// 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_rabin7.nm b/prism-examples/rabin/modified/mod_rabin7.nm new file mode 100644 index 00000000..fe02af4c --- /dev/null +++ b/prism-examples/rabin/modified/mod_rabin7.nm @@ -0,0 +1,97 @@ +// 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 + +// 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); + +// one of the processes is trying +label "one_trying" = p1=1|p2=1|p3=1|p4=1|p5=1|p6=1|p7=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; + +// maximum value of the bi's +formula maxb = max(b1,b2 ,b3 ,b4 ,b5 ,b6 ,b7 ); + diff --git a/prism-examples/rabin/modified/mod_rabin8.nm b/prism-examples/rabin/modified/mod_rabin8.nm new file mode 100644 index 00000000..4500a634 --- /dev/null +++ b/prism-examples/rabin/modified/mod_rabin8.nm @@ -0,0 +1,98 @@ +// 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 ); +