Skip to content
Snippets Groups Projects
Commit 9830ac4e authored by Guzman Llambias's avatar Guzman Llambias
Browse files

Changes generated by reviewers comments

parent e522ab0a
No related branches found
No related tags found
No related merge requests found
...@@ -64,9 +64,9 @@ ...@@ -64,9 +64,9 @@
<org.eventb.core.scAction name=")" org.eventb.core.assignment="subscriptions ≔ ∅ ⦂ ℙ(GATEWAYS×CROSS_CHAIN_SMART_CONTRACTS)" org.eventb.core.label="act3" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#'|org.eventb.core.action#_zpBzkcQ4Ee609fto5wotHA"/> <org.eventb.core.scAction name=")" org.eventb.core.assignment="subscriptions ≔ ∅ ⦂ ℙ(GATEWAYS×CROSS_CHAIN_SMART_CONTRACTS)" org.eventb.core.label="act3" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#'|org.eventb.core.action#_zpBzkcQ4Ee609fto5wotHA"/>
<org.eventb.core.scAction name="*" org.eventb.core.assignment="gateway_pending_events ≔ ∅ ⦂ ℙ(GATEWAYS×TARGET_TRANSACTIONS)" org.eventb.core.label="act4" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#'|org.eventb.core.action#_zpBzksQ4Ee609fto5wotHA"/> <org.eventb.core.scAction name="*" org.eventb.core.assignment="gateway_pending_events ≔ ∅ ⦂ ℙ(GATEWAYS×TARGET_TRANSACTIONS)" org.eventb.core.label="act4" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#'|org.eventb.core.action#_zpBzksQ4Ee609fto5wotHA"/>
<org.eventb.core.scAction name="+" org.eventb.core.assignment="received_target_transactions ≔ ∅ ⦂ ℙ(CROSS_CHAIN_SMART_CONTRACTS×TARGET_TRANSACTIONS)" org.eventb.core.label="act6" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#'|org.eventb.core.action#_zpCaoMQ4Ee609fto5wotHA"/> <org.eventb.core.scAction name="+" org.eventb.core.assignment="received_target_transactions ≔ ∅ ⦂ ℙ(CROSS_CHAIN_SMART_CONTRACTS×TARGET_TRANSACTIONS)" org.eventb.core.label="act6" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#'|org.eventb.core.action#_zpCaoMQ4Ee609fto5wotHA"/>
<org.eventb.core.scAction name="," org.eventb.core.assignment="authenticated_users ≔ ∅ ⦂ ℙ(USERS)" org.eventb.core.label="act11" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh|org.eventb.core.action#_jV8FAMEWEe6yC4BToIaAqA"/> <org.eventb.core.scAction name="," org.eventb.core.assignment="authenticated_users ≔ ∅ ⦂ ℙ(USERS)" org.eventb.core.label="act11" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_CJbpkPRrEe60CqkwWvstGA|org.eventb.core.action#_jV8FAMEWEe6yC4BToIaAqA"/>
<org.eventb.core.scAction name="-" org.eventb.core.assignment="authenticated_transactions ≔ ∅ ⦂ ℙ(CROSS_CHAIN_SMART_CONTRACTS×TARGET_TRANSACTIONS×USERS)" org.eventb.core.label="act12" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh|org.eventb.core.action#_jV8FAcEWEe6yC4BToIaAqA"/> <org.eventb.core.scAction name="-" org.eventb.core.assignment="authenticated_transactions ≔ ∅ ⦂ ℙ(CROSS_CHAIN_SMART_CONTRACTS×TARGET_TRANSACTIONS×USERS)" org.eventb.core.label="act12" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_CJbpkPRrEe60CqkwWvstGA|org.eventb.core.action#_jV8FAcEWEe6yC4BToIaAqA"/>
<org.eventb.core.scAction name="." org.eventb.core.assignment="grants ≔ ∅ ⦂ ℙ(USERS×PERMISSIONS)" org.eventb.core.label="act14" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh|org.eventb.core.action#_0oC5cMErEe6yC4BToIaAqA"/> <org.eventb.core.scAction name="." org.eventb.core.assignment="grants ≔ ∅ ⦂ ℙ(USERS×PERMISSIONS)" org.eventb.core.label="act14" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_CJbpkPRrEe60CqkwWvstGA|org.eventb.core.action#_0oC5cMErEe6yC4BToIaAqA"/>
<org.eventb.core.scAction name="/" org.eventb.core.assignment="subscribed ≔ 0" org.eventb.core.label="act31" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh|org.eventb.core.action#_FVN5wMHOEe609fto5wotHA"/> <org.eventb.core.scAction name="/" org.eventb.core.assignment="subscribed ≔ 0" org.eventb.core.label="act31" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh|org.eventb.core.action#_FVN5wMHOEe609fto5wotHA"/>
<org.eventb.core.scAction name="0" org.eventb.core.assignment="initiated ≔ 0" org.eventb.core.label="act32" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh|org.eventb.core.action#_FVN5wcHOEe609fto5wotHA"/> <org.eventb.core.scAction name="0" org.eventb.core.assignment="initiated ≔ 0" org.eventb.core.label="act32" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh|org.eventb.core.action#_FVN5wcHOEe609fto5wotHA"/>
<org.eventb.core.scAction name="1" org.eventb.core.assignment="emitted ≔ 0" org.eventb.core.label="act33" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh|org.eventb.core.action#_FVOg0MHOEe609fto5wotHA"/> <org.eventb.core.scAction name="1" org.eventb.core.assignment="emitted ≔ 0" org.eventb.core.label="act33" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh|org.eventb.core.action#_FVOg0MHOEe609fto5wotHA"/>
......
<?xml version="1.0" encoding="UTF-8" standalone="no"?> <?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.poFile org.eventb.core.poStamp="11"> <org.eventb.core.poFile org.eventb.core.poStamp="12">
<org.eventb.core.poPredicateSet name="CTXHYP" org.eventb.core.poStamp="11"> <org.eventb.core.poPredicateSet name="CTXHYP" org.eventb.core.poStamp="11">
<org.eventb.core.poIdentifier name="TARGET_TRANSACTIONS" org.eventb.core.type="ℙ(TARGET_TRANSACTIONS)"/> <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="GATEWAYS" org.eventb.core.type="ℙ(GATEWAYS)"/>
...@@ -47,64 +47,64 @@ ...@@ -47,64 +47,64 @@
<org.eventb.core.poPredicate name="received_target_transaction|" org.eventb.core.predicate="grants∈authenticated_users ↔ PERMISSIONS" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.invariant#_OTstIMHNEe609fto5wotHA"/> <org.eventb.core.poPredicate name="received_target_transaction|" org.eventb.core.predicate="grants∈authenticated_users ↔ PERMISSIONS" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.invariant#_OTstIMHNEe609fto5wotHA"/>
<org.eventb.core.poPredicate name="received_target_transaction}" org.eventb.core.predicate="∀u⦂USERS·u∈authenticated_transactions[received_target_transactions]⇒u ↦ write∈grants" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.invariant#_jCLrMcHJEe6yC4BToIaAqA"/> <org.eventb.core.poPredicate name="received_target_transaction}" org.eventb.core.predicate="∀u⦂USERS·u∈authenticated_transactions[received_target_transactions]⇒u ↦ write∈grants" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.invariant#_jCLrMcHJEe6yC4BToIaAqA"/>
</org.eventb.core.poPredicateSet> </org.eventb.core.poPredicateSet>
<org.eventb.core.poSequent name="INITIALISATION/inv11/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant establishment" org.eventb.core.poStamp="11"> <org.eventb.core.poSequent name="INITIALISATION/inv11/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant establishment" org.eventb.core.poStamp="12">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#EVTALLHYPreceived_target_transactiont"/> <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#EVTALLHYPreceived_target_transactiont"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="0∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_DmAl8MHOEe609fto5wotHA"/> <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="0∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_DmAl8MHOEe609fto5wotHA"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh"/> <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_CJbpkPRrEe60CqkwWvstGA"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh"/> <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh"/>
<org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_DmAl8MHOEe609fto5wotHA"/> <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_DmAl8MHOEe609fto5wotHA"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poSequent#INITIALISATION\/inv11\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poSequent#INITIALISATION\/inv11\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD0"/> <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD0"/>
</org.eventb.core.poSequent> </org.eventb.core.poSequent>
<org.eventb.core.poSequent name="INITIALISATION/inv12/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant establishment" org.eventb.core.poStamp="11"> <org.eventb.core.poSequent name="INITIALISATION/inv12/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant establishment" org.eventb.core.poStamp="12">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#EVTALLHYPreceived_target_transactiont"/> <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#EVTALLHYPreceived_target_transactiont"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="0∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_DmB0EMHOEe609fto5wotHA"/> <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="0∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_DmB0EMHOEe609fto5wotHA"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh"/> <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_CJbpkPRrEe60CqkwWvstGA"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh"/> <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh"/>
<org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_DmB0EMHOEe609fto5wotHA"/> <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_DmB0EMHOEe609fto5wotHA"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poSequent#INITIALISATION\/inv12\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poSequent#INITIALISATION\/inv12\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD1"/> <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD1"/>
</org.eventb.core.poSequent> </org.eventb.core.poSequent>
<org.eventb.core.poSequent name="INITIALISATION/inv13/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant establishment" org.eventb.core.poStamp="11"> <org.eventb.core.poSequent name="INITIALISATION/inv13/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant establishment" org.eventb.core.poStamp="12">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#EVTALLHYPreceived_target_transactiont"/> <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#EVTALLHYPreceived_target_transactiont"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="0∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_DmCbIMHOEe609fto5wotHA"/> <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="0∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_DmCbIMHOEe609fto5wotHA"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh"/> <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_CJbpkPRrEe60CqkwWvstGA"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh"/> <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh"/>
<org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_DmCbIMHOEe609fto5wotHA"/> <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_DmCbIMHOEe609fto5wotHA"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poSequent#INITIALISATION\/inv13\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poSequent#INITIALISATION\/inv13\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD2"/> <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD2"/>
</org.eventb.core.poSequent> </org.eventb.core.poSequent>
<org.eventb.core.poSequent name="INITIALISATION/inv14/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant establishment" org.eventb.core.poStamp="11"> <org.eventb.core.poSequent name="INITIALISATION/inv14/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant establishment" org.eventb.core.poStamp="12">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#EVTALLHYPreceived_target_transactiont"/> <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#EVTALLHYPreceived_target_transactiont"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="0∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_DmDCMMHOEe609fto5wotHA"/> <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="0∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_DmDCMMHOEe609fto5wotHA"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh"/> <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_CJbpkPRrEe60CqkwWvstGA"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh"/> <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh"/>
<org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_DmDCMMHOEe609fto5wotHA"/> <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_DmDCMMHOEe609fto5wotHA"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poSequent#INITIALISATION\/inv14\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poSequent#INITIALISATION\/inv14\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD3"/> <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD3"/>
</org.eventb.core.poSequent> </org.eventb.core.poSequent>
<org.eventb.core.poSequent name="INITIALISATION/inv15/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant establishment" org.eventb.core.poStamp="11"> <org.eventb.core.poSequent name="INITIALISATION/inv15/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant establishment" org.eventb.core.poStamp="12">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#EVTALLHYPreceived_target_transactiont"/> <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#EVTALLHYPreceived_target_transactiont"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="0∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_DmDpQMHOEe609fto5wotHA"/> <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="0∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_DmDpQMHOEe609fto5wotHA"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh"/> <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_CJbpkPRrEe60CqkwWvstGA"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh"/> <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh"/>
<org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_DmDpQMHOEe609fto5wotHA"/> <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_DmDpQMHOEe609fto5wotHA"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poSequent#INITIALISATION\/inv15\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poSequent#INITIALISATION\/inv15\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD4"/> <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD4"/>
</org.eventb.core.poSequent> </org.eventb.core.poSequent>
<org.eventb.core.poSequent name="INITIALISATION/inv16/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant establishment" org.eventb.core.poStamp="11"> <org.eventb.core.poSequent name="INITIALISATION/inv16/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant establishment" org.eventb.core.poStamp="12">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#EVTALLHYPreceived_target_transactiont"/> <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#EVTALLHYPreceived_target_transactiont"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="0∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_DmEQUMHOEe609fto5wotHA"/> <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="0∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_DmEQUMHOEe609fto5wotHA"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh"/> <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_CJbpkPRrEe60CqkwWvstGA"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh"/> <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh"/>
<org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_DmEQUMHOEe609fto5wotHA"/> <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_DmEQUMHOEe609fto5wotHA"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poSequent#INITIALISATION\/inv16\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poSequent#INITIALISATION\/inv16\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD5"/> <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD5"/>
</org.eventb.core.poSequent> </org.eventb.core.poSequent>
<org.eventb.core.poSequent name="INITIALISATION/inv17/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant establishment" org.eventb.core.poStamp="11"> <org.eventb.core.poSequent name="INITIALISATION/inv17/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant establishment" org.eventb.core.poStamp="12">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#EVTALLHYPreceived_target_transactiont"/> <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#EVTALLHYPreceived_target_transactiont"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="0∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_2MNd0MHOEe609fto5wotHA"/> <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="0∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_2MNd0MHOEe609fto5wotHA"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh"/> <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_CJbpkPRrEe60CqkwWvstGA"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh"/> <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh"/>
<org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_2MNd0MHOEe609fto5wotHA"/> <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_2MNd0MHOEe609fto5wotHA"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poSequent#INITIALISATION\/inv17\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poSequent#INITIALISATION\/inv17\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
......
<?xml version="1.0" encoding="UTF-8" standalone="no"?> <?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.psFile> <org.eventb.core.psFile>
<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/inv11/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="12" 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/inv12/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="12" 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/inv13/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="12" 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/inv14/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="12" 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/inv15/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="12" 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/inv16/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="12" 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="INITIALISATION/inv17/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="12" 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="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/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="INITIATE_CC_TX_IN_ETHEREUM/inv15/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="11" org.eventb.core.psManual="false"/>
......
<?xml version="1.0" encoding="UTF-8" standalone="no"?> <?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="_c2YQRcQ6Ee609fto5wotHA" org.eventb.texttools.text_lastmodified="1707146581829" org.eventb.texttools.text_representation="context CCTx_Ethereum_Fabric_c2 extends CCTx_Abstract_DLT_c1&#10;&#10;sets PERMISSIONS USERS&#10;&#10;constants read write gateway_user&#10;&#10;axioms&#10; @axm11 partition(PERMISSIONS, {read}, {write}) // Two only types of permissions exist: read and write&#10; @axm12 gateway_user ∈ USERS // The gateway has an Hyperledger Fabric user&#10;end" version="3"> <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="_mAbXh_RqEe60CqkwWvstGA" org.eventb.texttools.text_lastmodified="1712444914938" org.eventb.texttools.text_representation="context CCTx_Ethereum_Fabric_c2 extends CCTx_Abstract_DLT_c1&#10;&#10;sets PERMISSIONS USERS&#10;&#10;constants read write gateway_user&#10;&#10;axioms&#10; @axm11 partition(PERMISSIONS, {read}, {write}) // Only two types of permissions exist: read and write (REQ1)&#10; @axm12 gateway_user ∈ USERS // The gateway has a Fabric user&#10;end" version="3">
<org.eventb.core.extendsContext name="'" org.eventb.core.target="CCTx_Abstract_DLT_c1"/> <org.eventb.core.extendsContext name="'" org.eventb.core.target="CCTx_Abstract_DLT_c1"/>
<org.eventb.core.axiom name="_c2chsMQ6Ee609fto5wotHA" org.eventb.core.comment="Two only types of permissions exist: read and write" org.eventb.core.generated="false" org.eventb.core.label="axm11" org.eventb.core.predicate="partition(PERMISSIONS, {read}, {write})" org.eventb.emf.persistence.emf_id="_c2YQQ8Q6Ee609fto5wotHA"/> <org.eventb.core.axiom name="_c2chsMQ6Ee609fto5wotHA" org.eventb.core.comment="Only two types of permissions exist: read and write (REQ1)" org.eventb.core.generated="false" org.eventb.core.label="axm11" org.eventb.core.predicate="partition(PERMISSIONS, {read}, {write})" org.eventb.emf.persistence.emf_id="_mAbXhfRqEe60CqkwWvstGA"/>
<org.eventb.core.axiom name="_c2dIwMQ6Ee609fto5wotHA" org.eventb.core.comment="The gateway has an Hyperledger Fabric user" org.eventb.core.generated="false" org.eventb.core.label="axm12" org.eventb.core.predicate="gateway_user ∈ USERS" org.eventb.emf.persistence.emf_id="_c2YQRMQ6Ee609fto5wotHA"/> <org.eventb.core.axiom name="_c2dIwMQ6Ee609fto5wotHA" org.eventb.core.comment="The gateway has a Fabric user" org.eventb.core.generated="false" org.eventb.core.label="axm12" org.eventb.core.predicate="gateway_user ∈ USERS" org.eventb.emf.persistence.emf_id="_mAbXhvRqEe60CqkwWvstGA"/>
<org.eventb.core.constant name="_olcsor7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="read" org.eventb.emf.persistence.emf_id="_c2YQQMQ6Ee609fto5wotHA"/> <org.eventb.core.constant name="_olcsor7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="read" org.eventb.emf.persistence.emf_id="_mAbXgvRqEe60CqkwWvstGA"/>
<org.eventb.core.constant name="_olcso77uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="write" org.eventb.emf.persistence.emf_id="_c2YQQcQ6Ee609fto5wotHA"/> <org.eventb.core.constant name="_olcso77uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="write" org.eventb.emf.persistence.emf_id="_mAbXg_RqEe60CqkwWvstGA"/>
<org.eventb.core.constant name="_olcspL7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="gateway_user" org.eventb.emf.persistence.emf_id="_c2YQQsQ6Ee609fto5wotHA"/> <org.eventb.core.constant name="_olcspL7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="gateway_user" org.eventb.emf.persistence.emf_id="_mAbXhPRqEe60CqkwWvstGA"/>
<org.eventb.core.carrierSet name="_olcspb7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="PERMISSIONS" org.eventb.emf.persistence.emf_id="_c2XpMMQ6Ee609fto5wotHA"/> <org.eventb.core.carrierSet name="_olcspb7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="PERMISSIONS" org.eventb.emf.persistence.emf_id="_mAbXgPRqEe60CqkwWvstGA"/>
<org.eventb.core.carrierSet name="_olcspr7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="USERS" org.eventb.emf.persistence.emf_id="_c2XpMcQ6Ee609fto5wotHA"/> <org.eventb.core.carrierSet name="_olcspr7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="USERS" org.eventb.emf.persistence.emf_id="_mAbXgfRqEe60CqkwWvstGA"/>
</org.eventb.core.contextFile> </org.eventb.core.contextFile>
...@@ -43,16 +43,16 @@ ...@@ -43,16 +43,16 @@
<org.eventb.core.scVariable name="grants" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.variable#_2RlqIMErEe6yC4BToIaAqA" org.eventb.core.type="ℙ(USERS×PERMISSIONS)"/> <org.eventb.core.scVariable name="grants" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.variable#_2RlqIMErEe6yC4BToIaAqA" org.eventb.core.type="ℙ(USERS×PERMISSIONS)"/>
<org.eventb.core.scVariable name="received_source_transactions" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.variable#_OjhzwPRgEe60CqkwWvstGA" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×SOURCE_TRANSACTIONS)"/> <org.eventb.core.scVariable name="received_source_transactions" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.variable#_OjhzwPRgEe60CqkwWvstGA" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×SOURCE_TRANSACTIONS)"/>
<org.eventb.core.scVariable name="authenticated_users" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.variable#_1toq4L7uEe6laZimEYihUg" org.eventb.core.type="ℙ(USERS)"/> <org.eventb.core.scVariable name="authenticated_users" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.variable#_1toq4L7uEe6laZimEYihUg" org.eventb.core.type="ℙ(USERS)"/>
<org.eventb.core.scEvent name="received_target_transactiont" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="INITIALISATION" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh"> <org.eventb.core.scEvent name="received_target_transactiont" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="INITIALISATION" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_CJbpkPRrEe60CqkwWvstGA">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/gateway-event-b/CCTx_Abstract_DLT_m1.bcm|org.eventb.core.scMachineFile#CCTx_Abstract_DLT_m1|org.eventb.core.scEvent#received_target_transactiont" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh"/> <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/gateway-event-b/CCTx_Abstract_DLT_m1.bcm|org.eventb.core.scMachineFile#CCTx_Abstract_DLT_m1|org.eventb.core.scEvent#received_target_transactiont" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_CJbpkPRrEe60CqkwWvstGA"/>
<org.eventb.core.scAction name="'" org.eventb.core.assignment="received_source_transactions ≔ ∅ ⦂ ℙ(CROSS_CHAIN_SMART_CONTRACTS×SOURCE_TRANSACTIONS)" org.eventb.core.label="act1" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#'|org.eventb.core.action#_zpBMgMQ4Ee609fto5wotHA"/> <org.eventb.core.scAction name="'" org.eventb.core.assignment="received_source_transactions ≔ ∅ ⦂ ℙ(CROSS_CHAIN_SMART_CONTRACTS×SOURCE_TRANSACTIONS)" org.eventb.core.label="act1" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#'|org.eventb.core.action#_zpBMgMQ4Ee609fto5wotHA"/>
<org.eventb.core.scAction name="(" org.eventb.core.assignment="emitted_events ≔ ∅ ⦂ ℙ(CROSS_CHAIN_SMART_CONTRACTS×SMART_CONTRACT_EVENTS)" org.eventb.core.label="act2" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#'|org.eventb.core.action#_zpBzkMQ4Ee609fto5wotHA"/> <org.eventb.core.scAction name="(" org.eventb.core.assignment="emitted_events ≔ ∅ ⦂ ℙ(CROSS_CHAIN_SMART_CONTRACTS×SMART_CONTRACT_EVENTS)" org.eventb.core.label="act2" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#'|org.eventb.core.action#_zpBzkMQ4Ee609fto5wotHA"/>
<org.eventb.core.scAction name=")" org.eventb.core.assignment="subscriptions ≔ ∅ ⦂ ℙ(GATEWAYS×CROSS_CHAIN_SMART_CONTRACTS)" org.eventb.core.label="act3" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#'|org.eventb.core.action#_zpBzkcQ4Ee609fto5wotHA"/> <org.eventb.core.scAction name=")" org.eventb.core.assignment="subscriptions ≔ ∅ ⦂ ℙ(GATEWAYS×CROSS_CHAIN_SMART_CONTRACTS)" org.eventb.core.label="act3" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#'|org.eventb.core.action#_zpBzkcQ4Ee609fto5wotHA"/>
<org.eventb.core.scAction name="*" org.eventb.core.assignment="gateway_pending_events ≔ ∅ ⦂ ℙ(GATEWAYS×TARGET_TRANSACTIONS)" org.eventb.core.label="act4" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#'|org.eventb.core.action#_zpBzksQ4Ee609fto5wotHA"/> <org.eventb.core.scAction name="*" org.eventb.core.assignment="gateway_pending_events ≔ ∅ ⦂ ℙ(GATEWAYS×TARGET_TRANSACTIONS)" org.eventb.core.label="act4" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#'|org.eventb.core.action#_zpBzksQ4Ee609fto5wotHA"/>
<org.eventb.core.scAction name="+" org.eventb.core.assignment="received_target_transactions ≔ ∅ ⦂ ℙ(CROSS_CHAIN_SMART_CONTRACTS×TARGET_TRANSACTIONS)" org.eventb.core.label="act6" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#'|org.eventb.core.action#_zpCaoMQ4Ee609fto5wotHA"/> <org.eventb.core.scAction name="+" org.eventb.core.assignment="received_target_transactions ≔ ∅ ⦂ ℙ(CROSS_CHAIN_SMART_CONTRACTS×TARGET_TRANSACTIONS)" org.eventb.core.label="act6" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#'|org.eventb.core.action#_zpCaoMQ4Ee609fto5wotHA"/>
<org.eventb.core.scAction name="," org.eventb.core.assignment="authenticated_users ≔ ∅ ⦂ ℙ(USERS)" org.eventb.core.label="act11" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh|org.eventb.core.action#_jV8FAMEWEe6yC4BToIaAqA"/> <org.eventb.core.scAction name="," org.eventb.core.assignment="authenticated_users ≔ ∅ ⦂ ℙ(USERS)" org.eventb.core.label="act11" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_CJbpkPRrEe60CqkwWvstGA|org.eventb.core.action#_jV8FAMEWEe6yC4BToIaAqA"/>
<org.eventb.core.scAction name="-" org.eventb.core.assignment="authenticated_transactions ≔ ∅ ⦂ ℙ(CROSS_CHAIN_SMART_CONTRACTS×TARGET_TRANSACTIONS×USERS)" org.eventb.core.label="act12" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh|org.eventb.core.action#_jV8FAcEWEe6yC4BToIaAqA"/> <org.eventb.core.scAction name="-" org.eventb.core.assignment="authenticated_transactions ≔ ∅ ⦂ ℙ(CROSS_CHAIN_SMART_CONTRACTS×TARGET_TRANSACTIONS×USERS)" org.eventb.core.label="act12" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_CJbpkPRrEe60CqkwWvstGA|org.eventb.core.action#_jV8FAcEWEe6yC4BToIaAqA"/>
<org.eventb.core.scAction name="." org.eventb.core.assignment="grants ≔ ∅ ⦂ ℙ(USERS×PERMISSIONS)" org.eventb.core.label="act14" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh|org.eventb.core.action#_0oC5cMErEe6yC4BToIaAqA"/> <org.eventb.core.scAction name="." org.eventb.core.assignment="grants ≔ ∅ ⦂ ℙ(USERS×PERMISSIONS)" org.eventb.core.label="act14" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_CJbpkPRrEe60CqkwWvstGA|org.eventb.core.action#_0oC5cMErEe6yC4BToIaAqA"/>
</org.eventb.core.scEvent> </org.eventb.core.scEvent>
<org.eventb.core.scEvent name="received_target_transactionu" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="SUBSCRIBE_SMART_CONTRACT_EVENTS_IN_ETHEREUM" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_1tlnkr7uEe6laZimEYihUg"> <org.eventb.core.scEvent name="received_target_transactionu" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="SUBSCRIBE_SMART_CONTRACT_EVENTS_IN_ETHEREUM" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_1tlnkr7uEe6laZimEYihUg">
<org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/gateway-event-b/CCTx_Abstract_DLT_m1.bcm|org.eventb.core.scMachineFile#CCTx_Abstract_DLT_m1|org.eventb.core.scEvent#received_target_transactionu" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_1tlnkr7uEe6laZimEYihUg|org.eventb.core.refinesEvent#_1tlnk77uEe6laZimEYihUg"/> <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/gateway-event-b/CCTx_Abstract_DLT_m1.bcm|org.eventb.core.scMachineFile#CCTx_Abstract_DLT_m1|org.eventb.core.scEvent#received_target_transactionu" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_1tlnkr7uEe6laZimEYihUg|org.eventb.core.refinesEvent#_1tlnk77uEe6laZimEYihUg"/>
......
<?xml version="1.0" encoding="UTF-8" standalone="no"?> <?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.poFile org.eventb.core.poStamp="39"> <org.eventb.core.poFile org.eventb.core.poStamp="40">
<org.eventb.core.poPredicateSet name="CTXHYP" org.eventb.core.poStamp="39"> <org.eventb.core.poPredicateSet name="CTXHYP" org.eventb.core.poStamp="39">
<org.eventb.core.poIdentifier name="TARGET_TRANSACTIONS" org.eventb.core.type="ℙ(TARGET_TRANSACTIONS)"/> <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="GATEWAYS" org.eventb.core.type="ℙ(GATEWAYS)"/>
...@@ -35,38 +35,38 @@ ...@@ -35,38 +35,38 @@
<org.eventb.core.poPredicate name="received_target_transactionw" 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="received_target_transactionw" 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="received_target_transactionx" 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"/> <org.eventb.core.poPredicate name="received_target_transactionx" 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"/>
</org.eventb.core.poPredicateSet> </org.eventb.core.poPredicateSet>
<org.eventb.core.poSequent name="INITIALISATION/inv12/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant establishment" org.eventb.core.poStamp="39"> <org.eventb.core.poSequent name="INITIALISATION/inv12/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant establishment" org.eventb.core.poStamp="40">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#EVTALLHYPreceived_target_transactiont"/> <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#EVTALLHYPreceived_target_transactiont"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="(∅ ⦂ ℙ(CROSS_CHAIN_SMART_CONTRACTS×TARGET_TRANSACTIONS×USERS))∈(∅ ⦂ ℙ(CROSS_CHAIN_SMART_CONTRACTS×TARGET_TRANSACTIONS)) → (∅ ⦂ ℙ(USERS))" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.invariant#_jV9TI8EWEe6yC4BToIaAqA"/> <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="(∅ ⦂ ℙ(CROSS_CHAIN_SMART_CONTRACTS×TARGET_TRANSACTIONS×USERS))∈(∅ ⦂ ℙ(CROSS_CHAIN_SMART_CONTRACTS×TARGET_TRANSACTIONS)) → (∅ ⦂ ℙ(USERS))" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.invariant#_jV9TI8EWEe6yC4BToIaAqA"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#'"/> <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#'"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh"/> <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_CJbpkPRrEe60CqkwWvstGA"/>
<org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.invariant#_jV9TI8EWEe6yC4BToIaAqA"/> <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.invariant#_jV9TI8EWEe6yC4BToIaAqA"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poSequent#INITIALISATION\/inv12\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poSequent#INITIALISATION\/inv12\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD1"/> <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD1"/>
</org.eventb.core.poSequent> </org.eventb.core.poSequent>
<org.eventb.core.poSequent name="INITIALISATION/inv13/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant establishment" org.eventb.core.poStamp="39"> <org.eventb.core.poSequent name="INITIALISATION/inv13/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant establishment" org.eventb.core.poStamp="40">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#EVTALLHYPreceived_target_transactiont"/> <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#EVTALLHYPreceived_target_transactiont"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀tx⦂CROSS_CHAIN_SMART_CONTRACTS×TARGET_TRANSACTIONS·tx∈(∅ ⦂ ℙ(CROSS_CHAIN_SMART_CONTRACTS×TARGET_TRANSACTIONS))⇒(∃u⦂USERS·u∈(∅ ⦂ ℙ(USERS))∧tx ↦ u∈(∅ ⦂ ℙ(CROSS_CHAIN_SMART_CONTRACTS×TARGET_TRANSACTIONS×USERS)))" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.invariant#_jV9TJMEWEe6yC4BToIaAqA"/> <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀tx⦂CROSS_CHAIN_SMART_CONTRACTS×TARGET_TRANSACTIONS·tx∈(∅ ⦂ ℙ(CROSS_CHAIN_SMART_CONTRACTS×TARGET_TRANSACTIONS))⇒(∃u⦂USERS·u∈(∅ ⦂ ℙ(USERS))∧tx ↦ u∈(∅ ⦂ ℙ(CROSS_CHAIN_SMART_CONTRACTS×TARGET_TRANSACTIONS×USERS)))" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.invariant#_jV9TJMEWEe6yC4BToIaAqA"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#'"/> <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#'"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh"/> <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_CJbpkPRrEe60CqkwWvstGA"/>
<org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.invariant#_jV9TJMEWEe6yC4BToIaAqA"/> <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.invariant#_jV9TJMEWEe6yC4BToIaAqA"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poSequent#INITIALISATION\/inv13\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poSequent#INITIALISATION\/inv13\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD2"/> <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD2"/>
</org.eventb.core.poSequent> </org.eventb.core.poSequent>
<org.eventb.core.poSequent name="INITIALISATION/inv14/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant establishment" org.eventb.core.poStamp="39"> <org.eventb.core.poSequent name="INITIALISATION/inv14/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant establishment" org.eventb.core.poStamp="40">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#EVTALLHYPreceived_target_transactiont"/> <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#EVTALLHYPreceived_target_transactiont"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="(∅ ⦂ ℙ(USERS×PERMISSIONS))∈(∅ ⦂ ℙ(USERS)) ↔ PERMISSIONS" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.invariant#_OTstIMHNEe609fto5wotHA"/> <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="(∅ ⦂ ℙ(USERS×PERMISSIONS))∈(∅ ⦂ ℙ(USERS)) ↔ PERMISSIONS" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.invariant#_OTstIMHNEe609fto5wotHA"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#'"/> <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#'"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh"/> <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_CJbpkPRrEe60CqkwWvstGA"/>
<org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.invariant#_OTstIMHNEe609fto5wotHA"/> <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.invariant#_OTstIMHNEe609fto5wotHA"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poSequent#INITIALISATION\/inv14\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poSequent#INITIALISATION\/inv14\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD3"/> <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD3"/>
</org.eventb.core.poSequent> </org.eventb.core.poSequent>
<org.eventb.core.poSequent name="INITIALISATION/inv15/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant establishment" org.eventb.core.poStamp="39"> <org.eventb.core.poSequent name="INITIALISATION/inv15/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant establishment" org.eventb.core.poStamp="40">
<org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#EVTALLHYPreceived_target_transactiont"/> <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#EVTALLHYPreceived_target_transactiont"/>
<org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀u⦂USERS·u∈(∅ ⦂ ℙ(CROSS_CHAIN_SMART_CONTRACTS×TARGET_TRANSACTIONS×USERS))[∅ ⦂ ℙ(CROSS_CHAIN_SMART_CONTRACTS×TARGET_TRANSACTIONS)]⇒u ↦ write∈(∅ ⦂ ℙ(USERS×PERMISSIONS))" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.invariant#_jCLrMcHJEe6yC4BToIaAqA"/> <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀u⦂USERS·u∈(∅ ⦂ ℙ(CROSS_CHAIN_SMART_CONTRACTS×TARGET_TRANSACTIONS×USERS))[∅ ⦂ ℙ(CROSS_CHAIN_SMART_CONTRACTS×TARGET_TRANSACTIONS)]⇒u ↦ write∈(∅ ⦂ ℙ(USERS×PERMISSIONS))" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.invariant#_jCLrMcHJEe6yC4BToIaAqA"/>
<org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#'"/> <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#'"/>
<org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh"/> <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_CJbpkPRrEe60CqkwWvstGA"/>
<org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.invariant#_jCLrMcHJEe6yC4BToIaAqA"/> <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.invariant#_jCLrMcHJEe6yC4BToIaAqA"/>
<org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poSequent#INITIALISATION\/inv15\/INV|org.eventb.core.poPredicateSet#SEQHYP"/> <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poSequent#INITIALISATION\/inv15\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
<org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD4"/> <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD4"/>
......
<?xml version="1.0" encoding="UTF-8" standalone="no"?> <?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.psFile> <org.eventb.core.psFile>
<org.eventb.core.psStatus name="INITIALISATION/inv12/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="39" org.eventb.core.psManual="false"/> <org.eventb.core.psStatus name="INITIALISATION/inv12/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="40" org.eventb.core.psManual="false"/>
<org.eventb.core.psStatus name="INITIALISATION/inv13/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="39" org.eventb.core.psManual="false"/> <org.eventb.core.psStatus name="INITIALISATION/inv13/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="40" org.eventb.core.psManual="false"/>
<org.eventb.core.psStatus name="INITIALISATION/inv14/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="39" org.eventb.core.psManual="false"/> <org.eventb.core.psStatus name="INITIALISATION/inv14/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="40" org.eventb.core.psManual="false"/>
<org.eventb.core.psStatus name="INITIALISATION/inv15/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="39" org.eventb.core.psManual="false"/> <org.eventb.core.psStatus name="INITIALISATION/inv15/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="40" org.eventb.core.psManual="false"/>
<org.eventb.core.psStatus name="SUBMIT_TX_TO_FABRIC/inv12/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="39" org.eventb.core.psManual="false"/> <org.eventb.core.psStatus name="SUBMIT_TX_TO_FABRIC/inv12/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="39" org.eventb.core.psManual="false"/>
<org.eventb.core.psStatus name="SUBMIT_TX_TO_FABRIC/inv13/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="39" org.eventb.core.psManual="false"/> <org.eventb.core.psStatus name="SUBMIT_TX_TO_FABRIC/inv13/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="39" 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="39" 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="39" org.eventb.core.psManual="false"/>
......
<?xml version="1.0" encoding="UTF-8" standalone="no"?> <?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.machineFile org.eventb.core.configuration="org.eventb.core.fwd" org.eventb.core.generated="false" org.eventb.emf.persistence.emf_id="_mFWC-vRhEe60CqkwWvstGA" org.eventb.texttools.text_lastmodified="1712441049982" org.eventb.texttools.text_representation="machine CCTx_Ethereum_Fabric_m2 refines CCTx_Abstract_DLT_m1 sees CCTx_Ethereum_Fabric_c2&#10;&#10;variables received_source_transactions emitted_events subscriptions gateway_pending_events received_target_transactions authenticated_users authenticated_transactions grants&#10;&#10;invariants&#10; @inv11 authenticated_users ⊆ USERS // Authenticated users are a subset of all the possible users&#10; @inv12 authenticated_transactions ∈ received_target_transactions → authenticated_users // Authenticated transactions are received transactions submitted by an authenticated user&#10; @inv13 ∀ tx · tx ∈ received_target_transactions ⇒ (∃ u · u ∈&#10; authenticated_users ∧ tx ↦ u ∈ authenticated_transactions) //Every submitted transaction to Fabric must be authenticated (REQ4)&#10; @inv14 grants ∈ authenticated_users ↔ PERMISSIONS // Users with read or write permissions&#10; @inv15 ∀ u · u ∈ authenticated_transactions[received_target_transactions] ⇒ u ↦ write ∈ grants //Authenticated users that submitted a transaction must have write permissions (REQ5)&#10;&#10;events&#10; event INITIALISATION extends INITIALISATION&#10; then&#10; @act11 authenticated_users ≔ ∅&#10; @act12 authenticated_transactions ≔ ∅&#10; @act14 grants ≔ ∅&#10; end&#10;&#10; event SUBSCRIBE_SMART_CONTRACT_EVENTS_IN_ETHEREUM extends SUBSCRIBE_SMART_CONTRACT_EVENTS&#10; end&#10;&#10; event INITIATE_CC_TX_IN_ETHEREUM extends INITIATE_CC_TX&#10; end&#10;&#10; event EMIT_EVENT_IN_ETHEREUM extends EMIT_EVENT&#10; end&#10;&#10; event LISTEN_EVENT_IN_ETHEREUM extends LISTEN_EVENT&#10; end&#10;&#10; event SUBMIT_TX_TO_FABRIC extends SUBMIT_TX&#10; any user&#10; where&#10; @grd11 user ∈ authenticated_users // Only allow authenticated users (REQ6)&#10; @grd12 user ↦ write ∈ grants // Only allow authorized users (REQ7)&#10; then&#10; @act11 authenticated_transactions(target_smart_contract ↦ transaction) ≔ user // Audit user that submitted a transaction to a smart contract (REQ4)&#10; end&#10;&#10; event CREATE_GATEWAY_USER&#10;&#9; when&#10;&#9; &#9;@grd1 gateway_user ∉ authenticated_users&#10;&#9; then&#10;&#9; &#9;@act1 authenticated_users ≔ authenticated_users ∪ {gateway_user} // Create credentials for a user (e.g. gateway) to authenticate them (REQ2)&#10; end&#10;&#10; event GRANT_PERMISSION&#10; &#9;any permission user&#10; &#9;where&#10; &#9;&#9;@grd1 permission ∈ PERMISSIONS&#10; &#9;&#9;@grd2 user ∈ authenticated_users&#10; &#9;&#9;@grd3 user ↦ permission ∉ grants&#10; &#9;then&#10; &#9;&#9;@act1 grants ≔ grants ∪ {user ↦ permission} // Grant permissions (e.g. write) to users (e.g. gateway) in Fabric (REQ3)&#10; end&#10;end&#10;" version="5"> <org.eventb.core.machineFile org.eventb.core.configuration="org.eventb.core.fwd" org.eventb.core.generated="false" org.eventb.emf.persistence.emf_id="_KQJcuvRsEe60CqkwWvstGA" org.eventb.texttools.text_lastmodified="1712445587675" org.eventb.texttools.text_representation="machine CCTx_Ethereum_Fabric_m2 refines CCTx_Abstract_DLT_m1 sees CCTx_Ethereum_Fabric_c2&#10;&#10;variables received_source_transactions emitted_events subscriptions gateway_pending_events received_target_transactions authenticated_users authenticated_transactions grants&#10;&#10;invariants&#10; @inv11 authenticated_users ⊆ USERS // Authenticated users are a subset of all the possible users&#10; @inv12 authenticated_transactions ∈ received_target_transactions → authenticated_users // Authenticated transactions are received transactions submitted by an authenticated user&#10; @inv13 ∀ tx · tx ∈ received_target_transactions ⇒ (∃ u · u ∈&#10; authenticated_users ∧ tx ↦ u ∈ authenticated_transactions) //Every submitted transaction to Fabric must be authenticated (REQ4)&#10; @inv14 grants ∈ authenticated_users ↔ PERMISSIONS // Users with read or write permissions&#10; @inv15 ∀ u · u ∈ authenticated_transactions[received_target_transactions] ⇒ u ↦ write ∈ grants //Authenticated users that submitted a transaction must have write permissions (REQ5)&#10;&#10;events&#10; event INITIALISATION extends INITIALISATION&#10; then&#10; @act11 authenticated_users ≔ ∅&#10; @act12 authenticated_transactions ≔ ∅&#10; @act14 grants ≔ ∅&#10; end&#10;&#10; event SUBSCRIBE_SMART_CONTRACT_EVENTS_IN_ETHEREUM extends SUBSCRIBE_SMART_CONTRACT_EVENTS&#10; end&#10;&#10; event INITIATE_CC_TX_IN_ETHEREUM extends INITIATE_CC_TX&#10; end&#10;&#10; event EMIT_EVENT_IN_ETHEREUM extends EMIT_EVENT&#10; end&#10;&#10; event LISTEN_EVENT_IN_ETHEREUM extends LISTEN_EVENT&#10; end&#10;&#10; event SUBMIT_TX_TO_FABRIC extends SUBMIT_TX&#10; any user&#10; where&#10; @grd11 user ∈ authenticated_users // Only allow authenticated users (REQ6)&#10; @grd12 user ↦ write ∈ grants // Only allow authorized users (REQ7)&#10; then&#10; @act11 authenticated_transactions(target_smart_contract ↦ transaction) ≔ user // Every submitted transaction to Fabric must be authenticated&#10; end&#10;&#10; event CREATE_GATEWAY_USER&#10;&#9; when&#10;&#9; &#9;@grd1 gateway_user ∉ authenticated_users&#10;&#9; then&#10;&#9; &#9;@act1 authenticated_users ≔ authenticated_users ∪ {gateway_user} // Create credentials for a user (e.g. gateway) to authenticate them (REQ2)&#10; end&#10;&#10; event GRANT_PERMISSION&#10; &#9;any permission user&#10; &#9;where&#10; &#9;&#9;@grd1 permission ∈ PERMISSIONS&#10; &#9;&#9;@grd2 user ∈ authenticated_users&#10; &#9;&#9;@grd3 user ↦ permission ∉ grants&#10; &#9;then&#10; &#9;&#9;@act1 grants ≔ grants ∪ {user ↦ permission} // Grant permissions (e.g. write) to users (e.g. gateway) in Fabric (REQ3)&#10; end&#10;end&#10;" version="5">
<org.eventb.core.refinesMachine name="'" org.eventb.core.target="CCTx_Abstract_DLT_m1"/> <org.eventb.core.refinesMachine name="'" org.eventb.core.target="CCTx_Abstract_DLT_m1"/>
<org.eventb.core.seesContext name="_1tlAgL7uEe6laZimEYihUg" org.eventb.core.target="CCTx_Ethereum_Fabric_c2"/> <org.eventb.core.seesContext name="_1tlAgL7uEe6laZimEYihUg" org.eventb.core.target="CCTx_Ethereum_Fabric_c2"/>
<org.eventb.core.event name="_yREdbb7uEe6laZimEYihUh" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="INITIALISATION" org.eventb.emf.persistence.emf_id="_mFWC4PRhEe60CqkwWvstGA"> <org.eventb.core.event name="_CJbpkPRrEe60CqkwWvstGA" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="INITIALISATION" org.eventb.emf.persistence.emf_id="_KQJcoPRsEe60CqkwWvstGA">
<org.eventb.core.action name="_jV8FAMEWEe6yC4BToIaAqA" org.eventb.core.assignment="authenticated_users ≔ ∅" org.eventb.core.generated="false" org.eventb.core.label="act11" org.eventb.emf.persistence.emf_id="_mFWC3fRhEe60CqkwWvstGA"/> <org.eventb.core.action name="_jV8FAMEWEe6yC4BToIaAqA" org.eventb.core.assignment="authenticated_users ≔ ∅" org.eventb.core.generated="false" org.eventb.core.label="act11" org.eventb.emf.persistence.emf_id="_KQJcnfRsEe60CqkwWvstGA"/>
<org.eventb.core.action name="_jV8FAcEWEe6yC4BToIaAqA" org.eventb.core.assignment="authenticated_transactions ≔ ∅" org.eventb.core.generated="false" org.eventb.core.label="act12" org.eventb.emf.persistence.emf_id="_mFWC3vRhEe60CqkwWvstGA"/> <org.eventb.core.action name="_jV8FAcEWEe6yC4BToIaAqA" org.eventb.core.assignment="authenticated_transactions ≔ ∅" org.eventb.core.generated="false" org.eventb.core.label="act12" org.eventb.emf.persistence.emf_id="_KQJcnvRsEe60CqkwWvstGA"/>
<org.eventb.core.action name="_0oC5cMErEe6yC4BToIaAqA" org.eventb.core.assignment="grants ≔ ∅" org.eventb.core.generated="false" org.eventb.core.label="act14" org.eventb.emf.persistence.emf_id="_mFWC3_RhEe60CqkwWvstGA"/> <org.eventb.core.action name="_0oC5cMErEe6yC4BToIaAqA" org.eventb.core.assignment="grants ≔ ∅" org.eventb.core.generated="false" org.eventb.core.label="act14" org.eventb.emf.persistence.emf_id="_KQJcn_RsEe60CqkwWvstGA"/>
</org.eventb.core.event> </org.eventb.core.event>
<org.eventb.core.event name="_1tlnkr7uEe6laZimEYihUg" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="SUBSCRIBE_SMART_CONTRACT_EVENTS_IN_ETHEREUM" org.eventb.emf.persistence.emf_id="_mFWC4vRhEe60CqkwWvstGA"> <org.eventb.core.event name="_1tlnkr7uEe6laZimEYihUg" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="SUBSCRIBE_SMART_CONTRACT_EVENTS_IN_ETHEREUM" org.eventb.emf.persistence.emf_id="_KQJcovRsEe60CqkwWvstGA">
<org.eventb.core.refinesEvent name="_1tlnk77uEe6laZimEYihUg" org.eventb.core.target="SUBSCRIBE_SMART_CONTRACT_EVENTS"/> <org.eventb.core.refinesEvent name="_1tlnk77uEe6laZimEYihUg" org.eventb.core.target="SUBSCRIBE_SMART_CONTRACT_EVENTS"/>
</org.eventb.core.event> </org.eventb.core.event>
<org.eventb.core.event name="_1g9W8MBFEe6yC4BToIaAqA" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="INITIATE_CC_TX_IN_ETHEREUM" org.eventb.emf.persistence.emf_id="_mFWC5PRhEe60CqkwWvstGA"> <org.eventb.core.event name="_1g9W8MBFEe6yC4BToIaAqA" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="INITIATE_CC_TX_IN_ETHEREUM" org.eventb.emf.persistence.emf_id="_KQJcpPRsEe60CqkwWvstGA">
<org.eventb.core.refinesEvent name="_1g9-AMBFEe6yC4BToIaAqA" org.eventb.core.target="INITIATE_CC_TX"/> <org.eventb.core.refinesEvent name="_1g9-AMBFEe6yC4BToIaAqA" org.eventb.core.target="INITIATE_CC_TX"/>
</org.eventb.core.event> </org.eventb.core.event>
<org.eventb.core.event name="_eB-pUPRhEe60CqkwWvstGA" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="EMIT_EVENT_IN_ETHEREUM" org.eventb.emf.persistence.emf_id="_mFWC5vRhEe60CqkwWvstGA"> <org.eventb.core.event name="_eB-pUPRhEe60CqkwWvstGA" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="EMIT_EVENT_IN_ETHEREUM" org.eventb.emf.persistence.emf_id="_KQJcpvRsEe60CqkwWvstGA">
<org.eventb.core.refinesEvent name="_eB-pUfRhEe60CqkwWvstGA" org.eventb.core.target="EMIT_EVENT"/> <org.eventb.core.refinesEvent name="_eB-pUfRhEe60CqkwWvstGA" org.eventb.core.target="EMIT_EVENT"/>
</org.eventb.core.event> </org.eventb.core.event>
<org.eventb.core.event name="_eB-pUvRhEe60CqkwWvstGA" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="LISTEN_EVENT_IN_ETHEREUM" org.eventb.emf.persistence.emf_id="_mFWC6PRhEe60CqkwWvstGA"> <org.eventb.core.event name="_eB-pUvRhEe60CqkwWvstGA" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="LISTEN_EVENT_IN_ETHEREUM" org.eventb.emf.persistence.emf_id="_KQJcqPRsEe60CqkwWvstGA">
<org.eventb.core.refinesEvent name="_eB-pU_RhEe60CqkwWvstGA" org.eventb.core.target="LISTEN_EVENT"/> <org.eventb.core.refinesEvent name="_eB-pU_RhEe60CqkwWvstGA" org.eventb.core.target="LISTEN_EVENT"/>
</org.eventb.core.event> </org.eventb.core.event>
<org.eventb.core.event name="_eB-pVPRhEe60CqkwWvstGA" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="SUBMIT_TX_TO_FABRIC" org.eventb.emf.persistence.emf_id="_mFWC7vRhEe60CqkwWvstGA"> <org.eventb.core.event name="_eB-pVPRhEe60CqkwWvstGA" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="SUBMIT_TX_TO_FABRIC" org.eventb.emf.persistence.emf_id="_KQJcrvRsEe60CqkwWvstGA">
<org.eventb.core.refinesEvent name="_eB-pVfRhEe60CqkwWvstGA" org.eventb.core.target="SUBMIT_TX"/> <org.eventb.core.refinesEvent name="_eB-pVfRhEe60CqkwWvstGA" org.eventb.core.target="SUBMIT_TX"/>
<org.eventb.core.action name="_jV8sEMEWEe6yC4BToIaAqA" org.eventb.core.assignment="authenticated_transactions(target_smart_contract ↦ transaction) ≔ user" org.eventb.core.comment="Audit user that submitted a transaction to a smart contract (REQ4)" org.eventb.core.generated="false" org.eventb.core.label="act11" org.eventb.emf.persistence.emf_id="_mFWC7fRhEe60CqkwWvstGA"/> <org.eventb.core.action name="_jV8sEMEWEe6yC4BToIaAqA" org.eventb.core.assignment="authenticated_transactions(target_smart_contract ↦ transaction) ≔ user" org.eventb.core.comment="Every submitted transaction to Fabric must be authenticated" org.eventb.core.generated="false" org.eventb.core.label="act11" org.eventb.emf.persistence.emf_id="_KQJcrfRsEe60CqkwWvstGA"/>
<org.eventb.core.guard name="_jV8sEcEWEe6yC4BToIaAqA" org.eventb.core.comment="Only allow authenticated users (REQ6)" org.eventb.core.generated="false" org.eventb.core.label="grd11" org.eventb.core.predicate="user ∈ authenticated_users" org.eventb.emf.persistence.emf_id="_mFWC6_RhEe60CqkwWvstGA"/> <org.eventb.core.guard name="_jV8sEcEWEe6yC4BToIaAqA" org.eventb.core.comment="Only allow authenticated users (REQ6)" org.eventb.core.generated="false" org.eventb.core.label="grd11" org.eventb.core.predicate="user ∈ authenticated_users" org.eventb.emf.persistence.emf_id="_KQJcq_RsEe60CqkwWvstGA"/>
<org.eventb.core.guard name="_jV8sEsEWEe6yC4BToIaAqA" org.eventb.core.comment="Only allow authorized users (REQ7)" org.eventb.core.generated="false" org.eventb.core.label="grd12" org.eventb.core.predicate="user ↦ write ∈ grants" org.eventb.emf.persistence.emf_id="_mFWC7PRhEe60CqkwWvstGA"/> <org.eventb.core.guard name="_jV8sEsEWEe6yC4BToIaAqA" org.eventb.core.comment="Only allow authorized users (REQ7)" org.eventb.core.generated="false" org.eventb.core.label="grd12" org.eventb.core.predicate="user ↦ write ∈ grants" org.eventb.emf.persistence.emf_id="_KQJcrPRsEe60CqkwWvstGA"/>
<org.eventb.core.parameter name="_1tncwL7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="user" org.eventb.emf.persistence.emf_id="_mFWC6vRhEe60CqkwWvstGA"/> <org.eventb.core.parameter name="_1tncwL7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="user" org.eventb.emf.persistence.emf_id="_KQJcqvRsEe60CqkwWvstGA"/>
</org.eventb.core.event> </org.eventb.core.event>
<org.eventb.core.event name="_K_21gMEXEe6yC4BToIaAqA" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="CREATE_GATEWAY_USER" org.eventb.emf.persistence.emf_id="_mFWC8vRhEe60CqkwWvstGA"> <org.eventb.core.event name="_K_21gMEXEe6yC4BToIaAqA" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="CREATE_GATEWAY_USER" org.eventb.emf.persistence.emf_id="_KQJcsvRsEe60CqkwWvstGA">
<org.eventb.core.action name="_jV9TIcEWEe6yC4BToIaAqA" org.eventb.core.assignment="authenticated_users ≔ authenticated_users ∪ {gateway_user}" org.eventb.core.comment="Create credentials for a user (e.g. gateway) to authenticate them (REQ2)" org.eventb.core.generated="false" org.eventb.core.label="act1" org.eventb.emf.persistence.emf_id="_mFWC8fRhEe60CqkwWvstGA"/> <org.eventb.core.action name="_jV9TIcEWEe6yC4BToIaAqA" org.eventb.core.assignment="authenticated_users ≔ authenticated_users ∪ {gateway_user}" org.eventb.core.comment="Create credentials for a user (e.g. gateway) to authenticate them (REQ2)" org.eventb.core.generated="false" org.eventb.core.label="act1" org.eventb.emf.persistence.emf_id="_KQJcsfRsEe60CqkwWvstGA"/>
<org.eventb.core.guard name="_y4y5cMEXEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.label="grd1" org.eventb.core.predicate="gateway_user ∉ authenticated_users" org.eventb.emf.persistence.emf_id="_mFWC8PRhEe60CqkwWvstGA"/> <org.eventb.core.guard name="_y4y5cMEXEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.label="grd1" org.eventb.core.predicate="gateway_user ∉ authenticated_users" org.eventb.emf.persistence.emf_id="_KQJcsPRsEe60CqkwWvstGA"/>
</org.eventb.core.event> </org.eventb.core.event>
<org.eventb.core.event name="_KHHS0MEbEe6yC4BToIaAqA" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="GRANT_PERMISSION" org.eventb.emf.persistence.emf_id="_mFWC-fRhEe60CqkwWvstGA"> <org.eventb.core.event name="_KHHS0MEbEe6yC4BToIaAqA" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="GRANT_PERMISSION" org.eventb.emf.persistence.emf_id="_KQJcufRsEe60CqkwWvstGA">
<org.eventb.core.action name="_KHH54MEbEe6yC4BToIaAqA" org.eventb.core.assignment="grants ≔ grants ∪ {user ↦ permission}" org.eventb.core.comment="Grant permissions (e.g. write) to users (e.g. gateway) in Fabric (REQ3)" org.eventb.core.generated="false" org.eventb.core.label="act1" org.eventb.emf.persistence.emf_id="_mFWC-PRhEe60CqkwWvstGA"/> <org.eventb.core.action name="_KHH54MEbEe6yC4BToIaAqA" org.eventb.core.assignment="grants ≔ grants ∪ {user ↦ permission}" org.eventb.core.comment="Grant permissions (e.g. write) to users (e.g. gateway) in Fabric (REQ3)" org.eventb.core.generated="false" org.eventb.core.label="act1" org.eventb.emf.persistence.emf_id="_KQJcuPRsEe60CqkwWvstGA"/>
<org.eventb.core.guard name="_KHH54cEbEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.label="grd1" org.eventb.core.predicate="permission ∈ PERMISSIONS" org.eventb.emf.persistence.emf_id="_mFWC9fRhEe60CqkwWvstGA"/> <org.eventb.core.guard name="_KHH54cEbEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.label="grd1" org.eventb.core.predicate="permission ∈ PERMISSIONS" org.eventb.emf.persistence.emf_id="_KQJctfRsEe60CqkwWvstGA"/>
<org.eventb.core.guard name="_KHH54sEbEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.label="grd2" org.eventb.core.predicate="user ∈ authenticated_users" org.eventb.emf.persistence.emf_id="_mFWC9vRhEe60CqkwWvstGA"/> <org.eventb.core.guard name="_KHH54sEbEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.label="grd2" org.eventb.core.predicate="user ∈ authenticated_users" org.eventb.emf.persistence.emf_id="_KQJctvRsEe60CqkwWvstGA"/>
<org.eventb.core.guard name="_5yZW0MHNEe609fto5wotHA" org.eventb.core.generated="false" org.eventb.core.label="grd3" org.eventb.core.predicate="user ↦ permission ∉ grants" org.eventb.emf.persistence.emf_id="_mFWC9_RhEe60CqkwWvstGA"/> <org.eventb.core.guard name="_5yZW0MHNEe609fto5wotHA" org.eventb.core.generated="false" org.eventb.core.label="grd3" org.eventb.core.predicate="user ↦ permission ∉ grants" org.eventb.emf.persistence.emf_id="_KQJct_RsEe60CqkwWvstGA"/>
<org.eventb.core.parameter name="_KHIg8MEbEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.identifier="permission" org.eventb.emf.persistence.emf_id="_mFWC8_RhEe60CqkwWvstGA"/> <org.eventb.core.parameter name="_KHIg8MEbEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.identifier="permission" org.eventb.emf.persistence.emf_id="_KQJcs_RsEe60CqkwWvstGA"/>
<org.eventb.core.parameter name="_KHIg8cEbEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.identifier="user" org.eventb.emf.persistence.emf_id="_mFWC9PRhEe60CqkwWvstGA"/> <org.eventb.core.parameter name="_KHIg8cEbEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.identifier="user" org.eventb.emf.persistence.emf_id="_KQJctPRsEe60CqkwWvstGA"/>
</org.eventb.core.event> </org.eventb.core.event>
<org.eventb.core.invariant name="_jV9TIsEWEe6yC4BToIaAqA" org.eventb.core.comment="Authenticated users are a subset of all the possible users" org.eventb.core.generated="false" org.eventb.core.label="inv11" org.eventb.core.predicate="authenticated_users ⊆ USERS" org.eventb.emf.persistence.emf_id="_mFWC2PRhEe60CqkwWvstGA"/> <org.eventb.core.invariant name="_jV9TIsEWEe6yC4BToIaAqA" org.eventb.core.comment="Authenticated users are a subset of all the possible users" org.eventb.core.generated="false" org.eventb.core.label="inv11" org.eventb.core.predicate="authenticated_users ⊆ USERS" org.eventb.emf.persistence.emf_id="_KQJcmPRsEe60CqkwWvstGA"/>
<org.eventb.core.invariant name="_jV9TI8EWEe6yC4BToIaAqA" org.eventb.core.comment="Authenticated transactions are received transactions submitted by an authenticated user" org.eventb.core.generated="false" org.eventb.core.label="inv12" org.eventb.core.predicate="authenticated_transactions ∈ received_target_transactions → authenticated_users" org.eventb.emf.persistence.emf_id="_mFWC2fRhEe60CqkwWvstGA"/> <org.eventb.core.invariant name="_jV9TI8EWEe6yC4BToIaAqA" org.eventb.core.comment="Authenticated transactions are received transactions submitted by an authenticated user" org.eventb.core.generated="false" org.eventb.core.label="inv12" org.eventb.core.predicate="authenticated_transactions ∈ received_target_transactions → authenticated_users" org.eventb.emf.persistence.emf_id="_KQJcmfRsEe60CqkwWvstGA"/>
<org.eventb.core.invariant name="_jV9TJMEWEe6yC4BToIaAqA" org.eventb.core.comment="Every submitted transaction to Fabric must be authenticated (REQ4)" org.eventb.core.generated="false" org.eventb.core.label="inv13" org.eventb.core.predicate="∀ tx · tx ∈ received_target_transactions ⇒ (∃ u · u ∈&#10; authenticated_users ∧ tx ↦ u ∈ authenticated_transactions)" org.eventb.emf.persistence.emf_id="_mFWC2vRhEe60CqkwWvstGA"/> <org.eventb.core.invariant name="_jV9TJMEWEe6yC4BToIaAqA" org.eventb.core.comment="Every submitted transaction to Fabric must be authenticated (REQ4)" org.eventb.core.generated="false" org.eventb.core.label="inv13" org.eventb.core.predicate="∀ tx · tx ∈ received_target_transactions ⇒ (∃ u · u ∈&#10; authenticated_users ∧ tx ↦ u ∈ authenticated_transactions)" org.eventb.emf.persistence.emf_id="_KQJcmvRsEe60CqkwWvstGA"/>
<org.eventb.core.invariant name="_OTstIMHNEe609fto5wotHA" org.eventb.core.comment="Users with read or write permissions" org.eventb.core.generated="false" org.eventb.core.label="inv14" org.eventb.core.predicate="grants ∈ authenticated_users ↔ PERMISSIONS" org.eventb.emf.persistence.emf_id="_mFWC2_RhEe60CqkwWvstGA"/> <org.eventb.core.invariant name="_OTstIMHNEe609fto5wotHA" org.eventb.core.comment="Users with read or write permissions" org.eventb.core.generated="false" org.eventb.core.label="inv14" org.eventb.core.predicate="grants ∈ authenticated_users ↔ PERMISSIONS" org.eventb.emf.persistence.emf_id="_KQJcm_RsEe60CqkwWvstGA"/>
<org.eventb.core.invariant name="_jCLrMcHJEe6yC4BToIaAqA" org.eventb.core.comment="Authenticated users that submitted a transaction must have write permissions (REQ5)" org.eventb.core.generated="false" org.eventb.core.label="inv15" org.eventb.core.predicate="∀ u · u ∈ authenticated_transactions[received_target_transactions] ⇒ u ↦ write ∈ grants" org.eventb.emf.persistence.emf_id="_mFWC3PRhEe60CqkwWvstGA"/> <org.eventb.core.invariant name="_jCLrMcHJEe6yC4BToIaAqA" org.eventb.core.comment="Authenticated users that submitted a transaction must have write permissions (REQ5)" org.eventb.core.generated="false" org.eventb.core.label="inv15" org.eventb.core.predicate="∀ u · u ∈ authenticated_transactions[received_target_transactions] ⇒ u ↦ write ∈ grants" org.eventb.emf.persistence.emf_id="_KQJcnPRsEe60CqkwWvstGA"/>
<org.eventb.core.variable name="_OjhzwPRgEe60CqkwWvstGA" org.eventb.core.generated="false" org.eventb.core.identifier="received_source_transactions" org.eventb.emf.persistence.emf_id="_mFWC0PRhEe60CqkwWvstGA"/> <org.eventb.core.variable name="_OjhzwPRgEe60CqkwWvstGA" org.eventb.core.generated="false" org.eventb.core.identifier="received_source_transactions" org.eventb.emf.persistence.emf_id="_KQJckPRsEe60CqkwWvstGA"/>
<org.eventb.core.variable name="_Zk8OdfKVEe60CqkwWvstGA" org.eventb.core.generated="false" org.eventb.core.identifier="emitted_events" org.eventb.emf.persistence.emf_id="_mFWC0fRhEe60CqkwWvstGA"/> <org.eventb.core.variable name="_Zk8OdfKVEe60CqkwWvstGA" org.eventb.core.generated="false" org.eventb.core.identifier="emitted_events" org.eventb.emf.persistence.emf_id="_KQJckfRsEe60CqkwWvstGA"/>
<org.eventb.core.variable name="_yREda77uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="subscriptions" org.eventb.emf.persistence.emf_id="_mFWC0vRhEe60CqkwWvstGA"/> <org.eventb.core.variable name="_yREda77uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="subscriptions" org.eventb.emf.persistence.emf_id="_KQJckvRsEe60CqkwWvstGA"/>
<org.eventb.core.variable name="_OjhzwfRgEe60CqkwWvstGA" org.eventb.core.generated="false" org.eventb.core.identifier="gateway_pending_events" org.eventb.emf.persistence.emf_id="_mFWC0_RhEe60CqkwWvstGA"/> <org.eventb.core.variable name="_OjhzwfRgEe60CqkwWvstGA" org.eventb.core.generated="false" org.eventb.core.identifier="gateway_pending_events" org.eventb.emf.persistence.emf_id="_KQJck_RsEe60CqkwWvstGA"/>
<org.eventb.core.variable name="_Ojia0PRgEe60CqkwWvstGA" org.eventb.core.generated="false" org.eventb.core.identifier="received_target_transactions" org.eventb.emf.persistence.emf_id="_mFWC1PRhEe60CqkwWvstGA"/> <org.eventb.core.variable name="_Ojia0PRgEe60CqkwWvstGA" org.eventb.core.generated="false" org.eventb.core.identifier="received_target_transactions" org.eventb.emf.persistence.emf_id="_KQJclPRsEe60CqkwWvstGA"/>
<org.eventb.core.variable name="_1toq4L7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="authenticated_users" org.eventb.emf.persistence.emf_id="_mFWC1fRhEe60CqkwWvstGA"/> <org.eventb.core.variable name="_1toq4L7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="authenticated_users" org.eventb.emf.persistence.emf_id="_KQJclfRsEe60CqkwWvstGA"/>
<org.eventb.core.variable name="_1toq4b7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="authenticated_transactions" org.eventb.emf.persistence.emf_id="_mFWC1vRhEe60CqkwWvstGA"/> <org.eventb.core.variable name="_1toq4b7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="authenticated_transactions" org.eventb.emf.persistence.emf_id="_KQJclvRsEe60CqkwWvstGA"/>
<org.eventb.core.variable name="_2RlqIMErEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.identifier="grants" org.eventb.emf.persistence.emf_id="_mFWC1_RhEe60CqkwWvstGA"/> <org.eventb.core.variable name="_2RlqIMErEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.identifier="grants" org.eventb.emf.persistence.emf_id="_KQJcl_RsEe60CqkwWvstGA"/>
</org.eventb.core.machineFile> </org.eventb.core.machineFile>
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment