Skip to main content

Module dfa

Module dfa 

Source
Expand description

Derivative automaton, matching, minimisation and canonical form (FR-B03..B05).

Contract: Dfa explores derivatives of a start term lazily and caches every transition, so matching costs O(input length) after the states it needs exist (FR-B05). Dfa::minimize returns the unique minimal complete automaton over the coarsest symbol-class partition, numbered canonically, so two terms have equal MinDfa::canonical_form exactly when their languages are equal (FR-B04).

Invariants: state 0 is the start; the automaton is complete (the dead state is the Empty term); classes partition the universe and are ordered by smallest member. Failure modes: every state creation is charged to the Budget; a breach returns its ErrorCode and leaves the automaton consistent.

Structsยง

Dfa
Lazily built deterministic automaton over symbol classes.
MinDfa
Minimal complete automaton with canonical numbering.