Profpatsch/users/Profpatsch/alloy-viz

View full contents ↓

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).

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.

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.

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.

alloy-viz(1)

alloy-viz - view Alloy instances in a browser

alloy-viz [-addr host:port] [-command index] [-no-run] <model.als>

alloy-viz solves a command from an Alloy model and renders the resulting instance as a graph in a browser, re-solving every time the file is saved. It replaces driving the Alloy Analyzer's Swing GUI by hand.

The browser is a viewer, not an editor: you keep editing the .als file in your own editor. alloy-viz watches it and pushes each new instance over server-sent events.

Only the selected command is run. Running every command in a file is what makes alloy6(1)'s exec slow – five commands in the shipped ceilingsAndFloors.als take about 15 seconds – and while editing it is almost never wanted.

If a theme file exists beside the model, named after it with a .thm extension, it is applied. Editing the theme also triggers a re-render.

-addr host:port

Address for the web UI. Default 127.0.0.1:8791.

-command index

Index of the command to run at startup, counting run and check commands from 0 in declaration order. Default 0.

-no-run

Do not solve at startup; wait for a command to be selected. Useful when the default command is a slow one.

alloy-viz is a supervisor; the solving happens in alloy-viz-solver, a Java process holding a warm JVM and the parsed model. It is kept alive between runs, so repeated runs skip both the JVM start and the parse. The saving is substantial: a solve that takes 566 ms on a cold worker takes about 150 ms on a warm one.

One model is viewed per process; to watch a second file, run a second alloy-viz on another port.

Solving runs in that separate process because it is the only way to stop it. A running SAT4J solve ignores Thread.interrupt() entirely – kodkod's SAT4J wrapper calls isSatisfiable() with no interrupt polling – so there is no in-process cancellation path. The Alloy GUI has the same constraint and solves it the same way.

Cancelling therefore kills the process, which also discards the parsed model; the next run re-parses it, costing under a second. This is a good trade for a solve that was taking long enough to be worth cancelling, and solve times vary enormously: a small structural model solves in a tenth of a second, while protocol-design/instance_19 takes over two minutes. Nothing in the UI ever blocks on a solve.

ALLOY_VIZ_SOLVER

Path to the alloy-viz-solver binary. The nix wrapper sets this; otherwise the binary is looked up on PATH.

View a model, running its first command:

$ alloy-viz filesystem.als

Start on a specific command, chosen from the list:

$ alloy-viz -command 3 filesystem.als

Open a model with a slow default command without solving it first:

$ alloy-viz -no-run leaderelection.als

dot(1)

The instance XML that alloy-viz renders is Alloy's own format, documented in edu/mit/csail/sdg/translator/instance.txt in the Alloy sources.

Profpatsch

Only the first state of a temporal (Electrum) trace is rendered. Stepping through a trace, enumerating further instances, and the evaluator are not implemented.

Theme support is partial: node visibility, colour and shape, and whether a relation is folded into node labels, are honoured. Projection, magic layout and per-atom overrides are not.