Change parameter names (K->COL, bmax->K) to align with MDP benchmark of same name.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4835 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism-examples/pta/csma/abst/auto

@@ -1,7 +1,7 @@
 #!/bin/csh
 
-prism csma.nm -const bmax=1 eventually.pctl -aroptions refine=all,nopre,opt
+prism csma.nm -const K=1 eventually.pctl -aroptions refine=all,nopre,opt
 
-prism csma.nm -const bmax=1 deadline.pctl -const T=1000 -aroptions refine=all,nopre,opt
-prism csma.nm -const bmax=1 deadline.pctl -const T=2000 -aroptions refine=all,nopre,opt
-prism csma.nm -const bmax=1 deadline.pctl -const T=3000 -aroptions refine=all,nopre,opt
+prism csma.nm -const K=1 deadline.pctl -const T=1000 -aroptions refine=all,nopre,opt
+prism csma.nm -const K=1 deadline.pctl -const T=2000 -aroptions refine=all,nopre,opt
+prism csma.nm -const K=1 deadline.pctl -const T=3000 -aroptions refine=all,nopre,opt

prism-examples/pta/csma/abst/csma.nm

@@ -8,7 +8,7 @@ pta
 
 //----------------------------------------------------------------------------------------------------------------------------
 // actual parameters
-const int bmax; // exponential backoff limit
+const int K; // exponential backoff limit (sometimes called bmax)
 const int slot=2*sigma; // length of slot
 const int sigma=26;
 const int lambda=808;
@@ -65,7 +65,7 @@ module station1
 	// LOCAL CLOCK
 	x1 : clock;
 	// COLLISION COUNTER
-	cd1 : [0..bmax];
+	cd1 : [0..K];
 
 	invariant
 		(s1=0 => x1=0) &
@@ -77,11 +77,11 @@ module station1
 
 	// start sending
 	[send1] (s1=0) -> (s1'=1) & (x1'=0); // start sending
-	[busy1] (s1=0) -> (s1'=2) & (x1'=0) & (cd1'=min(bmax,cd1+1)); // detects channel is busy so go into backoff
+	[busy1] (s1=0) -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // detects channel is busy so go into backoff
 	
 	// transmitting
 	[end1] (s1=1) & (x1=lambda) -> (s1'=4) & (x1'=0); // finished
-	[cd]   (s1=1) -> (s1'=2) & (x1'=0) & (cd1'=min(bmax,cd1+1)); // collision detected
+	[cd]   (s1=1) -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // collision detected
 	
 	// set backoff (no time can pass in this state)
 	// first retransmission
@@ -121,7 +121,7 @@ module station1
 	
 	// finished backoff
 	[send1] (s1=3) & (x1=pow(2, cd1)*slot) -> (s1'=1) & (x1'=0); // channel free
-	[busy1] (s1=3) & (x1=pow(2, cd1)*slot) -> (s1'=2) & (x1'=0) & (cd1'=min(bmax,cd1+1)); // channel busy
+	[busy1] (s1=3) & (x1=pow(2, cd1)*slot) -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // channel busy
 	
 	// once finished nothing matters
 	[done] (s1=4) -> true;