Alloy headless: varlink service + web UI — implementation plan

Status: slice 1 implemented. See README.md for usage and CLAUDE.md for implementation notes.

This document is the original research, kept for its findings about Alloy's internals (§1, §2, §5), which remain accurate and are worth not rediscovering.

Three parts of it were superseded by what was actually built:

• §3.2 (the architecture). The built design inverts it: Java is a dumb worker driven over stdin/stdout, with one long-lived worker per model file rather than a Java varlink parent forking a child JVM per solve. This is warmer (the JVM start is paid once per file, not once per solve, so the warm-child pool is unnecessary) and uses one protocol instead of two. Everything §3.2 says about why solving must happen in a killable process still stands — that is the finding the design rests on.
• §4 (the varlink API) is gone entirely. The interface was implemented as specified, then removed: nothing consumed it, and the web UI never went through it. The method set survives as the methods on *server in serve.go (Reload, RunCommand, Cancel, Invalidate), so the modelling work in §4 was not wasted — only its wire format was. See CLAUDE.md for the rationale and for when re-adding it would be justified.
• §5's figure reference. filesystem.als corresponds to _images/instance83.png, not instance8.png (which is the filesharing model).

Goal: replace the broken Alloy Swing GUI with a headless pipeline — a long-running Java varlink service wrapping the Alloy solver API, plus a Go web UI that renders instances as graphs.

This document is written so a fresh session can start implementing immediately. Everything marked "VERIFIED" was empirically tested; do not re-litigate it. Everything marked "UNVERIFIED" still needs checking.

0. Orientation: paths and prerequisites

Paths written as ./probes/… in this document are relative to this project directory, users/Profpatsch/alloy-viz/.

Both halves — the Java varlink service and the Go web UI — live in this one project directory. Planned layout:

users/Profpatsch/alloy-viz/
├── IMPL.md                  # this document
├── alloy.varlink            # IDL, single source of truth
├── probes/                  # verified throwaway probes (see §1.8)
├── java/
│   └── src/de/profpatsch/alloy/…   # the varlink service (alloy-viz-solver)
├── *.go                     # the web UI + varlink client (alloy-viz)
├── go.mod
├── default.nix              # builds both, wraps both
├── alloy-viz.service
├── README.md
├── alloy-viz.1
└── CLAUDE.md

Binary names: alloy-viz (Go, the thing you run) and alloy-viz-solver (Java, spawned by it or run as a user service).

The Alloy jar comes from nixpkgs, we do not build Alloy from source:

nix build --no-link --print-out-paths nixpkgs#alloy6
# -> /nix/store/3lkny2f8r6lbxbm125czkfrvjzg4rdmc-alloy6-6.2.0
#    jar at $out/share/alloy/alloy6.jar

Note java is not on $PATH in the dev shell. Use the JDK from the alloy6 closure, or add one to shell.nix (requires asking the user to restart the nix-shell):

JAVA=/nix/store/x2glvhmg5af3cd5vcmvn6p4l3mqq4b3k-openjdk-21.0.10+7/bin/java
JAVAC=.../bin/javac

1. Findings that drive the design

1.1 There is already a CLI (VERIFIED)

The shipped 6.2.0 jar has a full CLI — no GUI needed:

java -jar alloy6.jar help          # exec, commands, solvers, natives, prefs, lsp, gui, version
java -jar alloy6.jar exec -c BelowToo -t json -o - foo.als

It is completely undocumented — no docs in the Alloy repo, nothing on alloytools.org. The only documentation is alloy help exec, generated from bnd @Description annotations. Source: org.alloytools.alloy.cli/…/CLI.java.

1.2 The CLI's JSON output is BROKEN — use XML (VERIFIED)

This is the single most important finding. Minimal repro:

sig A { f : set B }
sig B {}
run { some f } for 3

Root cause: A4Solution.toDTO() at org.alloytools.alloy.core/…/translator/A4Solution.java:2158 does instance.tuples(s.label) against the raw Kodkod instance, whose atom naming does not match Alloy's. It also drops sig-hierarchy atoms and invents phantom atoms (Object$2).

Consequence: never use SolutionDTO / --type json. Serialize with A4SolutionWriter.writeInstance() (…/translator/A4SolutionWriter.java:326) — the same path the GUI and --type xml use. Format is documented in ~/kot/alloy/alloy/org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/translator/instance.txt:

