Skip to content
Snippets Groups Projects
Normal view History Permalink
CCTx_Ethereum_Fabric_m2.bcm 35.3 KiB
Newer Older
Guzman Llambias's avatar
Change project name
Guzman Llambias committed
1 2 3 4 5 6 7 8 
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.scMachineFile org.eventb.core.accurate="true" org.eventb.core.configuration="org.eventb.core.fwd">
    <org.eventb.core.scRefinesMachine name="'" org.eventb.core.scTarget="/gateway-event-b/CCTx_Abstract_DLT_m1.bcm" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.refinesMachine#'"/>
    <org.eventb.core.scSeesContext name="(" org.eventb.core.scTarget="/gateway-event-b/CCTx_Ethereum_Fabric_c2.bcc" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.seesContext#_1tlAgL7uEe6laZimEYihUg"/>
    <org.eventb.core.scInternalContext name="CCTx_Abstract_DLT_c1">
        <org.eventb.core.scAxiom name="'" org.eventb.core.label="axm1;" org.eventb.core.predicate="source_smart_contract∈CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_c1.buc|org.eventb.core.contextFile#CCTx_Abstract_DLT_c1|org.eventb.core.axiom#_lhKcab7uEe6laZimEYihUg" org.eventb.core.theorem="false"/>
        <org.eventb.core.scAxiom name="(" org.eventb.core.label="axm2;" org.eventb.core.predicate="target_smart_contract∈CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_c1.buc|org.eventb.core.contextFile#CCTx_Abstract_DLT_c1|org.eventb.core.axiom#_lhKcar7uEe6laZimEYihUg" org.eventb.core.theorem="false"/>
        <org.eventb.core.scAxiom name=")" org.eventb.core.label="axm3;" org.eventb.core.predicate="gateway∈GATEWAYS" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_c1.buc|org.eventb.core.contextFile#CCTx_Abstract_DLT_c1|org.eventb.core.axiom#_lhKca77uEe6laZimEYihUg" org.eventb.core.theorem="false"/>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
9 
        <org.eventb.core.scCarrierSet name="TARGET_TRANSACTIONS" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_c1.buc|org.eventb.core.contextFile#CCTx_Abstract_DLT_c1|org.eventb.core.carrierSet#_dldMwPReEe60CqkwWvstGA" org.eventb.core.type="ℙ(TARGET_TRANSACTIONS)"/>
Guzman Llambias's avatar
Change project name
Guzman Llambias committed
10 11 12 
        <org.eventb.core.scConstant name="source_smart_contract" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_c1.buc|org.eventb.core.contextFile#CCTx_Abstract_DLT_c1|org.eventb.core.constant#_lhTmML7uEe6laZimEYihUg" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
        <org.eventb.core.scConstant name="gateway" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_c1.buc|org.eventb.core.contextFile#CCTx_Abstract_DLT_c1|org.eventb.core.constant#_lhTmMr7uEe6laZimEYihUg" org.eventb.core.type="GATEWAYS"/>
        <org.eventb.core.scCarrierSet name="GATEWAYS" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_c1.buc|org.eventb.core.contextFile#CCTx_Abstract_DLT_c1|org.eventb.core.carrierSet#_lhTmM77uEe6laZimEYihUg" org.eventb.core.type="ℙ(GATEWAYS)"/>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
13 14 
        <org.eventb.core.scCarrierSet name="SOURCE_TRANSACTIONS" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_c1.buc|org.eventb.core.contextFile#CCTx_Abstract_DLT_c1|org.eventb.core.carrierSet#_XWUxAPReEe60CqkwWvstGA" org.eventb.core.type="ℙ(SOURCE_TRANSACTIONS)"/>
        <org.eventb.core.scCarrierSet name="SMART_CONTRACT_EVENTS" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_c1.buc|org.eventb.core.contextFile#CCTx_Abstract_DLT_c1|org.eventb.core.carrierSet#_H4R8YPRjEe60CqkwWvstGA" org.eventb.core.type="ℙ(SMART_CONTRACT_EVENTS)"/>
