Browse Source

Model keyword tidy-up: nondeterministic -> mdp.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@573 bbc10eb1-c90d-0410-af57-cb519fbb1720
master
Dave Parker 18 years ago
parent
commit
644026f7ea
  1. 2
      prism-examples/firewire/abst/deadline.nm
  2. 2
      prism-examples/firewire/abst/firewire.nm
  3. 2
      prism-examples/leader/asynchronous/leader10.nm
  4. 2
      prism-examples/leader/asynchronous/leader3.nm
  5. 2
      prism-examples/leader/asynchronous/leader4.nm
  6. 2
      prism-examples/leader/asynchronous/leader5.nm
  7. 2
      prism-examples/leader/asynchronous/leader6.nm
  8. 2
      prism-examples/leader/asynchronous/leader7.nm
  9. 2
      prism-examples/leader/asynchronous/leader8.nm
  10. 2
      prism-examples/leader/asynchronous/leader9.nm
  11. 2
      prism-examples/mutual/mutual10.nm
  12. 2
      prism-examples/mutual/mutual3.nm
  13. 2
      prism-examples/mutual/mutual4.nm
  14. 2
      prism-examples/mutual/mutual5.nm
  15. 2
      prism-examples/mutual/mutual8.nm
  16. 6
      prism-examples/phil/nofair/phil-nofair10.nm
  17. 6
      prism-examples/phil/nofair/phil-nofair3.nm
  18. 6
      prism-examples/phil/nofair/phil-nofair4.nm
  19. 6
      prism-examples/phil/nofair/phil-nofair5.nm
  20. 6
      prism-examples/phil/nofair/phil-nofair6.nm
  21. 6
      prism-examples/phil/nofair/phil-nofair7.nm
  22. 6
      prism-examples/phil/nofair/phil-nofair8.nm
  23. 8
      prism-examples/phil/nofair/phil-nofair9.nm
  24. 3
      prism-examples/phil/original/phil10.nm
  25. 3
      prism-examples/phil/original/phil15.nm
  26. 3
      prism-examples/phil/original/phil20.nm
  27. 3
      prism-examples/phil/original/phil25.nm
  28. 3
      prism-examples/phil/original/phil3.nm
  29. 3
      prism-examples/phil/original/phil30.nm
  30. 3
      prism-examples/phil/original/phil4.nm
  31. 3
      prism-examples/phil/original/phil5.nm
  32. 3
      prism-examples/phil/original/phil6.nm
  33. 3
      prism-examples/phil/original/phil7.nm
  34. 3
      prism-examples/phil/original/phil8.nm
  35. 2
      prism-examples/phil/original/phil9.nm
  36. 4
      prism-examples/phil_lss/phil_lss3.nm
  37. 4
      prism-examples/phil_lss/phil_lss4.nm

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

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

2
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

2
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

2
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

2
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

2
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

2
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

2
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

2
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

2
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

2
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

2
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

2
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

2
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

4
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

4
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
Loading…
Cancel
Save