Skip to content
Snippets Groups Projects
Normal view History Permalink
CCTx_Ethereum_Fabric_Animation_m3.bcm 49.4 KiB
Newer Older
Guzman Llambias's avatar
Add Ethereum -> Fabric animation (WIP)
Guzman Llambias committed
1 2 3 4 5 6 7 8 
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.scMachineFile org.eventb.core.accurate="true" org.eventb.core.configuration="org.eventb.core.fwd">
    <org.eventb.core.scRefinesMachine name="'" org.eventb.core.scTarget="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bcm" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.refinesMachine#'"/>
    <org.eventb.core.scSeesContext name="(" org.eventb.core.scTarget="/gateway-event-b/CCTx_Ethereum_Fabric_c2.bcc" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.seesContext#_1tlAgL7uEe6laZimEYihUg"/>
    <org.eventb.core.scInternalContext name="CCTx_Abstract_DLT_c1">
        <org.eventb.core.scAxiom name="'" org.eventb.core.label="axm1;" org.eventb.core.predicate="source_smart_contract∈CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_c1.buc|org.eventb.core.contextFile#CCTx_Abstract_DLT_c1|org.eventb.core.axiom#_lhKcab7uEe6laZimEYihUg" org.eventb.core.theorem="false"/>
        <org.eventb.core.scAxiom name="(" org.eventb.core.label="axm2;" org.eventb.core.predicate="target_smart_contract∈CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_c1.buc|org.eventb.core.contextFile#CCTx_Abstract_DLT_c1|org.eventb.core.axiom#_lhKcar7uEe6laZimEYihUg" org.eventb.core.theorem="false"/>
        <org.eventb.core.scAxiom name=")" org.eventb.core.label="axm3;" org.eventb.core.predicate="gateway∈GATEWAYS" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_c1.buc|org.eventb.core.contextFile#CCTx_Abstract_DLT_c1|org.eventb.core.axiom#_lhKca77uEe6laZimEYihUg" org.eventb.core.theorem="false"/>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
9 
        <org.eventb.core.scCarrierSet name="TARGET_TRANSACTIONS" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_c1.buc|org.eventb.core.contextFile#CCTx_Abstract_DLT_c1|org.eventb.core.carrierSet#_dldMwPReEe60CqkwWvstGA" org.eventb.core.type="ℙ(TARGET_TRANSACTIONS)"/>
Guzman Llambias's avatar
Add Ethereum -> Fabric animation (WIP)
Guzman Llambias committed
10 11 12 
        <org.eventb.core.scConstant name="source_smart_contract" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_c1.buc|org.eventb.core.contextFile#CCTx_Abstract_DLT_c1|org.eventb.core.constant#_lhTmML7uEe6laZimEYihUg" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
        <org.eventb.core.scConstant name="gateway" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_c1.buc|org.eventb.core.contextFile#CCTx_Abstract_DLT_c1|org.eventb.core.constant#_lhTmMr7uEe6laZimEYihUg" org.eventb.core.type="GATEWAYS"/>
        <org.eventb.core.scCarrierSet name="GATEWAYS" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_c1.buc|org.eventb.core.contextFile#CCTx_Abstract_DLT_c1|org.eventb.core.carrierSet#_lhTmM77uEe6laZimEYihUg" org.eventb.core.type="ℙ(GATEWAYS)"/>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
13 14 
        <org.eventb.core.scCarrierSet name="SOURCE_TRANSACTIONS" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_c1.buc|org.eventb.core.contextFile#CCTx_Abstract_DLT_c1|org.eventb.core.carrierSet#_XWUxAPReEe60CqkwWvstGA" org.eventb.core.type="ℙ(SOURCE_TRANSACTIONS)"/>
        <org.eventb.core.scCarrierSet name="SMART_CONTRACT_EVENTS" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_c1.buc|org.eventb.core.contextFile#CCTx_Abstract_DLT_c1|org.eventb.core.carrierSet#_H4R8YPRjEe60CqkwWvstGA" org.eventb.core.type="ℙ(SMART_CONTRACT_EVENTS)"/>
Guzman Llambias's avatar
Add Ethereum -> Fabric animation (WIP)
Guzman Llambias committed
15 16 17 18 19 
        <org.eventb.core.scConstant name="target_smart_contract" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_c1.buc|org.eventb.core.contextFile#CCTx_Abstract_DLT_c1|org.eventb.core.constant#_lhTmMb7uEe6laZimEYihUg" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
        <org.eventb.core.scCarrierSet name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_c1.buc|org.eventb.core.contextFile#CCTx_Abstract_DLT_c1|org.eventb.core.carrierSet#_lhTmNb7uEe6laZimEYihUg" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS)"/>
    </org.eventb.core.scInternalContext>
    <org.eventb.core.scInternalContext name="CCTx_Ethereum_Fabric_c2">
        <org.eventb.core.scExtendsContext name="'" org.eventb.core.scTarget="/gateway-event-b/CCTx_Abstract_DLT_c1.bcc|org.eventb.core.scContextFile#CCTx_Abstract_DLT_c1" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_c2.buc|org.eventb.core.contextFile#CCTx_Ethereum_Fabric_c2|org.eventb.core.extendsContext#'"/>
Guzman Llambias's avatar
Change trigger for emit event  
Guzman Llambias committed
20 21 
        <org.eventb.core.scAxiom name="CCTx_Abstract_DLT_c2" org.eventb.core.label="axm11" org.eventb.core.predicate="partition(PERMISSIONS,{read},{write})" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_c2.buc|org.eventb.core.contextFile#CCTx_Ethereum_Fabric_c2|org.eventb.core.axiom#_c2chsMQ6Ee609fto5wotHA" org.eventb.core.theorem="false"/>
        <org.eventb.core.scAxiom name="CCTx_Abstract_DLT_c3" org.eventb.core.label="axm12" org.eventb.core.predicate="gateway_user∈USERS" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_c2.buc|org.eventb.core.contextFile#CCTx_Ethereum_Fabric_c2|org.eventb.core.axiom#_c2dIwMQ6Ee609fto5wotHA" org.eventb.core.theorem="false"/>
Guzman Llambias's avatar
Add Ethereum -> Fabric animation (WIP)
Guzman Llambias committed
22 23 24 25 26 27 
        <org.eventb.core.scConstant name="write" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_c2.buc|org.eventb.core.contextFile#CCTx_Ethereum_Fabric_c2|org.eventb.core.constant#_olcso77uEe6laZimEYihUg" org.eventb.core.type="PERMISSIONS"/>
        <org.eventb.core.scCarrierSet name="USERS" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_c2.buc|org.eventb.core.contextFile#CCTx_Ethereum_Fabric_c2|org.eventb.core.carrierSet#_olcspr7uEe6laZimEYihUg" org.eventb.core.type="ℙ(USERS)"/>
        <org.eventb.core.scConstant name="read" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_c2.buc|org.eventb.core.contextFile#CCTx_Ethereum_Fabric_c2|org.eventb.core.constant#_olcsor7uEe6laZimEYihUg" org.eventb.core.type="PERMISSIONS"/>
        <org.eventb.core.scCarrierSet name="PERMISSIONS" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_c2.buc|org.eventb.core.contextFile#CCTx_Ethereum_Fabric_c2|org.eventb.core.carrierSet#_olcspb7uEe6laZimEYihUg" org.eventb.core.type="ℙ(PERMISSIONS)"/>
        <org.eventb.core.scConstant name="gateway_user" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_c2.buc|org.eventb.core.contextFile#CCTx_Ethereum_Fabric_c2|org.eventb.core.constant#_olcspL7uEe6laZimEYihUg" org.eventb.core.type="USERS"/>
    </org.eventb.core.scInternalContext>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
28 29 
    <org.eventb.core.scInvariant name="CCTx_Abstract_DLT_c2" org.eventb.core.label="inv1" org.eventb.core.predicate="received_source_transactions∈CROSS_CHAIN_SMART_CONTRACTS ↔ SOURCE_TRANSACTIONS" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.invariant#_zpKWcMQ4Ee609fto5wotHA" org.eventb.core.theorem="false"/>
    <org.eventb.core.scInvariant name="CCTx_Abstract_DLT_c3" org.eventb.core.label="inv2" org.eventb.core.predicate="emitted_events∈CROSS_CHAIN_SMART_CONTRACTS ↔ SMART_CONTRACT_EVENTS" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.invariant#_zpKWccQ4Ee609fto5wotHA" org.eventb.core.theorem="false"/>
Guzman Llambias's avatar
Change trigger for emit event  
Guzman Llambias committed
30 
    <org.eventb.core.scInvariant name="CCTx_Abstract_DLT_c4" org.eventb.core.label="inv3" org.eventb.core.predicate="subscriptions∈GATEWAYS ↔ CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.invariant#_zpK9gMQ4Ee609fto5wotHA" org.eventb.core.theorem="false"/>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
31 32 
    <org.eventb.core.scInvariant name="CCTx_Abstract_DLT_c5" org.eventb.core.label="inv4" org.eventb.core.predicate="gateway_pending_events∈GATEWAYS ↔ TARGET_TRANSACTIONS" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.invariant#_zpK9gcQ4Ee609fto5wotHA" org.eventb.core.theorem="false"/>
    <org.eventb.core.scInvariant name="CCTx_Abstract_DLT_c6" org.eventb.core.label="inv5" org.eventb.core.predicate="received_target_transactions∈CROSS_CHAIN_SMART_CONTRACTS ↔ TARGET_TRANSACTIONS" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.invariant#_qTKs0MT7Ee609fto5wotHA" org.eventb.core.theorem="false"/>
Guzman Llambias's avatar
Add Ethereum -> Fabric animation (WIP)
Guzman Llambias committed
33 
    <org.eventb.core.scInvariant name="CCTx_Ethereum_Fabric_c3" org.eventb.core.label="inv11" org.eventb.core.predicate="authenticated_users⊆USERS" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.invariant#_jV9TIsEWEe6yC4BToIaAqA" org.eventb.core.theorem="false"/>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
