s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

fixed model files 

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@882 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Gethin Norman 18 years ago
parent
e9bcc66bd1
commit
fcd68cef29
8 changed files with 216 additions and 256 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 59
      prism-examples/rabin/rabin10.nm
  2. 59
      prism-examples/rabin/rabin3.nm
  3. 59
      prism-examples/rabin/rabin4.nm
  4. 59
      prism-examples/rabin/rabin5.nm
  5. 59
      prism-examples/rabin/rabin6.nm
  6. 59
      prism-examples/rabin/rabin7.nm
  7. 59
      prism-examples/rabin/rabin8.nm
  8. 59
      prism-examples/rabin/rabin9.nm

59
prism-examples/rabin/rabin10.nm
View File

@ -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<b1 | r!=r1);
// formula to keep drawing phase atomic
// (can onlymove if no process is drawing
// (a process can only move if no other process is in the middle of 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];
p1 : [0..2]; // local state
// 0 remainder
// 1 trying
// 2 critical section
b1 : [0..K]; // current draw: bi
r1 : [0..2]; // current round: ri
draw1 : [0..1]; // performed first step of drawing phase
// remain in remainder
// [] go & p1=0 -> (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);

59
prism-examples/rabin/rabin3.nm
View File

@ -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<b1 | r!=r1);
// formula to keep drawing phase atomic
// (can onlymove if no process is drawing
// (a process can only move if no other process is in the middle of drawing)
formula go = (draw2=0&draw3=0);
module process1
p1 : [0..2];
b1 : [0..K];
r1 : [0..2];
draw1 : [0..1];
p1 : [0..2]; // local state
// 0 remainder
// 1 trying
// 2 critical section
b1 : [0..K]; // current draw: bi
r1 : [0..2]; // current round: ri
draw1 : [0..1]; // performed first step of drawing phase
// remain in remainder
// [] go & p1=0 -> (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);

59
prism-examples/rabin/rabin4.nm
View File

@ -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<b1 | r!=r1);
// formula to keep drawing phase atomic
// (can onlymove if no process is drawing
// (a process can only move if no other process is in the middle of drawing)
formula go = (draw2=0&draw3=0&draw4=0);
module process1
p1 : [0..2];
b1 : [0..K];
r1 : [0..2];
draw1 : [0..1];
p1 : [0..2]; // local state
// 0 remainder
// 1 trying
// 2 critical section
b1 : [0..K]; // current draw: bi
r1 : [0..2]; // current round: ri
draw1 : [0..1]; // performed first step of drawing phase
// remain in remainder
// [] go & p1=0 -> (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);

59
prism-examples/rabin/rabin5.nm
View File

@ -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<b1 | r!=r1);
// formula to keep drawing phase atomic
// (can onlymove if no process is drawing
// (a process can only move if no other process is in the middle of 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];
p1 : [0..2]; // local state
// 0 remainder
// 1 trying
// 2 critical section
b1 : [0..K]; // current draw: bi
r1 : [0..2]; // current round: ri
draw1 : [0..1]; // performed first step of drawing phase
// remain in remainder
// [] go & p1=0 -> (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);

59
prism-examples/rabin/rabin6.nm
View File

@ -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<b1 | r!=r1);
// formula to keep drawing phase atomic
// (can onlymove if no process is drawing
// (a process can only move if no other process is in the middle of 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];
p1 : [0..2]; // local state
// 0 remainder
// 1 trying
// 2 critical section
b1 : [0..K]; // current draw: bi
r1 : [0..2]; // current round: ri
draw1 : [0..1]; // performed first step of drawing phase
// remain in remainder
// [] go & p1=0 -> (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);

59
prism-examples/rabin/rabin7.nm
View File

@ -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<b1 | r!=r1);
// formula to keep drawing phase atomic
// (can onlymove if no process is drawing
// (a process can only move if no other process is in the middle of drawing)
formula go = (draw2=0&draw3=0&draw4=0&draw5=0&draw6=0&draw7=0);
module process1
p1 : [0..2];
b1 : [0..K];
r1 : [0..2];
draw1 : [0..1];
p1 : [0..2]; // local state
// 0 remainder
// 1 trying
// 2 critical section
b1 : [0..K]; // current draw: bi
r1 : [0..2]; // current round: ri
draw1 : [0..1]; // performed first step of drawing phase
// remain in remainder
// [] go & p1=0 -> (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);

59
prism-examples/rabin/rabin8.nm
View File

@ -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<b1 | r!=r1);
// formula to keep drawing phase atomic
// (can onlymove if no process is drawing
// (a process can only move if no other process is in the middle of 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];
p1 : [0..2]; // local state
// 0 remainder
// 1 trying
// 2 critical section
b1 : [0..K]; // current draw: bi
r1 : [0..2]; // current round: ri
draw1 : [0..1]; // performed first step of drawing phase
// remain in remainder
// [] go & p1=0 -> (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);

59
prism-examples/rabin/rabin9.nm
View File

@ -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<b1 | r!=r1);
// formula to keep drawing phase atomic
// (can onlymove if no process is drawing
// (a process can only move if no other process is in the middle of drawing)
formula go = (draw2=0&draw3=0&draw4=0&draw5=0&draw6=0&draw7=0&draw8=0&draw9=0);
module process1
p1 : [0..2];
b1 : [0..K];
r1 : [0..2];
draw1 : [0..1];
p1 : [0..2]; // local state
// 0 remainder
// 1 trying
// 2 critical section
b1 : [0..K]; // current draw: bi
r1 : [0..2]; // current round: ri
draw1 : [0..1]; // performed first step of drawing phase
// remain in remainder
// [] go & p1=0 -> (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);
Write Preview
Loading…
Cancel
Save