diff --git a/prism-examples/brp/brp.pm b/prism-examples/brp/brp.pm
index 37bd600e..bf168ee9 100644
--- a/prism-examples/brp/brp.pm
+++ b/prism-examples/brp/brp.pm
@@ -1,7 +1,7 @@
 // bounded retransmission protocol [D'AJJL01]
 // gxn/dxp 23/05/2001
 
-probabilistic
+dtmc
 
 // number of chunks
 const int N;
diff --git a/prism-examples/dice/dice.pm b/prism-examples/dice/dice.pm
index 4a82208a..699c4662 100644
--- a/prism-examples/dice/dice.pm
+++ b/prism-examples/dice/dice.pm
@@ -1,4 +1,4 @@
-probabilistic
+dtmc
 
 module die
 
diff --git a/prism-examples/dice/two_dice.nm b/prism-examples/dice/two_dice.nm
index 58732acb..2eef9c47 100644
--- a/prism-examples/dice/two_dice.nm
+++ b/prism-examples/dice/two_dice.nm
@@ -1,4 +1,4 @@
-nondeterministic
+mdp
 
 module die1
 
diff --git a/prism-examples/dice/two_dice_knuth.pm b/prism-examples/dice/two_dice_knuth.pm
index a29560b8..9591bb9d 100644
--- a/prism-examples/dice/two_dice_knuth.pm
+++ b/prism-examples/dice/two_dice_knuth.pm
@@ -1,4 +1,4 @@
-probabilistic
+dtmc
 
 module sum_of_two_dice
 	
diff --git a/prism-examples/leader/synchronous/leader10_2.pm b/prism-examples/leader/synchronous/leader10_2.pm
index fa34031e..98334408 100644
--- a/prism-examples/leader/synchronous/leader10_2.pm
+++ b/prism-examples/leader/synchronous/leader10_2.pm
@@ -2,7 +2,7 @@
 // dxp/gxn 25/01/01
 // N=10 and K=2
 
-probabilistic
+dtmc
 
 // CONSTANTS
 const N=10; // number of processes
diff --git a/prism-examples/leader/synchronous/leader3_10.pm b/prism-examples/leader/synchronous/leader3_10.pm
index 6f1edcd0..8faa7f47 100644
--- a/prism-examples/leader/synchronous/leader3_10.pm
+++ b/prism-examples/leader/synchronous/leader3_10.pm
@@ -2,7 +2,7 @@
 // dxp/gxn 25/01/01
 // N=3 and K=10
 
-probabilistic
+dtmc
 
 // CONSTANTS
 const N=3; // number of processes
diff --git a/prism-examples/leader/synchronous/leader3_12.pm b/prism-examples/leader/synchronous/leader3_12.pm
index b7bb70ea..c4f6492a 100644
--- a/prism-examples/leader/synchronous/leader3_12.pm
+++ b/prism-examples/leader/synchronous/leader3_12.pm
@@ -2,7 +2,7 @@
 // dxp/gxn 25/01/01
 // N=3 and K=12
 
-probabilistic
+dtmc
 
 // CONSTANTS
 const N=3; // number of processes
diff --git a/prism-examples/leader/synchronous/leader3_14.pm b/prism-examples/leader/synchronous/leader3_14.pm
index 8ee1973e..6d8fee6f 100644
--- a/prism-examples/leader/synchronous/leader3_14.pm
+++ b/prism-examples/leader/synchronous/leader3_14.pm
@@ -2,7 +2,7 @@
 // dxp/gxn 25/01/01
 // N=3 and K=14
 
-probabilistic
+dtmc
 
 // CONSTANTS
 const N=3; // number of processes
diff --git a/prism-examples/leader/synchronous/leader3_16.pm b/prism-examples/leader/synchronous/leader3_16.pm
index 8b91da94..2a9ab224 100644
--- a/prism-examples/leader/synchronous/leader3_16.pm
+++ b/prism-examples/leader/synchronous/leader3_16.pm
@@ -2,7 +2,7 @@
 // dxp/gxn 25/01/01
 // N=3 and K=16
 