Guzman Llambias's avatar
Change project name
Guzman Llambias committed
15 16 17 18 19 
        <org.eventb.core.scConstant name="target_smart_contract" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_c1.buc|org.eventb.core.contextFile#CCTx_Abstract_DLT_c1|org.eventb.core.constant#_lhTmMb7uEe6laZimEYihUg" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
        <org.eventb.core.scCarrierSet name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_c1.buc|org.eventb.core.contextFile#CCTx_Abstract_DLT_c1|org.eventb.core.carrierSet#_lhTmNb7uEe6laZimEYihUg" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS)"/>
    </org.eventb.core.scInternalContext>
    <org.eventb.core.scInternalContext name="CCTx_Ethereum_Fabric_c2">
        <org.eventb.core.scExtendsContext name="'" org.eventb.core.scTarget="/gateway-event-b/CCTx_Abstract_DLT_c1.bcc|org.eventb.core.scContextFile#CCTx_Abstract_DLT_c1" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_c2.buc|org.eventb.core.contextFile#CCTx_Ethereum_Fabric_c2|org.eventb.core.extendsContext#'"/>
Guzman Llambias's avatar
Change trigger for emit event  
Guzman Llambias committed
20 21 
        <org.eventb.core.scAxiom name="CCTx_Abstract_DLT_c2" org.eventb.core.label="axm11" org.eventb.core.predicate="partition(PERMISSIONS,{read},{write})" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_c2.buc|org.eventb.core.contextFile#CCTx_Ethereum_Fabric_c2|org.eventb.core.axiom#_c2chsMQ6Ee609fto5wotHA" org.eventb.core.theorem="false"/>
        <org.eventb.core.scAxiom name="CCTx_Abstract_DLT_c3" org.eventb.core.label="axm12" org.eventb.core.predicate="gateway_user∈USERS" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_c2.buc|org.eventb.core.contextFile#CCTx_Ethereum_Fabric_c2|org.eventb.core.axiom#_c2dIwMQ6Ee609fto5wotHA" org.eventb.core.theorem="false"/>
Guzman Llambias's avatar
Change project name
Guzman Llambias committed
22 23 24 25 26 27 
        <org.eventb.core.scConstant name="write" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_c2.buc|org.eventb.core.contextFile#CCTx_Ethereum_Fabric_c2|org.eventb.core.constant#_olcso77uEe6laZimEYihUg" org.eventb.core.type="PERMISSIONS"/>
        <org.eventb.core.scCarrierSet name="USERS" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_c2.buc|org.eventb.core.contextFile#CCTx_Ethereum_Fabric_c2|org.eventb.core.carrierSet#_olcspr7uEe6laZimEYihUg" org.eventb.core.type="ℙ(USERS)"/>
        <org.eventb.core.scConstant name="read" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_c2.buc|org.eventb.core.contextFile#CCTx_Ethereum_Fabric_c2|org.eventb.core.constant#_olcsor7uEe6laZimEYihUg" org.eventb.core.type="PERMISSIONS"/>
        <org.eventb.core.scCarrierSet name="PERMISSIONS" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_c2.buc|org.eventb.core.contextFile#CCTx_Ethereum_Fabric_c2|org.eventb.core.carrierSet#_olcspb7uEe6laZimEYihUg" org.eventb.core.type="ℙ(PERMISSIONS)"/>
        <org.eventb.core.scConstant name="gateway_user" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_c2.buc|org.eventb.core.contextFile#CCTx_Ethereum_Fabric_c2|org.eventb.core.constant#_olcspL7uEe6laZimEYihUg" org.eventb.core.type="USERS"/>
    </org.eventb.core.scInternalContext>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
28 29 
    <org.eventb.core.scInvariant name="CCTx_Abstract_DLT_c2" org.eventb.core.label="inv1" org.eventb.core.predicate="received_source_transactions∈CROSS_CHAIN_SMART_CONTRACTS ↔ SOURCE_TRANSACTIONS" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.invariant#_zpKWcMQ4Ee609fto5wotHA" org.eventb.core.theorem="false"/>
    <org.eventb.core.scInvariant name="CCTx_Abstract_DLT_c3" org.eventb.core.label="inv2" org.eventb.core.predicate="emitted_events∈CROSS_CHAIN_SMART_CONTRACTS ↔ SMART_CONTRACT_EVENTS" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.invariant#_zpKWccQ4Ee609fto5wotHA" org.eventb.core.theorem="false"/>
