-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathgraphReachability.page
187 lines (126 loc) · 7.63 KB
/
graphReachability.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
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
---
title: Directed Graph Reachability in Presence of Variability
...
Metamodeling a directed graph
-----------------------------
We can model a directed graph with non-zero weighted edges as follows:
```clafer
abstract Node
abstract Edge ->> Node *
weight -> integer
[ this > 0 ]
```
That is, every node can be connected to zero or more other nodes and multiple edges in the same direction are allowed between any two nodes. To only allow at most one edge in the same direction between any two nodes, one would use a set-valued reference: `abstract Edge -> Node *`.
We compute total weight of all edges present in a graph as follows:
```clafer
total_weight -> integer = sum Edge.weight
```
Modeling a concrete graph
-------------------------
Then, we can specify a concrete graph in which every edge is optional shown below. The optionality of the edges is indicated using question marks, and the weights are shown in parentheses.
> 
We model the example graph in Clafer directly as follows.
Note, that we are **refining** the original reference clafer `Edge`:
* `->>` (bag) into `->` (set),
* `*` into `?`, and
* type `Node` into the specific nodes (`N1`, `N2`, etc.)
```clafer
N1 : Node
E1 : Edge -> N2 ?
[ weight = 1 ]
E2 : Edge -> N2 ?
[ weight = 2 ]
E3 : Edge -> N3 ?
[ weight = 5 ]
N2 : Node
E4 : Edge -> N3 ?
[ weight = 2 ]
N3 : Node
E5 : Edge -> N4 ?
[ weight = 1 ]
N4 : Node
[alloy|
fact {
c0_N4 in c0_N1.^(r_c0_Edge.c0_Edge_ref)
}
|]
```
Expressing reachability constraint
----------------------------------
Now, we would like to express a constraint that the node `N4` must be reachable from `N1`.
That is not currently possible in Clafer 0.4.1; however, as of 0.4.1 we can use Alloy escapes to write the constraint directly in Alloy. Markers `[alloy|` and `|]` indicates the beginning and the end of embedded Alloy code.
```
[alloy|
fact {
c0_N4 in c0_N1.^(r_c0_Edge.c0_Edge_ref)
}
|]
```
The expression `r_c0_Edge.c0_Edge_ref` computes a relation `Node->Node`, so that we can compute a transitive closure of that relation and thus express the reachability constraint.
When writing Alloy code in the escapes, we have to use names from the Alloy output generated by Clafer compiler.
A simple rule is that whenever a name of a clafer is unique, it will always be prefixed with `c0_` in the Alloy output.
Non-unique clafer names have prefixes `c0_`, `c1_`, ..., assigned in the order of the appearance of the clafers in the model.
For reference, here's the relevant Alloy output generated for clafers `Node` and `Edge`:
```alloy
abstract sig c0_Node
{ r_c0_Edge : set c0_Edge }
```
The field `r_c0_Edge` is a relation `c0_Node->c0_Edge`.
```alloy
abstract sig c0_Edge
{ c0_Edge_ref : one c0_Node }
{ one @r_c0_Edge.this }
```
The field `c0_Edge_ref` is a relation `c0_Edge->c0_Node`. Thus, the composition `r_c0_Edge.c0_Edge_ref` is a relation `Node->Node`.
In ClaferIDE, you can see the Alloy output in the `Compiled Formats` window by selecting `Alloy Model`:
> 
Playing with the model
----------------------
Use ClaferIDE with the Alloy-based backend to see all graphs in which the node `N4` is reachable.
The Choco-based backend does not yet support nested abstract clafers but one can already escape into `chocosolver`'s JavaScript using the `[choco|` ... `|]` escape.
> Tip: in IDE, you can keep the ClaferIG session running but you must click on `Compile` button after each change to the model. ClaferIG will then reload the session and keep all settings, such as, scopes and bitwidth.
```{.clafer .ide}
```
```{.clafer .config}
```
1. Can you make `N1` prohibited (that is give it cardinality `0`) and get an instance? Why?
2. Make the edges `E1` and `E2` mutually exclusive. You can use the `xor` operator. We would like to obtain a graph which can be visualized as follows:
> 
* Can you make `N1` optional and get an instance without `N1`? Why?
3. Make the node `N2` prohibited and see what happens. Is that what you expected? Why aren't there more instances?
4. Make the node `N2` optional (that is give it cardinality `?`) and see what happens. Is that what you expected?
* Then add a constraint `[no N2]`.
5. Make the edge `E2` point to either `N2` or `N3`. We would like to obtain a graph which can be visualized as follows:
> 
Note that this case is different from point 2, where we have two different edges which are exclusive. Here, we have a single edge which can have different targets.
See [answers to these questions](#answers-to-the-questions) at the end of page.
Model summary
-------------
Finally, here's a summary of our model.
Double click on the graph to show/hide references.
Our example graph is actually visible in the graphical rendering of our model.
Why? Only because we used *reference refinement* and we specified the targets of edges as types of the references. That made this information available statically. Had we used constraints to specify the targets of the edges, this information could only be obtained by constraint solving and it would be different for every instance.
Thus, using reference refinement makes more structure statically visible compared to using constraints from which such structure is hard to recover.
```{.clafer .summary}
```
Answers to the questions
------------------------
1. No. The reachability constraint requires `N4` to be in a set of nodes reachable from `N1`. If `N1` is empty, so is the set of reachable nodes, and so `N4` cannot be in an empty set.
2. The constraint can be written as `[E1 xor E2]`.
* No, if the constraint is nested under `N1`. In this case, ignoring the reachability constraint, the `xor` means that exactly one of `E1` and `E2` must be present. For that to be true, `N1` must always be present because the edges are nested under nodes and `E1` and `E2` cannot exist without their parent node `N1`. To mitigate that, we could also nest the constraint under `N1`, so that the constraint only must hold when an instance of `N1` is present:
```
N1 : Node
[E1 xor E2]
...
```
3. Because `N2` is not present, there cannot be any edges incoming to or outgoing from `N2`, which leaves only one possible path via `E3` and `E5`.
4. Yes. Graphs both with or without `N2` are possible. Adding the constraint `no N2` is equivalent to making `N2` prohibited as in point 3.
5. The idea that an edge points to either `N2` or `N3` can be formalized by introducing an derived `sum` node `N2++N3` which represents the union of the two nodes. Such a derived node can then be used as a target of `E2`.
> 
Also, observe that we now have two derived projections of `E2` called `E2->N2` and `E2->N3`, which illustrates the possible concrete edges in a resulting graph.
Concretely, specify the target type of the edge `E2` as `N2 ++ N3`, that is, `E2 : Edge -> N2 ++ N3 ?`. Observe that the edge is still optional, meaning there will be at most one instance of `E2` in the model. The type specifies the set of valid values from which at most one can be taken due to the cardinality. That is significantly different then specifying a constraint
```
E2 -> Node 2
[ E2 = N2 ++ N3 ]
```
Constraints are expressed over instances and this constraint specifies there will be two instances of the edge `E2`, such that `E2$1 = N2` and `E2$2 = N3`.