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="_WA6ZPvRlEe60CqkwWvstGA" org.eventb.texttools.text_lastmodified="1712442660130" org.eventb.texttools.text_representation="machine CCTx_Abstract_DLT_m1 sees CCTx_Abstract_DLT_c1 variables received_source_transactions emitted_events subscriptions gateway_pending_events received_target_transactions invariants @inv1 received_source_transactions ∈ CROSS_CHAIN_SMART_CONTRACTS ↔ SOURCE_TRANSACTIONS @inv2 emitted_events ∈ CROSS_CHAIN_SMART_CONTRACTS ↔ SMART_CONTRACT_EVENTS @inv3 subscriptions ∈ GATEWAYS ↔ CROSS_CHAIN_SMART_CONTRACTS @inv4 gateway_pending_events ∈ GATEWAYS ↔ TARGET_TRANSACTIONS @inv5 received_target_transactions ∈ CROSS_CHAIN_SMART_CONTRACTS ↔ TARGET_TRANSACTIONS events event INITIALISATION then @act1 received_source_transactions ≔ ∅ @act2 emitted_events ≔ ∅ @act3 subscriptions ≔ ∅ @act4 gateway_pending_events ≔ ∅ @act6 received_target_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 ∈ SOURCE_TRANSACTIONS @grd3 transaction ∉ received_source_transactions[{source_smart_contract}] // The transaction was not received by the smart contract then @act1 received_source_transactions ≔ received_source_transactions ∪ {source_smart_contract ↦ transaction} // Add the transaction to the received transactions of the smart contract end event EMIT_EVENT any transaction emitted_event where @grd1 source_smart_contract ↦ transaction ∈ received_source_transactions // The smart contract has a pending transaction to process @grd2 emitted_event ∉ emitted_events[{source_smart_contract}] // The smart contract will always emit a new event then @act1 emitted_events ≔ emitted_events ∪ {source_smart_contract ↦ emitted_event} // The smart contract emits a new event related to the transaction processing @act2 received_source_transactions ≔ received_source_transactions ∖ {source_smart_contract ↦ transaction} // The smart contract processed the transaction end event LISTEN_EVENT any emitted_event pending_event where @grd1 source_smart_contract ↦ emitted_event ∈ emitted_events // The smart contract has emitted an event @grd2 gateway ↦ source_smart_contract ∈ subscriptions // Exist a subscription to the smart contract events @grd3 gateway ↦ pending_event ∉ gateway_pending_events // The event was not already listened then @act1 gateway_pending_events ≔ gateway_pending_events ∪ {gateway ↦ pending_event} // The event is added to the pending events to be processed by the gateway @act2 emitted_events ≔ emitted_events ∖ {source_smart_contract ↦ emitted_event} // The event is removed from the pending events to listen end event SUBMIT_TX any pending_event transaction where @grd1 gateway ↦ pending_event ∈ gateway_pending_events // There is one pending event to be processed @grd2 transaction ∈ TARGET_TRANSACTIONS then @act1 received_target_transactions ≔ received_target_transactions ∪ {target_smart_contract ↦ transaction} // The transaction is received by the target smart contract @act2 gateway_pending_events ≔ gateway_pending_events ∖ {gateway ↦ pending_event} // Remove the event from the pending events of the gateway 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="_WA6ZH_RlEe60CqkwWvstGA">
<org.eventb.core.action name="_zpBMgMQ4Ee609fto5wotHA" org.eventb.core.assignment="received_source_transactions ≔ ∅" org.eventb.core.generated="false" org.eventb.core.label="act1" org.eventb.emf.persistence.emf_id="_WA6ZGvRlEe60CqkwWvstGA"/>
<org.eventb.core.action name="_zpBzkMQ4Ee609fto5wotHA" org.eventb.core.assignment="emitted_events ≔ ∅" org.eventb.core.generated="false" org.eventb.core.label="act2" org.eventb.emf.persistence.emf_id="_WA6ZG_RlEe60CqkwWvstGA"/>
<org.eventb.core.action name="_zpBzkcQ4Ee609fto5wotHA" org.eventb.core.assignment="subscriptions ≔ ∅" org.eventb.core.generated="false" org.eventb.core.label="act3" org.eventb.emf.persistence.emf_id="_WA6ZHPRlEe60CqkwWvstGA"/>
<org.eventb.core.action name="_zpBzksQ4Ee609fto5wotHA" org.eventb.core.assignment="gateway_pending_events ≔ ∅" org.eventb.core.generated="false" org.eventb.core.label="act4" org.eventb.emf.persistence.emf_id="_WA6ZHfRlEe60CqkwWvstGA"/>
<org.eventb.core.action name="_zpCaoMQ4Ee609fto5wotHA" org.eventb.core.assignment="received_target_transactions ≔ ∅" org.eventb.core.generated="false" org.eventb.core.label="act6" org.eventb.emf.persistence.emf_id="_WA6ZHvRlEe60CqkwWvstGA"/>
<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="_WA6ZIvRlEe60CqkwWvstGA">
<org.eventb.core.action name="_zpDBsMQ4Ee609fto5wotHA" 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="_WA6ZIfRlEe60CqkwWvstGA"/>
<org.eventb.core.guard name="_zpDBscQ4Ee609fto5wotHA" 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="_WA6ZIPRlEe60CqkwWvstGA"/>
<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="_WA6ZJ_RlEe60CqkwWvstGA">
<org.eventb.core.action name="_zpDowMQ4Ee609fto5wotHA" org.eventb.core.assignment="received_source_transactions ≔ received_source_transactions ∪ {source_smart_contract ↦ transaction}" org.eventb.core.comment="Add the transaction to the received transactions of the smart contract" org.eventb.core.generated="false" org.eventb.core.label="act1" org.eventb.emf.persistence.emf_id="_WA6ZJvRlEe60CqkwWvstGA"/>
<org.eventb.core.guard name="_zpDowcQ4Ee609fto5wotHA" org.eventb.core.generated="false" org.eventb.core.label="grd1" org.eventb.core.predicate="transaction ∈ SOURCE_TRANSACTIONS" org.eventb.emf.persistence.emf_id="_WA6ZJPRlEe60CqkwWvstGA"/>
<org.eventb.core.guard name="_zpEP0MQ4Ee609fto5wotHA" org.eventb.core.comment="The transaction was not received by the smart contract" org.eventb.core.generated="false" org.eventb.core.label="grd3" org.eventb.core.predicate="transaction ∉ received_source_transactions[{source_smart_contract}]" org.eventb.emf.persistence.emf_id="_WA6ZJfRlEe60CqkwWvstGA"/>
<org.eventb.core.parameter name="_yQ9vvb7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="transaction" org.eventb.emf.persistence.emf_id="_WA6ZI_RlEe60CqkwWvstGA"/>
<org.eventb.core.event name="_WGbIAPRhEe60CqkwWvstGA" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="EMIT_EVENT" org.eventb.emf.persistence.emf_id="_WA6ZLvRlEe60CqkwWvstGA">
<org.eventb.core.action name="_zpE24MQ4Ee609fto5wotHA" org.eventb.core.assignment="emitted_events ≔ emitted_events ∪ {source_smart_contract ↦ emitted_event}" org.eventb.core.comment="The smart contract emits a new event related to the transaction processing" org.eventb.core.generated="false" org.eventb.core.label="act1" org.eventb.emf.persistence.emf_id="_WA6ZLPRlEe60CqkwWvstGA"/>
<org.eventb.core.action name="_zpFd8MQ4Ee609fto5wotHA" org.eventb.core.assignment="received_source_transactions ≔ received_source_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="_WA6ZLfRlEe60CqkwWvstGA"/>
<org.eventb.core.guard name="_zpFd8cQ4Ee609fto5wotHA" 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_source_transactions" org.eventb.emf.persistence.emf_id="_WA6ZKvRlEe60CqkwWvstGA"/>
<org.eventb.core.guard name="_zpGFAMQ4Ee609fto5wotHA" org.eventb.core.comment="The smart contract will always emit a new event" org.eventb.core.generated="false" org.eventb.core.label="grd2" org.eventb.core.predicate="emitted_event ∉ emitted_events[{source_smart_contract}]" org.eventb.emf.persistence.emf_id="_WA6ZK_RlEe60CqkwWvstGA"/>
<org.eventb.core.parameter name="_yQ9vw77uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="transaction" org.eventb.emf.persistence.emf_id="_WA6ZKPRlEe60CqkwWvstGA"/>
<org.eventb.core.parameter name="_RRvi8PRfEe60CqkwWvstGA" org.eventb.core.generated="false" org.eventb.core.identifier="emitted_event" org.eventb.emf.persistence.emf_id="_WA6ZKfRlEe60CqkwWvstGA"/>
<org.eventb.core.event name="_WGbvEPRhEe60CqkwWvstGA" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="LISTEN_EVENT" org.eventb.emf.persistence.emf_id="_WA6ZNvRlEe60CqkwWvstGA">
<org.eventb.core.action name="_zpGsEMQ4Ee609fto5wotHA" org.eventb.core.assignment="gateway_pending_events ≔ gateway_pending_events ∪ {gateway ↦ pending_event}" org.eventb.core.comment="The event is added to the pending events to be processed by the gateway" org.eventb.core.generated="false" org.eventb.core.label="act1" org.eventb.emf.persistence.emf_id="_WA6ZNPRlEe60CqkwWvstGA"/>
<org.eventb.core.action name="_zpHTIMQ4Ee609fto5wotHA" org.eventb.core.assignment="emitted_events ≔ emitted_events ∖ {source_smart_contract ↦ emitted_event}" org.eventb.core.comment="The event is removed from the pending events to listen" org.eventb.core.generated="false" org.eventb.core.label="act2" org.eventb.emf.persistence.emf_id="_WA6ZNfRlEe60CqkwWvstGA"/>
<org.eventb.core.guard name="_zpHTIcQ4Ee609fto5wotHA" org.eventb.core.comment="The smart contract has emitted an event" org.eventb.core.generated="false" org.eventb.core.label="grd1" org.eventb.core.predicate="source_smart_contract ↦ emitted_event ∈ emitted_events" org.eventb.emf.persistence.emf_id="_WA6ZMfRlEe60CqkwWvstGA"/>
<org.eventb.core.guard name="_zpH6MMQ4Ee609fto5wotHA" 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="_WA6ZMvRlEe60CqkwWvstGA"/>
<org.eventb.core.guard name="_zpH6McQ4Ee609fto5wotHA" 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 ↦ pending_event ∉ gateway_pending_events" org.eventb.emf.persistence.emf_id="_WA6ZM_RlEe60CqkwWvstGA"/>
<org.eventb.core.parameter name="_WbZkYPRfEe60CqkwWvstGA" org.eventb.core.generated="false" org.eventb.core.identifier="emitted_event" org.eventb.emf.persistence.emf_id="_WA6ZL_RlEe60CqkwWvstGA"/>
<org.eventb.core.parameter name="_rW2qoPRfEe60CqkwWvstGA" org.eventb.core.generated="false" org.eventb.core.identifier="pending_event" org.eventb.emf.persistence.emf_id="_WA6ZMPRlEe60CqkwWvstGA"/>
<org.eventb.core.event name="_WGc9MPRhEe60CqkwWvstGA" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="SUBMIT_TX" org.eventb.emf.persistence.emf_id="_WA6ZPfRlEe60CqkwWvstGA">
<org.eventb.core.action name="_zpJIUMQ4Ee609fto5wotHA" org.eventb.core.assignment="received_target_transactions ≔ received_target_transactions ∪ {target_smart_contract ↦ transaction}" org.eventb.core.comment="The transaction is received by the target smart contract" org.eventb.core.generated="false" org.eventb.core.label="act1" org.eventb.emf.persistence.emf_id="_WA6ZO_RlEe60CqkwWvstGA"/>
<org.eventb.core.action name="_zpJvYMQ4Ee609fto5wotHA" org.eventb.core.assignment="gateway_pending_events ≔ gateway_pending_events ∖ {gateway ↦ pending_event}" org.eventb.core.comment="Remove the event from the pending events of the gateway" org.eventb.core.generated="false" org.eventb.core.label="act2" org.eventb.emf.persistence.emf_id="_WA6ZPPRlEe60CqkwWvstGA"/>
<org.eventb.core.guard name="_zpJvYcQ4Ee609fto5wotHA" org.eventb.core.comment="There is one pending event to be processed" org.eventb.core.generated="false" org.eventb.core.label="grd1" org.eventb.core.predicate="gateway ↦ pending_event ∈ gateway_pending_events" org.eventb.emf.persistence.emf_id="_WA6ZOfRlEe60CqkwWvstGA"/>
<org.eventb.core.guard name="_L7ASUPRgEe60CqkwWvstGA" org.eventb.core.generated="false" org.eventb.core.label="grd2" org.eventb.core.predicate="transaction ∈ TARGET_TRANSACTIONS" org.eventb.emf.persistence.emf_id="_WA6ZOvRlEe60CqkwWvstGA"/>
<org.eventb.core.parameter name="_rW3RsPRfEe60CqkwWvstGA" org.eventb.core.generated="false" org.eventb.core.identifier="pending_event" org.eventb.emf.persistence.emf_id="_WA6ZN_RlEe60CqkwWvstGA"/>
<org.eventb.core.parameter name="_AlhAwPRgEe60CqkwWvstGA" org.eventb.core.generated="false" org.eventb.core.identifier="transaction" org.eventb.emf.persistence.emf_id="_WA6ZOPRlEe60CqkwWvstGA"/>
<org.eventb.core.invariant name="_zpKWcMQ4Ee609fto5wotHA" org.eventb.core.generated="false" org.eventb.core.label="inv1" org.eventb.core.predicate="received_source_transactions ∈ CROSS_CHAIN_SMART_CONTRACTS ↔ SOURCE_TRANSACTIONS" org.eventb.emf.persistence.emf_id="_WA6ZFfRlEe60CqkwWvstGA"/>
<org.eventb.core.invariant name="_zpKWccQ4Ee609fto5wotHA" org.eventb.core.generated="false" org.eventb.core.label="inv2" org.eventb.core.predicate="emitted_events ∈ CROSS_CHAIN_SMART_CONTRACTS ↔ SMART_CONTRACT_EVENTS" org.eventb.emf.persistence.emf_id="_WA6ZFvRlEe60CqkwWvstGA"/>
<org.eventb.core.invariant name="_zpK9gMQ4Ee609fto5wotHA" 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="_WA6ZF_RlEe60CqkwWvstGA"/>
<org.eventb.core.invariant name="_zpK9gcQ4Ee609fto5wotHA" org.eventb.core.generated="false" org.eventb.core.label="inv4" org.eventb.core.predicate="gateway_pending_events ∈ GATEWAYS ↔ TARGET_TRANSACTIONS" org.eventb.emf.persistence.emf_id="_WA6ZGPRlEe60CqkwWvstGA"/>
<org.eventb.core.invariant name="_qTKs0MT7Ee609fto5wotHA" org.eventb.core.generated="false" org.eventb.core.label="inv5" org.eventb.core.predicate="received_target_transactions ∈ CROSS_CHAIN_SMART_CONTRACTS ↔ TARGET_TRANSACTIONS" org.eventb.emf.persistence.emf_id="_WA6ZGfRlEe60CqkwWvstGA"/>
<org.eventb.core.variable name="_ykmgMPReEe60CqkwWvstGA" org.eventb.core.generated="false" org.eventb.core.identifier="received_source_transactions" org.eventb.emf.persistence.emf_id="_WA6ZEPRlEe60CqkwWvstGA"/>
<org.eventb.core.variable name="_PlDdwPKVEe60CqkwWvstGA" org.eventb.core.generated="false" org.eventb.core.identifier="emitted_events" org.eventb.emf.persistence.emf_id="_WA6ZEfRlEe60CqkwWvstGA"/>
<org.eventb.core.variable name="_yREda77uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="subscriptions" org.eventb.emf.persistence.emf_id="_WA6ZEvRlEe60CqkwWvstGA"/>
<org.eventb.core.variable name="_fu8zYPRfEe60CqkwWvstGA" org.eventb.core.generated="false" org.eventb.core.identifier="gateway_pending_events" org.eventb.emf.persistence.emf_id="_WA6ZE_RlEe60CqkwWvstGA"/>
<org.eventb.core.variable name="_1yk4EPReEe60CqkwWvstGA" org.eventb.core.generated="false" org.eventb.core.identifier="received_target_transactions" org.eventb.emf.persistence.emf_id="_WA6ZFPRlEe60CqkwWvstGA"/>