Skip to content
Snippets Groups Projects
Normal view Permalink
CCTx_Fabric_Ethereum_Animation_m3.bcm 50.8 KiB
Newer Older
Guzman Llambias's avatar
Add Fabric -> Ethereum animation
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_Fabric_Ethereum_m2.bcm" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.refinesMachine#'"/>
    <org.eventb.core.scSeesContext name="(" org.eventb.core.scTarget="/gateway-event-b/CCTx_Fabric_Ethereum_c2.bcc" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.seesContext#_8rq0TL7uEe6laZimEYihUg"/>
    <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 Fabric -> Ethereum animation
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 Fabric -> Ethereum animation
Guzman Llambias committed
15 16 17 18 19 20 21 22 23 
        <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_Fabric_Ethereum_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_Fabric_Ethereum_c2.buc|org.eventb.core.contextFile#CCTx_Fabric_Ethereum_c2|org.eventb.core.extendsContext#'"/>
        <org.eventb.core.scAxiom name="CCTx_Abstract_DLT_c2" org.eventb.core.label="axm11;" org.eventb.core.predicate="gateway_address∈ADDRESS" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_c2.buc|org.eventb.core.contextFile#CCTx_Fabric_Ethereum_c2|org.eventb.core.axiom#_seJcgL7uEe6laZimEYihUg" org.eventb.core.theorem="false"/>
        <org.eventb.core.scCarrierSet name="ADDRESS" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_c2.buc|org.eventb.core.contextFile#CCTx_Fabric_Ethereum_c2|org.eventb.core.carrierSet#_seJchL7uEe6laZimEYihUg" org.eventb.core.type="ℙ(ADDRESS)"/>
        <org.eventb.core.scConstant name="gateway_address" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_c2.buc|org.eventb.core.contextFile#CCTx_Fabric_Ethereum_c2|org.eventb.core.constant#_seJcgr7uEe6laZimEYihUg" org.eventb.core.type="ADDRESS"/>
    </org.eventb.core.scInternalContext>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
24 25 
    <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
26 
    <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
27 28 
    <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 Fabric -> Ethereum animation
Guzman Llambias committed
29 30 31 
    <org.eventb.core.scInvariant name="CCTx_Fabric_Ethereum_c3" org.eventb.core.label="inv11" org.eventb.core.predicate="accounts∈ADDRESS ⇸ ℕ" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_m2|org.eventb.core.invariant#_XvjdQMEBEe6yC4BToIaAqA" org.eventb.core.theorem="false"/>
    <org.eventb.core.scInvariant name="CCTx_Fabric_Ethereum_c4" org.eventb.core.label="inv31" org.eventb.core.predicate="subscribed∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.invariant#_qWNdEMEGEe6yC4BToIaAqA" org.eventb.core.theorem="false"/>
    <org.eventb.core.scInvariant name="CCTx_Fabric_Ethereum_c5" org.eventb.core.label="inv32" org.eventb.core.predicate="initiated∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.invariant#_qWNdEcEGEe6yC4BToIaAqA" org.eventb.core.theorem="false"/>
Guzman Llambias's avatar
Change trigger for emit event  
Guzman Llambias committed
32 
    <org.eventb.core.scInvariant name="CCTx_Fabric_Ethereum_c6" org.eventb.core.label="inv33" org.eventb.core.predicate="emitted∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.invariant#_qWNdEsEGEe6yC4BToIaAqA" org.eventb.core.theorem="false"/>
