Skip to content
Snippets Groups Projects
Normal view Permalink
CCTx_Ethereum_Fabric_Animation_m3.bum 15.5 KiB
Newer Older
Guzman Llambias's avatar
Add Ethereum -> Fabric animation (WIP)
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="_WiIIXPKWEe60CqkwWvstGA" org.eventb.texttools.text_lastmodified="1712243806626" 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 emitted_events subscriptions gateway_pending_transactions received_cross_chain_transactions authenticated_users authenticated_transactions grants subscribed initiated emitted gateway_processing submit_cc_tx user_created write_granted&#10;&#10;invariants&#10;  @inv11 subscribed ∈ {0,1}&#10;  @inv12 initiated ∈ {0,1}&#10;  @inv13 emitted ∈ {0,1}&#10;  @inv14 gateway_processing ∈ {0,1}&#10;  @inv15 submit_cc_tx ∈ {0,1}&#10;  @inv16 user_created ∈ {0,1}&#10;  @inv17 write_granted ∈ {0,1}&#10;&#10;events&#10;  event INITIALISATION extends INITIALISATION&#10;    then&#10;      @act31 subscribed ≔ 0&#10;      @act32 initiated ≔  0&#10;      @act33 emitted ≔  0&#10;      @act34 gateway_processing ≔ 0&#10;      @act35 submit_cc_tx ≔  0&#10;      @act36 user_created ≔  0&#10;      @act37 write_granted ≔  0&#10;  end&#10;&#10;  event SUBSCRIBE_SMART_CONTRACT_EVENTS_IN_ETHEREUM extends SUBSCRIBE_SMART_CONTRACT_EVENTS_IN_ETHEREUM&#10;    then&#10;      @act31 subscribed ≔ 1&#10;  end&#10;&#10;  event INITIATE_CC_TX_IN_ETHEREUM extends INITIATE_CC_TX_IN_ETHEREUM&#10;    then&#10;      @act31 initiated ≔ 1&#10;      @act32 submit_cc_tx ≔ 0&#10;  end&#10;&#10;  event EMIT_CC_TX_EVENT_IN_ETHEREUM extends EMIT_CC_TX_EVENT_IN_ETHEREUM&#10;    then&#10;      @act31 emitted ≔ 1&#10;      @act32 initiated ≔ 0&#10;      @act33 submit_cc_tx ≔ 0&#10;  end&#10;&#10;  event LISTEN_CC_TX_EVENT_IN_ETHEREUM extends LISTEN_CC_TX_EVENT_IN_ETHEREUM&#10;    then&#10;      @act31 gateway_processing ≔ 1&#10;      @act32 emitted ≔  0&#10;      @act33 submit_cc_tx ≔ 0&#10;  end&#10;&#10;  event SUBMIT_CC_TX_TO_FABRIC extends SUBMIT_CC_TX_TO_FABRIC&#10;    then&#10;      @act31 submit_cc_tx ≔ 1&#10;      @act32 gateway_processing ≔ 0&#10;  end&#10;&#10;  event CREATE_GATEWAY_USER extends CREATE_GATEWAY_USER&#10;    then&#10;      @act31 user_created ≔ 1&#10;  end&#10;&#10;  event GRANT_PERMISSION extends GRANT_PERMISSION&#10;    where&#10;      @grd31 user = gateway_user&#10;      @grd32 permission = write&#10;    then&#10;      @act31 write_granted ≔ 1&#10;  end&#10;end&#10;" version="5">
Guzman Llambias's avatar
Add Ethereum -> Fabric animation (WIP)
Guzman Llambias committed
3 4 
    <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"/>
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="_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="_WiIIPfKWEe60CqkwWvstGA">
        <org.eventb.core.action name="_FVN5wMHOEe609fto5wotHA" org.eventb.core.assignment="subscribed ≔ 0" org.eventb.core.generated="false" org.eventb.core.label="act31" org.eventb.emf.persistence.emf_id="_WiIINvKWEe60CqkwWvstGA"/>
        <org.eventb.core.action name="_FVN5wcHOEe609fto5wotHA" org.eventb.core.assignment="initiated ≔  0" org.eventb.core.generated="false" org.eventb.core.label="act32" org.eventb.emf.persistence.emf_id="_WiIIN_KWEe60CqkwWvstGA"/>
        <org.eventb.core.action name="_FVOg0MHOEe609fto5wotHA" org.eventb.core.assignment="emitted ≔  0" org.eventb.core.generated="false" org.eventb.core.label="act33" org.eventb.emf.persistence.emf_id="_WiIIOPKWEe60CqkwWvstGA"/>
        <org.eventb.core.action name="_FVOg0cHOEe609fto5wotHA" org.eventb.core.assignment="gateway_processing ≔ 0" org.eventb.core.generated="false" org.eventb.core.label="act34" org.eventb.emf.persistence.emf_id="_WiIIOfKWEe60CqkwWvstGA"/>
        <org.eventb.core.action name="_FVPH4MHOEe609fto5wotHA" org.eventb.core.assignment="submit_cc_tx ≔  0" org.eventb.core.generated="false" org.eventb.core.label="act35" org.eventb.emf.persistence.emf_id="_WiIIOvKWEe60CqkwWvstGA"/>
        <org.eventb.core.action name="_FVPH4cHOEe609fto5wotHA" org.eventb.core.assignment="user_created ≔  0" org.eventb.core.generated="false" org.eventb.core.label="act36" org.eventb.emf.persistence.emf_id="_WiIIO_KWEe60CqkwWvstGA"/>
        <org.eventb.core.action name="_4VMjkMHOEe609fto5wotHA" org.eventb.core.assignment="write_granted ≔  0" org.eventb.core.generated="false" org.eventb.core.label="act37" org.eventb.emf.persistence.emf_id="_WiIIPPKWEe60CqkwWvstGA"/>
Guzman Llambias's avatar
Complete Ethereum -> Fabric animation  
Guzman Llambias committed
13 
    </org.eventb.core.event>
Guzman Llambias's avatar
Change trigger for emit event  
Guzman Llambias committed
14 
    <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="_WiIIQPKWEe60CqkwWvstGA">
Guzman Llambias's avatar
Add Ethereum -> Fabric animation (WIP)
Guzman Llambias committed
15 
        <org.eventb.core.refinesEvent name="'" org.eventb.core.target="SUBSCRIBE_SMART_CONTRACT_EVENTS_IN_ETHEREUM"/>
Guzman Llambias's avatar
Change trigger for emit event  
Guzman Llambias committed
16 
        <org.eventb.core.action name="_G4NWgMHOEe609fto5wotHA" org.eventb.core.assignment="subscribed ≔ 1" org.eventb.core.generated="false" org.eventb.core.label="act31" org.eventb.emf.persistence.emf_id="_WiIIP_KWEe60CqkwWvstGA"/>
Guzman Llambias's avatar
Add Ethereum -> Fabric animation (WIP)
Guzman Llambias committed
17 
    </org.eventb.core.event>
Guzman Llambias's avatar
Change trigger for emit event  
Guzman Llambias committed
18 
    <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="_WiIIRPKWEe60CqkwWvstGA">
Guzman Llambias's avatar
Add Ethereum -> Fabric animation (WIP)
Guzman Llambias committed
19 
        <org.eventb.core.refinesEvent name="'" org.eventb.core.target="INITIATE_CC_TX_IN_ETHEREUM"/>
Guzman Llambias's avatar
Change trigger for emit event  
Guzman Llambias committed
20 21 
        <org.eventb.core.action name="_I7eOwMHOEe609fto5wotHA" org.eventb.core.assignment="initiated ≔ 1" org.eventb.core.generated="false" org.eventb.core.label="act31" org.eventb.emf.persistence.emf_id="_WiIIQvKWEe60CqkwWvstGA"/>
        <org.eventb.core.action name="_I7eOwcHOEe609fto5wotHA" org.eventb.core.assignment="submit_cc_tx ≔ 0" org.eventb.core.generated="false" org.eventb.core.label="act32" org.eventb.emf.persistence.emf_id="_WiIIQ_KWEe60CqkwWvstGA"/>
Guzman Llambias's avatar
Add Ethereum -> Fabric animation (WIP)
Guzman Llambias committed
22 
    </org.eventb.core.event>
