File Format

File Format Specification

AutomataLab saves and loads machines using a single, self-contained JSON object with the extension .autolab.json. The format is intentionally designed to be human-readable, easily parsed by external scripts, and strictly backward compatible. New fields are always additive and optional.

---

1. Top-Level Object

Every .autolab.json file contains a single JSON object.

{
  "type": "DFA",              // Enum: "DFA"|"NFA"|"ENFA"|"DPDA"|"NPDA"|"TM"|"LBA"
  "name": "My Machine",       // Optional: Display name
  "language": "...",          // Optional: A free-text description of the machine
  
  // Formal Definition Sets (Optional, but used for strict validation)
  "alphabet": ["a", "b"],     // Input alphabet Σ
  "stackAlphabet": ["X", "Y"],// Stack alphabet Γ (DPDA/NPDA only)
  "tapeAlphabet": ["0", "1"], // Tape alphabet Γ (TM/LBA only)
  
  // Graph Data
  "states": [ ... ],          // Required: Array of State objects
  "transitions": [ ... ],     // Required: Array of Transition objects
  
  // Turing Machine Specifics
  "blankSymbol": "_",         // Default "_"
  "stepLimit": 10000,         // Loop guard for execution (default 10000)
  "tapeCount": 1              // Number of tapes (default 1)
}

---

2. State Objects

States represent the nodes in the React Flow graph. They contain both formal logical data and visual layout data.

{ 
  "id": "q0",               // Unique string. Transitions reference this.
  "label": "Start State",   // Visual label (can be different from ID)
  "isStart": true,          // Exactly ONE state in the array must be true
  "isAccept": false,        // True if this is an accepting/final state
  
  // UI Data
  "x": 80,                  // Canvas X coordinate
  "y": 160,                 // Canvas Y coordinate
  
  // Advanced
  "isReject": false,        // TM/LBA only: immediate halt-and-reject
  "isText": false           // True if this is just a floating text note
}

---

3. Transition Objects

Transitions are the edges connecting the states. Their structure depends entirely on the top-level "type" of the machine.

Finite Automata (DFA, NFA, $\epsilon$-NFA)

FA transitions define an array of symbols.

{ 
  "id": "t1", 
  "from": "q0", 
  "to": "q1", 
  "symbols": ["a", "b"] // Fires on 'a' or 'b'
}

Note: For an $\epsilon$-transition (ENFA only), use ["ε"], ["eps"], or [""].

Pushdown Automata (DPDA, NPDA)

PDA transitions use read, pop, and push strings. They ignore the symbols array.

{ 
  "id": "t2", 
  "from": "q0", 
  "to": "q1", 
  "symbols": [], 
  "read": "a",          // Input token to consume. "" means ε.
  "pop": "X",           // Stack token to pop. "" means ε.
  "push": "YZ"          // Tokens to push. 
}

Important Note on PDA Pushes: The push string is parsed dynamically based on the "stackAlphabet". If your stack alphabet contains multi-character tokens (e.g., ["id", "+"]), and you set "push": "id+", AutomataLab intelligently parses it into the tokens ["id", "+"] and pushes them. The first token in the string is placed at the top of the stack.

Turing Machines (TM, LBA)

TM transitions use read, write, and direction.

{ 
  "id": "t3", 
  "from": "q0", 
  "to": "q1", 
  "symbols": [], 
  "read": "0", 
  "write": "1", 
  "direction": "R"      // "L" (Left), "R" (Right), or "S" (Stay)
}

Multi-Tape Turing Machines

If "tapeCount" > 1, transitions use array-based variants:

{ 
  "id": "t4", 
  "from": "q0", 
  "to": "q1", 
  "symbols": [], 
  "reads": ["a", "_"], 
  "writes": ["a", "X"], 
  "directions": ["R", "L"] 
}

---

4. Full Example: Minimal DFA

{
  "type": "DFA",
  "name": "Ends with 'a'",
  "alphabet": ["a", "b"],
  "states": [
    { "id": "q0", "label": "q0", "isStart": true, "isAccept": false, "x": 0, "y": 0 },
    { "id": "q1", "label": "q1", "isStart": false, "isAccept": true, "x": 200, "y": 0 }
  ],
  "transitions": [
    { "id": "e1", "from": "q0", "to": "q1", "symbols": ["a"] },
    { "id": "e2", "from": "q0", "to": "q0", "symbols": ["b"] },
    { "id": "e3", "from": "q1", "to": "q1", "symbols": ["a"] },
    { "id": "e4", "from": "q1", "to": "q0", "symbols": ["b"] }
  ]
}