mirror of
http://172.16.200.102/MOISE/Pattern-Instanciation-On-System-Engineering-Model.git
synced 2026-03-12 05:51:48 +01:00
36 lines
4.8 KiB
XML
36 lines
4.8 KiB
XML
<?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="1575026127695" org.eventb.texttools.text_representation="machine mProperty refines mComponent sees cComponent variables components container containers c_multiplicity c_index to_unfold_c to_unfold_c_in cProperties inst2pat_c M P c_indexes invariants @prop cProperties ∈ Component ↔ Property events event instanciate_pattern extends instanciate_pattern end event unfold_root_c extends unfold_root_c then @prop cProperties ≔ cProperties ∪ (ran(new_c)×cProperties[{c}]) end event unfold_node_c extends unfold_node_c then @prop cProperties ≔ cProperties ∪ (ran(new_c)×cProperties[{c}]) end event apply_pattern extends apply_pattern any inst_props where @inst_prop inst_props ∈ Property ⇸ Property // pattern properties to model properties then @prop cProperties ≔ cProperties ∪ ((inst_components ∪ new_components)∼;cProperties; (id inst_props)) end end " version="5">
|
||
<org.eventb.core.refinesMachine name="_0kfYMPqeEeectLZKwQfI0A" org.eventb.core.target="mComponent"/>
|
||
<org.eventb.core.seesContext name="_Rf6I4ADlEei-meqqkXX9bA" org.eventb.core.target="cComponent"/>
|
||
<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.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="prop" org.eventb.core.predicate="cProperties ∈ Component ↔ Property"/>
|
||
<org.eventb.core.variable name="_btIX4fqwEeectLZKwQfI0A" org.eventb.core.identifier="c_index"/>
|
||
<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="_bAhygAKxEeiAPf1wPUl3Gw" org.eventb.core.target="unfold_root_c"/>
|
||
<org.eventb.core.action name="_btIX4PqwEeectLZKwQfI0A" org.eventb.core.assignment="cProperties ≔ cProperties ∪ (ran(new_c)×cProperties[{c}])" org.eventb.core.label="prop"/>
|
||
</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="_MU_ooBH9EeqU6uo9ksjEPA" org.eventb.core.target="unfold_node_c"/>
|
||
<org.eventb.core.action name="_btJmA_qwEeectLZKwQfI0A" org.eventb.core.assignment="cProperties ≔ cProperties ∪ (ran(new_c)×cProperties[{c}])" org.eventb.core.label="prop"/>
|
||
</org.eventb.core.event>
|
||
<org.eventb.core.event name="_btKNEfqwEeectLZKwQfI0A" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="apply_pattern">
|
||
<org.eventb.core.refinesEvent name="_MVAPsBH9EeqU6uo9ksjEPA" org.eventb.core.target="apply_pattern"/>
|
||
<org.eventb.core.parameter name="_btHw0fqwEeectLZKwQfI0A" org.eventb.core.identifier="inst_props"/>
|
||
<org.eventb.core.guard name="_btHw0_qwEeectLZKwQfI0A" org.eventb.core.comment="pattern properties to model properties" org.eventb.core.label="inst_prop" org.eventb.core.predicate="inst_props ∈ Property ⇸ Property"/>
|
||
<org.eventb.core.action name="_bAhyggKxEeiAPf1wPUl3Gw" org.eventb.core.assignment="cProperties ≔ cProperties ∪ ((inst_components ∪ new_components)∼;cProperties; (id inst_props))" org.eventb.core.label="prop"/>
|
||
</org.eventb.core.event>
|
||
<org.eventb.core.variable name="_zYW3EPqwEeectLZKwQfI0A" org.eventb.core.identifier="to_unfold_c"/>
|
||
<org.eventb.core.variable name="_ANiZwPqxEeectLZKwQfI0A" org.eventb.core.identifier="to_unfold_c_in"/>
|
||
<org.eventb.core.variable name="_JtPOYPqxEeectLZKwQfI0A" org.eventb.core.identifier="cProperties"/>
|
||
<org.eventb.core.variable name="_gk8cUAK8EeiAPf1wPUl3Gw" org.eventb.core.identifier="inst2pat_c"/>
|
||
<org.eventb.core.variable name="_auDgABKZEeqU6uo9ksjEPA" org.eventb.core.identifier="M"/>
|
||
<org.eventb.core.variable name="_auDgARKZEeqU6uo9ksjEPA" org.eventb.core.identifier="P"/>
|
||
<org.eventb.core.variable name="_auDgAhKZEeqU6uo9ksjEPA" org.eventb.core.identifier="c_indexes"/>
|
||
</org.eventb.core.machineFile>
|