File Format

File Format (.autolab.json)

AutomataLab saves each machine as a single, self‑contained JSON object with the extension .autolab.json (it's just JSON — no wrapper or version header). The format is stable and backward compatible: new fields are additive and optional, so old files keep loading.

This page is a practical summary. The canonical, exhaustive specification — every field, the full execution semantics, and complete examples for all seven types — lives in fsm_format.md in the repo. That file is also designed to be pasted into an LLM to generate or simulate machines.

Top‑level object

{
  "type": "DFA",              // "DFA"|"NFA"|"ENFA"|"DPDA"|"NPDA"|"TM"|"LBA"
  "name": "My machine",       // optional, display only
  "language": "…",            // optional, free‑text description
  "alphabet": ["a", "b"],     // optional, input alphabet Σ
  "stackAlphabet": ["A","Z"], // optional, DPDA/NPDA — stack alphabet Γ (validation only)
  "tapeAlphabet": ["0","1","_"], // optional, TM/LBA — tape alphabet Γ (validation only)
  "states": [ … ],            // required
  "transitions": [ … ],       // required
  "blankSymbol": "_",         // optional, TM/LBA only — default "_"
  "stepLimit": 10000,         // optional, TM/LBA only — loop guard, default 10000
  "tapeCount": 1              // optional, TM only — number of tapes, default 1
}

State

{ "id": "q0", "label": "q0", "isStart": true, "isAccept": false, "x": 80, "y": 160 }

• id unique; transitions reference states by id.
• Exactly one state has isStart: true; isAccept is true for accepting states.
• x/y are canvas pixels (run Auto Layout after importing hand‑written files).
• isReject (TM/LBA only) marks a halt‑and‑reject state; isText marks a non‑machine annotation.

Transitions — three flavours

Finite automata use symbols; PDAs use read/pop/push; TM/LBA use read/write/direction. PDA and TM transitions set symbols: [].

// FA: fires on 'a' (use ["ε"] for an ε‑edge, ENFA only)
{ "from": "q0", "to": "q1", "symbols": ["a"] }

// PDA: (read, pop → push) — "" means ε
{ "from": "q0", "to": "q0", "symbols": [], "read": "a", "pop": "", "push": "A" }

// TM/LBA: (read → write, direction) — direction is "L"|"R"|"S"
{ "from": "q0", "to": "q1", "symbols": [], "read": "0", "write": "X", "direction": "R" }

// Multi‑tape TM (tapeCount > 1): arrays of length N
{ "from": "q0", "to": "q0", "symbols": [], "reads": ["a","_"], "writes": ["a","a"], "directions": ["R","R"] }

Example — DFA, strings over {a,b} ending in a

{
  "type": "DFA",
  "name": "ends with a",
  "alphabet": ["a", "b"],
  "states": [
    { "id": "q0", "label": "q0", "isStart": true,  "isAccept": false, "x": 80,  "y": 160 },
    { "id": "q1", "label": "q1", "isStart": false, "isAccept": true,  "x": 280, "y": 160 }
  ],
  "transitions": [
    { "id": "t0", "from": "q0", "to": "q1", "symbols": ["a"] },
    { "id": "t1", "from": "q0", "to": "q0", "symbols": ["b"] },
    { "id": "t2", "from": "q1", "to": "q1", "symbols": ["a"] },
    { "id": "t3", "from": "q1", "to": "q0", "symbols": ["b"] }
  ]
}

Conventions to remember

• ε / empty: "", ε, eps, λ, lambda all mean empty. Canonical: ε for FA symbols, "" for PDA fields.
• Stack: ordered bottom → top; top = last array element; push puts its first character on top.
• Tape: input in cells 0…n‑1, everything else is the blank; TM tape is two‑way infinite; an LBA head is bounded to [0, n].

For the complete rules, acceptance semantics per type, and full TM/LBA/multi‑tape examples, read fsm_format.md.