-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathDSR_3_old.bum
More file actions
60 lines (60 loc) · 5.17 KB
/
DSR_3_old.bum
File metadata and controls
60 lines (60 loc) · 5.17 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
<?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_2"/>
<org.eventb.core.seesContext name="(" org.eventb.core.target="DSR_ctx_2"/>
<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.variable name="L" org.eventb.core.identifier="TableRoutage"/>
<org.eventb.core.variable name="V" org.eventb.core.identifier="DonneesGros"/>
<org.eventb.core.event name="W" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="INITIALISATION">
<org.eventb.core.action name="'" org.eventb.core.assignment="RREQ≔∅" org.eventb.core.label="act7"/>
<org.eventb.core.action name="(" org.eventb.core.assignment="RREQTransit≔∅" org.eventb.core.label="act8"/>
</org.eventb.core.event>
<org.eventb.core.event name="X" 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.event>
<org.eventb.core.event name="Y" 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.event>
<org.eventb.core.event name="Z" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="Envoyer">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="Envoyer"/>
</org.eventb.core.event>
<org.eventb.core.event name="[" 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="\" 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="]" 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="^" 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="_" 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.event name="`" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="Router">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="Router"/>
</org.eventb.core.event>
<org.eventb.core.event name="a" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="Derouter">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="Derouter"/>
</org.eventb.core.event>
<org.eventb.core.variable name="b" org.eventb.core.identifier="RREQ"/>
<org.eventb.core.invariant name="c" org.eventb.core.label="inv1" org.eventb.core.predicate="RREQ∈(NOEUDS↔ROUTES)"/>
<org.eventb.core.event name="d" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="SendRREQ">
<org.eventb.core.parameter name="'" org.eventb.core.identifier="n"/>
<org.eventb.core.guard name="(" org.eventb.core.label="grd1" org.eventb.core.predicate="n∈NOEUDS"/>
<org.eventb.core.action name=")" org.eventb.core.assignment="RREQ ≔ RREQ ∪ {n2↦{n↦n3}}" org.eventb.core.comment="RREQ ≔ RREQ ∪ {n2↦{n↦Reseau(n)}}" org.eventb.core.label="act1"/>
<org.eventb.core.guard name="*" org.eventb.core.label="grd2" org.eventb.core.predicate="n2∈NOEUDS"/>
<org.eventb.core.parameter name="+" org.eventb.core.identifier="n2"/>
<org.eventb.core.guard name="," org.eventb.core.comment="n2∉dom(RREQ)∨(n2∈dom(RREQ)∧n∉dom(RREQ(n2)))" org.eventb.core.label="grd3" org.eventb.core.predicate="n∈dom(Reseau)"/>
<org.eventb.core.guard name="-" org.eventb.core.label="grd4" org.eventb.core.predicate="n≠n2"/>
<org.eventb.core.parameter name="." org.eventb.core.identifier="n3"/>
<org.eventb.core.guard name="/" org.eventb.core.label="grd5" org.eventb.core.predicate="n3∈Reseau[{n}]"/>
</org.eventb.core.event>
<org.eventb.core.variable name="e" org.eventb.core.identifier="RREQTransit"/>
<org.eventb.core.invariant name="f" org.eventb.core.label="inv2" org.eventb.core.predicate="RREQTransit∈RREQ⇸NOEUDS"/>
</org.eventb.core.machineFile>