34 35 
    <org.eventb.core.scInvariant name="CCTx_Ethereum_Fabric_c4" org.eventb.core.label="inv12" org.eventb.core.predicate="authenticated_transactions∈received_target_transactions → authenticated_users" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.invariant#_jV9TI8EWEe6yC4BToIaAqA" org.eventb.core.theorem="false"/>
    <org.eventb.core.scInvariant name="CCTx_Ethereum_Fabric_c5" org.eventb.core.label="inv13" org.eventb.core.predicate="∀tx⦂CROSS_CHAIN_SMART_CONTRACTS×TARGET_TRANSACTIONS·tx∈received_target_transactions⇒(∃u⦂USERS·u∈authenticated_users∧tx ↦ u∈authenticated_transactions)" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.invariant#_jV9TJMEWEe6yC4BToIaAqA" org.eventb.core.theorem="false"/>
Guzman Llambias's avatar
Complete Ethereum -> Fabric animation  
Guzman Llambias committed
36 
    <org.eventb.core.scInvariant name="CCTx_Ethereum_Fabric_c6" org.eventb.core.label="inv14" org.eventb.core.predicate="grants∈authenticated_users ↔ PERMISSIONS" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.invariant#_OTstIMHNEe609fto5wotHA" org.eventb.core.theorem="false"/>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
37 
    <org.eventb.core.scInvariant name="CCTx_Ethereum_Fabric_c7" org.eventb.core.label="inv15" org.eventb.core.predicate="∀u⦂USERS·u∈authenticated_transactions[received_target_transactions]⇒u ↦ write∈grants" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.invariant#_jCLrMcHJEe6yC4BToIaAqA" org.eventb.core.theorem="false"/>
Guzman Llambias's avatar
Complete Ethereum -> Fabric animation  
Guzman Llambias committed
38 39 
    <org.eventb.core.scInvariant name="CCTx_Ethereum_Fabric_c8" org.eventb.core.label="inv11" org.eventb.core.predicate="subscribed∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_DmAl8MHOEe609fto5wotHA" org.eventb.core.theorem="false"/>
    <org.eventb.core.scInvariant name="CCTx_Ethereum_Fabric_c9" org.eventb.core.label="inv12" org.eventb.core.predicate="initiated∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_DmB0EMHOEe609fto5wotHA" org.eventb.core.theorem="false"/>
Guzman Llambias's avatar
Change trigger for emit event  
Guzman Llambias committed
40 
    <org.eventb.core.scInvariant name="CCTx_Ethereum_Fabric_c:" org.eventb.core.label="inv13" org.eventb.core.predicate="emitted∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_DmCbIMHOEe609fto5wotHA" org.eventb.core.theorem="false"/>
Guzman Llambias's avatar
Complete Ethereum -> Fabric animation  
Guzman Llambias committed
41 42 43 44 45 46 
    <org.eventb.core.scInvariant name="CCTx_Ethereum_Fabric_c;" org.eventb.core.label="inv14" org.eventb.core.predicate="gateway_processing∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_DmDCMMHOEe609fto5wotHA" org.eventb.core.theorem="false"/>
    <org.eventb.core.scInvariant name="CCTx_Ethereum_Fabric_c=" org.eventb.core.label="inv15" org.eventb.core.predicate="submit_cc_tx∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_DmDpQMHOEe609fto5wotHA" org.eventb.core.theorem="false"/>
    <org.eventb.core.scInvariant name="CCTx_Ethereum_Fabric_c&gt;" org.eventb.core.label="inv16" org.eventb.core.predicate="user_created∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_DmEQUMHOEe609fto5wotHA" org.eventb.core.theorem="false"/>
    <org.eventb.core.scInvariant name="CCTx_Ethereum_Fabric_c?" org.eventb.core.label="inv17" org.eventb.core.predicate="write_granted∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_2MNd0MHOEe609fto5wotHA" org.eventb.core.theorem="false"/>
    <org.eventb.core.scVariable name="gateway_processing" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.variable#_DmMMIsHOEe609fto5wotHA" org.eventb.core.type="ℤ"/>
    <org.eventb.core.scVariable name="initiated" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.variable#_DmMMIMHOEe609fto5wotHA" org.eventb.core.type="ℤ"/>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
47 
    <org.eventb.core.scVariable name="received_target_transactions" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.variable#_SS0wAvRgEe60CqkwWvstGA" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×TARGET_TRANSACTIONS)"/>
Guzman Llambias's avatar
Complete Ethereum -> Fabric animation  
Guzman Llambias committed
48 49 
    <org.eventb.core.scVariable name="submit_cc_tx" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.variable#_DmMMI8HOEe609fto5wotHA" org.eventb.core.type="ℤ"/>
    <org.eventb.core.scVariable name="subscribed" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.variable#_DmLlEMHOEe609fto5wotHA" org.eventb.core.type="ℤ"/>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
50 51 
    <org.eventb.core.scVariable name="gateway_pending_events" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.variable#_SS0wAfRgEe60CqkwWvstGA" org.eventb.core.type="ℙ(GATEWAYS×TARGET_TRANSACTIONS)"/>
    <org.eventb.core.scVariable name="authenticated_transactions" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.variable#_1toq4b7uEe6laZimEYihUg" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×TARGET_TRANSACTIONS×USERS)"/>
