SCC and EC computation optimisations#281
Merged
Merged
Conversation
…ion. Replace the recursive tarjan(int) implementation with an iterative one using an explicit frame stack, eliminating StackOverflowError risk on large models. Replace ArrayList<Node> and LinkedList<Integer> with primitive int[] arrays, cutting per-state overhead from ~96 bytes to ~8 bytes (nodeIndex[] + lowlink[]).
processedSCCs was a field, so it accumulated every processed E BitSet for the lifetime of the ECComputerDefault object. Make processedSCCs a local variable in findEndComponents so it is eligible for GC as soon as the method returns, and pass it explicitly to canLBeChanged.
SubNondetModel previously stored three HashMap<Integer,X> lookup tables (stateLookupTable, inverseStateLookupTable, actionLookupTable) that carried ~64 bytes of boxing overhead per entry. Replace with primitive arrays (subToOrig int[], origToSub int[], subActionToOrig int[][]) that use 4 bytes per entry. Merge the separate generateStatistics() and generateLookupTable() passes into a single init() method, and drop the actions Map<Integer,BitSet> field so the caller's map is eligible for GC immediately after the SubNondetModel constructor returns. Cache the state count so getNumStates() no longer scans the BitSet every call. ECComputerDefault.restrict() now iterates only over states present in the current subset (nextSetBit loop) rather than scanning the entire original model, and skips storing empty-action BitSets that will be discarded anyway.
…C detection Replace the convergence-detection loop (which accumulated a HashSet of every candidate BitSet seen, one per algorithm iteration) with a direct termination condition: a candidate E is an MEC iff restrict() removes no states AND the restricted submodel is a single strongly-connected component covering all of those states. When that condition holds, E is added directly to the result list; otherwise its SCCs are queued for further refinement. This removes the O(iterations × stateSpace) memory cost of processedSCCs as well as the now-redundant canLBeChanged, replaceEWithSCCs, isMEC helpers.
The previous algorithm placed all SCCs returned by one Tarjan pass into the worklist L simultaneously. Replace the flat worklist loop with a streaming approach: as Tarjan emits each SCC via notifyEndSCC/notifyDone, immediately recurse into it (findMECsStreaming) rather than adding it to L. Recursion uses the SubNondetModel directly as the model for child calls, so inner SCC computations operate on a compact re-indexed state space. At any moment only one SCC per recursion level is live, reducing peak heap use to O(depth × stateSpaceSize). Also adds throws PrismException to SCCConsumer.notifyDone() so the streaming callback can propagate errors without wrapping.
The streaming SCC fix prevented accumulating SCCs in the worklist, but findEndComponents still collected all confirmed MECs into a List<BitSet> before returning. Add MECConsumer (package-private @FunctionalInterface in ECComputer.java) and ECComputer.computeMECStatesStreaming(MECConsumer) so callers can process each MEC as it is found without accumulation. ECComputerDefault overrides this to call findMECsStreaming directly, bypassing the list entirely. Modify MDPModelChecker.computeTotalRewardsMax to use computeMECStatesStreaming: each MEC is inspected for positive rewards, OR'd into positiveECs if positive, then immediately eligible for GC. Peak memory for EC precomputation is now O(depth x stateSpaceSize).
…location. For singleton SCCs in the streaming EC consumer, check directly whether the single state has a self-loop action (isSingletonMEC) instead of recursing into findMECsStreaming. The recursive path allocated a SubNondetModel with an origToSub[parentSize] per singleton, so O(numSingletonMECs) such allocations accumulated as GC pressure. The new path is O(choices) with no heap allocation for the common singleton case.
Contributor
There was a problem hiding this comment.
Pull request overview
This PR optimises SCC (BSCC) and EC/MEC computation in both the explicit and symbolic engines, focusing on reducing allocations/peak memory (especially for many small SCCs/MECs) and adding lightweight timing instrumentation.
Changes:
- Add
StopWatchtiming around BSCC/MEC computations across several model checkers. - Rework explicit Tarjan SCC computation to an iterative, array-based implementation to reduce recursion risk and allocations.
- Introduce streaming MEC enumeration (callback-based) in the explicit EC computation to avoid accumulating all MEC BitSets at once; refactor
SubNondetModelto use compact lookup arrays instead of hash maps.
Reviewed changes
Copilot reviewed 10 out of 10 changed files in this pull request and generated 2 comments.
Show a summary per file
| File | Description |
|---|---|
| prism/src/symbolic/comp/ProbModelChecker.java | Adds timing around BSCC computation in steady-state/reward routines. |
| prism/src/symbolic/comp/NondetModelChecker.java | Adds timing around MEC computation in reward routines. |
| prism/src/explicit/SubNondetModel.java | Replaces map-based translation tables with primitive arrays; avoids retaining the actions map post-construction. |
| prism/src/explicit/SCCConsumer.java | Allows notifyDone() to throw PrismException for streaming consumers that may fail. |
| prism/src/explicit/SCCComputerTarjan.java | Reimplements Tarjan SCC using an explicit (iterative) DFS and primitive arrays. |
| prism/src/explicit/MDPModelChecker.java | Switches one MEC-processing use case to streaming enumeration; adds MEC timing. |
| prism/src/explicit/LTLModelChecker.java | Adds timing around BSCC/MEC computations in LTL acceptance routines. |
| prism/src/explicit/ECComputerDefault.java | Implements streaming MEC discovery to reduce peak memory; optimises restrict iteration. |
| prism/src/explicit/ECComputer.java | Adds MEC streaming API entry point (computeMECStatesStreaming). |
| prism/src/explicit/DTMCModelChecker.java | Adds timing around BSCC computations in reward and steady-state routines. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
| // If v is the root of an SCC, pop the SCC from the Tarjan stack | ||
| if (lowlink[v] == nodeIndex[v]) { | ||
| boolean singletonSCC = (tarjanStack[tarjanStackTop - 1] == v); | ||
| if (singletonSCC && filterTrivialSCCs && !frameHadSelfloop[frameTop]) { |
Comment on lines
+35
to
+41
| /** | ||
| * Functional interface for consuming MECs one at a time, allowing PrismException. | ||
| */ | ||
| @FunctionalInterface | ||
| interface MECConsumer { | ||
| void accept(BitSet mec) throws PrismException; | ||
| } |
(Copilot bug report in prismmodelchecker#281 seems to be a false positive)
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.
Optimise code and remove memory leaks in SCC/EC computation
code in explicit engine, including case of many small/trivial SCC/ECs.