Guzman Llambias's avatar
Add Fabric -> Ethereum animation
Guzman Llambias committed
33 34 35 36 37 38 39 
    <org.eventb.core.scInvariant name="CCTx_Fabric_Ethereum_c7" org.eventb.core.label="inv34" org.eventb.core.predicate="gateway_processing∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.invariant#_qWNdE8EGEe6yC4BToIaAqA" org.eventb.core.theorem="false"/>
    <org.eventb.core.scInvariant name="CCTx_Fabric_Ethereum_c8" org.eventb.core.label="inv35" org.eventb.core.predicate="submit_cc_tx∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.invariant#_qWNdFMEGEe6yC4BToIaAqA" org.eventb.core.theorem="false"/>
    <org.eventb.core.scInvariant name="CCTx_Fabric_Ethereum_c9" org.eventb.core.label="inv36" org.eventb.core.predicate="wallet_created∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.invariant#_qWOEIMEGEe6yC4BToIaAqA" org.eventb.core.theorem="false"/>
    <org.eventb.core.scInvariant name="CCTx_Fabric_Ethereum_c:" org.eventb.core.label="inv37" org.eventb.core.predicate="wallet_amount∈ℕ" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.invariant#_9cXZIMEHEe6yC4BToIaAqA" 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_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.variable#_LY1Q0cEEEe6yC4BToIaAqA" org.eventb.core.type="ℤ"/>
    <org.eventb.core.scVariable name="wallet_amount" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.variable#_9cZOUMEHEe6yC4BToIaAqA" 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_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.variable#_LY0pwcEEEe6yC4BToIaAqA" org.eventb.core.type="ℤ"/>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
40 
    <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_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.variable#_2ZLTIvRgEe60CqkwWvstGA" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×TARGET_TRANSACTIONS)"/>
Guzman Llambias's avatar
Add Fabric -> Ethereum animation
Guzman Llambias committed
41 42 43 
    <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_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.variable#_LY134MEEEe6yC4BToIaAqA" 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_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.variable#_LY0pwMEEEe6yC4BToIaAqA" org.eventb.core.type="ℤ"/>
    <org.eventb.core.scVariable name="accounts" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.variable#_8rz-D77uEe6laZimEYihUg" org.eventb.core.type="ℙ(ADDRESS×ℤ)"/>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
44 
    <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_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.variable#_2ZLTIfRgEe60CqkwWvstGA" org.eventb.core.type="ℙ(GATEWAYS×TARGET_TRANSACTIONS)"/>
Guzman Llambias's avatar
Add Fabric -> Ethereum animation
Guzman Llambias committed
45 
    <org.eventb.core.scVariable name="subscriptions" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_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
46 47 
    <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_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.variable#_cNBD0PKVEe60CqkwWvstGA" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×SMART_CONTRACT_EVENTS)"/>
    <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_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.variable#_2ZLTIPRgEe60CqkwWvstGA" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×SOURCE_TRANSACTIONS)"/>
Guzman Llambias's avatar
Change trigger for emit event  
Guzman Llambias committed
48 
    <org.eventb.core.scVariable name="emitted" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.variable#_ZQ-UAfKWEe60CqkwWvstGA" org.eventb.core.type="ℤ"/>
Guzman Llambias's avatar
Add Fabric -> Ethereum animation
Guzman Llambias committed
49 
    <org.eventb.core.scVariable name="wallet_created" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.variable#_qWPSQMEGEe6yC4BToIaAqA" org.eventb.core.type="ℤ"/>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
50 51 52 53 
    <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_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh">
        <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/gateway-event-b/CCTx_Fabric_Ethereum_m2.bcm|org.eventb.core.scMachineFile#CCTx_Fabric_Ethereum_m2|org.eventb.core.scEvent#received_target_transactiont" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_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
54 
        <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
55 56 
        <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 Fabric -> Ethereum animation
Guzman Llambias committed
57 58 59 
        <org.eventb.core.scAction name="," org.eventb.core.assignment="accounts ≔ ∅ ⦂ ℙ(ADDRESS×ℤ)" org.eventb.core.label="act11" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh|org.eventb.core.action#_XvgZ8MEBEe6yC4BToIaAqA"/>
        <org.eventb.core.scAction name="-" org.eventb.core.assignment="subscribed ≔ 0" org.eventb.core.label="init_subscribed" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh|org.eventb.core.action#_Xag6AMEEEe6yC4BToIaAqA"/>
        <org.eventb.core.scAction name="." org.eventb.core.assignment="initiated ≔ 0" org.eventb.core.label="init_initiated" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh|org.eventb.core.action#_XahhEMEEEe6yC4BToIaAqA"/>