Guzman Llambias's avatar
Add Ethereum -> Fabric animation (WIP)
Guzman Llambias committed
52 
    <org.eventb.core.scVariable name="subscriptions" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.variable#_yREda77uEe6laZimEYihUg" org.eventb.core.type="ℙ(GATEWAYS×CROSS_CHAIN_SMART_CONTRACTS)"/>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
53 
    <org.eventb.core.scVariable name="emitted_events" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.variable#_YjCFYPKVEe60CqkwWvstGA" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×SMART_CONTRACT_EVENTS)"/>
Guzman Llambias's avatar
Complete Ethereum -> Fabric animation  
Guzman Llambias committed
54 55 
    <org.eventb.core.scVariable name="grants" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.variable#_2RlqIMErEe6yC4BToIaAqA" org.eventb.core.type="ℙ(USERS×PERMISSIONS)"/>
    <org.eventb.core.scVariable name="write_granted" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.variable#_2MPTAMHOEe609fto5wotHA" org.eventb.core.type="ℤ"/>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
56 
    <org.eventb.core.scVariable name="received_source_transactions" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.variable#_SS0wAPRgEe60CqkwWvstGA" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×SOURCE_TRANSACTIONS)"/>
Guzman Llambias's avatar
Change trigger for emit event  
Guzman Llambias committed
57 
    <org.eventb.core.scVariable name="emitted" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.variable#_Wik0EPKWEe60CqkwWvstGA" org.eventb.core.type="ℤ"/>
Guzman Llambias's avatar
Complete Ethereum -> Fabric animation  
Guzman Llambias committed
58 
    <org.eventb.core.scVariable name="user_created" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.variable#_DmMMJMHOEe609fto5wotHA" org.eventb.core.type="ℤ"/>
Guzman Llambias's avatar
Add Ethereum -> Fabric animation (WIP)
Guzman Llambias committed
59 
    <org.eventb.core.scVariable name="authenticated_users" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.variable#_1toq4L7uEe6laZimEYihUg" org.eventb.core.type="ℙ(USERS)"/>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
60 61 62 63 
    <org.eventb.core.scEvent name="received_target_transactiont" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="INITIALISATION" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh">
        <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bcm|org.eventb.core.scMachineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.scEvent#received_target_transactiont" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh"/>
        <org.eventb.core.scAction name="'" org.eventb.core.assignment="received_source_transactions ≔ ∅ ⦂ ℙ(CROSS_CHAIN_SMART_CONTRACTS×SOURCE_TRANSACTIONS)" org.eventb.core.label="act1" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#'|org.eventb.core.action#_zpBMgMQ4Ee609fto5wotHA"/>
        <org.eventb.core.scAction name="(" org.eventb.core.assignment="emitted_events ≔ ∅ ⦂ ℙ(CROSS_CHAIN_SMART_CONTRACTS×SMART_CONTRACT_EVENTS)" org.eventb.core.label="act2" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#'|org.eventb.core.action#_zpBzkMQ4Ee609fto5wotHA"/>
Guzman Llambias's avatar
Change trigger for emit event  
Guzman Llambias committed
64 
        <org.eventb.core.scAction name=")" org.eventb.core.assignment="subscriptions ≔ ∅ ⦂ ℙ(GATEWAYS×CROSS_CHAIN_SMART_CONTRACTS)" org.eventb.core.label="act3" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#'|org.eventb.core.action#_zpBzkcQ4Ee609fto5wotHA"/>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
65 66 
        <org.eventb.core.scAction name="*" org.eventb.core.assignment="gateway_pending_events ≔ ∅ ⦂ ℙ(GATEWAYS×TARGET_TRANSACTIONS)" org.eventb.core.label="act4" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#'|org.eventb.core.action#_zpBzksQ4Ee609fto5wotHA"/>
        <org.eventb.core.scAction name="+" org.eventb.core.assignment="received_target_transactions ≔ ∅ ⦂ ℙ(CROSS_CHAIN_SMART_CONTRACTS×TARGET_TRANSACTIONS)" org.eventb.core.label="act6" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#'|org.eventb.core.action#_zpCaoMQ4Ee609fto5wotHA"/>
Guzman Llambias's avatar
Add Ethereum -> Fabric animation (WIP)
Guzman Llambias committed
67 
        <org.eventb.core.scAction name="," org.eventb.core.assignment="authenticated_users ≔ ∅ ⦂ ℙ(USERS)" org.eventb.core.label="act11" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh|org.eventb.core.action#_jV8FAMEWEe6yC4BToIaAqA"/>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
68 
        <org.eventb.core.scAction name="-" org.eventb.core.assignment="authenticated_transactions ≔ ∅ ⦂ ℙ(CROSS_CHAIN_SMART_CONTRACTS×TARGET_TRANSACTIONS×USERS)" org.eventb.core.label="act12" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh|org.eventb.core.action#_jV8FAcEWEe6yC4BToIaAqA"/>
