Skip to content
Snippets Groups Projects
Normal view History 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
Fix from reviewers comments  
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="_x2YoLPRhEe60CqkwWvstGA" org.eventb.texttools.text_lastmodified="1712441128944" 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_source_transactions emitted_events subscriptions gateway_pending_events received_target_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_EVENT_IN_ETHEREUM extends EMIT_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_EVENT_IN_ETHEREUM extends LISTEN_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_TX_TO_FABRIC extends SUBMIT_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
Fix from reviewers comments  
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="_x2YoDfRhEe60CqkwWvstGA">
        <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="_x2YoBvRhEe60CqkwWvstGA"/>
        <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="_x2YoB_RhEe60CqkwWvstGA"/>
        <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="_x2YoCPRhEe60CqkwWvstGA"/>
        <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="_x2YoCfRhEe60CqkwWvstGA"/>
        <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="_x2YoCvRhEe60CqkwWvstGA"/>
        <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="_x2YoC_RhEe60CqkwWvstGA"/>
        <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="_x2YoDPRhEe60CqkwWvstGA"/>
Guzman Llambias's avatar
Complete Ethereum -> Fabric animation  
Guzman Llambias committed
13 
    </org.eventb.core.event>
Guzman Llambias's avatar
Fix from reviewers comments  
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="_x2YoEPRhEe60CqkwWvstGA">
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
Fix from reviewers comments  
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="_x2YoD_RhEe60CqkwWvstGA"/>
Guzman Llambias's avatar
Add Ethereum -> Fabric animation (WIP)
Guzman Llambias committed
17 
    </org.eventb.core.event>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
18 19 20 21 
    <org.eventb.core.event name="_x24-QPRhEe60CqkwWvstGA" 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="_x2YoFPRhEe60CqkwWvstGA">
        <org.eventb.core.refinesEvent name="_x24-QfRhEe60CqkwWvstGA" org.eventb.core.target="INITIATE_CC_TX_IN_ETHEREUM"/>
        <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="_x2YoEvRhEe60CqkwWvstGA"/>
        <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="_x2YoE_RhEe60CqkwWvstGA"/>
Guzman Llambias's avatar
Add Ethereum -> Fabric animation (WIP)
Guzman Llambias committed
22 
    </org.eventb.core.event>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
23 24 25 26 27 
    <org.eventb.core.event name="_vbddoPRhEe60CqkwWvstGA" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="EMIT_EVENT_IN_ETHEREUM" org.eventb.emf.persistence.emf_id="_x2YoGfRhEe60CqkwWvstGA">
        <org.eventb.core.refinesEvent name="_vbddofRhEe60CqkwWvstGA" org.eventb.core.target="EMIT_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="_x2YoFvRhEe60CqkwWvstGA"/>
        <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="_x2YoF_RhEe60CqkwWvstGA"/>
        <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="_x2YoGPRhEe60CqkwWvstGA"/>
Guzman Llambias's avatar
Add Ethereum -> Fabric animation (WIP)
Guzman Llambias committed
28 
    </org.eventb.core.event>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
29 30 31 32 33 
    <org.eventb.core.event name="_vbddovRhEe60CqkwWvstGA" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="LISTEN_EVENT_IN_ETHEREUM" org.eventb.emf.persistence.emf_id="_x2YoHvRhEe60CqkwWvstGA">
        <org.eventb.core.refinesEvent name="_vbeEsPRhEe60CqkwWvstGA" org.eventb.core.target="LISTEN_EVENT_IN_ETHEREUM"/>
        <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="_x2YoG_RhEe60CqkwWvstGA"/>
        <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="_x2YoHPRhEe60CqkwWvstGA"/>
        <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="_x2YoHfRhEe60CqkwWvstGA"/>
Guzman Llambias's avatar
Add Ethereum -> Fabric animation (WIP)
Guzman Llambias committed
34 
    </org.eventb.core.event>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
35 36 37 38 
    <org.eventb.core.event name="_vbeEsfRhEe60CqkwWvstGA" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="SUBMIT_TX_TO_FABRIC" org.eventb.emf.persistence.emf_id="_x2YoIvRhEe60CqkwWvstGA">
        <org.eventb.core.refinesEvent name="_vbeEsvRhEe60CqkwWvstGA" org.eventb.core.target="SUBMIT_TX_TO_FABRIC"/>
        <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="_x2YoIPRhEe60CqkwWvstGA"/>
        <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="_x2YoIfRhEe60CqkwWvstGA"/>
Guzman Llambias's avatar
Complete Ethereum -> Fabric animation  
Guzman Llambias committed
39 
    </org.eventb.core.event>
Guzman Llambias's avatar
Fix from reviewers comments  
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="_x2YoJfRhEe60CqkwWvstGA">
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
Fix from reviewers comments  
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="_x2YoJPRhEe60CqkwWvstGA"/>
Guzman Llambias's avatar
Complete Ethereum -> Fabric animation  
Guzman Llambias committed
43 
    </org.eventb.core.event>
