diff --git a/prism-examples/rabin/.autopp b/prism-examples/rabin/.autopp
index 5ba73e4f..b46e45ca 100755
--- a/prism-examples/rabin/.autopp
+++ b/prism-examples/rabin/.autopp
@@ -4,6 +4,4 @@ foreach N ( 3 4 5 6 8 10 12 )
 	echo "Generating for N=$N"
 	prismpp .rabinN.nm.pp $N >! rabin$N.nm
 	unix2dos rabin$N.nm
-	prismpp .rabinN.pctl.pp $N >! rabin$N.pctl
-	unix2dos rabin$N.pctl
 end
diff --git a/prism-examples/rabin/.rabinN.nm.pp b/prism-examples/rabin/.rabinN.nm.pp
index 5dd46968..0341e44c 100644
--- a/prism-examples/rabin/.rabinN.nm.pp
+++ b/prism-examples/rabin/.rabinN.nm.pp
@@ -4,7 +4,7 @@
 // with global variables to remove sychronization 
 // gxn/dxp 02/02/00
 
-nondeterministic
+mdp
 
 // size of shared counter
 const int K = #K#; // 4+ceil(log_2 N)
@@ -58,3 +58,14 @@ endmodule
 // construct further modules through renaming
 #for i=2:N#
 module process#i# = process1 [p1=p#i#, b1=b#i#, r1=r#i#] endmodule
#end#
+
+// formulas/labels for use in properties:
+
+// number of processes in critical section
+formula num_procs_in_crit = #+ i=1:N#(p#i#=2?1:0)#end#;
+
+// one of the processes is trying
+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#;
diff --git a/prism-examples/rabin/.rabinN.pctl.pp b/prism-examples/rabin/.rabinN.pctl.pp
deleted file mode 100644
index c3c02e3c..00000000
--- a/prism-examples/rabin/.rabinN.pctl.pp
+++ /dev/null
@@ -1,8 +0,0 @@
-#const N#
-label "one_trying" = #| i=1:N#p#i#=1#end#;
label "one_critical" = #| i=1:N#p#i#=2#end#;
-
-// Mutual exclusion
-#+ i=1:N#(p#i#=2?1:0)#end# <= 1
-
-// Liveness: If a process is trying, then eventually a process enters the critical section
-"one_trying" => P>=1 [ true U "one_critical" ]
diff --git a/prism-examples/rabin/auto b/prism-examples/rabin/auto
index 138e0ca1..4914802e 100755
--- a/prism-examples/rabin/auto
+++ b/prism-examples/rabin/auto
@@ -1,9 +1,9 @@
 #!/bin/csh
 
-prism rabin3.nm rabin3.pctl -fair
-prism rabin4.nm rabin4.pctl -fair
-prism rabin5.nm rabin5.pctl -fair
-prism rabin6.nm rabin6.pctl -fair
-prism rabin8.nm rabin8.pctl -fair
-prism rabin10.nm rabin10.pctl -fair
-prism rabin12.nm rabin12.pctl -fair
+prism rabin3.nm rabin.pctl -fair
+prism rabin4.nm rabin.pctl -fair
+prism rabin5.nm rabin.pctl -fair
+prism rabin6.nm rabin.pctl -fair
+prism rabin8.nm rabin.pctl -fair
+prism rabin10.nm rabin.pctl -fair
+prism rabin12.nm rabin.pctl -fair
diff --git a/prism-examples/rabin/rabin3.pctl b/prism-examples/rabin/rabin.pctl
similarity index 56%
rename from prism-examples/rabin/rabin3.pctl
rename to prism-examples/rabin/rabin.pctl
index e7065df7..1812c520 100644
--- a/prism-examples/rabin/rabin3.pctl
+++ b/prism-examples/rabin/rabin.pctl
@@ -1,8 +1,5 @@
-label "one_trying" = p1=1|p2=1|p3=1;
-label "one_critical" = p1=2|p2=2|p3=2;
-
 // Mutual exclusion
-(p1=2?1:0)+(p2=2?1:0)+(p3=2?1:0) <= 1
+num_procs_in_crit <= 1
 
 // Liveness: If a process is trying, then eventually a process enters the critical section
 "one_trying" => P>=1 [ true U "one_critical" ]
diff --git a/prism-examples/rabin/rabin10.nm b/prism-examples/rabin/rabin10.nm
index 08d26943..1e7714cf 100644
--- a/prism-examples/rabin/rabin10.nm
+++ b/prism-examples/rabin/rabin10.nm
@@ -2,7 +2,7 @@
 // with global variables to remove sychronization 
 // gxn/dxp 02/02/00
 
