Skip to content
Snippets Groups Projects
Normal view History Permalink
CCTx_Ethereum_Fabric_m2.bpo 47.1 KiB
Newer Older
Guzman Llambias's avatar
Change project name
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 3 4 
<org.eventb.core.poFile org.eventb.core.poStamp="39">
    <org.eventb.core.poPredicateSet name="CTXHYP" org.eventb.core.poStamp="39">
        <org.eventb.core.poIdentifier name="TARGET_TRANSACTIONS" org.eventb.core.type="ℙ(TARGET_TRANSACTIONS)"/>
Guzman Llambias's avatar
Change project name
Guzman Llambias committed
5 
        <org.eventb.core.poIdentifier name="GATEWAYS" org.eventb.core.type="ℙ(GATEWAYS)"/>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
6 7 
        <org.eventb.core.poIdentifier name="SOURCE_TRANSACTIONS" org.eventb.core.type="ℙ(SOURCE_TRANSACTIONS)"/>
        <org.eventb.core.poIdentifier name="SMART_CONTRACT_EVENTS" org.eventb.core.type="ℙ(SMART_CONTRACT_EVENTS)"/>
Guzman Llambias's avatar
Change project name
Guzman Llambias committed
8 9 10 11 12 13 14 15 16 17 18 19 
        <org.eventb.core.poIdentifier name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS)"/>
        <org.eventb.core.poIdentifier name="source_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
        <org.eventb.core.poIdentifier name="gateway" org.eventb.core.type="GATEWAYS"/>
        <org.eventb.core.poIdentifier name="target_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
        <org.eventb.core.poPredicate name="CROSS_CHAIN_SMART_CONTRACTT" 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.poPredicate name="CROSS_CHAIN_SMART_CONTRACTU" 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.poPredicate name="CROSS_CHAIN_SMART_CONTRACTV" 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.poIdentifier name="USERS" org.eventb.core.type="ℙ(USERS)"/>
        <org.eventb.core.poIdentifier name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
        <org.eventb.core.poIdentifier name="write" org.eventb.core.type="PERMISSIONS"/>
        <org.eventb.core.poIdentifier name="read" org.eventb.core.type="PERMISSIONS"/>
        <org.eventb.core.poIdentifier name="gateway_user" org.eventb.core.type="USERS"/>
Guzman Llambias's avatar
Change trigger for emit event  
Guzman Llambias committed
20 21 
        <org.eventb.core.poPredicate name="CROSS_CHAIN_SMART_CONTRACTW" 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.poPredicate name="CROSS_CHAIN_SMART_CONTRACTX" 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"/>
Guzman Llambias's avatar
Change project name
Guzman Llambias committed
22 
    </org.eventb.core.poPredicateSet>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
23 24 25 26 
    <org.eventb.core.poPredicateSet name="ABSHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poStamp="39">
        <org.eventb.core.poIdentifier name="received_target_transactions" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×TARGET_TRANSACTIONS)"/>
        <org.eventb.core.poIdentifier name="gateway_pending_events" org.eventb.core.type="ℙ(GATEWAYS×TARGET_TRANSACTIONS)"/>
        <org.eventb.core.poIdentifier name="authenticated_transactions" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×TARGET_TRANSACTIONS×USERS)"/>
Guzman Llambias's avatar
Change project name
Guzman Llambias committed
27 
        <org.eventb.core.poIdentifier name="subscriptions" org.eventb.core.type="ℙ(GATEWAYS×CROSS_CHAIN_SMART_CONTRACTS)"/>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
28 
        <org.eventb.core.poIdentifier name="emitted_events" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×SMART_CONTRACT_EVENTS)"/>
Guzman Llambias's avatar
Complete Ethereum -> Fabric animation  
Guzman Llambias committed
29 
        <org.eventb.core.poIdentifier name="grants" org.eventb.core.type="ℙ(USERS×PERMISSIONS)"/>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
30 
        <org.eventb.core.poIdentifier name="received_source_transactions" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×SOURCE_TRANSACTIONS)"/>
Guzman Llambias's avatar
Change project name
Guzman Llambias committed
31 
        <org.eventb.core.poIdentifier name="authenticated_users" org.eventb.core.type="ℙ(USERS)"/>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
32 33 34 35 36 
        <org.eventb.core.poPredicate name="received_target_transactiont" 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.poPredicate name="received_target_transactionu" 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.poPredicate name="received_target_transactionv" 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.poPredicate name="received_target_transactionw" 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.poPredicate name="received_target_transactionx" 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"/>
Guzman Llambias's avatar
Change project name
Guzman Llambias committed
37 
    </org.eventb.core.poPredicateSet>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
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 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 
    <org.eventb.core.poSequent name="INITIALISATION/inv12/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  establishment" org.eventb.core.poStamp="39">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#EVTALLHYPreceived_target_transactiont"/>
        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="(∅ ⦂ ℙ(CROSS_CHAIN_SMART_CONTRACTS×TARGET_TRANSACTIONS×USERS))∈(∅ ⦂ ℙ(CROSS_CHAIN_SMART_CONTRACTS×TARGET_TRANSACTIONS)) → (∅ ⦂ ℙ(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.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" 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.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" 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.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" 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.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poSequent#INITIALISATION\/inv12\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
        <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD1"/>
    </org.eventb.core.poSequent>
    <org.eventb.core.poSequent name="INITIALISATION/inv13/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  establishment" org.eventb.core.poStamp="39">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#EVTALLHYPreceived_target_transactiont"/>
        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀tx⦂CROSS_CHAIN_SMART_CONTRACTS×TARGET_TRANSACTIONS·tx∈(∅ ⦂ ℙ(CROSS_CHAIN_SMART_CONTRACTS×TARGET_TRANSACTIONS))⇒(∃u⦂USERS·u∈(∅ ⦂ ℙ(USERS))∧tx ↦ u∈(∅ ⦂ ℙ(CROSS_CHAIN_SMART_CONTRACTS×TARGET_TRANSACTIONS×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#_jV9TJMEWEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" 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.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" 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.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" 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.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poSequent#INITIALISATION\/inv13\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
        <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD2"/>
    </org.eventb.core.poSequent>
    <org.eventb.core.poSequent name="INITIALISATION/inv14/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  establishment" org.eventb.core.poStamp="39">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#EVTALLHYPreceived_target_transactiont"/>
        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="(∅ ⦂ ℙ(USERS×PERMISSIONS))∈(∅ ⦂ ℙ(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.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" 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.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" 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.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" 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.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poSequent#INITIALISATION\/inv14\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
        <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD3"/>
    </org.eventb.core.poSequent>
    <org.eventb.core.poSequent name="INITIALISATION/inv15/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  establishment" org.eventb.core.poStamp="39">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#EVTALLHYPreceived_target_transactiont"/>
        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀u⦂USERS·u∈(∅ ⦂ ℙ(CROSS_CHAIN_SMART_CONTRACTS×TARGET_TRANSACTIONS×USERS))[∅ ⦂ ℙ(CROSS_CHAIN_SMART_CONTRACTS×TARGET_TRANSACTIONS)]⇒u ↦ write∈(∅ ⦂ ℙ(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#_jCLrMcHJEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" 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.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" 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.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" 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.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poSequent#INITIALISATION\/inv15\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
        <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD4"/>
    </org.eventb.core.poSequent>
    <org.eventb.core.poPredicateSet name="EVTIDENTreceived_target_transactiont" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poStamp="39">
        <org.eventb.core.poIdentifier name="gateway_pending_events'" org.eventb.core.type="ℙ(GATEWAYS×TARGET_TRANSACTIONS)"/>
        <org.eventb.core.poIdentifier name="authenticated_users'" org.eventb.core.type="ℙ(USERS)"/>
        <org.eventb.core.poIdentifier name="authenticated_transactions'" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×TARGET_TRANSACTIONS×USERS)"/>
        <org.eventb.core.poIdentifier name="subscriptions'" org.eventb.core.type="ℙ(GATEWAYS×CROSS_CHAIN_SMART_CONTRACTS)"/>
        <org.eventb.core.poIdentifier name="received_source_transactions'" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×SOURCE_TRANSACTIONS)"/>
        <org.eventb.core.poIdentifier name="grants'" org.eventb.core.type="ℙ(USERS×PERMISSIONS)"/>
        <org.eventb.core.poIdentifier name="emitted_events'" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×SMART_CONTRACT_EVENTS)"/>
        <org.eventb.core.poIdentifier name="received_target_transactions'" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×TARGET_TRANSACTIONS)"/>
    </org.eventb.core.poPredicateSet>
    <org.eventb.core.poPredicateSet name="EVTALLHYPreceived_target_transactiont" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#EVTIDENTreceived_target_transactiont" org.eventb.core.poStamp="39"/>
    <org.eventb.core.poPredicateSet name="EVTIDENTreceived_target_transactionu" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="39">
Guzman Llambias's avatar
Change project name
Guzman Llambias committed
86 87 
        <org.eventb.core.poIdentifier name="subscriptions'" org.eventb.core.type="ℙ(GATEWAYS×CROSS_CHAIN_SMART_CONTRACTS)"/>
    </org.eventb.core.poPredicateSet>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
88 
    <org.eventb.core.poPredicateSet name="EVTALLHYPreceived_target_transactionu" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#EVTIDENTreceived_target_transactionu" org.eventb.core.poStamp="39">
Guzman Llambias's avatar
Change trigger for emit event  
Guzman Llambias committed
89 
        <org.eventb.core.poPredicate name="PRD0" 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"/>
Guzman Llambias's avatar
Change project name
Guzman Llambias committed
90 
    </org.eventb.core.poPredicateSet>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 
    <org.eventb.core.poPredicateSet name="EVTIDENTreceived_target_transactionv" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="39">
        <org.eventb.core.poIdentifier name="transaction" org.eventb.core.type="SOURCE_TRANSACTIONS"/>
        <org.eventb.core.poIdentifier name="received_source_transactions'" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×SOURCE_TRANSACTIONS)"/>
    </org.eventb.core.poPredicateSet>
    <org.eventb.core.poPredicateSet name="EVTALLHYPreceived_target_transactionv" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#EVTIDENTreceived_target_transactionv" org.eventb.core.poStamp="39">
        <org.eventb.core.poPredicate name="PRD0" 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.poPredicate name="PRD1" 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.poPredicateSet>
    <org.eventb.core.poPredicateSet name="EVTIDENTreceived_target_transactionw" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="39">
        <org.eventb.core.poIdentifier name="transaction" org.eventb.core.type="SOURCE_TRANSACTIONS"/>
        <org.eventb.core.poIdentifier name="emitted_event" org.eventb.core.type="SMART_CONTRACT_EVENTS"/>
        <org.eventb.core.poIdentifier name="received_source_transactions'" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×SOURCE_TRANSACTIONS)"/>
        <org.eventb.core.poIdentifier name="emitted_events'" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×SMART_CONTRACT_EVENTS)"/>
    </org.eventb.core.poPredicateSet>
    <org.eventb.core.poPredicateSet name="EVTALLHYPreceived_target_transactionw" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#EVTIDENTreceived_target_transactionw" org.eventb.core.poStamp="39">
        <org.eventb.core.poPredicate name="PRD0" 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.poPredicate name="PRD1" 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.poPredicateSet>
    <org.eventb.core.poPredicateSet name="EVTIDENTreceived_target_transactionx" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="39">
        <org.eventb.core.poIdentifier name="gateway_pending_events'" org.eventb.core.type="ℙ(GATEWAYS×TARGET_TRANSACTIONS)"/>
        <org.eventb.core.poIdentifier name="pending_event" org.eventb.core.type="TARGET_TRANSACTIONS"/>
        <org.eventb.core.poIdentifier name="emitted_event" org.eventb.core.type="SMART_CONTRACT_EVENTS"/>
        <org.eventb.core.poIdentifier name="emitted_events'" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×SMART_CONTRACT_EVENTS)"/>
