1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
|
.Dd August 3, 2026
.Dt ALLOY-VIZ 1
.Os
.Sh NAME
.Nm alloy-viz
.Nd view Alloy instances in a browser
.Sh SYNOPSIS
.Nm
.Op Fl addr Ar host:port
.Op Fl command Ar index
.Op Fl no-run
.Aq Pa model.als
.Sh DESCRIPTION
.Nm
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.
.Pp
The browser is a viewer, not an editor: you keep editing the
.Pa .als
file in your own editor.
.Nm
watches it and pushes each new instance over server-sent events.
.Pp
Only the
.Em selected
command is run.
Running every command in a file is what makes
.Xr alloy6 1 Ns 's
.Cm exec
slow \(en five commands in the shipped
.Pa ceilingsAndFloors.als
take about 15 seconds \(en and while editing it is almost never wanted.
.Pp
If a theme file exists beside the model, named after it with a
.Pa .thm
extension, it is applied.
Editing the theme also triggers a re-render.
.Ss Options
.Bl -tag -width Ds
.It Fl addr Ar host:port
Address for the web UI.
Default
.Ar 127.0.0.1:8791 .
.It Fl command Ar index
Index of the command to run at startup, counting
.Ic run
and
.Ic check
commands from 0 in declaration order.
Default 0.
.It Fl no-run
Do not solve at startup; wait for a command to be selected.
Useful when the default command is a slow one.
.El
.Sh ARCHITECTURE
.Nm
is a supervisor; the solving happens in
.Nm 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.
.Pp
One model is viewed per process; to watch a second file, run a second
.Nm
on another port.
.Pp
Solving runs in that separate process because it is the only way to stop it.
A running SAT4J solve ignores
.Fn Thread.interrupt
entirely \(en kodkod's SAT4J wrapper calls
.Fn isSatisfiable
with no interrupt polling \(en so there is no in-process cancellation path.
The Alloy GUI has the same constraint and solves it the same way.
.Pp
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
.Pa protocol-design/instance_19
takes over two minutes.
Nothing in the UI ever blocks on a solve.
.Sh ENVIRONMENT
.Bl -tag -width Ds
.It Ev ALLOY_VIZ_SOLVER
Path to the
.Nm alloy-viz-solver
binary.
The nix wrapper sets this; otherwise the binary is looked up on
.Ev PATH .
.El
.Sh EXAMPLES
View a model, running its first command:
.Pp
.Dl $ alloy-viz filesystem.als
.Pp
Start on a specific command, chosen from the list:
.Pp
.Dl $ alloy-viz -command 3 filesystem.als
.Pp
Open a model with a slow default command without solving it first:
.Pp
.Dl $ alloy-viz -no-run leaderelection.als
.Sh SEE ALSO
.Xr dot 1
.Pp
The instance XML that
.Nm
renders is Alloy's own format, documented in
.Pa edu/mit/csail/sdg/translator/instance.txt
in the Alloy sources.
.Sh AUTHORS
.An Profpatsch
.Sh CAVEATS
Only the first state of a temporal (Electrum) trace is rendered.
Stepping through a trace, enumerating further instances, and the evaluator are
not implemented.
.Pp
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.
|