diff --git a/prism-examples/csma/.autopp b/prism-examples/csma/.autopp
index e21af2c2..3273167e 100755
--- a/prism-examples/csma/.autopp
+++ b/prism-examples/csma/.autopp
@@ -1,10 +1,9 @@
 #!/bin/csh
 
-foreach K ( 2 4 6 )
-	echo "Generating for K=$K"
-	prismpp .csmaK.pctl.pp $K >! csma$K.pctl
-	foreach N ( 2 3 4 )
-		echo " and N=$N"
-		prismpp .csmaK_N.nm.pp $N $K >! csma$K"_"$N.nm
-	end
+foreach N ( 2 3 4 )
+  foreach K ( 2 4 6 )
+    echo "Generating for N=$N and K=$K"
+    prismpp .csmaN_K.nm.pp $N $K >! csma$N"_"$K.nm
+  end
 end
+
diff --git a/prism-examples/csma/.csmaK_N.nm.pp b/prism-examples/csma/.csmaN_K.nm.pp
similarity index 95%
rename from prism-examples/csma/.csmaK_N.nm.pp
rename to prism-examples/csma/.csmaN_K.nm.pp
index 537cd92b..3d37a73e 100644
--- a/prism-examples/csma/.csmaK_N.nm.pp
+++ b/prism-examples/csma/.csmaN_K.nm.pp
@@ -128,14 +128,11 @@ endrewards
 
 //----------------------------------------------------------------------------------------------------------------------------
 
+// labels/formulae
 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#;
-#for i=1:K#
-label "success_with_backoff_under_#i#" = #| j=1:N#(cd#j#<=#i# & s#j#=4)#end#;
-#end#
-#for i=1:K#
-label "collisions_equal_#i#" = #| j=1:N#(cd#j#=#i#)#end#;
-#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);
 
diff --git a/prism-examples/csma/auto b/prism-examples/csma/auto
index 67de7784..d2717178 100755
--- a/prism-examples/csma/auto
+++ b/prism-examples/csma/auto
@@ -1,12 +1,12 @@
 #!/bin/csh
 
-prism csma2_2.nm csma2.pctl -s
-prism csma2_3.nm csma2.pctl -s
-prism csma2_4.nm csma2.pctl -s
-prism csma4_2.nm csma4.pctl -s
-prism csma4_3.nm csma4.pctl -s
-#prism csma4_4.nm csma4.pctl -s
-prism csma6_2.nm csma6.pctl -s
-prism csma6_3.nm csma6.pctl -s
-#prism csma6_4.nm csma6.pctl -s
+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
 
diff --git a/prism-examples/csma/csma.pctl b/prism-examples/csma/csma.pctl
new file mode 100644
index 00000000..bc4e6906
--- /dev/null
+++ b/prism-examples/csma/csma.pctl
@@ -0,0 +1,22 @@
+const int k;
+
+// expected time for all messages to be sent
+R{"time"}min=?[ F "all_delivered" ]
+R{"time"}max=?[ F "all_delivered" ]
+
+// expected time for one message to be sent
+Rmin=?[ F "one_delivered" ]
+Rmax=?[ F "one_delivered" ]
+
+// message of any station eventually delivered before k backoffs
+Pmin=?[ F min_backoff_after_success<=k ]
+Pmax=?[ F min_backoff_after_success<=k ]
+
+// probability all sent successfully before a collision with max backoff 
+Pmin=?[ !"collision_max_backoff" U "all_delivered" ]
+Pmax=?[ !"collision_max_backoff" U "all_delivered" ]
+
+// probability some station suffers at least k collisions
+Pmin=?[ F max_collisions>=k ]
+Pmax=?[ F max_collisions>=k ]
+
diff --git a/prism-examples/csma/csma2.pctl b/prism-examples/csma/csma2.pctl
deleted file mode 100644
index e11b03a5..00000000
--- a/prism-examples/csma/csma2.pctl
+++ /dev/null
@@ -1,26 +0,0 @@
-
-// expected time for all messages to be sent
-R{"time"}min=?[ F "all_delivered" ]
-R{"time"}max=?[ F "all_delivered" ]
-
-// expected time for one message to be sent
-Rmin=?[ F "one_delivered" ]
-Rmax=?[ F "one_delivered" ]
-
-// message of any station eventually delivered before i backoffs
-Pmin=?[ F "success_with_backoff_under_1" ]
-Pmax=?[ F "success_with_backoff_under_1" ]
-Pmin=?[ F "success_with_backoff_under_2" ]
-Pmax=?[ F "success_with_backoff_under_2" ]
-
-// probability all sent successfully before a collision with max backoff 
-Pmin=?[ !"collision_max_backoff" U "all_delivered" ]
-Pmax=?[ !"collision_max_backoff" U "all_delivered" ]
-
-// probability a station suffers i collisions
-Pmin=?[ F "collisions_equal_1" ]
-Pmax=?[ F "collisions_equal_1" ]
-Pmin=?[ F "collisions_equal_2" ]
-Pmax=?[ F "collisions_equal_2" ]
-
-
diff --git a/prism-examples/csma/csma2_2.nm b/prism-examples/csma/csma2_2.nm
index 277cd58e..09a0a9a7 100644
--- a/prism-examples/csma/csma2_2.nm
+++ b/prism-examples/csma/csma2_2.nm
@@ -118,12 +118,11 @@ endrewards
 
 //----------------------------------------------------------------------------------------------------------------------------
 