Guzman Llambias's avatar
Change trigger for emit event  
Guzman Llambias committed
60 
        <org.eventb.core.scAction name="/" org.eventb.core.assignment="emitted ≔ 0" org.eventb.core.label="init_emitted" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh|org.eventb.core.action#_ZQ-UAPKWEe60CqkwWvstGA"/>
Guzman Llambias's avatar
Add Fabric -> Ethereum animation
Guzman Llambias committed
61 62 63 64 65 
        <org.eventb.core.scAction name="0" org.eventb.core.assignment="gateway_processing ≔ 0" org.eventb.core.label="init_gateway_processing" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh|org.eventb.core.action#_XahhEsEEEe6yC4BToIaAqA"/>
        <org.eventb.core.scAction name="1" org.eventb.core.assignment="submit_cc_tx ≔ 0" org.eventb.core.label="init_submit_cc_tx" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh|org.eventb.core.action#_XahhE8EEEe6yC4BToIaAqA"/>
        <org.eventb.core.scAction name="2" org.eventb.core.assignment="wallet_created ≔ 0" org.eventb.core.label="init_wallet_created" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh|org.eventb.core.action#_y69sYMEGEe6yC4BToIaAqA"/>
        <org.eventb.core.scAction name="3" org.eventb.core.assignment="wallet_amount ≔ 0" org.eventb.core.label="init_wallet_amount" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh|org.eventb.core.action#_BKVfsMEIEe6yC4BToIaAqA"/>
    </org.eventb.core.scEvent>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
66 67 
    <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_FABRIC" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUi">
        <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/gateway-event-b/CCTx_Fabric_Ethereum_m2.bcm|org.eventb.core.scMachineFile#CCTx_Fabric_Ethereum_m2|org.eventb.core.scEvent#received_target_transactionu" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUi|org.eventb.core.refinesEvent#'"/>
Guzman Llambias's avatar
Change trigger for emit event  
Guzman Llambias committed
68 69 
        <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
Add Fabric -> Ethereum animation
Guzman Llambias committed
70 71 
        <org.eventb.core.scAction name=")" org.eventb.core.assignment="subscribed ≔ 1" org.eventb.core.label="act111" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUi|org.eventb.core.action#_hvM14MEEEe6yC4BToIaAqA"/>
    </org.eventb.core.scEvent>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
72 73 74 75 76 77 
    <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_FABRIC" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUj">
        <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/gateway-event-b/CCTx_Fabric_Ethereum_m2.bcm|org.eventb.core.scMachineFile#CCTx_Fabric_Ethereum_m2|org.eventb.core.scEvent#received_target_transactionv" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUj|org.eventb.core.refinesEvent#'"/>
        <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"/>
Guzman Llambias's avatar
Add Fabric -> Ethereum animation
Guzman Llambias committed
78 79 80 
        <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_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUj|org.eventb.core.action#_kp_MAMEEEe6yC4BToIaAqA"/>
        <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_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUj|org.eventb.core.action#_kqAaIMEEEe6yC4BToIaAqA"/>
    </org.eventb.core.scEvent>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
81 82 83 84 85 86 87 88 89 90 91 
    <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_FABRIC" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.event#_5dHIwPRhEe60CqkwWvstGA">
        <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/gateway-event-b/CCTx_Fabric_Ethereum_m2.bcm|org.eventb.core.scMachineFile#CCTx_Fabric_Ethereum_m2|org.eventb.core.scEvent#received_target_transactionw" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.event#_5dHIwPRhEe60CqkwWvstGA|org.eventb.core.refinesEvent#_5dHIwfRhEe60CqkwWvstGA"/>
        <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_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.event#_5dHIwPRhEe60CqkwWvstGA|org.eventb.core.action#_kp_zEMEEEe6yC4BToIaAqA"/>
        <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_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.event#_5dHIwPRhEe60CqkwWvstGA|org.eventb.core.action#_kqBoQMEEEe6yC4BToIaAqA"/>
        <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_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.event#_5dHIwPRhEe60CqkwWvstGA|org.eventb.core.action#_y9WKoMEJEe6yC4BToIaAqA"/>
