RLTL model checking support - #20
Draft
Immad (imnaseer) wants to merge 6 commits into
Draft
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>
Reconstruct the RLTL/model-checking work on top of the refined lazy state-graph branch (itself based on current main) so the lazy state-graph implementation lives in exactly one place and is consumed here rather than duplicated: - Add the Accordant.ModelChecking and Accordant.ModelChecking.Bdd projects, the model-checking test suite, the concurrency samples (AlternatingBit, DiningPhilosophers, Paxos, Peterson, TerminationDetection) and the Accordant.slnx solution. - Model checking consumes lazy (on-the-fly) exploration via StateGraph.ExploreStateGraph(..., lazy: true); the checkers walk the graph through Edges so it materializes only as far as the emptiness search needs. - Package Accordant.ModelChecking in the Microsoft.Accordant NuGet package. The lazy state-graph core (StateGraph, StateGraphExpander, SystemChecker and the eager/lazy equivalence + path tests) is inherited unchanged from the lazy-state-graph branch, not re-introduced here. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Immad (imnaseer)
force-pushed
the
personal/imnaseer/rltl-port
branch
from
August 5, 2026 22:03
d7099a6 to
b1c8176
Compare
Extend atomic propositions from p(state) to optionally observe the transition: p(state, action, state'). Adds Observe overloads for (s), (s, s'), and (s, a, s'), a reserved stutter action for self-loops, and enriches the atom eval interface with a transition context. The automata/SAT core is untouched; only the three product evaluators gained per-node transition-awareness detection and per-edge evaluation, with a byte-identical source-anchored fast path for state-only formulas. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
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
1 participant
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.
No description provided.