-probabilistic
+dtmc
 
 // CONSTANTS
 const N=3; // number of processes
diff --git a/prism-examples/leader/synchronous/leader3_2.pm b/prism-examples/leader/synchronous/leader3_2.pm
index 14d6bf83..87fc7f31 100644
--- a/prism-examples/leader/synchronous/leader3_2.pm
+++ b/prism-examples/leader/synchronous/leader3_2.pm
@@ -2,7 +2,7 @@
 // dxp/gxn 25/01/01
 // N=3 and K=2
 
-probabilistic
+dtmc
 
 // CONSTANTS
 const N=3; // number of processes
diff --git a/prism-examples/leader/synchronous/leader3_3.pm b/prism-examples/leader/synchronous/leader3_3.pm
index 8703904c..05a6356b 100644
--- a/prism-examples/leader/synchronous/leader3_3.pm
+++ b/prism-examples/leader/synchronous/leader3_3.pm
@@ -2,7 +2,7 @@
 // dxp/gxn 25/01/01
 // N=3 and K=4
 
-probabilistic
+dtmc
 
 // CONSTANTS
 const N=3; // number of processes
diff --git a/prism-examples/leader/synchronous/leader3_4.pm b/prism-examples/leader/synchronous/leader3_4.pm
index 6784f16a..c2bc37b4 100644
--- a/prism-examples/leader/synchronous/leader3_4.pm
+++ b/prism-examples/leader/synchronous/leader3_4.pm
@@ -2,7 +2,7 @@
 // dxp/gxn 25/01/01
 // N=3 and K=4
 
-probabilistic
+dtmc
 
 // CONSTANTS
 const N=3; // number of processes
diff --git a/prism-examples/leader/synchronous/leader3_5.pm b/prism-examples/leader/synchronous/leader3_5.pm
index e20cfd83..a5885618 100644
--- a/prism-examples/leader/synchronous/leader3_5.pm
+++ b/prism-examples/leader/synchronous/leader3_5.pm
@@ -2,7 +2,7 @@
 // dxp/gxn 25/01/01
 // N=3 and K=6
 
-probabilistic
+dtmc
 
 // CONSTANTS
 const N=3; // number of processes
diff --git a/prism-examples/leader/synchronous/leader3_6.pm b/prism-examples/leader/synchronous/leader3_6.pm
index 7a8f4c9a..fbfd6150 100644
--- a/prism-examples/leader/synchronous/leader3_6.pm
+++ b/prism-examples/leader/synchronous/leader3_6.pm
@@ -2,7 +2,7 @@
 // dxp/gxn 25/01/01
 // N=3 and K=6
 
-probabilistic
+dtmc
 
 // CONSTANTS
 const N=3; // number of processes
diff --git a/prism-examples/leader/synchronous/leader3_8.pm b/prism-examples/leader/synchronous/leader3_8.pm
index 8be0eaa1..f461cc78 100644
--- a/prism-examples/leader/synchronous/leader3_8.pm
+++ b/prism-examples/leader/synchronous/leader3_8.pm
@@ -2,7 +2,7 @@
 // dxp/gxn 25/01/01
 // N=3 and K=8
 
-probabilistic
+dtmc
 
 // CONSTANTS
 const N=3; // number of processes
diff --git a/prism-examples/leader/synchronous/leader4_10.pm b/prism-examples/leader/synchronous/leader4_10.pm
index 7959ba0c..1f703d32 100644
--- a/prism-examples/leader/synchronous/leader4_10.pm
+++ b/prism-examples/leader/synchronous/leader4_10.pm
@@ -2,7 +2,7 @@
 // dxp/gxn 25/01/01
 // N=4 and K=10
 
-probabilistic
+dtmc
 
 // CONSTANTS
 const N=4; // number of processes