Guzman Llambias's avatar
Add Fabric -> Ethereum animation
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 104 
    <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_FABRIC" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.event#_5dHv0PRhEe60CqkwWvstGA">
        <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/gateway-event-b/CCTx_Fabric_Ethereum_m2.bcm|org.eventb.core.scMachineFile#CCTx_Fabric_Ethereum_m2|org.eventb.core.scEvent#received_target_transactionx" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.event#_5dHv0PRhEe60CqkwWvstGA|org.eventb.core.refinesEvent#_5dHv0fRhEe60CqkwWvstGA"/>
        <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_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.event#_5dHv0PRhEe60CqkwWvstGA|org.eventb.core.action#_kqBBMMEEEe6yC4BToIaAqA"/>
        <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_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.event#_5dHv0PRhEe60CqkwWvstGA|org.eventb.core.action#_pHPaccEEEe6yC4BToIaAqA"/>
        <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_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.event#_5dHv0PRhEe60CqkwWvstGA|org.eventb.core.action#_EcXw0MELEe6yC4BToIaAqA"/>
Guzman Llambias's avatar
Add Fabric -> Ethereum animation
Guzman Llambias committed
105 
    </org.eventb.core.scEvent>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 
    <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_ETHEREUM" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.event#_5dIW4PRhEe60CqkwWvstGA">
        <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/gateway-event-b/CCTx_Fabric_Ethereum_m2.bcm|org.eventb.core.scMachineFile#CCTx_Fabric_Ethereum_m2|org.eventb.core.scEvent#received_target_transactiony" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.event#_5dIW4PRhEe60CqkwWvstGA|org.eventb.core.refinesEvent#_5dIW4fRhEe60CqkwWvstGA"/>
        <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="gateway_address∈dom(accounts)" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_m2|org.eventb.core.event#_1TfoBPRhEe60CqkwWvstGA|org.eventb.core.guard#_XvhBAcEBEe6yC4BToIaAqA" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="pending_evenx" org.eventb.core.label="grd12" org.eventb.core.predicate="accounts(gateway_address)≥fee" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_m2|org.eventb.core.event#_1TfoBPRhEe60CqkwWvstGA|org.eventb.core.guard#_XvhBAsEBEe6yC4BToIaAqA" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="pending_eveny" org.eventb.core.label="grd13" org.eventb.core.predicate="fee&gt;0" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_m2|org.eventb.core.event#_1TfoBPRhEe60CqkwWvstGA|org.eventb.core.guard#_XvhBA8EBEe6yC4BToIaAqA" 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_evenz" org.eventb.core.assignment="accounts ≔ accounts{gateway_address ↦ accounts(gateway_address) − fee}" org.eventb.core.label="act11" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_m2|org.eventb.core.event#_1TfoBPRhEe60CqkwWvstGA|org.eventb.core.action#_XvhBAMEBEe6yC4BToIaAqA"/>
        <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="fee" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_m2|org.eventb.core.event#_1TfoBPRhEe60CqkwWvstGA|org.eventb.core.parameter#_8rz9977uEe6laZimEYihUg" org.eventb.core.type="ℤ"/>
        <org.eventb.core.scAction name="pending_even{" org.eventb.core.assignment="submit_cc_tx ≔ 1" org.eventb.core.label="act31" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.event#_5dIW4PRhEe60CqkwWvstGA|org.eventb.core.action#_pHPacMEEEe6yC4BToIaAqA"/>
        <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_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.event#_5dIW4PRhEe60CqkwWvstGA|org.eventb.core.action#_EcY-8MELEe6yC4BToIaAqA"/>
        <org.eventb.core.scAction name="pending_even}" org.eventb.core.assignment="wallet_amount ≔ accounts(gateway_address) − fee" org.eventb.core.label="act33" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.event#_5dIW4PRhEe60CqkwWvstGA|org.eventb.core.action#_EcZmAMELEe6yC4BToIaAqA"/>
Guzman Llambias's avatar
Add Fabric -> Ethereum animation
Guzman Llambias committed
122 
    </org.eventb.core.scEvent>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
123 124 
    <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_ADDRESS_IN_ETHEREUM" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUn">
        <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/gateway-event-b/CCTx_Fabric_Ethereum_m2.bcm|org.eventb.core.scMachineFile#CCTx_Fabric_Ethereum_m2|org.eventb.core.scEvent#received_target_transactionz" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUn|org.eventb.core.refinesEvent#'"/>
