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
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
|
package main
// Minimal support for Alloy's .thm theme files.
//
// Slice 1 honours only the four settings that visibly change the book figures:
// node `visible`, node `color`, node `shape`, and edge `attribute` (fold a
// relation into its source node's label instead of drawing an arrow), plus the
// view-level `hideSkolem`. Everything else in the format -- palettes, per-atom
// overrides, projection, magic layout, font size, weights -- is ignored.
//
// Format (verified against practicalalloy-models/**/*.thm):
//
// <alloy><view nodetheme=".." edgetheme=".." hideSkolem="yes">
// <node color="Gray"><type name="Entry"/></node>
// <node shape="House"><type name="Root"/></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></alloy>
//
// A <node>/<edge> element with no child selector sets the default for all types.
import (
"encoding/xml"
"os"
"strings"
)
type xmlThemeFile struct {
XMLName xml.Name `xml:"alloy"`
View xmlView `xml:"view"`
}
type xmlView struct {
HideSkolem string `xml:"hideSkolem,attr"`
HidePrivate string `xml:"hidePrivate,attr"`
Nodes []xmlNodeT `xml:"node"`
Edges []xmlEdgeT `xml:"edge"`
}
type xmlNodeT struct {
Visible string `xml:"visible,attr"`
Color string `xml:"color,attr"`
Shape string `xml:"shape,attr"`
Types []xmlNameRef `xml:"type"`
Sets []xmlNameRef `xml:"set"`
}
type xmlEdgeT struct {
Visible string `xml:"visible,attr"`
Attribute string `xml:"attribute,attr"`
Color string `xml:"color,attr"`
Relations []xmlNameRef `xml:"relation"`
}
type xmlNameRef struct {
Name string `xml:"name,attr"`
}
// Theme holds the subset of theme settings we apply.
type Theme struct {
HideSkolem bool
// Per-type node settings. Absent key means "use the default".
NodeVisible map[string]bool
NodeColor map[string]string // graphviz color name
NodeShape map[string]string // graphviz shape name
// Per-relation edge settings.
EdgeVisible map[string]bool
EdgeAttribute map[string]bool
DefaultNodeVisible bool
DefaultNodeColor string
DefaultNodeShape string
}
// DefaultTheme mirrors VizState.resetTheme(): yellow boxes, everything visible,
// nothing folded into labels.
//
// The yellow box is not a guess. resetTheme first sets the null (= default) key
// to ELLIPSE/WHITE (VizState.java:105,121), then unconditionally overwrites it
// with BOX/YELLOW thirty lines later (VizState.java:151-152) under a comment
// about meta-model defaults. The second write wins, which is why the book's
// figures show unthemed sigs as yellow boxes.
func DefaultTheme() *Theme {
return &Theme{
NodeVisible: map[string]bool{},
NodeColor: map[string]string{},
NodeShape: map[string]string{},
EdgeVisible: map[string]bool{},
EdgeAttribute: map[string]bool{},
DefaultNodeVisible: true,
DefaultNodeColor: "gold",
DefaultNodeShape: "box",
}
}
// themeColors maps Alloy's DotColor display names to graphviz colors, taking the
// first (CLASSIC palette) entry of each DotColor enum constant.
var themeColors = map[string]string{
"Yellow": "gold",
"Green": "limegreen",
"Blue": "cornflowerblue",
"Red": "palevioletred",
"Gray": "lightgray",
"White": "white",
"Black": "black",
// "Magic" means "auto-assign from the palette"; we render it as the default.
"Magic": "",
}
// themeShapes maps Alloy's DotShape display names to graphviz shape names,
// transcribed from edu.mit.csail.sdg.alloy4graph.DotShape.
var themeShapes = map[string]string{
"Ellipse": "ellipse",
"Box": "box",
"Circle": "circle",
"Egg": "egg",
"Triangle": "triangle",
"Diamond": "diamond",
"Trapezoid": "trapezium",
"Parallelogram": "parallelogram",
"House": "house",
"Hexagon": "hexagon",
"Octagon": "octagon",
"Dbl Circle": "doublecircle",
"Dbl Octagon": "doubleoctagon",
"Tpl Octagon": "tripleoctagon",
"Inv Triangle": "invtriangle",
"Inv House": "invhouse",
"Inv Trapezoid": "invtrapezium",
"Lined Diamond": "Mdiamond",
"Lined Square": "Msquare",
"Lined Circle": "Mcircle",
}
// LoadTheme reads a .thm file. A missing file is not an error: it just means the
// model has no theme and the defaults apply.
func LoadTheme(path string) (*Theme, error) {
t := DefaultTheme()
data, err := os.ReadFile(path)
if err != nil {
if os.IsNotExist(err) {
return t, nil
}
return t, err
}
var f xmlThemeFile
if err := xml.Unmarshal(data, &f); err != nil {
return t, err
}
t.HideSkolem = f.View.HideSkolem == "yes"
for _, n := range f.View.Nodes {
// No selector => this element sets the defaults.
if len(n.Types) == 0 && len(n.Sets) == 0 {
if n.Visible != "" {
t.DefaultNodeVisible = n.Visible == "yes"
}
if c, ok := themeColors[n.Color]; ok && c != "" {
t.DefaultNodeColor = c
}
if s, ok := themeShapes[n.Shape]; ok {
t.DefaultNodeShape = s
}
continue
}
for _, ref := range n.Types {
name := sigDisplayName(ref.Name)
if n.Visible != "" {
t.NodeVisible[name] = n.Visible == "yes"
}
if c, ok := themeColors[n.Color]; ok && c != "" {
t.NodeColor[name] = c
}
if s, ok := themeShapes[n.Shape]; ok {
t.NodeShape[name] = s
}
}
}
for _, e := range f.View.Edges {
for _, ref := range e.Relations {
name := relationRefName(ref.Name)
if e.Visible != "" {
t.EdgeVisible[name] = e.Visible == "yes"
}
if e.Attribute != "" {
t.EdgeAttribute[name] = e.Attribute == "yes"
}
}
}
return t, nil
}
// relationRefName normalizes a theme relation reference. Themes may write either
// a bare field name ("object") or a qualified one ("this/Entry<:object").
func relationRefName(s string) string {
if i := strings.LastIndex(s, "<:"); i >= 0 {
s = s[i+2:]
}
if i := strings.LastIndex(s, "/"); i >= 0 {
s = s[i+1:]
}
return s
}
// Node settings resolve along the sig hierarchy: the most specific sig with an
// explicit setting wins, otherwise the setting is inherited from an ancestor,
// otherwise the theme default applies. This mirrors VizState.MMap.resolve, and
// is why `<node color="Red"><type name="Object"/></node>` colours every sig that
// extends Object. `chain` is the atom's type followed by its ancestors.
// nodeVisible reports whether atoms of a type should be drawn.
func (t *Theme) nodeVisible(chain []string) bool {
for _, typ := range chain {
if v, ok := t.NodeVisible[typ]; ok {
return v
}
}
return t.DefaultNodeVisible
}
func (t *Theme) nodeColor(chain []string) string {
for _, typ := range chain {
if c, ok := t.NodeColor[typ]; ok {
return c
}
}
return t.DefaultNodeColor
}
func (t *Theme) nodeShape(chain []string) string {
for _, typ := range chain {
if s, ok := t.NodeShape[typ]; ok {
return s
}
}
return t.DefaultNodeShape
}
// edgeVisible reports whether a relation should be drawn as arrows.
func (t *Theme) edgeVisible(rel string) bool {
if v, ok := t.EdgeVisible[rel]; ok {
return v
}
return true
}
// edgeAttribute reports whether a relation should be folded into the source
// node's label instead of drawn.
func (t *Theme) edgeAttribute(rel string) bool {
return t.EdgeAttribute[rel]
}
|