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.
3 Commits
1 Branch
0 Tags
3.4 MiB
Tree: 3bf1aadfd6
Branches Tags
${ item.name }
Create tag ${ searchTerm }
Create branch ${ searchTerm }
from '3bf1aadfd6'
${ noResults }
Pattern-Instanciation-On-Sy.../Event-B/pseim/team/pattern_safety.buc.xmb

279 lines
19 KiB
Raw Normal View History Unescape

Initial commit.
6 years ago
<?xml version="1.0" encoding="UTF-8"?>
<context:Context xmi:version="2.0" xmlns:xmi="http://www.omg.org/XMI" xmlns:context="http://emf.eventb.org/models/core/context/2014" name="pattern_safety">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="configuration" value="org.eventb.core.fwd;de.prob.symbolic.ctxBase;de.prob.units.mchBase;org.eventb.codegen.ui.cgConfig"/>
<details key="name" value="pattern_safety"/>
</annotations>
<annotations source="http:///org/eventb/core/RodinReferenceNamesAnnotations">
<details key="extends cLink" value="_-yB9QAAPEeis7pYemx4WBQ"/>
</annotations>
<attributes key="org.eventb.texttools.text_lastmodified">
<value type="Long" value="ACED00057372000E6A6176612E6C616E672E4C6F6E673B8BE490CC8F23DF0200014A000576616C7565787200106A6176612E6C616E672E4E756D62657286AC951D0B94E08B02000078700000016128212865"/>
</attributes>
<attributes key="org.eventb.texttools.text_representation">
<value type="String" value="ACED0005740913636F6E74657874207061747465726E5F73616665747920657874656E647320634C696E6B0A0A636F6E7374616E7473207265706C696361746F722062616C6C6F745F626F78207361666574795F6D6F64656C207361666574795F636F6D70207361666574795F636F6E7461696E657220746F795F6D6F64656C20746F795F636F6E7461696E657220746F795F61707020746F795F696E705F3120746F795F696E705F3220746F795F6F757470757420636F6D706F6E656E74735F76617220636F6E7461696E65725F76617220665F636F6E7461696E65725F76617220696E73745F636F6D706F6E656E74735F70617220635F6D756C745F6F74686572735F70617220635F6D756C7469706C69636974795F76617220746F5F756E666F6C645F635F7661720A0A6178696F6D730A2020407265706C696361746F725F7479207265706C696361746F7220E2888820436F6D706F6E656E74202F2F20736166657479207061747465726E0A20204062616C6C6F745F626F785F74792062616C6C6F745F626F7820E2888820436F6D706F6E656E740A2020407361666574795F636F6D70207361666574795F636F6D7020E2888820436F6D706F6E656E740A202040616C6C5F646966665F636F6D706F6E656E74207265706C696361746F7220E289A02062616C6C6F745F626F7820E288A7207265706C696361746F7220E289A0207361666574795F636F6D7020E288A72062616C6C6F745F626F7820E289A0207361666574795F636F6D700A2020407361666574795F636F6E7461696E6572207361666574795F636F6E7461696E6572203D207B7265706C696361746F7220E286A6207361666574795F636F6D702C2062616C6C6F745F626F7820E286A6207361666574795F636F6D707D0A202040746F795F636F6E7461696E65725F747920746F795F636F6E7461696E657220E2888820436F6D706F6E656E7420E287B820436F6D706F6E656E740A202040746F795F636F6E7461696E65725F64656620746F795F636F6E7461696E6572203D20E288850A2020407361666574795F6D6F64656C207361666574795F6D6F64656C20E28888204D6F64656C0A202040746F795F6D6F64656C5F747920746F795F6D6F64656C20E28888204D6F64656C0A2020407361666574795F646966665F746F79207361666574795F6D6F64656C20E289A020746F795F6D6F64656C0A2020404D6F64656C5F646566204D6F64656C203D207B7361666574795F6D6F64656C2C746F795F6D6F64656C7D0A202040746F795F6170705F747920746F795F61707020E2888820436F6D706F6E656E74202F2F20746F79206170706C69636174696F6E0A202040746F795F696E705F315F747920746F795F696E705F3120E288882049506F72740A202040746F795F696E705F325F747920746F795F696E705F3220E288882049506F72740A202040746F795F6F75747075745F747920746F795F6F757470757420E28888204F506F72740A202040636F6D706F6E656E74735F7661725F64656620636F6D706F6E656E74735F766172203D207B7361666574795F6D6F64656C20E286A6207B7265706C696361746F722C62616C6C6F745F626F782C7361666574795F636F6D707D2C0A20202020202020202020202020202020202020202020202020202020202020202020202020202020746F795F6D6F64656C20E286A62020207B746F795F6170707D0A2020202020202020202020202020202020202020202020202020202020202020202020202020207D0A202040636F6E7461696E65725F7661725F64656620636F6E7461696E65725F766172203D207B7361666574795F6D6F64656C20E286A6207361666574795F636F6E7461696E65722C20746F795F6D6F64656C20E286A620746F795F636F6E7461696E65727D0A202040665F636F6E7461696E65725F76617220665F636F6E7461696E65725F766172203D207B7265706C696361746F7220E286A6207361666574795F636F6D702C2062616C6C6F745F626F7820E286A6207361666574795F636F6D707D0A20207468656F72656D2040665F616379636C20E288806DC2B720636F6E7461696E65725F766172286D2920E28A8620665F636F6E7461696E65725F7661720A20202020202020202020202020202020202020E288A720665F636F6E7461696E65725F7661723B665F636F6E7461696E65725F76617220E28A8620665F636F6E7461696E65725F7661720A20202020202020202020202020202020202020E288A720696420E288A920665F636F6E7461696E65725F766172203D20E288850A202040696E73745F636F6D706F6E656E74735F64656620696E73745F636F6D706F6E656E74735F706172203D207B7361666574795F636F6D7020E286A620746F795F6170707D0A202040635F6D756C745F6F74686572735F64656620635F6D756C745F6F74686572735F706172203D207B7265706C696361746F7220E286A620332C2062616C6C6F745F626F7820E286A620317D202F2F207061747465726E20696E7374616E74696174696F6E0A202040635F6D756C69706C69636974795F7661725F64656620635F6D756C7469706C69636974795F766172203D207B7361666574795F6D6F64656C20E286A6207B7361666574795F636F6D7020E286A620312C207265706C696361746F7220E286A620332C2062616C6C6F745F626F7820E286A620317D7D0A20207468656F72656D2040635F6D756C7469706C69636974795F61737369676E0A200909635F6D756C7469706C69636974795F7661722873616
</attributes>
<extends href="../cLink.buc#http://emf.eventb.org/models/core/context/2014::Context::cLink"/>
<constants name="replicator">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_-yB9QQAPEeis7pYemx4WBQ"/>
<details key="identifier" value="replicator"/>
</annotations>
</constants>
<constants name="ballot_box">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_-yCkUAAPEeis7pYemx4WBQ"/>
<details key="identifier" value="ballot_box"/>
</annotations>
</constants>
<constants name="safety_model">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_-yCkUQAPEeis7pYemx4WBQ"/>
<details key="identifier" value="safety_model"/>
</annotations>
</constants>
<constants name="safety_comp">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_H1oEsAAQEeis7pYemx4WBQ"/>
<details key="identifier" value="safety_comp"/>
</annotations>
</constants>
<constants name="safety_container">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_oim4QAAQEeis7pYemx4WBQ"/>
<details key="identifier" value="safety_container"/>
</annotations>
</constants>
<constants name="toy_model">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_oim4QQAQEeis7pYemx4WBQ"/>
<details key="identifier" value="toy_model"/>
</annotations>
</constants>
<constants name="toy_container">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_oim4QgAQEeis7pYemx4WBQ"/>
<details key="identifier" value="toy_container"/>
</annotations>
</constants>
<constants name="toy_app">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_oim4QwAQEeis7pYemx4WBQ"/>
<details key="identifier" value="toy_app"/>
</annotations>
</constants>
<constants name="toy_inp_1">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_9c9V0AAREeis7pYemx4WBQ"/>
<details key="identifier" value="toy_inp_1"/>
</annotations>
</constants>
<constants name="toy_inp_2">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_9c9V0QAREeis7pYemx4WBQ"/>
<details key="identifier" value="toy_inp_2"/>
</annotations>
</constants>
<constants name="toy_output">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_9lz6YAASEeis7pYemx4WBQ"/>
<details key="identifier" value="toy_output"/>
</annotations>
</constants>
<constants name="components_var">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_9lz6YQASEeis7pYemx4WBQ"/>
<details key="identifier" value="components_var"/>
</annotations>
</constants>
<constants name="container_var">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_kRNbAAEBEei-meqqkXX9bA"/>
<details key="identifier" value="container_var"/>
</annotations>
</constants>
<constants name="f_container_var">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_kRNbAQEBEei-meqqkXX9bA"/>
<details key="identifier" value="f_container_var"/>
</annotations>
</constants>
<constants name="inst_components_par">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_kRNbAgEBEei-meqqkXX9bA"/>
<details key="identifier" value="inst_components_par"/>
</annotations>
</constants>
<constants name="c_mult_others_par">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_kRNbAwEBEei-meqqkXX9bA"/>
<details key="identifier" value="c_mult_others_par"/>
</annotations>
</constants>
<constants name="c_multiplicity_var">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_kROCEAEBEei-meqqkXX9bA"/>
<details key="identifier" value="c_multiplicity_var"/>
</annotations>
</constants>
<constants name="to_unfold_c_var">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_kROCEQEBEei-meqqkXX9bA"/>
<details key="identifier" value="to_unfold_c_var"/>
</annotations>
</constants>
<axioms comment="safety pattern" name="replicator_ty" predicate="replicator ∈ Component">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_-yCkUgAPEeis7pYemx4WBQ"/>
<details key="label" value="replicator_ty"/>
<details key="comment" value="safety pattern"/>
</annotations>
</axioms>
<axioms name="ballot_box_ty" predicate="ballot_box ∈ Component">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_-yCkUwAPEeis7pYemx4WBQ"/>
<details key="label" value="ballot_box_ty"/>
</annotations>
</axioms>
<axioms name="safety_comp" predicate="safety_comp ∈ Component">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_-yCkVAAPEeis7pYemx4WBQ"/>
<details key="label" value="safety_comp"/>
</annotations>
</axioms>
<axioms name="all_diff_component" predicate="replicator ≠ ballot_box ∧ replicator ≠ safety_comp ∧ ballot_box ≠ safety_comp">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_-yCkVQAPEeis7pYemx4WBQ"/>
<details key="label" value="all_diff_component"/>
</annotations>
</axioms>
<axioms name="safety_container" predicate="safety_container = {replicator ↦ safety_comp, ballot_box ↦ safety_comp}">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_oim4RAAQEeis7pYemx4WBQ"/>
<details key="label" value="safety_container"/>
</annotations>
</axioms>
<axioms name="toy_container_ty" predicate="toy_container ∈ Component ⇸ Component">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_oim4RQAQEeis7pYemx4WBQ"/>
<details key="label" value="toy_container_ty"/>
</annotations>
</axioms>
<axioms name="toy_container_def" predicate="toy_container = ∅">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_oim4RgAQEeis7pYemx4WBQ"/>
<details key="label" value="toy_container_def"/>
</annotations>
</axioms>
<axioms name="safety_model" predicate="safety_model ∈ Model">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_oinfUAAQEeis7pYemx4WBQ"/>
<details key="label" value="safety_model"/>
</annotations>
</axioms>
<axioms name="toy_model_ty" predicate="toy_model ∈ Model">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_9c9V0gAREeis7pYemx4WBQ"/>
<details key="label" value="toy_model_ty"/>
</annotations>
</axioms>
<axioms name="safety_diff_toy" predicate="safety_model ≠ toy_model">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_9c9V0wAREeis7pYemx4WBQ"/>
<details key="label" value="safety_diff_toy"/>
</annotations>
</axioms>
<axioms name="Model_def" predicate="Model = {safety_model,toy_model}">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_9c9V1AAREeis7pYemx4WBQ"/>
<details key="label" value="Model_def"/>
</annotations>
</axioms>
<axioms comment="toy application" name="toy_app_ty" predicate="toy_app ∈ Component">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_9c984AAREeis7pYemx4WBQ"/>
<details key="label" value="toy_app_ty"/>
<details key="comment" value="toy application"/>
</annotations>
</axioms>
<axioms name="toy_inp_1_ty" predicate="toy_inp_1 ∈ IPort">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_9lz6YgASEeis7pYemx4WBQ"/>
<details key="label" value="toy_inp_1_ty"/>
</annotations>
</axioms>
<axioms name="toy_inp_2_ty" predicate="toy_inp_2 ∈ IPort">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_kROCEgEBEei-meqqkXX9bA"/>
<details key="label" value="toy_inp_2_ty"/>
</annotations>
</axioms>
<axioms name="toy_output_ty" predicate="toy_output ∈ OPort">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_kROCEwEBEei-meqqkXX9bA"/>
<details key="label" value="toy_output_ty"/>
</annotations>
</axioms>
<axioms name="components_var_def" predicate="components_var = {safety_model ↦ {replicator,ballot_box,safety_comp},&#xA; toy_model ↦ {toy_app}&#xA; }">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_kROCFAEBEei-meqqkXX9bA"/>
<details key="label" value="components_var_def"/>
</annotations>
</axioms>
<axioms name="container_var_def" predicate="container_var = {safety_model ↦ safety_container, toy_model ↦ toy_container}">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_kROCFQEBEei-meqqkXX9bA"/>
<details key="label" value="container_var_def"/>
</annotations>
</axioms>
<axioms name="f_container_var" predicate="f_container_var = {replicator ↦ safety_comp, ballot_box ↦ safety_comp}">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_kROCFgEBEei-meqqkXX9bA"/>
<details key="label" value="f_container_var"/>
</annotations>
</axioms>
<axioms name="f_acycl" predicate="∀m· container_var(m) ⊆ f_container_var&#xA; ∧ f_container_var;f_container_var ⊆ f_container_var&#xA; ∧ id ∩ f_container_var = ∅" theorem="true">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_kROCFwEBEei-meqqkXX9bA"/>
<details key="label" value="f_acycl"/>
</annotations>
</axioms>
<axioms name="inst_components_def" predicate="inst_components_par = {safety_comp ↦ toy_app}">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_kROpIAEBEei-meqqkXX9bA"/>
<details key="label" value="inst_components_def"/>
</annotations>
</axioms>
<axioms comment="pattern instantiation" name="c_mult_others_def" predicate="c_mult_others_par = {replicator ↦ 3, ballot_box ↦ 1}">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_kROpIQEBEei-meqqkXX9bA"/>
<details key="label" value="c_mult_others_def"/>
<details key="comment" value="pattern instantiation"/>
</annotations>
</axioms>
<axioms name="c_muliplicity_var_def" predicate="c_multiplicity_var = {safety_model ↦ {safety_comp ↦ 1, replicator ↦ 3, ballot_box ↦ 1}}">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_kROpIgEBEei-meqqkXX9bA"/>
<details key="label" value="c_muliplicity_var_def"/>
</annotations>
</axioms>
<axioms name="c_multiplicity_assign&#xA;" predicate="c_multiplicity_var(safety_model) = c_mult_others_par&#xA; &#x9;&#x9;&#x9; {pc· pc ∈ dom(inst_components_par) ∣ pc ↦ card(inst_components_par[{pc}])}" theorem="true">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_kROpIwEBEei-meqqkXX9bA"/>
<details key="label" value="c_multiplicity_assign&#xA;"/>
</annotations>
</axioms>
<axioms name="to_unfold_c_var_def" predicate="to_unfold_c_var = {safety_comp}">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_kROpJAEBEei-meqqkXX9bA"/>
<details key="label" value="to_unfold_c_var_def"/>
</annotations>
</axioms>
<axioms name="to_unfold_c_var&#xA;" predicate="to_unfold_c_var = (components_var(safety_model) ∖ dom(container_var(safety_model)))" theorem="true">
<annotations source="http:///org/eventb/core/RodinInternalAnnotations">
<details key="name" value="_kROpJQEBEei-meqqkXX9bA"/>
<details key="label" value="to_unfold_c_var&#xA;"/>
</annotations>
</axioms>
</context:Context>