diff --git a/prism/src/explicit/PartiallyObservableModel.java b/prism/src/explicit/PartiallyObservableModel.java index 644fd387..72dbc612 100644 --- a/prism/src/explicit/PartiallyObservableModel.java +++ b/prism/src/explicit/PartiallyObservableModel.java @@ -69,11 +69,43 @@ public interface PartiallyObservableModel extends Model */ public int getObservation(int s); + /** + * Get the observation of state {@code s} as a {@code State}. + * Equivalent to calling {@link #getObservation(int)} + * and then looking up via {@link #getObservationsList()}. + * Returns null if the observation is unavailable. + */ + public default State getObservationAsState(int s) + { + int o = getObservation(s); + List obsList = getObservationsList(); + if (obsList != null && obsList.size() > o) { + return obsList.get(o); + } + return null; + } + /** * Get the unobservation of state {@code s}. */ public int getUnobservation(int s); + /** + * Get the unobservation of state {@code s} as a {@code State}. + * Equivalent to calling {@link #getUnbservation(int)} + * and then looking up via {@link #getUnobservationsList()}. + * Returns null if the unobservation is unavailable. + */ + public default State getUnobservationAsState(int s) + { + int u = getUnobservation(s); + List unobsList = getUnobservationsList(); + if (unobsList != null && unobsList.size() > u) { + return unobsList.get(u); + } + return null; + } + /** * Get the probability of observing observation {@code o} in state {@code s}. */ diff --git a/prism/src/explicit/StateModelChecker.java b/prism/src/explicit/StateModelChecker.java index ef369af7..e6e2a1e5 100644 --- a/prism/src/explicit/StateModelChecker.java +++ b/prism/src/explicit/StateModelChecker.java @@ -909,8 +909,7 @@ public class StateModelChecker extends PrismComponent int numStates = model.getNumStates(); StateValues res = new StateValues(expr.getType(), model); for (int i = 0; i < numStates; i++) { - int iObservation = poModel.getObservation(i); - State observation = poModel.getObservationsList().get(iObservation); + State observation = poModel.getObservationAsState(i); Object val = observation.varValues[iObservable]; res.setValue(i, val); }