From 644026f7ea0f6e61e4bd954cb5f61a3c5f0f8703 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Thu, 28 Feb 2008 10:15:35 +0000
Subject: [PATCH] Model keyword tidy-up: nondeterministic -> mdp.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@573 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism-examples/firewire/abst/deadline.nm       | 2 +-
 prism-examples/firewire/abst/firewire.nm       | 2 +-
 prism-examples/leader/asynchronous/leader10.nm | 2 +-
 prism-examples/leader/asynchronous/leader3.nm  | 2 +-
 prism-examples/leader/asynchronous/leader4.nm  | 2 +-
 prism-examples/leader/asynchronous/leader5.nm  | 2 +-
 prism-examples/leader/asynchronous/leader6.nm  | 2 +-
 prism-examples/leader/asynchronous/leader7.nm  | 2 +-
 prism-examples/leader/asynchronous/leader8.nm  | 2 +-
 prism-examples/leader/asynchronous/leader9.nm  | 2 +-
 prism-examples/mutual/mutual10.nm              | 2 +-
 prism-examples/mutual/mutual3.nm               | 2 +-
 prism-examples/mutual/mutual4.nm               | 2 +-
 prism-examples/mutual/mutual5.nm               | 2 +-
 prism-examples/mutual/mutual8.nm               | 2 +-
 prism-examples/phil/nofair/phil-nofair10.nm    | 6 +++---
 prism-examples/phil/nofair/phil-nofair3.nm     | 6 +++---
 prism-examples/phil/nofair/phil-nofair4.nm     | 6 +++---
 prism-examples/phil/nofair/phil-nofair5.nm     | 6 +++---
 prism-examples/phil/nofair/phil-nofair6.nm     | 6 +++---
 prism-examples/phil/nofair/phil-nofair7.nm     | 6 +++---
 prism-examples/phil/nofair/phil-nofair8.nm     | 6 +++---
 prism-examples/phil/nofair/phil-nofair9.nm     | 8 ++++----
 prism-examples/phil/original/phil10.nm         | 3 ---
 prism-examples/phil/original/phil15.nm         | 3 ---
 prism-examples/phil/original/phil20.nm         | 3 ---
 prism-examples/phil/original/phil25.nm         | 3 ---
 prism-examples/phil/original/phil3.nm          | 3 ---
 prism-examples/phil/original/phil30.nm         | 3 ---
 prism-examples/phil/original/phil4.nm          | 3 ---
 prism-examples/phil/original/phil5.nm          | 3 ---
 prism-examples/phil/original/phil6.nm          | 3 ---
 prism-examples/phil/original/phil7.nm          | 3 ---
 prism-examples/phil/original/phil8.nm          | 3 ---
 prism-examples/phil/original/phil9.nm          | 2 +-
 prism-examples/phil_lss/phil_lss3.nm           | 4 ++--
 prism-examples/phil_lss/phil_lss4.nm           | 4 ++--
 37 files changed, 45 insertions(+), 78 deletions(-)

diff --git a/prism-examples/firewire/abst/deadline.nm b/prism-examples/firewire/abst/deadline.nm
index e2004204..7ebe3e84 100644
--- a/prism-examples/firewire/abst/deadline.nm
+++ b/prism-examples/firewire/abst/deadline.nm
@@ -1,7 +1,7 @@
 // integer semantics version of abstract firewire protocol
 // gxn 23/05/2001
 
-nondeterministic
+mdp
 
 //deadline
 const int deadline;
diff --git a/prism-examples/firewire/abst/firewire.nm b/prism-examples/firewire/abst/firewire.nm
index 0b0bf4cf..f1b30837 100644
--- a/prism-examples/firewire/abst/firewire.nm
+++ b/prism-examples/firewire/abst/firewire.nm
@@ -1,7 +1,7 @@
 // integer semantics version of abstract firewire protocol
 // gxn 23/05/2001
 
-nondeterministic
+mdp
 
 // largest constant the clock of the system is compared to
 const int kx = 167;
