Newer
Older
<?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="_-e8JPMHOEe609fto5wotHA" org.eventb.texttools.text_lastmodified="1706880519570" org.eventb.texttools.text_representation="machine CCTx_Ethereum_Fabric_m3 refines CCTx_Ethereum_Fabric_m2 sees CCTx_Ethereum_Fabric_c2 variables received_transactions triggered_events subscriptions gateway_pending_transactions received_cross_chain_transactions authenticated_users authenticated_transactions grants subscribed initiated triggered gateway_processing submit_cc_tx user_created write_granted invariants 	@inv11 subscribed ∈ {0,1} 	@inv12 initiated ∈ {0,1} 	@inv13 triggered ∈ {0,1} 	@inv14 gateway_processing ∈ {0,1} 	@inv15 submit_cc_tx ∈ {0,1} 	@inv16 user_created ∈ {0,1} 	@inv17 write_granted ∈ {0,1} events event INITIALISATION extends INITIALISATION 	then 		@act31 subscribed ≔ 0 		@act32 initiated ≔ 0 		@act33 triggered ≔ 0 		@act34 gateway_processing ≔ 0 		@act35 submit_cc_tx ≔ 0 		@act36 user_created ≔ 0 		@act37 write_granted ≔ 0 end event SUBSCRIBE_SMART_CONTRACT_EVENTS_IN_ETHEREUM extends SUBSCRIBE_SMART_CONTRACT_EVENTS_IN_ETHEREUM 	then 		@act31 subscribed ≔ 1 end event INITIATE_CC_TX_IN_ETHEREUM extends INITIATE_CC_TX_IN_ETHEREUM 	then 		@act31 initiated ≔ 1 		@act32 submit_cc_tx ≔ 0 end event TRIGGER_CC_TX_EVENT_IN_ETHEREUM extends TRIGGER_CC_TX_EVENT_IN_ETHEREUM 	then 		@act31 triggered ≔ 1 		@act32 initiated ≔ 0 		@act33 submit_cc_tx ≔ 0 end event LISTEN_CC_TX_EVENT_IN_ETHEREUM extends LISTEN_CC_TX_EVENT_IN_ETHEREUM 	then 		@act31 gateway_processing ≔ 1 		@act32 triggered ≔ 0 		@act33 submit_cc_tx ≔ 0 end event SUBMIT_CC_TX_TO_FABRIC extends SUBMIT_CC_TX_TO_FABRIC 	then 		@act31 submit_cc_tx ≔ 1 		@act32 gateway_processing ≔ 0 end event CREATE_GATEWAY_USER extends CREATE_GATEWAY_USER 	then 		@act31 user_created ≔ 1 end event GRANT_PERMISSION extends GRANT_PERMISSION 	when 		@grd31 user = gateway_user 		@grd32 permission = write 	then 		@act31 write_granted ≔ 1 end end " version="5">
<org.eventb.core.refinesMachine name="'" org.eventb.core.target="CCTx_Ethereum_Fabric_m2"/>
<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="_-e8JHcHOEe609fto5wotHA">
<org.eventb.core.action name="_FVN5wMHOEe609fto5wotHA" org.eventb.core.assignment="subscribed ≔ 0" org.eventb.core.generated="false" org.eventb.core.label="act31" org.eventb.emf.persistence.emf_id="_-e8JFsHOEe609fto5wotHA"/>
<org.eventb.core.action name="_FVN5wcHOEe609fto5wotHA" org.eventb.core.assignment="initiated ≔ 0" org.eventb.core.generated="false" org.eventb.core.label="act32" org.eventb.emf.persistence.emf_id="_-e8JF8HOEe609fto5wotHA"/>
<org.eventb.core.action name="_FVOg0MHOEe609fto5wotHA" org.eventb.core.assignment="triggered ≔ 0" org.eventb.core.generated="false" org.eventb.core.label="act33" org.eventb.emf.persistence.emf_id="_-e8JGMHOEe609fto5wotHA"/>
<org.eventb.core.action name="_FVOg0cHOEe609fto5wotHA" org.eventb.core.assignment="gateway_processing ≔ 0" org.eventb.core.generated="false" org.eventb.core.label="act34" org.eventb.emf.persistence.emf_id="_-e8JGcHOEe609fto5wotHA"/>
<org.eventb.core.action name="_FVPH4MHOEe609fto5wotHA" org.eventb.core.assignment="submit_cc_tx ≔ 0" org.eventb.core.generated="false" org.eventb.core.label="act35" org.eventb.emf.persistence.emf_id="_-e8JGsHOEe609fto5wotHA"/>
<org.eventb.core.action name="_FVPH4cHOEe609fto5wotHA" org.eventb.core.assignment="user_created ≔ 0" org.eventb.core.generated="false" org.eventb.core.label="act36" org.eventb.emf.persistence.emf_id="_-e8JG8HOEe609fto5wotHA"/>
<org.eventb.core.action name="_4VMjkMHOEe609fto5wotHA" org.eventb.core.assignment="write_granted ≔ 0" org.eventb.core.generated="false" org.eventb.core.label="act37" org.eventb.emf.persistence.emf_id="_-e8JHMHOEe609fto5wotHA"/>
</org.eventb.core.event>
<org.eventb.core.event name="_yREdbb7uEe6laZimEYihUi" 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="_-e8JIMHOEe609fto5wotHA">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="SUBSCRIBE_SMART_CONTRACT_EVENTS_IN_ETHEREUM"/>
<org.eventb.core.action name="_G4NWgMHOEe609fto5wotHA" org.eventb.core.assignment="subscribed ≔ 1" org.eventb.core.generated="false" org.eventb.core.label="act31" org.eventb.emf.persistence.emf_id="_-e8JH8HOEe609fto5wotHA"/>
<org.eventb.core.event name="_yREdbb7uEe6laZimEYihUj" 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="_-e8JJMHOEe609fto5wotHA">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="INITIATE_CC_TX_IN_ETHEREUM"/>
<org.eventb.core.action name="_I7eOwMHOEe609fto5wotHA" org.eventb.core.assignment="initiated ≔ 1" org.eventb.core.generated="false" org.eventb.core.label="act31" org.eventb.emf.persistence.emf_id="_-e8JIsHOEe609fto5wotHA"/>
<org.eventb.core.action name="_I7eOwcHOEe609fto5wotHA" org.eventb.core.assignment="submit_cc_tx ≔ 0" org.eventb.core.generated="false" org.eventb.core.label="act32" org.eventb.emf.persistence.emf_id="_-e8JI8HOEe609fto5wotHA"/>
<org.eventb.core.event name="_yREdbb7uEe6laZimEYihUk" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="TRIGGER_CC_TX_EVENT_IN_ETHEREUM" org.eventb.emf.persistence.emf_id="_-e8JKcHOEe609fto5wotHA">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="TRIGGER_CC_TX_EVENT_IN_ETHEREUM"/>
<org.eventb.core.action name="_LjZ6UMHOEe609fto5wotHA" org.eventb.core.assignment="triggered ≔ 1" org.eventb.core.generated="false" org.eventb.core.label="act31" org.eventb.emf.persistence.emf_id="_-e8JJsHOEe609fto5wotHA"/>
<org.eventb.core.action name="_LjZ6UcHOEe609fto5wotHA" org.eventb.core.assignment="initiated ≔ 0" org.eventb.core.generated="false" org.eventb.core.label="act32" org.eventb.emf.persistence.emf_id="_-e8JJ8HOEe609fto5wotHA"/>
<org.eventb.core.action name="_LjahYMHOEe609fto5wotHA" org.eventb.core.assignment="submit_cc_tx ≔ 0" org.eventb.core.generated="false" org.eventb.core.label="act33" org.eventb.emf.persistence.emf_id="_-e8JKMHOEe609fto5wotHA"/>
<org.eventb.core.event name="_yREdbb7uEe6laZimEYihUl" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="LISTEN_CC_TX_EVENT_IN_ETHEREUM" org.eventb.emf.persistence.emf_id="_-e8JLsHOEe609fto5wotHA">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="LISTEN_CC_TX_EVENT_IN_ETHEREUM"/>
<org.eventb.core.action name="_NY1x8MHOEe609fto5wotHA" org.eventb.core.assignment="gateway_processing ≔ 1" org.eventb.core.generated="false" org.eventb.core.label="act31" org.eventb.emf.persistence.emf_id="_-e8JK8HOEe609fto5wotHA"/>
<org.eventb.core.action name="_NY1x8cHOEe609fto5wotHA" org.eventb.core.assignment="triggered ≔ 0" org.eventb.core.generated="false" org.eventb.core.label="act32" org.eventb.emf.persistence.emf_id="_-e8JLMHOEe609fto5wotHA"/>
<org.eventb.core.action name="_NY1x8sHOEe609fto5wotHA" org.eventb.core.assignment="submit_cc_tx ≔ 0" org.eventb.core.generated="false" org.eventb.core.label="act33" org.eventb.emf.persistence.emf_id="_-e8JLcHOEe609fto5wotHA"/>
<org.eventb.core.event name="_yREdbb7uEe6laZimEYihUm" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="SUBMIT_CC_TX_TO_FABRIC" org.eventb.emf.persistence.emf_id="_-e8JMsHOEe609fto5wotHA">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="SUBMIT_CC_TX_TO_FABRIC"/>
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
<org.eventb.core.action name="_RH42kMHOEe609fto5wotHA" org.eventb.core.assignment="submit_cc_tx ≔ 1" org.eventb.core.generated="false" org.eventb.core.label="act31" org.eventb.emf.persistence.emf_id="_-e8JMMHOEe609fto5wotHA"/>
<org.eventb.core.action name="_RH5doMHOEe609fto5wotHA" org.eventb.core.assignment="gateway_processing ≔ 0" org.eventb.core.generated="false" org.eventb.core.label="act32" org.eventb.emf.persistence.emf_id="_-e8JMcHOEe609fto5wotHA"/>
</org.eventb.core.event>
<org.eventb.core.event name="_yREdbb7uEe6laZimEYihUn" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="CREATE_GATEWAY_USER" org.eventb.emf.persistence.emf_id="_-e8JNcHOEe609fto5wotHA">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="CREATE_GATEWAY_USER"/>
<org.eventb.core.action name="_RH5docHOEe609fto5wotHA" org.eventb.core.assignment="user_created ≔ 1" org.eventb.core.generated="false" org.eventb.core.label="act31" org.eventb.emf.persistence.emf_id="_-e8JNMHOEe609fto5wotHA"/>
</org.eventb.core.event>
<org.eventb.core.event name="_yREdbb7uEe6laZimEYihUo" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="GRANT_PERMISSION" org.eventb.emf.persistence.emf_id="_-e8JOsHOEe609fto5wotHA">
<org.eventb.core.refinesEvent name="'" org.eventb.core.target="GRANT_PERMISSION"/>
<org.eventb.core.action name="_yeWE8MHOEe609fto5wotHA" org.eventb.core.assignment="write_granted ≔ 1" org.eventb.core.generated="false" org.eventb.core.label="act31" org.eventb.emf.persistence.emf_id="_-e8JOcHOEe609fto5wotHA"/>
<org.eventb.core.guard name="_yeWE8cHOEe609fto5wotHA" org.eventb.core.generated="false" org.eventb.core.label="grd31" org.eventb.core.predicate="user = gateway_user" org.eventb.emf.persistence.emf_id="_-e8JN8HOEe609fto5wotHA"/>
<org.eventb.core.guard name="_-iJ1EMHOEe609fto5wotHA" org.eventb.core.generated="false" org.eventb.core.label="grd32" org.eventb.core.predicate="permission = write" org.eventb.emf.persistence.emf_id="_-e8JOMHOEe609fto5wotHA"/>
</org.eventb.core.event>
<org.eventb.core.invariant name="_DmAl8MHOEe609fto5wotHA" org.eventb.core.generated="false" org.eventb.core.label="inv11" org.eventb.core.predicate="subscribed ∈ {0,1}" org.eventb.emf.persistence.emf_id="_-e8JD8HOEe609fto5wotHA"/>
<org.eventb.core.invariant name="_DmB0EMHOEe609fto5wotHA" org.eventb.core.generated="false" org.eventb.core.label="inv12" org.eventb.core.predicate="initiated ∈ {0,1}" org.eventb.emf.persistence.emf_id="_-e8JEMHOEe609fto5wotHA"/>
<org.eventb.core.invariant name="_DmCbIMHOEe609fto5wotHA" org.eventb.core.generated="false" org.eventb.core.label="inv13" org.eventb.core.predicate="triggered ∈ {0,1}" org.eventb.emf.persistence.emf_id="_-e8JEcHOEe609fto5wotHA"/>
<org.eventb.core.invariant name="_DmDCMMHOEe609fto5wotHA" org.eventb.core.generated="false" org.eventb.core.label="inv14" org.eventb.core.predicate="gateway_processing ∈ {0,1}" org.eventb.emf.persistence.emf_id="_-e8JEsHOEe609fto5wotHA"/>
<org.eventb.core.invariant name="_DmDpQMHOEe609fto5wotHA" org.eventb.core.generated="false" org.eventb.core.label="inv15" org.eventb.core.predicate="submit_cc_tx ∈ {0,1}" org.eventb.emf.persistence.emf_id="_-e8JE8HOEe609fto5wotHA"/>
<org.eventb.core.invariant name="_DmEQUMHOEe609fto5wotHA" org.eventb.core.generated="false" org.eventb.core.label="inv16" org.eventb.core.predicate="user_created ∈ {0,1}" org.eventb.emf.persistence.emf_id="_-e8JFMHOEe609fto5wotHA"/>
<org.eventb.core.invariant name="_2MNd0MHOEe609fto5wotHA" org.eventb.core.generated="false" org.eventb.core.label="inv17" org.eventb.core.predicate="write_granted ∈ {0,1}" org.eventb.emf.persistence.emf_id="_-e8JFcHOEe609fto5wotHA"/>
<org.eventb.core.variable name="_yREdab7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="received_transactions" org.eventb.emf.persistence.emf_id="_-e8JAMHOEe609fto5wotHA"/>
<org.eventb.core.variable name="_yREdar7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="triggered_events" org.eventb.emf.persistence.emf_id="_-e8JAcHOEe609fto5wotHA"/>
<org.eventb.core.variable name="_yREda77uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="subscriptions" org.eventb.emf.persistence.emf_id="_-e8JAsHOEe609fto5wotHA"/>
<org.eventb.core.variable name="_yREdbL7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="gateway_pending_transactions" org.eventb.emf.persistence.emf_id="_-e8JA8HOEe609fto5wotHA"/>
<org.eventb.core.variable name="_yREdbb7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="received_cross_chain_transactions" org.eventb.emf.persistence.emf_id="_-e8JBMHOEe609fto5wotHA"/>
<org.eventb.core.variable name="_1toq4L7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="authenticated_users" org.eventb.emf.persistence.emf_id="_-e8JBcHOEe609fto5wotHA"/>
<org.eventb.core.variable name="_1toq4b7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="authenticated_transactions" org.eventb.emf.persistence.emf_id="_-e8JBsHOEe609fto5wotHA"/>
<org.eventb.core.variable name="_2RlqIMErEe6yC4BToIaAqA" org.eventb.core.generated="false" org.eventb.core.identifier="grants" org.eventb.emf.persistence.emf_id="_-e8JB8HOEe609fto5wotHA"/>
<org.eventb.core.variable name="_DmLlEMHOEe609fto5wotHA" org.eventb.core.generated="false" org.eventb.core.identifier="subscribed" org.eventb.emf.persistence.emf_id="_-e8JCMHOEe609fto5wotHA"/>
<org.eventb.core.variable name="_DmMMIMHOEe609fto5wotHA" org.eventb.core.generated="false" org.eventb.core.identifier="initiated" org.eventb.emf.persistence.emf_id="_-e8JCcHOEe609fto5wotHA"/>
<org.eventb.core.variable name="_DmMMIcHOEe609fto5wotHA" org.eventb.core.generated="false" org.eventb.core.identifier="triggered" org.eventb.emf.persistence.emf_id="_-e8JCsHOEe609fto5wotHA"/>
<org.eventb.core.variable name="_DmMMIsHOEe609fto5wotHA" org.eventb.core.generated="false" org.eventb.core.identifier="gateway_processing" org.eventb.emf.persistence.emf_id="_-e8JC8HOEe609fto5wotHA"/>
<org.eventb.core.variable name="_DmMMI8HOEe609fto5wotHA" org.eventb.core.generated="false" org.eventb.core.identifier="submit_cc_tx" org.eventb.emf.persistence.emf_id="_-e8JDMHOEe609fto5wotHA"/>
<org.eventb.core.variable name="_DmMMJMHOEe609fto5wotHA" org.eventb.core.generated="false" org.eventb.core.identifier="user_created" org.eventb.emf.persistence.emf_id="_-e8JDcHOEe609fto5wotHA"/>
<org.eventb.core.variable name="_2MPTAMHOEe609fto5wotHA" org.eventb.core.generated="false" org.eventb.core.identifier="write_granted" org.eventb.emf.persistence.emf_id="_-e8JDsHOEe609fto5wotHA"/>