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="_9LSDvvRhEe60CqkwWvstGA" org.eventb.texttools.text_lastmodified="1712441204955" org.eventb.texttools.text_representation="machine CCTx_Preserve_Balance_Gateway_m3 refines CCTx_Fabric_Ethereum_m2 sees CCTx_Fabric_Ethereum_c2 variables received_source_transactions emitted_events subscriptions gateway_pending_events received_target_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 EMIT_EVENT_IN_FABRIC extends EMIT_EVENT_IN_FABRIC end event LISTEN_EVENT_IN_FABRIC extends LISTEN_EVENT_IN_FABRIC end event SUBMIT_TX_TO_ETHEREUM extends SUBMIT_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="_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="_9LSDqfRhEe60CqkwWvstGA">
<org.eventb.core.action name="_ySjRNsTuEe609fto5wotHA" 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="_9LSDqPRhEe60CqkwWvstGA"/>
</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="_9LSDq_RhEe60CqkwWvstGA">
<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="_9LSDrfRhEe60CqkwWvstGA">
<org.eventb.core.refinesEvent name="_4AD2ocBFEe6yC4BToIaAqA" org.eventb.core.target="INITIATE_CC_TX_IN_FABRIC"/>
</org.eventb.core.event>
<org.eventb.core.event name="_9LbNkPRhEe60CqkwWvstGA" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="EMIT_EVENT_IN_FABRIC" org.eventb.emf.persistence.emf_id="_9LSDr_RhEe60CqkwWvstGA">
<org.eventb.core.refinesEvent name="_9LbNkfRhEe60CqkwWvstGA" org.eventb.core.target="EMIT_EVENT_IN_FABRIC"/>
<org.eventb.core.event name="_9LbNkvRhEe60CqkwWvstGA" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="LISTEN_EVENT_IN_FABRIC" org.eventb.emf.persistence.emf_id="_9LSDsfRhEe60CqkwWvstGA">
<org.eventb.core.refinesEvent name="_9Lb0oPRhEe60CqkwWvstGA" org.eventb.core.target="LISTEN_EVENT_IN_FABRIC"/>
<org.eventb.core.event name="_9Lb0ofRhEe60CqkwWvstGA" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="SUBMIT_TX_TO_ETHEREUM" org.eventb.emf.persistence.emf_id="_9LSDtPRhEe60CqkwWvstGA">
<org.eventb.core.refinesEvent name="_9Lb0ovRhEe60CqkwWvstGA" org.eventb.core.target="SUBMIT_TX_TO_ETHEREUM"/>
<org.eventb.core.guard name="_ySjRNMTuEe609fto5wotHA" 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="_9LSDs_RhEe60CqkwWvstGA"/>
<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="_9LSDtvRhEe60CqkwWvstGA">
<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="_9LSDufRhEe60CqkwWvstGA">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="DEPOSIT_CRYPTOCURRENCY_IN_ETHEREUM"/>
<org.eventb.core.guard name="_ySjRNcTuEe609fto5wotHA" 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="_9LSDuPRhEe60CqkwWvstGA"/>
</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="_9LSDvPRhEe60CqkwWvstGA">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="SUBMIT_TRANSFER_TRANSACTION_IN_ETHEREUM"/>
<org.eventb.core.action name="_ySsbEMTuEe609fto5wotHA" 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="_9LSDu_RhEe60CqkwWvstGA"/>
</org.eventb.core.event>
<org.eventb.core.invariant name="_ySjRN8TuEe609fto5wotHA" org.eventb.core.generated="false" org.eventb.core.label="inv31" org.eventb.core.predicate="estimated_cross_chain_cost ∈ ℕ" org.eventb.emf.persistence.emf_id="_9LSDp_RhEe60CqkwWvstGA"/>
<org.eventb.core.variable name="_4g-GEPRgEe60CqkwWvstGA" org.eventb.core.generated="false" org.eventb.core.identifier="received_source_transactions" org.eventb.emf.persistence.emf_id="_9LSDoPRhEe60CqkwWvstGA"/>
<org.eventb.core.variable name="_lV7wYPKVEe60CqkwWvstGA" org.eventb.core.generated="false" org.eventb.core.identifier="emitted_events" org.eventb.emf.persistence.emf_id="_9LSDofRhEe60CqkwWvstGA"/>
<org.eventb.core.variable name="_yREda77uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="subscriptions" org.eventb.emf.persistence.emf_id="_9LSDovRhEe60CqkwWvstGA"/>
<org.eventb.core.variable name="_4g-tIPRgEe60CqkwWvstGA" org.eventb.core.generated="false" org.eventb.core.identifier="gateway_pending_events" org.eventb.emf.persistence.emf_id="_9LSDo_RhEe60CqkwWvstGA"/>
<org.eventb.core.variable name="_4g-tIfRgEe60CqkwWvstGA" org.eventb.core.generated="false" org.eventb.core.identifier="received_target_transactions" org.eventb.emf.persistence.emf_id="_9LSDpPRhEe60CqkwWvstGA"/>
<org.eventb.core.variable name="_8rz-D77uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="accounts" org.eventb.emf.persistence.emf_id="_9LSDpfRhEe60CqkwWvstGA"/>
<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="_9LSDpvRhEe60CqkwWvstGA"/>
</org.eventb.core.machineFile>