Dynamic-Source-Routing-Protocol/DSR_0.bum 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
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.machineFile org.eventb.core.configuration="org.eventb.core.fwd" version="5">
    <org.eventb.core.event name="'" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="INITIALISATION">
        <org.eventb.core.action name="'" org.eventb.core.assignment="Reseau≔∅" org.eventb.core.label="act1"/>
        <org.eventb.core.action name="(" org.eventb.core.assignment="StockNoeud≔∅" org.eventb.core.label="act2"/>
        <org.eventb.core.action name=")" org.eventb.core.assignment="EnvoiVers≔∅" org.eventb.core.label="act3"/>
        <org.eventb.core.action name="*" org.eventb.core.assignment="DonneesGros≔∅" org.eventb.core.label="act4"/>
    </org.eventb.core.event>
    <org.eventb.core.seesContext name="(" org.eventb.core.target="DSR_ctx_0"/>
    <org.eventb.core.variable name=")" org.eventb.core.identifier="Reseau"/>
    <org.eventb.core.invariant name="*" org.eventb.core.label="inv1" org.eventb.core.predicate="Reseau∈NOEUDS↔NOEUDS"/>
    <org.eventb.core.event name="+" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="Lier">
        <org.eventb.core.parameter name="'" org.eventb.core.identifier="n1"/>
        <org.eventb.core.parameter name="(" org.eventb.core.identifier="n2"/>
        <org.eventb.core.guard name=")" org.eventb.core.label="grd1" org.eventb.core.predicate="n1∈NOEUDS"/>
        <org.eventb.core.guard name="*" org.eventb.core.label="grd2" org.eventb.core.predicate="n2∈NOEUDS"/>
        <org.eventb.core.guard name="+" org.eventb.core.label="grd3" org.eventb.core.predicate="n1≠n2"/>
        <org.eventb.core.action name="," org.eventb.core.assignment="Reseau≔Reseau∪{n1↦n2}" org.eventb.core.label="act1"/>
        <org.eventb.core.guard name="-" org.eventb.core.label="grd4" org.eventb.core.predicate="n1↦n2∉Reseau"/>
    </org.eventb.core.event>
    <org.eventb.core.invariant name="," org.eventb.core.label="inv2" org.eventb.core.predicate="Reseau∩id=∅"/>
    <org.eventb.core.invariant name="-" org.eventb.core.label="inv3" org.eventb.core.predicate="∀s1,s2·s1↦s2∈Reseau⇒s2≠s1" org.eventb.core.theorem="true"/>
    <org.eventb.core.event name="." org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="Delier">
        <org.eventb.core.parameter name="'" org.eventb.core.identifier="n1"/>
        <org.eventb.core.parameter name="(" org.eventb.core.identifier="n2"/>
        <org.eventb.core.guard name=")" org.eventb.core.label="grd1" org.eventb.core.predicate="n1↦n2∈Reseau"/>
        <org.eventb.core.action name="*" org.eventb.core.assignment="Reseau≔Reseau∖{n1↦n2}" org.eventb.core.label="act1"/>
        <org.eventb.core.guard name="+" org.eventb.core.label="grd2" org.eventb.core.predicate="n1≠n2"/>
    </org.eventb.core.event>
    <org.eventb.core.event name="/" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="Envoyer">
        <org.eventb.core.parameter name="'" org.eventb.core.identifier="data"/>
        <org.eventb.core.parameter name=")" org.eventb.core.identifier="n"/>
        <org.eventb.core.guard name="*" org.eventb.core.label="grd1" org.eventb.core.predicate="data∈dom(StockNoeud)"/>
        <org.eventb.core.action name="-" org.eventb.core.assignment="EnvoiVers≔EnvoiVers∪{data↦(StockNoeud(data)↦n)}" org.eventb.core.label="act1"/>
        <org.eventb.core.action name="." org.eventb.core.assignment="StockNoeud≔StockNoeud∖{data↦StockNoeud(data)}" org.eventb.core.label="act2"/>
        <org.eventb.core.guard name="/" org.eventb.core.label="grd4" org.eventb.core.predicate="data∉dom(EnvoiVers)"/>
        <org.eventb.core.guard name="0" org.eventb.core.label="grd5" org.eventb.core.predicate="n∈NOEUDS"/>
        <org.eventb.core.guard name="2" org.eventb.core.label="grd7" org.eventb.core.predicate="n≠StockNoeud(data)"/>
        <org.eventb.core.guard name="3" org.eventb.core.comment="Peut être enlever pour plus de liberté plus tard (Vérifie qu'on puisse bien acceder au noeud suivant depuis le noeud de depart)" org.eventb.core.label="grd8" org.eventb.core.predicate="n ∈ Reseau[{StockNoeud(data)}]"/>
    </org.eventb.core.event>
    <org.eventb.core.variable name="0" org.eventb.core.identifier="StockNoeud"/>
    <org.eventb.core.invariant name="1" org.eventb.core.label="inv4" org.eventb.core.predicate="StockNoeud∈DONNEES⇸NOEUDS"/>
    <org.eventb.core.event name="2" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="Produire">
        <org.eventb.core.parameter name="'" org.eventb.core.identifier="n"/>
        <org.eventb.core.parameter name="(" org.eventb.core.identifier="data"/>
        <org.eventb.core.action name=")" org.eventb.core.assignment="StockNoeud≔StockNoeud∪{data↦n}" org.eventb.core.label="act1"/>
        <org.eventb.core.guard name="*" org.eventb.core.label="grd1" org.eventb.core.predicate="n∈NOEUDS"/>
        <org.eventb.core.guard name="+" org.eventb.core.label="grd2" org.eventb.core.predicate="data∈DONNEES"/>
        <org.eventb.core.guard name="," org.eventb.core.label="grd3" org.eventb.core.predicate="data∉dom(StockNoeud)"/>
        <org.eventb.core.guard name="-" org.eventb.core.label="grd4" org.eventb.core.predicate="data∉dom(EnvoiVers)"/>
        <org.eventb.core.guard name="." org.eventb.core.label="grd5" org.eventb.core.predicate="data∉DonneesGros"/>
    </org.eventb.core.event>
    <org.eventb.core.variable name="3" org.eventb.core.identifier="EnvoiVers"/>
    <org.eventb.core.invariant name="4" org.eventb.core.comment="Pas sûr de l'utilité de garder le noeud de départ mais à voir plus tard" org.eventb.core.label="inv5" org.eventb.core.predicate="EnvoiVers∈DONNEES⇸(NOEUDS×NOEUDS)"/>
    <org.eventb.core.invariant name="5" org.eventb.core.label="inv6" org.eventb.core.predicate="dom(StockNoeud)∩dom(EnvoiVers)=∅"/>
    <org.eventb.core.event name="6" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="Perdre">
        <org.eventb.core.parameter name="'" org.eventb.core.identifier="d"/>
        <org.eventb.core.guard name=")" org.eventb.core.label="grd1" org.eventb.core.predicate="d∈dom(EnvoiVers)"/>
        <org.eventb.core.action name="*" org.eventb.core.assignment="EnvoiVers≔EnvoiVers∖{d↦EnvoiVers(d)}" org.eventb.core.label="act1"/>
        <org.eventb.core.action name="+" org.eventb.core.assignment="DonneesGros≔DonneesGros∪{d}" org.eventb.core.label="act2"/>
    </org.eventb.core.event>
    <org.eventb.core.event name="7" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="Recevoir">
        <org.eventb.core.parameter name="'" org.eventb.core.identifier="data"/>
        <org.eventb.core.action name="*" org.eventb.core.assignment="EnvoiVers≔EnvoiVers∖{data↦EnvoiVers(data)}" org.eventb.core.label="act1"/>
        <org.eventb.core.guard name="," org.eventb.core.label="grd2" org.eventb.core.predicate="data∈dom(EnvoiVers)"/>
        <org.eventb.core.guard name="-" org.eventb.core.label="grd3" org.eventb.core.predicate="data∉dom(StockNoeud)"/>
        <org.eventb.core.guard name="." org.eventb.core.label="grd4" org.eventb.core.predicate="EnvoiVers(data)∈Reseau"/>
        <org.eventb.core.action name="/" org.eventb.core.assignment="DonneesGros≔DonneesGros∪{data}" org.eventb.core.label="act2"/>
    </org.eventb.core.event>
    <org.eventb.core.event name="8" org.eventb.core.comment="Obligatoire, on ne peut pas modifier des variables abstraites non modifié de la machine abstraite dans les raffinements" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="Store">
        <org.eventb.core.parameter name="'" org.eventb.core.identifier="data"/>
        <org.eventb.core.guard name="(" org.eventb.core.label="grd1" org.eventb.core.predicate="data∈dom(EnvoiVers)"/>
        <org.eventb.core.guard name=")" org.eventb.core.label="grd2" org.eventb.core.predicate="data∉dom(StockNoeud)"/>
        <org.eventb.core.guard name="*" org.eventb.core.label="grd3" org.eventb.core.predicate="EnvoiVers(data)∈Reseau"/>
        <org.eventb.core.action name="+" org.eventb.core.assignment="EnvoiVers≔EnvoiVers∖{data↦EnvoiVers(data)}" org.eventb.core.label="act1"/>
        <org.eventb.core.action name="," org.eventb.core.assignment="StockNoeud≔StockNoeud∪{data↦prj2(EnvoiVers(data))}" org.eventb.core.label="act2"/>
    </org.eventb.core.event>
    <org.eventb.core.variable name="9" org.eventb.core.identifier="DonneesGros"/>
    <org.eventb.core.invariant name=":" org.eventb.core.label="inv7" org.eventb.core.predicate="DonneesGros⊆DONNEES"/>
    <org.eventb.core.invariant name=";" org.eventb.core.label="inv8" org.eventb.core.predicate="dom(StockNoeud)∩DonneesGros=∅"/>
    <org.eventb.core.invariant name="=" org.eventb.core.label="inv9" org.eventb.core.predicate="DonneesGros∩dom(EnvoiVers)=∅"/>
</org.eventb.core.machineFile>