Pattern-Instanciation-On-System-Engineering-Model/Event-B/pseim/team/mLink.bum.xmb

<?xml version="1.0" encoding="UTF-8"?>
<machine:Machine xmi:version="2.0" xmlns:xmi="http://www.omg.org/XMI" xmlns:machine="http://emf.eventb.org/models/core/machine/2014" name="mLink">
  <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
    <details key="configuration" value="org.eventb.core.fwd;de.prob.units.mchBase;org.eventb.codegen.ui.cgConfig"/>
    <details key="name" value="mLink"/>
  </annotations>
  <annotations source="http:///org/eventb/core/RodinReferenceNamesAnnotations">
    <details key="refines mPort" value="_a6WF0MOWEeeQteb5bDCu6g"/>
    <details key="sees cLink" value="_a6WF0cOWEeeQteb5bDCu6g"/>
  </annotations>
  <attributes key="org.eventb.texttools.text_lastmodified">
    <value type="Long" value="ACED00057372000E6A6176612E6C616E672E4C6F6E673B8BE490CC8F23DF0200014A000576616C7565787200106A6176612E6C616E672E4E756D62657286AC951D0B94E08B02000078700000016268312F21"/>
  </attributes>
  <attributes key="org.eventb.texttools.text_representation">
    <value type="String" value="ACED00057415A26D616368696E65206D4C696E6B20726566696E6573206D506F727420207365657320634C696E6B0A0A7661726961626C657320636F6D706F6E656E747320636F6E7461696E657220635F6D756C7469706C696369747920746F5F636C6F6E655F6320635F696E64657820746F5F756E666F6C645F6320746F5F756E666F6C645F635F696E20696E7374327061745F632070726F7065727469657320706F72747320705F6D756C7469706C696369747920705F696E64657820746F5F756E666F6C645F705F696E20696E7374327061745F70206C696E6B73207372632064737420635F6C696E6B735F646F6E6520696E7374327061745F6C0A0A696E76617269616E74730A2020406C696E6B5F7479206C696E6B7320E288882072616E28636F6D706F6E656E74732920E28694204C696E6B0A2020406C696E6B5F66696E69746520E2888063C2B766696E697465286C696E6B735B7B637D5D290A2020406C696E6B5F6E6F745F736861726564206C696E6B73E288BC20E28888204C696E6B20E287B820436F6D706F6E656E740A2020407372635F74792073726320E288882072616E286C696E6B732920E286922072616E28706F727473290A2020406473745F74792064737420E288882072616E286C696E6B732920E286922072616E28706F727473290A2020406C696E6B5F636969206C696E6B733B20282873726320E28A97206473742920E296B7202849506F727420C3972049506F7274292920E28A8620706F72747320E28A972028636F6E7461696E6572E288BC3B20706F727473290A2020406C696E6B5F636F69206C696E6B733B20282873726320E28A97206473742920E296B720284F506F727420C3972049506F7274292920E28A862028636F6E7461696E6572E288BC3B706F7274732920E28A972028636F6E7461696E6572E288BC3B20706F727473290A2020406C696E6B5F636F6F206C696E6B733B20282873726320E28A97206473742920E296B720284F506F727420C397204F506F7274292920E28A862028636F6E7461696E6572E288BC3B20706F7274732920E28A9720706F7274730A2020406C696E6B5F63696F206C696E6B733B20282873726320E28A97206473742920E296B7202849506F727420C397204F506F7274292920E28A8620706F72747320E28A9720706F7274730A2020407472616E73705F73726320E288806CC2B76CE2888828636F6D706F6E656E74733B6C696E6B73295B7B5061747D5DE288A95472616E73706F736520E2879220705F6D756C7469706C696369747928737263286C2929203D20635F6D756C7469706C696369747928706F727473E288BC28647374286C2929290A2020407472616E73705F64737420E288806CC2B76CE2888828636F6D706F6E656E74733B6C696E6B73295B7B5061747D5DE288A95472616E73706F736520E2879220705F6D756C7469706C696369747928647374286C2929203D20635F6D756C7469706C696369747928706F727473E288BC28737263286C2929290A202040635F6C696E6B735F646F6E6520635F6C696E6B735F646F6E6520E28A862028636F6D706F6E656E74733B6C696E6B73295B7B5061747D5D20C39720636F6D706F6E656E74735B7B496E73747D5D0A202040696E7374327061745F6C5F747920696E7374327061745F6C20E288882028636F6D706F6E656E74733B6C696E6B73295B7B496E73747D5D20E286922028636F6D706F6E656E74733B6C696E6B73295B7B5061747D5D0A202040696E7374327061745F6C5F70726573657276655F7479706520E288804BC2B74BE288884C4B696E6420E2879220696E7374327061745F6C5B4B5D20E28A86204B0A202040696E7374327061745F6C5F73726320696E7374327061745F6C3B737263203D207372633B696E7374327061745F700A202040696E7374327061745F6C5F64737420696E7374327061745F6C3B647374203D206473743B696E7374327061745F700A2020407472616E73705F636F72726563743120E288806CC2B76CE2888828636F6D706F6E656E74733B6C696E6B73295B7B496E73747D5D20E288A9205472616E73706F736520E2879220705F696E64657828737263286C2929203D20635F696E64657828706F727473E288BC28647374286C2929290A2020407472616E73705F636F72726563743220E288806CC2B76CE2888828636F6D706F6E656E74733B6C696E6B73295B7B496E73747D5D20E288A9205472616E73706F736520E2879220705F696E64657828647374286C2929203D20635F696E64657828706F727473E288BC28737263286C2929290A0A76617269616E74202828636F6D706F6E656E74733B6C696E6B73295B7B5061747D5D20C39720636F6D706F6E656E74735B7B496E73747D5D2920E2889620635F6C696E6B735F646F6E650A0A6576656E74730A20206576656E7420696E7374616E63696174655F7061747465726E20657874656E647320696E7374616E63696174655F7061747465726E0A2020202077686572650A202020202020407472616E73705F6374723120E288806CC2B76CE2888828636F6D706F6E656E74733B6C696E6B73295B7B5061747D5DE288A95472616E73706F736520E288A720706F727473E288BC28647374286C292920E2888820646F6D28696E73745F636F6D706F6E656E74732920E28792206361726428696E73745F706F7274735B7B737263286C297D5D293D6361726428696E73745F636F6D706F6E656E74735B7B706F727473E288BC28647374286C29297D5D290A202020202020407472616E73705F6
  </attributes>
  <refines href="../mPort.bum#http://emf.eventb.org/models/core/machine/2014::Machine::mPort"/>
  <sees href="../cLink.buc#http://emf.eventb.org/models/core/context/2014::Context::cLink"/>
  <variables name="components">
    <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
      <details key="name" value="_S_fWQr4_EeeN0675uvquSw"/>
      <details key="identifier" value="components"/>
    </annotations>
  </variables>
  <variables name="container">
    <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
      <details key="name" value="_S_fWRL4_EeeN0675uvquSw"/>
      <details key="identifier" value="container"/>
    </annotations>
  </variables>
  <variables name="c_multiplicity">
    <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
      <details key="name" value="_S_fWRb4_EeeN0675uvquSw"/>
      <details key="identifier" value="c_multiplicity"/>
    </annotations>
  </variables>
  <variables name="to_clone_c">
    <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
      <details key="name" value="_S_fWRr4_EeeN0675uvquSw"/>
      <details key="identifier" value="to_clone_c"/>
    </annotations>
  </variables>
  <variables name="c_index">
    <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
      <details key="name" value="_73nGMMOYEeeQteb5bDCu6g"/>
      <details key="identifier" value="c_index"/>
    </annotations>
  </variables>
  <variables name="to_unfold_c">
    <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
      <details key="name" value="_0ffzsMOZEeeQteb5bDCu6g"/>
      <details key="identifier" value="to_unfold_c"/>
    </annotations>
  </variables>
  <variables name="to_unfold_c_in">
    <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
      <details key="name" value="_j2NdQOGVEeeUoZak4Ibgcg"/>
      <details key="identifier" value="to_unfold_c_in"/>
    </annotations>
  </variables>
  <variables name="inst2pat_c">
    <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
      <details key="name" value="_j2NdQeGVEeeUoZak4Ibgcg"/>
      <details key="identifier" value="inst2pat_c"/>
    </annotations>
  </variables>
  <variables name="cProperties">
    <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
      <details key="name" value="_QZUfgOTyEeemadOWCHlIvw"/>
      <details key="identifier" value="cProperties"/>
    </annotations>
  </variables>
  <variables name="ports">
    <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
      <details key="name" value="_QZUfgeTyEeemadOWCHlIvw"/>
      <details key="identifier" value="ports"/>
    </annotations>
  </variables>
  <variables name="p_multiplicity">
    <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
      <details key="name" value="_Z5iv0Pg-EeeeS5KQUtrGlw"/>
      <details key="identifier" value="p_multiplicity"/>
    </annotations>
  </variables>
  <variables name="p_index">
    <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
      <details key="name" value="_Z5iv0fg-EeeeS5KQUtrGlw"/>
      <details key="identifier" value="p_index"/>
    </annotations>
  </variables>
  <variables name="to_unfold_p_in">
    <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
      <details key="name" value="_Ajk8sPloEeeeS5KQUtrGlw"/>
      <details key="identifier" value="to_unfold_p_in"/>
    </annotations>
  </variables>
  <variables name="inst2pat_p">
    <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
      <details key="name" value="_X1DEEAA3EeictLZKwQfI0A"/>
      <details key="identifier" value="inst2pat_p"/>
    </annotations>
  </variables>
  <variables name="links">
    <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
      <details key="name" value="_X1DEEQA3EeictLZKwQfI0A"/>
      <details key="identifier" value="links"/>
    </annotations>
  </variables>
  <variables name="src">
    <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
      <details key="name" value="_X1DEEgA3EeictLZKwQfI0A"/>
      <details key="identifier" value="src"/>
    </annotations>
  </variables>
  <variables name="dst">
    <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
      <details key="name" value="_X1DEEwA3EeictLZKwQfI0A"/>
      <details key="identifier" value="dst"/>
    </annotations>
  </variables>
  <variables name="c_links_done">
    <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
      <details key="name" value="_cztlsAi3EeiFlqW-8GKglg"/>
      <details key="identifier" value="c_links_done"/>
    </annotations>
  </variables>
  <variables name="inst2pat_l">
    <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
      <details key="name" value="_rQxpAAskEeigQsLVMUeRQw"/>
      <details key="identifier" value="inst2pat_l"/>
    </annotations>
  </variables>
  <invariants name="link_ty" predicate="links ∈ ran(components) ↔ Link">
    <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
      <details key="name" value="_S_fWR74_EeeN0675uvquSw"/>
      <details key="label" value="link_ty"/>
    </annotations>
  </invariants>
  <invariants name="link_finite" predicate="∀c·finite(links[{c}])">
    <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
      <details key="name" value="_S_fWSL4_EeeN0675uvquSw"/>
      <details key="label" value="link_finite"/>
    </annotations>
  </invariants>
  <invariants name="link_not_shared" predicate="links∼ ∈ Link ⇸ Component">
    <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
      <details key="name" value="_S_f9UL4_EeeN0675uvquSw"/>
      <details key="label" value="link_not_shared"/>
    </annotations>
  </invariants>
  <invariants name="src_ty" predicate="src ∈ ran(links) → ran(ports)">
    <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
      <details key="name" value="_S_f9Ub4_EeeN0675uvquSw"/>
      <details key="label" value="src_ty"/>
    </annotations>
  </invariants>
  <invariants name="dst_ty" predicate="dst ∈ ran(links) → ran(ports)">
    <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
      <details key="name" value="_S_f9Ur4_EeeN0675uvquSw"/>
      <details key="label" value="dst_ty"/>
    </annotations>
  </invariants>
  <invariants name="link_cii" predicate="links; ((src ⊗ dst) ▷ (IPort × IPort)) ⊆ ports ⊗ (container∼; ports)">
    <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
      <details key="name" value="_0ffzssOZEeeQteb5bDCu6g"/>
      <details key="label" value="link_cii"/>
    </annotations>
  </invariants>
  <invariants name="link_coi" predicate="links; ((src ⊗ dst) ▷ (OPort × IPort)) ⊆ (container∼;ports) ⊗ (container∼; ports)">
    <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
      <details key="name" value="_Z5iv0vg-EeeeS5KQUtrGlw"/>
      <details key="label" value="link_coi"/>
    </annotations>
  </invariants>
  <invariants name="link_coo" predicate="links; ((src ⊗ dst) ▷ (OPort × OPort)) ⊆ (container∼; ports) ⊗ ports">
    <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
      <details key="name" value="_GNeQ0_qOEeectLZKwQfI0A"/>
      <details key="label" value="link_coo"/>
    </annotations>
  </invariants>
  <invariants name="link_cio" predicate="links; ((src ⊗ dst) ▷ (IPort × OPort)) ⊆ ports ⊗ ports">
    <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
      <details key="name" value="_GNe34PqOEeectLZKwQfI0A"/>
      <details key="label" value="link_cio"/>
    </annotations>
  </invariants>
  <invariants name="transp_src" predicate="∀l·l∈(components;links)[{Pat}]∩Transpose ⇒ p_multiplicity(src(l)) = c_multiplicity(ports∼(dst(l)))">
    <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
      <details key="name" value="_69ZZAPq0EeectLZKwQfI0A"/>
      <details key="label" value="transp_src"/>
    </annotations>
  </invariants>
  <invariants name="transp_dst" predicate="∀l·l∈(components;links)[{Pat}]∩Transpose ⇒ p_multiplicity(dst(l)) = c_multiplicity(ports∼(src(l)))">
    <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
      <details key="name" value="_X1DEFAA3EeictLZKwQfI0A"/>
      <details key="label" value="transp_dst"/>
    </annotations>
  </invariants>
  <invariants name="c_links_done" predicate="c_links_done ⊆ (components;links)[{Pat}] × components[{Inst}]">
    <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
      <details key="name" value="_ocRYQAbKEeiFlqW-8GKglg"/>
      <details key="label" value="c_links_done"/>
    </annotations>
  </invariants>
  <invariants name="inst2pat_l_ty" predicate="inst2pat_l ∈ (components;links)[{Inst}] → (components;links)[{Pat}]">
    <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
      <details key="name" value="_ocRYQQbKEeiFlqW-8GKglg"/>
      <details key="label" value="inst2pat_l_ty"/>
    </annotations>
  </invariants>
  <invariants name="inst2pat_l_preserve_type" predicate="∀K·K∈LKind ⇒ inst2pat_l[K] ⊆ K">
    <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
      <details key="name" value="_cztlsQi3EeiFlqW-8GKglg"/>
      <details key="label" value="inst2pat_l_preserve_type"/>
    </annotations>
  </invariants>
  <invariants name="inst2pat_l_src" predicate="inst2pat_l;src = src;inst2pat_p">
    <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
      <details key="name" value="_rQxpAQskEeigQsLVMUeRQw"/>
      <details key="label" value="inst2pat_l_src"/>
    </annotations>
  </invariants>
  <invariants name="inst2pat_l_dst" predicate="inst2pat_l;dst = dst;inst2pat_p">
    <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
      <details key="name" value="_rQxpAgskEeigQsLVMUeRQw"/>
      <details key="label" value="inst2pat_l_dst"/>
    </annotations>
  </invariants>
  <invariants name="transp_correct1" predicate="∀l·l∈(components;links)[{Inst}] ∩ Transpose ⇒ p_index(src(l)) = c_index(ports∼(dst(l)))">
    <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
      <details key="name" value="_EviiYAslEeigQsLVMUeRQw"/>
      <details key="label" value="transp_correct1"/>
    </annotations>
  </invariants>
  <invariants name="transp_correct2" predicate="∀l·l∈(components;links)[{Inst}] ∩ Transpose ⇒ p_index(dst(l)) = c_index(ports∼(src(l)))">
    <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
      <details key="name" value="_EviiYQslEeigQsLVMUeRQw"/>
      <details key="label" value="transp_correct2"/>
    </annotations>
  </invariants>
  <variant expression="((components;links)[{Pat}] × components[{Inst}]) ∖ c_links_done">
    <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
      <details key="name" value="_K8id4Ai5EeiFlqW-8GKglg"/>
    </annotations>
  </variant>
  <events name="instanciate_pattern" extended="true">
    <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
      <details key="name" value="'"/>
      <details key="label" value="instanciate_pattern"/>
    </annotations>
    <annotations source="http:///org/eventb/core/RodinReferenceNamesAnnotations">
      <details key="refines instanciate_pattern" value="_ypF-0PlnEeeeS5KQUtrGlw"/>
    </annotations>
    <refines href="../mPort.bum#http://emf.eventb.org/models/core/machine/2014::Event::mPort.instanciate_pattern"/>
    <guards name="transp_ctr1" predicate="∀l·l∈(components;links)[{Pat}]∩Transpose ∧ ports∼(dst(l)) ∈ dom(inst_components) ⇒ card(inst_ports[{src(l)}])=card(inst_components[{ports∼(dst(l))}])">
      <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
        <details key="name" value="_S_eIJL4_EeeN0675uvquSw"/>
        <details key="label" value="transp_ctr1"/>
      </annotations>
    </guards>
    <guards name="transp_ctr2" predicate="∀l·l∈(components;links)[{Pat}]∩Transpose ∧ ports∼(dst(l)) ∉ dom(inst_components) ⇒ card(inst_ports[{src(l)}])=c_mult_others(ports∼(dst(l)))">
      <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
        <details key="name" value="_S_eIJb4_EeeN0675uvquSw"/>
        <details key="label" value="transp_ctr2"/>
      </annotations>
    </guards>
    <guards name="transp_ctr3" predicate="∀l·l∈(components;links)[{Pat}]∩Transpose ∧ ports∼(src(l)) ∈ dom(inst_components) ⇒ card(inst_ports[{dst(l)}])=card(inst_components[{ports∼(src(l))}])">
      <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
        <details key="name" value="_S_eIJr4_EeeN0675uvquSw"/>
        <details key="label" value="transp_ctr3"/>
      </annotations>
    </guards>
    <guards name="transp_ctr4" predicate="∀l·l∈(components;links)[{Pat}]∩Transpose ∧ ports∼(src(l)) ∉ dom(inst_components) ⇒ card(inst_ports[{dst(l)}])=c_mult_others(ports∼(src(l)))">
      <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
        <details key="name" value="_S_eIJ74_EeeN0675uvquSw"/>
        <details key="label" value="transp_ctr4"/>
      </annotations>
    </guards>
    <actions name="links" action="links ≔ components[{Inst}] ⩤ links">
      <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
        <details key="name" value="_S_evNr4_EeeN0675uvquSw"/>
        <details key="label" value="links"/>
      </annotations>
    </actions>
    <actions name="src" action="src ≔ (components;links)[{Inst}] ⩤ src">
      <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
        <details key="name" value="_oe6yMMOjEeeQteb5bDCu6g"/>
        <details key="label" value="src"/>
      </annotations>
    </actions>
    <actions name="dst" action="dst ≔ (components;links)[{Inst}] ⩤ dst">
      <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
        <details key="name" value="_oe6yMcOjEeeQteb5bDCu6g"/>
        <details key="label" value="dst"/>
      </annotations>
    </actions>
    <actions name="inst2pat_l" action="inst2pat_l ≔ ∅">
      <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
        <details key="name" value="_0IWfoAK-EeiAPf1wPUl3Gw"/>
        <details key="label" value="inst2pat_l"/>
      </annotations>
    </actions>
    <actions name="c_links_done" action="c_links_done ≔ ∅">
      <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
        <details key="name" value="_SwNs4ALXEei9ocE08JsPSw"/>
        <details key="label" value="c_links_done"/>
      </annotations>
    </actions>
  </events>
  <events name="unfold_root_c" extended="true">
    <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
      <details key="name" value="_JZbnAOGWEeeUoZak4Ibgcg"/>
      <details key="label" value="unfold_root_c"/>
    </annotations>
    <annotations source="http:///org/eventb/core/RodinReferenceNamesAnnotations">
      <details key="refines unfold_root_c" value="_7XcAsAK3EeiAPf1wPUl3Gw"/>
    </annotations>
    <refines href="../mPort.bum#http://emf.eventb.org/models/core/machine/2014::Event::mPort.unfold_root_c"/>
  </events>
  <events name="unfold_p" extended="true">
    <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
      <details key="name" value="_QZUfguTyEeemadOWCHlIvw"/>
      <details key="label" value="unfold_p"/>
    </annotations>
    <annotations source="http:///org/eventb/core/RodinReferenceNamesAnnotations">
      <details key="refines unfold_p" value="_-RPi0P06Eees7pYemx4WBQ"/>
    </annotations>
    <refines href="../mPort.bum#http://emf.eventb.org/models/core/machine/2014::Event::mPort.unfold_p"/>
  </events>
  <events name="clone_c" extended="true">
    <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
      <details key="name" value="_QZVGk-TyEeemadOWCHlIvw"/>
      <details key="label" value="clone_c"/>
    </annotations>
    <annotations source="http:///org/eventb/core/RodinReferenceNamesAnnotations">
      <details key="refines clone_c" value="_-RQJ4P06Eees7pYemx4WBQ"/>
    </annotations>
    <refines href="../mPort.bum#http://emf.eventb.org/models/core/machine/2014::Event::mPort.clone_c"/>
  </events>
  <events name="unfold_node_c" extended="true">
    <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
      <details key="name" value="_H7W2gPg_EeeeS5KQUtrGlw"/>
      <details key="label" value="unfold_node_c"/>
    </annotations>
    <annotations source="http:///org/eventb/core/RodinReferenceNamesAnnotations">
      <details key="refines unfold_node_c" value="_7XlKoAK3EeiAPf1wPUl3Gw"/>
    </annotations>
    <refines href="../mPort.bum#http://emf.eventb.org/models/core/machine/2014::Event::mPort.unfold_node_c"/>
  </events>
  <events comment="between 2 subcomponents" name="unfold_node_link_oi_Transpose" convergence="convergent" extended="false">
    <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
      <details key="name" value="_ypJCIflnEeeeS5KQUtrGlw"/>
      <details key="label" value="unfold_node_link_oi_Transpose"/>
      <details key="comment" value="between 2 subcomponents"/>
    </annotations>
    <parameters name="spi">
      <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
        <details key="name" value="_S_dhEr4_EeeN0675uvquSw"/>
        <details key="identifier" value="spi"/>
      </annotations>
    </parameters>
    <parameters name="sci">
      <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
        <details key="name" value="_S_eIIL4_EeeN0675uvquSw"/>
        <details key="identifier" value="sci"/>
      </annotations>
    </parameters>
    <parameters name="dpi">
      <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
        <details key="name" value="_JZbnAuGWEeeUoZak4Ibgcg"/>
        <details key="identifier" value="dpi"/>
      </annotations>
    </parameters>
    <parameters comment="source/dest ports and components in instance" name="dci">
      <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
        <details key="name" value="_nOhFwOGpEeeUoZak4Ibgcg"/>
        <details key="identifier" value="dci"/>
        <details key="comment" value="source/dest ports and components in instance"/>
      </annotations>
    </parameters>
    <parameters name="l">
      <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
        <details key="name" value="_RYtJ0OT7EeemadOWCHlIvw"/>
        <details key="identifier" value="l"/>
      </annotations>
    </parameters>
    <parameters name="new_l">
      <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
        <details key="name" value="_nHIsIARrEei9ocE08JsPSw"/>
        <details key="identifier" value="new_l"/>
      </annotations>
    </parameters>
    <parameters comment="container" name="c">
      <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
        <details key="name" value="_nHJTMARrEei9ocE08JsPSw"/>
        <details key="identifier" value="c"/>
        <details key="comment" value="container"/>
      </annotations>
    </parameters>
    <guards name="l_ty" predicate="l ∈ (components;links)[{Pat}] ∩ Transpose">
      <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
        <details key="name" value="_JZbnBOGWEeeUoZak4Ibgcg"/>
        <details key="label" value="l_ty"/>
      </annotations>
    </guards>
    <guards name="src_o" predicate="src(l) ∈ OPort">
      <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
        <details key="name" value="_nOhFweGpEeeUoZak4Ibgcg"/>
        <details key="label" value="src_o"/>
      </annotations>
    </guards>
    <guards name="dst_i" predicate="dst(l) ∈ IPort">
      <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
        <details key="name" value="_yq8FweGpEeeUoZak4Ibgcg"/>
        <details key="label" value="dst_i"/>
      </annotations>
    </guards>
    <guards name="c" predicate="c ∈ components[{Inst}] ∩ dom(inst2pat_c)">
      <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
        <details key="name" value="_3EQ2ceGpEeeUoZak4Ibgcg"/>
        <details key="label" value="c"/>
      </annotations>
    </guards>
    <guards name="not_done" predicate="l↦c ∉ c_links_done">
      <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
        <details key="name" value="_RYtJ0uT7EeemadOWCHlIvw"/>
        <details key="label" value="not_done"/>
      </annotations>
    </guards>
    <guards name="sci" predicate="sci ∈ 1‥c_multiplicity(ports∼(src(l))) ↣ container∼[{c}]">
      <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
        <details key="name" value="_RYtJ0-T7EeemadOWCHlIvw"/>
        <details key="label" value="sci"/>
      </annotations>
    </guards>
    <guards name="sci_ctr" predicate="inst2pat_c[ran(sci)] ⊆ {ports∼(src(l))}">
      <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
        <details key="name" value="_RYtJ1OT7EeemadOWCHlIvw"/>
        <details key="label" value="sci_ctr"/>
      </annotations>
    </guards>
    <guards name="sci_c_index" predicate="sci;c_index = id">
      <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
        <details key="name" value="_RYtJ1eT7EeemadOWCHlIvw"/>
        <details key="label" value="sci_c_index"/>
      </annotations>
    </guards>
    <guards name="dci" predicate="dci ∈ 1‥c_multiplicity(ports∼(dst(l))) ↣ container∼[{c}]">
      <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
        <details key="name" value="_WfAcMAK-EeiAPf1wPUl3Gw"/>
        <details key="label" value="dci"/>
      </annotations>
    </guards>
    <guards name="dci_ctr" predicate="inst2pat_c[ran(dci)] ⊆ {ports∼(dst(l))}">
      <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
        <details key="name" value="_nHJTNQRrEei9ocE08JsPSw"/>
        <details key="label" value="dci_ctr"/>
      </annotations>
    </guards>
    <guards name="dci_c_index" predicate="dci;c_index = id">
      <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
        <details key="name" value="_DdBJsAc3EeiFlqW-8GKglg"/>
        <details key="label" value="dci_c_index"/>
      </annotations>
    </guards>
    <guards name="spi_ty" predicate="spi ∈ ran(sci) → (1‥p_multiplicity(src(l)) ↣ inst2pat_p∼[{src(l)}])">
      <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
        <details key="name" value="_70QzIAc3EeiFlqW-8GKglg"/>
        <details key="label" value="spi_ty"/>
      </annotations>
    </guards>
    <guards name="spi_ctr" predicate="∀ci·ci∈ran(sci) ⇒ spi(ci) ∈ 1‥p_multiplicity(src(l)) ↣ ports[{ci}] ∩ OPort">
      <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
        <details key="name" value="_6bPz8AdGEeiFlqW-8GKglg"/>
        <details key="label" value="spi_ctr"/>
      </annotations>
    </guards>
    <guards name="spi_p_index" predicate="∀ci·ci∈ran(sci) ⇒ spi(ci);p_index = id">
      <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
        <details key="name" value="_6bPz8QdGEeiFlqW-8GKglg"/>
        <details key="label" value="spi_p_index"/>
      </annotations>
    </guards>
    <guards name="dpi_ty" predicate="dpi ∈ ran(dci) → (1‥p_multiplicity(dst(l)) ↣ inst2pat_p∼[{dst(l)}])">
      <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
        <details key="name" value="_nxuuQQi-EeiFlqW-8GKglg"/>
        <details key="label" value="dpi_ty"/>
      </annotations>
    </guards>
    <guards name="dpi_ctr" predicate="∀ci·ci∈ran(dci) ⇒ dpi(ci) ∈ 1‥p_multiplicity(dst(l)) ↣ ports[{ci}] ∩ IPort">
      <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
        <details key="name" value="_quOpsAjAEeiFlqW-8GKglg"/>
        <details key="label" value="dpi_ctr"/>
      </annotations>
    </guards>
    <guards name="dpi_p_index" predicate="∀ci·ci∈ran(dci) ⇒ dpi(ci);p_index = id">
      <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
        <details key="name" value="_BL1LoAkjEeiFlqW-8GKglg"/>
        <details key="label" value="dpi_p_index"/>
      </annotations>
    </guards>
    <guards name="new_l_ty" predicate="new_l ∈ 1‥p_multiplicity(src(l)) × 1‥c_multiplicity(ports∼(src(l))) ↣ Transpose ∖ ran(links)">
      <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
        <details key="name" value="_BL1ysAkjEeiFlqW-8GKglg"/>
        <details key="label" value="new_l_ty"/>
      </annotations>
    </guards>
    <actions name="links" action="links ≔ links ∪ ({c} × ran(new_l))">
      <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
        <details key="name" value="_ov6eYALXEei9ocE08JsPSw"/>
        <details key="label" value="links"/>
      </annotations>
    </actions>
    <actions name="nsrc" action="src ≔ src ∪ {ip,ic· ip ↦ ic ∈ dom(new_l) ∣ new_l(ip↦ic) ↦ spi(sci(ic))(ip)}">
      <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
        <details key="name" value="_ztHbMAaaEeiFlqW-8GKglg"/>
        <details key="label" value="nsrc"/>
      </annotations>
    </actions>
    <actions name="ndst" action="dst ≔ dst ∪ {ip,ic· ip ↦ ic ∈ dom(new_l) ∣ new_l(ip↦ic) ↦ dpi(dci(ip))(ic)}">
      <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
        <details key="name" value="_1ZIboAabEeiFlqW-8GKglg"/>
        <details key="label" value="ndst"/>
      </annotations>
    </actions>
    <actions name="inst2pat_l" action="inst2pat_l ≔ inst2pat_l ∪ (ran(new_l) × {l})">
      <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
        <details key="name" value="_1ZIboQabEeiFlqW-8GKglg"/>
        <details key="label" value="inst2pat_l"/>
      </annotations>
    </actions>
    <actions name="c_links_done" action="c_links_done ≔ c_links_done ∪ {l↦c}">
      <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
        <details key="name" value="_czs-oAi3EeiFlqW-8GKglg"/>
        <details key="label" value="c_links_done"/>
      </annotations>
    </actions>
  </events>
  <events name="apply_pattern" extended="true">
    <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
      <details key="name" value="_u6P4gAK9EeiAPf1wPUl3Gw"/>
      <details key="label" value="apply_pattern"/>
    </annotations>
    <annotations source="http:///org/eventb/core/RodinReferenceNamesAnnotations">
      <details key="refines apply_pattern" value="_u6P4gQK9EeiAPf1wPUl3Gw"/>
    </annotations>
    <refines href="../mPort.bum#http://emf.eventb.org/models/core/machine/2014::Event::mPort.apply_pattern"/>
    <parameters name="inst_links">
      <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
        <details key="name" value="_nHJTMQRrEei9ocE08JsPSw"/>
        <details key="identifier" value="inst_links"/>
      </annotations>
    </parameters>
    <parameters name="new_links">
      <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
        <details key="name" value="_nxuuQAi-EeiFlqW-8GKglg"/>
        <details key="identifier" value="new_links"/>
      </annotations>
    </parameters>
    <guards name="inst_links_ty" predicate="inst_links ∈ (components;links)[{Inst}] ⤔ (components;links)[{Mdl}]">
      <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
        <details key="name" value="_Bszp0AsoEeigQsLVMUeRQw"/>
        <details key="label" value="inst_links_ty"/>
      </annotations>
    </guards>
    <guards comment="Les ports sources d'un lien instancié sont instanciés" name="inst_src" predicate="inst_links ; src ⊆ src; inst_ports">
      <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
        <details key="name" value="_G8ASkAsoEeigQsLVMUeRQw"/>
        <details key="label" value="inst_src"/>
        <details key="comment" value="Les ports sources d'un lien instancié sont instanciés"/>
      </annotations>
    </guards>
    <guards comment="Les ports cibles d'un lien instancié sont instanciés" name="inst_dst" predicate="inst_links ; dst ⊆ dst; inst_ports">
      <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
        <details key="name" value="_78O84AsoEeigQsLVMUeRQw"/>
        <details key="label" value="inst_dst"/>
        <details key="comment" value="Les ports cibles d'un lien instancié sont instanciés"/>
      </annotations>
    </guards>
    <guards name="nl" predicate="new_links ∈ (components;links)[{Inst}] ∖ dom(inst_links) ↣ Link ∖ ran(links)">
      <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
        <details key="name" value="_78O84QsoEeigQsLVMUeRQw"/>
        <details key="label" value="nl"/>
      </annotations>
    </guards>
    <actions name="s" action="src ≔ src  (new_links∼;src;(inst_ports ∪ new_ports))">
      <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
        <details key="name" value="_czuz0gi3EeiFlqW-8GKglg"/>
        <details key="label" value="s"/>
      </annotations>
    </actions>
    <actions name="d" action="dst ≔ dst  (new_links∼;dst;(inst_ports ∪ new_ports))">
      <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
        <details key="name" value="_vsWoMAs_EeiJbMmmYBswhA"/>
        <details key="label" value="d"/>
      </annotations>
    </actions>
    <actions name="l" action="links ≔ links ∪ ((inst_components∪new_components)∼;links;new_links)">
      <annotations source="http:///org/eventb/core/RodinInternalAnnotations">
        <details key="name" value="_Ce3aEAtCEeiJbMmmYBswhA"/>
        <details key="label" value="l"/>
      </annotations>
    </actions>
  </events>
</machine:Machine>