diff --git a/Gateway_Event_B_specification___ICBC_Cross_chain_workshop (3).pdf b/Gateway_Event_B_specification___ICBC_Cross_chain_workshop (3).pdf
new file mode 100644
index 0000000000000000000000000000000000000000..3e8385c8ae6fc5ac2252ff150bd5e9cd33171196
Binary files /dev/null and b/Gateway_Event_B_specification___ICBC_Cross_chain_workshop (3).pdf differ
diff --git a/gateway-event-b/latex/CCTx_Abstract_Animation_m2.tex b/gateway-event-b/latex/CCTx_Abstract_Animation_m2.tex
new file mode 100644
index 0000000000000000000000000000000000000000..7ce515c3df96a933fd457b41785ba8905f803c08
--- /dev/null
+++ b/gateway-event-b/latex/CCTx_Abstract_Animation_m2.tex
@@ -0,0 +1,116 @@
+\documentclass[10pt,a4paper]{report}
+\usepackage{bsymb,b2latex}
+\begin{document}
+\SingleHeader{CCTx\_Abstract\_Animation\_m2}
+\MACHINE{CCTx\_Abstract\_Animation\_m2}{CCTx\_Abstract\_DLT\_m1}{CCTx\_Abstract\_DLT\_c1}{}
+\VARIABLES{
+ \Variable{received\_source\_transactions}{}
+ \Variable{emitted\_events}{}
+ \Variable{subscriptions}{}
+ \Variable{gateway\_pending\_events}{}
+ \Variable{received\_target\_transactions}{}
+ \Variable{subscribed}{}
+ \Variable{initiated}{}
+ \Variable{emitted}{}
+ \Variable{gateway\_processing}{}
+ \Variable{submit\_cc\_tx}{}
+}
+\INVARIANTS{
+ \Invariant{inv11}{false}{$subscribed \in{} \{0,1\}$}{}
+ \Invariant{inv12}{false}{$initiated \in{} \{0,1\}$}{}
+ \Invariant{inv13}{false}{$emitted \in{} \{0,1\}$}{}
+ \Invariant{inv14}{false}{$gateway\_processing \in{} \{0,1\}$}{}
+ \Invariant{inv15}{false}{$submit\_cc\_tx \in{} \{0,1\}$}{}
+}
+\EVENTS{
+\INITIALISATION{true}{}{
+ \ACTIONS{false}{
+ \Action{act1}{$received\_source\_transactions \bcmeq{} \emptyset{}$}{false}{}
+ \Action{act2}{$emitted\_events \bcmeq{} \emptyset{}$}{false}{}
+ \Action{act3}{$subscriptions \bcmeq{} \emptyset{}$}{false}{}
+ \Action{act4}{$gateway\_pending\_events \bcmeq{} \emptyset{}$}{false}{}
+ \Action{act6}{$received\_target\_transactions \bcmeq{} \emptyset{}$}{false}{}
+ \Action{act11}{$subscribed \bcmeq{} 0$}{true}{}
+ \Action{act12}{$initiated \bcmeq{} 0$}{true}{}
+ \Action{act13}{$emitted \bcmeq{} 0$}{true}{}
+ \Action{act14}{$gateway\_processing \bcmeq{} 0$}{true}{}
+ \Action{act15}{$submit\_cc\_tx \bcmeq{} 0$}{true}{}
+ }
+}
+\EVT{SUBSCRIBE\_SMART\_CONTRACT\_EVENTS}{true}{ordinary}{SUBSCRIBE\_SMART\_CONTRACT\_EVENTS}{}{
+ \GUARDS{false}{
+ \Guard{grd1}{false}{$gateway \mapsto{} source\_smart\_contract \notin{} subscriptions$}{false}{\\The gateway is not already subscribed to the smart contract events}
+ }
+ \ACTIONS{true}{
+ \Action{act1}{$subscriptions \bcmeq{} subscriptions \bunion{} \{gateway \mapsto{} source\_smart\_contract\}$}{false}{\\The gateway is subscribed to listen to the smart contract events}
+ \Action{act11}{$subscribed \bcmeq{} 1$}{true}{}
+ }
+}
+\EVT{INITIATE\_CC\_TX}{true}{ordinary}{INITIATE\_CC\_TX}{}{
+ \ANY{
+ \Param{transaction}{false}{}
+ }
+ \GUARDS{true}{
+ \Guard{grd1}{false}{$transaction \in{} SOURCE\_TRANSACTIONS$}{false}{}
+ \Guard{grd3}{false}{$transaction \notin{} received\_source\_transactions[\{source\_smart\_contract\}]$}{false}{\\The transaction was not received by the smart contract}
+ }
+ \ACTIONS{true}{
+ \Action{act1}{$received\_source\_transactions \bcmeq{} received\_source\_transactions \bunion{} \{source\_smart\_contract \mapsto{} transaction\}$}{false}{\\Add the transaction to the received transactions of the smart contract}
+ \Action{act11}{$initiated \bcmeq{} 1$}{true}{}
+ \Action{act12}{$submit\_cc\_tx \bcmeq{} 0$}{true}{}
+ }
+}
+\EVT{EMIT\_EVENT}{true}{ordinary}{EMIT\_EVENT}{}{
+ \ANY{
+ \Param{transaction}{false}{}
+ \Param{emitted\_event}{false}{}
+ }
+ \GUARDS{true}{
+ \Guard{grd1}{false}{$source\_smart\_contract \mapsto{} transaction \in{} received\_source\_transactions$}{false}{\\The smart contract has a pending transaction to process}
+ \Guard{grd2}{false}{$emitted\_event \notin{} emitted\_events[\{source\_smart\_contract\}]$}{false}{\\The smart contract will always emit a new event}
+ }
+ \ACTIONS{true}{
+ \Action{act1}{$emitted\_events \bcmeq{} emitted\_events \bunion{} \{source\_smart\_contract \mapsto{} emitted\_event\}$}{false}{\\The smart contract emits a new event related to the transaction processing}
+ \Action{act2}{$received\_source\_transactions \bcmeq{} received\_source\_transactions \setminus{} \{source\_smart\_contract \mapsto{} transaction\}$}{false}{\\The smart contract processed the transaction}
+ \Action{act11}{$emitted \bcmeq{} 1$}{true}{}
+ \Action{act12}{$initiated \bcmeq{} 0$}{true}{}
+ \Action{act13}{$submit\_cc\_tx \bcmeq{} 0$}{true}{}
+ }
+}
+\EVT{LISTEN\_EVENT}{true}{ordinary}{LISTEN\_EVENT}{}{
+ \ANY{
+ \Param{emitted\_event}{false}{}
+ \Param{pending\_event}{false}{}
+ }
+ \GUARDS{true}{
+ \Guard{grd1}{false}{$source\_smart\_contract \mapsto{} emitted\_event \in{} emitted\_events$}{false}{\\The smart contract has emitted an event}
+ \Guard{grd2}{false}{$gateway \mapsto{} source\_smart\_contract \in{} subscriptions$}{false}{\\Exist a subscription to the smart contract events}
+ \Guard{grd3}{false}{$gateway \mapsto{} pending\_event \notin{} gateway\_pending\_events$}{false}{\\The event was not already listened}
+ }
+ \ACTIONS{true}{
+ \Action{act1}{$gateway\_pending\_events \bcmeq{} gateway\_pending\_events \bunion{} \{gateway \mapsto{} pending\_event\}$}{false}{\\The event is added to the pending events to be processed by the gateway}
+ \Action{act2}{$emitted\_events \bcmeq{} emitted\_events \setminus{} \{source\_smart\_contract \mapsto{} emitted\_event\}$}{false}{\\The event is removed from the pending events to listen}
+ \Action{act11}{$gateway\_processing \bcmeq{} 1$}{true}{}
+ \Action{act12}{$emitted \bcmeq{} 0$}{true}{}
+ \Action{act13}{$submit\_cc\_tx \bcmeq{} 0$}{true}{}
+ }
+}
+\EVT{SUBMIT\_TX}{true}{ordinary}{SUBMIT\_TX}{}{
+ \ANY{
+ \Param{pending\_event}{false}{}
+ \Param{transaction}{false}{}
+ }
+ \GUARDS{true}{
+ \Guard{grd1}{false}{$gateway \mapsto{} pending\_event \in{} gateway\_pending\_events$}{false}{\\There is one pending event to be processed}
+ \Guard{grd2}{false}{$transaction \in{} TARGET\_TRANSACTIONS$}{false}{}
+ }
+ \ACTIONS{true}{
+ \Action{act1}{$received\_target\_transactions \bcmeq{} received\_target\_transactions \bunion{} \{target\_smart\_contract \mapsto{} transaction\}$}{false}{\\The transaction is received by the target smart contract}
+ \Action{act2}{$gateway\_pending\_events \bcmeq{} gateway\_pending\_events \setminus{} \{gateway \mapsto{} pending\_event\}$}{false}{\\Remove the event from the pending events of the gateway}
+ \Action{act11}{$submit\_cc\_tx \bcmeq{} 1$}{true}{}
+ \Action{act12}{$gateway\_processing \bcmeq{} 0$}{true}{}
+ }
+}
+}
+\END
+\end{document}
diff --git a/gateway-event-b/latex/CCTx_Abstract_DLT_c1.tex b/gateway-event-b/latex/CCTx_Abstract_DLT_c1.tex
index 59293abbc80fbbcdf98f03ee4f0da390e62dfcd3..7b04cb4eb2aa35435f707f9fa4bcd2ab1e804b58 100644
--- a/gateway-event-b/latex/CCTx_Abstract_DLT_c1.tex
+++ b/gateway-event-b/latex/CCTx_Abstract_DLT_c1.tex
@@ -5,10 +5,10 @@
\CONTEXT{CCTx\_Abstract\_DLT\_c1}{}{}
\SETS{
\Set{GATEWAYS}{}
- \Set{TRANSACTIONS}{}
+ \Set{SOURCE\_TRANSACTIONS}{}
\Set{CROSS\_CHAIN\_SMART\_CONTRACTS}{}
- \Set{CROSS\_CHAIN\_EVENTS}{}
- \Set{CROSS\_CHAIN\_TRANSACTIONS}{}
+ \Set{SMART\_CONTRACT\_EVENTS}{}
+ \Set{TARGET\_TRANSACTIONS}{}
}
\CONSTANTS{
\Constant{source\_smart\_contract}{}
diff --git a/gateway-event-b/latex/CCTx_Abstract_DLT_m1.tex b/gateway-event-b/latex/CCTx_Abstract_DLT_m1.tex
index 1013c97d74e3b2c08accb8c0e0e89b1a55c0b7ba..32c74971868e31be8ac55b34e3323dc9699d1465 100644
--- a/gateway-event-b/latex/CCTx_Abstract_DLT_m1.tex
+++ b/gateway-event-b/latex/CCTx_Abstract_DLT_m1.tex
@@ -4,27 +4,27 @@
\SingleHeader{CCTx\_Abstract\_DLT\_m1}
\MACHINE{CCTx\_Abstract\_DLT\_m1}{}{CCTx\_Abstract\_DLT\_c1}{}
\VARIABLES{
- \Variable{received\_transactions}{}
- \Variable{triggered\_events}{}
+ \Variable{received\_source\_transactions}{}
+ \Variable{emitted\_events}{}
\Variable{subscriptions}{}
- \Variable{gateway\_pending\_transactions}{}
- \Variable{received\_cross\_chain\_transactions}{}
+ \Variable{gateway\_pending\_events}{}
+ \Variable{received\_target\_transactions}{}
}
\INVARIANTS{
- \Invariant{inv1}{false}{$received\_transactions \in{} CROSS\_CHAIN\_SMART\_CONTRACTS \rel{} TRANSACTIONS$}{}
- \Invariant{inv2}{false}{$triggered\_events \in{} CROSS\_CHAIN\_SMART\_CONTRACTS \rel{} CROSS\_CHAIN\_EVENTS$}{}
+ \Invariant{inv1}{false}{$received\_source\_transactions \in{} CROSS\_CHAIN\_SMART\_CONTRACTS \rel{} SOURCE\_TRANSACTIONS$}{}
+ \Invariant{inv2}{false}{$emitted\_events \in{} CROSS\_CHAIN\_SMART\_CONTRACTS \rel{} SMART\_CONTRACT\_EVENTS$}{}
\Invariant{inv3}{false}{$subscriptions \in{} GATEWAYS \rel{} CROSS\_CHAIN\_SMART\_CONTRACTS$}{}
- \Invariant{inv4}{false}{$gateway\_pending\_transactions \in{} GATEWAYS \rel{} CROSS\_CHAIN\_TRANSACTIONS$}{}
- \Invariant{inv5}{false}{$received\_cross\_chain\_transactions \in{} CROSS\_CHAIN\_SMART\_CONTRACTS \rel{} CROSS\_CHAIN\_TRANSACTIONS$}{}
+ \Invariant{inv4}{false}{$gateway\_pending\_events \in{} GATEWAYS \rel{} TARGET\_TRANSACTIONS$}{}
+ \Invariant{inv5}{false}{$received\_target\_transactions \in{} CROSS\_CHAIN\_SMART\_CONTRACTS \rel{} TARGET\_TRANSACTIONS$}{}
}
\EVENTS{
\INITIALISATION{false}{}{
\ACTIONS{false}{
- \Action{act1}{$received\_transactions \bcmeq{} \emptyset{}$}{true}{}
- \Action{act2}{$triggered\_events \bcmeq{} \emptyset{}$}{true}{}
+ \Action{act1}{$received\_source\_transactions \bcmeq{} \emptyset{}$}{true}{}
+ \Action{act2}{$emitted\_events \bcmeq{} \emptyset{}$}{true}{}
\Action{act3}{$subscriptions \bcmeq{} \emptyset{}$}{true}{}
- \Action{act4}{$gateway\_pending\_transactions \bcmeq{} \emptyset{}$}{true}{}
- \Action{act6}{$received\_cross\_chain\_transactions \bcmeq{} \emptyset{}$}{true}{}
+ \Action{act4}{$gateway\_pending\_events \bcmeq{} \emptyset{}$}{true}{}
+ \Action{act6}{$received\_target\_transactions \bcmeq{} \emptyset{}$}{true}{}
}
}
\EVT{SUBSCRIBE\_SMART\_CONTRACT\_EVENTS}{false}{ordinary}{}{}{
@@ -40,52 +40,54 @@
\Param{transaction}{true}{}
}
\GUARDS{true}{
- \Guard{grd1}{false}{$transaction \in{} TRANSACTIONS$}{true}{}
- \Guard{grd3}{false}{$transaction \notin{} received\_transactions[\{source\_smart\_contract\}]$}{true}{\\The transaction was not received by the smart contract}
+ \Guard{grd1}{false}{$transaction \in{} SOURCE\_TRANSACTIONS$}{true}{}
+ \Guard{grd3}{false}{$transaction \notin{} received\_source\_transactions[\{source\_smart\_contract\}]$}{true}{\\The transaction was not received by the smart contract}
}
\ACTIONS{true}{
- \Action{act1}{$received\_transactions \bcmeq{} received\_transactions \bunion{} \{source\_smart\_contract \mapsto{} transaction\}$}{true}{\\Add the transaction to the received transactions of the smart contract}
+ \Action{act1}{$received\_source\_transactions \bcmeq{} received\_source\_transactions \bunion{} \{source\_smart\_contract \mapsto{} transaction\}$}{true}{\\Add the transaction to the received transactions of the smart contract}
}
}
-\EVT{TRIGGER\_CC\_TX\_EVENT}{false}{ordinary}{}{}{
+\EVT{EMIT\_EVENT}{false}{ordinary}{}{}{
\ANY{
\Param{transaction}{true}{}
- \Param{cross\_chain\_event}{true}{}
+ \Param{emitted\_event}{true}{}
}
\GUARDS{true}{
- \Guard{grd1}{false}{$source\_smart\_contract \mapsto{} transaction \in{} received\_transactions$}{true}{\\The smart contract has a pending transaction to process}
- \Guard{grd2}{false}{$cross\_chain\_event \notin{} triggered\_events[\{source\_smart\_contract\}]$}{true}{\\The smart contract will always trigger a new event}
+ \Guard{grd1}{false}{$source\_smart\_contract \mapsto{} transaction \in{} received\_source\_transactions$}{true}{\\The smart contract has a pending transaction to process}
+ \Guard{grd2}{false}{$emitted\_event \notin{} emitted\_events[\{source\_smart\_contract\}]$}{true}{\\The smart contract will always emit a new event}
}
\ACTIONS{true}{
- \Action{act1}{$triggered\_events \bcmeq{} triggered\_events \bunion{} \{source\_smart\_contract \mapsto{} cross\_chain\_event\}$}{true}{\\The smart contract triggers a new event related to the transaction processing}
- \Action{act2}{$received\_transactions \bcmeq{} received\_transactions \setminus{} \{source\_smart\_contract \mapsto{} transaction\}$}{true}{\\The smart contract processed the transaction}
+ \Action{act1}{$emitted\_events \bcmeq{} emitted\_events \bunion{} \{source\_smart\_contract \mapsto{} emitted\_event\}$}{true}{\\The smart contract emits a new event related to the transaction processing}
+ \Action{act2}{$received\_source\_transactions \bcmeq{} received\_source\_transactions \setminus{} \{source\_smart\_contract \mapsto{} transaction\}$}{true}{\\The smart contract processed the transaction}
}
}
-\EVT{LISTEN\_CC\_TX\_EVENT}{false}{ordinary}{}{}{
+\EVT{LISTEN\_EVENT}{false}{ordinary}{}{}{
\ANY{
- \Param{cross\_chain\_event}{true}{}
- \Param{cross\_chain\_transaction}{true}{}
+ \Param{emitted\_event}{true}{}
+ \Param{pending\_event}{true}{}
}
\GUARDS{true}{
- \Guard{grd1}{false}{$source\_smart\_contract \mapsto{} cross\_chain\_event \in{} triggered\_events$}{true}{\\The smart contract has triggered an event}
+ \Guard{grd1}{false}{$source\_smart\_contract \mapsto{} emitted\_event \in{} emitted\_events$}{true}{\\The smart contract has emitted an event}
\Guard{grd2}{false}{$gateway \mapsto{} source\_smart\_contract \in{} subscriptions$}{true}{\\Exist a subscription to the smart contract events}
- \Guard{grd3}{false}{$gateway \mapsto{} cross\_chain\_transaction \notin{} gateway\_pending\_transactions$}{true}{\\The event was not already listened}
+ \Guard{grd3}{false}{$gateway \mapsto{} pending\_event \notin{} gateway\_pending\_events$}{true}{\\The event was not already listened}
}
\ACTIONS{true}{
- \Action{act1}{$gateway\_pending\_transactions \bcmeq{} gateway\_pending\_transactions \bunion{} \{gateway \mapsto{} cross\_chain\_transaction\}$}{true}{\\The event is added to the cross-chain transactions to be processed by the gateway}
- \Action{act2}{$triggered\_events \bcmeq{} triggered\_events \setminus{} \{source\_smart\_contract \mapsto{} cross\_chain\_event\}$}{true}{\\The event is removed from the pending events to listen}
+ \Action{act1}{$gateway\_pending\_events \bcmeq{} gateway\_pending\_events \bunion{} \{gateway \mapsto{} pending\_event\}$}{true}{\\The event is added to the pending events to be processed by the gateway}
+ \Action{act2}{$emitted\_events \bcmeq{} emitted\_events \setminus{} \{source\_smart\_contract \mapsto{} emitted\_event\}$}{true}{\\The event is removed from the pending events to listen}
}
}
-\EVT{SUBMIT\_CC\_TX}{false}{ordinary}{}{}{
+\EVT{SUBMIT\_TX}{false}{ordinary}{}{}{
\ANY{
- \Param{cross\_chain\_transaction}{true}{}
+ \Param{pending\_event}{true}{}
+ \Param{transaction}{true}{}
}
\GUARDS{true}{
- \Guard{grd1}{false}{$gateway \mapsto{} cross\_chain\_transaction \in{} gateway\_pending\_transactions$}{true}{\\There is one pending cross-chain transaction to process}
+ \Guard{grd1}{false}{$gateway \mapsto{} pending\_event \in{} gateway\_pending\_events$}{true}{\\There is one pending event to be processed}
+ \Guard{grd2}{false}{$transaction \in{} TARGET\_TRANSACTIONS$}{true}{}
}
\ACTIONS{true}{
- \Action{act1}{$received\_cross\_chain\_transactions \bcmeq{} received\_cross\_chain\_transactions \bunion{} \{target\_smart\_contract \mapsto{} cross\_chain\_transaction\}$}{true}{\\The cross-chain transaction is received by the target smart contract}
- \Action{act2}{$gateway\_pending\_transactions \bcmeq{} gateway\_pending\_transactions \setminus{} \{gateway \mapsto{} cross\_chain\_transaction\}$}{true}{\\Remove the cross-chain transaction to the pending transactions of the Gateway}
+ \Action{act1}{$received\_target\_transactions \bcmeq{} received\_target\_transactions \bunion{} \{target\_smart\_contract \mapsto{} transaction\}$}{true}{\\The transaction is received by the target smart contract}
+ \Action{act2}{$gateway\_pending\_events \bcmeq{} gateway\_pending\_events \setminus{} \{gateway \mapsto{} pending\_event\}$}{true}{\\Remove the event from the pending events of the gateway}
}
}
}
diff --git a/gateway-event-b/latex/CCTx_Ethereum_Fabric_Animation_m3.tex b/gateway-event-b/latex/CCTx_Ethereum_Fabric_Animation_m3.tex
new file mode 100644
index 0000000000000000000000000000000000000000..6c024e9a9d181d5c7969150678f069130a68edc6
--- /dev/null
+++ b/gateway-event-b/latex/CCTx_Ethereum_Fabric_Animation_m3.tex
@@ -0,0 +1,158 @@
+\documentclass[10pt,a4paper]{report}
+\usepackage{bsymb,b2latex}
+\begin{document}
+\SingleHeader{CCTx\_Ethereum\_Fabric\_Animation\_m3}
+\MACHINE{CCTx\_Ethereum\_Fabric\_Animation\_m3}{CCTx\_Ethereum\_Fabric\_m2}{CCTx\_Ethereum\_Fabric\_c2}{}
+\VARIABLES{
+ \Variable{received\_source\_transactions}{}
+ \Variable{emitted\_events}{}
+ \Variable{subscriptions}{}
+ \Variable{gateway\_pending\_events}{}
+ \Variable{received\_target\_transactions}{}
+ \Variable{authenticated\_users}{}
+ \Variable{authenticated\_transactions}{}
+ \Variable{grants}{}
+ \Variable{subscribed}{}
+ \Variable{initiated}{}
+ \Variable{emitted}{}
+ \Variable{gateway\_processing}{}
+ \Variable{submit\_cc\_tx}{}
+ \Variable{user\_created}{}
+ \Variable{write\_granted}{}
+}
+\INVARIANTS{
+ \Invariant{inv11}{false}{$subscribed \in{} \{0,1\}$}{}
+ \Invariant{inv12}{false}{$initiated \in{} \{0,1\}$}{}
+ \Invariant{inv13}{false}{$emitted \in{} \{0,1\}$}{}
+ \Invariant{inv14}{false}{$gateway\_processing \in{} \{0,1\}$}{}
+ \Invariant{inv15}{false}{$submit\_cc\_tx \in{} \{0,1\}$}{}
+ \Invariant{inv16}{false}{$user\_created \in{} \{0,1\}$}{}
+ \Invariant{inv17}{false}{$write\_granted \in{} \{0,1\}$}{}
+}
+\EVENTS{
+\INITIALISATION{true}{}{
+ \ACTIONS{false}{
+ \Action{act1}{$received\_source\_transactions \bcmeq{} \emptyset{}$}{false}{}
+ \Action{act2}{$emitted\_events \bcmeq{} \emptyset{}$}{false}{}
+ \Action{act3}{$subscriptions \bcmeq{} \emptyset{}$}{false}{}
+ \Action{act4}{$gateway\_pending\_events \bcmeq{} \emptyset{}$}{false}{}
+ \Action{act6}{$received\_target\_transactions \bcmeq{} \emptyset{}$}{false}{}
+ \Action{act11}{$authenticated\_users \bcmeq{} \emptyset{}$}{false}{}
+ \Action{act12}{$authenticated\_transactions \bcmeq{} \emptyset{}$}{false}{}
+ \Action{act14}{$grants \bcmeq{} \emptyset{}$}{false}{}
+ \Action{act31}{$subscribed \bcmeq{} 0$}{true}{}
+ \Action{act32}{$initiated \bcmeq{} 0$}{true}{}
+ \Action{act33}{$emitted \bcmeq{} 0$}{true}{}
+ \Action{act34}{$gateway\_processing \bcmeq{} 0$}{true}{}
+ \Action{act35}{$submit\_cc\_tx \bcmeq{} 0$}{true}{}
+ \Action{act36}{$user\_created \bcmeq{} 0$}{true}{}
+ \Action{act37}{$write\_granted \bcmeq{} 0$}{true}{}
+ }
+}
+\EVT{SUBSCRIBE\_SMART\_CONTRACT\_EVENTS\_IN\_ETHEREUM}{true}{ordinary}{SUBSCRIBE\_SMART\_CONTRACT\_EVENTS\_IN\_ETHEREUM}{}{
+ \GUARDS{false}{
+ \Guard{grd1}{false}{$gateway \mapsto{} source\_smart\_contract \notin{} subscriptions$}{false}{\\The gateway is not already subscribed to the smart contract events}
+ }
+ \ACTIONS{true}{
+ \Action{act1}{$subscriptions \bcmeq{} subscriptions \bunion{} \{gateway \mapsto{} source\_smart\_contract\}$}{false}{\\The gateway is subscribed to listen to the smart contract events}
+ \Action{act31}{$subscribed \bcmeq{} 1$}{true}{}
+ }
+}
+\EVT{INITIATE\_CC\_TX\_IN\_ETHEREUM}{true}{ordinary}{INITIATE\_CC\_TX\_IN\_ETHEREUM}{}{
+ \ANY{
+ \Param{transaction}{false}{}
+ }
+ \GUARDS{true}{
+ \Guard{grd1}{false}{$transaction \in{} SOURCE\_TRANSACTIONS$}{false}{}
+ \Guard{grd3}{false}{$transaction \notin{} received\_source\_transactions[\{source\_smart\_contract\}]$}{false}{\\The transaction was not received by the smart contract}
+ }
+ \ACTIONS{true}{
+ \Action{act1}{$received\_source\_transactions \bcmeq{} received\_source\_transactions \bunion{} \{source\_smart\_contract \mapsto{} transaction\}$}{false}{\\Add the transaction to the received transactions of the smart contract}
+ \Action{act31}{$initiated \bcmeq{} 1$}{true}{}
+ \Action{act32}{$submit\_cc\_tx \bcmeq{} 0$}{true}{}
+ }
+}
+\EVT{EMIT\_EVENT\_IN\_ETHEREUM}{true}{ordinary}{EMIT\_EVENT\_IN\_ETHEREUM}{}{
+ \ANY{
+ \Param{transaction}{false}{}
+ \Param{emitted\_event}{false}{}
+ }
+ \GUARDS{true}{
+ \Guard{grd1}{false}{$source\_smart\_contract \mapsto{} transaction \in{} received\_source\_transactions$}{false}{\\The smart contract has a pending transaction to process}
+ \Guard{grd2}{false}{$emitted\_event \notin{} emitted\_events[\{source\_smart\_contract\}]$}{false}{\\The smart contract will always emit a new event}
+ }
+ \ACTIONS{true}{
+ \Action{act1}{$emitted\_events \bcmeq{} emitted\_events \bunion{} \{source\_smart\_contract \mapsto{} emitted\_event\}$}{false}{\\The smart contract emits a new event related to the transaction processing}
+ \Action{act2}{$received\_source\_transactions \bcmeq{} received\_source\_transactions \setminus{} \{source\_smart\_contract \mapsto{} transaction\}$}{false}{\\The smart contract processed the transaction}
+ \Action{act31}{$emitted \bcmeq{} 1$}{true}{}
+ \Action{act32}{$initiated \bcmeq{} 0$}{true}{}
+ \Action{act33}{$submit\_cc\_tx \bcmeq{} 0$}{true}{}
+ }
+}
+\EVT{LISTEN\_EVENT\_IN\_ETHEREUM}{true}{ordinary}{LISTEN\_EVENT\_IN\_ETHEREUM}{}{
+ \ANY{
+ \Param{emitted\_event}{false}{}
+ \Param{pending\_event}{false}{}
+ }
+ \GUARDS{true}{
+ \Guard{grd1}{false}{$source\_smart\_contract \mapsto{} emitted\_event \in{} emitted\_events$}{false}{\\The smart contract has emitted an event}
+ \Guard{grd2}{false}{$gateway \mapsto{} source\_smart\_contract \in{} subscriptions$}{false}{\\Exist a subscription to the smart contract events}
+ \Guard{grd3}{false}{$gateway \mapsto{} pending\_event \notin{} gateway\_pending\_events$}{false}{\\The event was not already listened}
+ }
+ \ACTIONS{true}{
+ \Action{act1}{$gateway\_pending\_events \bcmeq{} gateway\_pending\_events \bunion{} \{gateway \mapsto{} pending\_event\}$}{false}{\\The event is added to the pending events to be processed by the gateway}
+ \Action{act2}{$emitted\_events \bcmeq{} emitted\_events \setminus{} \{source\_smart\_contract \mapsto{} emitted\_event\}$}{false}{\\The event is removed from the pending events to listen}
+ \Action{act31}{$gateway\_processing \bcmeq{} 1$}{true}{}
+ \Action{act32}{$emitted \bcmeq{} 0$}{true}{}
+ \Action{act33}{$submit\_cc\_tx \bcmeq{} 0$}{true}{}
+ }
+}
+\EVT{SUBMIT\_TX\_TO\_FABRIC}{true}{ordinary}{SUBMIT\_TX\_TO\_FABRIC}{}{
+ \ANY{
+ \Param{pending\_event}{false}{}
+ \Param{transaction}{false}{}
+ \Param{user}{false}{}
+ }
+ \GUARDS{true}{
+ \Guard{grd1}{false}{$gateway \mapsto{} pending\_event \in{} gateway\_pending\_events$}{false}{\\There is one pending event to be processed}
+ \Guard{grd2}{false}{$transaction \in{} TARGET\_TRANSACTIONS$}{false}{}
+ \Guard{grd11}{false}{$user \in{} authenticated\_users$}{false}{\\Only allow authenticated users (REQ6)}
+ \Guard{grd12}{false}{$user \mapsto{} write \in{} grants$}{false}{\\Only allow authorized users (REQ7)}
+ }
+ \ACTIONS{true}{
+ \Action{act1}{$received\_target\_transactions \bcmeq{} received\_target\_transactions \bunion{} \{target\_smart\_contract \mapsto{} transaction\}$}{false}{\\The transaction is received by the target smart contract}
+ \Action{act2}{$gateway\_pending\_events \bcmeq{} gateway\_pending\_events \setminus{} \{gateway \mapsto{} pending\_event\}$}{false}{\\Remove the event from the pending events of the gateway}
+ \Action{act11}{$authenticated\_transactions(target\_smart\_contract \mapsto{} transaction) \bcmeq{} user$}{false}{\\Every submitted transaction to Fabric must be authenticated}
+ \Action{act31}{$submit\_cc\_tx \bcmeq{} 1$}{true}{}
+ \Action{act32}{$gateway\_processing \bcmeq{} 0$}{true}{}
+ }
+}
+\EVT{CREATE\_GATEWAY\_USER}{true}{ordinary}{CREATE\_GATEWAY\_USER}{}{
+ \GUARDS{false}{
+ \Guard{grd1}{false}{$gateway\_user \notin{} authenticated\_users$}{false}{}
+ }
+ \ACTIONS{true}{
+ \Action{act1}{$authenticated\_users \bcmeq{} authenticated\_users \bunion{} \{gateway\_user\}$}{false}{\\Create credentials for a user (e.g. gateway) to authenticate them (REQ2)}
+ \Action{act31}{$user\_created \bcmeq{} 1$}{true}{}
+ }
+}
+\EVT{GRANT\_PERMISSION}{true}{ordinary}{GRANT\_PERMISSION}{}{
+ \ANY{
+ \Param{permission}{false}{}
+ \Param{user}{false}{}
+ }
+ \GUARDS{true}{
+ \Guard{grd1}{false}{$permission \in{} PERMISSIONS$}{false}{}
+ \Guard{grd2}{false}{$user \in{} authenticated\_users$}{false}{}
+ \Guard{grd3}{false}{$user \mapsto{} permission \notin{} grants$}{false}{}
+ \Guard{grd31}{false}{$user = gateway\_user$}{true}{}
+ \Guard{grd32}{false}{$permission = write$}{true}{}
+ }
+ \ACTIONS{true}{
+ \Action{act1}{$grants \bcmeq{} grants \bunion{} \{user \mapsto{} permission\}$}{false}{\\Grant permissions (e.g. write) to users (e.g. gateway) in Fabric (REQ3)}
+ \Action{act31}{$write\_granted \bcmeq{} 1$}{true}{}
+ }
+}
+}
+\END
+\end{document}
diff --git a/gateway-event-b/latex/CCTx_Ethereum_Fabric_c2.tex b/gateway-event-b/latex/CCTx_Ethereum_Fabric_c2.tex
index b5b4ec02d5da236cd53d1ce546293f0913b57c5c..3feadf513f3b21d94fd331cd069c6f0548a783ba 100644
--- a/gateway-event-b/latex/CCTx_Ethereum_Fabric_c2.tex
+++ b/gateway-event-b/latex/CCTx_Ethereum_Fabric_c2.tex
@@ -13,8 +13,8 @@
\Constant{gateway\_user}{}
}
\AXIOMS{
- \Axiom{axm11}{false}{$partition(PERMISSIONS, \{read\}, \{write\})$}{\\Two only types of permissions exist: read and write}
- \Axiom{axm12}{false}{$gateway\_user \in{} USERS$}{\\The gateway has an Hyperledger Fabric user}
+ \Axiom{axm11}{false}{$partition(PERMISSIONS, \{read\}, \{write\})$}{\\Only two types of permissions exist: read and write (REQ1)}
+ \Axiom{axm12}{false}{$gateway\_user \in{} USERS$}{\\The gateway has a Fabric user}
}
\END
\end{document}
diff --git a/gateway-event-b/latex/CCTx_Ethereum_Fabric_m2.tex b/gateway-event-b/latex/CCTx_Ethereum_Fabric_m2.tex
index 238080c9bba50341aeeb779e4b83b9fd18b8fd80..3ace914837e4fa7ffbb2230bae982d8775ffe3f2 100644
--- a/gateway-event-b/latex/CCTx_Ethereum_Fabric_m2.tex
+++ b/gateway-event-b/latex/CCTx_Ethereum_Fabric_m2.tex
@@ -4,30 +4,30 @@
\SingleHeader{CCTx\_Ethereum\_Fabric\_m2}
\MACHINE{CCTx\_Ethereum\_Fabric\_m2}{CCTx\_Abstract\_DLT\_m1}{CCTx\_Ethereum\_Fabric\_c2}{}
\VARIABLES{
- \Variable{received\_transactions}{}
- \Variable{triggered\_events}{}
+ \Variable{received\_source\_transactions}{}
+ \Variable{emitted\_events}{}
\Variable{subscriptions}{}
- \Variable{gateway\_pending\_transactions}{}
- \Variable{received\_cross\_chain\_transactions}{}
+ \Variable{gateway\_pending\_events}{}
+ \Variable{received\_target\_transactions}{}
\Variable{authenticated\_users}{}
\Variable{authenticated\_transactions}{}
\Variable{grants}{}
}
\INVARIANTS{
\Invariant{inv11}{false}{$authenticated\_users \subseteq{} USERS$}{\\Authenticated users are a subset of all the possible users}
- \Invariant{inv12}{false}{$authenticated\_transactions \in{} received\_cross\_chain\_transactions \tfun{} authenticated\_users$}{\\Authenticated transactions are received transactions submitted by an authenticated user}
- \Invariant{inv13}{false}{$\\\forall{} tx \qdot{} tx \in{} received\_cross\_chain\_transactions \limp{} (\exists{} u \qdot{} u \in{}\\~ authenticated\_users \land{} tx \mapsto{} u \in{} authenticated\_transactions)$}{\\Every submitted transaction to Fabric must be authenticated (RQ4)}
+ \Invariant{inv12}{false}{$authenticated\_transactions \in{} received\_target\_transactions \tfun{} authenticated\_users$}{\\Authenticated transactions are received transactions submitted by an authenticated user}
+ \Invariant{inv13}{false}{$\\\forall{} tx \qdot{} tx \in{} received\_target\_transactions \limp{} (\exists{} u \qdot{} u \in{}\\~ authenticated\_users \land{} tx \mapsto{} u \in{} authenticated\_transactions)$}{\\Every submitted transaction to Fabric must be authenticated (REQ4)}
\Invariant{inv14}{false}{$grants \in{} authenticated\_users \rel{} PERMISSIONS$}{\\Users with read or write permissions}
- \Invariant{inv15}{false}{$\forall{} u \qdot{} u \in{} authenticated\_transactions[received\_cross\_chain\_transactions] \limp{} u \mapsto{} write \in{} grants$}{\\Authenticated users that submitted a transaction must have write permissions (RQ5)}
+ \Invariant{inv15}{false}{$\forall{} u \qdot{} u \in{} authenticated\_transactions[received\_target\_transactions] \limp{} u \mapsto{} write \in{} grants$}{\\Authenticated users that submitted a transaction must have write permissions (REQ5)}
}
\EVENTS{
\INITIALISATION{true}{}{
\ACTIONS{false}{
- \Action{act1}{$received\_transactions \bcmeq{} \emptyset{}$}{false}{}
- \Action{act2}{$triggered\_events \bcmeq{} \emptyset{}$}{false}{}
+ \Action{act1}{$received\_source\_transactions \bcmeq{} \emptyset{}$}{false}{}
+ \Action{act2}{$emitted\_events \bcmeq{} \emptyset{}$}{false}{}
\Action{act3}{$subscriptions \bcmeq{} \emptyset{}$}{false}{}
- \Action{act4}{$gateway\_pending\_transactions \bcmeq{} \emptyset{}$}{false}{}
- \Action{act6}{$received\_cross\_chain\_transactions \bcmeq{} \emptyset{}$}{false}{}
+ \Action{act4}{$gateway\_pending\_events \bcmeq{} \emptyset{}$}{false}{}
+ \Action{act6}{$received\_target\_transactions \bcmeq{} \emptyset{}$}{false}{}
\Action{act11}{$authenticated\_users \bcmeq{} \emptyset{}$}{true}{}
\Action{act12}{$authenticated\_transactions \bcmeq{} \emptyset{}$}{true}{}
\Action{act14}{$grants \bcmeq{} \emptyset{}$}{true}{}
@@ -46,56 +46,58 @@
\Param{transaction}{false}{}
}
\GUARDS{true}{
- \Guard{grd1}{false}{$transaction \in{} TRANSACTIONS$}{false}{}
- \Guard{grd3}{false}{$transaction \notin{} received\_transactions[\{source\_smart\_contract\}]$}{false}{\\The transaction was not received by the smart contract}
+ \Guard{grd1}{false}{$transaction \in{} SOURCE\_TRANSACTIONS$}{false}{}
+ \Guard{grd3}{false}{$transaction \notin{} received\_source\_transactions[\{source\_smart\_contract\}]$}{false}{\\The transaction was not received by the smart contract}
}
\ACTIONS{true}{
- \Action{act1}{$received\_transactions \bcmeq{} received\_transactions \bunion{} \{source\_smart\_contract \mapsto{} transaction\}$}{false}{\\Add the transaction to the received transactions of the smart contract}
+ \Action{act1}{$received\_source\_transactions \bcmeq{} received\_source\_transactions \bunion{} \{source\_smart\_contract \mapsto{} transaction\}$}{false}{\\Add the transaction to the received transactions of the smart contract}
}
}
-\EVT{TRIGGER\_CC\_TX\_EVENT\_IN\_ETHEREUM}{true}{ordinary}{TRIGGER\_CC\_TX\_EVENT}{}{
+\EVT{EMIT\_EVENT\_IN\_ETHEREUM}{true}{ordinary}{EMIT\_EVENT}{}{
\ANY{
\Param{transaction}{false}{}
- \Param{cross\_chain\_event}{false}{}
+ \Param{emitted\_event}{false}{}
}
\GUARDS{true}{
- \Guard{grd1}{false}{$source\_smart\_contract \mapsto{} transaction \in{} received\_transactions$}{false}{\\The smart contract has a pending transaction to process}
- \Guard{grd2}{false}{$cross\_chain\_event \notin{} triggered\_events[\{source\_smart\_contract\}]$}{false}{\\The smart contract will always trigger a new event}
+ \Guard{grd1}{false}{$source\_smart\_contract \mapsto{} transaction \in{} received\_source\_transactions$}{false}{\\The smart contract has a pending transaction to process}
+ \Guard{grd2}{false}{$emitted\_event \notin{} emitted\_events[\{source\_smart\_contract\}]$}{false}{\\The smart contract will always emit a new event}
}
\ACTIONS{true}{
- \Action{act1}{$triggered\_events \bcmeq{} triggered\_events \bunion{} \{source\_smart\_contract \mapsto{} cross\_chain\_event\}$}{false}{\\The smart contract triggers a new event related to the transaction processing}
- \Action{act2}{$received\_transactions \bcmeq{} received\_transactions \setminus{} \{source\_smart\_contract \mapsto{} transaction\}$}{false}{\\The smart contract processed the transaction}
+ \Action{act1}{$emitted\_events \bcmeq{} emitted\_events \bunion{} \{source\_smart\_contract \mapsto{} emitted\_event\}$}{false}{\\The smart contract emits a new event related to the transaction processing}
+ \Action{act2}{$received\_source\_transactions \bcmeq{} received\_source\_transactions \setminus{} \{source\_smart\_contract \mapsto{} transaction\}$}{false}{\\The smart contract processed the transaction}
}
}
-\EVT{LISTEN\_CC\_TX\_EVENT\_IN\_ETHEREUM}{true}{ordinary}{LISTEN\_CC\_TX\_EVENT}{}{
+\EVT{LISTEN\_EVENT\_IN\_ETHEREUM}{true}{ordinary}{LISTEN\_EVENT}{}{
\ANY{
- \Param{cross\_chain\_event}{false}{}
- \Param{cross\_chain\_transaction}{false}{}
+ \Param{emitted\_event}{false}{}
+ \Param{pending\_event}{false}{}
}
\GUARDS{true}{
- \Guard{grd1}{false}{$source\_smart\_contract \mapsto{} cross\_chain\_event \in{} triggered\_events$}{false}{\\The smart contract has triggered an event}
+ \Guard{grd1}{false}{$source\_smart\_contract \mapsto{} emitted\_event \in{} emitted\_events$}{false}{\\The smart contract has emitted an event}
\Guard{grd2}{false}{$gateway \mapsto{} source\_smart\_contract \in{} subscriptions$}{false}{\\Exist a subscription to the smart contract events}
- \Guard{grd3}{false}{$gateway \mapsto{} cross\_chain\_transaction \notin{} gateway\_pending\_transactions$}{false}{\\The event was not already listened}
+ \Guard{grd3}{false}{$gateway \mapsto{} pending\_event \notin{} gateway\_pending\_events$}{false}{\\The event was not already listened}
}
\ACTIONS{true}{
- \Action{act1}{$gateway\_pending\_transactions \bcmeq{} gateway\_pending\_transactions \bunion{} \{gateway \mapsto{} cross\_chain\_transaction\}$}{false}{\\The event is added to the cross-chain transactions to be processed by the gateway}
- \Action{act2}{$triggered\_events \bcmeq{} triggered\_events \setminus{} \{source\_smart\_contract \mapsto{} cross\_chain\_event\}$}{false}{\\The event is removed from the pending events to listen}
+ \Action{act1}{$gateway\_pending\_events \bcmeq{} gateway\_pending\_events \bunion{} \{gateway \mapsto{} pending\_event\}$}{false}{\\The event is added to the pending events to be processed by the gateway}
+ \Action{act2}{$emitted\_events \bcmeq{} emitted\_events \setminus{} \{source\_smart\_contract \mapsto{} emitted\_event\}$}{false}{\\The event is removed from the pending events to listen}
}
}
-\EVT{SUBMIT\_CC\_TX\_TO\_FABRIC}{true}{ordinary}{SUBMIT\_CC\_TX}{}{
+\EVT{SUBMIT\_TX\_TO\_FABRIC}{true}{ordinary}{SUBMIT\_TX}{}{
\ANY{
- \Param{cross\_chain\_transaction}{false}{}
+ \Param{pending\_event}{false}{}
+ \Param{transaction}{false}{}
\Param{user}{true}{}
}
\GUARDS{true}{
- \Guard{grd1}{false}{$gateway \mapsto{} cross\_chain\_transaction \in{} gateway\_pending\_transactions$}{false}{\\There is one pending cross-chain transaction to process}
- \Guard{grd11}{false}{$user \in{} authenticated\_users$}{true}{\\Only allow authenticated users (RQ6)}
- \Guard{grd12}{false}{$user \mapsto{} write \in{} grants$}{true}{\\Only allow authorized users (RQ7)}
+ \Guard{grd1}{false}{$gateway \mapsto{} pending\_event \in{} gateway\_pending\_events$}{false}{\\There is one pending event to be processed}
+ \Guard{grd2}{false}{$transaction \in{} TARGET\_TRANSACTIONS$}{false}{}
+ \Guard{grd11}{false}{$user \in{} authenticated\_users$}{true}{\\Only allow authenticated users (REQ6)}
+ \Guard{grd12}{false}{$user \mapsto{} write \in{} grants$}{true}{\\Only allow authorized users (REQ7)}
}
\ACTIONS{true}{
- \Action{act1}{$received\_cross\_chain\_transactions \bcmeq{} received\_cross\_chain\_transactions \bunion{} \{target\_smart\_contract \mapsto{} cross\_chain\_transaction\}$}{false}{\\The cross-chain transaction is received by the target smart contract}
- \Action{act2}{$gateway\_pending\_transactions \bcmeq{} gateway\_pending\_transactions \setminus{} \{gateway \mapsto{} cross\_chain\_transaction\}$}{false}{\\Remove the cross-chain transaction to the pending transactions of the Gateway}
- \Action{act11}{$authenticated\_transactions(target\_smart\_contract \mapsto{} cross\_chain\_transaction) \bcmeq{} user$}{true}{\\Audit user that submitted a transaction to a smart contract (RQ4)}
+ \Action{act1}{$received\_target\_transactions \bcmeq{} received\_target\_transactions \bunion{} \{target\_smart\_contract \mapsto{} transaction\}$}{false}{\\The transaction is received by the target smart contract}
+ \Action{act2}{$gateway\_pending\_events \bcmeq{} gateway\_pending\_events \setminus{} \{gateway \mapsto{} pending\_event\}$}{false}{\\Remove the event from the pending events of the gateway}
+ \Action{act11}{$authenticated\_transactions(target\_smart\_contract \mapsto{} transaction) \bcmeq{} user$}{true}{\\Every submitted transaction to Fabric must be authenticated}
}
}
\EVT{CREATE\_GATEWAY\_USER}{false}{ordinary}{}{}{
@@ -103,7 +105,7 @@
\Guard{grd1}{false}{$gateway\_user \notin{} authenticated\_users$}{true}{}
}
\ACTIONS{true}{
- \Action{act1}{$authenticated\_users \bcmeq{} authenticated\_users \bunion{} \{gateway\_user\}$}{true}{\\Create credentials for a user (e.g. gateway) to authenticate them (RQ2)}
+ \Action{act1}{$authenticated\_users \bcmeq{} authenticated\_users \bunion{} \{gateway\_user\}$}{true}{\\Create credentials for a user (e.g. gateway) to authenticate them (REQ2)}
}
}
\EVT{GRANT\_PERMISSION}{false}{ordinary}{}{}{
@@ -117,7 +119,7 @@
\Guard{grd3}{false}{$user \mapsto{} permission \notin{} grants$}{true}{}
}
\ACTIONS{true}{
- \Action{act1}{$grants \bcmeq{} grants \bunion{} \{user \mapsto{} permission\}$}{true}{\\Grant permissions (e.g. write) to users (e.g. gateway) in Fabric (RQ3)}
+ \Action{act1}{$grants \bcmeq{} grants \bunion{} \{user \mapsto{} permission\}$}{true}{\\Grant permissions (e.g. write) to users (e.g. gateway) in Fabric (REQ3)}
}
}
}
diff --git a/gateway-event-b/latex/CCTx_Fabric_Ethereum_Animation_m3.tex b/gateway-event-b/latex/CCTx_Fabric_Ethereum_Animation_m3.tex
new file mode 100644
index 0000000000000000000000000000000000000000..7a3d1248368d04c3b6cd1c8ed33473e4a4509bd1
--- /dev/null
+++ b/gateway-event-b/latex/CCTx_Fabric_Ethereum_Animation_m3.tex
@@ -0,0 +1,177 @@
+\documentclass[10pt,a4paper]{report}
+\usepackage{bsymb,b2latex}
+\begin{document}
+\SingleHeader{CCTx\_Fabric\_Ethereum\_Animation\_m3}
+\MACHINE{CCTx\_Fabric\_Ethereum\_Animation\_m3}{CCTx\_Fabric\_Ethereum\_m2}{CCTx\_Fabric\_Ethereum\_c2}{}
+\VARIABLES{
+ \Variable{received\_source\_transactions}{}
+ \Variable{emitted\_events}{}
+ \Variable{subscriptions}{}
+ \Variable{gateway\_pending\_events}{}
+ \Variable{received\_target\_transactions}{}
+ \Variable{accounts}{}
+ \Variable{subscribed}{}
+ \Variable{initiated}{}
+ \Variable{emitted}{}
+ \Variable{gateway\_processing}{}
+ \Variable{submit\_cc\_tx}{}
+ \Variable{wallet\_created}{}
+ \Variable{wallet\_amount}{}
+}
+\INVARIANTS{
+ \Invariant{inv31}{false}{$subscribed \in{} \{0,1\}$}{}
+ \Invariant{inv32}{false}{$initiated \in{} \{0,1\}$}{}
+ \Invariant{inv33}{false}{$emitted \in{} \{0,1\}$}{}
+ \Invariant{inv34}{false}{$gateway\_processing \in{} \{0,1\}$}{}
+ \Invariant{inv35}{false}{$submit\_cc\_tx \in{} \{0,1\}$}{}
+ \Invariant{inv36}{false}{$wallet\_created \in{} \{0,1\}$}{}
+ \Invariant{inv37}{false}{$wallet\_amount \in{} \nat{}$}{}
+}
+\EVENTS{
+\INITIALISATION{true}{}{
+ \ACTIONS{false}{
+ \Action{act1}{$received\_source\_transactions \bcmeq{} \emptyset{}$}{false}{}
+ \Action{act2}{$emitted\_events \bcmeq{} \emptyset{}$}{false}{}
+ \Action{act3}{$subscriptions \bcmeq{} \emptyset{}$}{false}{}
+ \Action{act4}{$gateway\_pending\_events \bcmeq{} \emptyset{}$}{false}{}
+ \Action{act6}{$received\_target\_transactions \bcmeq{} \emptyset{}$}{false}{}
+ \Action{act11}{$accounts \bcmeq{} \emptyset{}$}{false}{}
+ \Action{init\_subscribed}{$subscribed \bcmeq{} 0$}{true}{}
+ \Action{init\_initiated}{$initiated \bcmeq{} 0$}{true}{}
+ \Action{init\_emitted}{$emitted \bcmeq{} 0$}{true}{}
+ \Action{init\_gateway\_processing}{$gateway\_processing \bcmeq{} 0$}{true}{}
+ \Action{init\_submit\_cc\_tx}{$submit\_cc\_tx \bcmeq{} 0$}{true}{}
+ \Action{init\_wallet\_created}{$wallet\_created \bcmeq{} 0$}{true}{}
+ \Action{init\_wallet\_amount}{$wallet\_amount \bcmeq{} 0$}{true}{}
+ }
+}
+\EVT{SUBSCRIBE\_SMART\_CONTRACT\_EVENTS\_IN\_FABRIC}{true}{ordinary}{SUBSCRIBE\_SMART\_CONTRACT\_EVENTS\_IN\_FABRIC}{}{
+ \GUARDS{false}{
+ \Guard{grd1}{false}{$gateway \mapsto{} source\_smart\_contract \notin{} subscriptions$}{false}{\\The gateway is not already subscribed to the smart contract events}
+ }
+ \ACTIONS{true}{
+ \Action{act1}{$subscriptions \bcmeq{} subscriptions \bunion{} \{gateway \mapsto{} source\_smart\_contract\}$}{false}{\\The gateway is subscribed to listen to the smart contract events}
+ \Action{act111}{$subscribed \bcmeq{} 1$}{true}{}
+ }
+}
+\EVT{INITIATE\_CC\_TX\_IN\_FABRIC}{true}{ordinary}{INITIATE\_CC\_TX\_IN\_FABRIC}{}{
+ \ANY{
+ \Param{transaction}{false}{}
+ }
+ \GUARDS{true}{
+ \Guard{grd1}{false}{$transaction \in{} SOURCE\_TRANSACTIONS$}{false}{}
+ \Guard{grd3}{false}{$transaction \notin{} received\_source\_transactions[\{source\_smart\_contract\}]$}{false}{\\The transaction was not received by the smart contract}
+ }
+ \ACTIONS{true}{
+ \Action{act1}{$received\_source\_transactions \bcmeq{} received\_source\_transactions \bunion{} \{source\_smart\_contract \mapsto{} transaction\}$}{false}{\\Add the transaction to the received transactions of the smart contract}
+ \Action{act31}{$initiated \bcmeq{} 1$}{true}{}
+ \Action{act32}{$submit\_cc\_tx \bcmeq{} 0$}{true}{}
+ }
+}
+\EVT{EMIT\_EVENT\_IN\_FABRIC}{true}{ordinary}{EMIT\_EVENT\_IN\_FABRIC}{}{
+ \ANY{
+ \Param{transaction}{false}{}
+ \Param{emitted\_event}{false}{}
+ }
+ \GUARDS{true}{
+ \Guard{grd1}{false}{$source\_smart\_contract \mapsto{} transaction \in{} received\_source\_transactions$}{false}{\\The smart contract has a pending transaction to process}
+ \Guard{grd2}{false}{$emitted\_event \notin{} emitted\_events[\{source\_smart\_contract\}]$}{false}{\\The smart contract will always emit a new event}
+ }
+ \ACTIONS{true}{
+ \Action{act1}{$emitted\_events \bcmeq{} emitted\_events \bunion{} \{source\_smart\_contract \mapsto{} emitted\_event\}$}{false}{\\The smart contract emits a new event related to the transaction processing}
+ \Action{act2}{$received\_source\_transactions \bcmeq{} received\_source\_transactions \setminus{} \{source\_smart\_contract \mapsto{} transaction\}$}{false}{\\The smart contract processed the transaction}
+ \Action{act31}{$emitted \bcmeq{} 1$}{true}{}
+ \Action{act32}{$initiated \bcmeq{} 0$}{true}{}
+ \Action{act33}{$submit\_cc\_tx \bcmeq{} 0$}{true}{}
+ }
+}
+\EVT{LISTEN\_EVENT\_IN\_FABRIC}{true}{ordinary}{LISTEN\_EVENT\_IN\_FABRIC}{}{
+ \ANY{
+ \Param{emitted\_event}{false}{}
+ \Param{pending\_event}{false}{}
+ }
+ \GUARDS{true}{
+ \Guard{grd1}{false}{$source\_smart\_contract \mapsto{} emitted\_event \in{} emitted\_events$}{false}{\\The smart contract has emitted an event}
+ \Guard{grd2}{false}{$gateway \mapsto{} source\_smart\_contract \in{} subscriptions$}{false}{\\Exist a subscription to the smart contract events}
+ \Guard{grd3}{false}{$gateway \mapsto{} pending\_event \notin{} gateway\_pending\_events$}{false}{\\The event was not already listened}
+ }
+ \ACTIONS{true}{
+ \Action{act1}{$gateway\_pending\_events \bcmeq{} gateway\_pending\_events \bunion{} \{gateway \mapsto{} pending\_event\}$}{false}{\\The event is added to the pending events to be processed by the gateway}
+ \Action{act2}{$emitted\_events \bcmeq{} emitted\_events \setminus{} \{source\_smart\_contract \mapsto{} emitted\_event\}$}{false}{\\The event is removed from the pending events to listen}
+ \Action{act31}{$gateway\_processing \bcmeq{} 1$}{true}{}
+ \Action{act32}{$emitted \bcmeq{} 0$}{true}{}
+ \Action{act33}{$submit\_cc\_tx \bcmeq{} 0$}{true}{}
+ }
+}
+\EVT{SUBMIT\_TX\_TO\_ETHEREUM}{true}{ordinary}{SUBMIT\_TX\_TO\_ETHEREUM}{}{
+ \ANY{
+ \Param{pending\_event}{false}{}
+ \Param{transaction}{false}{}
+ \Param{fee}{false}{}
+ }
+ \GUARDS{true}{
+ \Guard{grd1}{false}{$gateway \mapsto{} pending\_event \in{} gateway\_pending\_events$}{false}{\\There is one pending event to be processed}
+ \Guard{grd2}{false}{$transaction \in{} TARGET\_TRANSACTIONS$}{false}{}
+ \Guard{grd11}{false}{$gateway\_address \in{} dom(accounts)$}{false}{}
+ \Guard{grd12}{false}{$accounts(gateway\_address) \geq{} fee$}{false}{\\The gateway has enough balance to pay the validators fee (REQ5)}
+ \Guard{grd13}{false}{$fee > 0$}{false}{}
+ }
+ \ACTIONS{true}{
+ \Action{act1}{$received\_target\_transactions \bcmeq{} received\_target\_transactions \bunion{} \{target\_smart\_contract \mapsto{} transaction\}$}{false}{\\The transaction is received by the target smart contract}
+ \Action{act2}{$gateway\_pending\_events \bcmeq{} gateway\_pending\_events \setminus{} \{gateway \mapsto{} pending\_event\}$}{false}{\\Remove the event from the pending events of the gateway}
+ \Action{act11}{$accounts(gateway\_address) \bcmeq{} accounts(gateway\_address) - fee$}{false}{\\The fee is subtracted from the gateways account (REQ5)}
+ \Action{act31}{$submit\_cc\_tx \bcmeq{} 1$}{true}{}
+ \Action{act32}{$gateway\_processing \bcmeq{} 0$}{true}{}
+ \Action{act33}{$wallet\_amount \bcmeq{} accounts(gateway\_address) - fee$}{true}{}
+ }
+}
+\EVT{CREATE\_ADDRESS\_IN\_ETHEREUM}{true}{ordinary}{CREATE\_ADDRESS\_IN\_ETHEREUM}{\\Users can create their address on Ethereum (RQ1 and RQ2)}{
+ \ANY{
+ \Param{address}{false}{}
+ }
+ \GUARDS{true}{
+ \Guard{grd1}{false}{$address \in{} ADDRESS$}{false}{}
+ \Guard{grd2}{false}{$address \notin{} dom(accounts)$}{false}{}
+ \Guard{grd31}{false}{$address = gateway\_address$}{true}{}
+ }
+ \ACTIONS{true}{
+ \Action{act1}{$accounts \bcmeq{} accounts \bunion{} \{address \mapsto{} 0\}$}{false}{}
+ \Action{act31}{$wallet\_created \bcmeq{} 1$}{true}{}
+ }
+}
+\EVT{DEPOSIT\_CRYPTOCURRENCY\_IN\_ETHEREUM}{true}{ordinary}{DEPOSIT\_CRYPTOCURRENCY\_IN\_ETHEREUM}{\\Users (including the gateway) can deposit Ethers on their address (RQ3)}{
+ \ANY{
+ \Param{amount}{false}{}
+ \Param{address}{false}{}
+ }
+ \GUARDS{true}{
+ \Guard{grd1}{false}{$amount > 0$}{false}{}
+ \Guard{grd2}{false}{$address \in{} dom(accounts)$}{false}{}
+ }
+ \ACTIONS{true}{
+ \Action{act1}{$accounts(address) \bcmeq{} accounts(address) + amount$}{false}{}
+ \Action{act31}{$wallet\_amount \bcmeq{} accounts(address) + amount$}{true}{}
+ \Action{act32}{$submit\_cc\_tx \bcmeq{} 0$}{true}{}
+ }
+}
+\EVT{SUBMIT\_TRANSFER\_TRANSACTION\_IN\_ETHEREUM}{true}{ordinary}{SUBMIT\_TRANSFER\_TRANSACTION\_IN\_ETHEREUM}{\\The user can transfer an estimated fee to the gateways account (RQ1)}{
+ \ANY{
+ \Param{validator\_fee}{false}{}
+ \Param{user\_address}{false}{}
+ \Param{transfer\_amount}{false}{}
+ }
+ \GUARDS{true}{
+ \Guard{grd1}{false}{$user\_address \in{} dom(accounts)$}{false}{\\The user has an account}
+ \Guard{grd2}{false}{$accounts(user\_address) \geq{} validator\_fee + transfer\_amount$}{false}{\\The user has enough balance to do the transfer and pay the validator's fee}
+ \Guard{grd3}{false}{$validator\_fee > 0$}{false}{}
+ \Guard{grd4}{false}{$transfer\_amount > 0$}{false}{}
+ \Guard{grd5}{false}{$gateway\_address \in{} dom(accounts)$}{false}{\\The gateway has an account}
+ \Guard{grd6}{false}{$(\{user\_address,gateway\_address\} \domsub{} accounts)\bunion{}\{gateway\_address \mapsto{} accounts(gateway\_address)+transfer\_amount\}\bunion{}\{user\_address \mapsto{} accounts(user\_address) - transfer\_amount - validator\_fee\}\in{}ADDRESS \pfun{} \nat{}$}{false}{}
+ }
+ \ACTIONS{true}{
+ \Action{act1}{$\\accounts \bcmeq{} (\{user\_address, gateway\_address\} \domsub{} accounts) \bunion{}\\~ \{gateway\_address \mapsto{} accounts(gateway\_address) + transfer\_amount\} \bunion{}\\~ \{user\_address \mapsto{} accounts(user\_address) - transfer\_amount - validator\_fee\}$}{false}{\\Subtracts the transfer amount and fee from the user's account and add the transfer amount to the gateways account}
+ }
+}
+}
+\END
+\end{document}
diff --git a/gateway-event-b/latex/CCTx_Fabric_Ethereum_m2.tex b/gateway-event-b/latex/CCTx_Fabric_Ethereum_m2.tex
index f39ba4d24d2e9df725bf68d116803df7de3eeaa9..cf1fc80d1287db40fbdfd291de08a60e5a4dba17 100644
--- a/gateway-event-b/latex/CCTx_Fabric_Ethereum_m2.tex
+++ b/gateway-event-b/latex/CCTx_Fabric_Ethereum_m2.tex
@@ -4,24 +4,24 @@
\SingleHeader{CCTx\_Fabric\_Ethereum\_m2}
\MACHINE{CCTx\_Fabric\_Ethereum\_m2}{CCTx\_Abstract\_DLT\_m1}{CCTx\_Fabric\_Ethereum\_c2}{}
\VARIABLES{
- \Variable{received\_transactions}{}
- \Variable{triggered\_events}{}
+ \Variable{received\_source\_transactions}{}
+ \Variable{emitted\_events}{}
\Variable{subscriptions}{}
- \Variable{gateway\_pending\_transactions}{}
- \Variable{received\_cross\_chain\_transactions}{}
+ \Variable{gateway\_pending\_events}{}
+ \Variable{received\_target\_transactions}{}
\Variable{accounts}{}
}
\INVARIANTS{
- \Invariant{inv11}{false}{$accounts \in{} ADDRESS \pfun{} \nat{}$}{\\The balance of each address must be equal or greater than zero (RQ4)}
+ \Invariant{inv11}{false}{$accounts \in{} ADDRESS \pfun{} \nat{}$}{\\The balance of each address must be equal or greater than zero (REQ4)}
}
\EVENTS{
\INITIALISATION{true}{}{
\ACTIONS{false}{
- \Action{act1}{$received\_transactions \bcmeq{} \emptyset{}$}{false}{}
- \Action{act2}{$triggered\_events \bcmeq{} \emptyset{}$}{false}{}
+ \Action{act1}{$received\_source\_transactions \bcmeq{} \emptyset{}$}{false}{}
+ \Action{act2}{$emitted\_events \bcmeq{} \emptyset{}$}{false}{}
\Action{act3}{$subscriptions \bcmeq{} \emptyset{}$}{false}{}
- \Action{act4}{$gateway\_pending\_transactions \bcmeq{} \emptyset{}$}{false}{}
- \Action{act6}{$received\_cross\_chain\_transactions \bcmeq{} \emptyset{}$}{false}{}
+ \Action{act4}{$gateway\_pending\_events \bcmeq{} \emptyset{}$}{false}{}
+ \Action{act6}{$received\_target\_transactions \bcmeq{} \emptyset{}$}{false}{}
\Action{act11}{$accounts \bcmeq{} \emptyset{}$}{true}{}
}
}
@@ -38,60 +38,62 @@
\Param{transaction}{false}{}
}
\GUARDS{true}{
- \Guard{grd1}{false}{$transaction \in{} TRANSACTIONS$}{false}{}
- \Guard{grd3}{false}{$transaction \notin{} received\_transactions[\{source\_smart\_contract\}]$}{false}{\\The transaction was not received by the smart contract}
+ \Guard{grd1}{false}{$transaction \in{} SOURCE\_TRANSACTIONS$}{false}{}
+ \Guard{grd3}{false}{$transaction \notin{} received\_source\_transactions[\{source\_smart\_contract\}]$}{false}{\\The transaction was not received by the smart contract}
}
\ACTIONS{true}{
- \Action{act1}{$received\_transactions \bcmeq{} received\_transactions \bunion{} \{source\_smart\_contract \mapsto{} transaction\}$}{false}{\\Add the transaction to the received transactions of the smart contract}
+ \Action{act1}{$received\_source\_transactions \bcmeq{} received\_source\_transactions \bunion{} \{source\_smart\_contract \mapsto{} transaction\}$}{false}{\\Add the transaction to the received transactions of the smart contract}
}
}
-\EVT{TRIGGER\_CC\_TX\_EVENT\_IN\_FABRIC}{true}{ordinary}{TRIGGER\_CC\_TX\_EVENT}{}{
+\EVT{EMIT\_EVENT\_IN\_FABRIC}{true}{ordinary}{EMIT\_EVENT}{}{
\ANY{
\Param{transaction}{false}{}
- \Param{cross\_chain\_event}{false}{}
+ \Param{emitted\_event}{false}{}
}
\GUARDS{true}{
- \Guard{grd1}{false}{$source\_smart\_contract \mapsto{} transaction \in{} received\_transactions$}{false}{\\The smart contract has a pending transaction to process}
- \Guard{grd2}{false}{$cross\_chain\_event \notin{} triggered\_events[\{source\_smart\_contract\}]$}{false}{\\The smart contract will always trigger a new event}
+ \Guard{grd1}{false}{$source\_smart\_contract \mapsto{} transaction \in{} received\_source\_transactions$}{false}{\\The smart contract has a pending transaction to process}
+ \Guard{grd2}{false}{$emitted\_event \notin{} emitted\_events[\{source\_smart\_contract\}]$}{false}{\\The smart contract will always emit a new event}
}
\ACTIONS{true}{
- \Action{act1}{$triggered\_events \bcmeq{} triggered\_events \bunion{} \{source\_smart\_contract \mapsto{} cross\_chain\_event\}$}{false}{\\The smart contract triggers a new event related to the transaction processing}
- \Action{act2}{$received\_transactions \bcmeq{} received\_transactions \setminus{} \{source\_smart\_contract \mapsto{} transaction\}$}{false}{\\The smart contract processed the transaction}
+ \Action{act1}{$emitted\_events \bcmeq{} emitted\_events \bunion{} \{source\_smart\_contract \mapsto{} emitted\_event\}$}{false}{\\The smart contract emits a new event related to the transaction processing}
+ \Action{act2}{$received\_source\_transactions \bcmeq{} received\_source\_transactions \setminus{} \{source\_smart\_contract \mapsto{} transaction\}$}{false}{\\The smart contract processed the transaction}
}
}
-\EVT{LISTEN\_CC\_TX\_EVENT\_IN\_FABRIC}{true}{ordinary}{LISTEN\_CC\_TX\_EVENT}{}{
+\EVT{LISTEN\_EVENT\_IN\_FABRIC}{true}{ordinary}{LISTEN\_EVENT}{}{
\ANY{
- \Param{cross\_chain\_event}{false}{}
- \Param{cross\_chain\_transaction}{false}{}
+ \Param{emitted\_event}{false}{}
+ \Param{pending\_event}{false}{}
}
\GUARDS{true}{
- \Guard{grd1}{false}{$source\_smart\_contract \mapsto{} cross\_chain\_event \in{} triggered\_events$}{false}{\\The smart contract has triggered an event}
+ \Guard{grd1}{false}{$source\_smart\_contract \mapsto{} emitted\_event \in{} emitted\_events$}{false}{\\The smart contract has emitted an event}
\Guard{grd2}{false}{$gateway \mapsto{} source\_smart\_contract \in{} subscriptions$}{false}{\\Exist a subscription to the smart contract events}
- \Guard{grd3}{false}{$gateway \mapsto{} cross\_chain\_transaction \notin{} gateway\_pending\_transactions$}{false}{\\The event was not already listened}
+ \Guard{grd3}{false}{$gateway \mapsto{} pending\_event \notin{} gateway\_pending\_events$}{false}{\\The event was not already listened}
}
\ACTIONS{true}{
- \Action{act1}{$gateway\_pending\_transactions \bcmeq{} gateway\_pending\_transactions \bunion{} \{gateway \mapsto{} cross\_chain\_transaction\}$}{false}{\\The event is added to the cross-chain transactions to be processed by the gateway}
- \Action{act2}{$triggered\_events \bcmeq{} triggered\_events \setminus{} \{source\_smart\_contract \mapsto{} cross\_chain\_event\}$}{false}{\\The event is removed from the pending events to listen}
+ \Action{act1}{$gateway\_pending\_events \bcmeq{} gateway\_pending\_events \bunion{} \{gateway \mapsto{} pending\_event\}$}{false}{\\The event is added to the pending events to be processed by the gateway}
+ \Action{act2}{$emitted\_events \bcmeq{} emitted\_events \setminus{} \{source\_smart\_contract \mapsto{} emitted\_event\}$}{false}{\\The event is removed from the pending events to listen}
}
}
-\EVT{SUBMIT\_CC\_TX\_TO\_ETHEREUM}{true}{ordinary}{SUBMIT\_CC\_TX}{}{
+\EVT{SUBMIT\_TX\_TO\_ETHEREUM}{true}{ordinary}{SUBMIT\_TX}{}{
\ANY{
- \Param{cross\_chain\_transaction}{false}{}
+ \Param{pending\_event}{false}{}
+ \Param{transaction}{false}{}
\Param{fee}{true}{}
}
\GUARDS{true}{
- \Guard{grd1}{false}{$gateway \mapsto{} cross\_chain\_transaction \in{} gateway\_pending\_transactions$}{false}{\\There is one pending cross-chain transaction to process}
+ \Guard{grd1}{false}{$gateway \mapsto{} pending\_event \in{} gateway\_pending\_events$}{false}{\\There is one pending event to be processed}
+ \Guard{grd2}{false}{$transaction \in{} TARGET\_TRANSACTIONS$}{false}{}
\Guard{grd11}{false}{$gateway\_address \in{} dom(accounts)$}{true}{}
- \Guard{grd12}{false}{$accounts(gateway\_address) \geq{} fee$}{true}{\\The gateway has enough balance to pay the validators fee (RQ5)}
+ \Guard{grd12}{false}{$accounts(gateway\_address) \geq{} fee$}{true}{\\The gateway has enough balance to pay the validators fee (REQ5)}
\Guard{grd13}{false}{$fee > 0$}{true}{}
}
\ACTIONS{true}{
- \Action{act1}{$received\_cross\_chain\_transactions \bcmeq{} received\_cross\_chain\_transactions \bunion{} \{target\_smart\_contract \mapsto{} cross\_chain\_transaction\}$}{false}{\\The cross-chain transaction is received by the target smart contract}
- \Action{act2}{$gateway\_pending\_transactions \bcmeq{} gateway\_pending\_transactions \setminus{} \{gateway \mapsto{} cross\_chain\_transaction\}$}{false}{\\Remove the cross-chain transaction to the pending transactions of the Gateway}
- \Action{act11}{$accounts(gateway\_address) \bcmeq{} accounts(gateway\_address) - fee$}{true}{\\The fee is subtracted from the gateways account (RQ5)}
+ \Action{act1}{$received\_target\_transactions \bcmeq{} received\_target\_transactions \bunion{} \{target\_smart\_contract \mapsto{} transaction\}$}{false}{\\The transaction is received by the target smart contract}
+ \Action{act2}{$gateway\_pending\_events \bcmeq{} gateway\_pending\_events \setminus{} \{gateway \mapsto{} pending\_event\}$}{false}{\\Remove the event from the pending events of the gateway}
+ \Action{act11}{$accounts(gateway\_address) \bcmeq{} accounts(gateway\_address) - fee$}{true}{\\The fee is subtracted from the gateways account (REQ5)}
}
}
-\EVT{CREATE\_ADDRESS\_IN\_ETHEREUM}{false}{ordinary}{}{\\Users can create their address on Ethereum (RQ1 and RQ2)}{
+\EVT{CREATE\_ADDRESS\_IN\_ETHEREUM}{false}{ordinary}{}{\\Users can create their address on Ethereum (REQ1 and REQ2)}{
\ANY{
\Param{address}{true}{}
}
@@ -103,7 +105,7 @@
\Action{act1}{$accounts \bcmeq{} accounts \bunion{} \{address \mapsto{} 0\}$}{true}{}
}
}
-\EVT{DEPOSIT\_CRYPTOCURRENCY\_IN\_ETHEREUM}{false}{ordinary}{}{\\Users (including the gateway) can deposit Ethers on their address (RQ3)}{
+\EVT{DEPOSIT\_CRYPTOCURRENCY\_IN\_ETHEREUM}{false}{ordinary}{}{\\Users (including the gateway) can deposit Ethers on their address (REQ3)}{
\ANY{
\Param{amount}{true}{}
\Param{address}{true}{}
@@ -116,7 +118,7 @@
\Action{act1}{$accounts(address) \bcmeq{} accounts(address) + amount$}{true}{}
}
}
-\EVT{SUBMIT\_TRANSFER\_TRANSACTION\_IN\_ETHEREUM}{false}{ordinary}{}{\\The user can transfer an estimated fee to the gateways account (RQ1)}{
+\EVT{SUBMIT\_TRANSFER\_TRANSACTION\_IN\_ETHEREUM}{false}{ordinary}{}{\\The user can transfer an estimated fee to the gateways account (REQ1)}{
\ANY{
\Param{validator\_fee}{true}{}
\Param{user\_address}{true}{}
diff --git a/gateway-event-b/latex/CCTx_Preserve_Balance_Gateway_m3.tex b/gateway-event-b/latex/CCTx_Preserve_Balance_Gateway_m3.tex
index 90e79bff42097480287ecea57d559396b278da35..87f52bff40324c533fa6bac20af1a5349224c0af 100644
--- a/gateway-event-b/latex/CCTx_Preserve_Balance_Gateway_m3.tex
+++ b/gateway-event-b/latex/CCTx_Preserve_Balance_Gateway_m3.tex
@@ -4,11 +4,11 @@
\SingleHeader{CCTx\_Preserve\_Balance\_Gateway\_m3}
\MACHINE{CCTx\_Preserve\_Balance\_Gateway\_m3}{CCTx\_Fabric\_Ethereum\_m2}{CCTx\_Fabric\_Ethereum\_c2}{}
\VARIABLES{
- \Variable{received\_transactions}{}
- \Variable{triggered\_events}{}
+ \Variable{received\_source\_transactions}{}
+ \Variable{emitted\_events}{}
\Variable{subscriptions}{}
- \Variable{gateway\_pending\_transactions}{}
- \Variable{received\_cross\_chain\_transactions}{}
+ \Variable{gateway\_pending\_events}{}
+ \Variable{received\_target\_transactions}{}
\Variable{accounts}{}
\Variable{estimated\_cross\_chain\_cost}{}
}
@@ -16,51 +16,84 @@
\Invariant{inv31}{false}{$estimated\_cross\_chain\_cost \in{} \nat{}$}{}
}
\EVENTS{
-\EVT{TRIGGER\_CC\_TX\_EVENT\_IN\_FABRIC}{true}{ordinary}{TRIGGER\_CC\_TX\_EVENT\_IN\_FABRIC}{}{
+\INITIALISATION{true}{}{
+ \ACTIONS{false}{
+ \Action{act1}{$received\_source\_transactions \bcmeq{} \emptyset{}$}{false}{}
+ \Action{act2}{$emitted\_events \bcmeq{} \emptyset{}$}{false}{}
+ \Action{act3}{$subscriptions \bcmeq{} \emptyset{}$}{false}{}
+ \Action{act4}{$gateway\_pending\_events \bcmeq{} \emptyset{}$}{false}{}
+ \Action{act6}{$received\_target\_transactions \bcmeq{} \emptyset{}$}{false}{}
+ \Action{act11}{$accounts \bcmeq{} \emptyset{}$}{false}{}
+ \Action{act31}{$estimated\_cross\_chain\_cost \bcmeq{} 0$}{true}{}
+ }
+}
+\EVT{SUBSCRIBE\_SMART\_CONTRACT\_EVENTS\_IN\_FABRIC}{true}{ordinary}{SUBSCRIBE\_SMART\_CONTRACT\_EVENTS\_IN\_FABRIC}{}{
+ \GUARDS{false}{
+ \Guard{grd1}{false}{$gateway \mapsto{} source\_smart\_contract \notin{} subscriptions$}{false}{\\The gateway is not already subscribed to the smart contract events}
+ }
+ \ACTIONS{true}{
+ \Action{act1}{$subscriptions \bcmeq{} subscriptions \bunion{} \{gateway \mapsto{} source\_smart\_contract\}$}{false}{\\The gateway is subscribed to listen to the smart contract events}
+ }
+}
+\EVT{INITIATE\_CC\_TX\_IN\_FABRIC}{true}{ordinary}{INITIATE\_CC\_TX\_IN\_FABRIC}{}{
+ \ANY{
+ \Param{transaction}{false}{}
+ }
+ \GUARDS{true}{
+ \Guard{grd1}{false}{$transaction \in{} SOURCE\_TRANSACTIONS$}{false}{}
+ \Guard{grd3}{false}{$transaction \notin{} received\_source\_transactions[\{source\_smart\_contract\}]$}{false}{\\The transaction was not received by the smart contract}
+ }
+ \ACTIONS{true}{
+ \Action{act1}{$received\_source\_transactions \bcmeq{} received\_source\_transactions \bunion{} \{source\_smart\_contract \mapsto{} transaction\}$}{false}{\\Add the transaction to the received transactions of the smart contract}
+ }
+}
+\EVT{EMIT\_EVENT\_IN\_FABRIC}{true}{ordinary}{EMIT\_EVENT\_IN\_FABRIC}{}{
\ANY{
\Param{transaction}{false}{}
- \Param{cross\_chain\_event}{false}{}
+ \Param{emitted\_event}{false}{}
}
\GUARDS{true}{
- \Guard{grd1}{false}{$source\_smart\_contract \mapsto{} transaction \in{} received\_transactions$}{false}{\\The smart contract has a pending transaction to process}
- \Guard{grd2}{false}{$cross\_chain\_event \notin{} triggered\_events[\{source\_smart\_contract\}]$}{false}{\\The smart contract will always trigger a new event}
+ \Guard{grd1}{false}{$source\_smart\_contract \mapsto{} transaction \in{} received\_source\_transactions$}{false}{\\The smart contract has a pending transaction to process}
+ \Guard{grd2}{false}{$emitted\_event \notin{} emitted\_events[\{source\_smart\_contract\}]$}{false}{\\The smart contract will always emit a new event}
}
\ACTIONS{true}{
- \Action{act1}{$triggered\_events \bcmeq{} triggered\_events \bunion{} \{source\_smart\_contract \mapsto{} cross\_chain\_event\}$}{false}{\\The smart contract triggers a new event related to the transaction processing}
- \Action{act2}{$received\_transactions \bcmeq{} received\_transactions \setminus{} \{source\_smart\_contract \mapsto{} transaction\}$}{false}{\\The smart contract processed the transaction}
+ \Action{act1}{$emitted\_events \bcmeq{} emitted\_events \bunion{} \{source\_smart\_contract \mapsto{} emitted\_event\}$}{false}{\\The smart contract emits a new event related to the transaction processing}
+ \Action{act2}{$received\_source\_transactions \bcmeq{} received\_source\_transactions \setminus{} \{source\_smart\_contract \mapsto{} transaction\}$}{false}{\\The smart contract processed the transaction}
}
}
-\EVT{LISTEN\_CC\_TX\_EVENT\_IN\_FABRIC}{true}{ordinary}{LISTEN\_CC\_TX\_EVENT\_IN\_FABRIC}{}{
+\EVT{LISTEN\_EVENT\_IN\_FABRIC}{true}{ordinary}{LISTEN\_EVENT\_IN\_FABRIC}{}{
\ANY{
- \Param{cross\_chain\_event}{false}{}
- \Param{cross\_chain\_transaction}{false}{}
+ \Param{emitted\_event}{false}{}
+ \Param{pending\_event}{false}{}
}
\GUARDS{true}{
- \Guard{grd1}{false}{$source\_smart\_contract \mapsto{} cross\_chain\_event \in{} triggered\_events$}{false}{\\The smart contract has triggered an event}
+ \Guard{grd1}{false}{$source\_smart\_contract \mapsto{} emitted\_event \in{} emitted\_events$}{false}{\\The smart contract has emitted an event}
\Guard{grd2}{false}{$gateway \mapsto{} source\_smart\_contract \in{} subscriptions$}{false}{\\Exist a subscription to the smart contract events}
- \Guard{grd3}{false}{$gateway \mapsto{} cross\_chain\_transaction \notin{} gateway\_pending\_transactions$}{false}{\\The event was not already listened}
+ \Guard{grd3}{false}{$gateway \mapsto{} pending\_event \notin{} gateway\_pending\_events$}{false}{\\The event was not already listened}
}
\ACTIONS{true}{
- \Action{act1}{$gateway\_pending\_transactions \bcmeq{} gateway\_pending\_transactions \bunion{} \{gateway \mapsto{} cross\_chain\_transaction\}$}{false}{\\The event is added to the cross-chain transactions to be processed by the gateway}
- \Action{act2}{$triggered\_events \bcmeq{} triggered\_events \setminus{} \{source\_smart\_contract \mapsto{} cross\_chain\_event\}$}{false}{\\The event is removed from the pending events to listen}
+ \Action{act1}{$gateway\_pending\_events \bcmeq{} gateway\_pending\_events \bunion{} \{gateway \mapsto{} pending\_event\}$}{false}{\\The event is added to the pending events to be processed by the gateway}
+ \Action{act2}{$emitted\_events \bcmeq{} emitted\_events \setminus{} \{source\_smart\_contract \mapsto{} emitted\_event\}$}{false}{\\The event is removed from the pending events to listen}
}
}
-\EVT{SUBMIT\_CC\_TX\_TO\_ETHEREUM}{true}{ordinary}{SUBMIT\_CC\_TX\_TO\_ETHEREUM}{}{
+\EVT{SUBMIT\_TX\_TO\_ETHEREUM}{true}{ordinary}{SUBMIT\_TX\_TO\_ETHEREUM}{}{
\ANY{
- \Param{cross\_chain\_transaction}{false}{}
+ \Param{pending\_event}{false}{}
+ \Param{transaction}{false}{}
\Param{fee}{false}{}
}
\GUARDS{true}{
- \Guard{grd1}{false}{$gateway \mapsto{} cross\_chain\_transaction \in{} gateway\_pending\_transactions$}{false}{\\There is one pending cross-chain transaction to process}
+ \Guard{grd1}{false}{$gateway \mapsto{} pending\_event \in{} gateway\_pending\_events$}{false}{\\There is one pending event to be processed}
+ \Guard{grd2}{false}{$transaction \in{} TARGET\_TRANSACTIONS$}{false}{}
\Guard{grd11}{false}{$gateway\_address \in{} dom(accounts)$}{false}{}
- \Guard{grd12}{false}{$accounts(gateway\_address) \geq{} fee$}{false}{\\The gateway has enough balance to pay the validators fee (RQ5)}
+ \Guard{grd12}{false}{$accounts(gateway\_address) \geq{} fee$}{false}{\\The gateway has enough balance to pay the validators fee (REQ5)}
\Guard{grd13}{false}{$fee > 0$}{false}{}
\Guard{grd31}{false}{$fee \leq{} estimated\_cross\_chain\_cost$}{true}{\\Check that the estimated fee is greater or equal to the validators fee (RQ2)}
}
\ACTIONS{true}{
- \Action{act1}{$received\_cross\_chain\_transactions \bcmeq{} received\_cross\_chain\_transactions \bunion{} \{target\_smart\_contract \mapsto{} cross\_chain\_transaction\}$}{false}{\\The cross-chain transaction is received by the target smart contract}
- \Action{act2}{$gateway\_pending\_transactions \bcmeq{} gateway\_pending\_transactions \setminus{} \{gateway \mapsto{} cross\_chain\_transaction\}$}{false}{\\Remove the cross-chain transaction to the pending transactions of the Gateway}
- \Action{act11}{$accounts(gateway\_address) \bcmeq{} accounts(gateway\_address) - fee$}{false}{\\The fee is subtracted from the gateways account (RQ5)}
+ \Action{act1}{$received\_target\_transactions \bcmeq{} received\_target\_transactions \bunion{} \{target\_smart\_contract \mapsto{} transaction\}$}{false}{\\The transaction is received by the target smart contract}
+ \Action{act2}{$gateway\_pending\_events \bcmeq{} gateway\_pending\_events \setminus{} \{gateway \mapsto{} pending\_event\}$}{false}{\\Remove the event from the pending events of the gateway}
+ \Action{act11}{$accounts(gateway\_address) \bcmeq{} accounts(gateway\_address) - fee$}{false}{\\The fee is subtracted from the gateways account (REQ5)}
}
}
\EVT{CREATE\_ADDRESS\_IN\_ETHEREUM}{true}{ordinary}{CREATE\_ADDRESS\_IN\_ETHEREUM}{}{
@@ -108,37 +141,6 @@
\Action{act31}{$estimated\_cross\_chain\_cost \bcmeq{} transfer\_amount$}{true}{}
}
}
-\INITIALISATION{true}{}{
- \ACTIONS{false}{
- \Action{act1}{$received\_transactions \bcmeq{} \emptyset{}$}{false}{}
- \Action{act2}{$triggered\_events \bcmeq{} \emptyset{}$}{false}{}
- \Action{act3}{$subscriptions \bcmeq{} \emptyset{}$}{false}{}
- \Action{act4}{$gateway\_pending\_transactions \bcmeq{} \emptyset{}$}{false}{}
- \Action{act6}{$received\_cross\_chain\_transactions \bcmeq{} \emptyset{}$}{false}{}
- \Action{act11}{$accounts \bcmeq{} \emptyset{}$}{false}{}
- \Action{act31}{$estimated\_cross\_chain\_cost \bcmeq{} 0$}{true}{}
- }
-}
-\EVT{SUBSCRIBE\_SMART\_CONTRACT\_EVENTS\_IN\_FABRIC}{true}{ordinary}{SUBSCRIBE\_SMART\_CONTRACT\_EVENTS\_IN\_FABRIC}{}{
- \GUARDS{false}{
- \Guard{grd1}{false}{$gateway \mapsto{} source\_smart\_contract \notin{} subscriptions$}{false}{\\The gateway is not already subscribed to the smart contract events}
- }
- \ACTIONS{true}{
- \Action{act1}{$subscriptions \bcmeq{} subscriptions \bunion{} \{gateway \mapsto{} source\_smart\_contract\}$}{false}{\\The gateway is subscribed to listen to the smart contract events}
- }
-}
-\EVT{INITIATE\_CC\_TX\_IN\_FABRIC}{true}{ordinary}{INITIATE\_CC\_TX\_IN\_FABRIC}{}{
- \ANY{
- \Param{transaction}{false}{}
- }
- \GUARDS{true}{
- \Guard{grd1}{false}{$transaction \in{} TRANSACTIONS$}{false}{}
- \Guard{grd3}{false}{$transaction \notin{} received\_transactions[\{source\_smart\_contract\}]$}{false}{\\The transaction was not received by the smart contract}
- }
- \ACTIONS{true}{
- \Action{act1}{$received\_transactions \bcmeq{} received\_transactions \bunion{} \{source\_smart\_contract \mapsto{} transaction\}$}{false}{\\Add the transaction to the received transactions of the smart contract}
- }
-}
}
\END
\end{document}
diff --git a/gateway-event-b/latex/b2latex.sty b/gateway-event-b/latex/b2latex.sty
deleted file mode 100644
index 7fa289cc55ad8198ea7d64dbaaf239fe7d0af7e0..0000000000000000000000000000000000000000
--- a/gateway-event-b/latex/b2latex.sty
+++ /dev/null
@@ -1,282 +0,0 @@
-%----------------------------------------------------------------------------
-% This is b2latex.sty, generated by B2Latex plugin on Rodin
-% Author: K. DAMCHOOM, kd06r@ecs.soton.ac.uk
-% Copyright(c) 2008 - 2012 University of Southampton and others.
-%----------------------------------------------------------------------------
-% This style is required for all latex files generated by the
-% B2Latex plugin 0.7.x. It can be modified for your own style.
-% Internal commands, which are not contained in the generated
-% latex document, are marked by the character '@' in the name.
-%----------------------------------------------------------------------------
-
-\usepackage[top=2.5cm, bottom=2.0cm, left=2.5cm, right=2.5cm]{geometry}
-\usepackage[utf8]{inputenc}
-\usepackage[ddmmyyyy]{datetime}
-\usepackage{fancyhdr,lastpage,color}
-
-\definecolor{keycolor}{rgb}{0,0,0.8} % Keywords, blue
-\definecolor{labelcolor}{rgb}{0,0.4,0.8} % Labels, cyan
-\definecolor{codecolor}{rgb}{0,0,0} % Formulas, black
-\definecolor{inhcolor}{rgb}{0.6,0.2,0} % Inherited formulas, maroon
-\definecolor{cmtcolor}{rgb}{0,0.4,0} % Comments, green
-
-\renewcommand{\chaptername}{}
-\renewcommand{\thechapter}{}
-\renewcommand{\dateseparator}{.}
-
-% Reduce space between paras
-\newcommand{\paraSpc@} {\hspace*{\fill} \setlength{\parskip}{-2pt}}
-% Reduce space between para items
-\newcommand{\itemSpc@} {\setlength{\itemsep}{-0pt}}
-
-% Keywords
-\newcommand{\key@}[1]{\textcolor{keycolor}{#1}}
-% Labels
-\newcommand{\lbl@}[1]{\textcolor{labelcolor}{\small{\texttt{#1}}}}
-% Formulas
-\newcommand{\code@}[1]{\textcolor{codecolor}{\small{#1}}}
-% Inherited formulas
-\newcommand{\inh@}[1]{\textcolor{inhcolor}{\small{#1}}}
-% Comments
-\newcommand{\cmt@}[1]{\textcolor{cmtcolor}{\small{#1}}}
-% Modifiers (inline keywords)
-\newcommand{\mod@}[1]{\key@{\small{$\langle$#1$\rangle$}}}
-
-% Optional comment
-\newcommand{\cmtOpt@}[1]{\ifthenelse{\equal{#1}{}}{}{\cmt@{#1}}}
-% Alternate keyword
-\newcommand{\keyAlt@}[3]{\ifthenelse{\boolean{#1}}{\key@{#2}}{\key@{#3}}}
-% Optional modifier
-\newcommand{\modOpt@}[2]{\ifthenelse{\boolean{#1}}{\mod@{#2}}{}}
-% Code or inherited code
-\newcommand{\codeInh@}[2]{\ifthenelse{\boolean{#1}}{\code@{#2}}{\inh@{\textit{#2}}}}
-
-%----------------------------------------------------------------------------
-
-% Common header definition
-\newcommand{\Header@}{
- \lfoot{\today~\currenttime}
- \cfoot{}
- \rfoot{\rm Page \thepage~of \pageref{LastPage}}
- \pagestyle{fancy}
-}
-
-% Header used if a single context or machine is exported
-% #1: Context / Machine name
-\newcommand{\SingleHeader}[1]{
- \Header@{}
- \lhead{}
- \chead{An Event-B Specification of #1}
- \rhead{}
-}
-
-% Title page used if a whole project is exported
-% #1: Project name
-\newcommand{\MultiTitle}[1]{
- \Header@{}
- \lhead{An Event-B Specification of #1}
- \chead{}
- \rhead{}
- \fancypagestyle{plain}{}
- \tableofcontents
-}
-
-% Subheader for each component if a whole project is exported
-% #1: Component type (CONTEXT / MACHINE); #2: Component name
-\newcommand{\MultiHeader}[2]{
- \newpage{}
- \rhead{\texttt{#1} #2}
- \addcontentsline{toc}{chapter}{\texttt{#1} #2}
-}
-
-%----------------------------------------------------------------------------
-% Special commands for CONTEXT
-%----------------------------------------------------------------------------
-
-% #1: Context name; #2: Extended contexts (optional); #3: Comment (optional)
-\newcommand{\CONTEXT}[3]{
- \begin{description}
- \item[\key@{CONTEXT}] #1 \cmtOpt@{#3} \paraSpc@
- \ifthenelse{\equal{#2}{}}{}{
- \item[\key@{EXTENDS}] #2 \paraSpc@
- }
-}
-% Alternative compact display:
-%\newcommand{\CONTEXT}[3]{
-% \begin{description}
-% \item[\key@{CONTEXT}] #1
-% \ifthenelse{\equal{#2}{}}{}{\key@{EXTENDS} #2}
-% \cmtOpt@{#3}
-% \paraSpc@
-%}
-
-% #1: Sets definitions
-\newcommand{\SETS}[1]{
- \item[\key@{SETS}] \paraSpc@
- \begin{description} #1 \end{description}
-}
-
-% #1: Identifier; #2: Comment (optional)
-\newcommand{\Set}[2]{
- \item \code@{#1} \cmtOpt@{#2} \itemSpc@
-}
-
-% #1: Constants definitions
-\newcommand{\CONSTANTS}[1]{
- \item[\key@{CONSTANTS}] \paraSpc@
- \begin{description} #1 \end{description}
-}
-
-% #1: Identifier; #2: Comment (optional)
-\newcommand{\Constant}[2]{
- \item \code@{#1} \cmtOpt@{#2} \itemSpc@
-}
-
-% #1: Axioms definitions
-\newcommand{\AXIOMS}[1]{
- \item[\key@{AXIOMS}] \paraSpc@
- \begin{description} #1 \end{description}
-}
-
-% #1: Label; #2: true if theorem; #3: Predicate; #4: Comment (optional)
-\newcommand{\Axiom}[4]{
- \item \lbl@{#1}: \modOpt@{#2}{theorem} \code@{#3} \cmtOpt@{#4} \itemSpc@
-}
-
-%----------------------------------------------------------------------------
-% Special commands for MACHINE
-%----------------------------------------------------------------------------
-
-% #1: Machine name; #2: Refined machines (optional);
-% #3: Seen contexts (optional); #4: Comment (optional)
-\newcommand{\MACHINE}[4]{
- \begin{description}
- \item[\key@{MACHINE}] #1 \cmtOpt@{#4} \paraSpc@
- \ifthenelse{\equal{#2}{}}{}{
- \item[\key@{REFINES}] #2 \paraSpc@
- }
- \ifthenelse{\equal{#3}{}}{}{
- \item[\key@{SEES}] #3 \paraSpc@
- }
-}
-
-% #1: variables definitions
-\newcommand{\VARIABLES}[1]{
- \item[\key@{VARIABLES}] \paraSpc@
- \begin{description} #1 \end{description}
-}
-
-% #1: Identifier; #2: Comment (optional)
-\newcommand{\Variable}[2]{
- \item \code@{#1} \cmtOpt@{#2} \itemSpc@
-}
-
-% #1: Invariants definitions
-\newcommand{\INVARIANTS}[1]{
- \item[\key@{INVARIANTS}] \paraSpc@
- \begin{description} #1 \end{description}
-}
-
-% #1: Label; #2: true if theorem; #3: Predicate; #4: Comment (optional)
-\newcommand{\Invariant}[4]{
- \item \lbl@{#1}: \modOpt@{#2}{theorem} \code@{#3} \cmtOpt@{#4} \itemSpc@
-}
-
-% #1: Variants definitions
-\newcommand{\VARIANT}[1]{
- \item[\key@{VARIANT}] \paraSpc@
- \begin{description} #1 \end{description}
-}
-
-% #1: Expression; #2: Comment (optional)
-\newcommand{\Variant}[2]{
- \item \code@{#1} \cmtOpt@{#2} \itemSpc@
-}
-
-\newcommand{\EVENTS}{
- \item[\key@{EVENTS}] \paraSpc@
-}
-
-% #1: true if extended; #2: Comment (optional); #3: Event content
-\newcommand{\INITIALISATION}[3]{
- \item[\key@{Initialisation}] \modOpt@{#1}{extended} \cmtOpt@{#2} \paraSpc@
- \begin{description} #3 \end{description}
-}
-
-% #1: Event name; #2: true if extended; #3 convergence;
-% #4: Refined events (optional); #5: Comment (optional); #6: Event content
-\newcommand{\EVT}[6]{
- \item[\key@{Event}] #1
-% deactivate above line and activate line below to display only event name
-% \item[\key@{#1}]
- \mod@{#3} $\defi$ \cmtOpt@{#5} \paraSpc@
- \ifthenelse{\equal{#4}{}}{}{
- \item[\keyAlt@{#2}{extends}{refines}] #4 \paraSpc@
- }
- \begin{description} #6 \end{description}
-}
-
-% #1: Parameters definitions
-\newcommand{\ANY}[1]{
- \item[\key@{any}] \paraSpc@ \itemSpc@
- \begin{description} #1 \end{description}
-}
-
-% #1: Identifier; #2: true if own, false if inherited; #3: Comment (optional)
-\newcommand{\Param}[3]{
- \item \codeInh@{#2}{#1} \cmtOpt@{#3} \itemSpc@
-}
-
-%1: true if the event has parameters; #2: Guards definitions
-\newcommand{\GUARDS}[2]{
- \item[\keyAlt@{#1}{where}{when}] \paraSpc@ \itemSpc@
- \begin{description} #2 \end{description}
-}
-
-% #1: Label; #2: true if theorem; #3: Predicate;
-% #4: true if own, false if inherited; #5: Comment (optional)
-\newcommand{\Guard}[5]{
- \item \lbl@{#1}: \modOpt@{#2}{theorem} \codeInh@{#4}{#3} \cmtOpt@{#5} \itemSpc@
-}
-
-% #1: Witnesses definitions
-\newcommand{\WITNESSES}[1]{
- \item[\key@{with}] \paraSpc@ \itemSpc@
- \begin{description} #1 \end{description}
-}
-
-% #1: Label; #3: Predicate; #3: Comment (optional)
-\newcommand{\Witness}[3]{
- \item \lbl@{#1}: \code@{#2} \cmtOpt@{#3} \itemSpc@
-}
-
-%1: true if the event has guards; #2: Actions definitions
-\newcommand{\ACTIONS}[2]{
- \item[\keyAlt@{#1}{then}{begin}] \paraSpc@ \itemSpc@
- \begin{description} #2 \end{description}
- \item[\key@{end}] \paraSpc@
-}
-
-% #1: Label; #2: Predicate; #3: true if own, false if inherited; #4: Comment (optional)
-\newcommand{\Action}[4]{
- \item \lbl@{#1}: \codeInh@{#3}{#2} \cmtOpt@{#4} \itemSpc@
-}
-
-% Skip action
-\newcommand{\Skip}{
- \item \key@{\textit{skip}} \itemSpc@
-}
-
-%----------------------------------------------------------------------------
-% General commands for both CONTEXT and MACHINE
-%----------------------------------------------------------------------------
-
-% End of MACHINE or CONTEXT
-\newcommand{\END}{
- \item[\key@{END}] \hspace*{\fill} \end{description}
-}
-
-% Missing in bsymb.sty version 1.9
-\newcommand{\converse}{^{-1}}
-
-%----------------------------------------------------------------------------
\ No newline at end of file