<?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="ACED00057415A26D616368696E65206D4C696E6B20726566696E6573206D506F727420207365657320634C696E6B0A0A7661726961626C657320636F6D706F6E656E747320636F6E7461696E657220635F6D756C7469706C696369747920746F5F636C6F6E655F6320635F696E64657820746F5F756E666F6C645F6320746F5F756E666F6C645F635F696E20696E7374327061745F632070726F7065727469657320706F72747320705F6D756C7469706C696369747920705F696E64657820746F5F756E666F6C645F705F696E20696E7374327061745F70206C696E6B73207372632064737420635F6C696E6B735F646F6E6520696E7374327061745F6C0A0A696E76617269616E74730A2020406C696E6B5F7479206C696E6B7320E288882072616E28636F6D706F6E656E74732920E28694204C696E6B0A2020406C696E6B5F66696E69746520E2888063C2B766696E697465286C696E6B735B7B637D5D290A2020406C696E6B5F6E6F745F736861726564206C696E6B73E288BC20E28888204C696E6B20E287B820436F6D706F6E656E740A2020407372635F74792073726320E288882072616E286C696E6B732920E286922072616E28706F727473290A2020406473745F74792064737420E288882072616E286C696E6B732920E286922072616E28706F727473290A2020406C696E6B5F636969206C696E6B733B20282873726320E28A97206473742920E296B7202849506F727420C3972049506F7274292920E28A8620706F72747320E28A972028636F6E7461696E6572E288BC3B20706F727473290A2020406C696E6B5F636F69206C696E6B733B20282873726320E28A97206473742920E296B720284F506F727420C3972049506F7274292920E28A862028636F6E7461696E6572E288BC3B706F7274732920E28A972028636F6E7461696E6572E288BC3B20706F727473290A2020406C696E6B5F636F6F206C696E6B733B20282873726320E28A97206473742920E296B720284F506F727420C397204F506F7274292920E28A862028636F6E7461696E6572E288BC3B20706F7274732920E28A9720706F7274730A2020406C696E6B5F63696F206C696E6B733B20282873726320E28A97206473742920E296B7202849506F727420C397204F506F7274292920E28A8620706F72747320E28A9720706F7274730A2020407472616E73705F73726320E288806CC2B76CE2888828636F6D706F6E656E74733B6C696E6B73295B7B5061747D5DE288A95472616E73706F736520E2879220705F6D756C7469706C696369747928737263286C2929203D20635F6D756C7469706C696369747928706F727473E288BC28647374286C2929290A2020407472616E73705F64737420E288806CC2B76CE2888828636F6D706F6E656E74733B6C696E6B73295B7B5061747D5DE288A95472616E73706F736520E2879220705F6D756C7469706C696369747928647374286C2929203D20635F6D756C7469706C696369747928706F727473E288BC28737263286C2929290A202040635F6C696E6B735F646F6E6520635F6C696E6B735F646F6E6520E28A862028636F6D706F6E656E74733B6C696E6B73295B7B5061747D5D20C39720636F6D706F6E656E74735B7B496E73747D5D0A202040696E7374327061745F6C5F747920696E7374327061745F6C20E288882028636F6D706F6E656E74733B6C696E6B73295B7B496E73747D5D20E286922028636F6D706F6E656E74733B6C696E6B73295B7B5061747D5D0A202040696E7374327061745F6C5F70726573657276655F7479706520E288804BC2B74BE288884C4B696E6420E2879220696E7374327061745F6C5B4B5D20E28A86204B0A202040696E7374327061745F6C5F73726320696E7374327061745F6C3B737263203D207372633B696E7374327061745F700A202040696E7374327061745F6C5F64737420696E7374327061745F6C3B647374203D206473743B696E7374327061745F700A2020407472616E73705F636F72726563743120E288806CC2B76CE2888828636F6D706F6E656E74733B6C696E6B73295B7B496E73747D5D20E288A9205472616E73706F736520E2879220705F696E64657828737263286C2929203D20635F696E64657828706F727473E288BC28647374286C2929290A2020407472616E73705F636F72726563743220E288806CC2B76CE2888828636F6D706F6E656E74733B6C696E6B73295B7B496E73747D5D20E288A9205472616E73706F736520E2879220705F696E64657828647374286C2929203D20635F696E64657828706F727473E288BC28737263286C2929290A0A76617269616E74202828636F6D706F6E656E74733B6C696E6B73295B7B5061747D5D20C39720636F6D706F6E656E74735B7B496E73747D5D2920E2889620635F6C696E6B735F646F6E650A0A6576656E74730A20206576656E7420696E7374616E63696174655F7061747465726E20657874656E647320696E7374616E63696174655F7061747465726E0A2020202077686572650A202020202020407472616E73705F6374723120E288806CC2B76CE2888828636F6D706F6E656E74733B6C696E6B73295B7B5061747D5DE288A95472616E73706F736520E288A720706F727473E288BC28647374286C292920E2888820646F6D28696E73745F636F6D706F6E656E74732920E28792206361726428696E73745F706F7274735B7B737263286C297D5D293D6361726428696E73745F636F6D706F6E656E74735B7B706F727473E288BC28647374286C29297D5D290A202020202020407472616E73705F6374723220E288806CC2B76CE2888828636F6D706F6E656E74733B6C696E6B73295B7B5061747D5DE288A95472616E73706F736520E288A720706F727473E288BC28647374286C292920E2888920646F6D28696E73745F636F6D706F6E656E74732920E28792206361726428696E73745F706F7274735B7B737263286C297D5D293D635F6D756C745F6F746865727328706F727473E288BC28647374286C2929290A202020202020407472616E73705F6374723320E288806CC2B76CE2888828636F6D706F6E656E74733B6C696E6B73295B7B5061747D5DE288A95472616E73706F736520E288A720706F727473E288BC28737263286C292920E2888820646F6D28696E73745F636F6D706F6E656E74732920E28792206361726428696E73745F706F7274735B7B647374286C297D5D293D6361726428696E73745F636F6D706F6E656E74735B7B706F727473E288BC28737263286C29297D5D290A202020202020407472616E73705F6374723420E288806CC2B76CE2888828636F6D706F6E656E74733B6C696E6B73295B7B5061747D5DE288A95472616E73706F736520E288A720706F727473E288BC28737263286C292920E2888920646F6D28696E73745F636F6D706F6E656E74732920E28792206361726428696E73745F706F7274735B7B647374286C297D5D293D635F6D756C745F6F746865727328706F727473E288BC28737263286C2929290A202020207468656E0A202020202020406C696E6B73206C696E6B7320E2899420636F6D706F6E656E74735B7B496E73747D5D20E2A9A4206C696E6B730A202020202020407372632073726320E289942028636F6D706F6E656E74733B6C696E6B73295B7B496E73747D5D20E2A9A4207372630A202020202020406473742064737420E289942028636F6D706F6E656E74733B6C696E6B73295B7B496E73747D5D20E2A9A4206473740A20202020202040696E7374327061745F6C20696E7374327061745F6C20E2899420E288850A20202020202040635F6C696E6B735F646F6E6520635F6C696E6B735F646F6E6520E2899420E288850A2020656E640A0A20206576656E7420756E666F6C645F726F6F745F6320657874656E647320756E666F6C645F726F6F745F630A2020656E640A0A20206576656E7420756E666F6C645F7020657874656E647320756E666F6C645F700A2020656E640A0A20206576656E7420636C6F6E655F6320657874656E647320636C6F6E655F630A2020656E640A0A20206576656E7420756E666F6C645F6E6F64655F6320657874656E647320756E666F6C645F6E6F64655F630A2020656E640A0A2020636F6E76657267656E74206576656E7420756E666F6C645F6E6F64655F6C696E6B5F6F695F5472616E73706F7365202F2F206265747765656E203220737562636F6D706F6E656E74730A20202020616E792073706920736369206470690A2020202020202020646369202F2F20736F757263652F6465737420706F72747320616E6420636F6D706F6E656E747320696E20696E7374616E63650A20202020202020206C206E65775F6C0A202020202020202063202F2F20636F6E7461696E65720A0A2020202077686572650A202020202020406C5F7479206C20E288882028636F6D706F6E656E74733B6C696E6B73295B7B5061747D5D20E288A9205472616E73706F73650A202020202020407372635F6F20737263286C2920E28888204F506F72740A202020202020406473745F6920647374286C2920E288882049506F72740A2020202020204063206320E2888820636F6D706F6E656E74735B7B496E73747D5D20E288A920646F6D28696E7374327061745F63290A202020202020406E6F745F646F6E65206CE286A66320E2888920635F6C696E6B735F646F6E650A202020202020407363692073636920E288882031E280A5635F6D756C7469706C696369747928706F727473E288BC28737263286C29292920E286A320636F6E7461696E6572E288BC5B7B637D5D0A202020202020407363695F63747220696E7374327061745F635B72616E28736369295D20E28A86207B706F727473E288BC28737263286C29297D0A202020202020407363695F635F696E646578207363693B635F696E646578203D2069640A202020202020406463692064636920E288882031E280A5635F6D756C7469706C696369747928706F727473E288BC28647374286C29292920E286A320636F6E7461696E6572E288BC5B7B637D5D0A202020202020406463695F63747220696E7374327061745F635B72616E28646369295D20E28A86207B706F727473E288BC28647374286C29297D0A202020202020406463695F635F696E646578206463693B635F696E646578203D2069640A202020202020407370695F74792073706920E288882072616E287363692920E28692202831E280A5705F6D756C7469706C696369747928737263286C292920E286A320696E7374327061745F70E288BC5B7B737263286C297D5D290A202020202020407370695F63747220E288806369C2B76369E2888872616E287363692920E28792207370692863692920E288882031E280A5705F6D756C7469706C696369747928737263286C292920E286A320706F7274735B7B63697D5D20E288A9204F506F72740A202020202020407370695F705F696E64657820E288806369C2B76369E2888872616E287363692920E2879220737069286369293B705F696E646578203D2069640A202020202020406470695F74792064706920E288882072616E286463692920E28692202831E280A5705F6D756C7469706C696369747928647374286C292920E286A320696E7374327061745F70E288BC5B7B647374286C297D5D290A202020202020406470695F63747220E288806369C2B76369E2888872616E286463692920E28792206470692863692920E288882031E280A5705F6D756C7469706C696369747928647374286C292920E286A320706F7274735B7B63697D5D20E288A92049506F72740A202020202020406470695F705F696E64657820E288806369C2B76369E2888872616E286463692920E2879220647069286369293B705F696E646578203D2069640A202020202020406E65775F6C5F7479206E65775F6C20E288882031E280A5705F6D756C7469706C696369747928737263286C292920C3972031E280A5635F6D756C7469706C696369747928706F727473E288BC28737263286C29292920E286A3205472616E73706F736520E288962072616E286C696E6B73290A202020207468656E0A202020202020406C696E6B73206C696E6B7320E28994206C696E6B7320E288AA20287B637D20C3972072616E286E65775F6C29290A202020202020406E7372632073726320E289942073726320E288AA207B69702C6963C2B720697020E286A620696320E2888820646F6D286E65775F6C2920E288A3206E65775F6C286970E286A669632920E286A620737069287363692869632929286970297D0A202020202020406E6473742064737420E289942064737420E288AA207B69702C6963C2B720697020E286A620696320E2888820646F6D286E65775F6C2920E288A3206E65775F6C286970E286A669632920E286A620647069286463692869702929286963297D0A20202020202040696E7374327061745F6C20696E7374327061745F6C20E2899420696E7374327061745F6C20E288AA202872616E286E65775F6C2920C397207B6C7D290A20202020202040635F6C696E6B735F646F6E6520635F6C696E6B735F646F6E6520E2899420635F6C696E6B735F646F6E6520E288AA207B6CE286A6637D0A2020656E640A0A20206576656E74206170706C795F7061747465726E20657874656E6473206170706C795F7061747465726E0A20202020616E7920696E73745F6C696E6B73206E65775F6C696E6B730A2020202077686572650A20202020202040696E73745F6C696E6B735F747920696E73745F6C696E6B7320E288882028636F6D706F6E656E74733B6C696E6B73295B7B496E73747D5D20E2A4942028636F6D706F6E656E74733B6C696E6B73295B7B4D646C7D5D0A20202020202040696E73745F73726320696E73745F6C696E6B73203B2073726320E28A86207372633B20696E73745F706F727473202F2F204C657320706F72747320736F7572636573206427756E206C69656E20696E7374616E6369C3A920736F6E7420696E7374616E6369C3A9730A20202020202040696E73745F64737420696E73745F6C696E6B73203B2064737420E28A86206473743B20696E73745F706F727473202F2F204C657320706F727473206369626C6573206427756E206C69656E20696E7374616E6369C3A920736F6E7420696E7374616E6369C3A9730A202020202020406E6C206E65775F6C696E6B7320E288882028636F6D706F6E656E74733B6C696E6B73295B7B496E73747D5D20E2889620646F6D28696E73745F6C696E6B732920E286A3204C696E6B20E288962072616E286C696E6B73290A202020207468656E0A20202020202040732073726320E289942073726320EE848320286E65775F6C696E6B73E288BC3B7372633B28696E73745F706F72747320E288AA206E65775F706F72747329290A20202020202040642064737420E289942064737420EE848320286E65775F6C696E6B73E288BC3B6473743B28696E73745F706F72747320E288AA206E65775F706F72747329290A202020202020406C206C696E6B7320E28994206C696E6B7320E288AA202828696E73745F636F6D706F6E656E7473E288AA6E65775F636F6D706F6E656E747329E288BC3B6C696E6B733B6E65775F6C696E6B73290A2020656E640A656E640A"/>
  </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>