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="_j63NnsBGEe6yC4BToIaAqA" org.eventb.texttools.text_lastmodified="1706711978585" org.eventb.texttools.text_representation="machine CCTx_Preserve_Balance_Gateway_m3 refines CCTx_Fabric_Ethereum_m2 sees CCTx_Fabric_Ethereum_c2 variables received_transactions triggered_events subscriptions gateway_pending_transactions received_cross_chain_transactions accounts estimated_cross_chain_cost invariants @inv31; estimated_cross_chain_cost ∈ ℕ events event INITIALISATION extends INITIALISATION then @act31; estimated_cross_chain_cost ≔ 0 end event SUBSCRIBE_SMART_CONTRACT_EVENTS_IN_FABRIC extends SUBSCRIBE_SMART_CONTRACT_EVENTS_IN_FABRIC end event INITIATE_CC_TX_IN_FABRIC extends INITIATE_CC_TX_IN_FABRIC end event TRIGGER_CC_TX_EVENT_IN_FABRIC extends TRIGGER_CC_TX_EVENT_IN_FABRIC end event LISTEN_CC_TX_EVENT_IN_FABRIC extends LISTEN_CC_TX_EVENT_IN_FABRIC end event SUBMIT_CC_TX_TO_ETHEREUM extends SUBMIT_CC_TX_TO_ETHEREUM where @grd31; fee ≤ estimated_cross_chain_cost // Check that the estimated fee is greater or equal to the validators fee (RQ2) end event CREATE_ADDRESS_IN_ETHEREUM extends CREATE_ADDRESS_IN_ETHEREUM end event DEPOSIT_CRYPTOCURRENCY_IN_ETHEREUM extends DEPOSIT_CRYPTOCURRENCY_IN_ETHEREUM where @grd31; address ≠ gateway_address // The gateway cannot deposit in its own account (RQ3) end event SUBMIT_TRANSFER_TRANSACTION_IN_ETHEREUM extends SUBMIT_TRANSFER_TRANSACTION_IN_ETHEREUM then @act31; estimated_cross_chain_cost ≔ transfer_amount end end" version="5">
<org.eventb.core.refinesMachine name="'" org.eventb.core.target="CCTx_Fabric_Ethereum_m2"/>
<org.eventb.core.seesContext name="_8rq0TL7uEe6laZimEYihUg" org.eventb.core.target="CCTx_Fabric_Ethereum_c2"/>
<org.eventb.core.event name="_ZAfKoMBGEe6yC4BToIaAqA" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="LISTEN_CC_TX_EVENT_IN_FABRIC" org.eventb.emf.persistence.emf_id="_j63NkcBGEe6yC4BToIaAqA">
<org.eventb.core.refinesEvent name="_ZAfKocBGEe6yC4BToIaAqA" org.eventb.core.target="LISTEN_CC_TX_EVENT_IN_FABRIC"/>
<org.eventb.core.event name="_j630sMBGEe6yC4BToIaAqA" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="SUBMIT_CC_TX_TO_ETHEREUM" org.eventb.emf.persistence.emf_id="_j63NlMBGEe6yC4BToIaAqA">
<org.eventb.core.refinesEvent name="_j630scBGEe6yC4BToIaAqA" org.eventb.core.target="SUBMIT_CC_TX_TO_ETHEREUM"/>
<org.eventb.core.guard name="_BvYlyL7vEe6laZimEYihUg" org.eventb.core.comment="Check that the estimated fee is greater or equal to the validators fee (RQ2)" org.eventb.core.generated="false" org.eventb.core.label="grd31;" org.eventb.core.predicate="fee ≤ estimated_cross_chain_cost" org.eventb.emf.persistence.emf_id="_j63Nk8BGEe6yC4BToIaAqA"/>
<org.eventb.core.event name="_yREdbb7uEe6laZimEYihUn" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="CREATE_ADDRESS_IN_ETHEREUM" org.eventb.emf.persistence.emf_id="_j63NlsBGEe6yC4BToIaAqA">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="CREATE_ADDRESS_IN_ETHEREUM"/>
</org.eventb.core.event>
<org.eventb.core.event name="_yREdbb7uEe6laZimEYihUo" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="DEPOSIT_CRYPTOCURRENCY_IN_ETHEREUM" org.eventb.emf.persistence.emf_id="_j63NmcBGEe6yC4BToIaAqA">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="DEPOSIT_CRYPTOCURRENCY_IN_ETHEREUM"/>
<org.eventb.core.guard name="_BvYlyb7vEe6laZimEYihUg" org.eventb.core.comment="The gateway cannot deposit in its own account (RQ3)" org.eventb.core.generated="false" org.eventb.core.label="grd31;" org.eventb.core.predicate="address ≠ gateway_address" org.eventb.emf.persistence.emf_id="_j63NmMBGEe6yC4BToIaAqA"/>
</org.eventb.core.event>
<org.eventb.core.event name="_yREdbb7uEe6laZimEYihUp" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="SUBMIT_TRANSFER_TRANSACTION_IN_ETHEREUM" org.eventb.emf.persistence.emf_id="_j63NnMBGEe6yC4BToIaAqA">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="SUBMIT_TRANSFER_TRANSACTION_IN_ETHEREUM"/>
<org.eventb.core.action name="_BvYlx77vEe6laZimEYihUg" org.eventb.core.assignment="estimated_cross_chain_cost ≔ transfer_amount" org.eventb.core.generated="false" org.eventb.core.label="act31;" org.eventb.emf.persistence.emf_id="_j63Nm8BGEe6yC4BToIaAqA"/>
</org.eventb.core.event>
<org.eventb.core.invariant name="_BvYlxr7vEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.label="inv31;" org.eventb.core.predicate="estimated_cross_chain_cost ∈ ℕ" org.eventb.emf.persistence.emf_id="_j63Nh8BGEe6yC4BToIaAqA"/>
<org.eventb.core.variable name="_yREdab7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="received_transactions" org.eventb.emf.persistence.emf_id="_j63NgMBGEe6yC4BToIaAqA"/>
<org.eventb.core.variable name="_yREdar7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="triggered_events" org.eventb.emf.persistence.emf_id="_j63NgcBGEe6yC4BToIaAqA"/>
<org.eventb.core.variable name="_yREda77uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="subscriptions" org.eventb.emf.persistence.emf_id="_j63NgsBGEe6yC4BToIaAqA"/>
<org.eventb.core.variable name="_yREdbL7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="gateway_pending_transactions" org.eventb.emf.persistence.emf_id="_j63Ng8BGEe6yC4BToIaAqA"/>
<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="_j63NhMBGEe6yC4BToIaAqA"/>
<org.eventb.core.variable name="_8rz-D77uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="accounts" org.eventb.emf.persistence.emf_id="_j63NhcBGEe6yC4BToIaAqA"/>
<org.eventb.core.event name="_yREdbb7uEe6laZimEYihUh" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="INITIALISATION" org.eventb.emf.persistence.emf_id="_j63NicBGEe6yC4BToIaAqA">
<org.eventb.core.action name="_BvYlxb7vEe6laZimEYihUg" org.eventb.core.assignment="estimated_cross_chain_cost ≔ 0" org.eventb.core.generated="false" org.eventb.core.label="act31;" org.eventb.emf.persistence.emf_id="_j63NiMBGEe6yC4BToIaAqA"/>
</org.eventb.core.event>
<org.eventb.core.event name="_yREdbb7uEe6laZimEYihUi" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="SUBSCRIBE_SMART_CONTRACT_EVENTS_IN_FABRIC" org.eventb.emf.persistence.emf_id="_j63Ni8BGEe6yC4BToIaAqA">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="SUBSCRIBE_SMART_CONTRACT_EVENTS_IN_FABRIC"/>
</org.eventb.core.event>
<org.eventb.core.event name="_4AD2oMBFEe6yC4BToIaAqA" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="INITIATE_CC_TX_IN_FABRIC" org.eventb.emf.persistence.emf_id="_j63NjcBGEe6yC4BToIaAqA">
<org.eventb.core.refinesEvent name="_4AD2ocBFEe6yC4BToIaAqA" org.eventb.core.target="INITIATE_CC_TX_IN_FABRIC"/>
</org.eventb.core.event>
<org.eventb.core.event name="_Jp9FgMBGEe6yC4BToIaAqA" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="TRIGGER_CC_TX_EVENT_IN_FABRIC" org.eventb.emf.persistence.emf_id="_j63Nj8BGEe6yC4BToIaAqA">
<org.eventb.core.refinesEvent name="_Jp9FgcBGEe6yC4BToIaAqA" org.eventb.core.target="TRIGGER_CC_TX_EVENT_IN_FABRIC"/>
<org.eventb.core.variable name="_BvYlyr7vEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="estimated_cross_chain_cost" org.eventb.emf.persistence.emf_id="_j63NhsBGEe6yC4BToIaAqA"/>
</org.eventb.core.machineFile>