Guzman Llambias's avatar
Complete Ethereum -> Fabric animation  
Guzman Llambias committed
69 70 71 
        <org.eventb.core.scAction name="." org.eventb.core.assignment="grants ≔ ∅ ⦂ ℙ(USERS×PERMISSIONS)" org.eventb.core.label="act14" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh|org.eventb.core.action#_0oC5cMErEe6yC4BToIaAqA"/>
        <org.eventb.core.scAction name="/" org.eventb.core.assignment="subscribed ≔ 0" org.eventb.core.label="act31" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh|org.eventb.core.action#_FVN5wMHOEe609fto5wotHA"/>
        <org.eventb.core.scAction name="0" org.eventb.core.assignment="initiated ≔ 0" org.eventb.core.label="act32" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh|org.eventb.core.action#_FVN5wcHOEe609fto5wotHA"/>
Guzman Llambias's avatar
Change trigger for emit event  
Guzman Llambias committed
72 
        <org.eventb.core.scAction name="1" org.eventb.core.assignment="emitted ≔ 0" org.eventb.core.label="act33" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh|org.eventb.core.action#_FVOg0MHOEe609fto5wotHA"/>
Guzman Llambias's avatar
Complete Ethereum -> Fabric animation  
Guzman Llambias committed
73 74 75 76 
        <org.eventb.core.scAction name="2" org.eventb.core.assignment="gateway_processing ≔ 0" org.eventb.core.label="act34" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh|org.eventb.core.action#_FVOg0cHOEe609fto5wotHA"/>
        <org.eventb.core.scAction name="3" org.eventb.core.assignment="submit_cc_tx ≔ 0" org.eventb.core.label="act35" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh|org.eventb.core.action#_FVPH4MHOEe609fto5wotHA"/>
        <org.eventb.core.scAction name="4" org.eventb.core.assignment="user_created ≔ 0" org.eventb.core.label="act36" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh|org.eventb.core.action#_FVPH4cHOEe609fto5wotHA"/>
        <org.eventb.core.scAction name="5" org.eventb.core.assignment="write_granted ≔ 0" org.eventb.core.label="act37" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh|org.eventb.core.action#_4VMjkMHOEe609fto5wotHA"/>
Guzman Llambias's avatar
Add Ethereum -> Fabric animation (WIP)
Guzman Llambias committed
77 
    </org.eventb.core.scEvent>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
78 79 
    <org.eventb.core.scEvent name="received_target_transactionu" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="SUBSCRIBE_SMART_CONTRACT_EVENTS_IN_ETHEREUM" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUi">
        <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bcm|org.eventb.core.scMachineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.scEvent#received_target_transactionu" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUi|org.eventb.core.refinesEvent#'"/>
Guzman Llambias's avatar
Change trigger for emit event  
Guzman Llambias committed
80 81 
        <org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="gateway ↦ source_smart_contract∉subscriptions" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_yQ9vtr7uEe6laZimEYihUg|org.eventb.core.guard#_zpDBscQ4Ee609fto5wotHA" org.eventb.core.theorem="false"/>
        <org.eventb.core.scAction name="(" org.eventb.core.assignment="subscriptions ≔ subscriptions∪{gateway ↦ source_smart_contract}" org.eventb.core.label="act1" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_yQ9vtr7uEe6laZimEYihUg|org.eventb.core.action#_zpDBsMQ4Ee609fto5wotHA"/>
Guzman Llambias's avatar
Complete Ethereum -> Fabric animation  
Guzman Llambias committed
82 
        <org.eventb.core.scAction name=")" org.eventb.core.assignment="subscribed ≔ 1" org.eventb.core.label="act31" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUi|org.eventb.core.action#_G4NWgMHOEe609fto5wotHA"/>
Guzman Llambias's avatar
Add Ethereum -> Fabric animation (WIP)
Guzman Llambias committed
83 
    </org.eventb.core.scEvent>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
84 85 86 87 88 89 90 91 
    <org.eventb.core.scEvent name="received_target_transactionv" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="INITIATE_CC_TX_IN_ETHEREUM" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_x24-QPRhEe60CqkwWvstGA">
        <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bcm|org.eventb.core.scMachineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.scEvent#received_target_transactionv" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_x24-QPRhEe60CqkwWvstGA|org.eventb.core.refinesEvent#_x24-QfRhEe60CqkwWvstGA"/>
        <org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="transaction∈SOURCE_TRANSACTIONS" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_y397cMBFEe6yC4BToIaAqA|org.eventb.core.guard#_zpDowcQ4Ee609fto5wotHA" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="(" org.eventb.core.label="grd3" org.eventb.core.predicate="transaction∉received_source_transactions[{source_smart_contract}]" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_y397cMBFEe6yC4BToIaAqA|org.eventb.core.guard#_zpEP0MQ4Ee609fto5wotHA" org.eventb.core.theorem="false"/>
        <org.eventb.core.scAction name="transactioo" org.eventb.core.assignment="received_source_transactions ≔ received_source_transactions∪{source_smart_contract ↦ transaction}" org.eventb.core.label="act1" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_y397cMBFEe6yC4BToIaAqA|org.eventb.core.action#_zpDowMQ4Ee609fto5wotHA"/>
        <org.eventb.core.scParameter name="transaction" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_y397cMBFEe6yC4BToIaAqA|org.eventb.core.parameter#_yQ9vvb7uEe6laZimEYihUg" org.eventb.core.type="SOURCE_TRANSACTIONS"/>
        <org.eventb.core.scAction name="transactiop" org.eventb.core.assignment="initiated ≔ 1" org.eventb.core.label="act31" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_x24-QPRhEe60CqkwWvstGA|org.eventb.core.action#_I7eOwMHOEe609fto5wotHA"/>
        <org.eventb.core.scAction name="transactioq" org.eventb.core.assignment="submit_cc_tx ≔ 0" org.eventb.core.label="act32" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_x24-QPRhEe60CqkwWvstGA|org.eventb.core.action#_I7eOwcHOEe609fto5wotHA"/>
