Artifact Content
Not logged in

Artifact 6faa06b86d76ce1ddb43b74cff807f5e8ccce656:


\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}
\stepcounter{subsection}
\setcounter{page}{19}
\subsection{Formal Specification: Universal mode}
\label{sec:universal-spec}
\tlatex
\setboolean{shading}{true}
\@x{}\moduleLeftDash\@xx{ {\MODULE} Universal}\moduleRightDash\@xx{}%
\begin{lcom}{0}%
\begin{cpar}{0}{T}{F}{2.5}{0}{}%
Formal Specification in TLA\ensuremath{\.{\mbox{}^+}} of the
 Interledger Protocol \ensuremath{Universal} (\ensuremath{ILP}/\ensuremath{U})
\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 ,\, FiniteSets ,\, 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}%
 Sender states
}%
\@xx{}%
\@x{ {\CONSTANTS} S\_Ready ,\, S\_ProposalWaiting ,\, S\_Waiting ,\, S\_Done}%
\@pvspace{8.0pt}%
\@x{}%
\@y{\@s{0}%
 Connector states
}%
\@xx{}%
\@x{ {\CONSTANTS} C\_Ready ,\, C\_Proposed}%
\@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} SubpaymentProposalRequest ,\, SubpaymentProposalResponse}%
\@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}%
 Under synchrony we are allowed to have a global clock
}%
\@xx{}%
\@x{ {\VARIABLE} clock}%
\@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}%
 Whether the sender has received a response from a given connector
}%
\@xx{}%
\@x{ {\VARIABLE} senderProposalResponses}%
\@pvspace{8.0pt}%
\@x{}%
\@y{\@s{0}%
 All sender variables
}%
\@xx{}%
 \@x{ senderVars \.{\defeq} {\langle} senderState ,\, senderProposalResponses
 {\rangle}}%
