Skip to content
Snippets Groups Projects
Normal view History Permalink
CCTx_Ethereum_Fabric_c2.bcc 5.74 KiB
Newer Older
Guzman Llambias's avatar
Change project name
Guzman Llambias committed
1 2 3 4 5 6 7 
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.scContextFile org.eventb.core.accurate="true" org.eventb.core.configuration="org.eventb.core.fwd;de.prob.symbolic.ctxBase">
    <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#'"/>
    <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
8 
        <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
9 10 11 
        <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
12 13 
        <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
14 15 16 
        <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>
Guzman Llambias's avatar
Change trigger for emit event  
Guzman Llambias committed
17 18 
    <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
19 20 21 22 23 24 
    <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.scContextFile>