Skip to content
Snippets Groups Projects
Commit 07d11c0a authored by Guzman Llambias's avatar Guzman Llambias
Browse files

Add animation to abstract machine

parent 9b9986c4
No related branches found
No related tags found
No related merge requests found
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.scMachineFile org.eventb.core.accurate="true" org.eventb.core.configuration="org.eventb.core.fwd">
<org.eventb.core.scRefinesMachine name="'" org.eventb.core.scTarget="/gateway-event-b/CCTx_Abstract_DLT_m1.bcm" org.eventb.core.source="/gateway-event-b/CCTx_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Animation_m2|org.eventb.core.refinesMachine#'"/>
<org.eventb.core.scSeesContext name="(" org.eventb.core.scTarget="/gateway-event-b/CCTx_Abstract_DLT_c1.bcc" org.eventb.core.source="/gateway-event-b/CCTx_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Animation_m2|org.eventb.core.seesContext#_yQ9vsL7uEe6laZimEYihUg"/>
<org.eventb.core.scInternalContext name="CCTx_Abstract_DLT_c1">
<org.eventb.core.scAxiom name="'" org.eventb.core.label="axm1;" org.eventb.core.predicate="source_smart_contract∈CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_c1.buc|org.eventb.core.contextFile#CCTx_Abstract_DLT_c1|org.eventb.core.axiom#_lhKcab7uEe6laZimEYihUg" org.eventb.core.theorem="false"/>
<org.eventb.core.scAxiom name="(" org.eventb.core.label="axm2;" org.eventb.core.predicate="target_smart_contract∈CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_c1.buc|org.eventb.core.contextFile#CCTx_Abstract_DLT_c1|org.eventb.core.axiom#_lhKcar7uEe6laZimEYihUg" org.eventb.core.theorem="false"/>
<org.eventb.core.scAxiom name=")" org.eventb.core.label="axm3;" org.eventb.core.predicate="gateway∈GATEWAYS" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_c1.buc|org.eventb.core.contextFile#CCTx_Abstract_DLT_c1|org.eventb.core.axiom#_lhKca77uEe6laZimEYihUg" org.eventb.core.theorem="false"/>
<org.eventb.core.scConstant name="source_smart_contract" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_c1.buc|org.eventb.core.contextFile#CCTx_Abstract_DLT_c1|org.eventb.core.constant#_lhTmML7uEe6laZimEYihUg" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
<org.eventb.core.scCarrierSet name="CROSS_CHAIN_EVENTS" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_c1.buc|org.eventb.core.contextFile#CCTx_Abstract_DLT_c1|org.eventb.core.carrierSet#_lhTmNr7uEe6laZimEYihUg" org.eventb.core.type="ℙ(CROSS_CHAIN_EVENTS)"/>
<org.eventb.core.scConstant name="gateway" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_c1.buc|org.eventb.core.contextFile#CCTx_Abstract_DLT_c1|org.eventb.core.constant#_lhTmMr7uEe6laZimEYihUg" org.eventb.core.type="GATEWAYS"/>
<org.eventb.core.scCarrierSet name="CROSS_CHAIN_TRANSACTIONS" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_c1.buc|org.eventb.core.contextFile#CCTx_Abstract_DLT_c1|org.eventb.core.carrierSet#_lhTmN77uEe6laZimEYihUg" org.eventb.core.type="ℙ(CROSS_CHAIN_TRANSACTIONS)"/>
<org.eventb.core.scCarrierSet name="GATEWAYS" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_c1.buc|org.eventb.core.contextFile#CCTx_Abstract_DLT_c1|org.eventb.core.carrierSet#_lhTmM77uEe6laZimEYihUg" org.eventb.core.type="ℙ(GATEWAYS)"/>
<org.eventb.core.scConstant name="target_smart_contract" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_c1.buc|org.eventb.core.contextFile#CCTx_Abstract_DLT_c1|org.eventb.core.constant#_lhTmMb7uEe6laZimEYihUg" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
<org.eventb.core.scCarrierSet name="TRANSACTIONS" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_c1.buc|org.eventb.core.contextFile#CCTx_Abstract_DLT_c1|org.eventb.core.carrierSet#_lhTmNL7uEe6laZimEYihUg" org.eventb.core.type="ℙ(TRANSACTIONS)"/>
<org.eventb.core.scCarrierSet name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_c1.buc|org.eventb.core.contextFile#CCTx_Abstract_DLT_c1|org.eventb.core.carrierSet#_lhTmNb7uEe6laZimEYihUg" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS)"/>
</org.eventb.core.scInternalContext>
<org.eventb.core.scInvariant name="CCTx_Abstract_DLT_c2" org.eventb.core.label="inv1;" org.eventb.core.predicate="received_transactions∈CROSS_CHAIN_SMART_CONTRACTS ↔ TRANSACTIONS" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.invariant#_yREdZL7uEe6laZimEYihUg" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="CCTx_Abstract_DLT_c3" org.eventb.core.label="inv2;" org.eventb.core.predicate="triggered_events∈CROSS_CHAIN_SMART_CONTRACTS ↔ CROSS_CHAIN_EVENTS" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.invariant#_yREdZb7uEe6laZimEYihUg" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="CCTx_Abstract_DLT_c4" org.eventb.core.label="inv3;" org.eventb.core.predicate="subscriptions∈GATEWAYS ↔ CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.invariant#_yREdZr7uEe6laZimEYihUg" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="CCTx_Abstract_DLT_c5" org.eventb.core.label="inv4;" org.eventb.core.predicate="gateway_pending_transactions∈GATEWAYS ↔ CROSS_CHAIN_TRANSACTIONS" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.invariant#_yREdZ77uEe6laZimEYihUg" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="CCTx_Abstract_DLT_c6" org.eventb.core.label="inv6;" org.eventb.core.predicate="received_cross_chain_transactions∈CROSS_CHAIN_SMART_CONTRACTS ↔ CROSS_CHAIN_TRANSACTIONS" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.invariant#_yREdaL7uEe6laZimEYihUg" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="CCTx_Abstract_DLT_c7" org.eventb.core.label="inv11" org.eventb.core.predicate="subscribed∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Animation_m2|org.eventb.core.invariant#_x2vr0MBBEe6yC4BToIaAqA" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="CCTx_Abstract_DLT_c8" org.eventb.core.label="inv12" org.eventb.core.predicate="initiated∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Animation_m2|org.eventb.core.invariant#_x2vr0cBBEe6yC4BToIaAqA" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="CCTx_Abstract_DLT_c9" org.eventb.core.label="inv13" org.eventb.core.predicate="triggered∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Animation_m2|org.eventb.core.invariant#_TQDZ4MBCEe6yC4BToIaAqA" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="CCTx_Abstract_DLT_c:" org.eventb.core.label="inv14" org.eventb.core.predicate="gateway_processing∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Animation_m2|org.eventb.core.invariant#_m7J2EMBDEe6yC4BToIaAqA" org.eventb.core.theorem="false"/>
<org.eventb.core.scInvariant name="CCTx_Abstract_DLT_c;" org.eventb.core.label="inv15" org.eventb.core.predicate="submit_cc_tx∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Animation_m2|org.eventb.core.invariant#_xgigYMBDEe6yC4BToIaAqA" org.eventb.core.theorem="false"/>
<org.eventb.core.scVariable name="gateway_processing" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/gateway-event-b/CCTx_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Animation_m2|org.eventb.core.variable#_m7KdIMBDEe6yC4BToIaAqA" org.eventb.core.type="ℤ"/>
<org.eventb.core.scVariable name="triggered_events" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/gateway-event-b/CCTx_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Animation_m2|org.eventb.core.variable#_yREdar7uEe6laZimEYihUg" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_EVENTS)"/>
<org.eventb.core.scVariable name="initiated" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/gateway-event-b/CCTx_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Animation_m2|org.eventb.core.variable#_zZtTYMBBEe6yC4BToIaAqA" org.eventb.core.type="ℤ"/>
<org.eventb.core.scVariable name="submit_cc_tx" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/gateway-event-b/CCTx_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Animation_m2|org.eventb.core.variable#_xgjHcMBDEe6yC4BToIaAqA" org.eventb.core.type="ℤ"/>
<org.eventb.core.scVariable name="subscribed" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/gateway-event-b/CCTx_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Animation_m2|org.eventb.core.variable#_65EIQMA-Ee6yC4BToIaAqA" org.eventb.core.type="ℤ"/>
<org.eventb.core.scVariable name="received_cross_chain_transactions" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/gateway-event-b/CCTx_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Animation_m2|org.eventb.core.variable#_yREdbb7uEe6laZimEYihUg" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_TRANSACTIONS)"/>
<org.eventb.core.scVariable name="subscriptions" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/gateway-event-b/CCTx_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Animation_m2|org.eventb.core.variable#_yREda77uEe6laZimEYihUg" org.eventb.core.type="ℙ(GATEWAYS×CROSS_CHAIN_SMART_CONTRACTS)"/>
<org.eventb.core.scVariable name="triggered" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/gateway-event-b/CCTx_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Animation_m2|org.eventb.core.variable#_RNsgkMBCEe6yC4BToIaAqA" org.eventb.core.type="ℤ"/>
<org.eventb.core.scVariable name="gateway_pending_transactions" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/gateway-event-b/CCTx_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Animation_m2|org.eventb.core.variable#_yREdbL7uEe6laZimEYihUg" org.eventb.core.type="ℙ(GATEWAYS×CROSS_CHAIN_TRANSACTIONS)"/>
<org.eventb.core.scVariable name="received_transactions" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/gateway-event-b/CCTx_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Animation_m2|org.eventb.core.variable#_yREdab7uEe6laZimEYihUg" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×TRANSACTIONS)"/>
<org.eventb.core.scEvent name="received_cross_chain_transactiont" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="INITIALISATION" org.eventb.core.source="/gateway-event-b/CCTx_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Animation_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/gateway-event-b/CCTx_Abstract_DLT_m1.bcm|org.eventb.core.scMachineFile#CCTx_Abstract_DLT_m1|org.eventb.core.scEvent#received_cross_chain_transactiont" org.eventb.core.source="/gateway-event-b/CCTx_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Animation_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh"/>
<org.eventb.core.scAction name="'" org.eventb.core.assignment="received_transactions ≔ ∅ ⦂ ℙ(CROSS_CHAIN_SMART_CONTRACTS×TRANSACTIONS)" org.eventb.core.label="act1;" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#'|org.eventb.core.action#_yQ9vsb7uEe6laZimEYihUg"/>
<org.eventb.core.scAction name="(" org.eventb.core.assignment="triggered_events ≔ ∅ ⦂ ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_EVENTS)" org.eventb.core.label="act2;" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#'|org.eventb.core.action#_yQ9vsr7uEe6laZimEYihUg"/>
<org.eventb.core.scAction name=")" org.eventb.core.assignment="subscriptions ≔ ∅ ⦂ ℙ(GATEWAYS×CROSS_CHAIN_SMART_CONTRACTS)" org.eventb.core.label="act3;" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#'|org.eventb.core.action#_yQ9vs77uEe6laZimEYihUg"/>
<org.eventb.core.scAction name="*" org.eventb.core.assignment="gateway_pending_transactions ≔ ∅ ⦂ ℙ(GATEWAYS×CROSS_CHAIN_TRANSACTIONS)" org.eventb.core.label="act4;" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#'|org.eventb.core.action#_yQ9vtL7uEe6laZimEYihUg"/>
<org.eventb.core.scAction name="+" org.eventb.core.assignment="received_cross_chain_transactions ≔ ∅ ⦂ ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_TRANSACTIONS)" org.eventb.core.label="act6;" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#'|org.eventb.core.action#_yQ9vtb7uEe6laZimEYihUg"/>
<org.eventb.core.scAction name="," org.eventb.core.assignment="subscribed ≔ 0" org.eventb.core.label="act11" org.eventb.core.source="/gateway-event-b/CCTx_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Animation_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh|org.eventb.core.action#_BPYKEMA_Ee6yC4BToIaAqA"/>
<org.eventb.core.scAction name="-" org.eventb.core.assignment="initiated ≔ 0" org.eventb.core.label="act12" org.eventb.core.source="/gateway-event-b/CCTx_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Animation_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh|org.eventb.core.action#_vcpn8MBBEe6yC4BToIaAqA"/>
<org.eventb.core.scAction name="." org.eventb.core.assignment="triggered ≔ 0" org.eventb.core.label="act13" org.eventb.core.source="/gateway-event-b/CCTx_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Animation_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh|org.eventb.core.action#_RNqrYMBCEe6yC4BToIaAqA"/>
<org.eventb.core.scAction name="/" org.eventb.core.assignment="gateway_processing ≔ 0" org.eventb.core.label="act14" org.eventb.core.source="/gateway-event-b/CCTx_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Animation_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh|org.eventb.core.action#_m7IA4MBDEe6yC4BToIaAqA"/>
<org.eventb.core.scAction name="0" org.eventb.core.assignment="submit_cc_tx ≔ 0" org.eventb.core.label="act15" org.eventb.core.source="/gateway-event-b/CCTx_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Animation_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh|org.eventb.core.action#_xggrMMBDEe6yC4BToIaAqA"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="received_cross_chain_transactionu" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="SUBSCRIBE_SMART_CONTRACT_EVENTS" org.eventb.core.source="/gateway-event-b/CCTx_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Animation_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUi">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/gateway-event-b/CCTx_Abstract_DLT_m1.bcm|org.eventb.core.scMachineFile#CCTx_Abstract_DLT_m1|org.eventb.core.scEvent#received_cross_chain_transactionu" org.eventb.core.source="/gateway-event-b/CCTx_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Animation_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUi|org.eventb.core.refinesEvent#'"/>
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1;" org.eventb.core.predicate="gateway ↦ source_smart_contract∉subscriptions" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_yQ9vtr7uEe6laZimEYihUg|org.eventb.core.guard#_yQ9vuL7uEe6laZimEYihUg" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="(" org.eventb.core.assignment="subscriptions ≔ subscriptions∪{gateway ↦ source_smart_contract}" org.eventb.core.label="act1;" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_yQ9vtr7uEe6laZimEYihUg|org.eventb.core.action#_yQ9vt77uEe6laZimEYihUg"/>
<org.eventb.core.scAction name=")" org.eventb.core.assignment="subscribed ≔ 1" org.eventb.core.label="act11" org.eventb.core.source="/gateway-event-b/CCTx_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Animation_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUi|org.eventb.core.action#_bhqLEMA_Ee6yC4BToIaAqA"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="received_cross_chain_transactionv" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="INITIATE_CROSS_CHAIN_TRANSACTION" org.eventb.core.source="/gateway-event-b/CCTx_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Animation_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUj">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/gateway-event-b/CCTx_Abstract_DLT_m1.bcm|org.eventb.core.scMachineFile#CCTx_Abstract_DLT_m1|org.eventb.core.scEvent#received_cross_chain_transactionv" org.eventb.core.source="/gateway-event-b/CCTx_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Animation_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUj|org.eventb.core.refinesEvent#'"/>
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1;" org.eventb.core.predicate="transaction∈TRANSACTIONS" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_yQ9vub7uEe6laZimEYihUg|org.eventb.core.guard#_yQ9vu77uEe6laZimEYihUg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd3;" org.eventb.core.predicate="transaction∉received_transactions[{source_smart_contract}]" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_yQ9vub7uEe6laZimEYihUg|org.eventb.core.guard#_yQ9vvL7uEe6laZimEYihUg" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="transactioo" org.eventb.core.assignment="received_transactions ≔ received_transactions∪{source_smart_contract ↦ transaction}" org.eventb.core.label="act1;" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_yQ9vub7uEe6laZimEYihUg|org.eventb.core.action#_yQ9vur7uEe6laZimEYihUg"/>
<org.eventb.core.scParameter name="transaction" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_yQ9vub7uEe6laZimEYihUg|org.eventb.core.parameter#_yQ9vvb7uEe6laZimEYihUg" org.eventb.core.type="TRANSACTIONS"/>
<org.eventb.core.scAction name="transactiop" org.eventb.core.assignment="initiated ≔ 1" org.eventb.core.label="act11" org.eventb.core.source="/gateway-event-b/CCTx_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Animation_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUj|org.eventb.core.action#_vcsEMMBBEe6yC4BToIaAqA"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="received_cross_chain_transactionw" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="PROCESS_CROSS_CHAIN_TRANSACTION" org.eventb.core.source="/gateway-event-b/CCTx_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Animation_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUk">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/gateway-event-b/CCTx_Abstract_DLT_m1.bcm|org.eventb.core.scMachineFile#CCTx_Abstract_DLT_m1|org.eventb.core.scEvent#received_cross_chain_transactionw" org.eventb.core.source="/gateway-event-b/CCTx_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Animation_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUk|org.eventb.core.refinesEvent#'"/>
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1;" org.eventb.core.predicate="source_smart_contract ↦ transaction∈received_transactions" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_yQ9vvr7uEe6laZimEYihUg|org.eventb.core.guard#_yQ9vwb7uEe6laZimEYihUg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2;" org.eventb.core.predicate="cross_chain_event∉triggered_events[{source_smart_contract}]" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_yQ9vvr7uEe6laZimEYihUg|org.eventb.core.guard#_yQ9vwr7uEe6laZimEYihUg" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="cross_chain_evenu" org.eventb.core.assignment="triggered_events ≔ triggered_events∪{source_smart_contract ↦ cross_chain_event}" org.eventb.core.label="act1;" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_yQ9vvr7uEe6laZimEYihUg|org.eventb.core.action#_yQ9vv77uEe6laZimEYihUg"/>
<org.eventb.core.scAction name="cross_chain_evenv" org.eventb.core.assignment="received_transactions ≔ received_transactions ∖ {source_smart_contract ↦ transaction}" org.eventb.core.label="act2;" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_yQ9vvr7uEe6laZimEYihUg|org.eventb.core.action#_yQ9vwL7uEe6laZimEYihUg"/>
<org.eventb.core.scParameter name="cross_chain_event" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_yQ9vvr7uEe6laZimEYihUg|org.eventb.core.parameter#_yQ9vxL7uEe6laZimEYihUg" org.eventb.core.type="CROSS_CHAIN_EVENTS"/>
<org.eventb.core.scParameter name="transaction" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_yQ9vvr7uEe6laZimEYihUg|org.eventb.core.parameter#_yQ9vw77uEe6laZimEYihUg" org.eventb.core.type="TRANSACTIONS"/>
<org.eventb.core.scAction name="cross_chain_evenw" org.eventb.core.assignment="triggered ≔ 1" org.eventb.core.label="act11" org.eventb.core.source="/gateway-event-b/CCTx_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Animation_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUk|org.eventb.core.action#_ZYQHMMBCEe6yC4BToIaAqA"/>
<org.eventb.core.scAction name="cross_chain_evenx" org.eventb.core.assignment="initiated ≔ 0" org.eventb.core.label="act12" org.eventb.core.source="/gateway-event-b/CCTx_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Animation_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUk|org.eventb.core.action#_ZYQHMcBCEe6yC4BToIaAqA"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="received_cross_chain_transactionx" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="LISTEN_SMART_CONTRACT_EVENT" org.eventb.core.source="/gateway-event-b/CCTx_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Animation_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUl">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/gateway-event-b/CCTx_Abstract_DLT_m1.bcm|org.eventb.core.scMachineFile#CCTx_Abstract_DLT_m1|org.eventb.core.scEvent#received_cross_chain_transactionx" org.eventb.core.source="/gateway-event-b/CCTx_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Animation_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUl|org.eventb.core.refinesEvent#'"/>
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1;" org.eventb.core.predicate="source_smart_contract ↦ cross_chain_event∈triggered_events" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_yQ9vxb7uEe6laZimEYihUg|org.eventb.core.guard#_yQ9vyL7uEe6laZimEYihUg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name="(" org.eventb.core.label="grd2;" org.eventb.core.predicate="gateway ↦ source_smart_contract∈subscriptions" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_yQ9vxb7uEe6laZimEYihUg|org.eventb.core.guard#_yQ9vyb7uEe6laZimEYihUg" org.eventb.core.theorem="false"/>
<org.eventb.core.scGuard name=")" org.eventb.core.label="grd3;" org.eventb.core.predicate="gateway ↦ cross_chain_transaction∉gateway_pending_transactions" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_yQ9vxb7uEe6laZimEYihUg|org.eventb.core.guard#_yQ9vyr7uEe6laZimEYihUg" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="cross_chain_transactioo" org.eventb.core.assignment="gateway_pending_transactions ≔ gateway_pending_transactions∪{gateway ↦ cross_chain_transaction}" org.eventb.core.label="act1;" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_yQ9vxb7uEe6laZimEYihUg|org.eventb.core.action#_yQ9vxr7uEe6laZimEYihUg"/>
<org.eventb.core.scAction name="cross_chain_transactiop" org.eventb.core.assignment="triggered_events ≔ triggered_events ∖ {source_smart_contract ↦ cross_chain_event}" org.eventb.core.label="act2;" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_yQ9vxb7uEe6laZimEYihUg|org.eventb.core.action#_yQ9vx77uEe6laZimEYihUg"/>
<org.eventb.core.scParameter name="cross_chain_event" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_yQ9vxb7uEe6laZimEYihUg|org.eventb.core.parameter#_yQ9vy77uEe6laZimEYihUg" org.eventb.core.type="CROSS_CHAIN_EVENTS"/>
<org.eventb.core.scParameter name="cross_chain_transaction" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_yQ9vxb7uEe6laZimEYihUg|org.eventb.core.parameter#_yQ9vzL7uEe6laZimEYihUg" org.eventb.core.type="CROSS_CHAIN_TRANSACTIONS"/>
<org.eventb.core.scAction name="cross_chain_transactioq" org.eventb.core.assignment="gateway_processing ≔ 1" org.eventb.core.label="act11" org.eventb.core.source="/gateway-event-b/CCTx_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Animation_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUl|org.eventb.core.action#_m7JPAMBDEe6yC4BToIaAqA"/>
<org.eventb.core.scAction name="cross_chain_transactior" org.eventb.core.assignment="triggered ≔ 0" org.eventb.core.label="act12" org.eventb.core.source="/gateway-event-b/CCTx_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Animation_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUl|org.eventb.core.action#_m7JPAcBDEe6yC4BToIaAqA"/>
</org.eventb.core.scEvent>
<org.eventb.core.scEvent name="received_cross_chain_transactiony" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="GATEWAY_PROCESS_CROSS_CHAIN_TRANSACTION" org.eventb.core.source="/gateway-event-b/CCTx_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Animation_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUm">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/gateway-event-b/CCTx_Abstract_DLT_m1.bcm|org.eventb.core.scMachineFile#CCTx_Abstract_DLT_m1|org.eventb.core.scEvent#received_cross_chain_transactiony" org.eventb.core.source="/gateway-event-b/CCTx_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Animation_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUm|org.eventb.core.refinesEvent#'"/>
<org.eventb.core.scGuard name="'" org.eventb.core.label="grd1;" org.eventb.core.predicate="gateway ↦ cross_chain_transaction∈gateway_pending_transactions" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_yQ9vzb7uEe6laZimEYihUg|org.eventb.core.guard#_yREdYr7uEe6laZimEYihUg" org.eventb.core.theorem="false"/>
<org.eventb.core.scAction name="cross_chain_transactioo" org.eventb.core.assignment="received_cross_chain_transactions ≔ received_cross_chain_transactions∪{target_smart_contract ↦ cross_chain_transaction}" org.eventb.core.label="act1;" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_yQ9vzb7uEe6laZimEYihUg|org.eventb.core.action#_yREdYL7uEe6laZimEYihUg"/>
<org.eventb.core.scAction name="cross_chain_transactiop" org.eventb.core.assignment="gateway_pending_transactions ≔ gateway_pending_transactions ∖ {gateway ↦ cross_chain_transaction}" org.eventb.core.label="act2;" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_yQ9vzb7uEe6laZimEYihUg|org.eventb.core.action#_yREdYb7uEe6laZimEYihUg"/>
<org.eventb.core.scParameter name="cross_chain_transaction" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_yQ9vzb7uEe6laZimEYihUg|org.eventb.core.parameter#_yREdY77uEe6laZimEYihUg" org.eventb.core.type="CROSS_CHAIN_TRANSACTIONS"/>
<org.eventb.core.scAction name="cross_chain_transactioq" org.eventb.core.assignment="submit_cc_tx ≔ 1" org.eventb.core.label="act11" org.eventb.core.source="/gateway-event-b/CCTx_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Animation_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUm|org.eventb.core.action#_xgh5UMBDEe6yC4BToIaAqA"/>
<org.eventb.core.scAction name="cross_chain_transactior" org.eventb.core.assignment="gateway_processing ≔ 0" org.eventb.core.label="act12" org.eventb.core.source="/gateway-event-b/CCTx_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Animation_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUm|org.eventb.core.action#_xgh5UcBDEe6yC4BToIaAqA"/>
</org.eventb.core.scEvent>
</org.eventb.core.scMachineFile>
This diff is collapsed.
<?xml version="1.0" encoding="UTF-8"?> <?xml version="1.0" encoding="UTF-8"?>
<org.eventb.core.scContextFile/> <org.eventb.core.poFile/>
\ No newline at end of file \ No newline at end of file
This diff is collapsed.
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.psFile>
<org.eventb.core.psStatus name="INITIALISATION/inv11/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="12" org.eventb.core.psManual="false"/>
<org.eventb.core.psStatus name="INITIALISATION/inv12/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="12" org.eventb.core.psManual="false"/>
<org.eventb.core.psStatus name="INITIALISATION/inv13/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="12" org.eventb.core.psManual="false"/>
<org.eventb.core.psStatus name="SUBSCRIBE_SMART_CONTRACT_EVENTS/inv11/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="12" org.eventb.core.psManual="false"/>
<org.eventb.core.psStatus name="INITIATE_CROSS_CHAIN_TRANSACTION/inv12/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="12" org.eventb.core.psManual="false"/>
<org.eventb.core.psStatus name="PROCESS_CROSS_CHAIN_TRANSACTION/inv12/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="13" org.eventb.core.psManual="false"/>
<org.eventb.core.psStatus name="PROCESS_CROSS_CHAIN_TRANSACTION/inv13/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="13" org.eventb.core.psManual="false"/>
</org.eventb.core.psFile>
<?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="_xeWIKMBDEe6yC4BToIaAqA" org.eventb.texttools.text_lastmodified="1706710781059" org.eventb.texttools.text_representation="machine CCTx_Animation_m2 refines CCTx_Abstract_DLT_m1 sees CCTx_Abstract_DLT_c1&#10;&#10;variables received_transactions triggered_events subscriptions gateway_pending_transactions received_cross_chain_transactions subscribed initiated triggered gateway_processing submit_cc_tx&#10;&#10;invariants&#10;&#9;@inv11 subscribed ∈ {0,1}&#10;&#9;@inv12 initiated ∈ {0,1}&#10;&#9;@inv13 triggered ∈ {0,1}&#10;&#9;@inv14 gateway_processing ∈ {0,1}&#10;&#9;@inv15 submit_cc_tx ∈ {0,1}&#10;&#10;events&#10; event INITIALISATION extends INITIALISATION&#10; &#9;then&#10; &#9;&#9;@act11 subscribed ≔ 0&#10; &#9;&#9;@act12 initiated ≔ 0&#10; &#9;&#9;@act13 triggered ≔ 0&#10; &#9;&#9;@act14 gateway_processing ≔ 0&#10; &#9;&#9;@act15 submit_cc_tx ≔ 0&#10; end&#10;&#10; event SUBSCRIBE_SMART_CONTRACT_EVENTS extends SUBSCRIBE_SMART_CONTRACT_EVENTS&#10;&#9;then&#10;&#9;&#9;@act11 subscribed ≔ 1&#10; end&#10;&#10; event INITIATE_CROSS_CHAIN_TRANSACTION extends INITIATE_CROSS_CHAIN_TRANSACTION&#10; &#9;then&#10; &#9;&#9;@act11 initiated ≔ 1&#10; end&#10;&#10; event PROCESS_CROSS_CHAIN_TRANSACTION extends PROCESS_CROSS_CHAIN_TRANSACTION&#10; &#9;then&#10; &#9;&#9;@act11 triggered ≔ 1&#10; &#9;&#9;@act12 initiated ≔ 0&#10; end&#10;&#10; event LISTEN_SMART_CONTRACT_EVENT extends LISTEN_SMART_CONTRACT_EVENT&#10; &#9;then&#10; &#9;&#9;@act11 gateway_processing ≔ 1&#10; &#9;&#9;@act12 triggered ≔ 0&#10; end&#10;&#10; event GATEWAY_PROCESS_CROSS_CHAIN_TRANSACTION extends GATEWAY_PROCESS_CROSS_CHAIN_TRANSACTION&#10; &#9;then&#10; &#9;&#9;@act11 submit_cc_tx ≔ 1&#10; &#9;&#9;@act12 gateway_processing ≔ 0&#10; end&#10;end&#10;" version="5">
<org.eventb.core.refinesMachine name="'" org.eventb.core.target="CCTx_Abstract_DLT_m1"/>
<org.eventb.core.seesContext name="_yQ9vsL7uEe6laZimEYihUg" org.eventb.core.target="CCTx_Abstract_DLT_c1"/>
<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="_xeWIFMBDEe6yC4BToIaAqA">
<org.eventb.core.action name="_BPYKEMA_Ee6yC4BToIaAqA" org.eventb.core.assignment="subscribed ≔ 0" org.eventb.core.generated="false" org.eventb.core.label="act11" org.eventb.emf.persistence.emf_id="_xeWID8BDEe6yC4BToIaAqA"/>
<org.eventb.core.action name="_vcpn8MBBEe6yC4BToIaAqA" org.eventb.core.assignment="initiated ≔ 0" org.eventb.core.generated="false" org.eventb.core.label="act12" org.eventb.emf.persistence.emf_id="_xeWIEMBDEe6yC4BToIaAqA"/>
<org.eventb.core.action name="_RNqrYMBCEe6yC4BToIaAqA" org.eventb.core.assignment="triggered ≔ 0" org.eventb.core.generated="false" org.eventb.core.label="act13" org.eventb.emf.persistence.emf_id="_xeWIEcBDEe6yC4BToIaAqA"/>
<org.eventb.core.action name="_m7IA4MBDEe6yC4BToIaAqA" org.eventb.core.assignment="gateway_processing ≔ 0" org.eventb.core.generated="false" org.eventb.core.label="act14" org.eventb.emf.persistence.emf_id="_xeWIEsBDEe6yC4BToIaAqA"/>
<org.eventb.core.action name="_xggrMMBDEe6yC4BToIaAqA" org.eventb.core.assignment="submit_cc_tx ≔ 0" org.eventb.core.generated="false" org.eventb.core.label="act15" org.eventb.emf.persistence.emf_id="_xeWIE8BDEe6yC4BToIaAqA"/>
</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" org.eventb.emf.persistence.emf_id="_xeWIF8BDEe6yC4BToIaAqA">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="SUBSCRIBE_SMART_CONTRACT_EVENTS"/>
<org.eventb.core.action name="_bhqLEMA_Ee6yC4BToIaAqA" org.eventb.core.assignment="subscribed ≔ 1" org.eventb.core.generated="false" org.eventb.core.label="act11" org.eventb.emf.persistence.emf_id="_xeWIFsBDEe6yC4BToIaAqA"/>
</org.eventb.core.event>
<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_CROSS_CHAIN_TRANSACTION" org.eventb.emf.persistence.emf_id="_xeWIGsBDEe6yC4BToIaAqA">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="INITIATE_CROSS_CHAIN_TRANSACTION"/>
<org.eventb.core.action name="_vcsEMMBBEe6yC4BToIaAqA" org.eventb.core.assignment="initiated ≔ 1" org.eventb.core.generated="false" org.eventb.core.label="act11" org.eventb.emf.persistence.emf_id="_xeWIGcBDEe6yC4BToIaAqA"/>
</org.eventb.core.event>
<org.eventb.core.event name="_yREdbb7uEe6laZimEYihUk" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="PROCESS_CROSS_CHAIN_TRANSACTION" org.eventb.emf.persistence.emf_id="_xeWIHsBDEe6yC4BToIaAqA">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="PROCESS_CROSS_CHAIN_TRANSACTION"/>
<org.eventb.core.action name="_ZYQHMMBCEe6yC4BToIaAqA" org.eventb.core.assignment="triggered ≔ 1" org.eventb.core.generated="false" org.eventb.core.label="act11" org.eventb.emf.persistence.emf_id="_xeWIHMBDEe6yC4BToIaAqA"/>
<org.eventb.core.action name="_ZYQHMcBCEe6yC4BToIaAqA" org.eventb.core.assignment="initiated ≔ 0" org.eventb.core.generated="false" org.eventb.core.label="act12" org.eventb.emf.persistence.emf_id="_xeWIHcBDEe6yC4BToIaAqA"/>
</org.eventb.core.event>
<org.eventb.core.event name="_yREdbb7uEe6laZimEYihUl" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="LISTEN_SMART_CONTRACT_EVENT" org.eventb.emf.persistence.emf_id="_xeWIIsBDEe6yC4BToIaAqA">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="LISTEN_SMART_CONTRACT_EVENT"/>
<org.eventb.core.action name="_m7JPAMBDEe6yC4BToIaAqA" org.eventb.core.assignment="gateway_processing ≔ 1" org.eventb.core.generated="false" org.eventb.core.label="act11" org.eventb.emf.persistence.emf_id="_xeWIIMBDEe6yC4BToIaAqA"/>
<org.eventb.core.action name="_m7JPAcBDEe6yC4BToIaAqA" org.eventb.core.assignment="triggered ≔ 0" org.eventb.core.generated="false" org.eventb.core.label="act12" org.eventb.emf.persistence.emf_id="_xeWIIcBDEe6yC4BToIaAqA"/>
</org.eventb.core.event>
<org.eventb.core.event name="_yREdbb7uEe6laZimEYihUm" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="GATEWAY_PROCESS_CROSS_CHAIN_TRANSACTION" org.eventb.emf.persistence.emf_id="_xeWIJsBDEe6yC4BToIaAqA">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="GATEWAY_PROCESS_CROSS_CHAIN_TRANSACTION"/>
<org.eventb.core.action name="_xgh5UMBDEe6yC4BToIaAqA" org.eventb.core.assignment="submit_cc_tx ≔ 1" org.eventb.core.generated="false" org.eventb.core.label="act11" org.eventb.emf.persistence.emf_id="_xeWIJMBDEe6yC4BToIaAqA"/>
<org.eventb.core.action name="_xgh5UcBDEe6yC4BToIaAqA" org.eventb.core.assignment="gateway_processing ≔ 0" org.eventb.core.generated="false" org.eventb.core.label="act12" org.eventb.emf.persistence.emf_id="_xeWIJcBDEe6yC4BToIaAqA"/>
</org.eventb.core.event>
<org.eventb.core.invariant name="_x2vr0MBBEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.label="inv11" org.eventb.core.predicate="subscribed ∈ {0,1}" org.eventb.emf.persistence.emf_id="_xeWICsBDEe6yC4BToIaAqA"/>
<org.eventb.core.invariant name="_x2vr0cBBEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.label="inv12" org.eventb.core.predicate="initiated ∈ {0,1}" org.eventb.emf.persistence.emf_id="_xeWIC8BDEe6yC4BToIaAqA"/>
<org.eventb.core.invariant name="_TQDZ4MBCEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.label="inv13" org.eventb.core.predicate="triggered ∈ {0,1}" org.eventb.emf.persistence.emf_id="_xeWIDMBDEe6yC4BToIaAqA"/>
<org.eventb.core.invariant name="_m7J2EMBDEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.label="inv14" org.eventb.core.predicate="gateway_processing ∈ {0,1}" org.eventb.emf.persistence.emf_id="_xeWIDcBDEe6yC4BToIaAqA"/>
<org.eventb.core.invariant name="_xgigYMBDEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.label="inv15" org.eventb.core.predicate="submit_cc_tx ∈ {0,1}" org.eventb.emf.persistence.emf_id="_xeWIDsBDEe6yC4BToIaAqA"/>
<org.eventb.core.variable name="_yREdab7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="received_transactions" org.eventb.emf.persistence.emf_id="_xeWIAMBDEe6yC4BToIaAqA"/>
<org.eventb.core.variable name="_yREdar7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="triggered_events" org.eventb.emf.persistence.emf_id="_xeWIAcBDEe6yC4BToIaAqA"/>
<org.eventb.core.variable name="_yREda77uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="subscriptions" org.eventb.emf.persistence.emf_id="_xeWIAsBDEe6yC4BToIaAqA"/>
<org.eventb.core.variable name="_yREdbL7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="gateway_pending_transactions" org.eventb.emf.persistence.emf_id="_xeWIA8BDEe6yC4BToIaAqA"/>
<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="_xeWIBMBDEe6yC4BToIaAqA"/>
<org.eventb.core.variable name="_65EIQMA-Ee6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.identifier="subscribed" org.eventb.emf.persistence.emf_id="_xeWIBcBDEe6yC4BToIaAqA"/>
<org.eventb.core.variable name="_zZtTYMBBEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.identifier="initiated" org.eventb.emf.persistence.emf_id="_xeWIBsBDEe6yC4BToIaAqA"/>
<org.eventb.core.variable name="_RNsgkMBCEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.identifier="triggered" org.eventb.emf.persistence.emf_id="_xeWIB8BDEe6yC4BToIaAqA"/>
<org.eventb.core.variable name="_m7KdIMBDEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.identifier="gateway_processing" org.eventb.emf.persistence.emf_id="_xeWICMBDEe6yC4BToIaAqA"/>
<org.eventb.core.variable name="_xgjHcMBDEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.identifier="submit_cc_tx" org.eventb.emf.persistence.emf_id="_xeWICcBDEe6yC4BToIaAqA"/>
</org.eventb.core.machineFile>
This diff is collapsed.
This diff is collapsed.
{
"svg": "gateway-event-b-animation.svg",
"items": [
{
"id": "subscription",
"attr": "visibility",
"value": "IF subscribed=1 THEN \"visible\" ELSE \"hidden\" END"
},
{
"id": "initiate-cc-tx",
"attr": "stroke",
"value": "IF initiated=1 THEN \"red\" ELSE \"black\" END"
},
{
"id": "trigger-event",
"attr": "stroke",
"value": "IF triggered=1 THEN \"red\" ELSE \"black\" END"
},
{
"id": "gateway",
"attr": "fill",
"value": "IF gateway_processing=1 THEN \"green\" ELSE \"white\" END"
},
{
"id": "submit-cc-tx",
"attr": "stroke",
"value": "IF submit_cc_tx=1 THEN \"red\" ELSE \"black\" END"
}
],
"events": [
{
"id": "subscription",
"event": "SUBSCRIBE_SMART_CONTRACT_EVENTS"
},
{
"id": "initiate-cc-tx",
"event": "INITIATE_CROSS_CHAIN_TRANSACTION"
},
{
"id": "trigger-event",
"event": "PROCESS_CROSS_CHAIN_TRANSACTION"
},
{
"id": "gateway",
"event": "LISTEN_SMART_CONTRACT_EVENT"
},
{
"id": "submit-cc-tx",
"event": "GATEWAY_PROCESS_CROSS_CHAIN_TRANSACTION"
}
]
}
\ No newline at end of file
{
"svg": "button.svg",
"items": [
{
"id": "button",
"attr": "visibility",
"value": "IF button=TRUE THEN \"visible\" ELSE \"hidden\" END"
}
],
"events": [
{
"id": "button",
"event": "press_button"
}
]
}
\ No newline at end of file
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment