Function may_violate_diagnostics
pub fn may_violate_diagnostics(
agent: &AgentDecl,
types: &HashMap<String, Arc<TypeDecl>>,
) -> Vec<CompileError>Expand description
#2221: bynk.transition.may_violate — a warning for each move a handler
can make that a transition refuses at commit (track §3.2–§3.5).
Only Certainty::Known violations fire, from start states the agent can
be in after a commit (the overlay already filters on
StateMachine::reachable_after_commit); a computed write that only may
land badly, a truncated handler and a transition outside the evaluated
fragment raise nothing. The warning sits on the write (or, for an unchanged
path, its tail), names the path’s guards, and carries the transition and
one handler that makes the start state reachable as related information.
The commit-time check is unchanged.