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="_5cjvXfRhEe60CqkwWvstGA" org.eventb.texttools.text_lastmodified="1712441179924" org.eventb.texttools.text_representation="machine CCTx_Fabric_Ethereum_Animation_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 subscribed initiated emitted gateway_processing submit_cc_tx wallet_created wallet_amount invariants 	@inv31 subscribed ∈ {0,1} 	@inv32 initiated ∈ {0,1} 	@inv33 emitted ∈ {0,1} 	@inv34 gateway_processing ∈ {0,1} 	@inv35 submit_cc_tx ∈ {0,1} 	@inv36 wallet_created ∈ {0,1} 	@inv37 wallet_amount ∈ ℕ events event INITIALISATION extends INITIALISATION 	then 		@init_subscribed 		 subscribed ≔ 0 		@init_initiated 		 initiated ≔ 0 		@init_emitted 		 	 emitted ≔ 0 		@init_gateway_processing gateway_processing ≔ 0 		@init_submit_cc_tx 		 submit_cc_tx ≔ 0 		@init_wallet_created	 wallet_created ≔ 0 		@init_wallet_amount		 wallet_amount ≔ 0 end event SUBSCRIBE_SMART_CONTRACT_EVENTS_IN_FABRIC extends SUBSCRIBE_SMART_CONTRACT_EVENTS_IN_FABRIC 	then 		@act111 subscribed ≔ 1 end event INITIATE_CC_TX_IN_FABRIC extends INITIATE_CC_TX_IN_FABRIC 	then 		@act31 initiated ≔ 1 		@act32 submit_cc_tx ≔ 0 end event EMIT_EVENT_IN_FABRIC extends EMIT_EVENT_IN_FABRIC 	then 		@act31 emitted ≔ 1 		@act32 initiated ≔ 0 		@act33 submit_cc_tx ≔ 0 end event LISTEN_EVENT_IN_FABRIC extends LISTEN_EVENT_IN_FABRIC then 		@act31 gateway_processing ≔ 1 		@act32 emitted ≔ 0 		@act33 submit_cc_tx ≔ 0 end event SUBMIT_TX_TO_ETHEREUM extends SUBMIT_TX_TO_ETHEREUM 	then 		@act31 submit_cc_tx ≔ 1 		@act32 gateway_processing ≔ 0 		@act33 wallet_amount ≔ accounts(gateway_address) − fee end event CREATE_ADDRESS_IN_ETHEREUM // Users can create their address on Ethereum (RQ1 and RQ2) extends CREATE_ADDRESS_IN_ETHEREUM 	when 		@grd31 address = gateway_address 	then 		@act31 wallet_created ≔ 1 end event DEPOSIT_CRYPTOCURRENCY_IN_ETHEREUM // Users (including the gateway) can deposit Ethers on their address (RQ3) extends DEPOSIT_CRYPTOCURRENCY_IN_ETHEREUM 	then 		@act31 wallet_amount ≔ accounts(address) + amount 		@act32 submit_cc_tx ≔ 0 end event SUBMIT_TRANSFER_TRANSACTION_IN_ETHEREUM // The user can transfer an estimated fee to the gateways account (RQ1) extends SUBMIT_TRANSFER_TRANSACTION_IN_ETHEREUM 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="_5cjvO_RhEe60CqkwWvstGA">
<org.eventb.core.action name="_Xag6AMEEEe6yC4BToIaAqA" org.eventb.core.assignment="subscribed ≔ 0" org.eventb.core.generated="false" org.eventb.core.label="init_subscribed" org.eventb.emf.persistence.emf_id="_5cjvNPRhEe60CqkwWvstGA"/>
<org.eventb.core.action name="_XahhEMEEEe6yC4BToIaAqA" org.eventb.core.assignment="initiated ≔ 0" org.eventb.core.generated="false" org.eventb.core.label="init_initiated" org.eventb.emf.persistence.emf_id="_5cjvNfRhEe60CqkwWvstGA"/>
<org.eventb.core.action name="_ZQ-UAPKWEe60CqkwWvstGA" org.eventb.core.assignment="emitted ≔ 0" org.eventb.core.generated="false" org.eventb.core.label="init_emitted" org.eventb.emf.persistence.emf_id="_5cjvNvRhEe60CqkwWvstGA"/>
<org.eventb.core.action name="_XahhEsEEEe6yC4BToIaAqA" org.eventb.core.assignment="gateway_processing ≔ 0" org.eventb.core.generated="false" org.eventb.core.label="init_gateway_processing" org.eventb.emf.persistence.emf_id="_5cjvN_RhEe60CqkwWvstGA"/>
<org.eventb.core.action name="_XahhE8EEEe6yC4BToIaAqA" org.eventb.core.assignment="submit_cc_tx ≔ 0" org.eventb.core.generated="false" org.eventb.core.label="init_submit_cc_tx" org.eventb.emf.persistence.emf_id="_5cjvOPRhEe60CqkwWvstGA"/>
<org.eventb.core.action name="_y69sYMEGEe6yC4BToIaAqA" org.eventb.core.assignment="wallet_created ≔ 0" org.eventb.core.generated="false" org.eventb.core.label="init_wallet_created" org.eventb.emf.persistence.emf_id="_5cjvOfRhEe60CqkwWvstGA"/>
<org.eventb.core.action name="_BKVfsMEIEe6yC4BToIaAqA" org.eventb.core.assignment="wallet_amount ≔ 0" org.eventb.core.generated="false" org.eventb.core.label="init_wallet_amount" org.eventb.emf.persistence.emf_id="_5cjvOvRhEe60CqkwWvstGA"/>
<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="_5cjvPvRhEe60CqkwWvstGA">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="SUBSCRIBE_SMART_CONTRACT_EVENTS_IN_FABRIC"/>
<org.eventb.core.action name="_hvM14MEEEe6yC4BToIaAqA" org.eventb.core.assignment="subscribed ≔ 1" org.eventb.core.generated="false" org.eventb.core.label="act111" org.eventb.emf.persistence.emf_id="_5cjvPfRhEe60CqkwWvstGA"/>
<org.eventb.core.event name="_yREdbb7uEe6laZimEYihUj" 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="_5cjvQvRhEe60CqkwWvstGA">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="INITIATE_CC_TX_IN_FABRIC"/>
<org.eventb.core.action name="_kp_MAMEEEe6yC4BToIaAqA" org.eventb.core.assignment="initiated ≔ 1" org.eventb.core.generated="false" org.eventb.core.label="act31" org.eventb.emf.persistence.emf_id="_5cjvQPRhEe60CqkwWvstGA"/>
<org.eventb.core.action name="_kqAaIMEEEe6yC4BToIaAqA" org.eventb.core.assignment="submit_cc_tx ≔ 0" org.eventb.core.generated="false" org.eventb.core.label="act32" org.eventb.emf.persistence.emf_id="_5cjvQfRhEe60CqkwWvstGA"/>
<org.eventb.core.event name="_5dHIwPRhEe60CqkwWvstGA" 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="_5cjvR_RhEe60CqkwWvstGA">
<org.eventb.core.refinesEvent name="_5dHIwfRhEe60CqkwWvstGA" org.eventb.core.target="EMIT_EVENT_IN_FABRIC"/>
<org.eventb.core.action name="_kp_zEMEEEe6yC4BToIaAqA" org.eventb.core.assignment="emitted ≔ 1" org.eventb.core.generated="false" org.eventb.core.label="act31" org.eventb.emf.persistence.emf_id="_5cjvRPRhEe60CqkwWvstGA"/>
<org.eventb.core.action name="_kqBoQMEEEe6yC4BToIaAqA" org.eventb.core.assignment="initiated ≔ 0" org.eventb.core.generated="false" org.eventb.core.label="act32" org.eventb.emf.persistence.emf_id="_5cjvRfRhEe60CqkwWvstGA"/>
<org.eventb.core.action name="_y9WKoMEJEe6yC4BToIaAqA" org.eventb.core.assignment="submit_cc_tx ≔ 0" org.eventb.core.generated="false" org.eventb.core.label="act33" org.eventb.emf.persistence.emf_id="_5cjvRvRhEe60CqkwWvstGA"/>
<org.eventb.core.event name="_5dHv0PRhEe60CqkwWvstGA" 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="_5cjvTPRhEe60CqkwWvstGA">
<org.eventb.core.refinesEvent name="_5dHv0fRhEe60CqkwWvstGA" org.eventb.core.target="LISTEN_EVENT_IN_FABRIC"/>
<org.eventb.core.action name="_kqBBMMEEEe6yC4BToIaAqA" org.eventb.core.assignment="gateway_processing ≔ 1" org.eventb.core.generated="false" org.eventb.core.label="act31" org.eventb.emf.persistence.emf_id="_5cjvSfRhEe60CqkwWvstGA"/>
<org.eventb.core.action name="_pHPaccEEEe6yC4BToIaAqA" org.eventb.core.assignment="emitted ≔ 0" org.eventb.core.generated="false" org.eventb.core.label="act32" org.eventb.emf.persistence.emf_id="_5cjvSvRhEe60CqkwWvstGA"/>
<org.eventb.core.action name="_EcXw0MELEe6yC4BToIaAqA" org.eventb.core.assignment="submit_cc_tx ≔ 0" org.eventb.core.generated="false" org.eventb.core.label="act33" org.eventb.emf.persistence.emf_id="_5cjvS_RhEe60CqkwWvstGA"/>
<org.eventb.core.event name="_5dIW4PRhEe60CqkwWvstGA" 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="_5cjvUfRhEe60CqkwWvstGA">
<org.eventb.core.refinesEvent name="_5dIW4fRhEe60CqkwWvstGA" org.eventb.core.target="SUBMIT_TX_TO_ETHEREUM"/>
<org.eventb.core.action name="_pHPacMEEEe6yC4BToIaAqA" org.eventb.core.assignment="submit_cc_tx ≔ 1" org.eventb.core.generated="false" org.eventb.core.label="act31" org.eventb.emf.persistence.emf_id="_5cjvTvRhEe60CqkwWvstGA"/>
<org.eventb.core.action name="_EcY-8MELEe6yC4BToIaAqA" org.eventb.core.assignment="gateway_processing ≔ 0" org.eventb.core.generated="false" org.eventb.core.label="act32" org.eventb.emf.persistence.emf_id="_5cjvT_RhEe60CqkwWvstGA"/>
<org.eventb.core.action name="_EcZmAMELEe6yC4BToIaAqA" org.eventb.core.assignment="wallet_amount ≔ accounts(gateway_address) − fee" org.eventb.core.generated="false" org.eventb.core.label="act33" org.eventb.emf.persistence.emf_id="_5cjvUPRhEe60CqkwWvstGA"/>
<org.eventb.core.event name="_yREdbb7uEe6laZimEYihUn" org.eventb.core.comment="Users can create their address on Ethereum (RQ1 and RQ2)" 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="_5cjvVfRhEe60CqkwWvstGA">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="CREATE_ADDRESS_IN_ETHEREUM"/>
<org.eventb.core.action name="_qWM2AMEGEe6yC4BToIaAqA" org.eventb.core.assignment="wallet_created ≔ 1" org.eventb.core.generated="false" org.eventb.core.label="act31" org.eventb.emf.persistence.emf_id="_5cjvVPRhEe60CqkwWvstGA"/>
<org.eventb.core.guard name="_wieyEMEGEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.label="grd31" org.eventb.core.predicate="address = gateway_address" org.eventb.emf.persistence.emf_id="_5cjvU_RhEe60CqkwWvstGA"/>
<org.eventb.core.event name="_yREdbb7uEe6laZimEYihUo" org.eventb.core.comment="Users (including the gateway) can deposit Ethers on their address (RQ3)" 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="_5cjvWfRhEe60CqkwWvstGA">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="DEPOSIT_CRYPTOCURRENCY_IN_ETHEREUM"/>
<org.eventb.core.action name="_7CFvEMEHEe6yC4BToIaAqA" org.eventb.core.assignment="wallet_amount ≔ accounts(address) + amount" org.eventb.core.generated="false" org.eventb.core.label="act31" org.eventb.emf.persistence.emf_id="_5cjvV_RhEe60CqkwWvstGA"/>
<org.eventb.core.action name="_FU5CUMENEe6yC4BToIaAqA" org.eventb.core.assignment="submit_cc_tx ≔ 0" org.eventb.core.generated="false" org.eventb.core.label="act32" org.eventb.emf.persistence.emf_id="_5cjvWPRhEe60CqkwWvstGA"/>
<org.eventb.core.event name="_yREdbb7uEe6laZimEYihUp" org.eventb.core.comment="The user can transfer an estimated fee to the gateways account (RQ1)" 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="_5cjvW_RhEe60CqkwWvstGA">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="SUBMIT_TRANSFER_TRANSACTION_IN_ETHEREUM"/>
</org.eventb.core.event>
<org.eventb.core.invariant name="_qWNdEMEGEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.label="inv31" org.eventb.core.predicate="subscribed ∈ {0,1}" org.eventb.emf.persistence.emf_id="_5cjvLfRhEe60CqkwWvstGA"/>
<org.eventb.core.invariant name="_qWNdEcEGEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.label="inv32" org.eventb.core.predicate="initiated ∈ {0,1}" org.eventb.emf.persistence.emf_id="_5cjvLvRhEe60CqkwWvstGA"/>
<org.eventb.core.invariant name="_qWNdEsEGEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.label="inv33" org.eventb.core.predicate="emitted ∈ {0,1}" org.eventb.emf.persistence.emf_id="_5cjvL_RhEe60CqkwWvstGA"/>
<org.eventb.core.invariant name="_qWNdE8EGEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.label="inv34" org.eventb.core.predicate="gateway_processing ∈ {0,1}" org.eventb.emf.persistence.emf_id="_5cjvMPRhEe60CqkwWvstGA"/>
<org.eventb.core.invariant name="_qWNdFMEGEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.label="inv35" org.eventb.core.predicate="submit_cc_tx ∈ {0,1}" org.eventb.emf.persistence.emf_id="_5cjvMfRhEe60CqkwWvstGA"/>
<org.eventb.core.invariant name="_qWOEIMEGEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.label="inv36" org.eventb.core.predicate="wallet_created ∈ {0,1}" org.eventb.emf.persistence.emf_id="_5cjvMvRhEe60CqkwWvstGA"/>
<org.eventb.core.invariant name="_9cXZIMEHEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.label="inv37" org.eventb.core.predicate="wallet_amount ∈ ℕ" org.eventb.emf.persistence.emf_id="_5cjvM_RhEe60CqkwWvstGA"/>
<org.eventb.core.variable name="_2ZLTIPRgEe60CqkwWvstGA" org.eventb.core.generated="false" org.eventb.core.identifier="received_source_transactions" org.eventb.emf.persistence.emf_id="_5cjvIPRhEe60CqkwWvstGA"/>
<org.eventb.core.variable name="_cNBD0PKVEe60CqkwWvstGA" org.eventb.core.generated="false" org.eventb.core.identifier="emitted_events" org.eventb.emf.persistence.emf_id="_5cjvIfRhEe60CqkwWvstGA"/>
<org.eventb.core.variable name="_yREda77uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="subscriptions" org.eventb.emf.persistence.emf_id="_5cjvIvRhEe60CqkwWvstGA"/>
<org.eventb.core.variable name="_2ZLTIfRgEe60CqkwWvstGA" org.eventb.core.generated="false" org.eventb.core.identifier="gateway_pending_events" org.eventb.emf.persistence.emf_id="_5cjvI_RhEe60CqkwWvstGA"/>
<org.eventb.core.variable name="_2ZLTIvRgEe60CqkwWvstGA" org.eventb.core.generated="false" org.eventb.core.identifier="received_target_transactions" org.eventb.emf.persistence.emf_id="_5cjvJPRhEe60CqkwWvstGA"/>
<org.eventb.core.variable name="_8rz-D77uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="accounts" org.eventb.emf.persistence.emf_id="_5cjvJfRhEe60CqkwWvstGA"/>
<org.eventb.core.variable name="_LY0pwMEEEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.identifier="subscribed" org.eventb.emf.persistence.emf_id="_5cjvJvRhEe60CqkwWvstGA"/>
<org.eventb.core.variable name="_LY0pwcEEEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.identifier="initiated" org.eventb.emf.persistence.emf_id="_5cjvJ_RhEe60CqkwWvstGA"/>
<org.eventb.core.variable name="_ZQ-UAfKWEe60CqkwWvstGA" org.eventb.core.generated="false" org.eventb.core.identifier="emitted" org.eventb.emf.persistence.emf_id="_5cjvKPRhEe60CqkwWvstGA"/>
<org.eventb.core.variable name="_LY1Q0cEEEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.identifier="gateway_processing" org.eventb.emf.persistence.emf_id="_5cjvKfRhEe60CqkwWvstGA"/>
<org.eventb.core.variable name="_LY134MEEEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.identifier="submit_cc_tx" org.eventb.emf.persistence.emf_id="_5cjvKvRhEe60CqkwWvstGA"/>
<org.eventb.core.variable name="_qWPSQMEGEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.identifier="wallet_created" org.eventb.emf.persistence.emf_id="_5cjvK_RhEe60CqkwWvstGA"/>
<org.eventb.core.variable name="_9cZOUMEHEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.identifier="wallet_amount" org.eventb.emf.persistence.emf_id="_5cjvLPRhEe60CqkwWvstGA"/>