-nondeterministic
+mdp
 
 // size of shared counter
 const int K = 8; // 4+ceil(log_2 N)
@@ -69,3 +69,14 @@ module process7 = process1 [p1=p7, b1=b7, r1=r7] endmodule
 module process8 = process1 [p1=p8, b1=b8, r1=r8] endmodule
 module process9 = process1 [p1=p9, b1=b9, r1=r9] endmodule
 module process10 = process1 [p1=p10, b1=b10, r1=r10] endmodule
+
+// formulas/labels for use in properties:
+
+// number of processes in critical section
+formula num_procs_in_crit = (p1=2?1:0)+(p2=2?1:0)+(p3=2?1:0)+(p4=2?1:0)+(p5=2?1:0)+(p6=2?1:0)+(p7=2?1:0)+(p8=2?1:0)+(p9=2?1:0)+(p10=2?1:0);
+
+// one of the processes is trying
+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;
diff --git a/prism-examples/rabin/rabin10.pctl b/prism-examples/rabin/rabin10.pctl
deleted file mode 100644
index 886db82f..00000000
--- a/prism-examples/rabin/rabin10.pctl
+++ /dev/null
@@ -1,8 +0,0 @@
-label "one_trying" = p1=1|p2=1|p3=1|p4=1|p5=1|p6=1|p7=1|p8=1|p9=1|p10=1;
-label "one_critical" = p1=2|p2=2|p3=2|p4=2|p5=2|p6=2|p7=2|p8=2|p9=2|p10=2;
-
-// Mutual exclusion
-(p1=2?1:0)+(p2=2?1:0)+(p3=2?1:0)+(p4=2?1:0)+(p5=2?1:0)+(p6=2?1:0)+(p7=2?1:0)+(p8=2?1:0)+(p9=2?1:0)+(p10=2?1:0) <= 1
-
-// Liveness: If a process is trying, then eventually a process enters the critical section
-"one_trying" => P>=1 [ true U "one_critical" ]
diff --git a/prism-examples/rabin/rabin12.nm b/prism-examples/rabin/rabin12.nm
index 9b09fa67..d535dbc7 100644
--- a/prism-examples/rabin/rabin12.nm
+++ b/prism-examples/rabin/rabin12.nm
@@ -2,7 +2,7 @@
 // with global variables to remove sychronization 
 // gxn/dxp 02/02/00
 
-nondeterministic
+mdp
 
 // size of shared counter
 const int K = 8; // 4+ceil(log_2 N)
@@ -71,3 +71,14 @@ module process9 = process1 [p1=p9, b1=b9, r1=r9] endmodule
 module process10 = process1 [p1=p10, b1=b10, r1=r10] endmodule
 module process11 = process1 [p1=p11, b1=b11, r1=r11] endmodule
 module process12 = process1 [p1=p12, b1=b12, r1=r12] endmodule
+
+// formulas/labels for use in properties:
+
+// number of processes in critical section
+formula num_procs_in_crit = (p1=2?1:0)+(p2=2?1:0)+(p3=2?1:0)+(p4=2?1:0)+(p5=2?1:0)+(p6=2?1:0)+(p7=2?1:0)+(p8=2?1:0)+(p9=2?1:0)+(p10=2?1:0)+(p11=2?1:0)+(p12=2?1:0);
+
+// one of the processes is trying
+label "one_trying" = p1=1|p2=1|p3=1|p4=1|p5=1|p6=1|p7=1|p8=1|p9=1|p10=1|p11=1|p12=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|p11=2|p12=2;
diff --git a/prism-examples/rabin/rabin12.pctl b/prism-examples/rabin/rabin12.pctl
deleted file mode 100644
index eee23e74..00000000
--- a/prism-examples/rabin/rabin12.pctl
+++ /dev/null
@@ -1,8 +0,0 @@
-label "one_trying" = p1=1|p2=1|p3=1|p4=1|p5=1|p6=1|p7=1|p8=1|p9=1|p10=1|p11=1|p12=1;
-label "one_critical" = p1=2|p2=2|p3=2|p4=2|p5=2|p6=2|p7=2|p8=2|p9=2|p10=2|p11=2|p12=2;
-
-// Mutual exclusion
-(p1=2?1:0)+(p2=2?1:0)+(p3=2?1:0)+(p4=2?1:0)+(p5=2?1:0)+(p6=2?1:0)+(p7=2?1:0)+(p8=2?1:0)+(p9=2?1:0)+(p10=2?1:0)+(p11=2?1:0)+(p12=2?1:0) <= 1
-
-// Liveness: If a process is trying, then eventually a process enters the critical section
-"one_trying" => P>=1 [ true U "one_critical" ]
diff --git a/prism-examples/rabin/rabin3.nm b/prism-examples/rabin/rabin3.nm
index 7f64b6ca..b0d042b0 100644
--- a/prism-examples/rabin/rabin3.nm
+++ b/prism-examples/rabin/rabin3.nm
@@ -2,7 +2,7 @@
 // with global variables to remove sychronization 
 // gxn/dxp 02/02/00
 
