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="_559ZqKvjEe6I4bA9GxwhqQ" org.eventb.texttools.text_lastmodified="1704470582699" org.eventb.texttools.text_representation="machine BIG_m1 sees BIG_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 SUBMIT_CROSS_CHAIN_TRANSACTION 	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 PROCESS_CROSS_CHAIN_TRANSACTION 	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_SMART_CONTRACT_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 GATEWAY_PROCESS_CROSS_CHAIN_TRANSACTION 	any cross_chain_transaction 	when 		@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="_sUpukKl_Ee6I4bA9GxwhqQ" org.eventb.core.target="BIG_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="_558yj6vjEe6I4bA9GxwhqQ">
<org.eventb.core.action name="_SAxOQKmDEe6I4bA9GxwhqQ" org.eventb.core.assignment="received_transactions ≔ ∅" org.eventb.core.generated="false" org.eventb.core.label="act1;" org.eventb.emf.persistence.emf_id="_558yiqvjEe6I4bA9GxwhqQ"/>
<org.eventb.core.action name="_TlWCkamHEe6I4bA9GxwhqQ" org.eventb.core.assignment="triggered_events ≔ ∅" org.eventb.core.generated="false" org.eventb.core.label="act2;" org.eventb.emf.persistence.emf_id="_558yi6vjEe6I4bA9GxwhqQ"/>
<org.eventb.core.action name="_mv5M0KpAEe6I4bA9GxwhqQ" org.eventb.core.assignment="subscriptions ≔ ∅" org.eventb.core.generated="false" org.eventb.core.label="act3;" org.eventb.emf.persistence.emf_id="_558yjKvjEe6I4bA9GxwhqQ"/>
<org.eventb.core.action name="_8Ty9sKpBEe6I4bA9GxwhqQ" org.eventb.core.assignment="gateway_pending_transactions ≔ ∅" org.eventb.core.generated="false" org.eventb.core.label="act4;" org.eventb.emf.persistence.emf_id="_558yjavjEe6I4bA9GxwhqQ"/>
<org.eventb.core.action name="_J6KjYKpbEe6I4bA9GxwhqQ" org.eventb.core.assignment="received_cross_chain_transactions ≔ ∅" org.eventb.core.generated="false" org.eventb.core.label="act6;" org.eventb.emf.persistence.emf_id="_558yjqvjEe6I4bA9GxwhqQ"/>
<org.eventb.core.event name="_I9G5gKpAEe6I4bA9GxwhqQ" 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="_558ykqvjEe6I4bA9GxwhqQ">
<org.eventb.core.action name="_a_IQYKmDEe6I4bA9GxwhqQ" 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="_558ykavjEe6I4bA9GxwhqQ"/>
<org.eventb.core.guard name="_SAx1UKmDEe6I4bA9GxwhqQ" 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="_558ykKvjEe6I4bA9GxwhqQ"/>
<org.eventb.core.event name="_58YTEKmAEe6I4bA9GxwhqQ" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="SUBMIT_CROSS_CHAIN_TRANSACTION" org.eventb.emf.persistence.emf_id="_559Zk6vjEe6I4bA9GxwhqQ">
<org.eventb.core.action name="_AeyzAKmIEe6I4bA9GxwhqQ" 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="_559ZkqvjEe6I4bA9GxwhqQ"/>
<org.eventb.core.guard name="_TlWCkqmHEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.label="grd1;" org.eventb.core.predicate="transaction ∈ TRANSACTIONS" org.eventb.emf.persistence.emf_id="_559ZkKvjEe6I4bA9GxwhqQ"/>
<org.eventb.core.guard name="_HCtL8KmIEe6I4bA9GxwhqQ" 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="_559ZkavjEe6I4bA9GxwhqQ"/>
<org.eventb.core.parameter name="_SAx1UqmDEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="transaction" org.eventb.emf.persistence.emf_id="_558yk6vjEe6I4bA9GxwhqQ"/>
<org.eventb.core.event name="_TlWCkKmHEe6I4bA9GxwhqQ" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="PROCESS_CROSS_CHAIN_TRANSACTION" org.eventb.emf.persistence.emf_id="_559ZmqvjEe6I4bA9GxwhqQ">
<org.eventb.core.action name="_I9G5gapAEe6I4bA9GxwhqQ" 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="_559ZmKvjEe6I4bA9GxwhqQ"/>
<org.eventb.core.action name="_gaDEIKmHEe6I4bA9GxwhqQ" 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="_559ZmavjEe6I4bA9GxwhqQ"/>
<org.eventb.core.guard name="_iUmtQKpAEe6I4bA9GxwhqQ" 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="_559ZlqvjEe6I4bA9GxwhqQ"/>
<org.eventb.core.guard name="_1SOwwKmDEe6I4bA9GxwhqQ" 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="_559Zl6vjEe6I4bA9GxwhqQ"/>
<org.eventb.core.parameter name="_TlWCk6mHEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="transaction" org.eventb.emf.persistence.emf_id="_559ZlKvjEe6I4bA9GxwhqQ"/>
<org.eventb.core.parameter name="_AezaEamIEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="cross_chain_event" org.eventb.emf.persistence.emf_id="_559ZlavjEe6I4bA9GxwhqQ"/>
<org.eventb.core.event name="_8VKFEKpAEe6I4bA9GxwhqQ" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="LISTEN_SMART_CONTRACT_EVENT" org.eventb.emf.persistence.emf_id="_559ZoqvjEe6I4bA9GxwhqQ">
<org.eventb.core.action name="_8T0y4KpBEe6I4bA9GxwhqQ" 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="_559ZoKvjEe6I4bA9GxwhqQ"/>
<org.eventb.core.action name="_NAy78KpBEe6I4bA9GxwhqQ" 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="_559ZoavjEe6I4bA9GxwhqQ"/>
<org.eventb.core.guard name="_DMOGsKpFEe6I4bA9GxwhqQ" 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="_559ZnavjEe6I4bA9GxwhqQ"/>
<org.eventb.core.guard name="_AezaEKmIEe6I4bA9GxwhqQ" 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="_559ZnqvjEe6I4bA9GxwhqQ"/>
<org.eventb.core.guard name="_x51DwKpCEe6I4bA9GxwhqQ" 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="_559Zn6vjEe6I4bA9GxwhqQ"/>
<org.eventb.core.parameter name="_8VKsIqpAEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="cross_chain_event" org.eventb.emf.persistence.emf_id="_559Zm6vjEe6I4bA9GxwhqQ"/>
<org.eventb.core.parameter name="_8T1Z8qpBEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="cross_chain_transaction" org.eventb.emf.persistence.emf_id="_559ZnKvjEe6I4bA9GxwhqQ"/>
<org.eventb.core.event name="_0sEN8KpaEe6I4bA9GxwhqQ" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="GATEWAY_PROCESS_CROSS_CHAIN_TRANSACTION" org.eventb.emf.persistence.emf_id="_559Zp6vjEe6I4bA9GxwhqQ">
<org.eventb.core.action name="_G1dcQKpbEe6I4bA9GxwhqQ" 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="_559ZpavjEe6I4bA9GxwhqQ"/>
<org.eventb.core.action name="_G1dcQapbEe6I4bA9GxwhqQ" 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="_559ZpqvjEe6I4bA9GxwhqQ"/>
<org.eventb.core.guard name="_tUzFcKpaEe6I4bA9GxwhqQ" 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="_559ZpKvjEe6I4bA9GxwhqQ"/>
<org.eventb.core.parameter name="_tUzFcapaEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="cross_chain_transaction" org.eventb.emf.persistence.emf_id="_559Zo6vjEe6I4bA9GxwhqQ"/>
<org.eventb.core.invariant name="_o6juoKviEe6I4bA9GxwhqQ" 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="_558yhavjEe6I4bA9GxwhqQ"/>
<org.eventb.core.invariant name="_d6dcQKmHEe6I4bA9GxwhqQ" 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="_558yhqvjEe6I4bA9GxwhqQ"/>
<org.eventb.core.invariant name="_Q6dKkKpAEe6I4bA9GxwhqQ" 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="_558yh6vjEe6I4bA9GxwhqQ"/>
<org.eventb.core.invariant name="_c7TQ0KpBEe6I4bA9GxwhqQ" 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="_558yiKvjEe6I4bA9GxwhqQ"/>
<org.eventb.core.invariant name="_G1eDUKpbEe6I4bA9GxwhqQ" 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="_558yiavjEe6I4bA9GxwhqQ"/>
<org.eventb.core.variable name="_SAycYamDEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="received_transactions" org.eventb.emf.persistence.emf_id="_558ygKvjEe6I4bA9GxwhqQ"/>
<org.eventb.core.variable name="_YvZFkamHEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="triggered_events" org.eventb.emf.persistence.emf_id="_558ygavjEe6I4bA9GxwhqQ"/>
<org.eventb.core.variable name="_I9HgkapAEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="subscriptions" org.eventb.emf.persistence.emf_id="_558ygqvjEe6I4bA9GxwhqQ"/>
<org.eventb.core.variable name="_8T2BAKpBEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="gateway_pending_transactions" org.eventb.emf.persistence.emf_id="_558yg6vjEe6I4bA9GxwhqQ"/>
<org.eventb.core.variable name="_H2zkgKpbEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="received_cross_chain_transactions" org.eventb.emf.persistence.emf_id="_558yhKvjEe6I4bA9GxwhqQ"/>