Skip to content
Snippets Groups Projects
Normal view History Permalink
CCTx_Abstract_DLT_m1.bpo 14.2 KiB
Newer Older
Guzmán Llambías's avatar
Initial specification of big
Guzmán Llambías 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="22">
    <org.eventb.core.poPredicateSet name="CTXHYP" org.eventb.core.poStamp="22">
        <org.eventb.core.poIdentifier name="TARGET_TRANSACTIONS" org.eventb.core.type="ℙ(TARGET_TRANSACTIONS)"/>
Guzmán Llambías's avatar
Initial specification of big
Guzmán Llambías 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)"/>
Guzmán Llambías's avatar
Initial specification of big
Guzmán Llambías committed
8 9 10 11 
        <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"/>
Guzman Llambias's avatar
Change project name  
Guzman Llambias committed
12 13 14 
        <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"/>
Guzmán Llambías's avatar
Initial specification of big
Guzmán Llambías committed
15 
    </org.eventb.core.poPredicateSet>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
16 17 18 
    <org.eventb.core.poPredicateSet name="ABSHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Abstract_DLT_m1.bpo|org.eventb.core.poFile#CCTx_Abstract_DLT_m1|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poStamp="22">
        <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)"/>
Guzmán Llambías's avatar
Fix proofs  
Guzmán Llambías committed
19 
        <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
20 21 
        <org.eventb.core.poIdentifier name="emitted_events" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×SMART_CONTRACT_EVENTS)"/>
        <org.eventb.core.poIdentifier name="received_source_transactions" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×SOURCE_TRANSACTIONS)"/>
Guzmán Llambías's avatar
Initial specification of big
Guzmán Llambías committed
22 
    </org.eventb.core.poPredicateSet>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
23 24 
    <org.eventb.core.poPredicateSet name="EVTIDENTreceived_target_transactiont" org.eventb.core.parentSet="/gateway-event-b/CCTx_Abstract_DLT_m1.bpo|org.eventb.core.poFile#CCTx_Abstract_DLT_m1|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poStamp="22">
        <org.eventb.core.poIdentifier name="gateway_pending_events'" org.eventb.core.type="ℙ(GATEWAYS×TARGET_TRANSACTIONS)"/>
Guzmán Llambías's avatar
Fix proofs  
Guzmán Llambías committed
25 
        <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
26 27 28 
        <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.poIdentifier name="received_target_transactions'" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×TARGET_TRANSACTIONS)"/>
Guzmán Llambías's avatar
Initial specification of big
Guzmán Llambías committed
29 
    </org.eventb.core.poPredicateSet>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
30 31 
    <org.eventb.core.poPredicateSet name="EVTALLHYPreceived_target_transactiont" org.eventb.core.parentSet="/gateway-event-b/CCTx_Abstract_DLT_m1.bpo|org.eventb.core.poFile#CCTx_Abstract_DLT_m1|org.eventb.core.poPredicateSet#EVTIDENTreceived_target_transactiont" org.eventb.core.poStamp="22"/>
    <org.eventb.core.poPredicateSet name="EVTIDENTreceived_target_transactionu" org.eventb.core.parentSet="/gateway-event-b/CCTx_Abstract_DLT_m1.bpo|org.eventb.core.poFile#CCTx_Abstract_DLT_m1|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="22">
Guzmán Llambías's avatar
Fix proofs  
Guzmán Llambías committed
32 33 
        <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
34 
    <org.eventb.core.poPredicateSet name="EVTALLHYPreceived_target_transactionu" org.eventb.core.parentSet="/gateway-event-b/CCTx_Abstract_DLT_m1.bpo|org.eventb.core.poFile#CCTx_Abstract_DLT_m1|org.eventb.core.poPredicateSet#EVTIDENTreceived_target_transactionu" org.eventb.core.poStamp="22">
Guzman Llambias's avatar
Change trigger for emit event  
Guzman Llambias committed
35 
        <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"/>
Guzmán Llambías's avatar
Fix proofs  
Guzmán Llambías committed
36 
    </org.eventb.core.poPredicateSet>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
37 38 39 
    <org.eventb.core.poPredicateSet name="EVTIDENTreceived_target_transactionv" org.eventb.core.parentSet="/gateway-event-b/CCTx_Abstract_DLT_m1.bpo|org.eventb.core.poFile#CCTx_Abstract_DLT_m1|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="22">
        <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)"/>
Guzmán Llambías's avatar
Initial specification of big
Guzmán Llambías committed
40 
    </org.eventb.core.poPredicateSet>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
