s14h
/
prism-accumulation
1
0
Fork 0
Code Releases Activity
Browse Source

Update some POMDP examples now that observables can be expressions. 

Also fix a bug in maze2.prism (location s=10).
accumulation-v4.7
Dave Parker 5 years ago
parent
35f392ec5e
commit
e5ea762d80
12 changed files with 282 additions and 427 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 48
      prism-examples/pomdps/gridworld/3x3grid.prism
  2. 51
      prism-examples/pomdps/gridworld/3x3grid_bounded.prism
  3. 64
      prism-examples/pomdps/gridworld/4x4grid.prism
  4. 63
      prism-examples/pomdps/gridworld/4x4grid_bounded.prism
  5. 2
      prism-examples/pomdps/gridworld/grid.props
  6. 2
      prism-examples/pomdps/gridworld/grid_bounded.props
  7. 117
      prism-examples/pomdps/simple/maze.prism
  8. 121
      prism-examples/pomdps/simple/maze2.prism
  9. 117
      prism-tests/functionality/verify/pomdps/maze.prism
  10. 121
      prism-tests/functionality/verify/pomdps/maze2.prism
  11. 2
      prism-tests/functionality/verify/pomdps/maze2.prism.props
  12. 1
      prism-tests/functionality/verify/pomdps/maze2.prism.props.args

48
prism-examples/pomdps/gridworld/3x3grid.prism
View File

