deduplicate same choices when building an explicit quotient. - #991
deduplicate same choices when building an explicit quotient.#991sjunges wants to merge 3 commits into
Conversation
… easier to ensure bisim and dd-to-bisim coincide, makes the MDP a bit smaller, and doesnt cost much
| for (uint64_t i = 0; i < rowPermutation.size(); ++i) { | ||
| uint64_t const rowIdx = rowPermutation[i]; | ||
| bool const isDuplicate = | ||
| i > 0 && rowToState[rowPermutation[i - 1]] == rowToState[rowIdx] && matrixEntries[rowPermutation[i - 1]] == matrixEntries[rowIdx]; |
There was a problem hiding this comment.
Does this distinguish choices with different rewards but equal transition probabilities?
There was a problem hiding this comment.
Pull request overview
This PR addresses a mismatch between DD-based bisimulation quotient extraction and the sparse engine by deduplicating redundant nondeterministic choices when extracting a sparse quotient from a symbolic (DD) bisimulation, and adds a regression test tied to issue #91.
Changes:
- Deduplicate identical MDP choices during DD→sparse quotient extraction to reduce gratuitous quotient size.
- Adjust state-action vector extraction to respect the (potentially shortened) row permutation after choice deduplication.
- Add a regression test asserting expected state/transition/choice counts for a representative MDP case.
Reviewed changes
Copilot reviewed 2 out of 2 changed files in this pull request and generated 2 comments.
| File | Description |
|---|---|
| src/test/storm/storage/SymbolicBisimulationDecompositionTest.cpp | Adds regression coverage for DD→sparse quotient choice deduplication (issue #91). |
| src/storm/storage/dd/bisimulation/QuotientExtractor.cpp | Implements deduplication of redundant nondeterministic choices and aligns vector reordering/matrix sizing with the reduced row set. |
💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.
| InternalSparseQuotientExtractor<DdType, ValueType, ExportValueType> sparseExtractor(model, partitionAsBdd, partition.getBlockVariable(), | ||
| partition.getNumberOfBlocks(), representatives); | ||
|
|
||
| // Collect the state-action rewards of the preserved reward models upfront, so that the extraction of the |
There was a problem hiding this comment.
Is this reused later? Where were these rewards previously collected?
|
Here something went wrong during the merge with upstream changes. |
Makes it easier to ensure bisim and dd-to-bisim coincide, makes the MDP a bit smaller, and doesnt cost much.
Relates to #91; this is only part of the solution, the main 'problem' lies on the sparse bisim side.