Guzman Llambias's avatar
Add Ethereum -> Fabric animation (WIP)
Guzman Llambias committed
92 
    </org.eventb.core.scEvent>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
93 94 95 96 97 98 99 100 101 102 103 
    <org.eventb.core.scEvent name="received_target_transactionw" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="EMIT_EVENT_IN_ETHEREUM" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_vbddoPRhEe60CqkwWvstGA">
        <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bcm|org.eventb.core.scMachineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.scEvent#received_target_transactionw" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_vbddoPRhEe60CqkwWvstGA|org.eventb.core.refinesEvent#_vbddofRhEe60CqkwWvstGA"/>
        <org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="source_smart_contract ↦ transaction∈received_source_transactions" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_WGbIAPRhEe60CqkwWvstGA|org.eventb.core.guard#_zpFd8cQ4Ee609fto5wotHA" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="emitted_event∉emitted_events[{source_smart_contract}]" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_WGbIAPRhEe60CqkwWvstGA|org.eventb.core.guard#_zpGFAMQ4Ee609fto5wotHA" org.eventb.core.theorem="false"/>
        <org.eventb.core.scAction name="emitted_evenu" org.eventb.core.assignment="emitted_events ≔ emitted_events∪{source_smart_contract ↦ emitted_event}" org.eventb.core.label="act1" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_WGbIAPRhEe60CqkwWvstGA|org.eventb.core.action#_zpE24MQ4Ee609fto5wotHA"/>
        <org.eventb.core.scAction name="emitted_evenv" org.eventb.core.assignment="received_source_transactions ≔ received_source_transactions ∖ {source_smart_contract ↦ transaction}" org.eventb.core.label="act2" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_WGbIAPRhEe60CqkwWvstGA|org.eventb.core.action#_zpFd8MQ4Ee609fto5wotHA"/>
        <org.eventb.core.scParameter name="emitted_event" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_WGbIAPRhEe60CqkwWvstGA|org.eventb.core.parameter#_RRvi8PRfEe60CqkwWvstGA" org.eventb.core.type="SMART_CONTRACT_EVENTS"/>
        <org.eventb.core.scParameter name="transaction" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_WGbIAPRhEe60CqkwWvstGA|org.eventb.core.parameter#_yQ9vw77uEe6laZimEYihUg" org.eventb.core.type="SOURCE_TRANSACTIONS"/>
        <org.eventb.core.scAction name="emitted_evenw" org.eventb.core.assignment="emitted ≔ 1" org.eventb.core.label="act31" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_vbddoPRhEe60CqkwWvstGA|org.eventb.core.action#_LjZ6UMHOEe609fto5wotHA"/>
        <org.eventb.core.scAction name="emitted_evenx" org.eventb.core.assignment="initiated ≔ 0" org.eventb.core.label="act32" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_vbddoPRhEe60CqkwWvstGA|org.eventb.core.action#_LjZ6UcHOEe609fto5wotHA"/>
        <org.eventb.core.scAction name="emitted_eveny" org.eventb.core.assignment="submit_cc_tx ≔ 0" org.eventb.core.label="act33" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_vbddoPRhEe60CqkwWvstGA|org.eventb.core.action#_LjahYMHOEe609fto5wotHA"/>
Guzman Llambias's avatar
Add Ethereum -> Fabric animation (WIP)
Guzman Llambias committed
104 
    </org.eventb.core.scEvent>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
