alloy-viz

View Alloy instances in a browser, without the Alloy GUI.

Point it at a .als file; it solves the selected command, renders the instance as a graph, and re-solves whenever you save. You keep editing in your own editor — the browser is a viewer.

nix run ~/kot/Profpatsch#alloy-viz -- model.als

Then open http://127.0.0.1:8791.

See man alloy-viz for the full reference (flags, and why solving happens in a separate process).

What it does

Watches the model. Saving re-solves and re-renders. Editing a sibling <model>.thm theme re-renders too.
Runs one command at a time. The command picker lists every run/check in the file; only the selected one is solved. Running all of them is what makes alloy exec slow.
Never blocks. Solve times range from 0.1 s to several minutes, so runs are asynchronous, with live progress (variables, clauses, elapsed time) and a Cancel button.
Applies the theme. Node visibility, colour and shape, and relations shown as attributes rather than arrows, are honoured — enough to reproduce the figures in Practical Alloy.

Building and installing

nix build ~/kot/Profpatsch#alloy-viz

# Or install it, to get `alloy-viz` and `man alloy-viz` on PATH
nix profile install ~/kot/Profpatsch#alloy-viz

There is no daemon to install: alloy-viz runs for as long as you are looking at a model, and exits with Ctrl-C.

How it is put together

browser ──HTTP+SSE──> alloy-viz (Go) ──NUL-JSON on stdin/stdout──> alloy-viz-solver (Java)
                        · watches the file                           · one warm JVM
                        · owns the job, kills to cancel              · parse + solve
                        · XML → graph → DOT → `dot -Tsvg`            · Alloy's own instance XML

The Java process is a dumb worker behind the Go one. It is kept warm between runs, so a re-solve after a save skips the JVM start and the parse — measured at 152 ms warm against 566 ms cold for the same command.

One model per process: alloy-viz views the file you name and nothing else, so watching a second model means running a second one on another port.

Cancelling kills the worker, because that is the only thing that stops a solve: SAT4J ignores Thread.interrupt() entirely. The next run transparently re-parses (~1 s).

Implementation notes, verified facts and traps are in CLAUDE.md; the original research and design rationale are in IMPL.md.

Status

Slice 1. Renders the first state of a solution.

Not implemented: instance enumeration (New Solution), the evaluator, trace stepping for temporal models, projection, and magic layout.