Repository navigation
Allow import of models with rational/double values in either mode - #311
Merged
Merged
Conversation
Importing a model whose values are stored as doubles in exact mode, or as rationals in non-exact mode, now works, converting values as needed (see issue prismmodelchecker#309). Previously, a double-valued UMB file in exact mode failed with a ClassCastException, and a rational-valued UMB or text (e.g. .tra) file in non-exact mode gave "Cannot import an exact model unless in exact mode" or "invalid value", respectively. In exact mode, doubles are converted to rationals via their (shortest) decimal representation, e.g. 0.4 -> 2/5, matching how decimal values in text files are interpreted. In non-exact mode, rationals are converted to the closest double, as for rational expressions in PRISM models. For UMB files, the value type is determined separately for each part (probabilities, exit rates, each reward structure), which also fixes a ClassCastException when importing, in non-exact mode, a file with double-valued probabilities but rational rewards. Add regression tests.
Contributor
There was a problem hiding this comment.
🟢 Approval recommended
Static review identified no blocking issues in the focused conversion changes and regression fixtures; tests were not executed.
No open issues 🎉
What changed in this PR
This PR addresses #309 by allowing explicit model imports to convert between rational and double values instead of rejecting mismatched modes or failing with a cast error.
Changes:
- Decode UMB probabilities, exit rates, and rewards using each component’s stored type, converting to the requested evaluation mode.
- Accept rational strings in floating-point parsing and remove model-wide exactness restrictions.
- Add regression cases for exact, non-exact, mixed-type UMB, and rational text imports.
| File | Description |
|---|---|
prism/src/symbolic/build/ExplicitFiles2MTBDD.java |
Removes the symbolic builder’s rejection of rational imports. |
prism/src/prism/Evaluator.java |
Supports rational strings in double and interval parsing. |
prism/src/io/UMBImporter.java |
Converts values according to per-component UMB types. |
prism/src/io/ExplicitModelImporter.java |
Removes the model-wide exactness query. |
prism/src/explicit/ExplicitFiles2Model.java |
Removes the explicit builder’s exactness restriction. |
prism-tests/functionality/import/third.umb.auto |
Exercises rational, mixed-type, and text imports. |
prism-tests/functionality/import/third.pm.props |
Defines expected probability and reward results. |
prism-tests/functionality/import/third.pm.orig |
Supplies the source model for conversion fixtures. |
prism-tests/functionality/import/third.exact.trew |
Adds rational transition rewards. |
prism-tests/functionality/import/third.exact.tra |
Adds rational transition probabilities. |
prism-tests/functionality/import/third.exact.sta |
Adds state definitions for text imports. |
prism-tests/functionality/import/third.exact.srew |
Adds rational state rewards. |
prism-tests/functionality/import/third.exact.lab |
Adds labels for the regression model. |
prism-tests/functionality/import/dice.umb.exact.auto |
Exercises double-valued UMB imports in exact mode. |
Review effort: Balanced
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.
Importing a model whose values are stored as doubles in exact mode, or as rationals in non-exact mode, now works, with values converted as needed.
Previously:
ClassCastException;.tra) in non-exact mode gave "invalid value".Conversions:
For UMB files, the value type is now determined separately for each part (probabilities, exit rates, each reward structure). This also fixes a
ClassCastExceptionwhen importing, in non-exact mode, a file with double-valued probabilities but rational rewards.Includes regression tests in
prism-tests/functionality/import(dice.umb.exact.auto,third.umb.auto).Fixes #309.