feat(math): add Petri net siphon/trap check operation (#1908) - #2143
Conversation
Add bounded exact place/transition Petri net operations: - Enabled transition detection (pre-condition satisfaction) - Single transition firing with marking update - Incidence matrix computation (Post - Pre) - Bounded reachability graph via BFS with truncation All operations use immutable Pydantic models with validation of non-negative arc weights, marking sizes, and transition indices.
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 34be2cd68a
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 1390db9e57
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
…ndary mutations fail-closed
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 2639507436
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
…hon bound, lint)" This reverts commit ce8bd72.
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: ecba676ef1
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| if any(w < 0 for w in row): | ||
| raise ValueError("pre weights must be non-negative") |
There was a problem hiding this comment.
When a net or marking contains values above the exported 1000-token/arc limits, these validators now accept them because they check only non-negativity. This makes native callers able to supply arbitrarily wide integers and lets reachability retain states outside the declared marking envelope; it also makes a disabled firing from an already oversized marking report ESCAPES_DECLARED_ENVELOPE instead of NOT_ENABLED. Restore the upper bounds on both arc weights and marking tokens.
AGENTS.md reference: AGENTS.md:L126-L136
Useful? React with 👍 / 👎.
| def enabled_transitions(net: PetriNet, marking: Marking) -> list[int]: | ||
| """Return indices of all transitions enabled at the given marking.""" | ||
| _require_marking_size(net, marking) | ||
| result: list[int] = [] |
There was a problem hiding this comment.
When a direct caller passes a valid Marking whose token count differs from net.place_count, the exported native functions no longer reject the cross-field mismatch: a short marking makes this indexing raise IndexError, while a long marking is silently truncated to the net's places. The request adapters still validate this relation, but enabled_transitions, fire_transition, and reachability_graph are themselves public native APIs, so restore the shared check inside the kernels.
AGENTS.md reference: AGENTS.md:L121-L124
Useful? React with 👍 / 👎.
| states: tuple[tuple[int, ...], ...] | ||
| edges: tuple[tuple[int, int, int], ...] | ||
| status: Literal["COMPLETE", "TRUNCATED", "ESCAPES_DECLARED_ENVELOPE"] | ||
| frontier: tuple[ReachabilityFrontier, ...] | ||
| envelope_escape: ReachabilityEnvelopeEscape | None = None | ||
| truncated: bool |
There was a problem hiding this comment.
When a serialized reachability response is revalidated or consumed later, this reduced model no longer retains the net, initial marking, or state bound and has removed the deterministic replay validator. Consequently, impossible or corrupted claims such as states=(), edges=(), truncated=False validate as authoritative results, with no way to check that the edges and truncation flag belong to the requested BFS; retain the source values and replay the defining traversal as before.
AGENTS.md reference: AGENTS.md:L156-L157
Useful? React with 👍 / 👎.
| siphons: tuple[tuple[int, ...], ...] | ||
| traps: tuple[tuple[int, ...], ...] |
There was a problem hiding this comment.
When this result is serialized or validated independently of the immediate call, it carries neither the source net nor its digest and performs no invariant validation, so payloads with out-of-range places, duplicates, nonminimal sets, or even siphons=((-1,),) are accepted as exact siphon/trap results. Retain the source value and validate the defining siphon/trap and minimality relations within the admitted 20-place bound.
AGENTS.md reference: AGENTS.md:L156-L157
Useful? React with 👍 / 👎.
1 participant
Summary
Add the
petri_net.siphon_trap.checkoperation to the existing Petri net domain, implementing minimal siphon and trap detection.Changes
find_minimal_siphonsandfind_minimal_trapskernels using inclusion-minimal subset enumeration with set-theoretic pre/post arc conditionsSiphonTrapRequestandSiphonTrapResultPydantic modelscompute_siphon_trapadapter wiring models to kernelspetri_net.siphon_trap.checkas a new builtin tool with examplesfind_minimal_siphonsandfind_minimal_trapsfrom the public package APIRegistered operations (5 total)
petri_net.enabled_transitions.compute— find enabled transitions at a markingpetri_net.fire_transition.compute— fire one transitionpetri_net.incidence_matrix.compute— compute C = Post - Prepetri_net.reachability_graph.compute— bounded reachability graph via BFSpetri_net.siphon_trap.check— minimal siphons and trapsTest results
All 24 tests pass (16 existing + 8 new).
Continue this on Linzumi