diff --git a/prism-examples/leader/synchronous/leader4_12.pm b/prism-examples/leader/synchronous/leader4_12.pm
index 9188e23c..619c4ee4 100644
--- a/prism-examples/leader/synchronous/leader4_12.pm
+++ b/prism-examples/leader/synchronous/leader4_12.pm
@@ -2,7 +2,7 @@
 // dxp/gxn 25/01/01
 // N=4 and K=12
 
-probabilistic
+dtmc
 
 // CONSTANTS
 const N=4; // number of processes
diff --git a/prism-examples/leader/synchronous/leader4_14.pm b/prism-examples/leader/synchronous/leader4_14.pm
index 036f2941..de9a8f1f 100644
--- a/prism-examples/leader/synchronous/leader4_14.pm
+++ b/prism-examples/leader/synchronous/leader4_14.pm
@@ -2,7 +2,7 @@
 // dxp/gxn 25/01/01
 // N=4 and K=14
 
-probabilistic
+dtmc
 
 // CONSTANTS
 const N=4; // number of processes
diff --git a/prism-examples/leader/synchronous/leader4_16.pm b/prism-examples/leader/synchronous/leader4_16.pm
index e8098d2e..76d75de0 100644
--- a/prism-examples/leader/synchronous/leader4_16.pm
+++ b/prism-examples/leader/synchronous/leader4_16.pm
@@ -2,7 +2,7 @@
 // dxp/gxn 25/01/01
 // N=4 and K=16
 
-probabilistic
+dtmc
 
 // CONSTANTS
 const N=4; // number of processes
diff --git a/prism-examples/leader/synchronous/leader4_2.pm b/prism-examples/leader/synchronous/leader4_2.pm
index 7cb78c3b..9e53cfe6 100644
--- a/prism-examples/leader/synchronous/leader4_2.pm
+++ b/prism-examples/leader/synchronous/leader4_2.pm
@@ -2,7 +2,7 @@
 // dxp/gxn 25/01/01
 // N=4 and K=2
 
-probabilistic
+dtmc
 
 // CONSTANTS
 const N=4; // number of processes
diff --git a/prism-examples/leader/synchronous/leader4_3.pm b/prism-examples/leader/synchronous/leader4_3.pm
index af3bf0b5..29123119 100644
--- a/prism-examples/leader/synchronous/leader4_3.pm
+++ b/prism-examples/leader/synchronous/leader4_3.pm
@@ -2,7 +2,7 @@
 // dxp/gxn 25/01/01
 // N=4 and K=4
 
-probabilistic
+dtmc
 
 // CONSTANTS
 const N=4; // number of processes
diff --git a/prism-examples/leader/synchronous/leader4_4.pm b/prism-examples/leader/synchronous/leader4_4.pm
index 16ea8fac..89cdb362 100644
--- a/prism-examples/leader/synchronous/leader4_4.pm
+++ b/prism-examples/leader/synchronous/leader4_4.pm
@@ -2,7 +2,7 @@
 // dxp/gxn 25/01/01
 // N=4 and K=4
 
-probabilistic
+dtmc
 
 // CONSTANTS
 const N=4; // number of processes
diff --git a/prism-examples/leader/synchronous/leader4_5.pm b/prism-examples/leader/synchronous/leader4_5.pm
index 5bf28bac..c77a2a7c 100644
--- a/prism-examples/leader/synchronous/leader4_5.pm
+++ b/prism-examples/leader/synchronous/leader4_5.pm
@@ -2,7 +2,7 @@
 // dxp/gxn 25/01/01
 // N=4 and K=6
 
-probabilistic
+dtmc
 
 // CONSTANTS
 const N=4; // number of processes
diff --git a/prism-examples/leader/synchronous/leader4_6.pm b/prism-examples/leader/synchronous/leader4_6.pm
index 3b58edd4..69050c23 100644
--- a/prism-examples/leader/synchronous/leader4_6.pm
+++ b/prism-examples/leader/synchronous/leader4_6.pm
@@ -2,7 +2,7 @@
 // dxp/gxn 25/01/01
 // N=4 and K=6
 
-probabilistic
+dtmc
 
 // CONSTANTS
 const N=4; // number of processes