\@x{}\midbar\@xx{}%
\@x{}%
\@y{\@s{0}%
 Connector variables
}%
\@xx{}%
\@pvspace{8.0pt}%
\@x{}%
\@y{\@s{0}%
 State of the connector (\ensuremath{C\_Ready}, \ensuremath{C\_Proposed})
}%
\@xx{}%
\@x{ {\VARIABLE} connectorState}%
\@pvspace{8.0pt}%
\@x{}%
\@y{\@s{0}%
 All sender variables
}%
\@xx{}%
\@x{ connectorVars \.{\defeq} {\langle} connectorState {\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}%
 The timeouts for each of the the transfers
}%
\@xx{}%
\@x{ {\VARIABLE} ledgerExpiration}%
\@pvspace{8.0pt}%
\@x{}%
\@y{\@s{0}%
 All ledger variables
}%
\@xx{}%
 \@x{ ledgerVars \.{\defeq} {\langle} ledgerState ,\, ledgerExpiration
 {\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} clock ,\, messages ,\, senderVars ,\,
 connectorVars ,\, ledgerVars {\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{}%
\@y{\@s{0}%
 The clock value we expect to be at after the proposal phase
}%
\@xx{}%
\@x{ ClockAfterProposal \.{\defeq} 2 \.{*} Cardinality ( Connector ) \.{+} 2}%
\@pvspace{8.0pt}%
\@x{}%
\@y{\@s{0}%
 The clock value we expect after the preparation phase
}%
\@xx{}%
 \@x{ ClockAfterPrepare \.{\defeq} ClockAfterProposal \.{+} 2 \.{*}
 Cardinality ( Ledger ) \.{+} 1}%
\@pvspace{8.0pt}%
\@x{}%
\@y{\@s{0}%
 The clock value we expect to be at after the execution phase
}%
\@xx{}%
 \@x{ ClockAfterExecution \.{\defeq} ClockAfterPrepare \.{+} 2 \.{*}
 Cardinality ( Ledger ) \.{+} 1}%
\@x{}\midbar\@xx{}%
\@x{}%
\@y{\@s{0}%
 Define type specification for all variables
}%
\@xx{}%
\@pvspace{8.0pt}%
\@x{ TypeOK \.{\defeq} \.{\land} clock \.{\in} Nat}%
\@x{\@s{56.14} \.{\land} IsABag ( messages )}%
 \@x{\@s{56.14} \.{\land} senderState \.{\in} \{ S\_Ready ,\,
 S\_ProposalWaiting ,\, S\_Waiting ,\, S\_Done \}}%
 \@x{\@s{56.14} \.{\land} senderProposalResponses \.{\in} [ Connector
 \.{\rightarrow} {\BOOLEAN} ]}%
 \@x{\@s{56.14} \.{\land} connectorState \.{\in} [ Connector \.{\rightarrow}
 \{ C\_Ready ,\, C\_Proposed \} ]}%
 \@x{\@s{56.14} \.{\land} ledgerState \.{\in} [ Ledger \.{\rightarrow} \{
 L\_Proposed ,\, L\_Prepared ,\, L\_Executed ,\, L\_Aborted \} ]}%
 \@x{\@s{56.14} \.{\land} ledgerExpiration \.{\in} [ Ledger \.{\rightarrow}
 Nat ]}%
\@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 \.{\defeq} \.{\land} senderState \.{=} S\_Ready}%
 \@x{\@s{85.43} \.{\land} senderProposalResponses \.{=} [ i \.{\in} Connector
 \.{\mapsto} {\FALSE} ]}%
\@pvspace{8.0pt}%
 \@x{ InitConnectorVars \.{\defeq} connectorState \.{=} [ i \.{\in} Connector
 \.{\mapsto} C\_Ready ]}%
\@pvspace{8.0pt}%
 \@x{ InitLedgerVars \.{\defeq} \.{\land} ledgerState \.{=} [ i\@s{3.38}
 \.{\in} Ledger \.{\mapsto} L\_Proposed ]}%
 \@x{\@s{84.03} \.{\land} ledgerExpiration \.{=} [ i \.{\in} Ledger
 \.{\mapsto} ClockAfterExecution \.{-} i ]}%
\@pvspace{8.0pt}%
\@x{ Init \.{\defeq} \.{\land} clock \.{=} 0}%
\@x{\@s{35.70} \.{\land} messages \.{=} EmptyBag}%
\@x{\@s{35.70} \.{\land} InitSenderVars}%
\@x{\@s{35.70} \.{\land} InitConnectorVars}%
\@x{\@s{35.70} \.{\land} InitLedgerVars}%
\@pvspace{8.0pt}%
\@x{}\midbar\@xx{}%
\@x{}%
\@y{\@s{0}%
 Define state transitions
}%
\@xx{}%
\@pvspace{8.0pt}%
\@x{}%
\@y{\@s{0}%
 Participant \ensuremath{i} proposes all the subpayments
}%
\@xx{}%
\@x{ StartProposalPhase ( i ) \.{\defeq}}%
\@x{\@s{16.4} \.{\land} senderState \.{=} S\_Ready}%
\@x{\@s{16.4} \.{\land} senderState \.{'} \.{=} S\_ProposalWaiting}%
\@x{\@s{16.4} \.{\land} Broadcast ( \{ [}%
\@x{\@s{35.71} mtype\@s{13.68} \.{\mapsto} SubpaymentProposalRequest ,\,}%
\@x{\@s{35.71} msource\@s{4.1} \.{\mapsto} i ,\,}%
\@x{\@s{35.71} mdest\@s{13.74} \.{\mapsto} k}%
\@x{\@s{27.51} ] \.{:} k \.{\in} Connector \} )}%
 \@x{\@s{16.4} \.{\land} {\UNCHANGED} {\langle} ledgerVars ,\, connectorVars
 ,\, senderProposalResponses {\rangle}}%
\@pvspace{8.0pt}%
\@x{}%
\@y{\@s{0}%
 Participant \ensuremath{i} starts off the preparation chain
}%
\@xx{}%
\@x{ StartPreparationPhase ( i ) \.{\defeq}}%
\@x{\@s{16.4} \.{\land} senderState \.{=} S\_ProposalWaiting}%
 \@x{\@s{16.4} \.{\land} \E\, p \.{\in} {\DOMAIN} senderProposalResponses
 \.{:} senderProposalResponses [ p ]}%
\@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 ,\, connectorVars
 ,\, senderProposalResponses {\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 ,\, connectorVars
 ,\, ledgerExpiration {\rangle}}%
\@pvspace{8.0pt}%
\@x{}%
\@y{\@s{0}%
 Transfer times out
}%
\@xx{}%
\@x{ LedgerTimeout ( l ) \.{\defeq}}%
\@x{\@s{16.4} \.{\land} {\lnot} IsFinalLedgerState ( ledgerState [ l ] )}%
\@x{\@s{16.4} \.{\land} ledgerExpiration [ l ] \.{\leq} clock}%
 \@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 ,\, connectorVars
 ,\, ledgerExpiration {\rangle}}%
\@pvspace{8.0pt}%
\@x{}%
\@y{\@s{0}%
 If no messages are in flight and the sender isn\mbox{'}t doing anything,
 advance the
}%
\@xx{}%
\@x{}%
\@y{\@s{0}%
 clock
}%
\@xx{}%
\@x{ NothingHappens \.{\defeq}}%
 \@x{\@s{16.4} \.{\land} clock \.{\leq} Max ( \{ ledgerExpiration [ x ] \.{:}
 x \.{\in} Ledger \} )}%
\@x{\@s{16.4} \.{\land} BagCardinality ( messages ) \.{=} 0}%
\@x{\@s{16.4} \.{\land} senderState \.{\neq} S\_Ready}%
\@x{\@s{16.4} \.{\land} \.{\lor} senderState \.{\neq} S\_ProposalWaiting}%
 \@x{\@s{27.51} \.{\lor} \A\, p \.{\in} {\DOMAIN} senderProposalResponses
 \.{:} {\lnot} senderProposalResponses [ p ]}%
 \@x{\@s{16.4} \.{\land} {\UNCHANGED} {\langle} messages ,\, senderVars ,\,
 connectorVars ,\, ledgerVars {\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 participant
 \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} i \.{\in} Ledger}%
 \@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 ,\, connectorVars
 ,\, ledgerExpiration {\rangle}}%
\@x{\@s{36.79} \.{\lor} \.{\land} {\lnot} valid}%
\@x{\@s{47.91} \.{\land} i \.{\in} Ledger}%
\@x{\@s{47.91} \.{\land} Discard ( m )}%
 \@x{\@s{47.91} \.{\land} {\UNCHANGED} {\langle} senderVars ,\, connectorVars
 ,\, ledgerVars {\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} ledgerExpiration [ i ] \.{>} clock}%
\@x{\@s{77.16} \.{\land} m . mreceipt \.{=} R\_ReceiptSignature}%
\@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{12.29} \.{\mapsto} ExecuteNotify
 ,\,}%
\@x{\@s{90.47} msource\@s{2.71} \.{\mapsto} i ,\,}%
\@x{\@s{90.47} mdest\@s{12.35} \.{\mapsto} i \.{-} 1 ,\,}%
\@x{\@s{90.47} mreceipt\@s{1.49} \.{\mapsto} m . mreceipt ] ,\, m )}%
 \@x{\@s{47.91} \.{\land} {\UNCHANGED} {\langle} senderVars ,\, connectorVars
 ,\, ledgerExpiration {\rangle}}%
