Repository navigation
Fix slow model checking of imported POMDPs (unobservations) - #312
Merged
Merged
Conversation
For POMDPs built from imported files, each state was its own "unobservation", rather than (as for models built from PRISM models) the values of its non-observable variables. Since beliefs are stored over unobservations, this made them as large as the state space, and model checking could be orders of magnitude slower (e.g. 2s -> >150s). Now, unobservations are derived from the variables that are not observable, provided that, with observations, they still identify states uniquely (otherwise, the previous behaviour is kept). Add PartiallyObservableModel.setUnobservation(int, int).
A variable is taken to be observable if there is an observable with the same name. Previously, the default (no variables observable) was used, e.g. for imported models. Use this when computing unobservations for imported POMDPs, as is done for models built from PRISM models.
Contributor
There was a problem hiding this comment.
🟡 Changes recommended
Regression coverage is needed to verify reduced belief storage, preserved state mappings, and correct collision fallback.
1 open issue
What changed in this PR
This PR reduces belief storage for imported POMDPs by deriving unobservations from non-observable variables, bringing imports closer to models built directly from PRISM files.
Changes:
- Identify observable variables by matching variable and observable names.
- Compact unobservations when observation/unobservation pairs uniquely identify states; otherwise retain state-index mappings.
- Add unobservation setters to the partially observable model interface and implementations.
| File | Description |
|---|---|
prism/src/prism/BasicModelInfo.java |
Determine variable observability by name. |
prism/src/explicit/POMDPSimple.java |
Delegate unobservation assignments to observation storage. |
prism/src/explicit/PartiallyObservableModel.java |
Add the unobservation assignment interface method. |
prism/src/explicit/IPOMDPSimple.java |
Forward unobservation assignments to the underlying POMDP. |
prism/src/explicit/ExplicitFiles2Model.java |
Compute compact unobservations with a uniqueness fallback. |
Review effort: Balanced
"make unittests" ran JUnit with only the classes directory on the classpath, so tests could not use code that needs the libraries in lib (e.g. model import, which uses commons-compress). Now the same classpath as for compilation is used, and only the classes directory is scanned for tests. Also update the single-test command in CLAUDE.md.
For a small POMDP, imported from explicit files and from UMB, check that unobservations are the values of the non-observable variables, that (observation, unobservation) pairs identify states uniquely, and that point beliefs map back to the right states; also that, when they would not identify states uniquely, each state is its own unobservation.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
For POMDPs built from imported files (UMB or explicit files), each state was its own "unobservation", rather than (as for models built from PRISM models) the values of its non-observable variables. Beliefs are stored over unobservations, so this made them as large as the state space, and model checking could be orders of magnitude slower.
Now, unobservations for imported POMDPs are derived from the variables that are not observable, provided that, with observations, they still identify states uniquely (otherwise, the previous behaviour is kept). The belief code only relies on states mapping to distinct (observation, unobservation) pairs, so results are unchanged.
Also,
BasicModelInfo.isVarObservable()is now implemented (a variable is observable if there is an observable with the same name), rather than using the default (no variables observable), and is used for the above.Example (
prism-examples/pomdps/crypt/crypt3.prism,-gridresolution 8,Pmax=? [ F correct=1 ]), exported to UMB/explicit files and imported: