diff --git a/prism-examples/rabin/rabin10.nm b/prism-examples/rabin/rabin10.nm index 3527e331..6d39b325 100644 --- a/prism-examples/rabin/rabin10.nm +++ b/prism-examples/rabin/rabin10.nm @@ -1,17 +1,18 @@ // N-processor mutual exclusion [Rab82] -// with global variables to remove sychronization // 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 +// modified version to analyse the bounded waiting property +// more precisely we analyse the waeker property: +// "the minimum probability a process enters the critical section given the process tries" -// note we have removed the self loops to eliminate the need for fairness constraints +// we modify the model by dividing the step corresponding to a process making a draw into two steps +// this allows one to identify states where a process will draw without knowing +// what value the process will randomly pick +// these two steps are atomic (i.e. no other process can move one the first step has been made) +// as otherwise the adversary can prevent the process from actually drawing in the current round +// by not scheduling it after it has performed the first step +// to remove the need for fairness constraints we have also removed the self loops from the model mdp @@ -19,36 +20,30 @@ mdp 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 + + + +global c : [0..1]; // 0/1 critical section free/taken +global b : [0..K]; // current highest draw +global r : [1..2]; // current round + // formula for process 1 drawing formula draw = p1=1 & (b (p1'=0); @@ -66,7 +61,7 @@ module process1 + 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); + + 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 @@ -98,6 +93,6 @@ 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 +// maximum current draw of the processes formula maxb = max(b1,b2,b3,b4,b5,b6,b7,b8,b9,b10); diff --git a/prism-examples/rabin/rabin3.nm b/prism-examples/rabin/rabin3.nm index a29698c0..84d40bb9 100644 --- a/prism-examples/rabin/rabin3.nm +++ b/prism-examples/rabin/rabin3.nm @@ -1,17 +1,18 @@ // N-processor mutual exclusion [Rab82] -// with global variables to remove sychronization // 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 +// modified version to analyse the bounded waiting property +// more precisely we analyse the waeker property: +// "the minimum probability a process enters the critical section given the process tries" -// note we have removed the self loops to eliminate the need for fairness constraints +// we modify the model by dividing the step corresponding to a process making a draw into two steps +// this allows one to identify states where a process will draw without knowing +// what value the process will randomly pick +// these two steps are atomic (i.e. no other process can move one the first step has been made) +// as otherwise the adversary can prevent the process from actually drawing in the current round +// by not scheduling it after it has performed the first step +// to remove the need for fairness constraints we have also removed the self loops from the model mdp @@ -19,36 +20,30 @@ mdp 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 + + + +global c : [0..1]; // 0/1 critical section free/taken +global b : [0..K]; // current highest draw +global r : [1..2]; // current round + // formula for process 1 drawing formula draw = p1=1 & (b (p1'=0); @@ -64,7 +59,7 @@ module process1 + 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); + + 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 @@ -89,6 +84,6 @@ 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 +// maximum current draw of the processes formula maxb = max(b1,b2,b3); diff --git a/prism-examples/rabin/rabin4.nm b/prism-examples/rabin/rabin4.nm index f4b3c416..23f9f4dd 100644 --- a/prism-examples/rabin/rabin4.nm +++ b/prism-examples/rabin/rabin4.nm @@ -1,17 +1,18 @@ // N-processor mutual exclusion [Rab82] -// with global variables to remove sychronization // 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 +// modified version to analyse the bounded waiting property +// more precisely we analyse the waeker property: +// "the minimum probability a process enters the critical section given the process tries" -// note we have removed the self loops to eliminate the need for fairness constraints +// we modify the model by dividing the step corresponding to a process making a draw into two steps +// this allows one to identify states where a process will draw without knowing +// what value the process will randomly pick +// these two steps are atomic (i.e. no other process can move one the first step has been made) +// as otherwise the adversary can prevent the process from actually drawing in the current round +// by not scheduling it after it has performed the first step +// to remove the need for fairness constraints we have also removed the self loops from the model mdp @@ -19,36 +20,30 @@ mdp 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 + + + +global c : [0..1]; // 0/1 critical section free/taken +global b : [0..K]; // current highest draw +global r : [1..2]; // current round + // formula for process 1 drawing formula draw = p1=1 & (b (p1'=0); @@ -64,7 +59,7 @@ module process1 + 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); + + 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 @@ -90,6 +85,6 @@ 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 +// maximum current draw of the processes formula maxb = max(b1,b2,b3,b4); diff --git a/prism-examples/rabin/rabin5.nm b/prism-examples/rabin/rabin5.nm index e227b243..dfdb2a3f 100644 --- a/prism-examples/rabin/rabin5.nm +++ b/prism-examples/rabin/rabin5.nm @@ -1,17 +1,18 @@ // N-processor mutual exclusion [Rab82] -// with global variables to remove sychronization // 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 +// modified version to analyse the bounded waiting property +// more precisely we analyse the waeker property: +// "the minimum probability a process enters the critical section given the process tries" -// note we have removed the self loops to eliminate the need for fairness constraints +// we modify the model by dividing the step corresponding to a process making a draw into two steps +// this allows one to identify states where a process will draw without knowing +// what value the process will randomly pick +// these two steps are atomic (i.e. no other process can move one the first step has been made) +// as otherwise the adversary can prevent the process from actually drawing in the current round +// by not scheduling it after it has performed the first step +// to remove the need for fairness constraints we have also removed the self loops from the model mdp @@ -19,36 +20,30 @@ mdp 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 + + + +global c : [0..1]; // 0/1 critical section free/taken +global b : [0..K]; // current highest draw +global r : [1..2]; // current round + // formula for process 1 drawing formula draw = p1=1 & (b (p1'=0); @@ -65,7 +60,7 @@ module process1 + 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); + + 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 @@ -92,6 +87,6 @@ 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 +// maximum current draw of the processes formula maxb = max(b1,b2,b3,b4,b5); diff --git a/prism-examples/rabin/rabin6.nm b/prism-examples/rabin/rabin6.nm index 33c9118b..4a8f18fc 100644 --- a/prism-examples/rabin/rabin6.nm +++ b/prism-examples/rabin/rabin6.nm @@ -1,17 +1,18 @@ // N-processor mutual exclusion [Rab82] -// with global variables to remove sychronization // 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 +// modified version to analyse the bounded waiting property +// more precisely we analyse the waeker property: +// "the minimum probability a process enters the critical section given the process tries" -// note we have removed the self loops to eliminate the need for fairness constraints +// we modify the model by dividing the step corresponding to a process making a draw into two steps +// this allows one to identify states where a process will draw without knowing +// what value the process will randomly pick +// these two steps are atomic (i.e. no other process can move one the first step has been made) +// as otherwise the adversary can prevent the process from actually drawing in the current round +// by not scheduling it after it has performed the first step +// to remove the need for fairness constraints we have also removed the self loops from the model mdp @@ -19,36 +20,30 @@ mdp 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 + + + +global c : [0..1]; // 0/1 critical section free/taken +global b : [0..K]; // current highest draw +global r : [1..2]; // current round + // formula for process 1 drawing formula draw = p1=1 & (b (p1'=0); @@ -65,7 +60,7 @@ module process1 + 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); + + 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 @@ -93,6 +88,6 @@ 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 +// maximum current draw of the processes formula maxb = max(b1,b2,b3,b4,b5,b6); diff --git a/prism-examples/rabin/rabin7.nm b/prism-examples/rabin/rabin7.nm index 50dc5e43..6f0cf342 100644 --- a/prism-examples/rabin/rabin7.nm +++ b/prism-examples/rabin/rabin7.nm @@ -1,17 +1,18 @@ // N-processor mutual exclusion [Rab82] -// with global variables to remove sychronization // 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 +// modified version to analyse the bounded waiting property +// more precisely we analyse the waeker property: +// "the minimum probability a process enters the critical section given the process tries" -// note we have removed the self loops to eliminate the need for fairness constraints +// we modify the model by dividing the step corresponding to a process making a draw into two steps +// this allows one to identify states where a process will draw without knowing +// what value the process will randomly pick +// these two steps are atomic (i.e. no other process can move one the first step has been made) +// as otherwise the adversary can prevent the process from actually drawing in the current round +// by not scheduling it after it has performed the first step +// to remove the need for fairness constraints we have also removed the self loops from the model mdp @@ -19,36 +20,30 @@ mdp 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 + + + +global c : [0..1]; // 0/1 critical section free/taken +global b : [0..K]; // current highest draw +global r : [1..2]; // current round + // formula for process 1 drawing formula draw = p1=1 & (b (p1'=0); @@ -65,7 +60,7 @@ module process1 + 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); + + 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 @@ -94,6 +89,6 @@ 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 +// maximum current draw of the processes formula maxb = max(b1,b2,b3,b4,b5,b6,b7); diff --git a/prism-examples/rabin/rabin8.nm b/prism-examples/rabin/rabin8.nm index 69c7070c..d10dff90 100644 --- a/prism-examples/rabin/rabin8.nm +++ b/prism-examples/rabin/rabin8.nm @@ -1,17 +1,18 @@ // N-processor mutual exclusion [Rab82] -// with global variables to remove sychronization // 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 +// modified version to analyse the bounded waiting property +// more precisely we analyse the waeker property: +// "the minimum probability a process enters the critical section given the process tries" -// note we have removed the self loops to eliminate the need for fairness constraints +// we modify the model by dividing the step corresponding to a process making a draw into two steps +// this allows one to identify states where a process will draw without knowing +// what value the process will randomly pick +// these two steps are atomic (i.e. no other process can move one the first step has been made) +// as otherwise the adversary can prevent the process from actually drawing in the current round +// by not scheduling it after it has performed the first step +// to remove the need for fairness constraints we have also removed the self loops from the model mdp @@ -19,36 +20,30 @@ mdp 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 + + + +global c : [0..1]; // 0/1 critical section free/taken +global b : [0..K]; // current highest draw +global r : [1..2]; // current round + // formula for process 1 drawing formula draw = p1=1 & (b (p1'=0); @@ -65,7 +60,7 @@ module process1 + 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); + + 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 @@ -95,6 +90,6 @@ 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 +// maximum current draw of the processes formula maxb = max(b1,b2,b3,b4,b5,b6,b7,b8); diff --git a/prism-examples/rabin/rabin9.nm b/prism-examples/rabin/rabin9.nm index fdb67853..961536c0 100644 --- a/prism-examples/rabin/rabin9.nm +++ b/prism-examples/rabin/rabin9.nm @@ -1,17 +1,18 @@ // N-processor mutual exclusion [Rab82] -// with global variables to remove sychronization // 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 +// modified version to analyse the bounded waiting property +// more precisely we analyse the waeker property: +// "the minimum probability a process enters the critical section given the process tries" -// note we have removed the self loops to eliminate the need for fairness constraints +// we modify the model by dividing the step corresponding to a process making a draw into two steps +// this allows one to identify states where a process will draw without knowing +// what value the process will randomly pick +// these two steps are atomic (i.e. no other process can move one the first step has been made) +// as otherwise the adversary can prevent the process from actually drawing in the current round +// by not scheduling it after it has performed the first step +// to remove the need for fairness constraints we have also removed the self loops from the model mdp @@ -19,36 +20,30 @@ mdp 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 + + + +global c : [0..1]; // 0/1 critical section free/taken +global b : [0..K]; // current highest draw +global r : [1..2]; // current round + // formula for process 1 drawing formula draw = p1=1 & (b (p1'=0); @@ -66,7 +61,7 @@ module process1 + 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); + + 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 @@ -97,6 +92,6 @@ label "one_trying" = p1=1|p2=1|p3=1|p4=1|p5=1|p6=1|p7=1|p8=1|p9=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; -// maximum value of the bi's +// maximum current draw of the processes formula maxb = max(b1,b2,b3,b4,b5,b6,b7,b8,b9);