Newer
Older
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.machineFile org.eventb.core.configuration="org.eventb.core.fwd" org.eventb.core.generated="false" org.eventb.emf.persistence.emf_id="_fuHgbMBGEe6yC4BToIaAqA" org.eventb.texttools.text_lastmodified="1706711950404" org.eventb.texttools.text_representation="machine CCTx_Abstract_DLT_m1 sees CCTx_Abstract_DLT_c1 variables received_transactions triggered_events subscriptions gateway_pending_transactions received_cross_chain_transactions invariants @inv1; received_transactions ∈ CROSS_CHAIN_SMART_CONTRACTS ↔ TRANSACTIONS @inv2; triggered_events ∈ CROSS_CHAIN_SMART_CONTRACTS ↔ CROSS_CHAIN_EVENTS @inv3; subscriptions ∈ GATEWAYS ↔ CROSS_CHAIN_SMART_CONTRACTS @inv4; gateway_pending_transactions ∈ GATEWAYS ↔ CROSS_CHAIN_TRANSACTIONS @inv6; received_cross_chain_transactions ∈ CROSS_CHAIN_SMART_CONTRACTS ↔ CROSS_CHAIN_TRANSACTIONS events event INITIALISATION then @act1; received_transactions ≔ ∅ @act2; triggered_events ≔ ∅ @act3; subscriptions ≔ ∅ @act4; gateway_pending_transactions ≔ ∅ @act6; received_cross_chain_transactions ≔ ∅ end event SUBSCRIBE_SMART_CONTRACT_EVENTS where @grd1; gateway ↦ source_smart_contract ∉ subscriptions // The gateway is not already subscribed to the smart contract events then @act1; subscriptions ≔ subscriptions ∪ {gateway ↦ source_smart_contract} // The gateway is subscribed to listen to the smart contract events end event INITIATE_CC_TX any transaction where @grd1; transaction ∈ TRANSACTIONS @grd3; transaction ∉ received_transactions[{source_smart_contract}] then @act1; received_transactions ≔ received_transactions ∪ {source_smart_contract ↦ transaction} end event TRIGGER_CC_TX_EVENT any transaction cross_chain_event where @grd1; source_smart_contract ↦ transaction ∈ received_transactions // The smart contract has a pending transaction to process @grd2; cross_chain_event ∉ triggered_events[{source_smart_contract}] // The smart contract will allways trigger a new event then @act1; triggered_events ≔ triggered_events ∪ {source_smart_contract ↦ cross_chain_event} // The smart contract triggers a new event related to the transaction processing @act2; received_transactions ≔ received_transactions ∖ {source_smart_contract ↦ transaction} // The smart contract processed the transaction end event LISTEN_CC_TX_EVENT any cross_chain_event cross_chain_transaction where @grd1; source_smart_contract ↦ cross_chain_event ∈ triggered_events // The smart contract has triggered an event @grd2; gateway ↦ source_smart_contract ∈ subscriptions // Exist a subscription to the smart contract events @grd3; gateway ↦ cross_chain_transaction ∉ gateway_pending_transactions // The event was not already listened then @act1; gateway_pending_transactions ≔ gateway_pending_transactions ∪ {gateway ↦ cross_chain_transaction} // The event is added to the cross-chain transactions to be processed by the gateway @act2; triggered_events ≔ triggered_events ∖ {source_smart_contract ↦ cross_chain_event} // The event is listened and processed end event SUBMIT_CC_TX any cross_chain_transaction where @grd1; gateway ↦ cross_chain_transaction ∈ gateway_pending_transactions // There is one pending cross-chain transaction to process then @act1; received_cross_chain_transactions ≔ received_cross_chain_transactions ∪ {target_smart_contract ↦ cross_chain_transaction} @act2; gateway_pending_transactions ≔ gateway_pending_transactions ∖ {gateway ↦ cross_chain_transaction} end end" version="5">
<org.eventb.core.seesContext name="_yQ9vsL7uEe6laZimEYihUg" org.eventb.core.target="CCTx_Abstract_DLT_c1"/>
<org.eventb.core.event name="'" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="INITIALISATION" org.eventb.emf.persistence.emf_id="_fuHgT8BGEe6yC4BToIaAqA">
<org.eventb.core.action name="_yQ9vsb7uEe6laZimEYihUg" org.eventb.core.assignment="received_transactions ≔ ∅" org.eventb.core.generated="false" org.eventb.core.label="act1;" org.eventb.emf.persistence.emf_id="_fuHgSsBGEe6yC4BToIaAqA"/>
<org.eventb.core.action name="_yQ9vsr7uEe6laZimEYihUg" org.eventb.core.assignment="triggered_events ≔ ∅" org.eventb.core.generated="false" org.eventb.core.label="act2;" org.eventb.emf.persistence.emf_id="_fuHgS8BGEe6yC4BToIaAqA"/>
<org.eventb.core.action name="_yQ9vs77uEe6laZimEYihUg" org.eventb.core.assignment="subscriptions ≔ ∅" org.eventb.core.generated="false" org.eventb.core.label="act3;" org.eventb.emf.persistence.emf_id="_fuHgTMBGEe6yC4BToIaAqA"/>
<org.eventb.core.action name="_yQ9vtL7uEe6laZimEYihUg" org.eventb.core.assignment="gateway_pending_transactions ≔ ∅" org.eventb.core.generated="false" org.eventb.core.label="act4;" org.eventb.emf.persistence.emf_id="_fuHgTcBGEe6yC4BToIaAqA"/>
<org.eventb.core.action name="_yQ9vtb7uEe6laZimEYihUg" org.eventb.core.assignment="received_cross_chain_transactions ≔ ∅" org.eventb.core.generated="false" org.eventb.core.label="act6;" org.eventb.emf.persistence.emf_id="_fuHgTsBGEe6yC4BToIaAqA"/>
<org.eventb.core.event name="_yQ9vtr7uEe6laZimEYihUg" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="SUBSCRIBE_SMART_CONTRACT_EVENTS" org.eventb.emf.persistence.emf_id="_fuHgUsBGEe6yC4BToIaAqA">
<org.eventb.core.action name="_yQ9vt77uEe6laZimEYihUg" org.eventb.core.assignment="subscriptions ≔ subscriptions ∪ {gateway ↦ source_smart_contract}" org.eventb.core.comment="The gateway is subscribed to listen to the smart contract events" org.eventb.core.generated="false" org.eventb.core.label="act1;" org.eventb.emf.persistence.emf_id="_fuHgUcBGEe6yC4BToIaAqA"/>
<org.eventb.core.guard name="_yQ9vuL7uEe6laZimEYihUg" org.eventb.core.comment="The gateway is not already subscribed to the smart contract events" org.eventb.core.generated="false" org.eventb.core.label="grd1;" org.eventb.core.predicate="gateway ↦ source_smart_contract ∉ subscriptions" org.eventb.emf.persistence.emf_id="_fuHgUMBGEe6yC4BToIaAqA"/>
<org.eventb.core.event name="_y397cMBFEe6yC4BToIaAqA" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="INITIATE_CC_TX" org.eventb.emf.persistence.emf_id="_fuHgV8BGEe6yC4BToIaAqA">
<org.eventb.core.action name="_yQ9vur7uEe6laZimEYihUg" org.eventb.core.assignment="received_transactions ≔ received_transactions ∪ {source_smart_contract ↦ transaction}" org.eventb.core.generated="false" org.eventb.core.label="act1;" org.eventb.emf.persistence.emf_id="_fuHgVsBGEe6yC4BToIaAqA"/>
<org.eventb.core.guard name="_yQ9vu77uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.label="grd1;" org.eventb.core.predicate="transaction ∈ TRANSACTIONS" org.eventb.emf.persistence.emf_id="_fuHgVMBGEe6yC4BToIaAqA"/>
<org.eventb.core.guard name="_yQ9vvL7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.label="grd3;" org.eventb.core.predicate="transaction ∉ received_transactions[{source_smart_contract}]" org.eventb.emf.persistence.emf_id="_fuHgVcBGEe6yC4BToIaAqA"/>
<org.eventb.core.parameter name="_yQ9vvb7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="transaction" org.eventb.emf.persistence.emf_id="_fuHgU8BGEe6yC4BToIaAqA"/>
<org.eventb.core.event name="_E_KKUMBGEe6yC4BToIaAqA" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="TRIGGER_CC_TX_EVENT" org.eventb.emf.persistence.emf_id="_fuHgXsBGEe6yC4BToIaAqA">
<org.eventb.core.action name="_yQ9vv77uEe6laZimEYihUg" org.eventb.core.assignment="triggered_events ≔ triggered_events ∪ {source_smart_contract ↦ cross_chain_event}" org.eventb.core.comment="The smart contract triggers a new event related to the transaction processing" org.eventb.core.generated="false" org.eventb.core.label="act1;" org.eventb.emf.persistence.emf_id="_fuHgXMBGEe6yC4BToIaAqA"/>
<org.eventb.core.action name="_yQ9vwL7uEe6laZimEYihUg" org.eventb.core.assignment="received_transactions ≔ received_transactions ∖ {source_smart_contract ↦ transaction}" org.eventb.core.comment="The smart contract processed the transaction" org.eventb.core.generated="false" org.eventb.core.label="act2;" org.eventb.emf.persistence.emf_id="_fuHgXcBGEe6yC4BToIaAqA"/>
<org.eventb.core.guard name="_yQ9vwb7uEe6laZimEYihUg" org.eventb.core.comment="The smart contract has a pending transaction to process" org.eventb.core.generated="false" org.eventb.core.label="grd1;" org.eventb.core.predicate="source_smart_contract ↦ transaction ∈ received_transactions" org.eventb.emf.persistence.emf_id="_fuHgWsBGEe6yC4BToIaAqA"/>
<org.eventb.core.guard name="_yQ9vwr7uEe6laZimEYihUg" org.eventb.core.comment="The smart contract will allways trigger a new event" org.eventb.core.generated="false" org.eventb.core.label="grd2;" org.eventb.core.predicate="cross_chain_event ∉ triggered_events[{source_smart_contract}]" org.eventb.emf.persistence.emf_id="_fuHgW8BGEe6yC4BToIaAqA"/>
<org.eventb.core.parameter name="_yQ9vw77uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="transaction" org.eventb.emf.persistence.emf_id="_fuHgWMBGEe6yC4BToIaAqA"/>
<org.eventb.core.parameter name="_yQ9vxL7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="cross_chain_event" org.eventb.emf.persistence.emf_id="_fuHgWcBGEe6yC4BToIaAqA"/>
<org.eventb.core.event name="_THog4MBGEe6yC4BToIaAqA" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="LISTEN_CC_TX_EVENT" org.eventb.emf.persistence.emf_id="_fuHgZsBGEe6yC4BToIaAqA">
<org.eventb.core.action name="_yQ9vxr7uEe6laZimEYihUg" org.eventb.core.assignment="gateway_pending_transactions ≔ gateway_pending_transactions ∪ {gateway ↦ cross_chain_transaction}" org.eventb.core.comment="The event is added to the cross-chain transactions to be processed by the gateway" org.eventb.core.generated="false" org.eventb.core.label="act1;" org.eventb.emf.persistence.emf_id="_fuHgZMBGEe6yC4BToIaAqA"/>
<org.eventb.core.action name="_yQ9vx77uEe6laZimEYihUg" org.eventb.core.assignment="triggered_events ≔ triggered_events ∖ {source_smart_contract ↦ cross_chain_event}" org.eventb.core.comment="The event is listened and processed" org.eventb.core.generated="false" org.eventb.core.label="act2;" org.eventb.emf.persistence.emf_id="_fuHgZcBGEe6yC4BToIaAqA"/>
<org.eventb.core.guard name="_yQ9vyL7uEe6laZimEYihUg" org.eventb.core.comment="The smart contract has triggered an event" org.eventb.core.generated="false" org.eventb.core.label="grd1;" org.eventb.core.predicate="source_smart_contract ↦ cross_chain_event ∈ triggered_events" org.eventb.emf.persistence.emf_id="_fuHgYcBGEe6yC4BToIaAqA"/>
<org.eventb.core.guard name="_yQ9vyb7uEe6laZimEYihUg" org.eventb.core.comment="Exist a subscription to the smart contract events" org.eventb.core.generated="false" org.eventb.core.label="grd2;" org.eventb.core.predicate="gateway ↦ source_smart_contract ∈ subscriptions" org.eventb.emf.persistence.emf_id="_fuHgYsBGEe6yC4BToIaAqA"/>
<org.eventb.core.guard name="_yQ9vyr7uEe6laZimEYihUg" org.eventb.core.comment="The event was not already listened" org.eventb.core.generated="false" org.eventb.core.label="grd3;" org.eventb.core.predicate="gateway ↦ cross_chain_transaction ∉ gateway_pending_transactions" org.eventb.emf.persistence.emf_id="_fuHgY8BGEe6yC4BToIaAqA"/>
<org.eventb.core.parameter name="_yQ9vy77uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="cross_chain_event" org.eventb.emf.persistence.emf_id="_fuHgX8BGEe6yC4BToIaAqA"/>
<org.eventb.core.parameter name="_yQ9vzL7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="cross_chain_transaction" org.eventb.emf.persistence.emf_id="_fuHgYMBGEe6yC4BToIaAqA"/>
<org.eventb.core.event name="_fwqd8MBGEe6yC4BToIaAqA" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="SUBMIT_CC_TX" org.eventb.emf.persistence.emf_id="_fuHga8BGEe6yC4BToIaAqA">
<org.eventb.core.action name="_yREdYL7uEe6laZimEYihUg" org.eventb.core.assignment="received_cross_chain_transactions ≔ received_cross_chain_transactions ∪ {target_smart_contract ↦ cross_chain_transaction}" org.eventb.core.generated="false" org.eventb.core.label="act1;" org.eventb.emf.persistence.emf_id="_fuHgacBGEe6yC4BToIaAqA"/>
<org.eventb.core.action name="_yREdYb7uEe6laZimEYihUg" org.eventb.core.assignment="gateway_pending_transactions ≔ gateway_pending_transactions ∖ {gateway ↦ cross_chain_transaction}" org.eventb.core.generated="false" org.eventb.core.label="act2;" org.eventb.emf.persistence.emf_id="_fuHgasBGEe6yC4BToIaAqA"/>
<org.eventb.core.guard name="_yREdYr7uEe6laZimEYihUg" org.eventb.core.comment="There is one pending cross-chain transaction to process" org.eventb.core.generated="false" org.eventb.core.label="grd1;" org.eventb.core.predicate="gateway ↦ cross_chain_transaction ∈ gateway_pending_transactions" org.eventb.emf.persistence.emf_id="_fuHgaMBGEe6yC4BToIaAqA"/>
<org.eventb.core.parameter name="_yREdY77uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="cross_chain_transaction" org.eventb.emf.persistence.emf_id="_fuHgZ8BGEe6yC4BToIaAqA"/>
<org.eventb.core.invariant name="_yREdZL7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.label="inv1;" org.eventb.core.predicate="received_transactions ∈ CROSS_CHAIN_SMART_CONTRACTS ↔ TRANSACTIONS" org.eventb.emf.persistence.emf_id="_fuHgRcBGEe6yC4BToIaAqA"/>
<org.eventb.core.invariant name="_yREdZb7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.label="inv2;" org.eventb.core.predicate="triggered_events ∈ CROSS_CHAIN_SMART_CONTRACTS ↔ CROSS_CHAIN_EVENTS" org.eventb.emf.persistence.emf_id="_fuHgRsBGEe6yC4BToIaAqA"/>
<org.eventb.core.invariant name="_yREdZr7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.label="inv3;" org.eventb.core.predicate="subscriptions ∈ GATEWAYS ↔ CROSS_CHAIN_SMART_CONTRACTS" org.eventb.emf.persistence.emf_id="_fuHgR8BGEe6yC4BToIaAqA"/>
<org.eventb.core.invariant name="_yREdZ77uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.label="inv4;" org.eventb.core.predicate="gateway_pending_transactions ∈ GATEWAYS ↔ CROSS_CHAIN_TRANSACTIONS" org.eventb.emf.persistence.emf_id="_fuHgSMBGEe6yC4BToIaAqA"/>
<org.eventb.core.invariant name="_yREdaL7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.label="inv6;" org.eventb.core.predicate="received_cross_chain_transactions ∈ CROSS_CHAIN_SMART_CONTRACTS ↔ CROSS_CHAIN_TRANSACTIONS" org.eventb.emf.persistence.emf_id="_fuHgScBGEe6yC4BToIaAqA"/>
<org.eventb.core.variable name="_yREdab7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="received_transactions" org.eventb.emf.persistence.emf_id="_fuHgQMBGEe6yC4BToIaAqA"/>
<org.eventb.core.variable name="_yREdar7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="triggered_events" org.eventb.emf.persistence.emf_id="_fuHgQcBGEe6yC4BToIaAqA"/>
<org.eventb.core.variable name="_yREda77uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="subscriptions" org.eventb.emf.persistence.emf_id="_fuHgQsBGEe6yC4BToIaAqA"/>
<org.eventb.core.variable name="_yREdbL7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="gateway_pending_transactions" org.eventb.emf.persistence.emf_id="_fuHgQ8BGEe6yC4BToIaAqA"/>
<org.eventb.core.variable name="_yREdbb7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="received_cross_chain_transactions" org.eventb.emf.persistence.emf_id="_fuHgRMBGEe6yC4BToIaAqA"/>