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
|
package main
import (
"os"
"strings"
"testing"
)
// The fixtures are real solver output: testdata/filesystem_instance_08.xml is
// what alloy-viz-solver emits for command 3 of
// practicalalloy-models/structural-modeling/instance_07_08/filesystem.als, and
// the .thm is that model's theme, verbatim.
//
// That command pins an exact instance ("some disj d0, r : Dir, ..."), so the
// expected rendering is deterministic and can be compared against the book's own
// screenshot of it (practicalalloy.github.io/_images/instance83.png).
func loadFixture(t *testing.T) (*Instance, *Theme) {
t.Helper()
data, err := os.ReadFile("testdata/filesystem_instance_08.xml")
if err != nil {
t.Fatal(err)
}
insts, err := ParseInstances(string(data))
if err != nil {
t.Fatal(err)
}
if len(insts) != 1 {
t.Fatalf("expected 1 instance (non-temporal model), got %d", len(insts))
}
thm, err := LoadTheme("testdata/filesystem.thm")
if err != nil {
t.Fatal(err)
}
return insts[0], thm
}
func TestParseInstanceAtoms(t *testing.T) {
inst, _ := loadFixture(t)
// Builtins (univ, Int, seq/Int, String) must not become atoms.
if len(inst.Atoms) != 8 {
t.Errorf("expected 8 atoms (Root, Dir, File, 4x Entry, Name), got %d", len(inst.Atoms))
}
byName := inst.AtomByName
// Each atom is listed under its most specific sig: Root$0 belongs to Root,
// not to Dir, even though Root extends Dir.
if got := byName["Root$0"].Type; got != "Root" {
t.Errorf("Root$0 type = %q, want Root", got)
}
// The sig hierarchy is recorded for theme inheritance.
if got := strings.Join(byName["Root$0"].TypeChain, ","); got != "Root,Dir,Object" {
t.Errorf("Root$0 chain = %q, want Root,Dir,Object", got)
}
// A sig with exactly one atom renders unnumbered; a sig with several does
// not. This is why the book shows "Root" and "Dir" but "Entry0".."Entry3".
if got := byName["Root$0"].Label(); got != "Root" {
t.Errorf("singleton sig label = %q, want Root", got)
}
if got := byName["Entry$2"].Label(); got != "Entry2" {
t.Errorf("multi-atom sig label = %q, want Entry2", got)
}
}
func TestParseInstanceSkolems(t *testing.T) {
inst, _ := loadFixture(t)
// Arity-1 skolems name an atom the existential picked; they annotate that
// atom rather than becoming nodes, and are kept separate from ordinary
// subset-sig membership so hideSkolem can drop them.
a := inst.AtomByName["Dir$0"]
if len(a.SkolemSets) != 1 || a.SkolemSets[0] != "d0" {
t.Errorf("Dir$0 skolem sets = %v, want [d0]", a.SkolemSets)
}
if len(a.Sets) != 0 {
t.Errorf("Dir$0 should have no non-skolem sets, got %v", a.Sets)
}
if got := a.FullLabel(true); got != "Dir" {
t.Errorf("label with hideSkolem = %q, want Dir", got)
}
if got := a.FullLabel(false); got != "Dir (d0)" {
t.Errorf("label without hideSkolem = %q, want Dir (d0)", got)
}
}
func TestLoadTheme(t *testing.T) {
_, thm := loadFixture(t)
if !thm.HideSkolem {
t.Error("hideSkolem should be true")
}
// Alloy display names map to graphviz names.
if got := thm.NodeShape["Root"]; got != "house" {
t.Errorf("Root shape = %q, want house", got)
}
if got := thm.NodeShape["Dir"]; got != "trapezium" {
t.Errorf("Dir shape = %q (Alloy 'Trapezoid'), want trapezium", got)
}
if got := thm.NodeColor["Object"]; got != "palevioletred" {
t.Errorf("Object color = %q (Alloy 'Red'), want palevioletred", got)
}
if thm.NodeVisible["Name"] {
t.Error("Name should be hidden")
}
if !thm.EdgeAttribute["name"] {
t.Error("name should be an attribute relation")
}
if thm.EdgeAttribute["object"] {
t.Error("object is attribute=\"no\" and must stay an edge")
}
}
func TestThemeInheritance(t *testing.T) {
_, thm := loadFixture(t)
// The theme colours "Object"; Dir/File/Root extend it and must inherit,
// exactly as VizState.MMap.resolve walks the sig hierarchy.
for _, chain := range [][]string{
{"Dir", "Object"},
{"File", "Object"},
{"Root", "Dir", "Object"},
} {
if got := thm.nodeColor(chain); got != "palevioletred" {
t.Errorf("nodeColor(%v) = %q, want inherited palevioletred", chain, got)
}
}
// An explicit setting on the specific sig beats the inherited one.
if got := thm.nodeColor([]string{"Entry"}); got != "lightgray" {
t.Errorf("Entry color = %q, want lightgray", got)
}
// Shape is set on Root itself, so it wins over Dir's trapezium.
if got := thm.nodeShape([]string{"Root", "Dir", "Object"}); got != "house" {
t.Errorf("Root shape = %q, want house", got)
}
}
func TestRenderDOT(t *testing.T) {
inst, thm := loadFixture(t)
dot := RenderDOT(inst, thm)
mustContain := []string{
// Singleton unnumbered, inherited colour, own shape.
`"Root$0" [label="Root", shape=house, fillcolor="palevioletred"]`,
`"Dir$0" [label="Dir", shape=trapezium, fillcolor="palevioletred"]`,
`"File$0" [label="File", shape=box, fillcolor="palevioletred"]`,
// Numbered, own colour, and the `name` relation folded into the label
// rather than drawn as an edge.
`"Entry$0" [label="Entry0\nname: Name", shape=box, fillcolor="lightgray"]`,
// attribute="no" keeps `object` as a real edge.
`"Entry$0" -> "Dir$0" [label="object"`,
`"Root$0" -> "Entry$1" [label="entries"`,
}
for _, want := range mustContain {
if !strings.Contains(dot, want) {
t.Errorf("DOT missing:\n %s\ngot:\n%s", want, dot)
}
}
// Name is visible="no": no node, and no edges into it.
if strings.Contains(dot, `"Name$0" [`) {
t.Error("Name$0 should not be drawn (theme sets visible=no)")
}
if strings.Contains(dot, `-> "Name$0"`) {
t.Error("no edge should point at the hidden Name$0")
}
// hideSkolem is on, so the witness annotations must not appear.
if strings.Contains(dot, "(d0)") || strings.Contains(dot, "(e0)") {
t.Error("skolem annotations should be hidden")
}
// Distinct relations get distinct colours, as the GUI's MAGIC palette does.
if strings.Contains(dot, `[label="entries", color="#a65628"`) {
t.Error("entries and object must not share a palette colour")
}
}
func TestRenderDOTNoTheme(t *testing.T) {
inst, _ := loadFixture(t)
dot := RenderDOT(inst, DefaultTheme())
// Without a theme everything is a white ellipse and nothing is hidden,
// matching VizState.resetTheme's defaults.
if !strings.Contains(dot, `"Name$0" [label="Name (n0)", shape=box, fillcolor="gold"]`) {
t.Errorf("default theme should show Name with its skolem label; got:\n%s", dot)
}
// `name` is only an attribute because the theme says so; by default it is
// an ordinary edge.
if !strings.Contains(dot, `-> "Name$0" [label="name"`) {
t.Error("name should be a drawn edge under the default theme")
}
}
func TestDotStringEscaping(t *testing.T) {
// Atom labels contain '$', and DOT treats \n as a line break, so both the
// quoting and the escaping have to be right or graphviz fails to parse.
cases := map[string]string{
`Dir$0`: `"Dir$0"`,
"a\nb": `"a\nb"`,
`say "hi"`: `"say \"hi\""`,
`back\slash`: `"back\\slash"`,
}
for in, want := range cases {
if got := dotString(in); got != want {
t.Errorf("dotString(%q) = %s, want %s", in, got, want)
}
}
}
func TestSkolemDisplayName(t *testing.T) {
// Alloy names skolems "$<command label>_<variable>"; the UI shows the
// variable the user actually wrote.
if got := skolemDisplayName("$structural_modeling_instance_08_d0"); got != "d0" {
t.Errorf("got %q, want d0", got)
}
}
func TestSigDisplayName(t *testing.T) {
if got := sigDisplayName("this/Dir"); got != "Dir" {
t.Errorf("got %q, want Dir", got)
}
if got := sigDisplayName("util/ordering/Ord"); got != "Ord" {
t.Errorf("got %q, want Ord", got)
}
}
|