Skip to content
Snippets Groups Projects
Normal view Permalink
CCTx_Ethereum_Fabric_Animation_m3.bum 13.6 KiB
Newer Older
Guzman Llambias's avatar
Add Ethereum -> Fabric animation (WIP)
Guzman Llambias committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 
<?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="_f2iCRMEaEe6yC4BToIaAqA" org.eventb.texttools.text_lastmodified="1706803004593" org.eventb.texttools.text_representation="machine CCTx_Ethereum_Fabric_Animation_m3 refines CCTx_Ethereum_Fabric_m2  sees CCTx_Ethereum_Fabric_c2&#10;&#10;variables received_transactions triggered_events subscriptions gateway_pending_transactions&#10;received_cross_chain_transactions authenticated_users authenticated_transactions write_grant&#10;subscribed initiated triggered gateway_processing submit_cc_tx user_created&#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;&#9;@inv16 user_created ∈ {0,1}&#10;&#10;events&#10;  event INITIALISATION extends INITIALISATION&#10;   &#9;then&#10;  &#9;&#9;@act31 subscribed ≔ 0&#10;  &#9;&#9;@act32 initiated ≔  0&#10;  &#9;&#9;@act33 triggered ≔  0&#10;  &#9;&#9;@act34 gateway_processing ≔ 0&#10;  &#9;&#9;@act35 submit_cc_tx ≔  0&#10;  &#9;&#9;@act36 user_created ≔  0&#10;  end&#10;&#10;  event SUBSCRIBE_SMART_CONTRACT_EVENTS_IN_ETHEREUM extends SUBSCRIBE_SMART_CONTRACT_EVENTS_IN_ETHEREUM&#10;&#9;then&#10;&#9;&#9;@act31 subscribed ≔ 1&#10;  end&#10;&#10;  event INITIATE_CC_TX_IN_ETHEREUM extends INITIATE_CC_TX_IN_ETHEREUM&#10;  &#9;then&#10;  &#9;&#9;@act31 initiated ≔ 1&#10;  &#9;&#9;@act32 submit_cc_tx ≔ 0&#10;  end&#10;&#10;  event TRIGGER_CC_TX_EVENT_IN_ETHEREUM extends TRIGGER_CC_TX_EVENT_IN_ETHEREUM&#10;  &#9;then&#10;  &#9;&#9;@act31 triggered ≔ 1&#10;  &#9;&#9;@act32 initiated ≔ 0&#10;  &#9;&#9;@act33 submit_cc_tx ≔ 0&#10;  end&#10;&#10;  event LISTEN_CC_TX_EVENT_IN_ETHEREUM extends LISTEN_CC_TX_EVENT_IN_ETHEREUM&#10;  &#9;then&#10;  &#9;&#9;@act31 gateway_processing ≔ 1&#10;  &#9;&#9;@act32 triggered ≔  0&#10;  &#9;&#9;@act33 submit_cc_tx ≔ 0&#10;  end&#10;&#10;  event SUBMIT_CC_TX_TO_FABRIC extends SUBMIT_CC_TX_TO_FABRIC&#10;  &#9;then&#10;  &#9;&#9;@act31 submit_cc_tx ≔ 1&#10;  &#9;&#9;@act32 gateway_processing ≔ 0&#10;  end&#10;&#10;  event CREATE_GATEWAY_USER extends CREATE_GATEWAY_USER&#10;  &#9;then&#10;  &#9;&#9;@act31 user_created ≔ 1&#10;  end&#10;end&#10;" version="5">
    <org.eventb.core.refinesMachine name="'" org.eventb.core.target="CCTx_Ethereum_Fabric_m2"/>
    <org.eventb.core.seesContext name="_1tlAgL7uEe6laZimEYihUg" org.eventb.core.target="CCTx_Ethereum_Fabric_c2"/>
    <org.eventb.core.event name="_yREdbb7uEe6laZimEYihUh" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="INITIALISATION" org.eventb.emf.persistence.emf_id="_f2iCKsEaEe6yC4BToIaAqA">
        <org.eventb.core.action name="_-rC08MEWEe6yC4BToIaAqA" org.eventb.core.assignment="subscribed ≔ 0" org.eventb.core.generated="false" org.eventb.core.label="act31" org.eventb.emf.persistence.emf_id="_f2iCJMEaEe6yC4BToIaAqA"/>
        <org.eventb.core.action name="_-rC08cEWEe6yC4BToIaAqA" org.eventb.core.assignment="initiated ≔  0" org.eventb.core.generated="false" org.eventb.core.label="act32" org.eventb.emf.persistence.emf_id="_f2iCJcEaEe6yC4BToIaAqA"/>
        <org.eventb.core.action name="_-rDcAMEWEe6yC4BToIaAqA" org.eventb.core.assignment="triggered ≔  0" org.eventb.core.generated="false" org.eventb.core.label="act33" org.eventb.emf.persistence.emf_id="_f2iCJsEaEe6yC4BToIaAqA"/>
        <org.eventb.core.action name="_-rDcAcEWEe6yC4BToIaAqA" org.eventb.core.assignment="gateway_processing ≔ 0" org.eventb.core.generated="false" org.eventb.core.label="act34" org.eventb.emf.persistence.emf_id="_f2iCJ8EaEe6yC4BToIaAqA"/>
        <org.eventb.core.action name="_-rEDEMEWEe6yC4BToIaAqA" org.eventb.core.assignment="submit_cc_tx ≔  0" org.eventb.core.generated="false" org.eventb.core.label="act35" org.eventb.emf.persistence.emf_id="_f2iCKMEaEe6yC4BToIaAqA"/>
        <org.eventb.core.action name="_bpmHkMEaEe6yC4BToIaAqA" org.eventb.core.assignment="user_created ≔  0" org.eventb.core.generated="false" org.eventb.core.label="act36" org.eventb.emf.persistence.emf_id="_f2iCKcEaEe6yC4BToIaAqA"/>
    </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_IN_ETHEREUM" org.eventb.emf.persistence.emf_id="_f2iCLcEaEe6yC4BToIaAqA">
        <org.eventb.core.refinesEvent name="'" org.eventb.core.target="SUBSCRIBE_SMART_CONTRACT_EVENTS_IN_ETHEREUM"/>
        <org.eventb.core.action name="_-rEqIMEWEe6yC4BToIaAqA" org.eventb.core.assignment="subscribed ≔ 1" org.eventb.core.generated="false" org.eventb.core.label="act31" org.eventb.emf.persistence.emf_id="_f2iCLMEaEe6yC4BToIaAqA"/>
    </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_CC_TX_IN_ETHEREUM" org.eventb.emf.persistence.emf_id="_f2iCMcEaEe6yC4BToIaAqA">
        <org.eventb.core.refinesEvent name="'" org.eventb.core.target="INITIATE_CC_TX_IN_ETHEREUM"/>
        <org.eventb.core.action name="_-rFRMMEWEe6yC4BToIaAqA" org.eventb.core.assignment="initiated ≔ 1" org.eventb.core.generated="false" org.eventb.core.label="act31" org.eventb.emf.persistence.emf_id="_f2iCL8EaEe6yC4BToIaAqA"/>
        <org.eventb.core.action name="_-rFRMcEWEe6yC4BToIaAqA" org.eventb.core.assignment="submit_cc_tx ≔ 0" org.eventb.core.generated="false" org.eventb.core.label="act32" org.eventb.emf.persistence.emf_id="_f2iCMMEaEe6yC4BToIaAqA"/>
    </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="TRIGGER_CC_TX_EVENT_IN_ETHEREUM" org.eventb.emf.persistence.emf_id="_f2iCNsEaEe6yC4BToIaAqA">
        <org.eventb.core.refinesEvent name="'" org.eventb.core.target="TRIGGER_CC_TX_EVENT_IN_ETHEREUM"/>
        <org.eventb.core.action name="_-rF4QMEWEe6yC4BToIaAqA" org.eventb.core.assignment="triggered ≔ 1" org.eventb.core.generated="false" org.eventb.core.label="act31" org.eventb.emf.persistence.emf_id="_f2iCM8EaEe6yC4BToIaAqA"/>
        <org.eventb.core.action name="_-rF4QcEWEe6yC4BToIaAqA" org.eventb.core.assignment="initiated ≔ 0" org.eventb.core.generated="false" org.eventb.core.label="act32" org.eventb.emf.persistence.emf_id="_f2iCNMEaEe6yC4BToIaAqA"/>
        <org.eventb.core.action name="_-rGfUMEWEe6yC4BToIaAqA" org.eventb.core.assignment="submit_cc_tx ≔ 0" org.eventb.core.generated="false" org.eventb.core.label="act33" org.eventb.emf.persistence.emf_id="_f2iCNcEaEe6yC4BToIaAqA"/>
    </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_CC_TX_EVENT_IN_ETHEREUM" org.eventb.emf.persistence.emf_id="_f2iCO8EaEe6yC4BToIaAqA">
        <org.eventb.core.refinesEvent name="'" org.eventb.core.target="LISTEN_CC_TX_EVENT_IN_ETHEREUM"/>
        <org.eventb.core.action name="_-rHGYMEWEe6yC4BToIaAqA" org.eventb.core.assignment="gateway_processing ≔ 1" org.eventb.core.generated="false" org.eventb.core.label="act31" org.eventb.emf.persistence.emf_id="_f2iCOMEaEe6yC4BToIaAqA"/>
        <org.eventb.core.action name="_-rHGYcEWEe6yC4BToIaAqA" org.eventb.core.assignment="triggered ≔  0" org.eventb.core.generated="false" org.eventb.core.label="act32" org.eventb.emf.persistence.emf_id="_f2iCOcEaEe6yC4BToIaAqA"/>
        <org.eventb.core.action name="_-rHGYsEWEe6yC4BToIaAqA" org.eventb.core.assignment="submit_cc_tx ≔ 0" org.eventb.core.generated="false" org.eventb.core.label="act33" org.eventb.emf.persistence.emf_id="_f2iCOsEaEe6yC4BToIaAqA"/>
    </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="SUBMIT_CC_TX_TO_FABRIC" org.eventb.emf.persistence.emf_id="_f2iCP8EaEe6yC4BToIaAqA">
        <org.eventb.core.refinesEvent name="'" org.eventb.core.target="SUBMIT_CC_TX_TO_FABRIC"/>
        <org.eventb.core.action name="_-rHtcMEWEe6yC4BToIaAqA" org.eventb.core.assignment="submit_cc_tx ≔ 1" org.eventb.core.generated="false" org.eventb.core.label="act31" org.eventb.emf.persistence.emf_id="_f2iCPcEaEe6yC4BToIaAqA"/>
        <org.eventb.core.action name="_-rIUgMEWEe6yC4BToIaAqA" org.eventb.core.assignment="gateway_processing ≔ 0" org.eventb.core.generated="false" org.eventb.core.label="act32" org.eventb.emf.persistence.emf_id="_f2iCPsEaEe6yC4BToIaAqA"/>
    </org.eventb.core.event>
    <org.eventb.core.event name="_g3fQIMEXEe6yC4BToIaAqA" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="CREATE_GATEWAY_USER" org.eventb.emf.persistence.emf_id="_f2iCQsEaEe6yC4BToIaAqA">
        <org.eventb.core.refinesEvent name="_g3f3MMEXEe6yC4BToIaAqA" org.eventb.core.target="CREATE_GATEWAY_USER"/>
        <org.eventb.core.action name="_f3UFMMEaEe6yC4BToIaAqA" org.eventb.core.assignment="user_created ≔ 1" org.eventb.core.generated="false" org.eventb.core.label="act31" org.eventb.emf.persistence.emf_id="_f2iCQcEaEe6yC4BToIaAqA"/>
    </org.eventb.core.event>
    <org.eventb.core.invariant name="_t-t3AMEVEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.label="inv11" org.eventb.core.predicate="subscribed ∈ {0,1}" org.eventb.emf.persistence.emf_id="_f2iCHsEaEe6yC4BToIaAqA"/>
    <org.eventb.core.invariant name="_t-t3AcEVEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.label="inv12" org.eventb.core.predicate="initiated ∈ {0,1}" org.eventb.emf.persistence.emf_id="_f2iCH8EaEe6yC4BToIaAqA"/>
    <org.eventb.core.invariant name="_t-ueEMEVEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.label="inv13" org.eventb.core.predicate="triggered ∈ {0,1}" org.eventb.emf.persistence.emf_id="_f2iCIMEaEe6yC4BToIaAqA"/>
    <org.eventb.core.invariant name="_t-ueEcEVEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.label="inv14" org.eventb.core.predicate="gateway_processing ∈ {0,1}" org.eventb.emf.persistence.emf_id="_f2iCIcEaEe6yC4BToIaAqA"/>
    <org.eventb.core.invariant name="_t-vFIMEVEe6yC4BToIaAqA" 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="_f2iCIsEaEe6yC4BToIaAqA"/>
    <org.eventb.core.invariant name="_ZH0uYMEaEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.label="inv16" org.eventb.core.predicate="user_created ∈ {0,1}" org.eventb.emf.persistence.emf_id="_f2iCI8EaEe6yC4BToIaAqA"/>
    <org.eventb.core.variable name="_yREdab7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="received_transactions" org.eventb.emf.persistence.emf_id="_f2iCEMEaEe6yC4BToIaAqA"/>
    <org.eventb.core.variable name="_yREdar7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="triggered_events" org.eventb.emf.persistence.emf_id="_f2iCEcEaEe6yC4BToIaAqA"/>
    <org.eventb.core.variable name="_yREda77uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="subscriptions" org.eventb.emf.persistence.emf_id="_f2iCEsEaEe6yC4BToIaAqA"/>
    <org.eventb.core.variable name="_yREdbL7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="gateway_pending_transactions" org.eventb.emf.persistence.emf_id="_f2iCE8EaEe6yC4BToIaAqA"/>
    <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="_f2iCFMEaEe6yC4BToIaAqA"/>
    <org.eventb.core.variable name="_1toq4L7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="authenticated_users" org.eventb.emf.persistence.emf_id="_f2iCFcEaEe6yC4BToIaAqA"/>
    <org.eventb.core.variable name="_1toq4b7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="authenticated_transactions" org.eventb.emf.persistence.emf_id="_f2iCFsEaEe6yC4BToIaAqA"/>
    <org.eventb.core.variable name="_1toq4r7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="write_grant" org.eventb.emf.persistence.emf_id="_f2iCF8EaEe6yC4BToIaAqA"/>
    <org.eventb.core.variable name="_t-w6UMEVEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.identifier="subscribed" org.eventb.emf.persistence.emf_id="_f2iCGMEaEe6yC4BToIaAqA"/>
    <org.eventb.core.variable name="_t-xhYMEVEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.identifier="initiated" org.eventb.emf.persistence.emf_id="_f2iCGcEaEe6yC4BToIaAqA"/>
    <org.eventb.core.variable name="_t-xhYcEVEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.identifier="triggered" org.eventb.emf.persistence.emf_id="_f2iCGsEaEe6yC4BToIaAqA"/>
    <org.eventb.core.variable name="_t-xhYsEVEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.identifier="gateway_processing" org.eventb.emf.persistence.emf_id="_f2iCG8EaEe6yC4BToIaAqA"/>
    <org.eventb.core.variable name="_t-yIcMEVEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.identifier="submit_cc_tx" org.eventb.emf.persistence.emf_id="_f2iCHMEaEe6yC4BToIaAqA"/>
    <org.eventb.core.variable name="_ZH18gMEaEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.identifier="user_created" org.eventb.emf.persistence.emf_id="_f2iCHcEaEe6yC4BToIaAqA"/>
</org.eventb.core.machineFile>