Browse Source
updated rabin example
updated rabin example
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@872 bbc10eb1-c90d-0410-af57-cb519fbb1720master
Gethin Norman
17 years ago
23 changed files with 327 additions and 939 deletions
-
2prism-examples/rabin/.autopp
-
46prism-examples/rabin/.rabinN.nm.pp
-
4prism-examples/rabin/README
-
16prism-examples/rabin/auto
-
7prism-examples/rabin/modified/.autopp
-
89prism-examples/rabin/modified/.mod_rabinN.nm.pp
-
23prism-examples/rabin/modified/mod_rabin.pctl
-
101prism-examples/rabin/modified/mod_rabin10.nm
-
92prism-examples/rabin/modified/mod_rabin3.nm
-
93prism-examples/rabin/modified/mod_rabin4.nm
-
95prism-examples/rabin/modified/mod_rabin5.nm
-
96prism-examples/rabin/modified/mod_rabin6.nm
-
98prism-examples/rabin/modified/mod_rabin8.nm
-
28prism-examples/rabin/rabin.pctl
-
71prism-examples/rabin/rabin10.nm
-
84prism-examples/rabin/rabin12.nm
-
53prism-examples/rabin/rabin3.nm
-
55prism-examples/rabin/rabin4.nm
-
59prism-examples/rabin/rabin5.nm
-
61prism-examples/rabin/rabin6.nm
-
14prism-examples/rabin/rabin7.nm
-
65prism-examples/rabin/rabin8.nm
-
14prism-examples/rabin/rabin9.nm
@ -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 |
|||
|
|||
@ -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 |
|||
|
|||
@ -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 |
|||
@ -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<b1 | r!=r1); |
|||
|
|||
// formula to keep drawing phase atomic |
|||
// (can onlymove if no process is drawing |
|||
formula go = (#& i=2:N#draw#i#=0#end#); |
|||
|
|||
module process1 |
|||
|
|||
p1 : [0..2]; |
|||
b1 : [0..K]; |
|||
r1 : [0..2]; |
|||
draw1 : [0..1]; |
|||
|
|||
// remain in remainder |
|||
// [] go & p1=0 -> (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#);
|
|||
@ -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 ] |
|||
|
|||
@ -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<b1 | r!=r1); |
|||
|
|||
// formula to keep drawing phase atomic |
|||
// (can onlymove if no process is drawing |
|||
formula go = (draw2=0&draw3=0&draw4=0&draw5=0&draw6=0&draw7=0&draw8=0&draw9=0&draw10=0); |
|||
|
|||
module process1 |
|||
|
|||
p1 : [0..2]; |
|||
b1 : [0..K]; |
|||
r1 : [0..2]; |
|||
draw1 : [0..1]; |
|||
|
|||
// remain in remainder |
|||
// [] go & p1=0 -> (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); |
|||
|
|||
@ -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<b1 | r!=r1); |
|||
|
|||
// formula to keep drawing phase atomic |
|||
// (can onlymove if no process is drawing |
|||
formula go = (draw2=0&draw3=0); |
|||
|
|||
module process1 |
|||
|
|||
p1 : [0..2]; |
|||
b1 : [0..K]; |
|||
r1 : [0..2]; |
|||
draw1 : [0..1]; |
|||
|
|||
// remain in remainder |
|||
// [] go & p1=0 -> (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); |
|||
|
|||
@ -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<b1 | r!=r1); |
|||
|
|||
// formula to keep drawing phase atomic |
|||
// (can onlymove if no process is drawing |
|||
formula go = (draw2=0&draw3=0&draw4=0); |
|||
|
|||
module process1 |
|||
|
|||
p1 : [0..2]; |
|||
b1 : [0..K]; |
|||
r1 : [0..2]; |
|||
draw1 : [0..1]; |
|||
|
|||
// remain in remainder |
|||
// [] go & p1=0 -> (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); |
|||
|
|||
@ -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<b1 | r!=r1); |
|||
|
|||
// formula to keep drawing phase atomic |
|||
// (can onlymove if no process is drawing |
|||
formula go = (draw2=0&draw3=0&draw4=0&draw5=0); |
|||
|
|||
module process1 |
|||
|
|||
p1 : [0..2]; |
|||
b1 : [0..K]; |
|||
r1 : [0..2]; |
|||
draw1 : [0..1]; |
|||
|
|||
// remain in remainder |
|||
// [] go & p1=0 -> (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); |
|||
|
|||
@ -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<b1 | r!=r1); |
|||
|
|||
// formula to keep drawing phase atomic |
|||
// (can onlymove if no process is drawing |
|||
formula go = (draw2=0&draw3=0&draw4=0&draw5=0&draw6=0); |
|||
|
|||
module process1 |
|||
|
|||
p1 : [0..2]; |
|||
b1 : [0..K]; |
|||
r1 : [0..2]; |
|||
draw1 : [0..1]; |
|||
|
|||
// remain in remainder |
|||
// [] go & p1=0 -> (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); |
|||
|
|||
@ -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<b1 | r!=r1); |
|||
|
|||
// formula to keep drawing phase atomic |
|||
// (can onlymove if no process is drawing |
|||
formula go = (draw2=0&draw3=0&draw4=0&draw5=0&draw6=0&draw7=0&draw8=0); |
|||
|
|||
module process1 |
|||
|
|||
p1 : [0..2]; |
|||
b1 : [0..K]; |
|||
r1 : [0..2]; |
|||
draw1 : [0..1]; |
|||
|
|||
// remain in remainder |
|||
// [] go & p1=0 -> (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); |
|||
|
|||
@ -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 ] |
|||
|
|||
@ -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<b1 | r!=r1); |
|||
|
|||
module process1 |
|||
|
|||
p1 : [0..2]; |
|||
b1 : [0..K]; |
|||
r1 : [0..2]; |
|||
|
|||
// remain in remainder |
|||
[] p1=0 -> (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; |
|||
Write
Preview
Loading…
Cancel
Save
Reference in new issue