Guzman Llambias's avatar
Change trigger for emit event  
Guzman Llambias committed
30 
    <org.eventb.core.scInvariant name="CCTx_Abstract_DLT_c4" org.eventb.core.label="inv3" org.eventb.core.predicate="subscriptions∈GATEWAYS ↔ CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.invariant#_zpK9gMQ4Ee609fto5wotHA" org.eventb.core.theorem="false"/>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
31 32 
    <org.eventb.core.scInvariant name="CCTx_Abstract_DLT_c5" org.eventb.core.label="inv4" org.eventb.core.predicate="gateway_pending_events∈GATEWAYS ↔ TARGET_TRANSACTIONS" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.invariant#_zpK9gcQ4Ee609fto5wotHA" org.eventb.core.theorem="false"/>
    <org.eventb.core.scInvariant name="CCTx_Abstract_DLT_c6" org.eventb.core.label="inv5" org.eventb.core.predicate="received_target_transactions∈CROSS_CHAIN_SMART_CONTRACTS ↔ TARGET_TRANSACTIONS" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.invariant#_qTKs0MT7Ee609fto5wotHA" org.eventb.core.theorem="false"/>
Guzman Llambias's avatar
Add Ethereum -> Fabric animation (WIP)  
Guzman Llambias committed
33 
    <org.eventb.core.scInvariant name="CCTx_Ethereum_Fabric_c3" org.eventb.core.label="inv11" org.eventb.core.predicate="authenticated_users⊆USERS" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.invariant#_jV9TIsEWEe6yC4BToIaAqA" org.eventb.core.theorem="false"/>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
34 35 
    <org.eventb.core.scInvariant name="CCTx_Ethereum_Fabric_c4" org.eventb.core.label="inv12" org.eventb.core.predicate="authenticated_transactions∈received_target_transactions → authenticated_users" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.invariant#_jV9TI8EWEe6yC4BToIaAqA" org.eventb.core.theorem="false"/>
    <org.eventb.core.scInvariant name="CCTx_Ethereum_Fabric_c5" org.eventb.core.label="inv13" org.eventb.core.predicate="∀tx⦂CROSS_CHAIN_SMART_CONTRACTS×TARGET_TRANSACTIONS·tx∈received_target_transactions⇒(∃u⦂USERS·u∈authenticated_users∧tx ↦ u∈authenticated_transactions)" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.invariant#_jV9TJMEWEe6yC4BToIaAqA" org.eventb.core.theorem="false"/>
Guzman Llambias's avatar
Complete Ethereum -> Fabric animation  
Guzman Llambias committed
36 
    <org.eventb.core.scInvariant name="CCTx_Ethereum_Fabric_c6" org.eventb.core.label="inv14" org.eventb.core.predicate="grants∈authenticated_users ↔ PERMISSIONS" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.invariant#_OTstIMHNEe609fto5wotHA" org.eventb.core.theorem="false"/>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
37 38 39 40 
    <org.eventb.core.scInvariant name="CCTx_Ethereum_Fabric_c7" org.eventb.core.label="inv15" org.eventb.core.predicate="∀u⦂USERS·u∈authenticated_transactions[received_target_transactions]⇒u ↦ write∈grants" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.invariant#_jCLrMcHJEe6yC4BToIaAqA" org.eventb.core.theorem="false"/>
    <org.eventb.core.scVariable name="received_target_transactions" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.variable#_Ojia0PRgEe60CqkwWvstGA" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×TARGET_TRANSACTIONS)"/>
    <org.eventb.core.scVariable name="gateway_pending_events" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.variable#_OjhzwfRgEe60CqkwWvstGA" org.eventb.core.type="ℙ(GATEWAYS×TARGET_TRANSACTIONS)"/>
    <org.eventb.core.scVariable name="authenticated_transactions" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.variable#_1toq4b7uEe6laZimEYihUg" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×TARGET_TRANSACTIONS×USERS)"/>
Guzman Llambias's avatar
Change project name
Guzman Llambias committed
41 
    <org.eventb.core.scVariable name="subscriptions" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.variable#_yREda77uEe6laZimEYihUg" org.eventb.core.type="ℙ(GATEWAYS×CROSS_CHAIN_SMART_CONTRACTS)"/>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
42 
    <org.eventb.core.scVariable name="emitted_events" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.variable#_Zk8OdfKVEe60CqkwWvstGA" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×SMART_CONTRACT_EVENTS)"/>
Guzman Llambias's avatar
Complete Ethereum -> Fabric animation  
Guzman Llambias committed
43 
    <org.eventb.core.scVariable name="grants" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.variable#_2RlqIMErEe6yC4BToIaAqA" org.eventb.core.type="ℙ(USERS×PERMISSIONS)"/>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
44 
    <org.eventb.core.scVariable name="received_source_transactions" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.variable#_OjhzwPRgEe60CqkwWvstGA" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×SOURCE_TRANSACTIONS)"/>
Guzman Llambias's avatar
Change project name
Guzman Llambias committed
45 
    <org.eventb.core.scVariable name="authenticated_users" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.variable#_1toq4L7uEe6laZimEYihUg" org.eventb.core.type="ℙ(USERS)"/>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
46 47 48 49 
    <org.eventb.core.scEvent name="received_target_transactiont" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="INITIALISATION" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh">
        <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/gateway-event-b/CCTx_Abstract_DLT_m1.bcm|org.eventb.core.scMachineFile#CCTx_Abstract_DLT_m1|org.eventb.core.scEvent#received_target_transactiont" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh"/>
        <org.eventb.core.scAction name="'" org.eventb.core.assignment="received_source_transactions ≔ ∅ ⦂ ℙ(CROSS_CHAIN_SMART_CONTRACTS×SOURCE_TRANSACTIONS)" org.eventb.core.label="act1" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#'|org.eventb.core.action#_zpBMgMQ4Ee609fto5wotHA"/>
        <org.eventb.core.scAction name="(" org.eventb.core.assignment="emitted_events ≔ ∅ ⦂ ℙ(CROSS_CHAIN_SMART_CONTRACTS×SMART_CONTRACT_EVENTS)" org.eventb.core.label="act2" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#'|org.eventb.core.action#_zpBzkMQ4Ee609fto5wotHA"/>
Guzman Llambias's avatar
Change trigger for emit event  
Guzman Llambias committed
50 
        <org.eventb.core.scAction name=")" org.eventb.core.assignment="subscriptions ≔ ∅ ⦂ ℙ(GATEWAYS×CROSS_CHAIN_SMART_CONTRACTS)" org.eventb.core.label="act3" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#'|org.eventb.core.action#_zpBzkcQ4Ee609fto5wotHA"/>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
51 52 
        <org.eventb.core.scAction name="*" org.eventb.core.assignment="gateway_pending_events ≔ ∅ ⦂ ℙ(GATEWAYS×TARGET_TRANSACTIONS)" org.eventb.core.label="act4" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#'|org.eventb.core.action#_zpBzksQ4Ee609fto5wotHA"/>
        <org.eventb.core.scAction name="+" org.eventb.core.assignment="received_target_transactions ≔ ∅ ⦂ ℙ(CROSS_CHAIN_SMART_CONTRACTS×TARGET_TRANSACTIONS)" org.eventb.core.label="act6" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#'|org.eventb.core.action#_zpCaoMQ4Ee609fto5wotHA"/>
Guzman Llambias's avatar
Add Ethereum -> Fabric animation (WIP)  
Guzman Llambias committed
53 
        <org.eventb.core.scAction name="," org.eventb.core.assignment="authenticated_users ≔ ∅ ⦂ ℙ(USERS)" org.eventb.core.label="act11" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh|org.eventb.core.action#_jV8FAMEWEe6yC4BToIaAqA"/>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