INSTANCE = <instance bitwidth=".." maxseq=".." command=".." tracelength=".." looplength="..">
             PRIMSIG* SUBSETSIG* FIELD* SKOLEM*
PRIMSIG  = <sig ID=".." parentID=".." label=".." builtin/one/lone/some/abstract/private/meta="yes"> ATOM* </sig>
SUBSETSIG= <sig ID=".." label=".." …> ATOM* TYPE+ </sig>
FIELD    = <field ID=".." parentID=".." label=".." var="yes"> TUPLE* TYPES </field>
SKOLEM   = <skolem ID=".." label=".."> TUPLE* TYPES </skolem>
TUPLE    = <tuple> ATOM+ </tuple>      ATOM = <atom label=".."/>

1.3 There is NO incremental solving across edits (VERIFIED)

"Incremental" in Alloy is overloaded three ways; none of them help with editing:

1. A4Solution.isIncremental() / .next() — solution enumeration only. isIncremental() is literally kEnumerator != null (A4Solution.java:1860), set from solver.solveAll(...) at A4Solution.java:1643. Keeps one SAT solver alive with one fixed CNF and adds blocking clauses. Useless once the formula changes.
2. kodkod.engine.IncrementalSolver — exists but Alloy never references it (grep -rn IncrementalSolver over alloy.core/application/cli → 0 hits). Its contract is monotone conjunction (IncrementalSolver.java:41-80): you can only add constraints, never retract. Structurally wrong for editing.
3. CompUtil.parseEverything_fromFile(rep, cache, …) — the cache map is a file-content cache for unsaved editor buffers, not a parse cache. The body clears it and reparses + re-resolves from scratch (CompUtil.java:374).

The GUI is not incremental either. SimpleGUI.doRun (SimpleGUI.java:1091) → SimpleTask1.run (SimpleReporter.java:738) does full parse → translate → solve every single time. Its only advantage over the CLI is that WorkerEngine reuses a warm subprocess (WorkerEngine.java:53-57).

So: a daemon captures 100% of the GUI's speed advantage, because that advantage is entirely JVM warmth. We are not leaving clever incremental analysis on the table — there isn't any.

1.4 Timing: startup dominates for small specs (VERIFIED)

ceilingsAndFloors.als (5 check commands):

So for small models JVM+classload ≈ 0.5 s dwarfs a ~0.1 s solve → a warm JVM is worth it.

But solve time varies enormously on real book models:

The UI must never assume sub-second solves.

1.5 next() and eval() are essentially free (VERIFIED)

• Via CLI --repeat 2 on a temporal model: first instance "duration":144 ms, second "duration":0 ms.
• Via direct API probe: sol.next() took 6 ms.
• A4Solution.eval(Expr, state) (A4Solution.java:1042) evaluates against an already-computed instance — no re-solve.

This is where a daemon genuinely beats the CLI.

1.6 CANCELLATION: Thread.interrupt() DOES NOT WORK (VERIFIED — important)

AbstractKodkodSolver.solveAll javadoc claims @throws AbortedException this solving task was interrupted with a call to Thread.interrupt (AbstractKodkodSolver.java:170). This is a lie for SAT4J.

Empirical test (./probes/Probe3.java): ran instance_19 eventually_elected on a worker thread, called worker.interrupt() after 3 s, then worker.join(20000). Result: worker alive after join? true.

Why: kodkod/solvers/SAT4J.java:115 implements solve() as a bare solver.isSatisfiable() with no interrupt polling and no timeout. free() (line 141) merely nulls the reference. There is no in-process cancel path.

For reference, the Alloy GUI solves this the same way we must: WorkerEngine runs solves in a subprocess and cancels via latest_sub.destroy() (WorkerEngine.java:192,211).

→ Design consequence: solving must happen in a killable child process. See §3.2.

1.7 Headless works (VERIFIED)

edu/mit/csail/sdg/{parser,translator,sim} have zero AWT/Swing imports. Only ast/Browsable.java, ast/Module.java (debug tree viewer) and alloy4/A4Preferences.java (java.awt.Font) touch AWT, on code paths we never take. -Djava.awt.headless=true suffices.

1.8 Plain javac against the release jar works (VERIFIED)

No Gradle, no bnd, no Maven, no varlink/java library. Compiled and ran a probe using CompUtil, TranslateAlloyToKodkod, A4Solution, A4SolutionWriter, A4Reporter, plus JDK21 UnixDomainSocketAddress/ServerSocketChannel:

OK unix socket bind: /tmp/probe-alloy.sock
OK parsed, commands=1
  [reporter] translate solver=sat4j bitwidth=4
  [reporter] solve vars=122 clauses=175
OK solved sat=true incremental=true
OK xml bytes=904
OK next() sat=true took_ms=6

Working probes are in ./probes/{Probe,Probe2,Probe3}.java — read them, they are the skeleton of the service.

Avoid the varlink/java binding: 7 stars, 81 commits, dead Travis CI, Maven+Tycho+Eclipse P2, and absent from varlink.org's own "existing bindings" list. Hand-roll it (§3.1) — the wire format is trivial and this repo already hand-rolls every varlink server.

1.9 slf4j noise (VERIFIED)

Kodkod logs progress to stderr via slf4j-simple. defaultLogLevel=off and per-logger =off do not work (6 lines still emitted). Only this works:

-Dorg.slf4j.simpleLogger.logFile=/dev/null

1.10 Exit-code semantics of the CLI (VERIFIED, informational)

Not used by the service, but documents the trap:

• Exit code reflects only expect mismatches, not SAT/UNSAT. A plain UNSAT run still exits 0.
• --type json --output - on UNSAT prints nothing at all, exit 0.
• --output <dir> mode is reliable: receipt.json lists every command with "solution": [] for UNSAT.
• --repeat N to stdout emits back-to-back JSON documents, no array wrapper.
• --evaluator produces no output on piped (non-TTY) stdin — jline needs a real terminal.

2. What the Alloy GUI actually offers (feature inventory)

From alloy4viz/VizGUI.java. This is the target feature set; we implement a subset.

Instance navigation — all map to A4Solution.fork(p), constants confirmed at A4Solution.java:448,462-469:

-1/-2/≥0 are temporal-only and throw UnsupportedOperationException otherwise. Only -3 is universally available.

View modes (VizGUI.java:1996-2046): Viz (graph), Txt, Table, Tree. Theme (VizState.java): per-type/per-relation nodeColor, nodeStyle, edgeColor, label, number, hideUnconnected, showAsAttr, showAsLabel; plus Magic Layout auto-theming. Saved as .thm XML. Projection (StaticProjector.java:144): collapse a dimension (e.g. over State). Evaluator panel, Export (Dot/XML/Predicate).

Reference screenshots showing exactly this UI: ~/kot/alloy/practicalalloy.github.io/_images/instance10.png (temporal trace, toolbar) and instance101.png (leader election, attributes-as-labels, skolem box, trace bar with loopback).

3. Architecture

  editor ──writes──> foo.als
                        │ (fsnotify)
                        ▼
  ┌──────────────────────────────┐   varlink    ┌────────────────────────────┐
  │ alloy-viz (Go)               │─unix socket─>│ alloy-viz-solver (Java)    │
  │ · file watcher               │  NUL-JSON    │ · warm JVM, headless       │
  │ · instance XML → graph model │              │ · parse/typecheck in-proc  │
  │ · DOT emit → graphviz dot    │              │ · SOLVE IN CHILD JVM (§3.2)│
  │ · HTTP + SSE                 │              │ · A4SolutionWriter → XML   │
  └──────────────────────────────┘              └────────────────────────────┘
            │ SVG
            ▼  browser (dumb viewer, no JS build)

Decisions already made with the user:

• Server-side graphviz → SVG, not d3. Rationale: dot's layered layout matches the book figures (d3-force would not); instances are small so layout cost is irrelevant; keeps the browser a dumb viewer with no npm/JS build, consistent with webchat/inventory which use plain inline <script>; precedent at users/Profpatsch/haskell-module-deps/default.nix:6 (getBins pkgs.graphviz [ "dot" ]).
• Async with progress + cancel, because of the >2 min solve in §1.4.
• External editor; browser is a viewer. No in-browser editing.
• Hand-rolled Java varlink. Ignore varlink-http-proxy / varlink-mcp-bridge.
• Use-case-driven vertical slices, not a big up-front API.