diff --git a/prism-examples/leader/synchronous/leader4_8.pm b/prism-examples/leader/synchronous/leader4_8.pm
index b55e6679..490c35ba 100644
--- a/prism-examples/leader/synchronous/leader4_8.pm
+++ b/prism-examples/leader/synchronous/leader4_8.pm
@@ -2,7 +2,7 @@
 // dxp/gxn 25/01/01
 // N=4 and K=8
 
-probabilistic
+dtmc
 
 // CONSTANTS
 const N=4; // number of processes
diff --git a/prism-examples/leader/synchronous/leader5_2.pm b/prism-examples/leader/synchronous/leader5_2.pm
index 7208c0c2..694b0c86 100644
--- a/prism-examples/leader/synchronous/leader5_2.pm
+++ b/prism-examples/leader/synchronous/leader5_2.pm
@@ -2,7 +2,7 @@
 // dxp/gxn 25/01/01
 // N=5 and K=2
 
-probabilistic
+dtmc
 
 // CONSTANTS
 const N=5; // number of processes
diff --git a/prism-examples/leader/synchronous/leader5_3.pm b/prism-examples/leader/synchronous/leader5_3.pm
index db586bba..75029822 100644
--- a/prism-examples/leader/synchronous/leader5_3.pm
+++ b/prism-examples/leader/synchronous/leader5_3.pm
@@ -2,7 +2,7 @@
 // dxp/gxn 25/01/01
 // N=5 and K=4
 
-probabilistic
+dtmc
 
 // CONSTANTS
 const N=5; // number of processes
diff --git a/prism-examples/leader/synchronous/leader5_4.pm b/prism-examples/leader/synchronous/leader5_4.pm
index 48adcfd2..6edecd6c 100644
--- a/prism-examples/leader/synchronous/leader5_4.pm
+++ b/prism-examples/leader/synchronous/leader5_4.pm
@@ -2,7 +2,7 @@
 // dxp/gxn 25/01/01
 // N=5 and K=4
 
-probabilistic
+dtmc
 
 // CONSTANTS
 const N=5; // number of processes
diff --git a/prism-examples/leader/synchronous/leader5_5.pm b/prism-examples/leader/synchronous/leader5_5.pm
index a7d5d3ec..f88e974c 100644
--- a/prism-examples/leader/synchronous/leader5_5.pm
+++ b/prism-examples/leader/synchronous/leader5_5.pm
@@ -2,7 +2,7 @@
 // dxp/gxn 25/01/01
 // N=5 and K=6
 
-probabilistic
+dtmc
 
 // CONSTANTS
 const N=5; // number of processes
diff --git a/prism-examples/leader/synchronous/leader5_6.pm b/prism-examples/leader/synchronous/leader5_6.pm
index 354916d8..b38888df 100644
--- a/prism-examples/leader/synchronous/leader5_6.pm
+++ b/prism-examples/leader/synchronous/leader5_6.pm
@@ -2,7 +2,7 @@
 // dxp/gxn 25/01/01
 // N=5 and K=6
 
-probabilistic
+dtmc
 
 // CONSTANTS
 const N=5; // number of processes
diff --git a/prism-examples/leader/synchronous/leader5_8.pm b/prism-examples/leader/synchronous/leader5_8.pm
index c66225a9..e5930709 100644
--- a/prism-examples/leader/synchronous/leader5_8.pm
+++ b/prism-examples/leader/synchronous/leader5_8.pm
@@ -2,7 +2,7 @@
 // dxp/gxn 25/01/01
 // N=5 and K=8
 
-probabilistic
+dtmc
 
 // CONSTANTS
 const N=5; // number of processes
diff --git a/prism-examples/leader/synchronous/leader6_2.pm b/prism-examples/leader/synchronous/leader6_2.pm
index f437269e..2d3ee80b 100644
--- a/prism-examples/leader/synchronous/leader6_2.pm
+++ b/prism-examples/leader/synchronous/leader6_2.pm
@@ -2,7 +2,7 @@
 // dxp/gxn 25/01/01
 // N=6 and K=2
 