+// labels/formulae
 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);
-label "success_with_backoff_under_1" = (cd1<=1 & s1=4)|(cd2<=1 & s2=4);
-label "success_with_backoff_under_2" = (cd1<=2 & s1=4)|(cd2<=2 & s2=4);
-label "collisions_equal_1" = (cd1=1)|(cd2=1);
-label "collisions_equal_2" = (cd1=2)|(cd2=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);
 
diff --git a/prism-examples/csma/csma2_4.nm b/prism-examples/csma/csma2_4.nm
index 2bf27a80..30d5ee7a 100644
--- a/prism-examples/csma/csma2_4.nm
+++ b/prism-examples/csma/csma2_4.nm
@@ -7,8 +7,8 @@ mdp
 // in digital clocks approach and suppose a station only sends one message
 
 // actual parameters
-const int N = 4; // number of processes
-const int K = 2; // exponential backoff limit
+const int N = 2; // number of processes
+const int K = 4; // exponential backoff limit
 const int slot = 2*sigma; // length of slot
 const int M = floor(pow(2, K))-1 ; // max number of slots to wait
 //const int lambda=782;
@@ -34,26 +34,18 @@ module bus
 	// a sender sends (ok - no other message being sent)
 	[send1] (b=0) -> (b'=1);
 	[send2] (b=0) -> (b'=1);
-	[send3] (b=0) -> (b'=1);
-	[send4] (b=0) -> (b'=1);
 	
 	// a sender sends (bus busy - collision)
 	[send1] (b=1|b=2) & (y1<sigma) -> (b'=2);
 	[send2] (b=1|b=2) & (y1<sigma) -> (b'=2);
-	[send3] (b=1|b=2) & (y1<sigma) -> (b'=2);
-	[send4] (b=1|b=2) & (y1<sigma) -> (b'=2);
 	
 	// finish sending
 	[end1] (b=1) -> (b'=0) & (y1'=0);
 	[end2] (b=1) -> (b'=0) & (y1'=0);
-	[end3] (b=1) -> (b'=0) & (y1'=0);
-	[end4] (b=1) -> (b'=0) & (y1'=0);
 	
 	// bus busy
 	[busy1] (b=1|b=2) & (y1>=sigma) -> (b'=b);  
 	[busy2] (b=1|b=2) & (y1>=sigma) -> (b'=b);  
-	[busy3] (b=1|b=2) & (y1>=sigma) -> (b'=b);  
-	[busy4] (b=1|b=2) & (y1>=sigma) -> (b'=b);  
 	
 	// collision detected
 	[cd] (b=2) & (y2<=sigma) -> (b'=0) & (y1'=0) & (y2'=0);
@@ -100,6 +92,8 @@ module station1
 	// probability depends on which transmission this is (cd1)
 	[] s1=2 & cd1=1 ->  1/2 : (s1'=3) & (bc1'=0) + 1/2 : (s1'=3) & (bc1'=1) ;
 	[] s1=2 & cd1=2 ->  1/4 : (s1'=3) & (bc1'=0) + 1/4 : (s1'=3) & (bc1'=1) + 1/4 : (s1'=3) & (bc1'=2) + 1/4 : (s1'=3) & (bc1'=3) ;
+	[] s1=2 & cd1=3 ->  1/8 : (s1'=3) & (bc1'=0) + 1/8 : (s1'=3) & (bc1'=1) + 1/8 : (s1'=3) & (bc1'=2) + 1/8 : (s1'=3) & (bc1'=3) + 1/8 : (s1'=3) & (bc1'=4) + 1/8 : (s1'=3) & (bc1'=5) + 1/8 : (s1'=3) & (bc1'=6) + 1/8 : (s1'=3) & (bc1'=7) ;
+	[] s1=2 & cd1=4 ->  1/16 : (s1'=3) & (bc1'=0) + 1/16 : (s1'=3) & (bc1'=1) + 1/16 : (s1'=3) & (bc1'=2) + 1/16 : (s1'=3) & (bc1'=3) + 1/16 : (s1'=3) & (bc1'=4) + 1/16 : (s1'=3) & (bc1'=5) + 1/16 : (s1'=3) & (bc1'=6) + 1/16 : (s1'=3) & (bc1'=7) + 1/16 : (s1'=3) & (bc1'=8) + 1/16 : (s1'=3) & (bc1'=9) + 1/16 : (s1'=3) & (bc1'=10) + 1/16 : (s1'=3) & (bc1'=11) + 1/16 : (s1'=3) & (bc1'=12) + 1/16 : (s1'=3) & (bc1'=13) + 1/16 : (s1'=3) & (bc1'=14) + 1/16 : (s1'=3) & (bc1'=15) ;
 	
 	// wait until backoff counter reaches 0 then send again
 	[time] (s1=3) & (x1<slot) -> (x1'=x1+1); // let time pass (in slot)
@@ -116,8 +110,6 @@ endmodule
 
 // construct further stations through renaming
 module station2=station1[s1=s2,x1=x2,cd1=cd2,bc1=bc2,send1=send2,busy1=busy2,end1=end2] endmodule
-module station3=station1[s1=s3,x1=x3,cd1=cd3,bc1=bc3,send1=send3,busy1=busy3,end1=end3] endmodule
-module station4=station1[s1=s4,x1=x4,cd1=cd4,bc1=bc4,send1=send4,busy1=busy4,end1=end4] endmodule
 
 //----------------------------------------------------------------------------------------------------------------------------
 
@@ -128,12 +120,11 @@ endrewards
 
 //----------------------------------------------------------------------------------------------------------------------------
 
-label "all_delivered" = s1=4&s2=4&s3=4&s4=4;
-label "one_delivered" = s1=4|s2=4|s3=4|s4=4;
-label "collision_max_backoff" = (cd1=K & s1=1 & b=2)|(cd2=K & s2=1 & b=2)|(cd3=K & s3=1 & b=2)|(cd4=K & s4=1 & b=2);
-label "success_with_backoff_under_1" = (cd1<=1 & s1=4)|(cd2<=1 & s2=4)|(cd3<=1 & s3=4)|(cd4<=1 & s4=4);
-label "success_with_backoff_under_2" = (cd1<=2 & s1=4)|(cd2<=2 & s2=4)|(cd3<=2 & s3=4)|(cd4<=2 & s4=4);
-label "collisions_equal_1" = (cd1=1)|(cd2=1)|(cd3=1)|(cd4=1);
-label "collisions_equal_2" = (cd1=2)|(cd2=2)|(cd3=2)|(cd4=2);
-
+// labels/formulae
+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);
 
diff --git a/prism-examples/csma/csma6_2.nm b/prism-examples/csma/csma2_6.nm
similarity index 91%
rename from prism-examples/csma/csma6_2.nm
rename to prism-examples/csma/csma2_6.nm
index d189eb4c..10a51d81 100644
--- a/prism-examples/csma/csma6_2.nm
+++ b/prism-examples/csma/csma2_6.nm
@@ -122,20 +122,11 @@ endrewards
 
 //----------------------------------------------------------------------------------------------------------------------------
 
+// labels/formulae
 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);
-label "success_with_backoff_under_1" = (cd1<=1 & s1=4)|(cd2<=1 & s2=4);
-label "success_with_backoff_under_2" = (cd1<=2 & s1=4)|(cd2<=2 & s2=4);
-label "success_with_backoff_under_3" = (cd1<=3 & s1=4)|(cd2<=3 & s2=4);
-label "success_with_backoff_under_4" = (cd1<=4 & s1=4)|(cd2<=4 & s2=4);
-label "success_with_backoff_under_5" = (cd1<=5 & s1=4)|(cd2<=5 & s2=4);
-label "success_with_backoff_under_6" = (cd1<=6 & s1=4)|(cd2<=6 & s2=4);
-label "collisions_equal_1" = (cd1=1)|(cd2=1);
-label "collisions_equal_2" = (cd1=2)|(cd2=2);
-label "collisions_equal_3" = (cd1=3)|(cd2=3);
-label "collisions_equal_4" = (cd1=4)|(cd2=4);
-label "collisions_equal_5" = (cd1=5)|(cd2=5);
-label "collisions_equal_6" = (cd1=6)|(cd2=6);
-
+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);
 
diff --git a/prism-examples/csma/csma2_3.nm b/prism-examples/csma/csma3_2.nm
similarity index 94%
rename from prism-examples/csma/csma2_3.nm
rename to prism-examples/csma/csma3_2.nm
index 514526d1..9bd6cde5 100644
--- a/prism-examples/csma/csma2_3.nm
+++ b/prism-examples/csma/csma3_2.nm
@@ -123,12 +123,11 @@ endrewards
 
 //----------------------------------------------------------------------------------------------------------------------------
 
+// labels/formulae
 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);
-label "success_with_backoff_under_1" = (cd1<=1 & s1=4)|(cd2<=1 & s2=4)|(cd3<=1 & s3=4);
-label "success_with_backoff_under_2" = (cd1<=2 & s1=4)|(cd2<=2 & s2=4)|(cd3<=2 & s3=4);
-label "collisions_equal_1" = (cd1=1)|(cd2=1)|(cd3=1);
-label "collisions_equal_2" = (cd1=2)|(cd2=2)|(cd3=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);
 
diff --git a/prism-examples/csma/csma4_3.nm b/prism-examples/csma/csma3_4.nm
similarity index 90%
rename from prism-examples/csma/csma4_3.nm
rename to prism-examples/csma/csma3_4.nm
index 5fa8de32..8387752a 100644
--- a/prism-examples/csma/csma4_3.nm
+++ b/prism-examples/csma/csma3_4.nm
@@ -125,16 +125,11 @@ endrewards
 
 //----------------------------------------------------------------------------------------------------------------------------
 
+// labels/formulae
 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);
-label "success_with_backoff_under_1" = (cd1<=1 & s1=4)|(cd2<=1 & s2=4)|(cd3<=1 & s3=4);
-label "success_with_backoff_under_2" = (cd1<=2 & s1=4)|(cd2<=2 & s2=4)|(cd3<=2 & s3=4);
-label "success_with_backoff_under_3" = (cd1<=3 & s1=4)|(cd2<=3 & s2=4)|(cd3<=3 & s3=4);
-label "success_with_backoff_under_4" = (cd1<=4 & s1=4)|(cd2<=4 & s2=4)|(cd3<=4 & s3=4);
-label "collisions_equal_1" = (cd1=1)|(cd2=1)|(cd3=1);
-label "collisions_equal_2" = (cd1=2)|(cd2=2)|(cd3=2);
-label "collisions_equal_3" = (cd1=3)|(cd2=3)|(cd3=3);
-label "collisions_equal_4" = (cd1=4)|(cd2=4)|(cd3=4);
-
+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);
 
diff --git a/prism-examples/csma/csma6_3.nm b/prism-examples/csma/csma3_6.nm
similarity index 90%
rename from prism-examples/csma/csma6_3.nm
rename to prism-examples/csma/csma3_6.nm
index 3938f9b9..73d93172 100644
--- a/prism-examples/csma/csma6_3.nm
+++ b/prism-examples/csma/csma3_6.nm
@@ -127,20 +127,11 @@ endrewards
 
 //----------------------------------------------------------------------------------------------------------------------------
 
+// labels/formulae
 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);
-label "success_with_backoff_under_1" = (cd1<=1 & s1=4)|(cd2<=1 & s2=4)|(cd3<=1 & s3=4);
-label "success_with_backoff_under_2" = (cd1<=2 & s1=4)|(cd2<=2 & s2=4)|(cd3<=2 & s3=4);
-label "success_with_backoff_under_3" = (cd1<=3 & s1=4)|(cd2<=3 & s2=4)|(cd3<=3 & s3=4);
-label "success_with_backoff_under_4" = (cd1<=4 & s1=4)|(cd2<=4 & s2=4)|(cd3<=4 & s3=4);
-label "success_with_backoff_under_5" = (cd1<=5 & s1=4)|(cd2<=5 & s2=4)|(cd3<=5 & s3=4);
-label "success_with_backoff_under_6" = (cd1<=6 & s1=4)|(cd2<=6 & s2=4)|(cd3<=6 & s3=4);
-label "collisions_equal_1" = (cd1=1)|(cd2=1)|(cd3=1);
-label "collisions_equal_2" = (cd1=2)|(cd2=2)|(cd3=2);
-label "collisions_equal_3" = (cd1=3)|(cd2=3)|(cd3=3);
-label "collisions_equal_4" = (cd1=4)|(cd2=4)|(cd3=4);
-label "collisions_equal_5" = (cd1=5)|(cd2=5)|(cd3=5);
-label "collisions_equal_6" = (cd1=6)|(cd2=6)|(cd3=6);
-
+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);
 
diff --git a/prism-examples/csma/csma4.pctl b/prism-examples/csma/csma4.pctl
deleted file mode 100644
index ae5ee091..00000000
--- a/prism-examples/csma/csma4.pctl
+++ /dev/null
@@ -1,34 +0,0 @@
-
-// expected time for all messages to be sent
-R{"time"}min=?[ F "all_delivered" ]
-R{"time"}max=?[ F "all_delivered" ]
-
-// expected time for one message to be sent
-Rmin=?[ F "one_delivered" ]
-Rmax=?[ F "one_delivered" ]
-
-// message of any station eventually delivered before i backoffs
-Pmin=?[ F "success_with_backoff_under_1" ]
-Pmax=?[ F "success_with_backoff_under_1" ]
-Pmin=?[ F "success_with_backoff_under_2" ]
-Pmax=?[ F "success_with_backoff_under_2" ]
-Pmin=?[ F "success_with_backoff_under_3" ]
-Pmax=?[ F "success_with_backoff_under_3" ]
-Pmin=?[ F "success_with_backoff_under_4" ]
-Pmax=?[ F "success_with_backoff_under_4" ]
-
-// probability all sent successfully before a collision with max backoff 
-Pmin=?[ !"collision_max_backoff" U "all_delivered" ]
-Pmax=?[ !"collision_max_backoff" U "all_delivered" ]
-
-// probability a station suffers i collisions
-Pmin=?[ F "collisions_equal_1" ]
-Pmax=?[ F "collisions_equal_1" ]
-Pmin=?[ F "collisions_equal_2" ]
-Pmax=?[ F "collisions_equal_2" ]
-Pmin=?[ F "collisions_equal_3" ]
-Pmax=?[ F "collisions_equal_3" ]
-Pmin=?[ F "collisions_equal_4" ]
-Pmax=?[ F "collisions_equal_4" ]
-
-
diff --git a/prism-examples/csma/csma4_2.nm b/prism-examples/csma/csma4_2.nm
index 8c57cd7e..85d6642f 100644
--- a/prism-examples/csma/csma4_2.nm
+++ b/prism-examples/csma/csma4_2.nm
@@ -7,8 +7,8 @@ mdp
 // in digital clocks approach and suppose a station only sends one message
 
 // actual parameters
-const int N = 2; // number of processes
-const int K = 4; // exponential backoff limit
+const int N = 4; // number of processes
+const int K = 2; // exponential backoff limit
 const int slot = 2*sigma; // length of slot
 const int M = floor(pow(2, K))-1 ; // max number of slots to wait
 //const int lambda=782;
@@ -34,18 +34,26 @@ module bus
 	// a sender sends (ok - no other message being sent)
 	[send1] (b=0) -> (b'=1);
 	[send2] (b=0) -> (b'=1);
+	[send3] (b=0) -> (b'=1);
+	[send4] (b=0) -> (b'=1);
 	
 	// a sender sends (bus busy - collision)
 	[send1] (b=1|b=2) & (y1<sigma) -> (b'=2);
 	[send2] (b=1|b=2) & (y1<sigma) -> (b'=2);
+	[send3] (b=1|b=2) & (y1<sigma) -> (b'=2);
+	[send4] (b=1|b=2) & (y1<sigma) -> (b'=2);
 	
 	// finish sending
 	[end1] (b=1) -> (b'=0) & (y1'=0);
 	[end2] (b=1) -> (b'=0) & (y1'=0);
+	[end3] (b=1) -> (b'=0) & (y1'=0);
+	[end4] (b=1) -> (b'=0) & (y1'=0);
 	
 	// bus busy
 	[busy1] (b=1|b=2) & (y1>=sigma) -> (b'=b);  
 	[busy2] (b=1|b=2) & (y1>=sigma) -> (b'=b);  
+	[busy3] (b=1|b=2) & (y1>=sigma) -> (b'=b);  
+	[busy4] (b=1|b=2) & (y1>=sigma) -> (b'=b);  
 	
 	// collision detected
 	[cd] (b=2) & (y2<=sigma) -> (b'=0) & (y1'=0) & (y2'=0);
@@ -92,8 +100,6 @@ module station1
 	// probability depends on which transmission this is (cd1)
 	[] s1=2 & cd1=1 ->  1/2 : (s1'=3) & (bc1'=0) + 1/2 : (s1'=3) & (bc1'=1) ;
 	[] s1=2 & cd1=2 ->  1/4 : (s1'=3) & (bc1'=0) + 1/4 : (s1'=3) & (bc1'=1) + 1/4 : (s1'=3) & (bc1'=2) + 1/4 : (s1'=3) & (bc1'=3) ;
-	[] s1=2 & cd1=3 ->  1/8 : (s1'=3) & (bc1'=0) + 1/8 : (s1'=3) & (bc1'=1) + 1/8 : (s1'=3) & (bc1'=2) + 1/8 : (s1'=3) & (bc1'=3) + 1/8 : (s1'=3) & (bc1'=4) + 1/8 : (s1'=3) & (bc1'=5) + 1/8 : (s1'=3) & (bc1'=6) + 1/8 : (s1'=3) & (bc1'=7) ;
-	[] s1=2 & cd1=4 ->  1/16 : (s1'=3) & (bc1'=0) + 1/16 : (s1'=3) & (bc1'=1) + 1/16 : (s1'=3) & (bc1'=2) + 1/16 : (s1'=3) & (bc1'=3) + 1/16 : (s1'=3) & (bc1'=4) + 1/16 : (s1'=3) & (bc1'=5) + 1/16 : (s1'=3) & (bc1'=6) + 1/16 : (s1'=3) & (bc1'=7) + 1/16 : (s1'=3) & (bc1'=8) + 1/16 : (s1'=3) & (bc1'=9) + 1/16 : (s1'=3) & (bc1'=10) + 1/16 : (s1'=3) & (bc1'=11) + 1/16 : (s1'=3) & (bc1'=12) + 1/16 : (s1'=3) & (bc1'=13) + 1/16 : (s1'=3) & (bc1'=14) + 1/16 : (s1'=3) & (bc1'=15) ;
 	
 	// wait until backoff counter reaches 0 then send again
 	[time] (s1=3) & (x1<slot) -> (x1'=x1+1); // let time pass (in slot)
@@ -110,6 +116,8 @@ endmodule
 
 // construct further stations through renaming
 module station2=station1[s1=s2,x1=x2,cd1=cd2,bc1=bc2,send1=send2,busy1=busy2,end1=end2] endmodule
+module station3=station1[s1=s3,x1=x3,cd1=cd3,bc1=bc3,send1=send3,busy1=busy3,end1=end3] endmodule
+module station4=station1[s1=s4,x1=x4,cd1=cd4,bc1=bc4,send1=send4,busy1=busy4,end1=end4] endmodule
 
 //----------------------------------------------------------------------------------------------------------------------------
 
@@ -120,16 +128,11 @@ endrewards
 
 //----------------------------------------------------------------------------------------------------------------------------
 
-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);
-label "success_with_backoff_under_1" = (cd1<=1 & s1=4)|(cd2<=1 & s2=4);
-label "success_with_backoff_under_2" = (cd1<=2 & s1=4)|(cd2<=2 & s2=4);
-label "success_with_backoff_under_3" = (cd1<=3 & s1=4)|(cd2<=3 & s2=4);
-label "success_with_backoff_under_4" = (cd1<=4 & s1=4)|(cd2<=4 & s2=4);
-label "collisions_equal_1" = (cd1=1)|(cd2=1);
-label "collisions_equal_2" = (cd1=2)|(cd2=2);
-label "collisions_equal_3" = (cd1=3)|(cd2=3);
-label "collisions_equal_4" = (cd1=4)|(cd2=4);
-
+// labels/formulae
+label "all_delivered" = s1=4&s2=4&s3=4&s4=4;
+label "one_delivered" = s1=4|s2=4|s3=4|s4=4;
+label "collision_max_backoff" = (cd1=K & s1=1 & b=2)|(cd2=K & s2=1 & b=2)|(cd3=K & s3=1 & b=2)|(cd4=K & s4=1 & b=2);
+formula min_backoff_after_success = min(s1=4?cd1:K+1,s2=4?cd2:K+1,s3=4?cd3:K+1,s4=4?cd4:K+1);
+formula min_collisions = min(cd1,cd2,cd3,cd4);
+formula max_collisions = max(cd1,cd2,cd3,cd4);
 
diff --git a/prism-examples/csma/csma4_4.nm b/prism-examples/csma/csma4_4.nm
index 65786dec..21d4b9d7 100644
--- a/prism-examples/csma/csma4_4.nm
+++ b/prism-examples/csma/csma4_4.nm
@@ -130,16 +130,11 @@ endrewards
 
 //----------------------------------------------------------------------------------------------------------------------------
 
+// labels/formulae
 label "all_delivered" = s1=4&s2=4&s3=4&s4=4;
 label "one_delivered" = s1=4|s2=4|s3=4|s4=4;
 label "collision_max_backoff" = (cd1=K & s1=1 & b=2)|(cd2=K & s2=1 & b=2)|(cd3=K & s3=1 & b=2)|(cd4=K & s4=1 & b=2);
-label "success_with_backoff_under_1" = (cd1<=1 & s1=4)|(cd2<=1 & s2=4)|(cd3<=1 & s3=4)|(cd4<=1 & s4=4);
-label "success_with_backoff_under_2" = (cd1<=2 & s1=4)|(cd2<=2 & s2=4)|(cd3<=2 & s3=4)|(cd4<=2 & s4=4);
-label "success_with_backoff_under_3" = (cd1<=3 & s1=4)|(cd2<=3 & s2=4)|(cd3<=3 & s3=4)|(cd4<=3 & s4=4);
-label "success_with_backoff_under_4" = (cd1<=4 & s1=4)|(cd2<=4 & s2=4)|(cd3<=4 & s3=4)|(cd4<=4 & s4=4);
-label "collisions_equal_1" = (cd1=1)|(cd2=1)|(cd3=1)|(cd4=1);
-label "collisions_equal_2" = (cd1=2)|(cd2=2)|(cd3=2)|(cd4=2);
-label "collisions_equal_3" = (cd1=3)|(cd2=3)|(cd3=3)|(cd4=3);
-label "collisions_equal_4" = (cd1=4)|(cd2=4)|(cd3=4)|(cd4=4);
-
+formula min_backoff_after_success = min(s1=4?cd1:K+1,s2=4?cd2:K+1,s3=4?cd3:K+1,s4=4?cd4:K+1);
+formula min_collisions = min(cd1,cd2,cd3,cd4);
+formula max_collisions = max(cd1,cd2,cd3,cd4);
 
diff --git a/prism-examples/csma/csma6_4.nm b/prism-examples/csma/csma4_6.nm
similarity index 89%
rename from prism-examples/csma/csma6_4.nm
rename to prism-examples/csma/csma4_6.nm
index 4de4368e..3bc405fa 100644
--- a/prism-examples/csma/csma6_4.nm
+++ b/prism-examples/csma/csma4_6.nm
@@ -132,20 +132,11 @@ endrewards
 
 //----------------------------------------------------------------------------------------------------------------------------
 
+// labels/formulae
 label "all_delivered" = s1=4&s2=4&s3=4&s4=4;
 label "one_delivered" = s1=4|s2=4|s3=4|s4=4;
 label "collision_max_backoff" = (cd1=K & s1=1 & b=2)|(cd2=K & s2=1 & b=2)|(cd3=K & s3=1 & b=2)|(cd4=K & s4=1 & b=2);
-label "success_with_backoff_under_1" = (cd1<=1 & s1=4)|(cd2<=1 & s2=4)|(cd3<=1 & s3=4)|(cd4<=1 & s4=4);
-label "success_with_backoff_under_2" = (cd1<=2 & s1=4)|(cd2<=2 & s2=4)|(cd3<=2 & s3=4)|(cd4<=2 & s4=4);
-label "success_with_backoff_under_3" = (cd1<=3 & s1=4)|(cd2<=3 & s2=4)|(cd3<=3 & s3=4)|(cd4<=3 & s4=4);
-label "success_with_backoff_under_4" = (cd1<=4 & s1=4)|(cd2<=4 & s2=4)|(cd3<=4 & s3=4)|(cd4<=4 & s4=4);
-label "success_with_backoff_under_5" = (cd1<=5 & s1=4)|(cd2<=5 & s2=4)|(cd3<=5 & s3=4)|(cd4<=5 & s4=4);
-label "success_with_backoff_under_6" = (cd1<=6 & s1=4)|(cd2<=6 & s2=4)|(cd3<=6 & s3=4)|(cd4<=6 & s4=4);
-label "collisions_equal_1" = (cd1=1)|(cd2=1)|(cd3=1)|(cd4=1);
-label "collisions_equal_2" = (cd1=2)|(cd2=2)|(cd3=2)|(cd4=2);
-label "collisions_equal_3" = (cd1=3)|(cd2=3)|(cd3=3)|(cd4=3);
-label "collisions_equal_4" = (cd1=4)|(cd2=4)|(cd3=4)|(cd4=4);
-label "collisions_equal_5" = (cd1=5)|(cd2=5)|(cd3=5)|(cd4=5);
-label "collisions_equal_6" = (cd1=6)|(cd2=6)|(cd3=6)|(cd4=6);
-
+formula min_backoff_after_success = min(s1=4?cd1:K+1,s2=4?cd2:K+1,s3=4?cd3:K+1,s4=4?cd4:K+1);
+formula min_collisions = min(cd1,cd2,cd3,cd4);
+formula max_collisions = max(cd1,cd2,cd3,cd4);
 
diff --git a/prism-examples/csma/csma6.pctl b/prism-examples/csma/csma6.pctl
deleted file mode 100644
index 3b363c69..00000000
--- a/prism-examples/csma/csma6.pctl
+++ /dev/null
@@ -1,42 +0,0 @@
-
-// expected time for all messages to be sent
-R{"time"}min=?[ F "all_delivered" ]
-R{"time"}max=?[ F "all_delivered" ]
-
-// expected time for one message to be sent
-Rmin=?[ F "one_delivered" ]
-Rmax=?[ F "one_delivered" ]
-
-// message of any station eventually delivered before i backoffs
-Pmin=?[ F "success_with_backoff_under_1" ]
-Pmax=?[ F "success_with_backoff_under_1" ]
-Pmin=?[ F "success_with_backoff_under_2" ]
-Pmax=?[ F "success_with_backoff_under_2" ]
-Pmin=?[ F "success_with_backoff_under_3" ]
-Pmax=?[ F "success_with_backoff_under_3" ]
-Pmin=?[ F "success_with_backoff_under_4" ]
-Pmax=?[ F "success_with_backoff_under_4" ]
-Pmin=?[ F "success_with_backoff_under_5" ]
-Pmax=?[ F "success_with_backoff_under_5" ]
-Pmin=?[ F "success_with_backoff_under_6" ]
-Pmax=?[ F "success_with_backoff_under_6" ]
-
-// probability all sent successfully before a collision with max backoff 
-Pmin=?[ !"collision_max_backoff" U "all_delivered" ]
-Pmax=?[ !"collision_max_backoff" U "all_delivered" ]
-
-// probability a station suffers i collisions
-Pmin=?[ F "collisions_equal_1" ]
-Pmax=?[ F "collisions_equal_1" ]
-Pmin=?[ F "collisions_equal_2" ]
-Pmax=?[ F "collisions_equal_2" ]
-Pmin=?[ F "collisions_equal_3" ]
-Pmax=?[ F "collisions_equal_3" ]
-Pmin=?[ F "collisions_equal_4" ]
-Pmax=?[ F "collisions_equal_4" ]
-Pmin=?[ F "collisions_equal_5" ]
-Pmax=?[ F "collisions_equal_5" ]
-Pmin=?[ F "collisions_equal_6" ]
-Pmax=?[ F "collisions_equal_6" ]
-
-