diff --git a/prism-examples/leader/asynchronous/leader10.nm b/prism-examples/leader/asynchronous/leader10.nm
index cb478272..59361e4f 100644
--- a/prism-examples/leader/asynchronous/leader10.nm
+++ b/prism-examples/leader/asynchronous/leader10.nm
@@ -2,7 +2,7 @@
 // 10 processes
 // gxn/dxp 29/01/01
 
-nondeterministic
+mdp
 
 const N=10; // number of processes
 
diff --git a/prism-examples/leader/asynchronous/leader3.nm b/prism-examples/leader/asynchronous/leader3.nm
index 109915fa..bdbba975 100644
--- a/prism-examples/leader/asynchronous/leader3.nm
+++ b/prism-examples/leader/asynchronous/leader3.nm
@@ -2,7 +2,7 @@
 // 3 processes
 // gxn/dxp 29/01/01
 
-nondeterministic
+mdp
 
 const N=3; // number of processes
 
diff --git a/prism-examples/leader/asynchronous/leader4.nm b/prism-examples/leader/asynchronous/leader4.nm
index f98ff23a..7e9d3bd3 100644
--- a/prism-examples/leader/asynchronous/leader4.nm
+++ b/prism-examples/leader/asynchronous/leader4.nm
@@ -2,7 +2,7 @@
 // 4 processes
 // gxn/dxp 29/01/01
 
-nondeterministic
+mdp
 
 const N=4; // number of processes
 
diff --git a/prism-examples/leader/asynchronous/leader5.nm b/prism-examples/leader/asynchronous/leader5.nm
index 2b2cbffa..898b7774 100644
--- a/prism-examples/leader/asynchronous/leader5.nm
+++ b/prism-examples/leader/asynchronous/leader5.nm
@@ -2,7 +2,7 @@
 // 5 processes
 // gxn/dxp 29/01/01
 
-nondeterministic
+mdp
 
 const N=5; // number of processes
 
diff --git a/prism-examples/leader/asynchronous/leader6.nm b/prism-examples/leader/asynchronous/leader6.nm
index dff20681..b122abe9 100644
--- a/prism-examples/leader/asynchronous/leader6.nm
+++ b/prism-examples/leader/asynchronous/leader6.nm
@@ -2,7 +2,7 @@
 // 6 processes
 // gxn/dxp 29/01/01
 
-nondeterministic
+mdp
 
 const N=6; // number of processes
 
diff --git a/prism-examples/leader/asynchronous/leader7.nm b/prism-examples/leader/asynchronous/leader7.nm
index d62611dd..74fb9fe7 100644
--- a/prism-examples/leader/asynchronous/leader7.nm
+++ b/prism-examples/leader/asynchronous/leader7.nm
@@ -2,7 +2,7 @@
 // 7 processes
 // gxn/dxp 29/01/01
 
-nondeterministic
+mdp
 
 const N=7; // number of processes
 
diff --git a/prism-examples/leader/asynchronous/leader8.nm b/prism-examples/leader/asynchronous/leader8.nm
index 8677b976..8e54eab1 100644
--- a/prism-examples/leader/asynchronous/leader8.nm
+++ b/prism-examples/leader/asynchronous/leader8.nm
@@ -2,7 +2,7 @@
 // 8 processes
 // gxn/dxp 29/01/01
 
-nondeterministic
+mdp
 
 const N=8; // number of processes
 
diff --git a/prism-examples/leader/asynchronous/leader9.nm b/prism-examples/leader/asynchronous/leader9.nm
index 191f7eec..5e97366e 100644
--- a/prism-examples/leader/asynchronous/leader9.nm
+++ b/prism-examples/leader/asynchronous/leader9.nm
@@ -2,7 +2,7 @@
 // 9 processes
 // gxn/dxp 29/01/01
 
-nondeterministic
+mdp
 
 const N=9; // number of processes
 