Guzman Llambias's avatar
Change project name
Guzman Llambias committed
114 
    </org.eventb.core.poPredicateSet>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
115 116 117 118 
    <org.eventb.core.poPredicateSet name="EVTALLHYPreceived_target_transactionx" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#EVTIDENTreceived_target_transactionx" org.eventb.core.poStamp="39">
        <org.eventb.core.poPredicate name="PRD0" 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.poPredicate name="PRD1" 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.poPredicate name="PRD2" 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"/>
Guzman Llambias's avatar
Change project name
Guzman Llambias committed
119 
    </org.eventb.core.poPredicateSet>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
120 121 122 123 124 
    <org.eventb.core.poSequent name="SUBMIT_TX_TO_FABRIC/inv12/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="39">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#EVTALLHYPreceived_target_transactiony"/>
        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="authenticated_transactions{target_smart_contract ↦ transaction ↦ user}∈received_target_transactions∪{target_smart_contract ↦ transaction} → 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.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" 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.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" 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"/>
Guzman Llambias's avatar
Add Ethereum -> Fabric animation (WIP)  
Guzman Llambias committed
125 
        <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" 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"/>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
126 
        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poSequent#SUBMIT_TX_TO_FABRIC\/inv12\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
Guzman Llambias's avatar
Change project name
Guzman Llambias committed
127 128 
        <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD1"/>
    </org.eventb.core.poSequent>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
