alloy-viz CLAUDE

Implementation notes. Read this before changing anything here; several of the non-obvious decisions below were arrived at empirically and are easy to "simplify" back into bugs.

IMPL.md is the original research document. It is still accurate about the Alloy internals, but its §3.2 architecture was not what got built — see "Architecture" below.

Reference material

Architecture

browser ──HTTP+SSE──> alloy-viz (Go) ──NUL-JSON stdin/stdout──> alloy-viz-solver (Java)
                        supervisor                               one warm JVM per model file

Java is a dumb worker; Go owns everything else. IMPL.md §3.2 proposed the opposite (Java serving varlink and forking a child JVM per solve, with a warm child pool as mitigation). That would have meant two hand-rolled protocols and a hand-rolled varlink server in Java, and it pays the JVM start per solve. The built design keeps one long-lived worker per model file, which is strictly warmer and needs no pool.

*server (serve.go) owns all of it: the worker, the one job in flight (s.current), and the connected browsers. jobs.go is now only job state and its subscriber fan-out; there is no manager type.

One model per process

This is an invariant, not an accident. An earlier version keyed workers and jobs by path so several models could be open at once. Nothing ever used more than one — the UI watches exactly the file named on the command line — and the job table it required retained a full instance XML per job, so every save leaked one. It was removed; to watch a second file, run a second alloy-viz on another port.

Do not re-introduce the map because it looks more general. It needs a real multi-model requirement first, and with one it is not just a map: jobs need eviction, and workers need idle shutdown, neither of which the old code had. The previous shape is in the history at 7a868f02^.

There was a varlink server here; it was removed

de.profpatsch.Alloy was implemented (~460 lines, varlink.go + alloy.varlink + a systemd unit) and then deleted, because nothing consumed it. The web UI never went through it — serve.go had zero references to varlink — so it was a 16%-of-the-project adapter over the server API with no caller.

Do not re-add it speculatively. If a real consumer turns up (driving Alloy from a script, or exposing it to an agent via varlink-mcp-bridge, which needs only an interface and a .mcp.json entry), it is a thin wrapper over the methods on *server in serve.go and is easy to write then. It is in the history at d2739f45 if the IDL is worth reviving.

Measured, on protocol-design/instance_19 command 2:

Non-obvious things, and why they are that way

Cancellation must kill the process

A running SAT4J solve cannot be interrupted. AbstractKodkodSolver.solveAll claims @throws AbortedException … Thread.interrupt, and that is simply false: kodkod/solvers/SAT4J.java:115 implements solve() as a bare isSatisfiable() with no interrupt polling. Verified empirically (probes/Probe3.java): after interrupt() and a 20 s join, the worker thread is still alive.

So Cancel is Process.Kill(). The Alloy GUI does the same thing (WorkerEngine runs solves in a subprocess and calls destroy()).

Consequence: cancelling discards the parsed CompModule, so the next run re-parses (~1 s). That is fine — cancel follows a solve that was already taking minutes.

No omitempty on command_index

workerRequest.CommandIndex must serialize even when it is 0, because 0 is a real command index — the default one. With omitempty the field vanishes from the JSON, req.get("command_index") returns null on the Java side, and running the first command in any file dies with a bare NullPointerException from gson. This shipped undetected for a while: the startup path is exercised with -command 3 in testing, and only the browser's run button hits index 0.

The Java side now answers a missing required field with a protocol error frame instead of dereferencing it, so the next instance of this is legible. When testing command selection, test index 0 explicitly.

Never use Alloy's JSON output

--type json / A4Solution.toDTO() is silently wrong: it queries the raw kodkod instance, whose atom naming does not match Alloy's. On a three-line model it reports the wrong atom (A$2 for A$0) and an empty relation for a field constrained to be non-empty.

Always serialize with A4SolutionWriter.writeInstance — the path the GUI and --type xml use. This is why RunResult.instance_xml is XML and not a bespoke JSON schema.

execute_commandFromBook, not execute_command

Both exist and differ by one boolean passed to frame.solve. The fromBook variant is what the GUI and the CLI use.

skolemDepth = 1

A4Options defaults to 0, but the GUI defaults to 1 (A4Preferences.java:604). At depth 0 existential quantifiers produce no skolem relations, and the book's models — which pin instances with some disj d0, r : Dir … — would render without their witnesses.

The default theme is a yellow box, not a white ellipse

VizState.resetTheme() sets the default shape/colour to ELLIPSE/WHITE at lines 105 and 121, then overwrites both with BOX/YELLOW at lines 151-152, under a comment about meta-model defaults. The second write wins. The book's figures confirm it: an unthemed File sig renders as a yellow box.

Theme settings inherit down the sig hierarchy

<node color="Red"><type name="Object"/></node> colours Dir, File and Root, because they extend Object. VizState.MMap.resolve walks parents until it finds a setting. This is why Atom.TypeChain exists and why the theme lookups take a chain rather than a type name.

Singleton sigs render unnumbered

Root and Dir, but Entry0..Entry3. Alloy drops the index when the sig holds exactly one atom (StaticInstanceReader.java:319).

Watch the directory, not the file