3.1 Varlink conventions in this repo (follow these exactly)

Read users/Profpatsch/claude-usage/varlink.go (415 lines, the most compact complete example) and users/Profpatsch/agent-last-position/agent-last-position.go:442.

• Wire format: NUL-terminated JSON over a unix socket. One JSON object per message, \0 delimiter. That's the whole protocol.
• Request: {"method":"iface.Method","parameters":{…}}; optional "more":true for streaming replies.
• Reply: {"parameters":{…}} or {"error":"…","parameters":{…}}; streaming replies set "continues":true on all but the last.
• Interface naming: de.profpatsch.Foo. Socket: /run/user/$UID/de.Profpatsch.Foo.
• Must implement org.varlink.service.GetInfo and org.varlink.service.GetInterfaceDescription (returning the IDL as a string literal). Everything generic in this repo depends on those.
• Errors use reverse-DNS names, e.g. de.profpatsch.Alloy.ParseError.

3.2 The solve-subprocess design (consequence of §1.6)

Because a running SAT4J solve cannot be interrupted in-process, alloy-viz-solver is a supervisor, not the solver:

• Parent JVM (long-lived): holds the varlink socket, parses/typechecks models (CompUtil.parseEverything_fromFile — cheap, ~0.3 s, interruptible enough), caches CompModule keyed by (path, mtime/content-hash), tracks jobs.
• Child JVM per solve: same jar, a --solve-worker mode. Receives command index + options on stdin, streams progress + final instance XML back on stdout as NUL-JSON. Killable with Process.destroyForcibly().
• Progress comes from an A4Reporter subclass in the child; the useful cheap callbacks are translate(solver,bitwidth,…) (A4Reporter.java:127) and solve(plength,primaryVars,totalVars,clauses) (A4Reporter.java:141).

Cost of this design: the child pays ~0.5 s JVM startup per solve, which partly defeats §1.4. Mitigations, in order of preference:

1. Warm child pool — keep one idle pre-forked child; it has already loaded the jar and JIT-compiled the parser. Hand it work over its stdin. Replace it after each solve (or after a kill).
2. Accept the 0.5 s for slice 1, optimise later. Solve time ≥ 0.1 s anyway, and correctness/cancellability matters more than 0.5 s.

next()/eval() must live in the child that holds the A4Solution — the solution object cannot cross a process boundary. So a child that produced a satisfiable solution is retained as the session for that solution handle, and Next/Eval are forwarded to it. This is why handles need explicit release + idle eviction from day one of slice 2.

UNVERIFIED: whether a pre-forked warm child meaningfully beats a cold one. Measure before building the pool.

4. Vertical slices

Slice 1 — "save file → browser shows graph"

The minimum that beats running the CLI by hand.

Superseded: this was implemented as a varlink interface and then removed (see the note at the top). The method set below survives as the server API in serve.go; read it as a data-model sketch, not as a wire protocol.

Java de.profpatsch.Alloy methods:

method ListCommands(path: string)
  -> (commands: []Command)
type Command (index: int, label: string, kind: string, scope: string, expects: int)

method Run(path: string, command_index: int, solver: ?string)
  -> (job: string)                       # returns immediately

method JobStatus(job: string, more: true)          # streaming
  -> (state: string,                     # "parsing"|"translating"|"solving"|"done"|"error"|"cancelled"
      progress: ?Progress,
      result: ?RunResult)
type Progress   (primary_vars: ?int, total_vars: ?int, clauses: ?int, solver: ?string, bitwidth: ?int)
type RunResult  (satisfiable: bool, instance_xml: ?string, trace_length: int,
                 loop_state: int, duration_ms: int, solution: ?string)  # solution = handle, slice 2

method Cancel(job: string) -> ()

error ParseError (message: string, filename: ?string, line: ?int, column: ?int)
error NoSuchCommand (index: int, available: int)
error SolverFailed (message: string)

Notes:

• instance_xml is the raw A4SolutionWriter.writeInstance output. Do not invent a JSON instance schema in slice 1 — XML is the tested-correct format and the Go side has to parse a tree anyway.
• Parse errors carry position: Alloy throws Err subclasses (ErrorSyntax, ErrorType) with a Pos (filename/line/column). Surface it.

