Skip to content
Snippets Groups Projects
Normal view Permalink
CCTx_Ethereum_Fabric_c2.bpo 3.19 KiB
Newer Older
Guzmán Llambías's avatar
Ethereum -> Fabric behaviour
Guzmán Llambías committed
1 
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
Guzman Llambias's avatar
CCTx Fabric -> Ethereum Preserve balance gateway  
Guzman Llambias committed
2 3 
<org.eventb.core.poFile org.eventb.core.poStamp="0">
    <org.eventb.core.poPredicateSet name="ABSHYP" org.eventb.core.poStamp="0">
Guzmán Llambías's avatar
Ethereum -> Fabric behaviour
Guzmán Llambías committed
4 5 6 7 8 9 10 11 
        <org.eventb.core.poIdentifier name="CROSS_CHAIN_EVENTS" org.eventb.core.type="ℙ(CROSS_CHAIN_EVENTS)"/>
        <org.eventb.core.poIdentifier name="CROSS_CHAIN_TRANSACTIONS" org.eventb.core.type="ℙ(CROSS_CHAIN_TRANSACTIONS)"/>
        <org.eventb.core.poIdentifier name="GATEWAYS" org.eventb.core.type="ℙ(GATEWAYS)"/>
        <org.eventb.core.poIdentifier name="TRANSACTIONS" org.eventb.core.type="ℙ(TRANSACTIONS)"/>
        <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
CCTx Fabric -> Ethereum Preserve balance gateway  
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="/BIG/CCTx_Abstract_DLT_c1.buc|org.eventb.core.contextFile#CCTx_Abstract_DLT_c1|org.eventb.core.axiom#_j4-IUKsXEe6I4bA9GxwhqQ"/>
        <org.eventb.core.poPredicate name="CROSS_CHAIN_SMART_CONTRACTU" org.eventb.core.predicate="target_smart_contract∈CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.source="/BIG/CCTx_Abstract_DLT_c1.buc|org.eventb.core.contextFile#CCTx_Abstract_DLT_c1|org.eventb.core.axiom#_j4-vYKsXEe6I4bA9GxwhqQ"/>
        <org.eventb.core.poPredicate name="CROSS_CHAIN_SMART_CONTRACTV" org.eventb.core.predicate="gateway∈GATEWAYS" org.eventb.core.source="/BIG/CCTx_Abstract_DLT_c1.buc|org.eventb.core.contextFile#CCTx_Abstract_DLT_c1|org.eventb.core.axiom#_j4-vYasXEe6I4bA9GxwhqQ"/>
Guzmán Llambías's avatar
Ethereum -> Fabric behaviour
Guzmán Llambías committed
15 16 17 18 19 20 
        <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"/>
    </org.eventb.core.poPredicateSet>
Guzman Llambias's avatar
CCTx Fabric -> Ethereum Preserve balance gateway  
Guzman Llambias committed
21 22 23 
    <org.eventb.core.poPredicateSet name="ALLHYP" org.eventb.core.parentSet="/BIG/CCTx_Ethereum_Fabric_c2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_c2|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poStamp="0">
        <org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="partition(PERMISSIONS,{read},{write})" org.eventb.core.source="/BIG/CCTx_Ethereum_Fabric_c2.buc|org.eventb.core.contextFile#CCTx_Ethereum_Fabric_c2|org.eventb.core.axiom#_e542gK75Ee6N-vMrFZcPfQ"/>
        <org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="gateway_user∈USERS" org.eventb.core.source="/BIG/CCTx_Ethereum_Fabric_c2.buc|org.eventb.core.contextFile#CCTx_Ethereum_Fabric_c2|org.eventb.core.axiom#_-6gTUK75Ee6N-vMrFZcPfQ"/>
Guzmán Llambías's avatar
Ethereum -> Fabric behaviour
Guzmán Llambías committed
24 25 
    </org.eventb.core.poPredicateSet>
</org.eventb.core.poFile>