Add check that POMDP property targets are observations.

prism/src/explicit/POMDPModelChecker.java

@@ -117,7 +117,7 @@ public class POMDPModelChecker extends ProbModelChecker
 		mainLog.println("Starting fixed-resolution grid approximation (" + (min ? "min" : "max") + ")...");
 
 		// Find out the observations for the target states
-		LinkedList<Integer> targetObservs = getTargetObservations(pomdp, target);
+		LinkedList<Integer> targetObservs = getAndCheckTargetObservations(pomdp, target);
 		
 		// Initialise the grid points
 		ArrayList<Belief> gridPoints = new ArrayList<>();//the set of grid points (discretized believes)
@@ -301,7 +301,7 @@ public class POMDPModelChecker extends ProbModelChecker
 		mainLog.println("Starting fixed-resolution grid approximation (" + (min ? "min" : "max") + ")...");
 
 		// Find out the observations for the target states
-		LinkedList<Integer> targetObservs = getTargetObservations(pomdp, target);
+		LinkedList<Integer> targetObservs = getAndCheckTargetObservations(pomdp, target);
 
 		// Initialise the grid points
 		ArrayList<Belief> gridPoints = new ArrayList<>();//the set of grid points (discretized believes)
@@ -444,13 +444,32 @@ public class POMDPModelChecker extends ProbModelChecker
 		return res;
 	}
 
-	protected LinkedList<Integer> getTargetObservations(POMDP pomdp, BitSet target)
+	/**
+	 * Get a list of target observations from a set of target states
+	 * (both are represented by their indices).
+	 * Also check that the set of target states corresponds to a set
+	 * of observations, and throw an exception if not.
+	 */
+	protected LinkedList<Integer> getAndCheckTargetObservations(POMDP pomdp, BitSet target) throws PrismException
 	{
+		// Find observations corresponding to each state in the target
 		TreeSet<Integer> targetObservsSet = new TreeSet<>();
-		for (int bit = target.nextSetBit(0); bit >= 0; bit = target.nextSetBit(bit + 1)) {
-			targetObservsSet.add(pomdp.getObservation(bit));
+		for (int s = target.nextSetBit(0); s >= 0; s = target.nextSetBit(s + 1)) {
+			targetObservsSet.add(pomdp.getObservation(s));
 		}
 		LinkedList<Integer> targetObservs = new LinkedList<>(targetObservsSet);
+		// Rereate the set of target states from the target observations
+		// and make sure it matches
+		BitSet target2 = new BitSet();
+		int numStates = pomdp.getNumStates();
+		for (int s = 0; s < numStates; s++) {
+			if (targetObservs.contains(pomdp.getObservation(s))) {
+				target2.set(s);
+			}
+		}
+		if (!target.equals(target2)) {
+			throw new PrismException("Target is not observable");
+		}
 		return targetObservs;
 	}
 	

prism/src/pta/DigitalClocks.java

@@ -367,6 +367,10 @@ public class DigitalClocks
 			timerModule.addCommand(timeCommand);
 			// Finally add module to model
 			mf.addModule(timerModule);
+			// For POPTAs, the variable needs to be observable
+			if (modulesFile.getModelType().partiallyObservable()) {
+				mf.addObservableVar(timerVarName);
+			}
 			
 			// Then modify the property
 			

prism/tests/pomdps/nonobs-target.prism

@@ -0,0 +1,16 @@
+pomdp
+
+observables o endobservables
+
+module M
+
+	s : [0..10];
+	o : [0..3];
+	
+	[] s=0 -> 0.5:(s'=1)&(o'=1) + 0.5:(s'=2)&(o'=1);
+	[g1] o=1 -> (o'=(s=1)?2:3);
+	[g2] o=1 -> (o'=(s=2)?2:3);
+//	[] s=3 -> 0.5:(s'=4) + 0.5:(s'=5);
+	[] o>=2 -> true;
+		
+endmodule

prism/tests/pomdps/nonobs-target.prism.props

@@ -0,0 +1,5 @@
+// RESULT: 0.5
+Pmax=? [ F o=2 ];
+
+// RESULT: Error observable
+Pmax=? [ F o>=2&s=2 ];

prism/tests/pomdps/nonobs-target.prism.props.args

@@ -0,0 +1 @@
+-gridresolution 50