engine: static validation — unreachable states & dead branches (SPEC §2)#44
Merged
Conversation
collect_errors now rejects (a) any declared state unreachable from the root's initial (conservative, guard-agnostic reachability over initial/region-initial/ on_events/after/choice targets; entering a state implies its ancestors), and (b) a guarded transition list or choice whose unguarded default branch is not last (later branches dead). Wired into CLI validate + the conformance static mode. Verified zero false positives across all 28 conformance definitions + examples. Two unit fixtures had genuinely unreachable states — made them reachable. Bump 0.0.3. Closes #42.
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.
Closes #42. Implements fruwehq/harel#34 (§2); cases fruwehq/harel-conformance#11.
What
collect_errorscomputes reachability from the root'sinitialover everyinitial/region-initial/on_events/after/choicetarget (conservative, guard-agnostic; entering a state implies its ancestors, whose edges are then also followed) and flags any declared state (≠top) that nothing can reach.choicewith an unguarded default branch that isn't last (later branches can never be selected). Generalizes the choiceelse-last rule.validate+ the conformancestaticmode. Bumps to 0.0.3 (so the fetch picks up cases 26–28 onmain).Verify
examples/*(verified before/after).tests/test_static_validation.py(6 tests: unreachable, composite-initial-only OK, deep-target ancestors, orthogonal regions, dead branch, unguarded-last OK). Two existing fixtures (test_model,test_validator) had genuinely unreachable states → made reachable. 138 unit, ruff + mypy clean.Note: 0.0.3 material (with submachines next); tag v0.0.3 once both land.