id: linter.model_shape kind: intent statement: “WHEN a spec file’s graph shape has passed, THE linter SHALL reject it if any transition lacks a guard or if the file declares a model without both a states section and a transitions section.”

Linter: Model Shape Check

Runs after linter.graph_shape — it needs the reference graph already proven acyclic before it can trust that a guard field pointing at a constraint isn’t secretly part of a cycle back through the model itself. Corresponds to invalid-states-diagnostician’s “unconstrained optionality” and “ad-hoc state machine” signals, made structural rather than advisory.

Purpose

Runs after linter.graph_shape — it needs the reference graph already proven acyclic before it can trust that a guard field pointing at a constraint isn’t secretly part of a cycle back through the model itself. Corresponds to invalid-states-diagnostician’s “unconstrained optionality” and “ad-hoc state machine” signals, made structural rather than advisory.

Constraints

| id | kind | expr | traces_to | satisfies | |————————|———–|———————————————————————————————–|————————————————| | guard_present | invariant | ∀ transition row: guard field is non-empty | [[linter.model_shape]] | | | model_sections_paired | invariant | if [[model.state]] exists then [[model.transition]] exists, and vice versa | [[linter.model_shape]] | | | every_state_used | invariant | ∀ state: state appears as from or to in ≥ 1 transition | [[linter.model_shape]] | | | every_transition_valid | invariant | ∀ transition: from ∈ states and to ∈ states | [[linter.model_shape]] | | | no_bool_state_field | invariant | no state or transition row has a column of boolean type | [[linter.model_shape]]| | | pairing_failure | effect | linter.model_shape.pairing_failure(detail) | [[linter.model_shape]] | [[errors.envelope_error_kind]] ∧ [[errors.exit_code_mapping]] ∧ [[errors.remediation_hint_present]] | | field_check_failure | effect | linter.model_shape.field_check_failure(detail) | [[linter.model_shape]] | [[errors.envelope_error_kind]] ∧ [[errors.exit_code_mapping]] ∧ [[errors.remediation_hint_present]] |

Model

States

• ungrouped
• pairing_checked
• states_checked
• passed
• pairing_failed (emits: [[linter.model_shape.pairing_failure]])
• field_check_failed (emits: [[linter.model_shape.field_check_failure]])

Transitions

Properties

Notes

Reference-typing reconciliation (2026-09-30, specodelic-cxq): the Constraints table’s traces_to cells previously pointed at the specodelic.md rows these checks re-own — a Constraint→Constraint target, which the Reference Typing table forbids (traces_to resolves to Intent only). Each now traces to this file’s own intent: specodelic.md keeps the corpus-wide statement of record, this file owns the checkable one (the “same claim, two altitudes” pattern the Notes below already use).

every_state_used and every_transition_valid are new relative to specodelic.md’s original list — guard_required only checked that a guard exists, not that the state machine around it is internally consistent (an unreferenced state, or a transition pointing at a state that was never declared). Both are structural prerequisites for the model_check transition in specodelic.md to mean anything: a TLA+ generator handed a dangling to field would either crash or silently model-check a different graph than the author wrote. Fourth candidate to fold back into specodelic.md’s constraint table.

no_bool_state_field restates specodelic.md’s no_boolean_columns scoped specifically to the model section, since that’s where a boolean column would actually manifest as an ad-hoc state machine (invalid-states-diagnostician’s central pathology) rather than merely a schema-hygiene issue elsewhere in the file.

Running tally of gaps found so far, all pending a pass back into specodelic.md: id_matches_file, ref_kind_compatible, single_root_reachable, every_state_used + every_transition_valid.

Requirements

Requirement: Property coverage mirror

Every property row SHALL be verified by exactly one dedicated scenario; ah sync SHALL derive one contract per VERIFIES link.

Scenario: missing_guard_rejected

• WHEN spec_file_with(transition_missing_guard: true)
• THEN check(file) == failed
• VERIFIES [[linter.model_shape.missing_guard_rejected]]

Scenario: unpaired_states_rejected

• WHEN spec_file_with(states_section_but_no_transitions: true)
• THEN check(file) == failed
• VERIFIES [[linter.model_shape.unpaired_states_rejected]]

Scenario: unreachable_state_rejected

• WHEN spec_file_with(declared_state_never_referenced: true)
• THEN check(file) == failed
• VERIFIES [[linter.model_shape.unreachable_state_rejected]]

Scenario: bad_edge_rejected

• WHEN spec_file_with(transition.to_not_in_states: true)
• THEN check(file) == failed
• VERIFIES [[linter.model_shape.bad_edge_rejected]]

Scenario: bool_column_rejected

• WHEN spec_file_with(state_row_having_bool_typed_column: true)
• THEN check(file) == failed
• VERIFIES [[linter.model_shape.bool_column_rejected]]

Scenario: well_formed_model_passes

• WHEN arbitrary_well_formed_state_machine()
• THEN check(file) == passed
• VERIFIES [[linter.model_shape.well_formed_model_passes]]

Scenario: pairing_failure_label_asserted

• WHEN pairing_failure_raised()
• THEN error_label == "linter.model_shape.pairing_failure" — renaming the label touches the error Constraint, this property, and its note together (EDGE-002)
• VERIFIES [[linter.model_shape.pairing_failure_label_asserted]]

Scenario: field_check_failure_label_asserted

• WHEN field_check_failure_raised()
• THEN error_label == "linter.model_shape.field_check_failure" — renaming the label touches the error Constraint, this property, and its note together (EDGE-002)
• VERIFIES [[linter.model_shape.field_check_failure_label_asserted]]