Finite State Machine Simulator mechanism

Model scope

The core DFA and non-epsilon-NFA algorithms are standard. The instrument needs an explicit contract for epsilon transitions, incomplete transition tables, invalid input symbols, NFA acceptance semantics, and deterministic rendering of subset traces before it can receive an unqualified PASS.

• The DFA rule δ(q,a) is standard and correct, provided δ is deterministic and total for every state and input symbol; the specification does not state how missing transitions are handled.
• NFA simulation by propagating subsets of states is standard and correct for NFAs without epsilon transitions.
• If epsilon transitions are supported, subset construction must apply epsilon-closure before processing the first symbol, after every symbol, and for final acceptance; this is not specified.
• The specification does not define whether an NFA accepts when any state in the final reachable subset is accepting, although that is the standard rule.

Units and conventions

• There are no physical units; states and alphabet symbols are discrete identifiers.
• Input symbols must be matched exactly as declared in the alphabet; case sensitivity, Unicode normalization, and treatment of undeclared symbols should be specified.
• The empty input string is a valid input and is accepted exactly when the start state, or the epsilon-closure of the start state for an epsilon-NFA, contains an accepting state.

Inspectable vector

One of 4 source-bound review vectors:

{
  "inputs": {
    "type": "DFA",
    "states": [
      "q_even",
      "q_odd"
    ],
    "alphabet": [
      "0",
      "1"
    ],
    "transitions": {
      "q_even": {
        "0": "q_even",
        "1": "q_odd"
      },
      "q_odd": {
        "0": "q_odd",
        "1": "q_even"
      }
    },
    "start_state": "q_even",
    "accept_states": [
      "q_even"
    ],
    "input_string": "1010"
  },
  "expected_outputs": {
    "verdict": "accepted",
    "state_trace": [
      "q_even",
      "q_odd",
      "q_odd",
      "q_even",
      "q_even"
    ]
  },
  "working": "Start q_even. Read 1: δ(q_even,1)=q_odd. Read 0: δ(q_odd,0)=q_odd. Read 1: δ(q_odd,1)=q_even. Read 0: δ(q_even,0)=q_even. Final state q_even is accepting, so the result is accepted."
}

Failure boundary

BREAK_CLAIMED · SELF_FLAGGED

The specification does not define behavior for an input symbol outside the declared alphabet or for an undefined transition. Such an input makes δ undefined, so an implementation that silently continues, invents a state, or returns a normal verdict would break the stated simulation model.

Other records

Sources and evidence

These pointers bind the page to evidence. They do not grant authority or collapse verification into deployment.

• VERIFIED_LEDGER.json
• evidence-tranche6/tranche6-results.json
• BOUNDARY_HAZARD_CATALOG.json