diff --git a/prism-examples/mutual/mutual10.nm b/prism-examples/mutual/mutual10.nm
index 99839cab..a51a40d7 100644
--- a/prism-examples/mutual/mutual10.nm
+++ b/prism-examples/mutual/mutual10.nm
@@ -1,7 +1,7 @@
 // mutual exclusion [PZ82]
 // dxp/gxn 19/12/99
 
-nondeterministic
+mdp
 
 // atomic formula
 // none in low, high, tie
diff --git a/prism-examples/mutual/mutual3.nm b/prism-examples/mutual/mutual3.nm
index 5d1f4b32..fe212e89 100644
--- a/prism-examples/mutual/mutual3.nm
+++ b/prism-examples/mutual/mutual3.nm
@@ -1,7 +1,7 @@
 // mutual exclusion [PZ82]
 // dxp/gxn 19/12/99
 
-nondeterministic
+mdp
 
 // atomic formula
 // none in low, high, tie
diff --git a/prism-examples/mutual/mutual4.nm b/prism-examples/mutual/mutual4.nm
index d0438646..1d468802 100644
--- a/prism-examples/mutual/mutual4.nm
+++ b/prism-examples/mutual/mutual4.nm
@@ -1,7 +1,7 @@
 // mutual exclusion [PZ82]
 // dxp/gxn 19/12/99
 
-nondeterministic
+mdp
 
 // atomic formula
 // none in low, high, tie
diff --git a/prism-examples/mutual/mutual5.nm b/prism-examples/mutual/mutual5.nm
index 1f3cf774..b3f10119 100644
--- a/prism-examples/mutual/mutual5.nm
+++ b/prism-examples/mutual/mutual5.nm
@@ -1,7 +1,7 @@
 // mutual exclusion [PZ82]
 // dxp/gxn 19/12/99
 
-nondeterministic
+mdp
 
 // atomic formula
 // none in low, high, tie
diff --git a/prism-examples/mutual/mutual8.nm b/prism-examples/mutual/mutual8.nm
index 5ee98f91..d834812a 100644
--- a/prism-examples/mutual/mutual8.nm
+++ b/prism-examples/mutual/mutual8.nm
@@ -1,7 +1,7 @@
 // mutual exclusion [PZ82]
 // dxp/gxn 19/12/99
 
-nondeterministic
+mdp
 
 // atomic formula
 // none in low, high, tie
diff --git a/prism-examples/phil/nofair/phil-nofair10.nm b/prism-examples/phil/nofair/phil-nofair10.nm
index f4c918b4..8b95e182 100644
--- a/prism-examples/phil/nofair/phil-nofair10.nm
+++ b/prism-examples/phil/nofair/phil-nofair10.nm
@@ -1,12 +1,12 @@
 // randomized dining philosophers [LR81]
-// dxp/gxn 23/01/02
-
+// dxp/gxn 23/01/02
+
 // model which does not require fairness
 // remove the possibility of loops:
 // (1) cannot stay in thinking 
 // (2) if first fork not free then cannot move (another philosopher must more)
 
-nondeterministic
+mdp
 
 // atomic formulae 
 // left fork free and right fork free resp.
diff --git a/prism-examples/phil/nofair/phil-nofair3.nm b/prism-examples/phil/nofair/phil-nofair3.nm
index ae71ccbc..9b46aaad 100644
--- a/prism-examples/phil/nofair/phil-nofair3.nm
+++ b/prism-examples/phil/nofair/phil-nofair3.nm
@@ -1,12 +1,12 @@
 // randomized dining philosophers [LR81]
-// dxp/gxn 23/01/02
-
+// dxp/gxn 23/01/02
+
 // model which does not require fairness
 // remove the possibility of loops:
 // (1) cannot stay in thinking 
 // (2) if first fork not free then cannot move (another philosopher must more)
 
-nondeterministic
+mdp
 
 // atomic formulae 
 // left fork free and right fork free resp.
diff --git a/prism-examples/phil/nofair/phil-nofair4.nm b/prism-examples/phil/nofair/phil-nofair4.nm
index 70c0718c..6ea7f254 100644
--- a/prism-examples/phil/nofair/phil-nofair4.nm
+++ b/prism-examples/phil/nofair/phil-nofair4.nm
@@ -1,12 +1,12 @@
 // randomized dining philosophers [LR81]