129 130 131 132 133 
    <org.eventb.core.poSequent name="SUBMIT_TX_TO_FABRIC/inv13/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="39">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#EVTALLHYPreceived_target_transactiony"/>
        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀tx⦂CROSS_CHAIN_SMART_CONTRACTS×TARGET_TRANSACTIONS·tx∈received_target_transactions∪{target_smart_contract ↦ transaction}⇒(∃u⦂USERS·u∈authenticated_users∧tx ↦ u∈authenticated_transactions{target_smart_contract ↦ transaction ↦ user})" 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.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" 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.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" 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"/>
Guzman Llambias's avatar
Add Ethereum -> Fabric animation (WIP)  
Guzman Llambias committed
134 
        <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" 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"/>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
135 
        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poSequent#SUBMIT_TX_TO_FABRIC\/inv13\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
Guzman Llambias's avatar
Change project name
Guzman Llambias committed
136 137 
        <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD2"/>
    </org.eventb.core.poSequent>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
138 139 140 141 142 
    <org.eventb.core.poSequent name="SUBMIT_TX_TO_FABRIC/inv15/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="39">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#EVTALLHYPreceived_target_transactiony"/>
        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀u⦂USERS·u∈(authenticated_transactions{target_smart_contract ↦ transaction ↦ user})[received_target_transactions∪{target_smart_contract ↦ transaction}]⇒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.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" 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.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" 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"/>
Guzman Llambias's avatar
Complete Ethereum -> Fabric animation  
Guzman Llambias committed
143 
        <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" 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"/>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
144 
        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poSequent#SUBMIT_TX_TO_FABRIC\/inv15\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
Guzman Llambias's avatar
Change project name
Guzman Llambias committed
145 146 
        <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD4"/>
    </org.eventb.core.poSequent>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
147 148 149 150 
    <org.eventb.core.poPredicateSet name="EVTIDENTreceived_target_transactiony" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="39">
        <org.eventb.core.poIdentifier name="gateway_pending_events'" org.eventb.core.type="ℙ(GATEWAYS×TARGET_TRANSACTIONS)"/>
        <org.eventb.core.poIdentifier name="authenticated_transactions'" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×TARGET_TRANSACTIONS×USERS)"/>
        <org.eventb.core.poIdentifier name="transaction" org.eventb.core.type="TARGET_TRANSACTIONS"/>
