drew
4d969eaf2b
When the reviewer finishes a review and judges the work fundamentally unworkable (implementation surfaced misdiagnosis, obsoleted-by-other-work, or irreducible complexity), it can now emit verdict='abstain' + suggested_next_action='abandon' with a Gate-3 abandon_reason_category. The controller routes REVIEWING → ABANDONED and (when the kill switch is on) performs the Forgejo close via the reviewer-abandon side-effect tick — no implementer/CI/merge cycles. Wired with the same defense-in-depth pattern Phase 2 established: MCP setter validation + outcomes mapper dispatch with confidence gating + Pydantic atomicity validator + side-effect tick with audit-trail attribution (cause=REVIEWER_ABANDON, event_type='reviewer_abandon'). Default-off CONTROLLER_GATE3_ABANDON_ENABLED kill switch so a fresh deploy is audit-only until the operator explicitly enables Forgejo writes. Bundled refactor: hoisted the 9 Gate-2 + 3 Gate-3-exclusive abandon categories into tools/controller/contracts/abandon_categories.py (triggered by Phase 3 per the plan's follow-up backlog). Both gates now consume the shared frozensets; doc-contract tests grep each agent prompt against the canonical list. Adversarial review (2 rounds): caught + fixed MCP cross-check ordering (atomicity FIRST so missing-setter shows actionable error), confidence=None symmetric downgrade across both gates, dead blocking-issues extraction in _run_close, idempotency clock-collision in the test, low-vs-missing reason-string conflation, and several test-quality gaps. 4064/4071 tests passing (7 pre-existing failures unrelated to Phase 3). Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
943 lines
41 KiB
Python
943 lines
41 KiB
Python
"""Controller state machine — TRANSITIONS table + invariants.
|
|
|
|
Plan v9 simplified scope: ship the 6 LOAD-BEARING property invariants
|
|
for v1; add the other 15 as bugs surface.
|
|
|
|
States (per plan v6+v9, with v8 metadata-only-no-bypass + v6
|
|
CONFLICT_RESOLVING + v6 MERGING + v6 CREATED_PR):
|
|
|
|
DISCOVERED
|
|
→ ANALYZING (estimator picks tier OR routes to metadata_only)
|
|
→ STUCK (estimator failed twice)
|
|
|
|
ANALYZING
|
|
→ IMPLEMENTING(tier) (normal path)
|
|
→ REVIEWING (metadata-only path; per v8 Hard Rule #1 still
|
|
goes through reviewer with lightweight profile)
|
|
→ STUCK (estimator output schema violation)
|
|
|
|
IMPLEMENTING
|
|
→ AWAITING_CI (worker pushed; head_sha advanced)
|
|
→ ESCALATING (worker emitted competence-failure; no push)
|
|
→ CONFLICT_RESOLVING (worker emitted rebase-failed)
|
|
→ STUCK (worker emitted blocked)
|
|
→ REVIEWING (top-tier worker emitted dispute-reviewer; T5-4)
|
|
|
|
AWAITING_CI
|
|
→ REVIEWING (CI green AND the PR still merges cleanly)
|
|
→ CONFLICT_RESOLVING (CI green but a cheap Forgejo mergeable
|
|
check shows the base advanced while CI
|
|
ran — pre-review gate skips the doomed
|
|
reviewer pass on code that needs rebasing)
|
|
→ IMPLEMENTING(tier) (CI red, attempts-per-tier remaining)
|
|
→ ESCALATING (CI red, attempts-per-tier exhausted)
|
|
→ AWAITING_CI (flake retry; one retry per flake-classifier
|
|
per gate; same state)
|
|
|
|
CONFLICT_RESOLVING
|
|
→ IMPLEMENTING(same tier) (1st conflict resolved)
|
|
→ ESCALATING (2nd conflict at same tier)
|
|
→ STUCK (3rd conflict; or resolver outcome=irreconcilable)
|
|
|
|
ESCALATING
|
|
→ IMPLEMENTING(tier+1) (next tier available)
|
|
→ ABANDONED (max tier exhausted)
|
|
|
|
REVIEWING
|
|
→ APPROVED (verdict=approve; T5-7: implementation/review
|
|
masters drop here so a singleton merge master can
|
|
own the Forgejo merge POST without N-way contention)
|
|
→ IMPLEMENTING(tier) (verdict=request-changes,
|
|
attempts-per-tier remaining)
|
|
→ ESCALATING (verdict=request-changes, attempts-per-tier
|
|
exhausted)
|
|
→ OPERATOR_ATTENTION (T5-4: re_examined_disputed_claim=True
|
|
and verdict=request-changes; reviewer
|
|
re-checked the disputed claim and still
|
|
disagrees with the implementer)
|
|
→ STUCK (verdict=abstain; retry-once-then-stuck handled
|
|
in v9 retry policy)
|
|
|
|
APPROVED (T5-7: handoff state — implementation/review masters drop
|
|
here; the singleton merge master picks workflows up via
|
|
the merge_start event and serializes Forgejo merges)
|
|
→ MERGING (merge_start; only the merge master fires this)
|
|
→ DISCOVERED (operator_unstick)
|
|
|
|
OPERATOR_ATTENTION (T5-4: post-dispute stalemate)
|
|
→ APPROVED (operator override: force "merge anyway" — hands
|
|
the workflow to the merge master same as a normal
|
|
approve)
|
|
→ ABANDONED (operator gave up)
|
|
→ DISCOVERED (operator restart via operator_unstick)
|
|
|
|
MERGING
|
|
→ MERGED (Forgejo 200)
|
|
→ CONFLICT_RESOLVING (Forgejo 409; post-approval base conflict;
|
|
hands directly to the LLM conflict_resolver
|
|
role, skipping the wasted implementer pass
|
|
that would just re-discover the conflict)
|
|
→ AWAITING_CI (Forgejo 422; CI status expired race)
|
|
→ STUCK (Forgejo 403 branch protection; or retry_count>=5)
|
|
→ MERGED OR ABANDONED (Forgejo 404; check external state)
|
|
→ APPROVED (merge_interrupted; the singleton merge master shut
|
|
down mid-merge before resolving — return the
|
|
workflow to the handoff state for clean re-pickup)
|
|
|
|
Terminal states:
|
|
MERGED, ABANDONED, STUCK, CREATED_PR
|
|
|
|
CREATED_PR is reachable only from issue-kind workflows (IMPLEMENTING
|
|
on an issue successfully creates a PR + spawns a new pr-kind workflow
|
|
with parent_workflow_id; the issue workflow terminates at CREATED_PR).
|
|
For v1 simplicity, this module models only the PR-kind state machine;
|
|
issue-kind handling lands in Phase 4.
|
|
"""
|
|
|
|
from __future__ import annotations
|
|
|
|
from dataclasses import dataclass, field
|
|
from typing import Iterable
|
|
|
|
|
|
# ─── states ──────────────────────────────────────────────────────────
|
|
|
|
|
|
KNOWN_STATES: frozenset[str] = frozenset(
|
|
{
|
|
"DISCOVERED",
|
|
"GROOMING",
|
|
"ANALYZING",
|
|
"IMPLEMENTING",
|
|
"AWAITING_CI",
|
|
"CONFLICT_RESOLVING",
|
|
"ESCALATING",
|
|
"REVIEWING",
|
|
"APPROVED",
|
|
"MERGING",
|
|
"PAUSED",
|
|
"OPERATOR_ATTENTION",
|
|
"MERGED",
|
|
"ABANDONED",
|
|
"STUCK",
|
|
"CREATED_PR",
|
|
}
|
|
)
|
|
|
|
TERMINAL_STATES: frozenset[str] = frozenset(
|
|
{
|
|
"MERGED",
|
|
"ABANDONED",
|
|
"STUCK",
|
|
"CREATED_PR",
|
|
}
|
|
)
|
|
|
|
NON_TERMINAL_STATES: frozenset[str] = KNOWN_STATES - TERMINAL_STATES
|
|
|
|
|
|
# Events that drive transitions. The event name captures "what the
|
|
# controller observed" so the transition table reads as data, not
|
|
# code.
|
|
@dataclass(frozen=True)
|
|
class Event:
|
|
name: str
|
|
description: str = ""
|
|
|
|
def __repr__(self) -> str:
|
|
return f"Event({self.name!r})"
|
|
|
|
|
|
# ─── canonical events ────────────────────────────────────────────────
|
|
|
|
|
|
EVENTS = {
|
|
# ANALYZING
|
|
"estimator_done": Event("estimator_done", "Estimator returned tier"),
|
|
"estimator_metadata_only": Event(
|
|
"estimator_metadata_only",
|
|
"Estimator flagged is_metadata_only=true",
|
|
),
|
|
"estimator_failed_twice": Event(
|
|
"estimator_failed_twice",
|
|
"Estimator hit repeated worker-internal-error — a flaky session "
|
|
"that never emits canonical output. The estimator has no "
|
|
"escalation or salvage path, so after _ESTIMATOR_WORKER_ERROR_LIMIT "
|
|
"such failures the workflow STUCKs (ANALYZING → STUCK). The "
|
|
"'twice' in the name is historical; the real cap is the constant. "
|
|
"(Strict-parse failures route via contract-violation → "
|
|
"pickup_exhausted, not this event.)",
|
|
),
|
|
"estimator_abandon": Event(
|
|
"estimator_abandon",
|
|
"Estimator judged the work item fundamentally unworkable and "
|
|
"emitted verdict='abandon' with a Gate 2 reason_category "
|
|
"(scope_intractable, intent_wrong, security_regression, "
|
|
"deprecated_dependency, breaks_protected_invariants, "
|
|
"out_of_scope, low_value, unmaintained_path, "
|
|
"policy_violation). Workflow routes ANALYZING → ABANDONED; "
|
|
"the estimator-abandon side-effect tick performs the Forgejo "
|
|
"close via close_act with cause=ESTIMATOR_ABANDON. Gate 2 "
|
|
"always closes — no preserved-value judgment at the cheapest "
|
|
"LLM stage. (Phase 2 corrected dispatch, 2026-05-25.)",
|
|
),
|
|
# IMPLEMENTING
|
|
"implementer_pushed": Event(
|
|
"implementer_pushed",
|
|
"Worker emitted outcome=resolved; head_sha advanced",
|
|
),
|
|
"implementer_competence_failure": Event(
|
|
"implementer_competence_failure",
|
|
"Worker emitted outcome=competence-failure",
|
|
),
|
|
"implementer_rebase_failed": Event(
|
|
"implementer_rebase_failed",
|
|
"Worker emitted outcome=rebase-failed",
|
|
),
|
|
"implementer_blocked": Event(
|
|
"implementer_blocked",
|
|
"Worker emitted outcome=blocked",
|
|
),
|
|
"implementer_dispute_reviewer": Event(
|
|
"implementer_dispute_reviewer",
|
|
"Top-tier implementer emitted outcome=dispute-reviewer; "
|
|
"re-route to REVIEWING with the implementer's rebuttal as "
|
|
"context (T5-4).",
|
|
),
|
|
"implementer_verified": Event(
|
|
"implementer_verified",
|
|
"Implementer ran post-conflict-resolution and emitted "
|
|
"outcome=verified-clean: the resolver's commits already cover "
|
|
"everything and no further code changes are needed. Route "
|
|
"directly to AWAITING_CI to verify CI on the resolver's "
|
|
"commits (T5-11). Prevents the implementer-noop → escalation "
|
|
"wart that wasted a tier when the resolver did clean work.",
|
|
),
|
|
"implementer_ci_not_ready": Event(
|
|
"implementer_ci_not_ready",
|
|
"Implementer emitted outcome=ci-not-ready: CI for the PR head "
|
|
"has no verdict yet (still pending) and there is nothing to "
|
|
"fix. Route to AWAITING_CI to wait for the verdict instead of "
|
|
"STUCK. Exists for RUN_CI_LOCAL, where CI is kicked on-demand "
|
|
"and finishes minutes after the implementer runs.",
|
|
),
|
|
"implementer_noop_ci_green": Event(
|
|
"implementer_noop_ci_green",
|
|
"Implementer emitted outcome=noop AND the attempt saw a "
|
|
"fully-green CI on the current HEAD (every gate passed, none "
|
|
"failed/pending) — nothing to fix, no commit pushed. Route "
|
|
"IMPLEMENTING → REVIEWING directly: the HEAD is already "
|
|
"CI-verified, so an AWAITING_CI round-trip would only re-poll "
|
|
"a verdict the controller already has — and with no fresh push "
|
|
"no fresh CI run is ever triggered, so the poll would never "
|
|
"resolve (the PR-41 deadlock). A no-push edge, same shape as "
|
|
"implementer_dispute_reviewer.",
|
|
),
|
|
"implementer_ci_infra_failure": Event(
|
|
"implementer_ci_infra_failure",
|
|
"Implementer emitted outcome=ci-infra-failure: the CI failure "
|
|
"it was sent to fix is not a code failure — the job log carries "
|
|
"no verdict (no ##[error], test summary, Traceback or exit "
|
|
"code), the run was hard-killed (OOM / pod eviction). There is "
|
|
"nothing to fix. Route IMPLEMENTING → DISCOVERED so the "
|
|
"CI-freshness gate re-handles it under its rerun budget "
|
|
"(empty-commit rerun, or STUCK once the budget is exhausted) "
|
|
"instead of dead-ending at blocked → STUCK.",
|
|
),
|
|
# AWAITING_CI
|
|
"ci_green": Event("ci_green", "CI overall_state=success"),
|
|
"pre_review_base_conflict": Event(
|
|
"pre_review_base_conflict",
|
|
"CI passed, but a cheap Forgejo mergeable check shows the PR "
|
|
"no longer merges cleanly into base (the base advanced while "
|
|
"CI ran). Route AWAITING_CI → CONFLICT_RESOLVING to hand the "
|
|
"conflict to the LLM conflict_resolver BEFORE the expensive "
|
|
"reviewer pass — reviewing code that must be rebased anyway "
|
|
"wastes an LLM review. One API call, no LLM. Only an explicit "
|
|
"mergeable=false fires this; an unknown/uncomputed bit falls "
|
|
"through to ci_green so a fresh PR is never false-routed.",
|
|
),
|
|
"ci_red_retry_same_tier": Event(
|
|
"ci_red_retry_same_tier",
|
|
"CI failed; attempts-per-tier remaining",
|
|
),
|
|
"ci_red_escalate": Event(
|
|
"ci_red_escalate",
|
|
"CI failed; attempts-per-tier exhausted",
|
|
),
|
|
"ci_flake_retry": Event(
|
|
"ci_flake_retry",
|
|
"CI failed but classified as flake; retry once per gate "
|
|
"(bounded by workflows.ci_flake_retries_remaining)",
|
|
),
|
|
"ci_flake_retries_exhausted": Event(
|
|
"ci_flake_retries_exhausted",
|
|
"ci_flake_retry was already taken; subsequent flake → real "
|
|
"failure path (ci_red_retry_same_tier / ci_red_escalate)",
|
|
),
|
|
"ci_polling_exhausted": Event(
|
|
"ci_polling_exhausted",
|
|
"AWAITING_CI polling exceeded the timeout threshold; STUCK so "
|
|
"operator can investigate (CI hang, runner outage, ...)",
|
|
),
|
|
"ci_infra_recheck": Event(
|
|
"ci_infra_recheck",
|
|
"CI in AWAITING_CI failed AGAIN with an infra-class failure "
|
|
"(checkout/setup, no code findings). Route back to DISCOVERED "
|
|
"so the CI-freshness gate re-handles it: the gate's "
|
|
"rerun-budget counter accumulates and triggers another "
|
|
"empty-commit rerun, or routes to STUCK once the budget is "
|
|
"exhausted. Sending an implementer to flail on infra (the "
|
|
"original incident) is avoided.",
|
|
),
|
|
# CONFLICT_RESOLVING
|
|
"conflict_resolved_first": Event(
|
|
"conflict_resolved_first",
|
|
"Resolver returned outcome=resolved (1st conflict at tier)",
|
|
),
|
|
"conflict_resolved_second_same_tier": Event(
|
|
"conflict_resolved_second_same_tier",
|
|
"Resolver returned outcome=resolved (2nd conflict at tier)",
|
|
),
|
|
"conflict_repeated_three_plus": Event(
|
|
"conflict_repeated_three_plus",
|
|
"3rd or later conflict — likely structural; STUCK",
|
|
),
|
|
"conflict_irreconcilable": Event(
|
|
"conflict_irreconcilable",
|
|
"Resolver returned outcome=irreconcilable",
|
|
),
|
|
# ESCALATING
|
|
"escalate_next_tier_available": Event(
|
|
"escalate_next_tier_available",
|
|
"Tier+1 ≤ MAX_TIER; transition to IMPLEMENTING(tier+1)",
|
|
),
|
|
"escalate_max_tier_exhausted": Event(
|
|
"escalate_max_tier_exhausted",
|
|
"Tier was MAX_TIER; ABANDONED",
|
|
),
|
|
# REVIEWING
|
|
"reviewer_approve": Event(
|
|
"reviewer_approve",
|
|
"Reviewer verdict=approve",
|
|
),
|
|
"reviewer_request_changes_retry": Event(
|
|
"reviewer_request_changes_retry",
|
|
"Reviewer verdict=request-changes; attempts-per-tier remaining",
|
|
),
|
|
"reviewer_request_changes_escalate": Event(
|
|
"reviewer_request_changes_escalate",
|
|
"Reviewer verdict=request-changes; attempts-per-tier exhausted",
|
|
),
|
|
"reviewer_abstain": Event(
|
|
"reviewer_abstain",
|
|
"Reviewer verdict=abstain (rare); per v6 retry-once-then-STUCK",
|
|
),
|
|
"reviewer_re_examined_request_changes": Event(
|
|
"reviewer_re_examined_request_changes",
|
|
"Reviewer was re-invoked after an implementer dispute at "
|
|
"top tier and stood by verdict=request-changes "
|
|
"(re_examined_disputed_claim=True); stalemate → OPERATOR_ATTENTION "
|
|
"(T5-4/T5-9: only fires when the disputer was already at MAX_TIER).",
|
|
),
|
|
"reviewer_re_examined_request_changes_escalate": Event(
|
|
"reviewer_re_examined_request_changes_escalate",
|
|
"Reviewer re-examined a dispute below top tier and still says "
|
|
"request-changes; rather than dead-end at OPERATOR_ATTENTION, "
|
|
"escalate the implementer to next tier so a more capable model "
|
|
"can take a fresh shot — either fix the code or make a more "
|
|
"credible dispute (T5-9).",
|
|
),
|
|
"reviewer_abandon": Event(
|
|
"reviewer_abandon",
|
|
"Reviewer judged the implementation revealed the work is "
|
|
"fundamentally unworkable and emitted verdict='abstain' + "
|
|
"suggested_next_action='abandon' with a Gate 3 "
|
|
"abandon_reason_category (the 9 Gate-2 categories plus "
|
|
"implementation_revealed_misdiagnosis, "
|
|
"obsoleted_by_other_merged_work, irreducible_complexity). "
|
|
"Workflow routes REVIEWING → ABANDONED; the reviewer-abandon "
|
|
"side-effect tick performs the Forgejo close via close_act "
|
|
"with cause=REVIEWER_ABANDON. Gate 3 is the backstop — only "
|
|
"fires when implementation surfaced evidence Gate 2 could not "
|
|
"see. (Phase 3, 2026-05-25.)",
|
|
),
|
|
# T5-7: handoff to singleton merge master
|
|
"merge_start": Event(
|
|
"merge_start",
|
|
"Singleton merge master picked up an APPROVED workflow; "
|
|
"transition to MERGING so the Forgejo merge POST runs on "
|
|
"exactly one machine.",
|
|
),
|
|
# OPERATOR_ATTENTION exits (operator-driven only)
|
|
"operator_force_merge": Event(
|
|
"operator_force_merge",
|
|
"Operator reviewed an OPERATOR_ATTENTION workflow and overrode "
|
|
"the disagreement; route through MERGING for the Forgejo POST.",
|
|
),
|
|
"operator_abandon": Event(
|
|
"operator_abandon",
|
|
"Operator reviewed an OPERATOR_ATTENTION workflow and decided "
|
|
"to abandon the PR.",
|
|
),
|
|
# MERGING
|
|
"merge_ok": Event("merge_ok", "Forgejo merge returned 200"),
|
|
"merge_base_conflict": Event(
|
|
"merge_base_conflict",
|
|
"Forgejo merge returned 409 (base advanced post-approval) OR "
|
|
"the merge driver's pre-merge rebase produced unresolvable "
|
|
"conflicts. Routes to CONFLICT_RESOLVING so the controller's "
|
|
"conflict_resolver role (LLM) handles it; the merge process "
|
|
"stays 100% deterministic and bounces ALL LLM-requiring work "
|
|
"back to the controller (T5-10).",
|
|
),
|
|
"merge_ci_required_missing": Event(
|
|
"merge_ci_required_missing",
|
|
"Forgejo merge returned 422; race with CI status",
|
|
),
|
|
"merge_branch_protection_blocked": Event(
|
|
"merge_branch_protection_blocked",
|
|
"Forgejo merge returned 403; operator must intervene",
|
|
),
|
|
"merge_retry_exhausted": Event(
|
|
"merge_retry_exhausted",
|
|
"merging_retry_count >= 5; STUCK",
|
|
),
|
|
"merge_external_action": Event(
|
|
"merge_external_action",
|
|
"Forgejo merge returned 404; reconcile via PR state",
|
|
),
|
|
"merge_interrupted": Event(
|
|
"merge_interrupted",
|
|
"The singleton merge master stopped mid-merge (graceful "
|
|
"shutdown caught the workflow in MERGING). Return it to "
|
|
"APPROVED so the next merge run picks it up cleanly instead "
|
|
"of leaving it stranded in MERGING with no owner.",
|
|
),
|
|
# DISCOVERED → ANALYZING
|
|
"discovery_picked_up": Event(
|
|
"discovery_picked_up",
|
|
"Master saw DISCOVERED workflow; queue estimator attempt",
|
|
),
|
|
# DISCOVERED → AWAITING_CI (CI-freshness gate)
|
|
"discovery_ci_rerun_triggered": Event(
|
|
"discovery_ci_rerun_triggered",
|
|
"Discovered PR had stale/infra-broken CI; controller triggered "
|
|
"a fresh CI run and routed to AWAITING_CI for a real verdict",
|
|
),
|
|
# Operator escape hatch (reachable from every non-terminal state)
|
|
"operator_unstick": Event(
|
|
"operator_unstick",
|
|
"Operator manually unstucking; back to DISCOVERED",
|
|
),
|
|
"pickup_exhausted": Event(
|
|
"pickup_exhausted",
|
|
"Attempt picked up MAX_PICKUPS times w/o success; STUCK",
|
|
),
|
|
# Phase 1k+ opt-in label gate transitions. The opt-in label is the
|
|
# operator's "pause / resume" knob: removing it pauses the
|
|
# workflow (non-terminal); re-adding it resumes back to the
|
|
# state recorded at pause-time (workflows.pre_pause_state).
|
|
"opt_in_label_removed": Event(
|
|
"opt_in_label_removed",
|
|
"Operator removed CONTROLLER_OPT_IN_LABEL; workflow → PAUSED",
|
|
),
|
|
# Phase 1 corrected dispatch (worker-queue shape) — 2026-05-25.
|
|
# Grooming is the duplicate/staleness gate that runs BEFORE the
|
|
# estimator. Promote-discovered fires ``grooming_started`` to route
|
|
# DISCOVERED → GROOMING; the scheduler then enqueues a
|
|
# ``grooming_stage_b`` attempt whose worker runs deterministic
|
|
# checks + suspicion scoring + Stage B LLM judgment internally.
|
|
# The worker's verdict drives one of three verdict events; the
|
|
# Forgejo side-effects (label swap, audit comment, PATCH
|
|
# state:closed) happen in ``run_grooming_side_effects_tick``
|
|
# AFTER the state-machine transition, matching the merging tick's
|
|
# pattern.
|
|
"grooming_started": Event(
|
|
"grooming_started",
|
|
"Promote-discovered transitioned the workflow into GROOMING; "
|
|
"the scheduler will enqueue a grooming_stage_b attempt. Only "
|
|
"fires when CONTROLLER_GROOMING_ENABLED=true.",
|
|
),
|
|
"groom_verdict_proceed": Event(
|
|
"groom_verdict_proceed",
|
|
"Grooming worker says: not a duplicate (or LLM confidence "
|
|
"below threshold). Resume normal pipeline via GROOMING → "
|
|
"ANALYZING for the estimator pass.",
|
|
),
|
|
"groom_verdict_defer": Event(
|
|
"groom_verdict_defer",
|
|
"Grooming worker says: defer (any verdict that maps to defer "
|
|
"per the action-mapping + CLOSE_ENABLED policy). State "
|
|
"transitions to PAUSED; ``run_grooming_side_effects_tick`` "
|
|
"will perform the Forgejo defer (label swap + audit comment).",
|
|
),
|
|
"groom_verdict_close": Event(
|
|
"groom_verdict_close",
|
|
"Grooming worker says: close (full_duplicate or unnecessary "
|
|
"with CLOSE_ENABLED=true). State transitions to ABANDONED; "
|
|
"``run_grooming_side_effects_tick`` will perform the Forgejo "
|
|
"close (PATCH state:closed + audit comment).",
|
|
),
|
|
"opt_in_label_restored": Event(
|
|
"opt_in_label_restored",
|
|
"Operator re-added the opt-in label; resume from pre_pause_state",
|
|
),
|
|
}
|
|
|
|
|
|
# ─── transitions ─────────────────────────────────────────────────────
|
|
|
|
|
|
# Map of (from_state, event_name) → to_state. Pure data; tests
|
|
# enumerate every key to verify invariants.
|
|
TRANSITIONS: dict[tuple[str, str], str] = {
|
|
("DISCOVERED", "discovery_picked_up"): "ANALYZING",
|
|
# CI-freshness gate: a Discovered PR whose CI is stale or
|
|
# infra-broken gets a fresh CI run triggered (empty-commit push)
|
|
# and routes straight to AWAITING_CI. A no-code-change CI rerun
|
|
# genuinely only needs CI + review (no estimator tier sizing), so
|
|
# skipping ANALYZING is correct here, not a missed-analysis bug.
|
|
("DISCOVERED", "discovery_ci_rerun_triggered"): "AWAITING_CI",
|
|
("ANALYZING", "estimator_done"): "IMPLEMENTING",
|
|
("ANALYZING", "estimator_metadata_only"): "REVIEWING",
|
|
("ANALYZING", "estimator_failed_twice"): "STUCK",
|
|
# Phase 2 (Gate 2 estimator abandon, 2026-05-25): estimator
|
|
# judged the work item fundamentally unworkable. The side-effect
|
|
# tick performs the Forgejo close via Phase 1's close_act
|
|
# orchestrator (cause=ESTIMATOR_ABANDON).
|
|
("ANALYZING", "estimator_abandon"): "ABANDONED",
|
|
("IMPLEMENTING", "implementer_pushed"): "AWAITING_CI",
|
|
("IMPLEMENTING", "implementer_competence_failure"): "ESCALATING",
|
|
("IMPLEMENTING", "implementer_rebase_failed"): "CONFLICT_RESOLVING",
|
|
("IMPLEMENTING", "implementer_blocked"): "STUCK",
|
|
("IMPLEMENTING", "implementer_dispute_reviewer"): "REVIEWING",
|
|
# Green-CI noop: implementer found nothing to fix and the HEAD is
|
|
# already CI-green. No push happened, so routing through AWAITING_CI
|
|
# would deadlock (ci_status_poll waits for a fresh run that a noop
|
|
# never triggers — the PR-41 incident). Direct to REVIEWING; the
|
|
# no-push invariant exception covers this edge.
|
|
("IMPLEMENTING", "implementer_noop_ci_green"): "REVIEWING",
|
|
("IMPLEMENTING", "implementer_verified"): "AWAITING_CI",
|
|
("IMPLEMENTING", "implementer_ci_not_ready"): "AWAITING_CI",
|
|
# ci-infra-failure: the CI failure is a hard-kill (OOM / eviction)
|
|
# with no verdict, not code. Route to DISCOVERED so the CI-freshness
|
|
# gate reruns it under RERUN_BUDGET rather than STUCK.
|
|
("IMPLEMENTING", "implementer_ci_infra_failure"): "DISCOVERED",
|
|
("IMPLEMENTING", "pickup_exhausted"): "STUCK",
|
|
("AWAITING_CI", "ci_green"): "REVIEWING",
|
|
# Pre-review mergeable gate: CI is green but the PR no longer
|
|
# merges cleanly into base. Hand the conflict straight to the LLM
|
|
# conflict_resolver and skip the doomed reviewer pass (the code
|
|
# gets re-CI'd + re-reviewed after the rebase anyway). Same target
|
|
# as the MERGING 409 path — cheap detection, expensive resolution.
|
|
("AWAITING_CI", "pre_review_base_conflict"): "CONFLICT_RESOLVING",
|
|
("AWAITING_CI", "ci_red_retry_same_tier"): "IMPLEMENTING",
|
|
("AWAITING_CI", "ci_red_escalate"): "ESCALATING",
|
|
("AWAITING_CI", "ci_flake_retry"): "AWAITING_CI",
|
|
("AWAITING_CI", "ci_flake_retries_exhausted"): "ESCALATING",
|
|
("AWAITING_CI", "ci_polling_exhausted"): "STUCK",
|
|
# CI-freshness gate loop: an AWAITING_CI workflow whose reran CI
|
|
# ALSO infra-failed routes back to DISCOVERED so the gate
|
|
# re-handles it (rerun-budget counter accumulates → another rerun,
|
|
# or STUCK at budget exhaustion). The DISCOVERED↔AWAITING_CI cycle
|
|
# is bounded by the gate's RERUN_BUDGET — not an unbounded loop.
|
|
("AWAITING_CI", "ci_infra_recheck"): "DISCOVERED",
|
|
("CONFLICT_RESOLVING", "conflict_resolved_first"): "IMPLEMENTING",
|
|
("CONFLICT_RESOLVING", "conflict_resolved_second_same_tier"): "ESCALATING",
|
|
("CONFLICT_RESOLVING", "conflict_repeated_three_plus"): "STUCK",
|
|
("CONFLICT_RESOLVING", "conflict_irreconcilable"): "STUCK",
|
|
("CONFLICT_RESOLVING", "pickup_exhausted"): "STUCK",
|
|
("ESCALATING", "escalate_next_tier_available"): "IMPLEMENTING",
|
|
("ESCALATING", "escalate_max_tier_exhausted"): "ABANDONED",
|
|
("REVIEWING", "reviewer_approve"): "APPROVED",
|
|
("REVIEWING", "reviewer_request_changes_retry"): "IMPLEMENTING",
|
|
("REVIEWING", "reviewer_request_changes_escalate"): "ESCALATING",
|
|
("REVIEWING", "reviewer_re_examined_request_changes"): "OPERATOR_ATTENTION",
|
|
("REVIEWING", "reviewer_re_examined_request_changes_escalate"): "ESCALATING",
|
|
("REVIEWING", "reviewer_abstain"): "STUCK",
|
|
# Phase 3 (Gate 3 reviewer abandon, 2026-05-25): reviewer judged
|
|
# the implementation revealed the work is fundamentally unworkable.
|
|
# The reviewer-abandon side-effect tick performs the Forgejo close
|
|
# via Phase 1's close_act orchestrator (cause=REVIEWER_ABANDON).
|
|
("REVIEWING", "reviewer_abandon"): "ABANDONED",
|
|
("REVIEWING", "pickup_exhausted"): "STUCK",
|
|
# T5-7: APPROVED is the handoff state between impl/review masters
|
|
# (which write here on reviewer_approve) and the singleton merge
|
|
# master (which fires merge_start to begin the Forgejo POST). Only
|
|
# the merge master fires this event; impl/review masters skip
|
|
# APPROVED workflows.
|
|
("APPROVED", "merge_start"): "MERGING",
|
|
("APPROVED", "operator_unstick"): "DISCOVERED",
|
|
("MERGING", "merge_ok"): "MERGED",
|
|
("MERGING", "merge_base_conflict"): "CONFLICT_RESOLVING",
|
|
("MERGING", "merge_ci_required_missing"): "AWAITING_CI",
|
|
("MERGING", "merge_branch_protection_blocked"): "STUCK",
|
|
("MERGING", "merge_retry_exhausted"): "STUCK",
|
|
("MERGING", "merge_external_action"): "MERGED", # reconciliation refines
|
|
("MERGING", "merge_interrupted"): "APPROVED", # graceful-shutdown re-pickup
|
|
# Operator escape hatch from STUCK.
|
|
("STUCK", "operator_unstick"): "DISCOVERED",
|
|
# PAUSED's operator escape hatch (also reachable for legacy data
|
|
# without pre_pause_state).
|
|
("PAUSED", "operator_unstick"): "DISCOVERED",
|
|
# OPERATOR_ATTENTION exits (T5-4): stalemate after implementer
|
|
# disputed a reviewer's blocking_issues. Operator decides the
|
|
# tiebreaker. operator_force_merge routes through APPROVED (per
|
|
# T5-7: same handoff state the normal-approve path uses), so the
|
|
# singleton merge master serializes the actual Forgejo POST.
|
|
("OPERATOR_ATTENTION", "operator_force_merge"): "APPROVED",
|
|
("OPERATOR_ATTENTION", "operator_abandon"): "ABANDONED",
|
|
("OPERATOR_ATTENTION", "operator_unstick"): "DISCOVERED",
|
|
# Phase 1 corrected dispatch (worker-queue shape) — 2026-05-25.
|
|
# Grooming sits BEFORE estimator: promote-discovered routes
|
|
# DISCOVERED → GROOMING (when enabled), the scheduler queues a
|
|
# grooming_stage_b attempt, the worker's verdict fires one of three
|
|
# outcome events. The PAUSED/ABANDONED targets are the same
|
|
# terminal/quiescent states that operator-driven abandonment +
|
|
# label-pause already use, so the Forgejo side-effects (audit
|
|
# comment + label swap or PATCH state:closed) live in a dedicated
|
|
# ``run_grooming_side_effects_tick`` (analogous to merging.py),
|
|
# not in the state transition itself.
|
|
("DISCOVERED", "grooming_started"): "GROOMING",
|
|
("GROOMING", "groom_verdict_proceed"): "ANALYZING",
|
|
("GROOMING", "groom_verdict_defer"): "PAUSED",
|
|
("GROOMING", "groom_verdict_close"): "ABANDONED",
|
|
# Operator escape hatch from GROOMING (matches the STUCK/PAUSED
|
|
# escape hatch shape).
|
|
("GROOMING", "operator_unstick"): "DISCOVERED",
|
|
# NOTE: ``opt_in_label_removed`` (any state → PAUSED) and
|
|
# ``opt_in_label_restored`` (PAUSED → pre_pause_state) are NOT
|
|
# listed here. They're out-of-band operator-driven events written
|
|
# directly by the reconciliation tick (via
|
|
# ``_apply_transition_with_pre_pause`` in master/reconciliation.py),
|
|
# which reads/writes ``workflows.pre_pause_state`` to determine
|
|
# the resume target. Encoding them per-state in this table would
|
|
# break the per-state event-set invariants (ESCALATING /
|
|
# CONFLICT_RESOLVING must have exactly the events they ship).
|
|
}
|
|
|
|
|
|
# ─── transition lookup ────────────────────────────────────────────────
|
|
|
|
|
|
class IllegalTransitionError(Exception):
|
|
"""Raised when ``apply_event`` is called with an event that has no
|
|
mapped transition from the current state. The master catches this
|
|
and transitions the workflow to STUCK with reason='illegal-event'."""
|
|
|
|
|
|
def apply_event(current_state: str, event_name: str) -> str:
|
|
"""Return the next state for ``event_name`` from ``current_state``.
|
|
|
|
Raises ``ValueError`` if ``current_state`` isn't in ``KNOWN_STATES``
|
|
(callers should validate state at load time per v6 unknown-state
|
|
guard). Raises ``IllegalTransitionError`` if no transition is
|
|
mapped.
|
|
"""
|
|
if current_state not in KNOWN_STATES:
|
|
raise ValueError(f"unknown state {current_state!r}; not in KNOWN_STATES")
|
|
try:
|
|
return TRANSITIONS[(current_state, event_name)]
|
|
except KeyError:
|
|
raise IllegalTransitionError(
|
|
f"no transition from {current_state!r} on event "
|
|
f"{event_name!r}; known events from this state: "
|
|
f"{sorted(e for (s, e) in TRANSITIONS if s == current_state)}"
|
|
) from None
|
|
|
|
|
|
def events_from(state: str) -> list[str]:
|
|
"""Return the list of event names that have a transition mapped
|
|
from ``state``. Useful for operator CLI 'what can I do from here?'
|
|
queries + property tests."""
|
|
return sorted(e for (s, e) in TRANSITIONS if s == state)
|
|
|
|
|
|
def reachable_from(state: str) -> set[str]:
|
|
"""Set of states reachable from ``state`` in one or more transitions.
|
|
|
|
Includes the starting state IFF it's part of a cycle (e.g.,
|
|
AWAITING_CI has a self-loop via ``ci_flake_retry``).
|
|
"""
|
|
seen: set[str] = set()
|
|
stack = [state]
|
|
cycles_back = False
|
|
while stack:
|
|
s = stack.pop()
|
|
for (frm, _evt), to in TRANSITIONS.items():
|
|
if frm != s:
|
|
continue
|
|
if to == state and s != state:
|
|
# A transition leads back to the start — that's a cycle.
|
|
cycles_back = True
|
|
if to == state and s == state:
|
|
# Self-loop on the start state.
|
|
cycles_back = True
|
|
if to in seen:
|
|
continue
|
|
seen.add(to)
|
|
stack.append(to)
|
|
if not cycles_back:
|
|
seen.discard(state)
|
|
return seen
|
|
|
|
|
|
# ─── property invariants (v9: ship 6 for v1) ──────────────────────────
|
|
|
|
|
|
@dataclass(frozen=True)
|
|
class InvariantViolation:
|
|
"""Returned by ``check_*`` helpers when an invariant fails. The
|
|
property tests assert ``check_*() == []``."""
|
|
|
|
invariant: str
|
|
message: str
|
|
|
|
|
|
def _violation(invariant: str, message: str) -> InvariantViolation:
|
|
return InvariantViolation(invariant=invariant, message=message)
|
|
|
|
|
|
def check_no_path_implementing_to_reviewing_skips_ci() -> list[InvariantViolation]:
|
|
"""Invariant #1 (v9 load-bearing): REVIEWING is reachable from
|
|
IMPLEMENTING only through AWAITING_CI, *except* when the
|
|
implementer didn't push (no head_sha advance).
|
|
|
|
Closes the no-mans-land race for the push path by construction.
|
|
|
|
T5-4 exception: ``implementer_dispute_reviewer`` is allowed as a
|
|
direct IMPLEMENTING → REVIEWING edge because no new commit was
|
|
pushed — the implementer is contesting the prior reviewer's claim
|
|
on the *existing* (already-CI-green) HEAD. Routing through
|
|
AWAITING_CI would be a no-op (nothing new to wait for) and would
|
|
confuse ci_status_poll which expects a fresh push to verify.
|
|
|
|
``implementer_noop_ci_green`` is allowed for the same reason: a
|
|
green-CI noop pushes nothing and the HEAD is already CI-verified.
|
|
Routing it through AWAITING_CI is worse than a no-op — ci_status_poll
|
|
only resolves a SHA from a 'resolved'/'ci-not-ready' attempt, so a
|
|
'noop' attempt would sit in AWAITING_CI forever (the PR-41 deadlock).
|
|
"""
|
|
name = "no_path_implementing_to_reviewing_skips_ci"
|
|
# Events that DO push (head_sha advances) must route through AWAITING_CI.
|
|
# The set below does NOT push, so each is allowed as a direct edge.
|
|
no_push_events = {"implementer_dispute_reviewer", "implementer_noop_ci_green"}
|
|
for (frm, evt), to in TRANSITIONS.items():
|
|
if frm == "IMPLEMENTING" and to == "REVIEWING" and evt not in no_push_events:
|
|
return [
|
|
_violation(
|
|
name,
|
|
f"direct IMPLEMENTING → REVIEWING via {evt!r}; must "
|
|
f"route through AWAITING_CI (only allowed direct edges: "
|
|
f"{sorted(no_push_events)})",
|
|
)
|
|
]
|
|
# AWAITING_CI is the only path for push events; check reachability.
|
|
if "AWAITING_CI" not in reachable_from("IMPLEMENTING"):
|
|
return [_violation(name, "IMPLEMENTING cannot reach AWAITING_CI")]
|
|
return []
|
|
|
|
|
|
def check_terminal_states_have_no_exits() -> list[InvariantViolation]:
|
|
"""Invariant #2: terminal states are sinks — no outgoing transitions.
|
|
|
|
Note: ``STUCK`` has the ``operator_unstick`` exit, which is the
|
|
OPERATOR-driven escape hatch. Treated as "outgoing for
|
|
operator-driven events, but not for controller-driven events" —
|
|
we permit it.
|
|
"""
|
|
name = "terminal_states_have_no_exits"
|
|
out: list[InvariantViolation] = []
|
|
for (frm, evt), to in TRANSITIONS.items():
|
|
if frm in {"MERGED", "ABANDONED", "CREATED_PR"}:
|
|
out.append(
|
|
_violation(
|
|
name, f"terminal {frm!r} has transition via {evt!r} → {to!r}"
|
|
)
|
|
)
|
|
# STUCK's only allowed exit is operator_unstick.
|
|
if frm == "STUCK" and evt != "operator_unstick":
|
|
out.append(
|
|
_violation(
|
|
name,
|
|
f"STUCK has unauthorized exit via {evt!r} → {to!r}; "
|
|
f"only 'operator_unstick' is allowed",
|
|
)
|
|
)
|
|
return out
|
|
|
|
|
|
def check_tier_monotonic_non_decreasing() -> list[InvariantViolation]:
|
|
"""Invariant #3: when ESCALATING fires, the next tier is strictly
|
|
greater than the previous. Encoded structurally: ESCALATING has
|
|
only two events — escalate_next_tier_available (→ IMPLEMENTING,
|
|
interpreted by master as tier+1) and escalate_max_tier_exhausted
|
|
(→ ABANDONED).
|
|
"""
|
|
name = "tier_monotonic_non_decreasing"
|
|
out: list[InvariantViolation] = []
|
|
escalating_events = events_from("ESCALATING")
|
|
if set(escalating_events) != {
|
|
"escalate_next_tier_available",
|
|
"escalate_max_tier_exhausted",
|
|
}:
|
|
out.append(
|
|
_violation(
|
|
name,
|
|
f"ESCALATING has unexpected events {escalating_events}; "
|
|
f"expected {{'escalate_next_tier_available', "
|
|
f"'escalate_max_tier_exhausted'}}",
|
|
)
|
|
)
|
|
return out
|
|
|
|
|
|
def check_every_pr_workflow_includes_reviewing() -> list[InvariantViolation]:
|
|
"""Invariant #4: every path from DISCOVERED to MERGED must pass
|
|
through REVIEWING.
|
|
|
|
Per Hard Rule #1: every PR receives a fresh LLM review.
|
|
|
|
T5-7 chain: REVIEWING → APPROVED → MERGING → MERGED. The handoff
|
|
via APPROVED separates impl/review masters (which terminate at
|
|
APPROVED for a given workflow) from the singleton merge master
|
|
(which owns APPROVED → MERGING → MERGED). The invariant tightens
|
|
to enforce the full chain, not just the direct edge.
|
|
"""
|
|
name = "every_pr_workflow_includes_reviewing"
|
|
out: list[InvariantViolation] = []
|
|
# Check: MERGED only reachable from MERGING.
|
|
for (frm, evt), to in TRANSITIONS.items():
|
|
if to == "MERGED" and frm != "MERGING":
|
|
out.append(
|
|
_violation(
|
|
name, f"MERGED reachable from {frm!r} via {evt!r} (not MERGING)"
|
|
)
|
|
)
|
|
# Check: MERGING only reachable from APPROVED (the merge-master
|
|
# handoff state). Direct REVIEWING → MERGING or OPERATOR_ATTENTION
|
|
# → MERGING would re-introduce N-way merge contention.
|
|
for (frm, evt), to in TRANSITIONS.items():
|
|
if to == "MERGING" and frm != "APPROVED":
|
|
out.append(
|
|
_violation(
|
|
name,
|
|
f"MERGING reachable from {frm!r} via {evt!r}; only "
|
|
"APPROVED → MERGING is allowed (T5-7: singleton merge "
|
|
"master owns the merge POST)",
|
|
)
|
|
)
|
|
# Check: APPROVED only reachable from REVIEWING, OPERATOR_ATTENTION,
|
|
# or MERGING. REVIEWING/OPERATOR_ATTENTION guarantee a REVIEWING
|
|
# attempt happened. MERGING (via merge_interrupted) is itself only
|
|
# reachable from APPROVED, so the "every PR was reviewed" spirit
|
|
# holds transitively — the workflow was already APPROVED once.
|
|
allowed_approved_predecessors = {
|
|
"REVIEWING",
|
|
"OPERATOR_ATTENTION",
|
|
"MERGING",
|
|
}
|
|
for (frm, evt), to in TRANSITIONS.items():
|
|
if to == "APPROVED" and frm not in allowed_approved_predecessors:
|
|
out.append(
|
|
_violation(
|
|
name,
|
|
f"APPROVED reachable from {frm!r} via {evt!r}; allowed "
|
|
f"predecessors: {sorted(allowed_approved_predecessors)}",
|
|
)
|
|
)
|
|
return out
|
|
|
|
|
|
def check_conflict_resolving_bounded() -> list[InvariantViolation]:
|
|
"""Invariant #5: CONFLICT_RESOLVING transitions for 1st-time
|
|
resolution go to IMPLEMENTING; 2nd same-tier resolution goes to
|
|
ESCALATING; 3rd-or-later goes to STUCK. Structurally enforced
|
|
via exactly these named events.
|
|
"""
|
|
name = "conflict_resolving_bounded"
|
|
out: list[InvariantViolation] = []
|
|
expected_events = {
|
|
"conflict_resolved_first": "IMPLEMENTING",
|
|
"conflict_resolved_second_same_tier": "ESCALATING",
|
|
"conflict_repeated_three_plus": "STUCK",
|
|
"conflict_irreconcilable": "STUCK",
|
|
"pickup_exhausted": "STUCK",
|
|
}
|
|
actual = {
|
|
evt: to for (frm, evt), to in TRANSITIONS.items() if frm == "CONFLICT_RESOLVING"
|
|
}
|
|
for evt, expected_to in expected_events.items():
|
|
got_to = actual.get(evt)
|
|
if got_to != expected_to:
|
|
out.append(
|
|
_violation(
|
|
name,
|
|
f"CONFLICT_RESOLVING + {evt!r}: expected → {expected_to!r}; "
|
|
f"got → {got_to!r}",
|
|
)
|
|
)
|
|
unexpected = set(actual) - set(expected_events)
|
|
if unexpected:
|
|
out.append(
|
|
_violation(
|
|
name, f"CONFLICT_RESOLVING has unexpected event(s) {sorted(unexpected)}"
|
|
)
|
|
)
|
|
return out
|
|
|
|
|
|
def check_escalation_deterministic() -> list[InvariantViolation]:
|
|
"""Invariant #6: ESCALATING has exactly two transitions, both
|
|
deterministic. Combined with tier-monotonic-non-decreasing, this
|
|
means the escalation policy is static (min(tier+1, MAX_TIER)).
|
|
"""
|
|
name = "escalation_deterministic"
|
|
out: list[InvariantViolation] = []
|
|
actual = {evt: to for (frm, evt), to in TRANSITIONS.items() if frm == "ESCALATING"}
|
|
if actual != {
|
|
"escalate_next_tier_available": "IMPLEMENTING",
|
|
"escalate_max_tier_exhausted": "ABANDONED",
|
|
}:
|
|
out.append(
|
|
_violation(name, f"ESCALATING transitions are non-deterministic: {actual}")
|
|
)
|
|
return out
|
|
|
|
|
|
# Registry of all v1 load-bearing invariants. Tests iterate this.
|
|
LOAD_BEARING_INVARIANTS: dict[str, callable] = { # type: ignore[type-arg]
|
|
"no_path_implementing_to_reviewing_skips_ci": check_no_path_implementing_to_reviewing_skips_ci,
|
|
"terminal_states_have_no_exits": check_terminal_states_have_no_exits,
|
|
"tier_monotonic_non_decreasing": check_tier_monotonic_non_decreasing,
|
|
"every_pr_workflow_includes_reviewing": check_every_pr_workflow_includes_reviewing,
|
|
"conflict_resolving_bounded": check_conflict_resolving_bounded,
|
|
"escalation_deterministic": check_escalation_deterministic,
|
|
}
|
|
|
|
|
|
def check_all_invariants() -> list[InvariantViolation]:
|
|
"""Run every load-bearing invariant; return concatenated violations."""
|
|
out: list[InvariantViolation] = []
|
|
for check in LOAD_BEARING_INVARIANTS.values():
|
|
out.extend(check())
|
|
return out
|
|
|
|
|
|
__all__ = [
|
|
"EVENTS",
|
|
"Event",
|
|
"IllegalTransitionError",
|
|
"InvariantViolation",
|
|
"KNOWN_STATES",
|
|
"LOAD_BEARING_INVARIANTS",
|
|
"NON_TERMINAL_STATES",
|
|
"TERMINAL_STATES",
|
|
"TRANSITIONS",
|
|
"apply_event",
|
|
"check_all_invariants",
|
|
"events_from",
|
|
"reachable_from",
|
|
]
|