Guzman Llambias's avatar
Change trigger for emit event  
Guzman Llambias committed
23 24 25 26 27 
    <org.eventb.core.event name="_hlSwd_KVEe60CqkwWvstGA" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="EMIT_CC_TX_EVENT_IN_ETHEREUM" org.eventb.emf.persistence.emf_id="_WiIISfKWEe60CqkwWvstGA">
        <org.eventb.core.refinesEvent name="_hlSwePKVEe60CqkwWvstGA" org.eventb.core.target="EMIT_CC_TX_EVENT_IN_ETHEREUM"/>
        <org.eventb.core.action name="_LjZ6UMHOEe609fto5wotHA" org.eventb.core.assignment="emitted ≔ 1" org.eventb.core.generated="false" org.eventb.core.label="act31" org.eventb.emf.persistence.emf_id="_WiIIRvKWEe60CqkwWvstGA"/>
        <org.eventb.core.action name="_LjZ6UcHOEe609fto5wotHA" org.eventb.core.assignment="initiated ≔ 0" org.eventb.core.generated="false" org.eventb.core.label="act32" org.eventb.emf.persistence.emf_id="_WiIIR_KWEe60CqkwWvstGA"/>
        <org.eventb.core.action name="_LjahYMHOEe609fto5wotHA" org.eventb.core.assignment="submit_cc_tx ≔ 0" org.eventb.core.generated="false" org.eventb.core.label="act33" org.eventb.emf.persistence.emf_id="_WiIISPKWEe60CqkwWvstGA"/>
Guzman Llambias's avatar
Add Ethereum -> Fabric animation (WIP)
Guzman Llambias committed
28 
    </org.eventb.core.event>
Guzman Llambias's avatar
Change trigger for emit event  
Guzman Llambias committed
29 
    <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="_WiIITvKWEe60CqkwWvstGA">
Guzman Llambias's avatar
Add Ethereum -> Fabric animation (WIP)
Guzman Llambias committed
30 
        <org.eventb.core.refinesEvent name="'" org.eventb.core.target="LISTEN_CC_TX_EVENT_IN_ETHEREUM"/>
Guzman Llambias's avatar
Change trigger for emit event  
Guzman Llambias committed
31 32 33 
        <org.eventb.core.action name="_NY1x8MHOEe609fto5wotHA" org.eventb.core.assignment="gateway_processing ≔ 1" org.eventb.core.generated="false" org.eventb.core.label="act31" org.eventb.emf.persistence.emf_id="_WiIIS_KWEe60CqkwWvstGA"/>
        <org.eventb.core.action name="_NY1x8cHOEe609fto5wotHA" org.eventb.core.assignment="emitted ≔  0" org.eventb.core.generated="false" org.eventb.core.label="act32" org.eventb.emf.persistence.emf_id="_WiIITPKWEe60CqkwWvstGA"/>
        <org.eventb.core.action name="_NY1x8sHOEe609fto5wotHA" org.eventb.core.assignment="submit_cc_tx ≔ 0" org.eventb.core.generated="false" org.eventb.core.label="act33" org.eventb.emf.persistence.emf_id="_WiIITfKWEe60CqkwWvstGA"/>
Guzman Llambias's avatar
Add Ethereum -> Fabric animation (WIP)
Guzman Llambias committed
34 
    </org.eventb.core.event>
Guzman Llambias's avatar
Change trigger for emit event  
Guzman Llambias committed
35 
    <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="_WiIIUvKWEe60CqkwWvstGA">
Guzman Llambias's avatar
Add Ethereum -> Fabric animation (WIP)
Guzman Llambias committed
36 
        <org.eventb.core.refinesEvent name="'" org.eventb.core.target="SUBMIT_CC_TX_TO_FABRIC"/>
Guzman Llambias's avatar
Change trigger for emit event  
Guzman Llambias committed
37 38 
        <org.eventb.core.action name="_RH42kMHOEe609fto5wotHA" org.eventb.core.assignment="submit_cc_tx ≔ 1" org.eventb.core.generated="false" org.eventb.core.label="act31" org.eventb.emf.persistence.emf_id="_WiIIUPKWEe60CqkwWvstGA"/>
        <org.eventb.core.action name="_RH5doMHOEe609fto5wotHA" org.eventb.core.assignment="gateway_processing ≔ 0" org.eventb.core.generated="false" org.eventb.core.label="act32" org.eventb.emf.persistence.emf_id="_WiIIUfKWEe60CqkwWvstGA"/>