\@x{\@s{36.79} \.{\lor} \.{\land} {\lnot} valid}%
\@x{\@s{47.91} \.{\land} Discard ( m )}%
 \@x{\@s{47.91} \.{\land} {\UNCHANGED} {\langle} senderVars ,\, connectorVars
 ,\, ledgerVars {\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 )}%
\@pvspace{8.0pt}%
\@x{}%
\@y{\@s{0}%
 Sender receives a \ensuremath{SubpaymentProposal} request
}%
\@xx{}%
\@x{ SenderHandleSubpaymentProposalResponse ( i ,\, j ,\, m ) \.{\defeq}}%
\@x{\@s{16.4} \.{\land} i \.{=} Sender}%
 \@x{\@s{16.4} \.{\land} senderProposalResponses \.{'} \.{=} [
 senderProposalResponses {\EXCEPT} {\bang} [ j ] \.{=} {\TRUE} ]}%
\@x{\@s{16.4} \.{\land} Discard ( m )}%
 \@x{\@s{16.4} \.{\land} {\UNCHANGED} {\langle} connectorVars ,\, ledgerVars
 ,\, senderState {\rangle}}%
\@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 ,\, connectorVars
 ,\, senderProposalResponses {\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 ,\, connectorVars
 ,\, ledgerVars {\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} senderState \.{\in} \{
 S\_ProposalWaiting ,\, S\_Waiting ,\, 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 ,\, connectorVars
 ,\, senderProposalResponses {\rangle}}%
\@x{\@s{36.79} \.{\lor} \.{\land} {\lnot} isSenderWaiting}%
\@x{\@s{47.91} \.{\land} Discard ( m )}%
 \@x{\@s{47.91} \.{\land} {\UNCHANGED} {\langle} senderVars ,\, connectorVars
 ,\, ledgerVars {\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 \.{=} SubpaymentProposalResponse}%
 \@x{\@s{27.51} \.{\land} SenderHandleSubpaymentProposalResponse ( i ,\, j ,\,
 m )}%
\@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} \.{\lor} \.{\land} Reply ( [ mtype\@s{12.29} \.{\mapsto}
 ExecuteRequest ,\,}%
\@x{\@s{70.07} msource\@s{2.71} \.{\mapsto} i ,\,}%
\@x{\@s{70.07} mdest\@s{12.35} \.{\mapsto} i \.{-} 1 ,\,}%
\@x{\@s{70.07} mreceipt\@s{1.49} \.{\mapsto} R\_ReceiptSignature ] ,\, m )}%
 \@x{\@s{27.51} \.{\land} {\UNCHANGED} {\langle} senderVars ,\, connectorVars
 ,\, ledgerVars {\rangle}}%