105 106 107 108 109 110 111 112 113 114 115 116 
    <org.eventb.core.scEvent name="received_target_transactionx" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="LISTEN_EVENT_IN_ETHEREUM" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_vbddovRhEe60CqkwWvstGA">
        <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bcm|org.eventb.core.scMachineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.scEvent#received_target_transactionx" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_vbddovRhEe60CqkwWvstGA|org.eventb.core.refinesEvent#_vbeEsPRhEe60CqkwWvstGA"/>
        <org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="source_smart_contract ↦ emitted_event∈emitted_events" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_WGbvEPRhEe60CqkwWvstGA|org.eventb.core.guard#_zpHTIcQ4Ee609fto5wotHA" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="gateway ↦ source_smart_contract∈subscriptions" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_WGbvEPRhEe60CqkwWvstGA|org.eventb.core.guard#_zpH6MMQ4Ee609fto5wotHA" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name=")" org.eventb.core.label="grd3" org.eventb.core.predicate="gateway ↦ pending_event∉gateway_pending_events" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_WGbvEPRhEe60CqkwWvstGA|org.eventb.core.guard#_zpH6McQ4Ee609fto5wotHA" org.eventb.core.theorem="false"/>
        <org.eventb.core.scAction name="pending_evenu" org.eventb.core.assignment="gateway_pending_events ≔ gateway_pending_events∪{gateway ↦ pending_event}" org.eventb.core.label="act1" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_WGbvEPRhEe60CqkwWvstGA|org.eventb.core.action#_zpGsEMQ4Ee609fto5wotHA"/>
        <org.eventb.core.scAction name="pending_evenv" org.eventb.core.assignment="emitted_events ≔ emitted_events ∖ {source_smart_contract ↦ emitted_event}" org.eventb.core.label="act2" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_WGbvEPRhEe60CqkwWvstGA|org.eventb.core.action#_zpHTIMQ4Ee609fto5wotHA"/>
        <org.eventb.core.scParameter name="pending_event" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_WGbvEPRhEe60CqkwWvstGA|org.eventb.core.parameter#_rW2qoPRfEe60CqkwWvstGA" org.eventb.core.type="TARGET_TRANSACTIONS"/>
        <org.eventb.core.scParameter name="emitted_event" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_WGbvEPRhEe60CqkwWvstGA|org.eventb.core.parameter#_WbZkYPRfEe60CqkwWvstGA" org.eventb.core.type="SMART_CONTRACT_EVENTS"/>
        <org.eventb.core.scAction name="pending_evenw" org.eventb.core.assignment="gateway_processing ≔ 1" org.eventb.core.label="act31" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_vbddovRhEe60CqkwWvstGA|org.eventb.core.action#_NY1x8MHOEe609fto5wotHA"/>
        <org.eventb.core.scAction name="pending_evenx" org.eventb.core.assignment="emitted ≔ 0" org.eventb.core.label="act32" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_vbddovRhEe60CqkwWvstGA|org.eventb.core.action#_NY1x8cHOEe609fto5wotHA"/>
        <org.eventb.core.scAction name="pending_eveny" org.eventb.core.assignment="submit_cc_tx ≔ 0" org.eventb.core.label="act33" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_vbddovRhEe60CqkwWvstGA|org.eventb.core.action#_NY1x8sHOEe609fto5wotHA"/>
Guzman Llambias's avatar
Add Ethereum -> Fabric animation (WIP)
Guzman Llambias committed
117 
    </org.eventb.core.scEvent>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
118 119 120 121 122 123 124 125 126 127 128 129 130 131 
    <org.eventb.core.scEvent name="received_target_transactiony" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="SUBMIT_TX_TO_FABRIC" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_vbeEsfRhEe60CqkwWvstGA">
        <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bcm|org.eventb.core.scMachineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.scEvent#received_target_transactiony" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_vbeEsfRhEe60CqkwWvstGA|org.eventb.core.refinesEvent#_vbeEsvRhEe60CqkwWvstGA"/>
        <org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="gateway ↦ pending_event∈gateway_pending_events" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_WGc9MPRhEe60CqkwWvstGA|org.eventb.core.guard#_zpJvYcQ4Ee609fto5wotHA" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="transaction∈TARGET_TRANSACTIONS" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_WGc9MPRhEe60CqkwWvstGA|org.eventb.core.guard#_L7ASUPRgEe60CqkwWvstGA" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="pending_evenw" org.eventb.core.label="grd11" org.eventb.core.predicate="user∈authenticated_users" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_eB-pVPRhEe60CqkwWvstGA|org.eventb.core.guard#_jV8sEcEWEe6yC4BToIaAqA" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="pending_evenx" org.eventb.core.label="grd12" org.eventb.core.predicate="user ↦ write∈grants" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_eB-pVPRhEe60CqkwWvstGA|org.eventb.core.guard#_jV8sEsEWEe6yC4BToIaAqA" org.eventb.core.theorem="false"/>
        <org.eventb.core.scAction name="pending_evenu" org.eventb.core.assignment="received_target_transactions ≔ received_target_transactions∪{target_smart_contract ↦ transaction}" org.eventb.core.label="act1" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_WGc9MPRhEe60CqkwWvstGA|org.eventb.core.action#_zpJIUMQ4Ee609fto5wotHA"/>
        <org.eventb.core.scAction name="pending_evenv" org.eventb.core.assignment="gateway_pending_events ≔ gateway_pending_events ∖ {gateway ↦ pending_event}" org.eventb.core.label="act2" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_WGc9MPRhEe60CqkwWvstGA|org.eventb.core.action#_zpJvYMQ4Ee609fto5wotHA"/>
        <org.eventb.core.scAction name="pending_eveny" org.eventb.core.assignment="authenticated_transactions ≔ authenticated_transactions{target_smart_contract ↦ transaction ↦ user}" org.eventb.core.label="act11" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_eB-pVPRhEe60CqkwWvstGA|org.eventb.core.action#_jV8sEMEWEe6yC4BToIaAqA"/>
        <org.eventb.core.scParameter name="pending_event" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_WGc9MPRhEe60CqkwWvstGA|org.eventb.core.parameter#_rW3RsPRfEe60CqkwWvstGA" org.eventb.core.type="TARGET_TRANSACTIONS"/>
        <org.eventb.core.scParameter name="transaction" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_WGc9MPRhEe60CqkwWvstGA|org.eventb.core.parameter#_AlhAwPRgEe60CqkwWvstGA" org.eventb.core.type="TARGET_TRANSACTIONS"/>
        <org.eventb.core.scParameter name="user" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_eB-pVPRhEe60CqkwWvstGA|org.eventb.core.parameter#_1tncwL7uEe6laZimEYihUg" org.eventb.core.type="USERS"/>
        <org.eventb.core.scAction name="pending_evenz" org.eventb.core.assignment="submit_cc_tx ≔ 1" org.eventb.core.label="act31" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_vbeEsfRhEe60CqkwWvstGA|org.eventb.core.action#_RH42kMHOEe609fto5wotHA"/>
        <org.eventb.core.scAction name="pending_even{" org.eventb.core.assignment="gateway_processing ≔ 0" org.eventb.core.label="act32" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_vbeEsfRhEe60CqkwWvstGA|org.eventb.core.action#_RH5doMHOEe609fto5wotHA"/>
