-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathDSR_1.bum
More file actions
66 lines (66 loc) · 6.82 KB
/
Copy pathDSR_1.bum
File metadata and controls
66 lines (66 loc) · 6.82 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
<?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_0"/>
<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.event name="4" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="INITIALISATION">
<org.eventb.core.action name="'" org.eventb.core.assignment="DonneesRoute≔∅" org.eventb.core.label="act5"/>
</org.eventb.core.event>
<org.eventb.core.event name="5" 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="6" 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="7" 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.guard name="*" org.eventb.core.label="grd1" org.eventb.core.predicate="data∈dom(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="r"/>
<org.eventb.core.action name="-" org.eventb.core.assignment="DonneesRoute≔DonneesRoute∪{data↦r}" org.eventb.core.label="act3"/>
<org.eventb.core.guard name="1" org.eventb.core.label="grd6" org.eventb.core.predicate="r∈ROUTES"/>
<org.eventb.core.guard name="internal2" org.eventb.core.comment="Le noeud de départ est au départ de la route" org.eventb.core.label="grd14" org.eventb.core.predicate="StockNoeud(data)∈dom(r)∧StockNoeud(data)∉ran(r)"/>
<org.eventb.core.guard name="internal4" org.eventb.core.label="grd16" org.eventb.core.predicate="data∉dom(DonneesRoute)"/>
<org.eventb.core.refinesEvent name="internal5" org.eventb.core.target="Envoyer"/>
<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)↦r(StockNoeud(data)))}" org.eventb.core.label="act5"/>
<org.eventb.core.witness name="internal8" org.eventb.core.label="n" org.eventb.core.predicate="n=r(StockNoeud(data))"/>
<org.eventb.core.guard name="internal9" org.eventb.core.label="grd17" org.eventb.core.predicate="r⊆Reseau"/>
</org.eventb.core.event>
<org.eventb.core.event name="8" 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="9" 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.action name="(" org.eventb.core.assignment="DonneesRoute≔DonneesRoute∖{d↦DonneesRoute(d)}" org.eventb.core.label="act3"/>
<org.eventb.core.guard name=")" org.eventb.core.label="grd2" org.eventb.core.predicate="d∈dom(DonneesRoute)"/>
</org.eventb.core.event>
<org.eventb.core.event name=":" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="Recevoir">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="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="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∈dom(DonneesRoute)"/>
<org.eventb.core.action name="0" org.eventb.core.assignment="DonneesRoute≔DonneesRoute∖{data↦DonneesRoute(data)}" org.eventb.core.label="act2"/>
<org.eventb.core.guard name="1" org.eventb.core.comment="Le noeud d'arrivé est le dernier de la route" org.eventb.core.label="grd6" org.eventb.core.predicate="prj2(EnvoiVers(data))∉dom(DonneesRoute(data))"/>
<org.eventb.core.guard name="2" org.eventb.core.label="grd7" org.eventb.core.predicate="EnvoiVers(data)∈Reseau"/>
<org.eventb.core.action name="3" org.eventb.core.assignment="DonneesGros≔DonneesGros∪{data}" org.eventb.core.label="act3"/>
</org.eventb.core.event>
<org.eventb.core.invariant name=";" org.eventb.core.label="inv1" org.eventb.core.predicate="DonneesRoute∈DONNEES⇸ROUTES"/>
<org.eventb.core.event name="?" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="Store">
<org.eventb.core.guard name="1" org.eventb.core.label="grd6" org.eventb.core.predicate="data∈dom(DonneesRoute)"/>
<org.eventb.core.guard name="5" org.eventb.core.comment="Le noeud d'arrivé n'est pas le dernier" org.eventb.core.label="grd8" org.eventb.core.predicate="prj2(EnvoiVers(data))∈dom(DonneesRoute(data))"/>
<org.eventb.core.refinesEvent name=";" org.eventb.core.target="Store"/>
</org.eventb.core.event>
<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="Forward">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="Envoyer"/>
<org.eventb.core.guard name="(" org.eventb.core.label="grd9" org.eventb.core.predicate="data∈dom(DonneesRoute)"/>
<org.eventb.core.guard name=")" org.eventb.core.label="grd10" org.eventb.core.predicate="StockNoeud(data)∈dom(DonneesRoute(data))"/>
<org.eventb.core.guard name="*" org.eventb.core.label="grd11" org.eventb.core.predicate="n = DonneesRoute(data)(StockNoeud(data))"/>
</org.eventb.core.event>
<org.eventb.core.variable name="D" org.eventb.core.identifier="DonneesGros"/>
</org.eventb.core.machineFile>