Pattern-Instanciation-On-System-Engineering-Model/Event-B/pseim/mComponent.bum

<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.machineFile org.eventb.core.configuration="org.eventb.core.fwd;de.prob.units.mchBase;org.eventb.codegen.ui.cgConfig" org.eventb.texttools.text_lastmodified="1522155117059" org.eventb.texttools.text_representation="machine mComponent sees cComponent&#10;&#10;variables components container c_multiplicity to_clone_c c_index to_unfold_c to_unfold_c_in inst2pat_c&#10;&#10;invariants&#10;  @comp components ∈ Model ↔ Component&#10;  @comp_finite ∀m·finite(components[{m}])&#10;  @comp_not_shared components∼ ∈ Component ⇸ Model&#10;  @c_mult c_multiplicity ∈ components[Pattern] → ℕ&#10;  @cont_ty container ∈ ran(components) ⇸ ran(components)&#10;  @cont_ctr components;container;components∼ ⊆ id&#10;  @acycl ∃f· f ∈ Component ↔ Component ∧ container ⊆ f ∧ f;f ⊆ f ∧ id ∩ f = ∅&#10;  theorem @irrefl container ∩ id = ∅&#10;  @to_unfold_c_in to_unfold_c_in ∈ components[{Pat}] ↔ components[{Inst}]&#10;  @to_clone_c to_clone_c ∈ components[{Inst}] ⇸ components[{Pat}] // From new component to original component&#10;  @to_unfold_c to_unfold_c ⊆ components[{Pat}]&#10;  @inst2pat_c_ty inst2pat_c ∈ components[{Inst}] → components[{Pat}]&#10;  @inst2pat_clone to_clone_c ⊆ inst2pat_c&#10;  @inst2pat_unfold_in to_unfold_c_in;inst2pat_c ⊆ container&#10;  @pat2inst_unfold to_unfold_c ∩ ran(inst2pat_c) = ∅&#10;  @unfold_root to_unfold_c ∩ dom(container) = ∅&#10;  @unfold_in dom(to_unfold_c_in) ⊆ dom(container)&#10;  theorem @unfold_unfold_in to_unfold_c ∩ dom(to_unfold_c_in) = ∅&#10;  theorem @unfold_clone to_unfold_c ∩ ran(to_clone_c) = ∅&#10;  @inst2pat_cont inst2pat_c;container = container;inst2pat_c&#10;  @c_index_ty c_index ∈ dom(inst2pat_c) → ℕ&#10;  @to_clone_c_mult ∀c· c∈dom(inst2pat_c) ⇒ c_index(c) ∈ 1‥c_multiplicity(inst2pat_c(c))&#10;&#10;variant ⋃ c · c∈(to_unfold_c ∪ ran(to_clone_c)) ∣ {c} × inter({ sc ∣ c∈sc ∧ container∼[sc] ⊆ sc})&#10;&#10;events&#10;  event instanciate_pattern&#10;    any inst_components c_mult_others&#10;    where&#10;      @ic inst_components ∈ components[{Pat}] ↔ components[{Mdl}]&#10;      @icr inst_components∼ ∈ components[{Mdl}] ⇸ components[{Pat}]&#10;      @cm c_mult_others ∈ components[{Pat}] ∖ dom(inst_components) → ℕ&#10;    then&#10;      @c_mult c_multiplicity ≔ c_multiplicity  (c_mult_others  {pc· pc ∈ dom(inst_components) ∣ pc ↦ card(inst_components[{pc}])})&#10;      @to_unfold_c to_unfold_c ≔ (components[{Pat}] ∖ dom(container))&#10;      @to_unfold_c_in to_unfold_c_in ≔ ∅&#10;      @components_inst components ≔ {Inst} ⩤ components&#10;      @container_inst container ≔ components[{Inst}] ⩤ container&#10;      @to_clone_c to_clone_c ≔ ∅&#10;      @c_index c_index ≔ ∅&#10;      @pat2inst_c inst2pat_c ≔ ∅&#10;  end&#10;&#10;  convergent event unfold_root_c&#10;    any c new_c&#10;    where&#10;      @c_ty c ∈ to_unfold_c&#10;      @new_c_ty new_c ∈ 1‥c_multiplicity(c) ↣ Component ∖ ran(components)&#10;    then&#10;      @new_c_model components ≔ components ∪ ({Inst}×ran(new_c))&#10;      @to_clone_c to_clone_c ≔ to_clone_c ∪ (ran(new_c)×{c})&#10;      @c_index c_index ≔ c_index ∪ new_c∼&#10;      @to_unfold_c to_unfold_c ≔ to_unfold_c ∖ {c}&#10;      @pat2inst_c inst2pat_c ≔ inst2pat_c ∪ (ran(new_c) × {c})&#10;  end&#10;&#10;  convergent event clone_c // Variante: spécifier directement la fermeture transitive.&#10;    any c&#10;    where&#10;      @c_ty c ∈ dom(to_clone_c)&#10;    then&#10;      @to_unfold_c_in to_unfold_c_in ≔ to_unfold_c_in ∪ (container∼[{to_clone_c(c)}] × {c})&#10;      @cloned_c to_clone_c ≔ {c} ⩤ to_clone_c&#10;  end&#10;&#10;  convergent event unfold_node_c // réplication des éléments composants // A voir: duplication du contenu de C&#10;    any c dest new_c&#10;    where&#10;      @c_ty c ↦ dest ∈ to_unfold_c_in&#10;      @new_c_ty new_c ∈ 1‥c_multiplicity(c) ↣ Component ∖ ran(components)&#10;    then&#10;      @new_c_model components ≔ components ∪ ({Inst}×ran(new_c))&#10;      @new_c_container container ≔ container ∪ (ran(new_c)×{dest})&#10;      @to_clone_c to_clone_c ≔ to_clone_c ∪ (ran(new_c)×{c})&#10;      @c_index c_index ≔ c_index ∪ new_c∼&#10;      @to_unfold_c_in to_unfold_c_in ≔ to_unfold_c_in ∖ {c ↦ dest}&#10;      @pat2inst_c inst2pat_c ≔ inst2pat_c ∪ (ran(new_c) × {c})&#10;  end&#10;&#10;  event apply_pattern // transformation du modèle&#10;    any inst_components // instance mapping&#10;        new_components&#10;    where&#10;      @ic inst_components ∈ components[{Inst}] ⤔ components[{Mdl}]&#10;      @nc new_components ∈ components[{Inst}] ∖ dom(inst_components) ↣ Component ∖ ran(components)&#10;      @acycl_inst_components dom(inst_components) ◁ container;inst_components ⊆ inst_components;container&#10;      @acycl_container container[dom(inst_components)] ⊆ dom(inst_components)&#10;    then&#10;      @m components ≔ components ∪ ({Mdl}×ran(new_components))&#10;      @f container ≔ container ∪ ((inst_components ∪ new_components)∼;container;(inst_components ∪ new_components))&#10;  end&#10;end&#10;" version="5">
<org.eventb.core.seesContext name="_cQf0YPqUEeectLZKwQfI0A" org.eventb.core.target="cComponent"/>
<org.eventb.core.event name="'" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="instanciate_pattern">
<org.eventb.core.parameter name="_O1UjgPqmEeectLZKwQfI0A" org.eventb.core.identifier="inst_components"/>
<org.eventb.core.guard name="_O1UjgvqmEeectLZKwQfI0A" org.eventb.core.label="ic" org.eventb.core.predicate="inst_components ∈ components[{Pat}] ↔ components[{Mdl}]"/>
<org.eventb.core.guard name="_O1Ujg_qmEeectLZKwQfI0A" org.eventb.core.label="icr" org.eventb.core.predicate="inst_components∼ ∈ components[{Mdl}] ⇸ components[{Pat}]"/>
<org.eventb.core.guard name="_O1UjhPqmEeectLZKwQfI0A" org.eventb.core.label="cm" org.eventb.core.predicate="c_mult_others ∈ components[{Pat}] ∖ dom(inst_components) → ℕ"/>
<org.eventb.core.action name="_O1UjhfqmEeectLZKwQfI0A" org.eventb.core.assignment="c_multiplicity ≔ c_multiplicity  (c_mult_others  {pc· pc ∈ dom(inst_components) ∣ pc ↦ card(inst_components[{pc}])})" org.eventb.core.label="c_mult"/>
<org.eventb.core.parameter name="_O1UjgfqmEeectLZKwQfI0A" org.eventb.core.identifier="c_mult_others"/>
<org.eventb.core.action name="_O1WYt_qmEeectLZKwQfI0A" org.eventb.core.assignment="to_unfold_c ≔ (components[{Pat}] ∖ dom(container))" org.eventb.core.label="to_unfold_c"/>
<org.eventb.core.action name="_O1WYuPqmEeectLZKwQfI0A" org.eventb.core.assignment="to_unfold_c_in ≔ ∅" org.eventb.core.label="to_unfold_c_in"/>
<org.eventb.core.action name="_O1W_xPqmEeectLZKwQfI0A" org.eventb.core.assignment="components ≔ {Inst} ⩤ components" org.eventb.core.label="components_inst"/>
<org.eventb.core.action name="_O1W_xfqmEeectLZKwQfI0A" org.eventb.core.assignment="container ≔ components[{Inst}] ⩤ container" org.eventb.core.label="container_inst"/>
<org.eventb.core.action name="_O1W_xvqmEeectLZKwQfI0A" org.eventb.core.assignment="to_clone_c ≔ ∅" org.eventb.core.label="to_clone_c"/>
<org.eventb.core.action name="_O1W_x_qmEeectLZKwQfI0A" org.eventb.core.assignment="c_index ≔ ∅" org.eventb.core.label="c_index"/>
<org.eventb.core.action name="_O1W_yPqmEeectLZKwQfI0A" org.eventb.core.assignment="inst2pat_c ≔ ∅" org.eventb.core.label="pat2inst_c"/>
</org.eventb.core.event>
<org.eventb.core.variable name="_cQf0YfqUEeectLZKwQfI0A" org.eventb.core.identifier="components"/>
<org.eventb.core.variable name="_cQf0YvqUEeectLZKwQfI0A" org.eventb.core.identifier="container"/>
<org.eventb.core.invariant name="_cQf0Y_qUEeectLZKwQfI0A" org.eventb.core.label="comp" org.eventb.core.predicate="components ∈ Model ↔ Component"/>
<org.eventb.core.invariant name="_cQf0ZPqUEeectLZKwQfI0A" org.eventb.core.label="comp_finite" org.eventb.core.predicate="∀m·finite(components[{m}])"/>
<org.eventb.core.invariant name="_ip9Q0PqUEeectLZKwQfI0A" org.eventb.core.label="comp_not_shared" org.eventb.core.predicate="components∼ ∈ Component ⇸ Model"/>
<org.eventb.core.invariant name="_GMp30PqWEeectLZKwQfI0A" org.eventb.core.label="c_mult" org.eventb.core.predicate="c_multiplicity ∈ components[Pattern] → ℕ"/>
<org.eventb.core.variable name="_gmDo8PqgEeectLZKwQfI0A" org.eventb.core.identifier="c_multiplicity"/>
<org.eventb.core.invariant name="_gmDo8fqgEeectLZKwQfI0A" org.eventb.core.label="cont_ty" org.eventb.core.predicate="container ∈ ran(components) ⇸ ran(components)"/>
<org.eventb.core.invariant name="_gmDo8vqgEeectLZKwQfI0A" org.eventb.core.label="cont_ctr" org.eventb.core.predicate="components;container;components∼ ⊆ id"/>
<org.eventb.core.invariant name="_oXBHAPqkEeectLZKwQfI0A" org.eventb.core.label="acycl" org.eventb.core.predicate="∃f· f ∈ Component ↔ Component ∧ container ⊆ f ∧ f;f ⊆ f ∧ id ∩ f = ∅"/>
<org.eventb.core.variable name="_1dqNIPqkEeectLZKwQfI0A" org.eventb.core.identifier="to_clone_c"/>
<org.eventb.core.variable name="_1dqNIfqkEeectLZKwQfI0A" org.eventb.core.identifier="c_index"/>
<org.eventb.core.variable name="_1dqNIvqkEeectLZKwQfI0A" org.eventb.core.identifier="to_unfold_c"/>
<org.eventb.core.invariant name="_1dqNI_qkEeectLZKwQfI0A" org.eventb.core.label="irrefl" org.eventb.core.predicate="container ∩ id = ∅" org.eventb.core.theorem="true"/>
<org.eventb.core.invariant name="_1dqNJPqkEeectLZKwQfI0A" org.eventb.core.label="to_unfold_c_in" org.eventb.core.predicate="to_unfold_c_in ∈ components[{Pat}] ↔ components[{Inst}]"/>
<org.eventb.core.invariant name="_1dq0MPqkEeectLZKwQfI0A" org.eventb.core.comment="From new component to original component" org.eventb.core.label="to_clone_c" org.eventb.core.predicate="to_clone_c ∈ components[{Inst}] ⇸ components[{Pat}]"/>
<org.eventb.core.event name="_O1VxoPqmEeectLZKwQfI0A" org.eventb.core.convergence="1" org.eventb.core.extended="false" org.eventb.core.label="unfold_root_c">
<org.eventb.core.guard name="_O1WYsfqmEeectLZKwQfI0A" org.eventb.core.label="c_ty" org.eventb.core.predicate="c ∈ to_unfold_c"/>
<org.eventb.core.guard name="_O1WYsvqmEeectLZKwQfI0A" org.eventb.core.label="new_c_ty" org.eventb.core.predicate="new_c ∈ 1‥c_multiplicity(c) ↣ Component ∖ ran(components)"/>
<org.eventb.core.parameter name="_O1VxofqmEeectLZKwQfI0A" org.eventb.core.identifier="c"/>
<org.eventb.core.parameter name="_O1WYsPqmEeectLZKwQfI0A" org.eventb.core.identifier="new_c"/>
<org.eventb.core.action name="_O1Xm1PqmEeectLZKwQfI0A" org.eventb.core.assignment="components ≔ components ∪ ({Inst}×ran(new_c))" org.eventb.core.label="new_c_model"/>
<org.eventb.core.action name="_O1Xm1fqmEeectLZKwQfI0A" org.eventb.core.assignment="to_clone_c ≔ to_clone_c ∪ (ran(new_c)×{c})" org.eventb.core.label="to_clone_c"/>
<org.eventb.core.action name="_O1Xm1vqmEeectLZKwQfI0A" org.eventb.core.assignment="c_index ≔ c_index ∪ new_c∼" org.eventb.core.label="c_index"/>
<org.eventb.core.action name="_O1Xm1_qmEeectLZKwQfI0A" org.eventb.core.assignment="to_unfold_c ≔ to_unfold_c ∖ {c}" org.eventb.core.label="to_unfold_c"/>
<org.eventb.core.action name="_O1YN4PqmEeectLZKwQfI0A" org.eventb.core.assignment="inst2pat_c ≔ inst2pat_c ∪ (ran(new_c) × {c})" org.eventb.core.label="pat2inst_c"/>
</org.eventb.core.event>
<org.eventb.core.event name="_O1WYufqmEeectLZKwQfI0A" org.eventb.core.comment="Variante: spécifier directement la fermeture transitive." org.eventb.core.convergence="1" org.eventb.core.extended="false" org.eventb.core.label="clone_c">
<org.eventb.core.action name="_O1YN4fqmEeectLZKwQfI0A" org.eventb.core.assignment="to_unfold_c_in ≔ to_unfold_c_in ∪ (container∼[{to_clone_c(c)}] × {c})" org.eventb.core.label="to_unfold_c_in"/>
<org.eventb.core.action name="_O1YN4vqmEeectLZKwQfI0A" org.eventb.core.assignment="to_clone_c ≔ {c} ⩤ to_clone_c" org.eventb.core.label="cloned_c"/>
<org.eventb.core.parameter name="_O1W_wPqmEeectLZKwQfI0A" org.eventb.core.identifier="c"/>
<org.eventb.core.guard name="_O1WYs_qmEeectLZKwQfI0A" org.eventb.core.label="c_ty" org.eventb.core.predicate="c ∈ dom(to_clone_c)"/>
</org.eventb.core.event>
<org.eventb.core.event name="_O1W_yfqmEeectLZKwQfI0A" org.eventb.core.comment="réplication des éléments composants // A voir: duplication du contenu de C" org.eventb.core.convergence="1" org.eventb.core.extended="false" org.eventb.core.label="unfold_node_c">
<org.eventb.core.parameter name="_O1W_wfqmEeectLZKwQfI0A" org.eventb.core.identifier="c"/>
<org.eventb.core.parameter name="_O1Xm0PqmEeectLZKwQfI0A" org.eventb.core.identifier="dest"/>
<org.eventb.core.action name="_lyJKIPreEeerIsS6OyYQ4w" org.eventb.core.assignment="components ≔ components ∪ ({Inst}×ran(new_c))" org.eventb.core.label="new_c_model"/>
<org.eventb.core.action name="_rQ0PgftxEeectLZKwQfI0A" org.eventb.core.assignment="container ≔ container ∪ (ran(new_c)×{dest})" org.eventb.core.label="new_c_container"/>
<org.eventb.core.action name="_xQWRoP01EeeINffjS36taQ" org.eventb.core.assignment="to_clone_c ≔ to_clone_c ∪ (ran(new_c)×{c})" org.eventb.core.label="to_clone_c"/>
<org.eventb.core.action name="_254qkAA2EeictLZKwQfI0A" org.eventb.core.assignment="c_index ≔ c_index ∪ new_c∼" org.eventb.core.label="c_index"/>
<org.eventb.core.action name="_254qkQA2EeictLZKwQfI0A" org.eventb.core.assignment="to_unfold_c_in ≔ to_unfold_c_in ∖ {c ↦ dest}" org.eventb.core.label="to_unfold_c_in"/>
<org.eventb.core.action name="_i0ODcAIQEei9ocE08JsPSw" org.eventb.core.assignment="inst2pat_c ≔ inst2pat_c ∪ (ran(new_c) × {c})" org.eventb.core.label="pat2inst_c"/>
<org.eventb.core.guard name="_O1WYtPqmEeectLZKwQfI0A" org.eventb.core.label="c_ty" org.eventb.core.predicate="c ↦ dest ∈ to_unfold_c_in"/>
<org.eventb.core.guard name="_O1WYtfqmEeectLZKwQfI0A" org.eventb.core.label="new_c_ty" org.eventb.core.predicate="new_c ∈ 1‥c_multiplicity(c) ↣ Component ∖ ran(components)"/>
<org.eventb.core.parameter name="_O1Xm0fqmEeectLZKwQfI0A" org.eventb.core.identifier="new_c"/>
</org.eventb.core.event>
<org.eventb.core.event name="_O1Xm2PqmEeectLZKwQfI0A" org.eventb.core.comment="transformation du modèle" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="apply_pattern">
<org.eventb.core.guard name="_O1WYtvqmEeectLZKwQfI0A" org.eventb.core.label="ic" org.eventb.core.predicate="inst_components ∈ components[{Inst}] ⤔ components[{Mdl}]"/>
<org.eventb.core.guard name="_O1W_wvqmEeectLZKwQfI0A" org.eventb.core.label="nc" org.eventb.core.predicate="new_components ∈ components[{Inst}] ∖ dom(inst_components) ↣ Component ∖ ran(components)"/>
<org.eventb.core.guard name="_O1W_w_qmEeectLZKwQfI0A" org.eventb.core.label="acycl_inst_components" org.eventb.core.predicate="dom(inst_components) ◁ container;inst_components ⊆ inst_components;container"/>
<org.eventb.core.guard name="_O1Xm0vqmEeectLZKwQfI0A" org.eventb.core.label="acycl_container" org.eventb.core.predicate="container[dom(inst_components)] ⊆ dom(inst_components)"/>
<org.eventb.core.parameter name="_rQ0PgPtxEeectLZKwQfI0A" org.eventb.core.comment="instance mapping" org.eventb.core.identifier="inst_components"/>
<org.eventb.core.parameter name="_h4VmkAKrEeiAPf1wPUl3Gw" org.eventb.core.identifier="new_components"/>
<org.eventb.core.action name="_reToAAK7EeiAPf1wPUl3Gw" org.eventb.core.assignment="components ≔ components ∪ ({Mdl}×ran(new_components))" org.eventb.core.label="m"/>
<org.eventb.core.action name="_szQBsAK7EeiAPf1wPUl3Gw" org.eventb.core.assignment="container ≔ container ∪ ((inst_components ∪ new_components)∼;container;(inst_components ∪ new_components))" org.eventb.core.label="f"/>
</org.eventb.core.event>
<org.eventb.core.invariant name="_l7KVEQA1EeictLZKwQfI0A" org.eventb.core.label="to_unfold_c" org.eventb.core.predicate="to_unfold_c ⊆ components[{Pat}]"/>
<org.eventb.core.invariant name="_l7KVEgA1EeictLZKwQfI0A" org.eventb.core.label="inst2pat_c_ty" org.eventb.core.predicate="inst2pat_c ∈ components[{Inst}] → components[{Pat}]"/>
<org.eventb.core.variable name="_9phD8AKqEeiAPf1wPUl3Gw" org.eventb.core.identifier="to_unfold_c_in"/>
<org.eventb.core.invariant name="_Hwdz4AKtEeiAPf1wPUl3Gw" org.eventb.core.label="inst2pat_clone" org.eventb.core.predicate="to_clone_c ⊆ inst2pat_c"/>
<org.eventb.core.variable name="_xudpYAK5EeiAPf1wPUl3Gw" org.eventb.core.identifier="inst2pat_c"/>
<org.eventb.core.invariant name="_xudpYQK5EeiAPf1wPUl3Gw" org.eventb.core.label="inst2pat_unfold_in" org.eventb.core.predicate="to_unfold_c_in;inst2pat_c ⊆ container"/>
<org.eventb.core.variant name="_yRrOsAK6EeiAPf1wPUl3Gw" org.eventb.core.expression="⋃ c · c∈(to_unfold_c ∪ ran(to_clone_c)) ∣ {c} × inter({ sc ∣ c∈sc ∧ container∼[sc] ⊆ sc})"/>
<org.eventb.core.invariant name="_fxu54ALAEeiAPf1wPUl3Gw" org.eventb.core.label="pat2inst_unfold" org.eventb.core.predicate="to_unfold_c ∩ ran(inst2pat_c) = ∅"/>
<org.eventb.core.invariant name="_PaxdoAMwEei9ocE08JsPSw" org.eventb.core.label="unfold_root" org.eventb.core.predicate="to_unfold_c ∩ dom(container) = ∅"/>
<org.eventb.core.invariant name="_PaxdoQMwEei9ocE08JsPSw" org.eventb.core.label="unfold_in" org.eventb.core.predicate="dom(to_unfold_c_in) ⊆ dom(container)"/>
<org.eventb.core.invariant name="_nieoAAMxEei9ocE08JsPSw" org.eventb.core.label="unfold_unfold_in" org.eventb.core.predicate="to_unfold_c ∩ dom(to_unfold_c_in) = ∅" org.eventb.core.theorem="true"/>
<org.eventb.core.invariant name="_gxZD0AMzEei9ocE08JsPSw" org.eventb.core.label="unfold_clone" org.eventb.core.predicate="to_unfold_c ∩ ran(to_clone_c) = ∅" org.eventb.core.theorem="true"/>
<org.eventb.core.invariant name="_gxZD0QMzEei9ocE08JsPSw" org.eventb.core.label="inst2pat_cont" org.eventb.core.predicate="inst2pat_c;container = container;inst2pat_c"/>
<org.eventb.core.invariant name="_gxZD0gMzEei9ocE08JsPSw" org.eventb.core.label="c_index_ty" org.eventb.core.predicate="c_index ∈ dom(inst2pat_c) → ℕ"/>
<org.eventb.core.invariant name="_V6rHAAM1Eei9ocE08JsPSw" org.eventb.core.label="to_clone_c_mult" org.eventb.core.predicate="∀c· c∈dom(inst2pat_c) ⇒ c_index(c) ∈ 1‥c_multiplicity(inst2pat_c(c))"/>
</org.eventb.core.machineFile>