diff --git a/README.md b/README.md index 558f997..c2b1006 100644 --- a/README.md +++ b/README.md @@ -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) @@ -32,6 +33,7 @@ accumulator after 331 steps. ## Contents - [Getting started](#getting-started) +- [Guides](#guides) - [Features](#features) - [Algorithms and theory](#algorithms-and-theory) - [Command line](#command-line) @@ -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. +## 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 @@ -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. +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 @@ -187,10 +206,22 @@ 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. +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 @@ -198,9 +229,14 @@ Ullman, Sipser), and each one can be stepped through: 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) + +`(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). 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 @@ -208,6 +244,8 @@ definition and what it can and cannot recognise. It also has sections on decidab ![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 @@ -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) `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 diff --git a/docs/algorithms.md b/docs/algorithms.md new file mode 100644 index 0000000..12ba0ba --- /dev/null +++ b/docs/algorithms.md @@ -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 3 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) + +`(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. + +- [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 + Ctrl+Z 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). diff --git a/docs/cli.md b/docs/cli.md index 9c66cd3..015459f 100644 --- a/docs/cli.md +++ b/docs/cli.md @@ -4,205 +4,24 @@ This guide walks through it by task. Every option of every command is in the [command reference](cli-reference.md), and `automata --help` prints the same thing in the terminal. -- [Install](#install) -- [Five minutes with it](#five-minutes-with-it) -- [Machines and words](#machines-and-words) -- [Running machines](#running-machines) -- [Looking at a machine](#looking-at-a-machine) -- [Comparing machines](#comparing-machines) -- [Building machines: pipes and expressions](#building-machines-pipes-and-expressions) -- [Formats: getting machines in and out](#formats-getting-machines-in-and-out) -- [Pictures and animations](#pictures-and-animations) -- [Teaching: exercises and grading](#teaching-exercises-and-grading) -- [Turing machines: does it halt?](#turing-machines-does-it-halt) -- [Learning a machine](#learning-a-machine) -- [Scripts, CI and git](#scripts-ci-and-git) -- [AI agents (MCP)](#ai-agents-mcp) -- [Exit codes](#exit-codes) -- [Colour and the terminal](#colour-and-the-terminal) -- [Troubleshooting](#troubleshooting) +![automata play animating a binary-addition Turing machine, with its space-time history](media/cli-play.webp) ---- - -## Install +`automata play` on the binary-addition Turing machine from `js/examples/tm.json`, adding 5 and 3. The states line lights the current state, the tape is drawn in colour with the head marked, and `--history` grows the space-time diagram a row per step. It accepts after 43 steps with `1000` (8) on the tape. -**With the desktop app.** The CLI ships inside it and runs on the app's own executable, so nothing else is needed. The installers put `automata` on your `PATH`: - -| Platform | How `automata` gets on your `PATH` | +| If you want to… | Read | | --- | --- | -| Windows | The installer adds `%LOCALAPPDATA%\Programs\AutomataStudio\resources\cli` to your user `PATH`, and the uninstaller removes it. Open a new terminal after installing. | -| macOS | In the app, choose **AutomataStudio → Install 'automata' Command in PATH**. It links `/usr/local/bin/automata`, asking for your password if that folder needs it. Move the app to Applications first. | -| Linux (.deb) | The package links `/usr/local/bin/automata`, and removing it takes the link away. An `automata` already there (from npm, say) is left alone. | -| Linux (AppImage) | Nothing to install: run `./AutomataStudio-*.AppImage --cli `. | -| Linux (AppImage) | run `./AutomataStudio-*.AppImage --cli …` | - -On macOS and Linux, `AutomataStudio --cli …` works without the launcher too. - -**From a checkout of the repository** (Node 20 or newer): - -```sh -npm install -npm link # puts `automata` on your PATH, running the source -automata --version -``` - -**As a single bundle**, for a machine with Node but without the repository: - -```sh -npm run cli:build # writes dist-cli/ -node dist-cli/automata.mjs --help -``` - -`dist-cli/` is self-contained; copy the folder anywhere. - ---- - -## Five minutes with it - -```sh -# What is this machine? -automata info js/examples/dfa.json - -# Does it accept these words? (exit code 0 = all accepted, 1 = some rejected) -automata run js/examples/dfa.json 0 101 11 "" - -# Watch it run, one step at a time (space to pause, arrows to step, q to quit) -automata play js/examples/tm.json 0101+11 --history - -# Build a machine from a regular expression, minimize it, draw it -automata from-regex "(a|b)*abb" | automata minimize - | automata svg - -o abb.svg - -# Does this Turing machine halt? -automata halts 1RB1LC_1RC1RB_1RD0LE_1LA1LD_1RZ0LA -``` - -The last one is the five-state busy beaver: it halts after 47,176,870 steps, which `halts` finds by running it, in a few seconds. - ---- - -## Machines and words - -### A machine can be a file, a pipe, or a line of text - -| You give | What it is | -| --- | --- | -| `machine.automaton`, `machine.json` | the app's own document — what Save writes | -| `machine.jff` | JFLAP (finite automata, PDAs, Turing machines, Mealy, Moore) | -| `chart.scxml`, `machine.js` | a statechart (SCXML, or an XState config), flattened into a machine | -| `nba.hoa` | Hanoi Omega-Automata, as Spot, Owl and other LTL tools write | -| `nba.ba`, `nfa.timbuk` | RABIT/GOAL Büchi automata; Timbuk word automata | -| `-` | standard input — so machines can be piped between commands | -| `1RB1LB_1LA1RZ` | a Turing machine in the standard (bbchallenge) notation | -| `fa.01:+AB_BA` | a *machine code*: any machine as one line (the app's **Copy Machine Code** writes these) | - -The standard Turing-machine notation lists one segment per state, `A`, `B`, `C`, …; within a segment, one triple per symbol read (0 first): the symbol written, `L` or `R`, and the next state. `Z` halts, and `---` is an undefined transition, which halts too. - -### Typing words - -- Single-character symbols run together: `0110`. -- Multi-character symbols are separated by spaces or commas: `"01 11 00"`. -- The empty word is `""`, `ε` or `eps`. -- An ω-automaton reads an infinite word written **u(v)**: a prefix `u`, then `v` forever. `"(ab)"` is ababab…, `"a(b)"` is abbbb…. - -A **words file** (for `test` and `learn`) has one word per line. `w => accept` or `w => reject` makes the line an expectation, and `#` starts a comment: - -```text -# multiples of five, in binary -0 => accept -101 => accept -11 => reject -``` - ---- - -## Running machines - -```sh -automata run machine.automaton 0110 101 "" # decide words -automata test machine.automaton words.txt # check expectations -automata trace machine.automaton 0110 # every step, in a table -automata play machine.automaton 0110 # every step, animated -``` - -**`run`** prints each word's verdict: `✔ accept`, `✘ reject`, or `? unknown` when the step budget ran out first. That third answer matters: a Turing machine still running after 100,000 steps has not been shown to reject, and `run` says so (exit code 2) instead of guessing. Raise the budget with `--max-steps`. A transducer (Mealy, Moore, FST, PDT) prints its output: `01 11 ● done → 10`. - -**`test`** reads a words file and reports each expectation as passed (`✓`), failed (`✗`) or undecided (`?`). With `--watch` it reruns whenever the machine or the file is saved — draw in the app, save, and see the results change in the terminal. - -**`trace`** prints the run the app's player would show: the state (or set of states, for a nondeterministic machine), what the step did, and the machine's memory — the tape with its head marked, the stack or stacks, the unread input, the output. `--limit` caps the steps. - -**`play`** animates the same run. In a terminal it takes over the screen: - -| Key | Does | -| --- | --- | -| `space` | play / pause | -| `←` `→` | step back / forward | -| `+` `−` | faster / slower | -| `Home` `End` | first / last step | -| `h` | show or hide the space-time history | -| `r` | replay from the start | -| `q` `Esc` | quit — the last frame stays on the screen | - -The screen shows every state with the current one lit, the tape in colour with its head marked by `▼` and its cells numbered, and, with `--history`, the space-time diagram growing a row per step. Each symbol keeps one colour throughout. - ---- - -## Looking at a machine - -```sh -automata info machine.automaton -automata lint machine.automaton -automata words machine.automaton --limit 20 -automata profile tm.automaton --to 12 -``` - -**`info`** answers "what is this?": the type, size and alphabets; the start and accepting states, or for other acceptance conditions (accepting by empty stack, parity, co-Büchi) what acceptance means; whether δ is deterministic. For a finite automaton it adds the language's class, whether it is empty, finite or universal, the minimal DFA's size (and whether this DFA already is minimal), and a regular expression. It ends with the machine's names: its standard notation, if it is a Turing machine, and its machine code. - -**`lint`** looks for mistakes: states the start cannot reach, states from which nothing can be accepted, symbols outside Σ, duplicate edges, a deterministic type whose δ branches, a weak automaton whose strongly connected components straddle F. Each finding names the rule that found it. It exits 1 on any error or warning — ready for CI. - -**`words`** lists the accepted words, shortest first. For a finite automaton it works from the DFA, so it is exact and fast, and it can also **count** the accepted words of each length (`--count`, exactly, at any length) and draw **uniformly random** accepted words of a given length (`--sample 5 --len 40`). For other machines it runs every word up to `--max-len`. - -**`profile`** measures how expensive a machine is: steps and space (cells visited on a tape, the tallest the stack got) for every input up to a length, worst and average, as CSV, with an estimate of the growth — linear, quadratic, exponential. `--family "0^n 1^n"` profiles one structured input per length instead of all of them. - ---- - -## Comparing machines - -```sh -automata equiv mine.automaton reference.automaton -automata diff old.automaton new.automaton -automata similar submissions/ -automata fuzz machine.automaton --oracle "python check.py {}" --mode stdout -``` - -**`equiv`** decides whether two machines accept the same language. For two finite automata it is exact and gives the shortest word they disagree on. For anything else it runs every word up to `--max-length` and says the check was bounded. Transducers are compared on their outputs. ω-automata are compared on every ultimately periodic word `u(v)` up to `--size` symbols. - -**`diff`** is for versions of one machine: what changed (states, accepting states and transitions, matched by name, so moving a state on the canvas is not a change), whether the two are the same machine up to renaming states, and whether the language changed — with the shortest word that shows it. - -**`similar`** groups a folder of machines that are the same: finite automata by language (whatever they look like), anything else by structure. It is built for a folder of submissions. - -**`fuzz`** tests a machine against a program that says what the language is meant to be: every word up to length 3, then random ones, until the two disagree — and then it shrinks the disagreement to a minimal word. The program gets the word as `{}` in the command (or appended), on stdin, and in `$AUTOMATA_WORD`. `{}` becomes a quoted reference to that variable rather than the word pasted in, so a word holding `# The `automata` command line - -`automata` is AutomataStudio's engine in a terminal: the same simulators, the same grader, the same exporters and the same Turing-machine analysis as the app, driven by commands instead of clicks. Use it to check machines in CI, grade a class at once, convert between tools, script experiments, or just watch a Turing machine run. - -This guide walks through it by task. Every option of every command is in the [command reference](cli-reference.md), and `automata --help` prints the same thing in the terminal. - -- [Install](#install) -- [Five minutes with it](#five-minutes-with-it) -- [Machines and words](#machines-and-words) -- [Running machines](#running-machines) -- [Looking at a machine](#looking-at-a-machine) -- [Comparing machines](#comparing-machines) -- [Building machines: pipes and expressions](#building-machines-pipes-and-expressions) -- [Formats: getting machines in and out](#formats-getting-machines-in-and-out) -- [Pictures and animations](#pictures-and-animations) -- [Teaching: exercises and grading](#teaching-exercises-and-grading) -- [Turing machines: does it halt?](#turing-machines-does-it-halt) -- [Learning a machine](#learning-a-machine) -- [Scripts, CI and git](#scripts-ci-and-git) -- [AI agents (MCP)](#ai-agents-mcp) -- [Exit codes](#exit-codes) -- [Colour and the terminal](#colour-and-the-terminal) -- [Troubleshooting](#troubleshooting) +| get it running | [Install](#install), then [Five minutes with it](#five-minutes-with-it) | +| run, test, trace or watch a machine | [Machines and words](#machines-and-words), [Running machines](#running-machines) | +| inspect, lint or profile one | [Looking at a machine](#looking-at-a-machine) | +| compare two machines, or a machine against a script | [Comparing machines](#comparing-machines) | +| build machines from regexes and operations | [Building machines: pipes and expressions](#building-machines-pipes-and-expressions) | +| convert to and from JFLAP, HOA, BA, Timbuk, SCXML, code | [Formats](#formats-getting-machines-in-and-out) | +| make diagrams and animations | [Pictures and animations](#pictures-and-animations) | +| set and grade exercises, or use Gradescope | [Teaching: exercises and grading](#teaching-exercises-and-grading) | +| prove whether Turing machines halt | [Turing machines: does it halt?](#turing-machines-does-it-halt) | +| learn a DFA from examples | [Learning a machine](#learning-a-machine) | +| use it in scripts, CI, git or an AI agent | [Scripts, CI and git](#scripts-ci-and-git), [AI agents (MCP)](#ai-agents-mcp), [Exit codes](#exit-codes) | +| fix a problem | [Colour and the terminal](#colour-and-the-terminal), [Troubleshooting](#troubleshooting) | --- @@ -215,8 +34,7 @@ This guide walks through it by task. Every option of every command is in the [co | Windows | The installer adds `%LOCALAPPDATA%\Programs\AutomataStudio\resources\cli` to your user `PATH`, and the uninstaller removes it. Open a new terminal after installing. | | macOS | In the app, choose **AutomataStudio → Install 'automata' Command in PATH**. It links `/usr/local/bin/automata`, asking for your password if that folder needs it. Move the app to Applications first. | | Linux (.deb) | The package links `/usr/local/bin/automata`, and removing it takes the link away. An `automata` already there (from npm, say) is left alone. | -| Linux (AppImage) | Nothing to install: run `./AutomataStudio-*.AppImage --cli `. | -| Linux (AppImage) | run `./AutomataStudio-*.AppImage --cli …` | +| Linux (AppImage) | Nothing to install: run `./AutomataStudio-*.AppImage --cli …`. | On macOS and Linux, `AutomataStudio --cli …` works without the launcher too. @@ -362,7 +180,7 @@ automata fuzz machine.automaton --oracle "python check.py {}" --mode stdout **`similar`** groups a folder of machines that are the same: finite automata by language (whatever they look like), anything else by structure. It is built for a folder of submissions. -**`fuzz`** tests a machine against a program that says what the language is meant to be: every word up to length 3, then random ones, until the two disagree — and then it shrinks the disagreement to a minimal word. , `&` or a backquote reaches the program as itself and is never run by the shell; every `{}` is replaced, so a script with braces of its own should read the variable instead. Under Windows' `cmd.exe`, a word containing `"` cannot be passed as an argument at all, and the CLI says so rather than guessing — read it from stdin. The program answers with its exit code (`--mode exit`), a yes/no line (`--mode stdout`), or, for transducers, the expected output (`--mode output`). With `--batch`, one process answers every word, a line each — much faster. +**`fuzz`** tests a machine against a program that says what the language is meant to be: every word up to length 3, then random ones, until the two disagree — and then it shrinks the disagreement to a minimal word. The program gets the word as `{}` in the command (or appended), on stdin, and in `$AUTOMATA_WORD`. `{}` becomes a quoted reference to that variable rather than the word pasted in, so a word holding `$`, `\`, `&` or a backquote reaches the program as itself and is never run by the shell; every `{}` is replaced, so a script with braces of its own should read the variable instead. Under Windows' `cmd.exe`, a word containing `"` cannot be passed as an argument at all, and the CLI says so rather than guessing — read it from stdin. The program answers with its exit code (`--mode exit`), a yes/no line (`--mode stdout`), or, for transducers, the expected output (`--mode output`). With `--batch`, one process answers every word, a line each — much faster. ```sh # check.py: import sys; print(int(sys.argv[1] or "0", 2) % 5 == 0) @@ -487,6 +305,10 @@ automata bb-search -n 3 automata sheet machines.txt -o sheet.svg ``` +![automata halts classifying nine Turing machines, then check-proof verifying the proofs](media/cli.webp) + +Nine machines, one for each method. The BB(2), BB(2,4) and BB(5) champions halt, five machines are proved never to halt by five different methods, and the last, Antihydra, is reported as unknown, since whether it halts is an open problem. `check-proof` then re-checks every proof file. + **`halts`** takes one machine, a file, or a text file with one machine per line, and tries, cheapest first: | Method | Proves | How | diff --git a/docs/grammar.md b/docs/grammar.md new file mode 100644 index 0000000..a13272b --- /dev/null +++ b/docs/grammar.md @@ -0,0 +1,131 @@ +# The grammar workbench + +The Grammar view is where you write a grammar once and then take it apart with 25 +tools: inspect it, normalise it, parse words with it, decide things about its +language, and convert it to and from machines on the canvas. + +Open it with the **Grammar** tab of the aux window, or 4 on the canvas. + +![Typing a grammar, filling a CYK table step by step, and finding an ambiguity witness](media/grammar.webp) + +The grammar is checked as you type it. CYK fills its table one span at a time on +`aabb`, then *Check ambiguity* finds two different parse trees for `ababab`, which proves +the grammar ambiguous. + +- [Writing a grammar](#writing-a-grammar) +- [The tools](#the-tools) +- [Parsing: CYK and derivations](#parsing-cyk-and-derivations) +- [Transforms show their working](#transforms-show-their-working) +- [Converting to and from the canvas](#converting-to-and-from-the-canvas) + +--- + +## Writing a grammar + +The grammar sits in a card at the top of the view, and every tool reads it. Write one +rule per line, with alternatives separated by `|`: + +```text +E -> E + T | T +T -> T * F | F +F -> ( E ) | id +``` + +- `->`, `→`, `=>` and `::=` all work as the arrow. The empty word is `ε`, `λ` or `eps`. + A bare `|` with nothing beside it is an error, so the empty word is never written by + accident. +- **Variables** are the symbols on left-hand sides. **Start** chooses the start symbol + from them, and defaults to the first rule's. +- **Whitespace separates symbols.** `a S b` is three symbols. A run of letters with no + variable in it, like `id`, is one terminal. Write `i d` if you mean two. +- `` and `[q0,A,q1]` are always single symbols, which is how the grammars that + *Canvas PDA → grammar* produces read back. +- **Source** shows what you typed. **Rules** shows what the parser read, symbol by + symbol, with variables and terminals coloured. If the two differ, the line above the + footer explains why. +- The footer counts V, Σ and R. **Library** loads one of the example grammars, and + **Format** rewrites the source in a canonical layout. + +The grammar is saved with the workspace and is on the undo stack. A run of keystrokes +is one undo step. + +![The overview of an expression grammar](media/grammar-overview.webp) + +## The tools + +| Group | Tools | +| --- | --- | +| **Inspect** | Overview · Chomsky class · Symbols · FIRST & FOLLOW | +| **Normalize** | Remove ε-rules · Remove unit rules · Remove useless symbols · Chomsky normal form · Greibach normal form · Remove left recursion · Left factoring | +| **Parse** | Parse a word · CYK table · Check ambiguity · LL(1) analysis · Test many words · Generate words | +| **Decide** | Is L(G) empty? · Is L(G) finite? | +| **Convert** | Grammar → NPDA (top-down) · Grammar → NPDA (bottom-up) · Canvas PDA → grammar · Grammar → automaton · Canvas automaton → grammar | +| **Library** | Example grammars | + +- **Overview** shows the tuple, the rules, and a row of facts at a glance: the + grammar's Chomsky type, ε-rules, unit rules, useless symbols, left recursion, whether + it is already in CNF or GNF, and whether its language is finite. +- **Chomsky class** tests the grammar against each type in turn, including the + non-contracting condition that separates type 1 from type 0. +- **FIRST & FOLLOW** gives both sets for every variable, which the LL(1) table is built + from. +- **LL(1) analysis** builds the predictive parsing table and lists each conflicted cell + with the rules that compete for it, and the usual fixes. Type a word and it traces the + predictive parse: the stack, the remaining input and the action at each step. +- **Test many words** decides a list of words at once. **Generate words** lists the + shortest words in the language. +- **Is L(G) finite?** answers with the cycle that makes it infinite (through symbols + that are both reachable and generating), or, when it is finite, lists every word. + +![The LL(1) table for the expression grammar, with its conflicts](media/grammar-ll1.webp) + +## Parsing: CYK and derivations + +There are two engines, and each has its own job. + +- **CYK** decides membership. It always answers, in cubic time, and works on Chomsky + normal form. The table you scrub through is the table of the *converted* grammar, and + the conversion is shown below it. +- **Parse trees, leftmost and rightmost derivations, and ambiguity witnesses** come from + a search over the rules **you wrote**, so they are about your grammar and not its CNF. + The search only runs on a word CYK has already accepted. + +**Check ambiguity** looks for two structurally different parse trees of a word. Finding +two proves the grammar ambiguous. Finding one is evidence, not proof: another word may +still be ambiguous, and whether a grammar is ambiguous at all is undecidable. The tool +says which of the two you are looking at. + +## Transforms show their working + +Every normalisation is a worked construction. It shows one stage per textbook step, +each with the grammar that step left behind, and a note of any precondition it had to +establish first: + +- **Greibach normal form** first converts to CNF, and says so. +- **Remove left recursion** removes ε-rules first, and handles indirect recursion + (`A → B a`, `B → A b`) by ordering the variables and substituting earlier ones out. + A variable whose every alternative is left-recursive is left alone, with the reason. +- **Left factoring** pulls out common prefixes until no two alternatives of a variable + share one. + +The tests check every transform by comparing the language before and after, word by +word up to a length, across several grammars. + +![Removing left recursion from the expression grammar](media/grammar-left-recursion.webp) + +## Converting to and from the canvas + +| Tool | Does | +| --- | --- | +| Grammar → NPDA (top-down) | the standard construction: expand variables on the stack, match terminals | +| Grammar → NPDA (bottom-up) | shift–reduce: push terminals, reduce right-hand sides | +| Canvas PDA → grammar | the triple construction, with variables `[p,A,q]` | +| Grammar → automaton | a right- or left-linear grammar to a finite automaton | +| Canvas automaton → grammar | a finite automaton to a right-linear grammar | + +A conversion to a machine shows the construction and offers **Load onto the canvas**. +A conversion from the canvas shows the grammar and offers **Apply to the editor**, which +puts it in the grammar card for every other tool to work on, or **Copy**. + +For the finite-automaton constructions themselves (subset construction, minimisation, +regular expressions), see [Algorithms](algorithms.md). diff --git a/docs/library.md b/docs/library.md new file mode 100644 index 0000000..43db9b3 --- /dev/null +++ b/docs/library.md @@ -0,0 +1,168 @@ +# The machine library + +The library is a public, searchable catalogue of machines you can run without opening +them, learn from, open on your canvas, remix, and add to. Every badge on a listing +comes from running the machine, not from what its author claimed. + +Open it with the **Library** tab of the aux window, from the header, or with +2 on the canvas. It is also published as a website at +[thethinkmachine.github.io/automata-library](https://thethinkmachine.github.io/automata-library/). + +![Searching the library, opening an entry, trying a word on it and opening it on the canvas](media/library.webp) + +Search for *divisibility*, open *Binary divisibility by 3*, run `1100` on it without +leaving the page (the path lights up, then *Accepted*), and *Open in a new tab* puts it +on the canvas with its test words as chips. + +- [What is in it](#what-is-in-it) +- [Finding a machine](#finding-a-machine) +- [An entry page](#an-entry-page) +- [Badges](#badges) +- [My Library and offline use](#my-library-and-offline-use) +- [Links to a machine](#links-to-a-machine) +- [Submitting a machine](#submitting-a-machine) +- [Updates and remixes](#updates-and-remixes) +- [Running your own copy](#running-your-own-copy) + +--- + +## What is in it + +Machines of every family the app can build (finite automata, ω-automata, pushdown and +other memory automata, Turing machines and transducers), grouped into **collections** +the way a course or a question would group them: *Regular languages, start to finish*, +*Beyond regular*, *The ω-automata zoo*, *Machines that write*, the *Busy Beaver Hall of +Fame*, and *Three ways to never halt*. + +Some entries and collections carry an **essay**: a write-up beside the machine, with +figures drawn from the machine itself. + +![The library's Discover page](media/library-discover.webp) + +## Finding a machine + +**Browse & search** lists everything, with filters down the side by family, by what +the library verified, by machine type and by tag. The search box takes plain words and +`key:value` filters, which combine: + +| Filter | Finds | +| --- | --- | +| `type:DFA` | one machine type (`NPDA`, `TM`, `NBA`, …) | +| `family:tm` | a whole family: `fa` (finite), `omega`, `mem` (memory automata), `tm`, `special` (transducers) | +| `badge:minimal` | entries with a badge: `tested`, `deterministic`, `minimal`, `halts`, `never-halts` | +| `states:<10`, `states:>=3` | by size | +| `accepts:0110`, `rejects:ab` | finite automata that accept (or reject) a word; the word is run on every candidate | +| `by:login` | one author | +| `tag:parity` | one tag | +| `level:intro` | `intro`, `intermediate` or `advanced` | + +`accepts:` and `rejects:` answer by running machines, so you can search by behaviour: +`type:DFA accepts:0110 rejects:011` finds the DFAs that tell those two words apart. + +**Pasting a machine code** (the one-line form from **Copy Machine Code**, or a Turing +machine in standard notation like `1RB1LB_1LA1RZ`) finds that exact machine, whatever +its states are named. + +**Match my canvas** searches with the machine you have open. It finds the same machine +(any type), and for a finite automaton any entry that recognises the same language, +however it is drawn. The result says which of the two it found. + +![Browsing Turing machines that halt](media/library-browse.webp) + +## An entry page + +An entry shows the machine's diagram, the language it accepts (as a strip of accepted +and rejected words), its formal definition, its badges, the author's test words, its +licence and its **machine code**. You do not need to open it to try it: + +- **Try it** runs a word on the machine in place and replays the run on the diagram. +- **The author's examples** are the test words from the machine's card. Click one to run it. +- **Open in a new tab** puts the machine on the canvas in a tab of its own, so whatever + you were working on stays where it was. +- **Save** keeps a copy in My Library. +- **More** downloads the `.automaton` file or copies a link to the entry. + +![An entry page](media/library-entry.webp) + +## Badges + +A badge is something the library's CI found by running the machine with this app's own +engine. Nothing on a listing is taken from the author except their words. + +| Badge | Means | +| --- | --- | +| **Tests pass** | Every accept, reject and output example the author declared was checked by running the machine. A failing example blocks the entry from being published. | +| **Deterministic** | No state has two transitions that could fire on the same input, by the editor's own rule. An NFA earns it only when it never actually branches. | +| **Minimal** | No DFA for this language has fewer states. | +| **Halts** | Run from a blank tape, the machine stops. The step count is exact. | +| **Never halts** | Proven never to halt from a blank tape, by the method named (see [halting proofs](cli.md#turing-machines-does-it-halt)). | + +The library lists each machine only once. Two submissions that are the same machine up +to state names, layout and symbol order count as one, and the later one is refused. +Two *different* machines that recognise the same language are both welcome. + +![What the library checks](media/library-badges.webp) + +## My Library and offline use + +**Save** on an entry keeps a copy in your browser. **My Library** lists those copies, +they open without a network, and when a newer version of one is published, My Library +says so. + +A machine opened from the library remembers where it came from, even after you edit it +and save it to a file. That is how its card can say "update available", and how +submitting it later knows whether it is an update or a remix. + +## Links to a machine + +| Link | Does | +| --- | --- | +| `…/AutomataStudio/#lib=` | opens the entry's machine on the canvas | +| `…/AutomataStudio/#library=` | shows the entry's page | +| `…/AutomataStudio/#collection=` | shows a collection | +| `…/AutomataStudio/#library` | opens the library | +| `automata-studio://…` | the same, in the desktop app | + +**More → Copy link** on an entry copies the second kind, and **Copy link** on a collection the third. + +## Submitting a machine + +**Submit a machine** sends the machine on your canvas to the library. There is no +server and nothing to sign in to inside the app. The form opens a GitHub issue, already +filled in, on the library's repository. You need a GitHub account, and you are credited +by it. + +1. Build the machine, give it a title and a description on its info card, and add test + words with their expected verdicts. Those become the **Tests pass** badge. +2. Open **Submit a machine**. It runs the same checks CI will run and shows the badges + the machine will earn, and anything that would stop it being published. +3. Choose a licence and tags, optionally write an essay, and press **Submit on GitHub**. +4. The library's CI turns the issue into a pull request and posts its report there. A + maintainer reviews and merges it, and the index and website rebuild. + +A machine already in the library is refused as a new entry. The form tells you to send +an update if it is yours, or a remix if it is someone else's. + +## Updates and remixes + +A machine you opened from the library and then changed is submitted as one of two +things, and your GitHub account decides which: + +- **An update**, if you are the entry's author. It replaces the entry in place, and + links to it keep working. +- **A remix**, if you are not. It becomes a new entry, credited to you, that links back + to the one it came from. + +## Running your own copy + +The library is an ordinary repository, so you can build and serve it locally, for +example to try a change before submitting it: + +```sh +npm run library:dev -- --library ../automata-library # serve a checkout locally +npm run library:build -- --library ../automata-library # build its index and website to _site/ +npm run library:init -- ../my-library # scaffold and seed a new one +``` + +`library:dev` prints a link that points the app at your local copy, and it emulates the +GitHub submission form too. **How it works → Source** in the Library view switches back. diff --git a/docs/media/algorithms-lexer.webp b/docs/media/algorithms-lexer.webp new file mode 100644 index 0000000..da34ba0 Binary files /dev/null and b/docs/media/algorithms-lexer.webp differ diff --git a/docs/media/algorithms-tree.webp b/docs/media/algorithms-tree.webp new file mode 100644 index 0000000..4ed74b4 Binary files /dev/null and b/docs/media/algorithms-tree.webp differ diff --git a/docs/media/algorithms.webp b/docs/media/algorithms.webp new file mode 100644 index 0000000..a56c895 Binary files /dev/null and b/docs/media/algorithms.webp differ diff --git a/docs/media/blocks.webp b/docs/media/blocks.webp index 6cb33f8..b67d821 100644 Binary files a/docs/media/blocks.webp and b/docs/media/blocks.webp differ diff --git a/docs/media/cli-play.webp b/docs/media/cli-play.webp new file mode 100644 index 0000000..60bba46 Binary files /dev/null and b/docs/media/cli-play.webp differ diff --git a/docs/media/cli.webp b/docs/media/cli.webp index 8a6e648..0fea43b 100644 Binary files a/docs/media/cli.webp and b/docs/media/cli.webp differ diff --git a/docs/media/grammar-left-recursion.webp b/docs/media/grammar-left-recursion.webp new file mode 100644 index 0000000..dd4bfc7 Binary files /dev/null and b/docs/media/grammar-left-recursion.webp differ diff --git a/docs/media/grammar-ll1.webp b/docs/media/grammar-ll1.webp new file mode 100644 index 0000000..7739227 Binary files /dev/null and b/docs/media/grammar-ll1.webp differ diff --git a/docs/media/grammar-overview.webp b/docs/media/grammar-overview.webp new file mode 100644 index 0000000..99f2cd2 Binary files /dev/null and b/docs/media/grammar-overview.webp differ diff --git a/docs/media/grammar.webp b/docs/media/grammar.webp index 2a86358..249fc57 100644 Binary files a/docs/media/grammar.webp and b/docs/media/grammar.webp differ diff --git a/docs/media/library-badges.webp b/docs/media/library-badges.webp new file mode 100644 index 0000000..97a93ea Binary files /dev/null and b/docs/media/library-badges.webp differ diff --git a/docs/media/library-browse.webp b/docs/media/library-browse.webp new file mode 100644 index 0000000..a803fa6 Binary files /dev/null and b/docs/media/library-browse.webp differ diff --git a/docs/media/library-discover.webp b/docs/media/library-discover.webp new file mode 100644 index 0000000..47dfb0f Binary files /dev/null and b/docs/media/library-discover.webp differ diff --git a/docs/media/library-entry.webp b/docs/media/library-entry.webp new file mode 100644 index 0000000..bb17944 Binary files /dev/null and b/docs/media/library-entry.webp differ diff --git a/docs/media/library.webp b/docs/media/library.webp new file mode 100644 index 0000000..67b2741 Binary files /dev/null and b/docs/media/library.webp differ diff --git a/docs/media/reference-decidability.webp b/docs/media/reference-decidability.webp new file mode 100644 index 0000000..a7d676f Binary files /dev/null and b/docs/media/reference-decidability.webp differ diff --git a/docs/media/reference-machine.webp b/docs/media/reference-machine.webp new file mode 100644 index 0000000..f01d055 Binary files /dev/null and b/docs/media/reference-machine.webp differ diff --git a/docs/media/reference.webp b/docs/media/reference.webp new file mode 100644 index 0000000..79996e5 Binary files /dev/null and b/docs/media/reference.webp differ diff --git a/docs/media/spacetime.webp b/docs/media/spacetime.webp index 0e4dccd..d4dfcef 100644 Binary files a/docs/media/spacetime.webp and b/docs/media/spacetime.webp differ diff --git a/docs/media/statemate-commands.webp b/docs/media/statemate-commands.webp new file mode 100644 index 0000000..c97e072 Binary files /dev/null and b/docs/media/statemate-commands.webp differ diff --git a/docs/media/statemate-settings.webp b/docs/media/statemate-settings.webp new file mode 100644 index 0000000..8a996d9 Binary files /dev/null and b/docs/media/statemate-settings.webp differ diff --git a/docs/media/statemate.webp b/docs/media/statemate.webp index 5bb24dc..26a5d25 100644 Binary files a/docs/media/statemate.webp and b/docs/media/statemate.webp differ diff --git a/docs/media/wizard.webp b/docs/media/wizard.webp index 65240bf..6b6caf0 100644 Binary files a/docs/media/wizard.webp and b/docs/media/wizard.webp differ diff --git a/docs/reference.md b/docs/reference.md new file mode 100644 index 0000000..23b9b31 --- /dev/null +++ b/docs/reference.md @@ -0,0 +1,67 @@ +# The reference + +The Reference view is a built-in textbook: one page for every machine the app can +build, plus sections on decidability and language classes. It is part of the app, so +it works offline, and it always matches what the editor does. + +Open it with the **Reference** tab of the aux window, or 5 on the canvas. +It opens on the page for the machine type on your canvas. + +![Reading the DFA and NBA pages, the decidability map and Rice's theorem](media/reference.webp) + +- [Machine pages](#machine-pages) +- [Decidability](#decidability) +- [Language classes](#language-classes) + +--- + +## Machine pages + +The rail lists the machines in the same groups as the model picker: finite automata, +ω-automata, memory automata, Turing machines and transducers. Each page covers, in +order: + +1. **What it is**, in plain words. +2. **Formal definition**: the tuple, and what each part is. +3. **How a run works**: configurations and the step relation. +4. **Acceptance**, including the ω-conditions (Büchi, co-Büchi, parity, weak) on the + ω-automata pages. +5. **What it can and cannot express**, with the languages that separate it from its + neighbours. +6. Topics particular to the model, such as minimality and the Myhill–Nerode theorem on + the DFA page, or why nondeterminism adds power to a pushdown automaton. +7. **In this editor**: how the app draws and runs it. + +The formal definition on each page is the same tuple the inspector prints for the +machine on your canvas, and a test checks that the two agree. A machine type added to +the app cannot go undocumented either: a test fails until it has a page. + +![The NPDA page](media/reference-machine.webp) + +## Decidability + +| Page | Covers | +| --- | --- | +| Decide vs Recognize | decidable and recognisable languages, and deciders versus recognisers | +| Deciding FA | membership, emptiness, finiteness, equivalence and universality for finite automata | +| Deciding CFLs | the same questions for context-free languages, and where they stop being decidable | +| TM Problems | the halting problem and its relatives | +| Diagonalization | why some languages are not even recognisable | +| Reductions | proving undecidability by reduction | +| Rice's Theorem | every non-trivial semantic property of a TM's language is undecidable | +| Decidability Map | every class against every standard question, in one table | + +The **Decidability Map** reads down a column: decidable, semi-decidable or +undecidable, for regular, ω-regular, deterministic context-free, context-free, +tree-adjoining, context-sensitive and recursively enumerable languages. A second table +does the same for questions about Turing machines. + +![The decidability map](media/reference-decidability.webp) + +## Language classes + +**Tree-Adjoining** explains tree-adjoining grammars, the grammar side of the embedded +pushdown automaton (EPDA). The app has no TAG editor, so this page is where the class is +explained. + +The EPDA's page links here, and links between pages stay inside the view. diff --git a/docs/statemate.md b/docs/statemate.md new file mode 100644 index 0000000..8b2d431 --- /dev/null +++ b/docs/statemate.md @@ -0,0 +1,152 @@ +# StateMate + +StateMate is the app's optional AI assistant. It builds and edits machines from a +sentence, answers questions about the machine on the canvas, and explains theory. It +never puts an unchecked machine in front of you: every machine it proposes is run on +the app's real simulator against its own test words first. + +It lives in the **StateMate** tab of the right panel. It is off until you turn it on and +choose a provider. + +![StateMate building a pushdown automaton for balanced brackets from a one-line prompt](media/statemate.webp) + +One prompt, *a pushdown automaton that accepts balanced strings of ( ) and [ ]*. The +proposal arrives as a diff with its test words already run (5/5 checks). **Apply** draws +it, and `([])` is accepted. + +- [Setting it up](#setting-it-up) +- [Asking for a machine](#asking-for-a-machine) +- [What happens to an answer](#what-happens-to-an-answer) +- [Chat, Build and Auto](#chat-build-and-auto) +- [Standard and Agentic](#standard-and-agentic) +- [Commands](#commands) +- [Privacy](#privacy) + +--- + +## Setting it up + +Open **Settings → StateMate** (or type `/model` in the console), turn on **Enable +StateMate**, and choose a provider: + +| Provider | Notes | +| --- | --- | +| Anthropic | the default | +| OpenAI | | +| Mistral AI | | +| Google AI Studio | | +| Cohere | | +| OpenRouter.ai | many models behind one key | +| Local Server (OpenAI-compatible) | llama.cpp, Ollama, LM Studio, vLLM and the like, at `http://localhost:8080/v1` by default. The server must allow the page's origin. | +| Claude Code (desktop app) | uses your own Claude Code sign-in. No key, and desktop only. | + +Paste your API key, pick a model (**Fetch models** lists what the key can use), and +press **Test connection**. + +In the browser, requests go straight from the page to the provider, which some +providers' CORS policies limit. The settings tab says when that applies. The desktop +app sends requests from its own process and is not affected. + +![StateMate's settings](media/statemate-settings.webp) + +## Asking for a machine + +Type what you want and press Enter: + +- *a DFA for binary numbers divisible by 3* +- *make it reject the empty word* +- *a Turing machine that doubles a unary number* +- *why does my machine reject `abba`?* +- *what is the difference between a DPDA and an NPDA?* + +The canvas's machine type is the default, but StateMate switches type when the request +needs it (a language no DFA can recognise, say) and tells you it did. With the canvas +attached, it edits the machine you have rather than starting over, and keeps the +positions and names of every state it did not need to change. Select part of the +diagram and use `/context` to point it at just that part. + +A request that could mean very different machines gets a question back. A small +ambiguity gets a machine, with the assumption stated. + +## What happens to an answer + +``` +your prompt → the model → parse → compile → lint → verify → apply + ↑ │ + └──── repair: "these tests failed" ─┘ +``` + +1. **Parse.** The answer is either a machine or a reply. A reply is shown as text and + never touches the canvas. +2. **Compile and lint.** The machine is built off-canvas and checked against the rules + of its type, for example that a DFA really is deterministic. +3. **Verify.** The model's own test words, each with the verdict it predicted, are run + on the real simulator. If any disagree, the model is sent the failing words with a + trace of where each run went wrong, and asked to repair the machine. +4. **Apply.** Only now is the canvas written, in one step that one + Ctrl+Z undoes. + +A failed run (a rejected key, an unreadable answer, a machine that fails its checks) +leaves your canvas exactly as it was. While the model is writing, the draft machine is +drawn dashed over the canvas, so you can see it take shape. + +## Chat, Build and Auto + +How much StateMate may change without asking is your choice, never the model's. +Shift+Tab in the console cycles through the modes, or use `/mode`. + +| Mode | Does | +| --- | --- | +| **Chat** | Read-only. StateMate answers and explains, and the canvas is never touched. | +| **Build** (default) | Builds and checks a machine, then shows you the diff (states, transitions and alphabet changes, line by line) with **Apply**, **Discard** and **Ask again**. | +| **Auto** | Draws straight onto the canvas once the machine passes its checks. An edit that would remove more than half your states is held as a proposal instead. | + +## Standard and Agentic + +The two buttons above the composer choose how StateMate works: + +- **Standard.** One model response builds the machine or answers. Fast and cheap. +- **Agentic.** StateMate works over several steps on a private copy of the machine, + using tools: it can inspect the canvas, add and change states and transitions, + simulate and trace words, lint, minimise a DFA, run the subset construction, search + the library, and ask you a question. It stops when it calls the result finished. It + is better for larger or fiddlier machines, and costs more requests. + +## Commands + +Type `/` in the console for the list. Enter on a command with arguments +completes it, and lists what it can take. + +| Command | Does | +| --- | --- | +| `/examples [search]` | browse the bundled example machines | +| `/library [search]` | search the [machine library](library.md) | +| `/algorithms [search]` | run an exact construction instead, with no model call | +| `/mode ask\|propose\|auto` | set the write mode (Chat, Build or Auto) | +| `/new ` | build from scratch, ignoring the canvas | +| `/canvas` | send the canvas with your prompt, or stop sending it | +| `/context [selection\|clear]` | say which part of the diagram the next prompt is about | +| `/undo` | undo the last change on the canvas | +| `/clear` | forget the conversation and start over | +| `/model` | StateMate's key, model and behaviour | +| `/settings [tab]` | the app's own settings | +| `/help` | everything you can type | + +When a request names a construction the app can do exactly, such as *minimise this +DFA*, a note above the composer offers the exact algorithm instead. + +![The command menu](media/statemate-commands.webp) + +## Privacy + +- **Your key stays in your browser** (or the desktop app's storage), under StateMate's + own storage key. It is never written into a saved file, a share link, a PNG with an + embedded workspace, an autosave or a workspace tab, and a test checks this. +- Requests go **directly** from your machine to the provider you chose. There is no + AutomataStudio server in between, and nothing is logged. +- What is sent is your prompt, the recent conversation, and, while `/canvas` is on, the + machine on the canvas. + +For testing prompts without a provider, the repository has an +[agent bridge](../tools/agent-bridge/statemate-bridge.mjs) that lets a Claude Code +session answer StateMate's requests by hand.