Dynamic-Source-Routing-Protocol/DSR_0.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
<?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.scSeesContext name="'" org.eventb.core.scTarget="/DSR2/DSR_ctx_0.bcc" org.eventb.core.source="/DSR2/DSR_0.bum|org.eventb.core.machineFile#DSR_0|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.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.scVariable name="DonneesGros" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/DSR2/DSR_0.bum|org.eventb.core.machineFile#DSR_0|org.eventb.core.variable#9" org.eventb.core.type="ℙ(DONNEES)"/>
    <org.eventb.core.scVariable name="EnvoiVers" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/DSR2/DSR_0.bum|org.eventb.core.machineFile#DSR_0|org.eventb.core.variable#3" org.eventb.core.type="ℙ(DONNEES×(NOEUDS×NOEUDS))"/>
    <org.eventb.core.scVariable name="Reseau" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/DSR2/DSR_0.bum|org.eventb.core.machineFile#DSR_0|org.eventb.core.variable#)" org.eventb.core.type="ℙ(NOEUDS×NOEUDS)"/>
    <org.eventb.core.scVariable name="StockNoeud" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/DSR2/DSR_0.bum|org.eventb.core.machineFile#DSR_0|org.eventb.core.variable#0" org.eventb.core.type="ℙ(DONNEES×NOEUDS)"/>
    <org.eventb.core.scEvent name="DonneesGrot" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="INITIALISATION" org.eventb.core.source="/DSR2/DSR_0.bum|org.eventb.core.machineFile#DSR_0|org.eventb.core.event#'">
        <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.scEvent>
    <org.eventb.core.scEvent name="DonneesGrou" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="Lier" org.eventb.core.source="/DSR2/DSR_0.bum|org.eventb.core.machineFile#DSR_0|org.eventb.core.event#+">
        <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.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.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.scEvent>
    <org.eventb.core.scEvent name="DonneesGrov" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="Delier" org.eventb.core.source="/DSR2/DSR_0.bum|org.eventb.core.machineFile#DSR_0|org.eventb.core.event#.">
        <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.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.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.scEvent>
    <org.eventb.core.scEvent name="DonneesGrow" 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_0.bum|org.eventb.core.machineFile#DSR_0|org.eventb.core.event#\/">
        <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.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.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.scEvent>
    <org.eventb.core.scEvent name="DonneesGrox" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="Produire" org.eventb.core.source="/DSR2/DSR_0.bum|org.eventb.core.machineFile#DSR_0|org.eventb.core.event#2">
        <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.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.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.scEvent>
    <org.eventb.core.scEvent name="DonneesGroy" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="Perdre" org.eventb.core.source="/DSR2/DSR_0.bum|org.eventb.core.machineFile#DSR_0|org.eventb.core.event#6">
        <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.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.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.scEvent>
    <org.eventb.core.scEvent name="DonneesGroz" 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_0.bum|org.eventb.core.machineFile#DSR_0|org.eventb.core.event#7">
        <org.eventb.core.scGuard name="'" org.eventb.core.label="grd2" 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#7|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#7|org.eventb.core.guard#-" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name=")" org.eventb.core.label="grd4" 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#7|org.eventb.core.guard#." org.eventb.core.theorem="false"/>
        <org.eventb.core.scParameter name="data" org.eventb.core.source="/DSR2/DSR_0.bum|org.eventb.core.machineFile#DSR_0|org.eventb.core.event#7|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_0.bum|org.eventb.core.machineFile#DSR_0|org.eventb.core.event#7|org.eventb.core.action#*"/>
        <org.eventb.core.scAction name="datc" org.eventb.core.assignment="DonneesGros ≔ DonneesGros∪{data}" org.eventb.core.label="act2" org.eventb.core.source="/DSR2/DSR_0.bum|org.eventb.core.machineFile#DSR_0|org.eventb.core.event#7|org.eventb.core.action#\/"/>
    </org.eventb.core.scEvent>
    <org.eventb.core.scEvent name="DonneesGro{" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="Store" org.eventb.core.source="/DSR2/DSR_0.bum|org.eventb.core.machineFile#DSR_0|org.eventb.core.event#8">
        <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.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.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.scEvent>
</org.eventb.core.scMachineFile>