MOISE
/
Pattern-Instanciation-On-System-Engineering-Model
mirror of http://172.16.200.102/MOISE/Pattern-Instanciation-On-System-Engineering-Model.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity
This project is a demonstrator of pattern instanciation on system engineering model (pseim), made by the MOISE project. It contains the metamodel of the pseim, graphical and textual editors, formal verification models (event-B) and examples.
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
7 Commits
1 Branch
0 Tags
3.4 MiB
 
 
 
Tree: 650ef7b56a
Branches Tags
${ item.name }
Create tag ${ searchTerm }
Create branch ${ searchTerm }
from '650ef7b56a'
${ noResults }
Pattern-Instanciation-On-Sy.../Event-B/pseim/team/mPort.bum.xmb

444 lines
29 KiB
Raw Blame History Escape

<?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="mPort">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="configuration" value="org.eventb.core.fwd;de.prob.units.mchBase"/>
<details key="name" value="mPort"/>
</annotations>
<annotations source="http:///org/eventb/core/RodinReferenceNamesAnnotations">
<details key="refines mProperty" value="_gbAPMADlEei-meqqkXX9bA"/>
<details key="sees cPort" value="_0kfYMfqeEeectLZKwQfI0A"/>
</annotations>
<attributes key="org.eventb.texttools.text_lastmodified">
<value type="Long" value="ACED00057372000E6A6176612E6C616E672E4C6F6E673B8BE490CC8F23DF0200014A000576616C7565787200106A6176612E6C616E672E4E756D62657286AC951D0B94E08B02000078700000016272817494"/>
</attributes>
<attributes key="org.eventb.texttools.text_representation">
<value type="String" value="ACED0005740D0A6D616368696E65206D506F727420726566696E6573206D50726F70657274792020736565732063506F72740A0A7661726961626C657320636F6D706F6E656E747320636F6E7461696E657220635F6D756C7469706C696369747920746F5F636C6F6E655F6320635F696E64657820746F5F756E666F6C645F6320746F5F756E666F6C645F635F696E20696E7374327061745F63206350726F7065727469657320706F72747320705F6D756C7469706C696369747920705F696E64657820746F5F756E666F6C645F705F696E20696E7374327061745F700A0A696E76617269616E74730A202040706F727420706F72747320E288882072616E28636F6D706F6E656E74732920E2869420506F72740A202040706F72745F66696E69746520E2888063C2B766696E69746528706F7274735B7B637D5D290A202040706F72745F6E6F745F73686172656420706F727473E288BC20E2888820506F727420E287B820436F6D706F6E656E740A202040705F6D756C7420705F6D756C7469706C696369747920E288882028636F6D706F6E656E74733B706F727473295B5061747465726E5D20E2869220E284950A202040746F5F756E666F6C645F705F696E20746F5F756E666F6C645F705F696E20E288882028636F6D706F6E656E74733B706F727473295B7B5061747D5D20E2869420636F6D706F6E656E74735B7B496E73747D5D0A202040696E7374327061745F705F747920696E7374327061745F7020E288882028636F6D706F6E656E74733B706F727473295B7B496E73747D5D20E286922028636F6D706F6E656E74733B706F727473295B7B5061747D5D0A202040696E7374327061745F636F6D6D7020696E7374327061745F703B706F727473E288BC203D20706F727473E288BC3B696E7374327061745F630A202040746F5F756E666F6C645F705F696E7374327061742072616E28746F5F756E666F6C645F705F696E2920E28A8620646F6D28696E7374327061745F63290A202040746F5F756E666F6C645F705F696E5F636F6D7020746F5F756E666F6C645F705F696E3B696E7374327061745F6320E28A8620706F727473E288BC0A2020406932705F49506F727420696E7374327061745F705B49506F72745D20E28A862049506F72740A2020406932705F4F506F727420696E7374327061745F705B4F506F72745D20E28A86204F506F72740A202040705F696E6465785F747920705F696E64657820E2888820646F6D28696E7374327061745F702920E2869220E284950A0A76617269616E7420746F5F756E666F6C645F705F696E0A0A6576656E74730A20206576656E7420696E7374616E63696174655F7061747465726E20657874656E647320696E7374616E63696174655F7061747465726E0A20202020616E7920696E73745F706F72747320705F6D756C745F6F74686572730A2020202077686572650A20202020202040697020696E73745F706F72747320E288882028636F6D706F6E656E74733B706F727473295B7B5061747D5D20E286942028636F6D706F6E656E74733B706F727473295B7B4D646C7D5D0A2020202020204069707220696E73745F706F727473E288BC20E288882028636F6D706F6E656E74733B706F727473295B7B4D646C7D5D20E287B82028636F6D706F6E656E74733B706F727473295B7B5061747D5D0A20202020202040706D20705F6D756C745F6F746865727320E288882028636F6D706F6E656E74733B706F727473295B7B5061747D5D20E2889620646F6D28696E73745F706F7274732920E2869220E284950A2020202020207468656F72656D204074686D20E2888070C2B72066696E69746528696E73745F706F7274735B7B707D5D290A202020207468656E0A20202020202040705F6D756C7420705F6D756C7469706C696369747920E2899420705F6D756C7469706C696369747920EE84832028705F6D756C745F6F746865727320EE8483207B7070C2B77070E2888828636F6D706F6E656E74733B706F727473295B7B5061747D5D20E288A320707020E286A6206361726428696E73745F706F7274735B7B70707D5D297D290A20202020202040696E7374327061745F7020696E7374327061745F7020E2899420E288850A20202020202040706F72747320706F72747320E289942028636F6D706F6E656E74735B7B496E73747D5D2920E2A9A420706F7274730A20202020202040756E666F6C645F7020746F5F756E666F6C645F705F696E20E2899420E288850A20202020202040705F696E64657820705F696E64657820E2899420E288850A2020656E640A0A20206576656E7420756E666F6C645F726F6F745F6320657874656E647320756E666F6C645F726F6F745F630A2020656E640A0A20206576656E7420636C6F6E655F6320657874656E647320636C6F6E655F630A202020207468656E0A20202020202040756E666F6C645F705F696E20746F5F756E666F6C645F705F696E20E2899420746F5F756E666F6C645F705F696E20E288AA2028706F7274735B7B746F5F636C6F6E655F632863297D5D20C397207B637D290A2020656E640A0A20206576656E7420756E666F6C645F6E6F64655F6320657874656E647320756E666F6C645F6E6F64655F630A2020656E640A0A2020636F6E76657267656E74206576656E7420756E666F6C645F700A20202020616E792070202F2F20706F727420746F20756E666F6C640A202020202020202063202F2F2074617267657420636F6D706F6E656E740A20202020202020206E65775F70202F2F207265706C69636174656420706F7274730A0A2020202077686572650A20202020202040705F7479207020E286A6206320E2888820746F5F756E666F6C645F705F696E0A202020202020406E65775F705F7479206E65775F7020E288882031E280A5705F6D756C7469706C696369747928702920E286A320506F727420E288962072616E28636F6D706F6E656E74733B706F727473290A202020202020406475706C69636174655F49506F7274735F646972656374696F6E207020E288882049506F727420E287922072616E286E65775F702920E28A862049506F72740A202020202020406475706C69636174655F4F506F7274735F646972656374696F6E207020E28888204F506F727420E287922072616E286E65775F702920E28A86204F506F72740A202020207468656E0A202020202020406E65775F705F636F6D706F6E656E7420706F72747320E2899420706F72747320E288AA20287B637D20C3972072616E286E65775F7029290A20202020202040647020746F5F756E666F6C645F705F696E20E2899420746F5F756E666F6C645F705F696E20E28896207B70E286A6637D0A20202020202040696E7374327061745F7020696E7374327061745F7020E2899420696E7374327061745F7020E288AA202872616E286E65775F702920C397207B707D290A20202020202040705F696E64657820705F696E64657820E2899420705F696E64657820E288AA206E65775F70E288BC0A2020656E640A0A20206576656E74206170706C795F7061747465726E20657874656E6473206170706C795F7061747465726E0A20202020616E7920696E73745F706F727473206E65775F706F7274730A2020202077686572650A20202020202040697020696E73745F706F72747320E288882028636F6D706F6E656E74733B706F727473295B7B496E73747D5D20E2A4942028636F6D706F6E656E74733B706F727473295B7B4D646C7D5D0A202020202020406D705F6920696E73745F706F7274735B49506F72745D20E28A862049506F72740A202020202020406D705F6F20696E73745F706F7274735B4F506F72745D20E28A86204F506F72740A20202020202040706F7274735F696E73745F72656C5F636F6D705F696E737420706F727473E288BC5B646F6D28696E73745F706F727473295D20E28A8620646F6D28696E73745F636F6D706F6E656E747329202F2F204C657320706F72747320696E7374616E6369C3A97320736F6E742064657320706F72747320646520636F6D706F73616E747320696E7374616E6369C3A9730A20202020202040706F7274735F696E73745F72656C5F706F72745F636F6D7020696E73745F706F727473E288BC3B706F727473E288BC3B696E73745F636F6D706F6E656E747320E28A8620706F727473E288BC0A202020202020406E70206E65775F706F72747320E288882028636F6D706F6E656E74733B706F727473295B7B496E73747D5D20E2889620646F6D28696E73745F706F7274732920E286A320506F727420E288962072616E28636F6D706F6E656E74733B706F727473290A202020202020406E705F69206E65775F706F7274735B49506F72745D20E28A862049506F72740A202020202020406E705F6F206E65775F706F7274735B4F506F72745D20E28A86204F506F72740A202020207468656E0A202020202020406320706F72747320E2899420706F72747320E288AA202828696E73745F636F6D706F6E656E747320E288AA206E65775F636F6D706F6E656E747329E288BC3B706F7274733B28696E73745F706F72747320E288AA206E65775F706F72747329290A2020656E640A656E640A"/>
</attributes>
<refines href="../mProperty.bum#http://emf.eventb.org/models/core/machine/2014::Machine::mProperty"/>
<sees href="../cPort.buc#http://emf.eventb.org/models/core/context/2014::Context::cPort"/>
<variables name="components">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_0kf_QPqeEeectLZKwQfI0A"/>
<details key="identifier" value="components"/>
</annotations>
</variables>
<variables name="container">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_0kf_QfqeEeectLZKwQfI0A"/>
<details key="identifier" value="container"/>
</annotations>
</variables>
<variables name="c_multiplicity">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_0kf_QvqeEeectLZKwQfI0A"/>
<details key="identifier" value="c_multiplicity"/>
</annotations>
</variables>
<variables name="to_clone_c">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_0kf_Q_qeEeectLZKwQfI0A"/>
<details key="identifier" value="to_clone_c"/>
</annotations>
</variables>
<variables name="c_index">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_btIX4fqwEeectLZKwQfI0A"/>
<details key="identifier" value="c_index"/>
</annotations>
</variables>
<variables name="to_unfold_c">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_zYW3EPqwEeectLZKwQfI0A"/>
<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="_ANiZwPqxEeectLZKwQfI0A"/>
<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="_JtPOYPqxEeectLZKwQfI0A"/>
<details key="identifier" value="inst2pat_c"/>
</annotations>
</variables>
<variables name="cProperties">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_jRoOoPqxEeectLZKwQfI0A"/>
<details key="identifier" value="cProperties"/>
</annotations>
</variables>
<variables name="ports">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_oU9JIPqyEeectLZKwQfI0A"/>
<details key="identifier" value="ports"/>
</annotations>
</variables>
<variables name="p_multiplicity">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_6RL9kAA2EeictLZKwQfI0A"/>
<details key="identifier" value="p_multiplicity"/>
</annotations>
</variables>
<variables name="p_index">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_h1eCEADlEei-meqqkXX9bA"/>
<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="_zY448AK7EeiAPf1wPUl3Gw"/>
<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="_zY448QK7EeiAPf1wPUl3Gw"/>
<details key="identifier" value="inst2pat_p"/>
</annotations>
</variables>
<invariants name="port" predicate="ports ∈ ran(components) ↔ Port">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_0kf_RPqeEeectLZKwQfI0A"/>
<details key="label" value="port"/>
</annotations>
</invariants>
<invariants name="port_finite" predicate="∀c·finite(ports[{c}])">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_0kf_RfqeEeectLZKwQfI0A"/>
<details key="label" value="port_finite"/>
</annotations>
</invariants>
<invariants name="port_not_shared" predicate="ports∼ ∈ Port ⇸ Component">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_0kf_RvqeEeectLZKwQfI0A"/>
<details key="label" value="port_not_shared"/>
</annotations>
</invariants>
<invariants name="p_mult" predicate="p_multiplicity ∈ (components;ports)[Pattern] → ℕ">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_0kf_R_qeEeectLZKwQfI0A"/>
<details key="label" value="p_mult"/>
</annotations>
</invariants>
<invariants name="to_unfold_p_in" predicate="to_unfold_p_in ∈ (components;ports)[{Pat}] ↔ components[{Inst}]">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_btIX4vqwEeectLZKwQfI0A"/>
<details key="label" value="to_unfold_p_in"/>
</annotations>
</invariants>
<invariants name="inst2pat_p_ty" predicate="inst2pat_p ∈ (components;ports)[{Inst}] → (components;ports)[{Pat}]">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_zYW3EfqwEeectLZKwQfI0A"/>
<details key="label" value="inst2pat_p_ty"/>
</annotations>
</invariants>
<invariants name="inst2pat_commp" predicate="inst2pat_p;ports∼ = ports∼;inst2pat_c">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_F0IYkPriEeerIsS6OyYQ4w"/>
<details key="label" value="inst2pat_commp"/>
</annotations>
</invariants>
<invariants name="to_unfold_p_inst2pat" predicate="ran(to_unfold_p_in) ⊆ dom(inst2pat_c)">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_ui7VEAFGEei9ocE08JsPSw"/>
<details key="label" value="to_unfold_p_inst2pat"/>
</annotations>
</invariants>
<invariants name="to_unfold_p_in_comp" predicate="to_unfold_p_in;inst2pat_c ⊆ ports∼">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_zY448gK7EeiAPf1wPUl3Gw"/>
<details key="label" value="to_unfold_p_in_comp"/>
</annotations>
</invariants>
<invariants name="i2p_IPort" predicate="inst2pat_p[IPort] ⊆ IPort">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_22_TUALCEeiAPf1wPUl3Gw"/>
<details key="label" value="i2p_IPort"/>
</annotations>
</invariants>
<invariants name="i2p_OPort" predicate="inst2pat_p[OPort] ⊆ OPort">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_QFUfMAWQEei9ocE08JsPSw"/>
<details key="label" value="i2p_OPort"/>
</annotations>
</invariants>
<invariants name="p_index_ty" predicate="p_index ∈ dom(inst2pat_p) → ℕ">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_QFVGQAWQEei9ocE08JsPSw"/>
<details key="label" value="p_index_ty"/>
</annotations>
</invariants>
<variant expression="to_unfold_p_in">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_7pQu4Af5EeiFlqW-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="_btHw0PqwEeectLZKwQfI0A"/>
</annotations>
<refines href="../mProperty.bum#http://emf.eventb.org/models/core/machine/2014::Event::mProperty.instanciate_pattern"/>
<parameters name="inst_ports">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_btHw0fqwEeectLZKwQfI0A"/>
<details key="identifier" value="inst_ports"/>
</annotations>
</parameters>
<parameters name="p_mult_others">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_btHw0vqwEeectLZKwQfI0A"/>
<details key="identifier" value="p_mult_others"/>
</annotations>
</parameters>
<guards name="ip" predicate="inst_ports ∈ (components;ports)[{Pat}] ↔ (components;ports)[{Mdl}]">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_btHw0_qwEeectLZKwQfI0A"/>
<details key="label" value="ip"/>
</annotations>
</guards>
<guards name="ipr" predicate="inst_ports∼ ∈ (components;ports)[{Mdl}] ⇸ (components;ports)[{Pat}]">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_btHw1PqwEeectLZKwQfI0A"/>
<details key="label" value="ipr"/>
</annotations>
</guards>
<guards name="pm" predicate="p_mult_others ∈ (components;ports)[{Pat}] ∖ dom(inst_ports) → ℕ">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_btHw1fqwEeectLZKwQfI0A"/>
<details key="label" value="pm"/>
</annotations>
</guards>
<guards name="thm" predicate="∀p· finite(inst_ports[{p}])" theorem="true">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_btHw1vqwEeectLZKwQfI0A"/>
<details key="label" value="thm"/>
</annotations>
</guards>
<actions name="p_mult" action="p_multiplicity ≔ p_multiplicity (p_mult_others {pp·pp∈(components;ports)[{Pat}] ∣ pp ↦ card(inst_ports[{pp}])})">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_btIX4PqwEeectLZKwQfI0A"/>
<details key="label" value="p_mult"/>
</annotations>
</actions>
<actions name="inst2pat_p" action="inst2pat_p ≔ ∅">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_btJmA_qwEeectLZKwQfI0A"/>
<details key="label" value="inst2pat_p"/>
</annotations>
</actions>
<actions name="ports" action="ports ≔ (components[{Inst}]) ⩤ ports">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_btJmCfqwEeectLZKwQfI0A"/>
<details key="label" value="ports"/>
</annotations>
</actions>
<actions name="unfold_p" action="to_unfold_p_in ≔ ∅">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_btJmCvqwEeectLZKwQfI0A"/>
<details key="label" value="unfold_p"/>
</annotations>
</actions>
<actions name="p_index" action="p_index ≔ ∅">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_btKNEPqwEeectLZKwQfI0A"/>
<details key="label" value="p_index"/>
</annotations>
</actions>
</events>
<events name="unfold_root_c" extended="true">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_btIX4_qwEeectLZKwQfI0A"/>
<details key="label" value="unfold_root_c"/>
</annotations>
<annotations source="http:///org/eventb/core/RodinReferenceNamesAnnotations">
<details key="refines unfold_root_c" value="_jNxEQAKyEeiAPf1wPUl3Gw"/>
</annotations>
<refines href="../mProperty.bum#http://emf.eventb.org/models/core/machine/2014::Event::mProperty.unfold_root_c"/>
</events>
<events name="clone_c" extended="true">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_btJmBfqwEeectLZKwQfI0A"/>
<details key="label" value="clone_c"/>
</annotations>
<annotations source="http:///org/eventb/core/RodinReferenceNamesAnnotations">
<details key="refines clone_c" value="_SDieEP06Eees7pYemx4WBQ"/>
</annotations>
<refines href="../mProperty.bum#http://emf.eventb.org/models/core/machine/2014::Event::mProperty.clone_c"/>
<actions name="unfold_p_in" action="to_unfold_p_in ≔ to_unfold_p_in ∪ (ports[{to_clone_c(c)}] × {c})">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_btKNFfqwEeectLZKwQfI0A"/>
<details key="label" value="unfold_p_in"/>
</annotations>
</actions>
</events>
<events name="unfold_node_c" extended="true">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_btKNEfqwEeectLZKwQfI0A"/>
<details key="label" value="unfold_node_c"/>
</annotations>
<annotations source="http:///org/eventb/core/RodinReferenceNamesAnnotations">
<details key="refines unfold_node_c" value="_YT9zsAKzEeiAPf1wPUl3Gw"/>
</annotations>
<refines href="../mProperty.bum#http://emf.eventb.org/models/core/machine/2014::Event::mProperty.unfold_node_c"/>
</events>
<events name="unfold_p" convergence="convergent" extended="false">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_btKNGPqwEeectLZKwQfI0A"/>
<details key="label" value="unfold_p"/>
</annotations>
<parameters comment="port to unfold" name="p">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_btI-8fqwEeectLZKwQfI0A"/>
<details key="identifier" value="p"/>
<details key="comment" value="port to unfold"/>
</annotations>
</parameters>
<parameters comment="target component" name="c">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_btI-8vqwEeectLZKwQfI0A"/>
<details key="identifier" value="c"/>
<details key="comment" value="target component"/>
</annotations>
</parameters>
<parameters comment="replicated ports" name="new_p">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_btJmB_qwEeectLZKwQfI0A"/>
<details key="identifier" value="new_p"/>
<details key="comment" value="replicated ports"/>
</annotations>
</parameters>
<guards name="p_ty" predicate="p ↦ c ∈ to_unfold_p_in">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_btHw1_qwEeectLZKwQfI0A"/>
<details key="label" value="p_ty"/>
</annotations>
</guards>
<guards name="new_p_ty" predicate="new_p ∈ 1‥p_multiplicity(p) ↣ Port ∖ ran(components;ports)">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_btHw2PqwEeectLZKwQfI0A"/>
<details key="label" value="new_p_ty"/>
</annotations>
</guards>
<guards name="duplicate_IPorts_direction" predicate="p ∈ IPort ⇒ ran(new_p) ⊆ IPort">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_btHw2fqwEeectLZKwQfI0A"/>
<details key="label" value="duplicate_IPorts_direction"/>
</annotations>
</guards>
<guards name="duplicate_OPorts_direction" predicate="p ∈ OPort ⇒ ran(new_p) ⊆ OPort">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_btI-8_qwEeectLZKwQfI0A"/>
<details key="label" value="duplicate_OPorts_direction"/>
</annotations>
</guards>
<actions name="new_p_component" action="ports ≔ ports ∪ ({c} × ran(new_p))">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_GO3gcAK8EeiAPf1wPUl3Gw"/>
<details key="label" value="new_p_component"/>
</annotations>
</actions>
<actions name="dp" action="to_unfold_p_in ≔ to_unfold_p_in ∖ {p↦c}">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_YHf5cAUuEei9ocE08JsPSw"/>
<details key="label" value="dp"/>
</annotations>
</actions>
<actions name="inst2pat_p" action="inst2pat_p ≔ inst2pat_p ∪ (ran(new_p) × {p})">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_YHiVsAUuEei9ocE08JsPSw"/>
<details key="label" value="inst2pat_p"/>
</annotations>
</actions>
<actions name="p_index" action="p_index ≔ p_index ∪ new_p∼">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_YHiVsQUuEei9ocE08JsPSw"/>
<details key="label" value="p_index"/>
</annotations>
</actions>
</events>
<events name="apply_pattern" extended="true">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_YUG9oAKzEeiAPf1wPUl3Gw"/>
<details key="label" value="apply_pattern"/>
</annotations>
<annotations source="http:///org/eventb/core/RodinReferenceNamesAnnotations">
<details key="refines apply_pattern" value="_YUG9oQKzEeiAPf1wPUl3Gw"/>
</annotations>
<refines href="../mProperty.bum#http://emf.eventb.org/models/core/machine/2014::Event::mProperty.apply_pattern"/>
<parameters name="inst_ports">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_btKNE_qwEeectLZKwQfI0A"/>
<details key="identifier" value="inst_ports"/>
</annotations>
</parameters>
<parameters name="new_ports">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_LNbVcAWLEei9ocE08JsPSw"/>
<details key="identifier" value="new_ports"/>
</annotations>
</parameters>
<guards name="ip" predicate="inst_ports ∈ (components;ports)[{Inst}] ⤔ (components;ports)[{Mdl}]">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_btI-9PqwEeectLZKwQfI0A"/>
<details key="label" value="ip"/>
</annotations>
</guards>
<guards name="mp_i" predicate="inst_ports[IPort] ⊆ IPort">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_btI-9fqwEeectLZKwQfI0A"/>
<details key="label" value="mp_i"/>
</annotations>
</guards>
<guards name="mp_o" predicate="inst_ports[OPort] ⊆ OPort">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_btI-9vqwEeectLZKwQfI0A"/>
<details key="label" value="mp_o"/>
</annotations>
</guards>
<guards comment="Les ports instanciés sont des ports de composants instanciés" name="ports_inst_rel_comp_inst" predicate="ports∼[dom(inst_ports)] ⊆ dom(inst_components)">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_btI-9_qwEeectLZKwQfI0A"/>
<details key="label" value="ports_inst_rel_comp_inst"/>
<details key="comment" value="Les ports instanciés sont des ports de composants instanciés"/>
</annotations>
</guards>
<guards name="ports_inst_rel_port_comp" predicate="inst_ports∼;ports∼;inst_components ⊆ ports∼">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_btI--PqwEeectLZKwQfI0A"/>
<details key="label" value="ports_inst_rel_port_comp"/>
</annotations>
</guards>
<guards name="np" predicate="new_ports ∈ (components;ports)[{Inst}] ∖ dom(inst_ports) ↣ Port ∖ ran(components;ports)">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_btI--fqwEeectLZKwQfI0A"/>
<details key="label" value="np"/>
</annotations>
</guards>
<guards name="np_i" predicate="new_ports[IPort] ⊆ IPort">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_knJVMAK2EeiAPf1wPUl3Gw"/>
<details key="label" value="np_i"/>
</annotations>
</guards>
<guards name="np_o" predicate="new_ports[OPort] ⊆ OPort">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_OuP8ACxHEeiUbZrF94gIyA"/>
<details key="label" value="np_o"/>
</annotations>
</guards>
<actions name="c" action="ports ≔ ports ∪ ((inst_components ∪ new_components)∼;ports;(inst_ports ∪ new_ports))">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_f2PGEAspEeigQsLVMUeRQw"/>
<details key="label" value="c"/>
</annotations>
</actions>
</events>
</machine:Machine>