54 
        <org.eventb.core.scAction name="-" org.eventb.core.assignment="authenticated_transactions ≔ ∅ ⦂ ℙ(CROSS_CHAIN_SMART_CONTRACTS×TARGET_TRANSACTIONS×USERS)" org.eventb.core.label="act12" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh|org.eventb.core.action#_jV8FAcEWEe6yC4BToIaAqA"/>
Guzman Llambias's avatar
Complete Ethereum -> Fabric animation  
Guzman Llambias committed
55 
        <org.eventb.core.scAction name="." org.eventb.core.assignment="grants ≔ ∅ ⦂ ℙ(USERS×PERMISSIONS)" org.eventb.core.label="act14" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh|org.eventb.core.action#_0oC5cMErEe6yC4BToIaAqA"/>
Guzman Llambias's avatar
Change project name
Guzman Llambias committed
56 
    </org.eventb.core.scEvent>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
57 58 
    <org.eventb.core.scEvent name="received_target_transactionu" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="SUBSCRIBE_SMART_CONTRACT_EVENTS_IN_ETHEREUM" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_1tlnkr7uEe6laZimEYihUg">
        <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/gateway-event-b/CCTx_Abstract_DLT_m1.bcm|org.eventb.core.scMachineFile#CCTx_Abstract_DLT_m1|org.eventb.core.scEvent#received_target_transactionu" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_1tlnkr7uEe6laZimEYihUg|org.eventb.core.refinesEvent#_1tlnk77uEe6laZimEYihUg"/>
Guzman Llambias's avatar
Change trigger for emit event  
Guzman Llambias committed
59 60 
        <org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="gateway ↦ source_smart_contract∉subscriptions" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_yQ9vtr7uEe6laZimEYihUg|org.eventb.core.guard#_zpDBscQ4Ee609fto5wotHA" org.eventb.core.theorem="false"/>
        <org.eventb.core.scAction name="(" org.eventb.core.assignment="subscriptions ≔ subscriptions∪{gateway ↦ source_smart_contract}" org.eventb.core.label="act1" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_yQ9vtr7uEe6laZimEYihUg|org.eventb.core.action#_zpDBsMQ4Ee609fto5wotHA"/>
Guzman Llambias's avatar
Change project name
Guzman Llambias committed
61 
    </org.eventb.core.scEvent>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
62 63 64 65 66 67 
    <org.eventb.core.scEvent name="received_target_transactionv" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="INITIATE_CC_TX_IN_ETHEREUM" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_1g9W8MBFEe6yC4BToIaAqA">
        <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/gateway-event-b/CCTx_Abstract_DLT_m1.bcm|org.eventb.core.scMachineFile#CCTx_Abstract_DLT_m1|org.eventb.core.scEvent#received_target_transactionv" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_1g9W8MBFEe6yC4BToIaAqA|org.eventb.core.refinesEvent#_1g9-AMBFEe6yC4BToIaAqA"/>
        <org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="transaction∈SOURCE_TRANSACTIONS" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_y397cMBFEe6yC4BToIaAqA|org.eventb.core.guard#_zpDowcQ4Ee609fto5wotHA" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="(" org.eventb.core.label="grd3" org.eventb.core.predicate="transaction∉received_source_transactions[{source_smart_contract}]" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_y397cMBFEe6yC4BToIaAqA|org.eventb.core.guard#_zpEP0MQ4Ee609fto5wotHA" org.eventb.core.theorem="false"/>
        <org.eventb.core.scAction name="transactioo" org.eventb.core.assignment="received_source_transactions ≔ received_source_transactions∪{source_smart_contract ↦ transaction}" org.eventb.core.label="act1" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_y397cMBFEe6yC4BToIaAqA|org.eventb.core.action#_zpDowMQ4Ee609fto5wotHA"/>
        <org.eventb.core.scParameter name="transaction" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_y397cMBFEe6yC4BToIaAqA|org.eventb.core.parameter#_yQ9vvb7uEe6laZimEYihUg" org.eventb.core.type="SOURCE_TRANSACTIONS"/>