Guzman Llambias's avatar
Change project name
Guzman Llambias committed
151 
        <org.eventb.core.poIdentifier name="user" org.eventb.core.type="USERS"/>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
152 153 
        <org.eventb.core.poIdentifier name="pending_event" org.eventb.core.type="TARGET_TRANSACTIONS"/>
        <org.eventb.core.poIdentifier name="received_target_transactions'" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×TARGET_TRANSACTIONS)"/>
Guzman Llambias's avatar
Change project name
Guzman Llambias committed
154 
    </org.eventb.core.poPredicateSet>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
155 156 157 158 159 
    <org.eventb.core.poPredicateSet name="EVTALLHYPreceived_target_transactiony" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#EVTIDENTreceived_target_transactiony" org.eventb.core.poStamp="39">
        <org.eventb.core.poPredicate name="PRD0" 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.poPredicate name="PRD1" 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.poPredicate name="PRD2" 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.poPredicate name="PRD3" 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"/>
Guzman Llambias's avatar
Add Ethereum -> Fabric animation (WIP)  
Guzman Llambias committed
160 
    </org.eventb.core.poPredicateSet>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
161 162 163 
    <org.eventb.core.poSequent name="CREATE_GATEWAY_USER/inv12/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="39">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#EVTALLHYPreceived_target_transactionz"/>
        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="authenticated_transactions∈received_target_transactions → authenticated_users∪{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.invariant#_jV9TI8EWEe6yC4BToIaAqA"/>
Guzman Llambias's avatar
Add Ethereum -> Fabric animation (WIP)  
Guzman Llambias committed
164 165 166 167 168 
        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" 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.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" 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.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poSequent#CREATE_GATEWAY_USER\/inv12\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD1"/>
    </org.eventb.core.poSequent>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
