Fix from reviewers comments

gateway-event-b/CCTx_Abstract_Animation_m2.bps

 <?xml version="1.0" encoding="UTF-8" standalone="no"?>
 <org.eventb.core.psFile>
-    <org.eventb.core.psStatus name="SUBSCRIBE_SMART_CONTRACT_EVENTS/inv11/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="INITIATE_CC_TX/inv12/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="INITIATE_CC_TX/inv15/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="SUBMIT_CC_TX/inv14/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="SUBMIT_CC_TX/inv15/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="INITIALISATION/inv11/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="13" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="INITIALISATION/inv12/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="13" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="INITIALISATION/inv13/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="13" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="INITIALISATION/inv14/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="13" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="INITIALISATION/inv15/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="13" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="SUBSCRIBE_SMART_CONTRACT_EVENTS/inv11/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="13" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="INITIATE_CC_TX/inv12/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="13" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="INITIATE_CC_TX/inv15/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="13" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="EMIT_EVENT/inv12/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="13" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="EMIT_EVENT/inv13/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="13" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="EMIT_EVENT/inv15/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="13" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="LISTEN_EVENT/inv13/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="13" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="LISTEN_EVENT/inv14/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="13" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="LISTEN_EVENT/inv15/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="13" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="SUBMIT_TX/inv14/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="13" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="SUBMIT_TX/inv15/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="13" org.eventb.core.psManual="false"/>
 </org.eventb.core.psFile>

gateway-event-b/CCTx_Abstract_DLT_c1.bcc

@@ -3,12 +3,12 @@
     <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"/>
+    <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)"/>
     <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.scCarrierSet name="CROSS_CHAIN_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#_lhTmNr7uEe6laZimEYihUg" org.eventb.core.type="ℙ(CROSS_CHAIN_EVENTS)"/>
     <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="CROSS_CHAIN_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#_lhTmN77uEe6laZimEYihUg" org.eventb.core.type="ℙ(CROSS_CHAIN_TRANSACTIONS)"/>
     <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)"/>
+    <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)"/>
     <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="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#_lhTmNL7uEe6laZimEYihUg" org.eventb.core.type="ℙ(TRANSACTIONS)"/>
     <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.scContextFile>

gateway-event-b/CCTx_Abstract_DLT_c1.bpo

 <?xml version="1.0" encoding="UTF-8" standalone="no"?>
-<org.eventb.core.poFile org.eventb.core.poStamp="4">
-    <org.eventb.core.poPredicateSet name="ABSHYP" org.eventb.core.poStamp="2">
-        <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.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)"/>
         <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="SOURCE_TRANSACTIONS" org.eventb.core.type="ℙ(SOURCE_TRANSACTIONS)"/>
+        <org.eventb.core.poIdentifier name="SMART_CONTRACT_EVENTS" org.eventb.core.type="ℙ(SMART_CONTRACT_EVENTS)"/>
         <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>
-    <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="4">
+    <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">
         <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"/>

gateway-event-b/CCTx_Abstract_DLT_c1.buc

 <?xml version="1.0" encoding="UTF-8" standalone="no"?>
