Skip to content
Snippets Groups Projects
Normal view Permalink
CCTx_Abstract_Animation_m2.bum 11.2 KiB
Newer Older
Guzman Llambias's avatar
Improve abstract machine animation
Guzman Llambias committed
1 
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
Guzman Llambias's avatar
Add Ethereum -> Fabric animation (WIP)  
Guzman Llambias committed
2 
<org.eventb.core.machineFile org.eventb.core.configuration="org.eventb.core.fwd" org.eventb.core.generated="false" org.eventb.emf.persistence.emf_id="_mS9FW8EVEe6yC4BToIaAqA" org.eventb.texttools.text_lastmodified="1706800900357" 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;  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">
Guzman Llambias's avatar
Improve abstract machine animation
Guzman Llambias committed
3 4 
    <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"/>
Guzman Llambias's avatar
Add Ethereum -> Fabric animation (WIP)  
Guzman Llambias committed
5 6 7 8 9 
    <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="_mS9FR8EVEe6yC4BToIaAqA">
        <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="_mS9FRsEVEe6yC4BToIaAqA"/>
    </org.eventb.core.event>
    <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="_mS9FS8EVEe6yC4BToIaAqA">
Guzman Llambias's avatar
Improve abstract machine animation
Guzman Llambias committed
10 
        <org.eventb.core.refinesEvent name="'" org.eventb.core.target="INITIATE_CC_TX"/>
Guzman Llambias's avatar
Add Ethereum -> Fabric animation (WIP)  
Guzman Llambias committed
11 12 
        <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="_mS9FScEVEe6yC4BToIaAqA"/>
        <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="_mS9FSsEVEe6yC4BToIaAqA"/>
Guzman Llambias's avatar
Improve abstract machine animation
Guzman Llambias committed
13 
    </org.eventb.core.event>
Guzman Llambias's avatar
Add Ethereum -> Fabric animation (WIP)  
Guzman Llambias committed
14 
    <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="_mS9FUMEVEe6yC4BToIaAqA">
Guzman Llambias's avatar
Improve abstract machine animation
Guzman Llambias committed
15 
        <org.eventb.core.refinesEvent name="'" org.eventb.core.target="TRIGGER_CC_TX_EVENT"/>
Guzman Llambias's avatar
Add Ethereum -> Fabric animation (WIP)  
Guzman Llambias committed
16 17 18 
        <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="_mS9FTcEVEe6yC4BToIaAqA"/>
        <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="_mS9FTsEVEe6yC4BToIaAqA"/>
        <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="_mS9FT8EVEe6yC4BToIaAqA"/>
Guzman Llambias's avatar
Improve abstract machine animation
Guzman Llambias committed
19 
    </org.eventb.core.event>
Guzman Llambias's avatar
Add Ethereum -> Fabric animation (WIP)  
Guzman Llambias committed
20 
    <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="_mS9FVcEVEe6yC4BToIaAqA">
Guzman Llambias's avatar
Improve abstract machine animation
Guzman Llambias committed
21 
        <org.eventb.core.refinesEvent name="'" org.eventb.core.target="LISTEN_CC_TX_EVENT"/>
Guzman Llambias's avatar
Add Ethereum -> Fabric animation (WIP)  
Guzman Llambias committed
22 23 24 
        <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="_mS9FUsEVEe6yC4BToIaAqA"/>
        <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="_mS9FU8EVEe6yC4BToIaAqA"/>
        <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="_mS9FVMEVEe6yC4BToIaAqA"/>
Guzman Llambias's avatar
Improve abstract machine animation
Guzman Llambias committed
25 
    </org.eventb.core.event>
Guzman Llambias's avatar
Add Ethereum -> Fabric animation (WIP)  
Guzman Llambias committed
26 
    <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="_mS9FWcEVEe6yC4BToIaAqA">
Guzman Llambias's avatar
Improve abstract machine animation
Guzman Llambias committed
27 
        <org.eventb.core.refinesEvent name="'" org.eventb.core.target="SUBMIT_CC_TX"/>
Guzman Llambias's avatar
Add Ethereum -> Fabric animation (WIP)  
Guzman Llambias committed
28 29 
        <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="_mS9FV8EVEe6yC4BToIaAqA"/>
        <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="_mS9FWMEVEe6yC4BToIaAqA"/>
Guzman Llambias's avatar
Improve abstract machine animation
Guzman Llambias committed
30 
    </org.eventb.core.event>
Guzman Llambias's avatar
Add Ethereum -> Fabric animation (WIP)  
Guzman Llambias committed
31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 
    <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="_mS9FOsEVEe6yC4BToIaAqA"/>
    <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="_mS9FO8EVEe6yC4BToIaAqA"/>
    <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="_mS9FPMEVEe6yC4BToIaAqA"/>
    <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="_mS9FPcEVEe6yC4BToIaAqA"/>
    <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="_mS9FPsEVEe6yC4BToIaAqA"/>
    <org.eventb.core.variable name="_yREdab7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="received_transactions" org.eventb.emf.persistence.emf_id="_mS9FMMEVEe6yC4BToIaAqA"/>
    <org.eventb.core.variable name="_yREdar7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="triggered_events" org.eventb.emf.persistence.emf_id="_mS9FMcEVEe6yC4BToIaAqA"/>
    <org.eventb.core.variable name="_yREda77uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="subscriptions" org.eventb.emf.persistence.emf_id="_mS9FMsEVEe6yC4BToIaAqA"/>
    <org.eventb.core.variable name="_yREdbL7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="gateway_pending_transactions" org.eventb.emf.persistence.emf_id="_mS9FM8EVEe6yC4BToIaAqA"/>
    <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="_mS9FNMEVEe6yC4BToIaAqA"/>
    <org.eventb.core.variable name="_65EIQMA-Ee6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.identifier="subscribed" org.eventb.emf.persistence.emf_id="_mS9FNcEVEe6yC4BToIaAqA"/>
    <org.eventb.core.variable name="_zZtTYMBBEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.identifier="initiated" org.eventb.emf.persistence.emf_id="_mS9FNsEVEe6yC4BToIaAqA"/>
    <org.eventb.core.variable name="_RNsgkMBCEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.identifier="triggered" org.eventb.emf.persistence.emf_id="_mS9FN8EVEe6yC4BToIaAqA"/>
    <org.eventb.core.variable name="_m7KdIMBDEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.identifier="gateway_processing" org.eventb.emf.persistence.emf_id="_mS9FOMEVEe6yC4BToIaAqA"/>
    <org.eventb.core.variable name="_xgjHcMBDEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.identifier="submit_cc_tx" org.eventb.emf.persistence.emf_id="_mS9FOcEVEe6yC4BToIaAqA"/>
    <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="_mS9FRMEVEe6yC4BToIaAqA">
        <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="_mS9FP8EVEe6yC4BToIaAqA"/>
        <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="_mS9FQMEVEe6yC4BToIaAqA"/>
        <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="_mS9FQcEVEe6yC4BToIaAqA"/>
        <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="_mS9FQsEVEe6yC4BToIaAqA"/>
        <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="_mS9FQ8EVEe6yC4BToIaAqA"/>
Guzman Llambias's avatar
Improve abstract machine animation
Guzman Llambias committed
52 53 
    </org.eventb.core.event>
</org.eventb.core.machineFile>