-// dxp/gxn 23/01/02
-
+// dxp/gxn 23/01/02
+
 // model which does not require fairness
 // remove the possibility of loops:
 // (1) cannot stay in thinking 
 // (2) if first fork not free then cannot move (another philosopher must more)
 
-nondeterministic
+mdp
 
 // atomic formulae 
 // left fork free and right fork free resp.
diff --git a/prism-examples/phil/nofair/phil-nofair5.nm b/prism-examples/phil/nofair/phil-nofair5.nm
index 5f4653d7..a12e9b69 100644
--- a/prism-examples/phil/nofair/phil-nofair5.nm
+++ b/prism-examples/phil/nofair/phil-nofair5.nm
@@ -1,12 +1,12 @@
 // randomized dining philosophers [LR81]
-// dxp/gxn 23/01/02
-
+// dxp/gxn 23/01/02
+
 // model which does not require fairness
 // remove the possibility of loops:
 // (1) cannot stay in thinking 
 // (2) if first fork not free then cannot move (another philosopher must more)
 
-nondeterministic
+mdp
 
 // atomic formulae 
 // left fork free and right fork free resp.
diff --git a/prism-examples/phil/nofair/phil-nofair6.nm b/prism-examples/phil/nofair/phil-nofair6.nm
index 17cc7f33..58588e9a 100644
--- a/prism-examples/phil/nofair/phil-nofair6.nm
+++ b/prism-examples/phil/nofair/phil-nofair6.nm
@@ -1,12 +1,12 @@
 // randomized dining philosophers [LR81]
-// dxp/gxn 23/01/02
-
+// dxp/gxn 23/01/02
+
 // model which does not require fairness
 // remove the possibility of loops:
 // (1) cannot stay in thinking 
 // (2) if first fork not free then cannot move (another philosopher must more)
 
-nondeterministic
+mdp
 
 // atomic formulae 
 // left fork free and right fork free resp.
diff --git a/prism-examples/phil/nofair/phil-nofair7.nm b/prism-examples/phil/nofair/phil-nofair7.nm
index e246ca65..95c1dc82 100644
--- a/prism-examples/phil/nofair/phil-nofair7.nm
+++ b/prism-examples/phil/nofair/phil-nofair7.nm
@@ -1,12 +1,12 @@
 // randomized dining philosophers [LR81]
-// dxp/gxn 23/01/02
-
+// dxp/gxn 23/01/02
+
 // model which does not require fairness
 // remove the possibility of loops:
 // (1) cannot stay in thinking 
 // (2) if first fork not free then cannot move (another philosopher must more)
 
-nondeterministic
+mdp
 
 // atomic formulae 
 // left fork free and right fork free resp.
diff --git a/prism-examples/phil/nofair/phil-nofair8.nm b/prism-examples/phil/nofair/phil-nofair8.nm
index 8b4086ab..cf7d2d2a 100644
--- a/prism-examples/phil/nofair/phil-nofair8.nm
+++ b/prism-examples/phil/nofair/phil-nofair8.nm
@@ -1,12 +1,12 @@
 // randomized dining philosophers [LR81]
-// dxp/gxn 23/01/02
-
+// dxp/gxn 23/01/02
+
 // model which does not require fairness
 // remove the possibility of loops:
 // (1) cannot stay in thinking 
 // (2) if first fork not free then cannot move (another philosopher must more)
 
-nondeterministic
+mdp
 
 // atomic formulae 
 // left fork free and right fork free resp.
diff --git a/prism-examples/phil/nofair/phil-nofair9.nm b/prism-examples/phil/nofair/phil-nofair9.nm
index f59d1aa3..f6c68452 100644
--- a/prism-examples/phil/nofair/phil-nofair9.nm
+++ b/prism-examples/phil/nofair/phil-nofair9.nm
@@ -1,12 +1,12 @@
 // randomized dining philosophers [LR81]
