diff --git a/prism/src/explicit/POMDPModelChecker.java b/prism/src/explicit/POMDPModelChecker.java index 02eb47b5..e74d0f13 100644 --- a/prism/src/explicit/POMDPModelChecker.java +++ b/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 targetObservs = getTargetObservations(pomdp, target); + LinkedList targetObservs = getAndCheckTargetObservations(pomdp, target); // Initialise the grid points ArrayList 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 targetObservs = getTargetObservations(pomdp, target); + LinkedList targetObservs = getAndCheckTargetObservations(pomdp, target); // Initialise the grid points ArrayList gridPoints = new ArrayList<>();//the set of grid points (discretized believes) @@ -444,13 +444,32 @@ public class POMDPModelChecker extends ProbModelChecker return res; } - protected LinkedList 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 getAndCheckTargetObservations(POMDP pomdp, BitSet target) throws PrismException { + // Find observations corresponding to each state in the target TreeSet 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 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; } diff --git a/prism/src/pta/DigitalClocks.java b/prism/src/pta/DigitalClocks.java index 62824781..e48a4605 100644 --- a/prism/src/pta/DigitalClocks.java +++ b/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 diff --git a/prism/tests/pomdps/nonobs-target.prism b/prism/tests/pomdps/nonobs-target.prism new file mode 100644 index 00000000..9e10c2e8 --- /dev/null +++ b/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 diff --git a/prism/tests/pomdps/nonobs-target.prism.props b/prism/tests/pomdps/nonobs-target.prism.props new file mode 100644 index 00000000..a9ded268 --- /dev/null +++ b/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 ]; diff --git a/prism/tests/pomdps/nonobs-target.prism.props.args b/prism/tests/pomdps/nonobs-target.prism.props.args new file mode 100644 index 00000000..7dfe0c2e --- /dev/null +++ b/prism/tests/pomdps/nonobs-target.prism.props.args @@ -0,0 +1 @@ +-gridresolution 50