-<org.eventb.core.contextFile org.eventb.core.configuration="org.eventb.core.fwd;de.prob.symbolic.ctxBase" org.eventb.core.generated="false" org.eventb.emf.persistence.emf_id="_lhKcS77uEe6laZimEYihUg" org.eventb.texttools.text_lastmodified="1706564242436" org.eventb.texttools.text_representation="context CCTx_Abstract_DLT_c1&#10;&#10;sets GATEWAYS TRANSACTIONS CROSS_CHAIN_SMART_CONTRACTS CROSS_CHAIN_EVENTS CROSS_CHAIN_TRANSACTIONS&#10;&#10;constants source_smart_contract target_smart_contract gateway&#10;&#10;axioms&#10;  @axm1; source_smart_contract ∈ CROSS_CHAIN_SMART_CONTRACTS&#10;  @axm2; target_smart_contract ∈ CROSS_CHAIN_SMART_CONTRACTS&#10;  @axm3; gateway ∈ GATEWAYS&#10;end" version="3">
-    <org.eventb.core.axiom name="_lhKcab7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.label="axm1;" org.eventb.core.predicate="source_smart_contract ∈ CROSS_CHAIN_SMART_CONTRACTS" org.eventb.emf.persistence.emf_id="_lhKcSL7uEe6laZimEYihUg"/>
-    <org.eventb.core.axiom name="_lhKcar7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.label="axm2;" org.eventb.core.predicate="target_smart_contract ∈ CROSS_CHAIN_SMART_CONTRACTS" org.eventb.emf.persistence.emf_id="_lhKcSb7uEe6laZimEYihUg"/>
-    <org.eventb.core.axiom name="_lhKca77uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.label="axm3;" org.eventb.core.predicate="gateway ∈ GATEWAYS" org.eventb.emf.persistence.emf_id="_lhKcSr7uEe6laZimEYihUg"/>
-    <org.eventb.core.constant name="_lhTmML7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="source_smart_contract" org.eventb.emf.persistence.emf_id="_lhKcRb7uEe6laZimEYihUg"/>
-    <org.eventb.core.constant name="_lhTmMb7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="target_smart_contract" org.eventb.emf.persistence.emf_id="_lhKcRr7uEe6laZimEYihUg"/>
-    <org.eventb.core.constant name="_lhTmMr7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="gateway" org.eventb.emf.persistence.emf_id="_lhKcR77uEe6laZimEYihUg"/>
-    <org.eventb.core.carrierSet name="_lhTmM77uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="GATEWAYS" org.eventb.emf.persistence.emf_id="_lhKcQL7uEe6laZimEYihUg"/>
-    <org.eventb.core.carrierSet name="_lhTmNL7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="TRANSACTIONS" org.eventb.emf.persistence.emf_id="_lhKcQb7uEe6laZimEYihUg"/>
-    <org.eventb.core.carrierSet name="_lhTmNb7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.emf.persistence.emf_id="_lhKcQr7uEe6laZimEYihUg"/>
-    <org.eventb.core.carrierSet name="_lhTmNr7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="CROSS_CHAIN_EVENTS" org.eventb.emf.persistence.emf_id="_lhKcQ77uEe6laZimEYihUg"/>
-    <org.eventb.core.carrierSet name="_lhTmN77uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="CROSS_CHAIN_TRANSACTIONS" org.eventb.emf.persistence.emf_id="_lhKcRL7uEe6laZimEYihUg"/>
+<org.eventb.core.contextFile org.eventb.core.configuration="org.eventb.core.fwd;de.prob.symbolic.ctxBase" org.eventb.core.generated="false" org.eventb.emf.persistence.emf_id="_H4L1y_RjEe60CqkwWvstGA" org.eventb.texttools.text_lastmodified="1712441706268" org.eventb.texttools.text_representation="context CCTx_Abstract_DLT_c1&#10;&#10;sets GATEWAYS SOURCE_TRANSACTIONS CROSS_CHAIN_SMART_CONTRACTS SMART_CONTRACT_EVENTS TARGET_TRANSACTIONS&#10;&#10;constants source_smart_contract target_smart_contract gateway&#10;&#10;axioms&#10;  @axm1; source_smart_contract ∈ CROSS_CHAIN_SMART_CONTRACTS&#10;  @axm2; target_smart_contract ∈ CROSS_CHAIN_SMART_CONTRACTS&#10;  @axm3; gateway ∈ GATEWAYS&#10;end" version="3">
+    <org.eventb.core.axiom name="_lhKcab7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.label="axm1;" org.eventb.core.predicate="source_smart_contract ∈ CROSS_CHAIN_SMART_CONTRACTS" org.eventb.emf.persistence.emf_id="_H4L1yPRjEe60CqkwWvstGA"/>
+    <org.eventb.core.axiom name="_lhKcar7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.label="axm2;" org.eventb.core.predicate="target_smart_contract ∈ CROSS_CHAIN_SMART_CONTRACTS" org.eventb.emf.persistence.emf_id="_H4L1yfRjEe60CqkwWvstGA"/>
+    <org.eventb.core.axiom name="_lhKca77uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.label="axm3;" org.eventb.core.predicate="gateway ∈ GATEWAYS" org.eventb.emf.persistence.emf_id="_H4L1yvRjEe60CqkwWvstGA"/>
+    <org.eventb.core.constant name="_lhTmML7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="source_smart_contract" org.eventb.emf.persistence.emf_id="_H4L1xfRjEe60CqkwWvstGA"/>
+    <org.eventb.core.constant name="_lhTmMb7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="target_smart_contract" org.eventb.emf.persistence.emf_id="_H4L1xvRjEe60CqkwWvstGA"/>
+    <org.eventb.core.constant name="_lhTmMr7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="gateway" org.eventb.emf.persistence.emf_id="_H4L1x_RjEe60CqkwWvstGA"/>
+    <org.eventb.core.carrierSet name="_lhTmM77uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="GATEWAYS" org.eventb.emf.persistence.emf_id="_H4L1wPRjEe60CqkwWvstGA"/>
+    <org.eventb.core.carrierSet name="_XWUxAPReEe60CqkwWvstGA" org.eventb.core.generated="false" org.eventb.core.identifier="SOURCE_TRANSACTIONS" org.eventb.emf.persistence.emf_id="_H4L1wfRjEe60CqkwWvstGA"/>
+    <org.eventb.core.carrierSet name="_lhTmNb7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.emf.persistence.emf_id="_H4L1wvRjEe60CqkwWvstGA"/>
+    <org.eventb.core.carrierSet name="_H4R8YPRjEe60CqkwWvstGA" org.eventb.core.generated="false" org.eventb.core.identifier="SMART_CONTRACT_EVENTS" org.eventb.emf.persistence.emf_id="_H4L1w_RjEe60CqkwWvstGA"/>
+    <org.eventb.core.carrierSet name="_dldMwPReEe60CqkwWvstGA" org.eventb.core.generated="false" org.eventb.core.identifier="TARGET_TRANSACTIONS" org.eventb.emf.persistence.emf_id="_H4L1xPRjEe60CqkwWvstGA"/>
 </org.eventb.core.contextFile>

gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bps

 <?xml version="1.0" encoding="UTF-8" standalone="no"?>
 <org.eventb.core.psFile>
-    <org.eventb.core.psStatus name="INITIALISATION/inv11/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="INITIALISATION/inv12/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="INITIALISATION/inv13/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="INITIALISATION/inv14/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="INITIALISATION/inv15/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="INITIALISATION/inv16/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="INITIALISATION/inv17/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="SUBSCRIBE_SMART_CONTRACT_EVENTS_IN_ETHEREUM/inv11/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="INITIATE_CC_TX_IN_ETHEREUM/inv12/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="INITIATE_CC_TX_IN_ETHEREUM/inv15/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="EMIT_CC_TX_EVENT_IN_ETHEREUM/inv12/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="EMIT_CC_TX_EVENT_IN_ETHEREUM/inv13/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="EMIT_CC_TX_EVENT_IN_ETHEREUM/inv15/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="LISTEN_CC_TX_EVENT_IN_ETHEREUM/inv13/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="LISTEN_CC_TX_EVENT_IN_ETHEREUM/inv14/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="LISTEN_CC_TX_EVENT_IN_ETHEREUM/inv15/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="SUBMIT_CC_TX_TO_FABRIC/inv14/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="SUBMIT_CC_TX_TO_FABRIC/inv15/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="CREATE_GATEWAY_USER/inv16/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="GRANT_PERMISSION/inv17/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="INITIALISATION/inv11/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="11" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="INITIALISATION/inv12/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="11" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="INITIALISATION/inv13/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="11" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="INITIALISATION/inv14/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="11" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="INITIALISATION/inv15/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="11" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="INITIALISATION/inv16/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="11" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="INITIALISATION/inv17/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="11" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="SUBSCRIBE_SMART_CONTRACT_EVENTS_IN_ETHEREUM/inv11/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="11" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="INITIATE_CC_TX_IN_ETHEREUM/inv12/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="11" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="INITIATE_CC_TX_IN_ETHEREUM/inv15/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="11" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="EMIT_EVENT_IN_ETHEREUM/inv12/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="11" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="EMIT_EVENT_IN_ETHEREUM/inv13/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="11" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="EMIT_EVENT_IN_ETHEREUM/inv15/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="11" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="LISTEN_EVENT_IN_ETHEREUM/inv13/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="11" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="LISTEN_EVENT_IN_ETHEREUM/inv14/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="11" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="LISTEN_EVENT_IN_ETHEREUM/inv15/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="11" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="SUBMIT_TX_TO_FABRIC/inv14/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="11" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="SUBMIT_TX_TO_FABRIC/inv15/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="11" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="CREATE_GATEWAY_USER/inv16/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="11" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="GRANT_PERMISSION/inv17/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="11" org.eventb.core.psManual="false"/>
 </org.eventb.core.psFile>

gateway-event-b/CCTx_Ethereum_Fabric_c2.bcc

@@ -5,13 +5,13 @@
         <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"/>
+        <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)"/>
         <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.scCarrierSet name="CROSS_CHAIN_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#_lhTmNr7uEe6laZimEYihUg" org.eventb.core.type="ℙ(CROSS_CHAIN_EVENTS)"/>
         <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="CROSS_CHAIN_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#_lhTmN77uEe6laZimEYihUg" org.eventb.core.type="ℙ(CROSS_CHAIN_TRANSACTIONS)"/>
         <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)"/>
+        <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)"/>
         <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="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#_lhTmNL7uEe6laZimEYihUg" org.eventb.core.type="ℙ(TRANSACTIONS)"/>
         <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>
     <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"/>

gateway-event-b/CCTx_Ethereum_Fabric_c2.bpo

 <?xml version="1.0" encoding="UTF-8" standalone="no"?>
-<org.eventb.core.poFile org.eventb.core.poStamp="5">
-    <org.eventb.core.poPredicateSet name="ABSHYP" org.eventb.core.poStamp="4">
-        <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.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)"/>
         <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="SOURCE_TRANSACTIONS" org.eventb.core.type="ℙ(SOURCE_TRANSACTIONS)"/>
+        <org.eventb.core.poIdentifier name="SMART_CONTRACT_EVENTS" org.eventb.core.type="ℙ(SMART_CONTRACT_EVENTS)"/>
         <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"/>
@@ -18,7 +18,7 @@
         <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>
-    <org.eventb.core.poPredicateSet name="ALLHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_c2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_c2|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poStamp="5">
+    <org.eventb.core.poPredicateSet name="ALLHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_c2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_c2|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poStamp="7">
         <org.eventb.core.poPredicate name="PRD0" 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="PRD1" 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.poPredicateSet>