Skip to content
Snippets Groups Projects
Normal view History Permalink
CCTx_Abstract_DLT_c1.bpo 2.21 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="7">
    <org.eventb.core.poPredicateSet name="ABSHYP" org.eventb.core.poStamp="7">
        <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 12 
        <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.poPredicateSet>
Guzman Llambias's avatar
Fix from reviewers comments  
Guzman Llambias committed
13 
    <org.eventb.core.poPredicateSet name="ALLHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Abstract_DLT_c1.bpo|org.eventb.core.poFile#CCTx_Abstract_DLT_c1|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poStamp="7">
Guzman Llambias's avatar
Change project name  
Guzman Llambias committed
14 15 16 
        <org.eventb.core.poPredicate name="PRD0" 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="PRD1" 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="PRD2" 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
17 18 
    </org.eventb.core.poPredicateSet>
</org.eventb.core.poFile>