MOISE/Pattern-Instanciation-On-System-Engineering-Model
1
0
Fork 0
mirror of http://172.16.200.102/MOISE/Pattern-Instanciation-On-System-Engineering-Model.git synced 2026-01-16 09:11:57 +01:00
Code Issues Projects Releases Wiki Activity
Files
master
Pattern-Instanciation-On-Sy…/Event-B/pseim/pattern_safety.bpo

118 lines
21 KiB
XML
Raw Permalink Blame History

This file contains ambiguous Unicode characters
This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.
<?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>
Reference in New Issue View Git Blame Copy Permalink