Add model editor support

[FedericoPonzi]

Adds a model editor similar to the one in the toolbox.

Fixes: #520 #159

Some features:

• Per-field dirty tracking with undo buttons
• Dirty indicator (*) on tabs, Save disabled when clean
• Live spec sync (constants/operators update as you edit the .tla file)
• Inline tooltips explaining every option
• Custom suggestion dropdowns (replaces native datalist)
• Clickable file links to open spec and MC files
• Fully responsive layout
• Feature flag with "Open Settings" prompt when disabled

---

Model Overview tab:

Spec Options tab:

TLC Options tab:

[FedericoPonzi]

I've prototyped the ui on Figma. I mostly worked with Claude for the implementation. I've asked to generate a prompt that could be used to implement this feature, this is the result:

Design doc for the feature

# Model Editor — Specification Document

This document is a precise specification of the TLA+ Model Editor feature for the VS Code TLA+ extension. It is detailed enough to rebuild the feature from scratch.

Feature summary

Entry points

• Command palette: Open with Model Editor
• Context menu on .tla and .cfg files
• "Open with Model Editor" option in the missing-config warning
• Reopen Editor With... on .cfg files

Model Overview tab

• Behavior spec selection (Init/Next, Temporal formula, No behavior spec)
• Init/Next auto-populated from spec with collapsed summary
• Deadlock checkbox
• Invariants with suggestion chips from spec operators
• Properties (shown only in temporal mode)
• Constants editor with kind selection (ordinary, model value, set of model values)
• Symmetry checkbox on set-of-model-values constants

Spec Options tab

• State constraint and action constraint
• Definition overrides (dynamic add/remove rows)
• Additional definitions (free-form TLA+ textarea)
• View expression, Alias, Post-condition

TLC Options tab

• Checking mode: BFS / DFID / Simulation (with mode-specific fields)
• Workers (0 = auto, uses all CPU cores)
• Fingerprint bits
• Profiling toggle

Model file generation

• Generates MC<Spec>.tla and MC<Spec>.cfg
• Full cfg directive coverage: INIT, NEXT, SPECIFICATION, CONSTANT, INVARIANT, PROPERTY, CHECK_DEADLOCK, CONSTRAINT, ACTION_CONSTRAINT, SYMMETRY, VIEW, ALIAS, POSTCONDITION
• JSON state marker for lossless round-tripping (no absolute paths stored)
• Editable model name for multiple configs per spec

TLC integration

• Run MC / Save & Run MC button launches TLC with configured parameters
• TLC options passed as CLI args with managed flag deconfliction
• Opens the model checking results panel automatically

UX

• Per-field dirty tracking with undo (↩) buttons
• Dirty indicator (*) on tabs, Save disabled when clean
• Live spec sync (constants/operators update as you edit the .tla file)
• Inline ⓘ tooltips explaining every option
• Custom suggestion dropdowns (replaces native datalist)
• Clickable file links to open spec and MC files
• Fully responsive layout
• Feature flag (tlaplus.modelEditor.enabled, off by default) with "Open Settings" prompt when disabled

Feature flag

The entire feature is gated behind tlaplus.modelEditor.enabled (boolean, default false). When disabled:

• All menu entries are hidden (via when clause: config.tlaplus.modelEditor.enabled)
• The command shows an info message with an "Open Settings" button
• The custom editor provider shows a disabled message

Entry points

1. Command palette: tlaplus.model.editor.display ("Open with Model Editor") — registered in package.json and main.ts
2. Missing config warning: when user runs TLC without a .cfg, the warning offers "Open with Model Editor" alongside "Create model file" — in modelResolver.ts
3. Reopen Editor With...: .cfg files can be reopened in the model editor via CustomTextEditorProvider (viewType tlaplus.cfgEditor, priority "option") — registered in package.json contributes.customEditors
4. Context menus: editor/context and explorer/context menus, gated behind the feature flag
5. When invoked with a .cfg URI, the command delegates to vscode.openWith for the custom editor. When invoked with a .tla URI, it opens the standalone webview panel.

Architecture

Files