-probabilistic
+dtmc
 
 // CONSTANTS
 const N=6; // number of processes
diff --git a/prism-examples/leader/synchronous/leader6_3.pm b/prism-examples/leader/synchronous/leader6_3.pm
index 4feaedd9..049dfc60 100644
--- a/prism-examples/leader/synchronous/leader6_3.pm
+++ b/prism-examples/leader/synchronous/leader6_3.pm
@@ -2,7 +2,7 @@
 // dxp/gxn 25/01/01
 // N=6 and K=4
 
-probabilistic
+dtmc
 
 // CONSTANTS
 const N=6; // number of processes
diff --git a/prism-examples/leader/synchronous/leader6_4.pm b/prism-examples/leader/synchronous/leader6_4.pm
index 02d7579d..cebd99a0 100644
--- a/prism-examples/leader/synchronous/leader6_4.pm
+++ b/prism-examples/leader/synchronous/leader6_4.pm
@@ -2,7 +2,7 @@
 // dxp/gxn 25/01/01
 // N=6 and K=4
 
-probabilistic
+dtmc
 
 // CONSTANTS
 const N=6; // number of processes
diff --git a/prism-examples/leader/synchronous/leader6_5.pm b/prism-examples/leader/synchronous/leader6_5.pm
index e373c5ef..c13c31eb 100644
--- a/prism-examples/leader/synchronous/leader6_5.pm
+++ b/prism-examples/leader/synchronous/leader6_5.pm
@@ -2,7 +2,7 @@
 // dxp/gxn 25/01/01
 // N=6 and K=6
 
-probabilistic
+dtmc
 
 // CONSTANTS
 const N=6; // number of processes
diff --git a/prism-examples/leader/synchronous/leader6_6.pm b/prism-examples/leader/synchronous/leader6_6.pm
index 74e37503..722ea76f 100644
--- a/prism-examples/leader/synchronous/leader6_6.pm
+++ b/prism-examples/leader/synchronous/leader6_6.pm
@@ -2,7 +2,7 @@
 // dxp/gxn 25/01/01
 // N=6 and K=6
 
-probabilistic
+dtmc
 
 // CONSTANTS
 const N=6; // number of processes
diff --git a/prism-examples/leader/synchronous/leader7_2.pm b/prism-examples/leader/synchronous/leader7_2.pm
index 7ba27b52..9b74ec71 100644
--- a/prism-examples/leader/synchronous/leader7_2.pm
+++ b/prism-examples/leader/synchronous/leader7_2.pm
@@ -2,7 +2,7 @@
 // dxp/gxn 25/01/01
 // N=6 and K=2
 
-probabilistic
+dtmc
 
 // CONSTANTS
 const N=7; // number of processes
diff --git a/prism-examples/leader/synchronous/leader7_3.pm b/prism-examples/leader/synchronous/leader7_3.pm
index 3758896e..ddec847a 100644
--- a/prism-examples/leader/synchronous/leader7_3.pm
+++ b/prism-examples/leader/synchronous/leader7_3.pm
@@ -2,7 +2,7 @@
 // dxp/gxn 25/01/01
 // N=6 and K=4
 
-probabilistic
+dtmc
 
 // CONSTANTS
 const N=7; // number of processes
diff --git a/prism-examples/leader/synchronous/leader7_4.pm b/prism-examples/leader/synchronous/leader7_4.pm
index 31ede985..0ca24e3a 100644
--- a/prism-examples/leader/synchronous/leader7_4.pm
+++ b/prism-examples/leader/synchronous/leader7_4.pm
@@ -2,7 +2,7 @@
 // dxp/gxn 25/01/01
 // N=6 and K=4
 
-probabilistic
+dtmc
 
 // CONSTANTS
 const N=7; // number of processes
