Dynamic-Source-Routing-Protocol/DSR_2.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
<?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_1.bcm" org.eventb.core.source="/DSR2/DSR_2.bum|org.eventb.core.machineFile#DSR_2|org.eventb.core.refinesMachine#'"/>
    <org.eventb.core.scSeesContext name="(" org.eventb.core.scTarget="/DSR2/DSR_ctx_1.bcc" org.eventb.core.source="/DSR2/DSR_2.bum|org.eventb.core.machineFile#DSR_2|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.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.scVariable name="DonneesRoute" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/DSR2/DSR_2.bum|org.eventb.core.machineFile#DSR_2|org.eventb.core.variable#B" org.eventb.core.type="ℙ(DONNEES×ℙ(NOEUDS×NOEUDS))"/>
    <org.eventb.core.scVariable name="DonneesGros" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/DSR2/DSR_2.bum|org.eventb.core.machineFile#DSR_2|org.eventb.core.variable#V" org.eventb.core.type="ℙ(DONNEES)"/>
    <org.eventb.core.scVariable name="EnvoiVers" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/DSR2/DSR_2.bum|org.eventb.core.machineFile#DSR_2|org.eventb.core.variable#3" org.eventb.core.type="ℙ(DONNEES×(NOEUDS×NOEUDS))"/>
    <org.eventb.core.scVariable name="TableRoutage" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/DSR2/DSR_2.bum|org.eventb.core.machineFile#DSR_2|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_2.bum|org.eventb.core.machineFile#DSR_2|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_2.bum|org.eventb.core.machineFile#DSR_2|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_2.bum|org.eventb.core.machineFile#DSR_2|org.eventb.core.event#C">
        <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/DSR2/DSR_1.bcm|org.eventb.core.scMachineFile#DSR_1|org.eventb.core.scEvent#DonneesRoutf" org.eventb.core.source="/DSR2/DSR_2.bum|org.eventb.core.machineFile#DSR_2|org.eventb.core.event#C"/>
        <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.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_2.bum|org.eventb.core.machineFile#DSR_2|org.eventb.core.event#D">
        <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/DSR2/DSR_1.bcm|org.eventb.core.scMachineFile#DSR_1|org.eventb.core.scEvent#DonneesRoutg" org.eventb.core.source="/DSR2/DSR_2.bum|org.eventb.core.machineFile#DSR_2|org.eventb.core.event#D|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.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.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.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="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.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_2.bum|org.eventb.core.machineFile#DSR_2|org.eventb.core.event#E">
        <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/DSR2/DSR_1.bcm|org.eventb.core.scMachineFile#DSR_1|org.eventb.core.scEvent#DonneesRouth" org.eventb.core.source="/DSR2/DSR_2.bum|org.eventb.core.machineFile#DSR_2|org.eventb.core.event#E|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.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.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.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="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.scEvent>
    <org.eventb.core.scEvent name="TableRoutagi" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="Envoyer" org.eventb.core.source="/DSR2/DSR_2.bum|org.eventb.core.machineFile#DSR_2|org.eventb.core.event#F">
        <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/DSR2/DSR_1.bcm|org.eventb.core.scMachineFile#DSR_1|org.eventb.core.scEvent#DonneesRouti" org.eventb.core.source="/DSR2/DSR_2.bum|org.eventb.core.machineFile#DSR_2|org.eventb.core.event#F|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.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.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.scWitness name="date" org.eventb.core.label="r" org.eventb.core.predicate="r=TableRoutage(StockNoeud(data))(n)" org.eventb.core.source="/DSR2/DSR_2.bum|org.eventb.core.machineFile#DSR_2|org.eventb.core.event#F|org.eventb.core.witness#internal;"/>
    </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_2.bum|org.eventb.core.machineFile#DSR_2|org.eventb.core.event#G">
        <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/DSR2/DSR_1.bcm|org.eventb.core.scMachineFile#DSR_1|org.eventb.core.scEvent#DonneesRoutj" org.eventb.core.source="/DSR2/DSR_2.bum|org.eventb.core.machineFile#DSR_2|org.eventb.core.event#G|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_2.bum|org.eventb.core.machineFile#DSR_2|org.eventb.core.event#H">
        <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/DSR2/DSR_1.bcm|org.eventb.core.scMachineFile#DSR_1|org.eventb.core.scEvent#DonneesRoutk" org.eventb.core.source="/DSR2/DSR_2.bum|org.eventb.core.machineFile#DSR_2|org.eventb.core.event#H|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_2.bum|org.eventb.core.machineFile#DSR_2|org.eventb.core.event#I">
        <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/DSR2/DSR_1.bcm|org.eventb.core.scMachineFile#DSR_1|org.eventb.core.scEvent#DonneesRoutl" org.eventb.core.source="/DSR2/DSR_2.bum|org.eventb.core.machineFile#DSR_2|org.eventb.core.event#I|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_2.bum|org.eventb.core.machineFile#DSR_2|org.eventb.core.event#J">
        <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/DSR2/DSR_1.bcm|org.eventb.core.scMachineFile#DSR_1|org.eventb.core.scEvent#DonneesRoutm" org.eventb.core.source="/DSR2/DSR_2.bum|org.eventb.core.machineFile#DSR_2|org.eventb.core.event#J|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_2.bum|org.eventb.core.machineFile#DSR_2|org.eventb.core.event#K">
        <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/DSR2/DSR_1.bcm|org.eventb.core.scMachineFile#DSR_1|org.eventb.core.scEvent#DonneesRoutn" org.eventb.core.source="/DSR2/DSR_2.bum|org.eventb.core.machineFile#DSR_2|org.eventb.core.event#K|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="false" org.eventb.core.label="Router" org.eventb.core.source="/DSR2/DSR_2.bum|org.eventb.core.machineFile#DSR_2|org.eventb.core.event#T">
        <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.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.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.scEvent>
    <org.eventb.core.scEvent name="TableRoutagp" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="Derouter" org.eventb.core.source="/DSR2/DSR_2.bum|org.eventb.core.machineFile#DSR_2|org.eventb.core.event#U">
        <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.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.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.scEvent>
</org.eventb.core.scMachineFile>