Go alloy-viz:

• fsnotify on the .als (watch the directory; editors rename-on-save). Debounce ~150 ms.
• On change: ListCommands, then Run the selected command (default: index 0, or last selected). Do not run all commands — 14.7 s for ceilingsAndFloors.als.
• Consume JobStatus stream, push state to browser over SSE.
• Parse instance XML → internal graph model → emit DOT → dot -Tsvg → inline SVG in the page.
• Minimal theme support: if a sibling <stem>.thm exists, honour only visible, attribute, color, shape. (Format verified, see §5.)
• UI: command picker, status line (state + vars/clauses + elapsed), Cancel button, SVG pane, raw-XML disclosure for debugging.

Done when: editing ~/kot/alloy/practicalalloy-models/structural-modeling/instance_07_08/filesystem.als and saving shows a graph resembling _images/instance83.png (not instance8.png, which is a different model — see the note at the top).

✅ Done. Verified: the rendering matches the book figure, rename-on-save re-solves (49 ms warm vs 389 ms cold), and cancelling instance_19 eventually_elected mid-solve terminates it in ~2 s and leaves the service usable.

Slice 2 — enumeration + evaluator

• Next(solution, kind) where kind ∈ next|config|trace|init|fork → fork(-3|-1|-2|0|state+1). Surface UnsupportedOperationException as a proper varlink error for non-temporal models.
• Eval(solution, expr, state) — CompUtil.parseOneExpression_fromString against the held CompModule, then A4Solution.eval. See org.alloytools.alloy.cli/…/Evaluator.java for the pattern (it binds atoms as globals first: world.clearGlobals() then loop current.getAllAtoms()).
• Release(handle), idle eviction, and killing the owning child JVM.
• Temporal trace navigation (trace_length, loop_state already returned).

Slice 3 — fidelity

Full theme support, projection over a sig, unsat cores (A4Solution.highLevelCore() — note it needs a non-incremental solver, which conflicts with enumeration), Magic Layout equivalent.

5. Test corpus

~/kot/alloy/practicalalloy-models: 192 .als + 178 .thm (VERIFIED counts). Layout: <chapter>/<section-or-instance_NN>/<model>.als + .thm.

Many models pin an exact instance, e.g. structural-modeling/instance_07_08/filesystem.als:

run structural_modeling_instance_08 {
  some disj d0, r : Dir, f0 : File, disj e0,e1,e2,e3 : Entry, n0 : Name {
    Dir = d0 + r ; Root = r ; File = f0 ; …
    entries = d0->e0 + … + r->e3
  }
} for 4 expect 1

so output is deterministic and each corresponds to a book screenshot in ~/kot/alloy/practicalalloy.github.io/_images/instance*.png (101 images). This is a golden-output corpus: render ours, eyeball against the book's.

Theme format is simple declarative XML (verified, structural-modeling/instance_07_08/filesystem.thm):

<view nodetheme="Martha" edgetheme="Martha" hideSkolem="yes">
  <node color="Gray"><type name="Entry"/></node>
  <node color="Red"><type name="Object"/></node>
  <node shape="House"><type name="Root"/></node>
  <node shape="Trapezoid"><type name="Dir"/></node>
  <node visible="no"><type name="Name"/></node>
  <edge attribute="no"><relation name="object">…</relation></edge>
  <edge visible="no" attribute="yes"><relation name="name">…</relation></edge>
</view>

Good starting models:

6. Packaging

Follow repo conventions exactly (see users/Profpatsch/claude-usage/ and users/Profpatsch/maildir-varlink/).

One project, one default.nix, two binaries. The Java half is built as an inner derivation and the Go half wraps it, so nix build .#alloy-viz gives a bin/alloy-viz that already knows where its solver is.

