Add lazy (on-the-fly) state-graph construction with a unified eager/l… - #34
Merged
Merged
Conversation
…azy driver Introduces an optional lazy exploration mode for StateGraph.ExploreStateGraph so consumers (e.g. model checking) can build the reachable graph on demand and stop at the first counterexample without materializing a huge — possibly intractable — graph up front. Rather than duplicate the traversal, both eager and lazy exploration are driven by a single StateGraphExpander: * Successor generation is factored into one path-independent kernel (StateGraph.GenerateSuccessors); constraint filtering, depth bounding, node interning, edge de-duplication and pre/post hooks all live in the shared ExpandNode. * The eager driver walks a worklist and stores each node's edges up front; the lazy driver expands a node the first time its Edges are accessed (StateGraphNode.EnsureExpanded). Eager nodes carry no back-reference to the expander so they never self-recompute. * The root->node traversal path and the discovery depth are both read from the node itself, reconstructed from per-node discovery back-pointers (DiscoveredFrom/DiscoveredVia). The path is flattened at most once and memoized (StateGraphNode.Path), and shared structurally across descendants. Consequently a given node is expanded with an identical path and depth in either mode, and neither driver has to thread that context. Adds base-project tests: LazyEagerEquivalenceTests (randomized graphs assert eager and lazy produce identical unbounded graphs / hooks, and that bounded graphs are subgraphs of the unbounded one) and StateGraphPathTests (eager and lazy hand each node the identical, well-formed, prefix-closed path, and the reconstructed path is memoized). Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Clarify the subtle eager/lazy expansion contract on StateGraphNode: - Rename the node's Expander property to LazyExpander, documenting that null means eager (edges pre-computed and stored by the worklist) and non-null means lazy (edges materialize on first access). - Remove the ComputeEdges wrapper so EnsureExpanded calls ExpandNode directly, eliminating a layer of indirection. - Add an explicit, Release-surviving guard in SetExpandedEdges that throws if a lazy-bound node is expanded eagerly, making the previously implicit invariant fail loudly instead of silently re-expanding with an empty path. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Broaden the property-based coverage of state-graph construction: - Widen the randomized model generator (up to 3 dimensions, bound 4, and 5 step functions) and raise the seed count to 400, exercising larger and more varied graphs across every property test. - Add an eager-determinism test asserting repeated eager runs of the same model produce identical node sets, edge sets, and hooked node sets. - Add a generateStateGraph:false hook-parity test asserting the memory-lean eager traversal (the SystemChecker mode, which retains no edges and returns no root) still fires its pre- and post-hooks on exactly the same node set as the full eager graph. These guard the eager-only risk surface on this branch, which has no production lazy consumer. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
- Reword the LazyEagerEquivalenceTests summary to describe the eager-only invariants without referring to the branch or production state, which does not belong in a long-lived code comment. - Bump the package version from 0.1.6 to 0.1.7 in Directory.Build.props and both NuGet nuspec files. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Margus Veanes (veanes)
approved these changes
Aug 5, 2026
Margus Veanes (veanes)
left a comment
Margus Veanes (veanes)
left a comment
Collaborator
There was a problem hiding this comment.
Overall, changes look reasonable to me. I'm assuming each node has a bounded out-degree, but that is a priory not known. When a lazy node has been fully expanded it is then "essentially eager" or fully expanded but remains lazy. Not sure if lazy vs eager is the ideal terminology but is ok.
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
2 participants
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.
…azy driver
Introduces an optional lazy exploration mode for StateGraph.ExploreStateGraph so consumers (e.g. model checking) can build the reachable graph on demand and stop at the first counterexample without materializing a huge — possibly intractable — graph up front.
Rather than duplicate the traversal, both eager and lazy exploration are driven by a single StateGraphExpander:
Adds base-project tests: LazyEagerEquivalenceTests (randomized graphs assert eager and lazy produce identical unbounded graphs / hooks, and that bounded graphs are subgraphs of the unbounded one) and StateGraphPathTests (eager and lazy hand each node the identical, well-formed, prefix-closed path, and the reconstructed path is memoized).