diff --git a/prism-examples/leader/synchronous/leader7_5.pm b/prism-examples/leader/synchronous/leader7_5.pm
index f1f3e21d..cea22744 100644
--- a/prism-examples/leader/synchronous/leader7_5.pm
+++ b/prism-examples/leader/synchronous/leader7_5.pm
@@ -2,7 +2,7 @@
 // dxp/gxn 25/01/01
 // N=6 and K=4
 
-probabilistic
+dtmc
 
 // CONSTANTS
 const N=7; // number of processes
diff --git a/prism-examples/leader/synchronous/leader8_2.pm b/prism-examples/leader/synchronous/leader8_2.pm
index b03ac96e..95e06211 100644
--- a/prism-examples/leader/synchronous/leader8_2.pm
+++ b/prism-examples/leader/synchronous/leader8_2.pm
@@ -2,7 +2,7 @@
 // dxp/gxn 25/01/01
 // N=8 and K=2
 
-probabilistic
+dtmc
 
 // CONSTANTS
 const N=8; // number of processes
diff --git a/prism-examples/leader/synchronous/leader8_3.pm b/prism-examples/leader/synchronous/leader8_3.pm
index dcd1e8d8..4ccb17d5 100644
--- a/prism-examples/leader/synchronous/leader8_3.pm
+++ b/prism-examples/leader/synchronous/leader8_3.pm
@@ -2,7 +2,7 @@
 // dxp/gxn 25/01/01
 // N=8 and K=4
 
-probabilistic
+dtmc
 
 // CONSTANTS
 const N=8; // number of processes
diff --git a/prism-examples/leader/synchronous/leader8_4.pm b/prism-examples/leader/synchronous/leader8_4.pm
index 4a220e75..75e26d8b 100644
--- a/prism-examples/leader/synchronous/leader8_4.pm
+++ b/prism-examples/leader/synchronous/leader8_4.pm
@@ -2,7 +2,7 @@
 // dxp/gxn 25/01/01
 // N=8 and K=4
 
-probabilistic
+dtmc
 
 // CONSTANTS
 const N=8; // number of processes
diff --git a/prism-examples/leader/synchronous/leader8_6.pm b/prism-examples/leader/synchronous/leader8_6.pm
index 39425e08..490faf28 100644
--- a/prism-examples/leader/synchronous/leader8_6.pm
+++ b/prism-examples/leader/synchronous/leader8_6.pm
@@ -2,7 +2,7 @@
 // dxp/gxn 25/01/01
 // N=8 and K=6
 
-probabilistic
+dtmc
 
 // CONSTANTS
 const N=8; // number of processes
diff --git a/prism-examples/leader/synchronous/leader9_2.pm b/prism-examples/leader/synchronous/leader9_2.pm
index 18a4dbe2..9e64ea5f 100644
--- a/prism-examples/leader/synchronous/leader9_2.pm
+++ b/prism-examples/leader/synchronous/leader9_2.pm
@@ -2,7 +2,7 @@
 // dxp/gxn 25/01/01
 // N=8 and K=2
 
-probabilistic
+dtmc
 
 // CONSTANTS
 const N=9; // number of processes
diff --git a/prism-examples/leader/synchronous/leader9_3.pm b/prism-examples/leader/synchronous/leader9_3.pm
index 1207e78d..082bee56 100644
--- a/prism-examples/leader/synchronous/leader9_3.pm
+++ b/prism-examples/leader/synchronous/leader9_3.pm
@@ -2,7 +2,7 @@
 // dxp/gxn 25/01/01
 // N=8 and K=4
 
-probabilistic
+dtmc
 
 // CONSTANTS
 const N=9; // number of processes
diff --git a/prism-examples/leader/synchronous/leader9_4.pm b/prism-examples/leader/synchronous/leader9_4.pm
index 23a489bf..f7e2aa78 100644
--- a/prism-examples/leader/synchronous/leader9_4.pm
+++ b/prism-examples/leader/synchronous/leader9_4.pm
@@ -2,7 +2,7 @@
 // dxp/gxn 25/01/01
 // N=8 and K=4
 
-probabilistic
+dtmc
 
 // CONSTANTS
 const N=9; // number of processes