Dynamic-Source-Routing-Protocol/DSR_1.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
<?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_0.bcm" org.eventb.core.source="/DSR2/DSR_1.bum|org.eventb.core.machineFile#DSR_1|org.eventb.core.refinesMachine#'"/>
    <org.eventb.core.scSeesContext name="(" org.eventb.core.scTarget="/DSR2/DSR_ctx_1.bcc" org.eventb.core.source="/DSR2/DSR_1.bum|org.eventb.core.machineFile#DSR_1|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.scVariable name="DonneesRoute" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/DSR2/DSR_1.bum|org.eventb.core.machineFile#DSR_1|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_1.bum|org.eventb.core.machineFile#DSR_1|org.eventb.core.variable#D" 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_1.bum|org.eventb.core.machineFile#DSR_1|org.eventb.core.variable#3" org.eventb.core.type="ℙ(DONNEES×(NOEUDS×NOEUDS))"/>
    <org.eventb.core.scVariable name="Reseau" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/DSR2/DSR_1.bum|org.eventb.core.machineFile#DSR_1|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_1.bum|org.eventb.core.machineFile#DSR_1|org.eventb.core.variable#0" org.eventb.core.type="ℙ(DONNEES×NOEUDS)"/>
    <org.eventb.core.scEvent name="DonneesRoutf" 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_1.bum|org.eventb.core.machineFile#DSR_1|org.eventb.core.event#4">
        <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/DSR2/DSR_0.bcm|org.eventb.core.scMachineFile#DSR_0|org.eventb.core.scEvent#DonneesGrot" org.eventb.core.source="/DSR2/DSR_1.bum|org.eventb.core.machineFile#DSR_1|org.eventb.core.event#4"/>
        <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.scEvent>
    <org.eventb.core.scEvent name="DonneesRoutg" 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_1.bum|org.eventb.core.machineFile#DSR_1|org.eventb.core.event#5">
        <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/DSR2/DSR_0.bcm|org.eventb.core.scMachineFile#DSR_0|org.eventb.core.scEvent#DonneesGrou" org.eventb.core.source="/DSR2/DSR_1.bum|org.eventb.core.machineFile#DSR_1|org.eventb.core.event#5|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.scEvent>
    <org.eventb.core.scEvent name="DonneesRouth" 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_1.bum|org.eventb.core.machineFile#DSR_1|org.eventb.core.event#6">
        <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/DSR2/DSR_0.bcm|org.eventb.core.scMachineFile#DSR_0|org.eventb.core.scEvent#DonneesGrov" org.eventb.core.source="/DSR2/DSR_1.bum|org.eventb.core.machineFile#DSR_1|org.eventb.core.event#6|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.scEvent>
    <org.eventb.core.scEvent name="DonneesRouti" 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_1.bum|org.eventb.core.machineFile#DSR_1|org.eventb.core.event#7">
        <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/DSR2/DSR_0.bcm|org.eventb.core.scMachineFile#DSR_0|org.eventb.core.scEvent#DonneesGrow" org.eventb.core.source="/DSR2/DSR_1.bum|org.eventb.core.machineFile#DSR_1|org.eventb.core.event#7|org.eventb.core.refinesEvent#internal5"/>
        <org.eventb.core.scGuard name="(" org.eventb.core.label="grd1" 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#7|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#7|org.eventb.core.guard#internal1" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="*" org.eventb.core.label="grd6" org.eventb.core.predicate="r∈ROUTES" org.eventb.core.source="/DSR2/DSR_1.bum|org.eventb.core.machineFile#DSR_1|org.eventb.core.event#7|org.eventb.core.guard#1" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="+" org.eventb.core.label="grd14" org.eventb.core.predicate="StockNoeud(data)∈dom(r)∧StockNoeud(data)∉ran(r)" org.eventb.core.source="/DSR2/DSR_1.bum|org.eventb.core.machineFile#DSR_1|org.eventb.core.event#7|org.eventb.core.guard#internal2" 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_1.bum|org.eventb.core.machineFile#DSR_1|org.eventb.core.event#7|org.eventb.core.guard#internal4" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="-" org.eventb.core.label="grd17" org.eventb.core.predicate="r⊆Reseau" org.eventb.core.source="/DSR2/DSR_1.bum|org.eventb.core.machineFile#DSR_1|org.eventb.core.event#7|org.eventb.core.guard#internal9" org.eventb.core.theorem="false"/>
        <org.eventb.core.scParameter name="data" org.eventb.core.source="/DSR2/DSR_1.bum|org.eventb.core.machineFile#DSR_1|org.eventb.core.event#7|org.eventb.core.parameter#'" org.eventb.core.type="DONNEES"/>
        <org.eventb.core.scParameter name="r" org.eventb.core.source="/DSR2/DSR_1.bum|org.eventb.core.machineFile#DSR_1|org.eventb.core.event#7|org.eventb.core.parameter#)" org.eventb.core.type="ℙ(NOEUDS×NOEUDS)"/>
        <org.eventb.core.scAction name="datb" org.eventb.core.assignment="DonneesRoute ≔ DonneesRoute∪{data ↦ r}" org.eventb.core.label="act3" org.eventb.core.source="/DSR2/DSR_1.bum|org.eventb.core.machineFile#DSR_1|org.eventb.core.event#7|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_1.bum|org.eventb.core.machineFile#DSR_1|org.eventb.core.event#7|org.eventb.core.action#internal6"/>
        <org.eventb.core.scAction name="datd" org.eventb.core.assignment="EnvoiVers ≔ EnvoiVers∪{data ↦ (StockNoeud(data) ↦ r(StockNoeud(data)))}" org.eventb.core.label="act5" org.eventb.core.source="/DSR2/DSR_1.bum|org.eventb.core.machineFile#DSR_1|org.eventb.core.event#7|org.eventb.core.action#internal7"/>
        <org.eventb.core.scWitness name="date" org.eventb.core.label="n" org.eventb.core.predicate="n=r(StockNoeud(data))" org.eventb.core.source="/DSR2/DSR_1.bum|org.eventb.core.machineFile#DSR_1|org.eventb.core.event#7|org.eventb.core.witness#internal8"/>
    </org.eventb.core.scEvent>
    <org.eventb.core.scEvent name="DonneesRoutj" 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_1.bum|org.eventb.core.machineFile#DSR_1|org.eventb.core.event#8">
        <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/DSR2/DSR_0.bcm|org.eventb.core.scMachineFile#DSR_0|org.eventb.core.scEvent#DonneesGrox" org.eventb.core.source="/DSR2/DSR_1.bum|org.eventb.core.machineFile#DSR_1|org.eventb.core.event#8|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="DonneesRoutk" 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_1.bum|org.eventb.core.machineFile#DSR_1|org.eventb.core.event#9">
        <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/DSR2/DSR_0.bcm|org.eventb.core.scMachineFile#DSR_0|org.eventb.core.scEvent#DonneesGroy" org.eventb.core.source="/DSR2/DSR_1.bum|org.eventb.core.machineFile#DSR_1|org.eventb.core.event#9|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.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.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.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="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.scEvent>
    <org.eventb.core.scEvent name="DonneesRoutl" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="Recevoir" org.eventb.core.source="/DSR2/DSR_1.bum|org.eventb.core.machineFile#DSR_1|org.eventb.core.event#:">
        <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/DSR2/DSR_0.bcm|org.eventb.core.scMachineFile#DSR_0|org.eventb.core.scEvent#DonneesGroz" org.eventb.core.source="/DSR2/DSR_1.bum|org.eventb.core.machineFile#DSR_1|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.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.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.scEvent>
    <org.eventb.core.scEvent name="DonneesRoutm" 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_1.bum|org.eventb.core.machineFile#DSR_1|org.eventb.core.event#?">
        <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/DSR2/DSR_0.bcm|org.eventb.core.scMachineFile#DSR_0|org.eventb.core.scEvent#DonneesGro{" org.eventb.core.source="/DSR2/DSR_1.bum|org.eventb.core.machineFile#DSR_1|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.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.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.scEvent>
    <org.eventb.core.scEvent name="DonneesRoutn" 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_1.bum|org.eventb.core.machineFile#DSR_1|org.eventb.core.event#C">
        <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/DSR2/DSR_0.bcm|org.eventb.core.scMachineFile#DSR_0|org.eventb.core.scEvent#DonneesGrow" org.eventb.core.source="/DSR2/DSR_1.bum|org.eventb.core.machineFile#DSR_1|org.eventb.core.event#C|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.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.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.scEvent>
</org.eventb.core.scMachineFile>