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
Change trigger for emit event  
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="_TPpq6_KWEe60CqkwWvstGA" org.eventb.texttools.text_lastmodified="1712243784556" 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 emitted_events subscriptions gateway_pending_transactions received_cross_chain_transactions subscribed initiated emitted gateway_processing submit_cc_tx&#10;&#10;invariants&#10;&#9;@inv11 subscribed ∈ {0,1}&#10;&#9;@inv12 initiated ∈ {0,1}&#10;&#9;@inv13 emitted ∈ {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 emitted ≔  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 EMIT_CC_TX_EVENT extends EMIT_CC_TX_EVENT&#10;  &#9;then&#10;  &#9;&#9;@act11 emitted ≔ 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 emitted ≔  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
Change trigger for emit event  
Guzman Llambias committed
5 6 7 8 9 10 11 12 
    <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="_TPpq1PKWEe60CqkwWvstGA">
        <org.eventb.core.action name="_VBQJUMEUEe6yC4BToIaAqA" org.eventb.core.assignment="subscribed ≔ 0" org.eventb.core.generated="false" org.eventb.core.label="act11" org.eventb.emf.persistence.emf_id="_TPpqz_KWEe60CqkwWvstGA"/>
        <org.eventb.core.action name="_VBRXccEUEe6yC4BToIaAqA" org.eventb.core.assignment="initiated ≔  0" org.eventb.core.generated="false" org.eventb.core.label="act12" org.eventb.emf.persistence.emf_id="_TPpq0PKWEe60CqkwWvstGA"/>
        <org.eventb.core.action name="_kIrbcMEUEe6yC4BToIaAqA" org.eventb.core.assignment="emitted ≔  0" org.eventb.core.generated="false" org.eventb.core.label="act13" org.eventb.emf.persistence.emf_id="_TPpq0fKWEe60CqkwWvstGA"/>
        <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="_TPpq0vKWEe60CqkwWvstGA"/>
        <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="_TPpq0_KWEe60CqkwWvstGA"/>
    </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="_TPpq1_KWEe60CqkwWvstGA">
Guzman Llambias's avatar
Add Ethereum -> Fabric animation (WIP)  
Guzman Llambias committed
13 
        <org.eventb.core.refinesEvent name="'" org.eventb.core.target="SUBSCRIBE_SMART_CONTRACT_EVENTS"/>
Guzman Llambias's avatar
Change trigger for emit event  
Guzman Llambias committed
14 
        <org.eventb.core.action name="_VBQwYMEUEe6yC4BToIaAqA" org.eventb.core.assignment="subscribed ≔ 1" org.eventb.core.generated="false" org.eventb.core.label="act11" org.eventb.emf.persistence.emf_id="_TPpq1vKWEe60CqkwWvstGA"/>
Guzman Llambias's avatar
Add Ethereum -> Fabric animation (WIP)  
Guzman Llambias committed
15 
    </org.eventb.core.event>
Guzman Llambias's avatar
Change trigger for emit event  
Guzman Llambias committed
16 
    <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="_TPpq2_KWEe60CqkwWvstGA">
Guzman Llambias's avatar
Improve abstract machine animation
Guzman Llambias committed
17 
        <org.eventb.core.refinesEvent name="'" org.eventb.core.target="INITIATE_CC_TX"/>
Guzman Llambias's avatar
Change trigger for emit event  
Guzman Llambias committed
18 19 
        <org.eventb.core.action name="_VBRXcMEUEe6yC4BToIaAqA" org.eventb.core.assignment="initiated ≔ 1" org.eventb.core.generated="false" org.eventb.core.label="act11" org.eventb.emf.persistence.emf_id="_TPpq2fKWEe60CqkwWvstGA"/>
        <org.eventb.core.action name="_VBR-gcEUEe6yC4BToIaAqA" org.eventb.core.assignment="submit_cc_tx ≔ 0" org.eventb.core.generated="false" org.eventb.core.label="act12" org.eventb.emf.persistence.emf_id="_TPpq2vKWEe60CqkwWvstGA"/>
Guzman Llambias's avatar
Improve abstract machine animation
Guzman Llambias committed
20 
    </org.eventb.core.event>
Guzman Llambias's avatar
Change trigger for emit event  
Guzman Llambias committed
21 22 23 24 25 
    <org.eventb.core.event name="_RGg0TPKWEe60CqkwWvstGA" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="EMIT_CC_TX_EVENT" org.eventb.emf.persistence.emf_id="_TPpq4PKWEe60CqkwWvstGA">
        <org.eventb.core.refinesEvent name="_RGg0TfKWEe60CqkwWvstGA" org.eventb.core.target="EMIT_CC_TX_EVENT"/>
        <org.eventb.core.action name="_VBR-gMEUEe6yC4BToIaAqA" org.eventb.core.assignment="emitted ≔ 1" org.eventb.core.generated="false" org.eventb.core.label="act11" org.eventb.emf.persistence.emf_id="_TPpq3fKWEe60CqkwWvstGA"/>
        <org.eventb.core.action name="_VBL34cEUEe6yC4BToIaAqA" org.eventb.core.assignment="initiated ≔ 0" org.eventb.core.generated="false" org.eventb.core.label="act12" org.eventb.emf.persistence.emf_id="_TPpq3vKWEe60CqkwWvstGA"/>
        <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="_TPpq3_KWEe60CqkwWvstGA"/>
Guzman Llambias's avatar
Improve abstract machine animation
Guzman Llambias committed
26 
    </org.eventb.core.event>
