Skip to content
Snippets Groups Projects
Normal view Permalink
CCTx_Abstract_Animation_m2.bcm 32.1 KiB
Newer Older
Guzman Llambias's avatar
Improve abstract machine animation
Guzman Llambias committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 
<?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_Abstract_DLT_m1.bcm" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.refinesMachine#_VBLQ0MEUEe6yC4BToIaAqA"/>
    <org.eventb.core.scSeesContext name="(" org.eventb.core.scTarget="/gateway-event-b/CCTx_Abstract_DLT_c1.bcc" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.seesContext#_yQ9vsL7uEe6laZimEYihUg"/>
    <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"/>
        <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.scCarrierSet name="CROSS_CHAIN_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#_lhTmNr7uEe6laZimEYihUg" org.eventb.core.type="ℙ(CROSS_CHAIN_EVENTS)"/>
        <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="CROSS_CHAIN_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#_lhTmN77uEe6laZimEYihUg" org.eventb.core.type="ℙ(CROSS_CHAIN_TRANSACTIONS)"/>
        <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)"/>
        <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="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#_lhTmNL7uEe6laZimEYihUg" org.eventb.core.type="ℙ(TRANSACTIONS)"/>
        <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.scInvariant name="CCTx_Abstract_DLT_c2" org.eventb.core.label="inv1;" org.eventb.core.predicate="received_transactions∈CROSS_CHAIN_SMART_CONTRACTS ↔ 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#_yREdZL7uEe6laZimEYihUg" org.eventb.core.theorem="false"/>
    <org.eventb.core.scInvariant name="CCTx_Abstract_DLT_c3" org.eventb.core.label="inv2;" org.eventb.core.predicate="triggered_events∈CROSS_CHAIN_SMART_CONTRACTS ↔ CROSS_CHAIN_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#_yREdZb7uEe6laZimEYihUg" org.eventb.core.theorem="false"/>
    <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#_yREdZr7uEe6laZimEYihUg" org.eventb.core.theorem="false"/>
    <org.eventb.core.scInvariant name="CCTx_Abstract_DLT_c5" org.eventb.core.label="inv4;" org.eventb.core.predicate="gateway_pending_transactions∈GATEWAYS ↔ CROSS_CHAIN_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#_yREdZ77uEe6laZimEYihUg" org.eventb.core.theorem="false"/>
    <org.eventb.core.scInvariant name="CCTx_Abstract_DLT_c6" org.eventb.core.label="inv6;" org.eventb.core.predicate="received_cross_chain_transactions∈CROSS_CHAIN_SMART_CONTRACTS ↔ CROSS_CHAIN_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#_yREdaL7uEe6laZimEYihUg" org.eventb.core.theorem="false"/>
    <org.eventb.core.scInvariant name="CCTx_Abstract_DLT_c7" org.eventb.core.label="inv11" org.eventb.core.predicate="subscribed∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.invariant#_VBL34sEUEe6yC4BToIaAqA" org.eventb.core.theorem="false"/>
    <org.eventb.core.scInvariant name="CCTx_Abstract_DLT_c8" org.eventb.core.label="inv12" org.eventb.core.predicate="initiated∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.invariant#_VBMe8MEUEe6yC4BToIaAqA" org.eventb.core.theorem="false"/>
    <org.eventb.core.scInvariant name="CCTx_Abstract_DLT_c9" org.eventb.core.label="inv13" org.eventb.core.predicate="triggered∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.invariant#_VBMe8cEUEe6yC4BToIaAqA" org.eventb.core.theorem="false"/>
    <org.eventb.core.scInvariant name="CCTx_Abstract_DLT_c:" org.eventb.core.label="inv14" org.eventb.core.predicate="gateway_processing∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.invariant#_VBNGAMEUEe6yC4BToIaAqA" org.eventb.core.theorem="false"/>
    <org.eventb.core.scInvariant name="CCTx_Abstract_DLT_c;" org.eventb.core.label="inv15" org.eventb.core.predicate="submit_cc_tx∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.invariant#_VBNGAcEUEe6yC4BToIaAqA" 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_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.variable#_m7KdIMBDEe6yC4BToIaAqA" org.eventb.core.type="ℤ"/>
    <org.eventb.core.scVariable name="triggered_events" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.variable#_yREdar7uEe6laZimEYihUg" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_EVENTS)"/>
    <org.eventb.core.scVariable name="initiated" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.variable#_zZtTYMBBEe6yC4BToIaAqA" org.eventb.core.type="ℤ"/>
    <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_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.variable#_xgjHcMBDEe6yC4BToIaAqA" 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_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.variable#_65EIQMA-Ee6yC4BToIaAqA" org.eventb.core.type="ℤ"/>
    <org.eventb.core.scVariable name="received_cross_chain_transactions" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.variable#_yREdbb7uEe6laZimEYihUg" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_TRANSACTIONS)"/>
    <org.eventb.core.scVariable name="subscriptions" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.variable#_yREda77uEe6laZimEYihUg" org.eventb.core.type="ℙ(GATEWAYS×CROSS_CHAIN_SMART_CONTRACTS)"/>
    <org.eventb.core.scVariable name="triggered" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.variable#_RNsgkMBCEe6yC4BToIaAqA" org.eventb.core.type="ℤ"/>
    <org.eventb.core.scVariable name="gateway_pending_transactions" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.variable#_yREdbL7uEe6laZimEYihUg" org.eventb.core.type="ℙ(GATEWAYS×CROSS_CHAIN_TRANSACTIONS)"/>
    <org.eventb.core.scVariable name="received_transactions" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.variable#_yREdab7uEe6laZimEYihUg" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×TRANSACTIONS)"/>
    <org.eventb.core.scEvent name="received_cross_chain_transactiont" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="INITIATE_CC_TX" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqD">
        <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/gateway-event-b/CCTx_Abstract_DLT_m1.bcm|org.eventb.core.scMachineFile#CCTx_Abstract_DLT_m1|org.eventb.core.scEvent#received_cross_chain_transactionv" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqD|org.eventb.core.refinesEvent#'"/>
        <org.eventb.core.scGuard name="'" org.eventb.core.label="grd1;" org.eventb.core.predicate="transaction∈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#_yQ9vu77uEe6laZimEYihUg" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="(" org.eventb.core.label="grd3;" org.eventb.core.predicate="transaction∉received_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#_yQ9vvL7uEe6laZimEYihUg" org.eventb.core.theorem="false"/>
        <org.eventb.core.scAction name="transactioo" org.eventb.core.assignment="received_transactions ≔ received_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#_yQ9vur7uEe6laZimEYihUg"/>
        <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="TRANSACTIONS"/>
        <org.eventb.core.scAction name="transactiop" org.eventb.core.assignment="initiated ≔ 1" org.eventb.core.label="act11" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqD|org.eventb.core.action#_VBQwYMEUEe6yC4BToIaAqA"/>
        <org.eventb.core.scAction name="transactioq" org.eventb.core.assignment="submit_cc_tx ≔ 0" org.eventb.core.label="act12" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqD|org.eventb.core.action#_VBRXccEUEe6yC4BToIaAqA"/>
    </org.eventb.core.scEvent>
    <org.eventb.core.scEvent name="received_cross_chain_transactionu" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="TRIGGER_CC_TX_EVENT" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqE">
        <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/gateway-event-b/CCTx_Abstract_DLT_m1.bcm|org.eventb.core.scMachineFile#CCTx_Abstract_DLT_m1|org.eventb.core.scEvent#received_cross_chain_transactionw" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqE|org.eventb.core.refinesEvent#'"/>
        <org.eventb.core.scGuard name="'" org.eventb.core.label="grd1;" org.eventb.core.predicate="source_smart_contract ↦ transaction∈received_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#_E_KKUMBGEe6yC4BToIaAqA|org.eventb.core.guard#_yQ9vwb7uEe6laZimEYihUg" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="(" org.eventb.core.label="grd2;" org.eventb.core.predicate="cross_chain_event∉triggered_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#_E_KKUMBGEe6yC4BToIaAqA|org.eventb.core.guard#_yQ9vwr7uEe6laZimEYihUg" org.eventb.core.theorem="false"/>
        <org.eventb.core.scAction name="cross_chain_evenu" org.eventb.core.assignment="triggered_events ≔ triggered_events∪{source_smart_contract ↦ cross_chain_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#_E_KKUMBGEe6yC4BToIaAqA|org.eventb.core.action#_yQ9vv77uEe6laZimEYihUg"/>
        <org.eventb.core.scAction name="cross_chain_evenv" org.eventb.core.assignment="received_transactions ≔ received_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#_E_KKUMBGEe6yC4BToIaAqA|org.eventb.core.action#_yQ9vwL7uEe6laZimEYihUg"/>
        <org.eventb.core.scParameter name="cross_chain_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#_E_KKUMBGEe6yC4BToIaAqA|org.eventb.core.parameter#_yQ9vxL7uEe6laZimEYihUg" org.eventb.core.type="CROSS_CHAIN_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#_E_KKUMBGEe6yC4BToIaAqA|org.eventb.core.parameter#_yQ9vw77uEe6laZimEYihUg" org.eventb.core.type="TRANSACTIONS"/>
        <org.eventb.core.scAction name="cross_chain_evenw" org.eventb.core.assignment="triggered ≔ 1" org.eventb.core.label="act11" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqE|org.eventb.core.action#_VBRXcMEUEe6yC4BToIaAqA"/>
        <org.eventb.core.scAction name="cross_chain_evenx" org.eventb.core.assignment="initiated ≔ 0" org.eventb.core.label="act12" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqE|org.eventb.core.action#_VBR-gcEUEe6yC4BToIaAqA"/>
        <org.eventb.core.scAction name="cross_chain_eveny" org.eventb.core.assignment="submit_cc_tx ≔ 0" org.eventb.core.label="act13" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqE|org.eventb.core.action#_kIrbcMEUEe6yC4BToIaAqA"/>
    </org.eventb.core.scEvent>
    <org.eventb.core.scEvent name="received_cross_chain_transactionv" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="LISTEN_CC_TX_EVENT" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqF">
        <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/gateway-event-b/CCTx_Abstract_DLT_m1.bcm|org.eventb.core.scMachineFile#CCTx_Abstract_DLT_m1|org.eventb.core.scEvent#received_cross_chain_transactionx" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqF|org.eventb.core.refinesEvent#'"/>
        <org.eventb.core.scGuard name="'" org.eventb.core.label="grd1;" org.eventb.core.predicate="source_smart_contract ↦ cross_chain_event∈triggered_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#_THog4MBGEe6yC4BToIaAqA|org.eventb.core.guard#_yQ9vyL7uEe6laZimEYihUg" 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#_THog4MBGEe6yC4BToIaAqA|org.eventb.core.guard#_yQ9vyb7uEe6laZimEYihUg" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name=")" org.eventb.core.label="grd3;" org.eventb.core.predicate="gateway ↦ cross_chain_transaction∉gateway_pending_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#_THog4MBGEe6yC4BToIaAqA|org.eventb.core.guard#_yQ9vyr7uEe6laZimEYihUg" org.eventb.core.theorem="false"/>
        <org.eventb.core.scAction name="cross_chain_transactioo" org.eventb.core.assignment="gateway_pending_transactions ≔ gateway_pending_transactions∪{gateway ↦ cross_chain_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#_THog4MBGEe6yC4BToIaAqA|org.eventb.core.action#_yQ9vxr7uEe6laZimEYihUg"/>
        <org.eventb.core.scAction name="cross_chain_transactiop" org.eventb.core.assignment="triggered_events ≔ triggered_events ∖ {source_smart_contract ↦ cross_chain_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#_THog4MBGEe6yC4BToIaAqA|org.eventb.core.action#_yQ9vx77uEe6laZimEYihUg"/>
        <org.eventb.core.scParameter name="cross_chain_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#_THog4MBGEe6yC4BToIaAqA|org.eventb.core.parameter#_yQ9vy77uEe6laZimEYihUg" org.eventb.core.type="CROSS_CHAIN_EVENTS"/>
        <org.eventb.core.scParameter name="cross_chain_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#_THog4MBGEe6yC4BToIaAqA|org.eventb.core.parameter#_yQ9vzL7uEe6laZimEYihUg" org.eventb.core.type="CROSS_CHAIN_TRANSACTIONS"/>
        <org.eventb.core.scAction name="cross_chain_transactioq" org.eventb.core.assignment="gateway_processing ≔ 1" org.eventb.core.label="act11" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqF|org.eventb.core.action#_VBR-gMEUEe6yC4BToIaAqA"/>
        <org.eventb.core.scAction name="cross_chain_transactior" org.eventb.core.assignment="triggered ≔ 0" org.eventb.core.label="act12" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqF|org.eventb.core.action#_VBL34cEUEe6yC4BToIaAqA"/>
        <org.eventb.core.scAction name="cross_chain_transactios" org.eventb.core.assignment="submit_cc_tx ≔ 0" org.eventb.core.label="act13" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqF|org.eventb.core.action#_k8Z-cMEUEe6yC4BToIaAqA"/>
    </org.eventb.core.scEvent>
    <org.eventb.core.scEvent name="received_cross_chain_transactionw" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="SUBMIT_CC_TX" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqG">
        <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/gateway-event-b/CCTx_Abstract_DLT_m1.bcm|org.eventb.core.scMachineFile#CCTx_Abstract_DLT_m1|org.eventb.core.scEvent#received_cross_chain_transactiony" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqG|org.eventb.core.refinesEvent#'"/>
        <org.eventb.core.scGuard name="'" org.eventb.core.label="grd1;" org.eventb.core.predicate="gateway ↦ cross_chain_transaction∈gateway_pending_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#_fwqd8MBGEe6yC4BToIaAqA|org.eventb.core.guard#_yREdYr7uEe6laZimEYihUg" org.eventb.core.theorem="false"/>
        <org.eventb.core.scAction name="cross_chain_transactioo" org.eventb.core.assignment="received_cross_chain_transactions ≔ received_cross_chain_transactions∪{target_smart_contract ↦ cross_chain_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#_fwqd8MBGEe6yC4BToIaAqA|org.eventb.core.action#_yREdYL7uEe6laZimEYihUg"/>
        <org.eventb.core.scAction name="cross_chain_transactiop" org.eventb.core.assignment="gateway_pending_transactions ≔ gateway_pending_transactions ∖ {gateway ↦ cross_chain_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#_fwqd8MBGEe6yC4BToIaAqA|org.eventb.core.action#_yREdYb7uEe6laZimEYihUg"/>
        <org.eventb.core.scParameter name="cross_chain_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#_fwqd8MBGEe6yC4BToIaAqA|org.eventb.core.parameter#_yREdY77uEe6laZimEYihUg" org.eventb.core.type="CROSS_CHAIN_TRANSACTIONS"/>
        <org.eventb.core.scAction name="cross_chain_transactioq" org.eventb.core.assignment="submit_cc_tx ≔ 1" org.eventb.core.label="act11" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqG|org.eventb.core.action#_VBL34MEUEe6yC4BToIaAqA"/>
        <org.eventb.core.scAction name="cross_chain_transactior" org.eventb.core.assignment="gateway_processing ≔ 0" org.eventb.core.label="act12" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqG|org.eventb.core.action#_isfxUMEUEe6yC4BToIaAqA"/>
    </org.eventb.core.scEvent>
    <org.eventb.core.scEvent name="received_cross_chain_transactionx" 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_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqB">
        <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/gateway-event-b/CCTx_Abstract_DLT_m1.bcm|org.eventb.core.scMachineFile#CCTx_Abstract_DLT_m1|org.eventb.core.scEvent#received_cross_chain_transactiont" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqB"/>
        <org.eventb.core.scAction name="'" org.eventb.core.assignment="received_transactions ≔ ∅ ⦂ ℙ(CROSS_CHAIN_SMART_CONTRACTS×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#_yQ9vsb7uEe6laZimEYihUg"/>
        <org.eventb.core.scAction name="(" org.eventb.core.assignment="triggered_events ≔ ∅ ⦂ ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_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#_yQ9vsr7uEe6laZimEYihUg"/>
        <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#_yQ9vs77uEe6laZimEYihUg"/>
        <org.eventb.core.scAction name="*" org.eventb.core.assignment="gateway_pending_transactions ≔ ∅ ⦂ ℙ(GATEWAYS×CROSS_CHAIN_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#_yQ9vtL7uEe6laZimEYihUg"/>
        <org.eventb.core.scAction name="+" org.eventb.core.assignment="received_cross_chain_transactions ≔ ∅ ⦂ ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_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#_yQ9vtb7uEe6laZimEYihUg"/>
        <org.eventb.core.scAction name="," org.eventb.core.assignment="subscribed ≔ 0" org.eventb.core.label="act11" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqB|org.eventb.core.action#_VBO7MMEUEe6yC4BToIaAqA"/>
        <org.eventb.core.scAction name="-" org.eventb.core.assignment="initiated ≔ 0" org.eventb.core.label="act12" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqB|org.eventb.core.action#_VBPiQMEUEe6yC4BToIaAqA"/>
        <org.eventb.core.scAction name="." org.eventb.core.assignment="triggered ≔ 0" org.eventb.core.label="act13" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqB|org.eventb.core.action#_VBPiQcEUEe6yC4BToIaAqA"/>
        <org.eventb.core.scAction name="/" org.eventb.core.assignment="gateway_processing ≔ 0" org.eventb.core.label="act14" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqB|org.eventb.core.action#_VBPiQsEUEe6yC4BToIaAqA"/>
        <org.eventb.core.scAction name="0" org.eventb.core.assignment="submit_cc_tx ≔ 0" org.eventb.core.label="act15" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqB|org.eventb.core.action#_VBPiQ8EUEe6yC4BToIaAqA"/>
    </org.eventb.core.scEvent>
    <org.eventb.core.scEvent name="received_cross_chain_transactiony" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="SUBSCRIBE_SMART_CONTRACT_EVENTS" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqC">
        <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/gateway-event-b/CCTx_Abstract_DLT_m1.bcm|org.eventb.core.scMachineFile#CCTx_Abstract_DLT_m1|org.eventb.core.scEvent#received_cross_chain_transactionu" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqC|org.eventb.core.refinesEvent#'"/>
        <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#_yQ9vuL7uEe6laZimEYihUg" 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#_yQ9vt77uEe6laZimEYihUg"/>
        <org.eventb.core.scAction name=")" org.eventb.core.assignment="subscribed ≔ 1" org.eventb.core.label="act11" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqC|org.eventb.core.action#_VBQJUMEUEe6yC4BToIaAqA"/>
    </org.eventb.core.scEvent>
</org.eventb.core.scMachineFile>