Diagnostics code reference

Diagnostic codes are stable identifiers used by pyfcstm inspect, CI filters, IDE integrations, and LLM repair prompts. The authoritative registry is the loaded pyfcstm.diagnostics.codes.CODE_REGISTRY object. Raw codes.yaml entries may omit emit_tier or capability; the loader fills those defaults as static_pipeline and pure_static.

This page is a reference, not a tutorial. Use it when you already have a code value from inspect output and need to know what it means, which report fields are stable, which pipeline can emit it, and how to repair or explain it.

How to read one diagnostic

A diagnostic object combines a stable identifier with source-location and repair context:

Diagnostic object keys

Key	Meaning
code	Stable identifier such as W_COMBO_DUPLICATE_EVENT.
severity	error blocks model construction; warning flags risky or suspicious design; info records a non-blocking observation.
message	Human-readable short explanation.
span	Source range when the analyzer can point to a concrete object.
refs	Structured payload used by tools and LLM repair prompts. Each code below lists the expected fields.
suggested_fix	Optional edit metadata when the registry can describe a safe local edit shape.

Emission tiers

Emit tiers

Tier	Meaning
static_pipeline	Produced by the default static inspect/model diagnostics path.
verify_pipeline	Produced only when closed, policy-budgeted structural or SMT-local verify algorithms run, normally through --enable-verify.
lookup_api	Produced by explicit resolver APIs, not by default static inspect output.
partial_static_pipeline	Registry contract exists, but not every frontend/backend currently emits it.
catalog_only	Compatibility contract only; current normal pyfcstm paths should not emit it.

Example kinds

Each code below has at least three visible examples or boundary examples. The source also carries hidden diagnostics-example markers so python tools/check_diagnostics_reference_docs.py --check can verify coverage.

Example kind labels

Kind	Meaning
repro_cli	Intended to be reproducible as a successful inspect report; use pyfcstm inspect -i <file> --format json and read diagnostics[].
cli_error	Intended to be reproducible as a controlled CLI/model-validation error. Current inspect formats exit non-zero before producing a successful JSON report, so assert stderr and exit status rather than diagnostics[].
repro_api	Intended to be reproducible through an explicit Python API call.
verify_opt_in	Requires optional verify integration and may depend on solver policy or timeout.
boundary_only	Documents a repair or anti-pattern boundary rather than a separate CLI trigger.
compatibility_only	Documents historical or cross-version behavior that current normal paths should not emit.

Machine coverage check

Run this repository-local maintenance check after editing this page or the code registry:

python tools/check_diagnostics_reference_docs.py --check

The check verifies code-set, severity, emit tier, capability, span object, refs schema, bilingual coverage, per-code reproduction-boundary markers, and per-code example-marker counts. It does not prove that examples are semantically distinct; reviewer sampling remains part of the PR acceptance gate.

Complete diagnostic code catalog

This catalog is synchronized with pyfcstm.diagnostics.codes.CODE_REGISTRY. The hidden diagnostics-meta and diagnostics-example source markers are checked by python tools/check_diagnostics_reference_docs.py --check.

Registry summary

Code	Severity	Emit tier	Capability	Span object
E_UNDEFINED_VAR	error	static_pipeline	pure_static	expression
E_DUPLICATE_VAR	error	static_pipeline	pure_static	variable_declaration
E_MISSING_STATE	error	static_pipeline	pure_static	state_identifier
E_DUPLICATE_STATE	error	static_pipeline	pure_static	state_identifier
E_EVENT_REF_INVALID	error	lookup_api	pure_static	event_declaration
E_EVENT_NOT_FOUND	error	lookup_api	pure_static	event_declaration
E_DANGLING_TRANSITION	error	static_pipeline	pure_static	transition
E_COMBO_TRIGGER_NOT_EXPANDED	error	catalog_only	pure_static	transition
W_COMBO_RESERVED_PREFIX_STATE_KIND	warning	partial_static_pipeline	pure_static	state_identifier
W_COMBO_RELAY_PSEUDO_HAS_ACTIONS	warning	partial_static_pipeline	pure_static	state_identifier
I_COMBO_PSEUDO_NAME_EXTENDED	info	partial_static_pipeline	pure_static	state_identifier
E_COMBO_PSEUDO_NAME_COLLISION	error	static_pipeline	pure_static	state_identifier
W_COMBO_DUPLICATE_EVENT	warning	static_pipeline	pure_static	transition
W_COMBO_GUARD_CONST_TRUE	warning	static_pipeline	requires_solver	guard_expression
W_COMBO_GUARD_CONST_FALSE	warning	static_pipeline	requires_solver	guard_expression
W_COMBO_GUARD_PREFIX_IMPLIED	warning	static_pipeline	requires_solver	guard_expression
W_COMBO_GUARD_PREFIX_CONTRADICTS	warning	static_pipeline	requires_solver	guard_expression
E_TYPE_MISMATCH	error	partial_static_pipeline	pure_static	expression
E_FORCED_TRANSITION_EXPANSION	error	static_pipeline	pure_static	transition
E_INITIAL_TRANSITION_INVALID	error	static_pipeline	pure_static	transition
E_DUPLICATE_FUNCTION_NAME	error	static_pipeline	pure_static	named_action_declaration
E_DURING_ASPECT_INVALID	error	static_pipeline	pure_static	lifecycle_action
E_PSEUDO_NOT_LEAF	error	static_pipeline	pure_static	state_identifier
E_NAMED_FUNCTION_REF_CYCLE	error	static_pipeline	pure_static	named_action_declaration
E_NAMED_FUNCTION_REF_NOT_FOUND	error	static_pipeline	pure_static	named_action_declaration
E_IMPORT_NOT_FOUND	error	static_pipeline	pure_static	import_statement
E_IMPORT_CIRCULAR	error	static_pipeline	pure_static	import_statement
E_IMPORT_ALIAS_CONFLICT	error	static_pipeline	pure_static	import_statement
E_IMPORT_DUPLICATE_MAPPING	error	static_pipeline	pure_static	import_statement
E_IMPORT_MAPPING_INVALID	error	static_pipeline	pure_static	import_statement
W_UNREACHABLE_STATE	warning	static_pipeline	pure_static	state_identifier
W_GUARD_CONST_FALSE	warning	static_pipeline	const_fold	guard_expression
W_GUARD_CONST_TRUE	warning	static_pipeline	const_fold	guard_expression
W_DURING_CONST_ASSIGN	warning	static_pipeline	const_fold	lifecycle_action
W_UNUSED_EVENT	warning	static_pipeline	pure_static	event_declaration
W_DEADLOCK_LEAF	warning	static_pipeline	pure_static	state_identifier
W_INITIAL_UNCONDITIONAL_MISSING	warning	static_pipeline	pure_static	composite_block
W_FORCED_NEVER_EXPANDS	warning	static_pipeline	pure_static	transition
W_DEAD_NAMED_ACTION	warning	static_pipeline	pure_static	named_action_declaration
W_UNREFERENCED_VAR	warning	static_pipeline	pure_static	variable_declaration
I_UNREFERENCED_VAR_MAYBE_ABSTRACT	info	static_pipeline	pure_static	variable_declaration
W_GUARD_VARS_NEVER_CHANGE	warning	static_pipeline	pure_static	guard_expression
W_UNWRITTEN_READ_VAR	warning	static_pipeline	pure_static	variable_declaration
W_WRITE_ONLY_VAR	warning	static_pipeline	pure_static	variable_declaration
W_REDUNDANT_TRANSITION	warning	static_pipeline	pure_static	transition
W_SELF_TRANSITION_NOP	warning	static_pipeline	pure_static	transition
W_EFFECT_SELF_ASSIGN	warning	static_pipeline	pure_static	effect_statement
W_FORCED_OVERRIDES_NORMAL	warning	static_pipeline	pure_static	transition
W_SHADOWED_EVENT	warning	static_pipeline	pure_static	event_declaration
W_NAMED_ACTION_SHADOWS_ANCESTOR	warning	static_pipeline	pure_static	named_action_declaration
W_LITERAL_TYPE_NARROWING	warning	static_pipeline	pure_static	expression
W_NUMERIC_LITERAL_OUT_OF_TARGET_RANGE	warning	static_pipeline	pure_static	expression
W_NUMERIC_CONSTANT_DIVISION_BY_ZERO	warning	static_pipeline	const_fold	expression
W_NUMERIC_SHIFT_COUNT_OUT_OF_TARGET_RANGE	warning	static_pipeline	const_fold	expression
W_NUMERIC_FLOAT_BITWISE	warning	static_pipeline	pure_static	expression
W_ASPECT_NO_DESCENDANT_LEAF	warning	static_pipeline	pure_static	lifecycle_action
W_HIGH_VAR_TO_LEAF_RATIO	warning	static_pipeline	pure_static	composite_block
W_DEEP_HIERARCHY	warning	static_pipeline	pure_static	state_identifier
W_LARGE_COMPOSITE	warning	static_pipeline	pure_static	composite_block
I_TRANSITION_TO_SELF_VIA_PARENT	info	static_pipeline	pure_static	transition
I_TRANSITION_NEVER_EVENT_TRIGGERED	info	static_pipeline	pure_static	transition
I_NONTRIVIAL_SCC	info	verify_pipeline	pure_static	state_identifier
W_TOPOLOGICAL_NOEXIT	warning	verify_pipeline	pure_static	state_identifier
I_TOPOLOGICAL_NON_TERMINATING	info	verify_pipeline	pure_static	state_identifier
W_EVENT_UNREACHABLE_EMIT	warning	verify_pipeline	pure_static	event_declaration
W_DEAD_GUARD	warning	verify_pipeline	requires_solver	guard_expression
W_GUARD_TAUTOLOGY	warning	verify_pipeline	requires_solver	guard_expression
W_FORCED_GUARD_UNSAT	warning	verify_pipeline	requires_solver	guard_expression
W_EFFECT_SMT_NO_OP	warning	verify_pipeline	requires_solver	effect_statement
I_EFFECT_GUARD_CONTRADICT	info	verify_pipeline	requires_solver	effect_statement
W_TRANSITION_SHADOWED	warning	verify_pipeline	requires_solver	transition
I_ENTER_DURING_CONTRADICT	info	verify_pipeline	requires_solver	lifecycle_action
W_COMPOSITE_INIT_INCOMPLETE	warning	verify_pipeline	requires_solver	composite_block

Names, variables, types, and imports

E_UNDEFINED_VAR

Registry facts. Severity error; emit tier static_pipeline; capability pure_static; span object expression.

Meaning. A guard, effect, or lifecycle-action block references a name that was never declared with a top-level def statement.

LLM repair summary. A variable identifier appears in an expression (guard, effect, or action block) but has not been declared with def at the file top, has not been assigned earlier in the same block (so the block-local temporary path doesn’t apply), and is not a known function name. The model refuses to bind unknown identifiers because the generated code would not compile.

Refs schema

Field	Type	Required	Meaning
var_name	str	yes	The undeclared identifier as it appeared in the source.
referenced_in	str	yes	Which kind of block contained the reference. (enum: guard, effect, enter, during, exit, during_aspect, init)
state_path	str_or_null	no	Dotted path of the state that owns the offending block, when the reference is inside a state body (not a guard/effect on a transition).
expr_text	str_or_null	no	Original expression text containing the reference.
is_temporary	bool	no	True when the identifier looked like a block-local temporary (the read occurred before the variable was assigned within the same enter / during / exit / effect block). Layer 2 merges what jsfcstm previously emitted as fcstm.readBeforeAssignTemporary into this single E_* code plus this flag. Defaults to False / absent for “real” undefined variables that have no matching def declaration anywhere.

Example 1 (cli_error) — reproduction boundary. This source shape reproduces a controlled model-validation failure through pyfcstm inspect. Current CLI formats exit non-zero before a successful inspect JSON report is produced, so assert the stderr/exit status rather than expecting this code inside diagnostics[].

def int x = 0;
state Root { state A; state B; A -> B : if [unknown_var > 0]; }

Example 2 (boundary_only) — repair direction for E_UNDEFINED_VAR. A typical repair is add_definition on file_top: If the variable is genuinely program state, declare it with def <type> <name> = <initial>; at the file top so the generated runtime allocates storage for it.

Example 3 (boundary_only) — anti-pattern boundary for E_UNDEFINED_VAR. Do not declare the variable inside an action block expecting it to leak out — block-local temps are discarded at block exit.

E_DUPLICATE_VAR

Registry facts. Severity error; emit tier static_pipeline; capability pure_static; span object variable_declaration.

Meaning. A top-level def statement re-declares an identifier that was already defined earlier in the file.

LLM repair summary. Two def declarations at the file top use the same variable name. The model allocates one storage slot per name, so a duplicate definition is ambiguous.

Refs schema

Field	Type	Required	Meaning
var_name	str	yes	The duplicated identifier.
previous_span	Span	no	Source position of the first declaration.

Example 1 (cli_error) — reproduction boundary. This source shape reproduces a controlled model-validation failure through pyfcstm inspect. Current CLI formats exit non-zero before a successful inspect JSON report is produced, so assert the stderr/exit status rather than expecting this code inside diagnostics[].

def int x = 0;
def int x = 1;
state Root { state A; }

Example 2 (boundary_only) — repair direction for E_DUPLICATE_VAR. A typical repair is drop_duplicate on variable_definition: If both definitions are meant to declare the same logical variable, keep the first one and delete the second.

Example 3 (boundary_only) — anti-pattern boundary for E_DUPLICATE_VAR. Do not assume the second def overrides the first — the generated runtime treats this as an error and refuses to compile.

E_TYPE_MISMATCH

Registry facts. Severity error; emit tier partial_static_pipeline; capability pure_static; span object expression.

Meaning. A guard, effect, or assignment uses an expression whose type does not match the expected category (arithmetic vs boolean).

LLM repair summary. An expression mixes an arithmetic and a boolean subexpression in a way the grammar does not allow. num_expression and cond_expression are strictly separated; comparison operators bridge them, ternary ? : converts boolean → arithmetic.

Refs schema

Field	Type	Required	Meaning
expected	str	yes	Expected category. One of: ‘numeric’, ‘boolean’.
actual	str	yes	Actual category produced by the expression.
expr_text	str	yes	Original expression text.

Example 1 (boundary_only) — reproduction boundary. This registry contract is intentionally ahead of full frontend/backend emission parity. Treat the source as the supported boundary shape and confirm the current emitter before promising default CLI JSON output.

def int x = 0;
state Root { state A; state B; A -> B : if [x]; }

Example 2 (boundary_only) — repair direction for E_TYPE_MISMATCH. A typical repair is wrap_in_ternary on expression: If you wanted to assign a boolean test, wrap it as (cond) ? 1 : 0 so the right-hand side is arithmetic.

Example 3 (boundary_only) — anti-pattern boundary for E_TYPE_MISMATCH. Do not rely on numeric → boolean implicit coercion; the generated runtimes treat the two domains as distinct.

E_DUPLICATE_FUNCTION_NAME

Registry facts. Severity error; emit tier static_pipeline; capability pure_static; span object named_action_declaration.