File	Role
src/model/modelEditorFiles.ts	Data model, serialization, parsing, discovery, TLC option conversion
src/panels/modelEditorView.ts	VS Code panel lifecycle, message handling, file I/O, TLC launch
src/webview/model-editor.tsx	React webview entry point (App component + mount)
src/webview/model-editor/components/	Individual React components (InfoTip, TabBar, DirtyField, TextField, etc.)
src/webview/model-editor/OverviewTab.tsx	Model Overview tab
src/webview/model-editor/SpecOptionsTab.tsx	Spec Options tab
src/webview/model-editor/TlcOptionsTab.tsx	TLC Options tab
src/webview/model-editor/styles.ts	Inline styles (S record)
src/webview/model-editor/tips.ts	Tooltip text strings
src/webview/model-editor/dirty.ts	Dirty-tracking helpers and TabId type
esbuild.js	Build entry webviewModelEditorConfig compiles model-editor.tsx → out/model-editor.js

Data flow

User edits in webview
  → React state updates
  → "saveModel" message to extension host
  → serializeModelEditorState() generates tla + cfg content
  → fs.writeFileSync() to MC<Spec>.tla and MC<Spec>.cfg
  → "saved" message back to webview
  → savedState updated, dirty indicators clear

User clicks "Run MC" / "Save & Run MC"
  → "saveAndRun" message with state + tlcOptions
  → save files (if save fails, stop here)
  → revealEmptyCheckResultView() opens the results panel
  → tlcOptionsToArgs() converts UI options to CLI args
  → doCheckModel() called with extraOpts + managedFlags (showOptionsPrompt: false)
  → TLC runs with configured parameters

User edits the .tla spec file
  → onDidChangeTextDocument fires (debounced 500ms)
  → discoverSpecInfo() re-scans the spec
  → "specUpdated" message with new discovered info
  → webview merges new constants (keeping existing assignments, adding new ones)

Message protocol

Webview → Extension:

Command	Payload	Trigger
ready	—	On mount (once, in useEffect)
saveModel	{ state, tlcOptions }	"Save Model Files" button
saveAndRun	{ state, tlcOptions }	"Run MC" / "Save & Run MC" button
openFile	{ path, modelName }	Click on spec name or MC file links. path is "tla", "cfg", or an absolute file path. modelName is used to construct correct file paths after rename.

Extension → Webview:

Type	Payload	Trigger
init	{ state, discovered, tlcOptions? }	Response to ready
saved	—	After successful file save
error	{ message }	After failed file save
specUpdated	{ discovered }	When the .tla spec file changes on disk or in the editor

Data model

ModelEditorState

interface ModelEditorState {
    specName: string;           // e.g. "Spec"
    specPath: string;           // absolute path to the .tla spec (not stored in marker)
    modelName: string;          // e.g. "MCSpec" — editable by user
    behavior: ModelEditorBehavior;
    checkDeadlock: boolean;
    constants: ModelEditorConstantAssignment[];
    invariants: string[];
    properties: string[];
    stateConstraint: string;
    actionConstraint: string;
    definitionOverrides: DefinitionOverride[];
    additionalDefinitions: string;
    symmetryConstants: string[];  // constant names with symmetry enabled
    viewExpression: string;       // VIEW cfg directive
    alias: string;                // ALIAS cfg directive
    postCondition: string;        // POSTCONDITION cfg directive
}

TlcOptionsState (persisted in JSON state marker, passed as CLI args at runtime)

interface TlcOptionsState {
    checkingMode: 'bfs' | 'dfid' | 'simulate';
    workers: number;            // 0 = auto (all CPUs)
    dfidDepth: number;          // default 100
    simulateTraces: number;     // 0 = unlimited
    simulateSeed: string;       // empty = random
    fpBits: number;             // default 1 (TLC default)
    enableProfiling: boolean;
}

Serialization

The state marker JSON has the format { state: {...}, tlcOptions?: {...} }. The specPath field is stripped before serialization to avoid storing absolute paths that become stale when the project moves. It is reconstructed from the file location on load.

MC.tla contains:

---- MODULE MCSpec ----
EXTENDS Spec, TLC
\* Generated by the TLA+ Model Editor.
\* MODEL_EDITOR_STATE {"state":{"specName":"Spec","modelName":"MCSpec",...},"tlcOptions":{...}}
MC_Nat == 0..10                                  ← definition override operators
                                                 ← additional definitions
====

MC.cfg contains:

\* Generated by the TLA+ Model Editor.
\* Manual edits may be overwritten by the editor.
\* MODEL_EDITOR_STATE {"state":{"specName":"Spec",...},"tlcOptions":{...}}
INIT Init
NEXT Next
CHECK_DEADLOCK FALSE
CONSTANT N = 3
CONSTANT Nodes = {a, b}
INVARIANT TypeOK
PROPERTY Liveness
CONSTRAINT StateLimit
ACTION_CONSTRAINT ActionLimit
CONSTANT Nat <- MC_Nat                          ← definition overrides use <- syntax
SYMMETRY MC_symm_Nodes                          ← symmetry set
VIEW <<pc, stack>>                               ← view expression
ALIAS MyAlias                                    ← alias operator
POSTCONDITION PostOp                             ← post-condition operator

Parsing

When opening existing files:

1. First try to find the \* MODEL_EDITOR_STATE JSON marker in cfg or tla — lossless round-trip. Format: { state: {...}, tlcOptions?: {...} }.
2. specPath and specName are always reconstructed from the actual file location (not stored in the marker).
3. If no marker found, fall back to regex parsing of ALL cfg directives (INIT, NEXT, SPECIFICATION, CONSTANT, INVARIANT, PROPERTY, CONSTRAINT, ACTION_CONSTRAINT, CONSTANT name <- replacement, SYMMETRY, VIEW, ALIAS, POSTCONDITION). When parsing SYMMETRY, the MC_symm_ prefix is stripped to recover the original constant name.
4. Constants are always merged from live spec discovery — discovered constants not in the saved state are added with empty values; constants removed from spec are dropped

Discovery

discoverSpecInfo(specText) scans the spec with regexes:

• CONSTANT/CONSTANTS declarations → constants[] (handles comma-separated, parameterized like N(_, _))
• Operator definitions (Name ==) → allOperators[]
• Ranked candidates for Init, Next, Spec, invariants, properties based on naming patterns
• Init/Next are filtered out of invariant and property candidate lists (they're never useful there)
• Discovery reads from the VS Code document model (picks up unsaved edits) with fallback to disk

cfg directive coverage

All TLC cfg directives are fully supported: INIT, NEXT, SPECIFICATION, CONSTANT(S), CONSTRAINT(S), ACTION_CONSTRAINT(S), INVARIANT(S), PROPERTY/PROPERTIES, CHECK_DEADLOCK, SYMMETRY, VIEW, ALIAS, POSTCONDITION.

CONSTANTS block parsing

When parsing a bare CONSTANTS block (no assignments on the same line), the parser reads subsequent lines as constant assignments until it encounters a line starting with a known cfg directive keyword (INIT, NEXT, SPECIFICATION, INVARIANT, etc.) or a line that doesn't parse as a constant assignment. Blank lines are skipped globally and do not terminate the block — constants can span across blank lines.

Definition overrides (CONSTANT name <- replacement) are excluded from the regular constants array to prevent duplicates.

UI Layout

Header section

┌─────────────────────────────────────────────────────────────┐
│  TLA+ Model Editor                                          │
│                                                             │
│  Spec: SpecName (clickable, opens .tla)                     │
│  MCSpec.tla / MCSpec.cfg (clickable, open files) ✎ (rename) │
│                                          [Save] [Run MC]    │
│                                                             │
│  [ Model Overview ] [ Spec Options ] [ TLC Options ]        │
└─────────────────────────────────────────────────────────────┘

• Spec name is a clickable link that opens the .tla file
• MC file names are clickable links; the ✎ button enters edit mode showing MC[___input___].tla / .cfg with ✓/✕ to confirm/cancel. This lets users create multiple MC files for the same spec.
• Save Model Files button: disabled when nothing changed (not dirty)
• Run MC / Save & Run MC: label changes based on dirty state. Saves files if dirty, then calls doCheckModel() with TLC options as extraOpts
• Error display: only shown when file save fails (red text). No status messages for successful saves — the dirty indicators clearing is sufficient feedback.

Tab bar

Three tabs spanning the full width of the panel, each taking equal space (flex: 1, centered text). The active tab has a 2px bottom indicator (a separate <div>, not borderBottom on the button — this avoids persistent border rendering bugs in VS Code webviews). Inactive tabs have no border at all. Tab buttons have outline: none to prevent browser focus borders from persisting.

Dirty tabs show a * suffix (e.g. "Model Overview *").

Model Overview tab

All section headings are uppercase (via textTransform: 'uppercase' CSS).

BEHAVIOR SPEC

• ⓘ tooltip on heading
• Mode dropdown: Init/Next, Temporal formula, No behavior spec — with ⓘ tooltip
• Init/Next mode: shows a collapsed summary ("Init = Init, Next = Next") with a "change" link that expands to show two text fields with suggestion dropdowns
• Temporal mode: shows a "Specification operator" text field with suggestions
• No behavior spec: no additional fields

WHAT TO CHECK

• Checkbox: "Check deadlock" with ⓘ tooltip
• Invariants: comma-separated input with suggestion chips below (Init/Next filtered out)
• Properties: only shown when mode is "temporal" — comma-separated input with suggestion chips (Init/Next filtered out)

WHAT IS THE MODEL (CONSTANTS)

• ⓘ tooltip on heading
• If no constants discovered: "No CONSTANT declarations were discovered."
• Each constant shown as a row: [Name] [Kind dropdown ▾] [Value input]
  • Kind options: Ordinary assignment, Model value, Set of model values
  • Placeholder changes based on kind
  • When kind is "Set of model values", a Symmetry checkbox with ⓘ tooltip appears. Checking it adds the constant name to symmetryConstants[], which serializes as SYMMETRY MC_symm_<Name> in cfg and MC_symm_<Name> == Permutations(<Name>) in the MC tla module.

Spec Options tab

Three grouped sections:

1. CONSTRAINTS: Contains two inline fields with ⓘ tooltips:

   • State constraint: text field, placeholder "e.g. Len(queue) < 5". Serialized as CONSTRAINT expr in cfg.
   • Action constraint: text field, placeholder "e.g. TotalMessages' < 100". Serialized as ACTION_CONSTRAINT expr in cfg.

2. DEFINITION OVERRIDES: Dynamic list of rows, each with [Original operator] → [Override expression] ✕. "+ Add override" button below. ⓘ tooltip on heading.

3. ADVANCED: Groups multiple fields in one section, each with ⓘ tooltip:

   • Additional definitions: multi-line textarea for free-form TLA+ text added to the MC module
   • View expression: text field, serialized as VIEW expr in cfg
   • Alias: text field, serialized as ALIAS OpName in cfg
   • Post-condition: text field, serialized as POSTCONDITION OpName in cfg

TLC Options tab

Three sections, each with uppercase heading:

1. CHECKING MODE: radio buttons (Model checking (BFS) / Depth-first (DFID) / Simulation) with ⓘ tooltip
   • DFID selected → shows "Max depth" number field
   • Simulation selected → shows "Number of traces" number field + "Seed" text field
2. RESOURCES: "Workers (threads)" number input (0 = auto, shows "(0 = auto, uses all available CPU cores)" label only when value is 0) + "Fingerprint bits" number input (default 1, TLC's actual default)
3. ADVANCED: "Enable profiling" checkbox with ⓘ

TLC Options → CLI args conversion

workers: 0 → -workers auto; N → -workers N
simulate → -simulate [num=N as separate arg if traces > 0] [-seed S if seed set]
dfid → -dfid N
fpBits > 0 → -fpbits N
profiling → -coverage 1

Note: VIEW, ALIAS, and POSTCONDITION are now cfg directives (written to the .cfg file), not CLI args.

Important: -simulate and num=N must be separate array elements (not concatenated as "-simulate num=5") because Node's spawn() passes each element as a separate OS argument.

Managed flags and conflict resolution

tlcOptionsManagedFlags() returns the set of all CLI flags the model editor controls: -workers, -simulate, -dfid, -seed, -fpbits, -coverage. When runTlc() receives a managedFlags set, it strips all of these flags from the user's default/prompted options — not just the ones present in extraOpts. This ensures that:

• Unchecking "Enable profiling" actually removes -coverage (instead of the default -coverage 1 leaking through)
• Selecting BFS mode removes any stale -simulate/-dfid from the user's saved TLC settings

Reusable components

InfoTip

Inline ⓘ icon with hover tooltip popover. Popover appears below the icon (not above, to avoid clipping at top edge), left-aligned. Uses editorHoverWidget theme variables. Resets textTransform, letterSpacing, fontWeight to prevent inheriting from uppercase section headings.

DirtyField

Wraps any field. When dirty (value differs from saved state), shows a 3px left border in editorWarning.foreground color and a ↩ undo button (top-right). When not dirty, no border at all (not even transparent — this avoids rendering artifacts in some themes).

TextField

Text input with a custom suggestion dropdown (not native <datalist>, which renders outside the webview in VS Code). Filters suggestions as user types, shows matches in a positioned div below the input using editorSuggestWidget theme variables. Closes on blur with 150ms delay for click selection.

TextListField

Comma-separated input with suggestion chips below. Chips add values on click (if not already present). Accepts optional info prop for an inline ⓘ tooltip.

InitNextFields

Collapsed summary when both Init and Next are populated: "Init = Init, Next = Next" with a "change" link. Expands to show two TextField inputs with suggestions. Defaults are auto-populated from discovery.

ModelNameEditor

Shows MCSpec.tla / MCSpec.cfg (clickable links) with a ✎ button. Edit mode shows MC[input].tla / .cfg with ✓/✕ buttons. Enter confirms, Escape cancels. Updates state.modelName.

TabBar

Renders the three tab buttons (Model Overview, Spec Options, TLC Options) in a flex row with equal width. Each tab shows a * suffix when dirty. The active tab has a 2px indicator <div> below it; inactive tabs have no indicator. See "Tab bar" in the UI Layout section for details.

TextArea

Multi-line <textarea> input with label. Used for the "Additional Definitions" field. Has minHeight: 80px and resize: vertical.

NumberField

Numeric input with label, optional ⓘ tooltip, and optional min constraint. Used for DFID depth, simulation traces, and fingerprint bits in the TLC Options tab.

Dirty tracking

• On init message, savedState and savedTlcOptions are set as deep clones of the received data
• isAnyDirty(current, saved, currentTlc, savedTlc) compares both model state and TLC options via JSON.stringify
• isTabDirty(tab, current, saved, currentTlc, savedTlc) checks fields relevant to each tab — the tlcOptions tab compares currentTlc vs savedTlc
• Per-field dirty: each DirtyField wrapper compares its specific field(s) via deepEqual
• After save confirmation (saved message), both savedState and savedTlcOptions are updated to current values
• Save button disabled when not dirty (including TLC options changes)
• "Run MC" label changes to "Save & Run MC" when dirty
• TLC Options tab shows * when TLC settings have been modified
• On webview re-hydration from vsCodeApi.getState(), both savedState and savedTlcOptions initialize from the same persisted data (prevents false dirty on restore)

Spec switching

When the user opens the model editor for a different spec:

• ModelEditorPanel.createOrReveal updates specPath and calls sendInitData() directly
• setupModelEditorWebview takes getSpecPath: () => string (a getter, not a captured string) so all closures read the current spec
• The onDidChangeTextDocument watcher clears pending timers when spec path changes

Tooltip texts

Every tooltip explains why the user would use the feature, with concrete examples. For instance:

• State constraint: "Limits which states TLC explores... Use this to make large or infinite models tractable — for example, Len(queue) < 5"
• Action constraint: "Useful for focusing model checking on specific scenarios — for example, only exploring paths where message count stays bounded"
• Workers: "Set to 0 to automatically use all available CPU cores (recommended). More workers check faster but use more memory."

Resource management

• A single module-level DiagnosticCollection is reused across all TLC runs from the model editor (cleared before each run, never leaked)
• The spec-sync debounce timer is disposed when the panel closes (prevents postMessage to disposed webview)
• The onDidChangeTextDocument listener is registered in disposables and cleaned up on panel disposal

Styling approach

All styles are inline React CSSProperties objects in a single S constant. No external CSS files. Uses VS Code theme CSS variables throughout:

• --vscode-foreground, --vscode-input-*, --vscode-button-* for standard controls
• --vscode-editorHoverWidget-* for tooltips
• --vscode-editorSuggestWidget-* for suggestion dropdowns
• --vscode-editorWarning-foreground for dirty field highlights
• --vscode-textLink-foreground for clickable file links
• --vscode-focusBorder for active tab indicator
• --vscode-panel-border for section borders
• --vscode-descriptionForeground for muted text and section headings

Section headings use textTransform: 'uppercase', fontSize: '0.8rem', letterSpacing: '0.5px'.

Responsive design

The UI must work at any panel width, including very narrow side panels. Key rules:

• Body: padding: 0 !important (VS Code adds its own), overflow-y: scroll (reserves scrollbar space to prevent layout shifts when content height changes between tabs)
• Page container: box-sizing: border-box, maxWidth: 980px, padding: 12px
• Header row: flexWrap: wrap, alignItems: flex-start — spec info and buttons stack vertically on narrow panels
• Button group: flexWrap: wrap, flexShrink: 0 — buttons stack when they don't fit side by side. Buttons have whiteSpace: nowrap to prevent label text from breaking.
• Tab bar: flexWrap: wrap, each tab has minWidth: 100px and flex: 1 1 0 — tabs wrap to multiple rows at very narrow widths. Tab text has whiteSpace: nowrap.
• Constants row: flex with flexWrap: wrap — name, kind dropdown, and value input stack vertically when narrow. Value input uses flex: 1 1 150px.
• Override row: flex with flexWrap: wrap — operator and expression inputs use flex: 1 1 120px.
• Model name row/edit: flexWrap: wrap

Security

• sanitizeModelName() strips /, \, and .. from model names before constructing file paths — prevents path traversal via crafted model names in JSON state markers or user input
• specPath is not stored in the JSON state marker (stripped before serialization) — prevents stale absolute paths and information leakage
• specPath and specName are always overridden from the current file location on load, not trusted from the marker

Testing

Tests in tests/suite/model/modelEditorFiles.test.ts cover:

• Path building (MC prefix)
• Serialization of all fields (behavior, constants, invariants, properties, constraints, overrides, additional definitions)
• Round-tripping through serialize → parse (including TLC options)
• Parsing raw cfg files without editor metadata
• Definition overrides in both cfg and tla output
• Unsupported directive detection
• Parameterized constants
• CONSTANTS block boundary detection at directive keywords
• TLC options round-trip through serialization

Tests in tests/suite/commands/modelResolver.test.ts cover:

• MC-prefixed model resolution
• Missing model warning offers "Open with Model Editor" option

Toolbox parity status

Features at parity with the TLA+ Toolbox

Feature	Notes
Behavior spec (Init/Next, Temporal, No spec)	Same as Toolbox Model Overview
Constants (ordinary, model value, set of model values)	Same assignment types
Symmetry sets	Checkbox on set-of-model-values constants
Deadlock checking	Checkbox
Invariants and Properties	Comma-separated with suggestions
State constraint, Action constraint	Text fields
Definition overrides	Dynamic rows with <- syntax
Additional definitions	Free-form TLA+ textarea
VIEW, ALIAS, POSTCONDITION	All cfg directives supported
All cfg directives	Full coverage
BFS / DFID / Simulation modes	Radio selection with mode-specific fields
Workers	Number input (0 = auto)
Fingerprint bits	Number input
Profiling / Coverage	Toggle (boolean)
Simulation seed	Text field
Model rename	Editable MC file names
Suggestion dropdowns	Auto-populated from spec

Features not yet implemented

Feature	Category	Notes
Standalone Model Values section	Spec Options	Named model values not tied to CONSTANT declarations
Model description / comments	UI	Free-text per-model notes
Simulation trace max length (-depth)	TLC Options	Max steps per simulated trace
Simulation aril (-aril)	TLC Options	Secondary seed adjustment
JVM heap memory slider (-Xmx)	TLC Options	Control RAM allocation for TLC
Max set size (-maxSetSize)	TLC Options	Bound on TLC set enumeration
Defer liveness checking (-lncheck final)	TLC Options	Check temporal properties only at end
Coverage interval selection	TLC Options	Granularity of profiling (every N minutes vs boolean)
Checkpoint recovery (-recover)	TLC Options	Resume from prior checkpoint
Extra JVM arguments field	TLC Options	Free-text box for arbitrary -D flags
Extra TLC parameters field	TLC Options	Free-text box for arbitrary TLC args
Inline validation	UI	Missing constant values, reserved keywords, symbol existence
Evaluate Constant Expressions	UI	Interactive expression evaluator
Integrated Results page	UI	State-space stats and error traces inside the editor
Model locking during run	UI	Read-only state while TLC runs + Stop button
Clone / Delete model	UI	Model management operations
Distributed / Cloud TLC	TLC Options	Remote worker configuration

VS Code-exclusive features (not in Toolbox)

Feature	Notes
Per-field dirty tracking with undo	↩ button on each modified field
Live spec sync	Constants/operators update as you edit the .tla file
ⓘ tooltip explanations	Every field has a hover tooltip explaining why to use it
Responsive layout	Works at any panel width
Feature flag	Experimental opt-in via settings
Editable model names	Create multiple MC configs per spec
MC file auto-resolution	Opening MCSpec.tla resolves to Spec.tla automatically

I don't plan to add any more features, the model editor currently works but I'd like to find opportunities to simplify the code. I'm also considering the idea of splitting in smaller PRs to ease the review.