Guzman Llambias's avatar
Change project name
Guzman Llambias committed
68 
    </org.eventb.core.scEvent>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
69 70 71 72 73 74 75 76 
    <org.eventb.core.scEvent name="received_target_transactionw" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="EMIT_EVENT_IN_ETHEREUM" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_eB-pUPRhEe60CqkwWvstGA">
        <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/gateway-event-b/CCTx_Abstract_DLT_m1.bcm|org.eventb.core.scMachineFile#CCTx_Abstract_DLT_m1|org.eventb.core.scEvent#received_target_transactionw" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_eB-pUPRhEe60CqkwWvstGA|org.eventb.core.refinesEvent#_eB-pUfRhEe60CqkwWvstGA"/>
        <org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="source_smart_contract ↦ transaction∈received_source_transactions" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_WGbIAPRhEe60CqkwWvstGA|org.eventb.core.guard#_zpFd8cQ4Ee609fto5wotHA" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="emitted_event∉emitted_events[{source_smart_contract}]" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_WGbIAPRhEe60CqkwWvstGA|org.eventb.core.guard#_zpGFAMQ4Ee609fto5wotHA" org.eventb.core.theorem="false"/>
        <org.eventb.core.scAction name="emitted_evenu" org.eventb.core.assignment="emitted_events ≔ emitted_events∪{source_smart_contract ↦ emitted_event}" org.eventb.core.label="act1" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_WGbIAPRhEe60CqkwWvstGA|org.eventb.core.action#_zpE24MQ4Ee609fto5wotHA"/>
        <org.eventb.core.scAction name="emitted_evenv" org.eventb.core.assignment="received_source_transactions ≔ received_source_transactions ∖ {source_smart_contract ↦ transaction}" org.eventb.core.label="act2" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_WGbIAPRhEe60CqkwWvstGA|org.eventb.core.action#_zpFd8MQ4Ee609fto5wotHA"/>
        <org.eventb.core.scParameter name="emitted_event" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_WGbIAPRhEe60CqkwWvstGA|org.eventb.core.parameter#_RRvi8PRfEe60CqkwWvstGA" org.eventb.core.type="SMART_CONTRACT_EVENTS"/>
        <org.eventb.core.scParameter name="transaction" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_WGbIAPRhEe60CqkwWvstGA|org.eventb.core.parameter#_yQ9vw77uEe6laZimEYihUg" org.eventb.core.type="SOURCE_TRANSACTIONS"/>
Guzman Llambias's avatar
Change project name
Guzman Llambias committed
77 
    </org.eventb.core.scEvent>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
78 79 80 81 82 83 84 85 86 
    <org.eventb.core.scEvent name="received_target_transactionx" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="LISTEN_EVENT_IN_ETHEREUM" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_eB-pUvRhEe60CqkwWvstGA">
        <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/gateway-event-b/CCTx_Abstract_DLT_m1.bcm|org.eventb.core.scMachineFile#CCTx_Abstract_DLT_m1|org.eventb.core.scEvent#received_target_transactionx" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_eB-pUvRhEe60CqkwWvstGA|org.eventb.core.refinesEvent#_eB-pU_RhEe60CqkwWvstGA"/>
        <org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="source_smart_contract ↦ emitted_event∈emitted_events" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_WGbvEPRhEe60CqkwWvstGA|org.eventb.core.guard#_zpHTIcQ4Ee609fto5wotHA" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="gateway ↦ source_smart_contract∈subscriptions" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_WGbvEPRhEe60CqkwWvstGA|org.eventb.core.guard#_zpH6MMQ4Ee609fto5wotHA" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name=")" org.eventb.core.label="grd3" org.eventb.core.predicate="gateway ↦ pending_event∉gateway_pending_events" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_WGbvEPRhEe60CqkwWvstGA|org.eventb.core.guard#_zpH6McQ4Ee609fto5wotHA" org.eventb.core.theorem="false"/>
        <org.eventb.core.scAction name="pending_evenu" org.eventb.core.assignment="gateway_pending_events ≔ gateway_pending_events∪{gateway ↦ pending_event}" org.eventb.core.label="act1" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_WGbvEPRhEe60CqkwWvstGA|org.eventb.core.action#_zpGsEMQ4Ee609fto5wotHA"/>
        <org.eventb.core.scAction name="pending_evenv" org.eventb.core.assignment="emitted_events ≔ emitted_events ∖ {source_smart_contract ↦ emitted_event}" org.eventb.core.label="act2" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_WGbvEPRhEe60CqkwWvstGA|org.eventb.core.action#_zpHTIMQ4Ee609fto5wotHA"/>
        <org.eventb.core.scParameter name="pending_event" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_WGbvEPRhEe60CqkwWvstGA|org.eventb.core.parameter#_rW2qoPRfEe60CqkwWvstGA" org.eventb.core.type="TARGET_TRANSACTIONS"/>
        <org.eventb.core.scParameter name="emitted_event" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_WGbvEPRhEe60CqkwWvstGA|org.eventb.core.parameter#_WbZkYPRfEe60CqkwWvstGA" org.eventb.core.type="SMART_CONTRACT_EVENTS"/>
