Model keyword tidy-up: probabilistic -> dtmc.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@572 bbc10eb1-c90d-0410-af57-cb519fbb1720
18 years ago · a8e1ca8379
47 changed files with 47 additions and 47 deletions
--- 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;
--- a/prism-examples/dice/dice.pm
+++ b/prism-examples/dice/dice.pm
@ -1,4 +1,4 @@
-probabilistic
+dtmc

 module die

--- a/prism-examples/dice/two_dice.nm
+++ b/prism-examples/dice/two_dice.nm
@ -1,4 +1,4 @@
-nondeterministic
+mdp

 module die1

--- 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
 	
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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
--- 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