Guzman Llambias's avatar
Complete Ethereum -> Fabric animation  
Guzman Llambias committed
39 
    </org.eventb.core.event>
Guzman Llambias's avatar
Change trigger for emit event  
Guzman Llambias committed
40 
    <org.eventb.core.event name="_yREdbb7uEe6laZimEYihUn" 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="_WiIIVfKWEe60CqkwWvstGA">
Guzman Llambias's avatar
Complete Ethereum -> Fabric animation  
Guzman Llambias committed
41 
        <org.eventb.core.refinesEvent name="'" org.eventb.core.target="CREATE_GATEWAY_USER"/>
Guzman Llambias's avatar
Change trigger for emit event  
Guzman Llambias committed
42 
        <org.eventb.core.action name="_RH5docHOEe609fto5wotHA" org.eventb.core.assignment="user_created ≔ 1" org.eventb.core.generated="false" org.eventb.core.label="act31" org.eventb.emf.persistence.emf_id="_WiIIVPKWEe60CqkwWvstGA"/>
Guzman Llambias's avatar
Complete Ethereum -> Fabric animation  
Guzman Llambias committed
43 
    </org.eventb.core.event>
Guzman Llambias's avatar
Change trigger for emit event  
Guzman Llambias committed
44 
    <org.eventb.core.event name="_yREdbb7uEe6laZimEYihUo" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="GRANT_PERMISSION" org.eventb.emf.persistence.emf_id="_WiIIWvKWEe60CqkwWvstGA">
Guzman Llambias's avatar
Complete Ethereum -> Fabric animation  
Guzman Llambias committed
45 
        <org.eventb.core.refinesEvent name="'" org.eventb.core.target="GRANT_PERMISSION"/>
Guzman Llambias's avatar
Change trigger for emit event  
Guzman Llambias committed
46 47 48 
        <org.eventb.core.action name="_yeWE8MHOEe609fto5wotHA" org.eventb.core.assignment="write_granted ≔ 1" org.eventb.core.generated="false" org.eventb.core.label="act31" org.eventb.emf.persistence.emf_id="_WiIIWfKWEe60CqkwWvstGA"/>
        <org.eventb.core.guard name="_yeWE8cHOEe609fto5wotHA" org.eventb.core.generated="false" org.eventb.core.label="grd31" org.eventb.core.predicate="user = gateway_user" org.eventb.emf.persistence.emf_id="_WiIIV_KWEe60CqkwWvstGA"/>
        <org.eventb.core.guard name="_-iJ1EMHOEe609fto5wotHA" org.eventb.core.generated="false" org.eventb.core.label="grd32" org.eventb.core.predicate="permission = write" org.eventb.emf.persistence.emf_id="_WiIIWPKWEe60CqkwWvstGA"/>
Guzman Llambias's avatar
Complete Ethereum -> Fabric animation  
Guzman Llambias committed
49 
    </org.eventb.core.event>