-nondeterministic
+mdp
 
 // size of shared counter
 const int K = 6; // 4+ceil(log_2 N)
@@ -60,3 +60,14 @@ endmodule
 // construct further modules through renaming
 module process2 = process1 [p1=p2, b1=b2, r1=r2] endmodule
 module process3 = process1 [p1=p3, b1=b3, r1=r3] endmodule
+
+// formulas/labels for use in properties:
+
+// number of processes in critical section
+formula num_procs_in_crit = (p1=2?1:0)+(p2=2?1:0)+(p3=2?1:0);
+
+// one of the processes is trying
+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;
diff --git a/prism-examples/rabin/rabin4.nm b/prism-examples/rabin/rabin4.nm
index b949d354..58a23194 100644
--- a/prism-examples/rabin/rabin4.nm
+++ b/prism-examples/rabin/rabin4.nm
@@ -2,7 +2,7 @@
 // with global variables to remove sychronization 
 // gxn/dxp 02/02/00
 
-nondeterministic
+mdp
 
 // size of shared counter
 const int K = 6; // 4+ceil(log_2 N)
@@ -61,3 +61,14 @@ endmodule
 module process2 = process1 [p1=p2, b1=b2, r1=r2] endmodule
 module process3 = process1 [p1=p3, b1=b3, r1=r3] endmodule
 module process4 = process1 [p1=p4, b1=b4, r1=r4] endmodule
+
+// formulas/labels for use in properties:
+
+// number of processes in critical section
+formula num_procs_in_crit = (p1=2?1:0)+(p2=2?1:0)+(p3=2?1:0)+(p4=2?1:0);
+
+// one of the processes is trying
+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;
diff --git a/prism-examples/rabin/rabin4.pctl b/prism-examples/rabin/rabin4.pctl
deleted file mode 100644
index ac26f07c..00000000
--- a/prism-examples/rabin/rabin4.pctl
+++ /dev/null
@@ -1,8 +0,0 @@
-label "one_trying" = p1=1|p2=1|p3=1|p4=1;
-label "one_critical" = p1=2|p2=2|p3=2|p4=2;
-
-// Mutual exclusion
-(p1=2?1:0)+(p2=2?1:0)+(p3=2?1:0)+(p4=2?1:0) <= 1
-
-// Liveness: If a process is trying, then eventually a process enters the critical section
-"one_trying" => P>=1 [ true U "one_critical" ]
diff --git a/prism-examples/rabin/rabin5.nm b/prism-examples/rabin/rabin5.nm
index 1d9c9e44..e3fb1a7e 100644
--- a/prism-examples/rabin/rabin5.nm
+++ b/prism-examples/rabin/rabin5.nm
@@ -2,7 +2,7 @@
 // with global variables to remove sychronization 
 // gxn/dxp 02/02/00
 
-nondeterministic
+mdp
 
 // size of shared counter
 const int K = 7; // 4+ceil(log_2 N)
@@ -63,3 +63,14 @@ module process2 = process1 [p1=p2, b1=b2, r1=r2] endmodule
 module process3 = process1 [p1=p3, b1=b3, r1=r3] endmodule
 module process4 = process1 [p1=p4, b1=b4, r1=r4] endmodule
 module process5 = process1 [p1=p5, b1=b5, r1=r5] endmodule
+
+// formulas/labels for use in properties:
+
+// number of processes in critical section
+formula num_procs_in_crit = (p1=2?1:0)+(p2=2?1:0)+(p3=2?1:0)+(p4=2?1:0)+(p5=2?1:0);
+
+// one of the processes is trying
+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;
diff --git a/prism-examples/rabin/rabin5.pctl b/prism-examples/rabin/rabin5.pctl
deleted file mode 100644
index 6e78b1f4..00000000
--- a/prism-examples/rabin/rabin5.pctl
+++ /dev/null
@@ -1,8 +0,0 @@
-label "one_trying" = p1=1|p2=1|p3=1|p4=1|p5=1;
-label "one_critical" = p1=2|p2=2|p3=2|p4=2|p5=2;
-
-// Mutual exclusion
-(p1=2?1:0)+(p2=2?1:0)+(p3=2?1:0)+(p4=2?1:0)+(p5=2?1:0) <= 1
-
-// Liveness: If a process is trying, then eventually a process enters the critical section
-"one_trying" => P>=1 [ true U "one_critical" ]
diff --git a/prism-examples/rabin/rabin6.nm b/prism-examples/rabin/rabin6.nm
index 28641f9a..c17d6905 100644
--- a/prism-examples/rabin/rabin6.nm
+++ b/prism-examples/rabin/rabin6.nm
@@ -2,7 +2,7 @@
 // with global variables to remove sychronization 
 // gxn/dxp 02/02/00
 
