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.
12 Commits
1 Branch
0 Tags
3.4 MiB
Branch: master
Branches Tags
${ item.name }
Create tag ${ searchTerm }
Create branch ${ searchTerm }
from 'master'
${ noResults }
Pattern-Instanciation-On-Sy.../Event-B/pseim/mPort.bum

104 lines
18 KiB
Raw Permalink Normal View History Unescape

Update Event-B models and proofs
5 years ago
<?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.texttools.text_lastmodified="1575026476482" org.eventb.texttools.text_representation="machine mPort refines mProperty sees cPort&#10;&#10;variables components container containers c_multiplicity c_index to_unfold_c to_unfold_c_in inst2pat_c cProperties M P c_indexes ports p_multiplicity p_index to_unfold_p_in inst2pat_p&#10;&#10;invariants&#10; @port ports ∈ ran(components) ↔ Port&#10; @port_finite ∀c·finite(ports[{c}])&#10; @port_not_shared ports∼ ∈ Port ⇸ Component&#10; @p_mult p_multiplicity ∈ (components;ports)[Pattern] → ℕ&#10; @to_unfold_p_in to_unfold_p_in ∈ (components;ports)[{Pat}] ↔ components[{Inst}]&#10; @inst2pat_p_ty inst2pat_p ∈ (components;ports)[{Inst}] → (components;ports)[{Pat}]&#10; @inst2pat_commp inst2pat_p;ports∼ = ports∼;inst2pat_c&#10; @to_unfold_p_inst2pat ran(to_unfold_p_in) ⊆ dom(inst2pat_c)&#10; @to_unfold_p_in_comp to_unfold_p_in;inst2pat_c ⊆ ports∼&#10; @i2p_IPort inst2pat_p[IPort] ⊆ IPort&#10; @i2p_OPort inst2pat_p[OPort] ⊆ OPort&#10; @p_index_ty p_index ∈ dom(inst2pat_p) → ℕ&#10;&#10;variant to_unfold_p_in&#10;&#10;events&#10; event instanciate_pattern extends instanciate_pattern&#10; any inst_ports p_mult_others&#10; where&#10; @ip inst_ports ∈ (components;ports)[{Pat}] ↔ (components;ports)[{Mdl}]&#10; @ipr inst_ports∼ ∈ (components;ports)[{Mdl}] ⇸ (components;ports)[{Pat}]&#10; @pm p_mult_others ∈ (components;ports)[{Pat}] ∖ dom(inst_ports) → ℕ&#10; theorem @thm ∀p· finite(inst_ports[{p}])&#10; then&#10; @p_mult p_multiplicity ≔ p_multiplicity (p_mult_others {pp·pp∈(components;ports)[{Pat}] ∣ pp ↦ card(inst_ports[{pp}])})&#10; @inst2pat_p inst2pat_p ≔ ∅&#10; @ports ports ≔ (components[{Inst}]) ⩤ ports&#10; @unfold_p to_unfold_p_in ≔ ∅&#10; @p_index p_index ≔ ∅&#10; end&#10;&#10; event unfold_root_c extends unfold_root_c&#10; then&#10;&#9;@unfold_p_in to_unfold_p_in ≔ to_unfold_p_in ∪ (ports[{c}] × ran(new_c))&#10; end&#10;&#10; event unfold_node_c extends unfold_node_c&#10; then&#10;&#9;@unfold_p_in to_unfold_p_in ≔ to_unfold_p_in ∪ (ports[{c}] × ran(new_c))&#10; end&#10;&#10; convergent event unfold_p&#10; any p // port to unfold&#10; c // target component&#10; new_p // replicated ports&#10;&#10; where&#10; @p_ty p ↦ c ∈ to_unfold_p_in&#10; @new_p_ty new_p ∈ 1‥p_multiplicity(p) ↣ Port ∖ ran(components;ports)&#10; @duplicate_IPorts_direction p ∈ IPort ⇒ ran(new_p) ⊆ IPort&#10; @duplicate_OPorts_direction p ∈ OPort ⇒ ran(new_p) ⊆ OPort&#10; then&#10; @new_p_component ports ≔ ports ∪ ({c} × ran(new_p))&#10; @dp to_unfold_p_in ≔ to_unfold_p_in ∖ {p↦c}&#10; @inst2pat_p inst2pat_p ≔ inst2pat_p ∪ (ran(new_p) × {p})&#10; @p_index p_index ≔ p_index ∪ new_p∼&#10; end&#10;&#10; event apply_pattern extends apply_pattern&#10; any inst_ports new_ports&#10; where&#10; @ip inst_ports ∈ (components;ports)[{Inst}] ⤔ (components;ports)[{Mdl}]&#10; @mp_i inst_ports[IPort] ⊆ IPort&#10; @mp_o inst_ports[OPort] ⊆ OPort&#10; @ports_inst_rel_comp_inst ports∼[dom(inst_ports)] ⊆ dom(inst_components) // Les ports instanciés sont des ports de composants instanciés&#10; @ports_inst_rel_port_comp inst_ports∼;ports∼;inst_components ⊆ ports∼&#10; @np new_ports ∈ (components;ports)[{Inst}] ∖ dom(inst_ports) ↣ Port ∖ ran(components;ports)&#10; @np_i new_ports[IPort] ⊆ IPort&#10; @np_o new_ports[OPort] ⊆ OPort&#10; then&#10; @p ports ≔ ports ∪ ((inst_components ∪ new_components)∼;ports;(inst_ports ∪ new_ports))&#10; end&#10;&#10; event apply_link_pattern extends apply_pattern&#10; any comp src_subc dst_subc src_ports dst_ports new_ports&#10; where&#10; @comp comp ∈ components[{Mdl}]&#10; @comp_map ra
<org.eventb.core.refinesMachine name="_gbAPMADlEei-meqqkXX9bA" org.eventb.core.target="mProperty"/>
<org.eventb.core.seesContext name="_0kfYMfqeEeectLZKwQfI0A" org.eventb.core.target="cPort"/>
<org.eventb.core.event name="'" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="instanciate_pattern">
<org.eventb.core.refinesEvent name="_btHw0PqwEeectLZKwQfI0A" org.eventb.core.target="instanciate_pattern"/>
<org.eventb.core.parameter name="_btHw0fqwEeectLZKwQfI0A" org.eventb.core.identifier="inst_ports"/>
<org.eventb.core.guard name="_btHw0_qwEeectLZKwQfI0A" org.eventb.core.label="ip" org.eventb.core.predicate="inst_ports ∈ (components;ports)[{Pat}] ↔ (components;ports)[{Mdl}]"/>
<org.eventb.core.guard name="_btHw1PqwEeectLZKwQfI0A" org.eventb.core.label="ipr" org.eventb.core.predicate="inst_ports∼ ∈ (components;ports)[{Mdl}] ⇸ (components;ports)[{Pat}]"/>
<org.eventb.core.guard name="_btHw1fqwEeectLZKwQfI0A" org.eventb.core.label="pm" org.eventb.core.predicate="p_mult_others ∈ (components;ports)[{Pat}] ∖ dom(inst_ports) → ℕ"/>
<org.eventb.core.action name="_btIX4PqwEeectLZKwQfI0A" org.eventb.core.assignment="p_multiplicity ≔ p_multiplicity (p_mult_others {pp·pp∈(components;ports)[{Pat}] ∣ pp ↦ card(inst_ports[{pp}])})" org.eventb.core.label="p_mult"/>
<org.eventb.core.parameter name="_btHw0vqwEeectLZKwQfI0A" org.eventb.core.identifier="p_mult_others"/>
<org.eventb.core.action name="_btJmA_qwEeectLZKwQfI0A" org.eventb.core.assignment="inst2pat_p ≔ ∅" org.eventb.core.label="inst2pat_p"/>
<org.eventb.core.action name="_btJmCfqwEeectLZKwQfI0A" org.eventb.core.assignment="ports ≔ (components[{Inst}]) ⩤ ports" org.eventb.core.label="ports"/>
<org.eventb.core.action name="_btJmCvqwEeectLZKwQfI0A" org.eventb.core.assignment="to_unfold_p_in ≔ ∅" org.eventb.core.label="unfold_p"/>
<org.eventb.core.action name="_btKNEPqwEeectLZKwQfI0A" org.eventb.core.assignment="p_index ≔ ∅" org.eventb.core.label="p_index"/>
<org.eventb.core.guard name="_btHw1vqwEeectLZKwQfI0A" org.eventb.core.label="thm" org.eventb.core.predicate="∀p· finite(inst_ports[{p}])" org.eventb.core.theorem="true"/>
</org.eventb.core.event>
<org.eventb.core.variable name="_0kf_QPqeEeectLZKwQfI0A" org.eventb.core.identifier="components"/>
<org.eventb.core.variable name="_0kf_QfqeEeectLZKwQfI0A" org.eventb.core.identifier="container"/>
<org.eventb.core.variable name="_0kf_QvqeEeectLZKwQfI0A" org.eventb.core.identifier="containers"/>
<org.eventb.core.variable name="_0kf_Q_qeEeectLZKwQfI0A" org.eventb.core.identifier="c_multiplicity"/>
<org.eventb.core.invariant name="_0kf_RPqeEeectLZKwQfI0A" org.eventb.core.label="port" org.eventb.core.predicate="ports ∈ ran(components) ↔ Port"/>
<org.eventb.core.invariant name="_0kf_RfqeEeectLZKwQfI0A" org.eventb.core.label="port_finite" org.eventb.core.predicate="∀c·finite(ports[{c}])"/>
<org.eventb.core.invariant name="_0kf_RvqeEeectLZKwQfI0A" org.eventb.core.label="port_not_shared" org.eventb.core.predicate="ports∼ ∈ Port ⇸ Component"/>
<org.eventb.core.invariant name="_0kf_R_qeEeectLZKwQfI0A" org.eventb.core.label="p_mult" org.eventb.core.predicate="p_multiplicity ∈ (components;ports)[Pattern] → ℕ"/>
<org.eventb.core.variable name="_btIX4fqwEeectLZKwQfI0A" org.eventb.core.identifier="c_index"/>
<org.eventb.core.invariant name="_btIX4vqwEeectLZKwQfI0A" org.eventb.core.label="to_unfold_p_in" org.eventb.core.predicate="to_unfold_p_in ∈ (components;ports)[{Pat}] ↔ components[{Inst}]"/>
<org.eventb.core.event name="_btIX4_qwEeectLZKwQfI0A" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="unfold_root_c">
<org.eventb.core.refinesEvent name="_jNxEQAKyEeiAPf1wPUl3Gw" org.eventb.core.target="unfold_root_c"/>
<org.eventb.core.action name="_btKNFfqwEeectLZKwQfI0A" org.eventb.core.assignment="to_unfold_p_in ≔ to_unfold_p_in ∪ (ports[{c}] × ran(new_c))" org.eventb.core.label="unfold_p_in"/>
</org.eventb.core.event>
<org.eventb.core.event name="_btJmBfqwEeectLZKwQfI0A" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="unfold_node_c">
<org.eventb.core.refinesEvent name="_LcQUcBKaEeqU6uo9ksjEPA" org.eventb.core.target="unfold_node_c"/>
<org.eventb.core.action name="_GO3gcAK8EeiAPf1wPUl3Gw" org.eventb.core.assignment="to_unfold_p_in ≔ to_unfold_p_in ∪ (ports[{c}] × ran(new_c))" org.eventb.core.label="unfold_p_in"/>
</org.eventb.core.event>
<org.eventb.core.event name="_btKNEfqwEeectLZKwQfI0A" org.eventb.core.convergence="1" org.eventb.core.extended="false" org.eventb.core.label="unfold_p">
<org.eventb.core.parameter name="_btI-8fqwEeectLZKwQfI0A" org.eventb.core.comment="port to unfold" org.eventb.core.identifier="p"/>
<org.eventb.core.parameter name="_btI-8vqwEeectLZKwQfI0A" org.eventb.core.comment="target component" org.eventb.core.identifier="c"/>
<org.eventb.core.parameter name="_btJmB_qwEeectLZKwQfI0A" org.eventb.core.comment="replicated ports" org.eventb.core.identifier="new_p"/>
<org.eventb.core.guard name="_btHw1_qwEeectLZKwQfI0A" org.eventb.core.label="p_ty" org.eventb.core.predicate="p ↦ c ∈ to_unfold_p_in"/>
<org.eventb.core.guard name="_btHw2PqwEeectLZKwQfI0A" org.eventb.core.label="new_p_ty" org.eventb.core.predicate="new_p ∈ 1‥p_multiplicity(p) ↣ Port ∖ ran(components;ports)"/>
<org.eventb.core.guard name="_btHw2fqwEeectLZKwQfI0A" org.eventb.core.label="duplicate_IPorts_direction" org.eventb.core.predicate="p ∈ IPort ⇒ ran(new_p) ⊆ IPort"/>
<org.eventb.core.guard name="_btI-8_qwEeectLZKwQfI0A" org.eventb.core.label="duplicate_OPorts_direction" org.eventb.core.predicate="p ∈ OPort ⇒ ran(new_p) ⊆ OPort"/>
<org.eventb.core.action name="_YHf5cAUuEei9ocE08JsPSw" org.eventb.core.assignment="ports ≔ ports ∪ ({c} × ran(new_p))" org.eventb.core.label="new_p_component"/>
<org.eventb.core.action name="_YHiVsAUuEei9ocE08JsPSw" org.eventb.core.assignment="to_unfold_p_in ≔ to_unfold_p_in ∖ {p↦c}" org.eventb.core.label="dp"/>
<org.eventb.core.action name="_YHiVsQUuEei9ocE08JsPSw" org.eventb.core.assignment="inst2pat_p ≔ inst2pat_p ∪ (ran(new_p) × {p})" org.eventb.core.label="inst2pat_p"/>
<org.eventb.core.action name="_f2PGEAspEeigQsLVMUeRQw" org.eventb.core.assignment="p_index ≔ p_index ∪ new_p∼" org.eventb.core.label="p_index"/>
</org.eventb.core.event>
<org.eventb.core.event name="_btKNGPqwEeectLZKwQfI0A" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="apply_pattern">
<org.eventb.core.refinesEvent name="_LcQ7gBKaEeqU6uo9ksjEPA" org.eventb.core.target="apply_pattern"/>
<org.eventb.core.parameter name="_btKNE_qwEeectLZKwQfI0A" org.eventb.core.identifier="inst_ports"/>
<org.eventb.core.parameter name="_LNbVcAWLEei9ocE08JsPSw" org.eventb.core.identifier="new_ports"/>
<org.eventb.core.guard name="_btI-9PqwEeectLZKwQfI0A" org.eventb.core.label="ip" org.eventb.core.predicate="inst_ports ∈ (components;ports)[{Inst}] ⤔ (components;ports)[{Mdl}]"/>
<org.eventb.core.guard name="_btI-9fqwEeectLZKwQfI0A" org.eventb.core.label="mp_i" org.eventb.core.predicate="inst_ports[IPort] ⊆ IPort"/>
<org.eventb.core.guard name="_btI-9vqwEeectLZKwQfI0A" org.eventb.core.label="mp_o" org.eventb.core.predicate="inst_ports[OPort] ⊆ OPort"/>
<org.eventb.core.guard name="_btI-9_qwEeectLZKwQfI0A" org.eventb.core.comment="Les ports instanciés sont des ports de composants instanciés" org.eventb.core.label="ports_inst_rel_comp_inst" org.eventb.core.predicate="ports∼[dom(inst_ports)] ⊆ dom(inst_components)"/>
<org.eventb.core.guard name="_btI--PqwEeectLZKwQfI0A" org.eventb.core.label="ports_inst_rel_port_comp" org.eventb.core.predicate="inst_ports∼;ports∼;inst_components ⊆ ports∼"/>
<org.eventb.core.guard name="_btI--fqwEeectLZKwQfI0A" org.eventb.core.label="np" org.eventb.core.predicate="new_ports ∈ (components;ports)[{Inst}] ∖ dom(inst_ports) ↣ Port ∖ ran(components;ports)"/>
<org.eventb.core.guard name="_knJVMAK2EeiAPf1wPUl3Gw" org.eventb.core.label="np_i" org.eventb.core.predicate="new_ports[IPort] ⊆ IPort"/>
<org.eventb.core.guard name="_OuP8ACxHEeiUbZrF94gIyA" org.eventb.core.label="np_o" org.eventb.core.predicate="new_ports[OPort] ⊆ OPort"/>
<org.eventb.core.action name="_nVtZw_I8EemlHb-ZV1EcBQ" org.eventb.core.assignment="ports ≔ ports ∪ ((inst_components ∪ new_components)∼;ports;(inst_ports ∪ new_ports))" org.eventb.core.label="p"/>
</org.eventb.core.event>
<org.eventb.core.variable name="_zYW3EPqwEeectLZKwQfI0A" org.eventb.core.identifier="to_unfold_c"/>
<org.eventb.core.invariant name="_zYW3EfqwEeectLZKwQfI0A" org.eventb.core.label="inst2pat_p_ty" org.eventb.core.predicate="inst2pat_p ∈ (components;ports)[{Inst}] → (components;ports)[{Pat}]"/>
<org.eventb.core.variable name="_ANiZwPqxEeectLZKwQfI0A" org.eventb.core.identifier="to_unfold_c_in"/>
<org.eventb.core.variable name="_JtPOYPqxEeectLZKwQfI0A" org.eventb.core.identifier="inst2pat_c"/>
<org.eventb.core.variable name="_jRoOoPqxEeectLZKwQfI0A" org.eventb.core.identifier="cProperties"/>
<org.eventb.core.variable name="_oU9JIPqyEeectLZKwQfI0A" org.eventb.core.identifier="M"/>
<org.eventb.core.invariant name="_F0IYkPriEeerIsS6OyYQ4w" org.eventb.core.label="inst2pat_commp" org.eventb.core.predicate="inst2pat_p;ports∼ = ports∼;inst2pat_c"/>
<org.eventb.core.variable name="_6RL9kAA2EeictLZKwQfI0A" org.eventb.core.identifier="P"/>
<org.eventb.core.variable name="_h1eCEADlEei-meqqkXX9bA" org.eventb.core.identifier="c_indexes"/>
<org.eventb.core.invariant name="_ui7VEAFGEei9ocE08JsPSw" org.eventb.core.label="to_unfold_p_inst2pat" org.eventb.core.predicate="ran(to_unfold_p_in) ⊆ dom(inst2pat_c)"/>
<org.eventb.core.event name="_YUG9oAKzEeiAPf1wPUl3Gw" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="apply_link_pattern">
<org.eventb.core.refinesEvent name="_YUG9oQKzEeiAPf1wPUl3Gw" org.eventb.core.target="apply_pattern"/>
<org.eventb.core.parameter name="_nVsysvI8EemlHb-ZV1EcBQ" org.eventb.core.identifier="comp"/>
<org.eventb.core.parameter name="_nVsys_I8EemlHb-ZV1EcBQ" org.eventb.core.identifier="src_subc"/>
<org.eventb.core.parameter name="_nVsytPI8EemlHb-ZV1EcBQ" org.eventb.core.identifier="dst_subc"/>
<org.eventb.core.parameter name="_nVsytfI8EemlHb-ZV1EcBQ" org.eventb.core.identifier="src_ports"/>
<org.eventb.core.parameter name="_nVsytvI8EemlHb-ZV1EcBQ" org.eventb.core.identifier="dst_ports"/>
<org.eventb.core.parameter name="_nVsyt_I8EemlHb-ZV1EcBQ" org.eventb.core.identifier="new_ports"/>
<org.eventb.core.guard name="_nVsyuPI8EemlHb-ZV1EcBQ" org.eventb.core.label="comp" org.eventb.core.predicate="comp ∈ components[{Mdl}]"/>
<org.eventb.core.guard name="_nVsyufI8EemlHb-ZV1EcBQ" org.eventb.core.label="comp_map" org.eventb.core.predicate="ran( inst_components) = {comp}"/>
<org.eventb.core.guard name="_nVsyuvI8EemlHb-ZV1EcBQ" org.eventb.core.label="src_subc" org.eventb.core.predicate="src_subc × {comp} ⊆ container"/>
<org.eventb.core.guard name="_nVsyu_I8EemlHb-ZV1EcBQ" org.eventb.core.label="dst_subc" org.eventb.core.predicate="dst_subc × {comp} ⊆ container"/>
<org.eventb.core.guard name="_nVsyvPI8EemlHb-ZV1EcBQ" org.eventb.core.label="ip" org.eventb.core.predicate="src_ports ∈ (inst_components∼;ports▷IPort)[{comp}] ⤔ ports[src_subc] ∩ OPort"/>
<org.eventb.core.guard name="_nVsyvfI8EemlHb-ZV1EcBQ" org.eventb.core.label="op" org.eventb.core.predicate="dst_ports ∈ (inst_components∼;ports▷OPort)[{comp}] ⤔ ports[dst_subc] ∩ IPort"/>
<org.eventb.core.guard name="_nVsyvvI8EemlHb-ZV1EcBQ" org.eventb.core.label="np" org.eventb.core.predicate="new_ports ∈ (components;ports)[{Inst}] ∖ (dom(src_ports) ∪ dom(src_ports)) ↣ Port ∖ ran(components;ports)"/>
<org.eventb.core.guard name="_nVtZwPI8EemlHb-ZV1EcBQ" org.eventb.core.label="np_i" org.eventb.core.predicate="new_ports[IPort] ⊆ IPort"/>
<org.eventb.core.guard name="_nVtZwfI8EemlHb-ZV1EcBQ" org.eventb.core.label="np_o" org.eventb.core.predicate="new_ports[OPort] ⊆ OPort"/>
<org.eventb.core.action name="_LcSJoBKaEeqU6uo9ksjEPA" org.eventb.core.assignment="ports ≔ ports ∪ ((inst_components ∪ new_components)∼;ports;new_ports)" org.eventb.core.label="p"/>
</org.eventb.core.event>
<org.eventb.core.variable name="_zY448AK7EeiAPf1wPUl3Gw" org.eventb.core.identifier="ports"/>
<org.eventb.core.variable name="_zY448QK7EeiAPf1wPUl3Gw" org.eventb.core.identifier="p_multiplicity"/>
<org.eventb.core.invariant name="_zY448gK7EeiAPf1wPUl3Gw" org.eventb.core.label="to_unfold_p_in_comp" org.eventb.core.predicate="to_unfold_p_in;inst2pat_c ⊆ ports∼"/>
<org.eventb.core.invariant name="_22_TUALCEeiAPf1wPUl3Gw" org.eventb.core.label="i2p_IPort" org.eventb.core.predicate="inst2pat_p[IPort] ⊆ IPort"/>
<org.eventb.core.invariant name="_QFUfMAWQEei9ocE08JsPSw" org.eventb.core.label="i2p_OPort" org.eventb.core.predicate="inst2pat_p[OPort] ⊆ OPort"/>
<org.eventb.core.invariant name="_QFVGQAWQEei9ocE08JsPSw" org.eventb.core.label="p_index_ty" org.eventb.core.predicate="p_index ∈ dom(inst2pat_p) → ℕ"/>
<org.eventb.core.variant name="_7pQu4Af5EeiFlqW-8GKglg" org.eventb.core.expression="to_unfold_p_in"/>
<org.eventb.core.variable name="_LcSJoRKaEeqU6uo9ksjEPA" org.eventb.core.identifier="p_index"/>
<org.eventb.core.variable name="_LcSJohKaEeqU6uo9ksjEPA" org.eventb.core.identifier="to_unfold_p_in"/>
<org.eventb.core.variable name="_XAX34BKaEeqU6uo9ksjEPA" org.eventb.core.identifier="inst2pat_p"/>
</org.eventb.core.machineFile>