-// dxp/gxn 23/01/02
-
+// dxp/gxn 23/01/02
+
 // model which does not require fairness
 // remove the possibility of loops:
 // (1) cannot stay in thinking 
 // (2) if first fork not free then cannot move (another philosopher must more)
- 
-nondeterministic
+
+mdp
 
 // atomic formulae 
 // left fork free and right fork free resp.
diff --git a/prism-examples/phil/original/phil10.nm b/prism-examples/phil/original/phil10.nm
index 54a65dbd..d9a30e31 100644
--- a/prism-examples/phil/original/phil10.nm
+++ b/prism-examples/phil/original/phil10.nm
@@ -1,8 +1,5 @@
 // randomized dining philosophers [LR81]
 // dxp/gxn 12/12/99
-
-nondeterministic
-
 // atomic formulae 
 // left fork free and right fork free resp.
 formula lfree = p2=0..4,6,10;
diff --git a/prism-examples/phil/original/phil15.nm b/prism-examples/phil/original/phil15.nm
index b65fcc93..ed368194 100644
--- a/prism-examples/phil/original/phil15.nm
+++ b/prism-examples/phil/original/phil15.nm
@@ -1,8 +1,5 @@
 // randomized dining philosophers [LR81]
 // dxp/gxn 12/12/99
-
-nondeterministic
-
 // atomic formulae 
 // left fork free and right fork free resp.
 formula lfree = p2=0..4,6,10;
diff --git a/prism-examples/phil/original/phil20.nm b/prism-examples/phil/original/phil20.nm
index 4ff677fd..5c787b18 100644
--- a/prism-examples/phil/original/phil20.nm
+++ b/prism-examples/phil/original/phil20.nm
@@ -1,8 +1,5 @@
 // randomized dining philosophers [LR81]
 // dxp/gxn 12/12/99
-
-nondeterministic
-
 // atomic formulae 
 // left fork free and right fork free resp.
 formula lfree = p2=0..4,6,10;
diff --git a/prism-examples/phil/original/phil25.nm b/prism-examples/phil/original/phil25.nm
index 287c401f..9119b731 100644
--- a/prism-examples/phil/original/phil25.nm
+++ b/prism-examples/phil/original/phil25.nm
@@ -1,8 +1,5 @@
 // randomized dining philosophers [LR81]
 // dxp/gxn 12/12/99
-
-nondeterministic
-
 // atomic formulae 
 // left fork free and right fork free resp.
 formula lfree = p2=0..4,6,10;
diff --git a/prism-examples/phil/original/phil3.nm b/prism-examples/phil/original/phil3.nm
index 2655edb9..7430d21a 100644
--- a/prism-examples/phil/original/phil3.nm
+++ b/prism-examples/phil/original/phil3.nm
@@ -1,8 +1,5 @@
 // randomized dining philosophers [LR81]
 // dxp/gxn 12/12/99
-
-nondeterministic
-
 // atomic formulae 
 // left fork free and right fork free resp.
 formula lfree = p2=0..4,6,10;
diff --git a/prism-examples/phil/original/phil30.nm b/prism-examples/phil/original/phil30.nm
index 6db52712..2c117c94 100644
--- a/prism-examples/phil/original/phil30.nm
+++ b/prism-examples/phil/original/phil30.nm
@@ -1,8 +1,5 @@
 // randomized dining philosophers [LR81]
 // dxp/gxn 12/12/99
-
-nondeterministic
-
 // atomic formulae 
 // left fork free and right fork free resp.
 formula lfree = p2=0..4,6,10;
diff --git a/prism-examples/phil/original/phil4.nm b/prism-examples/phil/original/phil4.nm
index 9671bb89..13aa8ee8 100644
--- a/prism-examples/phil/original/phil4.nm
+++ b/prism-examples/phil/original/phil4.nm
@@ -1,8 +1,5 @@
 // randomized dining philosophers [LR81]
 // dxp/gxn 12/12/99
-
-nondeterministic
-
 // atomic formulae 
 // left fork free and right fork free resp.
 formula lfree = p2=0..4,6,10;