@ -5,41 +5,39 @@
pomdp
const int N = 3; // grid size
// only the target is observable which is in the south east corner
observables
o
endobservables
// (also if the initialisation step has been done)
formula target = x=N-1 & y=0;
observable "target" = target;
observable "started" = started;
module grid
x : [0..2]; // x coordinate
y : [0..2]; // y coordinate
o : [0..2]; // observables
// 0 - initial observation
// 1 - in the grid (not target)
// 2 - observe target
x : [0..N-1]; // x coordinate
y : [0..N-1]; // y coordinate
started : bool; // initialised?
// initially randomly placed within the grid (not at the target)
[] o=0 -> 1/8 : (o'=1) & (x'=0) & (y'=0)
+ 1/8 : (o'=1) & (x'=0) & (y'=1)
+ 1/8 : (o'=1) & (x'=0) & (y'=2)
+ 1/8 : (o'=1) & (x'=1) & (y'=0)
+ 1/8 : (o'=1) & (x'=1) & (y'=1)
+ 1/8 : (o'=1) & (x'=1) & (y'=2)
// + 1/8 : (o'=1) & (x'=2) & (y'=0) the target
+ 1/8 : (o'=1) & (x'=2) & (y'=1)
+ 1/8 : (o'=1) & (x'=2) & (y'=2);
[] !started -> 1/8 : (started'=true) & (x'=0) & (y'=0)
+ 1/8 : (started'=true) & (x'=0) & (y'=1)
+ 1/8 : (started'=true) & (x'=0) & (y'=2)
+ 1/8 : (started'=true) & (x'=1) & (y'=0)
+ 1/8 : (started'=true) & (x'=1) & (y'=1)
+ 1/8 : (started'=true) & (x'=1) & (y'=2)
// + 1/8 : (started'=true) & (x'=2) & (y'=0) the target
+ 1/8 : (started'=true) & (x'=2) & (y'=1)
+ 1/8 : (started'=true) & (x'=2) & (y'=2);
// move around the grid
[east] o=1 & !(x=1 & y=0) -> (x'=min(x+1,2)); // not reached target
[east] o=1 & x=1 & y=0 -> (x'=min(x+1,2)) & (o'=2);
[west] o=1 -> (x'=max(x-1,0)); // not reached target
[north] o=1 -> (x'=min(y+1,2)); // reached target
[south] o=1 & !(x=2 & y=1) -> (y'=max(y-1,0)); // not reached target
[south] o=1 & x=2 & y=1 -> (y'=max(y-1,0)) & (o'=2); // reached target
[east] started & !target -> (x'=min(x+1,N-1));
[west] started & !target -> (x'=max(x-1,0));
[north] started & !target -> (x'=min(y+1,N-1));
[south] started & !target -> (y'=max(y-1,0));
// reached target
[done] o=2 -> true;
[done] target -> true;
endmodule

51
prism-examples/pomdps/gridworld/3x3grid_bounded.prism
View File

@ -5,45 +5,42 @@
pomdp
const int N = 3; // grid size
const int K; // step bound in property
// only the target is observable which is in the south east corner
// (and the step bound)
observables
o, k
endobservables
// (also if the initialisation step has been done and the step count)
formula target = x=N-1 & y=0;
observable "target" = target;
observable "started" = started;
observable "k" = k;
module grid
x : [0..2]; // x coordinate
y : [0..2]; // y coordinate
o : [0..2]; // observables
// 0 - initial observation
// 1 - in the grid (not target)
// 2 - observe target
x : [0..N-1]; // x coordinate
y : [0..N-1]; // y coordinate
started : bool; // initialised?
// initially randomly placed within the grid (not at the target)
[] o=0 -> 1/8 : (o'=1) & (x'=0) & (y'=0)
+ 1/8 : (o'=1) & (x'=0) & (y'=1)
+ 1/8 : (o'=1) & (x'=0) & (y'=2)
+ 1/8 : (o'=1) & (x'=1) & (y'=0)
+ 1/8 : (o'=1) & (x'=1) & (y'=1)
+ 1/8 : (o'=1) & (x'=1) & (y'=2)
// + 1/8 : (o'=1) & (x'=2) & (y'=0) the target
+ 1/8 : (o'=1) & (x'=2) & (y'=1)
+ 1/8 : (o'=1) & (x'=2) & (y'=2);
[] !started -> 1/8 : (started'=true) & (x'=0) & (y'=0)
+ 1/8 : (started'=true) & (x'=0) & (y'=1)
+ 1/8 : (started'=true) & (x'=0) & (y'=2)
+ 1/8 : (started'=true) & (x'=1) & (y'=0)
+ 1/8 : (started'=true) & (x'=1) & (y'=1)
+ 1/8 : (started'=true) & (x'=1) & (y'=2)
// + 1/8 : (started'=true) & (x'=2) & (y'=0) the target
+ 1/8 : (started'=true) & (x'=2) & (y'=1)
+ 1/8 : (started'=true) & (x'=2) & (y'=2);
// move around the grid
[east] o=1 & !(x=1 & y=0) -> (x'=min(x+1,2)); // not reached target
[east] o=1 & x=1 & y=0 -> (x'=min(x+1,2)) & (o'=2); // reached target
[west] o=1 -> (x'=max(x-1,0)); // not reached target
[north] o=1 -> (x'=min(y+1,2)); // reached target
[south] o=1 & !(x=2 & y=1) -> (y'=max(y-1,0)); // not reached target
[south] o=1 & x=2 & y=1 -> (y'=max(y-1,0)) & (o'=2); // reached target
[east] started & !target -> (x'=min(x+1,N-1));
[west] started & !target -> (x'=max(x-1,0));
[north] started & !target -> (x'=min(y+1,N-1));
[south] started & !target -> (y'=max(y-1,0));
// reached target
[done] o=2 -> true;
[done] target -> true;
endmodule
// module for the step bound

64
prism-examples/pomdps/gridworld/4x4grid.prism
View File

@ -5,48 +5,46 @@
pomdp
const int N = 4; // grid size
// only the target is observable which is in the south east corner
observables
o
endobservables
// (also if the initialisation step has been done)
formula target = x=N-1 & y=0;
observable "target" = target;
observable "started" = started;
module grid
x : [0..2]; // x coordinate
y : [0..2]; // y coordinate
o : [0..2]; // observables
// 0 - initial observation
// 1 - in the grid (not target)
// 2 - observe target
x : [0..N-1]; // x coordinate
y : [0..N-1]; // y coordinate
started : bool; // initialised?
// initially randomly placed within the grid (not at the target)
[] o=0 -> 1/15 : (o'=1) & (x'=0) & (y'=0)
+ 1/15 : (o'=1) & (x'=0) & (y'=1)
+ 1/15 : (o'=1) & (x'=0) & (y'=2)
+ 1/15 : (o'=1) & (x'=0) & (y'=3)
+ 1/15 : (o'=1) & (x'=1) & (y'=0)
+ 1/15 : (o'=1) & (x'=1) & (y'=1)
+ 1/15 : (o'=1) & (x'=1) & (y'=2)
+ 1/15 : (o'=1) & (x'=1) & (y'=3)
+ 1/15 : (o'=1) & (x'=2) & (y'=0)
+ 1/15 : (o'=1) & (x'=2) & (y'=1)
+ 1/15 : (o'=1) & (x'=2) & (y'=2)
+ 1/15 : (o'=1) & (x'=2) & (y'=3)
// + 1/15 : (o'=1) & (x'=3) & (y'=0) this is the traget
+ 1/15 : (o'=1) & (x'=3) & (y'=1)
+ 1/15 : (o'=1) & (x'=3) & (y'=2)
+ 1/15 : (o'=1) & (x'=3) & (y'=3);
[] !started -> 1/15 : (started'=true) & (x'=0) & (y'=0)
+ 1/15 : (started'=true) & (x'=0) & (y'=1)
+ 1/15 : (started'=true) & (x'=0) & (y'=2)
+ 1/15 : (started'=true) & (x'=0) & (y'=3)
+ 1/15 : (started'=true) & (x'=1) & (y'=0)
+ 1/15 : (started'=true) & (x'=1) & (y'=1)
+ 1/15 : (started'=true) & (x'=1) & (y'=2)
+ 1/15 : (started'=true) & (x'=1) & (y'=3)
+ 1/15 : (started'=true) & (x'=2) & (y'=0)
+ 1/15 : (started'=true) & (x'=2) & (y'=1)
+ 1/15 : (started'=true) & (x'=2) & (y'=2)
+ 1/15 : (started'=true) & (x'=2) & (y'=3)
// + 1/15 : (started'=true) & (x'=3) & (y'=0) the target
+ 1/15 : (started'=true) & (x'=3) & (y'=1)
+ 1/15 : (started'=true) & (x'=3) & (y'=2)
+ 1/15 : (started'=true) & (x'=3) & (y'=3);
// move around the grid
[east] o=1 & !(x=2 & y=0) -> (x'=min(x+1,3)); // not reached target
[east] o=1 & x=2 & y=0 -> (x'=min(x+1,3)) & (o'=2); // reached target
[west] o=1 -> (x'=max(x-1,0)); // not reached target
[north] o=1 -> (x'=min(y+1,3)); // reached target
[south] o=1 & !(x=3 & y=1) -> (y'=max(y-1,0)); // not reached target
[south] o=1 & x=3 & y=1 -> (y'=max(y-1,0)) & (o'=2); // reached target
[east] started & !target -> (x'=min(x+1,N-1));
[west] started & !target -> (x'=max(x-1,0));
[north] started & !target -> (x'=min(y+1,N-1));
[south] started & !target -> (y'=max(y-1,0));
// reached target
[done] o=2 -> true;
[done] target -> true;
endmodule

63
prism-examples/pomdps/gridworld/4x4grid_bounded.prism
View File

@ -6,51 +6,48 @@
pomdp
const int N = 4; // grid size
const int K; // step bound in property
// only the target is observable which is in the south east corner
// (and the step bound)
observables
o, k
endobservables
// (also if the initialisation step has been done and the step count)
formula target = x=N-1 & y=0;
observable "target" = target;
observable "started" = started;
observable "k" = k;
module grid
x : [0..2]; // x coordinate
y : [0..2]; // y coordinate
o : [0..2]; // observables
// 0 - initial observation
// 1 - in the grid (not target)
// 2 - observe target
x : [0..N-1]; // x coordinate
y : [0..N-1]; // y coordinate
started : bool; // initialised?
// initially randomly placed within the grid (not at the target)
[] o=0 -> 1/15 : (o'=1) & (x'=0) & (y'=0)
+ 1/15 : (o'=1) & (x'=0) & (y'=1)
+ 1/15 : (o'=1) & (x'=0) & (y'=2)
+ 1/15 : (o'=1) & (x'=0) & (y'=3)
+ 1/15 : (o'=1) & (x'=1) & (y'=0)
+ 1/15 : (o'=1) & (x'=1) & (y'=1)
+ 1/15 : (o'=1) & (x'=1) & (y'=2)
+ 1/15 : (o'=1) & (x'=1) & (y'=3)
+ 1/15 : (o'=1) & (x'=2) & (y'=0)
+ 1/15 : (o'=1) & (x'=2) & (y'=1)
+ 1/15 : (o'=1) & (x'=2) & (y'=2)
+ 1/15 : (o'=1) & (x'=2) & (y'=3)
// + 1/15 : (o'=1) & (x'=3) & (y'=0) this is the traget
+ 1/15 : (o'=1) & (x'=3) & (y'=1)
+ 1/15 : (o'=1) & (x'=3) & (y'=2)
+ 1/15 : (o'=1) & (x'=3) & (y'=3);
[] !started -> 1/15 : (started'=true) & (x'=0) & (y'=0)
+ 1/15 : (started'=true) & (x'=0) & (y'=1)
+ 1/15 : (started'=true) & (x'=0) & (y'=2)
+ 1/15 : (started'=true) & (x'=0) & (y'=3)
+ 1/15 : (started'=true) & (x'=1) & (y'=0)
+ 1/15 : (started'=true) & (x'=1) & (y'=1)
+ 1/15 : (started'=true) & (x'=1) & (y'=2)
+ 1/15 : (started'=true) & (x'=1) & (y'=3)
+ 1/15 : (started'=true) & (x'=2) & (y'=0)
+ 1/15 : (started'=true) & (x'=2) & (y'=1)
+ 1/15 : (started'=true) & (x'=2) & (y'=2)
+ 1/15 : (started'=true) & (x'=2) & (y'=3)
// + 1/15 : (started'=true) & (x'=3) & (y'=0) the target
+ 1/15 : (started'=true) & (x'=3) & (y'=1)
+ 1/15 : (started'=true) & (x'=3) & (y'=2)
+ 1/15 : (started'=true) & (x'=3) & (y'=3);
// move around the grid
[east] o=1 & !(x=2 & y=0) -> (x'=min(x+1,3)); // not reached target
[east] o=1 & x=2 & y=0 -> (x'=min(x+1,3)) & (o'=2); // reached target
[west] o=1 -> (x'=max(x-1,0)); // not reached target
[north] o=1 -> (x'=min(y+1,3)); // reached target
[south] o=1 & !(x=3 & y=1) -> (y'=max(y-1,0)); // not reached target
[south] o=1 & x=3 & y=1 -> (y'=max(y-1,0)) & (o'=2); // reached target
[east] started & !target -> (x'=min(x+1,N-1));
[west] started & !target -> (x'=max(x-1,0));
[north] started & !target -> (x'=min(y+1,N-1));
[south] started & !target -> (y'=max(y-1,0));
// reached target
[done] o=2 -> true;
[done] target -> true;
endmodule

2
prism-examples/pomdps/gridworld/grid.props
View File

@ -1,2 +1,2 @@
// Minimum steps to reach goal
Rmin=? [ F o=2 ]
Rmin=? [ F "target" ]

2
prism-examples/pomdps/gridworld/grid_bounded.props
View File

@ -1,2 +1,2 @@
// Maximum probability to reach goal (for use with step bound property)
Pmax=? [ F o=2 ]
Pmax=? [ F "target" ]

117
prism-examples/pomdps/simple/maze.prism
View File

@ -15,86 +15,58 @@
pomdp
// can observe the walls and target
observables
o
endobservables
// o=0 - observation in initial state
// o=1 - west and north walls (s0)
// o=2 - north and south ways (s1 and s3)
// o=3 - north wall (s2)
// o=4 - east and north way (s4)
// o=5 - east and west walls (s5, s6 and s7)
// o=6 - east, west and south walls (s8 and s9)
// o=7 - the target (s10)
observable "west" = s=0|s=5|s=6|s=7|s=8|s=9|s=10; // wall to the west
observable "east" = s=4|s=5|s=6|s=7|s=8|s=9|s=10; // wall to the east
observable "north" = s=0|s=1|s=2|s=3|s=4; // wall to the north
observable "south" = s=1|s=3|s=8|s=9|s=10; // wall to the south
observable "target" = s=10; //target
module maze
s : [-1..10];
o : [0..7];
// initialisation
[] s=-1 -> 0.1 : (s'=0) & (o'=1)
+ 0.1 : (s'=1) & (o'=2)
+ 0.1 : (s'=2) & (o'=3)
+ 0.1 : (s'=3) & (o'=2)
+ 0.1 : (s'=4) & (o'=4)
+ 0.1 : (s'=5) & (o'=5)
+ 0.1 : (s'=6) & (o'=5)
+ 0.1 : (s'=7) & (o'=5)
+ 0.1 : (s'=8) & (o'=6)
+ 0.1 : (s'=9) & (o'=6);
[] s=-1 -> 0.1 : (s'=0)
+ 0.1 : (s'=1)
+ 0.1 : (s'=2)
+ 0.1 : (s'=3)
+ 0.1 : (s'=4)
+ 0.1 : (s'=5)
+ 0.1 : (s'=6)
+ 0.1 : (s'=7)
+ 0.1 : (s'=8)
+ 0.1 : (s'=9);
// moving around the maze
[east] s=0 -> (s'=1) & (o'=2);
[west] s=0 -> (s'=0);
[north] s=0 -> (s'=0);
[south] s=0 -> (s'=5) & (o'=5);
[east] s=1 -> (s'=2) & (o'=3);
[west] s=1 -> (s'=0) & (o'=1);
[north] s=1 -> (s'=1);
[south] s=1 -> (s'=1);
[east] s=2 -> (s'=3) & (o'=2);
[west] s=2 -> (s'=1) & (o'=2);
[north] s=2 -> (s'=2);
[south] s=2 -> (s'=6) & (o'=5);
[east] s=3 -> (s'=4) & (o'=4);
[west] s=3 -> (s'=2) & (o'=2);
[north] s=3 -> (s'=3);
[south] s=3 -> (s'=3);
[east] s=4 -> (s'=4);
[west] s=4 -> (s'=3) & (o'=2);
[north] s=4 -> (s'=4);
[south] s=4 -> (s'=7) & (o'=5);
[east] s=5 -> (s'=5);
[west] s=5 -> (s'=5);
[north] s=5 -> (s'=0) & (o'=1);
[south] s=5 -> (s'=8) & (o'=6);
[east] s=6 -> (s'=6);
[west] s=6 -> (s'=6);
[north] s=6 -> (s'=2) & (o'=3);
[south] s=6 -> (s'=10) & (o'=7);
[east] s=7 -> (s'=7);
[west] s=7 -> (s'=7);
[north] s=7 -> (s'=4) & (o'=4);
[south] s=7 -> (s'=9) & (o'=6);
[east] s=8 -> (s'=8);
[west] s=8 -> (s'=8);
[north] s=8 -> (s'=5) & (o'=5);
[south] s=8 -> (s'=8);
[east] s=9 -> (s'=9);
[west] s=9 -> (s'=9);
[north] s=9 -> (s'=7) & (o'=5);
[south] s=9 -> (s'=9);
[east] s=0 -> (s'=1);
[south] s=0 -> (s'=5);
[east] s=1 -> (s'=2);
[west] s=1 -> (s'=0);
[east] s=2 -> (s'=3);
[west] s=2 -> (s'=1);
[south] s=2 -> (s'=6);
[east] s=3 -> (s'=4);
[west] s=3 -> (s'=2);
[west] s=4 -> (s'=3);
[south] s=4 -> (s'=7);
[north] s=5 -> (s'=0);
[south] s=5 -> (s'=8);
[north] s=6 -> (s'=2);
[south] s=6 -> (s'=10);
[north] s=7 -> (s'=4);
[south] s=7 -> (s'=9);
[north] s=8 -> (s'=5);
[north] s=9 -> (s'=7);
// loop when we reach the target
[done] s=10 -> true;
@ -110,6 +82,3 @@ rewards
[south] true : 1;
endrewards
// target observation
label "target" = o=7;

121
prism-examples/pomdps/simple/maze2.prism
View File

@ -17,104 +17,70 @@
pomdp
// can observe the walls and target
observables
o
endobservables
// o=0 - observation in initial state
// o=1 - west and north walls (s0)
// o=2 - north and south ways (s1 and s3)
// o=3 - north wall (s2)
// o=4 - east and north way (s4)
// o=5 - east and west walls (s5, s6, s7, s8, s9 and s10)
// o=6 - east, west and south walls (s11 and s12)
// o=7 - the target (s13)
observable "west" = s=0|s=5|s=6|s=7|s=8|s=9|s=10|s=11|s=12|s=13; // wall to the west
observable "east" = s=4|s=5|s=6|s=7|s=8|s=9|s=10|s=10|s=11|s=12|s=13; // wall to the east
observable "north" = s=0|s=1|s=2|s=3|s=4; // wall to the north
observable "south" = s=1|s=3|s=11|s=12|s=13; // wall to the south
observable "target" = s=13; //target
module maze
s : [-1..13];
o : [0..7];
// initialisation
[] s=-1 -> 1/13 : (s'=0) & (o'=1)
+ 1/13 : (s'=1) & (o'=2)
+ 1/13 : (s'=2) & (o'=3)
+ 1/13 : (s'=3) & (o'=2)
+ 1/13 : (s'=4) & (o'=4)
+ 1/13 : (s'=5) & (o'=5)
+ 1/13 : (s'=6) & (o'=5)
+ 1/13 : (s'=7) & (o'=5)
+ 1/13 : (s'=8) & (o'=5)
+ 1/13 : (s'=9) & (o'=5)
+ 1/13 : (s'=10) & (o'=5)
+ 1/13 : (s'=11) & (o'=6)
+ 1/13 : (s'=12) & (o'=6);
[] s=-1 -> 1/13 : (s'=0)
+ 1/13 : (s'=1)
+ 1/13 : (s'=2)
+ 1/13 : (s'=3)
+ 1/13 : (s'=4)
+ 1/13 : (s'=5)
+ 1/13 : (s'=6)
+ 1/13 : (s'=7)
+ 1/13 : (s'=8)
+ 1/13 : (s'=9)
+ 1/13 : (s'=10)
+ 1/13 : (s'=11)
+ 1/13 : (s'=12);
// moving around the maze
[east] s=0 -> (s'=1) & (o'=2);
[west] s=0 -> (s'=0);
[north] s=0 -> (s'=0);
[south] s=0 -> (s'=5) & (o'=5);
[east] s=1 -> (s'=2) & (o'=3);
[west] s=1 -> (s'=0) & (o'=1);
[north] s=1 -> (s'=1);
[south] s=1 -> (s'=1);
[east] s=2 -> (s'=3) & (o'=2);
[west] s=2 -> (s'=1) & (o'=2);
[north] s=2 -> (s'=2);
[south] s=2 -> (s'=6) & (o'=5);
[east] s=3 -> (s'=4) & (o'=4);
[west] s=3 -> (s'=2) & (o'=2);
[north] s=3 -> (s'=3);
[south] s=3 -> (s'=3);
[east] s=4 -> (s'=4);
[west] s=4 -> (s'=3) & (o'=2);
[north] s=4 -> (s'=4);
[south] s=4 -> (s'=7) & (o'=5);
[east] s=5 -> (s'=5);
[west] s=5 -> (s'=5);
[north] s=5 -> (s'=0) & (o'=1);
[east] s=0 -> (s'=1);
[south] s=0 -> (s'=5);
[east] s=1 -> (s'=2);
[west] s=1 -> (s'=0);
[east] s=2 -> (s'=3);
[west] s=2 -> (s'=1);
[south] s=2 -> (s'=6);
[east] s=3 -> (s'=4);
[west] s=3 -> (s'=2);
[west] s=4 -> (s'=3);
[south] s=4 -> (s'=7);
[north] s=5 -> (s'=0);
[south] s=5 -> (s'=8);
[east] s=6 -> (s'=6);
[west] s=6 -> (s'=6);
[north] s=6 -> (s'=2) & (o'=3);
[north] s=6 -> (s'=2);
[south] s=6 -> (s'=9);
[east] s=7 -> (s'=7);
[west] s=7 -> (s'=7);
[north] s=7 -> (s'=4) & (o'=4);
[north] s=7 -> (s'=4);
[south] s=7 -> (s'=10);
[east] s=8 -> (s'=8);
[west] s=8 -> (s'=8);
[north] s=8 -> (s'=5);
[south] s=8 -> (s'=11) & (o'=6);
[south] s=8 -> (s'=11);
[east] s=9 -> (s'=9);
[west] s=9 -> (s'=9);
[north] s=9 -> (s'=6);
[south] s=9 -> (s'=13) & (o'=7);
[south] s=9 -> (s'=13);
[east] s=10 -> (s'=9);
[west] s=10 -> (s'=9);
[north] s=10 -> (s'=7);
[south] s=10 -> (s'=12) & (o'=6);
[south] s=10 -> (s'=12);
[east] s=11 -> (s'=11);
[west] s=11 -> (s'=11);
[north] s=11 -> (s'=8) & (o'=5);
[south] s=11 -> (s'=11);
[north] s=11 -> (s'=8);
[east] s=12 -> (s'=12);
[west] s=12 -> (s'=12);
[north] s=12 -> (s'=10) & (o'=5);
[south] s=12 -> (s'=12);
[north] s=12 -> (s'=10);
// loop when we reach the target
[done] s=13 -> true;
@ -130,6 +96,3 @@ rewards
[south] true : 1;
endrewards
// target observation
label "target" = o=7;

117
prism-tests/functionality/verify/pomdps/maze.prism
View File

@ -15,86 +15,58 @@
pomdp
// can observe the walls and target
observables
o
endobservables
// o=0 - observation in initial state
// o=1 - west and north walls (s0)
// o=2 - north and south ways (s1 and s3)
// o=3 - north wall (s2)
// o=4 - east and north way (s4)
// o=5 - east and west walls (s5, s6 and s7)
// o=6 - east, west and south walls (s8 and s9)
// o=7 - the target (s10)
observable "west" = s=0|s=5|s=6|s=7|s=8|s=9|s=10; // wall to the west
observable "east" = s=4|s=5|s=6|s=7|s=8|s=9|s=10; // wall to the east
observable "north" = s=0|s=1|s=2|s=3|s=4; // wall to the north
observable "south" = s=1|s=3|s=8|s=9|s=10; // wall to the south
observable "target" = s=10; //target
module maze
s : [-1..10];
o : [0..7];
// initialisation
[] s=-1 -> 0.1 : (s'=0) & (o'=1)
+ 0.1 : (s'=1) & (o'=2)
+ 0.1 : (s'=2) & (o'=3)
+ 0.1 : (s'=3) & (o'=2)
+ 0.1 : (s'=4) & (o'=4)
+ 0.1 : (s'=5) & (o'=5)
+ 0.1 : (s'=6) & (o'=5)
+ 0.1 : (s'=7) & (o'=5)
+ 0.1 : (s'=8) & (o'=6)
+ 0.1 : (s'=9) & (o'=6);
[] s=-1 -> 0.1 : (s'=0)
+ 0.1 : (s'=1)
+ 0.1 : (s'=2)
+ 0.1 : (s'=3)
+ 0.1 : (s'=4)
+ 0.1 : (s'=5)
+ 0.1 : (s'=6)
+ 0.1 : (s'=7)
+ 0.1 : (s'=8)
+ 0.1 : (s'=9);
// moving around the maze
[east] s=0 -> (s'=1) & (o'=2);
[west] s=0 -> (s'=0);
[north] s=0 -> (s'=0);
[south] s=0 -> (s'=5) & (o'=5);
[east] s=1 -> (s'=2) & (o'=3);
[west] s=1 -> (s'=0) & (o'=1);
[north] s=1 -> (s'=1);
[south] s=1 -> (s'=1);
[east] s=2 -> (s'=3) & (o'=2);
[west] s=2 -> (s'=1) & (o'=2);
[north] s=2 -> (s'=2);
[south] s=2 -> (s'=6) & (o'=5);
[east] s=3 -> (s'=4) & (o'=4);
[west] s=3 -> (s'=2) & (o'=2);
[north] s=3 -> (s'=3);
[south] s=3 -> (s'=3);
[east] s=4 -> (s'=4);
[west] s=4 -> (s'=3) & (o'=2);
[north] s=4 -> (s'=4);
[south] s=4 -> (s'=7) & (o'=5);
[east] s=5 -> (s'=5);
[west] s=5 -> (s'=5);
[north] s=5 -> (s'=0) & (o'=1);
[south] s=5 -> (s'=8) & (o'=6);
[east] s=6 -> (s'=6);
[west] s=6 -> (s'=6);
[north] s=6 -> (s'=2) & (o'=3);
[south] s=6 -> (s'=10) & (o'=7);
[east] s=7 -> (s'=7);
[west] s=7 -> (s'=7);
[north] s=7 -> (s'=4) & (o'=4);
[south] s=7 -> (s'=9) & (o'=6);
[east] s=8 -> (s'=8);
[west] s=8 -> (s'=8);
[north] s=8 -> (s'=5) & (o'=5);
[south] s=8 -> (s'=8);
[east] s=9 -> (s'=9);
[west] s=9 -> (s'=9);
[north] s=9 -> (s'=7) & (o'=5);
[south] s=9 -> (s'=9);
[east] s=0 -> (s'=1);
[south] s=0 -> (s'=5);
[east] s=1 -> (s'=2);
[west] s=1 -> (s'=0);
[east] s=2 -> (s'=3);
[west] s=2 -> (s'=1);
[south] s=2 -> (s'=6);
[east] s=3 -> (s'=4);
[west] s=3 -> (s'=2);
[west] s=4 -> (s'=3);
[south] s=4 -> (s'=7);
[north] s=5 -> (s'=0);
[south] s=5 -> (s'=8);
[north] s=6 -> (s'=2);
[south] s=6 -> (s'=10);
[north] s=7 -> (s'=4);
[south] s=7 -> (s'=9);
[north] s=8 -> (s'=5);
[north] s=9 -> (s'=7);
// loop when we reach the target
[done] s=10 -> true;
@ -110,6 +82,3 @@ rewards
[south] true : 1;
endrewards
// target observation
label "target" = o=7;

121
prism-tests/functionality/verify/pomdps/maze2.prism
View File

@ -17,104 +17,70 @@
pomdp
// can observe the walls and target
observables
o
endobservables
// o=0 - observation in initial state
// o=1 - west and north walls (s0)
// o=2 - north and south ways (s1 and s3)
// o=3 - north wall (s2)
// o=4 - east and north way (s4)
// o=5 - east and west walls (s5, s6, s7, s8, s9 and s10)
// o=6 - east, west and south walls (s11 and s12)
// o=7 - the target (s13)
observable "west" = s=0|s=5|s=6|s=7|s=8|s=9|s=10|s=11|s=12|s=13; // wall to the west
observable "east" = s=4|s=5|s=6|s=7|s=8|s=9|s=10|s=10|s=11|s=12|s=13; // wall to the east
observable "north" = s=0|s=1|s=2|s=3|s=4; // wall to the north
observable "south" = s=1|s=3|s=11|s=12|s=13; // wall to the south
observable "target" = s=13; //target
module maze
s : [-1..13];
o : [0..7];
// initialisation
[] s=-1 -> 1/13 : (s'=0) & (o'=1)
+ 1/13 : (s'=1) & (o'=2)
+ 1/13 : (s'=2) & (o'=3)
+ 1/13 : (s'=3) & (o'=2)
+ 1/13 : (s'=4) & (o'=4)
+ 1/13 : (s'=5) & (o'=5)
+ 1/13 : (s'=6) & (o'=5)
+ 1/13 : (s'=7) & (o'=5)
+ 1/13 : (s'=8) & (o'=5)
+ 1/13 : (s'=9) & (o'=5)
+ 1/13 : (s'=10) & (o'=5)
+ 1/13 : (s'=11) & (o'=6)
+ 1/13 : (s'=12) & (o'=6);
[] s=-1 -> 1/13 : (s'=0)
+ 1/13 : (s'=1)
+ 1/13 : (s'=2)
+ 1/13 : (s'=3)
+ 1/13 : (s'=4)
+ 1/13 : (s'=5)
+ 1/13 : (s'=6)
+ 1/13 : (s'=7)
+ 1/13 : (s'=8)
+ 1/13 : (s'=9)
+ 1/13 : (s'=10)
+ 1/13 : (s'=11)
+ 1/13 : (s'=12);
// moving around the maze
[east] s=0 -> (s'=1) & (o'=2);
[west] s=0 -> (s'=0);
[north] s=0 -> (s'=0);
[south] s=0 -> (s'=5) & (o'=5);
[east] s=1 -> (s'=2) & (o'=3);
[west] s=1 -> (s'=0) & (o'=1);
[north] s=1 -> (s'=1);
[south] s=1 -> (s'=1);
[east] s=2 -> (s'=3) & (o'=2);
[west] s=2 -> (s'=1) & (o'=2);
[north] s=2 -> (s'=2);
[south] s=2 -> (s'=6) & (o'=5);
[east] s=3 -> (s'=4) & (o'=4);
[west] s=3 -> (s'=2) & (o'=2);
[north] s=3 -> (s'=3);
[south] s=3 -> (s'=3);
[east] s=4 -> (s'=4);
[west] s=4 -> (s'=3) & (o'=2);
[north] s=4 -> (s'=4);
[south] s=4 -> (s'=7) & (o'=5);
[east] s=5 -> (s'=5);
[west] s=5 -> (s'=5);
[north] s=5 -> (s'=0) & (o'=1);
[east] s=0 -> (s'=1);
[south] s=0 -> (s'=5);
[east] s=1 -> (s'=2);
[west] s=1 -> (s'=0);
[east] s=2 -> (s'=3);
[west] s=2 -> (s'=1);
[south] s=2 -> (s'=6);
[east] s=3 -> (s'=4);
[west] s=3 -> (s'=2);
[west] s=4 -> (s'=3);
[south] s=4 -> (s'=7);
[north] s=5 -> (s'=0);
[south] s=5 -> (s'=8);
[east] s=6 -> (s'=6);
[west] s=6 -> (s'=6);
[north] s=6 -> (s'=2) & (o'=3);
[north] s=6 -> (s'=2);
[south] s=6 -> (s'=9);
[east] s=7 -> (s'=7);
[west] s=7 -> (s'=7);
[north] s=7 -> (s'=4) & (o'=4);
[north] s=7 -> (s'=4);
[south] s=7 -> (s'=10);
[east] s=8 -> (s'=8);
[west] s=8 -> (s'=8);
[north] s=8 -> (s'=5);
[south] s=8 -> (s'=11) & (o'=6);
[south] s=8 -> (s'=11);
[east] s=9 -> (s'=9);
[west] s=9 -> (s'=9);
[north] s=9 -> (s'=6);
[south] s=9 -> (s'=13) & (o'=7);
[south] s=9 -> (s'=13);
[east] s=10 -> (s'=9);
[west] s=10 -> (s'=9);
[north] s=10 -> (s'=7);
[south] s=10 -> (s'=12) & (o'=6);
[south] s=10 -> (s'=12);
[east] s=11 -> (s'=11);
[west] s=11 -> (s'=11);
[north] s=11 -> (s'=8) & (o'=5);
[south] s=11 -> (s'=11);
[north] s=11 -> (s'=8);
[east] s=12 -> (s'=12);
[west] s=12 -> (s'=12);
[north] s=12 -> (s'=10) & (o'=5);
[south] s=12 -> (s'=12);
[north] s=12 -> (s'=10);
// loop when we reach the target
[done] s=13 -> true;
@ -130,6 +96,3 @@ rewards
[south] true : 1;
endrewards
// target observation
label "target" = o=7;

2
prism-tests/functionality/verify/pomdps/maze2.prism.props
View File

@ -1,3 +1,3 @@
// Minimum expected number of steps to reach the target
// RESULT: [5.199999938461538,5.230769230769232] (grid resolution 20)
// RESULT: [5.69230763076923,5.692307692307692] (grid resolution 20)
Rmin=? [ F "target" ]

1
prism-tests/functionality/verify/pomdps/maze2.prism.props.args
View File

@ -0,0 +1 @@
-gridresolution 20
Write Preview
Loading…
Cancel
Save