diff --git a/prism-examples/pomdps/gridworld/3x3grid.prism b/prism-examples/pomdps/gridworld/3x3grid.prism
index 6a34344e..27a1677b 100644
--- a/prism-examples/pomdps/gridworld/3x3grid.prism
+++ b/prism-examples/pomdps/gridworld/3x3grid.prism
@@ -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
 
diff --git a/prism-examples/pomdps/gridworld/3x3grid_bounded.prism b/prism-examples/pomdps/gridworld/3x3grid_bounded.prism
index 80665612..e465110e 100644
--- a/prism-examples/pomdps/gridworld/3x3grid_bounded.prism
+++ b/prism-examples/pomdps/gridworld/3x3grid_bounded.prism
@@ -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
diff --git a/prism-examples/pomdps/gridworld/4x4grid.prism b/prism-examples/pomdps/gridworld/4x4grid.prism
index 08f43fac..be1ca9a4 100644
--- a/prism-examples/pomdps/gridworld/4x4grid.prism
+++ b/prism-examples/pomdps/gridworld/4x4grid.prism
@@ -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
 
diff --git a/prism-examples/pomdps/gridworld/4x4grid_bounded.prism b/prism-examples/pomdps/gridworld/4x4grid_bounded.prism
index c1c0efc6..4c5ad5b8 100644
--- a/prism-examples/pomdps/gridworld/4x4grid_bounded.prism
+++ b/prism-examples/pomdps/gridworld/4x4grid_bounded.prism
@@ -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
 
diff --git a/prism-examples/pomdps/gridworld/grid.props b/prism-examples/pomdps/gridworld/grid.props
index 908b79e4..37f9e41c 100644
--- a/prism-examples/pomdps/gridworld/grid.props
+++ b/prism-examples/pomdps/gridworld/grid.props
@@ -1,2 +1,2 @@
 // Minimum steps to reach goal
-Rmin=? [ F o=2 ]
+Rmin=? [ F "target" ]
diff --git a/prism-examples/pomdps/gridworld/grid_bounded.props b/prism-examples/pomdps/gridworld/grid_bounded.props
index 28c12a74..b284f44b 100644
--- a/prism-examples/pomdps/gridworld/grid_bounded.props
+++ b/prism-examples/pomdps/gridworld/grid_bounded.props
@@ -1,2 +1,2 @@
 // Maximum probability to reach goal (for use with step bound property)
-Pmax=? [ F o=2 ]
+Pmax=? [ F "target" ]
diff --git a/prism-examples/pomdps/simple/maze.prism b/prism-examples/pomdps/simple/maze.prism
index 81cc2d5b..9f68874d 100644
--- a/prism-examples/pomdps/simple/maze.prism
+++ b/prism-examples/pomdps/simple/maze.prism
@@ -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;
diff --git a/prism-examples/pomdps/simple/maze2.prism b/prism-examples/pomdps/simple/maze2.prism
index b364fde7..d82fccb9 100644
--- a/prism-examples/pomdps/simple/maze2.prism
+++ b/prism-examples/pomdps/simple/maze2.prism
@@ -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;
\ No newline at end of file
diff --git a/prism-tests/functionality/verify/pomdps/maze.prism b/prism-tests/functionality/verify/pomdps/maze.prism
index 81cc2d5b..9f68874d 100644
--- a/prism-tests/functionality/verify/pomdps/maze.prism
+++ b/prism-tests/functionality/verify/pomdps/maze.prism
@@ -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;
diff --git a/prism-tests/functionality/verify/pomdps/maze2.prism b/prism-tests/functionality/verify/pomdps/maze2.prism
index b364fde7..d82fccb9 100644
--- a/prism-tests/functionality/verify/pomdps/maze2.prism
+++ b/prism-tests/functionality/verify/pomdps/maze2.prism
@@ -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;
\ No newline at end of file
diff --git a/prism-tests/functionality/verify/pomdps/maze2.prism.props b/prism-tests/functionality/verify/pomdps/maze2.prism.props
index 383c1e7f..f3b118f8 100644
--- a/prism-tests/functionality/verify/pomdps/maze2.prism.props
+++ b/prism-tests/functionality/verify/pomdps/maze2.prism.props
@@ -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" ]
diff --git a/prism-tests/functionality/verify/pomdps/maze2.prism.props.args b/prism-tests/functionality/verify/pomdps/maze2.prism.props.args
new file mode 100644
index 00000000..a993c4f8
--- /dev/null
+++ b/prism-tests/functionality/verify/pomdps/maze2.prism.props.args
@@ -0,0 +1 @@
+-gridresolution 20