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

Improve abstract machine animation

parent 4b4a6a99
No related branches found
No related tags found
No related merge requests found
Expand all Show whitespace changes
Inline Side-by-side
Showing
with 755 additions and 1 deletion
gateway-event-b/CCTx_Abstract_Animation_m2.bcm 0 → 100644
+ 100
− 0
View file @ 75773655
<?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_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.refinesMachine#_VBLQ0MEUEe6yC4BToIaAqA"/>
<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_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_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_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.invariant#_VBL34sEUEe6yC4BToIaAqA" 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_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.invariant#_VBMe8MEUEe6yC4BToIaAqA" 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_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.invariant#_VBMe8cEUEe6yC4BToIaAqA" 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_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.invariant#_VBNGAMEUEe6yC4BToIaAqA" 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_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.invariant#_VBNGAcEUEe6yC4BToIaAqA" 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_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_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_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_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_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_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_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_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_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_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_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_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_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_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_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_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_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_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_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_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="INITIATE_CC_TX" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqD">
<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_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqD|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#_y397cMBFEe6yC4BToIaAqA|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#_y397cMBFEe6yC4BToIaAqA|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#_y397cMBFEe6yC4BToIaAqA|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#_y397cMBFEe6yC4BToIaAqA|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_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqD|org.eventb.core.action#_VBQwYMEUEe6yC4BToIaAqA"/>
<org.eventb.core.scAction name="transactioq" org.eventb.core.assignment="submit_cc_tx ≔ 0" org.eventb.core.label="act12" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqD|org.eventb.core.action#_VBRXccEUEe6yC4BToIaAqA"/>
</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="TRIGGER_CC_TX_EVENT" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqE">
<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_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqE|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#_E_KKUMBGEe6yC4BToIaAqA|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#_E_KKUMBGEe6yC4BToIaAqA|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#_E_KKUMBGEe6yC4BToIaAqA|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#_E_KKUMBGEe6yC4BToIaAqA|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#_E_KKUMBGEe6yC4BToIaAqA|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#_E_KKUMBGEe6yC4BToIaAqA|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_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqE|org.eventb.core.action#_VBRXcMEUEe6yC4BToIaAqA"/>
<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_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqE|org.eventb.core.action#_VBR-gcEUEe6yC4BToIaAqA"/>
<org.eventb.core.scAction name="cross_chain_eveny" org.eventb.core.assignment="submit_cc_tx ≔ 0" org.eventb.core.label="act13" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqE|org.eventb.core.action#_kIrbcMEUEe6yC4BToIaAqA"/>
</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="LISTEN_CC_TX_EVENT" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqF">
<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_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqF|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#_THog4MBGEe6yC4BToIaAqA|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#_THog4MBGEe6yC4BToIaAqA|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#_THog4MBGEe6yC4BToIaAqA|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#_THog4MBGEe6yC4BToIaAqA|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#_THog4MBGEe6yC4BToIaAqA|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#_THog4MBGEe6yC4BToIaAqA|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#_THog4MBGEe6yC4BToIaAqA|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_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqF|org.eventb.core.action#_VBR-gMEUEe6yC4BToIaAqA"/>
<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_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqF|org.eventb.core.action#_VBL34cEUEe6yC4BToIaAqA"/>
<org.eventb.core.scAction name="cross_chain_transactios" org.eventb.core.assignment="submit_cc_tx ≔ 0" org.eventb.core.label="act13" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqF|org.eventb.core.action#_k8Z-cMEUEe6yC4BToIaAqA"/>
</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="SUBMIT_CC_TX" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqG">
<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_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqG|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#_fwqd8MBGEe6yC4BToIaAqA|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#_fwqd8MBGEe6yC4BToIaAqA|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#_fwqd8MBGEe6yC4BToIaAqA|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#_fwqd8MBGEe6yC4BToIaAqA|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_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqG|org.eventb.core.action#_VBL34MEUEe6yC4BToIaAqA"/>
<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_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqG|org.eventb.core.action#_isfxUMEUEe6yC4BToIaAqA"/>
</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="INITIALISATION" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqB">
<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_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqB"/>
<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_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqB|org.eventb.core.action#_VBO7MMEUEe6yC4BToIaAqA"/>
<org.eventb.core.scAction name="-" org.eventb.core.assignment="initiated ≔ 0" org.eventb.core.label="act12" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqB|org.eventb.core.action#_VBPiQMEUEe6yC4BToIaAqA"/>
<org.eventb.core.scAction name="." org.eventb.core.assignment="triggered ≔ 0" org.eventb.core.label="act13" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqB|org.eventb.core.action#_VBPiQcEUEe6yC4BToIaAqA"/>
<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_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqB|org.eventb.core.action#_VBPiQsEUEe6yC4BToIaAqA"/>
<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_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqB|org.eventb.core.action#_VBPiQ8EUEe6yC4BToIaAqA"/>
</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="SUBSCRIBE_SMART_CONTRACT_EVENTS" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqC">
<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_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqC|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_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqC|org.eventb.core.action#_VBQJUMEUEe6yC4BToIaAqA"/>
</org.eventb.core.scEvent>
</org.eventb.core.scMachineFile>
gateway-event-b/CCTx_Abstract_Animation_m2.bpo 0 → 100644
+ 251
− 0
View file @ 75773655
This diff is collapsed.
gateway-event-b/CCTx_Abstract_Animation_m2.bpr 0 → 100644
+ 330
− 0
View file @ 75773655
This diff is collapsed.
gateway-event-b/CCTx_Abstract_Animation_m2.bps 0 → 100644
+ 19
− 0
View file @ 75773655
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.psFile>
<org.eventb.core.psStatus name="INITIATE_CC_TX/inv12/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="3" org.eventb.core.psManual="false"/>
<org.eventb.core.psStatus name="INITIATE_CC_TX/inv15/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="3" org.eventb.core.psManual="false"/>
<org.eventb.core.psStatus name="TRIGGER_CC_TX_EVENT/inv12/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="3" org.eventb.core.psManual="false"/>
<org.eventb.core.psStatus name="TRIGGER_CC_TX_EVENT/inv13/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="3" org.eventb.core.psManual="false"/>
<org.eventb.core.psStatus name="TRIGGER_CC_TX_EVENT/inv15/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="3" org.eventb.core.psManual="false"/>
<org.eventb.core.psStatus name="LISTEN_CC_TX_EVENT/inv13/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="3" org.eventb.core.psManual="false"/>
<org.eventb.core.psStatus name="LISTEN_CC_TX_EVENT/inv14/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="3" org.eventb.core.psManual="false"/>
<org.eventb.core.psStatus name="LISTEN_CC_TX_EVENT/inv15/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="3" org.eventb.core.psManual="false"/>
<org.eventb.core.psStatus name="SUBMIT_CC_TX/inv14/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="3" org.eventb.core.psManual="false"/>
<org.eventb.core.psStatus name="SUBMIT_CC_TX/inv15/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="3" org.eventb.core.psManual="false"/>
<org.eventb.core.psStatus name="INITIALISATION/inv11/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="3" org.eventb.core.psManual="false"/>
<org.eventb.core.psStatus name="INITIALISATION/inv12/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="3" org.eventb.core.psManual="false"/>
<org.eventb.core.psStatus name="INITIALISATION/inv13/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="3" org.eventb.core.psManual="false"/>
<org.eventb.core.psStatus name="INITIALISATION/inv14/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="3" org.eventb.core.psManual="false"/>
<org.eventb.core.psStatus name="INITIALISATION/inv15/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="3" 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="3" org.eventb.core.psManual="false"/>
</org.eventb.core.psFile>
gateway-event-b/CCTx_Abstract_Animation_m2.bum 0 → 100644
+ 53
− 0
View file @ 75773655
<?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="_k8LVAsEUEe6yC4BToIaAqA" org.eventb.texttools.text_lastmodified="1706800461760" org.eventb.texttools.text_representation="machine CCTx_Abstract_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_CC_TX extends INITIATE_CC_TX&#10; &#9;then&#10; &#9;&#9;@act11 initiated ≔ 1&#10; &#9;&#9;@act12 submit_cc_tx ≔ 0&#10;&#10; end&#10;&#10; event TRIGGER_CC_TX_EVENT extends TRIGGER_CC_TX_EVENT&#10; &#9;then&#10; &#9;&#9;@act11 triggered ≔ 1&#10; &#9;&#9;@act12 initiated ≔ 0&#10; &#9;&#9;@act13 submit_cc_tx ≔ 0&#10; end&#10;&#10; event LISTEN_CC_TX_EVENT extends LISTEN_CC_TX_EVENT&#10; &#9;then&#10; &#9;&#9;@act11 gateway_processing ≔ 1&#10; &#9;&#9;@act12 triggered ≔ 0&#10; &#9;&#9;@act13 submit_cc_tx ≔ 0&#10; end&#10;&#10; event SUBMIT_CC_TX extends SUBMIT_CC_TX&#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="_VBLQ0MEUEe6yC4BToIaAqA" 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="_zZtTYMBBEe6yC4BToIaAqD" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="INITIATE_CC_TX" org.eventb.emf.persistence.emf_id="_k8LU8sEUEe6yC4BToIaAqA">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="INITIATE_CC_TX"/>
<org.eventb.core.action name="_VBQwYMEUEe6yC4BToIaAqA" org.eventb.core.assignment="initiated ≔ 1" org.eventb.core.generated="false" org.eventb.core.label="act11" org.eventb.emf.persistence.emf_id="_k8LU8MEUEe6yC4BToIaAqA"/>
<org.eventb.core.action name="_VBRXccEUEe6yC4BToIaAqA" org.eventb.core.assignment="submit_cc_tx ≔ 0" org.eventb.core.generated="false" org.eventb.core.label="act12" org.eventb.emf.persistence.emf_id="_k8LU8cEUEe6yC4BToIaAqA"/>
</org.eventb.core.event>
<org.eventb.core.event name="_zZtTYMBBEe6yC4BToIaAqE" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="TRIGGER_CC_TX_EVENT" org.eventb.emf.persistence.emf_id="_k8LU98EUEe6yC4BToIaAqA">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="TRIGGER_CC_TX_EVENT"/>
<org.eventb.core.action name="_VBRXcMEUEe6yC4BToIaAqA" org.eventb.core.assignment="triggered ≔ 1" org.eventb.core.generated="false" org.eventb.core.label="act11" org.eventb.emf.persistence.emf_id="_k8LU9MEUEe6yC4BToIaAqA"/>
<org.eventb.core.action name="_VBR-gcEUEe6yC4BToIaAqA" org.eventb.core.assignment="initiated ≔ 0" org.eventb.core.generated="false" org.eventb.core.label="act12" org.eventb.emf.persistence.emf_id="_k8LU9cEUEe6yC4BToIaAqA"/>
<org.eventb.core.action name="_kIrbcMEUEe6yC4BToIaAqA" org.eventb.core.assignment="submit_cc_tx ≔ 0" org.eventb.core.generated="false" org.eventb.core.label="act13" org.eventb.emf.persistence.emf_id="_k8LU9sEUEe6yC4BToIaAqA"/>
</org.eventb.core.event>
<org.eventb.core.event name="_zZtTYMBBEe6yC4BToIaAqF" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="LISTEN_CC_TX_EVENT" org.eventb.emf.persistence.emf_id="_k8LU_MEUEe6yC4BToIaAqA">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="LISTEN_CC_TX_EVENT"/>
<org.eventb.core.action name="_VBR-gMEUEe6yC4BToIaAqA" org.eventb.core.assignment="gateway_processing ≔ 1" org.eventb.core.generated="false" org.eventb.core.label="act11" org.eventb.emf.persistence.emf_id="_k8LU-cEUEe6yC4BToIaAqA"/>
<org.eventb.core.action name="_VBL34cEUEe6yC4BToIaAqA" org.eventb.core.assignment="triggered ≔ 0" org.eventb.core.generated="false" org.eventb.core.label="act12" org.eventb.emf.persistence.emf_id="_k8LU-sEUEe6yC4BToIaAqA"/>
<org.eventb.core.action name="_k8Z-cMEUEe6yC4BToIaAqA" org.eventb.core.assignment="submit_cc_tx ≔ 0" org.eventb.core.generated="false" org.eventb.core.label="act13" org.eventb.emf.persistence.emf_id="_k8LU-8EUEe6yC4BToIaAqA"/>
</org.eventb.core.event>
<org.eventb.core.event name="_zZtTYMBBEe6yC4BToIaAqG" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="SUBMIT_CC_TX" org.eventb.emf.persistence.emf_id="_k8LVAMEUEe6yC4BToIaAqA">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="SUBMIT_CC_TX"/>
<org.eventb.core.action name="_VBL34MEUEe6yC4BToIaAqA" org.eventb.core.assignment="submit_cc_tx ≔ 1" org.eventb.core.generated="false" org.eventb.core.label="act11" org.eventb.emf.persistence.emf_id="_k8LU_sEUEe6yC4BToIaAqA"/>
<org.eventb.core.action name="_isfxUMEUEe6yC4BToIaAqA" org.eventb.core.assignment="gateway_processing ≔ 0" org.eventb.core.generated="false" org.eventb.core.label="act12" org.eventb.emf.persistence.emf_id="_k8LU_8EUEe6yC4BToIaAqA"/>
</org.eventb.core.event>
<org.eventb.core.invariant name="_VBL34sEUEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.label="inv11" org.eventb.core.predicate="subscribed ∈ {0,1}" org.eventb.emf.persistence.emf_id="_k8Kt6sEUEe6yC4BToIaAqA"/>
<org.eventb.core.invariant name="_VBMe8MEUEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.label="inv12" org.eventb.core.predicate="initiated ∈ {0,1}" org.eventb.emf.persistence.emf_id="_k8Kt68EUEe6yC4BToIaAqA"/>
<org.eventb.core.invariant name="_VBMe8cEUEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.label="inv13" org.eventb.core.predicate="triggered ∈ {0,1}" org.eventb.emf.persistence.emf_id="_k8Kt7MEUEe6yC4BToIaAqA"/>
<org.eventb.core.invariant name="_VBNGAMEUEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.label="inv14" org.eventb.core.predicate="gateway_processing ∈ {0,1}" org.eventb.emf.persistence.emf_id="_k8Kt7cEUEe6yC4BToIaAqA"/>
<org.eventb.core.invariant name="_VBNGAcEUEe6yC4BToIaAqA" 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="_k8Kt7sEUEe6yC4BToIaAqA"/>
<org.eventb.core.variable name="_yREdab7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="received_transactions" org.eventb.emf.persistence.emf_id="_k8Kt4MEUEe6yC4BToIaAqA"/>
<org.eventb.core.variable name="_yREdar7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="triggered_events" org.eventb.emf.persistence.emf_id="_k8Kt4cEUEe6yC4BToIaAqA"/>
<org.eventb.core.variable name="_yREda77uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="subscriptions" org.eventb.emf.persistence.emf_id="_k8Kt4sEUEe6yC4BToIaAqA"/>
<org.eventb.core.variable name="_yREdbL7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="gateway_pending_transactions" org.eventb.emf.persistence.emf_id="_k8Kt48EUEe6yC4BToIaAqA"/>
<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="_k8Kt5MEUEe6yC4BToIaAqA"/>
<org.eventb.core.variable name="_65EIQMA-Ee6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.identifier="subscribed" org.eventb.emf.persistence.emf_id="_k8Kt5cEUEe6yC4BToIaAqA"/>
<org.eventb.core.variable name="_zZtTYMBBEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.identifier="initiated" org.eventb.emf.persistence.emf_id="_k8Kt5sEUEe6yC4BToIaAqA"/>
<org.eventb.core.variable name="_RNsgkMBCEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.identifier="triggered" org.eventb.emf.persistence.emf_id="_k8Kt58EUEe6yC4BToIaAqA"/>
<org.eventb.core.variable name="_m7KdIMBDEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.identifier="gateway_processing" org.eventb.emf.persistence.emf_id="_k8Kt6MEUEe6yC4BToIaAqA"/>
<org.eventb.core.variable name="_xgjHcMBDEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.identifier="submit_cc_tx" org.eventb.emf.persistence.emf_id="_k8Kt6cEUEe6yC4BToIaAqA"/>
<org.eventb.core.event name="_zZtTYMBBEe6yC4BToIaAqB" 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="_k8Kt9MEUEe6yC4BToIaAqA">
<org.eventb.core.action name="_VBO7MMEUEe6yC4BToIaAqA" org.eventb.core.assignment="subscribed ≔ 0" org.eventb.core.generated="false" org.eventb.core.label="act11" org.eventb.emf.persistence.emf_id="_k8Kt78EUEe6yC4BToIaAqA"/>
<org.eventb.core.action name="_VBPiQMEUEe6yC4BToIaAqA" org.eventb.core.assignment="initiated ≔ 0" org.eventb.core.generated="false" org.eventb.core.label="act12" org.eventb.emf.persistence.emf_id="_k8Kt8MEUEe6yC4BToIaAqA"/>
<org.eventb.core.action name="_VBPiQcEUEe6yC4BToIaAqA" org.eventb.core.assignment="triggered ≔ 0" org.eventb.core.generated="false" org.eventb.core.label="act13" org.eventb.emf.persistence.emf_id="_k8Kt8cEUEe6yC4BToIaAqA"/>
<org.eventb.core.action name="_VBPiQsEUEe6yC4BToIaAqA" org.eventb.core.assignment="gateway_processing ≔ 0" org.eventb.core.generated="false" org.eventb.core.label="act14" org.eventb.emf.persistence.emf_id="_k8Kt8sEUEe6yC4BToIaAqA"/>
<org.eventb.core.action name="_VBPiQ8EUEe6yC4BToIaAqA" org.eventb.core.assignment="submit_cc_tx ≔ 0" org.eventb.core.generated="false" org.eventb.core.label="act15" org.eventb.emf.persistence.emf_id="_k8Kt88EUEe6yC4BToIaAqA"/>
</org.eventb.core.event>
<org.eventb.core.event name="_zZtTYMBBEe6yC4BToIaAqC" 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="_k8Kt98EUEe6yC4BToIaAqA">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="SUBSCRIBE_SMART_CONTRACT_EVENTS"/>
<org.eventb.core.action name="_VBQJUMEUEe6yC4BToIaAqA" org.eventb.core.assignment="subscribed ≔ 1" org.eventb.core.generated="false" org.eventb.core.label="act11" org.eventb.emf.persistence.emf_id="_k8Kt9sEUEe6yC4BToIaAqA"/>
</org.eventb.core.event>
</org.eventb.core.machineFile>
gateway-prob-animation/abstract-machine/gateway-event-b-animation.svg
+ 2
− 1
View file @ 75773655
......@@ -396,5 +396,6 @@
xlink:href="data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAAMgAAAAoCAYAAAC7HLUcAAAAAXNSR0IArs4c6QAAAARnQU1BAACxjwv8YQUAAAAJcEhZcwAAFiUAABYlAUlSJPAAAAfISURBVHhe7dytj1RLEAXw/UPRJDgSDAKBQGNRaBQagULiUDgUH4ZsCCFBgJiX3749m3693bP33rlzZ3n0SYrZ6VtdVV1dpz9mJpw9efJkd//+/SFDhlTy+PHj3Zk/Hj161FQYMmRtefjw4R9Rb2J88ODB7sw/3pyfn+++fPlyJZ8+fbom5XPy+fPnazraar1ah9Q6a+uN2JbpHTM271++fHlRgO/fv+/qlfqlbJU3Nq8RZGBgC7x69Wp37969iwX5NsPxahBkYHOEIF+/fr1suZ0YBBk4CQZBBgb2YBBkYGAPjkkQF3+yBgZBBk6CYxHk3bt3F3bJGiQZBBk4CdYmyNu3b3dPnz69+n6F+FubZ0vBziDIwOZYiyA/f/7c+RVI6rclvm+hQ3cu9P9jCeIzdKuDL52IpH/48OHy6WH49u3bxXbtC6Pbivqs/ePHj4uYfcG1NcwF31O/11iLIAq/3DV6QofuXOj7RxLk+fPnV2fNu3fvXv1ttZCMQxNvstl9/fr1Zcvtwu/fv69+ChEgi5gV39awUPH95s2by5b9WIMgbOzbOWqRr7nHLf1OSpAl58MXL15cDNYFSlFIspXL7oE4nhEr6lLksjd1wrcGgjhfP3v27LJldzF+4z4Fqc0j31sSpCz+qaJm5kCfkxFEoVt1vE6Fc2TI0QN7xuPYtRS3nSAt/E0EcfTlryz+KaLPnJ+3nOxTLCtffCLJx48fL5/sBz2JtVP0IOls1mfO79+/dy9qnpU7Tk0QE6LtpjsO+3a1KbpgPHT1acVWxkyHTbsHiNfzoCaIH91NjYOtxD3l3sUm3czb1gThO/UzR/QxzqnYnCAmt7xYSeqUCQxMpMTqu+8I9evXr8u//oWJvHPnTpNYCtCzklAmgB/FhswIFxFzK8nZEWvd1jHSmOWg1OVP4QTGJy5tYvCc5FjlbzaCkiB1zOa3FYf5kJNSl8hFq3hbcTvqIcaWBOEnNTRHennoYVOCKEQOMzA+l3xKZEL1ZccxyqTVhKjBjwlpHef09cxEBwhiwhMrQvhkS3L5pl/ueiacPvt80dUnxVQWgnj1Z4c9umzxrz1FhiBsavcaooScbJekZjd58UrPDsOHNrZrYuuvXdxidPxIsbNR7lDGpZ3Q8YxPNuiSQZCFkMz4MDCO9+0AN6G8jEcUksS3kr6UIGKu41RknpXFqS/dGuwYc1k4Kfi6WMWhXSxgQfG+pWvl7xGEflnY4Jn2Ul9MfLXuavzV+UJONoypRGLheyuC2CX/NwSxOsZ+JvWmFX8KJFeiUpwmL6/1UWopQXoXfYnTJ/cDxcO3iU9bC/GlfwsK090BQhA5q9EjCP3WGMH4+LZjle97EGN8x18rFjAPfG9FEP3FUhb/FNFnaoygj3k9GkGy2sZRWYRrwgQqEAXNDylJsoQg2nqrDTue55jFt/fGStgyifyWiF6viEuEIK2c9QjCdq8A+GSPHqTg5akWughC3w7q6MV27j81suNsRRAxLiXInE839TmYIJIp4BqKS4LjpKUzF4q5Pj7U8Jxfko/0lhDE3aE+2gSSrE95D+GLfZPgWWJQxDmmpYinTBKC0G0V5T6C9EidmEuCmBs2kKH1SkfsCtlYenMoD2xvRRBzJfYl0lpweqB/EEGyKpFy0rPlslk/OwQGV196W0hcKfC1dxCF4nnvZx3iUyyKTG5jO4XUKzSxBEsJ0itSPuUkpNbf+ylwLOvFAlvuIAib2loi5qPM8z5EfzFBBJuVSNCIgQwZgCRoWwtsi/UmwplIvnPE2XdEoCPemiDaWoQCMXgOitWEkxbkh28wMQjey7UizgKwhCBi6pGPrufsgvF63yO5HJs7voA/427B2NnagiD6pl6XiL5T44z+QUcsq4vk6C+JIYwEzPnEYAocn9jlr0e8TFZZPDnPt8aoAMXcIoi85JgWZHcsyaO/tvr4x2+dW/7o1rmx2JS62dnmEER/fXIRDxQEnyV5cgQubQSesVPmJAtfvThlRef72ATJYiZHh0hrXltw1KR78CXdJy9l4AavyI6BHH/4IybdpClY40h7nYAUpkGbSKI4vBdziyDa+DKh2nJMUZwlEhP/0WWfXTtCSYbckeiLO7r6asuxUOF5P3cH0cYnIrMtL4mNzRLJiTjFUOprrwuYnnb96GaxSCGxMQVLCJLjqXGvIeIu75AtrEYQyAQRfx8Til+xips/iUsRmOAcI2qkwBUQ/ZBCv5ognntVxP5OH8XROsPSlcNS13vtNRRqijO6CrvM2xKCsMVfCrCMuSZHoMiNv9avdyHgt86hfOcOMvXEMJcgYudHvzXF3PZqBVYlCEjQTaxcG1ZkW29rQnugP/WiBgpjah+TSbdXkCXYUyRTdOciMe8rgBLyR1+/mzAnHy0ozjkEmQLxsFeKtkOwOkEGBqbgGASxo7Jpd8up4tCaHgQZOAmOQRC21HAIorjnnCpaYG8QZGBzHIMgQf5/3TUwCDJwEhyTIGtiEGTgJBgEGRjYgz+FIOOSPnASDIIMDOxBCDLl5x6nxDWCuP37RnbIkGOJL5J9K+6jWN/6t3Rui1zdQQSbN0OGHFPUmi/1bnu9hRNez/wOqaU0ZMjfLn7vdua3NS5MzoSR1u9s/K6n1OldsnyDOUWv9ln/XBxGbNcxYvsvjhvb+e4f63MOYTUJxBUAAAAASUVORK5CYII="
preserveAspectRatio="none"
id="subscription"
inkscape:svg-dpi="1" />
inkscape:svg-dpi="1"
visibility="hidden"/>
</svg>
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment