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
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
|
package main
// Parsing of Alloy's instance XML into a graph model.
//
// The XML produced by A4SolutionWriter is the only trustworthy serialization of
// a solution. (The CLI's `--type json` / A4Solution.toDTO() path queries the raw
// kodkod instance, whose atom naming does not match Alloy's; it emits wrong atom
// names, drops sig-hierarchy atoms, invents phantom ones, and returns empty
// relations for non-empty fields. Never use it.)
//
// Format, from edu/mit/csail/sdg/translator/instance.txt:
//
// <alloy builddate="..">
// <instance bitwidth=".." maxseq=".." command=".." tracelength=".." looplength="..">
// <sig ID=".." parentID=".." label=".." builtin/one/lone/some/abstract/private/meta="yes">
// <atom label=".."/>*
// </sig>*
// <field ID=".." parentID=".." label=".." var="yes"> <tuple><atom label=".."/>+</tuple>* <types>..</types> </field>*
// <skolem ID=".." label=".."> <tuple>..</tuple>* <types>..</types> </skolem>*
// </instance>*
// </alloy>
//
// Verified against real output: each atom is listed under its *most specific*
// sig only (Root$0 appears under this/Root, not also under this/Dir), so no
// hierarchy flattening is needed to assign an atom its type.
//
// A temporal solution contains one <instance> element per state of the trace.
import (
"encoding/xml"
"fmt"
"strings"
)
// ── XML shapes ─────────────────────────────────────────────────────────────
type xmlAlloy struct {
XMLName xml.Name `xml:"alloy"`
Instances []xmlInstance `xml:"instance"`
}
type xmlInstance struct {
Bitwidth int `xml:"bitwidth,attr"`
MaxSeq int `xml:"maxseq,attr"`
Command string `xml:"command,attr"`
TraceLength int `xml:"tracelength,attr"`
LoopLength int `xml:"looplength,attr"`
Sigs []xmlSig `xml:"sig"`
Fields []xmlField `xml:"field"`
Skolems []xmlSkolem `xml:"skolem"`
}
type xmlSig struct {
ID string `xml:"ID,attr"`
ParentID string `xml:"parentID,attr"`
Label string `xml:"label,attr"`
Builtin string `xml:"builtin,attr"`
One string `xml:"one,attr"`
Abstract string `xml:"abstract,attr"`
Private string `xml:"private,attr"`
Meta string `xml:"meta,attr"`
Var string `xml:"var,attr"`
Atoms []xmlAtom `xml:"atom"`
Types []xmlType `xml:"type"` // subset sigs only
}
type xmlField struct {
ID string `xml:"ID,attr"`
ParentID string `xml:"parentID,attr"`
Label string `xml:"label,attr"`
Private string `xml:"private,attr"`
Meta string `xml:"meta,attr"`
Var string `xml:"var,attr"`
Tuples []xmlTuple `xml:"tuple"`
Types xmlTypes `xml:"types"`
}
type xmlSkolem struct {
ID string `xml:"ID,attr"`
Label string `xml:"label,attr"`
Tuples []xmlTuple `xml:"tuple"`
Types xmlTypes `xml:"types"`
}
type xmlTuple struct {
Atoms []xmlAtom `xml:"atom"`
}
type xmlAtom struct {
Label string `xml:"label,attr"`
}
type xmlTypes struct {
Types []xmlType `xml:"type"`
}
type xmlType struct {
ID string `xml:"ID,attr"`
}
func isYes(s string) bool { return s == "yes" }
// ── graph model ────────────────────────────────────────────────────────────
// Atom is one node candidate: an element of the universe.
type Atom struct {
Name string // raw label, e.g. "Dir$0"
Type string // owning sig's display label, e.g. "Dir"
// TypeChain is Type followed by its ancestor sigs, nearest first. Theme
// settings inherit down the sig hierarchy (VizState.MMap.resolve walks
// parents), so `<node color="Red"><type name="Object"/></node>` must also
// colour Dir, File and Root, which extend Object.
TypeChain []string
// Index is the N in "Dir$N", or -1 when the atom is rendered without a
// number. Alloy omits the number when the atom is the *only* one of its
// sig (StaticInstanceReader.java:319), which is why the book figures show
// "Root" and "Dir" but "Entry0".."Entry3".
Index int
// Sets are subset-sig memberships shown as "(...)" annotations.
Sets []string
// SkolemSets are memberships arising from skolemization (the existential
// witnesses "$cmd_d0"). Kept apart from Sets so `hideSkolem` can drop them.
SkolemSets []string
// Attrs are relation values folded into the node label by `attribute="yes"`,
// one entry per relation, e.g. "name: Name0, Name1".
Attrs []string
}
// Relation is one field or skolem relation, arity >= 2.
type Relation struct {
Name string
Tuples [][]string // each tuple is a list of atom labels, len == arity
IsSkolem bool
Arity int
}
// Instance is one state of a solution, ready for rendering.
type Instance struct {
Command string
Bitwidth int
TraceLength int
LoopLength int
Atoms []*Atom
Relations []*Relation
// AtomByName indexes Atoms for edge endpoint lookup.
AtomByName map[string]*Atom
}
// builtinSigs are never drawn: they are the ambient universe, not model content.
// (Int/seq/Int are additionally hideUnconnected by default in the Alloy theme.)
var builtinSigs = map[string]bool{
"univ": true, "Int": true, "seq/Int": true, "String": true, "none": true,
}
// sigDisplayName strips Alloy's module qualification. Sig labels are written as
// "this/Dir" for the top-level module and "util/ordering/Ord" for imports; the
// GUI displays only the final segment.
func sigDisplayName(label string) string {
if i := strings.LastIndex(label, "/"); i >= 0 {
return label[i+1:]
}
return label
}
// atomIndex splits "Dir$0" into ("Dir", 0). Returns index -1 when there is no
// "$N" suffix, which happens for singleton sigs Alloy chose not to number.
func atomIndex(label string) (string, int) {
i := strings.LastIndex(label, "$")
if i < 0 {
return label, -1
}
n := 0
for _, c := range label[i+1:] {
if c < '0' || c > '9' {
return label, -1
}
n = n*10 + int(c-'0')
}
return label[:i], n
}
// ParseInstances decodes the full XML document into one Instance per trace state.
func ParseInstances(data string) ([]*Instance, error) {
var doc xmlAlloy
if err := xml.Unmarshal([]byte(data), &doc); err != nil {
return nil, fmt.Errorf("parse instance xml: %w", err)
}
if len(doc.Instances) == 0 {
return nil, fmt.Errorf("instance xml contains no <instance> element")
}
out := make([]*Instance, 0, len(doc.Instances))
for i := range doc.Instances {
out = append(out, buildInstance(&doc.Instances[i]))
}
return out, nil
}
func buildInstance(xi *xmlInstance) *Instance {
inst := &Instance{
Command: xi.Command,
Bitwidth: xi.Bitwidth,
TraceLength: xi.TraceLength,
LoopLength: xi.LoopLength,
AtomByName: make(map[string]*Atom),
}
// sigByID lets us walk the sig hierarchy for theme inheritance.
sigByID := make(map[string]*xmlSig, len(xi.Sigs))
for i := range xi.Sigs {
sigByID[xi.Sigs[i].ID] = &xi.Sigs[i]
}
// typeChain returns a sig's display name followed by its ancestors'.
typeChain := func(s *xmlSig) []string {
var chain []string
seen := map[string]bool{}
for cur := s; cur != nil && !seen[cur.ID]; cur = sigByID[cur.ParentID] {
seen[cur.ID] = true
name := sigDisplayName(cur.Label)
if builtinSigs[name] {
break
}
chain = append(chain, name)
}
return chain
}
// Atoms. Each atom is listed exactly once, under its most specific sig.
for i := range xi.Sigs {
s := &xi.Sigs[i]
name := sigDisplayName(s.Label)
if isYes(s.Builtin) || builtinSigs[name] {
continue
}
// Subset sigs (which carry <type> children) are memberships, not
// owners: their atoms already belong to a primitive sig.
if len(s.Types) > 0 {
for _, a := range s.Atoms {
if at, ok := inst.AtomByName[a.Label]; ok {
at.Sets = append(at.Sets, name)
}
}
continue
}
chain := typeChain(s)
// A sig holding exactly one atom is displayed without its index, so a
// "one sig Root" renders as "Root" rather than "Root0".
singleton := len(s.Atoms) == 1
for _, a := range s.Atoms {
idx := -1
if !singleton {
_, idx = atomIndex(a.Label)
}
at := &Atom{Name: a.Label, Type: name, TypeChain: chain, Index: idx}
inst.Atoms = append(inst.Atoms, at)
inst.AtomByName[a.Label] = at
}
}
// Fields become relations. Arity is read from the widest tuple rather than
// the <types> element, so a malformed types list cannot desync us.
for i := range xi.Fields {
f := &xi.Fields[i]
if isYes(f.Private) || isYes(f.Meta) {
continue
}
rel := &Relation{Name: f.Label}
for _, t := range f.Tuples {
tuple := make([]string, 0, len(t.Atoms))
for _, a := range t.Atoms {
tuple = append(tuple, a.Label)
}
if len(tuple) > rel.Arity {
rel.Arity = len(tuple)
}
rel.Tuples = append(rel.Tuples, tuple)
}
if len(rel.Tuples) > 0 {
inst.Relations = append(inst.Relations, rel)
}
}
// Skolems. Arity-1 skolems name a specific atom ("$inst_08_d0" means "the
// atom the existential picked"), and the GUI shows them as a set membership
// label on that atom rather than as a node. Higher-arity skolems are drawn
// as relations.
for i := range xi.Skolems {
sk := &xi.Skolems[i]
name := skolemDisplayName(sk.Label)
arity := 0
for _, t := range sk.Tuples {
if len(t.Atoms) > arity {
arity = len(t.Atoms)
}
}
if arity == 1 {
for _, t := range sk.Tuples {
if len(t.Atoms) == 1 {
if at, ok := inst.AtomByName[t.Atoms[0].Label]; ok {
at.SkolemSets = append(at.SkolemSets, name)
}
}
}
continue
}
rel := &Relation{Name: name, IsSkolem: true, Arity: arity}
for _, t := range sk.Tuples {
tuple := make([]string, 0, len(t.Atoms))
for _, a := range t.Atoms {
tuple = append(tuple, a.Label)
}
rel.Tuples = append(rel.Tuples, tuple)
}
if len(rel.Tuples) > 0 {
inst.Relations = append(inst.Relations, rel)
}
}
return inst
}
// skolemDisplayName turns "$structural_modeling_instance_08_d0" into "d0".
//
// Alloy names a skolem "$<command label>_<variable>", so stripping the leading
// '$' and the command-label prefix leaves the variable the user actually wrote.
// The command label is not available here, so we take the final underscore
// segment, which is what the GUI effectively displays for book models.
func skolemDisplayName(label string) string {
s := strings.TrimPrefix(label, "$")
if i := strings.LastIndex(s, "_"); i >= 0 && i+1 < len(s) {
return s[i+1:]
}
return s
}
// Label is the atom's display name, matching AlloyAtom.getVizName with the
// default theme (number=true): type name followed by the atom's index.
func (a *Atom) Label() string {
if a.Index < 0 {
return a.Type
}
return fmt.Sprintf("%s%d", a.Type, a.Index)
}
// FullLabel is the node label including set memberships and attributes, e.g.
// "Entry0 (d0)" or "Entry0\nname: Name".
//
// hideSkolem drops the skolem witness annotations, which is what the book's
// themes ask for; ordinary subset-sig memberships are always shown.
func (a *Atom) FullLabel(hideSkolem bool) string {
label := a.Label()
sets := a.Sets
if !hideSkolem {
sets = append(append([]string(nil), sets...), a.SkolemSets...)
}
if len(sets) > 0 {
label += " (" + strings.Join(sets, ", ") + ")"
}
for _, at := range a.Attrs {
label += "\n" + at
}
return label
}
|