DSR_3.bum

<?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.action name=")" org.eventb.core.assignment="RREP≔∅" org.eventb.core.label="act9"/>
        <org.eventb.core.action name="*" org.eventb.core.assignment="RREPTransit≔∅" org.eventb.core.label="act10"/>
    </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="EnvoyerRREQ">
        <org.eventb.core.parameter name="'" org.eventb.core.identifier="n1"/>
        <org.eventb.core.guard name="(" org.eventb.core.label="grd1" org.eventb.core.predicate="n1∈NOEUDS"/>
        <org.eventb.core.action name=")" org.eventb.core.assignment="RREQ ≔ RREQ ∪ {n2↦∅}" 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="n1∈dom(Reseau)"/>
        <org.eventb.core.guard name="-" org.eventb.core.label="grd4" org.eventb.core.predicate="n1≠n2"/>
        <org.eventb.core.guard name="." org.eventb.core.comment="Garde très limitante" org.eventb.core.label="grd5" org.eventb.core.predicate="n2∉dom(RREQ)"/>
        <org.eventb.core.action name="/" org.eventb.core.assignment="RREQTransit ≔ RREQTransit ∪ { (n2 ↦ ∅) ↦ ({ n1 ↦ Reseau[{n1}] }) }" org.eventb.core.label="act2"/>
        <org.eventb.core.guard name="0" org.eventb.core.label="grd6" org.eventb.core.predicate="n2∉dom(TableRoutage(n1))"/>
    </org.eventb.core.event>
    <org.eventb.core.event name="g" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="StoreRREQ">
        <org.eventb.core.parameter name="'" org.eventb.core.identifier="d"/>
        <org.eventb.core.parameter name="(" org.eventb.core.identifier="r"/>
        <org.eventb.core.guard name=")" org.eventb.core.label="grd1" org.eventb.core.predicate="(d ↦ r) ∈ dom(RREQTransit)"/>
        <org.eventb.core.parameter name="." org.eventb.core.identifier="from"/>
        <org.eventb.core.parameter name="/" org.eventb.core.identifier="n"/>
        <org.eventb.core.guard name="0" org.eventb.core.label="grd5" org.eventb.core.predicate="from∈dom(RREQTransit(d↦r))"/>
        <org.eventb.core.action name="1" org.eventb.core.assignment="RREQTransit ≔ &#10;            routesToClean ⩤ (RREQTransit  &#10;            { (d↦r) ↦ &#10;                ( RREQTransit(d↦r)  { from ↦ (RREQTransit(d↦r)(from) ∖ {n}) } )&#10;            })" org.eventb.core.label="act2"/>
        <org.eventb.core.guard name="2" org.eventb.core.label="grd6" org.eventb.core.predicate="from ∉ dom(r)"/>
        <org.eventb.core.guard name="3" org.eventb.core.label="grd7" org.eventb.core.predicate="n ∉ dom(r) ∧ n ∉ ran(r)"/>
        <org.eventb.core.guard name="4" org.eventb.core.label="grd8" org.eventb.core.predicate="r ≠ ∅ ⇒ from ∈ ran(r)"/>
        <org.eventb.core.guard name="5" org.eventb.core.label="grd9" org.eventb.core.predicate="n∈RREQTransit(d↦r)(from)"/>
        <org.eventb.core.guard name="6" org.eventb.core.label="grd10" org.eventb.core.predicate="r∪{from ↦ n}∈ROUTES"/>
        <org.eventb.core.parameter name="7" org.eventb.core.identifier="routesToClean"/>
        <org.eventb.core.guard name="8" org.eventb.core.label="grd11" org.eventb.core.predicate="routesToClean = {&#10;request ∣&#10;request∈RREQ ∧&#10;request∈dom(RREQTransit) ∧&#10;from∈dom(RREQTransit(request)) ∧&#10;RREQTransit(request)(from)={n}&#10;}"/>
        <org.eventb.core.action name="9" org.eventb.core.assignment="RREQ≔(RREQ∪{d↦(r∪{from↦n})})∖routesToClean" org.eventb.core.label="act3"/>
        <org.eventb.core.guard name=":" org.eventb.core.label="grd12" org.eventb.core.predicate="card(dom(r))&lt;MaxSauts"/>
        <org.eventb.core.guard name=";" org.eventb.core.label="grd13" org.eventb.core.predicate="n≠d"/>
        <org.eventb.core.guard name="=" org.eventb.core.label="grd14" org.eventb.core.predicate="Reseau[{n}]⊈dom(r)"/>
    </org.eventb.core.event>
    <org.eventb.core.event name="j" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="RecevoirRREQ">
        <org.eventb.core.parameter name="internal1" org.eventb.core.identifier="n"/>
        <org.eventb.core.parameter name="(" org.eventb.core.identifier="d"/>
        <org.eventb.core.parameter name="internal2" org.eventb.core.identifier="r"/>
        <org.eventb.core.parameter name=")" org.eventb.core.identifier="from"/>
        <org.eventb.core.parameter name="+" org.eventb.core.identifier="routesToClean"/>
        <org.eventb.core.action name="," org.eventb.core.assignment="RREQTransit ≔ &#10;           routesToClean ⩤ (RREQTransit &#10;&#9;&#9;&#9;{ (d↦r) ↦ &#10;                ( RREQTransit(d↦r)  { from ↦ (RREQTransit(d↦r)(from) ∖ {n}) } )&#10;            })" org.eventb.core.label="act1"/>
        <org.eventb.core.action name="-" org.eventb.core.assignment="RREQ≔RREQ∖routesToClean" org.eventb.core.label="act2"/>
        <org.eventb.core.guard name="." org.eventb.core.label="grd1" org.eventb.core.predicate="(d ↦ r) ∈ dom(RREQTransit)"/>
        <org.eventb.core.guard name="/" org.eventb.core.label="grd2" org.eventb.core.predicate="from∈dom(RREQTransit(d↦r))"/>
        <org.eventb.core.guard name="0" org.eventb.core.label="grd0" org.eventb.core.predicate="n∈RREQTransit(d↦r)(from)"/>
        <org.eventb.core.guard name="1" org.eventb.core.label="grd4" org.eventb.core.predicate="routesToClean = {&#10;request ∣&#10;request∈RREQ ∧&#10;request∈dom(RREQTransit) ∧&#10;from∈dom(RREQTransit(request)) ∧&#10;RREQTransit(request)(from)={n}&#10;}"/>
        <org.eventb.core.guard name="2" org.eventb.core.label="grd5" org.eventb.core.predicate="n=d"/>
        <org.eventb.core.action name="3" org.eventb.core.assignment="RREP≔RREP∪{(r∪{from↦n})∼↦n}" org.eventb.core.label="act3"/>
        <org.eventb.core.action name="4" org.eventb.core.assignment="RREPTransit≔RREPTransit∪{(r∪{from↦n})∼↦n}" org.eventb.core.label="act4"/>
        <org.eventb.core.guard name="internal3" org.eventb.core.label="grd6" org.eventb.core.predicate="(r∪{from↦n})∈ROUTES"/>
        <org.eventb.core.guard name="internal4" org.eventb.core.label="grd7" org.eventb.core.predicate="(r∪{from ↦ n})∼∈ROUTES"/>
        <org.eventb.core.guard name="internal5" org.eventb.core.label="grd8" org.eventb.core.predicate="(r∪{from↦n})∼↦n∉RREP"/>
    </org.eventb.core.event>
    <org.eventb.core.event name="i" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="RejectRREQ">
        <org.eventb.core.parameter name="'" org.eventb.core.identifier="d"/>
        <org.eventb.core.parameter name="(" org.eventb.core.identifier="r"/>
        <org.eventb.core.parameter name=")" org.eventb.core.identifier="from"/>
        <org.eventb.core.parameter name="*" org.eventb.core.identifier="n"/>
        <org.eventb.core.guard name="+" org.eventb.core.label="grd1" org.eventb.core.predicate="(d ↦ r) ∈ dom(RREQTransit)"/>
        <org.eventb.core.guard name="-" org.eventb.core.label="grd3" org.eventb.core.predicate="card(dom(r))=MaxSauts ∨ n∈dom(r) ∨ (Reseau[{n}]⊆dom(r) ∧ n≠d)"/>
        <org.eventb.core.action name="." org.eventb.core.assignment="RREQTransit ≔ &#10;           routesToClean ⩤ (RREQTransit &#10;&#9;&#9;&#9;{ (d↦r) ↦ &#10;                ( RREQTransit(d↦r)  { from ↦ (RREQTransit(d↦r)(from) ∖ {n}) } )&#10;            })" org.eventb.core.label="act1"/>
        <org.eventb.core.guard name="/" org.eventb.core.label="grd4" org.eventb.core.predicate="from∈dom(RREQTransit(d↦r))"/>
        <org.eventb.core.guard name="0" org.eventb.core.label="grd5" org.eventb.core.predicate="n∈RREQTransit(d↦r)(from)"/>
        <org.eventb.core.guard name="1" org.eventb.core.label="grd6" org.eventb.core.predicate="routesToClean = {&#10;request ∣&#10;request∈RREQ ∧&#10;request∈dom(RREQTransit) ∧&#10;from∈dom(RREQTransit(request)) ∧&#10;RREQTransit(request)(from)={n}&#10;}"/>
        <org.eventb.core.parameter name="2" org.eventb.core.identifier="routesToClean"/>
        <org.eventb.core.action name="3" org.eventb.core.assignment="RREQ≔RREQ∖routesToClean" org.eventb.core.label="act2"/>
    </org.eventb.core.event>
    <org.eventb.core.invariant name="e" org.eventb.core.label="inv2" org.eventb.core.predicate="RREQTransit∈RREQ⇸(NOEUDS⇸ℙ(NOEUDS))"/>
    <org.eventb.core.variable name="f" org.eventb.core.identifier="RREQTransit"/>
    <org.eventb.core.event name="h" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="ForwardRREQ">
        <org.eventb.core.parameter name="'" org.eventb.core.identifier="d"/>
        <org.eventb.core.parameter name="(" org.eventb.core.identifier="r"/>
        <org.eventb.core.parameter name=")" org.eventb.core.identifier="n"/>
        <org.eventb.core.guard name="*" org.eventb.core.label="grd1" org.eventb.core.predicate="(d ↦ r) ∈ RREQ"/>
        <org.eventb.core.guard name="+" org.eventb.core.label="grd2" org.eventb.core.predicate="n∈ran(r)∖dom(r)"/>
        <org.eventb.core.action name="." org.eventb.core.assignment="RREQTransit ≔ RREQTransit ∪ {(d↦r)↦({n↦Reseau[{n}]})}" org.eventb.core.label="act1"/>
        <org.eventb.core.guard name="0" org.eventb.core.label="grd6" org.eventb.core.predicate="d↦r∉dom(RREQTransit)∨(d↦r∈dom(RREQTransit)∧n ∉ dom(RREQTransit(d ↦ r)))"/>
        <org.eventb.core.guard name="1" org.eventb.core.comment="j'arrivais pas à prouver" org.eventb.core.label="grd7" org.eventb.core.predicate="RREQTransit∪{d ↦ r ↦ {n ↦ Reseau[{n}]}}∈RREQ ⇸ (NOEUDS ⇸ ℙ(NOEUDS))"/>
        <org.eventb.core.guard name="2" org.eventb.core.label="grd8" org.eventb.core.predicate="Reseau[{n}]≠∅"/>
        <org.eventb.core.guard name="3" org.eventb.core.label="grd9" org.eventb.core.predicate="n≠d"/>
    </org.eventb.core.event>
    <org.eventb.core.event name="k" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="PerdreRREQ">
        <org.eventb.core.action name="'" org.eventb.core.assignment="RREQTransit ≔ &#10;           routesToClean ⩤ (RREQTransit &#10;&#9;&#9;&#9;{ (d↦r) ↦ &#10;                ( RREQTransit(d↦r)  { from ↦ (RREQTransit(d↦r)(from) ∖ {n}) } )&#10;            })" org.eventb.core.label="act1"/>
        <org.eventb.core.parameter name="(" org.eventb.core.identifier="d"/>
        <org.eventb.core.parameter name=")" org.eventb.core.identifier="r"/>
        <org.eventb.core.parameter name="*" org.eventb.core.identifier="from"/>
        <org.eventb.core.parameter name="+" org.eventb.core.identifier="n"/>
        <org.eventb.core.guard name="," org.eventb.core.label="grd1" org.eventb.core.predicate="(d ↦ r) ∈ dom(RREQTransit)"/>
        <org.eventb.core.guard name="-" org.eventb.core.label="grd2" org.eventb.core.predicate="from∈dom(RREQTransit(d↦r))"/>
        <org.eventb.core.guard name="." org.eventb.core.label="grd3" org.eventb.core.predicate="n∈RREQTransit(d↦r)(from)"/>
        <org.eventb.core.parameter name="/" org.eventb.core.identifier="routesToClean"/>
        <org.eventb.core.guard name="0" org.eventb.core.label="grd4" org.eventb.core.predicate="routesToClean = {&#10;request ∣&#10;request∈RREQ ∧&#10;request∈dom(RREQTransit) ∧&#10;from∈dom(RREQTransit(request)) ∧&#10;RREQTransit(request)(from)={n}&#10;}"/>
        <org.eventb.core.action name="1" org.eventb.core.assignment="RREQ≔RREQ∖routesToClean" org.eventb.core.label="act2"/>
    </org.eventb.core.event>
    <org.eventb.core.invariant name="l" org.eventb.core.label="inv3" org.eventb.core.predicate="RREP∈ROUTES⇸NOEUDS"/>
    <org.eventb.core.variable name="m" org.eventb.core.identifier="RREP"/>
    <org.eventb.core.variable name="n" org.eventb.core.identifier="RREPTransit"/>
    <org.eventb.core.invariant name="o" org.eventb.core.label="inv4" org.eventb.core.predicate="RREPTransit⊆RREP"/>
    <org.eventb.core.event name="p" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="StoreRREP">
        <org.eventb.core.parameter name="'" org.eventb.core.identifier="n1"/>
        <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="grd1" org.eventb.core.predicate="r↦n1∈RREP"/>
        <org.eventb.core.guard name="+" org.eventb.core.label="grd2" org.eventb.core.predicate="n1∈dom(r)"/>
        <org.eventb.core.action name="," org.eventb.core.assignment="RREP(r)≔n2" org.eventb.core.label="act1"/>
        <org.eventb.core.action name="-" org.eventb.core.assignment="RREPTransit≔ {r} ⩤ RREPTransit" org.eventb.core.label="act2"/>
        <org.eventb.core.guard name="." org.eventb.core.label="grd3" org.eventb.core.predicate="n1↦n2∈Reseau"/>
        <org.eventb.core.guard name="/" org.eventb.core.label="grd4" org.eventb.core.predicate="r∈dom(RREPTransit)"/>
        <org.eventb.core.guard name="0" org.eventb.core.label="grd5" org.eventb.core.predicate="n2=r(n1)"/>
        <org.eventb.core.parameter name="1" org.eventb.core.identifier="s"/>
        <org.eventb.core.guard name="2" org.eventb.core.label="grd6" org.eventb.core.predicate="s∈ran(r)∖dom(r)"/>
        <org.eventb.core.guard name="3" org.eventb.core.label="grd7" org.eventb.core.predicate="n2≠s"/>
    </org.eventb.core.event>
    <org.eventb.core.event name="q" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="ForwardRREP">
        <org.eventb.core.parameter name="'" org.eventb.core.identifier="n1"/>
        <org.eventb.core.parameter name=")" org.eventb.core.identifier="r"/>
        <org.eventb.core.guard name="*" org.eventb.core.label="grd1" org.eventb.core.predicate="r↦n1∈RREP"/>
        <org.eventb.core.action name="-" org.eventb.core.assignment="RREPTransit≔{r↦n1} ∪ RREPTransit" org.eventb.core.label="act2"/>
        <org.eventb.core.guard name="." org.eventb.core.label="grd3" org.eventb.core.predicate="r∉dom(RREPTransit)"/>
    </org.eventb.core.event>
    <org.eventb.core.event name="r" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="PerdreRREP">
        <org.eventb.core.parameter name="'" org.eventb.core.identifier="r"/>
        <org.eventb.core.parameter name="(" org.eventb.core.identifier="n1"/>
        <org.eventb.core.guard name=")" org.eventb.core.label="grd1" org.eventb.core.predicate="r↦n1∈RREP"/>
        <org.eventb.core.action name="*" org.eventb.core.assignment="RREPTransit≔{r} ⩤ RREPTransit" org.eventb.core.label="act1"/>
        <org.eventb.core.action name="+" org.eventb.core.assignment="RREP≔{r} ⩤ RREP" org.eventb.core.label="act2"/>
        <org.eventb.core.guard name="," org.eventb.core.label="grd2" org.eventb.core.predicate="r∈dom(RREPTransit)"/>
    </org.eventb.core.event>
    <org.eventb.core.event name="s" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="RecevoirRREP">
        <org.eventb.core.parameter name="'" org.eventb.core.identifier="n1"/>
        <org.eventb.core.parameter name="(" org.eventb.core.identifier="d"/>
        <org.eventb.core.parameter name=")" org.eventb.core.identifier="r"/>
        <org.eventb.core.guard name="*" org.eventb.core.label="grd1" org.eventb.core.predicate="r∼↦n1∈RREP"/>
        <org.eventb.core.parameter name="+" org.eventb.core.identifier="s"/>
        <org.eventb.core.guard name="," org.eventb.core.label="grd2" org.eventb.core.predicate="r∼∈dom(RREPTransit)"/>
        <org.eventb.core.guard name="-" org.eventb.core.label="grd3" org.eventb.core.predicate="s∈dom(r)∖ran(r)"/>
        <org.eventb.core.guard name="." org.eventb.core.label="grd4" org.eventb.core.predicate="d∈ran(r)∖dom(r)"/>
        <org.eventb.core.action name="/" org.eventb.core.assignment="RREP≔{r∼} ⩤ RREP" org.eventb.core.label="act1"/>
        <org.eventb.core.action name="0" org.eventb.core.assignment="RREPTransit≔{r∼} ⩤ RREPTransit" org.eventb.core.label="act2"/>
        <org.eventb.core.action name="1" org.eventb.core.assignment="TableRoutage(s)≔{d↦r}  TableRoutage(s)" org.eventb.core.label="act3"/>
        <org.eventb.core.refinesEvent name="2" org.eventb.core.target="Router"/>
        <org.eventb.core.witness name="3" org.eventb.core.label="n" org.eventb.core.predicate="n=s"/>
        <org.eventb.core.witness name="4" org.eventb.core.label="n2" org.eventb.core.predicate="n2=d"/>
        <org.eventb.core.guard name="5" org.eventb.core.label="grd5" org.eventb.core.predicate="n1∈dom(r∼)"/>
        <org.eventb.core.guard name="6" org.eventb.core.label="grd6" org.eventb.core.predicate="r∼(n1)=s"/>
        <org.eventb.core.guard name="7" org.eventb.core.label="grd7" org.eventb.core.predicate="r∈ROUTES"/>
        <org.eventb.core.guard name="8" org.eventb.core.label="grd8" org.eventb.core.predicate="d ↦ r∉TableRoutage(s)"/>
    </org.eventb.core.event>
</org.eventb.core.machineFile>