Editors save by writing a temp file and renaming it over the target, which replaces the inode. A watch on the file follows the old inode and goes silent after the first save. Debounced 150 ms because one save emits several events.

slf4j is only silenced by a log file

-Dorg.slf4j.simpleLogger.logFile=/dev/null. Neither defaultLogLevel=off nor per-logger levels work — kodkod still emits six lines. Set in the nix wrapper.

The worker's stdout is captured before anything can redirect it

Worker.java grabs FileDescriptor.out and then points System.out at System.err. A stray println from Alloy in the middle of a frame would corrupt the stream irrecoverably; this makes it harmless log noise instead.

Worker generation counter

worker.gen exists to fix a real race: when a killed process's readLoop exits, a replacement may already be running. Without the generation check it would mark the new process dead and close its pending requests, so the first run after any cancel failed.

kill() is synchronous now, so it can no longer cause that overlap itself, but gen is still load-bearing: a JVM that dies on its own has nobody waiting for its readLoop, and a concurrent send() can respawn while it is still unwinding. Do not delete gen on the grounds that the kill path is ordered.

send() holds one lock across respawn and registration

send() keeps w.mu across both ensureStarted() (which bumps gen) and the w.pending registration. That single acquisition is what makes cancel and supersede safe: a request can never be registered against a generation that is about to change, so a departing readLoop either sees a mismatch and touches nothing, or finishes entirely before the new request exists. Splitting it into two acquisitions looks harmless and reintroduces the failure above. w.nextID survives respawns for the same reason — monotonic IDs mean a late frame from a dead process cannot alias a live request.

Cancelling waits for the process to die

kill() blocks until readLoop has reaped the process. Without the wait, a caller that kills and immediately sends can have ensureStarted spawn a replacement before SIGKILL lands, so two JVMs are briefly alive, each holding an open SAT solver; under a burst of saves that fans out. Waiting makes "at most one solver process" structural rather than a matter of timing.

The done channel is closed by readLoop last, after its teardown, so observing it closed means the loop is finished with the worker's state — not merely that the process exited. It is created only after a successful spawn, so a failed Start cannot leave a later kill() blocked forever.

Cancellation is one-shot, and stale updates are dropped

A job stays non-terminal for a moment after its solver is killed: its execute goroutine has to wake on the closed frame channel first. Two consequences, both of which were bugs:

• markCancelled() returns whether this call did the marking, and only the caller that gets true kills. Otherwise a second look at the same job concludes it is still running and kills again — hitting whichever process has since taken the worker's place. This is reachable on a save, where Reload cancels and then RunCommand looks again.
• publish() drops updates from a job that is no longer s.current. A superseded job records cancelled after its replacement may already have reported solving, and the SSE stream is last-write-wins, so publishing it leaves the browser reading "cancelled" during a live solve.

Reload cancels before it parses

The worker handles one op at a time, so a parse issued during a solve queues behind it — a save during a two-minute solve would otherwise block the reload for those two minutes. Since a save means the file changed, a solve still running is working on text that no longer exists, so cancelling it costs nothing. The re-parse this forces was already the price of any cancel.

If you ever add a go:embed here

default.nix passes ./foo.go paths straight to buildGo.program, which puts each file in its own store path. buildGo derives the embed directory from the first entry of srcs, so an embedded file would not be next to the source embedding it, and the build fails with "build system did not supply embed configuration". The fix is to assemble a real source directory with runCommandLocal first, as ../asciinema-server does. (This was needed for the varlink IDL; it went away with it.)

Building and testing

java is deliberately not in the dev shell (the JDK is large). For iteration, use the pinned store path:

JAVA=$(nix-build ~/kot/Profpatsch -A third_party.nixpkgs.openjdk21 --no-out-link)
JAR=$(nix-build ~/kot/Profpatsch -A third_party.nixpkgs.alloy6 --no-out-link)/share/alloy/alloy6.jar

$JAVA/bin/javac -cp $JAR -d ./tmp/classes java/src/de/profpatsch/alloy/Worker.java

The Go tests need no Java: they run against testdata/, which holds real solver output for filesystem.als command 3 plus that model's theme.

go test ./users/Profpatsch/alloy-viz/
nix build ~/kot/Profpatsch#alloy-viz

Verifying against the book

The corpus is a golden-output suite: many models pin an exact instance, and each corresponds to a screenshot in practicalalloy.github.io/_images/. Render and compare by eye.

Careful: IMPL.md claims filesystem.als corresponds to instance8.png. It does not — that image is the filesharing model. The right one is instance83.png, found by searching the chapter HTML for _images/.

Useful models:

Note that several commands in instance_19/leaderelection.als fail with "You must specify a scope for sig this/Message". That is the model's own doing — stock alloy6 exec reports the identical error at the identical line. Use command 2 for a quick satisfiable run.

Not implemented (slice 2+)

Instance enumeration (fork(-3/-1/-2/0/state+1)), the evaluator, trace stepping for temporal models, projection, unsat cores, magic layout.

Enumeration and evaluation need the live A4Solution, which cannot cross a process boundary — so they must be new ops on the worker that holds it, and the worker then becomes a session with a lifetime, needing explicit release and idle eviction (a live A4Solution pins an open SAT solver).