-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathmulti-relation-composition.page
98 lines (80 loc) · 2 KB
/
multi-relation-composition.page
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
---
title: Example of composing of a multi-set with a multi-relation
...
A span from Bundle to Item.
```clafer
abstract Bundle
contains ->> Item +
```
Two bundles.
```clafer
B1 : Bundle
[ contains in Bread ]
[ #contains = 2 ]
B2 : Bundle
[ contains = Milk, Butter ]
```
And three items.
```clafer
abstract Item
Bread : Item
Butter : Item
Milk : Item
```
A family of bundles
```clafer
abstract bundles ->> Bundle
bundlesIB1 : bundles ->> B1 2
bundlesIB2 : bundles ->> B2
```
A family to represent the result of the composition `bundles ; contains`.
```clafer
allItem ->> Item 6..*
[alloy|
fact {
compose
[ c0_bundles, c0_bundles_ref
, c0_contains, ~r_c0_contains, c0_contains_ref
, c0_allItem, c0_allItem_ref
]
}
pred compose[
idx: univ, i_elem: idx->univ,
hd: univ, sleg: hd->univ, tleg: hd->univ,
res: univ, r_elem: res->univ]
{
some r1: res->idx | some r2: res->hd |
all a: idx, b: hd |
a.i_elem = b.sleg implies { one r: res | r.r1 = a && r.r2 = b } &&
#res = #(idx<:i_elem).~(hd<:sleg) &&
res<:r_elem = r2.(hd<:tleg)
}
|]
```
Escape to Alloy to compose `allItem = bundles ; contains`:
```
[alloy|
fact {
compose
[ c0_bundles, c0_bundles_ref // family
, c0_contains, ~r_c0_contains, c0_contains_ref // span
, c0_allItem, c0_allItem_ref // family
]
}
pred compose[
idx: univ, i_elem: idx->univ, // family
hd: univ, sleg: hd->univ, tleg: hd->univ, // span
res: univ, r_elem: res->univ] // family
{
some idx && some hd // why is it needed? we should be able to compose empty families and spans as well
some r1: res->idx | some r2: res->hd |
all a: idx, b: hd |
a.i_elem = b.sleg implies { one r: res | r.r1 = a && r.r2 = b } &&
#res = #(idx<:i_elem).~(hd<:sleg) &&
res<:r_elem = r2.(hd<:tleg)
}
|]
```
```{.clafer .ide}
```
Next, we elaborate the model to illustrate the [composition of two multi-relations](multi-relation-composition2).