Guzman Llambias's avatar
Change trigger for emit event  
Guzman Llambias committed
50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 
    <org.eventb.core.invariant name="_DmAl8MHOEe609fto5wotHA" org.eventb.core.generated="false" org.eventb.core.label="inv11" org.eventb.core.predicate="subscribed ∈ {0,1}" org.eventb.emf.persistence.emf_id="_WiIIL_KWEe60CqkwWvstGA"/>
    <org.eventb.core.invariant name="_DmB0EMHOEe609fto5wotHA" org.eventb.core.generated="false" org.eventb.core.label="inv12" org.eventb.core.predicate="initiated ∈ {0,1}" org.eventb.emf.persistence.emf_id="_WiIIMPKWEe60CqkwWvstGA"/>
    <org.eventb.core.invariant name="_DmCbIMHOEe609fto5wotHA" org.eventb.core.generated="false" org.eventb.core.label="inv13" org.eventb.core.predicate="emitted ∈ {0,1}" org.eventb.emf.persistence.emf_id="_WiIIMfKWEe60CqkwWvstGA"/>
    <org.eventb.core.invariant name="_DmDCMMHOEe609fto5wotHA" org.eventb.core.generated="false" org.eventb.core.label="inv14" org.eventb.core.predicate="gateway_processing ∈ {0,1}" org.eventb.emf.persistence.emf_id="_WiIIMvKWEe60CqkwWvstGA"/>
    <org.eventb.core.invariant name="_DmDpQMHOEe609fto5wotHA" 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="_WiIIM_KWEe60CqkwWvstGA"/>
    <org.eventb.core.invariant name="_DmEQUMHOEe609fto5wotHA" org.eventb.core.generated="false" org.eventb.core.label="inv16" org.eventb.core.predicate="user_created ∈ {0,1}" org.eventb.emf.persistence.emf_id="_WiIINPKWEe60CqkwWvstGA"/>
    <org.eventb.core.invariant name="_2MNd0MHOEe609fto5wotHA" org.eventb.core.generated="false" org.eventb.core.label="inv17" org.eventb.core.predicate="write_granted ∈ {0,1}" org.eventb.emf.persistence.emf_id="_WiIINfKWEe60CqkwWvstGA"/>
    <org.eventb.core.variable name="_yREdab7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="received_transactions" org.eventb.emf.persistence.emf_id="_WiIIIPKWEe60CqkwWvstGA"/>
    <org.eventb.core.variable name="_YjCFYPKVEe60CqkwWvstGA" org.eventb.core.generated="false" org.eventb.core.identifier="emitted_events" org.eventb.emf.persistence.emf_id="_WiIIIfKWEe60CqkwWvstGA"/>
    <org.eventb.core.variable name="_yREda77uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="subscriptions" org.eventb.emf.persistence.emf_id="_WiIIIvKWEe60CqkwWvstGA"/>
    <org.eventb.core.variable name="_yREdbL7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="gateway_pending_transactions" org.eventb.emf.persistence.emf_id="_WiIII_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="_WiIIJPKWEe60CqkwWvstGA"/>
    <org.eventb.core.variable name="_1toq4L7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="authenticated_users" org.eventb.emf.persistence.emf_id="_WiIIJfKWEe60CqkwWvstGA"/>
    <org.eventb.core.variable name="_1toq4b7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="authenticated_transactions" org.eventb.emf.persistence.emf_id="_WiIIJvKWEe60CqkwWvstGA"/>
    <org.eventb.core.variable name="_2RlqIMErEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.identifier="grants" org.eventb.emf.persistence.emf_id="_WiIIJ_KWEe60CqkwWvstGA"/>
    <org.eventb.core.variable name="_DmLlEMHOEe609fto5wotHA" org.eventb.core.generated="false" org.eventb.core.identifier="subscribed" org.eventb.emf.persistence.emf_id="_WiIIKPKWEe60CqkwWvstGA"/>
    <org.eventb.core.variable name="_DmMMIMHOEe609fto5wotHA" org.eventb.core.generated="false" org.eventb.core.identifier="initiated" org.eventb.emf.persistence.emf_id="_WiIIKfKWEe60CqkwWvstGA"/>
    <org.eventb.core.variable name="_Wik0EPKWEe60CqkwWvstGA" org.eventb.core.generated="false" org.eventb.core.identifier="emitted" org.eventb.emf.persistence.emf_id="_WiIIKvKWEe60CqkwWvstGA"/>
    <org.eventb.core.variable name="_DmMMIsHOEe609fto5wotHA" org.eventb.core.generated="false" org.eventb.core.identifier="gateway_processing" org.eventb.emf.persistence.emf_id="_WiIIK_KWEe60CqkwWvstGA"/>
    <org.eventb.core.variable name="_DmMMI8HOEe609fto5wotHA" org.eventb.core.generated="false" org.eventb.core.identifier="submit_cc_tx" org.eventb.emf.persistence.emf_id="_WiIILPKWEe60CqkwWvstGA"/>
    <org.eventb.core.variable name="_DmMMJMHOEe609fto5wotHA" org.eventb.core.generated="false" org.eventb.core.identifier="user_created" org.eventb.emf.persistence.emf_id="_WiIILfKWEe60CqkwWvstGA"/>
    <org.eventb.core.variable name="_2MPTAMHOEe609fto5wotHA" org.eventb.core.generated="false" org.eventb.core.identifier="write_granted" org.eventb.emf.persistence.emf_id="_WiIILvKWEe60CqkwWvstGA"/>
Guzman Llambias's avatar
Add Ethereum -> Fabric animation (WIP)
Guzman Llambias committed
72 
</org.eventb.core.machineFile>