`automata` command reference

Every command, as automata <command> --help prints it. For a guided tour see cli.md.

Running: run · test · trace · play
Looking: info · lint · words · profile
Comparing: equiv · diff · similar · fuzz
Transforming: from-regex · to-regex · determinize · minimize · complement · reverse · star · union · concat · intersect · difference · eps-elim · eval
Formats: convert · export · codegen · svg · animate
Teaching: grade · generate
Turing machines: halts · check-proof · bb-search · tm-normalize · sheet
Learning: learn
Elsewhere: library · mcp
Topics: machines · words · exit-codes · formats · turing · proofs · omega · grading · learning · scripting · mcp · install · colour

Running

run

Decide words: accept, reject or unknown (and a transducer's output).

automata run <machine> [word ...]

Decide each word. With no words, reads one word per line from standard input.
The empty word is "" or ε. An ω-automaton reads u(v). A transducer prints its
output after the verdict.

  --json            one object per word
  --max-steps N     step budget per word (default 100000)

Exit: 0 all accepted, 1 some rejected, 2 some had no verdict within the budget,
3 a word could not be read.

Examples

# decide three words ("" is the empty word)
automata run machine.automaton 0110 "" 101
# a Turing machine in the standard notation, on a blank tape
automata run 1RB1LB_1LA1RZ ""
# an ω-automaton reads u(v): prefix, then the repeating part
automata run buchi.json "a(b)" "(ab)"
# one word per line from standard input
cat words.txt | automata run machine.automaton
# machine-readable: [{ word, verdict, output, error }]
automata run machine.automaton 0110 --json

See also: test, trace, play, help words.

test

Batch-test words from a file; "w => accept" lines are expectations. --watch reruns on save.

automata test <machine> <words-file | ->

One word per line; "w => accept" or "w => reject" (also acc/rej, a/r, ✓/✗) makes
the line an expectation. Blank lines and lines starting with # are skipped.

  --watch           rerun whenever the machine or the words file changes
  --failures        show only the lines that did not pass
  --json            summary and rows as JSON

Exit: 0 every expectation held, 1 one failed, 2 one had no verdict, 3 a line
could not be read.

Examples

# lines like "0110 => accept" are expectations
automata test machine.automaton words.txt
# rerun on every save of either file
automata test machine.automaton words.txt --watch
# show only what did not pass
automata test machine.automaton words.txt --failures
# make a test file from another machine
automata words reference.automaton --max-len 6 | sed "s/$/ => accept/" > words.txt

trace

Print a word's run step by step.

automata trace <machine> <word>

The run the player would show, one line per step: the state(s), what happened,
and the tape, stack, unread input or output where the machine has them.

  --limit N         at most N steps (default 200)
  --json            the steps as JSON

Examples

# every step: state, what happened, tape or stack
automata trace machine.automaton 0110
# the first 20 steps of a Turing machine
automata trace 1RB1LB_1LA1RZ "" --limit 20
# the steps as JSON, for a script
automata trace pda.automaton abba --json

play

Animate a run in the terminal.

automata play <machine> <word> [options]

Plays the run in the terminal, one step at a time: the states (the current
one lit), what the step did, and the machine's memory — a tape in colour with
its head marked and cells numbered, a stack with its top, the input with what
has been read dimmed, and the output. Each symbol keeps one colour throughout.

In a terminal it takes over the screen and takes keys:

  space        play / pause           ← →             step back / forward
  + −          faster / slower        home end        first / last step
  h            history on or off      r               replay from the start
  q  esc       quit (the last frame is left on screen)

Piped or redirected, it prints every frame in turn instead.

Options:
  --fps N           steps per second to start at (default 6)
  --limit N         at most N steps (default 500)
  --history         show the space-time diagram under the tape: one row per
                    step, time running down
  --paused          start paused on step 0

Examples:
  $ automata play 1RB1LB_1LA1RZ ""            the 2-state busy beaver
  $ automata play machine.automaton 0110 --history --fps 15
  $ automata play js/examples/npda.json abba   watch the stack fill and empty

Exit: 0 accept (or a transducer finished), 1 reject, 2 cut short or no verdict.

Looking

info

Type, tuple, size, determinism, language class, regex, minimal DFA size.

automata info <machine>

Type, language class, size, alphabets, start and accepting states, whether δ is
deterministic; for a finite automaton also the minimal DFA's size, whether the
language is empty, finite or universal, and a regular expression; for a Turing
machine its standard notation; and the machine code that names it.

  --latex           include the formal definition as LaTeX
  --no-regex        skip the regular expression (large automata)
  --json

Examples

# type, size, alphabets, determinism, language, regex, codes
automata info machine.automaton
# works on inline machines too
automata info 1RB1LB_1LA1RZ
# with the formal 5-tuple (or 7-tuple) as LaTeX
automata info machine.automaton --latex
# one fact, for a script
automata info machine.automaton --json | jq .minimalDfaStates

lint

Find unreachable and dead states, unused symbols, branching D-types, ….

automata lint <machine ...>

Findings are errors (the machine cannot be run as drawn), warnings (almost
always a mistake) and infos (worth knowing, often deliberate):

  no-start, dangling-edge, branches, guard          errors
  unreachable, dead, no-accepting, not-in-sigma,
  duplicate-edge, duplicate-name, no-priority       warnings
  unused-symbol, sinks, could-be-dfa, no-blank-move info

  --strict          infos count too
  --json

Exit: 0 nothing found, 1 an error or warning (or an info under --strict).

Examples

# errors, warnings and infos, with the rule that found each
automata lint machine.automaton
# every file; infos count as findings too
automata lint submissions/*.automaton --strict
# findings as JSON, for CI annotations
automata lint machine.automaton --json

words

List, count or uniformly sample the accepted words of a finite automaton.

automata words <machine>

The accepted words, shortest first. For a finite automaton this walks its DFA,
so it is exact and fast; anything else is run word by word up to --max-len.

  --max-len N       longest word (default 8)
  --limit N         at most N words (default 50)
  --rejected        list the rejected words instead
  --count           how many words of each length are accepted (finite
                    automata: exact, any length, by dynamic programming)
  --sample N        N accepted words of length --len, uniformly at random
  --len L           the length for --sample (default --max-len)
  --seed S          make --sample repeatable
  --json

Examples

# the shortest accepted words, in order
automata words machine.automaton
# the shortest rejected words
automata words machine.automaton --rejected --limit 20
# how many words of each length (exact, even at length 30)
automata words machine.automaton --count --max-len 30
# five accepted words of length 40, uniformly at random
automata words machine.automaton --sample 5 --len 40 --seed 1

profile

Steps and space per input length, with a growth estimate (CSV).

automata profile <machine>

Runs the machine on inputs of length --from … --to and measures each run:
steps, and space (cells visited on a tape, the tallest the store got on a
stack). Prints the Complexity section's CSV — worst and mean per length — and
a growth estimate for each. An estimate from a few lengths, not a proof.

  --from N --to N     lengths (default 1 … 12)
  --family PATTERN    one word per length from a pattern: a^n b^n, (ab)^{2n}, 1^n+1^n
  --cap N             words per length when sampling Σⁿ (default 64)
  --json

Examples

# steps and cells for every input up to length 10
automata profile tm.automaton --to 10
# one structured input per length
automata profile tm.automaton --family "0^n 1^n" --to 30
# the CSV to plot; the growth estimate goes to stderr
automata profile pda.automaton > cost.csv

Comparing

equiv

Do two machines accept the same language? Prints a counterexample if not.

automata equiv <machine-a> <machine-b>

Exact for two finite automata (a product search, with the shortest word they
disagree on). Otherwise every word of Σ* up to --max-length is run on both —
comparing outputs as well for transducers — and ω-automata are compared on
every ultimately periodic word u(v) up to --size symbols.

  --max-length N    bound for the finite-word check (default 8)
  --size N          bound for the lasso check (default 6)
  --json

Exit: 0 equal, 1 different, 2 no difference found but some word was undecided,
or the check was bounded (use --json to see which).

Examples

# the shortest word they disagree on, if any
automata equiv mine.automaton reference.automaton
# formats can differ
automata equiv a.jff b.automaton
# ω-automata: every u(v) up to 8 symbols
automata equiv nba.hoa dba.automaton --size 8

diff

Structural and language differences between two versions of a machine.

automata diff <old> <new>
       automata diff --textconv <machine>

What changed between two versions: the type, Σ, states, start, accepting states
and transitions (matched by state name, so moving a state on the canvas is not
a change), whether the two are the same machine up to renaming, and whether the
language changed — with the shortest word that tells them apart.

--textconv prints a stable listing with no coordinates, for git:

  git config diff.automaton.textconv "automata diff --textconv"
  echo "*.automaton diff=automaton" >> .gitattributes

and as a difftool:  git difftool -x "automata diff" -- machine.automaton

  --no-language     skip the language comparison
  --json

Exit: 0 no change to the language, 1 the language changed, 2 undecided.

Examples

# what changed, and whether the language did
automata diff old.automaton new.automaton
# as git's difftool
git difftool -x "automata diff" -- machine.automaton
# make plain git diff readable (with .gitattributes: *.automaton diff=automaton)
git config diff.automaton.textconv "automata diff --textconv"

similar

Group machines that recognise the same language (or are the same machine).

automata similar <machine|dir ...>

Groups machines that are the same: finite automata by language (their minimal
DFAs match, whatever they look like), anything else by structure (the same
machine up to renaming states). --bounded N groups the rest by behaviour
instead: the same verdict (and output) on every word up to length N.

Built for a folder of submissions, where two students' identical answers are
worth a look.

  --bounded N       compare non-finite automata by behaviour up to length N
  --all             list machines that are in no group too
  --json

Exit: 0 no two alike, 1 at least one group.

Examples

# group identical answers (same language, or same machine)
automata similar submissions/
# group PDAs and TMs by behaviour on words up to length 6
automata similar submissions/ --bounded 6

fuzz

Compare a machine with an external program on random words, and shrink a disagreement.

automata fuzz <machine> --oracle '<command>'

Runs the machine and the oracle on the same words — every word up to length 3,
then random ones — and stops at the first disagreement, which it shrinks to a
minimal counterexample.

The oracle gets the word three ways: as {} in the command (or appended), on
stdin, and in $AUTOMATA_WORD. {} becomes a quoted reference to that variable
("$AUTOMATA_WORD", or "%AUTOMATA_WORD%" under cmd.exe), so a word's symbols
reach the program as themselves and are never run by the shell. Every {} is
replaced, so a script with braces of its own should read $AUTOMATA_WORD
instead. It answers by
  --mode exit       exit code 0 = accept (default)
  --mode stdout     yes/no, true/false, 1/0, accept/reject on its first line
  --mode output     its first line is the expected output (transducers)
  --batch           one process for all words: a word per stdin line, an answer per stdout line

  --count N         words to try (default 500)
  --max-len N       longest random word (default 12)
  --seed S          repeatable words
  --timeout MS      per oracle call (default 5000)
  --no-shrink
  --json

  automata fuzz even-ones.automaton --oracle 'python -c "import sys; print(sys.argv[1].count(\"1\") % 2 == 0)" {}' --mode stdout

Exit: 0 no disagreement, 1 a disagreement, 2 the machine had no verdict on some word.

Examples

# the oracle prints yes/no for the word in {}
automata fuzz machine.automaton --oracle "python check.py {}" --mode stdout
# one process answers every word, a line each
automata fuzz machine.automaton --oracle "node check.js" --batch
# more and longer words, repeatably
automata fuzz machine.automaton --oracle "./is_valid" --count 5000 --max-len 20 --seed 7

Transforming

from-regex

Regular expression → ε-NFA (Thompson).

automata from-regex '<regex>' [--sigma ab]

Thompson's construction, with the app's regex syntax: | concatenation * + ?
{n,m} [a-z] [^…] . and ε. --sigma sets what . and [^…] range over.

  -o, --output FILE   write here (the extension picks the format); default stdout
  -t, --to FORMAT     automaton (default), jff, hoa, ba, timbuk, code, dot, …

Examples

# an ε-NFA document on standard output
automata from-regex "(a|b)*abb"
# minimized, to a file
automata from-regex "(a|b)*abb" --min -o abb.automaton
# . ranges over {x, y, z}
automata from-regex "a.b" --sigma xyz

to-regex

Finite automaton → regular expression (state elimination).

automata to-regex <machine>

State elimination, least-connected state first.

Examples

# a regular expression for the language
automata to-regex machine.automaton
# round trip
automata from-regex "(ab)*" | automata to-regex -

determinize

Subset construction → DFA.

automata determinize <machine>

The reachable subset construction. --complete keeps the empty-set sink.
  -o, --output FILE   write here (the extension picks the format); default stdout
  -t, --to FORMAT     automaton (default), jff, hoa, ba, timbuk, code, dot, …

Examples

# the subset construction
automata determinize nfa.automaton -o dfa.automaton
# keep the ∅ sink, as Graphviz
automata determinize nfa.jff --complete --to dot

minimize

Minimal DFA.

automata minimize <machine>

The minimal DFA, states in breadth-first order. --complete keeps the sink.
  -o, --output FILE   write here (the extension picks the format); default stdout
  -t, --to FORMAT     automaton (default), jff, hoa, ba, timbuk, code, dot, …

Examples

# the minimal DFA (without its dead sink)
automata minimize dfa.automaton
# in a pipe
automata from-regex "(a|b)*abb" | automata minimize - | automata info -

complement

Complement DFA over Σ.

automata complement <machine>

A complete DFA for Σ* minus the language.
  -o, --output FILE   write here (the extension picks the format); default stdout
  -t, --to FORMAT     automaton (default), jff, hoa, ba, timbuk, code, dot, …

Examples

# Σ* minus the language
automata complement dfa.automaton -o not.automaton

reverse

Reverse the language.

automata reverse <machine>
  -o, --output FILE   write here (the extension picks the format); default stdout
  -t, --to FORMAT     automaton (default), jff, hoa, ba, timbuk, code, dot, …

Examples

# the reversal, minimized
automata reverse dfa.automaton | automata minimize -

star

Kleene star.

automata star <machine>
  -o, --output FILE   write here (the extension picks the format); default stdout
  -t, --to FORMAT     automaton (default), jff, hoa, ba, timbuk, code, dot, …

Examples

# the Kleene star, as an ε-NFA
automata star dfa.automaton

union

Union of two finite automata.

automata union <machine-a> <machine-b>
  -o, --output FILE   write here (the extension picks the format); default stdout
  -t, --to FORMAT     automaton (default), jff, hoa, ba, timbuk, code, dot, …

Examples

# L(a) ∪ L(b)
automata union a.automaton b.automaton -o either.automaton

concat

Concatenation of two finite automata.

automata concat <machine-a> <machine-b>
  -o, --output FILE   write here (the extension picks the format); default stdout
  -t, --to FORMAT     automaton (default), jff, hoa, ba, timbuk, code, dot, …

Examples

# L(a)·L(b)
automata concat a.automaton b.automaton

intersect

Product DFA for the intersection.

automata intersect <machine-a> <machine-b>
  -o, --output FILE   write here (the extension picks the format); default stdout
  -t, --to FORMAT     automaton (default), jff, hoa, ba, timbuk, code, dot, …

Examples

# words both accept
automata intersect a.automaton b.automaton | automata words -

difference

Product DFA for A \ B.

automata difference <machine-a> <machine-b>
  -o, --output FILE   write here (the extension picks the format); default stdout
  -t, --to FORMAT     automaton (default), jff, hoa, ba, timbuk, code, dot, …

Examples

# words a accepts and b does not
automata difference a.automaton b.automaton | automata words -

eps-elim

Remove ε-moves.

automata eps-elim <machine>
  -o, --output FILE   write here (the extension picks the format); default stdout
  -t, --to FORMAT     automaton (default), jff, hoa, ba, timbuk, code, dot, …

Examples

# the same language, no ε-moves
automata eps-elim enfa.automaton

eval

Evaluate an expression over machines: min(det(A) & ~B).

automata eval '<expression>' [NAME=machine ...]

  min(det(A) & ~B)          A=a.automaton B=b.jff
  /(a|b)*abb/ == A          compare a regex with a machine
  A <= B                    is L(A) contained in L(B)?

Operators, tightest first: postfix * (star), ~ (complement), . (concatenation),
& (intersection), \ (difference), | or + (union). Functions: min, det, comp,
rev, star, eps, union, inter, diff, xor, concat, regex('…'). A /regex/ or a
'quoted/path' is a machine too. With ==, !=, <= or >= at the top the answer is
a verdict, not a machine.

  --sigma abc         the alphabet for ~ and for . in a regex

  -o, --output FILE   write here (the extension picks the format); default stdout
  -t, --to FORMAT     automaton (default), jff, hoa, ba, timbuk, code, dot, …

Exit (comparisons): 0 true, 1 false.

Examples

# an expression over machines
automata eval "min(det(A) & ~B)" A=a.automaton B=b.jff
# is my machine this regex? (exit 0 yes, 1 no)
automata eval "/(a|b)*abb/ == A" A=mine.automaton
# is L(A) contained in L(B)?
automata eval "A <= B" A=a.automaton B=b.automaton

Formats

convert

Convert between .automaton, .jff, HOA, BA, Timbuk, machine codes, ….

automata convert <machine> [-o out.ext] [--to format]

Reads any machine the CLI reads and writes it in the format --to names, or the
one -o's extension implies, or as an .automaton document on standard output.

  Formats: automaton, jff, hoa, ba, timbuk, code (machine code), standard (TM
  notation), svg, and every export format (automata export --list).

  --determinize, --minimize, --eps-elim   transform on the way (finite automata)
  --opt key=value                          options for an export format

Examples

# JFLAP → the app's format
automata convert machine.jff -o machine.automaton
# an ω-automaton for Spot/Owl
automata convert nba.automaton --to hoa
# and back
automata convert spot-output.hoa -o machine.automaton
# transform on the way
automata convert nfa.automaton --minimize -o min.jff
# a Turing machine as 1RB1LB_1LA1RZ
automata convert tm.automaton --to standard

export

Any of the app's export formats: DOT, TikZ, tables, samples, code, tests.

automata export <machine> -f <format> [--opt key=value ...] [-o file]
       automata export --list

The app's export dialog, from the command line: the same formats, the same
options, the same output.

Examples

# every format and its options
automata export --list
# Graphviz, top to bottom
automata export machine.automaton -f dot --opt rankdir=TB | dot -Tpng > m.png
# a compilable LaTeX figure
automata export machine.automaton -f tikz --opt standalone=true -o m.tex
# accepted and rejected words
automata export machine.automaton -f samples --opt format=json

codegen

automata codegen <machine> --lang js|py|java|c|xstate|scxml|jest|pytest [--style table|switch|class] [-o file]

The code the export dialog generates. --class-name sets Java's class.

Examples

# a Python accepts() function
automata codegen dfa.automaton --lang py -o recogniser.py
# a Java class
automata codegen dfa.automaton --lang java --style class --class-name Parser
# C, one switch per state
automata codegen dfa.automaton --lang c --style switch
# a test suite derived from the language
automata codegen dfa.automaton --lang jest

svg

Draw the machine as an SVG.

automata svg <machine> [-o file.svg]

The machine drawn with state names, and edge labels where it is small enough to read them.

Examples

# a labelled diagram that carries its own styles
automata svg machine.automaton -o m.svg
# dark colours
automata svg tm.automaton --theme dark

animate

A run as an animated SVG, or a Turing machine's space-time diagram as a GIF.

automata animate <machine> <word> [-o run.svg]

The run as an animated SVG of the diagram: each step lights the states the
machine is in and the edge it took, and the last frame holds in the verdict's
colour. Opens in any browser and drops into slides that take SVG.

  --gif             a tape machine's run as an animated GIF instead: the
                    space-time diagram growing one row per step. For video,
                    ffmpeg -i run.gif -pix_fmt yuv420p run.mp4
  --step-ms N       milliseconds per step (default 600)
  --theme dark      dark colours (default light)
  --limit N         at most N steps (default 200)

Examples

# the run as a self-playing SVG
automata animate machine.automaton 0110 -o run.svg
# BB(5)'s first 400 steps as a GIF
automata animate 1RB1LC_1RC1RB_1RD0LE_1LA1LD_1RZ0LA "" --gif --limit 400 --cell 3 -o bb5.gif

Teaching

grade

Grade submissions against an exercise; CSV or Gradescope results.json.

automata grade <exercise> <submission | dir ...>

Grades each submission the way the app's exercise panel does: exactly for
finite automata, word by word up to the exercise's length bound otherwise.
The exercise is an .automaton file with an exercise in it (the app's
Create Exercise writes one), or any machine, which is then the reference.

  --csv FILE            one row per submission (default: a table on stdout)
  --gradescope FILE     Gradescope's results.json, for one submission
  --points N            score for a correct answer (default 1)
  --allow DFA,NFA       for a bare reference: the machine types accepted
  --max-states N        for a bare reference: the most states allowed
  --max-length N        for a bare reference: the bound for non-exact grading
  --json

Exit: 0 every submission passed, 1 one did not.

Examples

# a class at once
automata grade exercise.automaton submissions/ --csv grades.csv
# inside a Gradescope autograder
automata grade exercise.automaton submission.automaton --gradescope /autograder/results/results.json
# a bare reference machine as the exercise
automata grade reference.automaton submissions/ --allow DFA --max-states 5

See also: generate, similar, help grading.

generate

Random exercises with answer keys.

automata generate [--states N] [--sigma 01] [--count K] [-o dir]

Random DFA exercises with the properties asked for, each with an answer key.
The student's file (exercise-1.automaton, …) opens in the app as an exercise
on a blank canvas; the key (key-1.automaton) is the reference DFA, drawn.

  --states N        states in the minimal DFA (default 4)
  --sigma 01        the alphabet (default 01)
  --count K         how many (default 1)
  --seed S          the same exercises again
  --prompt KIND     regex (the language as a regular expression, default) or
                    examples (words it accepts and rejects)
  --from-regex RE   one exercise from a regular expression instead of at random
  --allow TYPES     machine types a student may answer with (default DFA,NFA,ε-NFA)
  --max-states N    the most states an answer may have
  --infinite        only languages with infinitely many words
  -o, --output DIR  where to write (default: the current directory)
  --json            print the exercises instead of writing files

Examples

# ten different exercises with keys
automata generate --states 4 --count 10 --seed 2026 -o week3/
# one exercise from a regex
automata generate --from-regex "(ab|ba)*" -o ex/
# described by example words instead of a regex
automata generate --states 3 --prompt examples --infinite

Turing machines

halts

Does it halt? Proof methods, growth class, workers, proof files.

automata halts <machine | list.txt | code ...>

Does each machine halt from a blank tape (or --input)? Methods, cheapest first:
simulation, cycler, translated cycler and backward reasoning (the app's own),
then n-gram closed position sets, then the busy beaver bound for machines in
the model whose S(n, k) is proved. What is still unknown gets a growth reading:
how fast its tape grows — logarithmic (counter-like), √t (bouncer-like), …

A text file is a list: one machine per line, in the standard notation or as a
machine code; # starts a comment.

  --budget N        steps for the simulation-based methods (default 1000000)
  --cps N           largest closed-position-set window (default 10; 0 = off)
  --induction-ms N  time for the inductive-rule prover per machine (default 2000; 0 = off)
  --no-bound        skip the busy beaver bound
  --no-growth       skip the growth reading for unknowns
  --input w         run on w instead of a blank tape (.automaton machines)
  --workers N       worker threads (default: one per core, for 3+ machines)
  --proof DIR       write one proof file per decided machine (check-proof reads them)
  --json

Exit: 0 every machine decided, 2 some unknown, 3 some could not be read.

Examples

# one machine
automata halts 1RB1LB_1LA1RZ
# a list, one per line, with a proof file per decided machine
automata halts machines.txt --proof proofs/
# a machine from a file, on a word
automata halts tm.automaton --input 0110
# what is still open
automata halts machines.txt --json | jq '.[] | select(.verdict=="unknown")'

check-proof

Independently re-check a proof file written by halts --proof.

automata check-proof <proof.json | dir ...>

Re-checks each proof with code that shares nothing with the prover: its own
tape, its own stepper, its own reading of the notation. Backward reasoning is
the exception — it is re-run with the app's search, and marked as such.

Exit: 0 every proof holds, 1 one does not.

Examples

# re-check every proof file
automata check-proof proofs/

bb-search

Enumerate n-state Turing machines and classify them all.

automata bb-search --states N [--symbols K]

Enumerates every N-state, K-symbol Turing machine in tree normal form and
classifies each one: it halts (the champion is the busy beaver candidate),
provably never halts (by method), or is a holdout. Does not use the busy beaver
bound, which would assume the answer. 2×2 and 3×2 take moments; 4×2 minutes.

  --budget N        steps per machine (default 100000)
  --cps N           largest closed-position-set window (default 4)
  --induction-ms N  inductive-rule prover time per machine (default 300)
  --workers N
  --holdouts FILE   write the unknown machines here, one per line
  --json

Examples

# every 3-state machine; finds BB(3) = 21
automata bb-search -n 3
# 2 states, 3 symbols; save the unsettled ones
automata bb-search -n 2 -k 3 --holdouts open.txt
# 4 states: minutes, on 8 cores
automata bb-search -n 4 --workers 8

tm-normalize

Put Turing machines in normal form and drop duplicates.

automata tm-normalize <list.txt | code ...> [--prune]

Prints each machine's normal form, dropping duplicates: mirrored so the first
move is R, states renamed breadth-first from A. --prune drops states that
cannot be reached. The count of duplicates goes to standard error.

  --keep-order      print every line (normalised), duplicates included
  --json            [{ machine, normal, duplicateOf }]

Examples

# drop renamings and mirror images
automata tm-normalize machines.txt > unique.txt
# drop unreachable states too
automata tm-normalize machines.txt --prune --json

sheet

A contact sheet of space-time diagrams, one per machine.

automata sheet <list.txt | machine ...> [-o sheet.svg]

A contact sheet: one space-time diagram per machine (time down, tape across,
the head in white), captioned with the machine and — unless --no-classify —
its halting verdict. Counters and bouncers are told apart at a glance.

  --steps N         steps drawn per machine (default 20000)
  --cols N          diagrams per row (default 3)
  --size N          diagram width and height in pixels (default 240)
  --png             write one PNG per machine instead, into the -o directory

Examples

# one space-time diagram per machine, captioned with its verdict
automata sheet machines.txt -o sheet.svg
# one PNG each instead
automata sheet machines.txt --png -o pictures/
# one machine, bigger
automata sheet 1RB1LB_1LA1RZ --steps 200 --size 400

Learning

learn

Learn a DFA: RPNI from labelled words, or L* from a membership oracle.

automata learn --from samples.txt
       automata learn --oracle '<command>' --sigma 01
       automata learn --target machine.automaton

--from     RPNI: the smallest-looking DFA consistent with labelled words, one
           per line as "w => accept" / "w => reject" (the test command's
           syntax). Never contradicts the sample; exact with enough examples.
--oracle   L* against a program (the fuzz command's protocol, --mode and
           --batch included). Equivalence is tested on every word up to
           --exhaustive and --tests random words, so the result is exact only
           up to that testing — it says so.
--target   L* against a machine. For a finite automaton equivalence is exact.

  --sigma 01          the alphabet (required with --oracle)
  --exhaustive N      every word up to this length per equivalence test (default 6)
  --tests N           random words per equivalence test (default 1000)
  --max-len N         longest random test word (default 14)
  --seed S
  -o, --output FILE   write the DFA here (default: a document on stdout)
  -t, --to FORMAT

Examples

# RPNI from "word => accept/reject" lines
automata learn --from samples.txt -o learned.automaton
# L* against a program
automata learn --oracle "./validator" --sigma 01 --mode exit
# L* against a machine: its minimal DFA
automata learn --target machine.automaton | automata info -

Elsewhere

library

Search and fetch machines from the machine library.

automata library search [query]
       automata library show <id>
       automata library pull <id> [-o file]

The query is the Library view's: words, plus type:DFA, family:tm, tag:…,
by:login, is:minimal, level:intro, states:<5, accepts:0110, rejects:…

  --library URL|DIR   another build of the library, or a local checkout
                      (also $AUTOMATA_LIBRARY)
  --sort KEY          relevance, added, updated, states, title
  --limit N           at most N results (default 30)
  --json

Examples

# search the machine library
automata library search "tag:textbook type:DFA"
# machines that accept a word
automata library search accepts:0110 is:minimal
# one entry
automata library show finite/dfa/binary-divisibility-by-5
# download it
automata library pull finite/dfa/binary-divisibility-by-5 -o div5.automaton

mcp

Serve the engine to AI agents over the Model Context Protocol (stdio).

automata mcp

Serves the engine over the Model Context Protocol on stdin/stdout, for an AI
agent to call. Tools: decide, info, lint, equiv, transform, from_regex, eval, convert, trace, words, halts.

  claude mcp add automata -- automata mcp

Examples

# register with Claude Code
claude mcp add automata -- automata mcp
# answer a recorded session
automata mcp < session.jsonl

Topics

machines

what a argument can be — automata help machines

Every command that takes a machine takes it the same way.

A file:
  .automaton .json      the app's own document (what Save writes)
  .jff                  JFLAP: finite automata, PDAs, Turing machines, Mealy, Moore
  .scxml  .js .ts       a statechart (SCXML, or an XState config), flattened
  .hoa                  Hanoi Omega-Automata, from Spot, Owl, ltl2tgba, …
  .ba                   RABIT / GOAL Büchi automata
  .timbuk .tmb          Timbuk word automata

Standard input:
  -                     read the machine from stdin, recognised by its content,
                        so machines can be piped from command to command

Inline, as an argument:
  1RB1LB_1LA1RZ         a Turing machine in the standard (bbchallenge) notation:
                        one segment per state A, B, C, …; per symbol read, the
                        symbol written, L or R, and the next state (Z halts,
                        --- is undefined, which also halts)
  fa.01:+AB_BA          a machine code: any machine the app has, as one line
                        (the app's Copy Machine Code writes these)

Every command that makes a machine writes an .automaton document to standard
output unless -o names a file, so they chain:

  $ automata from-regex "(a|b)*abb" | automata minimize - | automata codegen - --lang c

words

how to type words, the empty word, and ω-words — automata help words

A word is typed the way the app's run box takes it.

  0110                  single-character symbols run together
  "01 11 00"            multi-character symbols separated by spaces (or commas)
  ""   ε   eps          the empty word

An ω-automaton (DBA, NBA, DPA, …) reads an infinite word, written u(v): a finite
prefix u, then v repeated forever. "(ab)" is abababab…, "a(b)" is abbbbb….

In a words file (test, learn --from) each line is one word; "w => accept" or
"w => reject" (also acc/rej, a/r, ✓/✗) makes it an expectation; blank lines and
lines starting with # are skipped.

Symbols outside Σ are an error for run and test, and simply have no transition
(so reject) for equiv and grade, which is how the app's grader treats them.

exit-codes

what each exit code means, per command — automata help exit-codes

Every command exits with the three-valued verdict wherever it decides
something. "Unknown" is never folded into "reject": a budget running out is
not a proof, and a script's && must not read it as one.

  0   accept · equal · every test passed · halts or never-halts proved · no
      findings · a transducer ran to the end
  1   reject · different · a test failed · a lint finding · a proof did not check
  2   unknown: a step budget ran out, a run was cut short, or a check was
      bounded and could not decide
  3   could not run: a file that does not read, a word outside Σ, a bad flag

In a shell:
  $ automata run m.automaton "$w" && echo accepted
  $ automata equiv mine.automaton ref.automaton || echo "they differ"
  $ automata halts tm.txt; [ $? -eq 2 ] && echo "some are still open"

formats

every format the CLI reads and writes, and what each loses — automata help formats

                    read   write   notes
  automaton/json     ✔      ✔      everything: layout, card, blocks, exercise
  jff (JFLAP)        ✔      ✔      FA, PDA, TM, Mealy, Moore; empty-stack
                                   acceptance is chosen in JFLAP, not the file
  hoa                ✔      ✔      ω-automata; transition-based and generalized
                                   Büchi acceptance are moved onto states
  ba                 ✔      ✔      Büchi (RABIT/GOAL read finite automata as
                                   Büchi too — the writer warns)
  timbuk             ✔      ✔      word automata only (arities 0 and 1)
  scxml / xstate     ✔      ✔      statecharts; parallel states are refused
  code (SMTF)        ✔      ✔      one line, the machine and nothing else
  standard           ✔      ✔      one-tape TMs over digits, L/R moves
  svg                       ✔      a labelled diagram with its own styles
  dot, tikz                 ✔      Graphviz and LaTeX
  table-csv/md              ✔      transition tables
  samples, coverage         ✔      words, as CSV/JSON/Markdown
  code-*, test-*            ✔      JS, Python, Java, C, XState, SCXML; Jest, pytest

--to FORMAT picks one; otherwise the output file's extension does:
.automaton .json .jff .hoa .ba .timbuk .txt .svg .dot .gv .tex .csv .md .js .py
.java .c .scxml .test.js

turing

Turing machines: halting, busy beavers, space-time pictures — automata help turing

halts        does it halt? tries, cheapest first:
               simulation            it halts within --budget steps
               cycler                a configuration repeats exactly
               translated cycler     it repeats, shifted along fresh tape
               backward reasoning    no halting configuration is reachable
               closed position set   an n-gram abstraction closed under δ
               inductive rule        a run-length pattern that grows forever
               busy beaver bound     it ran past S(n,k), for n ≤ 5 (2 symbols)
             and otherwise reports "unknown" with how its tape grows:
             logarithmic (counter-like) or √t (bouncer-like)
bb-search    every n-state machine, the champion, and the holdouts
sheet        a contact sheet of space-time diagrams
play, trace  one run, step by step; play --history draws the diagram live
profile      steps and cells as the input grows, with a growth estimate

The standard notation: 1RB1LB_1LA1RZ is state A: on 0 write 1, move R, go to
B; on 1 write 1, move L, go to B — then state B likewise. Z (or any letter past
the last state) halts; --- is undefined, which halts too.

proofs

how far each halting proof can be trusted, and check-proof — automata help proofs

halts --proof DIR writes one JSON file per decided machine: the machine as a
table, the verdict, the method, and the method's evidence. check-proof
re-checks them:

  simulation, cycler,       independently: its own tape, its own stepper,
  translated cycler, CPS    sharing no code with the prover
  busy beaver bound         independently simulated; the value of S(n,k) is
                            cited (BB(5) was proved in 2024), not re-proved
  backward reasoning,       re-derived by running the prover again — said so
  inductive rule            in the output

The provers are tested against ground truth: every machine in the 3-state and
2-state 3-symbol enumerations halts within S(n,k) steps if it halts at all,
and no "never halts" claim over either enumeration is wrong.

omega

ω-automata: Büchi, co-Büchi, parity, weak — automata help omega

The eight ω-automata are determinism × acceptance: D/N × Büchi (BA),
co-Büchi (coBA), parity (PA), weak (WA). They read u(v) words (help words).

run, test, trace      decide u(v) words
equiv, diff           compare on every u(v) up to --size symbols — a bounded
                      check, and the output says so
convert --to hoa      for Spot, Owl and the other LTL tools; .hoa files read
                      back, including transition-based and generalized
                      Büchi acceptance and every parity flavour
info                  shows the acceptance: F and whether it must be visited
                      infinitely or finitely often, or the parity priorities

grading

exercises, grading a class, Gradescope — automata help grading

An exercise is an .automaton file with an exercise inside — the app's
Create Exercise writes one, and so does automata generate. It carries the
reference sealed, the machine types allowed, a state limit and hints.

  $ automata generate --states 4 --count 20 --seed 1 -o week3/
      exercise-N.automaton   what students open (a blank canvas + the task)
      key-N.automaton        the answer, drawn
  $ automata grade week3/exercise-1.automaton submissions/ --csv grades.csv

Grading is exact for finite automata (proved equal, or the shortest word they
disagree on) and word by word up to the exercise's length bound otherwise.

For Gradescope, in the autograder's run_autograder:
  automata grade /autograder/source/exercise.automaton \
    /autograder/submission/*.automaton \
    --gradescope /autograder/results/results.json

automata similar submissions/ groups identical answers.

learning

learn a DFA from examples (RPNI) or from a program (L*) — automata help learning

learn --from samples.txt      RPNI: labelled words in, a DFA consistent with
                              every one out; exact with enough examples
learn --oracle "cmd" --sigma  L*: asks the program membership questions and
                              tests its guesses on words; exact as far as the
                              testing reached, and it says so
learn --target m.automaton    L* against a machine; exact for a finite automaton

The oracle protocol is fuzz's: the word as {} in the command (or appended), on
stdin, and in $AUTOMATA_WORD; the answer as the exit code (--mode exit) or a
yes/no line (--mode stdout); --batch for one process answering a line per word.

scripting

pipes, --json, git, CI and shells — automata help scripting

Every command takes --json. Machines travel on stdin/stdout. Exit codes are
verdicts (help exit-codes).

In git:
  git config diff.automaton.textconv "automata diff --textconv"
  echo "*.automaton diff=automaton" >> .gitattributes
  git difftool -x "automata diff" -- machine.automaton

In CI (a GitHub Actions step):
  - run: npx automata lint machines/*.automaton --strict
  - run: npx automata test machines/parser.automaton tests/parser.txt

Colour: automatic in a terminal; NO_COLOR=1 turns it off; FORCE_COLOR=1..3
turns it on for a pager: FORCE_COLOR=3 automata info m.automaton | less -R

mcp

give AI agents the engine as tools — automata help mcp

automata mcp serves the Model Context Protocol on stdin/stdout. Tools:
decide, info, lint, equiv, transform, from_regex, eval, convert, trace,
words, halts. Machines are passed as paths, machine codes, standard-notation
TMs, or .automaton JSON text.

  $ claude mcp add automata -- automata mcp
  (or in another client's config: command "automata", args ["mcp"])

install

installing: the desktop app, npm link, or the bundle — automata help install

With the desktop app (no Node needed): the CLI is inside it.
  Windows   add  %LOCALAPPDATA%\Programs\AutomataStudio\resources\cli  to PATH
  macOS     ln -s "/Applications/AutomataStudio.app/Contents/Resources/cli/automata" /usr/local/bin/automata
  Linux     ln -s /opt/AutomataStudio/resources/cli/automata /usr/local/bin/automata
  or run    AutomataStudio --cli <command> …   (macOS, Linux)

From a checkout:   npm install && npm link
The bundle:        npm run cli:build, then node dist-cli/automata.mjs (Node 20+)

colour

colour, and turning it off — automata help colour

Colour is automatic in a terminal and off when output is piped. Depth is
detected: truecolor (Windows Terminal, iTerm, VS Code, COLORTERM=truecolor),
256 colours (TERM=*256*), or the basic 16.

  NO_COLOR=1       no colour at all (https://no-color.org)
  FORCE_COLOR=3    truecolor even into a pipe:  … | less -R
  FORCE_COLOR=1    the basic 16 colours

Each tape symbol keeps one colour in every command, in play, trace and the
space-time pictures alike; the blank is always the faint one.

FilesExpand file tree

cli-reference.md

Latest commit

History

cli-reference.md

File metadata and controls

automata command reference

Contents

Running

run

test

trace

play

Looking

info

lint

words

profile

Comparing

equiv

diff

similar

fuzz

Transforming

from-regex

to-regex

determinize

minimize

complement

reverse

star

union

concat

intersect

difference

eps-elim

eval

Formats

convert

export

codegen

svg

animate

Teaching

grade

generate

Turing machines

halts

check-proof

bb-search

tm-normalize

sheet

Learning

learn

Elsewhere

library

mcp

Topics

machines

words

exit-codes

formats

turing

proofs

omega

grading

learning

scripting

mcp

install

colour

`automata` command reference