From edaccf8c4bd2ef40e997e2400de5b44e9f1d38ff Mon Sep 17 00:00:00 2001
From: Gethin Norman <gethin.norman@glasgow.ac.uk>
Date: Mon, 8 Dec 2008 09:47:29 +0000
Subject: [PATCH] update to auto file

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@876 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism-examples/rabin/.rabinN.nm.pp | 57 +++++++++++++-----------------
 1 file changed, 25 insertions(+), 32 deletions(-)

diff --git a/prism-examples/rabin/.rabinN.nm.pp b/prism-examples/rabin/.rabinN.nm.pp
index 7b69712d..2ea483d7 100644
--- a/prism-examples/rabin/.rabinN.nm.pp
+++ b/prism-examples/rabin/.rabinN.nm.pp
@@ -1,19 +1,20 @@
 #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
 
-// 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
 
@@ -21,36 +22,28 @@ mdp
 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
 
+ 

+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 = (#& i=2:N#draw#i#=0#end#);
 
 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);
@@ -62,7 +55,7 @@ module process1
 	         #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);
+	                                  + 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
@@ -87,5 +80,5 @@ 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
+// maximum current draw of the processes
 formula maxb = max(b1#for i=2:N#,b#i##end#);