Fix(es) for previous commit.

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

prism-examples/csma/.csmaN_K.nm.pp

@@ -133,6 +133,6 @@ label "all_delivered" = #& i=1:N#s#i#=4#end#;
 label "one_delivered" = #| i=1:N#s#i#=4#end#;
 label "collision_max_backoff" = #| i=1:N#(cd#i#=K & s#i#=1 & b=2)#end#;
 formula min_backoff_after_success = min(#, i=1:N#s#i#=4?cd#i#:K+1#end#);
-formula min_collisions = min(cd1,cd2,cd3,cd4);
-formula max_collisions = max(cd1,cd2,cd3,cd4);
+formula min_collisions = min(#, i=1:N#cd#i##end#);
+formula max_collisions = max(#, i=1:N#cd#i##end#);
 

prism-examples/csma/auto

@@ -1,12 +1,12 @@
 #!/bin/csh
 
-prism csma2_2.nm csma.pctl -s
-prism csma2_4.nm csma.pctl -s
-prism csma2_6.nm csma.pctl -s
-prism csma3_2.nm csma.pctl -s
-prism csma3_4.nm csma.pctl -s
-prism csma3_6.nm csma.pctl -s
-prism csma4_2.nm csma.pctl -s
-#prism csma4_4.nm csma.pctl -s
-#prism csma4_6.nm csma.pctl -s
+prism csma2_2.nm csma.pctl -const k=1 -s
+prism csma2_4.nm csma.pctl -const k=1 -s
+prism csma2_6.nm csma.pctl -const k=1 -s
+prism csma3_2.nm csma.pctl -const k=1 -s
+prism csma3_4.nm csma.pctl -const k=1 -s
+prism csma3_6.nm csma.pctl -const k=1 -s
+prism csma4_2.nm csma.pctl -const k=1 -s
+#prism csma4_4.nm csma.pctl -const k=1 -s
+#prism csma4_6.nm csma.pctl -const k=1 -s
 

prism-examples/csma/csma.pctl

@@ -8,7 +8,7 @@ R{"time"}max=?[ F "all_delivered" ]
 Rmin=?[ F "one_delivered" ]
 Rmax=?[ F "one_delivered" ]
 
-// message of any station eventually delivered before k backoffs
+// message of some station eventually delivered before k backoffs
 Pmin=?[ F min_backoff_after_success<=k ]
 Pmax=?[ F min_backoff_after_success<=k ]
 

prism-examples/csma/csma2_2.nm

@@ -123,6 +123,6 @@ label "all_delivered" = s1=4&s2=4;
 label "one_delivered" = s1=4|s2=4;
 label "collision_max_backoff" = (cd1=K & s1=1 & b=2)|(cd2=K & s2=1 & b=2);
 formula min_backoff_after_success = min(s1=4?cd1:K+1,s2=4?cd2:K+1);
-formula min_collisions = min(cd1,cd2,cd3,cd4);
-formula max_collisions = max(cd1,cd2,cd3,cd4);
+formula min_collisions = min(cd1,cd2);
+formula max_collisions = max(cd1,cd2);
 

prism-examples/csma/csma2_4.nm

@@ -125,6 +125,6 @@ label "all_delivered" = s1=4&s2=4;
 label "one_delivered" = s1=4|s2=4;
 label "collision_max_backoff" = (cd1=K & s1=1 & b=2)|(cd2=K & s2=1 & b=2);
 formula min_backoff_after_success = min(s1=4?cd1:K+1,s2=4?cd2:K+1);
-formula min_collisions = min(cd1,cd2,cd3,cd4);
-formula max_collisions = max(cd1,cd2,cd3,cd4);
+formula min_collisions = min(cd1,cd2);
+formula max_collisions = max(cd1,cd2);
 

prism-examples/csma/csma2_6.nm

@@ -127,6 +127,6 @@ label "all_delivered" = s1=4&s2=4;
 label "one_delivered" = s1=4|s2=4;
 label "collision_max_backoff" = (cd1=K & s1=1 & b=2)|(cd2=K & s2=1 & b=2);
 formula min_backoff_after_success = min(s1=4?cd1:K+1,s2=4?cd2:K+1);
-formula min_collisions = min(cd1,cd2,cd3,cd4);
-formula max_collisions = max(cd1,cd2,cd3,cd4);
+formula min_collisions = min(cd1,cd2);
+formula max_collisions = max(cd1,cd2);
 

prism-examples/csma/csma3_2.nm

@@ -128,6 +128,6 @@ label "all_delivered" = s1=4&s2=4&s3=4;
 label "one_delivered" = s1=4|s2=4|s3=4;
 label "collision_max_backoff" = (cd1=K & s1=1 & b=2)|(cd2=K & s2=1 & b=2)|(cd3=K & s3=1 & b=2);
 formula min_backoff_after_success = min(s1=4?cd1:K+1,s2=4?cd2:K+1,s3=4?cd3:K+1);
-formula min_collisions = min(cd1,cd2,cd3,cd4);
-formula max_collisions = max(cd1,cd2,cd3,cd4);
+formula min_collisions = min(cd1,cd2,cd3);
+formula max_collisions = max(cd1,cd2,cd3);
 

prism-examples/csma/csma3_4.nm

@@ -130,6 +130,6 @@ label "all_delivered" = s1=4&s2=4&s3=4;
 label "one_delivered" = s1=4|s2=4|s3=4;
 label "collision_max_backoff" = (cd1=K & s1=1 & b=2)|(cd2=K & s2=1 & b=2)|(cd3=K & s3=1 & b=2);
 formula min_backoff_after_success = min(s1=4?cd1:K+1,s2=4?cd2:K+1,s3=4?cd3:K+1);
-formula min_collisions = min(cd1,cd2,cd3,cd4);
-formula max_collisions = max(cd1,cd2,cd3,cd4);
+formula min_collisions = min(cd1,cd2,cd3);
+formula max_collisions = max(cd1,cd2,cd3);
 

prism-examples/csma/csma3_6.nm

@@ -132,6 +132,6 @@ label "all_delivered" = s1=4&s2=4&s3=4;
 label "one_delivered" = s1=4|s2=4|s3=4;
 label "collision_max_backoff" = (cd1=K & s1=1 & b=2)|(cd2=K & s2=1 & b=2)|(cd3=K & s3=1 & b=2);
 formula min_backoff_after_success = min(s1=4?cd1:K+1,s2=4?cd2:K+1,s3=4?cd3:K+1);
-formula min_collisions = min(cd1,cd2,cd3,cd4);
-formula max_collisions = max(cd1,cd2,cd3,cd4);
+formula min_collisions = min(cd1,cd2,cd3);
+formula max_collisions = max(cd1,cd2,cd3);