Guzman Llambias's avatar
Add Ethereum -> Fabric animation (WIP)
Guzman Llambias committed
132 
    </org.eventb.core.scEvent>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
133 134 
    <org.eventb.core.scEvent name="received_target_transactionz" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="CREATE_GATEWAY_USER" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUn">
        <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bcm|org.eventb.core.scMachineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.scEvent#received_target_transactionz" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUn|org.eventb.core.refinesEvent#'"/>
Guzman Llambias's avatar
Add Ethereum -> Fabric animation (WIP)
Guzman Llambias committed
135 136 
        <org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="gateway_user∉authenticated_users" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_K_21gMEXEe6yC4BToIaAqA|org.eventb.core.guard#_y4y5cMEXEe6yC4BToIaAqA" org.eventb.core.theorem="false"/>
        <org.eventb.core.scAction name="(" org.eventb.core.assignment="authenticated_users ≔ authenticated_users∪{gateway_user}" org.eventb.core.label="act1" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_K_21gMEXEe6yC4BToIaAqA|org.eventb.core.action#_jV9TIcEWEe6yC4BToIaAqA"/>
Guzman Llambias's avatar
Complete Ethereum -> Fabric animation  
Guzman Llambias committed
137 138 
        <org.eventb.core.scAction name=")" org.eventb.core.assignment="user_created ≔ 1" org.eventb.core.label="act31" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUn|org.eventb.core.action#_RH5docHOEe609fto5wotHA"/>
    </org.eventb.core.scEvent>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
139 140 
    <org.eventb.core.scEvent name="received_target_transaction{" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="GRANT_PERMISSION" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUo">
        <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bcm|org.eventb.core.scMachineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.scEvent#received_target_transaction{" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUo|org.eventb.core.refinesEvent#'"/>
Guzman Llambias's avatar
Complete Ethereum -> Fabric animation  
Guzman Llambias committed
141 142 143 144 145 146 147 148 149 
        <org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="permission∈PERMISSIONS" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_KHHS0MEbEe6yC4BToIaAqA|org.eventb.core.guard#_KHH54cEbEe6yC4BToIaAqA" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="user∈authenticated_users" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_KHHS0MEbEe6yC4BToIaAqA|org.eventb.core.guard#_KHH54sEbEe6yC4BToIaAqA" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name=")" org.eventb.core.label="grd3" org.eventb.core.predicate="user ↦ permission∉grants" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_KHHS0MEbEe6yC4BToIaAqA|org.eventb.core.guard#_5yZW0MHNEe609fto5wotHA" org.eventb.core.theorem="false"/>
        <org.eventb.core.scAction name="permissioo" org.eventb.core.assignment="grants ≔ grants∪{user ↦ permission}" org.eventb.core.label="act1" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_KHHS0MEbEe6yC4BToIaAqA|org.eventb.core.action#_KHH54MEbEe6yC4BToIaAqA"/>
        <org.eventb.core.scParameter name="permission" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_KHHS0MEbEe6yC4BToIaAqA|org.eventb.core.parameter#_KHIg8MEbEe6yC4BToIaAqA" org.eventb.core.type="PERMISSIONS"/>
        <org.eventb.core.scParameter name="user" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_KHHS0MEbEe6yC4BToIaAqA|org.eventb.core.parameter#_KHIg8cEbEe6yC4BToIaAqA" org.eventb.core.type="USERS"/>
        <org.eventb.core.scGuard name="permissiop" org.eventb.core.label="grd31" org.eventb.core.predicate="user=gateway_user" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUo|org.eventb.core.guard#_yeWE8cHOEe609fto5wotHA" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="permissioq" org.eventb.core.label="grd32" org.eventb.core.predicate="permission=write" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUo|org.eventb.core.guard#_-iJ1EMHOEe609fto5wotHA" org.eventb.core.theorem="false"/>
        <org.eventb.core.scAction name="permissior" org.eventb.core.assignment="write_granted ≔ 1" org.eventb.core.label="act31" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUo|org.eventb.core.action#_yeWE8MHOEe609fto5wotHA"/>
Guzman Llambias's avatar
Add Ethereum -> Fabric animation (WIP)
Guzman Llambias committed
150 151 
    </org.eventb.core.scEvent>
</org.eventb.core.scMachineFile>