|
|
<?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 variables components container c_multiplicity to_clone_c c_index to_unfold_c to_unfold_c_in inst2pat_c invariants @comp components ∈ Model ↔ Component @comp_finite ∀m·finite(components[{m}]) @comp_not_shared components∼ ∈ Component ⇸ Model @c_mult c_multiplicity ∈ components[Pattern] → ℕ @cont_ty container ∈ ran(components) ⇸ ran(components) @cont_ctr components;container;components∼ ⊆ id @acycl ∃f· f ∈ Component ↔ Component ∧ container ⊆ f ∧ f;f ⊆ f ∧ id ∩ f = ∅ theorem @irrefl container ∩ id = ∅ @to_unfold_c_in to_unfold_c_in ∈ components[{Pat}] ↔ components[{Inst}] @to_clone_c to_clone_c ∈ components[{Inst}] ⇸ components[{Pat}] // From new component to original component @to_unfold_c to_unfold_c ⊆ components[{Pat}] @inst2pat_c_ty inst2pat_c ∈ components[{Inst}] → components[{Pat}] @inst2pat_clone to_clone_c ⊆ inst2pat_c @inst2pat_unfold_in to_unfold_c_in;inst2pat_c ⊆ container @pat2inst_unfold to_unfold_c ∩ ran(inst2pat_c) = ∅ @unfold_root to_unfold_c ∩ dom(container) = ∅ @unfold_in dom(to_unfold_c_in) ⊆ dom(container) theorem @unfold_unfold_in to_unfold_c ∩ dom(to_unfold_c_in) = ∅ theorem @unfold_clone to_unfold_c ∩ ran(to_clone_c) = ∅ @inst2pat_cont inst2pat_c;container = container;inst2pat_c @c_index_ty c_index ∈ dom(inst2pat_c) → ℕ @to_clone_c_mult ∀c· c∈dom(inst2pat_c) ⇒ c_index(c) ∈ 1‥c_multiplicity(inst2pat_c(c)) variant ⋃ c · c∈(to_unfold_c ∪ ran(to_clone_c)) ∣ {c} × inter({ sc ∣ c∈sc ∧ container∼[sc] ⊆ sc}) events event instanciate_pattern any inst_components c_mult_others where @ic inst_components ∈ components[{Pat}] ↔ components[{Mdl}] @icr inst_components∼ ∈ components[{Mdl}] ⇸ components[{Pat}] @cm c_mult_others ∈ components[{Pat}] ∖ dom(inst_components) → ℕ then @c_mult c_multiplicity ≔ c_multiplicity (c_mult_others {pc· pc ∈ dom(inst_components) ∣ pc ↦ card(inst_components[{pc}])}) @to_unfold_c to_unfold_c ≔ (components[{Pat}] ∖ dom(container)) @to_unfold_c_in to_unfold_c_in ≔ ∅ @components_inst components ≔ {Inst} ⩤ components @container_inst container ≔ components[{Inst}] ⩤ container @to_clone_c to_clone_c ≔ ∅ @c_index c_index ≔ ∅ @pat2inst_c inst2pat_c ≔ ∅ end convergent event unfold_root_c any c new_c where @c_ty c ∈ to_unfold_c @new_c_ty new_c ∈ 1‥c_multiplicity(c) ↣ Component ∖ ran(components) then @new_c_model components ≔ components ∪ ({Inst}×ran(new_c)) @to_clone_c to_clone_c ≔ to_clone_c ∪ (ran(new_c)×{c}) @c_index c_index ≔ c_index ∪ new_c∼ @to_unfold_c to_unfold_c ≔ to_unfold_c ∖ {c} @pat2inst_c inst2pat_c ≔ inst2pat_c ∪ (ran(new_c) × {c}) end convergent event clone_c // Variante: spécifier directement la fermeture transitive. any c where @c_ty c ∈ dom(to_clone_c) then @to_unfold_c_in to_unfold_c_in ≔ to_unfold_c_in ∪ (container∼[{to_clone_c(c)}] × {c}) @cloned_c to_clone_c ≔ {c} ⩤ to_clone_c end convergent event unfold_node_c // réplication des éléments composants // A voir: duplication du contenu de C any c dest new_c where @c_ty c ↦ dest ∈ to_unfold_c_in @new_c_ty new_c ∈ 1‥c_multiplicity(c) ↣ Component ∖ ran(components) then @new_c_model components ≔ components ∪ ({Inst}×ran(new_c)) @new_c_container container ≔ container ∪ (ran(new_c)×{dest}) @to_clone_c to_clone_c ≔ to_clone_c ∪ (ran(new_c)×{c}) @c_index c_index ≔ c_index ∪ new_c∼ @to_unfold_c_in to_unfold_c_in ≔ to_unfold_c_in ∖ {c ↦ dest} @pat2inst_c inst2pat_c ≔ inst2pat_c ∪ (ran(new_c) × {c}) end event apply_pattern // transformation du modèle any inst_components // instance mapping new_components where @ic inst_components ∈ components[{Inst}] ⤔ components[{Mdl}] @nc new_components ∈ components[{Inst}] ∖ dom(inst_components) ↣ Component ∖ ran(components) @acycl_inst_components dom(inst_components) ◁ container;inst_components ⊆ inst_components;container @acycl_container container[dom(inst_components)] ⊆ dom(inst_components) then @m components ≔ components ∪ ({Mdl}×ran(new_components)) @f container ≔ container ∪ ((inst_components ∪ new_components)∼;container;(inst_components ∪ new_components)) end end " 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>
|
|
|
|