Guzman Llambias's avatar
Change project name
Guzman Llambias committed
87 
    </org.eventb.core.scEvent>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
88 89 90 91 92 93 94 95 96 97 98 99 
    <org.eventb.core.scEvent name="received_target_transactiony" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="SUBMIT_TX_TO_FABRIC" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_eB-pVPRhEe60CqkwWvstGA">
        <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/gateway-event-b/CCTx_Abstract_DLT_m1.bcm|org.eventb.core.scMachineFile#CCTx_Abstract_DLT_m1|org.eventb.core.scEvent#received_target_transactiony" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_eB-pVPRhEe60CqkwWvstGA|org.eventb.core.refinesEvent#_eB-pVfRhEe60CqkwWvstGA"/>
        <org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="gateway ↦ pending_event∈gateway_pending_events" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_WGc9MPRhEe60CqkwWvstGA|org.eventb.core.guard#_zpJvYcQ4Ee609fto5wotHA" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="transaction∈TARGET_TRANSACTIONS" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_WGc9MPRhEe60CqkwWvstGA|org.eventb.core.guard#_L7ASUPRgEe60CqkwWvstGA" org.eventb.core.theorem="false"/>
        <org.eventb.core.scAction name="pending_evenu" org.eventb.core.assignment="received_target_transactions ≔ received_target_transactions∪{target_smart_contract ↦ transaction}" org.eventb.core.label="act1" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_WGc9MPRhEe60CqkwWvstGA|org.eventb.core.action#_zpJIUMQ4Ee609fto5wotHA"/>
        <org.eventb.core.scAction name="pending_evenv" org.eventb.core.assignment="gateway_pending_events ≔ gateway_pending_events ∖ {gateway ↦ pending_event}" org.eventb.core.label="act2" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_WGc9MPRhEe60CqkwWvstGA|org.eventb.core.action#_zpJvYMQ4Ee609fto5wotHA"/>
        <org.eventb.core.scParameter name="pending_event" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_WGc9MPRhEe60CqkwWvstGA|org.eventb.core.parameter#_rW3RsPRfEe60CqkwWvstGA" org.eventb.core.type="TARGET_TRANSACTIONS"/>
        <org.eventb.core.scParameter name="transaction" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_WGc9MPRhEe60CqkwWvstGA|org.eventb.core.parameter#_AlhAwPRgEe60CqkwWvstGA" org.eventb.core.type="TARGET_TRANSACTIONS"/>
        <org.eventb.core.scGuard name="pending_evenw" org.eventb.core.label="grd11" org.eventb.core.predicate="user∈authenticated_users" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_eB-pVPRhEe60CqkwWvstGA|org.eventb.core.guard#_jV8sEcEWEe6yC4BToIaAqA" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="pending_evenx" org.eventb.core.label="grd12" org.eventb.core.predicate="user ↦ write∈grants" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_eB-pVPRhEe60CqkwWvstGA|org.eventb.core.guard#_jV8sEsEWEe6yC4BToIaAqA" org.eventb.core.theorem="false"/>
        <org.eventb.core.scParameter name="user" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_eB-pVPRhEe60CqkwWvstGA|org.eventb.core.parameter#_1tncwL7uEe6laZimEYihUg" org.eventb.core.type="USERS"/>
        <org.eventb.core.scAction name="pending_eveny" org.eventb.core.assignment="authenticated_transactions ≔ authenticated_transactions{target_smart_contract ↦ transaction ↦ user}" org.eventb.core.label="act11" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_eB-pVPRhEe60CqkwWvstGA|org.eventb.core.action#_jV8sEMEWEe6yC4BToIaAqA"/>
