Dynamic-Source-Routing-Protocol/DSR_3.bcm at main · alegoupil/Dynamic-Source-Routing-Protocol · GitHub

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
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.scMachineFile org.eventb.core.accurate="true" org.eventb.core.configuration="org.eventb.core.fwd">
    <org.eventb.core.scRefinesMachine name="'" org.eventb.core.scTarget="/DSR2/DSR_2.bcm" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.refinesMachine#'"/>
    <org.eventb.core.scSeesContext name="(" org.eventb.core.scTarget="/DSR2/DSR_ctx_2.bcc" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.seesContext#("/>
    <org.eventb.core.scInternalContext name="DSR_ctx_0">
        <org.eventb.core.scAxiom name="'" org.eventb.core.label="axm1" org.eventb.core.predicate="finite(NOEUDS)" org.eventb.core.source="/DSR2/DSR_ctx_0.buc|org.eventb.core.contextFile#DSR_ctx_0|org.eventb.core.axiom#(" org.eventb.core.theorem="false"/>
        <org.eventb.core.scAxiom name="(" org.eventb.core.label="axm2" org.eventb.core.predicate="card(NOEUDS)=4" org.eventb.core.source="/DSR2/DSR_ctx_0.buc|org.eventb.core.contextFile#DSR_ctx_0|org.eventb.core.axiom#)" org.eventb.core.theorem="false"/>
        <org.eventb.core.scAxiom name=")" org.eventb.core.label="axm3" org.eventb.core.predicate="finite(DONNEES)" org.eventb.core.source="/DSR2/DSR_ctx_0.buc|org.eventb.core.contextFile#DSR_ctx_0|org.eventb.core.axiom#+" org.eventb.core.theorem="false"/>
        <org.eventb.core.scCarrierSet name="DONNEES" org.eventb.core.source="/DSR2/DSR_ctx_0.buc|org.eventb.core.contextFile#DSR_ctx_0|org.eventb.core.carrierSet#*" org.eventb.core.type="ℙ(DONNEES)"/>
        <org.eventb.core.scCarrierSet name="NOEUDS" org.eventb.core.source="/DSR2/DSR_ctx_0.buc|org.eventb.core.contextFile#DSR_ctx_0|org.eventb.core.carrierSet#'" org.eventb.core.type="ℙ(NOEUDS)"/>
    </org.eventb.core.scInternalContext>
    <org.eventb.core.scInternalContext name="DSR_ctx_1">
        <org.eventb.core.scExtendsContext name="'" org.eventb.core.scTarget="/DSR2/DSR_ctx_0.bcc|org.eventb.core.scContextFile#DSR_ctx_0" org.eventb.core.source="/DSR2/DSR_ctx_1.buc|org.eventb.core.contextFile#DSR_ctx_1|org.eventb.core.extendsContext#'"/>
        <org.eventb.core.scAxiom name="DSR_ctx_1" org.eventb.core.label="axm1" org.eventb.core.predicate="ROUTES={r⦂ℙ(NOEUDS×NOEUDS)·r∈NOEUDS ⤔ NOEUDS∧finite(r)∧r∩(id ⦂ ℙ(NOEUDS×NOEUDS))=(∅ ⦂ ℙ(NOEUDS×NOEUDS))∧(r=(∅ ⦂ ℙ(NOEUDS×NOEUDS))∨(∃d⦂NOEUDS,a⦂NOEUDS·d∈dom(r)∧a∈ran(r)∧dom(r) ∖ {d}=ran(r) ∖ {a}))∧(∀s⦂ℙ(NOEUDS)·s⊆dom(r)∧s≠(∅ ⦂ ℙ(NOEUDS))⇒(∃n⦂NOEUDS·n∈s∧r(n)∉s)) ∣ r}" org.eventb.core.source="/DSR2/DSR_ctx_1.buc|org.eventb.core.contextFile#DSR_ctx_1|org.eventb.core.axiom#)" org.eventb.core.theorem="false"/>
        <org.eventb.core.scAxiom name="DSR_ctx_2" org.eventb.core.label="axm13" org.eventb.core.predicate="(∅ ⦂ ℙ(NOEUDS×NOEUDS))∈ROUTES" org.eventb.core.source="/DSR2/DSR_ctx_1.buc|org.eventb.core.contextFile#DSR_ctx_1|org.eventb.core.axiom#8" org.eventb.core.theorem="false"/>
        <org.eventb.core.scAxiom name="DSR_ctx_3" org.eventb.core.label="axm6" org.eventb.core.predicate="finite(ROUTES)" org.eventb.core.source="/DSR2/DSR_ctx_1.buc|org.eventb.core.contextFile#DSR_ctx_1|org.eventb.core.axiom#1" org.eventb.core.theorem="false"/>
        <org.eventb.core.scAxiom name="DSR_ctx_4" org.eventb.core.label="axm7" org.eventb.core.predicate="⊤" org.eventb.core.source="/DSR2/DSR_ctx_1.buc|org.eventb.core.contextFile#DSR_ctx_1|org.eventb.core.axiom#2" org.eventb.core.theorem="false"/>
        <org.eventb.core.scAxiom name="DSR_ctx_5" org.eventb.core.label="axm8" org.eventb.core.predicate="⊤" org.eventb.core.source="/DSR2/DSR_ctx_1.buc|org.eventb.core.contextFile#DSR_ctx_1|org.eventb.core.axiom#3" org.eventb.core.theorem="false"/>
        <org.eventb.core.scAxiom name="DSR_ctx_6" org.eventb.core.label="axm9" org.eventb.core.predicate="⊤" org.eventb.core.source="/DSR2/DSR_ctx_1.buc|org.eventb.core.contextFile#DSR_ctx_1|org.eventb.core.axiom#4" org.eventb.core.theorem="false"/>
        <org.eventb.core.scAxiom name="DSR_ctx_7" org.eventb.core.label="axm10" org.eventb.core.predicate="⊤" org.eventb.core.source="/DSR2/DSR_ctx_1.buc|org.eventb.core.contextFile#DSR_ctx_1|org.eventb.core.axiom#5" org.eventb.core.theorem="false"/>
        <org.eventb.core.scAxiom name="DSR_ctx_8" org.eventb.core.label="axm11" org.eventb.core.predicate="⊤" org.eventb.core.source="/DSR2/DSR_ctx_1.buc|org.eventb.core.contextFile#DSR_ctx_1|org.eventb.core.axiom#6" org.eventb.core.theorem="false"/>
        <org.eventb.core.scAxiom name="DSR_ctx_9" org.eventb.core.label="axm12" org.eventb.core.predicate="⊤" org.eventb.core.source="/DSR2/DSR_ctx_1.buc|org.eventb.core.contextFile#DSR_ctx_1|org.eventb.core.axiom#7" org.eventb.core.theorem="false"/>
        <org.eventb.core.scConstant de.prob.symbolic.symbolicAttribute="false" name="ROUTES" org.eventb.core.source="/DSR2/DSR_ctx_1.buc|org.eventb.core.contextFile#DSR_ctx_1|org.eventb.core.constant#(" org.eventb.core.type="ℙ(ℙ(NOEUDS×NOEUDS))"/>
    </org.eventb.core.scInternalContext>
    <org.eventb.core.scInternalContext name="DSR_ctx_2">
        <org.eventb.core.scExtendsContext name="'" org.eventb.core.scTarget="/DSR2/DSR_ctx_1.bcc|org.eventb.core.scContextFile#DSR_ctx_1" org.eventb.core.source="/DSR2/DSR_ctx_2.buc|org.eventb.core.contextFile#DSR_ctx_2|org.eventb.core.extendsContext#'"/>
        <org.eventb.core.scAxiom name="DSR_ctx_2" org.eventb.core.label="axm1" org.eventb.core.predicate="MaxSauts∈ℕ" org.eventb.core.source="/DSR2/DSR_ctx_2.buc|org.eventb.core.contextFile#DSR_ctx_2|org.eventb.core.axiom#)" org.eventb.core.theorem="false"/>
        <org.eventb.core.scAxiom name="DSR_ctx_3" org.eventb.core.label="axm2" org.eventb.core.predicate="MaxSauts=2" org.eventb.core.source="/DSR2/DSR_ctx_2.buc|org.eventb.core.contextFile#DSR_ctx_2|org.eventb.core.axiom#*" org.eventb.core.theorem="false"/>
        <org.eventb.core.scConstant de.prob.symbolic.symbolicAttribute="false" name="MaxSauts" org.eventb.core.source="/DSR2/DSR_ctx_2.buc|org.eventb.core.contextFile#DSR_ctx_2|org.eventb.core.constant#(" org.eventb.core.type="ℤ"/>
    </org.eventb.core.scInternalContext>
    <org.eventb.core.scInvariant name="DSR_ctx_1" org.eventb.core.label="inv1" org.eventb.core.predicate="Reseau∈NOEUDS ↔ NOEUDS" org.eventb.core.source="/DSR2/DSR_0.bum|org.eventb.core.machineFile#DSR_0|org.eventb.core.invariant#*" org.eventb.core.theorem="false"/>
    <org.eventb.core.scInvariant name="DSR_ctx_2" org.eventb.core.label="inv2" org.eventb.core.predicate="Reseau∩(id ⦂ ℙ(NOEUDS×NOEUDS))=(∅ ⦂ ℙ(NOEUDS×NOEUDS))" org.eventb.core.source="/DSR2/DSR_0.bum|org.eventb.core.machineFile#DSR_0|org.eventb.core.invariant#," org.eventb.core.theorem="false"/>
    <org.eventb.core.scInvariant name="DSR_ctx_3" org.eventb.core.label="inv3" org.eventb.core.predicate="∀s1⦂NOEUDS,s2⦂NOEUDS·s1 ↦ s2∈Reseau⇒s2≠s1" org.eventb.core.source="/DSR2/DSR_0.bum|org.eventb.core.machineFile#DSR_0|org.eventb.core.invariant#-" org.eventb.core.theorem="true"/>
    <org.eventb.core.scInvariant name="DSR_ctx_4" org.eventb.core.label="inv4" org.eventb.core.predicate="StockNoeud∈DONNEES ⇸ NOEUDS" org.eventb.core.source="/DSR2/DSR_0.bum|org.eventb.core.machineFile#DSR_0|org.eventb.core.invariant#1" org.eventb.core.theorem="false"/>
    <org.eventb.core.scInvariant name="DSR_ctx_5" org.eventb.core.label="inv5" org.eventb.core.predicate="EnvoiVers∈DONNEES ⇸ NOEUDS × NOEUDS" org.eventb.core.source="/DSR2/DSR_0.bum|org.eventb.core.machineFile#DSR_0|org.eventb.core.invariant#4" org.eventb.core.theorem="false"/>
    <org.eventb.core.scInvariant name="DSR_ctx_6" org.eventb.core.label="inv6" org.eventb.core.predicate="dom(StockNoeud)∩dom(EnvoiVers)=(∅ ⦂ ℙ(DONNEES))" org.eventb.core.source="/DSR2/DSR_0.bum|org.eventb.core.machineFile#DSR_0|org.eventb.core.invariant#5" org.eventb.core.theorem="false"/>
    <org.eventb.core.scInvariant name="DSR_ctx_7" org.eventb.core.label="inv7" org.eventb.core.predicate="DonneesGros⊆DONNEES" org.eventb.core.source="/DSR2/DSR_0.bum|org.eventb.core.machineFile#DSR_0|org.eventb.core.invariant#:" org.eventb.core.theorem="false"/>
    <org.eventb.core.scInvariant name="DSR_ctx_8" org.eventb.core.label="inv8" org.eventb.core.predicate="dom(StockNoeud)∩DonneesGros=(∅ ⦂ ℙ(DONNEES))" org.eventb.core.source="/DSR2/DSR_0.bum|org.eventb.core.machineFile#DSR_0|org.eventb.core.invariant#;" org.eventb.core.theorem="false"/>
    <org.eventb.core.scInvariant name="DSR_ctx_9" org.eventb.core.label="inv9" org.eventb.core.predicate="DonneesGros∩dom(EnvoiVers)=(∅ ⦂ ℙ(DONNEES))" org.eventb.core.source="/DSR2/DSR_0.bum|org.eventb.core.machineFile#DSR_0|org.eventb.core.invariant#=" org.eventb.core.theorem="false"/>
    <org.eventb.core.scInvariant name="DSR_ctx_:" org.eventb.core.label="inv1" org.eventb.core.predicate="DonneesRoute∈DONNEES ⇸ ROUTES" org.eventb.core.source="/DSR2/DSR_1.bum|org.eventb.core.machineFile#DSR_1|org.eventb.core.invariant#;" org.eventb.core.theorem="false"/>
    <org.eventb.core.scInvariant name="DSR_ctx_;" org.eventb.core.label="inv1" org.eventb.core.predicate="TableRoutage∈NOEUDS → (NOEUDS ⇸ ROUTES)" org.eventb.core.source="/DSR2/DSR_2.bum|org.eventb.core.machineFile#DSR_2|org.eventb.core.invariant#M" org.eventb.core.theorem="false"/>
    <org.eventb.core.scInvariant name="DSR_ctx_=" org.eventb.core.label="inv4" org.eventb.core.predicate="∀x⦂NOEUDS,y⦂NOEUDS·x∈dom(TableRoutage)∧y∈dom(TableRoutage(x))⇒x∈dom(TableRoutage(x)(y))∧x∉ran(TableRoutage(x)(y))" org.eventb.core.source="/DSR2/DSR_2.bum|org.eventb.core.machineFile#DSR_2|org.eventb.core.invariant#P" org.eventb.core.theorem="false"/>
    <org.eventb.core.scInvariant name="DSR_ctx_&gt;" org.eventb.core.label="inv5" org.eventb.core.predicate="∀x⦂NOEUDS,y⦂NOEUDS·x∈dom(TableRoutage)∧y∈dom(TableRoutage(x))⇒y∈ran(TableRoutage(x)(y))∧y∉dom(TableRoutage(x)(y))" org.eventb.core.source="/DSR2/DSR_2.bum|org.eventb.core.machineFile#DSR_2|org.eventb.core.invariant#Q" org.eventb.core.theorem="false"/>
    <org.eventb.core.scInvariant name="DSR_ctx_?" org.eventb.core.label="inv6" org.eventb.core.predicate="∀x⦂NOEUDS,y⦂NOEUDS·x∈dom(TableRoutage)∧y∈dom(TableRoutage(x))⇒x≠y" org.eventb.core.source="/DSR2/DSR_2.bum|org.eventb.core.machineFile#DSR_2|org.eventb.core.invariant#W" org.eventb.core.theorem="false"/>
    <org.eventb.core.scInvariant name="DSR_ctx_@" org.eventb.core.label="inv1" org.eventb.core.predicate="RREQ∈NOEUDS ↔ ROUTES" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.invariant#c" org.eventb.core.theorem="false"/>
    <org.eventb.core.scInvariant name="DSR_ctx_A" org.eventb.core.label="inv2" org.eventb.core.predicate="RREQTransit∈RREQ ⇸ (NOEUDS ⇸ ℙ(NOEUDS))" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.invariant#e" org.eventb.core.theorem="false"/>
    <org.eventb.core.scInvariant name="DSR_ctx_B" org.eventb.core.label="inv3" org.eventb.core.predicate="RREP∈ROUTES ⇸ NOEUDS" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.invariant#l" org.eventb.core.theorem="false"/>
    <org.eventb.core.scInvariant name="DSR_ctx_C" org.eventb.core.label="inv4" org.eventb.core.predicate="RREPTransit⊆RREP" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.invariant#o" org.eventb.core.theorem="false"/>
    <org.eventb.core.scVariable name="DonneesRoute" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.variable#B" org.eventb.core.type="ℙ(DONNEES×ℙ(NOEUDS×NOEUDS))"/>
    <org.eventb.core.scVariable name="RREQTransit" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.variable#f" org.eventb.core.type="ℙ(NOEUDS×ℙ(NOEUDS×NOEUDS)×ℙ(NOEUDS×ℙ(NOEUDS)))"/>
    <org.eventb.core.scVariable name="DonneesGros" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.variable#V" org.eventb.core.type="ℙ(DONNEES)"/>
    <org.eventb.core.scVariable name="RREQ" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.variable#b" org.eventb.core.type="ℙ(NOEUDS×ℙ(NOEUDS×NOEUDS))"/>
    <org.eventb.core.scVariable name="RREP" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.variable#m" org.eventb.core.type="ℙ(ℙ(NOEUDS×NOEUDS)×NOEUDS)"/>
    <org.eventb.core.scVariable name="EnvoiVers" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.variable#3" org.eventb.core.type="ℙ(DONNEES×(NOEUDS×NOEUDS))"/>
    <org.eventb.core.scVariable name="RREPTransit" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.variable#n" org.eventb.core.type="ℙ(ℙ(NOEUDS×NOEUDS)×NOEUDS)"/>
    <org.eventb.core.scVariable name="TableRoutage" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.variable#L" org.eventb.core.type="ℙ(NOEUDS×ℙ(NOEUDS×ℙ(NOEUDS×NOEUDS)))"/>
    <org.eventb.core.scVariable name="Reseau" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.variable#)" org.eventb.core.type="ℙ(NOEUDS×NOEUDS)"/>
    <org.eventb.core.scVariable name="StockNoeud" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.variable#0" org.eventb.core.type="ℙ(DONNEES×NOEUDS)"/>
    <org.eventb.core.scEvent name="TableRoutagf" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="INITIALISATION" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#W">
        <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/DSR2/DSR_2.bcm|org.eventb.core.scMachineFile#DSR_2|org.eventb.core.scEvent#TableRoutagf" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#W"/>
        <org.eventb.core.scAction name="'" org.eventb.core.assignment="Reseau ≔ ∅ ⦂ ℙ(NOEUDS×NOEUDS)" org.eventb.core.label="act1" org.eventb.core.source="/DSR2/DSR_0.bum|org.eventb.core.machineFile#DSR_0|org.eventb.core.event#'|org.eventb.core.action#'"/>
        <org.eventb.core.scAction name="(" org.eventb.core.assignment="StockNoeud ≔ ∅ ⦂ ℙ(DONNEES×NOEUDS)" org.eventb.core.label="act2" org.eventb.core.source="/DSR2/DSR_0.bum|org.eventb.core.machineFile#DSR_0|org.eventb.core.event#'|org.eventb.core.action#("/>
        <org.eventb.core.scAction name=")" org.eventb.core.assignment="EnvoiVers ≔ ∅ ⦂ ℙ(DONNEES×(NOEUDS×NOEUDS))" org.eventb.core.label="act3" org.eventb.core.source="/DSR2/DSR_0.bum|org.eventb.core.machineFile#DSR_0|org.eventb.core.event#'|org.eventb.core.action#)"/>
        <org.eventb.core.scAction name="*" org.eventb.core.assignment="DonneesGros ≔ ∅ ⦂ ℙ(DONNEES)" org.eventb.core.label="act4" org.eventb.core.source="/DSR2/DSR_0.bum|org.eventb.core.machineFile#DSR_0|org.eventb.core.event#'|org.eventb.core.action#*"/>
        <org.eventb.core.scAction name="+" org.eventb.core.assignment="DonneesRoute ≔ ∅ ⦂ ℙ(DONNEES×ℙ(NOEUDS×NOEUDS))" org.eventb.core.label="act5" org.eventb.core.source="/DSR2/DSR_1.bum|org.eventb.core.machineFile#DSR_1|org.eventb.core.event#4|org.eventb.core.action#'"/>
        <org.eventb.core.scAction name="," org.eventb.core.assignment="TableRoutage :∈ NOEUDS → {∅ ⦂ ℙ(NOEUDS×ℙ(NOEUDS×NOEUDS))}" org.eventb.core.label="act6" org.eventb.core.source="/DSR2/DSR_2.bum|org.eventb.core.machineFile#DSR_2|org.eventb.core.event#C|org.eventb.core.action#'"/>
        <org.eventb.core.scAction name="-" org.eventb.core.assignment="RREQ ≔ ∅ ⦂ ℙ(NOEUDS×ℙ(NOEUDS×NOEUDS))" org.eventb.core.label="act7" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#W|org.eventb.core.action#'"/>
        <org.eventb.core.scAction name="." org.eventb.core.assignment="RREQTransit ≔ ∅ ⦂ ℙ(NOEUDS×ℙ(NOEUDS×NOEUDS)×ℙ(NOEUDS×ℙ(NOEUDS)))" org.eventb.core.label="act8" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#W|org.eventb.core.action#("/>
        <org.eventb.core.scAction name="/" org.eventb.core.assignment="RREP ≔ ∅ ⦂ ℙ(ℙ(NOEUDS×NOEUDS)×NOEUDS)" org.eventb.core.label="act9" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#W|org.eventb.core.action#)"/>
        <org.eventb.core.scAction name="0" org.eventb.core.assignment="RREPTransit ≔ ∅ ⦂ ℙ(ℙ(NOEUDS×NOEUDS)×NOEUDS)" org.eventb.core.label="act10" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#W|org.eventb.core.action#*"/>
    </org.eventb.core.scEvent>
    <org.eventb.core.scEvent name="TableRoutagg" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="Lier" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#X">
        <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/DSR2/DSR_2.bcm|org.eventb.core.scMachineFile#DSR_2|org.eventb.core.scEvent#TableRoutagg" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#X|org.eventb.core.refinesEvent#'"/>
        <org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="n1∈NOEUDS" org.eventb.core.source="/DSR2/DSR_0.bum|org.eventb.core.machineFile#DSR_0|org.eventb.core.event#+|org.eventb.core.guard#)" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="n2∈NOEUDS" org.eventb.core.source="/DSR2/DSR_0.bum|org.eventb.core.machineFile#DSR_0|org.eventb.core.event#+|org.eventb.core.guard#*" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name=")" org.eventb.core.label="grd3" org.eventb.core.predicate="n1≠n2" org.eventb.core.source="/DSR2/DSR_0.bum|org.eventb.core.machineFile#DSR_0|org.eventb.core.event#+|org.eventb.core.guard#+" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="*" org.eventb.core.label="grd4" org.eventb.core.predicate="n1 ↦ n2∉Reseau" org.eventb.core.source="/DSR2/DSR_0.bum|org.eventb.core.machineFile#DSR_0|org.eventb.core.event#+|org.eventb.core.guard#-" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="n4" org.eventb.core.label="grd5" org.eventb.core.predicate="n2∉dom(TableRoutage(n1))" org.eventb.core.source="/DSR2/DSR_2.bum|org.eventb.core.machineFile#DSR_2|org.eventb.core.event#D|org.eventb.core.guard#)" org.eventb.core.theorem="false"/>
        <org.eventb.core.scAction name="n3" org.eventb.core.assignment="Reseau ≔ Reseau∪{n1 ↦ n2}" org.eventb.core.label="act1" org.eventb.core.source="/DSR2/DSR_0.bum|org.eventb.core.machineFile#DSR_0|org.eventb.core.event#+|org.eventb.core.action#,"/>
        <org.eventb.core.scAction name="n5" org.eventb.core.assignment="TableRoutage ≔ TableRoutage{n1 ↦ TableRoutage(n1)∪{n2 ↦ {n1 ↦ n2}}}" org.eventb.core.label="act2" org.eventb.core.source="/DSR2/DSR_2.bum|org.eventb.core.machineFile#DSR_2|org.eventb.core.event#D|org.eventb.core.action#("/>
        <org.eventb.core.scParameter name="n1" org.eventb.core.source="/DSR2/DSR_0.bum|org.eventb.core.machineFile#DSR_0|org.eventb.core.event#+|org.eventb.core.parameter#'" org.eventb.core.type="NOEUDS"/>
        <org.eventb.core.scParameter name="n2" org.eventb.core.source="/DSR2/DSR_0.bum|org.eventb.core.machineFile#DSR_0|org.eventb.core.event#+|org.eventb.core.parameter#(" org.eventb.core.type="NOEUDS"/>
    </org.eventb.core.scEvent>
    <org.eventb.core.scEvent name="TableRoutagh" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="Delier" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#Y">
        <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/DSR2/DSR_2.bcm|org.eventb.core.scMachineFile#DSR_2|org.eventb.core.scEvent#TableRoutagh" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#Y|org.eventb.core.refinesEvent#'"/>
        <org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="n1 ↦ n2∈Reseau" org.eventb.core.source="/DSR2/DSR_0.bum|org.eventb.core.machineFile#DSR_0|org.eventb.core.event#.|org.eventb.core.guard#)" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="n1≠n2" org.eventb.core.source="/DSR2/DSR_0.bum|org.eventb.core.machineFile#DSR_0|org.eventb.core.event#.|org.eventb.core.guard#+" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="n4" org.eventb.core.label="grd3" org.eventb.core.predicate="n1∈dom(TableRoutage)" org.eventb.core.source="/DSR2/DSR_2.bum|org.eventb.core.machineFile#DSR_2|org.eventb.core.event#E|org.eventb.core.guard#(" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="n5" org.eventb.core.label="grd4" org.eventb.core.predicate="n2∈dom(TableRoutage(n1))" org.eventb.core.source="/DSR2/DSR_2.bum|org.eventb.core.machineFile#DSR_2|org.eventb.core.event#E|org.eventb.core.guard#*" org.eventb.core.theorem="false"/>
        <org.eventb.core.scAction name="n3" org.eventb.core.assignment="Reseau ≔ Reseau ∖ {n1 ↦ n2}" org.eventb.core.label="act1" org.eventb.core.source="/DSR2/DSR_0.bum|org.eventb.core.machineFile#DSR_0|org.eventb.core.event#.|org.eventb.core.action#*"/>
        <org.eventb.core.scAction name="n6" org.eventb.core.assignment="TableRoutage ≔ TableRoutage{n1 ↦ TableRoutage(n1) ∖ {n2 ↦ {n1 ↦ n2}}}" org.eventb.core.label="act2" org.eventb.core.source="/DSR2/DSR_2.bum|org.eventb.core.machineFile#DSR_2|org.eventb.core.event#E|org.eventb.core.action#)"/>
        <org.eventb.core.scParameter name="n1" org.eventb.core.source="/DSR2/DSR_0.bum|org.eventb.core.machineFile#DSR_0|org.eventb.core.event#.|org.eventb.core.parameter#'" org.eventb.core.type="NOEUDS"/>
        <org.eventb.core.scParameter name="n2" org.eventb.core.source="/DSR2/DSR_0.bum|org.eventb.core.machineFile#DSR_0|org.eventb.core.event#.|org.eventb.core.parameter#(" org.eventb.core.type="NOEUDS"/>
    </org.eventb.core.scEvent>
    <org.eventb.core.scEvent name="TableRoutagi" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="Envoyer" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#Z">
        <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/DSR2/DSR_2.bcm|org.eventb.core.scMachineFile#DSR_2|org.eventb.core.scEvent#TableRoutagi" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#Z|org.eventb.core.refinesEvent#'"/>
        <org.eventb.core.scGuard name="(" org.eventb.core.label="grd1" org.eventb.core.predicate="data∈dom(StockNoeud)" org.eventb.core.source="/DSR2/DSR_2.bum|org.eventb.core.machineFile#DSR_2|org.eventb.core.event#F|org.eventb.core.guard#*" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name=")" org.eventb.core.label="grd3" org.eventb.core.predicate="data ↦ StockNoeud(data)∈StockNoeud" org.eventb.core.source="/DSR2/DSR_2.bum|org.eventb.core.machineFile#DSR_2|org.eventb.core.event#F|org.eventb.core.guard#," org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="*" org.eventb.core.label="grd4" org.eventb.core.predicate="data∉dom(EnvoiVers)" org.eventb.core.source="/DSR2/DSR_2.bum|org.eventb.core.machineFile#DSR_2|org.eventb.core.event#F|org.eventb.core.guard#internal1" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="+" org.eventb.core.label="grd16" org.eventb.core.predicate="data∉dom(DonneesRoute)" org.eventb.core.source="/DSR2/DSR_2.bum|org.eventb.core.machineFile#DSR_2|org.eventb.core.event#F|org.eventb.core.guard#internal4" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="," org.eventb.core.label="grd18" org.eventb.core.predicate="n∈NOEUDS" org.eventb.core.source="/DSR2/DSR_2.bum|org.eventb.core.machineFile#DSR_2|org.eventb.core.event#F|org.eventb.core.guard#internal:" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="-" org.eventb.core.label="grd19" org.eventb.core.predicate="n∈dom(TableRoutage(StockNoeud(data)))" org.eventb.core.source="/DSR2/DSR_2.bum|org.eventb.core.machineFile#DSR_2|org.eventb.core.event#F|org.eventb.core.guard#internal=" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="." org.eventb.core.label="grd20" org.eventb.core.predicate="TableRoutage(StockNoeud(data))(n)⊆Reseau" org.eventb.core.source="/DSR2/DSR_2.bum|org.eventb.core.machineFile#DSR_2|org.eventb.core.event#F|org.eventb.core.guard#internal&gt;" org.eventb.core.theorem="false"/>
        <org.eventb.core.scAction name="datb" org.eventb.core.assignment="DonneesRoute ≔ DonneesRoute∪{data ↦ TableRoutage(StockNoeud(data))(n)}" org.eventb.core.label="act3" org.eventb.core.source="/DSR2/DSR_2.bum|org.eventb.core.machineFile#DSR_2|org.eventb.core.event#F|org.eventb.core.action#-"/>
        <org.eventb.core.scAction name="datc" org.eventb.core.assignment="StockNoeud ≔ StockNoeud ∖ {data ↦ StockNoeud(data)}" org.eventb.core.label="act4" org.eventb.core.source="/DSR2/DSR_2.bum|org.eventb.core.machineFile#DSR_2|org.eventb.core.event#F|org.eventb.core.action#internal6"/>
        <org.eventb.core.scAction name="datd" org.eventb.core.assignment="EnvoiVers ≔ EnvoiVers∪{data ↦ (StockNoeud(data) ↦ TableRoutage(StockNoeud(data))(n)(StockNoeud(data)))}" org.eventb.core.label="act5" org.eventb.core.source="/DSR2/DSR_2.bum|org.eventb.core.machineFile#DSR_2|org.eventb.core.event#F|org.eventb.core.action#internal7"/>
        <org.eventb.core.scParameter name="data" org.eventb.core.source="/DSR2/DSR_2.bum|org.eventb.core.machineFile#DSR_2|org.eventb.core.event#F|org.eventb.core.parameter#'" org.eventb.core.type="DONNEES"/>
        <org.eventb.core.scParameter name="n" org.eventb.core.source="/DSR2/DSR_2.bum|org.eventb.core.machineFile#DSR_2|org.eventb.core.event#F|org.eventb.core.parameter#)" org.eventb.core.type="NOEUDS"/>
    </org.eventb.core.scEvent>
    <org.eventb.core.scEvent name="TableRoutagj" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="Produire" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#[">
        <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/DSR2/DSR_2.bcm|org.eventb.core.scMachineFile#DSR_2|org.eventb.core.scEvent#TableRoutagj" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#[|org.eventb.core.refinesEvent#'"/>
        <org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="n∈NOEUDS" org.eventb.core.source="/DSR2/DSR_0.bum|org.eventb.core.machineFile#DSR_0|org.eventb.core.event#2|org.eventb.core.guard#*" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="data∈DONNEES" org.eventb.core.source="/DSR2/DSR_0.bum|org.eventb.core.machineFile#DSR_0|org.eventb.core.event#2|org.eventb.core.guard#+" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name=")" org.eventb.core.label="grd3" org.eventb.core.predicate="data∉dom(StockNoeud)" org.eventb.core.source="/DSR2/DSR_0.bum|org.eventb.core.machineFile#DSR_0|org.eventb.core.event#2|org.eventb.core.guard#," org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="*" org.eventb.core.label="grd4" org.eventb.core.predicate="data∉dom(EnvoiVers)" org.eventb.core.source="/DSR2/DSR_0.bum|org.eventb.core.machineFile#DSR_0|org.eventb.core.event#2|org.eventb.core.guard#-" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="+" org.eventb.core.label="grd5" org.eventb.core.predicate="data∉DonneesGros" org.eventb.core.source="/DSR2/DSR_0.bum|org.eventb.core.machineFile#DSR_0|org.eventb.core.event#2|org.eventb.core.guard#." org.eventb.core.theorem="false"/>
        <org.eventb.core.scAction name="datb" org.eventb.core.assignment="StockNoeud ≔ StockNoeud∪{data ↦ n}" org.eventb.core.label="act1" org.eventb.core.source="/DSR2/DSR_0.bum|org.eventb.core.machineFile#DSR_0|org.eventb.core.event#2|org.eventb.core.action#)"/>
        <org.eventb.core.scParameter name="data" org.eventb.core.source="/DSR2/DSR_0.bum|org.eventb.core.machineFile#DSR_0|org.eventb.core.event#2|org.eventb.core.parameter#(" org.eventb.core.type="DONNEES"/>
        <org.eventb.core.scParameter name="n" org.eventb.core.source="/DSR2/DSR_0.bum|org.eventb.core.machineFile#DSR_0|org.eventb.core.event#2|org.eventb.core.parameter#'" org.eventb.core.type="NOEUDS"/>
    </org.eventb.core.scEvent>
    <org.eventb.core.scEvent name="TableRoutagk" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="Perdre" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#\\">
        <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/DSR2/DSR_2.bcm|org.eventb.core.scMachineFile#DSR_2|org.eventb.core.scEvent#TableRoutagk" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#\\|org.eventb.core.refinesEvent#'"/>
        <org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="d∈dom(EnvoiVers)" org.eventb.core.source="/DSR2/DSR_0.bum|org.eventb.core.machineFile#DSR_0|org.eventb.core.event#6|org.eventb.core.guard#)" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="g" org.eventb.core.label="grd2" org.eventb.core.predicate="d∈dom(DonneesRoute)" org.eventb.core.source="/DSR2/DSR_1.bum|org.eventb.core.machineFile#DSR_1|org.eventb.core.event#9|org.eventb.core.guard#)" org.eventb.core.theorem="false"/>
        <org.eventb.core.scAction name="e" org.eventb.core.assignment="EnvoiVers ≔ EnvoiVers ∖ {d ↦ EnvoiVers(d)}" org.eventb.core.label="act1" org.eventb.core.source="/DSR2/DSR_0.bum|org.eventb.core.machineFile#DSR_0|org.eventb.core.event#6|org.eventb.core.action#*"/>
        <org.eventb.core.scAction name="f" org.eventb.core.assignment="DonneesGros ≔ DonneesGros∪{d}" org.eventb.core.label="act2" org.eventb.core.source="/DSR2/DSR_0.bum|org.eventb.core.machineFile#DSR_0|org.eventb.core.event#6|org.eventb.core.action#+"/>
        <org.eventb.core.scAction name="h" org.eventb.core.assignment="DonneesRoute ≔ DonneesRoute ∖ {d ↦ DonneesRoute(d)}" org.eventb.core.label="act3" org.eventb.core.source="/DSR2/DSR_1.bum|org.eventb.core.machineFile#DSR_1|org.eventb.core.event#9|org.eventb.core.action#("/>
        <org.eventb.core.scParameter name="d" org.eventb.core.source="/DSR2/DSR_0.bum|org.eventb.core.machineFile#DSR_0|org.eventb.core.event#6|org.eventb.core.parameter#'" org.eventb.core.type="DONNEES"/>
    </org.eventb.core.scEvent>
    <org.eventb.core.scEvent name="TableRoutagl" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="Recevoir" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#]">
        <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/DSR2/DSR_2.bcm|org.eventb.core.scMachineFile#DSR_2|org.eventb.core.scEvent#TableRoutagl" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#]|org.eventb.core.refinesEvent#'"/>
        <org.eventb.core.scGuard name="(" org.eventb.core.label="grd3" org.eventb.core.predicate="data∉dom(StockNoeud)" org.eventb.core.source="/DSR2/DSR_1.bum|org.eventb.core.machineFile#DSR_1|org.eventb.core.event#:|org.eventb.core.guard#-" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name=")" org.eventb.core.label="grd4" org.eventb.core.predicate="data∈dom(EnvoiVers)" org.eventb.core.source="/DSR2/DSR_1.bum|org.eventb.core.machineFile#DSR_1|org.eventb.core.event#:|org.eventb.core.guard#." org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="*" org.eventb.core.label="grd5" org.eventb.core.predicate="data∈dom(DonneesRoute)" org.eventb.core.source="/DSR2/DSR_1.bum|org.eventb.core.machineFile#DSR_1|org.eventb.core.event#:|org.eventb.core.guard#\/" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="+" org.eventb.core.label="grd6" org.eventb.core.predicate="(prj2 ⦂ ℙ(NOEUDS×NOEUDS×NOEUDS))(EnvoiVers(data))∉dom(DonneesRoute(data))" org.eventb.core.source="/DSR2/DSR_1.bum|org.eventb.core.machineFile#DSR_1|org.eventb.core.event#:|org.eventb.core.guard#1" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="," org.eventb.core.label="grd7" org.eventb.core.predicate="EnvoiVers(data)∈Reseau" org.eventb.core.source="/DSR2/DSR_1.bum|org.eventb.core.machineFile#DSR_1|org.eventb.core.event#:|org.eventb.core.guard#2" org.eventb.core.theorem="false"/>
        <org.eventb.core.scAction name="datb" org.eventb.core.assignment="EnvoiVers ≔ EnvoiVers ∖ {data ↦ EnvoiVers(data)}" org.eventb.core.label="act1" org.eventb.core.source="/DSR2/DSR_1.bum|org.eventb.core.machineFile#DSR_1|org.eventb.core.event#:|org.eventb.core.action#*"/>
        <org.eventb.core.scAction name="datc" org.eventb.core.assignment="DonneesRoute ≔ DonneesRoute ∖ {data ↦ DonneesRoute(data)}" org.eventb.core.label="act2" org.eventb.core.source="/DSR2/DSR_1.bum|org.eventb.core.machineFile#DSR_1|org.eventb.core.event#:|org.eventb.core.action#0"/>
        <org.eventb.core.scAction name="datd" org.eventb.core.assignment="DonneesGros ≔ DonneesGros∪{data}" org.eventb.core.label="act3" org.eventb.core.source="/DSR2/DSR_1.bum|org.eventb.core.machineFile#DSR_1|org.eventb.core.event#:|org.eventb.core.action#3"/>
        <org.eventb.core.scParameter name="data" org.eventb.core.source="/DSR2/DSR_1.bum|org.eventb.core.machineFile#DSR_1|org.eventb.core.event#:|org.eventb.core.parameter#'" org.eventb.core.type="DONNEES"/>
    </org.eventb.core.scEvent>
    <org.eventb.core.scEvent name="TableRoutagm" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="Store" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#^">
        <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/DSR2/DSR_2.bcm|org.eventb.core.scMachineFile#DSR_2|org.eventb.core.scEvent#TableRoutagm" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#^|org.eventb.core.refinesEvent#'"/>
        <org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="data∈dom(EnvoiVers)" org.eventb.core.source="/DSR2/DSR_0.bum|org.eventb.core.machineFile#DSR_0|org.eventb.core.event#8|org.eventb.core.guard#(" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="data∉dom(StockNoeud)" org.eventb.core.source="/DSR2/DSR_0.bum|org.eventb.core.machineFile#DSR_0|org.eventb.core.event#8|org.eventb.core.guard#)" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name=")" org.eventb.core.label="grd3" org.eventb.core.predicate="EnvoiVers(data)∈Reseau" org.eventb.core.source="/DSR2/DSR_0.bum|org.eventb.core.machineFile#DSR_0|org.eventb.core.event#8|org.eventb.core.guard#*" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="datd" org.eventb.core.label="grd6" org.eventb.core.predicate="data∈dom(DonneesRoute)" org.eventb.core.source="/DSR2/DSR_1.bum|org.eventb.core.machineFile#DSR_1|org.eventb.core.event#?|org.eventb.core.guard#1" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="date" org.eventb.core.label="grd8" org.eventb.core.predicate="(prj2 ⦂ ℙ(NOEUDS×NOEUDS×NOEUDS))(EnvoiVers(data))∈dom(DonneesRoute(data))" org.eventb.core.source="/DSR2/DSR_1.bum|org.eventb.core.machineFile#DSR_1|org.eventb.core.event#?|org.eventb.core.guard#5" org.eventb.core.theorem="false"/>
        <org.eventb.core.scAction name="datb" org.eventb.core.assignment="EnvoiVers ≔ EnvoiVers ∖ {data ↦ EnvoiVers(data)}" org.eventb.core.label="act1" org.eventb.core.source="/DSR2/DSR_0.bum|org.eventb.core.machineFile#DSR_0|org.eventb.core.event#8|org.eventb.core.action#+"/>
        <org.eventb.core.scAction name="datc" org.eventb.core.assignment="StockNoeud ≔ StockNoeud∪{data ↦ (prj2 ⦂ ℙ(NOEUDS×NOEUDS×NOEUDS))(EnvoiVers(data))}" org.eventb.core.label="act2" org.eventb.core.source="/DSR2/DSR_0.bum|org.eventb.core.machineFile#DSR_0|org.eventb.core.event#8|org.eventb.core.action#,"/>
        <org.eventb.core.scParameter name="data" org.eventb.core.source="/DSR2/DSR_0.bum|org.eventb.core.machineFile#DSR_0|org.eventb.core.event#8|org.eventb.core.parameter#'" org.eventb.core.type="DONNEES"/>
    </org.eventb.core.scEvent>
    <org.eventb.core.scEvent name="TableRoutagn" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="Forward" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#_">
        <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/DSR2/DSR_2.bcm|org.eventb.core.scMachineFile#DSR_2|org.eventb.core.scEvent#TableRoutagn" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#_|org.eventb.core.refinesEvent#'"/>
        <org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="data∈dom(StockNoeud)" org.eventb.core.source="/DSR2/DSR_0.bum|org.eventb.core.machineFile#DSR_0|org.eventb.core.event#\/|org.eventb.core.guard#*" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="(" org.eventb.core.label="grd4" org.eventb.core.predicate="data∉dom(EnvoiVers)" org.eventb.core.source="/DSR2/DSR_0.bum|org.eventb.core.machineFile#DSR_0|org.eventb.core.event#\/|org.eventb.core.guard#\/" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name=")" org.eventb.core.label="grd5" org.eventb.core.predicate="n∈NOEUDS" org.eventb.core.source="/DSR2/DSR_0.bum|org.eventb.core.machineFile#DSR_0|org.eventb.core.event#\/|org.eventb.core.guard#0" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="*" org.eventb.core.label="grd7" org.eventb.core.predicate="n≠StockNoeud(data)" org.eventb.core.source="/DSR2/DSR_0.bum|org.eventb.core.machineFile#DSR_0|org.eventb.core.event#\/|org.eventb.core.guard#2" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="+" org.eventb.core.label="grd8" org.eventb.core.predicate="n∈Reseau[{StockNoeud(data)}]" org.eventb.core.source="/DSR2/DSR_0.bum|org.eventb.core.machineFile#DSR_0|org.eventb.core.event#\/|org.eventb.core.guard#3" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="datd" org.eventb.core.label="grd9" org.eventb.core.predicate="data∈dom(DonneesRoute)" org.eventb.core.source="/DSR2/DSR_1.bum|org.eventb.core.machineFile#DSR_1|org.eventb.core.event#C|org.eventb.core.guard#(" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="date" org.eventb.core.label="grd10" org.eventb.core.predicate="StockNoeud(data)∈dom(DonneesRoute(data))" org.eventb.core.source="/DSR2/DSR_1.bum|org.eventb.core.machineFile#DSR_1|org.eventb.core.event#C|org.eventb.core.guard#)" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="datf" org.eventb.core.label="grd11" org.eventb.core.predicate="n=DonneesRoute(data)(StockNoeud(data))" org.eventb.core.source="/DSR2/DSR_1.bum|org.eventb.core.machineFile#DSR_1|org.eventb.core.event#C|org.eventb.core.guard#*" org.eventb.core.theorem="false"/>
        <org.eventb.core.scAction name="datb" org.eventb.core.assignment="EnvoiVers ≔ EnvoiVers∪{data ↦ (StockNoeud(data) ↦ n)}" org.eventb.core.label="act1" org.eventb.core.source="/DSR2/DSR_0.bum|org.eventb.core.machineFile#DSR_0|org.eventb.core.event#\/|org.eventb.core.action#-"/>
        <org.eventb.core.scAction name="datc" org.eventb.core.assignment="StockNoeud ≔ StockNoeud ∖ {data ↦ StockNoeud(data)}" org.eventb.core.label="act2" org.eventb.core.source="/DSR2/DSR_0.bum|org.eventb.core.machineFile#DSR_0|org.eventb.core.event#\/|org.eventb.core.action#."/>
        <org.eventb.core.scParameter name="data" org.eventb.core.source="/DSR2/DSR_0.bum|org.eventb.core.machineFile#DSR_0|org.eventb.core.event#\/|org.eventb.core.parameter#'" org.eventb.core.type="DONNEES"/>
        <org.eventb.core.scParameter name="n" org.eventb.core.source="/DSR2/DSR_0.bum|org.eventb.core.machineFile#DSR_0|org.eventb.core.event#\/|org.eventb.core.parameter#)" org.eventb.core.type="NOEUDS"/>
    </org.eventb.core.scEvent>
    <org.eventb.core.scEvent name="TableRoutago" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="Router" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#`">
        <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/DSR2/DSR_2.bcm|org.eventb.core.scMachineFile#DSR_2|org.eventb.core.scEvent#TableRoutago" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#`|org.eventb.core.refinesEvent#'"/>
        <org.eventb.core.scGuard name="'" org.eventb.core.label="grd3" org.eventb.core.predicate="r∈ROUTES" org.eventb.core.source="/DSR2/DSR_2.bum|org.eventb.core.machineFile#DSR_2|org.eventb.core.event#T|org.eventb.core.guard#," org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="(" org.eventb.core.label="grd6" org.eventb.core.predicate="n∈dom(r)∧n∉ran(r)" org.eventb.core.source="/DSR2/DSR_2.bum|org.eventb.core.machineFile#DSR_2|org.eventb.core.event#T|org.eventb.core.guard#\/" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name=")" org.eventb.core.label="grd7" org.eventb.core.predicate="n2∈ran(r)∧n2∉dom(r)" org.eventb.core.source="/DSR2/DSR_2.bum|org.eventb.core.machineFile#DSR_2|org.eventb.core.event#T|org.eventb.core.guard#0" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="*" org.eventb.core.label="grd9" org.eventb.core.predicate="n∈dom(TableRoutage)" org.eventb.core.source="/DSR2/DSR_2.bum|org.eventb.core.machineFile#DSR_2|org.eventb.core.event#T|org.eventb.core.guard#3" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="+" org.eventb.core.label="grd11" org.eventb.core.predicate="n2 ↦ r∉TableRoutage(n)" org.eventb.core.source="/DSR2/DSR_2.bum|org.eventb.core.machineFile#DSR_2|org.eventb.core.event#T|org.eventb.core.guard#7" org.eventb.core.theorem="false"/>
        <org.eventb.core.scAction name="n3" org.eventb.core.assignment="TableRoutage ≔ TableRoutage{n ↦ {n2 ↦ r}TableRoutage(n)}" org.eventb.core.label="act1" org.eventb.core.source="/DSR2/DSR_2.bum|org.eventb.core.machineFile#DSR_2|org.eventb.core.event#T|org.eventb.core.action#5"/>
        <org.eventb.core.scParameter name="n2" org.eventb.core.source="/DSR2/DSR_2.bum|org.eventb.core.machineFile#DSR_2|org.eventb.core.event#T|org.eventb.core.parameter#(" org.eventb.core.type="NOEUDS"/>
        <org.eventb.core.scParameter name="n" org.eventb.core.source="/DSR2/DSR_2.bum|org.eventb.core.machineFile#DSR_2|org.eventb.core.event#T|org.eventb.core.parameter#'" org.eventb.core.type="NOEUDS"/>
        <org.eventb.core.scParameter name="r" org.eventb.core.source="/DSR2/DSR_2.bum|org.eventb.core.machineFile#DSR_2|org.eventb.core.event#T|org.eventb.core.parameter#)" org.eventb.core.type="ℙ(NOEUDS×NOEUDS)"/>
    </org.eventb.core.scEvent>
    <org.eventb.core.scEvent name="TableRoutagp" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="Derouter" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#a">
        <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/DSR2/DSR_2.bcm|org.eventb.core.scMachineFile#DSR_2|org.eventb.core.scEvent#TableRoutagp" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#a|org.eventb.core.refinesEvent#'"/>
        <org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="n∈dom(TableRoutage)" org.eventb.core.source="/DSR2/DSR_2.bum|org.eventb.core.machineFile#DSR_2|org.eventb.core.event#U|org.eventb.core.guard#)" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="n2∈dom(TableRoutage(n))" org.eventb.core.source="/DSR2/DSR_2.bum|org.eventb.core.machineFile#DSR_2|org.eventb.core.event#U|org.eventb.core.guard#*" org.eventb.core.theorem="false"/>
        <org.eventb.core.scAction name="n3" org.eventb.core.assignment="TableRoutage ≔ TableRoutage{n ↦ {n2} ⩤ TableRoutage(n)}" org.eventb.core.label="act1" org.eventb.core.source="/DSR2/DSR_2.bum|org.eventb.core.machineFile#DSR_2|org.eventb.core.event#U|org.eventb.core.action#+"/>
        <org.eventb.core.scParameter name="n2" org.eventb.core.source="/DSR2/DSR_2.bum|org.eventb.core.machineFile#DSR_2|org.eventb.core.event#U|org.eventb.core.parameter#(" org.eventb.core.type="NOEUDS"/>
        <org.eventb.core.scParameter name="n" org.eventb.core.source="/DSR2/DSR_2.bum|org.eventb.core.machineFile#DSR_2|org.eventb.core.event#U|org.eventb.core.parameter#'" org.eventb.core.type="NOEUDS"/>
    </org.eventb.core.scEvent>
    <org.eventb.core.scEvent name="TableRoutagq" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="EnvoyerRREQ" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#d">
        <org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="n1∈NOEUDS" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#d|org.eventb.core.guard#(" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="n2∈NOEUDS" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#d|org.eventb.core.guard#*" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name=")" org.eventb.core.label="grd3" org.eventb.core.predicate="n1∈dom(Reseau)" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#d|org.eventb.core.guard#," org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="*" org.eventb.core.label="grd4" org.eventb.core.predicate="n1≠n2" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#d|org.eventb.core.guard#-" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="+" org.eventb.core.label="grd5" org.eventb.core.predicate="n2∉dom(RREQ)" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#d|org.eventb.core.guard#." org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="," org.eventb.core.label="grd6" org.eventb.core.predicate="n2∉dom(TableRoutage(n1))" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#d|org.eventb.core.guard#0" org.eventb.core.theorem="false"/>
        <org.eventb.core.scParameter name="n1" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#d|org.eventb.core.parameter#'" org.eventb.core.type="NOEUDS"/>
        <org.eventb.core.scParameter name="n2" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#d|org.eventb.core.parameter#+" org.eventb.core.type="NOEUDS"/>
        <org.eventb.core.scAction name="n3" org.eventb.core.assignment="RREQ ≔ RREQ∪{n2 ↦ (∅ ⦂ ℙ(NOEUDS×NOEUDS))}" org.eventb.core.label="act1" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#d|org.eventb.core.action#)"/>
        <org.eventb.core.scAction name="n4" org.eventb.core.assignment="RREQTransit ≔ RREQTransit∪{n2 ↦ (∅ ⦂ ℙ(NOEUDS×NOEUDS)) ↦ {n1 ↦ Reseau[{n1}]}}" org.eventb.core.label="act2" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#d|org.eventb.core.action#\/"/>
    </org.eventb.core.scEvent>
    <org.eventb.core.scEvent name="TableRoutagr" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="StoreRREQ" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#g">
        <org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="d ↦ r∈dom(RREQTransit)" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#g|org.eventb.core.guard#)" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="(" org.eventb.core.label="grd5" org.eventb.core.predicate="from∈dom(RREQTransit(d ↦ r))" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#g|org.eventb.core.guard#0" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name=")" org.eventb.core.label="grd6" org.eventb.core.predicate="from∉dom(r)" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#g|org.eventb.core.guard#2" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="*" org.eventb.core.label="grd7" org.eventb.core.predicate="n∉dom(r)∧n∉ran(r)" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#g|org.eventb.core.guard#3" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="+" org.eventb.core.label="grd8" org.eventb.core.predicate="r≠(∅ ⦂ ℙ(NOEUDS×NOEUDS))⇒from∈ran(r)" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#g|org.eventb.core.guard#4" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="," org.eventb.core.label="grd9" org.eventb.core.predicate="n∈RREQTransit(d ↦ r)(from)" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#g|org.eventb.core.guard#5" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="-" org.eventb.core.label="grd10" org.eventb.core.predicate="r∪{from ↦ n}∈ROUTES" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#g|org.eventb.core.guard#6" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="." org.eventb.core.label="grd11" org.eventb.core.predicate="routesToClean={request⦂NOEUDS×ℙ(NOEUDS×NOEUDS)·request∈RREQ∧request∈dom(RREQTransit)∧from∈dom(RREQTransit(request))∧RREQTransit(request)(from)={n} ∣ request}" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#g|org.eventb.core.guard#8" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="/" org.eventb.core.label="grd12" org.eventb.core.predicate="card(dom(r))&lt;MaxSauts" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#g|org.eventb.core.guard#:" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="0" org.eventb.core.label="grd13" org.eventb.core.predicate="n≠d" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#g|org.eventb.core.guard#;" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="1" org.eventb.core.label="grd14" org.eventb.core.predicate="Reseau[{n}]⊈dom(r)" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#g|org.eventb.core.guard#=" org.eventb.core.theorem="false"/>
        <org.eventb.core.scParameter name="d" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#g|org.eventb.core.parameter#'" org.eventb.core.type="NOEUDS"/>
        <org.eventb.core.scParameter name="n" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#g|org.eventb.core.parameter#\/" org.eventb.core.type="NOEUDS"/>
        <org.eventb.core.scParameter name="routesToClean" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#g|org.eventb.core.parameter#7" org.eventb.core.type="ℙ(NOEUDS×ℙ(NOEUDS×NOEUDS))"/>
        <org.eventb.core.scParameter name="r" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#g|org.eventb.core.parameter#(" org.eventb.core.type="ℙ(NOEUDS×NOEUDS)"/>
        <org.eventb.core.scParameter name="from" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#g|org.eventb.core.parameter#." org.eventb.core.type="NOEUDS"/>
        <org.eventb.core.scAction name="routesToCleao" org.eventb.core.assignment="RREQTransit ≔ routesToClean ⩤ (RREQTransit{d ↦ r ↦ RREQTransit(d ↦ r){from ↦ RREQTransit(d ↦ r)(from) ∖ {n}}})" org.eventb.core.label="act2" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#g|org.eventb.core.action#1"/>
        <org.eventb.core.scAction name="routesToCleap" org.eventb.core.assignment="RREQ ≔ (RREQ∪{d ↦ r∪{from ↦ n}}) ∖ routesToClean" org.eventb.core.label="act3" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#g|org.eventb.core.action#9"/>
    </org.eventb.core.scEvent>
    <org.eventb.core.scEvent name="TableRoutags" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="RecevoirRREQ" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#j">
        <org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="d ↦ r∈dom(RREQTransit)" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#j|org.eventb.core.guard#." org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="from∈dom(RREQTransit(d ↦ r))" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#j|org.eventb.core.guard#\/" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name=")" org.eventb.core.label="grd0" org.eventb.core.predicate="n∈RREQTransit(d ↦ r)(from)" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#j|org.eventb.core.guard#0" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="*" org.eventb.core.label="grd4" org.eventb.core.predicate="routesToClean={request⦂NOEUDS×ℙ(NOEUDS×NOEUDS)·request∈RREQ∧request∈dom(RREQTransit)∧from∈dom(RREQTransit(request))∧RREQTransit(request)(from)={n} ∣ request}" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#j|org.eventb.core.guard#1" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="+" org.eventb.core.label="grd5" org.eventb.core.predicate="n=d" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#j|org.eventb.core.guard#2" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="," org.eventb.core.label="grd6" org.eventb.core.predicate="r∪{from ↦ n}∈ROUTES" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#j|org.eventb.core.guard#internal3" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="-" org.eventb.core.label="grd7" org.eventb.core.predicate="(r∪{from ↦ n})∼∈ROUTES" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#j|org.eventb.core.guard#internal4" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="." org.eventb.core.label="grd8" org.eventb.core.predicate="(r∪{from ↦ n})∼ ↦ n∉RREP" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#j|org.eventb.core.guard#internal5" org.eventb.core.theorem="false"/>
        <org.eventb.core.scParameter name="d" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#j|org.eventb.core.parameter#(" org.eventb.core.type="NOEUDS"/>
        <org.eventb.core.scParameter name="n" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#j|org.eventb.core.parameter#internal1" org.eventb.core.type="NOEUDS"/>
        <org.eventb.core.scParameter name="routesToClean" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#j|org.eventb.core.parameter#+" org.eventb.core.type="ℙ(NOEUDS×ℙ(NOEUDS×NOEUDS))"/>
        <org.eventb.core.scParameter name="r" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#j|org.eventb.core.parameter#internal2" org.eventb.core.type="ℙ(NOEUDS×NOEUDS)"/>
        <org.eventb.core.scParameter name="from" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#j|org.eventb.core.parameter#)" org.eventb.core.type="NOEUDS"/>
        <org.eventb.core.scAction name="routesToCleao" org.eventb.core.assignment="RREQTransit ≔ routesToClean ⩤ (RREQTransit{d ↦ r ↦ RREQTransit(d ↦ r){from ↦ RREQTransit(d ↦ r)(from) ∖ {n}}})" org.eventb.core.label="act1" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#j|org.eventb.core.action#,"/>
        <org.eventb.core.scAction name="routesToCleap" org.eventb.core.assignment="RREQ ≔ RREQ ∖ routesToClean" org.eventb.core.label="act2" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#j|org.eventb.core.action#-"/>
        <org.eventb.core.scAction name="routesToCleaq" org.eventb.core.assignment="RREP ≔ RREP∪{(r∪{from ↦ n})∼ ↦ n}" org.eventb.core.label="act3" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#j|org.eventb.core.action#3"/>
        <org.eventb.core.scAction name="routesToClear" org.eventb.core.assignment="RREPTransit ≔ RREPTransit∪{(r∪{from ↦ n})∼ ↦ n}" org.eventb.core.label="act4" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#j|org.eventb.core.action#4"/>
    </org.eventb.core.scEvent>
    <org.eventb.core.scEvent name="TableRoutagt" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="RejectRREQ" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#i">
        <org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="d ↦ r∈dom(RREQTransit)" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#i|org.eventb.core.guard#+" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="(" org.eventb.core.label="grd3" org.eventb.core.predicate="card(dom(r))=MaxSauts∨n∈dom(r)∨(Reseau[{n}]⊆dom(r)∧n≠d)" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#i|org.eventb.core.guard#-" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name=")" org.eventb.core.label="grd4" org.eventb.core.predicate="from∈dom(RREQTransit(d ↦ r))" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#i|org.eventb.core.guard#\/" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="*" org.eventb.core.label="grd5" org.eventb.core.predicate="n∈RREQTransit(d ↦ r)(from)" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#i|org.eventb.core.guard#0" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="+" org.eventb.core.label="grd6" org.eventb.core.predicate="routesToClean={request⦂NOEUDS×ℙ(NOEUDS×NOEUDS)·request∈RREQ∧request∈dom(RREQTransit)∧from∈dom(RREQTransit(request))∧RREQTransit(request)(from)={n} ∣ request}" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#i|org.eventb.core.guard#1" org.eventb.core.theorem="false"/>
        <org.eventb.core.scParameter name="d" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#i|org.eventb.core.parameter#'" org.eventb.core.type="NOEUDS"/>
        <org.eventb.core.scParameter name="n" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#i|org.eventb.core.parameter#*" org.eventb.core.type="NOEUDS"/>
        <org.eventb.core.scParameter name="routesToClean" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#i|org.eventb.core.parameter#2" org.eventb.core.type="ℙ(NOEUDS×ℙ(NOEUDS×NOEUDS))"/>
        <org.eventb.core.scParameter name="r" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#i|org.eventb.core.parameter#(" org.eventb.core.type="ℙ(NOEUDS×NOEUDS)"/>
        <org.eventb.core.scParameter name="from" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#i|org.eventb.core.parameter#)" org.eventb.core.type="NOEUDS"/>
        <org.eventb.core.scAction name="routesToCleao" org.eventb.core.assignment="RREQTransit ≔ routesToClean ⩤ (RREQTransit{d ↦ r ↦ RREQTransit(d ↦ r){from ↦ RREQTransit(d ↦ r)(from) ∖ {n}}})" org.eventb.core.label="act1" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#i|org.eventb.core.action#."/>
        <org.eventb.core.scAction name="routesToCleap" org.eventb.core.assignment="RREQ ≔ RREQ ∖ routesToClean" org.eventb.core.label="act2" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#i|org.eventb.core.action#3"/>
    </org.eventb.core.scEvent>
    <org.eventb.core.scEvent name="TableRoutagu" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="ForwardRREQ" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#h">
        <org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="d ↦ r∈RREQ" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#h|org.eventb.core.guard#*" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="n∈ran(r) ∖ dom(r)" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#h|org.eventb.core.guard#+" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name=")" org.eventb.core.label="grd6" org.eventb.core.predicate="d ↦ r∉dom(RREQTransit)∨(d ↦ r∈dom(RREQTransit)∧n∉dom(RREQTransit(d ↦ r)))" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#h|org.eventb.core.guard#0" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="*" org.eventb.core.label="grd7" org.eventb.core.predicate="RREQTransit∪{d ↦ r ↦ {n ↦ Reseau[{n}]}}∈RREQ ⇸ (NOEUDS ⇸ ℙ(NOEUDS))" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#h|org.eventb.core.guard#1" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="+" org.eventb.core.label="grd8" org.eventb.core.predicate="Reseau[{n}]≠(∅ ⦂ ℙ(NOEUDS))" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#h|org.eventb.core.guard#2" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="," org.eventb.core.label="grd9" org.eventb.core.predicate="n≠d" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#h|org.eventb.core.guard#3" org.eventb.core.theorem="false"/>
        <org.eventb.core.scParameter name="d" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#h|org.eventb.core.parameter#'" org.eventb.core.type="NOEUDS"/>
        <org.eventb.core.scParameter name="n" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#h|org.eventb.core.parameter#)" org.eventb.core.type="NOEUDS"/>
        <org.eventb.core.scParameter name="r" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#h|org.eventb.core.parameter#(" org.eventb.core.type="ℙ(NOEUDS×NOEUDS)"/>
        <org.eventb.core.scAction name="s" org.eventb.core.assignment="RREQTransit ≔ RREQTransit∪{d ↦ r ↦ {n ↦ Reseau[{n}]}}" org.eventb.core.label="act1" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#h|org.eventb.core.action#."/>
    </org.eventb.core.scEvent>
    <org.eventb.core.scEvent name="TableRoutagv" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="PerdreRREQ" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#k">
        <org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="d ↦ r∈dom(RREQTransit)" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#k|org.eventb.core.guard#," org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="from∈dom(RREQTransit(d ↦ r))" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#k|org.eventb.core.guard#-" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name=")" org.eventb.core.label="grd3" org.eventb.core.predicate="n∈RREQTransit(d ↦ r)(from)" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#k|org.eventb.core.guard#." org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="*" org.eventb.core.label="grd4" org.eventb.core.predicate="routesToClean={request⦂NOEUDS×ℙ(NOEUDS×NOEUDS)·request∈RREQ∧request∈dom(RREQTransit)∧from∈dom(RREQTransit(request))∧RREQTransit(request)(from)={n} ∣ request}" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#k|org.eventb.core.guard#0" org.eventb.core.theorem="false"/>
        <org.eventb.core.scParameter name="d" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#k|org.eventb.core.parameter#(" org.eventb.core.type="NOEUDS"/>
        <org.eventb.core.scParameter name="n" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#k|org.eventb.core.parameter#+" org.eventb.core.type="NOEUDS"/>
        <org.eventb.core.scParameter name="routesToClean" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#k|org.eventb.core.parameter#\/" org.eventb.core.type="ℙ(NOEUDS×ℙ(NOEUDS×NOEUDS))"/>
        <org.eventb.core.scParameter name="r" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#k|org.eventb.core.parameter#)" org.eventb.core.type="ℙ(NOEUDS×NOEUDS)"/>
        <org.eventb.core.scParameter name="from" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#k|org.eventb.core.parameter#*" org.eventb.core.type="NOEUDS"/>
        <org.eventb.core.scAction name="routesToCleao" org.eventb.core.assignment="RREQTransit ≔ routesToClean ⩤ (RREQTransit{d ↦ r ↦ RREQTransit(d ↦ r){from ↦ RREQTransit(d ↦ r)(from) ∖ {n}}})" org.eventb.core.label="act1" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#k|org.eventb.core.action#'"/>
        <org.eventb.core.scAction name="routesToCleap" org.eventb.core.assignment="RREQ ≔ RREQ ∖ routesToClean" org.eventb.core.label="act2" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#k|org.eventb.core.action#1"/>
    </org.eventb.core.scEvent>
    <org.eventb.core.scEvent name="TableRoutagw" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="StoreRREP" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#p">
        <org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="r ↦ n1∈RREP" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#p|org.eventb.core.guard#*" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="n1∈dom(r)" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#p|org.eventb.core.guard#+" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name=")" org.eventb.core.label="grd3" org.eventb.core.predicate="n1 ↦ n2∈Reseau" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#p|org.eventb.core.guard#." org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="*" org.eventb.core.label="grd4" org.eventb.core.predicate="r∈dom(RREPTransit)" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#p|org.eventb.core.guard#\/" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="+" org.eventb.core.label="grd5" org.eventb.core.predicate="n2=r(n1)" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#p|org.eventb.core.guard#0" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="," org.eventb.core.label="grd6" org.eventb.core.predicate="s∈ran(r) ∖ dom(r)" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#p|org.eventb.core.guard#2" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="-" org.eventb.core.label="grd7" org.eventb.core.predicate="n2≠s" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#p|org.eventb.core.guard#3" org.eventb.core.theorem="false"/>
        <org.eventb.core.scParameter name="n1" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#p|org.eventb.core.parameter#'" org.eventb.core.type="NOEUDS"/>
        <org.eventb.core.scParameter name="n2" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#p|org.eventb.core.parameter#(" org.eventb.core.type="NOEUDS"/>
        <org.eventb.core.scParameter name="r" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#p|org.eventb.core.parameter#)" org.eventb.core.type="ℙ(NOEUDS×NOEUDS)"/>
        <org.eventb.core.scParameter name="s" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#p|org.eventb.core.parameter#1" org.eventb.core.type="NOEUDS"/>
        <org.eventb.core.scAction name="n3" org.eventb.core.assignment="RREP ≔ RREP{r ↦ n2}" org.eventb.core.label="act1" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#p|org.eventb.core.action#,"/>
        <org.eventb.core.scAction name="n4" org.eventb.core.assignment="RREPTransit ≔ {r} ⩤ RREPTransit" org.eventb.core.label="act2" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#p|org.eventb.core.action#-"/>
    </org.eventb.core.scEvent>
    <org.eventb.core.scEvent name="TableRoutagx" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="ForwardRREP" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#q">
        <org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="r ↦ n1∈RREP" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#q|org.eventb.core.guard#*" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="(" org.eventb.core.label="grd3" org.eventb.core.predicate="r∉dom(RREPTransit)" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#q|org.eventb.core.guard#." org.eventb.core.theorem="false"/>
        <org.eventb.core.scParameter name="n1" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#q|org.eventb.core.parameter#'" org.eventb.core.type="NOEUDS"/>
        <org.eventb.core.scParameter name="r" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#q|org.eventb.core.parameter#)" org.eventb.core.type="ℙ(NOEUDS×NOEUDS)"/>
        <org.eventb.core.scAction name="n2" org.eventb.core.assignment="RREPTransit ≔ {r ↦ n1}∪RREPTransit" org.eventb.core.label="act2" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#q|org.eventb.core.action#-"/>
    </org.eventb.core.scEvent>
    <org.eventb.core.scEvent name="TableRoutagy" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="PerdreRREP" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#r">
        <org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="r ↦ n1∈RREP" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#r|org.eventb.core.guard#)" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="r∈dom(RREPTransit)" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#r|org.eventb.core.guard#," org.eventb.core.theorem="false"/>
        <org.eventb.core.scParameter name="n1" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#r|org.eventb.core.parameter#(" org.eventb.core.type="NOEUDS"/>
        <org.eventb.core.scParameter name="r" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#r|org.eventb.core.parameter#'" org.eventb.core.type="ℙ(NOEUDS×NOEUDS)"/>
        <org.eventb.core.scAction name="n2" org.eventb.core.assignment="RREPTransit ≔ {r} ⩤ RREPTransit" org.eventb.core.label="act1" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#r|org.eventb.core.action#*"/>
        <org.eventb.core.scAction name="n3" org.eventb.core.assignment="RREP ≔ {r} ⩤ RREP" org.eventb.core.label="act2" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#r|org.eventb.core.action#+"/>
    </org.eventb.core.scEvent>
    <org.eventb.core.scEvent name="TableRoutagz" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="RecevoirRREP" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#s">
        <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/DSR2/DSR_2.bcm|org.eventb.core.scMachineFile#DSR_2|org.eventb.core.scEvent#TableRoutago" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#s|org.eventb.core.refinesEvent#2"/>
        <org.eventb.core.scGuard name="(" org.eventb.core.label="grd1" org.eventb.core.predicate="r∼ ↦ n1∈RREP" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#s|org.eventb.core.guard#*" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name=")" org.eventb.core.label="grd2" org.eventb.core.predicate="r∼∈dom(RREPTransit)" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#s|org.eventb.core.guard#," org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="*" org.eventb.core.label="grd3" org.eventb.core.predicate="s∈dom(r) ∖ ran(r)" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#s|org.eventb.core.guard#-" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="+" org.eventb.core.label="grd4" org.eventb.core.predicate="d∈ran(r) ∖ dom(r)" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#s|org.eventb.core.guard#." org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="," org.eventb.core.label="grd5" org.eventb.core.predicate="n1∈dom(r∼)" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#s|org.eventb.core.guard#5" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="-" org.eventb.core.label="grd6" org.eventb.core.predicate="r∼(n1)=s" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#s|org.eventb.core.guard#6" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="." org.eventb.core.label="grd7" org.eventb.core.predicate="r∈ROUTES" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#s|org.eventb.core.guard#7" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="/" org.eventb.core.label="grd8" org.eventb.core.predicate="d ↦ r∉TableRoutage(s)" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#s|org.eventb.core.guard#8" org.eventb.core.theorem="false"/>
        <org.eventb.core.scParameter name="n1" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#s|org.eventb.core.parameter#'" org.eventb.core.type="NOEUDS"/>
        <org.eventb.core.scParameter name="d" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#s|org.eventb.core.parameter#(" org.eventb.core.type="NOEUDS"/>
        <org.eventb.core.scParameter name="r" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#s|org.eventb.core.parameter#)" org.eventb.core.type="ℙ(NOEUDS×NOEUDS)"/>
        <org.eventb.core.scParameter name="s" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#s|org.eventb.core.parameter#+" org.eventb.core.type="NOEUDS"/>
        <org.eventb.core.scAction name="n2" org.eventb.core.assignment="RREP ≔ {r∼} ⩤ RREP" org.eventb.core.label="act1" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#s|org.eventb.core.action#\/"/>
        <org.eventb.core.scAction name="n3" org.eventb.core.assignment="RREPTransit ≔ {r∼} ⩤ RREPTransit" org.eventb.core.label="act2" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#s|org.eventb.core.action#0"/>
        <org.eventb.core.scAction name="n4" org.eventb.core.assignment="TableRoutage ≔ TableRoutage{s ↦ {d ↦ r}TableRoutage(s)}" org.eventb.core.label="act3" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#s|org.eventb.core.action#1"/>
        <org.eventb.core.scWitness name="n5" org.eventb.core.label="n" org.eventb.core.predicate="n=s" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#s|org.eventb.core.witness#3"/>
        <org.eventb.core.scWitness name="n6" org.eventb.core.label="n2" org.eventb.core.predicate="n2=d" org.eventb.core.source="/DSR2/DSR_3.bum|org.eventb.core.machineFile#DSR_3|org.eventb.core.event#s|org.eventb.core.witness#4"/>
    </org.eventb.core.scEvent>
</org.eventb.core.scMachineFile>