-nondeterministic
+mdp
 
 // size of shared counter
 const int K = 7; // 4+ceil(log_2 N)
@@ -64,3 +64,14 @@ module process3 = process1 [p1=p3, b1=b3, r1=r3] endmodule
 module process4 = process1 [p1=p4, b1=b4, r1=r4] endmodule
 module process5 = process1 [p1=p5, b1=b5, r1=r5] endmodule
 module process6 = process1 [p1=p6, b1=b6, r1=r6] endmodule
+
+// formulas/labels for use in properties:
+
+// number of processes in critical section
+formula num_procs_in_crit = (p1=2?1:0)+(p2=2?1:0)+(p3=2?1:0)+(p4=2?1:0)+(p5=2?1:0)+(p6=2?1:0);
+
+// one of the processes is trying
+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;
diff --git a/prism-examples/rabin/rabin6.pctl b/prism-examples/rabin/rabin6.pctl
deleted file mode 100644
index 6f51c121..00000000
--- a/prism-examples/rabin/rabin6.pctl
+++ /dev/null
@@ -1,8 +0,0 @@
-label "one_trying" = p1=1|p2=1|p3=1|p4=1|p5=1|p6=1;
-label "one_critical" = p1=2|p2=2|p3=2|p4=2|p5=2|p6=2;
-
-// Mutual exclusion
-(p1=2?1:0)+(p2=2?1:0)+(p3=2?1:0)+(p4=2?1:0)+(p5=2?1:0)+(p6=2?1:0) <= 1
-
-// Liveness: If a process is trying, then eventually a process enters the critical section
-"one_trying" => P>=1 [ true U "one_critical" ]
diff --git a/prism-examples/rabin/rabin8.nm b/prism-examples/rabin/rabin8.nm
index 51e9226f..30de7c7e 100644
--- a/prism-examples/rabin/rabin8.nm
+++ b/prism-examples/rabin/rabin8.nm
@@ -2,7 +2,7 @@
 // with global variables to remove sychronization 
 // gxn/dxp 02/02/00
 
-nondeterministic
+mdp
 
 // size of shared counter
 const int K = 7; // 4+ceil(log_2 N)
@@ -66,3 +66,14 @@ module process5 = process1 [p1=p5, b1=b5, r1=r5] endmodule
 module process6 = process1 [p1=p6, b1=b6, r1=r6] endmodule
 module process7 = process1 [p1=p7, b1=b7, r1=r7] endmodule
 module process8 = process1 [p1=p8, b1=b8, r1=r8] endmodule
+
+// formulas/labels for use in properties:
+
+// number of processes in critical section
+formula num_procs_in_crit = (p1=2?1:0)+(p2=2?1:0)+(p3=2?1:0)+(p4=2?1:0)+(p5=2?1:0)+(p6=2?1:0)+(p7=2?1:0)+(p8=2?1:0);
+
+// one of the processes is trying
+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;
diff --git a/prism-examples/rabin/rabin8.pctl b/prism-examples/rabin/rabin8.pctl
deleted file mode 100644
index 0be844cd..00000000
--- a/prism-examples/rabin/rabin8.pctl
+++ /dev/null
@@ -1,8 +0,0 @@
-label "one_trying" = p1=1|p2=1|p3=1|p4=1|p5=1|p6=1|p7=1|p8=1;
-label "one_critical" = p1=2|p2=2|p3=2|p4=2|p5=2|p6=2|p7=2|p8=2;
-
-// Mutual exclusion
-(p1=2?1:0)+(p2=2?1:0)+(p3=2?1:0)+(p4=2?1:0)+(p5=2?1:0)+(p6=2?1:0)+(p7=2?1:0)+(p8=2?1:0) <= 1
-
-// Liveness: If a process is trying, then eventually a process enters the critical section
-"one_trying" => P>=1 [ true U "one_critical" ]