Guzman Llambias's avatar
Add Fabric -> Ethereum animation
Guzman Llambias committed
125 126 127 128 129 130 131 
        <org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="address∈ADDRESS" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_m2|org.eventb.core.event#_8rz9-L7uEe6laZimEYihUg|org.eventb.core.guard#_XvhoEcEBEe6yC4BToIaAqA" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="address∉dom(accounts)" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_m2|org.eventb.core.event#_8rz9-L7uEe6laZimEYihUg|org.eventb.core.guard#_XvhoEsEBEe6yC4BToIaAqA" org.eventb.core.theorem="false"/>
        <org.eventb.core.scAction name="addrest" org.eventb.core.assignment="accounts ≔ accounts∪{address ↦ 0}" org.eventb.core.label="act1" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_m2|org.eventb.core.event#_8rz9-L7uEe6laZimEYihUg|org.eventb.core.action#_XvhoEMEBEe6yC4BToIaAqA"/>
        <org.eventb.core.scParameter name="address" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_m2|org.eventb.core.event#_8rz9-L7uEe6laZimEYihUg|org.eventb.core.parameter#_8rz9_L7uEe6laZimEYihUg" org.eventb.core.type="ADDRESS"/>
        <org.eventb.core.scGuard name="addresu" org.eventb.core.label="grd31" org.eventb.core.predicate="address=gateway_address" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUn|org.eventb.core.guard#_wieyEMEGEe6yC4BToIaAqA" org.eventb.core.theorem="false"/>
        <org.eventb.core.scAction name="addresv" org.eventb.core.assignment="wallet_created ≔ 1" org.eventb.core.label="act31" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUn|org.eventb.core.action#_qWM2AMEGEe6yC4BToIaAqA"/>
    </org.eventb.core.scEvent>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
132 133 
    <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="DEPOSIT_CRYPTOCURRENCY_IN_ETHEREUM" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUo">
        <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/gateway-event-b/CCTx_Fabric_Ethereum_m2.bcm|org.eventb.core.scMachineFile#CCTx_Fabric_Ethereum_m2|org.eventb.core.scEvent#received_target_transaction{" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUo|org.eventb.core.refinesEvent#'"/>
Guzman Llambias's avatar
Add Fabric -> Ethereum animation
Guzman Llambias committed
134 135 136 137 138 139 140 141 
        <org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="amount&gt;0" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_m2|org.eventb.core.event#_8rz9_b7uEe6laZimEYihUg|org.eventb.core.guard#_XvhoFMEBEe6yC4BToIaAqA" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="address∈dom(accounts)" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_m2|org.eventb.core.event#_8rz9_b7uEe6laZimEYihUg|org.eventb.core.guard#_XvhoFcEBEe6yC4BToIaAqA" org.eventb.core.theorem="false"/>
        <org.eventb.core.scAction name="addrest" org.eventb.core.assignment="accounts ≔ accounts{address ↦ accounts(address)+amount}" org.eventb.core.label="act1" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_m2|org.eventb.core.event#_8rz9_b7uEe6laZimEYihUg|org.eventb.core.action#_XvhoE8EBEe6yC4BToIaAqA"/>
        <org.eventb.core.scParameter name="amount" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_m2|org.eventb.core.event#_8rz9_b7uEe6laZimEYihUg|org.eventb.core.parameter#_8rz-Ab7uEe6laZimEYihUg" org.eventb.core.type="ℤ"/>
        <org.eventb.core.scParameter name="address" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_m2|org.eventb.core.event#_8rz9_b7uEe6laZimEYihUg|org.eventb.core.parameter#_8rz-Ar7uEe6laZimEYihUg" org.eventb.core.type="ADDRESS"/>
        <org.eventb.core.scAction name="addresu" org.eventb.core.assignment="wallet_amount ≔ accounts(address)+amount" org.eventb.core.label="act31" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUo|org.eventb.core.action#_7CFvEMEHEe6yC4BToIaAqA"/>
        <org.eventb.core.scAction name="addresv" org.eventb.core.assignment="submit_cc_tx ≔ 0" org.eventb.core.label="act32" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUo|org.eventb.core.action#_FU5CUMENEe6yC4BToIaAqA"/>
    </org.eventb.core.scEvent>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
