Repository navigation
UMB export performance improvements - #308
Merged
Merged
Conversation
Compression dominated export time with the default gzip level (6). Level 1 is several times faster on typical model data, for files only slightly larger (e.g. 6-8x faster, 4-10% larger on consensus and kanban models).
Setters now write (part of) a byte at a time, rather than looping over individual bits, mirroring the earlier change to the getters.
Check the setters against a bit-by-bit reference, including that bits outside the portion being set are left unchanged.
String data is written as UTF-8, but the offsets were computed using the platform default charset, so could be wrong for non-ASCII strings (e.g., action names) on platforms where the default is not UTF-8.
…o a file When exporting UMB in text mode to a file (rather than a PrismLog), the text was written but the export then fell through to a binary export, overwriting the same file. (Not reachable from the command line, which routes text-mode exports via a PrismLog.)
…overhead Look up each variable's types, offset and size once, rather than for every value of every valuation, and write values directly to the bit string. Also use a plain iterator over the states rather than a stream.
DTMCSparse and MDPSparse store transitions in the same sparse matrix form as UMB, so add getSparseTransitions() to give (read-only) access to the underlying arrays, as IOUtils.SparseMCTransitions/ SparseMDPTransitions (as used for import), and have ModelAccess iterate over these directly for offsets, successors and probabilities. This avoids creating a Map.Entry with a boxed probability for each transition, on each pass over the transitions.
The default implementations sum the counts over all states, but models already store (or compute) the totals, so use these instead.
… DTMC Successors were extracted from the embedded DTMC transitions, which compute each state's exit rate and divide each rate by it, only for the probabilities to be discarded. Take them directly from CTMCSimple.
Contributor
There was a problem hiding this comment.
🟢 Approval recommended
The optimizations preserve existing representations and are supported by targeted and broad export testing.
0 open findings
What changed in this PR
Improves UMB export performance while fixing text export and UTF-8 string offsets.
Changes:
- Accelerates gzip compression and bit-packed valuation encoding.
- Exports sparse and CTMC transitions more efficiently.
- Prevents binary overwrite after text export and corrects UTF-8 offsets.
| File | Description |
|---|---|
prism/unit-tests/io/github/pmctools/umbj/UMBBitStringTest.java |
Tests optimized bit setters. |
prism/src/io/UMBExporter.java |
Optimizes valuations and fixes text export. |
prism/src/io/ModelAccess.java |
Adds optimized transition access. |
prism/src/io/github/pmctools/umbj/UMBWriter.java |
Uses faster gzip and UTF-8 offsets. |
prism/src/io/github/pmctools/umbj/UMBFormat.java |
Defines gzip compression level. |
prism/src/io/github/pmctools/umbj/UMBBitString.java |
Writes values byte-wise. |
prism/src/explicit/MDPSparse.java |
Exposes sparse MDP transitions. |
prism/src/explicit/DTMCSparse.java |
Exposes sparse DTMC transitions. |
🧠 Review effort: Balanced
💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.
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.
Performance improvements for UMB model export, plus two small fixes. Follows #306 (import).
1. Faster gzip compression (
umbj: UMBWriter).Profiling showed 75–85% of export time was spent in gzip (
Deflater.deflate) at the default level (6). New default is level 1 (UMBFormat.GZIP_COMPRESSION_LEVEL): 6–8x faster compression, for files 4–10% larger on the models below. xz is unchanged.2. Faster encoding of state/observation valuations.
umbj: UMBBitString: store values using whole bytes rather than single bits (mirrors the earlier change to the getters), plus a unit test against a bit-by-bit reference.UMBExporter: look up each variable's type/offset/size once, not per value, and avoid a stream.3. Transitions directly from sparse storage.
DTMCSparse/MDPSparsegetgetSparseTransitions(), giving read-only access to their arrays asIOUtils.SparseMCTransitions/SparseMDPTransitions(the structs used for import).ModelAccessiterates these directly for offsets, successors and probabilities, avoiding aMap.Entrywith a boxed probability per transition on each pass. Also: total choice/transition counts are taken from the model rather than summed over states.4. CTMC successors without the embedded DTMC.
Successors were taken from the embedded DTMC transitions, computing exit rates and dividing every rate only to discard the result.
Fixes
umbj: UMBWriter: string offsets were computed with the platform default charset, but strings are written as UTF-8 (wrong offsets for non-ASCII action names on non-UTF-8 platforms).UMBExporter: a text-mode export to aFilefell through to a binary export, overwriting the file (not reachable from the command line).Results (default export settings, i.e., gzipped):
The remaining CTMC cost is mainly computing the embedded probabilities from
CTMCSimpleandActionList.actionIndexlookups; improving those would need new primitive accessors in the model classes, so is left for now.Testing
masterand this branch compared (binary contents and.umbt, ignoring timestamps): identical for 24 cases covering DTMC, CTMC, MDP, POMDP, IDTMC, IMDP and LTS; exact models; negative/bool/int variables; state/branch/choice rewards; labels; observations; and models re-exported after UMB import.prism-testonfunctionality/exportandfunctionality/import: 1673 passed, 0 failures.