41 42 43 
    <org.eventb.core.poPredicateSet name="EVTALLHYPreceived_target_transactionv" org.eventb.core.parentSet="/gateway-event-b/CCTx_Abstract_DLT_m1.bpo|org.eventb.core.poFile#CCTx_Abstract_DLT_m1|org.eventb.core.poPredicateSet#EVTIDENTreceived_target_transactionv" org.eventb.core.poStamp="22">
        <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"/>
Guzmán Llambías's avatar
Initial specification of big
Guzmán Llambías committed
44 
    </org.eventb.core.poPredicateSet>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
45 46 47 48 49 
    <org.eventb.core.poPredicateSet name="EVTIDENTreceived_target_transactionw" org.eventb.core.parentSet="/gateway-event-b/CCTx_Abstract_DLT_m1.bpo|org.eventb.core.poFile#CCTx_Abstract_DLT_m1|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="22">
        <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)"/>
Guzmán Llambías's avatar
Initial specification of big
Guzmán Llambías committed
50 
    </org.eventb.core.poPredicateSet>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
51 52 53 
    <org.eventb.core.poPredicateSet name="EVTALLHYPreceived_target_transactionw" org.eventb.core.parentSet="/gateway-event-b/CCTx_Abstract_DLT_m1.bpo|org.eventb.core.poFile#CCTx_Abstract_DLT_m1|org.eventb.core.poPredicateSet#EVTIDENTreceived_target_transactionw" org.eventb.core.poStamp="22">
        <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"/>
Guzmán Llambías's avatar
Initial specification of big
Guzmán Llambías committed
54 
    </org.eventb.core.poPredicateSet>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
55 56 57 58 59 
    <org.eventb.core.poPredicateSet name="EVTIDENTreceived_target_transactionx" org.eventb.core.parentSet="/gateway-event-b/CCTx_Abstract_DLT_m1.bpo|org.eventb.core.poFile#CCTx_Abstract_DLT_m1|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="22">
        <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)"/>
Guzmán Llambías's avatar
Initial specification of big
Guzmán Llambías committed
60 
    </org.eventb.core.poPredicateSet>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
61 62 63 64 
    <org.eventb.core.poPredicateSet name="EVTALLHYPreceived_target_transactionx" org.eventb.core.parentSet="/gateway-event-b/CCTx_Abstract_DLT_m1.bpo|org.eventb.core.poFile#CCTx_Abstract_DLT_m1|org.eventb.core.poPredicateSet#EVTIDENTreceived_target_transactionx" org.eventb.core.poStamp="22">
        <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"/>
Guzmán Llambías's avatar
Initial specification of big
Guzmán Llambías committed
65 
    </org.eventb.core.poPredicateSet>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
66 67 68 69 70 
    <org.eventb.core.poPredicateSet name="EVTIDENTreceived_target_transactiony" org.eventb.core.parentSet="/gateway-event-b/CCTx_Abstract_DLT_m1.bpo|org.eventb.core.poFile#CCTx_Abstract_DLT_m1|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="22">
        <org.eventb.core.poIdentifier name="gateway_pending_events'" org.eventb.core.type="ℙ(GATEWAYS×TARGET_TRANSACTIONS)"/>
        <org.eventb.core.poIdentifier name="transaction" org.eventb.core.type="TARGET_TRANSACTIONS"/>
        <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)"/>
Guzmán Llambías's avatar
Initial specification of big
Guzmán Llambías committed
71 
    </org.eventb.core.poPredicateSet>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
72 73 74 
    <org.eventb.core.poPredicateSet name="EVTALLHYPreceived_target_transactiony" org.eventb.core.parentSet="/gateway-event-b/CCTx_Abstract_DLT_m1.bpo|org.eventb.core.poFile#CCTx_Abstract_DLT_m1|org.eventb.core.poPredicateSet#EVTIDENTreceived_target_transactiony" org.eventb.core.poStamp="22">
        <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"/>
Guzmán Llambías's avatar
Initial specification of big
Guzmán Llambías committed
75 
    </org.eventb.core.poPredicateSet>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
76 77 78 
    <org.eventb.core.poPredicateSet name="ALLHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Abstract_DLT_m1.bpo|org.eventb.core.poFile#CCTx_Abstract_DLT_m1|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poStamp="22">
        <org.eventb.core.poPredicate name="PRD0" 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="PRD1" 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"/>
Guzman Llambias's avatar
Change trigger for emit event  
Guzman Llambias committed
79 
        <org.eventb.core.poPredicate name="PRD2" 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"/>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
80 81 
        <org.eventb.core.poPredicate name="PRD3" 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="PRD4" 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"/>
Guzmán Llambías's avatar
Initial specification of big
Guzmán Llambías committed
82 83 
    </org.eventb.core.poPredicateSet>
</org.eventb.core.poFile>