{ depot, pkgs, lib, ... }:
let
  alloyJar = "${pkgs.alloy6}/share/alloy/alloy6.jar";
  jdk      = pkgs.openjdk21;

  # Java varlink service — plain javac, no Gradle/bnd/Maven (see §1.8).
  solver = pkgs.stdenv.mkDerivation {
    name = "alloy-viz-solver";
    src = ./java;
    nativeBuildInputs = [ jdk pkgs.makeWrapper ];
    buildPhase = ''
      mkdir -p classes
      javac -cp ${alloyJar} -d classes $(find src -name '*.java')
      jar cf alloy-viz-solver.jar -C classes .
    '';
    installPhase = ''
      mkdir -p $out/share/java $out/bin
      cp alloy-viz-solver.jar $out/share/java/
      makeWrapper ${jdk}/bin/java $out/bin/alloy-viz-solver \
        --add-flags "-Djava.awt.headless=true" \
        --add-flags "-Dorg.slf4j.simpleLogger.logFile=/dev/null" \
        --add-flags "-cp ${alloyJar}:$out/share/java/alloy-viz-solver.jar" \
        --add-flags "de.profpatsch.alloy.Main"
    '';
  };

  ui = pkgs.buildGoModule {
    name = "alloy-viz-unwrapped";
    src = ./.;
    vendorHash = null;   # or the real hash once deps are pinned
  };
in
pkgs.symlinkJoin {
  name = "alloy-viz";
  paths = [ ui solver ];
  buildInputs = [ pkgs.makeWrapper ];
  postBuild = ''
    wrapProgram $out/bin/alloy-viz \
      --prefix PATH : ${lib.makeBinPath [ pkgs.graphviz ]} \
      --set ALLOY_VIZ_SOLVER ${solver}/bin/alloy-viz-solver
  '';
}

ALLOY_VIZ_SOLVER lets the Go side spawn the solver itself when no service socket is present — makes nix run .#alloy-viz -- foo.als work with no setup, while still allowing a long-running systemd user service.

Also required:

• add module to /home/philip/kot/Profpatsch/go.work
• add to flake.nix packages and apps (~line 65–135)
• alloy-viz.service systemd user unit (see agent-last-position.service)
• README.md pointing at a troff alloy-viz.1 manpage
• CLAUDE.md with implementation notes

Note: pkgs.alloy6 in nixpkgs installs only the jar plus a desktop entry (verified: its buildCommand is install -Dm644 $src $jar + makeWrapper). The jar path $out/share/alloy/alloy6.jar is stable, but pin/verify it when writing the derivation rather than trusting this note.

Install/restart flow is in the root CLAUDE.md (nix profile install/upgrade, copy .service, daemon-reload, enable, restart).

7. Implementation order (concrete first steps)

1. mkdir -p users/Profpatsch/alloy-viz/java/src/de/profpatsch/alloy. Port ./probes/Probe.java into a real Main.java: bind the unix socket, NUL-JSON read/write loop, GetInfo + GetInterfaceDescription returning the IDL string. Verify with printf '{"method":"org.varlink.service.GetInfo"}\0' | nc -U /run/user/$UID/de.Profpatsch.Alloy.
2. Add ListCommands (parse only — no solving yet). Test against filesystem.als (expect 4 commands) and ceilingsAndFloors.als (expect 5).
3. Add the solve child-process mode + Run/JobStatus/Cancel. Test cancel against instance_19 eventually_elected — that's the whole reason for the subprocess design.
4. Go side: varlink client (reuse users/Profpatsch/varlink-lib), XML parse, DOT emit, dot -Tsvg, HTTP page + SSE, fsnotify.
5. Nix packaging, service files, docs.

Write the .varlink IDL file at the project root as users/Profpatsch/alloy-viz/alloy.varlink (like capability-token-service/capability-tokens.varlink). Both halves need it — Java serves it from GetInterfaceDescription, Go may parse it — so make it a build input rather than duplicating it as a string literal in the Java source.

8. Traps / gotchas summary

• ❌ Never use --type json or SolutionDTO — silently wrong (§1.2).
• ❌ Thread.interrupt() will not stop a solve (§1.6) — must kill a process.
• ⚠ slf4j only silenced by logFile=/dev/null (§1.9).
• ⚠ A4Solution cannot cross process boundaries → Next/Eval must be routed to the child that owns it (§3.2).
• ⚠ A live A4Solution pins an open SAT solver → handles need eviction.
• ⚠ fork(-1/-2/≥0) throw on non-temporal models — catch and report.
• ⚠ Editors rename-on-save → watch the directory, not the file.
• ⚠ java is not on $PATH in the dev shell.
• ⚠ Solve times range 0.1 s … >2 min. Never block the UI.