\@pvspace{8.0pt}%
\@x{}%
\@y{\@s{0}%
 Recipient receives a message
}%
\@xx{}%
\@x{ RecipientReceive ( i ,\, j ,\, m ) \.{\defeq}}%
\@x{\@s{16.4} \.{\lor} \.{\land} m . mtype \.{=} PrepareNotify}%
\@x{\@s{27.51} \.{\land} RecipientHandlePrepareNotify ( i ,\, j ,\, m )}%
\@pvspace{8.0pt}%
\@x{}%
\@y{\@s{0}%
 Connector \ensuremath{i} receives a \ensuremath{SubpaymentProposal} request
}%
\@xx{}%
\@x{ ConnectorHandleSubpaymentProposalRequest ( i ,\, j ,\, m ) \.{\defeq}}%
 \@x{\@s{16.4} \.{\land} connectorState \.{'} \.{=} [ connectorState {\EXCEPT}
 {\bang} [ i ] \.{=} C\_Proposed ]}%
 \@x{\@s{16.4} \.{\land} Reply ( [ mtype\@s{13.68} \.{\mapsto}
 SubpaymentProposalResponse ,\,}%
\@x{\@s{58.96} msource\@s{4.1} \.{\mapsto} i ,\,}%
\@x{\@s{58.96} mdest\@s{13.74} \.{\mapsto} j ] ,\, m )}%
 \@x{\@s{16.4} \.{\land} {\UNCHANGED} {\langle} senderVars ,\, ledgerVars
 {\rangle}}%
\@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} \.{\lor} \.{\land} Reply ( [ mtype\@s{9.58} \.{\mapsto}
 PrepareRequest ,\,}%
\@x{\@s{70.07} msource \.{\mapsto} i ,\,}%
\@x{\@s{70.07} mdest\@s{9.64} \.{\mapsto} i \.{+} 1 ] ,\, m )}%
 \@x{\@s{27.51} \.{\land} {\UNCHANGED} {\langle} senderVars ,\, connectorVars
 ,\, ledgerVars {\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{12.29} \.{\mapsto} ExecuteRequest
 ,\,}%
\@x{\@s{58.96} msource\@s{2.71} \.{\mapsto} i ,\,}%
\@x{\@s{58.96} mdest\@s{12.35} \.{\mapsto} i \.{-} 1 ,\,}%
\@x{\@s{58.96} mreceipt\@s{1.49} \.{\mapsto} m . mreceipt ] ,\, m )}%
 \@x{\@s{16.4} \.{\land} {\UNCHANGED} {\langle} senderVars ,\, connectorVars
 ,\, ledgerVars {\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 ,\, connectorVars
 ,\, ledgerVars {\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 \.{=} SubpaymentProposalRequest}%
 \@x{\@s{27.51} \.{\land} ConnectorHandleSubpaymentProposalRequest ( i ,\, j
 ,\, m )}%
\@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}%
 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 )}%
\@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} \.{\land} \.{\lor} StartProposalPhase ( Sender
 )}%
\@x{\@s{62.05} \.{\lor} StartPreparationPhase ( Sender )}%
 \@x{\@s{62.05} \.{\lor} \E\, l\@s{5.35} \.{\in} Ledger \.{:} LedgerAbort ( l
 )}%
 \@x{\@s{62.05} \.{\lor} \E\, l\@s{5.35} \.{\in} Ledger \.{:} LedgerTimeout (
 l )}%
 \@x{\@s{62.05} \.{\lor} \E\, m \.{\in} {\DOMAIN} messages \.{:} Receive ( m
 )}%
\@x{\@s{62.05} \.{\lor} NothingHappens}%
\@x{\@s{50.94} \.{\land} clock \.{'} \.{=} clock \.{+} 1}%
\@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}