Guzman Llambias's avatar
Fix from reviewers comments  
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="_x2YoKvRhEe60CqkwWvstGA">
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
Fix from reviewers comments  
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="_x2YoKfRhEe60CqkwWvstGA"/>
        <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="_x2YoJ_RhEe60CqkwWvstGA"/>
        <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="_x2YoKPRhEe60CqkwWvstGA"/>
Guzman Llambias's avatar
Complete Ethereum -> Fabric animation  
Guzman Llambias committed
49 
    </org.eventb.core.event>
Guzman Llambias's avatar
Fix from reviewers comments  
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="_x2Yn__RhEe60CqkwWvstGA"/>
    <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="_x2YoAPRhEe60CqkwWvstGA"/>
    <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="_x2YoAfRhEe60CqkwWvstGA"/>
    <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="_x2YoAvRhEe60CqkwWvstGA"/>
    <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="_x2YoA_RhEe60CqkwWvstGA"/>
    <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="_x2YoBPRhEe60CqkwWvstGA"/>
    <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="_x2YoBfRhEe60CqkwWvstGA"/>
    <org.eventb.core.variable name="_SS0wAPRgEe60CqkwWvstGA" org.eventb.core.generated="false" org.eventb.core.identifier="received_source_transactions" org.eventb.emf.persistence.emf_id="_x2Yn8PRhEe60CqkwWvstGA"/>
    <org.eventb.core.variable name="_YjCFYPKVEe60CqkwWvstGA" org.eventb.core.generated="false" org.eventb.core.identifier="emitted_events" org.eventb.emf.persistence.emf_id="_x2Yn8fRhEe60CqkwWvstGA"/>
    <org.eventb.core.variable name="_yREda77uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="subscriptions" org.eventb.emf.persistence.emf_id="_x2Yn8vRhEe60CqkwWvstGA"/>
    <org.eventb.core.variable name="_SS0wAfRgEe60CqkwWvstGA" org.eventb.core.generated="false" org.eventb.core.identifier="gateway_pending_events" org.eventb.emf.persistence.emf_id="_x2Yn8_RhEe60CqkwWvstGA"/>
    <org.eventb.core.variable name="_SS0wAvRgEe60CqkwWvstGA" org.eventb.core.generated="false" org.eventb.core.identifier="received_target_transactions" org.eventb.emf.persistence.emf_id="_x2Yn9PRhEe60CqkwWvstGA"/>
    <org.eventb.core.variable name="_1toq4L7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="authenticated_users" org.eventb.emf.persistence.emf_id="_x2Yn9fRhEe60CqkwWvstGA"/>
    <org.eventb.core.variable name="_1toq4b7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="authenticated_transactions" org.eventb.emf.persistence.emf_id="_x2Yn9vRhEe60CqkwWvstGA"/>
    <org.eventb.core.variable name="_2RlqIMErEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.identifier="grants" org.eventb.emf.persistence.emf_id="_x2Yn9_RhEe60CqkwWvstGA"/>
    <org.eventb.core.variable name="_DmLlEMHOEe609fto5wotHA" org.eventb.core.generated="false" org.eventb.core.identifier="subscribed" org.eventb.emf.persistence.emf_id="_x2Yn-PRhEe60CqkwWvstGA"/>
    <org.eventb.core.variable name="_DmMMIMHOEe609fto5wotHA" org.eventb.core.generated="false" org.eventb.core.identifier="initiated" org.eventb.emf.persistence.emf_id="_x2Yn-fRhEe60CqkwWvstGA"/>
    <org.eventb.core.variable name="_Wik0EPKWEe60CqkwWvstGA" org.eventb.core.generated="false" org.eventb.core.identifier="emitted" org.eventb.emf.persistence.emf_id="_x2Yn-vRhEe60CqkwWvstGA"/>
    <org.eventb.core.variable name="_DmMMIsHOEe609fto5wotHA" org.eventb.core.generated="false" org.eventb.core.identifier="gateway_processing" org.eventb.emf.persistence.emf_id="_x2Yn-_RhEe60CqkwWvstGA"/>
    <org.eventb.core.variable name="_DmMMI8HOEe609fto5wotHA" org.eventb.core.generated="false" org.eventb.core.identifier="submit_cc_tx" org.eventb.emf.persistence.emf_id="_x2Yn_PRhEe60CqkwWvstGA"/>
    <org.eventb.core.variable name="_DmMMJMHOEe609fto5wotHA" org.eventb.core.generated="false" org.eventb.core.identifier="user_created" org.eventb.emf.persistence.emf_id="_x2Yn_fRhEe60CqkwWvstGA"/>
    <org.eventb.core.variable name="_2MPTAMHOEe609fto5wotHA" org.eventb.core.generated="false" org.eventb.core.identifier="write_granted" org.eventb.emf.persistence.emf_id="_x2Yn_vRhEe60CqkwWvstGA"/>
Guzman Llambias's avatar
Add Ethereum -> Fabric animation (WIP)
Guzman Llambias committed
72 
</org.eventb.core.machineFile>