-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathDSR_2.bum
More file actions
78 lines (78 loc) · 8.2 KB
/
DSR_2.bum
File metadata and controls
78 lines (78 loc) · 8.2 KB
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
<?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.refinesMachine name="'" org.eventb.core.target="DSR_1"/>
<org.eventb.core.seesContext name="(" org.eventb.core.target="DSR_ctx_1"/>
<org.eventb.core.variable name=")" org.eventb.core.identifier="Reseau"/>
<org.eventb.core.variable name="0" org.eventb.core.identifier="StockNoeud"/>
<org.eventb.core.variable name="3" org.eventb.core.identifier="EnvoiVers"/>
<org.eventb.core.variable name="B" org.eventb.core.identifier="DonneesRoute"/>
<org.eventb.core.event name="C" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="INITIALISATION">
<org.eventb.core.action name="'" org.eventb.core.assignment="TableRoutage:∈NOEUDS→{∅}" org.eventb.core.label="act6"/>
</org.eventb.core.event>
<org.eventb.core.event name="D" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="Lier">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="Lier"/>
<org.eventb.core.action name="(" org.eventb.core.assignment="TableRoutage(n1)≔TableRoutage(n1)∪{n2↦{n1↦n2}}" org.eventb.core.label="act2"/>
<org.eventb.core.guard name=")" org.eventb.core.label="grd5" org.eventb.core.predicate="n2∉dom(TableRoutage(n1))"/>
</org.eventb.core.event>
<org.eventb.core.event name="E" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="Delier">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="Delier"/>
<org.eventb.core.guard name="(" org.eventb.core.label="grd3" org.eventb.core.predicate="n1∈dom(TableRoutage)"/>
<org.eventb.core.action name=")" org.eventb.core.assignment="TableRoutage(n1)≔TableRoutage(n1)∖{n2↦{n1↦n2}}" org.eventb.core.label="act2"/>
<org.eventb.core.guard name="*" org.eventb.core.label="grd4" org.eventb.core.predicate="n2∈dom(TableRoutage(n1))"/>
</org.eventb.core.event>
<org.eventb.core.event name="F" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="Envoyer">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="Envoyer"/>
<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(StockNoeud)"/>
<org.eventb.core.guard name="," org.eventb.core.label="grd3" org.eventb.core.predicate="data↦StockNoeud(data)∈StockNoeud"/>
<org.eventb.core.guard name="internal1" org.eventb.core.label="grd4" org.eventb.core.predicate="data∉dom(EnvoiVers)"/>
<org.eventb.core.parameter name=")" org.eventb.core.identifier="n"/>
<org.eventb.core.action name="-" org.eventb.core.assignment="DonneesRoute≔DonneesRoute∪{data↦TableRoutage(StockNoeud(data))(n)}" org.eventb.core.label="act3"/>
<org.eventb.core.guard name="internal4" org.eventb.core.label="grd16" org.eventb.core.predicate="data∉dom(DonneesRoute)"/>
<org.eventb.core.action name="internal6" org.eventb.core.assignment="StockNoeud≔StockNoeud∖{data↦StockNoeud(data)}" org.eventb.core.label="act4"/>
<org.eventb.core.action name="internal7" org.eventb.core.assignment="EnvoiVers≔EnvoiVers∪{data↦(StockNoeud(data)↦TableRoutage(StockNoeud(data))(n)(StockNoeud(data)))}" org.eventb.core.label="act5"/>
<org.eventb.core.guard name="internal:" org.eventb.core.label="grd18" org.eventb.core.predicate="n∈NOEUDS"/>
<org.eventb.core.witness name="internal;" org.eventb.core.label="r" org.eventb.core.predicate="r=TableRoutage(StockNoeud(data))(n)"/>
<org.eventb.core.guard name="internal=" org.eventb.core.label="grd19" org.eventb.core.predicate="n∈dom(TableRoutage(StockNoeud(data)))"/>
<org.eventb.core.guard name="internal>" org.eventb.core.comment="peut etre a chagner" org.eventb.core.label="grd20" org.eventb.core.predicate="TableRoutage(StockNoeud(data))(n)⊆Reseau"/>
</org.eventb.core.event>
<org.eventb.core.event name="G" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="Produire">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="Produire"/>
</org.eventb.core.event>
<org.eventb.core.event name="H" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="Perdre">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="Perdre"/>
</org.eventb.core.event>
<org.eventb.core.event name="I" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="Recevoir">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="Recevoir"/>
</org.eventb.core.event>
<org.eventb.core.event name="J" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="Store">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="Store"/>
</org.eventb.core.event>
<org.eventb.core.event name="K" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="Forward">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="Forward"/>
</org.eventb.core.event>
<org.eventb.core.variable name="L" org.eventb.core.identifier="TableRoutage"/>
<org.eventb.core.invariant name="M" org.eventb.core.label="inv1" org.eventb.core.predicate="TableRoutage∈NOEUDS→(NOEUDS⇸ROUTES)"/>
<org.eventb.core.invariant name="P" org.eventb.core.comment="Les routes partent du noeud de la table de routage" org.eventb.core.label="inv4" org.eventb.core.predicate="∀x,y·x∈dom(TableRoutage)∧y∈dom(TableRoutage(x))⇒x∈dom(TableRoutage(x)(y)) ∧ x∉ran(TableRoutage(x)(y))"/>
<org.eventb.core.invariant name="Q" org.eventb.core.comment="Les routes terminent au noeud d'arrivée de la table de routage" org.eventb.core.label="inv5" org.eventb.core.predicate="∀x,y·x∈dom(TableRoutage)∧y∈dom(TableRoutage(x))⇒y∈ran(TableRoutage(x)(y)) ∧ y∉dom(TableRoutage(x)(y))"/>
<org.eventb.core.event name="T" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="Router">
<org.eventb.core.parameter name="'" org.eventb.core.identifier="n"/>
<org.eventb.core.parameter name="(" org.eventb.core.identifier="n2"/>
<org.eventb.core.parameter name=")" org.eventb.core.identifier="r"/>
<org.eventb.core.guard name="," org.eventb.core.label="grd3" org.eventb.core.predicate="r∈ROUTES"/>
<org.eventb.core.guard name="/" org.eventb.core.label="grd6" org.eventb.core.predicate="n∈dom(r)∧n∉ran(r)"/>
<org.eventb.core.guard name="0" org.eventb.core.label="grd7" org.eventb.core.predicate="n2∈ran(r)∧n2∉dom(r)"/>
<org.eventb.core.guard name="3" org.eventb.core.label="grd9" org.eventb.core.predicate="n∈dom(TableRoutage)"/>
<org.eventb.core.action name="5" org.eventb.core.assignment="TableRoutage(n)≔{n2↦r}TableRoutage(n)" org.eventb.core.label="act1"/>
<org.eventb.core.guard name="7" org.eventb.core.label="grd11" org.eventb.core.predicate="n2↦r∉TableRoutage(n)"/>
</org.eventb.core.event>
<org.eventb.core.event name="U" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="Derouter">
<org.eventb.core.parameter name="'" org.eventb.core.identifier="n"/>
<org.eventb.core.parameter name="(" org.eventb.core.identifier="n2"/>
<org.eventb.core.guard name=")" org.eventb.core.label="grd1" org.eventb.core.predicate="n∈dom(TableRoutage)"/>
<org.eventb.core.guard name="*" org.eventb.core.label="grd2" org.eventb.core.predicate="n2∈dom(TableRoutage(n))"/>
<org.eventb.core.action name="+" org.eventb.core.assignment="TableRoutage(n)≔{n2}⩤TableRoutage(n)" org.eventb.core.label="act1"/>
</org.eventb.core.event>
<org.eventb.core.variable name="V" org.eventb.core.identifier="DonneesGros"/>
<org.eventb.core.invariant name="W" org.eventb.core.comment="pas de table de soi-même" org.eventb.core.label="inv6" org.eventb.core.predicate="∀x,y·x∈dom(TableRoutage)∧y∈dom(TableRoutage(x))⇒x≠y"/>
</org.eventb.core.machineFile>