Guzman Llambias's avatar
Add Ethereum -> Fabric animation (WIP)  
Guzman Llambias committed
100 
    </org.eventb.core.scEvent>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
101 
    <org.eventb.core.scEvent name="received_target_transactionz" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="CREATE_GATEWAY_USER" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_K_21gMEXEe6yC4BToIaAqA">
Guzman Llambias's avatar
Add Ethereum -> Fabric animation (WIP)  
Guzman Llambias committed
102 103 104 
        <org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="gateway_user∉authenticated_users" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_K_21gMEXEe6yC4BToIaAqA|org.eventb.core.guard#_y4y5cMEXEe6yC4BToIaAqA" org.eventb.core.theorem="false"/>
        <org.eventb.core.scAction name="(" org.eventb.core.assignment="authenticated_users ≔ authenticated_users∪{gateway_user}" org.eventb.core.label="act1" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_K_21gMEXEe6yC4BToIaAqA|org.eventb.core.action#_jV9TIcEWEe6yC4BToIaAqA"/>
    </org.eventb.core.scEvent>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
105 
    <org.eventb.core.scEvent name="received_target_transaction{" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="GRANT_PERMISSION" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_KHHS0MEbEe6yC4BToIaAqA">
Guzman Llambias's avatar
Add Ethereum -> Fabric animation (WIP)  
Guzman Llambias committed
106 107 
        <org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="permission∈PERMISSIONS" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_KHHS0MEbEe6yC4BToIaAqA|org.eventb.core.guard#_KHH54cEbEe6yC4BToIaAqA" org.eventb.core.theorem="false"/>
        <org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="user∈authenticated_users" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_KHHS0MEbEe6yC4BToIaAqA|org.eventb.core.guard#_KHH54sEbEe6yC4BToIaAqA" org.eventb.core.theorem="false"/>
Guzman Llambias's avatar
Complete Ethereum -> Fabric animation  
Guzman Llambias committed
108 
        <org.eventb.core.scGuard name=")" org.eventb.core.label="grd3" org.eventb.core.predicate="user ↦ permission∉grants" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_KHHS0MEbEe6yC4BToIaAqA|org.eventb.core.guard#_5yZW0MHNEe609fto5wotHA" org.eventb.core.theorem="false"/>
Guzman Llambias's avatar
Add Ethereum -> Fabric animation (WIP)  
Guzman Llambias committed
109 110 
        <org.eventb.core.scParameter name="permission" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_KHHS0MEbEe6yC4BToIaAqA|org.eventb.core.parameter#_KHIg8MEbEe6yC4BToIaAqA" org.eventb.core.type="PERMISSIONS"/>
        <org.eventb.core.scParameter name="user" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_KHHS0MEbEe6yC4BToIaAqA|org.eventb.core.parameter#_KHIg8cEbEe6yC4BToIaAqA" org.eventb.core.type="USERS"/>
Guzman Llambias's avatar
Complete Ethereum -> Fabric animation  
Guzman Llambias committed
111 
        <org.eventb.core.scAction name="permissioo" org.eventb.core.assignment="grants ≔ grants∪{user ↦ permission}" org.eventb.core.label="act1" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_KHHS0MEbEe6yC4BToIaAqA|org.eventb.core.action#_KHH54MEbEe6yC4BToIaAqA"/>
Guzman Llambias's avatar
Change project name
Guzman Llambias committed
112 113 
    </org.eventb.core.scEvent>
</org.eventb.core.scMachineFile>