diff --git a/prism-examples/phil/original/phil5.nm b/prism-examples/phil/original/phil5.nm
index ea024be2..430d1ba7 100644
--- a/prism-examples/phil/original/phil5.nm
+++ b/prism-examples/phil/original/phil5.nm
@@ -1,8 +1,5 @@
 // randomized dining philosophers [LR81]
 // dxp/gxn 12/12/99
-
-nondeterministic
-
 // atomic formulae 
 // left fork free and right fork free resp.
 formula lfree = p2=0..4,6,10;
diff --git a/prism-examples/phil/original/phil6.nm b/prism-examples/phil/original/phil6.nm
index 76320189..16319711 100644
--- a/prism-examples/phil/original/phil6.nm
+++ b/prism-examples/phil/original/phil6.nm
@@ -1,8 +1,5 @@
 // randomized dining philosophers [LR81]
 // dxp/gxn 12/12/99
-
-nondeterministic
-
 // atomic formulae 
 // left fork free and right fork free resp.
 formula lfree = p2=0..4,6,10;
diff --git a/prism-examples/phil/original/phil7.nm b/prism-examples/phil/original/phil7.nm
index 77a6a822..4b0e5b3f 100644
--- a/prism-examples/phil/original/phil7.nm
+++ b/prism-examples/phil/original/phil7.nm
@@ -1,8 +1,5 @@
 // randomized dining philosophers [LR81]
 // dxp/gxn 12/12/99
-
-nondeterministic
-
 // atomic formulae 
 // left fork free and right fork free resp.
 formula lfree = p2=0..4,6,10;
diff --git a/prism-examples/phil/original/phil8.nm b/prism-examples/phil/original/phil8.nm
index c3ae741b..f1f6be1e 100644
--- a/prism-examples/phil/original/phil8.nm
+++ b/prism-examples/phil/original/phil8.nm
@@ -1,8 +1,5 @@
 // randomized dining philosophers [LR81]
 // dxp/gxn 12/12/99
-
-nondeterministic
-
 // atomic formulae 
 // left fork free and right fork free resp.
 formula lfree = p2=0..4,6,10;
diff --git a/prism-examples/phil/original/phil9.nm b/prism-examples/phil/original/phil9.nm
index f0de0ae9..6789c58b 100644
--- a/prism-examples/phil/original/phil9.nm
+++ b/prism-examples/phil/original/phil9.nm
@@ -1,7 +1,7 @@
 // randomized dining philosophers [LR81]
 // dxp/gxn 12/12/99
 
-nondeterministic
+mdp
 
 // atomic formulae 
 // left fork free and right fork free resp.
diff --git a/prism-examples/phil_lss/phil_lss3.nm b/prism-examples/phil_lss/phil_lss3.nm
index ff56d849..c5e818fa 100644
--- a/prism-examples/phil_lss/phil_lss3.nm
+++ b/prism-examples/phil_lss/phil_lss3.nm
@@ -3,7 +3,7 @@
 // an a process can wait at most K time units before making a transition
 // gxn/dxp 01/02/00
 
-nondeterministic
+mdp
 
 // CONSTANTS
 const K;
@@ -96,4 +96,4 @@ rewards "steps"
 	[s1] true : 1;
 	[s2] true : 1;
 	[s3] true : 1;
-endrewards
+endrewards
diff --git a/prism-examples/phil_lss/phil_lss4.nm b/prism-examples/phil_lss/phil_lss4.nm
index 3326c901..0ef63eb3 100644
--- a/prism-examples/phil_lss/phil_lss4.nm
+++ b/prism-examples/phil_lss/phil_lss4.nm
@@ -3,7 +3,7 @@
 // an a process can wait at most K time units before making a transition
 // gxn/dxp 01/02/00
 
-nondeterministic
+mdp
 
 // CONSTANTS
 const K;
@@ -125,4 +125,4 @@ rewards "steps"
 	[s2] true : 1;
 	[s3] true : 1;
 	[s4] true : 1;
-endrewards
+endrewards