169 170 171 
    <org.eventb.core.poSequent name="CREATE_GATEWAY_USER/inv13/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="39">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#EVTALLHYPreceived_target_transactionz"/>
        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀tx⦂CROSS_CHAIN_SMART_CONTRACTS×TARGET_TRANSACTIONS·tx∈received_target_transactions⇒(∃u⦂USERS·u∈authenticated_users∪{gateway_user}∧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"/>
Guzman Llambias's avatar
Add Ethereum -> Fabric animation (WIP)  
Guzman Llambias committed
172 173 174 175 176 
        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" 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.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" 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.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poSequent#CREATE_GATEWAY_USER\/inv13\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD2"/>
    </org.eventb.core.poSequent>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
177 178 
    <org.eventb.core.poSequent name="CREATE_GATEWAY_USER/inv14/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="39">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#EVTALLHYPreceived_target_transactionz"/>
Guzman Llambias's avatar
Complete Ethereum -> Fabric animation  
Guzman Llambias committed
179 
        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="grants∈authenticated_users∪{gateway_user} ↔ 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"/>
Guzman Llambias's avatar
Add Ethereum -> Fabric animation (WIP)  
Guzman Llambias committed
180 
        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" 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
Complete Ethereum -> Fabric animation  
Guzman Llambias committed
181 
        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" 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"/>
Guzman Llambias's avatar
Add Ethereum -> Fabric animation (WIP)  
Guzman Llambias committed
182 183 184 
        <org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poSequent#CREATE_GATEWAY_USER\/inv14\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD3"/>
    </org.eventb.core.poSequent>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
185 
    <org.eventb.core.poPredicateSet name="EVTIDENTreceived_target_transactionz" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="39">
Guzman Llambias's avatar
Add Ethereum -> Fabric animation (WIP)  
Guzman Llambias committed
186 187 
        <org.eventb.core.poIdentifier name="authenticated_users'" org.eventb.core.type="ℙ(USERS)"/>
    </org.eventb.core.poPredicateSet>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
188 
    <org.eventb.core.poPredicateSet name="EVTALLHYPreceived_target_transactionz" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#EVTIDENTreceived_target_transactionz" org.eventb.core.poStamp="39">
Guzman Llambias's avatar
Add Ethereum -> Fabric animation (WIP)  
Guzman Llambias committed
189 190 
        <org.eventb.core.poPredicate name="PRD0" 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.poPredicateSet>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
191 192 
    <org.eventb.core.poSequent name="GRANT_PERMISSION/inv14/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="39">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#EVTALLHYPreceived_target_transaction{"/>
Guzman Llambias's avatar
Complete Ethereum -> Fabric animation  
Guzman Llambias committed
193 194 195 196 197 198 
        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="grants∪{user ↦ permission}∈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.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" 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.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" 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.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poSequent#GRANT_PERMISSION\/inv14\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD3"/>
    </org.eventb.core.poSequent>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
199 200 201 
    <org.eventb.core.poSequent name="GRANT_PERMISSION/inv15/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="39">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#EVTALLHYPreceived_target_transaction{"/>
        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀u⦂USERS·u∈authenticated_transactions[received_target_transactions]⇒u ↦ write∈grants∪{user ↦ permission}" 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"/>
Guzman Llambias's avatar
Complete Ethereum -> Fabric animation  
Guzman Llambias committed
202 203 204 205 206 
        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" 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.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" 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.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poSequent#GRANT_PERMISSION\/inv15\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD4"/>
    </org.eventb.core.poSequent>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
207 
    <org.eventb.core.poPredicateSet name="EVTIDENTreceived_target_transaction{" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="39">
Guzman Llambias's avatar
Add Ethereum -> Fabric animation (WIP)  
Guzman Llambias committed
208 209 
        <org.eventb.core.poIdentifier name="permission" org.eventb.core.type="PERMISSIONS"/>
        <org.eventb.core.poIdentifier name="user" org.eventb.core.type="USERS"/>
Guzman Llambias's avatar
Complete Ethereum -> Fabric animation  
Guzman Llambias committed
210 
        <org.eventb.core.poIdentifier name="grants'" org.eventb.core.type="ℙ(USERS×PERMISSIONS)"/>
Guzman Llambias's avatar
Add Ethereum -> Fabric animation (WIP)  
Guzman Llambias committed
211 
    </org.eventb.core.poPredicateSet>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
212 
    <org.eventb.core.poPredicateSet name="EVTALLHYPreceived_target_transaction{" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#EVTIDENTreceived_target_transaction{" org.eventb.core.poStamp="39">
Guzman Llambias's avatar
Add Ethereum -> Fabric animation (WIP)  
Guzman Llambias committed
213 214 
        <org.eventb.core.poPredicate name="PRD0" 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.poPredicate name="PRD1" 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"/>
Guzman Llambias's avatar
Complete Ethereum -> Fabric animation  
Guzman Llambias committed
215 
        <org.eventb.core.poPredicate name="PRD2" 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"/>
Guzman Llambias's avatar
Add Ethereum -> Fabric animation (WIP)  
Guzman Llambias committed
216 
    </org.eventb.core.poPredicateSet>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
217 
    <org.eventb.core.poPredicateSet name="ALLHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poStamp="39">
Guzman Llambias's avatar
Add Ethereum -> Fabric animation (WIP)  
Guzman Llambias committed
218 
        <org.eventb.core.poPredicate name="PRD0" 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"/>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
219 220 
        <org.eventb.core.poPredicate name="PRD1" 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.poPredicate name="PRD2" 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"/>
Guzman Llambias's avatar
Complete Ethereum -> Fabric animation  
Guzman Llambias committed
221 
        <org.eventb.core.poPredicate name="PRD3" 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"/>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
222 
        <org.eventb.core.poPredicate name="PRD4" 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"/>
Guzman Llambias's avatar
Change project name
Guzman Llambias committed
223 224 
    </org.eventb.core.poPredicateSet>
</org.eventb.core.poFile>