Guzman Llambias's avatar
Change trigger for emit event  
Guzman Llambias committed
27 
    <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="_TPpq5fKWEe60CqkwWvstGA">
Guzman Llambias's avatar
Improve abstract machine animation
Guzman Llambias committed
28 
        <org.eventb.core.refinesEvent name="'" org.eventb.core.target="LISTEN_CC_TX_EVENT"/>
Guzman Llambias's avatar
Change trigger for emit event  
Guzman Llambias committed
29 30 31 
        <org.eventb.core.action name="_VBL34MEUEe6yC4BToIaAqA" org.eventb.core.assignment="gateway_processing ≔ 1" org.eventb.core.generated="false" org.eventb.core.label="act11" org.eventb.emf.persistence.emf_id="_TPpq4vKWEe60CqkwWvstGA"/>
        <org.eventb.core.action name="_isfxUMEUEe6yC4BToIaAqA" org.eventb.core.assignment="emitted ≔  0" org.eventb.core.generated="false" org.eventb.core.label="act12" org.eventb.emf.persistence.emf_id="_TPpq4_KWEe60CqkwWvstGA"/>
        <org.eventb.core.action name="_VBPiQcEUEe6yC4BToIaAqA" org.eventb.core.assignment="submit_cc_tx ≔ 0" org.eventb.core.generated="false" org.eventb.core.label="act13" org.eventb.emf.persistence.emf_id="_TPpq5PKWEe60CqkwWvstGA"/>
Guzman Llambias's avatar
Improve abstract machine animation
Guzman Llambias committed
32 
    </org.eventb.core.event>
Guzman Llambias's avatar
Change trigger for emit event  
Guzman Llambias committed
33 
    <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="_TPpq6fKWEe60CqkwWvstGA">
Guzman Llambias's avatar
Improve abstract machine animation
Guzman Llambias committed
34 
        <org.eventb.core.refinesEvent name="'" org.eventb.core.target="SUBMIT_CC_TX"/>
Guzman Llambias's avatar
Change trigger for emit event  
Guzman Llambias committed
35 36 
        <org.eventb.core.action name="_VBO7MMEUEe6yC4BToIaAqA" org.eventb.core.assignment="submit_cc_tx ≔ 1" org.eventb.core.generated="false" org.eventb.core.label="act11" org.eventb.emf.persistence.emf_id="_TPpq5_KWEe60CqkwWvstGA"/>
        <org.eventb.core.action name="_VBPiQMEUEe6yC4BToIaAqA" org.eventb.core.assignment="gateway_processing ≔ 0" org.eventb.core.generated="false" org.eventb.core.label="act12" org.eventb.emf.persistence.emf_id="_TPpq6PKWEe60CqkwWvstGA"/>
Guzman Llambias's avatar
Improve abstract machine animation
Guzman Llambias committed
37 
    </org.eventb.core.event>
Guzman Llambias's avatar
Change trigger for emit event  
Guzman Llambias committed
38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 
    <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="_TPpqyvKWEe60CqkwWvstGA"/>
    <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="_TPpqy_KWEe60CqkwWvstGA"/>
    <org.eventb.core.invariant name="_VBMe8cEUEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.label="inv13" org.eventb.core.predicate="emitted ∈ {0,1}" org.eventb.emf.persistence.emf_id="_TPpqzPKWEe60CqkwWvstGA"/>
    <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="_TPpqzfKWEe60CqkwWvstGA"/>
    <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="_TPpqzvKWEe60CqkwWvstGA"/>
    <org.eventb.core.variable name="_yREdab7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="received_transactions" org.eventb.emf.persistence.emf_id="_TPpqwPKWEe60CqkwWvstGA"/>
    <org.eventb.core.variable name="_RGqlAPKWEe60CqkwWvstGA" org.eventb.core.generated="false" org.eventb.core.identifier="emitted_events" org.eventb.emf.persistence.emf_id="_TPpqwfKWEe60CqkwWvstGA"/>
    <org.eventb.core.variable name="_yREda77uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="subscriptions" org.eventb.emf.persistence.emf_id="_TPpqwvKWEe60CqkwWvstGA"/>
    <org.eventb.core.variable name="_yREdbL7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="gateway_pending_transactions" org.eventb.emf.persistence.emf_id="_TPpqw_KWEe60CqkwWvstGA"/>
    <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="_TPpqxPKWEe60CqkwWvstGA"/>
    <org.eventb.core.variable name="_65EIQMA-Ee6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.identifier="subscribed" org.eventb.emf.persistence.emf_id="_TPpqxfKWEe60CqkwWvstGA"/>
    <org.eventb.core.variable name="_zZtTYMBBEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.identifier="initiated" org.eventb.emf.persistence.emf_id="_TPpqxvKWEe60CqkwWvstGA"/>
    <org.eventb.core.variable name="_TP7-oPKWEe60CqkwWvstGA" org.eventb.core.generated="false" org.eventb.core.identifier="emitted" org.eventb.emf.persistence.emf_id="_TPpqx_KWEe60CqkwWvstGA"/>
    <org.eventb.core.variable name="_m7KdIMBDEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.identifier="gateway_processing" org.eventb.emf.persistence.emf_id="_TPpqyPKWEe60CqkwWvstGA"/>
    <org.eventb.core.variable name="_xgjHcMBDEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.identifier="submit_cc_tx" org.eventb.emf.persistence.emf_id="_TPpqyfKWEe60CqkwWvstGA"/>
Guzman Llambias's avatar
Improve abstract machine animation
Guzman Llambias committed
53 
</org.eventb.core.machineFile>