Artifact Content
Not logged in

Artifact 1226bdf77e761c3483fb3b7e7b0a5536939b0bf5:


\batchmode %% Suppresses most terminal output.
\documentclass[letterpaper,twocolumn,10pt]{article}
\usepackage{color}
\usepackage{ilpspec}
% \usepackage{usenix}
\definecolor{boxshade}{gray}{0.95}

\setlength{\headheight}{0.0in}

\usepackage{latexsym}
\usepackage{ifthen}
% \usepackage{color}
\usepackage{tlatex}

\begin{document}
\onecolumn
\appendix
\stepcounter{section}
\stepcounter{subsection}
\stepcounter{subsection}
\setcounter{page}{12}
\subsection{Formal Specification: Atomic mode}
\label{sec:atomic-spec}
\tlatex
\setboolean{shading}{true}
\@x{}\moduleLeftDash\@xx{ {\MODULE} Atomic}\moduleRightDash\@xx{}%
\begin{lcom}{0}%
\begin{cpar}{0}{T}{F}{2.5}{0}{}%
Formal Specification in TLA\ensuremath{\.{\mbox{}^+}} of the
 Interledger Protocol \ensuremath{Atomic} (\ensuremath{ILP}/A)
\end{cpar}%
\vshade{10.0}%
\begin{cpar}{1}{F}{F}{0}{0}{}%
\begin{minipage}[t]{\linewidth}
\begin{verbatim}
 Modeled after the excellent Raft specification by Diego Ongaro.         
   Available at https://github.com/ongardie/raft.tla                     
\end{verbatim}
\end{minipage}
\end{cpar}%
\vshade{5.0}%
\begin{cpar}{0}{F}{F}{0}{0}{}%
\begin{minipage}[t]{\linewidth}
\begin{verbatim}
   Copyright 2014 Diego Ongaro.                                          
   This work is licensed under the Creative Commons Attribution-4.0      
   International License https://creativecommons.org/licenses/by/4.0/  
\end{verbatim}
\end{minipage}
\end{cpar}%
\end{lcom}%
\@pvspace{8.0pt}%
\@x{ {\EXTENDS} Naturals ,\, Sequences ,\, Bags ,\, TLC}%
\@pvspace{8.0pt}%
\@x{}%
\@y{\@s{0}%
 The set of ledger \ensuremath{IDs
}}%
\@xx{}%
\@x{ {\CONSTANTS} Ledger}%
\@pvspace{8.0pt}%
\@x{}%
\@y{\@s{0}%
 The set of participant \ensuremath{IDs
}}%
\@xx{}%
\@x{ {\CONSTANTS} Participant}%
\@pvspace{8.0pt}%
\@x{}%
\@y{\@s{0}%
 The notary
}%
\@xx{}%
\@x{ {\CONSTANTS} Notary}%
\@pvspace{8.0pt}%
\@x{}%
\@y{\@s{0}%
 Sender states
}%
\@xx{}%
\@x{ {\CONSTANTS} S\_Ready ,\, S\_Waiting ,\, S\_Done}%
\@pvspace{8.0pt}%
\@x{}%
\@y{\@s{0}%
 Notary states
}%
\@xx{}%
\@x{ {\CONSTANTS} N\_Waiting ,\, N\_Committed ,\, N\_Aborted}%
\@pvspace{8.0pt}%
\@x{}%
\@y{\@s{0}%
 Ledger states
}%
\@xx{}%
\@x{ {\CONSTANTS} L\_Proposed ,\, L\_Prepared ,\, L\_Executed ,\, L\_Aborted}%
\@pvspace{8.0pt}%
\@x{}%
\@y{\@s{0}%
 Message types
}%
\@xx{}%
\@x{ {\CONSTANTS} PrepareRequest ,\, ExecuteRequest ,\, AbortRequest ,\,}%
\@x{\@s{54.75} PrepareNotify ,\, ExecuteNotify ,\, AbortNotify ,\,}%
\@x{\@s{54.75} SubmitReceiptRequest}%
\@pvspace{8.0pt}%
\@x{}%
\@y{\@s{0}%
 Receipt signature
}%
\@xx{}%
\@x{ {\CONSTANTS} R\_ReceiptSignature}%
\@pvspace{8.0pt}%
\@x{}\midbar\@xx{}%
\@x{}%
\@y{\@s{0}%
 Global variables
}%
\@xx{}%
\@pvspace{8.0pt}%
\@x{}%
\@y{\@s{0}%
 A bag of records representing requests and responses sent from one process
}%
\@xx{}%
\@x{}%
\@y{\@s{0}%
 to another
}%
\@xx{}%
\@x{ {\VARIABLE} messages}%
\@pvspace{8.0pt}%
\@x{}\midbar\@xx{}%
\@x{}%
\@y{\@s{0}%
 Sender variables
}%
\@xx{}%
\@pvspace{8.0pt}%
\@x{}%
\@y{\@s{0}%
 State of the sender (\ensuremath{S\_Ready}, \ensuremath{S\_Waiting},
 \ensuremath{S\_Done})
}%
\@xx{}%
\@x{ {\VARIABLE} senderState}%
\@pvspace{8.0pt}%
\@x{}%
\@y{\@s{0}%
 All sender variables
}%
\@xx{}%
\@x{ senderVars \.{\defeq} {\langle} senderState {\rangle}}%
\@x{}\midbar\@xx{}%
\@x{}%
\@y{\@s{0}%
 The following variables are all per ledger (functions with domain
 \ensuremath{Ledger})
}%
\@xx{}%
\@pvspace{8.0pt}%
\@x{}%
\@y{\@s{0}%
 The ledger state (\ensuremath{L\_Proposed}, \ensuremath{L\_Prepared},
 \ensuremath{L\_Executed} or \ensuremath{L\_Aborted})
}%
\@xx{}%
\@x{ {\VARIABLE} ledgerState}%
\@pvspace{8.0pt}%
\@x{}%
\@y{\@s{0}%
 All ledger variables
}%
\@xx{}%
\@x{ ledgerVars \.{\defeq} {\langle} ledgerState {\rangle}}%
\@x{}\midbar\@xx{}%
\@x{}%
\@y{\@s{0}%
 Notary variables
}%
\@xx{}%
\@pvspace{8.0pt}%
\@x{}%
\@y{\@s{0}%
 State of the notary (\ensuremath{N\_Waiting}, \ensuremath{N\_Committed},
 \ensuremath{N\_Aborted})
}%
\@xx{}%
\@x{ {\VARIABLE} notaryState}%
\@pvspace{8.0pt}%
\@x{}%
\@y{\@s{0}%
 All notary variables
}%
\@xx{}%
\@x{ notaryVars \.{\defeq} {\langle} notaryState {\rangle}}%
\@x{}\midbar\@xx{}%
\@pvspace{8.0pt}%
\@x{}%
\@y{\@s{0}%
 All variables; used for stuttering (asserting state hasn\mbox{'}t changed)
}%
\@xx{}%
 \@x{ vars \.{\defeq} {\langle} messages ,\, senderVars ,\, ledgerVars ,\,
 notaryVars {\rangle}}%
\@pvspace{8.0pt}%
\@x{}\midbar\@xx{}%
\@x{}%
\@y{\@s{0}%
 Helpers
}%
\@xx{}%
\@pvspace{8.0pt}%
\@x{}%
\@y{\@s{0}%
 Add a set of new messages in transit
}%
\@xx{}%
 \@x{ Broadcast ( m ) \.{\defeq} messages \.{'} \.{=} messages \.{\oplus}
 SetToBag ( m )}%
\@pvspace{8.0pt}%
\@x{}%
\@y{\@s{0}%
 Add a message to the bag of messages
}%
\@xx{}%
\@x{ Send ( m ) \.{\defeq} Broadcast ( \{ m \} )}%
\@pvspace{8.0pt}%
\@x{}%
\@y{\@s{0}%
 Remove a message from the bag of messages. Used when a process is done
}%
\@xx{}%
\@x{}%
\@y{\@s{0}%
 processing a message.
}%
\@xx{}%
 \@x{ Discard ( m ) \.{\defeq} messages \.{'} \.{=} messages \.{\ominus}
 SetToBag ( \{ m \} )}%
\@pvspace{8.0pt}%
\@x{}%
\@y{\@s{0}%
 Respond to a message by sending multiple messages
}%
\@xx{}%
\@x{ ReplyBroadcast ( responses ,\, request ) \.{\defeq}}%
 \@x{\@s{16.4} messages \.{'} \.{=} messages \.{\ominus} SetToBag ( \{ request
 \} ) \.{\oplus} SetToBag ( responses )}%
\@pvspace{8.0pt}%
\@x{}%
\@y{\@s{0}%
 Combination of \ensuremath{Send} and \ensuremath{Discard
}}%
\@xx{}%
\@x{ Reply ( response ,\, request ) \.{\defeq}}%
\@x{\@s{16.4} ReplyBroadcast ( \{ response \} ,\, request )}%
\@pvspace{16.0pt}%
\@x{}%
\@y{\@s{0}%
 Return the minimum value from a set, or undefined if the set is empty.
}%
\@xx{}%
 \@x{ Min ( s ) \.{\defeq} {\CHOOSE} x \.{\in} s \.{:} \A\, y \.{\in} s \.{:}
 x \.{\leq} y}%
\@x{}%
\@y{\@s{0}%
 Return the maximum value from a set, or undefined if the set is empty.
}%
\@xx{}%
 \@x{ Max ( s ) \.{\defeq} {\CHOOSE} x \.{\in} s \.{:} \A\, y \.{\in} s \.{:}
 x \.{\geq} y}%
\@pvspace{8.0pt}%
\@x{}%
\@y{\@s{0}%
 Is a final ledger state
}%
\@xx{}%
 \@x{ IsFinalLedgerState ( i ) \.{\defeq} i \.{\in} \{ L\_Executed ,\,
 L\_Aborted \}}%
\@pvspace{8.0pt}%
\@x{}%
\@y{\@s{0}%
 Sender
}%
\@xx{}%
\@x{ Sender \.{\defeq} Min ( Participant )}%
\@pvspace{8.0pt}%
\@x{}%
\@y{\@s{0}%
 Recipient
}%
\@xx{}%
\@x{ Recipient \.{\defeq} Max ( Participant )}%
\@pvspace{8.0pt}%
\@x{}%
\@y{\@s{0}%
 Set of connectors
}%
\@xx{}%
 \@x{ Connector \.{\defeq} Participant \.{\,\backslash\,} \{ Sender ,\,
 Recipient \}}%
\@pvspace{8.0pt}%
\@x{}\midbar\@xx{}%
\@x{}%
\@y{\@s{0}%
 Define type specification for all variables
}%
\@xx{}%
\@pvspace{8.0pt}%
\@x{ TypeOK \.{\defeq} \.{\land} IsABag ( messages )}%
 \@x{\@s{56.14} \.{\land} senderState \.{\in} \{ S\_Ready ,\, S\_Waiting ,\,
 S\_Done \}}%
 \@x{\@s{56.14} \.{\land} ledgerState\@s{3.06} \.{\in} [ Ledger
 \.{\rightarrow} \{ L\_Proposed ,\, L\_Prepared ,\, L\_Executed ,\,
 L\_Aborted \} ]}%
\@pvspace{8.0pt}%
\@x{ Consistency \.{\defeq}}%
 \@x{\@s{16.4} \A\, l1 ,\, l2 \.{\in} Ledger \.{:} {\lnot} \.{\land}
 ledgerState [ l1 ] \.{=} L\_Aborted}%
\@x{\@s{104.69} \.{\land} ledgerState [ l2 ] \.{=} L\_Executed}%
\@pvspace{8.0pt}%
\@x{ Inv \.{\defeq} \.{\land} TypeOK}%
\@x{\@s{34.04} \.{\land} Consistency}%
\@pvspace{8.0pt}%
\@x{}\midbar\@xx{}%
\@x{}%
\@y{\@s{0}%
 Define initial values for all variables
}%
\@xx{}%
\@pvspace{8.0pt}%
\@x{ InitSenderVars\@s{0.27} \.{\defeq} \.{\land} senderState \.{=} S\_Ready}%
\@pvspace{8.0pt}%
 \@x{ InitLedgerVars\@s{1.67} \.{\defeq} \.{\land} ledgerState\@s{3.06} \.{=}
 [ i \.{\in} Ledger \.{\mapsto} L\_Proposed ]}%
\@pvspace{8.0pt}%
\@x{ InitNotaryVars \.{\defeq} \.{\land} notaryState \.{=} N\_Waiting}%
\@pvspace{8.0pt}%
\@x{ Init \.{\defeq} \.{\land} messages \.{=} EmptyBag}%
\@x{\@s{35.70} \.{\land} InitSenderVars}%
\@x{\@s{35.70} \.{\land} InitLedgerVars}%
\@x{\@s{35.70} \.{\land} InitNotaryVars}%
\@pvspace{8.0pt}%
\@x{}\midbar\@xx{}%
\@x{}%
\@y{\@s{0}%
 Define state transitions
}%
\@xx{}%
\@pvspace{8.0pt}%
\@x{}%
\@y{\@s{0}%
 Participant \ensuremath{i} starts off the chain
}%
\@xx{}%
\@x{ Start ( i ) \.{\defeq}}%
\@x{\@s{16.4} \.{\land} senderState \.{=} S\_Ready}%
\@x{\@s{16.4} \.{\land} senderState \.{'} \.{=} S\_Waiting}%
 \@x{\@s{16.4} \.{\land} Send ( [ mtype\@s{9.58} \.{\mapsto} PrepareRequest
 ,\,}%
\@x{\@s{56.16} msource \.{\mapsto} i ,\,}%
\@x{\@s{56.16} mdest\@s{9.64} \.{\mapsto} i \.{+} 1 ] )}%
 \@x{\@s{16.4} \.{\land} {\UNCHANGED} {\langle} ledgerVars ,\, notaryVars
 {\rangle}}%
\@pvspace{8.0pt}%
\@x{}%
\@y{\@s{0}%
 Notary times out
}%
\@xx{}%
\@x{ NotaryTimeout \.{\defeq}}%
\@x{\@s{16.4} \.{\land} notaryState \.{=} N\_Waiting}%
\@x{\@s{16.4} \.{\land} notaryState \.{'} \.{=} N\_Aborted}%
\@x{\@s{16.4} \.{\land} Broadcast (}%
\@x{\@s{48.01} \{ [ mtype\@s{13.68} \.{\mapsto} AbortRequest ,\,}%
\@x{\@s{55.78} msource\@s{4.10} \.{\mapsto} Notary ,\,}%
\@x{\@s{55.78} mdest\@s{13.74} \.{\mapsto} k ] \.{:} k \.{\in} Ledger \} )}%
 \@x{\@s{16.4} \.{\land} {\UNCHANGED} {\langle} senderVars ,\, ledgerVars
 {\rangle}}%
\@pvspace{8.0pt}%
\@x{}%
\@y{\@s{0}%
 Ledger spontaneously aborts
}%
\@xx{}%
\@x{ LedgerAbort ( l ) \.{\defeq}}%
\@x{\@s{16.4} \.{\land} ledgerState [ l ] \.{=} L\_Proposed}%
 \@x{\@s{16.4} \.{\land} ledgerState \.{'} \.{=} [ ledgerState {\EXCEPT}
 {\bang} [ l ] \.{=} L\_Aborted ]}%
\@x{\@s{16.4} \.{\land} Send ( [ mtype\@s{9.58} \.{\mapsto} AbortNotify ,\,}%
\@x{\@s{56.16} msource \.{\mapsto} l ,\,}%
\@x{\@s{56.16} mdest\@s{9.64} \.{\mapsto} l \.{-} 1 ] )}%
 \@x{\@s{16.4} \.{\land} {\UNCHANGED} {\langle} senderVars ,\, notaryVars
 {\rangle}}%
\@pvspace{8.0pt}%
\@x{}\midbar\@xx{}%
\@x{}%
\@y{\@s{0}%
 Message handlers
}%
\@xx{}%
\@x{}%
\@y{\@s{0}%
 \ensuremath{i \.{=}} recipient, \ensuremath{j \.{=}} sender, \ensuremath{m
 \.{=}} message
}%
\@xx{}%
\@pvspace{8.0pt}%
\@x{}%
\@y{\@s{0}%
 Ledger \ensuremath{i} receives a Prepare request from process \ensuremath{j
}}%
\@xx{}%
\@x{ LedgerHandlePrepareRequest ( i ,\, j ,\, m ) \.{\defeq}}%
 \@x{\@s{16.4} \.{\LET} valid \.{\defeq} \.{\land} ledgerState [ i ] \.{=}
 L\_Proposed}%
\@x{\@s{77.16} \.{\land} j \.{=} i \.{-} 1}%
\@x{\@s{16.4} \.{\IN} \.{\lor} \.{\land} valid}%
 \@x{\@s{47.91} \.{\land} ledgerState \.{'} \.{=} [ ledgerState {\EXCEPT}
 {\bang} [ i ] \.{=} L\_Prepared ]}%
 \@x{\@s{47.91} \.{\land} Reply ( [ mtype\@s{9.58} \.{\mapsto} PrepareNotify
 ,\,}%
\@x{\@s{90.47} msource \.{\mapsto} i ,\,}%
\@x{\@s{90.47} mdest\@s{9.64} \.{\mapsto} i \.{+} 1 ] ,\, m )}%
 \@x{\@s{47.91} \.{\land} {\UNCHANGED} {\langle} senderVars ,\, notaryVars
 {\rangle}}%
\@x{\@s{36.79} \.{\lor} \.{\land} {\lnot} valid}%
\@x{\@s{47.91} \.{\land} Discard ( m )}%
 \@x{\@s{47.91} \.{\land} {\UNCHANGED} {\langle} senderVars ,\, ledgerVars ,\,
 notaryVars {\rangle}}%
\@pvspace{8.0pt}%
\@x{}%
\@y{\@s{0}%
 Ledger \ensuremath{i} receives an Execute request from process \ensuremath{j
}}%
\@xx{}%
\@x{ LedgerHandleExecuteRequest ( i ,\, j ,\, m ) \.{\defeq}}%
 \@x{\@s{16.4} \.{\LET} valid \.{\defeq} \.{\land} ledgerState [ i ] \.{=}
 L\_Prepared}%
\@x{\@s{77.16} \.{\land} j \.{=} Notary}%
\@x{\@s{16.4} \.{\IN} \.{\lor} \.{\land} valid}%
 \@x{\@s{47.91} \.{\land} ledgerState \.{'} \.{=} [ ledgerState {\EXCEPT}
 {\bang} [ i ] \.{=} L\_Executed ]}%
 \@x{\@s{47.91} \.{\land} Reply ( [ mtype\@s{9.58} \.{\mapsto} ExecuteNotify
 ,\,}%
\@x{\@s{90.47} msource \.{\mapsto} i ,\,}%
\@x{\@s{90.47} mdest\@s{9.64} \.{\mapsto} i \.{-} 1 ] ,\, m )}%
 \@x{\@s{47.91} \.{\land} {\UNCHANGED} {\langle} senderVars ,\, notaryVars
 {\rangle}}%
\@x{\@s{36.79} \.{\lor} \.{\land} {\lnot} valid}%
\@x{\@s{47.91} \.{\land} Discard ( m )}%
 \@x{\@s{47.91} \.{\land} {\UNCHANGED} {\langle} senderVars ,\, ledgerVars ,\,
 notaryVars {\rangle}}%
\@pvspace{8.0pt}%
\@x{}%
\@y{\@s{0}%
 Ledger \ensuremath{i} receives an Abort request from process \ensuremath{j
}}%
\@xx{}%
\@x{ LedgerHandleAbortRequest ( i ,\, j ,\, m ) \.{\defeq}}%
 \@x{\@s{16.4} \.{\LET} valid \.{\defeq} \.{\land} \.{\lor} ledgerState [ i ]
 \.{=} L\_Proposed}%
\@x{\@s{88.27} \.{\lor} ledgerState [ i ] \.{=} L\_Prepared}%
\@x{\@s{77.16} \.{\land} j \.{=} Notary}%
\@x{\@s{16.4} \.{\IN} \.{\lor} \.{\land} valid}%
 \@x{\@s{47.91} \.{\land} ledgerState \.{'} \.{=} [ ledgerState {\EXCEPT}
 {\bang} [ i ] \.{=} L\_Aborted ]}%
 \@x{\@s{47.91} \.{\land} Reply ( [ mtype\@s{9.58} \.{\mapsto} AbortNotify
 ,\,}%
\@x{\@s{90.47} msource \.{\mapsto} i ,\,}%
\@x{\@s{90.47} mdest\@s{9.64} \.{\mapsto} i \.{-} 1 ] ,\, m )}%
 \@x{\@s{47.91} \.{\land} {\UNCHANGED} {\langle} senderVars ,\, notaryVars
 {\rangle}}%
\@x{\@s{36.79} \.{\lor} \.{\land} {\lnot} valid}%
\@x{\@s{47.91} \.{\land} Discard ( m )}%
 \@x{\@s{47.91} \.{\land} {\UNCHANGED} {\langle} senderVars ,\, ledgerVars ,\,
 notaryVars {\rangle}}%
\@pvspace{8.0pt}%
\@x{}%
\@y{\@s{0}%
 Ledger \ensuremath{i} receives a message
}%
\@xx{}%
\@x{ LedgerReceive ( i ,\, j ,\, m ) \.{\defeq}}%
\@x{\@s{16.4} \.{\lor} \.{\land} m . mtype \.{=} PrepareRequest}%
\@x{\@s{27.51} \.{\land} LedgerHandlePrepareRequest ( i ,\, j ,\, m )}%
\@x{\@s{16.4} \.{\lor} \.{\land} m . mtype \.{=} ExecuteRequest}%
\@x{\@s{27.51} \.{\land} LedgerHandleExecuteRequest ( i ,\, j ,\, m )}%
\@x{\@s{16.4} \.{\lor} \.{\land} m . mtype \.{=} AbortRequest}%
\@x{\@s{27.51} \.{\land} LedgerHandleAbortRequest ( i ,\, j ,\, m )}%
\@pvspace{8.0pt}%
\@x{}%
\@y{\@s{0}%
 Ledger \ensuremath{j} notifies sender that the transfer is executed
}%
\@xx{}%
\@x{ SenderHandleExecuteNotify ( i ,\, j ,\, m ) \.{\defeq}}%
\@x{\@s{16.4} \.{\lor} \.{\land} senderState \.{=} S\_Waiting}%
\@x{\@s{27.51} \.{\land} senderState \.{'} \.{=} S\_Done}%
\@x{\@s{27.51} \.{\land} Discard ( m )}%
 \@x{\@s{27.51} \.{\land} {\UNCHANGED} {\langle} ledgerVars ,\, notaryVars
 {\rangle}}%
\@x{\@s{16.4} \.{\lor} \.{\land} senderState \.{\neq} S\_Waiting}%
\@x{\@s{27.51} \.{\land} Discard ( m )}%
 \@x{\@s{27.51} \.{\land} {\UNCHANGED} {\langle} senderVars ,\, ledgerVars ,\,
 notaryVars {\rangle}}%
\@pvspace{8.0pt}%
\@x{}%
\@y{\@s{0}%
 Ledger \ensuremath{j} notifies sender that the transfer is aborted
}%
\@xx{}%
\@x{ SenderHandleAbortNotify ( i ,\, j ,\, m ) \.{\defeq}}%
 \@x{\@s{16.4} \.{\LET} isSenderWaiting \.{\defeq} \.{\lor} senderState \.{=}
 S\_Waiting}%
\@x{\@s{128.27} \.{\lor} senderState \.{=} S\_Ready}%
\@x{\@s{16.4} \.{\IN} \.{\lor} \.{\land} isSenderWaiting}%
\@x{\@s{47.91} \.{\land} senderState \.{'} \.{=} S\_Done}%
\@x{\@s{47.91} \.{\land} Discard ( m )}%
 \@x{\@s{47.91} \.{\land} {\UNCHANGED} {\langle} ledgerVars ,\, notaryVars
 {\rangle}}%
\@x{\@s{36.79} \.{\lor} \.{\land} {\lnot} isSenderWaiting}%
\@x{\@s{47.91} \.{\land} Discard ( m )}%
 \@x{\@s{47.91} \.{\land} {\UNCHANGED} {\langle} senderVars ,\, ledgerVars ,\,
 notaryVars {\rangle}}%
\@pvspace{8.0pt}%
\@x{}%
\@y{\@s{0}%
 Sender receives a message
}%
\@xx{}%
\@x{ SenderReceive ( i ,\, j ,\, m ) \.{\defeq}}%
\@x{\@s{16.4} \.{\lor} \.{\land} m . mtype \.{=} ExecuteNotify}%
\@x{\@s{27.51} \.{\land} SenderHandleExecuteNotify ( i ,\, j ,\, m )}%
\@x{\@s{16.4} \.{\lor} \.{\land} m . mtype \.{=} AbortNotify}%
\@x{\@s{27.51} \.{\land} SenderHandleAbortNotify ( i ,\, j ,\, m )}%
\@pvspace{8.0pt}%
\@x{}%
\@y{\@s{0}%
 Ledger \ensuremath{j} notifies recipient that the transfer is prepared
}%
\@xx{}%
\@x{ RecipientHandlePrepareNotify ( i ,\, j ,\, m ) \.{\defeq}}%
 \@x{\@s{16.4} \.{\land} Reply ( [ mtype\@s{12.29} \.{\mapsto}
 SubmitReceiptRequest ,\,}%
\@x{\@s{58.96} msource\@s{2.71} \.{\mapsto} i ,\,}%
\@x{\@s{58.96} mdest\@s{12.35} \.{\mapsto} Notary ,\,}%
\@x{\@s{58.96} mreceipt\@s{1.49} \.{\mapsto} R\_ReceiptSignature ] ,\, m )}%
 \@x{\@s{16.4} \.{\land} {\UNCHANGED} {\langle} senderVars ,\, ledgerVars ,\,
 notaryVars {\rangle}}%
\@pvspace{8.0pt}%
\@x{}%
\@y{\@s{0}%
 Recipient receives a message
}%
\@xx{}%
\@x{ RecipientReceive ( i ,\, j ,\, m ) \.{\defeq}}%
\@x{\@s{16.4} \.{\land} m . mtype \.{=} PrepareNotify}%
\@x{\@s{16.4} \.{\land} RecipientHandlePrepareNotify ( i ,\, j ,\, m )}%
\@pvspace{8.0pt}%
\@x{}%
\@y{\@s{0}%
 Ledger \ensuremath{j} notifies connector \ensuremath{i} that the transfer is
 prepared
}%
\@xx{}%
\@x{ ConnectorHandlePrepareNotify ( i ,\, j ,\, m ) \.{\defeq}}%
 \@x{\@s{16.4} \.{\land} Reply ( [ mtype\@s{9.58} \.{\mapsto} PrepareRequest
 ,\,}%
\@x{\@s{58.96} msource \.{\mapsto} i ,\,}%
\@x{\@s{58.96} mdest\@s{9.64} \.{\mapsto} i \.{+} 1 ] ,\, m )}%
 \@x{\@s{16.4} \.{\land} {\UNCHANGED} {\langle} senderVars ,\, ledgerVars ,\,
 notaryVars {\rangle}}%
\@pvspace{8.0pt}%
\@x{}%
\@y{\@s{0}%
 Ledger \ensuremath{j} notifies connector \ensuremath{i} that the transfer is
 executed
}%
\@xx{}%
\@x{ ConnectorHandleExecuteNotify ( i ,\, j ,\, m ) \.{\defeq}}%
 \@x{\@s{16.4} \.{\land} Reply ( [ mtype\@s{9.58} \.{\mapsto} ExecuteRequest
 ,\,}%
\@x{\@s{58.96} msource \.{\mapsto} i ,\,}%
\@x{\@s{58.96} mdest\@s{9.64} \.{\mapsto} i \.{-} 1 ] ,\, m )}%
 \@x{\@s{16.4} \.{\land} {\UNCHANGED} {\langle} senderVars ,\, ledgerVars ,\,
 notaryVars {\rangle}}%
\@pvspace{8.0pt}%
\@x{}%
\@y{\@s{0}%
 Ledger \ensuremath{j} notifies connector \ensuremath{i} that the transfer is
 aborted
}%
\@xx{}%
\@x{ ConnectorHandleAbortNotify ( i ,\, j ,\, m ) \.{\defeq}}%
\@x{\@s{16.4} \.{\land} Discard ( m )}%
 \@x{\@s{16.4} \.{\land} {\UNCHANGED} {\langle} senderVars ,\, ledgerVars ,\,
 notaryVars {\rangle}}%
\@pvspace{8.0pt}%
\@x{}%
\@y{\@s{0}%
 Connector receives a message
}%
\@xx{}%
\@x{ ConnectorReceive ( i ,\, j ,\, m ) \.{\defeq}}%
\@x{\@s{16.4} \.{\lor} \.{\land} m . mtype \.{=} PrepareNotify}%
\@x{\@s{27.51} \.{\land} ConnectorHandlePrepareNotify ( i ,\, j ,\, m )}%
\@x{\@s{16.4} \.{\lor} \.{\land} m . mtype \.{=} ExecuteNotify}%
\@x{\@s{27.51} \.{\land} ConnectorHandleExecuteNotify ( i ,\, j ,\, m )}%
\@x{\@s{16.4} \.{\lor} \.{\land} m . mtype \.{=} AbortNotify}%
\@x{\@s{27.51} \.{\land} ConnectorHandleAbortNotify ( i ,\, j ,\, m )}%
\@pvspace{8.0pt}%
\@x{}%
\@y{\@s{0}%
 Notary receives a signed receipt
}%
\@xx{}%
\@x{ NotaryHandleSubmitReceiptRequest ( i ,\, j ,\, m ) \.{\defeq}}%
\@x{\@s{16.4} \.{\lor} \.{\land} m . mreceipt \.{=} R\_ReceiptSignature}%
\@x{\@s{27.51} \.{\land} notaryState \.{=} N\_Waiting}%
\@x{\@s{27.51} \.{\land} notaryState \.{'} \.{=} N\_Committed}%
\@x{\@s{27.51} \.{\land} ReplyBroadcast (}%
\@x{\@s{46.82} \{ [ mtype\@s{13.68} \.{\mapsto} ExecuteRequest ,\,}%
\@x{\@s{54.59} msource\@s{4.1} \.{\mapsto} i ,\,}%
 \@x{\@s{54.59} mdest\@s{13.74} \.{\mapsto} k ] \.{:} k \.{\in} Ledger \} ,\,
 m )}%
 \@x{\@s{27.51} \.{\land} {\UNCHANGED} {\langle} senderVars ,\, ledgerVars
 {\rangle}}%
\@x{\@s{16.4} \.{\lor} \.{\land} notaryState \.{\neq} N\_Waiting}%
\@x{\@s{27.51} \.{\land} Discard ( m )}%
 \@x{\@s{27.51} \.{\land} {\UNCHANGED} {\langle} senderVars ,\, ledgerVars ,\,
 notaryVars {\rangle}}%
\@pvspace{8.0pt}%
\@x{}%
\@y{\@s{0}%
 Notary receives a message
}%
\@xx{}%
\@x{ NotaryReceive ( i ,\, j ,\, m ) \.{\defeq}}%
\@x{\@s{16.4} \.{\land} m . mtype \.{=} SubmitReceiptRequest}%
\@x{\@s{16.4} \.{\land} NotaryHandleSubmitReceiptRequest ( i ,\, j ,\, m )}%
\@pvspace{8.0pt}%
\@x{}%
\@y{\@s{0}%
 Receive a message
}%
\@xx{}%
\@x{ Receive ( m ) \.{\defeq}}%
\@x{\@s{16.4} \.{\LET} i\@s{0.42} \.{\defeq} m . mdest}%
\@x{\@s{36.79} j \.{\defeq} m . msource}%
\@x{\@s{16.4} \.{\IN} \.{\lor} \.{\land} i \.{\in} Ledger}%
\@x{\@s{47.91} \.{\land} LedgerReceive ( i ,\, j ,\, m )}%
\@x{\@s{36.79} \.{\lor} \.{\land} i \.{=} Sender}%
\@x{\@s{47.91} \.{\land} SenderReceive ( i ,\, j ,\, m )}%
\@x{\@s{36.79} \.{\lor} \.{\land} i \.{=} Recipient}%
\@x{\@s{47.91} \.{\land} RecipientReceive ( i ,\, j ,\, m )}%
\@x{\@s{36.79} \.{\lor} \.{\land} i \.{\in} Connector}%
\@x{\@s{47.91} \.{\land} ConnectorReceive ( i ,\, j ,\, m )}%
\@x{\@s{36.79} \.{\lor} \.{\land} i \.{=} Notary}%
\@x{\@s{47.91} \.{\land} NotaryReceive ( i ,\, j ,\, m )}%
\@pvspace{8.0pt}%
\@x{}%
\@y{\@s{0}%
 End of message handlers
}%
\@xx{}%
\@x{}\midbar\@xx{}%
\@x{}%
\@y{\@s{0}%
 Defines how the variables may transition
}%
\@xx{}%
\@pvspace{8.0pt}%
\@x{ Termination \.{\defeq}}%
 \@x{\@s{16.4} \.{\land} \A\, l \.{\in} Ledger \.{:} IsFinalLedgerState (
 ledgerState [ l ] )}%
\@x{\@s{16.4} \.{\land} senderState \.{=} S\_Done}%
\@x{\@s{16.4} \.{\land} {\UNCHANGED} vars}%
\@pvspace{8.0pt}%
\@x{ Next \.{\defeq} \.{\lor} Start ( Sender )}%
\@x{\@s{39.83} \.{\lor} NotaryTimeout}%
 \@x{\@s{39.83} \.{\lor} \E\, l\@s{5.35} \.{\in} Ledger \.{:} LedgerAbort ( l
 )}%
 \@x{\@s{39.83} \.{\lor} \E\, m \.{\in} {\DOMAIN} messages \.{:} Receive ( m
 )}%
\@x{\@s{39.83} \.{\lor} Termination}%
\@pvspace{8.0pt}%
\@x{}%
\@y{\@s{0}%
 The specification must start with the initial state and transition according
}%
\@xx{}%
\@x{}%
\@y{\@s{0}%
 to \ensuremath{Next}.
}%
\@xx{}%
\@x{ Spec \.{\defeq} Init \.{\land} {\Box} [ Next ]_{ vars}}%
\@pvspace{8.0pt}%
\@x{}\bottombar\@xx{}%
\end{document}