Meaning. Two named lifecycle actions (enter / during / exit / during-aspect) within the same state share the same name. Named actions are referenced via ref <name> and must be uniquely identifiable.

LLM repair summary. Two named action / function blocks share the same name within the same scope. Named blocks must be uniquely identifiable so ref lookups can bind to a single definition.

Refs schema

Field	Type	Required	Meaning
function_name	str	yes	The duplicated named-action name.
state_path	str	yes	Dotted path of the state declaring the duplicates.
stage	str	yes	Lifecycle stage where the duplicate appears. (enum: enter, during, exit, during_aspect)

Example 1 (cli_error) — reproduction boundary. This source shape reproduces a controlled model-validation failure through pyfcstm inspect. Current CLI formats exit non-zero before a successful inspect JSON report is produced, so assert the stderr/exit status rather than expecting this code inside diagnostics[].

state Root {
    state A {
        enter Foo { }
        enter Foo { }
    }
}

Example 2 (boundary_only) — repair direction for E_DUPLICATE_FUNCTION_NAME. A typical repair is rename_one on named_action: Give one of the named blocks a distinct identifier so ref <name> calls resolve unambiguously.

Example 3 (boundary_only) — anti-pattern boundary for E_DUPLICATE_FUNCTION_NAME. Do not assume the second declaration shadows the first — the resolver treats this as a hard error.

E_NAMED_FUNCTION_REF_CYCLE

Registry facts. Severity error; emit tier static_pipeline; capability pure_static; span object named_action_declaration.

Meaning. A lifecycle action ref chain forms a cycle and therefore never reaches a concrete or abstract action implementation.

LLM repair summary. An enter ref ... / exit ref ... / during ref ... clause ultimately points back to itself through one or more named actions.

Refs schema

Field	Type	Required	Meaning
ref_path	str	yes	Dot-separated action path where cycle validation started.
cycle_path	str	yes	Dot-separated action path chain that closes the cycle.
reason	str	yes	Short tag describing the failure. (enum: action_ref_cycle)

Example 1 (cli_error) — reproduction boundary. This source shape reproduces a controlled model-validation failure through pyfcstm inspect. Current CLI formats exit non-zero before a successful inspect JSON report is produced, so assert the stderr/exit status rather than expecting this code inside diagnostics[].

state Root {
    state A {
        enter ref First;
        enter First ref Second;
        enter Second ref First;
    }
}

Example 2 (boundary_only) — repair direction for E_NAMED_FUNCTION_REF_CYCLE. A typical repair is break_ref_cycle on action_ref: Replace one link in the cycle with a concrete action block or an abstract action declaration so the reference chain terminates.

Example 3 (boundary_only) — anti-pattern boundary for E_NAMED_FUNCTION_REF_CYCLE. Do not execute or render cyclic lifecycle references; reject the model before runtime execution.

E_NAMED_FUNCTION_REF_NOT_FOUND

Registry facts. Severity error; emit tier static_pipeline; capability pure_static; span object named_action_declaration.

Meaning. A ref lifecycle action could not resolve its target named action. Either the path walks through a state that does not exist, or the final segment is not a named action defined inside the resolved state.

LLM repair summary. An enter ref ... / exit ref ... / during ref ... clause points at a named action that does not exist. The resolver could not find a matching named block in the indicated scope.

Refs schema

Field	Type	Required	Meaning
ref_path	str	yes	Dotted path of the unresolved reference.
reason	str	yes	Short tag describing the resolution failure. (enum: state_not_found, named_function_not_found)
missing_segment	str_or_null	no	The path segment that failed to resolve. For ‘state_not_found’ this is the state name that does not exist under the parent path; for ‘named_function_not_found’ this is the action name searched for in the resolved state.

Example 1 (cli_error) — reproduction boundary. This source shape reproduces a controlled model-validation failure through pyfcstm inspect. Current CLI formats exit non-zero before a successful inspect JSON report is produced, so assert the stderr/exit status rather than expecting this code inside diagnostics[].

state Root {
    state A {
        enter ref NoSuch.NoSuch;
    }
}

Example 2 (boundary_only) — repair direction for E_NAMED_FUNCTION_REF_NOT_FOUND. A typical repair is fix_ref_path on action_ref: Confirm the dotted ref path matches a real named action. Use / to anchor at the root, or a relative name for the current state.

Example 3 (boundary_only) — anti-pattern boundary for E_NAMED_FUNCTION_REF_NOT_FOUND. Do not silently swap ref with an inline block — that loses the deduplication that ref was meant to provide.

E_IMPORT_NOT_FOUND

Registry facts. Severity error; emit tier static_pipeline; capability pure_static; span object import_statement.

Meaning. An import statement points at a source file that cannot be found, cannot be read, or fails to parse.

