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/pattern_safety.bpo

117 lines
21 KiB
Raw Permalink Blame History Escape

<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.poFile org.eventb.core.poStamp="2">
<org.eventb.core.poPredicateSet name="ABSHYP" org.eventb.core.poStamp="2">
<org.eventb.core.poIdentifier name="Model" org.eventb.core.type="ℙ(Model)"/>
<org.eventb.core.poIdentifier name="Property" org.eventb.core.type="ℙ(Property)"/>
<org.eventb.core.poIdentifier name="Inst" org.eventb.core.type="Model"/>
<org.eventb.core.poIdentifier name="Mdl" org.eventb.core.type="Model"/>
<org.eventb.core.poIdentifier name="Pat" org.eventb.core.type="Model"/>
<org.eventb.core.poIdentifier name="Pattern" org.eventb.core.type="ℙ(Model)"/>
<org.eventb.core.poPredicate name="Propertz" org.eventb.core.predicate="Pattern⊆Model" org.eventb.core.source="/MODELS_INC_V9_VAR/cModel.buc|org.eventb.core.contextFile#cModel|org.eventb.core.axiom#_h20wcfqkEeectLZKwQfI0A"/>
<org.eventb.core.poPredicate name="Propert{" org.eventb.core.predicate="Mdl∈Model ∖ Pattern" org.eventb.core.source="/MODELS_INC_V9_VAR/cModel.buc|org.eventb.core.contextFile#cModel|org.eventb.core.axiom#_h20wcvqkEeectLZKwQfI0A"/>
<org.eventb.core.poPredicate name="Propert|" org.eventb.core.predicate="Pat∈Pattern" org.eventb.core.source="/MODELS_INC_V9_VAR/cModel.buc|org.eventb.core.contextFile#cModel|org.eventb.core.axiom#_h20wc_qkEeectLZKwQfI0A"/>
<org.eventb.core.poPredicate name="Propert}" org.eventb.core.predicate="Inst∈Model ∖ Pattern" org.eventb.core.source="/MODELS_INC_V9_VAR/cModel.buc|org.eventb.core.contextFile#cModel|org.eventb.core.axiom#_fxjdEQKnEeiAPf1wPUl3Gw"/>
<org.eventb.core.poPredicate name="Propert~" org.eventb.core.predicate="Inst≠Mdl" org.eventb.core.source="/MODELS_INC_V9_VAR/cModel.buc|org.eventb.core.contextFile#cModel|org.eventb.core.axiom#_DGgrYAUMEei9ocE08JsPSw"/>
<org.eventb.core.poIdentifier name="Component" org.eventb.core.type="ℙ(Component)"/>
<org.eventb.core.poIdentifier name="Port" org.eventb.core.type="ℙ(Port)"/>
<org.eventb.core.poIdentifier name="IPort" org.eventb.core.type="ℙ(Port)"/>
<org.eventb.core.poIdentifier name="OPort" org.eventb.core.type="ℙ(Port)"/>
<org.eventb.core.poPredicate name="Componenu" org.eventb.core.predicate="partition(Port,IPort,OPort)" org.eventb.core.source="/MODELS_INC_V9_VAR/cPort.buc|org.eventb.core.contextFile#cPort|org.eventb.core.axiom#_Y1LocvqyEeectLZKwQfI0A"/>
<org.eventb.core.poIdentifier name="Link" org.eventb.core.type="ℙ(Link)"/>
<org.eventb.core.poIdentifier name="First" org.eventb.core.type="ℙ(Link)"/>
<org.eventb.core.poIdentifier name="Identity" org.eventb.core.type="ℙ(Link)"/>
<org.eventb.core.poIdentifier name="LKind" org.eventb.core.type="ℙ(ℙ(Link))"/>
<org.eventb.core.poIdentifier name="Rotate" org.eventb.core.type="ℙ(Link)"/>
<org.eventb.core.poIdentifier name="Shift" org.eventb.core.type="ℙ(Link)"/>
<org.eventb.core.poIdentifier name="Transpose" org.eventb.core.type="ℙ(Link)"/>
<org.eventb.core.poPredicate name="Transposf" org.eventb.core.predicate="partition(Link,Transpose,Identity,Shift,First,Rotate)" org.eventb.core.source="/MODELS_INC_V9_VAR/cLink.buc|org.eventb.core.contextFile#cLink|org.eventb.core.axiom#_u1ZfsfgzEeeeS5KQUtrGlw"/>
<org.eventb.core.poPredicate name="Transposg" org.eventb.core.predicate="LKind={Transpose,Identity,Shift,First,Rotate}" org.eventb.core.source="/MODELS_INC_V9_VAR/cLink.buc|org.eventb.core.contextFile#cLink|org.eventb.core.axiom#_u1ZfsvgzEeeeS5KQUtrGlw"/>
<org.eventb.core.poIdentifier name="ballot_box" org.eventb.core.type="Component"/>
<org.eventb.core.poIdentifier name="c_mult_others_par" org.eventb.core.type="ℙ(Component×ℤ)"/>
<org.eventb.core.poIdentifier name="c_multiplicity_var" org.eventb.core.type="ℙ(Model×ℙ(Component×ℤ))"/>
<org.eventb.core.poIdentifier name="components_var" org.eventb.core.type="ℙ(Model×ℙ(Component))"/>
<org.eventb.core.poIdentifier name="container_var" org.eventb.core.type="ℙ(Model×ℙ(Component×Component))"/>
<org.eventb.core.poIdentifier name="f_container_var" org.eventb.core.type="ℙ(Component×Component)"/>
<org.eventb.core.poIdentifier name="inst_components_par" org.eventb.core.type="ℙ(Component×Component)"/>
<org.eventb.core.poIdentifier name="replicator" org.eventb.core.type="Component"/>
<org.eventb.core.poIdentifier name="safety_comp" org.eventb.core.type="Component"/>
<org.eventb.core.poIdentifier name="safety_container" org.eventb.core.type="ℙ(Component×Component)"/>
<org.eventb.core.poIdentifier name="safety_model" org.eventb.core.type="Model"/>
<org.eventb.core.poIdentifier name="to_unfold_c_var" org.eventb.core.type="ℙ(Component)"/>
<org.eventb.core.poIdentifier name="toy_app" org.eventb.core.type="Component"/>
<org.eventb.core.poIdentifier name="toy_container" org.eventb.core.type="ℙ(Component×Component)"/>
<org.eventb.core.poIdentifier name="toy_inp_1" org.eventb.core.type="Port"/>
<org.eventb.core.poIdentifier name="toy_inp_2" org.eventb.core.type="Port"/>
<org.eventb.core.poIdentifier name="toy_model" org.eventb.core.type="Model"/>
<org.eventb.core.poIdentifier name="toy_output" org.eventb.core.type="Port"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poSequent name="f_acycl/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Theorem" org.eventb.core.poStamp="2">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/MODELS_INC_V9_VAR/pattern_safety.bpo|org.eventb.core.poFile#pattern_safety|org.eventb.core.poPredicateSet#HYPcComponeo."/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀m⦂Model·m∈dom(container_var)∧container_var∈Model ⇸ ℙ(Component × Component)" org.eventb.core.source="/MODELS_INC_V9_VAR/pattern_safety.buc|org.eventb.core.contextFile#pattern_safety|org.eventb.core.axiom#_kROCFwEBEei-meqqkXX9bA"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/MODELS_INC_V9_VAR/pattern_safety.buc|org.eventb.core.contextFile#pattern_safety|org.eventb.core.axiom#_kROCFwEBEei-meqqkXX9bA"/>
<org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/MODELS_INC_V9_VAR/pattern_safety.bpo|org.eventb.core.poFile#pattern_safety|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poSelHintSnd="/MODELS_INC_V9_VAR/pattern_safety.bpo|org.eventb.core.poFile#pattern_safety|org.eventb.core.poPredicateSet#HYPcComponeo."/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="f_acycl/THM" org.eventb.core.accurate="true" org.eventb.core.poDesc="Theorem" org.eventb.core.poStamp="2">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/MODELS_INC_V9_VAR/pattern_safety.bpo|org.eventb.core.poFile#pattern_safety|org.eventb.core.poPredicateSet#HYPcComponeo."/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀m⦂Model·container_var(m)⊆f_container_var∧f_container_var;f_container_var⊆f_container_var∧(id ⦂ ℙ(Component×Component))∩f_container_var=(∅ ⦂ ℙ(Component×Component))" org.eventb.core.source="/MODELS_INC_V9_VAR/pattern_safety.buc|org.eventb.core.contextFile#pattern_safety|org.eventb.core.axiom#_kROCFwEBEei-meqqkXX9bA"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/MODELS_INC_V9_VAR/pattern_safety.buc|org.eventb.core.contextFile#pattern_safety|org.eventb.core.axiom#_kROCFwEBEei-meqqkXX9bA"/>
<org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/MODELS_INC_V9_VAR/pattern_safety.bpo|org.eventb.core.poFile#pattern_safety|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poSelHintSnd="/MODELS_INC_V9_VAR/pattern_safety.bpo|org.eventb.core.poFile#pattern_safety|org.eventb.core.poPredicateSet#HYPcComponeo."/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="c_multiplicity_assign&#10;/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Theorem" org.eventb.core.poStamp="2">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/MODELS_INC_V9_VAR/pattern_safety.bpo|org.eventb.core.poFile#pattern_safety|org.eventb.core.poPredicateSet#HYPcComponeo2"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="safety_model∈dom(c_multiplicity_var)∧c_multiplicity_var∈Model ⇸ ℙ(Component × ℤ)∧(∀pc⦂Component·pc∈dom(inst_components_par)⇒finite(inst_components_par[{pc}]))" org.eventb.core.source="/MODELS_INC_V9_VAR/pattern_safety.buc|org.eventb.core.contextFile#pattern_safety|org.eventb.core.axiom#_kROpIwEBEei-meqqkXX9bA"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/MODELS_INC_V9_VAR/pattern_safety.buc|org.eventb.core.contextFile#pattern_safety|org.eventb.core.axiom#_kROpIwEBEei-meqqkXX9bA"/>
<org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/MODELS_INC_V9_VAR/pattern_safety.bpo|org.eventb.core.poFile#pattern_safety|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poSelHintSnd="/MODELS_INC_V9_VAR/pattern_safety.bpo|org.eventb.core.poFile#pattern_safety|org.eventb.core.poPredicateSet#HYPcComponeo2"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="c_multiplicity_assign&#10;/THM" org.eventb.core.accurate="true" org.eventb.core.poDesc="Theorem" org.eventb.core.poStamp="2">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/MODELS_INC_V9_VAR/pattern_safety.bpo|org.eventb.core.poFile#pattern_safety|org.eventb.core.poPredicateSet#HYPcComponeo2"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="c_multiplicity_var(safety_model)=c_mult_others_par{pc⦂Component·pc∈dom(inst_components_par) ∣ pc ↦ card(inst_components_par[{pc}])}" org.eventb.core.source="/MODELS_INC_V9_VAR/pattern_safety.buc|org.eventb.core.contextFile#pattern_safety|org.eventb.core.axiom#_kROpIwEBEei-meqqkXX9bA"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/MODELS_INC_V9_VAR/pattern_safety.buc|org.eventb.core.contextFile#pattern_safety|org.eventb.core.axiom#_kROpIwEBEei-meqqkXX9bA"/>
<org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/MODELS_INC_V9_VAR/pattern_safety.bpo|org.eventb.core.poFile#pattern_safety|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poSelHintSnd="/MODELS_INC_V9_VAR/pattern_safety.bpo|org.eventb.core.poFile#pattern_safety|org.eventb.core.poPredicateSet#HYPcComponeo2"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="to_unfold_c_var&#10;/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Theorem" org.eventb.core.poStamp="2">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/MODELS_INC_V9_VAR/pattern_safety.bpo|org.eventb.core.poFile#pattern_safety|org.eventb.core.poPredicateSet#HYPcComponeo4"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="safety_model∈dom(components_var)∧components_var∈Model ⇸ ℙ(Component)∧safety_model∈dom(container_var)∧container_var∈Model ⇸ ℙ(Component × Component)" org.eventb.core.source="/MODELS_INC_V9_VAR/pattern_safety.buc|org.eventb.core.contextFile#pattern_safety|org.eventb.core.axiom#_kROpJQEBEei-meqqkXX9bA"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/MODELS_INC_V9_VAR/pattern_safety.buc|org.eventb.core.contextFile#pattern_safety|org.eventb.core.axiom#_kROpJQEBEei-meqqkXX9bA"/>
<org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/MODELS_INC_V9_VAR/pattern_safety.bpo|org.eventb.core.poFile#pattern_safety|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poSelHintSnd="/MODELS_INC_V9_VAR/pattern_safety.bpo|org.eventb.core.poFile#pattern_safety|org.eventb.core.poPredicateSet#HYPcComponeo4"/>
</org.eventb.core.poSequent>
<org.eventb.core.poSequent name="to_unfold_c_var&#10;/THM" org.eventb.core.accurate="true" org.eventb.core.poDesc="Theorem" org.eventb.core.poStamp="2">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/MODELS_INC_V9_VAR/pattern_safety.bpo|org.eventb.core.poFile#pattern_safety|org.eventb.core.poPredicateSet#HYPcComponeo4"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="to_unfold_c_var=components_var(safety_model) ∖ dom(container_var(safety_model))" org.eventb.core.source="/MODELS_INC_V9_VAR/pattern_safety.buc|org.eventb.core.contextFile#pattern_safety|org.eventb.core.axiom#_kROpJQEBEei-meqqkXX9bA"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/MODELS_INC_V9_VAR/pattern_safety.buc|org.eventb.core.contextFile#pattern_safety|org.eventb.core.axiom#_kROpJQEBEei-meqqkXX9bA"/>
<org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/MODELS_INC_V9_VAR/pattern_safety.bpo|org.eventb.core.poFile#pattern_safety|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poSelHintSnd="/MODELS_INC_V9_VAR/pattern_safety.bpo|org.eventb.core.poFile#pattern_safety|org.eventb.core.poPredicateSet#HYPcComponeo4"/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="HYPcComponeo." org.eventb.core.parentSet="/MODELS_INC_V9_VAR/pattern_safety.bpo|org.eventb.core.poFile#pattern_safety|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poStamp="2">
<org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="replicator∈Component" org.eventb.core.source="/MODELS_INC_V9_VAR/pattern_safety.buc|org.eventb.core.contextFile#pattern_safety|org.eventb.core.axiom#_-yCkUgAPEeis7pYemx4WBQ"/>
<org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="ballot_box∈Component" org.eventb.core.source="/MODELS_INC_V9_VAR/pattern_safety.buc|org.eventb.core.contextFile#pattern_safety|org.eventb.core.axiom#_-yCkUwAPEeis7pYemx4WBQ"/>
<org.eventb.core.poPredicate name="PRD2" org.eventb.core.predicate="safety_comp∈Component" org.eventb.core.source="/MODELS_INC_V9_VAR/pattern_safety.buc|org.eventb.core.contextFile#pattern_safety|org.eventb.core.axiom#_-yCkVAAPEeis7pYemx4WBQ"/>
<org.eventb.core.poPredicate name="PRD3" org.eventb.core.predicate="replicator≠ballot_box∧replicator≠safety_comp∧ballot_box≠safety_comp" org.eventb.core.source="/MODELS_INC_V9_VAR/pattern_safety.buc|org.eventb.core.contextFile#pattern_safety|org.eventb.core.axiom#_-yCkVQAPEeis7pYemx4WBQ"/>
<org.eventb.core.poPredicate name="PRD4" org.eventb.core.predicate="safety_container={replicator ↦ safety_comp,ballot_box ↦ safety_comp}" org.eventb.core.source="/MODELS_INC_V9_VAR/pattern_safety.buc|org.eventb.core.contextFile#pattern_safety|org.eventb.core.axiom#_oim4RAAQEeis7pYemx4WBQ"/>
<org.eventb.core.poPredicate name="PRD5" org.eventb.core.predicate="toy_container∈Component ⇸ Component" org.eventb.core.source="/MODELS_INC_V9_VAR/pattern_safety.buc|org.eventb.core.contextFile#pattern_safety|org.eventb.core.axiom#_oim4RQAQEeis7pYemx4WBQ"/>
<org.eventb.core.poPredicate name="PRD6" org.eventb.core.predicate="toy_container=(∅ ⦂ ℙ(Component×Component))" org.eventb.core.source="/MODELS_INC_V9_VAR/pattern_safety.buc|org.eventb.core.contextFile#pattern_safety|org.eventb.core.axiom#_oim4RgAQEeis7pYemx4WBQ"/>
<org.eventb.core.poPredicate name="PRD7" org.eventb.core.predicate="safety_model∈Model" org.eventb.core.source="/MODELS_INC_V9_VAR/pattern_safety.buc|org.eventb.core.contextFile#pattern_safety|org.eventb.core.axiom#_oinfUAAQEeis7pYemx4WBQ"/>
<org.eventb.core.poPredicate name="PRD8" org.eventb.core.predicate="toy_model∈Model" org.eventb.core.source="/MODELS_INC_V9_VAR/pattern_safety.buc|org.eventb.core.contextFile#pattern_safety|org.eventb.core.axiom#_9c9V0gAREeis7pYemx4WBQ"/>
<org.eventb.core.poPredicate name="PRD9" org.eventb.core.predicate="safety_model≠toy_model" org.eventb.core.source="/MODELS_INC_V9_VAR/pattern_safety.buc|org.eventb.core.contextFile#pattern_safety|org.eventb.core.axiom#_9c9V0wAREeis7pYemx4WBQ"/>
<org.eventb.core.poPredicate name="PRD10" org.eventb.core.predicate="Model={safety_model,toy_model}" org.eventb.core.source="/MODELS_INC_V9_VAR/pattern_safety.buc|org.eventb.core.contextFile#pattern_safety|org.eventb.core.axiom#_9c9V1AAREeis7pYemx4WBQ"/>
<org.eventb.core.poPredicate name="PRD11" org.eventb.core.predicate="toy_app∈Component" org.eventb.core.source="/MODELS_INC_V9_VAR/pattern_safety.buc|org.eventb.core.contextFile#pattern_safety|org.eventb.core.axiom#_9c984AAREeis7pYemx4WBQ"/>
<org.eventb.core.poPredicate name="PRD12" org.eventb.core.predicate="toy_inp_1∈IPort" org.eventb.core.source="/MODELS_INC_V9_VAR/pattern_safety.buc|org.eventb.core.contextFile#pattern_safety|org.eventb.core.axiom#_9lz6YgASEeis7pYemx4WBQ"/>
<org.eventb.core.poPredicate name="PRD13" org.eventb.core.predicate="toy_inp_2∈IPort" org.eventb.core.source="/MODELS_INC_V9_VAR/pattern_safety.buc|org.eventb.core.contextFile#pattern_safety|org.eventb.core.axiom#_kROCEgEBEei-meqqkXX9bA"/>
<org.eventb.core.poPredicate name="PRD14" org.eventb.core.predicate="toy_output∈OPort" org.eventb.core.source="/MODELS_INC_V9_VAR/pattern_safety.buc|org.eventb.core.contextFile#pattern_safety|org.eventb.core.axiom#_kROCEwEBEei-meqqkXX9bA"/>
<org.eventb.core.poPredicate name="PRD15" org.eventb.core.predicate="components_var={safety_model ↦ {replicator,ballot_box,safety_comp},toy_model ↦ {toy_app}}" org.eventb.core.source="/MODELS_INC_V9_VAR/pattern_safety.buc|org.eventb.core.contextFile#pattern_safety|org.eventb.core.axiom#_kROCFAEBEei-meqqkXX9bA"/>
<org.eventb.core.poPredicate name="PRD16" org.eventb.core.predicate="container_var={safety_model ↦ safety_container,toy_model ↦ toy_container}" org.eventb.core.source="/MODELS_INC_V9_VAR/pattern_safety.buc|org.eventb.core.contextFile#pattern_safety|org.eventb.core.axiom#_kROCFQEBEei-meqqkXX9bA"/>
<org.eventb.core.poPredicate name="PRD17" org.eventb.core.predicate="f_container_var={replicator ↦ safety_comp,ballot_box ↦ safety_comp}" org.eventb.core.source="/MODELS_INC_V9_VAR/pattern_safety.buc|org.eventb.core.contextFile#pattern_safety|org.eventb.core.axiom#_kROCFgEBEei-meqqkXX9bA"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="HYPcComponeo2" org.eventb.core.parentSet="/MODELS_INC_V9_VAR/pattern_safety.bpo|org.eventb.core.poFile#pattern_safety|org.eventb.core.poPredicateSet#HYPcComponeo." org.eventb.core.poStamp="2">
<org.eventb.core.poPredicate name="PRD18" org.eventb.core.predicate="∀m⦂Model·container_var(m)⊆f_container_var∧f_container_var;f_container_var⊆f_container_var∧(id ⦂ ℙ(Component×Component))∩f_container_var=(∅ ⦂ ℙ(Component×Component))" org.eventb.core.source="/MODELS_INC_V9_VAR/pattern_safety.buc|org.eventb.core.contextFile#pattern_safety|org.eventb.core.axiom#_kROCFwEBEei-meqqkXX9bA"/>
<org.eventb.core.poPredicate name="PRD19" org.eventb.core.predicate="inst_components_par={safety_comp ↦ toy_app}" org.eventb.core.source="/MODELS_INC_V9_VAR/pattern_safety.buc|org.eventb.core.contextFile#pattern_safety|org.eventb.core.axiom#_kROpIAEBEei-meqqkXX9bA"/>
<org.eventb.core.poPredicate name="PRD20" org.eventb.core.predicate="c_mult_others_par={replicator ↦ 3,ballot_box ↦ 1}" org.eventb.core.source="/MODELS_INC_V9_VAR/pattern_safety.buc|org.eventb.core.contextFile#pattern_safety|org.eventb.core.axiom#_kROpIQEBEei-meqqkXX9bA"/>
<org.eventb.core.poPredicate name="PRD21" org.eventb.core.predicate="c_multiplicity_var={safety_model ↦ {safety_comp ↦ 1,replicator ↦ 3,ballot_box ↦ 1}}" org.eventb.core.source="/MODELS_INC_V9_VAR/pattern_safety.buc|org.eventb.core.contextFile#pattern_safety|org.eventb.core.axiom#_kROpIgEBEei-meqqkXX9bA"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="HYPcComponeo4" org.eventb.core.parentSet="/MODELS_INC_V9_VAR/pattern_safety.bpo|org.eventb.core.poFile#pattern_safety|org.eventb.core.poPredicateSet#HYPcComponeo2" org.eventb.core.poStamp="2">
<org.eventb.core.poPredicate name="PRD22" org.eventb.core.predicate="c_multiplicity_var(safety_model)=c_mult_others_par{pc⦂Component·pc∈dom(inst_components_par) ∣ pc ↦ card(inst_components_par[{pc}])}" org.eventb.core.source="/MODELS_INC_V9_VAR/pattern_safety.buc|org.eventb.core.contextFile#pattern_safety|org.eventb.core.axiom#_kROpIwEBEei-meqqkXX9bA"/>
<org.eventb.core.poPredicate name="PRD23" org.eventb.core.predicate="to_unfold_c_var={safety_comp}" org.eventb.core.source="/MODELS_INC_V9_VAR/pattern_safety.buc|org.eventb.core.contextFile#pattern_safety|org.eventb.core.axiom#_kROpJAEBEei-meqqkXX9bA"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="ALLHYP" org.eventb.core.parentSet="/MODELS_INC_V9_VAR/pattern_safety.bpo|org.eventb.core.poFile#pattern_safety|org.eventb.core.poPredicateSet#HYPcComponeo4" org.eventb.core.poStamp="2">
<org.eventb.core.poPredicate name="PRD24" org.eventb.core.predicate="to_unfold_c_var=components_var(safety_model) ∖ dom(container_var(safety_model))" org.eventb.core.source="/MODELS_INC_V9_VAR/pattern_safety.buc|org.eventb.core.contextFile#pattern_safety|org.eventb.core.axiom#_kROpJQEBEei-meqqkXX9bA"/>
</org.eventb.core.poPredicateSet>
</org.eventb.core.poFile>