142 143 
    <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="SUBMIT_TRANSFER_TRANSACTION_IN_ETHEREUM" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUp">
        <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/gateway-event-b/CCTx_Fabric_Ethereum_m2.bcm|org.eventb.core.scMachineFile#CCTx_Fabric_Ethereum_m2|org.eventb.core.scEvent#received_target_transaction\|" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUp|org.eventb.core.refinesEvent#'"/>
Guzman Llambias's avatar
Add Fabric -> Ethereum animation
Guzman Llambias committed
144 145 146 147 148 149 150 151 152 153 154 155 
        <org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="user_address∈dom(accounts)" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_m2|org.eventb.core.event#_8rz-A77uEe6laZimEYihUg|org.eventb.core.guard#_XviPIcEBEe6yC4BToIaAqA" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="accounts(user_address)≥validator_fee+transfer_amount" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_m2|org.eventb.core.event#_8rz-A77uEe6laZimEYihUg|org.eventb.core.guard#_XviPIsEBEe6yC4BToIaAqA" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name=")" org.eventb.core.label="grd3" org.eventb.core.predicate="validator_fee&gt;0" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_m2|org.eventb.core.event#_8rz-A77uEe6laZimEYihUg|org.eventb.core.guard#_XviPI8EBEe6yC4BToIaAqA" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="*" org.eventb.core.label="grd4" org.eventb.core.predicate="transfer_amount&gt;0" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_m2|org.eventb.core.event#_8rz-A77uEe6laZimEYihUg|org.eventb.core.guard#_Xvi2MMEBEe6yC4BToIaAqA" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="+" org.eventb.core.label="grd5" org.eventb.core.predicate="gateway_address∈dom(accounts)" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_m2|org.eventb.core.event#_8rz-A77uEe6laZimEYihUg|org.eventb.core.guard#_Xvi2McEBEe6yC4BToIaAqA" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="," org.eventb.core.label="grd6" org.eventb.core.predicate="({user_address,gateway_address} ⩤ accounts)∪{gateway_address ↦ accounts(gateway_address)+transfer_amount}∪{user_address ↦ accounts(user_address) − transfer_amount − validator_fee}∈ADDRESS ⇸ ℕ" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_m2|org.eventb.core.event#_8rz-A77uEe6laZimEYihUg|org.eventb.core.guard#_Xvi2MsEBEe6yC4BToIaAqA" org.eventb.core.theorem="false"/>
        <org.eventb.core.scAction name="transfer_amounu" org.eventb.core.assignment="accounts ≔ ({user_address,gateway_address} ⩤ accounts)∪{gateway_address ↦ accounts(gateway_address)+transfer_amount}∪{user_address ↦ accounts(user_address) − transfer_amount − validator_fee}" org.eventb.core.label="act1" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_m2|org.eventb.core.event#_8rz-A77uEe6laZimEYihUg|org.eventb.core.action#_XviPIMEBEe6yC4BToIaAqA"/>
        <org.eventb.core.scParameter name="user_address" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_m2|org.eventb.core.event#_8rz-A77uEe6laZimEYihUg|org.eventb.core.parameter#_8rz-DL7uEe6laZimEYihUg" org.eventb.core.type="ADDRESS"/>
        <org.eventb.core.scParameter name="validator_fee" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_m2|org.eventb.core.event#_8rz-A77uEe6laZimEYihUg|org.eventb.core.parameter#_8rz-C77uEe6laZimEYihUg" org.eventb.core.type="ℤ"/>
        <org.eventb.core.scParameter name="transfer_amount" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_m2|org.eventb.core.event#_8rz-A77uEe6laZimEYihUg|org.eventb.core.parameter#_8rz-Db7uEe6laZimEYihUg" org.eventb.core.type="ℤ"/>
    </org.eventb.core.scEvent>
</org.eventb.core.scMachineFile>