LLM repair summary. An import target could not be resolved. Inspect refs.reason to branch the fix: file_not_found means the path is wrong or the file does not exist; read_error means the file exists but the I/O layer rejected it (permissions / encoding); parse_error means the file was loaded but is not valid FCSTM DSL; no_root_state means the file parses but declares no state Root { ... } block. The four reasons need different fixes — do not collapse them. Cross-end note (I2 from PR #115 final review): jsfcstm currently only distinguishes file_not_found and no_root_state; its workspace index treats I/O failures and parse failures alike as missing and emits file_not_found for both. When consuming jsfcstm-side diagnostics, treat file_not_found as “any pre-no_root_state failure” and inspect the imported file directly to disambiguate read vs parse failures.

Refs schema

Field	Type	Required	Meaning
source_path	str	yes	The source-path token from the import statement, exactly as it appeared in the DSL.
alias	str	yes	The alias under which the import was declared.
host_state_path	str	yes	Dotted path of the composite state hosting the import statement.
reason	str	yes	Why resolution failed. (enum: file_not_found, read_error, parse_error, no_root_state)

Example 1 (cli_error) — reproduction boundary. This source shape reproduces a controlled model-validation failure through pyfcstm inspect. Current CLI formats exit non-zero before a successful inspect JSON report is produced, so assert the stderr/exit status rather than expecting this code inside diagnostics[].

state System {
    import "missing.fcstm" as Sub;
}

Example 2 (boundary_only) — repair direction for E_IMPORT_NOT_FOUND. A typical repair is fix_path on import_statement: For file_not_found, adjust the source_path to a real file relative to the host file, or remove the import if the sub-machine is no longer required.

Example 3 (boundary_only) — anti-pattern boundary for E_IMPORT_NOT_FOUND. Do not silently rename the alias to dodge the missing file.

E_IMPORT_CIRCULAR

Registry facts. Severity error; emit tier static_pipeline; capability pure_static; span object import_statement.

Meaning. A cycle was detected while resolving import statements between two or more state-machine source files.

LLM repair summary. Two or more state-machine files import each other transitively. The compiler refuses to resolve cycles to keep the merged hierarchy tractable.

Refs schema

Field	Type	Required	Meaning
source_path	str	yes	The source-path token that closed the cycle.
alias	str	yes	The alias under which the cyclic import was declared.
host_state_path	str	yes	Dotted path of the composite state hosting the import.
cycle_chain	list[str]	yes	Ordered list of file paths that participate in the cycle, starting and ending at the same file.

Example 1 (cli_error) — reproduction boundary. This source shape reproduces a controlled model-validation failure through pyfcstm inspect. Current CLI formats exit non-zero before a successful inspect JSON report is produced, so assert the stderr/exit status rather than expecting this code inside diagnostics[].

# a.fcstm
state A { import "b.fcstm" as B; }
# b.fcstm
state B { import "a.fcstm" as A; }

Example 2 (boundary_only) — repair direction for E_IMPORT_CIRCULAR. A typical repair is refactor on import_statement: Break the cycle by extracting the shared state(s) into a third file that both ends import without depending on each other.

Example 3 (boundary_only) — anti-pattern boundary for E_IMPORT_CIRCULAR. Do not duplicate the imported states inline to break the cycle — that defeats the purpose of imports.

E_IMPORT_ALIAS_CONFLICT

Registry facts. Severity error; emit tier static_pipeline; capability pure_static; span object import_statement.

Meaning. An import alias clashes with an existing child state (or with another import alias) under the same composite state.

LLM repair summary. The import alias collides with an already-defined name in the same composite scope. The merged hierarchy cannot have two children sharing a name.

Refs schema

Field	Type	Required	Meaning
alias	str	yes	The conflicting alias name.
host_state_path	str	yes	Dotted path of the composite state hosting the import.
conflicting_kind	str	yes	What the alias clashed with. (enum: existing_substate, previous_import_alias)

Example 1 (cli_error) — reproduction boundary. This source shape reproduces a controlled model-validation failure through pyfcstm inspect. Current CLI formats exit non-zero before a successful inspect JSON report is produced, so assert the stderr/exit status rather than expecting this code inside diagnostics[].

state System {
    state Worker;
    import "worker.fcstm" as Worker;
}

Example 2 (boundary_only) — repair direction for E_IMPORT_ALIAS_CONFLICT. A typical repair is rename_alias on import_statement: Pick a unique alias for the import; references to the imported machine elsewhere in the file must follow the new alias.

Example 3 (boundary_only) — anti-pattern boundary for E_IMPORT_ALIAS_CONFLICT. Do not silently drop one of the conflicting definitions.

E_IMPORT_DUPLICATE_MAPPING

Registry facts. Severity error; emit tier static_pipeline; capability pure_static; span object import_statement.

Meaning. Two or more mapping clauses under the same import { ... } block target the same source name (event or variable), or two source names target the same host name.

LLM repair summary. An import-mapping block contains a duplicate source or target name. Each source identifier can be mapped at most once; each target host slot can receive at most one source.

Refs schema

Field	Type	Required	Meaning
alias	str	yes	The import alias whose mapping is duplicated.
mapping_kind	str	yes	Which mapping flavor was duplicated. (enum: event, variable)
duplicated_name	str	yes	The source-side or target-side name that appears more than once.
direction	str	yes	Which side of the mapping was duplicated. (enum: source_duplicated, target_duplicated)
host_state_path	str	yes	Dotted path of the composite state hosting the import.

Example 1 (cli_error) — reproduction boundary. This source shape reproduces a controlled model-validation failure through pyfcstm inspect. Current CLI formats exit non-zero before a successful inspect JSON report is produced, so assert the stderr/exit status rather than expecting this code inside diagnostics[].

state System {
    import "sub.fcstm" as Sub {
        def x = a;
        def x = b;
    }
}

Example 2 (boundary_only) — repair direction for E_IMPORT_DUPLICATE_MAPPING. A typical repair is drop_duplicate on mapping_clause: Delete the duplicated mapping line — keep the intended one.

Example 3 (boundary_only) — anti-pattern boundary for E_IMPORT_DUPLICATE_MAPPING. Do not merge mappings by concatenating their values.

E_IMPORT_MAPPING_INVALID

Registry facts. Severity error; emit tier static_pipeline; capability pure_static; span object import_statement.

Meaning. An import-mapping clause refers to a source name that does not exist in the imported machine, uses an invalid selector / template, or points at a host target that cannot host the mapped element.

LLM repair summary. An import { ... } mapping clause is malformed or points at a non-existent element on the source side / a non-receivable element on the host side.

Refs schema

Field	Type	Required	Meaning
alias	str	yes	The import alias whose mapping is malformed.
mapping_kind	str	yes	Mapping flavor. (enum: event, variable)
host_state_path	str	yes	Dotted path of the composite state hosting the import.
reason	str	yes	Short tag describing the failure mode. (enum: source_not_found, target_invalid, selector_invalid, template_invalid, empty_path, host_root_mismatch)
detail	str	yes	Human-readable specifics of the mapping failure (mapping text, selector / template literal, or path that failed to resolve).

Example 1 (cli_error) — reproduction boundary. This source shape reproduces a controlled model-validation failure through pyfcstm inspect. Current CLI formats exit non-zero before a successful inspect JSON report is produced, so assert the stderr/exit status rather than expecting this code inside diagnostics[].

state System {
    import "sub.fcstm" as Sub {
        def x = no_such_var;
    }
}

Example 2 (boundary_only) — repair direction for E_IMPORT_MAPPING_INVALID. A typical repair is fix_source on mapping_clause: Update the source-side name to match a real def / event in the imported file.

Example 3 (boundary_only) — anti-pattern boundary for E_IMPORT_MAPPING_INVALID. Do not invent fake source names to make the selector match.

States and transitions

E_MISSING_STATE

Registry facts. Severity error; emit tier static_pipeline; capability pure_static; span object state_identifier.

Meaning. A transition target references a state path that cannot be resolved in the surrounding hierarchy.

LLM repair summary. A transition references a state name that does not exist in the machine. The transition target / source must resolve to a state declared in this file or imported.

Refs schema

Field	Type	Required	Meaning
state_path	str	yes	The unresolved dotted state path.
referenced_from	str_or_null	no	Dotted path of the state from which the reference was made.
reason	str	no	Short tag describing the resolution failure mode. (enum: not_found, parent_missing, ambiguous, event_path_not_found)

Example 1 (cli_error) — reproduction boundary. This source shape reproduces a controlled model-validation failure through pyfcstm inspect. Current CLI formats exit non-zero before a successful inspect JSON report is produced, so assert the stderr/exit status rather than expecting this code inside diagnostics[].

state Root { state A; A -> NoSuch; }

Example 2 (boundary_only) — repair direction for E_MISSING_STATE. A typical repair is fix_typo on transition: If the name was meant to refer to an existing state, correct the spelling. refs.state_name carries the missing token.

Example 3 (boundary_only) — anti-pattern boundary for E_MISSING_STATE. Do not silently delete the transition; the original intent of the missing state is lost.

E_DUPLICATE_STATE

Registry facts. Severity error; emit tier static_pipeline; capability pure_static; span object state_identifier.

Meaning. Two states share the same name within the same parent scope.

LLM repair summary. Two state declarations under the same composite parent use the same name. State names must be unique inside their immediate composite scope.

Refs schema

Field	Type	Required	Meaning
state_name	str	yes	The duplicated state name.
parent_path	str	yes	Dotted path of the parent that contains both states.
previous_span	Span	no	Source position of the first declaration.

Example 1 (cli_error) — reproduction boundary. This source shape reproduces a controlled model-validation failure through pyfcstm inspect. Current CLI formats exit non-zero before a successful inspect JSON report is produced, so assert the stderr/exit status rather than expecting this code inside diagnostics[].

state Root { state A; state A; }

Example 2 (boundary_only) — repair direction for E_DUPLICATE_STATE. A typical repair is drop_duplicate on state_definition: If both declarations describe the same logical state, keep one and remove the other (merge any actions/transitions onto the survivor).

Example 3 (boundary_only) — anti-pattern boundary for E_DUPLICATE_STATE. Do not assume the second declaration overrides the first — duplicate state names produce a hard error.

E_DANGLING_TRANSITION

Registry facts. Severity error; emit tier static_pipeline; capability pure_static; span object transition.

Meaning. A transition cannot resolve either its source or its target.

LLM repair summary. A transition’s source or target points at a state that exists neither in the local composite scope nor in any ancestor scope. The transition cannot be wired into the dispatch graph.

Refs schema

Field	Type	Required	Meaning
src	str_or_null	no	Raw source state expression as written in the DSL.
tgt	str_or_null	no	Raw target state expression as written in the DSL.
reason	str	yes	Short tag describing the dangling reason. (enum: src_not_found, tgt_not_found, both_not_found)

Example 1 (cli_error) — reproduction boundary. This source shape reproduces a controlled model-validation failure through pyfcstm inspect. Current CLI formats exit non-zero before a successful inspect JSON report is produced, so assert the stderr/exit status rather than expecting this code inside diagnostics[].

state Root { state A; NoSuch -> A; }

Example 2 (boundary_only) — repair direction for E_DANGLING_TRANSITION. A typical repair is fix_typo on transition: If the dangling name is misspelled, correct it. refs.state_path carries the location of the offending transition.

Example 3 (boundary_only) — anti-pattern boundary for E_DANGLING_TRANSITION. Do not pretend the transition resolves to [*] — that has a specific entry/exit semantics.

E_INITIAL_TRANSITION_INVALID

Registry facts. Severity error; emit tier static_pipeline; capability pure_static; span object transition.

Meaning. A composite state either lacks an entry transition ([*] -> child) or declares one whose target is not a direct child of the composite.

LLM repair summary. A composite state lacks a valid [*] -> Child initial transition, or its declared initial target is not actually a child of this composite. The runtime cannot decide which child to enter when this composite is activated.

Refs schema

Field	Type	Required	Meaning
composite_path	str	yes	Dotted path of the offending composite state.
reason	str	yes	Short tag describing the failure. (enum: missing_entry, target_not_child)

Example 1 (cli_error) — reproduction boundary. This source shape reproduces a controlled model-validation failure through pyfcstm inspect. Current CLI formats exit non-zero before a successful inspect JSON report is produced, so assert the stderr/exit status rather than expecting this code inside diagnostics[].

state Root { state Outer { state Inner; } }

Example 2 (boundary_only) — repair direction for E_INITIAL_TRANSITION_INVALID. A typical repair is add_initial_transition on composite_state: Add [*] -> <ChildName>; inside the composite, picking a direct substate as the entry point.

Example 3 (boundary_only) — anti-pattern boundary for E_INITIAL_TRANSITION_INVALID. Do not rely on a default ordering of substates; the runtime requires an explicit initial transition.

W_REDUNDANT_TRANSITION

Registry facts. Severity warning; emit tier static_pipeline; capability pure_static; span object transition.

Meaning. Multiple transitions share the same source, target, event, guard, and effect. Forced and normal transitions with the same behavioral key are counted here as redundant and may also emit W_FORCED_OVERRIDES_NORMAL.

LLM repair summary. These transitions are indistinguishable by source, target, event, guard, and effect, so later copies do not add behavior.

Refs schema

Field	Type	Required	Meaning
from_path	str	yes	Dotted source state path.
to_path	str	yes	Dotted target state path.
duplicate_spans	list[Span]	yes	Source spans for the duplicate transition declarations, using null for declarations whose span is unavailable.
transition_index	int	no	Zero-based index in parent-first model transition order, including expanded forced transitions at their declaring state before ordinary transitions and descendant-state transitions. This is used only as a source-range disambiguation hint when spans are unavailable.

Example 1 (repro_cli) — reproduction boundary. This diagnostic can appear in a successful inspect report. Reproduce it with pyfcstm inspect -i <file> --format json and read the diagnostics[] array.

state Root {
    state A;
    state B;
    [*] -> A;
    A -> B :: Go;
    A -> B :: Go;
}

Example 2 (boundary_only) — repair direction for W_REDUNDANT_TRANSITION. A typical repair is remove_duplicate on transition: Keep one transition and remove redundant copies.

Example 3 (boundary_only) — anti-pattern boundary for W_REDUNDANT_TRANSITION. Do not keep duplicate transitions as comments.

W_SELF_TRANSITION_NOP

Registry facts. Severity warning; emit tier static_pipeline; capability pure_static; span object transition.

Meaning. A leaf self transition has no event, guard, effect, own lifecycle action, or ancestor aspect action.

LLM repair summary. The transition points from a state to itself and has no trigger, guard, effect, or re-entry lifecycle behavior, so it does not model useful behavior.

Refs schema

Field	Type	Required	Meaning
state_path	str	yes	Dotted path of the state with the no-op self transition.
from_path	str	no	Dotted source state path.
to_path	str	no	Dotted target state path.
transition_span	Span	no	Source span of the no-op self transition when available.
transition_index	int	no	Zero-based index in parent-first model transition order, including expanded forced transitions at their declaring state before ordinary transitions and descendant-state transitions. This is used only as a source-range disambiguation hint when spans are unavailable.

Example 1 (repro_cli) — reproduction boundary. This diagnostic can appear in a successful inspect report. Reproduce it with pyfcstm inspect -i <file> --format json and read the diagnostics[] array.

state Root {
    state A;
    [*] -> A;
    A -> A;
}

Example 2 (boundary_only) — repair direction for W_SELF_TRANSITION_NOP. A typical repair is remove_transition on transition: Remove the no-op transition.

Example 3 (boundary_only) — anti-pattern boundary for W_SELF_TRANSITION_NOP. Do not apply this warning to self transitions whose re-entry would run enter, during, exit, or ancestor aspect actions.

I_TRANSITION_TO_SELF_VIA_PARENT

Registry facts. Severity info; emit tier static_pipeline; capability pure_static; span object transition.

Meaning. A composite state transitions to itself, which can intentionally force a re-entry path through child initialization and lifecycle actions.

LLM repair summary. This is an informational observation rather than a defect: a composite self-transition may be a deliberate reinitialization pattern.

Refs schema

Field	Type	Required	Meaning
state_path	str	yes	Dotted path of the self-transitioning composite state.
crosses_composite	bool	yes	Always True for this info because the state is composite.

Example 1 (repro_cli) — reproduction boundary. This diagnostic can appear in a successful inspect report. Reproduce it with pyfcstm inspect -i <file> --format json and read the diagnostics[] array.

state Root {
    state Active { state Leaf; [*] -> Leaf; }
    [*] -> Active;
    Active -> Active;
}

Example 2 (boundary_only) — repair direction for I_TRANSITION_TO_SELF_VIA_PARENT. A typical repair is preserve_if_intentional on transition: Keep the transition when the model should re-run composite entry semantics.

Example 3 (boundary_only) — anti-pattern boundary for I_TRANSITION_TO_SELF_VIA_PARENT. Do not delete this transition automatically; it may be the intended reset path.

W_TRANSITION_SHADOWED

Registry facts. Severity warning; emit tier verify_pipeline; capability requires_solver; span object transition.

Meaning. A later outgoing transition is fully covered by earlier same-source triggers and therefore cannot be selected.

LLM repair summary. Transition ordering means an earlier same-source transition consumes all cases that could have reached this later transition.

Refs schema

Field	Type	Required	Meaning
algorithm_name	str	yes	Verify registry algorithm that produced the raw finding.
verification_scope	str	yes	Verify scope for this finding. (enum: smt_local)
transition	dict	yes	Raw verify transition payload for the shadowed transition.
transition_summary	str	yes	Stable human-readable transition summary derived from the raw payload.
source_state_path	str	yes	Dotted source state path whose outgoing order creates the shadowing.
reason	str	yes	Shadowing reason classification. (enum: guard_shadow, duplicate_event, unconditional_catchall, prior_trigger_cover)
shadowed_by_count	int	yes	Number of earlier transitions covering this transition.
shadowed_by	list[str]	yes	Stable summaries of earlier transitions that shadow this transition.

Example 1 (verify_opt_in) — reproduction boundary. This diagnostic requires optional verify integration. Reproduce it with pyfcstm inspect -i <file> --enable-verify --max-complexity-tier smt_linear --format json; the default structural verify budget does not run the solver-local algorithm that emits it.

state System {
    state A;
    state B;
    state C;
    [*] -> A;
    A -> B;
    A -> C;
}

Example 2 (boundary_only) — repair direction for W_TRANSITION_SHADOWED. A typical repair is reorder_transitions on transition_list: Move the more specific transition before the broader predecessor if both are needed.

Example 3 (boundary_only) — anti-pattern boundary for W_TRANSITION_SHADOWED. Do not reorder transitions without checking FCSTM first-match semantics.

Events and scopes

E_EVENT_REF_INVALID

Registry facts. Severity error; emit tier lookup_api; capability pure_static; span object event_declaration.

Meaning. The textual form of an event reference is syntactically invalid (e.g. bare ‘/’, trailing dots, going beyond the root state).

LLM repair summary. An event reference (::, :, or / scoped) cannot resolve to a known event under the indicated scope. The grammar accepts the syntactic form, but the resolver cannot bind it to a real event object.

Refs schema

Field	Type	Required	Meaning
event_ref	str	yes	The raw event reference text.
reason	str	yes	Short tag describing why the reference is invalid. (enum: empty, bare_slash, invalid_absolute, invalid_relative, trailing_dots, beyond_root)

Example 1 (repro_api) — reproduction boundary. This diagnostic is emitted by explicit resolver API calls. Default pyfcstm inspect normally does not call that API in a way that reports this code, so use the referenced API boundary rather than a default CLI JSON expectation.

state Root { state A; state B; A -> B : /; }

Example 2 (boundary_only) — repair direction for E_EVENT_REF_INVALID. A typical repair is fix_scope_operator on transition: The three scope operators do not interchange freely. :: is source-local, : is parent-chain, / is root-absolute. Pick the one that matches where the event is actually declared.

Example 3 (boundary_only) — anti-pattern boundary for E_EVENT_REF_INVALID. Do not invent a new event by silently aliasing — the dispatcher won’t fire on an undeclared name.

E_EVENT_NOT_FOUND

Registry facts. Severity error; emit tier lookup_api; capability pure_static; span object event_declaration.

Meaning. An event reference parses correctly but does not resolve to any event defined in the targeted scope.

LLM repair summary. A dotted event path could not be resolved against the assembled state hierarchy. The path syntax was valid but no event with that name exists at the resolved state.

Refs schema

Field	Type	Required	Meaning
event_ref	str	yes	The raw event reference text.
scope	str	yes	Resolution scope used. (enum: local, chain, absolute)
searched_from	str_or_null	no	Dotted state path of the caller that initiated the lookup (i.e. the state on which .resolve_event() was invoked, or, for StateMachine.resolve_event, the state machine’s root). This is the originating location of the bad reference in source — not the effective search root, which is always the model root for absolute references.

Example 1 (repro_api) — reproduction boundary. This diagnostic is emitted by explicit resolver API calls. Default pyfcstm inspect normally does not call that API in a way that reports this code, so use the referenced API boundary rather than a default CLI JSON expectation.

state Root { state A; state B; A -> B :: NoEvent; }

Example 2 (boundary_only) — repair direction for E_EVENT_NOT_FOUND. A typical repair is fix_event_path on transition: Confirm the dotted path matches the state hierarchy that actually exists after imports have been merged.

Example 3 (boundary_only) — anti-pattern boundary for E_EVENT_NOT_FOUND. Do not paper over the error by introducing a wildcard alias — events are uniquely bound by their scope.

W_COMBO_DUPLICATE_EVENT

Registry facts. Severity warning; emit tier static_pipeline; capability pure_static; span object transition.

Meaning. A combo transition trigger repeats the same canonical event term. The model still executes the two generated hops, but the second event term is usually redundant or a typo.

LLM repair summary. The combo trigger contains the same resolved event twice, for example E1 + E1. This is legal but normally redundant because one cycle’s input event set already contains E1.

Refs schema

Field	Type	Required	Meaning
origin_id	str	yes	Stable identifier of the original combo transition.
event_name	str	yes	Canonical qualified event name that appears more than once.
term_index	int	yes	Zero-based index of the repeated event term.
first_term_index	int	yes	Zero-based index of the first matching event term.
term_text	str	yes	Canonical source text of the repeated event term.
first_term_text	str	yes	Canonical source text of the first matching event term.
transition_span	Span	no	Source span of the original combo transition.
trigger_span	Span	no	Source span of the combo trigger suffix.
term_span	Span	no	Source span of the repeated event term.
first_term_span	Span	no	Source span of the first matching event term.

Example 1 (repro_cli) — reproduction boundary. This diagnostic can appear in a successful inspect report. Reproduce it with pyfcstm inspect -i <file> --format json and read the diagnostics[] array.

def int x = 0;
state Root {
    state A;
    state B;
    [*] -> A;
    A -> B :: E1 + E1;
}

Example 2 (boundary_only) — repair direction for W_COMBO_DUPLICATE_EVENT. A typical repair is inspect_terms on transition: Check whether the second event was meant to be a different event.

Example 3 (boundary_only) — anti-pattern boundary for W_COMBO_DUPLICATE_EVENT. Do not silently delete the repeated event; the explicit pseudo-chain shape may be intentional.

W_UNUSED_EVENT

Registry facts. Severity warning; emit tier static_pipeline; capability pure_static; span object event_declaration.

Meaning. An event declaration is never referenced by any transition.

LLM repair summary. An event is declared but never triggers any transition, so it is unused from the machine’s perspective.

Refs schema

Field	Type	Required	Meaning
event_qualified_name	str	yes	Fully qualified event name (e.g. Root.SubA.Pause).
scope	str	yes	Scope at which the event is declared. (enum: local, chain, absolute)

Example 1 (repro_cli) — reproduction boundary. This diagnostic can appear in a successful inspect report. Reproduce it with pyfcstm inspect -i <file> --format json and read the diagnostics[] array.

state Root {
    event Unused;
    state A;
    state B;
    [*] -> A;
    A -> B :: SomethingElse;
}

Example 2 (boundary_only) — repair direction for W_UNUSED_EVENT. A typical repair is wire_event on transition: Add a transition that uses the event if it was meant to be emitted.

Example 3 (boundary_only) — anti-pattern boundary for W_UNUSED_EVENT. Do not rename the event to dodge the warning — that just shifts the problem.

W_SHADOWED_EVENT

Registry facts. Severity warning; emit tier static_pipeline; capability pure_static; span object event_declaration.

Meaning. A local event name shadows a chain or absolute event with the same leaf name.

LLM repair summary. The same event leaf name exists in local and broader scopes, which can make transition triggers easy to misread.

Refs schema

Field	Type	Required	Meaning
event_name	str	yes	Shared event leaf name.
local_path	str	yes	Qualified local event path.
chain_path	str	yes	Qualified chain or absolute event path.

Example 1 (repro_cli) — reproduction boundary. This diagnostic can appear in a successful inspect report. Reproduce it with pyfcstm inspect -i <file> --format json and read the diagnostics[] array.

state Root {
    event Tick;
    state A;
    state B;
    [*] -> A;
    A -> B : Tick;
    B -> A :: Tick;
}

Example 2 (boundary_only) — repair direction for W_SHADOWED_EVENT. A typical repair is rename_event on event: Use distinct event names for different scopes.

Example 3 (boundary_only) — anti-pattern boundary for W_SHADOWED_EVENT. Do not rename only one trigger without checking all emitters.

I_TRANSITION_NEVER_EVENT_TRIGGERED

Registry facts. Severity info; emit tier static_pipeline; capability pure_static; span object transition.

Meaning. A normal transition has no event and no guard, so it is an unconditional fall-through candidate.

LLM repair summary. The transition is not event-triggered and has no guard. This may be a deliberate unconditional fall-through, so treat it as context rather than a fix target.

Refs schema

Field	Type	Required	Meaning
from_path	str	yes	Dotted source state path.
to_path	str	yes	Dotted target state path.
transition_span	Span	no	Source span of the transition when available.
transition_index	int	no	Zero-based index in parent-first model transition order, including expanded forced transitions at their declaring state before ordinary transitions and descendant-state transitions. This is used only as a source-range disambiguation hint when spans are unavailable.

Example 1 (repro_cli) — reproduction boundary. This diagnostic can appear in a successful inspect report. Reproduce it with pyfcstm inspect -i <file> --format json and read the diagnostics[] array.

state Root {
    state A;
    state B;
    [*] -> A;
    A -> B;
}

Example 2 (boundary_only) — repair direction for I_TRANSITION_NEVER_EVENT_TRIGGERED. A typical repair is keep_if_fallthrough on transition: Keep it when the state should immediately advance.

Example 3 (boundary_only) — anti-pattern boundary for I_TRANSITION_NEVER_EVENT_TRIGGERED. Do not add a meaningless event just to silence this info.

W_EVENT_UNREACHABLE_EMIT

Registry facts. Severity warning; emit tier verify_pipeline; capability pure_static; span object event_declaration.

Meaning. A used event has no consumer source that is reachable in the guard-agnostic topology graph.

LLM repair summary. The event is used by transitions, but those transition sources are not reachable from the root entry topology.

Refs schema

Field	Type	Required	Meaning
algorithm_name	str	yes	Verify registry algorithm that produced the raw finding.
verification_scope	str	yes	Verify scope for this finding. (enum: topological_only)
event_name	str	yes	Qualified event name whose consumers are unreachable.
consumer_count	int	yes	Number of unreachable consumer transitions represented by this finding.

Example 1 (verify_opt_in) — reproduction boundary. This diagnostic requires optional verify integration. Reproduce it with pyfcstm inspect -i <file> --enable-verify --max-complexity-tier smt_linear --format json; the default structural verify budget does not run the solver-local algorithm that emits it.

state System {
    event Panic;
    state A;
    state LostA;
    state LostB;
    [*] -> A;
    LostA -> A : Panic;
    LostB -> A : Panic;
}

Example 2 (boundary_only) — repair direction for W_EVENT_UNREACHABLE_EMIT. A typical repair is connect_consumer on transition_source: Add a topology path that reaches the state consuming the event.

Example 3 (boundary_only) — anti-pattern boundary for W_EVENT_UNREACHABLE_EMIT. Do not add an emitter for this event if no reachable state can consume it.

Combo and relay diagnostics

E_COMBO_TRIGGER_NOT_EXPANDED

Registry facts. Severity error; emit tier catalog_only; capability pure_static; span object transition.

Meaning. A legacy fail-closed compatibility code for implementations that parse combo trigger syntax before model expansion support is available.

LLM repair summary. Older pyfcstm/jsfcstm builds may accept a transition trigger such as :: E1 + E2 or : E1 + [x > 0] but stop before pseudo-state expansion support. Current pyfcstm expands combo triggers instead of emitting this code; the catalog entry remains for cross-version consumers.

Refs schema

Field	Type	Required	Meaning
state_path	str_or_null	no	Dotted path of the state that owns the combo transition.
trigger	str	yes	Canonical text of the combo trigger suffix.

Example 1 (compatibility_only) — reproduction boundary. This code documents a compatibility or historical fail-closed contract. Current normal pyfcstm paths should not emit it; consumers keep it so older tools can be explained safely.

state Root { state A; state B; A -> B :: Go + Done; }

Example 2 (boundary_only) — repair direction for E_COMBO_TRIGGER_NOT_EXPANDED. A typical repair is wait_for_expansion_support on transition: Keep the DSL syntax if you are testing parser/provenance support; wait for model-expansion support before running simulation, verification, or code generation on combo triggers.

Example 3 (boundary_only) — anti-pattern boundary for E_COMBO_TRIGGER_NOT_EXPANDED. Do not treat the first event term as the whole transition; that would silently change model semantics.

W_COMBO_RESERVED_PREFIX_STATE_KIND

Registry facts. Severity warning; emit tier partial_static_pipeline; capability pure_static; span object state_identifier.

Meaning. A non-pseudo state name starts with the automatic combo relay prefix.

LLM repair summary. A normal leaf or composite state uses the __combo_ prefix reserved for combo relay pseudo states. The model can still build, but the name is visually ambiguous with generated relay nodes.

Refs schema

Field	Type	Required	Meaning
state_name	str	yes	State name using the combo relay reserved prefix.
state_path	str	yes	Dotted path of the offending state.
reserved_prefix	str	yes	Reserved prefix used by generated combo pseudo states.
state_kind	str	yes	Kind of user-authored state that used the reserved prefix. (enum: state, composite)

Example 1 (boundary_only) — reproduction boundary. This registry contract is intentionally ahead of full frontend/backend emission parity. Treat the source as the supported boundary shape and confirm the current emitter before promising default CLI JSON output.

state Root { state __combo_user; [*] -> __combo_user; }

Example 2 (boundary_only) — repair direction for W_COMBO_RESERVED_PREFIX_STATE_KIND. A typical repair is rename_state on state_identifier: Rename the user-authored state so readers and generated artifacts do not confuse it with an expanded combo relay.

Example 3 (boundary_only) — anti-pattern boundary for W_COMBO_RESERVED_PREFIX_STATE_KIND. Do not fix this by declaring a business state as pseudo unless it is truly only a relay.

W_COMBO_RELAY_PSEUDO_HAS_ACTIONS

Registry facts. Severity warning; emit tier partial_static_pipeline; capability pure_static; span object state_identifier.

Meaning. A pseudo state in the combo relay namespace contains lifecycle or aspect actions, so it is not a pure relay.

LLM repair summary. A pseudo state __combo_* node is allowed so expanded combo DSL can be reimported, but relay pseudo states should stay pure. Lifecycle or aspect actions make the relay observable and may surprise readers.

Refs schema

Field	Type	Required	Meaning
state_name	str	yes	Pseudo-state name using the combo relay reserved prefix.
state_path	str	yes	Dotted path of the pseudo state.
reserved_prefix	str	yes	Reserved prefix used by combo relay pseudo states.
action_kinds	list[str]	yes	Lifecycle or aspect action kinds present on the pseudo state. (item enum: enter, during, exit, during_aspect)

Example 1 (boundary_only) — reproduction boundary. This registry contract is intentionally ahead of full frontend/backend emission parity. Treat the source as the supported boundary shape and confirm the current emitter before promising default CLI JSON output.

def int x = 0; state Root { pseudo state __combo_user { enter { x = x + 1; } } state A; [*] -> A; }

Example 2 (boundary_only) — repair direction for W_COMBO_RELAY_PSEUDO_HAS_ACTIONS. A typical repair is move_action on lifecycle_action: Move the action to the authored source or target state if it is business behavior rather than routing metadata.

Example 3 (boundary_only) — anti-pattern boundary for W_COMBO_RELAY_PSEUDO_HAS_ACTIONS. Do not add business logic to generated combo relay pseudo states.

I_COMBO_PSEUDO_NAME_EXTENDED

Registry facts. Severity info; emit tier partial_static_pipeline; capability pure_static; span object state_identifier.

Meaning. Combo trigger expansion extended a generated relay name’s digest prefix to avoid a same-scope name collision.

LLM repair summary. The combo expander found a same-scope name collision at the default digest length and deterministically used a longer digest prefix. This is informational and does not mean the model is invalid.

Refs schema

Field	Type	Required	Meaning
state_path	str	yes	Dotted path of the state where expansion allocated the relay.
pseudo_name	str	yes	Final generated pseudo-state name after digest extension.
payload_digest	str	yes	Full digest of the semantic payload that owns the relay.
default_digest_size	int	yes	Default visible digest length before extension.
final_digest_size	int	yes	Visible digest length used by the final generated name.

Example 1 (boundary_only) — reproduction boundary. This registry contract is intentionally ahead of full frontend/backend emission parity. Treat the source as the supported boundary shape and confirm the current emitter before promising default CLI JSON output.

state Root {
    state A;
    state B;
    pseudo state __combo_root_a__e1_hbafca7f66598;
    [*] -> A;
    A -> B :: E1 + E2;
}

Example 2 (boundary_only) — repair direction for I_COMBO_PSEUDO_NAME_EXTENDED. A typical repair is keep_generated_name on pseudo_state: Leave the extended generated name as-is unless you are manually rewriting the expanded relay chain.

Example 3 (boundary_only) — anti-pattern boundary for I_COMBO_PSEUDO_NAME_EXTENDED. Do not shorten the digest manually; that can reintroduce the collision.

E_COMBO_PSEUDO_NAME_COLLISION

Registry facts. Severity error; emit tier static_pipeline; capability pure_static; span object state_identifier.

Meaning. Combo trigger expansion could not allocate a safe pseudo-state name even after extending to the full payload digest.

LLM repair summary. The combo expander first uses a short digest prefix and then lengthens it deterministically on collision. If the full digest still cannot identify a safe relay name in the owning scope, expansion fails rather than silently reusing the wrong pseudo state.

Refs schema

Field	Type	Required	Meaning
state_path	str	yes	Dotted path of the state where expansion attempted to add the pseudo state.
pseudo_name	str	yes	Generated pseudo-state name that collided.
payload_digest	str	yes	Full digest of the semantic payload that attempted to claim the name.

Example 1 (cli_error) — reproduction boundary. This source shape reproduces a controlled model-validation failure through pyfcstm inspect. Current CLI formats exit non-zero before a successful inspect JSON report is produced, so assert the stderr/exit status rather than expecting this code inside diagnostics[].

state Root { state A; state B; [*] -> A; A -> B :: E1 + E2; }

Example 2 (boundary_only) — repair direction for E_COMBO_PSEUDO_NAME_COLLISION. A typical repair is report_internal_collision on transition: This is an internal collision guard. Keep the model unchanged and report the diagnostic, including refs.payload_digest.

Example 3 (boundary_only) — anti-pattern boundary for E_COMBO_PSEUDO_NAME_COLLISION. Do not append an ad-hoc sequence number; user-visible combo names must remain deterministic.

W_COMBO_GUARD_CONST_TRUE

Registry facts. Severity warning; emit tier static_pipeline; capability requires_solver; span object guard_expression.

Meaning. SMT proves that a guard term inside a combo trigger is always true. The term is redundant for the generated pseudo chain, and the primary span points at the original bracketed guard term.

LLM repair summary. SMT proves that a combo guard term is always true and does not constrain the combo chain.

Refs schema

Field	Type	Required	Meaning
origin_id	str	yes	Stable identifier of the original combo transition.
term_index	int	yes	Zero-based index of the constant guard term.
term_text	str	yes	Canonical source text of the guard term.
folded_value	bool	yes	Solver-proven guard value, always true for this code.
transition_span	Span	no	Source span of the original combo transition.
trigger_span	Span	no	Source span of the combo trigger suffix.
term_span	Span	no	Source span of the bracketed guard term.
value_span	Span	no	Source span of the guard expression inside the brackets.

Example 1 (repro_cli) — reproduction boundary. This diagnostic can appear in a successful inspect report. Reproduce it with pyfcstm inspect -i <file> --format json and read the diagnostics[] array.

def int x = 0;
state Root {
    state A;
    state B;
    [*] -> A;
    A -> B :: E1 + [x > 0 || x <= 0] + E2;
}

Example 2 (boundary_only) — repair direction for W_COMBO_GUARD_CONST_TRUE. A typical repair is remove_guard_term on transition: Remove the guard term if it was only a placeholder.

Example 3 (boundary_only) — anti-pattern boundary for W_COMBO_GUARD_CONST_TRUE. Do not add a dummy variable dependency only to silence the diagnostic.

W_COMBO_GUARD_CONST_FALSE

Registry facts. Severity warning; emit tier static_pipeline; capability requires_solver; span object guard_expression.

Meaning. SMT proves that a guard term inside a combo trigger is always false. Any combo branch that must pass through this term can never complete.

LLM repair summary. SMT proves that a combo guard term is always false, so the generated combo branch cannot complete past that term.

Refs schema

Field	Type	Required	Meaning
origin_id	str	yes	Stable identifier of the original combo transition.
term_index	int	yes	Zero-based index of the constant guard term.
term_text	str	yes	Canonical source text of the guard term.
folded_value	bool	yes	Solver-proven guard value, always false for this code.
transition_span	Span	no	Source span of the original combo transition.
trigger_span	Span	no	Source span of the combo trigger suffix.
term_span	Span	no	Source span of the bracketed guard term.
value_span	Span	no	Source span of the guard expression inside the brackets.

Example 1 (repro_cli) — reproduction boundary. This diagnostic can appear in a successful inspect report. Reproduce it with pyfcstm inspect -i <file> --format json and read the diagnostics[] array.

def int x = 0;
state Root {
    state A;
    state B;
    [*] -> A;
    A -> B :: E1 + [x > 0 && x <= 0] + E2;
}

Example 2 (boundary_only) — repair direction for W_COMBO_GUARD_CONST_FALSE. A typical repair is fix_guard_term on transition: Rewrite the guard so it can become true under some valid state.

Example 3 (boundary_only) — anti-pattern boundary for W_COMBO_GUARD_CONST_FALSE. Do not silently remove the guard term — that would change the combo semantics.

W_COMBO_GUARD_PREFIX_IMPLIED

Registry facts. Severity warning; emit tier static_pipeline; capability requires_solver; span object guard_expression.

Meaning. In a side-effect-free combo prefix, prior guard terms imply a later guard term. The later guard is redundant under the current static approximation.

LLM repair summary. Earlier guard terms in the combo prefix already guarantee this later guard term when no relevant side effects can occur between them.

Refs schema

Field	Type	Required	Meaning
origin_id	str	yes	Stable identifier of the original combo transition.
term_index	int	yes	Zero-based index of the implied guard term.
prior_term_index	int	yes	Zero-based index of the earliest prior guard term that makes the prefix implication or contradiction decisive.
term_text	str	yes	Canonical source text of the implied guard term.
prior_term_text	str	yes	Canonical source text of the prior guard term.
transition_span	Span	no	Source span of the original combo transition.
trigger_span	Span	no	Source span of the combo trigger suffix.
term_span	Span	no	Source span of the implied guard term.
value_span	Span	no	Source span of the implied guard expression inside brackets.
prior_term_span	Span	no	Source span of the prior guard term.
prior_value_span	Span	no	Source span of the prior guard expression inside brackets.

Example 1 (repro_cli) — reproduction boundary. This diagnostic can appear in a successful inspect report. Reproduce it with pyfcstm inspect -i <file> --format json and read the diagnostics[] array.

def int x = 0;
state Root {
    state A;
    state B;
    [*] -> A;
    A -> B : [x > 0] + [x > -1];
}

Example 2 (boundary_only) — repair direction for W_COMBO_GUARD_PREFIX_IMPLIED. A typical repair is remove_guard_term on transition: Remove the later guard if it is intentionally redundant.

Example 3 (boundary_only) — anti-pattern boundary for W_COMBO_GUARD_PREFIX_IMPLIED. Do not apply this reasoning across abstract/ref or unknown side-effect boundaries.

W_COMBO_GUARD_PREFIX_CONTRADICTS

Registry facts. Severity warning; emit tier static_pipeline; capability requires_solver; span object guard_expression.

Meaning. In a side-effect-free combo prefix, prior guard terms contradict a later guard term. The generated combo branch cannot complete through that term under the current static approximation.

LLM repair summary. Earlier guard terms in the combo prefix make this later guard impossible when no relevant side effects can occur between them.

Refs schema

Field	Type	Required	Meaning
origin_id	str	yes	Stable identifier of the original combo transition.
term_index	int	yes	Zero-based index of the contradictory guard term.
prior_term_index	int	yes	Zero-based index of the earliest prior guard term that makes the prefix implication or contradiction decisive.
term_text	str	yes	Canonical source text of the contradictory guard term.
prior_term_text	str	yes	Canonical source text of the prior guard term.
transition_span	Span	no	Source span of the original combo transition.
trigger_span	Span	no	Source span of the combo trigger suffix.
term_span	Span	no	Source span of the contradictory guard term.
value_span	Span	no	Source span of the contradictory guard expression inside brackets.
prior_term_span	Span	no	Source span of the prior guard term.
prior_value_span	Span	no	Source span of the prior guard expression inside brackets.

Example 1 (repro_cli) — reproduction boundary. This diagnostic can appear in a successful inspect report. Reproduce it with pyfcstm inspect -i <file> --format json and read the diagnostics[] array.

def int x = 0;
state Root {
    state A;
    state B;
    [*] -> A;
    A -> B : [x > 0] + [x < 0];
}

Example 2 (boundary_only) — repair direction for W_COMBO_GUARD_PREFIX_CONTRADICTS. A typical repair is fix_guard_term on transition: Rewrite the later guard if it was meant to describe a reachable branch.

Example 3 (boundary_only) — anti-pattern boundary for W_COMBO_GUARD_PREFIX_CONTRADICTS. Do not apply this reasoning across abstract/ref or unknown side-effect boundaries.

Forced transition diagnostics

E_FORCED_TRANSITION_EXPANSION

Registry facts. Severity error; emit tier static_pipeline; capability pure_static; span object transition.

Meaning. A forced transition (!State -> … or !*) cannot be expanded because the source or target reference is invalid.

LLM repair summary. A forced transition (!Source -> Target or !* -> Target) failed to expand cleanly — typically because the source name cannot be found, or because the expansion would create an empty/inconsistent fan-out under the current scope.

Refs schema

Field	Type	Required	Meaning
original_raw	str	yes	Raw forced-transition text as written.
reason	str	yes	Short tag describing why expansion failed. (enum: src_not_found, tgt_not_found, src_is_root, wildcard_no_descendants)

Example 1 (cli_error) — reproduction boundary. This source shape reproduces a controlled model-validation failure through pyfcstm inspect. Current CLI formats exit non-zero before a successful inspect JSON report is produced, so assert the stderr/exit status rather than expecting this code inside diagnostics[].

state Root { state A; !NoSuch -> A; }

Example 2 (boundary_only) — repair direction for E_FORCED_TRANSITION_EXPANSION. A typical repair is fix_source on forced_transition: Confirm the !Name source is a real state inside the current composite scope. !* only matches direct substates; deeper descendants need explicit names.

Example 3 (boundary_only) — anti-pattern boundary for E_FORCED_TRANSITION_EXPANSION. Do not add an effect { ... } block to a forced transition — forced transitions cannot carry effects and the expansion would fail anyway.

W_FORCED_NEVER_EXPANDS

Registry facts. Severity warning; emit tier static_pipeline; capability pure_static; span object transition.

Meaning. A forced transition declaration has no concrete child state in its declaration scope to expand from.

LLM repair summary. The forced transition declaration expands to zero concrete transitions, so it has no runtime effect.

Refs schema

Field	Type	Required	Meaning
state_path	str	yes	Dotted path of the state containing the forced transition.
original_raw	str	yes	Original forced transition DSL text.

Example 1 (repro_cli) — reproduction boundary. This diagnostic can appear in a successful inspect report. Reproduce it with pyfcstm inspect -i <file> --format json and read the diagnostics[] array.

state Root {
    state A {
        !* -> [*];
    }
    [*] -> A;
}

Example 2 (boundary_only) — repair direction for W_FORCED_NEVER_EXPANDS. A typical repair is move_transition on forced_transition: Move the forced transition to a composite scope that owns matching children.

Example 3 (boundary_only) — anti-pattern boundary for W_FORCED_NEVER_EXPANDS. Do not leave a zero-expansion forced transition as documentation.

W_FORCED_OVERRIDES_NORMAL

Registry facts. Severity warning; emit tier static_pipeline; capability pure_static; span object transition.

Meaning. A forced transition expands to the same source, target, event, and guard as a normal transition.

LLM repair summary. The forced transition duplicates a normal transition, which can make the forced declaration misleading or redundant.

Refs schema

Field	Type	Required	Meaning
from_path	str	yes	Dotted source state path.
to_path	str	yes	Dotted target state path.
forced_declaration_span	Span	no	Source span of the forced transition when available.
normal_transition_span	Span	no	Source span of the normal transition when available.

Example 1 (repro_cli) — reproduction boundary. This diagnostic can appear in a successful inspect report. Reproduce it with pyfcstm inspect -i <file> --format json and read the diagnostics[] array.

state Root {
    state A;
    state B;
    [*] -> A;
    A -> B :: Go;
    !A -> B :: Go;
}

Example 2 (boundary_only) — repair direction for W_FORCED_OVERRIDES_NORMAL. A typical repair is remove_duplicate on forced_transition: Remove the forced transition if the normal one already covers it.

Example 3 (boundary_only) — anti-pattern boundary for W_FORCED_OVERRIDES_NORMAL. Do not keep both unless the generated runtime intentionally treats forced metadata differently.

W_FORCED_GUARD_UNSAT

Registry facts. Severity warning; emit tier verify_pipeline; capability requires_solver; span object guard_expression.

Meaning. A forced-transition guard cannot be satisfied under declaration initializer values.

LLM repair summary. The forced transition expands structurally, but its guard is false under top-level declaration initializers.

Refs schema

Field	Type	Required	Meaning
algorithm_name	str	yes	Verify registry algorithm that produced the raw finding.
verification_scope	str	yes	Verify scope for this finding. (enum: smt_local)
transition	dict	yes	Raw verify transition payload for the forced transition.
transition_summary	str	yes	Stable human-readable transition summary derived from the raw payload.
scope	str	yes	Initial-value scope used by the verify algorithm. (enum: dsl_def_init_only)

Example 1 (verify_opt_in) — reproduction boundary. This diagnostic requires optional verify integration. Reproduce it with pyfcstm inspect -i <file> --enable-verify --max-complexity-tier smt_linear --format json; the default structural verify budget does not run the solver-local algorithm that emits it.

def int x = 0;
state System {
    state A;
    state B;
    [*] -> A;
    !A -> B : if [x > 0];
}

Example 2 (boundary_only) — repair direction for W_FORCED_GUARD_UNSAT. A typical repair is adjust_initializer on variable_definition: Change the initializer if the forced transition must be possible at startup.

Example 3 (boundary_only) — anti-pattern boundary for W_FORCED_GUARD_UNSAT. Do not delete the forced transition solely because it is impossible at declaration time; later runtime values may still matter for normal guards.

Guard, effect, and solver diagnostics

W_GUARD_CONST_FALSE

Registry facts. Severity warning; emit tier static_pipeline; capability const_fold; span object guard_expression.

Meaning. A transition’s guard condition folds to the boolean literal false using the built-in constant folder, so the transition can never fire. The folder is intentionally side-effect free: it handles literal-only boolean, comparison, arithmetic, bitwise, unary, and ternary expressions, but does not evaluate variables, functions, solvers, or runtime state.

LLM repair summary. The transition’s guard is statically known to be false and the transition is effectively dead code.

Refs schema

Field	Type	Required	Meaning
transition_span	Span	no	Source span of the transition declaration.
folded_value	bool	yes	Constant-folded guard value (always false).
from_path	str	no	Source state path of the transition, or [*] for an initial transition.
to_path	str	no	Target state path of the transition, or [*] for an exit transition.
guard_text	str	no	Normalized guard expression text used to disambiguate spanless inspect diagnostics. Pyfcstm and jsfcstm both render this with the shared inspect expression format: canonical boolean/operator spelling, decimal integer literals, and normalized spacing.
transition_index	int	no	Zero-based index in parent-first model transition order, including expanded forced transitions at their declaring state before ordinary transitions and descendant-state transitions. This is used only as a source-range disambiguation hint when spans are unavailable.

Example 1 (repro_cli) — reproduction boundary. This diagnostic can appear in a successful inspect report. Reproduce it with pyfcstm inspect -i <file> --format json and read the diagnostics[] array.

state Root {
    state A;
    state B;
    [*] -> A;
    A -> B : if [(0x0F & 0xF0) != 0];
}

Example 2 (boundary_only) — repair direction for W_GUARD_CONST_FALSE. A typical repair is fix_guard on transition: Rewrite the guard so it can become true under some valid state.

Example 3 (boundary_only) — anti-pattern boundary for W_GUARD_CONST_FALSE. Do not silently remove the guard — that would change the semantics.

W_GUARD_CONST_TRUE

Registry facts. Severity warning; emit tier static_pipeline; capability const_fold; span object guard_expression.

Meaning. A transition’s guard condition folds to the boolean literal true using the built-in constant folder, so the guard is redundant for all runtime states covered by that literal-only expression.

LLM repair summary. The transition’s guard is statically known to be true and does not constrain the transition.

Refs schema

Field	Type	Required	Meaning
transition_span	Span	no	Source span of the transition declaration.
guard_span	Span	no	Source span of the removable guard suffix, including the leading trigger separator when needed. This is reserved for future emitters that can provide a stable guard-only span; the current inspect emitters intentionally omit it.
folded_value	bool	yes	Constant-folded guard value (always true).
from_path	str	no	Source state path of the transition, or [*] for an initial transition.
to_path	str	no	Target state path of the transition, or [*] for an exit transition.
guard_text	str	no	Normalized guard expression text used to disambiguate spanless inspect diagnostics. Pyfcstm and jsfcstm both render this with the shared inspect expression format: canonical boolean/operator spelling, decimal integer literals, and normalized spacing.
transition_index	int	no	Zero-based index in parent-first model transition order, including expanded forced transitions at their declaring state before ordinary transitions and descendant-state transitions. This is used only as a source-range disambiguation hint when spans are unavailable.

Example 1 (repro_cli) — reproduction boundary. This diagnostic can appear in a successful inspect report. Reproduce it with pyfcstm inspect -i <file> --format json and read the diagnostics[] array.

state Root {
    state A;
    state B;
    [*] -> A;
    A -> B : if [(1 + 2) == 3];
}

Example 2 (boundary_only) — repair direction for W_GUARD_CONST_TRUE. A typical repair is remove_guard on transition: Remove the guard if the transition is meant to be unconditional.

Example 3 (boundary_only) — anti-pattern boundary for W_GUARD_CONST_TRUE. Do not add a dummy variable dependency only to silence the diagnostic.

W_GUARD_VARS_NEVER_CHANGE

Registry facts. Severity warning; emit tier static_pipeline; capability pure_static; span object guard_expression.

Meaning. A transition guard reads variables that are never changed by any lifecycle action or transition effect, so the guard only depends on initial values.

LLM repair summary. This guard is controlled only by initial variable values. If those values never change, the transition condition is effectively fixed.

Refs schema

Field	Type	Required	Meaning
from_path	str	yes	Source state path of the transition, or [*] for an entry marker.
to_path	str	yes	Target state path of the transition, or [*] for an exit marker.
guard_vars	list[str]	yes	Guard variables that never change.

Example 1 (repro_cli) — reproduction boundary. This diagnostic can appear in a successful inspect report. Reproduce it with pyfcstm inspect -i <file> --format json and read the diagnostics[] array.

def int ready = 0;
state Root {
    state A;
    state B;
    [*] -> A;
    A -> B : if [ready > 0];
}

Example 2 (boundary_only) — repair direction for W_GUARD_VARS_NEVER_CHANGE. A typical repair is add_write on action_or_effect: Add the missing state update if the guard should evolve at runtime.

Example 3 (boundary_only) — anti-pattern boundary for W_GUARD_VARS_NEVER_CHANGE. Do not add a meaningless self-assignment; it does not model a real change.

W_EFFECT_SELF_ASSIGN

Registry facts. Severity warning; emit tier static_pipeline; capability pure_static; span object effect_statement.

Meaning. An effect statement assigns a variable directly to itself.

LLM repair summary. The assignment does not change model state and is likely dead code.

Refs schema

Field	Type	Required	Meaning
state_path	str	yes	Source state path when known.
from_path	str	no	Public source path for combo terminal effect diagnostics after authored-subject remapping. Ordinary self-assignment diagnostics may omit this field and use state_path only.
generated_state_path	str	no	Generated combo pseudo state path kept only as secondary debug provenance after the public subject is remapped.
generated_from_path	str	no	Generated transition source path kept as secondary debug provenance.
generated_to_path	str	no	Generated transition target path kept as secondary debug provenance.
combo_origin_id	str	no	Original combo transition identifier for a generated terminal effect.
combo_owner_path	str	no	Owner composite path for entry combo diagnostics whose public subject is the initial marker [*].
transition_span	Span	no	Source span of the transition containing the effect.
var_name	str	yes	Variable assigned to itself.
effect_self_assign_anchor	str	no	Variable name repeated only when the self-assignment occurrence can be uniquely mapped back to a non-initial effect statement for the same source state and variable.
suggested_fix	dict	no	Structured quick-fix payload for removing the no-op effect statement.
transition_index	int	no	Zero-based index in parent-first model transition order, including expanded forced transitions at their declaring state before ordinary transitions and descendant-state transitions. This is used only as a source-range disambiguation hint when spans are unavailable.

Example 1 (repro_cli) — reproduction boundary. This diagnostic can appear in a successful inspect report. Reproduce it with pyfcstm inspect -i <file> --format json and read the diagnostics[] array.

def int x = 0;
state Root {
    state A;
    state B;
    [*] -> A;
    A -> B effect { x = x; }
}

Example 2 (boundary_only) — repair direction for W_EFFECT_SELF_ASSIGN. A typical repair is remove_statement on effect_statement: Delete the self-assignment.

Example 3 (boundary_only) — anti-pattern boundary for W_EFFECT_SELF_ASSIGN. Do not replace it with another no-op expression.

W_DEAD_GUARD

Registry facts. Severity warning; emit tier verify_pipeline; capability requires_solver; span object guard_expression.

Meaning. A transition guard is unsatisfiable under model variable type and runtime-definedness constraints.

LLM repair summary. SMT proves the guard cannot become true for any valid variable valuation. This differs from W_GUARD_CONST_FALSE, which only reports literal-only guards folded syntactically to false.

Refs schema

Field	Type	Required	Meaning
algorithm_name	str	yes	Verify registry algorithm that produced the raw finding.
verification_scope	str	yes	Verify scope for this finding. (enum: smt_local)
transition	dict	yes	Raw verify transition payload for the guarded transition.
transition_summary	str	yes	Stable human-readable transition summary derived from the raw payload.

Example 1 (verify_opt_in) — reproduction boundary. This diagnostic requires optional verify integration. Reproduce it with pyfcstm inspect -i <file> --enable-verify --max-complexity-tier smt_linear --format json; the default structural verify budget does not run the solver-local algorithm that emits it.

def int x = 0;
state System {
    state A;
    state B;
    [*] -> A;
    A -> B : if [x > 1 && x < 0];
}

Example 2 (boundary_only) — repair direction for W_DEAD_GUARD. A typical repair is fix_guard on transition: Relax or correct the contradictory guard condition.

Example 3 (boundary_only) — anti-pattern boundary for W_DEAD_GUARD. Do not replace the guard with true unless the transition really should become unconditional.

W_GUARD_TAUTOLOGY

Registry facts. Severity warning; emit tier verify_pipeline; capability requires_solver; span object guard_expression.

Meaning. A transition guard is true for every variable valuation that satisfies model type and runtime-definedness constraints.

LLM repair summary. SMT proves the guard is always true under the modeled variable constraints. This differs from W_GUARD_CONST_TRUE, which only reports literal-only guards folded syntactically to true.

Refs schema

Field	Type	Required	Meaning
algorithm_name	str	yes	Verify registry algorithm that produced the raw finding.
verification_scope	str	yes	Verify scope for this finding. (enum: smt_local)
transition	dict	yes	Raw verify transition payload for the guarded transition.
transition_summary	str	yes	Stable human-readable transition summary derived from the raw payload.

Example 1 (verify_opt_in) — reproduction boundary. This diagnostic requires optional verify integration. Reproduce it with pyfcstm inspect -i <file> --enable-verify --max-complexity-tier smt_linear --format json; the default structural verify budget does not run the solver-local algorithm that emits it.

def int x = 0;
state System {
    state A;
    state B;
    [*] -> A;
    A -> B : if [x >= 0 || x < 0];
}

Example 2 (boundary_only) — repair direction for W_GUARD_TAUTOLOGY. A typical repair is remove_redundant_guard on transition: Remove the guard if the transition should be unconditional.

Example 3 (boundary_only) — anti-pattern boundary for W_GUARD_TAUTOLOGY. Do not assume every tautological guard is wrong; it may document intent.

W_EFFECT_SMT_NO_OP

Registry facts. Severity warning; emit tier verify_pipeline; capability requires_solver; span object effect_statement.

Meaning. A transition effect leaves all model variables unchanged for every guarded, runtime-defined execution.

LLM repair summary. Symbolic execution proves the effect does not change any persistent model variable when its guard is enabled.

Refs schema

Field	Type	Required	Meaning
algorithm_name	str	yes	Verify registry algorithm that produced the raw finding.
verification_scope	str	yes	Verify scope for this finding. (enum: smt_local)
transition	dict	yes	Raw verify transition payload for the transition with the effect.
transition_summary	str	yes	Stable human-readable transition summary derived from the raw payload.

Example 1 (verify_opt_in) — reproduction boundary. This diagnostic requires optional verify integration. Reproduce it with pyfcstm inspect -i <file> --enable-verify --max-complexity-tier smt_linear --format json; the default structural verify budget does not run the solver-local algorithm that emits it.

def int x = 0;
state System {
    state A;
    state B;
    [*] -> A;
    A -> B : if [x >= 0] effect { x = x + 0; };
}

Example 2 (boundary_only) — repair direction for W_EFFECT_SMT_NO_OP. A typical repair is remove_effect on effect_block: Remove the effect if it is dead or only placeholder logic.

Example 3 (boundary_only) — anti-pattern boundary for W_EFFECT_SMT_NO_OP. Do not report block-local temporary-only changes as state changes; they disappear after the effect block.

I_EFFECT_GUARD_CONTRADICT

Registry facts. Severity info; emit tier verify_pipeline; capability requires_solver; span object effect_statement.

Meaning. A transition effect makes the same transition guard false after every guarded, runtime-defined execution.

LLM repair summary. The effect immediately invalidates the guard that enabled the transition. This may be a deliberate one-shot or latch reset pattern.

Refs schema

Field	Type	Required	Meaning
algorithm_name	str	yes	Verify registry algorithm that produced the raw finding.
verification_scope	str	yes	Verify scope for this finding. (enum: smt_local)
transition	dict	yes	Raw verify transition payload for the transition with the effect.
transition_summary	str	yes	Stable human-readable transition summary derived from the raw payload.

Example 1 (verify_opt_in) — reproduction boundary. This diagnostic requires optional verify integration. Reproduce it with pyfcstm inspect -i <file> --enable-verify --max-complexity-tier smt_linear --format json; the default structural verify budget does not run the solver-local algorithm that emits it.

def int x = 0;
state System {
    state A;
    state B;
    [*] -> A;
    A -> B : if [x > 0] effect { x = 0; };
}

Example 2 (boundary_only) — repair direction for I_EFFECT_GUARD_CONTRADICT. A typical repair is review_one_shot on transition: Confirm the effect is meant to falsify the enabling guard.

Example 3 (boundary_only) — anti-pattern boundary for I_EFFECT_GUARD_CONTRADICT. Do not treat this info as an automatic defect; guard-reset effects are often intentional.

Lifecycle, aspect, and composite diagnostics

E_DURING_ASPECT_INVALID

Registry facts. Severity error; emit tier static_pipeline; capability pure_static; span object lifecycle_action.

Meaning. A during block is declared inconsistently with the host state’s leaf/composite kind. Leaf states must use during { … } without an aspect modifier; composite states must use during before { … } or during after { … } (the aspect is mandatory on composites). The global >> during before/after aspect form is also invalid on a leaf state — aspect actions fan out to every descendant leaf, and a leaf has nothing to fan into.

LLM repair summary. A during before / during after or >> during ... aspect declaration was placed on a state that cannot legally receive it (typically a leaf state with no descendant for the aspect to fan out to).

Refs schema

Field	Type	Required	Meaning
state_path	str	yes	Dotted path of the offending state.
state_kind	str	yes	Kind of the host state. (enum: leaf, composite)
aspect	str_or_null	no	The aspect token that was actually used. 'before' or 'after' for during before / during after and >> during before/after; null when the user wrote a bare during on a composite state. null is intentional — the consumer should branch on the bare-during case rather than treat it as an enum value.

Example 1 (cli_error) — reproduction boundary. This source shape reproduces a controlled model-validation failure through pyfcstm inspect. Current CLI formats exit non-zero before a successful inspect JSON report is produced, so assert the stderr/exit status rather than expecting this code inside diagnostics[].

state Root {
    state A {
        during before { }
    }
}

Example 2 (boundary_only) — repair direction for E_DURING_ASPECT_INVALID. A typical repair is move_to_composite on aspect_declaration: Aspect actions only make sense on composite states. Move the declaration to a composite ancestor whose descendants should receive the aspect.

Example 3 (boundary_only) — anti-pattern boundary for E_DURING_ASPECT_INVALID. Do not convert the leaf into a composite just to host the aspect — that changes the runtime entry/exit semantics.

E_PSEUDO_NOT_LEAF

Registry facts. Severity error; emit tier static_pipeline; capability pure_static; span object state_identifier.

Meaning. A state was declared with the pseudo keyword but has nested substates. Pseudo states must be leaves: they skip ancestor >> during aspects and only make sense without inner structure.

LLM repair summary. A pseudo state declaration was given a composite body (or otherwise treated as if it had descendants). Pseudo states must be leaves: they cannot host substates because their semantics explicitly skip ancestor >> during aspects.

Refs schema

Field	Type	Required	Meaning
state_path	str	yes	Dotted path of the offending pseudo state.

Example 1 (cli_error) — reproduction boundary. This source shape reproduces a controlled model-validation failure through pyfcstm inspect. Current CLI formats exit non-zero before a successful inspect JSON report is produced, so assert the stderr/exit status rather than expecting this code inside diagnostics[].

state Root {
    pseudo state Outer {
        state Inner;
        [*] -> Inner;
    }
}

Example 2 (boundary_only) — repair direction for E_PSEUDO_NOT_LEAF. A typical repair is drop_pseudo_marker on state_definition: If the state genuinely needs substates, remove the pseudo keyword and treat it as a normal composite.

Example 3 (boundary_only) — anti-pattern boundary for E_PSEUDO_NOT_LEAF. Do not rely on pseudo states for normal hierarchy modeling — they exist solely to bypass >> during aspect application.

W_DURING_CONST_ASSIGN

Registry facts. Severity warning; emit tier static_pipeline; capability const_fold; span object lifecycle_action.

Meaning. A concrete during action assigns a variable to the same literal-only numeric value every cycle. The analyzer only checks the direct statements in ordinary during { ... } blocks; it skips abstract actions, refs, composite during before / during after actions, aspect actions, functions, variables, and nested control flow.

LLM repair summary. The during block writes the same constant numeric value on every cycle, which often indicates initialization logic was placed in during instead of enter.

Refs schema

Field	Type	Required	Meaning
state_path	str	yes	Dotted path of the state that owns the during action.
var_name	str	yes	Variable assigned by the constant during statement.
value	number	yes	JSON-stable numeric value assigned on every cycle.

Example 1 (repro_cli) — reproduction boundary. This diagnostic can appear in a successful inspect report. Reproduce it with pyfcstm inspect -i <file> --format json and read the diagnostics[] array.

def int counter = 0;
state Root {
    state Idle {
        during { counter = (2 + 3) * 4; }
    }
    [*] -> Idle;
}

Example 2 (boundary_only) — repair direction for W_DURING_CONST_ASSIGN. A typical repair is move_to_enter on action: Move the assignment to enter if it should run once on state entry.

Example 3 (boundary_only) — anti-pattern boundary for W_DURING_CONST_ASSIGN. Do not suppress the warning by adding a meaningless arithmetic no-op.

W_ASPECT_NO_DESCENDANT_LEAF

Registry facts. Severity warning; emit tier static_pipeline; capability pure_static; span object lifecycle_action.

Meaning. A >> during aspect is attached to a state with no descendant non-pseudo leaf states, so the aspect cannot affect any leaf cycle.

LLM repair summary. The aspect action has no descendant leaf state to wrap, so it has no modeled runtime target.

Refs schema

Field	Type	Required	Meaning
composite_path	str	yes	Dotted path of the state declaring the aspect.
aspect	str	yes	Aspect direction. (enum: before, after)

Example 1 (repro_cli) — reproduction boundary. This diagnostic can appear in a successful inspect report. Reproduce it with pyfcstm inspect -i <file> --format json and read the diagnostics[] array.

state Root {
    pseudo state Marker;
    [*] -> Marker;
    >> during before { }
}

Example 2 (boundary_only) — repair direction for W_ASPECT_NO_DESCENDANT_LEAF. A typical repair is add_leaf on composite_state: Add the intended descendant leaf state under this composite.

Example 3 (boundary_only) — anti-pattern boundary for W_ASPECT_NO_DESCENDANT_LEAF. Do not replace it with a normal during action unless the execution semantics really should change.

I_ENTER_DURING_CONTRADICT

Registry facts. Severity info; emit tier verify_pipeline; capability requires_solver; span object lifecycle_action.

Meaning. Entry-time assignments make a first-cycle during branch condition predetermined; the enter postcondition does not leave both during branches feasible.

LLM repair summary. After entering the leaf, the first during cycle already has a fixed branch decision. This may be intentional initialization logic, but the branch is not genuinely conditional on the first cycle.

Refs schema

Field	Type	Required	Meaning
algorithm_name	str	yes	Verify registry algorithm that produced the raw finding.
verification_scope	str	yes	Verify scope for this finding. (enum: smt_local)
state_path	str	yes	Dotted leaf state path inspected by the lifecycle algorithm.
condition	str	yes	First-cycle during condition proven predetermined.
condition_source	str	yes	Source label for the condition inside the during operation block.
branch_taken	str	yes	Branch direction forced after entry. (enum: true, false)

Example 1 (verify_opt_in) — reproduction boundary. This diagnostic requires optional verify integration. Reproduce it with pyfcstm inspect -i <file> --enable-verify --max-complexity-tier smt_linear --format json; the default structural verify budget does not run the solver-local algorithm that emits it.

def int x = 0;
state System {
    state A {
        enter { x = 1; }
        during {
            if [x > 0] { x = x + 1; } else { x = x - 1; }
        }
    }
    [*] -> A;
}

Example 2 (boundary_only) — repair direction for I_ENTER_DURING_CONTRADICT. A typical repair is review_enter_during_relation on lifecycle_action: Check whether enter assignments intentionally force the first during branch.

Example 3 (boundary_only) — anti-pattern boundary for I_ENTER_DURING_CONTRADICT. Do not remove the enter action just to make the first-cycle branch variable; entry side effects may be required.

W_COMPOSITE_INIT_INCOMPLETE

Registry facts. Severity warning; emit tier verify_pipeline; capability requires_solver; span object composite_block.

Meaning. A composite state’s initial transitions do not jointly cover all variable and event inputs.

LLM repair summary. There is a variable/event assignment for which none of the composite initial transitions can fire, so entry can get stuck at the composite.

Refs schema

Field	Type	Required	Meaning
algorithm_name	str	yes	Verify registry algorithm that produced the raw finding.
verification_scope	str	yes	Verify scope for this finding. (enum: smt_local)
composite_path	str	yes	Dotted composite state path whose initial transitions have a coverage gap.
init_transition_count	int	yes	Number of initial transitions considered for the composite.
init_transitions	list[str]	yes	Stable summaries of the initial transitions considered.
witness	str_or_null	no	Solver model demonstrating an uncovered input valuation, when available.

Example 1 (verify_opt_in) — reproduction boundary. This diagnostic requires optional verify integration. Reproduce it with pyfcstm inspect -i <file> --enable-verify --max-complexity-tier smt_linear --format json; the default structural verify budget does not run the solver-local algorithm that emits it.

def int x = 0;
state System {
    state A;
    state B;
    [*] -> A : if [x > 0];
    [*] -> B : if [x < 0];
}

Example 2 (boundary_only) — repair direction for W_COMPOSITE_INIT_INCOMPLETE. A typical repair is add_catch_all_initial on composite_state: Add an unconditional fallback initial transition if one child should be the default.

Example 3 (boundary_only) — anti-pattern boundary for W_COMPOSITE_INIT_INCOMPLETE. Do not add overlapping initial transitions without reviewing declaration order and guard intent.

Data-flow diagnostics

W_UNREFERENCED_VAR

Registry facts. Severity warning; emit tier static_pipeline; capability pure_static; span object variable_declaration.

Meaning. A variable cannot affect any transition guard either directly or through the action/effect use-def graph, and no abstract action is visible that might use it outside the DSL.

LLM repair summary. This variable does not participate in model decisions. It is dead from the DSL’s guard-affect data-flow perspective.

Refs schema

Field	Type	Required	Meaning
var_name	str	yes	Variable name.
init_value	str	yes	Source text of the initial value.
definition_delete_anchor	str	no	Variable name repeated only when the declaration has no DSL reads or writes, so deleting the declaration alone is a safe quick-fix.
suggested_fix	dict	no	Structured quick-fix payload for removing the variable definition.

Example 1 (repro_cli) — reproduction boundary. This diagnostic can appear in a successful inspect report. Reproduce it with pyfcstm inspect -i <file> --format json and read the diagnostics[] array.

def int unused = 0;
def int ready = 0;
state Root {
    state A;
    state B;
    [*] -> A;
    A -> B : if [ready > 0];
}

Example 2 (boundary_only) — repair direction for W_UNREFERENCED_VAR. A typical repair is remove_variable on variable_definition: Remove the variable and related writes if it was speculative scaffolding.

Example 3 (boundary_only) — anti-pattern boundary for W_UNREFERENCED_VAR. Do not add a dummy guard reference only to silence the diagnostic.

I_UNREFERENCED_VAR_MAYBE_ABSTRACT

Registry facts. Severity info; emit tier static_pipeline; capability pure_static; span object variable_declaration.

Meaning. A variable cannot affect any transition guard through DSL data-flow, but at least one visible abstract action may use it outside the DSL.

LLM repair summary. This variable is unused by DSL guard-affect data-flow, but abstract action implementations may still use it.

Refs schema

Field	Type	Required	Meaning
var_name	str	yes	Variable name.
abstract_actions_in_scope	list[str]	yes	Abstract action owners that may access the variable. FCSTM variables are global, so this is the full machine abstract-action inventory.

Example 1 (repro_cli) — reproduction boundary. This diagnostic can appear in a successful inspect report. Reproduce it with pyfcstm inspect -i <file> --format json and read the diagnostics[] array.

def int maybe_external = 0;
def int ready = 0;
state Root {
    state A { enter abstract ExternalHook; }
    state B;
    [*] -> A;
    A -> B : if [ready > 0];
}

Example 2 (boundary_only) — repair direction for I_UNREFERENCED_VAR_MAYBE_ABSTRACT. A typical repair is inspect_abstract_action on abstract_action: Check the external implementation before removing the variable.

Example 3 (boundary_only) — anti-pattern boundary for I_UNREFERENCED_VAR_MAYBE_ABSTRACT. Do not remove the variable without checking the abstract implementation.

W_UNWRITTEN_READ_VAR

Registry facts. Severity warning; emit tier static_pipeline; capability pure_static; span object variable_declaration.

Meaning. A variable is read in guards or actions but is never written by any lifecycle action or transition effect.

LLM repair summary. The variable is used as input but never updated after its initial definition, so model behavior may be accidentally constant.

Refs schema

Field	Type	Required	Meaning
var_name	str	yes	Variable name.
read_states	list[str]	yes	State paths where the variable is read.
init_value	str	yes	Source text of the initial value.

Example 1 (repro_cli) — reproduction boundary. This diagnostic can appear in a successful inspect report. Reproduce it with pyfcstm inspect -i <file> --format json and read the diagnostics[] array.

def int ready = 0;
state Root {
    state A;
    state B;
    [*] -> A;
    A -> B : if [ready > 0];
}

Example 2 (boundary_only) — repair direction for W_UNWRITTEN_READ_VAR. A typical repair is add_write on action_or_effect: Add the intended update if the variable should change.

Example 3 (boundary_only) — anti-pattern boundary for W_UNWRITTEN_READ_VAR. Do not add a meaningless self-assignment.

W_WRITE_ONLY_VAR

Registry facts. Severity warning; emit tier static_pipeline; capability pure_static; span object variable_declaration.

Meaning. A variable is written by actions or effects but is never read by any guard, action, or transition effect expression.

LLM repair summary. The variable is updated but never influences model behavior.

Refs schema

Field	Type	Required	Meaning
var_name	str	yes	Variable name.
written_states	list[str]	yes	State paths where the variable is written.

Example 1 (repro_cli) — reproduction boundary. This diagnostic can appear in a successful inspect report. Reproduce it with pyfcstm inspect -i <file> --format json and read the diagnostics[] array.

def int counter = 0;
state Root {
    state A { during { counter = 1; } }
    [*] -> A;
}

Example 2 (boundary_only) — repair direction for W_WRITE_ONLY_VAR. A typical repair is add_read on guard_or_action: Read the variable where it should affect behavior.

Example 3 (boundary_only) — anti-pattern boundary for W_WRITE_ONLY_VAR. Do not add an unused read just to silence the warning.

Numeric and target-profile diagnostics

W_LITERAL_TYPE_NARROWING

Registry facts. Severity warning; emit tier static_pipeline; capability pure_static; span object expression.

Meaning. An int variable is initialized or assigned directly from a floating-point literal, which can imply silent narrowing in generated code. Compound expressions containing floating-point literals are out of scope for this warning.

LLM repair summary. A direct float literal value flows into an int variable. The model may truncate or generate target-language code with a narrowing conversion; compound expressions such as 3.0 + 0.5 are intentionally outside this warning’s scope.

Refs schema

Field	Type	Required	Meaning
var_name	str	yes	Target variable name.
target_type	str	yes	Declared target variable type. (enum: int)
source_expr	str	yes	Source text of the direct float literal.

Example 1 (repro_cli) — reproduction boundary. This diagnostic can appear in a successful inspect report. Reproduce it with pyfcstm inspect -i <file> --format json and read the diagnostics[] array.

def int truncated = 3.5;
state Root { state A; [*] -> A; }

Example 2 (boundary_only) — repair direction for W_LITERAL_TYPE_NARROWING. A typical repair is change_type on variable_definition: Use def float when fractional values are intended.

Example 3 (boundary_only) — anti-pattern boundary for W_LITERAL_TYPE_NARROWING. Do not silently rely on target-language truncation rules.

W_NUMERIC_LITERAL_OUT_OF_TARGET_RANGE

Registry facts. Severity warning; emit tier static_pipeline; capability pure_static; span object expression.

Meaning. An integer literal that would be rendered into a C/C++ family template falls outside the default PYFCSTM_GENERATED_INT64 signed range. This warning is target-profile-specific: Python generated runtimes may not have the same fixed-width integer carrying risk.

LLM repair summary. A literal intended for C/C++ generated code exceeds the default 64-bit signed integer profile. Treat this as a C/C++ deployment-profile warning, not as proof that Python generated code is invalid.

Refs schema

Field	Type	Required	Meaning
target_family	str	yes	Target family whose default deployment profile owns this risk. (enum: c_family)
target_templates	list[str]	yes	Ordered target templates covered by this default C/C++ profile: c, c_poll, cpp, cpp_poll. (item enum: c, c_poll, cpp, cpp_poll; exact: c, c_poll, cpp, cpp_poll)
runtime_note	str	yes	Human-readable note that this is a C/C++ deployment-profile risk and that Python generated runtimes may not have the same risk.
context	str	yes	Expression location where the literal appears. (enum: var_initializer, guard, transition_effect, lifecycle_action)
statement_kind	str	no	Statement shape when the expression is an operation assignment RHS. (enum: operation_assignment)
expr_text	str	yes	Source text of the expression containing the literal.
literal_text	str	yes	Source text of the integer literal after applying a unary sign when present.
target_bits	int	yes	Target integer width in bits.
signed	bool	yes	Whether the target integer profile is signed.
min_value_text	str	yes	Decimal text of the minimum representable target value.
max_value_text	str	yes	Decimal text of the maximum representable target value.
var_name	str	no	Variable receiving the literal when the location can be named.

Example 1 (repro_cli) — reproduction boundary. This diagnostic can appear in a successful inspect report. Reproduce it with pyfcstm inspect -i <file> --format json and read the diagnostics[] array.

def int too_large = 9223372036854775808;
state Root { state A; [*] -> A; }

Example 2 (boundary_only) — repair direction for W_NUMERIC_LITERAL_OUT_OF_TARGET_RANGE. A typical repair is reduce_literal on expression: Keep integer literals within the documented C/C++ target range when deploying to C-family templates.

Example 3 (boundary_only) — anti-pattern boundary for W_NUMERIC_LITERAL_OUT_OF_TARGET_RANGE. Do not describe this as a target-independent FCSTM model error; the risk is tied to the C/C++ default integer profile.

W_NUMERIC_CONSTANT_DIVISION_BY_ZERO

Registry facts. Severity warning; emit tier static_pipeline; capability const_fold; span object expression.

Meaning. A / or % operation has a right-hand side that the lightweight literal-only constant folder can classify as zero. This is reported as a C/C++ deployment-profile risk because generated C/C++ code needs an explicit definition or failure channel; Python runtime exception semantics are different.

LLM repair summary. A division or modulo RHS is statically zero under the lightweight literal-only folder. For C/C++ generated code this needs a design fix or explicit failure policy; do not conflate it with Python’s exception model.

Refs schema

Field	Type	Required	Meaning
target_family	str	yes	Target family whose default deployment profile owns this risk. (enum: c_family)
target_templates	list[str]	yes	Ordered target templates covered by this default C/C++ profile: c, c_poll, cpp, cpp_poll. (item enum: c, c_poll, cpp, cpp_poll; exact: c, c_poll, cpp, cpp_poll)
runtime_note	str	yes	Human-readable note that this is a C/C++ deployment-profile risk and that Python generated runtimes may not have the same failure contract.
context	str	yes	Expression location where the operator appears. (enum: var_initializer, guard, transition_effect, lifecycle_action)
statement_kind	str	no	Statement shape when the expression is an operation assignment RHS. (enum: operation_assignment)
expr_text	str	yes	Source text of the expression containing the operation.
operator	str	yes	Operator whose right-hand side folded to zero. (enum: /, %)
rhs_text	str	yes	Source text of the right-hand side that folded to zero.

Example 1 (repro_cli) — reproduction boundary. This diagnostic can appear in a successful inspect report. Reproduce it with pyfcstm inspect -i <file> --format json and read the diagnostics[] array.

def int result = 0;
def int input = 1;
state Root {
    state A;
    state B;
    [*] -> A;
    A -> B effect { result = input / (1 - 1); };
}

Example 2 (boundary_only) — repair direction for W_NUMERIC_CONSTANT_DIVISION_BY_ZERO. A typical repair is fix_denominator on expression: Replace the zero RHS with a non-zero expression or guard the operation before C/C++ deployment.

Example 3 (boundary_only) — anti-pattern boundary for W_NUMERIC_CONSTANT_DIVISION_BY_ZERO. Do not require the whole expression to be literal-only; only the RHS of / or % needs to fold to zero.

W_NUMERIC_SHIFT_COUNT_OUT_OF_TARGET_RANGE

Registry facts. Severity warning; emit tier static_pipeline; capability const_fold; span object expression.

Meaning. A shift count folds to a constant below zero or not less than the default C/C++ target integer width. This is a C/C++ 64-bit deployment-profile portability risk; Python big-integer shifting is not the same target contract.

LLM repair summary. A shift count is statically outside the C/C++ default 64-bit profile. Treat this as a target-profile portability warning, not as a Python generated-runtime error.

Refs schema

Field	Type	Required	Meaning
target_family	str	yes	Target family whose default deployment profile owns this risk. (enum: c_family)
target_templates	list[str]	yes	Ordered target templates covered by this default C/C++ profile: c, c_poll, cpp, cpp_poll. (item enum: c, c_poll, cpp, cpp_poll; exact: c, c_poll, cpp, cpp_poll)
runtime_note	str	yes	Human-readable note that this is a C/C++ deployment-profile risk and that Python generated runtimes may not have the same fixed-width shift risk.
context	str	yes	Expression location where the shift appears. (enum: var_initializer, guard, transition_effect, lifecycle_action)
statement_kind	str	no	Statement shape when the expression is an operation assignment RHS. (enum: operation_assignment)
expr_text	str	yes	Source text of the shift expression.
operator	str	yes	Shift operator. (enum: <<, >>)
target_bits	int	yes	Target integer width in bits.
shift_count_text	str	yes	Source text of the shift count after lightweight folding.

Example 1 (repro_cli) — reproduction boundary. This diagnostic can appear in a successful inspect report. Reproduce it with pyfcstm inspect -i <file> --format json and read the diagnostics[] array.

def int flags = 1;
state Root {
    state A;
    state B;
    [*] -> A;
    A -> B : if [(flags << 64) != 0];
}

Example 2 (boundary_only) — repair direction for W_NUMERIC_SHIFT_COUNT_OUT_OF_TARGET_RANGE. A typical repair is bound_shift_count on expression: Keep constant shift counts within 0 <= count < 64 for the default C/C++ profile.

Example 3 (boundary_only) — anti-pattern boundary for W_NUMERIC_SHIFT_COUNT_OUT_OF_TARGET_RANGE. Do not report dynamic shift counts as proven unsafe from this catalog-only rule.

W_NUMERIC_FLOAT_BITWISE

Registry facts. Severity warning; emit tier static_pipeline; capability pure_static; span object expression.

Meaning. A value known to be float participates in a bitwise or shift operator that belongs to the C/C++ integer operation profile. The warning is target-profile-specific even when other runtimes may also reject some float-bitwise shapes for different reasons.

LLM repair summary. A float-shaped operand reaches a C/C++ integer bitwise operation. Keep the diagnostic target-specific and use the operand type refs to explain why the expression is considered risky.

Refs schema

Field	Type	Required	Meaning
target_family	str	yes	Target family whose default deployment profile owns this risk. (enum: c_family)
target_templates	list[str]	yes	Ordered target templates covered by this default C/C++ profile: c, c_poll, cpp, cpp_poll. (item enum: c, c_poll, cpp, cpp_poll; exact: c, c_poll, cpp, cpp_poll)
runtime_note	str	yes	Human-readable note that this is a C/C++ integer-operation profile risk and that other runtimes may fail for different reasons.
context	str	yes	Expression location where the bitwise operation appears. (enum: var_initializer, guard, transition_effect, lifecycle_action)
statement_kind	str	no	Statement shape when the expression is an operation assignment RHS. (enum: operation_assignment)
expr_text	str	yes	Source text of the bitwise expression.
operator	str	yes	Bitwise or shift operator involving a float-shaped operand. (enum: &, ^, |, <<, >>)
operand_types	list[str]	yes	Operand type tags in expression order. Allowed members are int, float, and unknown. (item enum: int, float, unknown)
operand_type_sources	list[str]	yes	Evidence source for each operand type tag. Allowed members are literal, declared_var, and local_expression. (item enum: literal, declared_var, local_expression)

Example 1 (repro_cli) — reproduction boundary. This diagnostic can appear in a successful inspect report. Reproduce it with pyfcstm inspect -i <file> --format json and read the diagnostics[] array.

def float gain = 1.5;
def int flags = 1;
state Root {
    state A {
        during { flags = flags & gain; }
    }
    [*] -> A;
}

Example 2 (boundary_only) — repair direction for W_NUMERIC_FLOAT_BITWISE. A typical repair is use_integer_operand on expression: Replace the float operand with an integer flag/mask value when deploying to C/C++ templates.

Example 3 (boundary_only) — anti-pattern boundary for W_NUMERIC_FLOAT_BITWISE. Do not describe this only as a generic Python TypeError; the shared contract is about the C/C++ integer-operation profile.

Topology and design-health diagnostics

W_UNREACHABLE_STATE

Registry facts. Severity warning; emit tier static_pipeline; capability pure_static; span object state_identifier.

Meaning. A state is not reachable from the model’s root entry path via any sequence of normal or forced transitions.

LLM repair summary. This state cannot be entered at runtime; the surrounding transitions never lead to it. It is dead from the machine’s perspective.

Refs schema

Field	Type	Required	Meaning
state_path	str	yes	Dotted path of the unreachable state.

Example 1 (repro_cli) — reproduction boundary. This diagnostic can appear in a successful inspect report. Reproduce it with pyfcstm inspect -i <file> --format json and read the diagnostics[] array.

state Root {
    state Idle;
    state Orphan;
    [*] -> Idle;
}

Example 2 (boundary_only) — repair direction for W_UNREACHABLE_STATE. A typical repair is add_inbound_transition on state: Add a transition that reaches the state if it was meant to be used.

Example 3 (boundary_only) — anti-pattern boundary for W_UNREACHABLE_STATE. Do not add a self-loop to mask the unreachability.

W_DEADLOCK_LEAF

Registry facts. Severity warning; emit tier static_pipeline; capability pure_static; span object state_identifier.

Meaning. A non-pseudo leaf state has no outgoing transition.

LLM repair summary. This leaf state has no outgoing transition, so once the machine enters it there is no modeled way to leave.

Refs schema

Field	Type	Required	Meaning
state_path	str	yes	Dotted path of the deadlocking leaf state.
parent_path	str	no	Dotted path of the leaf state’s parent. Present only when an exit-transition quick-fix can be inserted inside a parent state.
reason	str	yes	Why the leaf is considered a deadlock. (enum: no_outgoing_transition)
suggested_fix	dict	no	Structured quick-fix payload for adding a parent exit transition.

Example 1 (repro_cli) — reproduction boundary. This diagnostic can appear in a successful inspect report. Reproduce it with pyfcstm inspect -i <file> --format json and read the diagnostics[] array.

state Root {
    state A;
    [*] -> A;
}

Example 2 (boundary_only) — repair direction for W_DEADLOCK_LEAF. A typical repair is add_transition on state: Add a modeled transition to the next intended state.

Example 3 (boundary_only) — anti-pattern boundary for W_DEADLOCK_LEAF. Do not add a self-loop just to silence the warning.

W_HIGH_VAR_TO_LEAF_RATIO

Registry facts. Severity warning; emit tier static_pipeline; capability pure_static; span object composite_block.

Meaning. The number of variables is high relative to the number of non-pseudo leaf states.

LLM repair summary. The model has many variables for its number of leaf states, which often indicates flag bloat or speculative state that does not belong in the DSL.

Refs schema

Field	Type	Required	Meaning
n_vars	int	yes	Number of top-level variable definitions.
n_leaf_states	int	yes	Number of non-pseudo leaf states.
actual	number	yes	Actual n_vars / max(n_leaf_states, 1) ratio.
threshold	number	yes	Effective threshold used for this inspection call.

Example 1 (repro_cli) — reproduction boundary. This diagnostic can appear in a successful inspect report. Reproduce it with pyfcstm inspect -i <file> --format json and read the diagnostics[] array.

def int a = 0;
def int b = 0;
def int c = 0;
state Root { state A; [*] -> A; }

Example 2 (boundary_only) — repair direction for W_HIGH_VAR_TO_LEAF_RATIO. A typical repair is audit_variables on variable_definitions: Remove or consolidate variables that do not represent durable machine state.

Example 3 (boundary_only) — anti-pattern boundary for W_HIGH_VAR_TO_LEAF_RATIO. Do not raise the threshold without checking whether the variables influence behavior.

W_DEEP_HIERARCHY

Registry facts. Severity warning; emit tier static_pipeline; capability pure_static; span object state_identifier.

Meaning. The state hierarchy exceeds the configured maximum depth.

LLM repair summary. The hierarchy is deeper than the configured readability threshold, making lifecycle order and transition scope harder to reason about.

Refs schema

Field	Type	Required	Meaning
max_depth	int	yes	Maximum hierarchy depth found in the model.
deepest_path	str	yes	One deepest state path that triggered the warning.
actual	int	yes	Actual maximum hierarchy depth.
threshold	int	yes	Effective threshold used for this inspection call.

Example 1 (repro_cli) — reproduction boundary. This diagnostic can appear in a successful inspect report. Reproduce it with pyfcstm inspect -i <file> --format json and read the diagnostics[] array.

state Root { state A { state B { state C; [*] -> C; } [*] -> B; } [*] -> A; }

Example 2 (boundary_only) — repair direction for W_DEEP_HIERARCHY. A typical repair is flatten_hierarchy on state_tree: Collapse levels that do not add lifecycle or transition semantics.

Example 3 (boundary_only) — anti-pattern boundary for W_DEEP_HIERARCHY. Do not flatten a level that carries required enter, exit, during, or aspect semantics.

W_LARGE_COMPOSITE

Registry facts. Severity warning; emit tier static_pipeline; capability pure_static; span object composite_block.

Meaning. A composite state has more direct children than the configured threshold.

LLM repair summary. A single composite state owns many direct children, which can make transition review and initial-state reasoning difficult.

Refs schema

Field	Type	Required	Meaning
composite_path	str	yes	Dotted path of the large composite state.
n_children	int	yes	Number of direct child states.
actual	int	yes	Actual direct child count.
threshold	int	yes	Effective threshold used for this inspection call.

Example 1 (repro_cli) — reproduction boundary. This diagnostic can appear in a successful inspect report. Reproduce it with pyfcstm inspect -i <file> --format json and read the diagnostics[] array.

state Root { state A; state B; state C; [*] -> A; }

Example 2 (boundary_only) — repair direction for W_LARGE_COMPOSITE. A typical repair is group_children on composite_state: Introduce meaningful nested composites to group related child states.

Example 3 (boundary_only) — anti-pattern boundary for W_LARGE_COMPOSITE. Do not add arbitrary grouping states that have no semantic meaning.

I_NONTRIVIAL_SCC

Registry facts. Severity info; emit tier verify_pipeline; capability pure_static; span object state_identifier.

Meaning. A non-trivial strongly connected component exists in the guard-agnostic leaf-level topology graph.

LLM repair summary. The topology contains a cycle. This is often intentional in state machines, so treat it as a review prompt rather than a direct defect.

Refs schema

Field	Type	Required	Meaning
algorithm_name	str	yes	Verify registry algorithm that produced the raw finding.
verification_scope	str	yes	Verify scope for this finding. (enum: topological_only)
representative_state_path	str	yes	One state path from the reported strongly connected component.
scc	list[str]	yes	State paths in the non-trivial strongly connected component.

Example 1 (verify_opt_in) — reproduction boundary. This diagnostic requires optional verify integration. Reproduce it with pyfcstm inspect -i <file> --enable-verify --max-complexity-tier smt_linear --format json; the default structural verify budget does not run the solver-local algorithm that emits it.

state System {
    state A;
    state B;
    [*] -> A;
    A -> B;
    B -> A;
}

Example 2 (boundary_only) — repair direction for I_NONTRIVIAL_SCC. A typical repair is review_cycle on topology: Confirm the cycle has a deliberate runtime exit or event-driven purpose.

Example 3 (boundary_only) — anti-pattern boundary for I_NONTRIVIAL_SCC. Do not delete cyclic transitions automatically; cyclic control flow can be valid FCSTM behavior.

W_TOPOLOGICAL_NOEXIT

Registry facts. Severity warning; emit tier verify_pipeline; capability pure_static; span object state_identifier.

Meaning. A root-reachable leaf or cycle has no guard-agnostic route to the root exit sink.

LLM repair summary. From the current topology, execution can enter a region that has no structural path to terminate at the root exit.

Refs schema

Field	Type	Required	Meaning
algorithm_name	str	yes	Verify registry algorithm that produced the raw finding.
verification_scope	str	yes	Verify scope for this finding. (enum: topological_only)
representative_state_path	str	yes	One state path from the no-exit counterexample.
counterexample_kind	str	yes	Shape of the topological counterexample. (enum: trap_cycle, deadlock)
scc	list[str]	yes	Trap-cycle component paths, or an empty list for a deadlock leaf.

Example 1 (verify_opt_in) — reproduction boundary. This diagnostic requires optional verify integration. Reproduce it with pyfcstm inspect -i <file> --enable-verify --max-complexity-tier smt_linear --format json; the default structural verify budget does not run the solver-local algorithm that emits it.

state System {
    state A;
    state B;
    [*] -> A;
    A -> B;
}

Example 2 (boundary_only) — repair direction for W_TOPOLOGICAL_NOEXIT. A typical repair is add_exit_transition on topology: Add a route from the stuck state or cycle to an exit-capable path.

Example 3 (boundary_only) — anti-pattern boundary for W_TOPOLOGICAL_NOEXIT. Do not add an unconditional exit without checking lifecycle and event semantics.

I_TOPOLOGICAL_NON_TERMINATING

Registry facts. Severity info; emit tier verify_pipeline; capability pure_static; span object state_identifier.

Meaning. The topology does not force all root-reachable executions to eventually reach the root terminator.

LLM repair summary. The structural graph allows a path that can avoid termination forever. This may be a valid service loop, but it should be reviewed explicitly.

Refs schema

Field	Type	Required	Meaning
algorithm_name	str	yes	Verify registry algorithm that produced the raw finding.
verification_scope	str	yes	Verify scope for this finding. (enum: topological_only)
representative_state_path	str	yes	One state path from the non-terminating counterexample.
counterexample_path	list[str]	yes	Representative cycle or deadlock path reported by topology verify.

Example 1 (verify_opt_in) — reproduction boundary. This diagnostic requires optional verify integration. Reproduce it with pyfcstm inspect -i <file> --enable-verify --max-complexity-tier smt_linear --format json; the default structural verify budget does not run the solver-local algorithm that emits it.

state System {
    state A;
    [*] -> A;
    A -> A;
    A -> [*];
}

Example 2 (boundary_only) — repair direction for I_TOPOLOGICAL_NON_TERMINATING. A typical repair is review_nontermination on topology: Decide whether the non-terminating path is intended.

Example 3 (boundary_only) — anti-pattern boundary for I_TOPOLOGICAL_NON_TERMINATING. Do not treat every loop as a bug; long-running control loops are common state-machine behavior.

Compatibility-only and miscellaneous diagnostics

W_INITIAL_UNCONDITIONAL_MISSING

Registry facts. Severity warning; emit tier static_pipeline; capability pure_static; span object composite_block.

Meaning. A composite state has no unconditional [*] -> child entry transition. Guarded or event-triggered entry transitions do not provide a guaranteed initial child.

LLM repair summary. The composite state can fail to choose an initial child because no unconditional entry transition is declared.

Refs schema

Field	Type	Required	Meaning
composite_path	str	yes	Dotted path of the composite state.
existing_conditional_count	int	yes	Number of existing initial transitions that are not unconditional.
first_child_name	str	no	First declared non-pseudo child state name used as the fallback insertion target.
suggested_fix	dict	no	Structured quick-fix payload for inserting an unconditional entry transition.

Example 1 (repro_cli) — reproduction boundary. This diagnostic can appear in a successful inspect report. Reproduce it with pyfcstm inspect -i <file> --format json and read the diagnostics[] array.

def int ready = 0;
state Root {
    state A;
    [*] -> A : if [ready > 0];
}

Example 2 (boundary_only) — repair direction for W_INITIAL_UNCONDITIONAL_MISSING. A typical repair is add_unconditional_initial on composite_state: Add a fallback [*] -> Child; entry transition.

Example 3 (boundary_only) — anti-pattern boundary for W_INITIAL_UNCONDITIONAL_MISSING. Do not assume a guarded initial transition always fires without proving the guard.

W_DEAD_NAMED_ACTION

Registry facts. Severity warning; emit tier static_pipeline; capability pure_static; span object named_action_declaration.

Meaning. A named action belongs to an unreachable state and is not referenced by any reachable action ref.

LLM repair summary. This named action cannot run through the reachable state graph and is not referenced from elsewhere.

Refs schema

Field	Type	Required	Meaning
function_name	str	yes	Named action identifier.
defined_in	str	yes	Dotted path of the state where the action is defined.

Example 1 (repro_cli) — reproduction boundary. This diagnostic can appear in a successful inspect report. Reproduce it with pyfcstm inspect -i <file> --format json and read the diagnostics[] array.

state Root {
    state A;
    state B { enter Cleanup {} }
    [*] -> A;
}

Example 2 (boundary_only) — repair direction for W_DEAD_NAMED_ACTION. A typical repair is connect_state on state: Add a transition path to the owning state if the action matters.

Example 3 (boundary_only) — anti-pattern boundary for W_DEAD_NAMED_ACTION. Do not add an unrelated ref just to silence the warning.

W_NAMED_ACTION_SHADOWS_ANCESTOR

Registry facts. Severity warning; emit tier static_pipeline; capability pure_static; span object named_action_declaration.

Meaning. A named lifecycle action reuses the same function name as an ancestor-scoped named action.

LLM repair summary. A nested state defines a named action with the same name as an ancestor action. Relative action refs can become hard to audit because the same leaf name means different functions at different hierarchy levels.

Refs schema

Field	Type	Required	Meaning
function_name	str	yes	Reused named action identifier.
inner_state_path	str	yes	Dotted path of the state containing the shadowing action.
outer_state_path	str	yes	Dotted path of the ancestor state containing the shadowed action.

Example 1 (repro_cli) — reproduction boundary. This diagnostic can appear in a successful inspect report. Reproduce it with pyfcstm inspect -i <file> --format json and read the diagnostics[] array.

state Root {
    enter Sync { }
    state Child { enter Sync { } }
    [*] -> Child;
}

Example 2 (boundary_only) — repair direction for W_NAMED_ACTION_SHADOWS_ANCESTOR. A typical repair is rename_inner_action on named_action: Give the nested action a distinct name when it implements different behavior.

Example 3 (boundary_only) — anti-pattern boundary for W_NAMED_ACTION_SHADOWS_ANCESTOR. Do not leave the shadowing name in place unless the scope distinction is intentional and documented outside the DSL.