Skip to content

docs: guides for the library, algorithms, grammar, StateMate and reference #126

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
thethinkmachine merged 1 commit into from
Oct 1, 2026
Merged

docs: guides for the library, algorithms, grammar, StateMate and reference #126

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
48 changes: 43 additions & 5 deletions README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,6 +16,7 @@ machine types, from DFAs to multi-tape Turing machines and ω-automata.
[**Open in the browser**](https://thethinkmachine.github.io/AutomataStudio/) ·
[Download the desktop app](https://github.com/thethinkmachine/AutomataStudio/releases/latest) ·
[Machine library](https://thethinkmachine.github.io/automata-library/) ·
[Guides](#guides) ·
[Cite](#citation)

![An 8-tape Turing machine executing a stored program, one step per frame](docs/media/cpu.gif)
Expand All @@ -32,6 +33,7 @@ accumulator after 331 steps.</sup>
## Contents

- [Getting started](#getting-started)
- [Guides](#guides)
- [Features](#features)
- [Algorithms and theory](#algorithms-and-theory)
- [Command line](#command-line)
Expand Down Expand Up @@ -79,6 +81,21 @@ machines to open and remix.
expression by state elimination, the tuple `M = (Q⁵, Σ², δ¹⁰, q₀, F¹)`, and an
acceptance fingerprint of the words decided so far.</sup>

## Guides

Each part of the app has a guide of its own in [`docs/`](docs), with clips and
screenshots:

| Guide | Covers |
| --- | --- |
| [The machine library](docs/library.md) | searching and running shared machines, badges, saving offline, submitting, updates and remixes |
| [Algorithms](docs/algorithms.md) | all 35 constructions, two-machine operations, the lexer generator |
| [The grammar workbench](docs/grammar.md) | writing grammars, the 25 tools, CYK and derivations, conversions to and from the canvas |
| [StateMate](docs/statemate.md) | setting up a provider, the build-and-verify pipeline, write modes, agentic mode, commands, privacy |
| [The reference](docs/reference.md) | the machine pages, decidability and language classes |
| [Building blocks](docs/building-blocks.md) | sub-machines, nesting and reuse, worked through on a small CPU |
| [The command line](docs/cli.md) | `automata` by task, with the full [command reference](docs/cli-reference.md) |

## Features

### Machines
Expand Down Expand Up @@ -159,6 +176,8 @@ derivations, ambiguity witnesses, LL(1) tables, and conversion to and from the c
*Check ambiguity* then finds two different parse trees for `ababab`, which proves the
grammar is ambiguous.</sup>

More in [the grammar workbench guide](docs/grammar.md).

### Import, export and sharing
- **Import:** JFLAP `.jff` (including 6.1 blocks), XState, SCXML, and machine codes.
- **Diagrams:** PNG and SVG, with text converted to outlines. A PNG can embed the
Expand Down Expand Up @@ -187,27 +206,46 @@ it, and `([])` is accepted. Recorded through the repository's agent bridge
([tools/agent-bridge](tools/agent-bridge/statemate-bridge.mjs)), so the answer goes
through the same parse, lint and verify steps as one from any provider.</sup>

More in [the StateMate guide](docs/statemate.md).

### The machine library
A public catalogue of machines you can search (by name, type, size, or by a word they
accept), run in place, open on your canvas, save for offline use, remix, and add to.
Every badge on a listing (tests pass, deterministic, minimal, halts, never halts) comes
from the library's CI running the machine, not from its author.

![Searching the library, trying a word on an entry and opening it on the canvas](docs/media/library.webp)

More in [the library guide](docs/library.md).

## Algorithms and theory

The app has 34 interactive constructions from the standard textbooks (Hopcroft &
Ullman, Sipser), and each one can be stepped through:
The app has 35 interactive constructions from the standard textbooks (Hopcroft &
Ullman, Sipser). Each one shows its working, and can put its result on the canvas:

- **Conversions:** subset construction, ε-NFA → NFA, regex ↔ NFA, DFA ↔ regular
grammar, TM → grammar, Moore ↔ Mealy
- **Analysis:** minimisation (table-filling and visual), equivalence with a
distinguishing word, ε-closure, dead states, computation trees
- **Closure:** union, intersection, concatenation, star, complement, reversal, product
- **Decision procedures:** emptiness, finiteness, universality
- **A universal Turing machine** visualiser
- **A universal Turing machine** visualiser, and a **lexer generator** that compiles
token rules into one minimal DFA and emits it as JavaScript, Python or C

![NFA to DFA subset construction](docs/media/algorithms.png)
![Regex to NFA to DFA to minimal DFA, each result loaded onto the canvas](docs/media/algorithms.webp)

<sup>`(a|b)*abb` through the whole pipeline: Thompson's construction gives a 14-state
ε-NFA, the subset construction a 5-state DFA, and minimisation the 4-state DFA from the
textbook. More in [the Algorithms guide](docs/algorithms.md).</sup>

A built-in **reference** has a page for every machine type, covering its formal
definition and what it can and cannot recognise. It also has sections on decidability
(Rice's theorem, reductions, diagonalisation) and on language classes.

![The reference page for a DFA](docs/media/reference.png)

More in [the reference guide](docs/reference.md).

## Command line

`automata` runs the same engine from a terminal. You can use it to run, test, trace and
Expand All @@ -222,7 +260,7 @@ automata grade exercise.automaton submissions/ --csv grades.csv
automata halts machines.txt --proof proofs/ # halting proofs, checkable with check-proof
```

![automata halts classifying nine Turing machines with seven different methods, then check-proof verifying the proofs](docs/media/cli.webp)
![automata halts classifying nine Turing machines, one per proof method, then check-proof verifying the proofs](docs/media/cli.webp)

<sup>`automata halts` on nine machines: the BB(2), BB(2,4) and BB(5) champions halt
(BB(5) after 47,176,870 steps), five machines are proved never to halt by five different
Expand Down
179 changes: 179 additions & 0 deletions docs/algorithms.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,179 @@
# Algorithms

The Algorithms view holds the textbook constructions of automata theory as
interactive pages. Each one works on the machine on your canvas, shows its working
step by step, and can put its result back on the canvas as an ordinary machine you can
edit, run or export.

Open it with the **Algorithms** tab of the aux window, or <kbd>3</kbd> on the canvas.
The chip at the top right names the machine it is reading. The search box at the top of
the list filters it.

![Regex to NFA to DFA to minimal DFA, each result loaded onto the canvas](media/algorithms.webp)

<sup>`(a|b)*abb` through the whole pipeline. Thompson's construction gives a 14-state
ε-NFA, the subset construction a 5-state DFA, and table-filling minimisation the 4-state
DFA from the textbook. Each result is loaded onto the canvas before the next step reads
it.</sup>

- [How a page works](#how-a-page-works)
- [The catalogue](#the-catalogue)
- [Two-machine operations](#two-machine-operations)
- [The lexer generator](#the-lexer-generator)
- [Grammars](#grammars)

---

## How a page works

Most pages compute from the machine on the canvas as soon as you open them. Some take an
input first: a regular expression, a word to trace, or a second machine.

- **Load Result into Canvas** replaces the canvas with the constructed machine. One
<kbd>Ctrl</kbd>+<kbd>Z</kbd> brings back what was there.
- **Construction steps** list what the algorithm did, in order, with the reason for each
step. The subset construction, for example, records each `δ(S, a)` it computed, and
which ones found a new DFA state.
- **Visual** pages (*DFA Minimize (Visual)*, *Regex → NFA (Visual)*) step through the
construction with **Back** and **Next**.

A page that does not apply to the machine on the canvas says so and why, for example
"Your automaton is already a DFA" on the subset construction.

![An NFA's computation tree for the word cab](media/algorithms-tree.webp)

## The catalogue

**Finite automata**

| Page | What it does |
| --- | --- |
| δ Transition Table | δ as a table: one row per state, one column per symbol |
| NFA → DFA (Subset) | the subset (powerset) construction, from ε-closure(q₀) |
| DFA Minimize | table-filling (Myhill–Nerode): distinguishable pairs, equivalence classes, the minimal DFA |
| DFA Minimize (Visual) | the same, stepped one marking round at a time |
| DFA Equivalence | whether two DFAs accept the same language |
| NFA Computation Tree | every branch an NFA takes on a word, level by level |
| ε-Closure Table | the ε-closure of every state of an ε-NFA |
| Dead State Analysis | which states are reachable, which can still reach acceptance, and which are dead |

**Pushdown automata and nondeterministic TMs**

| Page | What it does |
| --- | --- |
| NPDA Simulation | breadth-first search over an NPDA's branches, each with its stack |
| NDTM Simulation | breadth-first search over a nondeterministic TM's branches |

**Regular grammars**

| Page | What it does |
| --- | --- |
| DFA/NFA → Regular Grammar | a right-linear grammar: states become variables, transitions become rules |
| Regular Grammar → NFA | right- or left-linear grammar to an automaton |

**Turing machines**

| Page | What it does |
| --- | --- |
| UTM Simulator | a universal Turing machine: describe a TM in JSON and run it on a word |
| TM → Grammar | an unrestricted (type 0) grammar that generates the TM's language |
| MTM Transition Table | a multi-tape TM's δ: Q × Γᵏ → Q × Γᵏ × {L,R}ᵏ, one row per transition |

**Transducers**

| Page | What it does |
| --- | --- |
| Moore Table, Mealy Table | the transition table with outputs, λ: Q → Δ or λ: Q × Σ → Δ |
| Moore → Mealy | moves each output from a state onto the transitions entering it |
| Mealy → Moore | splits each state once per output that enters it |

**Regular expressions**

| Page | What it does |
| --- | --- |
| Regex → NFA (Thompson) | Thompson's construction: one NFA fragment per operator, joined by ε-moves |
| Regex → NFA (Visual) | the same, assembled one fragment per step |
| NFA → Regex (GNFA) | state elimination on a generalised NFA |

The regex syntax is `|` (union), concatenation, `*`, `+`, `?`, `()`, `[abc]`, `[a-z]`,
`{n,m}` and `ε`.

**Transformations**

| Page | What it does |
| --- | --- |
| ε-NFA → NFA | removes ε-moves by adding the transitions they stood for |
| DFA Complement | completes the DFA with a trap state, then swaps accepting and non-accepting |
| Product Construction | pairs of states simulating two DFAs at once, for ∩ and ∪ |

**Decision properties**

| Page | What it does |
| --- | --- |
| Is Empty? | whether any accepting state is reachable |
| Is Finite? | whether there is a cycle among useful states |
| Is Universal? (DFA) | whether L(M) = Σ\*, by checking the complement is empty |
| Full Equivalence | L(M₁) = L(M₂), by checking the symmetric difference is empty |

**Closure operations**

| Page | What it does |
| --- | --- |
| Kleene Star (NFA) | L\* |
| Reversal (NFA) | Lᴿ |
| Union with M₂ | L(M₁) ∪ L(M₂) |
| Intersection with M₂ | L(M₁) ∩ L(M₂), by the product construction |
| Concat with M₂ | L(M₁) · L(M₂) |

**Engineering**

| Page | What it does |
| --- | --- |
| Lexer Generator | token rules → one minimal DFA → a working tokenizer, with generated code |

## Two-machine operations

Equivalence, union, intersection and concatenation need a second machine, M₂. To set
one:

1. Draw (or open) the machine you want as M₂.
2. On the page, press **Save Current as M₂**.
3. Open or draw M₁ on the canvas, and run the page.

**Restore M₂ to Canvas** brings the saved M₂ back.

## The lexer generator

The **Lexer Generator** takes the constructions above to their practical end. Each rule
is a token name and a pattern:

```text
NUMBER \d+(\.\d+)?
IDENT [A-Za-z_]\w*
STRING "([^"\\]|\\.)*"
skip WS \s+
```

The patterns are compiled together, by Thompson's construction and the subset
construction, into one DFA whose accepting states name a token, and then minimised.
The tokenizer takes the longest match, and when two rules match the same text, the one
listed first wins. A rule prefixed with `skip` is matched and dropped.

- **Try it** tokenises text as you type.
- The two most common lexer bugs are caught as you write the rules. A rule that matches
the empty string is refused, since it would produce empty tokens forever. A rule that
can never win, because an earlier one always matches first, is named in a warning
along with the rules that shadow it (an `IDENT` listed above the keywords, say).
- Anchors, lazy quantifiers, backreferences and lookaround are refused, each with the
reason it has no meaning in a lexer.
- **Generated code** is the same tokenizer in JavaScript, Python or C. It is the same
program the page runs, and the tests check that all three produce the same tokens.
- **Load DFA onto canvas** opens the DFA in a new tab, so the machine you were working
on is left alone.

![The lexer generator](media/algorithms-lexer.webp)

## Grammars

Constructions on context-free grammars (CNF, GNF, CYK, LL(1), grammar ↔ PDA) live in
the [grammar workbench](grammar.md).
Loading
Loading