Hex Artifact Content
Not logged in

## Artifact 6faa06b86d76ce1ddb43b74cff807f5e8ccce656:

0000: 5c 62 61 74 63 68 6d 6f 64 65 20 25 25 20 53 75  \batchmode %% Su
0010: 70 70 72 65 73 73 65 73 20 6d 6f 73 74 20 74 65  ppresses most te
0020: 72 6d 69 6e 61 6c 20 6f 75 74 70 75 74 2e 0a 5c  rminal output..\
0030: 64 6f 63 75 6d 65 6e 74 63 6c 61 73 73 5b 6c 65  documentclass[le
0040: 74 74 65 72 70 61 70 65 72 2c 74 77 6f 63 6f 6c  tterpaper,twocol
0050: 75 6d 6e 2c 31 30 70 74 5d 7b 61 72 74 69 63 6c  umn,10pt]{articl
0060: 65 7d 0a 5c 75 73 65 70 61 63 6b 61 67 65 7b 63  e}.\usepackage{c
0070: 6f 6c 6f 72 7d 0a 5c 75 73 65 70 61 63 6b 61 67  olor}.\usepackag
0080: 65 7b 69 6c 70 73 70 65 63 7d 0a 25 20 5c 75 73  e{ilpspec}.% \us
0090: 65 70 61 63 6b 61 67 65 7b 75 73 65 6e 69 78 7d  epackage{usenix}
00a0: 0a 5c 64 65 66 69 6e 65 63 6f 6c 6f 72 7b 62 6f  .\definecolor{bo
00b0: 78 73 68 61 64 65 7d 7b 67 72 61 79 7d 7b 30 2e  xshade}{gray}{0.
00c0: 39 35 7d 0a 0a 5c 73 65 74 6c 65 6e 67 74 68 7b  95}..\setlength{
00d0: 5c 68 65 61 64 68 65 69 67 68 74 7d 7b 30 2e 30  \headheight}{0.0
00e0: 69 6e 7d 0a 0a 5c 75 73 65 70 61 63 6b 61 67 65  in}..\usepackage
00f0: 7b 6c 61 74 65 78 73 79 6d 7d 0a 5c 75 73 65 70  {latexsym}.\usep
0100: 61 63 6b 61 67 65 7b 69 66 74 68 65 6e 7d 0a 25  ackage{ifthen}.%
0110: 20 5c 75 73 65 70 61 63 6b 61 67 65 7b 63 6f 6c   \usepackage{col
0120: 6f 72 7d 0a 5c 75 73 65 70 61 63 6b 61 67 65 7b  or}.\usepackage{
0130: 74 6c 61 74 65 78 7d 0a 0a 5c 62 65 67 69 6e 7b  tlatex}..\begin{
0140: 64 6f 63 75 6d 65 6e 74 7d 0a 5c 6f 6e 65 63 6f  document}.\oneco
0150: 6c 75 6d 6e 0a 5c 61 70 70 65 6e 64 69 78 0a 5c  lumn.\appendix.\
0160: 73 74 65 70 63 6f 75 6e 74 65 72 7b 73 65 63 74  stepcounter{sect
0170: 69 6f 6e 7d 0a 5c 73 74 65 70 63 6f 75 6e 74 65  ion}.\stepcounte
0180: 72 7b 73 75 62 73 65 63 74 69 6f 6e 7d 0a 5c 73  r{subsection}.\s
0190: 74 65 70 63 6f 75 6e 74 65 72 7b 73 75 62 73 65  tepcounter{subse
01a0: 63 74 69 6f 6e 7d 0a 5c 73 74 65 70 63 6f 75 6e  ction}.\stepcoun
01b0: 74 65 72 7b 73 75 62 73 65 63 74 69 6f 6e 7d 0a  ter{subsection}.
01c0: 5c 73 65 74 63 6f 75 6e 74 65 72 7b 70 61 67 65  \setcounter{page
01d0: 7d 7b 31 39 7d 0a 5c 73 75 62 73 65 63 74 69 6f  }{19}.\subsectio
01e0: 6e 7b 46 6f 72 6d 61 6c 20 53 70 65 63 69 66 69  n{Formal Specifi
01f0: 63 61 74 69 6f 6e 3a 20 55 6e 69 76 65 72 73 61  cation: Universa
0200: 6c 20 6d 6f 64 65 7d 0a 5c 6c 61 62 65 6c 7b 73  l mode}.\label{s
0210: 65 63 3a 75 6e 69 76 65 72 73 61 6c 2d 73 70 65  ec:universal-spe
0220: 63 7d 0a 5c 74 6c 61 74 65 78 0a 5c 73 65 74 62  c}.\tlatex.\setb
0230: 6f 6f 6c 65 61 6e 7b 73 68 61 64 69 6e 67 7d 7b  oolean{shading}{
0240: 74 72 75 65 7d 0a 5c 40 78 7b 7d 5c 6d 6f 64 75  true}.\@x{}\modu
0250: 6c 65 4c 65 66 74 44 61 73 68 5c 40 78 78 7b 20  leLeftDash\@xx{
0260: 7b 5c 4d 4f 44 55 4c 45 7d 20 55 6e 69 76 65 72  {\MODULE} Univer
0270: 73 61 6c 7d 5c 6d 6f 64 75 6c 65 52 69 67 68 74  sal}\moduleRight
0280: 44 61 73 68 5c 40 78 78 7b 7d 25 0a 5c 62 65 67  Dash\@xx{}%.\beg
0290: 69 6e 7b 6c 63 6f 6d 7d 7b 30 7d 25 0a 5c 62 65  in{lcom}{0}%.\be
02a0: 67 69 6e 7b 63 70 61 72 7d 7b 30 7d 7b 54 7d 7b  gin{cpar}{0}{T}{
02b0: 46 7d 7b 32 2e 35 7d 7b 30 7d 7b 7d 25 0a 46 6f  F}{2.5}{0}{}%.Fo
02c0: 72 6d 61 6c 20 53 70 65 63 69 66 69 63 61 74 69  rmal Specificati
02d0: 6f 6e 20 69 6e 20 54 4c 41 5c 65 6e 73 75 72 65  on in TLA\ensure
02e0: 6d 61 74 68 7b 5c 2e 7b 5c 6d 62 6f 78 7b 7d 5e  math{\.{\mbox{}^
02f0: 2b 7d 7d 20 6f 66 20 74 68 65 0a 20 49 6e 74 65  +}} of the. Inte
0300: 72 6c 65 64 67 65 72 20 50 72 6f 74 6f 63 6f 6c  rledger Protocol
0310: 20 5c 65 6e 73 75 72 65 6d 61 74 68 7b 55 6e 69   \ensuremath{Uni
0320: 76 65 72 73 61 6c 7d 20 28 5c 65 6e 73 75 72 65  versal} (\ensure
0330: 6d 61 74 68 7b 49 4c 50 7d 2f 5c 65 6e 73 75 72  math{ILP}/\ensur
0340: 65 6d 61 74 68 7b 55 7d 29 0a 5c 65 6e 64 7b 63  emath{U}).\end{c
0350: 70 61 72 7d 25 0a 5c 76 73 68 61 64 65 7b 31 30  par}%.\vshade{10
0360: 2e 30 7d 25 0a 5c 62 65 67 69 6e 7b 63 70 61 72  .0}%.\begin{cpar
0370: 7d 7b 31 7d 7b 46 7d 7b 46 7d 7b 30 7d 7b 30 7d  }{1}{F}{F}{0}{0}
0380: 7b 7d 25 0a 5c 62 65 67 69 6e 7b 6d 69 6e 69 70  {}%.\begin{minip
0390: 61 67 65 7d 5b 74 5d 7b 5c 6c 69 6e 65 77 69 64  age}[t]{\linewid
03a0: 74 68 7d 0a 5c 62 65 67 69 6e 7b 76 65 72 62 61  th}.\begin{verba
03b0: 74 69 6d 7d 0a 20 4d 6f 64 65 6c 65 64 20 61 66  tim}. Modeled af
03c0: 74 65 72 20 74 68 65 20 65 78 63 65 6c 6c 65 6e  ter the excellen
03d0: 74 20 52 61 66 74 20 73 70 65 63 69 66 69 63 61  t Raft specifica
03e0: 74 69 6f 6e 20 62 79 20 44 69 65 67 6f 20 4f 6e  tion by Diego On
03f0: 67 61 72 6f 2e 20 20 20 20 20 20 20 20 20 0a 20  garo.         .
0400: 20 20 41 76 61 69 6c 61 62 6c 65 20 61 74 20 68    Available at h
0410: 74 74 70 73 3a 2f 2f 67 69 74 68 75 62 2e 63 6f  ttps://github.co
0420: 6d 2f 6f 6e 67 61 72 64 69 65 2f 72 61 66 74 2e  m/ongardie/raft.
0430: 74 6c 61 20 20 20 20 20 20 20 20 20 20 20 20 20  tla
0440: 20 20 20 20 20 20 20 20 0a 5c 65 6e 64 7b 76 65          .\end{ve
0450: 72 62 61 74 69 6d 7d 0a 5c 65 6e 64 7b 6d 69 6e  rbatim}.\end{min
0460: 69 70 61 67 65 7d 0a 5c 65 6e 64 7b 63 70 61 72  ipage}.\end{cpar
0470: 7d 25 0a 5c 76 73 68 61 64 65 7b 35 2e 30 7d 25  }%.\vshade{5.0}%
0480: 0a 5c 62 65 67 69 6e 7b 63 70 61 72 7d 7b 30 7d  .\begin{cpar}{0}
0490: 7b 46 7d 7b 46 7d 7b 30 7d 7b 30 7d 7b 7d 25 0a  {F}{F}{0}{0}{}%.
04a0: 5c 62 65 67 69 6e 7b 6d 69 6e 69 70 61 67 65 7d  \begin{minipage}
04b0: 5b 74 5d 7b 5c 6c 69 6e 65 77 69 64 74 68 7d 0a  [t]{\linewidth}.
04c0: 5c 62 65 67 69 6e 7b 76 65 72 62 61 74 69 6d 7d  \begin{verbatim}
04d0: 0a 20 20 20 43 6f 70 79 72 69 67 68 74 20 32 30  .   Copyright 20
04e0: 31 34 20 44 69 65 67 6f 20 4f 6e 67 61 72 6f 2e  14 Diego Ongaro.
04f0: 20 20 20 20 20 20 20 20 20 20 20 20 20 20 20 20
0500: 20 20 20 20 20 20 20 20 20 20 20 20 20 20 20 20
0510: 20 20 20 20 20 20 20 20 20 20 0a 20 20 20 54 68            .   Th
0520: 69 73 20 77 6f 72 6b 20 69 73 20 6c 69 63 65 6e  is work is licen
0530: 73 65 64 20 75 6e 64 65 72 20 74 68 65 20 43 72  sed under the Cr
0540: 65 61 74 69 76 65 20 43 6f 6d 6d 6f 6e 73 20 41  eative Commons A
0550: 74 74 72 69 62 75 74 69 6f 6e 2d 34 2e 30 20 20  ttribution-4.0
0560: 20 20 20 20 0a 20 20 20 49 6e 74 65 72 6e 61 74      .   Internat
0570: 69 6f 6e 61 6c 20 4c 69 63 65 6e 73 65 20 68 74  ional License ht
0580: 74 70 73 3a 2f 2f 63 72 65 61 74 69 76 65 63 6f  tps://creativeco
0590: 6d 6d 6f 6e 73 2e 6f 72 67 2f 6c 69 63 65 6e 73  mmons.org/licens
05a0: 65 73 2f 62 79 2f 34 2e 30 2f 20 20 0a 5c 65 6e  es/by/4.0/  .\en
05b0: 64 7b 76 65 72 62 61 74 69 6d 7d 0a 5c 65 6e 64  d{verbatim}.\end
05c0: 7b 6d 69 6e 69 70 61 67 65 7d 0a 5c 65 6e 64 7b  {minipage}.\end{
05d0: 63 70 61 72 7d 25 0a 5c 65 6e 64 7b 6c 63 6f 6d  cpar}%.\end{lcom
05e0: 7d 25 0a 5c 40 70 76 73 70 61 63 65 7b 38 2e 30  }%.\@pvspace{8.0
05f0: 70 74 7d 25 0a 5c 40 78 7b 20 7b 5c 45 58 54 45  pt}%.\@x{ {\EXTE
0600: 4e 44 53 7d 20 4e 61 74 75 72 61 6c 73 20 2c 5c  NDS} Naturals ,\
0610: 2c 20 53 65 71 75 65 6e 63 65 73 20 2c 5c 2c 20  , Sequences ,\,
0620: 46 69 6e 69 74 65 53 65 74 73 20 2c 5c 2c 20 42  FiniteSets ,\, B
0630: 61 67 73 20 2c 5c 2c 20 54 4c 43 7d 25 0a 5c 40  ags ,\, TLC}%.\@
0640: 70 76 73 70 61 63 65 7b 38 2e 30 70 74 7d 25 0a  pvspace{8.0pt}%.
0650: 5c 40 78 7b 7d 25 0a 5c 40 79 7b 5c 40 73 7b 30  \@x{}%.\@y{\@s{0
0660: 7d 25 0a 20 54 68 65 20 73 65 74 20 6f 66 20 6c  }%. The set of l
0670: 65 64 67 65 72 20 5c 65 6e 73 75 72 65 6d 61 74  edger \ensuremat
0680: 68 7b 49 44 73 0a 7d 7d 25 0a 5c 40 78 78 7b 7d  h{IDs.}}%.\@xx{}
0690: 25 0a 5c 40 78 7b 20 7b 5c 43 4f 4e 53 54 41 4e  %.\@x{ {\CONSTAN
06a0: 54 53 7d 20 4c 65 64 67 65 72 7d 25 0a 5c 40 70  TS} Ledger}%.\@p
06b0: 76 73 70 61 63 65 7b 38 2e 30 70 74 7d 25 0a 5c  vspace{8.0pt}%.\
06c0: 40 78 7b 7d 25 0a 5c 40 79 7b 5c 40 73 7b 30 7d  @x{}%.\@y{\@s{0}
06d0: 25 0a 20 54 68 65 20 73 65 74 20 6f 66 20 70 61  %. The set of pa
06e0: 72 74 69 63 69 70 61 6e 74 20 5c 65 6e 73 75 72  rticipant \ensur
06f0: 65 6d 61 74 68 7b 49 44 73 0a 7d 7d 25 0a 5c 40  emath{IDs.}}%.\@
0700: 78 78 7b 7d 25 0a 5c 40 78 7b 20 7b 5c 43 4f 4e  xx{}%.\@x{ {\CON
0710: 53 54 41 4e 54 53 7d 20 50 61 72 74 69 63 69 70  STANTS} Particip
0720: 61 6e 74 7d 25 0a 5c 40 70 76 73 70 61 63 65 7b  ant}%.\@pvspace{
0730: 38 2e 30 70 74 7d 25 0a 5c 40 78 7b 7d 25 0a 5c  8.0pt}%.\@x{}%.\
0740: 40 79 7b 5c 40 73 7b 30 7d 25 0a 20 53 65 6e 64  @y{\@s{0}%. Send
0750: 65 72 20 73 74 61 74 65 73 0a 7d 25 0a 5c 40 78  er states.}%.\@x
0760: 78 7b 7d 25 0a 5c 40 78 7b 20 7b 5c 43 4f 4e 53  x{}%.\@x{ {\CONS
0770: 54 41 4e 54 53 7d 20 53 5c 5f 52 65 61 64 79 20  TANTS} S\_Ready
0780: 2c 5c 2c 20 53 5c 5f 50 72 6f 70 6f 73 61 6c 57  ,\, S\_ProposalW
0790: 61 69 74 69 6e 67 20 2c 5c 2c 20 53 5c 5f 57 61  aiting ,\, S\_Wa
07a0: 69 74 69 6e 67 20 2c 5c 2c 20 53 5c 5f 44 6f 6e  iting ,\, S\_Don
07b0: 65 7d 25 0a 5c 40 70 76 73 70 61 63 65 7b 38 2e  e}%.\@pvspace{8.
07c0: 30 70 74 7d 25 0a 5c 40 78 7b 7d 25 0a 5c 40 79  0pt}%.\@x{}%.\@y
07d0: 7b 5c 40 73 7b 30 7d 25 0a 20 43 6f 6e 6e 65 63  {\@s{0}%. Connec
07e0: 74 6f 72 20 73 74 61 74 65 73 0a 7d 25 0a 5c 40  tor states.}%.\@
07f0: 78 78 7b 7d 25 0a 5c 40 78 7b 20 7b 5c 43 4f 4e  xx{}%.\@x{ {\CON
0800: 53 54 41 4e 54 53 7d 20 43 5c 5f 52 65 61 64 79  STANTS} C\_Ready
0810: 20 2c 5c 2c 20 43 5c 5f 50 72 6f 70 6f 73 65 64   ,\, C\_Proposed
0820: 7d 25 0a 5c 40 70 76 73 70 61 63 65 7b 38 2e 30  }%.\@pvspace{8.0
0830: 70 74 7d 25 0a 5c 40 78 7b 7d 25 0a 5c 40 79 7b  pt}%.\@x{}%.\@y{
0840: 5c 40 73 7b 30 7d 25 0a 20 4c 65 64 67 65 72 20  \@s{0}%. Ledger
0850: 73 74 61 74 65 73 0a 7d 25 0a 5c 40 78 78 7b 7d  states.}%.\@xx{}
0860: 25 0a 5c 40 78 7b 20 7b 5c 43 4f 4e 53 54 41 4e  %.\@x{ {\CONSTAN
0870: 54 53 7d 20 4c 5c 5f 50 72 6f 70 6f 73 65 64 20  TS} L\_Proposed
0880: 2c 5c 2c 20 4c 5c 5f 50 72 65 70 61 72 65 64 20  ,\, L\_Prepared
0890: 2c 5c 2c 20 4c 5c 5f 45 78 65 63 75 74 65 64 20  ,\, L\_Executed
08a0: 2c 5c 2c 20 4c 5c 5f 41 62 6f 72 74 65 64 7d 25  ,\, L\_Aborted}%
08b0: 0a 5c 40 70 76 73 70 61 63 65 7b 38 2e 30 70 74  .\@pvspace{8.0pt
08c0: 7d 25 0a 5c 40 78 7b 7d 25 0a 5c 40 79 7b 5c 40  }%.\@x{}%.\@y{\@
08d0: 73 7b 30 7d 25 0a 20 4d 65 73 73 61 67 65 20 74  s{0}%. Message t
08e0: 79 70 65 73 0a 7d 25 0a 5c 40 78 78 7b 7d 25 0a  ypes.}%.\@xx{}%.
08f0: 5c 40 78 7b 20 7b 5c 43 4f 4e 53 54 41 4e 54 53  \@x{ {\CONSTANTS
0900: 7d 20 50 72 65 70 61 72 65 52 65 71 75 65 73 74  } PrepareRequest
0910: 20 2c 5c 2c 20 45 78 65 63 75 74 65 52 65 71 75   ,\, ExecuteRequ
0920: 65 73 74 20 2c 5c 2c 20 41 62 6f 72 74 52 65 71  est ,\, AbortReq
0930: 75 65 73 74 20 2c 5c 2c 7d 25 0a 5c 40 78 7b 5c  uest ,\,}%.\@x{\
0940: 40 73 7b 35 34 2e 37 35 7d 20 50 72 65 70 61 72  @s{54.75} Prepar
0950: 65 4e 6f 74 69 66 79 20 2c 5c 2c 20 45 78 65 63  eNotify ,\, Exec
0960: 75 74 65 4e 6f 74 69 66 79 20 2c 5c 2c 20 41 62  uteNotify ,\, Ab
0970: 6f 72 74 4e 6f 74 69 66 79 20 2c 5c 2c 7d 25 0a  ortNotify ,\,}%.
0980: 5c 40 78 7b 5c 40 73 7b 35 34 2e 37 35 7d 20 53  \@x{\@s{54.75} S
0990: 75 62 70 61 79 6d 65 6e 74 50 72 6f 70 6f 73 61  ubpaymentProposa
09a0: 6c 52 65 71 75 65 73 74 20 2c 5c 2c 20 53 75 62  lRequest ,\, Sub
09b0: 70 61 79 6d 65 6e 74 50 72 6f 70 6f 73 61 6c 52  paymentProposalR
09c0: 65 73 70 6f 6e 73 65 7d 25 0a 5c 40 70 76 73 70  esponse}%.\@pvsp
09d0: 61 63 65 7b 38 2e 30 70 74 7d 25 0a 5c 40 78 7b  ace{8.0pt}%.\@x{
09e0: 7d 25 0a 5c 40 79 7b 5c 40 73 7b 30 7d 25 0a 20  }%.\@y{\@s{0}%.
09f0: 52 65 63 65 69 70 74 20 73 69 67 6e 61 74 75 72  Receipt signatur
0a00: 65 0a 7d 25 0a 5c 40 78 78 7b 7d 25 0a 5c 40 78  e.}%.\@xx{}%.\@x
0a10: 7b 20 7b 5c 43 4f 4e 53 54 41 4e 54 53 7d 20 52  { {\CONSTANTS} R
0a20: 5c 5f 52 65 63 65 69 70 74 53 69 67 6e 61 74 75  \_ReceiptSignatu
0a30: 72 65 7d 25 0a 5c 40 70 76 73 70 61 63 65 7b 38  re}%.\@pvspace{8
0a40: 2e 30 70 74 7d 25 0a 5c 40 78 7b 7d 5c 6d 69 64  .0pt}%.\@x{}\mid
0a50: 62 61 72 5c 40 78 78 7b 7d 25 0a 5c 40 78 7b 7d  bar\@xx{}%.\@x{}
0a60: 25 0a 5c 40 79 7b 5c 40 73 7b 30 7d 25 0a 20 47  %.\@y{\@s{0}%. G
0a70: 6c 6f 62 61 6c 20 76 61 72 69 61 62 6c 65 73 0a  lobal variables.
0a80: 7d 25 0a 5c 40 78 78 7b 7d 25 0a 5c 40 70 76 73  }%.\@xx{}%.\@pvs
0a90: 70 61 63 65 7b 38 2e 30 70 74 7d 25 0a 5c 40 78  pace{8.0pt}%.\@x
0aa0: 7b 7d 25 0a 5c 40 79 7b 5c 40 73 7b 30 7d 25 0a  {}%.\@y{\@s{0}%.
0ab0: 20 55 6e 64 65 72 20 73 79 6e 63 68 72 6f 6e 79   Under synchrony
0ac0: 20 77 65 20 61 72 65 20 61 6c 6c 6f 77 65 64 20   we are allowed
0ad0: 74 6f 20 68 61 76 65 20 61 20 67 6c 6f 62 61 6c  to have a global
0ae0: 20 63 6c 6f 63 6b 0a 7d 25 0a 5c 40 78 78 7b 7d   clock.}%.\@xx{}
0af0: 25 0a 5c 40 78 7b 20 7b 5c 56 41 52 49 41 42 4c  %.\@x{ {\VARIABL
0b00: 45 7d 20 63 6c 6f 63 6b 7d 25 0a 5c 40 70 76 73  E} clock}%.\@pvs
0b10: 70 61 63 65 7b 38 2e 30 70 74 7d 25 0a 5c 40 78  pace{8.0pt}%.\@x
0b20: 7b 7d 25 0a 5c 40 79 7b 5c 40 73 7b 30 7d 25 0a  {}%.\@y{\@s{0}%.
0b30: 20 41 20 62 61 67 20 6f 66 20 72 65 63 6f 72 64   A bag of record
0b40: 73 20 72 65 70 72 65 73 65 6e 74 69 6e 67 20 72  s representing r
0b50: 65 71 75 65 73 74 73 20 61 6e 64 20 72 65 73 70  equests and resp
0b60: 6f 6e 73 65 73 20 73 65 6e 74 20 66 72 6f 6d 20  onses sent from
0b70: 6f 6e 65 20 70 72 6f 63 65 73 73 0a 7d 25 0a 5c  one process.}%.\
0b80: 40 78 78 7b 7d 25 0a 5c 40 78 7b 7d 25 0a 5c 40  @xx{}%.\@x{}%.\@
0b90: 79 7b 5c 40 73 7b 30 7d 25 0a 20 74 6f 20 61 6e  y{\@s{0}%. to an
0ba0: 6f 74 68 65 72 0a 7d 25 0a 5c 40 78 78 7b 7d 25  other.}%.\@xx{}%
0bb0: 0a 5c 40 78 7b 20 7b 5c 56 41 52 49 41 42 4c 45  .\@x{ {\VARIABLE
0bc0: 7d 20 6d 65 73 73 61 67 65 73 7d 25 0a 5c 40 70  } messages}%.\@p
0bd0: 76 73 70 61 63 65 7b 38 2e 30 70 74 7d 25 0a 5c  vspace{8.0pt}%.\
0be0: 40 78 7b 7d 5c 6d 69 64 62 61 72 5c 40 78 78 7b  @x{}\midbar\@xx{
0bf0: 7d 25 0a 5c 40 78 7b 7d 25 0a 5c 40 79 7b 5c 40  }%.\@x{}%.\@y{\@
0c00: 73 7b 30 7d 25 0a 20 53 65 6e 64 65 72 20 76 61  s{0}%. Sender va
0c10: 72 69 61 62 6c 65 73 0a 7d 25 0a 5c 40 78 78 7b  riables.}%.\@xx{
0c20: 7d 25 0a 5c 40 70 76 73 70 61 63 65 7b 38 2e 30  }%.\@pvspace{8.0
0c30: 70 74 7d 25 0a 5c 40 78 7b 7d 25 0a 5c 40 79 7b  pt}%.\@x{}%.\@y{
0c40: 5c 40 73 7b 30 7d 25 0a 20 53 74 61 74 65 20 6f  \@s{0}%. State o
0c50: 66 20 74 68 65 20 73 65 6e 64 65 72 20 28 5c 65  f the sender (\e
0c60: 6e 73 75 72 65 6d 61 74 68 7b 53 5c 5f 52 65 61  nsuremath{S\_Rea
0c70: 64 79 7d 2c 20 5c 65 6e 73 75 72 65 6d 61 74 68  dy}, \ensuremath
0c80: 7b 53 5c 5f 57 61 69 74 69 6e 67 7d 2c 0a 20 5c  {S\_Waiting},. \
0c90: 65 6e 73 75 72 65 6d 61 74 68 7b 53 5c 5f 44 6f  ensuremath{S\_Do
0ca0: 6e 65 7d 29 0a 7d 25 0a 5c 40 78 78 7b 7d 25 0a  ne}).}%.\@xx{}%.
0cb0: 5c 40 78 7b 20 7b 5c 56 41 52 49 41 42 4c 45 7d  \@x{ {\VARIABLE}
0cc0: 20 73 65 6e 64 65 72 53 74 61 74 65 7d 25 0a 5c   senderState}%.\
0cd0: 40 70 76 73 70 61 63 65 7b 38 2e 30 70 74 7d 25  @pvspace{8.0pt}%
0ce0: 0a 5c 40 78 7b 7d 25 0a 5c 40 79 7b 5c 40 73 7b  .\@x{}%.\@y{\@s{
0cf0: 30 7d 25 0a 20 57 68 65 74 68 65 72 20 74 68 65  0}%. Whether the
0d00: 20 73 65 6e 64 65 72 20 68 61 73 20 72 65 63 65   sender has rece
0d10: 69 76 65 64 20 61 20 72 65 73 70 6f 6e 73 65 20  ived a response
0d20: 66 72 6f 6d 20 61 20 67 69 76 65 6e 20 63 6f 6e  from a given con
0d30: 6e 65 63 74 6f 72 0a 7d 25 0a 5c 40 78 78 7b 7d  nector.}%.\@xx{}
0d40: 25 0a 5c 40 78 7b 20 7b 5c 56 41 52 49 41 42 4c  %.\@x{ {\VARIABL
0d50: 45 7d 20 73 65 6e 64 65 72 50 72 6f 70 6f 73 61  E} senderProposa
0d60: 6c 52 65 73 70 6f 6e 73 65 73 7d 25 0a 5c 40 70  lResponses}%.\@p
0d70: 76 73 70 61 63 65 7b 38 2e 30 70 74 7d 25 0a 5c  vspace{8.0pt}%.\
0d80: 40 78 7b 7d 25 0a 5c 40 79 7b 5c 40 73 7b 30 7d  @x{}%.\@y{\@s{0}
0d90: 25 0a 20 41 6c 6c 20 73 65 6e 64 65 72 20 76 61  %. All sender va
0da0: 72 69 61 62 6c 65 73 0a 7d 25 0a 5c 40 78 78 7b  riables.}%.\@xx{
0db0: 7d 25 0a 20 5c 40 78 7b 20 73 65 6e 64 65 72 56  }%. \@x{ senderV
0dc0: 61 72 73 20 5c 2e 7b 5c 64 65 66 65 71 7d 20 7b  ars \.{\defeq} {
0dd0: 5c 6c 61 6e 67 6c 65 7d 20 73 65 6e 64 65 72 53  \langle} senderS
0de0: 74 61 74 65 20 2c 5c 2c 20 73 65 6e 64 65 72 50  tate ,\, senderP
0df0: 72 6f 70 6f 73 61 6c 52 65 73 70 6f 6e 73 65 73  roposalResponses
0e00: 0a 20 7b 5c 72 61 6e 67 6c 65 7d 7d 25 0a 5c 40  . {\rangle}}%.\@
0e10: 78 7b 7d 5c 6d 69 64 62 61 72 5c 40 78 78 7b 7d  x{}\midbar\@xx{}
0e20: 25 0a 5c 40 78 7b 7d 25 0a 5c 40 79 7b 5c 40 73  %.\@x{}%.\@y{\@s
0e30: 7b 30 7d 25 0a 20 43 6f 6e 6e 65 63 74 6f 72 20  {0}%. Connector
0e40: 76 61 72 69 61 62 6c 65 73 0a 7d 25 0a 5c 40 78  variables.}%.\@x
0e50: 78 7b 7d 25 0a 5c 40 70 76 73 70 61 63 65 7b 38  x{}%.\@pvspace{8
0e60: 2e 30 70 74 7d 25 0a 5c 40 78 7b 7d 25 0a 5c 40  .0pt}%.\@x{}%.\@
0e70: 79 7b 5c 40 73 7b 30 7d 25 0a 20 53 74 61 74 65  y{\@s{0}%. State
0e80: 20 6f 66 20 74 68 65 20 63 6f 6e 6e 65 63 74 6f   of the connecto
0e90: 72 20 28 5c 65 6e 73 75 72 65 6d 61 74 68 7b 43  r (\ensuremath{C
0ea0: 5c 5f 52 65 61 64 79 7d 2c 20 5c 65 6e 73 75 72  \_Ready}, \ensur
0eb0: 65 6d 61 74 68 7b 43 5c 5f 50 72 6f 70 6f 73 65  emath{C\_Propose
0ec0: 64 7d 29 0a 7d 25 0a 5c 40 78 78 7b 7d 25 0a 5c  d}).}%.\@xx{}%.\
0ed0: 40 78 7b 20 7b 5c 56 41 52 49 41 42 4c 45 7d 20  @x{ {\VARIABLE}
0ee0: 63 6f 6e 6e 65 63 74 6f 72 53 74 61 74 65 7d 25  connectorState}%
0ef0: 0a 5c 40 70 76 73 70 61 63 65 7b 38 2e 30 70 74  .\@pvspace{8.0pt
0f00: 7d 25 0a 5c 40 78 7b 7d 25 0a 5c 40 79 7b 5c 40  }%.\@x{}%.\@y{\@
0f10: 73 7b 30 7d 25 0a 20 41 6c 6c 20 73 65 6e 64 65  s{0}%. All sende
0f20: 72 20 76 61 72 69 61 62 6c 65 73 0a 7d 25 0a 5c  r variables.}%.\
0f30: 40 78 78 7b 7d 25 0a 5c 40 78 7b 20 63 6f 6e 6e  @xx{}%.\@x{ conn
0f40: 65 63 74 6f 72 56 61 72 73 20 5c 2e 7b 5c 64 65  ectorVars \.{\de
0f50: 66 65 71 7d 20 7b 5c 6c 61 6e 67 6c 65 7d 20 63  feq} {\langle} c
0f60: 6f 6e 6e 65 63 74 6f 72 53 74 61 74 65 20 7b 5c  onnectorState {\
0f70: 72 61 6e 67 6c 65 7d 7d 25 0a 5c 40 78 7b 7d 5c  rangle}}%.\@x{}\
0f80: 6d 69 64 62 61 72 5c 40 78 78 7b 7d 25 0a 5c 40  midbar\@xx{}%.\@
0f90: 78 7b 7d 25 0a 5c 40 79 7b 5c 40 73 7b 30 7d 25  x{}%.\@y{\@s{0}%
0fa0: 0a 20 54 68 65 20 66 6f 6c 6c 6f 77 69 6e 67 20  . The following
0fb0: 76 61 72 69 61 62 6c 65 73 20 61 72 65 20 61 6c  variables are al
0fc0: 6c 20 70 65 72 20 6c 65 64 67 65 72 20 28 66 75  l per ledger (fu
0fd0: 6e 63 74 69 6f 6e 73 20 77 69 74 68 20 64 6f 6d  nctions with dom
0fe0: 61 69 6e 0a 20 5c 65 6e 73 75 72 65 6d 61 74 68  ain. \ensuremath
0ff0: 7b 4c 65 64 67 65 72 7d 29 0a 7d 25 0a 5c 40 78  {Ledger}).}%.\@x
1000: 78 7b 7d 25 0a 5c 40 70 76 73 70 61 63 65 7b 38  x{}%.\@pvspace{8
1010: 2e 30 70 74 7d 25 0a 5c 40 78 7b 7d 25 0a 5c 40  .0pt}%.\@x{}%.\@
1020: 79 7b 5c 40 73 7b 30 7d 25 0a 20 54 68 65 20 6c  y{\@s{0}%. The l
1030: 65 64 67 65 72 20 73 74 61 74 65 20 28 5c 65 6e  edger state (\en
1040: 73 75 72 65 6d 61 74 68 7b 4c 5c 5f 50 72 6f 70  suremath{L\_Prop
1050: 6f 73 65 64 7d 2c 20 5c 65 6e 73 75 72 65 6d 61  osed}, \ensurema
1060: 74 68 7b 4c 5c 5f 50 72 65 70 61 72 65 64 7d 2c  th{L\_Prepared},
1070: 0a 20 5c 65 6e 73 75 72 65 6d 61 74 68 7b 4c 5c  . \ensuremath{L\
1080: 5f 45 78 65 63 75 74 65 64 7d 20 6f 72 20 5c 65  _Executed} or \e
1090: 6e 73 75 72 65 6d 61 74 68 7b 4c 5c 5f 41 62 6f  nsuremath{L\_Abo
10a0: 72 74 65 64 7d 29 0a 7d 25 0a 5c 40 78 78 7b 7d  rted}).}%.\@xx{}
10b0: 25 0a 5c 40 78 7b 20 7b 5c 56 41 52 49 41 42 4c  %.\@x{ {\VARIABL
10c0: 45 7d 20 6c 65 64 67 65 72 53 74 61 74 65 7d 25  E} ledgerState}%
10d0: 0a 5c 40 70 76 73 70 61 63 65 7b 38 2e 30 70 74  .\@pvspace{8.0pt
10e0: 7d 25 0a 5c 40 78 7b 7d 25 0a 5c 40 79 7b 5c 40  }%.\@x{}%.\@y{\@
10f0: 73 7b 30 7d 25 0a 20 54 68 65 20 74 69 6d 65 6f  s{0}%. The timeo
1100: 75 74 73 20 66 6f 72 20 65 61 63 68 20 6f 66 20  uts for each of
1110: 74 68 65 20 74 68 65 20 74 72 61 6e 73 66 65 72  the the transfer
1120: 73 0a 7d 25 0a 5c 40 78 78 7b 7d 25 0a 5c 40 78  s.}%.\@xx{}%.\@x
1130: 7b 20 7b 5c 56 41 52 49 41 42 4c 45 7d 20 6c 65  { {\VARIABLE} le
1140: 64 67 65 72 45 78 70 69 72 61 74 69 6f 6e 7d 25  dgerExpiration}%
1150: 0a 5c 40 70 76 73 70 61 63 65 7b 38 2e 30 70 74  .\@pvspace{8.0pt
1160: 7d 25 0a 5c 40 78 7b 7d 25 0a 5c 40 79 7b 5c 40  }%.\@x{}%.\@y{\@
1170: 73 7b 30 7d 25 0a 20 41 6c 6c 20 6c 65 64 67 65  s{0}%. All ledge
1180: 72 20 76 61 72 69 61 62 6c 65 73 0a 7d 25 0a 5c  r variables.}%.\
1190: 40 78 78 7b 7d 25 0a 20 5c 40 78 7b 20 6c 65 64  @xx{}%. \@x{ led
11a0: 67 65 72 56 61 72 73 20 5c 2e 7b 5c 64 65 66 65  gerVars \.{\defe
11b0: 71 7d 20 7b 5c 6c 61 6e 67 6c 65 7d 20 6c 65 64  q} {\langle} led
11c0: 67 65 72 53 74 61 74 65 20 2c 5c 2c 20 6c 65 64  gerState ,\, led
11d0: 67 65 72 45 78 70 69 72 61 74 69 6f 6e 0a 20 7b  gerExpiration. {
11e0: 5c 72 61 6e 67 6c 65 7d 7d 25 0a 5c 40 78 7b 7d  \rangle}}%.\@x{}
11f0: 5c 6d 69 64 62 61 72 5c 40 78 78 7b 7d 25 0a 5c  \midbar\@xx{}%.\
1200: 40 70 76 73 70 61 63 65 7b 38 2e 30 70 74 7d 25  @pvspace{8.0pt}%
1210: 0a 5c 40 78 7b 7d 25 0a 5c 40 79 7b 5c 40 73 7b  .\@x{}%.\@y{\@s{
1220: 30 7d 25 0a 20 41 6c 6c 20 76 61 72 69 61 62 6c  0}%. All variabl
1230: 65 73 3b 20 75 73 65 64 20 66 6f 72 20 73 74 75  es; used for stu
1240: 74 74 65 72 69 6e 67 20 28 61 73 73 65 72 74 69  ttering (asserti
1250: 6e 67 20 73 74 61 74 65 20 68 61 73 6e 5c 6d 62  ng state hasn\mb
1260: 6f 78 7b 27 7d 74 20 63 68 61 6e 67 65 64 29 0a  ox{'}t changed).
1270: 7d 25 0a 5c 40 78 78 7b 7d 25 0a 20 5c 40 78 7b  }%.\@xx{}%. \@x{
1280: 20 76 61 72 73 20 5c 2e 7b 5c 64 65 66 65 71 7d   vars \.{\defeq}
1290: 20 7b 5c 6c 61 6e 67 6c 65 7d 20 63 6c 6f 63 6b   {\langle} clock
12a0: 20 2c 5c 2c 20 6d 65 73 73 61 67 65 73 20 2c 5c   ,\, messages ,\
12b0: 2c 20 73 65 6e 64 65 72 56 61 72 73 20 2c 5c 2c  , senderVars ,\,
12c0: 0a 20 63 6f 6e 6e 65 63 74 6f 72 56 61 72 73 20  . connectorVars
12d0: 2c 5c 2c 20 6c 65 64 67 65 72 56 61 72 73 20 7b  ,\, ledgerVars {
12e0: 5c 72 61 6e 67 6c 65 7d 7d 25 0a 5c 40 70 76 73  \rangle}}%.\@pvs
12f0: 70 61 63 65 7b 38 2e 30 70 74 7d 25 0a 5c 40 78  pace{8.0pt}%.\@x
1300: 7b 7d 5c 6d 69 64 62 61 72 5c 40 78 78 7b 7d 25  {}\midbar\@xx{}%
1310: 0a 5c 40 78 7b 7d 25 0a 5c 40 79 7b 5c 40 73 7b  .\@x{}%.\@y{\@s{
1320: 30 7d 25 0a 20 48 65 6c 70 65 72 73 0a 7d 25 0a  0}%. Helpers.}%.
1330: 5c 40 78 78 7b 7d 25 0a 5c 40 70 76 73 70 61 63  \@xx{}%.\@pvspac
1340: 65 7b 38 2e 30 70 74 7d 25 0a 5c 40 78 7b 7d 25  e{8.0pt}%.\@x{}%
1350: 0a 5c 40 79 7b 5c 40 73 7b 30 7d 25 0a 20 41 64  .\@y{\@s{0}%. Ad
1360: 64 20 61 20 73 65 74 20 6f 66 20 6e 65 77 20 6d  d a set of new m
1370: 65 73 73 61 67 65 73 20 69 6e 20 74 72 61 6e 73  essages in trans
1380: 69 74 0a 7d 25 0a 5c 40 78 78 7b 7d 25 0a 20 5c  it.}%.\@xx{}%. \
1390: 40 78 7b 20 42 72 6f 61 64 63 61 73 74 20 28 20  @x{ Broadcast (
13a0: 6d 20 29 20 5c 2e 7b 5c 64 65 66 65 71 7d 20 6d  m ) \.{\defeq} m
13b0: 65 73 73 61 67 65 73 20 5c 2e 7b 27 7d 20 5c 2e  essages \.{'} \.
13c0: 7b 3d 7d 20 6d 65 73 73 61 67 65 73 20 5c 2e 7b  {=} messages \.{
13d0: 5c 6f 70 6c 75 73 7d 0a 20 53 65 74 54 6f 42 61  \oplus}. SetToBa
13e0: 67 20 28 20 6d 20 29 7d 25 0a 5c 40 70 76 73 70  g ( m )}%.\@pvsp
13f0: 61 63 65 7b 38 2e 30 70 74 7d 25 0a 5c 40 78 7b  ace{8.0pt}%.\@x{
1400: 7d 25 0a 5c 40 79 7b 5c 40 73 7b 30 7d 25 0a 20  }%.\@y{\@s{0}%.
1410: 41 64 64 20 61 20 6d 65 73 73 61 67 65 20 74 6f  Add a message to
1420: 20 74 68 65 20 62 61 67 20 6f 66 20 6d 65 73 73   the bag of mess
1430: 61 67 65 73 0a 7d 25 0a 5c 40 78 78 7b 7d 25 0a  ages.}%.\@xx{}%.
1440: 5c 40 78 7b 20 53 65 6e 64 20 28 20 6d 20 29 20  \@x{ Send ( m )
1450: 5c 2e 7b 5c 64 65 66 65 71 7d 20 42 72 6f 61 64  \.{\defeq} Broad
1460: 63 61 73 74 20 28 20 5c 7b 20 6d 20 5c 7d 20 29  cast ( \{ m \} )
1470: 7d 25 0a 5c 40 70 76 73 70 61 63 65 7b 38 2e 30  }%.\@pvspace{8.0
1480: 70 74 7d 25 0a 5c 40 78 7b 7d 25 0a 5c 40 79 7b  pt}%.\@x{}%.\@y{
1490: 5c 40 73 7b 30 7d 25 0a 20 52 65 6d 6f 76 65 20  \@s{0}%. Remove
14a0: 61 20 6d 65 73 73 61 67 65 20 66 72 6f 6d 20 74  a message from t
14b0: 68 65 20 62 61 67 20 6f 66 20 6d 65 73 73 61 67  he bag of messag
14c0: 65 73 2e 20 55 73 65 64 20 77 68 65 6e 20 61 20  es. Used when a
14d0: 70 72 6f 63 65 73 73 20 69 73 20 64 6f 6e 65 0a  process is done.
14e0: 7d 25 0a 5c 40 78 78 7b 7d 25 0a 5c 40 78 7b 7d  }%.\@xx{}%.\@x{}
14f0: 25 0a 5c 40 79 7b 5c 40 73 7b 30 7d 25 0a 20 70  %.\@y{\@s{0}%. p
1500: 72 6f 63 65 73 73 69 6e 67 20 61 20 6d 65 73 73  rocessing a mess
1510: 61 67 65 2e 0a 7d 25 0a 5c 40 78 78 7b 7d 25 0a  age..}%.\@xx{}%.
1520: 20 5c 40 78 7b 20 44 69 73 63 61 72 64 20 28 20   \@x{ Discard (
1530: 6d 20 29 20 5c 2e 7b 5c 64 65 66 65 71 7d 20 6d  m ) \.{\defeq} m
1540: 65 73 73 61 67 65 73 20 5c 2e 7b 27 7d 20 5c 2e  essages \.{'} \.
1550: 7b 3d 7d 20 6d 65 73 73 61 67 65 73 20 5c 2e 7b  {=} messages \.{
1560: 5c 6f 6d 69 6e 75 73 7d 0a 20 53 65 74 54 6f 42  \ominus}. SetToB
1570: 61 67 20 28 20 5c 7b 20 6d 20 5c 7d 20 29 7d 25  ag ( \{ m \} )}%
1580: 0a 5c 40 70 76 73 70 61 63 65 7b 38 2e 30 70 74  .\@pvspace{8.0pt
1590: 7d 25 0a 5c 40 78 7b 7d 25 0a 5c 40 79 7b 5c 40  }%.\@x{}%.\@y{\@
15a0: 73 7b 30 7d 25 0a 20 52 65 73 70 6f 6e 64 20 74  s{0}%. Respond t
15b0: 6f 20 61 20 6d 65 73 73 61 67 65 20 62 79 20 73  o a message by s
15c0: 65 6e 64 69 6e 67 20 6d 75 6c 74 69 70 6c 65 20  ending multiple
15d0: 6d 65 73 73 61 67 65 73 0a 7d 25 0a 5c 40 78 78  messages.}%.\@xx
15e0: 7b 7d 25 0a 5c 40 78 7b 20 52 65 70 6c 79 42 72  {}%.\@x{ ReplyBr
15f0: 6f 61 64 63 61 73 74 20 28 20 72 65 73 70 6f 6e  oadcast ( respon
1600: 73 65 73 20 2c 5c 2c 20 72 65 71 75 65 73 74 20  ses ,\, request
1610: 29 20 5c 2e 7b 5c 64 65 66 65 71 7d 7d 25 0a 20  ) \.{\defeq}}%.
1620: 5c 40 78 7b 5c 40 73 7b 31 36 2e 34 7d 20 6d 65  \@x{\@s{16.4} me
1630: 73 73 61 67 65 73 20 5c 2e 7b 27 7d 20 5c 2e 7b  ssages \.{'} \.{
1640: 3d 7d 20 6d 65 73 73 61 67 65 73 20 5c 2e 7b 5c  =} messages \.{\
1650: 6f 6d 69 6e 75 73 7d 20 53 65 74 54 6f 42 61 67  ominus} SetToBag
1660: 20 28 20 5c 7b 20 72 65 71 75 65 73 74 0a 20 5c   ( \{ request. \
1670: 7d 20 29 20 5c 2e 7b 5c 6f 70 6c 75 73 7d 20 53  } ) \.{\oplus} S
1680: 65 74 54 6f 42 61 67 20 28 20 72 65 73 70 6f 6e  etToBag ( respon
1690: 73 65 73 20 29 7d 25 0a 5c 40 70 76 73 70 61 63  ses )}%.\@pvspac
16a0: 65 7b 38 2e 30 70 74 7d 25 0a 5c 40 78 7b 7d 25  e{8.0pt}%.\@x{}%
16b0: 0a 5c 40 79 7b 5c 40 73 7b 30 7d 25 0a 20 43 6f  .\@y{\@s{0}%. Co
16c0: 6d 62 69 6e 61 74 69 6f 6e 20 6f 66 20 5c 65 6e  mbination of \en
16d0: 73 75 72 65 6d 61 74 68 7b 53 65 6e 64 7d 20 61  suremath{Send} a
16e0: 6e 64 20 5c 65 6e 73 75 72 65 6d 61 74 68 7b 44  nd \ensuremath{D
16f0: 69 73 63 61 72 64 0a 7d 7d 25 0a 5c 40 78 78 7b  iscard.}}%.\@xx{
1700: 7d 25 0a 5c 40 78 7b 20 52 65 70 6c 79 20 28 20  }%.\@x{ Reply (
1710: 72 65 73 70 6f 6e 73 65 20 2c 5c 2c 20 72 65 71  response ,\, req
1720: 75 65 73 74 20 29 20 5c 2e 7b 5c 64 65 66 65 71  uest ) \.{\defeq
1730: 7d 7d 25 0a 5c 40 78 7b 5c 40 73 7b 31 36 2e 34  }}%.\@x{\@s{16.4
1740: 7d 20 52 65 70 6c 79 42 72 6f 61 64 63 61 73 74  } ReplyBroadcast
1750: 20 28 20 5c 7b 20 72 65 73 70 6f 6e 73 65 20 5c   ( \{ response \
1760: 7d 20 2c 5c 2c 20 72 65 71 75 65 73 74 20 29 7d  } ,\, request )}
1770: 25 0a 5c 40 70 76 73 70 61 63 65 7b 31 36 2e 30  %.\@pvspace{16.0
1780: 70 74 7d 25 0a 5c 40 78 7b 7d 25 0a 5c 40 79 7b  pt}%.\@x{}%.\@y{
1790: 5c 40 73 7b 30 7d 25 0a 20 52 65 74 75 72 6e 20  \@s{0}%. Return
17a0: 74 68 65 20 6d 69 6e 69 6d 75 6d 20 76 61 6c 75  the minimum valu
17b0: 65 20 66 72 6f 6d 20 61 20 73 65 74 2c 20 6f 72  e from a set, or
17c0: 20 75 6e 64 65 66 69 6e 65 64 20 69 66 20 74 68   undefined if th
17d0: 65 20 73 65 74 20 69 73 20 65 6d 70 74 79 2e 0a  e set is empty..
17e0: 7d 25 0a 5c 40 78 78 7b 7d 25 0a 20 5c 40 78 7b  }%.\@xx{}%. \@x{
17f0: 20 4d 69 6e 20 28 20 73 20 29 20 5c 2e 7b 5c 64   Min ( s ) \.{\d
1800: 65 66 65 71 7d 20 7b 5c 43 48 4f 4f 53 45 7d 20  efeq} {\CHOOSE}
1810: 78 20 5c 2e 7b 5c 69 6e 7d 20 73 20 5c 2e 7b 3a  x \.{\in} s \.{:
1820: 7d 20 5c 41 5c 2c 20 79 20 5c 2e 7b 5c 69 6e 7d  } \A\, y \.{\in}
1830: 20 73 20 5c 2e 7b 3a 7d 0a 20 78 20 5c 2e 7b 5c   s \.{:}. x \.{\
1840: 6c 65 71 7d 20 79 7d 25 0a 5c 40 78 7b 7d 25 0a  leq} y}%.\@x{}%.
1850: 5c 40 79 7b 5c 40 73 7b 30 7d 25 0a 20 52 65 74  \@y{\@s{0}%. Ret
1860: 75 72 6e 20 74 68 65 20 6d 61 78 69 6d 75 6d 20  urn the maximum
1870: 76 61 6c 75 65 20 66 72 6f 6d 20 61 20 73 65 74  value from a set
1880: 2c 20 6f 72 20 75 6e 64 65 66 69 6e 65 64 20 69  , or undefined i
1890: 66 20 74 68 65 20 73 65 74 20 69 73 20 65 6d 70  f the set is emp
18a0: 74 79 2e 0a 7d 25 0a 5c 40 78 78 7b 7d 25 0a 20  ty..}%.\@xx{}%.
18b0: 5c 40 78 7b 20 4d 61 78 20 28 20 73 20 29 20 5c  \@x{ Max ( s ) \
18c0: 2e 7b 5c 64 65 66 65 71 7d 20 7b 5c 43 48 4f 4f  .{\defeq} {\CHOO
18d0: 53 45 7d 20 78 20 5c 2e 7b 5c 69 6e 7d 20 73 20  SE} x \.{\in} s
18e0: 5c 2e 7b 3a 7d 20 5c 41 5c 2c 20 79 20 5c 2e 7b  \.{:} \A\, y \.{
18f0: 5c 69 6e 7d 20 73 20 5c 2e 7b 3a 7d 0a 20 78 20  \in} s \.{:}. x
1900: 5c 2e 7b 5c 67 65 71 7d 20 79 7d 25 0a 5c 40 70  \.{\geq} y}%.\@p
1910: 76 73 70 61 63 65 7b 38 2e 30 70 74 7d 25 0a 5c  vspace{8.0pt}%.\
1920: 40 78 7b 7d 25 0a 5c 40 79 7b 5c 40 73 7b 30 7d  @x{}%.\@y{\@s{0}
1930: 25 0a 20 49 73 20 61 20 66 69 6e 61 6c 20 6c 65  %. Is a final le
1940: 64 67 65 72 20 73 74 61 74 65 0a 7d 25 0a 5c 40  dger state.}%.\@
1950: 78 78 7b 7d 25 0a 20 5c 40 78 7b 20 49 73 46 69  xx{}%. \@x{ IsFi
1960: 6e 61 6c 4c 65 64 67 65 72 53 74 61 74 65 20 28  nalLedgerState (
1970: 20 69 20 29 20 5c 2e 7b 5c 64 65 66 65 71 7d 20   i ) \.{\defeq}
1980: 69 20 5c 2e 7b 5c 69 6e 7d 20 5c 7b 20 4c 5c 5f  i \.{\in} \{ L\_
1990: 45 78 65 63 75 74 65 64 20 2c 5c 2c 0a 20 4c 5c  Executed ,\,. L\
19a0: 5f 41 62 6f 72 74 65 64 20 5c 7d 7d 25 0a 5c 40  _Aborted \}}%.\@
19b0: 70 76 73 70 61 63 65 7b 38 2e 30 70 74 7d 25 0a  pvspace{8.0pt}%.
19c0: 5c 40 78 7b 7d 25 0a 5c 40 79 7b 5c 40 73 7b 30  \@x{}%.\@y{\@s{0
19d0: 7d 25 0a 20 53 65 6e 64 65 72 0a 7d 25 0a 5c 40  }%. Sender.}%.\@
19e0: 78 78 7b 7d 25 0a 5c 40 78 7b 20 53 65 6e 64 65  xx{}%.\@x{ Sende
19f0: 72 20 5c 2e 7b 5c 64 65 66 65 71 7d 20 4d 69 6e  r \.{\defeq} Min
1a00: 20 28 20 50 61 72 74 69 63 69 70 61 6e 74 20 29   ( Participant )
1a10: 7d 25 0a 5c 40 70 76 73 70 61 63 65 7b 38 2e 30  }%.\@pvspace{8.0
1a20: 70 74 7d 25 0a 5c 40 78 7b 7d 25 0a 5c 40 79 7b  pt}%.\@x{}%.\@y{
1a30: 5c 40 73 7b 30 7d 25 0a 20 52 65 63 69 70 69 65  \@s{0}%. Recipie
1a40: 6e 74 0a 7d 25 0a 5c 40 78 78 7b 7d 25 0a 5c 40  nt.}%.\@xx{}%.\@
1a50: 78 7b 20 52 65 63 69 70 69 65 6e 74 20 5c 2e 7b  x{ Recipient \.{
1a60: 5c 64 65 66 65 71 7d 20 4d 61 78 20 28 20 50 61  \defeq} Max ( Pa
1a70: 72 74 69 63 69 70 61 6e 74 20 29 7d 25 0a 5c 40  rticipant )}%.\@
1a80: 70 76 73 70 61 63 65 7b 38 2e 30 70 74 7d 25 0a  pvspace{8.0pt}%.
1a90: 5c 40 78 7b 7d 25 0a 5c 40 79 7b 5c 40 73 7b 30  \@x{}%.\@y{\@s{0
1aa0: 7d 25 0a 20 53 65 74 20 6f 66 20 63 6f 6e 6e 65  }%. Set of conne
1ab0: 63 74 6f 72 73 0a 7d 25 0a 5c 40 78 78 7b 7d 25  ctors.}%.\@xx{}%
1ac0: 0a 20 5c 40 78 7b 20 43 6f 6e 6e 65 63 74 6f 72  . \@x{ Connector
1ad0: 20 5c 2e 7b 5c 64 65 66 65 71 7d 20 50 61 72 74   \.{\defeq} Part
1ae0: 69 63 69 70 61 6e 74 20 5c 2e 7b 5c 2c 5c 62 61  icipant \.{\,\ba
1af0: 63 6b 73 6c 61 73 68 5c 2c 7d 20 5c 7b 20 53 65  ckslash\,} \{ Se
1b00: 6e 64 65 72 20 2c 5c 2c 0a 20 52 65 63 69 70 69  nder ,\,. Recipi
1b10: 65 6e 74 20 5c 7d 7d 25 0a 5c 40 70 76 73 70 61  ent \}}%.\@pvspa
1b20: 63 65 7b 38 2e 30 70 74 7d 25 0a 5c 40 78 7b 7d  ce{8.0pt}%.\@x{}
1b30: 25 0a 5c 40 79 7b 5c 40 73 7b 30 7d 25 0a 20 54  %.\@y{\@s{0}%. T
1b40: 68 65 20 63 6c 6f 63 6b 20 76 61 6c 75 65 20 77  he clock value w
1b50: 65 20 65 78 70 65 63 74 20 74 6f 20 62 65 20 61  e expect to be a
1b60: 74 20 61 66 74 65 72 20 74 68 65 20 70 72 6f 70  t after the prop
1b70: 6f 73 61 6c 20 70 68 61 73 65 0a 7d 25 0a 5c 40  osal phase.}%.\@
1b80: 78 78 7b 7d 25 0a 5c 40 78 7b 20 43 6c 6f 63 6b  xx{}%.\@x{ Clock
1b90: 41 66 74 65 72 50 72 6f 70 6f 73 61 6c 20 5c 2e  AfterProposal \.
1ba0: 7b 5c 64 65 66 65 71 7d 20 32 20 5c 2e 7b 2a 7d  {\defeq} 2 \.{*}
1bb0: 20 43 61 72 64 69 6e 61 6c 69 74 79 20 28 20 43   Cardinality ( C
1bc0: 6f 6e 6e 65 63 74 6f 72 20 29 20 5c 2e 7b 2b 7d  onnector ) \.{+}
1bd0: 20 32 7d 25 0a 5c 40 70 76 73 70 61 63 65 7b 38   2}%.\@pvspace{8
1be0: 2e 30 70 74 7d 25 0a 5c 40 78 7b 7d 25 0a 5c 40  .0pt}%.\@x{}%.\@
1bf0: 79 7b 5c 40 73 7b 30 7d 25 0a 20 54 68 65 20 63  y{\@s{0}%. The c
1c00: 6c 6f 63 6b 20 76 61 6c 75 65 20 77 65 20 65 78  lock value we ex
1c10: 70 65 63 74 20 61 66 74 65 72 20 74 68 65 20 70  pect after the p
1c20: 72 65 70 61 72 61 74 69 6f 6e 20 70 68 61 73 65  reparation phase
1c30: 0a 7d 25 0a 5c 40 78 78 7b 7d 25 0a 20 5c 40 78  .}%.\@xx{}%. \@x
1c40: 7b 20 43 6c 6f 63 6b 41 66 74 65 72 50 72 65 70  { ClockAfterPrep
1c50: 61 72 65 20 5c 2e 7b 5c 64 65 66 65 71 7d 20 43  are \.{\defeq} C
1c60: 6c 6f 63 6b 41 66 74 65 72 50 72 6f 70 6f 73 61  lockAfterProposa
1c70: 6c 20 5c 2e 7b 2b 7d 20 32 20 5c 2e 7b 2a 7d 0a  l \.{+} 2 \.{*}.
1c80: 20 43 61 72 64 69 6e 61 6c 69 74 79 20 28 20 4c   Cardinality ( L
1c90: 65 64 67 65 72 20 29 20 5c 2e 7b 2b 7d 20 31 7d  edger ) \.{+} 1}
1ca0: 25 0a 5c 40 70 76 73 70 61 63 65 7b 38 2e 30 70  %.\@pvspace{8.0p
1cb0: 74 7d 25 0a 5c 40 78 7b 7d 25 0a 5c 40 79 7b 5c  t}%.\@x{}%.\@y{\
1cc0: 40 73 7b 30 7d 25 0a 20 54 68 65 20 63 6c 6f 63  @s{0}%. The cloc
1cd0: 6b 20 76 61 6c 75 65 20 77 65 20 65 78 70 65 63  k value we expec
1ce0: 74 20 74 6f 20 62 65 20 61 74 20 61 66 74 65 72  t to be at after
1cf0: 20 74 68 65 20 65 78 65 63 75 74 69 6f 6e 20 70   the execution p
1d00: 68 61 73 65 0a 7d 25 0a 5c 40 78 78 7b 7d 25 0a  hase.}%.\@xx{}%.
1d10: 20 5c 40 78 7b 20 43 6c 6f 63 6b 41 66 74 65 72   \@x{ ClockAfter
1d20: 45 78 65 63 75 74 69 6f 6e 20 5c 2e 7b 5c 64 65  Execution \.{\de
1d30: 66 65 71 7d 20 43 6c 6f 63 6b 41 66 74 65 72 50  feq} ClockAfterP
1d40: 72 65 70 61 72 65 20 5c 2e 7b 2b 7d 20 32 20 5c  repare \.{+} 2 \
1d50: 2e 7b 2a 7d 0a 20 43 61 72 64 69 6e 61 6c 69 74  .{*}. Cardinalit
1d60: 79 20 28 20 4c 65 64 67 65 72 20 29 20 5c 2e 7b  y ( Ledger ) \.{
1d70: 2b 7d 20 31 7d 25 0a 5c 40 78 7b 7d 5c 6d 69 64  +} 1}%.\@x{}\mid
1d80: 62 61 72 5c 40 78 78 7b 7d 25 0a 5c 40 78 7b 7d  bar\@xx{}%.\@x{}
1d90: 25 0a 5c 40 79 7b 5c 40 73 7b 30 7d 25 0a 20 44  %.\@y{\@s{0}%. D
1da0: 65 66 69 6e 65 20 74 79 70 65 20 73 70 65 63 69  efine type speci
1db0: 66 69 63 61 74 69 6f 6e 20 66 6f 72 20 61 6c 6c  fication for all
1dc0: 20 76 61 72 69 61 62 6c 65 73 0a 7d 25 0a 5c 40   variables.}%.\@
1dd0: 78 78 7b 7d 25 0a 5c 40 70 76 73 70 61 63 65 7b  xx{}%.\@pvspace{
1de0: 38 2e 30 70 74 7d 25 0a 5c 40 78 7b 20 54 79 70  8.0pt}%.\@x{ Typ
1df0: 65 4f 4b 20 5c 2e 7b 5c 64 65 66 65 71 7d 20 5c  eOK \.{\defeq} \
1e00: 2e 7b 5c 6c 61 6e 64 7d 20 63 6c 6f 63 6b 20 5c  .{\land} clock \
1e10: 2e 7b 5c 69 6e 7d 20 4e 61 74 7d 25 0a 5c 40 78  .{\in} Nat}%.\@x
1e20: 7b 5c 40 73 7b 35 36 2e 31 34 7d 20 5c 2e 7b 5c  {\@s{56.14} \.{\
1e30: 6c 61 6e 64 7d 20 49 73 41 42 61 67 20 28 20 6d  land} IsABag ( m
1e40: 65 73 73 61 67 65 73 20 29 7d 25 0a 20 5c 40 78  essages )}%. \@x
1e50: 7b 5c 40 73 7b 35 36 2e 31 34 7d 20 5c 2e 7b 5c  {\@s{56.14} \.{\
1e60: 6c 61 6e 64 7d 20 73 65 6e 64 65 72 53 74 61 74  land} senderStat
1e70: 65 20 5c 2e 7b 5c 69 6e 7d 20 5c 7b 20 53 5c 5f  e \.{\in} \{ S\_
1e80: 52 65 61 64 79 20 2c 5c 2c 0a 20 53 5c 5f 50 72  Ready ,\,. S\_Pr
1e90: 6f 70 6f 73 61 6c 57 61 69 74 69 6e 67 20 2c 5c  oposalWaiting ,\
1ea0: 2c 20 53 5c 5f 57 61 69 74 69 6e 67 20 2c 5c 2c  , S\_Waiting ,\,
1eb0: 20 53 5c 5f 44 6f 6e 65 20 5c 7d 7d 25 0a 20 5c   S\_Done \}}%. \
1ec0: 40 78 7b 5c 40 73 7b 35 36 2e 31 34 7d 20 5c 2e  @x{\@s{56.14} \.
1ed0: 7b 5c 6c 61 6e 64 7d 20 73 65 6e 64 65 72 50 72  {\land} senderPr
1ee0: 6f 70 6f 73 61 6c 52 65 73 70 6f 6e 73 65 73 20  oposalResponses
1ef0: 5c 2e 7b 5c 69 6e 7d 20 5b 20 43 6f 6e 6e 65 63  \.{\in} [ Connec
1f00: 74 6f 72 0a 20 5c 2e 7b 5c 72 69 67 68 74 61 72  tor. \.{\rightar
1f10: 72 6f 77 7d 20 7b 5c 42 4f 4f 4c 45 41 4e 7d 20  row} {\BOOLEAN}
1f20: 5d 7d 25 0a 20 5c 40 78 7b 5c 40 73 7b 35 36 2e  ]}%. \@x{\@s{56.
1f30: 31 34 7d 20 5c 2e 7b 5c 6c 61 6e 64 7d 20 63 6f  14} \.{\land} co
1f40: 6e 6e 65 63 74 6f 72 53 74 61 74 65 20 5c 2e 7b  nnectorState \.{
1f50: 5c 69 6e 7d 20 5b 20 43 6f 6e 6e 65 63 74 6f 72  \in} [ Connector
1f60: 20 5c 2e 7b 5c 72 69 67 68 74 61 72 72 6f 77 7d   \.{\rightarrow}
1f70: 0a 20 5c 7b 20 43 5c 5f 52 65 61 64 79 20 2c 5c  . \{ C\_Ready ,\
1f80: 2c 20 43 5c 5f 50 72 6f 70 6f 73 65 64 20 5c 7d  , C\_Proposed \}
1f90: 20 5d 7d 25 0a 20 5c 40 78 7b 5c 40 73 7b 35 36   ]}%. \@x{\@s{56
1fa0: 2e 31 34 7d 20 5c 2e 7b 5c 6c 61 6e 64 7d 20 6c  .14} \.{\land} l
1fb0: 65 64 67 65 72 53 74 61 74 65 20 5c 2e 7b 5c 69  edgerState \.{\i
1fc0: 6e 7d 20 5b 20 4c 65 64 67 65 72 20 5c 2e 7b 5c  n} [ Ledger \.{\
1fd0: 72 69 67 68 74 61 72 72 6f 77 7d 20 5c 7b 0a 20  rightarrow} \{.
1fe0: 4c 5c 5f 50 72 6f 70 6f 73 65 64 20 2c 5c 2c 20  L\_Proposed ,\,
1ff0: 4c 5c 5f 50 72 65 70 61 72 65 64 20 2c 5c 2c 20  L\_Prepared ,\,
2000: 4c 5c 5f 45 78 65 63 75 74 65 64 20 2c 5c 2c 20  L\_Executed ,\,
2010: 4c 5c 5f 41 62 6f 72 74 65 64 20 5c 7d 20 5d 7d  L\_Aborted \} ]}
2020: 25 0a 20 5c 40 78 7b 5c 40 73 7b 35 36 2e 31 34  %. \@x{\@s{56.14
2030: 7d 20 5c 2e 7b 5c 6c 61 6e 64 7d 20 6c 65 64 67  } \.{\land} ledg
2040: 65 72 45 78 70 69 72 61 74 69 6f 6e 20 5c 2e 7b  erExpiration \.{
2050: 5c 69 6e 7d 20 5b 20 4c 65 64 67 65 72 20 5c 2e  \in} [ Ledger \.
2060: 7b 5c 72 69 67 68 74 61 72 72 6f 77 7d 0a 20 4e  {\rightarrow}. N
2070: 61 74 20 5d 7d 25 0a 5c 40 70 76 73 70 61 63 65  at ]}%.\@pvspace
2080: 7b 38 2e 30 70 74 7d 25 0a 5c 40 78 7b 20 43 6f  {8.0pt}%.\@x{ Co
2090: 6e 73 69 73 74 65 6e 63 79 20 5c 2e 7b 5c 64 65  nsistency \.{\de
20a0: 66 65 71 7d 7d 25 0a 20 5c 40 78 7b 5c 40 73 7b  feq}}%. \@x{\@s{
20b0: 31 36 2e 34 7d 20 5c 41 5c 2c 20 6c 31 20 2c 5c  16.4} \A\, l1 ,\
20c0: 2c 20 6c 32 20 5c 2e 7b 5c 69 6e 7d 20 4c 65 64  , l2 \.{\in} Led
20d0: 67 65 72 20 5c 2e 7b 3a 7d 20 7b 5c 6c 6e 6f 74  ger \.{:} {\lnot
20e0: 7d 20 5c 2e 7b 5c 6c 61 6e 64 7d 0a 20 6c 65 64  } \.{\land}. led
20f0: 67 65 72 53 74 61 74 65 20 5b 20 6c 31 20 5d 20  gerState [ l1 ]
2100: 5c 2e 7b 3d 7d 20 4c 5c 5f 41 62 6f 72 74 65 64  \.{=} L\_Aborted
2110: 7d 25 0a 5c 40 78 7b 5c 40 73 7b 31 30 34 2e 36  }%.\@x{\@s{104.6
2120: 39 7d 20 5c 2e 7b 5c 6c 61 6e 64 7d 20 6c 65 64  9} \.{\land} led
2130: 67 65 72 53 74 61 74 65 20 5b 20 6c 32 20 5d 20  gerState [ l2 ]
2140: 5c 2e 7b 3d 7d 20 4c 5c 5f 45 78 65 63 75 74 65  \.{=} L\_Execute
2150: 64 7d 25 0a 5c 40 70 76 73 70 61 63 65 7b 38 2e  d}%.\@pvspace{8.
2160: 30 70 74 7d 25 0a 5c 40 78 7b 20 49 6e 76 20 5c  0pt}%.\@x{ Inv \
2170: 2e 7b 5c 64 65 66 65 71 7d 20 5c 2e 7b 5c 6c 61  .{\defeq} \.{\la
2180: 6e 64 7d 20 54 79 70 65 4f 4b 7d 25 0a 5c 40 78  nd} TypeOK}%.\@x
2190: 7b 5c 40 73 7b 33 34 2e 30 34 7d 20 5c 2e 7b 5c  {\@s{34.04} \.{\
21a0: 6c 61 6e 64 7d 20 43 6f 6e 73 69 73 74 65 6e 63  land} Consistenc
21b0: 79 7d 25 0a 5c 40 70 76 73 70 61 63 65 7b 38 2e  y}%.\@pvspace{8.
21c0: 30 70 74 7d 25 0a 5c 40 78 7b 7d 5c 6d 69 64 62  0pt}%.\@x{}\midb
21d0: 61 72 5c 40 78 78 7b 7d 25 0a 5c 40 78 7b 7d 25  ar\@xx{}%.\@x{}%
21e0: 0a 5c 40 79 7b 5c 40 73 7b 30 7d 25 0a 20 44 65  .\@y{\@s{0}%. De
21f0: 66 69 6e 65 20 69 6e 69 74 69 61 6c 20 76 61 6c  fine initial val
2200: 75 65 73 20 66 6f 72 20 61 6c 6c 20 76 61 72 69  ues for all vari
2210: 61 62 6c 65 73 0a 7d 25 0a 5c 40 78 78 7b 7d 25  ables.}%.\@xx{}%
2220: 0a 5c 40 70 76 73 70 61 63 65 7b 38 2e 30 70 74  .\@pvspace{8.0pt
2230: 7d 25 0a 5c 40 78 7b 20 49 6e 69 74 53 65 6e 64  }%.\@x{ InitSend
2240: 65 72 56 61 72 73 20 5c 2e 7b 5c 64 65 66 65 71  erVars \.{\defeq
2250: 7d 20 5c 2e 7b 5c 6c 61 6e 64 7d 20 73 65 6e 64  } \.{\land} send
2260: 65 72 53 74 61 74 65 20 5c 2e 7b 3d 7d 20 53 5c  erState \.{=} S\
2270: 5f 52 65 61 64 79 7d 25 0a 20 5c 40 78 7b 5c 40  _Ready}%. \@x{\@
2280: 73 7b 38 35 2e 34 33 7d 20 5c 2e 7b 5c 6c 61 6e  s{85.43} \.{\lan
2290: 64 7d 20 73 65 6e 64 65 72 50 72 6f 70 6f 73 61  d} senderProposa
22a0: 6c 52 65 73 70 6f 6e 73 65 73 20 5c 2e 7b 3d 7d  lResponses \.{=}
22b0: 20 5b 20 69 20 5c 2e 7b 5c 69 6e 7d 20 43 6f 6e   [ i \.{\in} Con
22c0: 6e 65 63 74 6f 72 0a 20 5c 2e 7b 5c 6d 61 70 73  nector. \.{\maps
22d0: 74 6f 7d 20 7b 5c 46 41 4c 53 45 7d 20 5d 7d 25  to} {\FALSE} ]}%
22e0: 0a 5c 40 70 76 73 70 61 63 65 7b 38 2e 30 70 74  .\@pvspace{8.0pt
22f0: 7d 25 0a 20 5c 40 78 7b 20 49 6e 69 74 43 6f 6e  }%. \@x{ InitCon
2300: 6e 65 63 74 6f 72 56 61 72 73 20 5c 2e 7b 5c 64  nectorVars \.{\d
2310: 65 66 65 71 7d 20 63 6f 6e 6e 65 63 74 6f 72 53  efeq} connectorS
2320: 74 61 74 65 20 5c 2e 7b 3d 7d 20 5b 20 69 20 5c  tate \.{=} [ i \
2330: 2e 7b 5c 69 6e 7d 20 43 6f 6e 6e 65 63 74 6f 72  .{\in} Connector
2340: 0a 20 5c 2e 7b 5c 6d 61 70 73 74 6f 7d 20 43 5c  . \.{\mapsto} C\
2350: 5f 52 65 61 64 79 20 5d 7d 25 0a 5c 40 70 76 73  _Ready ]}%.\@pvs
2360: 70 61 63 65 7b 38 2e 30 70 74 7d 25 0a 20 5c 40  pace{8.0pt}%. \@
2370: 78 7b 20 49 6e 69 74 4c 65 64 67 65 72 56 61 72  x{ InitLedgerVar
2380: 73 20 5c 2e 7b 5c 64 65 66 65 71 7d 20 5c 2e 7b  s \.{\defeq} \.{
2390: 5c 6c 61 6e 64 7d 20 6c 65 64 67 65 72 53 74 61  \land} ledgerSta
23a0: 74 65 20 5c 2e 7b 3d 7d 20 5b 20 69 5c 40 73 7b  te \.{=} [ i\@s{
23b0: 33 2e 33 38 7d 0a 20 5c 2e 7b 5c 69 6e 7d 20 4c  3.38}. \.{\in} L
23c0: 65 64 67 65 72 20 5c 2e 7b 5c 6d 61 70 73 74 6f  edger \.{\mapsto
23d0: 7d 20 4c 5c 5f 50 72 6f 70 6f 73 65 64 20 5d 7d  } L\_Proposed ]}
23e0: 25 0a 20 5c 40 78 7b 5c 40 73 7b 38 34 2e 30 33  %. \@x{\@s{84.03
23f0: 7d 20 5c 2e 7b 5c 6c 61 6e 64 7d 20 6c 65 64 67  } \.{\land} ledg
2400: 65 72 45 78 70 69 72 61 74 69 6f 6e 20 5c 2e 7b  erExpiration \.{
2410: 3d 7d 20 5b 20 69 20 5c 2e 7b 5c 69 6e 7d 20 4c  =} [ i \.{\in} L
2420: 65 64 67 65 72 0a 20 5c 2e 7b 5c 6d 61 70 73 74  edger. \.{\mapst
2430: 6f 7d 20 43 6c 6f 63 6b 41 66 74 65 72 45 78 65  o} ClockAfterExe
2440: 63 75 74 69 6f 6e 20 5c 2e 7b 2d 7d 20 69 20 5d  cution \.{-} i ]
2450: 7d 25 0a 5c 40 70 76 73 70 61 63 65 7b 38 2e 30  }%.\@pvspace{8.0
2460: 70 74 7d 25 0a 5c 40 78 7b 20 49 6e 69 74 20 5c  pt}%.\@x{ Init \
2470: 2e 7b 5c 64 65 66 65 71 7d 20 5c 2e 7b 5c 6c 61  .{\defeq} \.{\la
2480: 6e 64 7d 20 63 6c 6f 63 6b 20 5c 2e 7b 3d 7d 20  nd} clock \.{=}
2490: 30 7d 25 0a 5c 40 78 7b 5c 40 73 7b 33 35 2e 37  0}%.\@x{\@s{35.7
24a0: 30 7d 20 5c 2e 7b 5c 6c 61 6e 64 7d 20 6d 65 73  0} \.{\land} mes
24b0: 73 61 67 65 73 20 5c 2e 7b 3d 7d 20 45 6d 70 74  sages \.{=} Empt
24c0: 79 42 61 67 7d 25 0a 5c 40 78 7b 5c 40 73 7b 33  yBag}%.\@x{\@s{3
24d0: 35 2e 37 30 7d 20 5c 2e 7b 5c 6c 61 6e 64 7d 20  5.70} \.{\land}
24e0: 49 6e 69 74 53 65 6e 64 65 72 56 61 72 73 7d 25  InitSenderVars}%
24f0: 0a 5c 40 78 7b 5c 40 73 7b 33 35 2e 37 30 7d 20  .\@x{\@s{35.70}
2500: 5c 2e 7b 5c 6c 61 6e 64 7d 20 49 6e 69 74 43 6f  \.{\land} InitCo
2510: 6e 6e 65 63 74 6f 72 56 61 72 73 7d 25 0a 5c 40  nnectorVars}%.\@
2520: 78 7b 5c 40 73 7b 33 35 2e 37 30 7d 20 5c 2e 7b  x{\@s{35.70} \.{
2530: 5c 6c 61 6e 64 7d 20 49 6e 69 74 4c 65 64 67 65  \land} InitLedge
2540: 72 56 61 72 73 7d 25 0a 5c 40 70 76 73 70 61 63  rVars}%.\@pvspac
2550: 65 7b 38 2e 30 70 74 7d 25 0a 5c 40 78 7b 7d 5c  e{8.0pt}%.\@x{}\
2560: 6d 69 64 62 61 72 5c 40 78 78 7b 7d 25 0a 5c 40  midbar\@xx{}%.\@
2570: 78 7b 7d 25 0a 5c 40 79 7b 5c 40 73 7b 30 7d 25  x{}%.\@y{\@s{0}%
2580: 0a 20 44 65 66 69 6e 65 20 73 74 61 74 65 20 74  . Define state t
2590: 72 61 6e 73 69 74 69 6f 6e 73 0a 7d 25 0a 5c 40  ransitions.}%.\@
25a0: 78 78 7b 7d 25 0a 5c 40 70 76 73 70 61 63 65 7b  xx{}%.\@pvspace{
25b0: 38 2e 30 70 74 7d 25 0a 5c 40 78 7b 7d 25 0a 5c  8.0pt}%.\@x{}%.\
25c0: 40 79 7b 5c 40 73 7b 30 7d 25 0a 20 50 61 72 74  @y{\@s{0}%. Part
25d0: 69 63 69 70 61 6e 74 20 5c 65 6e 73 75 72 65 6d  icipant \ensurem
25e0: 61 74 68 7b 69 7d 20 70 72 6f 70 6f 73 65 73 20  ath{i} proposes
25f0: 61 6c 6c 20 74 68 65 20 73 75 62 70 61 79 6d 65  all the subpayme
2600: 6e 74 73 0a 7d 25 0a 5c 40 78 78 7b 7d 25 0a 5c  nts.}%.\@xx{}%.\
2610: 40 78 7b 20 53 74 61 72 74 50 72 6f 70 6f 73 61  @x{ StartProposa
2620: 6c 50 68 61 73 65 20 28 20 69 20 29 20 5c 2e 7b  lPhase ( i ) \.{
2630: 5c 64 65 66 65 71 7d 7d 25 0a 5c 40 78 7b 5c 40  \defeq}}%.\@x{\@
2640: 73 7b 31 36 2e 34 7d 20 5c 2e 7b 5c 6c 61 6e 64  s{16.4} \.{\land
2650: 7d 20 73 65 6e 64 65 72 53 74 61 74 65 20 5c 2e  } senderState \.
2660: 7b 3d 7d 20 53 5c 5f 52 65 61 64 79 7d 25 0a 5c  {=} S\_Ready}%.\
2670: 40 78 7b 5c 40 73 7b 31 36 2e 34 7d 20 5c 2e 7b  @x{\@s{16.4} \.{
2680: 5c 6c 61 6e 64 7d 20 73 65 6e 64 65 72 53 74 61  \land} senderSta
2690: 74 65 20 5c 2e 7b 27 7d 20 5c 2e 7b 3d 7d 20 53  te \.{'} \.{=} S
26a0: 5c 5f 50 72 6f 70 6f 73 61 6c 57 61 69 74 69 6e  \_ProposalWaitin
26b0: 67 7d 25 0a 5c 40 78 7b 5c 40 73 7b 31 36 2e 34  g}%.\@x{\@s{16.4
26c0: 7d 20 5c 2e 7b 5c 6c 61 6e 64 7d 20 42 72 6f 61  } \.{\land} Broa
26d0: 64 63 61 73 74 20 28 20 5c 7b 20 5b 7d 25 0a 5c  dcast ( \{ [}%.\
26e0: 40 78 7b 5c 40 73 7b 33 35 2e 37 31 7d 20 6d 74  @x{\@s{35.71} mt
26f0: 79 70 65 5c 40 73 7b 31 33 2e 36 38 7d 20 5c 2e  ype\@s{13.68} \.
2700: 7b 5c 6d 61 70 73 74 6f 7d 20 53 75 62 70 61 79  {\mapsto} Subpay
2710: 6d 65 6e 74 50 72 6f 70 6f 73 61 6c 52 65 71 75  mentProposalRequ
2720: 65 73 74 20 2c 5c 2c 7d 25 0a 5c 40 78 7b 5c 40  est ,\,}%.\@x{\@
2730: 73 7b 33 35 2e 37 31 7d 20 6d 73 6f 75 72 63 65  s{35.71} msource
2740: 5c 40 73 7b 34 2e 31 7d 20 5c 2e 7b 5c 6d 61 70  \@s{4.1} \.{\map
2750: 73 74 6f 7d 20 69 20 2c 5c 2c 7d 25 0a 5c 40 78  sto} i ,\,}%.\@x
2760: 7b 5c 40 73 7b 33 35 2e 37 31 7d 20 6d 64 65 73  {\@s{35.71} mdes
2770: 74 5c 40 73 7b 31 33 2e 37 34 7d 20 5c 2e 7b 5c  t\@s{13.74} \.{\
2780: 6d 61 70 73 74 6f 7d 20 6b 7d 25 0a 5c 40 78 7b  mapsto} k}%.\@x{
2790: 5c 40 73 7b 32 37 2e 35 31 7d 20 5d 20 5c 2e 7b  \@s{27.51} ] \.{
27a0: 3a 7d 20 6b 20 5c 2e 7b 5c 69 6e 7d 20 43 6f 6e  :} k \.{\in} Con
27b0: 6e 65 63 74 6f 72 20 5c 7d 20 29 7d 25 0a 20 5c  nector \} )}%. \
27c0: 40 78 7b 5c 40 73 7b 31 36 2e 34 7d 20 5c 2e 7b  @x{\@s{16.4} \.{
27d0: 5c 6c 61 6e 64 7d 20 7b 5c 55 4e 43 48 41 4e 47  \land} {\UNCHANG
27e0: 45 44 7d 20 7b 5c 6c 61 6e 67 6c 65 7d 20 6c 65  ED} {\langle} le
27f0: 64 67 65 72 56 61 72 73 20 2c 5c 2c 20 63 6f 6e  dgerVars ,\, con
2800: 6e 65 63 74 6f 72 56 61 72 73 0a 20 2c 5c 2c 20  nectorVars. ,\,
2810: 73 65 6e 64 65 72 50 72 6f 70 6f 73 61 6c 52 65  senderProposalRe
2820: 73 70 6f 6e 73 65 73 20 7b 5c 72 61 6e 67 6c 65  sponses {\rangle
2830: 7d 7d 25 0a 5c 40 70 76 73 70 61 63 65 7b 38 2e  }}%.\@pvspace{8.
2840: 30 70 74 7d 25 0a 5c 40 78 7b 7d 25 0a 5c 40 79  0pt}%.\@x{}%.\@y
2850: 7b 5c 40 73 7b 30 7d 25 0a 20 50 61 72 74 69 63  {\@s{0}%. Partic
2860: 69 70 61 6e 74 20 5c 65 6e 73 75 72 65 6d 61 74  ipant \ensuremat
2870: 68 7b 69 7d 20 73 74 61 72 74 73 20 6f 66 66 20  h{i} starts off
2880: 74 68 65 20 70 72 65 70 61 72 61 74 69 6f 6e 20  the preparation
2890: 63 68 61 69 6e 0a 7d 25 0a 5c 40 78 78 7b 7d 25  chain.}%.\@xx{}%
28a0: 0a 5c 40 78 7b 20 53 74 61 72 74 50 72 65 70 61  .\@x{ StartPrepa
28b0: 72 61 74 69 6f 6e 50 68 61 73 65 20 28 20 69 20  rationPhase ( i
28c0: 29 20 5c 2e 7b 5c 64 65 66 65 71 7d 7d 25 0a 5c  ) \.{\defeq}}%.\
28d0: 40 78 7b 5c 40 73 7b 31 36 2e 34 7d 20 5c 2e 7b  @x{\@s{16.4} \.{
28e0: 5c 6c 61 6e 64 7d 20 73 65 6e 64 65 72 53 74 61  \land} senderSta
28f0: 74 65 20 5c 2e 7b 3d 7d 20 53 5c 5f 50 72 6f 70  te \.{=} S\_Prop
2900: 6f 73 61 6c 57 61 69 74 69 6e 67 7d 25 0a 20 5c  osalWaiting}%. \
2910: 40 78 7b 5c 40 73 7b 31 36 2e 34 7d 20 5c 2e 7b  @x{\@s{16.4} \.{
2920: 5c 6c 61 6e 64 7d 20 5c 45 5c 2c 20 70 20 5c 2e  \land} \E\, p \.
2930: 7b 5c 69 6e 7d 20 7b 5c 44 4f 4d 41 49 4e 7d 20  {\in} {\DOMAIN}
2940: 73 65 6e 64 65 72 50 72 6f 70 6f 73 61 6c 52 65  senderProposalRe
2950: 73 70 6f 6e 73 65 73 0a 20 5c 2e 7b 3a 7d 20 73  sponses. \.{:} s
2960: 65 6e 64 65 72 50 72 6f 70 6f 73 61 6c 52 65 73  enderProposalRes
2970: 70 6f 6e 73 65 73 20 5b 20 70 20 5d 7d 25 0a 5c  ponses [ p ]}%.\
2980: 40 78 7b 5c 40 73 7b 31 36 2e 34 7d 20 5c 2e 7b  @x{\@s{16.4} \.{
2990: 5c 6c 61 6e 64 7d 20 73 65 6e 64 65 72 53 74 61  \land} senderSta
29a0: 74 65 20 5c 2e 7b 27 7d 20 5c 2e 7b 3d 7d 20 53  te \.{'} \.{=} S
29b0: 5c 5f 57 61 69 74 69 6e 67 7d 25 0a 20 5c 40 78  \_Waiting}%. \@x
29c0: 7b 5c 40 73 7b 31 36 2e 34 7d 20 5c 2e 7b 5c 6c  {\@s{16.4} \.{\l
29d0: 61 6e 64 7d 20 53 65 6e 64 20 28 20 5b 20 6d 74  and} Send ( [ mt
29e0: 79 70 65 5c 40 73 7b 39 2e 35 38 7d 20 5c 2e 7b  ype\@s{9.58} \.{
29f0: 5c 6d 61 70 73 74 6f 7d 20 50 72 65 70 61 72 65  \mapsto} Prepare
2a00: 52 65 71 75 65 73 74 0a 20 2c 5c 2c 7d 25 0a 5c  Request. ,\,}%.\
2a10: 40 78 7b 5c 40 73 7b 35 36 2e 31 36 7d 20 6d 73  @x{\@s{56.16} ms
2a20: 6f 75 72 63 65 20 5c 2e 7b 5c 6d 61 70 73 74 6f  ource \.{\mapsto
2a30: 7d 20 69 20 2c 5c 2c 7d 25 0a 5c 40 78 7b 5c 40  } i ,\,}%.\@x{\@
2a40: 73 7b 35 36 2e 31 36 7d 20 6d 64 65 73 74 5c 40  s{56.16} mdest\@
2a50: 73 7b 39 2e 36 34 7d 20 5c 2e 7b 5c 6d 61 70 73  s{9.64} \.{\maps
2a60: 74 6f 7d 20 69 20 5c 2e 7b 2b 7d 20 31 20 5d 20  to} i \.{+} 1 ]
2a70: 29 7d 25 0a 20 5c 40 78 7b 5c 40 73 7b 31 36 2e  )}%. \@x{\@s{16.
2a80: 34 7d 20 5c 2e 7b 5c 6c 61 6e 64 7d 20 7b 5c 55  4} \.{\land} {\U
2a90: 4e 43 48 41 4e 47 45 44 7d 20 7b 5c 6c 61 6e 67  NCHANGED} {\lang
2aa0: 6c 65 7d 20 6c 65 64 67 65 72 56 61 72 73 20 2c  le} ledgerVars ,
2ab0: 5c 2c 20 63 6f 6e 6e 65 63 74 6f 72 56 61 72 73  \, connectorVars
2ac0: 0a 20 2c 5c 2c 20 73 65 6e 64 65 72 50 72 6f 70  . ,\, senderProp
2ad0: 6f 73 61 6c 52 65 73 70 6f 6e 73 65 73 20 7b 5c  osalResponses {\
2ae0: 72 61 6e 67 6c 65 7d 7d 25 0a 5c 40 70 76 73 70  rangle}}%.\@pvsp
2af0: 61 63 65 7b 38 2e 30 70 74 7d 25 0a 5c 40 78 7b  ace{8.0pt}%.\@x{
2b00: 7d 25 0a 5c 40 79 7b 5c 40 73 7b 30 7d 25 0a 20  }%.\@y{\@s{0}%.
2b10: 4c 65 64 67 65 72 20 73 70 6f 6e 74 61 6e 65 6f  Ledger spontaneo
2b20: 75 73 6c 79 20 61 62 6f 72 74 73 0a 7d 25 0a 5c  usly aborts.}%.\
2b30: 40 78 78 7b 7d 25 0a 5c 40 78 7b 20 4c 65 64 67  @xx{}%.\@x{ Ledg
2b40: 65 72 41 62 6f 72 74 20 28 20 6c 20 29 20 5c 2e  erAbort ( l ) \.
2b50: 7b 5c 64 65 66 65 71 7d 7d 25 0a 5c 40 78 7b 5c  {\defeq}}%.\@x{\
2b60: 40 73 7b 31 36 2e 34 7d 20 5c 2e 7b 5c 6c 61 6e  @s{16.4} \.{\lan
2b70: 64 7d 20 6c 65 64 67 65 72 53 74 61 74 65 20 5b  d} ledgerState [
2b80: 20 6c 20 5d 20 5c 2e 7b 3d 7d 20 4c 5c 5f 50 72   l ] \.{=} L\_Pr
2b90: 6f 70 6f 73 65 64 7d 25 0a 20 5c 40 78 7b 5c 40  oposed}%. \@x{\@
2ba0: 73 7b 31 36 2e 34 7d 20 5c 2e 7b 5c 6c 61 6e 64  s{16.4} \.{\land
2bb0: 7d 20 6c 65 64 67 65 72 53 74 61 74 65 20 5c 2e  } ledgerState \.
2bc0: 7b 27 7d 20 5c 2e 7b 3d 7d 20 5b 20 6c 65 64 67  {'} \.{=} [ ledg
2bd0: 65 72 53 74 61 74 65 20 7b 5c 45 58 43 45 50 54  erState {\EXCEPT
2be0: 7d 0a 20 7b 5c 62 61 6e 67 7d 20 5b 20 6c 20 5d  }. {\bang} [ l ]
2bf0: 20 5c 2e 7b 3d 7d 20 4c 5c 5f 41 62 6f 72 74 65   \.{=} L\_Aborte
2c00: 64 20 5d 7d 25 0a 5c 40 78 7b 5c 40 73 7b 31 36  d ]}%.\@x{\@s{16
2c10: 2e 34 7d 20 5c 2e 7b 5c 6c 61 6e 64 7d 20 53 65  .4} \.{\land} Se
2c20: 6e 64 20 28 20 5b 20 6d 74 79 70 65 5c 40 73 7b  nd ( [ mtype\@s{
2c30: 39 2e 35 38 7d 20 5c 2e 7b 5c 6d 61 70 73 74 6f  9.58} \.{\mapsto
2c40: 7d 20 41 62 6f 72 74 4e 6f 74 69 66 79 20 2c 5c  } AbortNotify ,\
2c50: 2c 7d 25 0a 5c 40 78 7b 5c 40 73 7b 35 36 2e 31  ,}%.\@x{\@s{56.1
2c60: 36 7d 20 6d 73 6f 75 72 63 65 20 5c 2e 7b 5c 6d  6} msource \.{\m
2c70: 61 70 73 74 6f 7d 20 6c 20 2c 5c 2c 7d 25 0a 5c  apsto} l ,\,}%.\
2c80: 40 78 7b 5c 40 73 7b 35 36 2e 31 36 7d 20 6d 64  @x{\@s{56.16} md
2c90: 65 73 74 5c 40 73 7b 39 2e 36 34 7d 20 5c 2e 7b  est\@s{9.64} \.{
2ca0: 5c 6d 61 70 73 74 6f 7d 20 6c 20 5c 2e 7b 2d 7d  \mapsto} l \.{-}
2cb0: 20 31 20 5d 20 29 7d 25 0a 20 5c 40 78 7b 5c 40   1 ] )}%. \@x{\@
2cc0: 73 7b 31 36 2e 34 7d 20 5c 2e 7b 5c 6c 61 6e 64  s{16.4} \.{\land
2cd0: 7d 20 7b 5c 55 4e 43 48 41 4e 47 45 44 7d 20 7b  } {\UNCHANGED} {
2ce0: 5c 6c 61 6e 67 6c 65 7d 20 73 65 6e 64 65 72 56  \langle} senderV
2cf0: 61 72 73 20 2c 5c 2c 20 63 6f 6e 6e 65 63 74 6f  ars ,\, connecto
2d00: 72 56 61 72 73 0a 20 2c 5c 2c 20 6c 65 64 67 65  rVars. ,\, ledge
2d10: 72 45 78 70 69 72 61 74 69 6f 6e 20 7b 5c 72 61  rExpiration {\ra
2d20: 6e 67 6c 65 7d 7d 25 0a 5c 40 70 76 73 70 61 63  ngle}}%.\@pvspac
2d30: 65 7b 38 2e 30 70 74 7d 25 0a 5c 40 78 7b 7d 25  e{8.0pt}%.\@x{}%
2d40: 0a 5c 40 79 7b 5c 40 73 7b 30 7d 25 0a 20 54 72  .\@y{\@s{0}%. Tr
2d50: 61 6e 73 66 65 72 20 74 69 6d 65 73 20 6f 75 74  ansfer times out
2d60: 0a 7d 25 0a 5c 40 78 78 7b 7d 25 0a 5c 40 78 7b  .}%.\@xx{}%.\@x{
2d70: 20 4c 65 64 67 65 72 54 69 6d 65 6f 75 74 20 28   LedgerTimeout (
2d80: 20 6c 20 29 20 5c 2e 7b 5c 64 65 66 65 71 7d 7d   l ) \.{\defeq}}
2d90: 25 0a 5c 40 78 7b 5c 40 73 7b 31 36 2e 34 7d 20  %.\@x{\@s{16.4}
2da0: 5c 2e 7b 5c 6c 61 6e 64 7d 20 7b 5c 6c 6e 6f 74  \.{\land} {\lnot
2db0: 7d 20 49 73 46 69 6e 61 6c 4c 65 64 67 65 72 53  } IsFinalLedgerS
2dc0: 74 61 74 65 20 28 20 6c 65 64 67 65 72 53 74 61  tate ( ledgerSta
2dd0: 74 65 20 5b 20 6c 20 5d 20 29 7d 25 0a 5c 40 78  te [ l ] )}%.\@x
2de0: 7b 5c 40 73 7b 31 36 2e 34 7d 20 5c 2e 7b 5c 6c  {\@s{16.4} \.{\l
2df0: 61 6e 64 7d 20 6c 65 64 67 65 72 45 78 70 69 72  and} ledgerExpir
2e00: 61 74 69 6f 6e 20 5b 20 6c 20 5d 20 5c 2e 7b 5c  ation [ l ] \.{\
2e10: 6c 65 71 7d 20 63 6c 6f 63 6b 7d 25 0a 20 5c 40  leq} clock}%. \@
2e20: 78 7b 5c 40 73 7b 31 36 2e 34 7d 20 5c 2e 7b 5c  x{\@s{16.4} \.{\
2e30: 6c 61 6e 64 7d 20 6c 65 64 67 65 72 53 74 61 74  land} ledgerStat
2e40: 65 20 5c 2e 7b 27 7d 20 5c 2e 7b 3d 7d 20 5b 20  e \.{'} \.{=} [
2e50: 6c 65 64 67 65 72 53 74 61 74 65 20 7b 5c 45 58  ledgerState {\EX
2e60: 43 45 50 54 7d 0a 20 7b 5c 62 61 6e 67 7d 20 5b  CEPT}. {\bang} [
2e70: 20 6c 20 5d 20 5c 2e 7b 3d 7d 20 4c 5c 5f 41 62   l ] \.{=} L\_Ab
2e80: 6f 72 74 65 64 20 5d 7d 25 0a 5c 40 78 7b 5c 40  orted ]}%.\@x{\@
2e90: 73 7b 31 36 2e 34 7d 20 5c 2e 7b 5c 6c 61 6e 64  s{16.4} \.{\land
2ea0: 7d 20 53 65 6e 64 20 28 20 5b 20 6d 74 79 70 65  } Send ( [ mtype
2eb0: 5c 40 73 7b 39 2e 35 38 7d 20 5c 2e 7b 5c 6d 61  \@s{9.58} \.{\ma
2ec0: 70 73 74 6f 7d 20 41 62 6f 72 74 4e 6f 74 69 66  psto} AbortNotif
2ed0: 79 20 2c 5c 2c 7d 25 0a 5c 40 78 7b 5c 40 73 7b  y ,\,}%.\@x{\@s{
2ee0: 35 36 2e 31 36 7d 20 6d 73 6f 75 72 63 65 20 5c  56.16} msource \
2ef0: 2e 7b 5c 6d 61 70 73 74 6f 7d 20 6c 20 2c 5c 2c  .{\mapsto} l ,\,
2f00: 7d 25 0a 5c 40 78 7b 5c 40 73 7b 35 36 2e 31 36  }%.\@x{\@s{56.16
2f10: 7d 20 6d 64 65 73 74 5c 40 73 7b 39 2e 36 34 7d  } mdest\@s{9.64}
2f20: 20 5c 2e 7b 5c 6d 61 70 73 74 6f 7d 20 6c 20 5c   \.{\mapsto} l \
2f30: 2e 7b 2d 7d 20 31 20 5d 20 29 7d 25 0a 20 5c 40  .{-} 1 ] )}%. \@
2f40: 78 7b 5c 40 73 7b 31 36 2e 34 7d 20 5c 2e 7b 5c  x{\@s{16.4} \.{\
2f50: 6c 61 6e 64 7d 20 7b 5c 55 4e 43 48 41 4e 47 45  land} {\UNCHANGE
2f60: 44 7d 20 7b 5c 6c 61 6e 67 6c 65 7d 20 73 65 6e  D} {\langle} sen
2f70: 64 65 72 56 61 72 73 20 2c 5c 2c 20 63 6f 6e 6e  derVars ,\, conn
2f80: 65 63 74 6f 72 56 61 72 73 0a 20 2c 5c 2c 20 6c  ectorVars. ,\, l
2f90: 65 64 67 65 72 45 78 70 69 72 61 74 69 6f 6e 20  edgerExpiration
2fa0: 7b 5c 72 61 6e 67 6c 65 7d 7d 25 0a 5c 40 70 76  {\rangle}}%.\@pv
2fb0: 73 70 61 63 65 7b 38 2e 30 70 74 7d 25 0a 5c 40  space{8.0pt}%.\@
2fc0: 78 7b 7d 25 0a 5c 40 79 7b 5c 40 73 7b 30 7d 25  x{}%.\@y{\@s{0}%
2fd0: 0a 20 49 66 20 6e 6f 20 6d 65 73 73 61 67 65 73  . If no messages
2fe0: 20 61 72 65 20 69 6e 20 66 6c 69 67 68 74 20 61   are in flight a
2ff0: 6e 64 20 74 68 65 20 73 65 6e 64 65 72 20 69 73  nd the sender is
3000: 6e 5c 6d 62 6f 78 7b 27 7d 74 20 64 6f 69 6e 67  n\mbox{'}t doing
3010: 20 61 6e 79 74 68 69 6e 67 2c 0a 20 61 64 76 61   anything,. adva
3020: 6e 63 65 20 74 68 65 0a 7d 25 0a 5c 40 78 78 7b  nce the.}%.\@xx{
3030: 7d 25 0a 5c 40 78 7b 7d 25 0a 5c 40 79 7b 5c 40  }%.\@x{}%.\@y{\@
3040: 73 7b 30 7d 25 0a 20 63 6c 6f 63 6b 0a 7d 25 0a  s{0}%. clock.}%.
3050: 5c 40 78 78 7b 7d 25 0a 5c 40 78 7b 20 4e 6f 74  \@xx{}%.\@x{ Not
3060: 68 69 6e 67 48 61 70 70 65 6e 73 20 5c 2e 7b 5c  hingHappens \.{\
3070: 64 65 66 65 71 7d 7d 25 0a 20 5c 40 78 7b 5c 40  defeq}}%. \@x{\@
3080: 73 7b 31 36 2e 34 7d 20 5c 2e 7b 5c 6c 61 6e 64  s{16.4} \.{\land
3090: 7d 20 63 6c 6f 63 6b 20 5c 2e 7b 5c 6c 65 71 7d  } clock \.{\leq}
30a0: 20 4d 61 78 20 28 20 5c 7b 20 6c 65 64 67 65 72   Max ( \{ ledger
30b0: 45 78 70 69 72 61 74 69 6f 6e 20 5b 20 78 20 5d  Expiration [ x ]
30c0: 20 5c 2e 7b 3a 7d 0a 20 78 20 5c 2e 7b 5c 69 6e   \.{:}. x \.{\in
30d0: 7d 20 4c 65 64 67 65 72 20 5c 7d 20 29 7d 25 0a  } Ledger \} )}%.
30e0: 5c 40 78 7b 5c 40 73 7b 31 36 2e 34 7d 20 5c 2e  \@x{\@s{16.4} \.
30f0: 7b 5c 6c 61 6e 64 7d 20 42 61 67 43 61 72 64 69  {\land} BagCardi
3100: 6e 61 6c 69 74 79 20 28 20 6d 65 73 73 61 67 65  nality ( message
3110: 73 20 29 20 5c 2e 7b 3d 7d 20 30 7d 25 0a 5c 40  s ) \.{=} 0}%.\@
3120: 78 7b 5c 40 73 7b 31 36 2e 34 7d 20 5c 2e 7b 5c  x{\@s{16.4} \.{\
3130: 6c 61 6e 64 7d 20 73 65 6e 64 65 72 53 74 61 74  land} senderStat
3140: 65 20 5c 2e 7b 5c 6e 65 71 7d 20 53 5c 5f 52 65  e \.{\neq} S\_Re
3150: 61 64 79 7d 25 0a 5c 40 78 7b 5c 40 73 7b 31 36  ady}%.\@x{\@s{16
3160: 2e 34 7d 20 5c 2e 7b 5c 6c 61 6e 64 7d 20 5c 2e  .4} \.{\land} \.
3170: 7b 5c 6c 6f 72 7d 20 73 65 6e 64 65 72 53 74 61  {\lor} senderSta
3180: 74 65 20 5c 2e 7b 5c 6e 65 71 7d 20 53 5c 5f 50  te \.{\neq} S\_P
3190: 72 6f 70 6f 73 61 6c 57 61 69 74 69 6e 67 7d 25  roposalWaiting}%
31a0: 0a 20 5c 40 78 7b 5c 40 73 7b 32 37 2e 35 31 7d  . \@x{\@s{27.51}
31b0: 20 5c 2e 7b 5c 6c 6f 72 7d 20 5c 41 5c 2c 20 70   \.{\lor} \A\, p
31c0: 20 5c 2e 7b 5c 69 6e 7d 20 7b 5c 44 4f 4d 41 49   \.{\in} {\DOMAI
31d0: 4e 7d 20 73 65 6e 64 65 72 50 72 6f 70 6f 73 61  N} senderProposa
31e0: 6c 52 65 73 70 6f 6e 73 65 73 0a 20 5c 2e 7b 3a  lResponses. \.{:
31f0: 7d 20 7b 5c 6c 6e 6f 74 7d 20 73 65 6e 64 65 72  } {\lnot} sender
3200: 50 72 6f 70 6f 73 61 6c 52 65 73 70 6f 6e 73 65  ProposalResponse
3210: 73 20 5b 20 70 20 5d 7d 25 0a 20 5c 40 78 7b 5c  s [ p ]}%. \@x{\
3220: 40 73 7b 31 36 2e 34 7d 20 5c 2e 7b 5c 6c 61 6e  @s{16.4} \.{\lan
3230: 64 7d 20 7b 5c 55 4e 43 48 41 4e 47 45 44 7d 20  d} {\UNCHANGED}
3240: 7b 5c 6c 61 6e 67 6c 65 7d 20 6d 65 73 73 61 67  {\langle} messag
3250: 65 73 20 2c 5c 2c 20 73 65 6e 64 65 72 56 61 72  es ,\, senderVar
3260: 73 20 2c 5c 2c 0a 20 63 6f 6e 6e 65 63 74 6f 72  s ,\,. connector
3270: 56 61 72 73 20 2c 5c 2c 20 6c 65 64 67 65 72 56  Vars ,\, ledgerV
3280: 61 72 73 20 7b 5c 72 61 6e 67 6c 65 7d 7d 25 0a  ars {\rangle}}%.
3290: 5c 40 70 76 73 70 61 63 65 7b 38 2e 30 70 74 7d  \@pvspace{8.0pt}
32a0: 25 0a 5c 40 78 7b 7d 5c 6d 69 64 62 61 72 5c 40  %.\@x{}\midbar\@
32b0: 78 78 7b 7d 25 0a 5c 40 78 7b 7d 25 0a 5c 40 79  xx{}%.\@x{}%.\@y
32c0: 7b 5c 40 73 7b 30 7d 25 0a 20 4d 65 73 73 61 67  {\@s{0}%. Messag
32d0: 65 20 68 61 6e 64 6c 65 72 73 0a 7d 25 0a 5c 40  e handlers.}%.\@
32e0: 78 78 7b 7d 25 0a 5c 40 78 7b 7d 25 0a 5c 40 79  xx{}%.\@x{}%.\@y
32f0: 7b 5c 40 73 7b 30 7d 25 0a 20 5c 65 6e 73 75 72  {\@s{0}%. \ensur
3300: 65 6d 61 74 68 7b 69 20 5c 2e 7b 3d 7d 7d 20 72  emath{i \.{=}} r
3310: 65 63 69 70 69 65 6e 74 2c 20 5c 65 6e 73 75 72  ecipient, \ensur
3320: 65 6d 61 74 68 7b 6a 20 5c 2e 7b 3d 7d 7d 20 73  emath{j \.{=}} s
3330: 65 6e 64 65 72 2c 20 5c 65 6e 73 75 72 65 6d 61  ender, \ensurema
3340: 74 68 7b 6d 0a 20 5c 2e 7b 3d 7d 7d 20 6d 65 73  th{m. \.{=}} mes
3350: 73 61 67 65 0a 7d 25 0a 5c 40 78 78 7b 7d 25 0a  sage.}%.\@xx{}%.
3360: 5c 40 70 76 73 70 61 63 65 7b 38 2e 30 70 74 7d  \@pvspace{8.0pt}
3370: 25 0a 5c 40 78 7b 7d 25 0a 5c 40 79 7b 5c 40 73  %.\@x{}%.\@y{\@s
3380: 7b 30 7d 25 0a 20 4c 65 64 67 65 72 20 5c 65 6e  {0}%. Ledger \en
3390: 73 75 72 65 6d 61 74 68 7b 69 7d 20 72 65 63 65  suremath{i} rece
33a0: 69 76 65 73 20 61 20 50 72 65 70 61 72 65 20 72  ives a Prepare r
33b0: 65 71 75 65 73 74 20 66 72 6f 6d 20 70 61 72 74  equest from part
33c0: 69 63 69 70 61 6e 74 0a 20 5c 65 6e 73 75 72 65  icipant. \ensure
33d0: 6d 61 74 68 7b 6a 0a 7d 7d 25 0a 5c 40 78 78 7b  math{j.}}%.\@xx{
33e0: 7d 25 0a 5c 40 78 7b 20 4c 65 64 67 65 72 48 61  }%.\@x{ LedgerHa
33f0: 6e 64 6c 65 50 72 65 70 61 72 65 52 65 71 75 65  ndlePrepareReque
3400: 73 74 20 28 20 69 20 2c 5c 2c 20 6a 20 2c 5c 2c  st ( i ,\, j ,\,
3410: 20 6d 20 29 20 5c 2e 7b 5c 64 65 66 65 71 7d 7d   m ) \.{\defeq}}
3420: 25 0a 20 5c 40 78 7b 5c 40 73 7b 31 36 2e 34 7d  %. \@x{\@s{16.4}
3430: 20 5c 2e 7b 5c 4c 45 54 7d 20 76 61 6c 69 64 20   \.{\LET} valid
3440: 5c 2e 7b 5c 64 65 66 65 71 7d 20 5c 2e 7b 5c 6c  \.{\defeq} \.{\l
3450: 61 6e 64 7d 20 6c 65 64 67 65 72 53 74 61 74 65  and} ledgerState
3460: 20 5b 20 69 20 5d 20 5c 2e 7b 3d 7d 0a 20 4c 5c   [ i ] \.{=}. L\
3470: 5f 50 72 6f 70 6f 73 65 64 7d 25 0a 5c 40 78 7b  _Proposed}%.\@x{
3480: 5c 40 73 7b 37 37 2e 31 36 7d 20 5c 2e 7b 5c 6c  \@s{77.16} \.{\l
3490: 61 6e 64 7d 20 6a 20 5c 2e 7b 3d 7d 20 69 20 5c  and} j \.{=} i \
34a0: 2e 7b 2d 7d 20 31 7d 25 0a 5c 40 78 7b 5c 40 73  .{-} 1}%.\@x{\@s
34b0: 7b 31 36 2e 34 7d 20 5c 2e 7b 5c 49 4e 7d 20 5c  {16.4} \.{\IN} \
34c0: 2e 7b 5c 6c 6f 72 7d 20 5c 2e 7b 5c 6c 61 6e 64  .{\lor} \.{\land
34d0: 7d 20 76 61 6c 69 64 7d 25 0a 5c 40 78 7b 5c 40  } valid}%.\@x{\@
34e0: 73 7b 34 37 2e 39 31 7d 20 5c 2e 7b 5c 6c 61 6e  s{47.91} \.{\lan
34f0: 64 7d 20 69 20 5c 2e 7b 5c 69 6e 7d 20 4c 65 64  d} i \.{\in} Led
3500: 67 65 72 7d 25 0a 20 5c 40 78 7b 5c 40 73 7b 34  ger}%. \@x{\@s{4
3510: 37 2e 39 31 7d 20 5c 2e 7b 5c 6c 61 6e 64 7d 20  7.91} \.{\land}
3520: 6c 65 64 67 65 72 53 74 61 74 65 20 5c 2e 7b 27  ledgerState \.{'
3530: 7d 20 5c 2e 7b 3d 7d 20 5b 20 6c 65 64 67 65 72  } \.{=} [ ledger
3540: 53 74 61 74 65 20 7b 5c 45 58 43 45 50 54 7d 0a  State {\EXCEPT}.
3550: 20 7b 5c 62 61 6e 67 7d 20 5b 20 69 20 5d 20 5c   {\bang} [ i ] \
3560: 2e 7b 3d 7d 20 4c 5c 5f 50 72 65 70 61 72 65 64  .{=} L\_Prepared
3570: 20 5d 7d 25 0a 20 5c 40 78 7b 5c 40 73 7b 34 37   ]}%. \@x{\@s{47
3580: 2e 39 31 7d 20 5c 2e 7b 5c 6c 61 6e 64 7d 20 52  .91} \.{\land} R
3590: 65 70 6c 79 20 28 20 5b 20 6d 74 79 70 65 5c 40  eply ( [ mtype\@
35a0: 73 7b 39 2e 35 38 7d 20 5c 2e 7b 5c 6d 61 70 73  s{9.58} \.{\maps
35b0: 74 6f 7d 20 50 72 65 70 61 72 65 4e 6f 74 69 66  to} PrepareNotif
35c0: 79 0a 20 2c 5c 2c 7d 25 0a 5c 40 78 7b 5c 40 73  y. ,\,}%.\@x{\@s
35d0: 7b 39 30 2e 34 37 7d 20 6d 73 6f 75 72 63 65 20  {90.47} msource
35e0: 5c 2e 7b 5c 6d 61 70 73 74 6f 7d 20 69 20 2c 5c  \.{\mapsto} i ,\
35f0: 2c 7d 25 0a 5c 40 78 7b 5c 40 73 7b 39 30 2e 34  ,}%.\@x{\@s{90.4
3600: 37 7d 20 6d 64 65 73 74 5c 40 73 7b 39 2e 36 34  7} mdest\@s{9.64
3610: 7d 20 5c 2e 7b 5c 6d 61 70 73 74 6f 7d 20 69 20  } \.{\mapsto} i
3620: 5c 2e 7b 2b 7d 20 31 20 5d 20 2c 5c 2c 20 6d 20  \.{+} 1 ] ,\, m
3630: 29 7d 25 0a 20 5c 40 78 7b 5c 40 73 7b 34 37 2e  )}%. \@x{\@s{47.
3640: 39 31 7d 20 5c 2e 7b 5c 6c 61 6e 64 7d 20 7b 5c  91} \.{\land} {\
3650: 55 4e 43 48 41 4e 47 45 44 7d 20 7b 5c 6c 61 6e  UNCHANGED} {\lan
3660: 67 6c 65 7d 20 73 65 6e 64 65 72 56 61 72 73 20  gle} senderVars
3670: 2c 5c 2c 20 63 6f 6e 6e 65 63 74 6f 72 56 61 72  ,\, connectorVar
3680: 73 0a 20 2c 5c 2c 20 6c 65 64 67 65 72 45 78 70  s. ,\, ledgerExp
3690: 69 72 61 74 69 6f 6e 20 7b 5c 72 61 6e 67 6c 65  iration {\rangle
36a0: 7d 7d 25 0a 5c 40 78 7b 5c 40 73 7b 33 36 2e 37  }}%.\@x{\@s{36.7
36b0: 39 7d 20 5c 2e 7b 5c 6c 6f 72 7d 20 5c 2e 7b 5c  9} \.{\lor} \.{\
36c0: 6c 61 6e 64 7d 20 7b 5c 6c 6e 6f 74 7d 20 76 61  land} {\lnot} va
36d0: 6c 69 64 7d 25 0a 5c 40 78 7b 5c 40 73 7b 34 37  lid}%.\@x{\@s{47
36e0: 2e 39 31 7d 20 5c 2e 7b 5c 6c 61 6e 64 7d 20 69  .91} \.{\land} i
36f0: 20 5c 2e 7b 5c 69 6e 7d 20 4c 65 64 67 65 72 7d   \.{\in} Ledger}
3700: 25 0a 5c 40 78 7b 5c 40 73 7b 34 37 2e 39 31 7d  %.\@x{\@s{47.91}
3710: 20 5c 2e 7b 5c 6c 61 6e 64 7d 20 44 69 73 63 61   \.{\land} Disca
3720: 72 64 20 28 20 6d 20 29 7d 25 0a 20 5c 40 78 7b  rd ( m )}%. \@x{
3730: 5c 40 73 7b 34 37 2e 39 31 7d 20 5c 2e 7b 5c 6c  \@s{47.91} \.{\l
3740: 61 6e 64 7d 20 7b 5c 55 4e 43 48 41 4e 47 45 44  and} {\UNCHANGED
3750: 7d 20 7b 5c 6c 61 6e 67 6c 65 7d 20 73 65 6e 64  } {\langle} send
3760: 65 72 56 61 72 73 20 2c 5c 2c 20 63 6f 6e 6e 65  erVars ,\, conne
3770: 63 74 6f 72 56 61 72 73 0a 20 2c 5c 2c 20 6c 65  ctorVars. ,\, le
3780: 64 67 65 72 56 61 72 73 20 7b 5c 72 61 6e 67 6c  dgerVars {\rangl
3790: 65 7d 7d 25 0a 5c 40 70 76 73 70 61 63 65 7b 38  e}}%.\@pvspace{8
37a0: 2e 30 70 74 7d 25 0a 5c 40 78 7b 7d 25 0a 5c 40  .0pt}%.\@x{}%.\@
37b0: 79 7b 5c 40 73 7b 30 7d 25 0a 20 4c 65 64 67 65  y{\@s{0}%. Ledge
37c0: 72 20 5c 65 6e 73 75 72 65 6d 61 74 68 7b 69 7d  r \ensuremath{i}
37d0: 20 72 65 63 65 69 76 65 73 20 61 6e 20 45 78 65   receives an Exe
37e0: 63 75 74 65 20 72 65 71 75 65 73 74 20 66 72 6f  cute request fro
37f0: 6d 20 70 72 6f 63 65 73 73 20 5c 65 6e 73 75 72  m process \ensur
3800: 65 6d 61 74 68 7b 6a 0a 7d 7d 25 0a 5c 40 78 78  emath{j.}}%.\@xx
3810: 7b 7d 25 0a 5c 40 78 7b 20 4c 65 64 67 65 72 48  {}%.\@x{ LedgerH
3820: 61 6e 64 6c 65 45 78 65 63 75 74 65 52 65 71 75  andleExecuteRequ
3830: 65 73 74 20 28 20 69 20 2c 5c 2c 20 6a 20 2c 5c  est ( i ,\, j ,\
3840: 2c 20 6d 20 29 20 5c 2e 7b 5c 64 65 66 65 71 7d  , m ) \.{\defeq}
3850: 7d 25 0a 20 5c 40 78 7b 5c 40 73 7b 31 36 2e 34  }%. \@x{\@s{16.4
3860: 7d 20 5c 2e 7b 5c 4c 45 54 7d 20 76 61 6c 69 64  } \.{\LET} valid
3870: 20 5c 2e 7b 5c 64 65 66 65 71 7d 20 5c 2e 7b 5c   \.{\defeq} \.{\
3880: 6c 61 6e 64 7d 20 6c 65 64 67 65 72 53 74 61 74  land} ledgerStat
3890: 65 20 5b 20 69 20 5d 20 5c 2e 7b 3d 7d 0a 20 4c  e [ i ] \.{=}. L
38a0: 5c 5f 50 72 65 70 61 72 65 64 7d 25 0a 5c 40 78  \_Prepared}%.\@x
38b0: 7b 5c 40 73 7b 37 37 2e 31 36 7d 20 5c 2e 7b 5c  {\@s{77.16} \.{\
38c0: 6c 61 6e 64 7d 20 6c 65 64 67 65 72 45 78 70 69  land} ledgerExpi
38d0: 72 61 74 69 6f 6e 20 5b 20 69 20 5d 20 5c 2e 7b  ration [ i ] \.{
38e0: 3e 7d 20 63 6c 6f 63 6b 7d 25 0a 5c 40 78 7b 5c  >} clock}%.\@x{\
38f0: 40 73 7b 37 37 2e 31 36 7d 20 5c 2e 7b 5c 6c 61  @s{77.16} \.{\la
3900: 6e 64 7d 20 6d 20 2e 20 6d 72 65 63 65 69 70 74  nd} m . mreceipt
3910: 20 5c 2e 7b 3d 7d 20 52 5c 5f 52 65 63 65 69 70   \.{=} R\_Receip
3920: 74 53 69 67 6e 61 74 75 72 65 7d 25 0a 5c 40 78  tSignature}%.\@x
3930: 7b 5c 40 73 7b 31 36 2e 34 7d 20 5c 2e 7b 5c 49  {\@s{16.4} \.{\I
3940: 4e 7d 20 5c 2e 7b 5c 6c 6f 72 7d 20 5c 2e 7b 5c  N} \.{\lor} \.{\
3950: 6c 61 6e 64 7d 20 76 61 6c 69 64 7d 25 0a 20 5c  land} valid}%. \
3960: 40 78 7b 5c 40 73 7b 34 37 2e 39 31 7d 20 5c 2e  @x{\@s{47.91} \.
3970: 7b 5c 6c 61 6e 64 7d 20 6c 65 64 67 65 72 53 74  {\land} ledgerSt
3980: 61 74 65 20 5c 2e 7b 27 7d 20 5c 2e 7b 3d 7d 20  ate \.{'} \.{=}
3990: 5b 20 6c 65 64 67 65 72 53 74 61 74 65 20 7b 5c  [ ledgerState {\
39a0: 45 58 43 45 50 54 7d 0a 20 7b 5c 62 61 6e 67 7d  EXCEPT}. {\bang}
39b0: 20 5b 20 69 20 5d 20 5c 2e 7b 3d 7d 20 4c 5c 5f   [ i ] \.{=} L\_
39c0: 45 78 65 63 75 74 65 64 20 5d 7d 25 0a 20 5c 40  Executed ]}%. \@
39d0: 78 7b 5c 40 73 7b 34 37 2e 39 31 7d 20 5c 2e 7b  x{\@s{47.91} \.{
39e0: 5c 6c 61 6e 64 7d 20 52 65 70 6c 79 20 28 20 5b  \land} Reply ( [
39f0: 20 6d 74 79 70 65 5c 40 73 7b 31 32 2e 32 39 7d   mtype\@s{12.29}
3a00: 20 5c 2e 7b 5c 6d 61 70 73 74 6f 7d 20 45 78 65   \.{\mapsto} Exe
3a10: 63 75 74 65 4e 6f 74 69 66 79 0a 20 2c 5c 2c 7d  cuteNotify. ,\,}
3a20: 25 0a 5c 40 78 7b 5c 40 73 7b 39 30 2e 34 37 7d  %.\@x{\@s{90.47}
3a30: 20 6d 73 6f 75 72 63 65 5c 40 73 7b 32 2e 37 31   msource\@s{2.71
3a40: 7d 20 5c 2e 7b 5c 6d 61 70 73 74 6f 7d 20 69 20  } \.{\mapsto} i
3a50: 2c 5c 2c 7d 25 0a 5c 40 78 7b 5c 40 73 7b 39 30  ,\,}%.\@x{\@s{90
3a60: 2e 34 37 7d 20 6d 64 65 73 74 5c 40 73 7b 31 32  .47} mdest\@s{12
3a70: 2e 33 35 7d 20 5c 2e 7b 5c 6d 61 70 73 74 6f 7d  .35} \.{\mapsto}
3a80: 20 69 20 5c 2e 7b 2d 7d 20 31 20 2c 5c 2c 7d 25   i \.{-} 1 ,\,}%
3a90: 0a 5c 40 78 7b 5c 40 73 7b 39 30 2e 34 37 7d 20  .\@x{\@s{90.47}
3aa0: 6d 72 65 63 65 69 70 74 5c 40 73 7b 31 2e 34 39  mreceipt\@s{1.49
3ab0: 7d 20 5c 2e 7b 5c 6d 61 70 73 74 6f 7d 20 6d 20  } \.{\mapsto} m
3ac0: 2e 20 6d 72 65 63 65 69 70 74 20 5d 20 2c 5c 2c  . mreceipt ] ,\,
3ad0: 20 6d 20 29 7d 25 0a 20 5c 40 78 7b 5c 40 73 7b   m )}%. \@x{\@s{
3ae0: 34 37 2e 39 31 7d 20 5c 2e 7b 5c 6c 61 6e 64 7d  47.91} \.{\land}
3af0: 20 7b 5c 55 4e 43 48 41 4e 47 45 44 7d 20 7b 5c   {\UNCHANGED} {\
3b00: 6c 61 6e 67 6c 65 7d 20 73 65 6e 64 65 72 56 61  langle} senderVa
3b10: 72 73 20 2c 5c 2c 20 63 6f 6e 6e 65 63 74 6f 72  rs ,\, connector
3b20: 56 61 72 73 0a 20 2c 5c 2c 20 6c 65 64 67 65 72  Vars. ,\, ledger
3b30: 45 78 70 69 72 61 74 69 6f 6e 20 7b 5c 72 61 6e  Expiration {\ran
3b40: 67 6c 65 7d 7d 25 0a 5c 40 78 7b 5c 40 73 7b 33  gle}}%.\@x{\@s{3
3b50: 36 2e 37 39 7d 20 5c 2e 7b 5c 6c 6f 72 7d 20 5c  6.79} \.{\lor} \
3b60: 2e 7b 5c 6c 61 6e 64 7d 20 7b 5c 6c 6e 6f 74 7d  .{\land} {\lnot}
3b70: 20 76 61 6c 69 64 7d 25 0a 5c 40 78 7b 5c 40 73   valid}%.\@x{\@s
3b80: 7b 34 37 2e 39 31 7d 20 5c 2e 7b 5c 6c 61 6e 64  {47.91} \.{\land
3b90: 7d 20 44 69 73 63 61 72 64 20 28 20 6d 20 29 7d  } Discard ( m )}
3ba0: 25 0a 20 5c 40 78 7b 5c 40 73 7b 34 37 2e 39 31  %. \@x{\@s{47.91
3bb0: 7d 20 5c 2e 7b 5c 6c 61 6e 64 7d 20 7b 5c 55 4e  } \.{\land} {\UN
3bc0: 43 48 41 4e 47 45 44 7d 20 7b 5c 6c 61 6e 67 6c  CHANGED} {\langl
3bd0: 65 7d 20 73 65 6e 64 65 72 56 61 72 73 20 2c 5c  e} senderVars ,\
3be0: 2c 20 63 6f 6e 6e 65 63 74 6f 72 56 61 72 73 0a  , connectorVars.
3bf0: 20 2c 5c 2c 20 6c 65 64 67 65 72 56 61 72 73 20   ,\, ledgerVars
3c00: 7b 5c 72 61 6e 67 6c 65 7d 7d 25 0a 5c 40 70 76  {\rangle}}%.\@pv
3c10: 73 70 61 63 65 7b 38 2e 30 70 74 7d 25 0a 5c 40  space{8.0pt}%.\@
3c20: 78 7b 7d 25 0a 5c 40 79 7b 5c 40 73 7b 30 7d 25  x{}%.\@y{\@s{0}%
3c30: 0a 20 4c 65 64 67 65 72 20 5c 65 6e 73 75 72 65  . Ledger \ensure
3c40: 6d 61 74 68 7b 69 7d 20 72 65 63 65 69 76 65 73  math{i} receives
3c50: 20 61 20 6d 65 73 73 61 67 65 0a 7d 25 0a 5c 40   a message.}%.\@
3c60: 78 78 7b 7d 25 0a 5c 40 78 7b 20 4c 65 64 67 65  xx{}%.\@x{ Ledge
3c70: 72 52 65 63 65 69 76 65 20 28 20 69 20 2c 5c 2c  rReceive ( i ,\,
3c80: 20 6a 20 2c 5c 2c 20 6d 20 29 20 5c 2e 7b 5c 64   j ,\, m ) \.{\d
3c90: 65 66 65 71 7d 7d 25 0a 5c 40 78 7b 5c 40 73 7b  efeq}}%.\@x{\@s{
3ca0: 31 36 2e 34 7d 20 5c 2e 7b 5c 6c 6f 72 7d 20 5c  16.4} \.{\lor} \
3cb0: 2e 7b 5c 6c 61 6e 64 7d 20 6d 20 2e 20 6d 74 79  .{\land} m . mty
3cc0: 70 65 20 5c 2e 7b 3d 7d 20 50 72 65 70 61 72 65  pe \.{=} Prepare
3cd0: 52 65 71 75 65 73 74 7d 25 0a 5c 40 78 7b 5c 40  Request}%.\@x{\@
3ce0: 73 7b 32 37 2e 35 31 7d 20 5c 2e 7b 5c 6c 61 6e  s{27.51} \.{\lan
3cf0: 64 7d 20 4c 65 64 67 65 72 48 61 6e 64 6c 65 50  d} LedgerHandleP
3d00: 72 65 70 61 72 65 52 65 71 75 65 73 74 20 28 20  repareRequest (
3d10: 69 20 2c 5c 2c 20 6a 20 2c 5c 2c 20 6d 20 29 7d  i ,\, j ,\, m )}
3d20: 25 0a 5c 40 78 7b 5c 40 73 7b 31 36 2e 34 7d 20  %.\@x{\@s{16.4}
3d30: 5c 2e 7b 5c 6c 6f 72 7d 20 5c 2e 7b 5c 6c 61 6e  \.{\lor} \.{\lan
3d40: 64 7d 20 6d 20 2e 20 6d 74 79 70 65 20 5c 2e 7b  d} m . mtype \.{
3d50: 3d 7d 20 45 78 65 63 75 74 65 52 65 71 75 65 73  =} ExecuteReques
3d60: 74 7d 25 0a 5c 40 78 7b 5c 40 73 7b 32 37 2e 35  t}%.\@x{\@s{27.5
3d70: 31 7d 20 5c 2e 7b 5c 6c 61 6e 64 7d 20 4c 65 64  1} \.{\land} Led
3d80: 67 65 72 48 61 6e 64 6c 65 45 78 65 63 75 74 65  gerHandleExecute
3d90: 52 65 71 75 65 73 74 20 28 20 69 20 2c 5c 2c 20  Request ( i ,\,
3da0: 6a 20 2c 5c 2c 20 6d 20 29 7d 25 0a 5c 40 70 76  j ,\, m )}%.\@pv
3db0: 73 70 61 63 65 7b 38 2e 30 70 74 7d 25 0a 5c 40  space{8.0pt}%.\@
3dc0: 78 7b 7d 25 0a 5c 40 79 7b 5c 40 73 7b 30 7d 25  x{}%.\@y{\@s{0}%
3dd0: 0a 20 53 65 6e 64 65 72 20 72 65 63 65 69 76 65  . Sender receive
3de0: 73 20 61 20 5c 65 6e 73 75 72 65 6d 61 74 68 7b  s a \ensuremath{
3df0: 53 75 62 70 61 79 6d 65 6e 74 50 72 6f 70 6f 73  SubpaymentPropos
3e00: 61 6c 7d 20 72 65 71 75 65 73 74 0a 7d 25 0a 5c  al} request.}%.\
3e10: 40 78 78 7b 7d 25 0a 5c 40 78 7b 20 53 65 6e 64  @xx{}%.\@x{ Send
3e20: 65 72 48 61 6e 64 6c 65 53 75 62 70 61 79 6d 65  erHandleSubpayme
3e30: 6e 74 50 72 6f 70 6f 73 61 6c 52 65 73 70 6f 6e  ntProposalRespon
3e40: 73 65 20 28 20 69 20 2c 5c 2c 20 6a 20 2c 5c 2c  se ( i ,\, j ,\,
3e50: 20 6d 20 29 20 5c 2e 7b 5c 64 65 66 65 71 7d 7d   m ) \.{\defeq}}
3e60: 25 0a 5c 40 78 7b 5c 40 73 7b 31 36 2e 34 7d 20  %.\@x{\@s{16.4}
3e70: 5c 2e 7b 5c 6c 61 6e 64 7d 20 69 20 5c 2e 7b 3d  \.{\land} i \.{=
3e80: 7d 20 53 65 6e 64 65 72 7d 25 0a 20 5c 40 78 7b  } Sender}%. \@x{
3e90: 5c 40 73 7b 31 36 2e 34 7d 20 5c 2e 7b 5c 6c 61  \@s{16.4} \.{\la
3ea0: 6e 64 7d 20 73 65 6e 64 65 72 50 72 6f 70 6f 73  nd} senderPropos
3eb0: 61 6c 52 65 73 70 6f 6e 73 65 73 20 5c 2e 7b 27  alResponses \.{'
3ec0: 7d 20 5c 2e 7b 3d 7d 20 5b 0a 20 73 65 6e 64 65  } \.{=} [. sende
3ed0: 72 50 72 6f 70 6f 73 61 6c 52 65 73 70 6f 6e 73  rProposalRespons
3ee0: 65 73 20 7b 5c 45 58 43 45 50 54 7d 20 7b 5c 62  es {\EXCEPT} {\b
3ef0: 61 6e 67 7d 20 5b 20 6a 20 5d 20 5c 2e 7b 3d 7d  ang} [ j ] \.{=}
3f00: 20 7b 5c 54 52 55 45 7d 20 5d 7d 25 0a 5c 40 78   {\TRUE} ]}%.\@x
3f10: 7b 5c 40 73 7b 31 36 2e 34 7d 20 5c 2e 7b 5c 6c  {\@s{16.4} \.{\l
3f20: 61 6e 64 7d 20 44 69 73 63 61 72 64 20 28 20 6d  and} Discard ( m
3f30: 20 29 7d 25 0a 20 5c 40 78 7b 5c 40 73 7b 31 36   )}%. \@x{\@s{16
3f40: 2e 34 7d 20 5c 2e 7b 5c 6c 61 6e 64 7d 20 7b 5c  .4} \.{\land} {\
3f50: 55 4e 43 48 41 4e 47 45 44 7d 20 7b 5c 6c 61 6e  UNCHANGED} {\lan
3f60: 67 6c 65 7d 20 63 6f 6e 6e 65 63 74 6f 72 56 61  gle} connectorVa
3f70: 72 73 20 2c 5c 2c 20 6c 65 64 67 65 72 56 61 72  rs ,\, ledgerVar
3f80: 73 0a 20 2c 5c 2c 20 73 65 6e 64 65 72 53 74 61  s. ,\, senderSta
3f90: 74 65 20 7b 5c 72 61 6e 67 6c 65 7d 7d 25 0a 5c  te {\rangle}}%.\
3fa0: 40 70 76 73 70 61 63 65 7b 38 2e 30 70 74 7d 25  @pvspace{8.0pt}%
3fb0: 0a 5c 40 78 7b 7d 25 0a 5c 40 79 7b 5c 40 73 7b  .\@x{}%.\@y{\@s{
3fc0: 30 7d 25 0a 20 4c 65 64 67 65 72 20 5c 65 6e 73  0}%. Ledger \ens
3fd0: 75 72 65 6d 61 74 68 7b 6a 7d 20 6e 6f 74 69 66  uremath{j} notif
3fe0: 69 65 73 20 73 65 6e 64 65 72 20 74 68 61 74 20  ies sender that
3ff0: 74 68 65 20 74 72 61 6e 73 66 65 72 20 69 73 20  the transfer is
4000: 65 78 65 63 75 74 65 64 0a 7d 25 0a 5c 40 78 78  executed.}%.\@xx
4010: 7b 7d 25 0a 5c 40 78 7b 20 53 65 6e 64 65 72 48  {}%.\@x{ SenderH
4020: 61 6e 64 6c 65 45 78 65 63 75 74 65 4e 6f 74 69  andleExecuteNoti
4030: 66 79 20 28 20 69 20 2c 5c 2c 20 6a 20 2c 5c 2c  fy ( i ,\, j ,\,
4040: 20 6d 20 29 20 5c 2e 7b 5c 64 65 66 65 71 7d 7d   m ) \.{\defeq}}
4050: 25 0a 5c 40 78 7b 5c 40 73 7b 31 36 2e 34 7d 20  %.\@x{\@s{16.4}
4060: 5c 2e 7b 5c 6c 6f 72 7d 20 5c 2e 7b 5c 6c 61 6e  \.{\lor} \.{\lan
4070: 64 7d 20 73 65 6e 64 65 72 53 74 61 74 65 20 5c  d} senderState \
4080: 2e 7b 3d 7d 20 53 5c 5f 57 61 69 74 69 6e 67 7d  .{=} S\_Waiting}
4090: 25 0a 5c 40 78 7b 5c 40 73 7b 32 37 2e 35 31 7d  %.\@x{\@s{27.51}
40a0: 20 5c 2e 7b 5c 6c 61 6e 64 7d 20 73 65 6e 64 65   \.{\land} sende
40b0: 72 53 74 61 74 65 20 5c 2e 7b 27 7d 20 5c 2e 7b  rState \.{'} \.{
40c0: 3d 7d 20 53 5c 5f 44 6f 6e 65 7d 25 0a 5c 40 78  =} S\_Done}%.\@x
40d0: 7b 5c 40 73 7b 32 37 2e 35 31 7d 20 5c 2e 7b 5c  {\@s{27.51} \.{\
40e0: 6c 61 6e 64 7d 20 44 69 73 63 61 72 64 20 28 20  land} Discard (
40f0: 6d 20 29 7d 25 0a 20 5c 40 78 7b 5c 40 73 7b 32  m )}%. \@x{\@s{2
4100: 37 2e 35 31 7d 20 5c 2e 7b 5c 6c 61 6e 64 7d 20  7.51} \.{\land}
4110: 7b 5c 55 4e 43 48 41 4e 47 45 44 7d 20 7b 5c 6c  {\UNCHANGED} {\l
4120: 61 6e 67 6c 65 7d 20 6c 65 64 67 65 72 56 61 72  angle} ledgerVar
4130: 73 20 2c 5c 2c 20 63 6f 6e 6e 65 63 74 6f 72 56  s ,\, connectorV
4140: 61 72 73 0a 20 2c 5c 2c 20 73 65 6e 64 65 72 50  ars. ,\, senderP
4150: 72 6f 70 6f 73 61 6c 52 65 73 70 6f 6e 73 65 73  roposalResponses
4160: 20 7b 5c 72 61 6e 67 6c 65 7d 7d 25 0a 5c 40 78   {\rangle}}%.\@x
4170: 7b 5c 40 73 7b 31 36 2e 34 7d 20 5c 2e 7b 5c 6c  {\@s{16.4} \.{\l
4180: 6f 72 7d 20 5c 2e 7b 5c 6c 61 6e 64 7d 20 73 65  or} \.{\land} se
4190: 6e 64 65 72 53 74 61 74 65 20 5c 2e 7b 5c 6e 65  nderState \.{\ne
41a0: 71 7d 20 53 5c 5f 57 61 69 74 69 6e 67 7d 25 0a  q} S\_Waiting}%.
41b0: 5c 40 78 7b 5c 40 73 7b 32 37 2e 35 31 7d 20 5c  \@x{\@s{27.51} \
41c0: 2e 7b 5c 6c 61 6e 64 7d 20 44 69 73 63 61 72 64  .{\land} Discard
41d0: 20 28 20 6d 20 29 7d 25 0a 20 5c 40 78 7b 5c 40   ( m )}%. \@x{\@
41e0: 73 7b 32 37 2e 35 31 7d 20 5c 2e 7b 5c 6c 61 6e  s{27.51} \.{\lan
41f0: 64 7d 20 7b 5c 55 4e 43 48 41 4e 47 45 44 7d 20  d} {\UNCHANGED}
4200: 7b 5c 6c 61 6e 67 6c 65 7d 20 73 65 6e 64 65 72  {\langle} sender
4210: 56 61 72 73 20 2c 5c 2c 20 63 6f 6e 6e 65 63 74  Vars ,\, connect
4220: 6f 72 56 61 72 73 0a 20 2c 5c 2c 20 6c 65 64 67  orVars. ,\, ledg
4230: 65 72 56 61 72 73 20 7b 5c 72 61 6e 67 6c 65 7d  erVars {\rangle}
4240: 7d 25 0a 5c 40 70 76 73 70 61 63 65 7b 38 2e 30  }%.\@pvspace{8.0
4250: 70 74 7d 25 0a 5c 40 78 7b 7d 25 0a 5c 40 79 7b  pt}%.\@x{}%.\@y{
4260: 5c 40 73 7b 30 7d 25 0a 20 4c 65 64 67 65 72 20  \@s{0}%. Ledger
4270: 5c 65 6e 73 75 72 65 6d 61 74 68 7b 6a 7d 20 6e  \ensuremath{j} n
4280: 6f 74 69 66 69 65 73 20 73 65 6e 64 65 72 20 74  otifies sender t
4290: 68 61 74 20 74 68 65 20 74 72 61 6e 73 66 65 72  hat the transfer
42a0: 20 69 73 20 61 62 6f 72 74 65 64 0a 7d 25 0a 5c   is aborted.}%.\
42b0: 40 78 78 7b 7d 25 0a 5c 40 78 7b 20 53 65 6e 64  @xx{}%.\@x{ Send
42c0: 65 72 48 61 6e 64 6c 65 41 62 6f 72 74 4e 6f 74  erHandleAbortNot
42d0: 69 66 79 20 28 20 69 20 2c 5c 2c 20 6a 20 2c 5c  ify ( i ,\, j ,\
42e0: 2c 20 6d 20 29 20 5c 2e 7b 5c 64 65 66 65 71 7d  , m ) \.{\defeq}
42f0: 7d 25 0a 20 5c 40 78 7b 5c 40 73 7b 31 36 2e 34  }%. \@x{\@s{16.4
4300: 7d 20 5c 2e 7b 5c 4c 45 54 7d 20 69 73 53 65 6e  } \.{\LET} isSen
4310: 64 65 72 57 61 69 74 69 6e 67 20 5c 2e 7b 5c 64  derWaiting \.{\d
4320: 65 66 65 71 7d 20 73 65 6e 64 65 72 53 74 61 74  efeq} senderStat
4330: 65 20 5c 2e 7b 5c 69 6e 7d 20 5c 7b 0a 20 53 5c  e \.{\in} \{. S\
4340: 5f 50 72 6f 70 6f 73 61 6c 57 61 69 74 69 6e 67  _ProposalWaiting
4350: 20 2c 5c 2c 20 53 5c 5f 57 61 69 74 69 6e 67 20   ,\, S\_Waiting
4360: 2c 5c 2c 20 53 5c 5f 52 65 61 64 79 20 5c 7d 7d  ,\, S\_Ready \}}
4370: 25 0a 5c 40 78 7b 5c 40 73 7b 31 36 2e 34 7d 20  %.\@x{\@s{16.4}
4380: 5c 2e 7b 5c 49 4e 7d 20 5c 2e 7b 5c 6c 6f 72 7d  \.{\IN} \.{\lor}
4390: 20 5c 2e 7b 5c 6c 61 6e 64 7d 20 69 73 53 65 6e   \.{\land} isSen
43a0: 64 65 72 57 61 69 74 69 6e 67 7d 25 0a 5c 40 78  derWaiting}%.\@x
43b0: 7b 5c 40 73 7b 34 37 2e 39 31 7d 20 5c 2e 7b 5c  {\@s{47.91} \.{\
43c0: 6c 61 6e 64 7d 20 73 65 6e 64 65 72 53 74 61 74  land} senderStat
43d0: 65 20 5c 2e 7b 27 7d 20 5c 2e 7b 3d 7d 20 53 5c  e \.{'} \.{=} S\
43e0: 5f 44 6f 6e 65 7d 25 0a 5c 40 78 7b 5c 40 73 7b  _Done}%.\@x{\@s{
43f0: 34 37 2e 39 31 7d 20 5c 2e 7b 5c 6c 61 6e 64 7d  47.91} \.{\land}
4400: 20 44 69 73 63 61 72 64 20 28 20 6d 20 29 7d 25   Discard ( m )}%
4410: 0a 20 5c 40 78 7b 5c 40 73 7b 34 37 2e 39 31 7d  . \@x{\@s{47.91}
4420: 20 5c 2e 7b 5c 6c 61 6e 64 7d 20 7b 5c 55 4e 43   \.{\land} {\UNC
4430: 48 41 4e 47 45 44 7d 20 7b 5c 6c 61 6e 67 6c 65  HANGED} {\langle
4440: 7d 20 6c 65 64 67 65 72 56 61 72 73 20 2c 5c 2c  } ledgerVars ,\,
4450: 20 63 6f 6e 6e 65 63 74 6f 72 56 61 72 73 0a 20   connectorVars.
4460: 2c 5c 2c 20 73 65 6e 64 65 72 50 72 6f 70 6f 73  ,\, senderPropos
4470: 61 6c 52 65 73 70 6f 6e 73 65 73 20 7b 5c 72 61  alResponses {\ra
4480: 6e 67 6c 65 7d 7d 25 0a 5c 40 78 7b 5c 40 73 7b  ngle}}%.\@x{\@s{
4490: 33 36 2e 37 39 7d 20 5c 2e 7b 5c 6c 6f 72 7d 20  36.79} \.{\lor}
44a0: 5c 2e 7b 5c 6c 61 6e 64 7d 20 7b 5c 6c 6e 6f 74  \.{\land} {\lnot
44b0: 7d 20 69 73 53 65 6e 64 65 72 57 61 69 74 69 6e  } isSenderWaitin
44c0: 67 7d 25 0a 5c 40 78 7b 5c 40 73 7b 34 37 2e 39  g}%.\@x{\@s{47.9
44d0: 31 7d 20 5c 2e 7b 5c 6c 61 6e 64 7d 20 44 69 73  1} \.{\land} Dis
44e0: 63 61 72 64 20 28 20 6d 20 29 7d 25 0a 20 5c 40  card ( m )}%. \@
44f0: 78 7b 5c 40 73 7b 34 37 2e 39 31 7d 20 5c 2e 7b  x{\@s{47.91} \.{
4500: 5c 6c 61 6e 64 7d 20 7b 5c 55 4e 43 48 41 4e 47  \land} {\UNCHANG
4510: 45 44 7d 20 7b 5c 6c 61 6e 67 6c 65 7d 20 73 65  ED} {\langle} se
4520: 6e 64 65 72 56 61 72 73 20 2c 5c 2c 20 63 6f 6e  nderVars ,\, con
4530: 6e 65 63 74 6f 72 56 61 72 73 0a 20 2c 5c 2c 20  nectorVars. ,\,
4540: 6c 65 64 67 65 72 56 61 72 73 20 7b 5c 72 61 6e  ledgerVars {\ran
4550: 67 6c 65 7d 7d 25 0a 5c 40 70 76 73 70 61 63 65  gle}}%.\@pvspace
4560: 7b 38 2e 30 70 74 7d 25 0a 5c 40 78 7b 7d 25 0a  {8.0pt}%.\@x{}%.
4570: 5c 40 79 7b 5c 40 73 7b 30 7d 25 0a 20 53 65 6e  \@y{\@s{0}%. Sen
4580: 64 65 72 20 72 65 63 65 69 76 65 73 20 61 20 6d  der receives a m
4590: 65 73 73 61 67 65 0a 7d 25 0a 5c 40 78 78 7b 7d  essage.}%.\@xx{}
45a0: 25 0a 5c 40 78 7b 20 53 65 6e 64 65 72 52 65 63  %.\@x{ SenderRec
45b0: 65 69 76 65 20 28 20 69 20 2c 5c 2c 20 6a 20 2c  eive ( i ,\, j ,
45c0: 5c 2c 20 6d 20 29 20 5c 2e 7b 5c 64 65 66 65 71  \, m ) \.{\defeq
45d0: 7d 7d 25 0a 5c 40 78 7b 5c 40 73 7b 31 36 2e 34  }}%.\@x{\@s{16.4
45e0: 7d 20 5c 2e 7b 5c 6c 6f 72 7d 20 5c 2e 7b 5c 6c  } \.{\lor} \.{\l
45f0: 61 6e 64 7d 20 6d 20 2e 20 6d 74 79 70 65 20 5c  and} m . mtype \
4600: 2e 7b 3d 7d 20 53 75 62 70 61 79 6d 65 6e 74 50  .{=} SubpaymentP
4610: 72 6f 70 6f 73 61 6c 52 65 73 70 6f 6e 73 65 7d  roposalResponse}
4620: 25 0a 20 5c 40 78 7b 5c 40 73 7b 32 37 2e 35 31  %. \@x{\@s{27.51
4630: 7d 20 5c 2e 7b 5c 6c 61 6e 64 7d 20 53 65 6e 64  } \.{\land} Send
4640: 65 72 48 61 6e 64 6c 65 53 75 62 70 61 79 6d 65  erHandleSubpayme
4650: 6e 74 50 72 6f 70 6f 73 61 6c 52 65 73 70 6f 6e  ntProposalRespon
4660: 73 65 20 28 20 69 20 2c 5c 2c 20 6a 20 2c 5c 2c  se ( i ,\, j ,\,
4670: 0a 20 6d 20 29 7d 25 0a 5c 40 78 7b 5c 40 73 7b  . m )}%.\@x{\@s{
4680: 31 36 2e 34 7d 20 5c 2e 7b 5c 6c 6f 72 7d 20 5c  16.4} \.{\lor} \
4690: 2e 7b 5c 6c 61 6e 64 7d 20 6d 20 2e 20 6d 74 79  .{\land} m . mty
46a0: 70 65 20 5c 2e 7b 3d 7d 20 45 78 65 63 75 74 65  pe \.{=} Execute
46b0: 4e 6f 74 69 66 79 7d 25 0a 5c 40 78 7b 5c 40 73  Notify}%.\@x{\@s
46c0: 7b 32 37 2e 35 31 7d 20 5c 2e 7b 5c 6c 61 6e 64  {27.51} \.{\land
46d0: 7d 20 53 65 6e 64 65 72 48 61 6e 64 6c 65 45 78  } SenderHandleEx
46e0: 65 63 75 74 65 4e 6f 74 69 66 79 20 28 20 69 20  ecuteNotify ( i
46f0: 2c 5c 2c 20 6a 20 2c 5c 2c 20 6d 20 29 7d 25 0a  ,\, j ,\, m )}%.
4700: 5c 40 78 7b 5c 40 73 7b 31 36 2e 34 7d 20 5c 2e  \@x{\@s{16.4} \.
4710: 7b 5c 6c 6f 72 7d 20 5c 2e 7b 5c 6c 61 6e 64 7d  {\lor} \.{\land}
4720: 20 6d 20 2e 20 6d 74 79 70 65 20 5c 2e 7b 3d 7d   m . mtype \.{=}
4730: 20 41 62 6f 72 74 4e 6f 74 69 66 79 7d 25 0a 5c   AbortNotify}%.\
4740: 40 78 7b 5c 40 73 7b 32 37 2e 35 31 7d 20 5c 2e  @x{\@s{27.51} \.
4750: 7b 5c 6c 61 6e 64 7d 20 53 65 6e 64 65 72 48 61  {\land} SenderHa
4760: 6e 64 6c 65 41 62 6f 72 74 4e 6f 74 69 66 79 20  ndleAbortNotify
4770: 28 20 69 20 2c 5c 2c 20 6a 20 2c 5c 2c 20 6d 20  ( i ,\, j ,\, m
4780: 29 7d 25 0a 5c 40 70 76 73 70 61 63 65 7b 38 2e  )}%.\@pvspace{8.
4790: 30 70 74 7d 25 0a 5c 40 78 7b 7d 25 0a 5c 40 79  0pt}%.\@x{}%.\@y
47a0: 7b 5c 40 73 7b 30 7d 25 0a 20 4c 65 64 67 65 72  {\@s{0}%. Ledger
47b0: 20 5c 65 6e 73 75 72 65 6d 61 74 68 7b 6a 7d 20   \ensuremath{j}
47c0: 6e 6f 74 69 66 69 65 73 20 72 65 63 69 70 69 65  notifies recipie
47d0: 6e 74 20 74 68 61 74 20 74 68 65 20 74 72 61 6e  nt that the tran
47e0: 73 66 65 72 20 69 73 20 70 72 65 70 61 72 65 64  sfer is prepared
47f0: 0a 7d 25 0a 5c 40 78 78 7b 7d 25 0a 5c 40 78 7b  .}%.\@xx{}%.\@x{
4800: 20 52 65 63 69 70 69 65 6e 74 48 61 6e 64 6c 65   RecipientHandle
4810: 50 72 65 70 61 72 65 4e 6f 74 69 66 79 20 28 20  PrepareNotify (
4820: 69 20 2c 5c 2c 20 6a 20 2c 5c 2c 20 6d 20 29 20  i ,\, j ,\, m )
4830: 5c 2e 7b 5c 64 65 66 65 71 7d 7d 25 0a 20 5c 40  \.{\defeq}}%. \@
4840: 78 7b 5c 40 73 7b 31 36 2e 34 7d 20 5c 2e 7b 5c  x{\@s{16.4} \.{\
4850: 6c 6f 72 7d 20 5c 2e 7b 5c 6c 61 6e 64 7d 20 52  lor} \.{\land} R
4860: 65 70 6c 79 20 28 20 5b 20 6d 74 79 70 65 5c 40  eply ( [ mtype\@
4870: 73 7b 31 32 2e 32 39 7d 20 5c 2e 7b 5c 6d 61 70  s{12.29} \.{\map
4880: 73 74 6f 7d 0a 20 45 78 65 63 75 74 65 52 65 71  sto}. ExecuteReq
4890: 75 65 73 74 20 2c 5c 2c 7d 25 0a 5c 40 78 7b 5c  uest ,\,}%.\@x{\
48a0: 40 73 7b 37 30 2e 30 37 7d 20 6d 73 6f 75 72 63  @s{70.07} msourc
48b0: 65 5c 40 73 7b 32 2e 37 31 7d 20 5c 2e 7b 5c 6d  e\@s{2.71} \.{\m
48c0: 61 70 73 74 6f 7d 20 69 20 2c 5c 2c 7d 25 0a 5c  apsto} i ,\,}%.\
48d0: 40 78 7b 5c 40 73 7b 37 30 2e 30 37 7d 20 6d 64  @x{\@s{70.07} md
48e0: 65 73 74 5c 40 73 7b 31 32 2e 33 35 7d 20 5c 2e  est\@s{12.35} \.
48f0: 7b 5c 6d 61 70 73 74 6f 7d 20 69 20 5c 2e 7b 2d  {\mapsto} i \.{-
4900: 7d 20 31 20 2c 5c 2c 7d 25 0a 5c 40 78 7b 5c 40  } 1 ,\,}%.\@x{\@
4910: 73 7b 37 30 2e 30 37 7d 20 6d 72 65 63 65 69 70  s{70.07} mreceip
4920: 74 5c 40 73 7b 31 2e 34 39 7d 20 5c 2e 7b 5c 6d  t\@s{1.49} \.{\m
4930: 61 70 73 74 6f 7d 20 52 5c 5f 52 65 63 65 69 70  apsto} R\_Receip
4940: 74 53 69 67 6e 61 74 75 72 65 20 5d 20 2c 5c 2c  tSignature ] ,\,
4950: 20 6d 20 29 7d 25 0a 20 5c 40 78 7b 5c 40 73 7b   m )}%. \@x{\@s{
4960: 32 37 2e 35 31 7d 20 5c 2e 7b 5c 6c 61 6e 64 7d  27.51} \.{\land}
4970: 20 7b 5c 55 4e 43 48 41 4e 47 45 44 7d 20 7b 5c   {\UNCHANGED} {\
4980: 6c 61 6e 67 6c 65 7d 20 73 65 6e 64 65 72 56 61  langle} senderVa
4990: 72 73 20 2c 5c 2c 20 63 6f 6e 6e 65 63 74 6f 72  rs ,\, connector
49a0: 56 61 72 73 0a 20 2c 5c 2c 20 6c 65 64 67 65 72  Vars. ,\, ledger
49b0: 56 61 72 73 20 7b 5c 72 61 6e 67 6c 65 7d 7d 25  Vars {\rangle}}%
49c0: 0a 5c 40 70 76 73 70 61 63 65 7b 38 2e 30 70 74  .\@pvspace{8.0pt
49d0: 7d 25 0a 5c 40 78 7b 7d 25 0a 5c 40 79 7b 5c 40  }%.\@x{}%.\@y{\@
49e0: 73 7b 30 7d 25 0a 20 52 65 63 69 70 69 65 6e 74  s{0}%. Recipient
49f0: 20 72 65 63 65 69 76 65 73 20 61 20 6d 65 73 73   receives a mess
4a00: 61 67 65 0a 7d 25 0a 5c 40 78 78 7b 7d 25 0a 5c  age.}%.\@xx{}%.\
4a10: 40 78 7b 20 52 65 63 69 70 69 65 6e 74 52 65 63  @x{ RecipientRec
4a20: 65 69 76 65 20 28 20 69 20 2c 5c 2c 20 6a 20 2c  eive ( i ,\, j ,
4a30: 5c 2c 20 6d 20 29 20 5c 2e 7b 5c 64 65 66 65 71  \, m ) \.{\defeq
4a40: 7d 7d 25 0a 5c 40 78 7b 5c 40 73 7b 31 36 2e 34  }}%.\@x{\@s{16.4
4a50: 7d 20 5c 2e 7b 5c 6c 6f 72 7d 20 5c 2e 7b 5c 6c  } \.{\lor} \.{\l
4a60: 61 6e 64 7d 20 6d 20 2e 20 6d 74 79 70 65 20 5c  and} m . mtype \
4a70: 2e 7b 3d 7d 20 50 72 65 70 61 72 65 4e 6f 74 69  .{=} PrepareNoti
4a80: 66 79 7d 25 0a 5c 40 78 7b 5c 40 73 7b 32 37 2e  fy}%.\@x{\@s{27.
4a90: 35 31 7d 20 5c 2e 7b 5c 6c 61 6e 64 7d 20 52 65  51} \.{\land} Re
4aa0: 63 69 70 69 65 6e 74 48 61 6e 64 6c 65 50 72 65  cipientHandlePre
4ab0: 70 61 72 65 4e 6f 74 69 66 79 20 28 20 69 20 2c  pareNotify ( i ,
4ac0: 5c 2c 20 6a 20 2c 5c 2c 20 6d 20 29 7d 25 0a 5c  \, j ,\, m )}%.\
4ad0: 40 70 76 73 70 61 63 65 7b 38 2e 30 70 74 7d 25  @pvspace{8.0pt}%
4ae0: 0a 5c 40 78 7b 7d 25 0a 5c 40 79 7b 5c 40 73 7b  .\@x{}%.\@y{\@s{
4af0: 30 7d 25 0a 20 43 6f 6e 6e 65 63 74 6f 72 20 5c  0}%. Connector \
4b00: 65 6e 73 75 72 65 6d 61 74 68 7b 69 7d 20 72 65  ensuremath{i} re
4b10: 63 65 69 76 65 73 20 61 20 5c 65 6e 73 75 72 65  ceives a \ensure
4b20: 6d 61 74 68 7b 53 75 62 70 61 79 6d 65 6e 74 50  math{SubpaymentP
4b30: 72 6f 70 6f 73 61 6c 7d 20 72 65 71 75 65 73 74  roposal} request
4b40: 0a 7d 25 0a 5c 40 78 78 7b 7d 25 0a 5c 40 78 7b  .}%.\@xx{}%.\@x{
4b50: 20 43 6f 6e 6e 65 63 74 6f 72 48 61 6e 64 6c 65   ConnectorHandle
4b60: 53 75 62 70 61 79 6d 65 6e 74 50 72 6f 70 6f 73  SubpaymentPropos
4b70: 61 6c 52 65 71 75 65 73 74 20 28 20 69 20 2c 5c  alRequest ( i ,\
4b80: 2c 20 6a 20 2c 5c 2c 20 6d 20 29 20 5c 2e 7b 5c  , j ,\, m ) \.{\
4b90: 64 65 66 65 71 7d 7d 25 0a 20 5c 40 78 7b 5c 40  defeq}}%. \@x{\@
4ba0: 73 7b 31 36 2e 34 7d 20 5c 2e 7b 5c 6c 61 6e 64  s{16.4} \.{\land
4bb0: 7d 20 63 6f 6e 6e 65 63 74 6f 72 53 74 61 74 65  } connectorState
4bc0: 20 5c 2e 7b 27 7d 20 5c 2e 7b 3d 7d 20 5b 20 63   \.{'} \.{=} [ c
4bd0: 6f 6e 6e 65 63 74 6f 72 53 74 61 74 65 20 7b 5c  onnectorState {\
4be0: 45 58 43 45 50 54 7d 0a 20 7b 5c 62 61 6e 67 7d  EXCEPT}. {\bang}
4bf0: 20 5b 20 69 20 5d 20 5c 2e 7b 3d 7d 20 43 5c 5f   [ i ] \.{=} C\_
4c00: 50 72 6f 70 6f 73 65 64 20 5d 7d 25 0a 20 5c 40  Proposed ]}%. \@
4c10: 78 7b 5c 40 73 7b 31 36 2e 34 7d 20 5c 2e 7b 5c  x{\@s{16.4} \.{\
4c20: 6c 61 6e 64 7d 20 52 65 70 6c 79 20 28 20 5b 20  land} Reply ( [
4c30: 6d 74 79 70 65 5c 40 73 7b 31 33 2e 36 38 7d 20  mtype\@s{13.68}
4c40: 5c 2e 7b 5c 6d 61 70 73 74 6f 7d 0a 20 53 75 62  \.{\mapsto}. Sub
4c50: 70 61 79 6d 65 6e 74 50 72 6f 70 6f 73 61 6c 52  paymentProposalR
4c60: 65 73 70 6f 6e 73 65 20 2c 5c 2c 7d 25 0a 5c 40  esponse ,\,}%.\@
4c70: 78 7b 5c 40 73 7b 35 38 2e 39 36 7d 20 6d 73 6f  x{\@s{58.96} mso
4c80: 75 72 63 65 5c 40 73 7b 34 2e 31 7d 20 5c 2e 7b  urce\@s{4.1} \.{
4c90: 5c 6d 61 70 73 74 6f 7d 20 69 20 2c 5c 2c 7d 25  \mapsto} i ,\,}%
4ca0: 0a 5c 40 78 7b 5c 40 73 7b 35 38 2e 39 36 7d 20  .\@x{\@s{58.96}
4cb0: 6d 64 65 73 74 5c 40 73 7b 31 33 2e 37 34 7d 20  mdest\@s{13.74}
4cc0: 5c 2e 7b 5c 6d 61 70 73 74 6f 7d 20 6a 20 5d 20  \.{\mapsto} j ]
4cd0: 2c 5c 2c 20 6d 20 29 7d 25 0a 20 5c 40 78 7b 5c  ,\, m )}%. \@x{\
4ce0: 40 73 7b 31 36 2e 34 7d 20 5c 2e 7b 5c 6c 61 6e  @s{16.4} \.{\lan
4cf0: 64 7d 20 7b 5c 55 4e 43 48 41 4e 47 45 44 7d 20  d} {\UNCHANGED}
4d00: 7b 5c 6c 61 6e 67 6c 65 7d 20 73 65 6e 64 65 72  {\langle} sender
4d10: 56 61 72 73 20 2c 5c 2c 20 6c 65 64 67 65 72 56  Vars ,\, ledgerV
4d20: 61 72 73 0a 20 7b 5c 72 61 6e 67 6c 65 7d 7d 25  ars. {\rangle}}%
4d30: 0a 5c 40 70 76 73 70 61 63 65 7b 38 2e 30 70 74  .\@pvspace{8.0pt
4d40: 7d 25 0a 5c 40 78 7b 7d 25 0a 5c 40 79 7b 5c 40  }%.\@x{}%.\@y{\@
4d50: 73 7b 30 7d 25 0a 20 4c 65 64 67 65 72 20 5c 65  s{0}%. Ledger \e
4d60: 6e 73 75 72 65 6d 61 74 68 7b 6a 7d 20 6e 6f 74  nsuremath{j} not
4d70: 69 66 69 65 73 20 63 6f 6e 6e 65 63 74 6f 72 20  ifies connector
4d80: 5c 65 6e 73 75 72 65 6d 61 74 68 7b 69 7d 20 74  \ensuremath{i} t
4d90: 68 61 74 20 74 68 65 20 74 72 61 6e 73 66 65 72  hat the transfer
4da0: 20 69 73 0a 20 70 72 65 70 61 72 65 64 0a 7d 25   is. prepared.}%
4db0: 0a 5c 40 78 78 7b 7d 25 0a 5c 40 78 7b 20 43 6f  .\@xx{}%.\@x{ Co
4dc0: 6e 6e 65 63 74 6f 72 48 61 6e 64 6c 65 50 72 65  nnectorHandlePre
4dd0: 70 61 72 65 4e 6f 74 69 66 79 20 28 20 69 20 2c  pareNotify ( i ,
4de0: 5c 2c 20 6a 20 2c 5c 2c 20 6d 20 29 20 5c 2e 7b  \, j ,\, m ) \.{
4df0: 5c 64 65 66 65 71 7d 7d 25 0a 20 5c 40 78 7b 5c  \defeq}}%. \@x{\
4e00: 40 73 7b 31 36 2e 34 7d 20 5c 2e 7b 5c 6c 6f 72  @s{16.4} \.{\lor
4e10: 7d 20 5c 2e 7b 5c 6c 61 6e 64 7d 20 52 65 70 6c  } \.{\land} Repl
4e20: 79 20 28 20 5b 20 6d 74 79 70 65 5c 40 73 7b 39  y ( [ mtype\@s{9
4e30: 2e 35 38 7d 20 5c 2e 7b 5c 6d 61 70 73 74 6f 7d  .58} \.{\mapsto}
4e40: 0a 20 50 72 65 70 61 72 65 52 65 71 75 65 73 74  . PrepareRequest
4e50: 20 2c 5c 2c 7d 25 0a 5c 40 78 7b 5c 40 73 7b 37   ,\,}%.\@x{\@s{7
4e60: 30 2e 30 37 7d 20 6d 73 6f 75 72 63 65 20 5c 2e  0.07} msource \.
4e70: 7b 5c 6d 61 70 73 74 6f 7d 20 69 20 2c 5c 2c 7d  {\mapsto} i ,\,}
4e80: 25 0a 5c 40 78 7b 5c 40 73 7b 37 30 2e 30 37 7d  %.\@x{\@s{70.07}
4e90: 20 6d 64 65 73 74 5c 40 73 7b 39 2e 36 34 7d 20   mdest\@s{9.64}
4ea0: 5c 2e 7b 5c 6d 61 70 73 74 6f 7d 20 69 20 5c 2e  \.{\mapsto} i \.
4eb0: 7b 2b 7d 20 31 20 5d 20 2c 5c 2c 20 6d 20 29 7d  {+} 1 ] ,\, m )}
4ec0: 25 0a 20 5c 40 78 7b 5c 40 73 7b 32 37 2e 35 31  %. \@x{\@s{27.51
4ed0: 7d 20 5c 2e 7b 5c 6c 61 6e 64 7d 20 7b 5c 55 4e  } \.{\land} {\UN
4ee0: 43 48 41 4e 47 45 44 7d 20 7b 5c 6c 61 6e 67 6c  CHANGED} {\langl
4ef0: 65 7d 20 73 65 6e 64 65 72 56 61 72 73 20 2c 5c  e} senderVars ,\
4f00: 2c 20 63 6f 6e 6e 65 63 74 6f 72 56 61 72 73 0a  , connectorVars.
4f10: 20 2c 5c 2c 20 6c 65 64 67 65 72 56 61 72 73 20   ,\, ledgerVars
4f20: 7b 5c 72 61 6e 67 6c 65 7d 7d 25 0a 5c 40 70 76  {\rangle}}%.\@pv
4f30: 73 70 61 63 65 7b 38 2e 30 70 74 7d 25 0a 5c 40  space{8.0pt}%.\@
4f40: 78 7b 7d 25 0a 5c 40 79 7b 5c 40 73 7b 30 7d 25  x{}%.\@y{\@s{0}%
4f50: 0a 20 4c 65 64 67 65 72 20 5c 65 6e 73 75 72 65  . Ledger \ensure
4f60: 6d 61 74 68 7b 6a 7d 20 6e 6f 74 69 66 69 65 73  math{j} notifies
4f70: 20 63 6f 6e 6e 65 63 74 6f 72 20 5c 65 6e 73 75   connector \ensu
4f80: 72 65 6d 61 74 68 7b 69 7d 20 74 68 61 74 20 74  remath{i} that t
4f90: 68 65 20 74 72 61 6e 73 66 65 72 20 69 73 0a 20  he transfer is.
4fa0: 65 78 65 63 75 74 65 64 0a 7d 25 0a 5c 40 78 78  executed.}%.\@xx
4fb0: 7b 7d 25 0a 5c 40 78 7b 20 43 6f 6e 6e 65 63 74  {}%.\@x{ Connect
4fc0: 6f 72 48 61 6e 64 6c 65 45 78 65 63 75 74 65 4e  orHandleExecuteN
4fd0: 6f 74 69 66 79 20 28 20 69 20 2c 5c 2c 20 6a 20  otify ( i ,\, j
4fe0: 2c 5c 2c 20 6d 20 29 20 5c 2e 7b 5c 64 65 66 65  ,\, m ) \.{\defe
4ff0: 71 7d 7d 25 0a 20 5c 40 78 7b 5c 40 73 7b 31 36  q}}%. \@x{\@s{16
5000: 2e 34 7d 20 5c 2e 7b 5c 6c 61 6e 64 7d 20 52 65  .4} \.{\land} Re
5010: 70 6c 79 20 28 20 5b 20 6d 74 79 70 65 5c 40 73  ply ( [ mtype\@s
5020: 7b 31 32 2e 32 39 7d 20 5c 2e 7b 5c 6d 61 70 73  {12.29} \.{\maps
5030: 74 6f 7d 20 45 78 65 63 75 74 65 52 65 71 75 65  to} ExecuteReque
5040: 73 74 0a 20 2c 5c 2c 7d 25 0a 5c 40 78 7b 5c 40  st. ,\,}%.\@x{\@
5050: 73 7b 35 38 2e 39 36 7d 20 6d 73 6f 75 72 63 65  s{58.96} msource
5060: 5c 40 73 7b 32 2e 37 31 7d 20 5c 2e 7b 5c 6d 61  \@s{2.71} \.{\ma
5070: 70 73 74 6f 7d 20 69 20 2c 5c 2c 7d 25 0a 5c 40  psto} i ,\,}%.\@
5080: 78 7b 5c 40 73 7b 35 38 2e 39 36 7d 20 6d 64 65  x{\@s{58.96} mde
5090: 73 74 5c 40 73 7b 31 32 2e 33 35 7d 20 5c 2e 7b  st\@s{12.35} \.{
50a0: 5c 6d 61 70 73 74 6f 7d 20 69 20 5c 2e 7b 2d 7d  \mapsto} i \.{-}
50b0: 20 31 20 2c 5c 2c 7d 25 0a 5c 40 78 7b 5c 40 73   1 ,\,}%.\@x{\@s
50c0: 7b 35 38 2e 39 36 7d 20 6d 72 65 63 65 69 70 74  {58.96} mreceipt
50d0: 5c 40 73 7b 31 2e 34 39 7d 20 5c 2e 7b 5c 6d 61  \@s{1.49} \.{\ma
50e0: 70 73 74 6f 7d 20 6d 20 2e 20 6d 72 65 63 65 69  psto} m . mrecei
50f0: 70 74 20 5d 20 2c 5c 2c 20 6d 20 29 7d 25 0a 20  pt ] ,\, m )}%.
5100: 5c 40 78 7b 5c 40 73 7b 31 36 2e 34 7d 20 5c 2e  \@x{\@s{16.4} \.
5110: 7b 5c 6c 61 6e 64 7d 20 7b 5c 55 4e 43 48 41 4e  {\land} {\UNCHAN
5120: 47 45 44 7d 20 7b 5c 6c 61 6e 67 6c 65 7d 20 73  GED} {\langle} s
5130: 65 6e 64 65 72 56 61 72 73 20 2c 5c 2c 20 63 6f  enderVars ,\, co
5140: 6e 6e 65 63 74 6f 72 56 61 72 73 0a 20 2c 5c 2c  nnectorVars. ,\,
5150: 20 6c 65 64 67 65 72 56 61 72 73 20 7b 5c 72 61   ledgerVars {\ra
5160: 6e 67 6c 65 7d 7d 25 0a 5c 40 70 76 73 70 61 63  ngle}}%.\@pvspac
5170: 65 7b 38 2e 30 70 74 7d 25 0a 5c 40 78 7b 7d 25  e{8.0pt}%.\@x{}%
5180: 0a 5c 40 79 7b 5c 40 73 7b 30 7d 25 0a 20 4c 65  .\@y{\@s{0}%. Le
5190: 64 67 65 72 20 5c 65 6e 73 75 72 65 6d 61 74 68  dger \ensuremath
51a0: 7b 6a 7d 20 6e 6f 74 69 66 69 65 73 20 63 6f 6e  {j} notifies con
51b0: 6e 65 63 74 6f 72 20 5c 65 6e 73 75 72 65 6d 61  nector \ensurema
51c0: 74 68 7b 69 7d 20 74 68 61 74 20 74 68 65 20 74  th{i} that the t
51d0: 72 61 6e 73 66 65 72 20 69 73 0a 20 61 62 6f 72  ransfer is. abor
51e0: 74 65 64 0a 7d 25 0a 5c 40 78 78 7b 7d 25 0a 5c  ted.}%.\@xx{}%.\
51f0: 40 78 7b 20 43 6f 6e 6e 65 63 74 6f 72 48 61 6e  @x{ ConnectorHan
5200: 64 6c 65 41 62 6f 72 74 4e 6f 74 69 66 79 20 28  dleAbortNotify (
5210: 20 69 20 2c 5c 2c 20 6a 20 2c 5c 2c 20 6d 20 29   i ,\, j ,\, m )
5220: 20 5c 2e 7b 5c 64 65 66 65 71 7d 7d 25 0a 5c 40   \.{\defeq}}%.\@
5230: 78 7b 5c 40 73 7b 31 36 2e 34 7d 20 5c 2e 7b 5c  x{\@s{16.4} \.{\
5240: 6c 61 6e 64 7d 20 44 69 73 63 61 72 64 20 28 20  land} Discard (
5250: 6d 20 29 7d 25 0a 20 5c 40 78 7b 5c 40 73 7b 31  m )}%. \@x{\@s{1
5260: 36 2e 34 7d 20 5c 2e 7b 5c 6c 61 6e 64 7d 20 7b  6.4} \.{\land} {
5270: 5c 55 4e 43 48 41 4e 47 45 44 7d 20 7b 5c 6c 61  \UNCHANGED} {\la
5280: 6e 67 6c 65 7d 20 73 65 6e 64 65 72 56 61 72 73  ngle} senderVars
5290: 20 2c 5c 2c 20 63 6f 6e 6e 65 63 74 6f 72 56 61   ,\, connectorVa
52a0: 72 73 0a 20 2c 5c 2c 20 6c 65 64 67 65 72 56 61  rs. ,\, ledgerVa
52b0: 72 73 20 7b 5c 72 61 6e 67 6c 65 7d 7d 25 0a 5c  rs {\rangle}}%.\
52c0: 40 70 76 73 70 61 63 65 7b 38 2e 30 70 74 7d 25  @pvspace{8.0pt}%
52d0: 0a 5c 40 78 7b 7d 25 0a 5c 40 79 7b 5c 40 73 7b  .\@x{}%.\@y{\@s{
52e0: 30 7d 25 0a 20 43 6f 6e 6e 65 63 74 6f 72 20 72  0}%. Connector r
52f0: 65 63 65 69 76 65 73 20 61 20 6d 65 73 73 61 67  eceives a messag
5300: 65 0a 7d 25 0a 5c 40 78 78 7b 7d 25 0a 5c 40 78  e.}%.\@xx{}%.\@x
5310: 7b 20 43 6f 6e 6e 65 63 74 6f 72 52 65 63 65 69  { ConnectorRecei
5320: 76 65 20 28 20 69 20 2c 5c 2c 20 6a 20 2c 5c 2c  ve ( i ,\, j ,\,
5330: 20 6d 20 29 20 5c 2e 7b 5c 64 65 66 65 71 7d 7d   m ) \.{\defeq}}
5340: 25 0a 5c 40 78 7b 5c 40 73 7b 31 36 2e 34 7d 20  %.\@x{\@s{16.4}
5350: 5c 2e 7b 5c 6c 6f 72 7d 20 5c 2e 7b 5c 6c 61 6e  \.{\lor} \.{\lan
5360: 64 7d 20 6d 20 2e 20 6d 74 79 70 65 20 5c 2e 7b  d} m . mtype \.{
5370: 3d 7d 20 53 75 62 70 61 79 6d 65 6e 74 50 72 6f  =} SubpaymentPro
5380: 70 6f 73 61 6c 52 65 71 75 65 73 74 7d 25 0a 20  posalRequest}%.
5390: 5c 40 78 7b 5c 40 73 7b 32 37 2e 35 31 7d 20 5c  \@x{\@s{27.51} \
53a0: 2e 7b 5c 6c 61 6e 64 7d 20 43 6f 6e 6e 65 63 74  .{\land} Connect
53b0: 6f 72 48 61 6e 64 6c 65 53 75 62 70 61 79 6d 65  orHandleSubpayme
53c0: 6e 74 50 72 6f 70 6f 73 61 6c 52 65 71 75 65 73  ntProposalReques
53d0: 74 20 28 20 69 20 2c 5c 2c 20 6a 0a 20 2c 5c 2c  t ( i ,\, j. ,\,
53e0: 20 6d 20 29 7d 25 0a 5c 40 78 7b 5c 40 73 7b 31   m )}%.\@x{\@s{1
53f0: 36 2e 34 7d 20 5c 2e 7b 5c 6c 6f 72 7d 20 5c 2e  6.4} \.{\lor} \.
5400: 7b 5c 6c 61 6e 64 7d 20 6d 20 2e 20 6d 74 79 70  {\land} m . mtyp
5410: 65 20 5c 2e 7b 3d 7d 20 50 72 65 70 61 72 65 4e  e \.{=} PrepareN
5420: 6f 74 69 66 79 7d 25 0a 5c 40 78 7b 5c 40 73 7b  otify}%.\@x{\@s{
5430: 32 37 2e 35 31 7d 20 5c 2e 7b 5c 6c 61 6e 64 7d  27.51} \.{\land}
5440: 20 43 6f 6e 6e 65 63 74 6f 72 48 61 6e 64 6c 65   ConnectorHandle
5450: 50 72 65 70 61 72 65 4e 6f 74 69 66 79 20 28 20  PrepareNotify (
5460: 69 20 2c 5c 2c 20 6a 20 2c 5c 2c 20 6d 20 29 7d  i ,\, j ,\, m )}
5470: 25 0a 5c 40 78 7b 5c 40 73 7b 31 36 2e 34 7d 20  %.\@x{\@s{16.4}
5480: 5c 2e 7b 5c 6c 6f 72 7d 20 5c 2e 7b 5c 6c 61 6e  \.{\lor} \.{\lan
5490: 64 7d 20 6d 20 2e 20 6d 74 79 70 65 20 5c 2e 7b  d} m . mtype \.{
54a0: 3d 7d 20 45 78 65 63 75 74 65 4e 6f 74 69 66 79  =} ExecuteNotify
54b0: 7d 25 0a 5c 40 78 7b 5c 40 73 7b 32 37 2e 35 31  }%.\@x{\@s{27.51
54c0: 7d 20 5c 2e 7b 5c 6c 61 6e 64 7d 20 43 6f 6e 6e  } \.{\land} Conn
54d0: 65 63 74 6f 72 48 61 6e 64 6c 65 45 78 65 63 75  ectorHandleExecu
54e0: 74 65 4e 6f 74 69 66 79 20 28 20 69 20 2c 5c 2c  teNotify ( i ,\,
54f0: 20 6a 20 2c 5c 2c 20 6d 20 29 7d 25 0a 5c 40 78   j ,\, m )}%.\@x
5500: 7b 5c 40 73 7b 31 36 2e 34 7d 20 5c 2e 7b 5c 6c  {\@s{16.4} \.{\l
5510: 6f 72 7d 20 5c 2e 7b 5c 6c 61 6e 64 7d 20 6d 20  or} \.{\land} m
5520: 2e 20 6d 74 79 70 65 20 5c 2e 7b 3d 7d 20 41 62  . mtype \.{=} Ab
5530: 6f 72 74 4e 6f 74 69 66 79 7d 25 0a 5c 40 78 7b  ortNotify}%.\@x{
5540: 5c 40 73 7b 32 37 2e 35 31 7d 20 5c 2e 7b 5c 6c  \@s{27.51} \.{\l
5550: 61 6e 64 7d 20 43 6f 6e 6e 65 63 74 6f 72 48 61  and} ConnectorHa
5560: 6e 64 6c 65 41 62 6f 72 74 4e 6f 74 69 66 79 20  ndleAbortNotify
5570: 28 20 69 20 2c 5c 2c 20 6a 20 2c 5c 2c 20 6d 20  ( i ,\, j ,\, m
5580: 29 7d 25 0a 5c 40 70 76 73 70 61 63 65 7b 38 2e  )}%.\@pvspace{8.
5590: 30 70 74 7d 25 0a 5c 40 78 7b 7d 25 0a 5c 40 79  0pt}%.\@x{}%.\@y
55a0: 7b 5c 40 73 7b 30 7d 25 0a 20 52 65 63 65 69 76  {\@s{0}%. Receiv
55b0: 65 20 61 20 6d 65 73 73 61 67 65 0a 7d 25 0a 5c  e a message.}%.\
55c0: 40 78 78 7b 7d 25 0a 5c 40 78 7b 20 52 65 63 65  @xx{}%.\@x{ Rece
55d0: 69 76 65 20 28 20 6d 20 29 20 5c 2e 7b 5c 64 65  ive ( m ) \.{\de
55e0: 66 65 71 7d 7d 25 0a 5c 40 78 7b 5c 40 73 7b 31  feq}}%.\@x{\@s{1
55f0: 36 2e 34 7d 20 5c 2e 7b 5c 4c 45 54 7d 20 69 5c  6.4} \.{\LET} i\
5600: 40 73 7b 30 2e 34 32 7d 20 5c 2e 7b 5c 64 65 66  @s{0.42} \.{\def
5610: 65 71 7d 20 6d 20 2e 20 6d 64 65 73 74 7d 25 0a  eq} m . mdest}%.
5620: 5c 40 78 7b 5c 40 73 7b 33 36 2e 37 39 7d 20 6a  \@x{\@s{36.79} j
5630: 20 5c 2e 7b 5c 64 65 66 65 71 7d 20 6d 20 2e 20   \.{\defeq} m .
5640: 6d 73 6f 75 72 63 65 7d 25 0a 5c 40 78 7b 5c 40  msource}%.\@x{\@
5650: 73 7b 31 36 2e 34 7d 20 5c 2e 7b 5c 49 4e 7d 20  s{16.4} \.{\IN}
5660: 5c 2e 7b 5c 6c 6f 72 7d 20 5c 2e 7b 5c 6c 61 6e  \.{\lor} \.{\lan
5670: 64 7d 20 69 20 5c 2e 7b 5c 69 6e 7d 20 4c 65 64  d} i \.{\in} Led
5680: 67 65 72 7d 25 0a 5c 40 78 7b 5c 40 73 7b 34 37  ger}%.\@x{\@s{47
5690: 2e 39 31 7d 20 5c 2e 7b 5c 6c 61 6e 64 7d 20 4c  .91} \.{\land} L
56a0: 65 64 67 65 72 52 65 63 65 69 76 65 20 28 20 69  edgerReceive ( i
56b0: 20 2c 5c 2c 20 6a 20 2c 5c 2c 20 6d 20 29 7d 25   ,\, j ,\, m )}%
56c0: 0a 5c 40 78 7b 5c 40 73 7b 33 36 2e 37 39 7d 20  .\@x{\@s{36.79}
56d0: 5c 2e 7b 5c 6c 6f 72 7d 20 5c 2e 7b 5c 6c 61 6e  \.{\lor} \.{\lan
56e0: 64 7d 20 69 20 5c 2e 7b 3d 7d 20 53 65 6e 64 65  d} i \.{=} Sende
56f0: 72 7d 25 0a 5c 40 78 7b 5c 40 73 7b 34 37 2e 39  r}%.\@x{\@s{47.9
5700: 31 7d 20 5c 2e 7b 5c 6c 61 6e 64 7d 20 53 65 6e  1} \.{\land} Sen
5710: 64 65 72 52 65 63 65 69 76 65 20 28 20 69 20 2c  derReceive ( i ,
5720: 5c 2c 20 6a 20 2c 5c 2c 20 6d 20 29 7d 25 0a 5c  \, j ,\, m )}%.\
5730: 40 78 7b 5c 40 73 7b 33 36 2e 37 39 7d 20 5c 2e  @x{\@s{36.79} \.
5740: 7b 5c 6c 6f 72 7d 20 5c 2e 7b 5c 6c 61 6e 64 7d  {\lor} \.{\land}
5750: 20 69 20 5c 2e 7b 3d 7d 20 52 65 63 69 70 69 65   i \.{=} Recipie
5760: 6e 74 7d 25 0a 5c 40 78 7b 5c 40 73 7b 34 37 2e  nt}%.\@x{\@s{47.
5770: 39 31 7d 20 5c 2e 7b 5c 6c 61 6e 64 7d 20 52 65  91} \.{\land} Re
5780: 63 69 70 69 65 6e 74 52 65 63 65 69 76 65 20 28  cipientReceive (
5790: 20 69 20 2c 5c 2c 20 6a 20 2c 5c 2c 20 6d 20 29   i ,\, j ,\, m )
57a0: 7d 25 0a 5c 40 78 7b 5c 40 73 7b 33 36 2e 37 39  }%.\@x{\@s{36.79
57b0: 7d 20 5c 2e 7b 5c 6c 6f 72 7d 20 5c 2e 7b 5c 6c  } \.{\lor} \.{\l
57c0: 61 6e 64 7d 20 69 20 5c 2e 7b 5c 69 6e 7d 20 43  and} i \.{\in} C
57d0: 6f 6e 6e 65 63 74 6f 72 7d 25 0a 5c 40 78 7b 5c  onnector}%.\@x{\
57e0: 40 73 7b 34 37 2e 39 31 7d 20 5c 2e 7b 5c 6c 61  @s{47.91} \.{\la
57f0: 6e 64 7d 20 43 6f 6e 6e 65 63 74 6f 72 52 65 63  nd} ConnectorRec
5800: 65 69 76 65 20 28 20 69 20 2c 5c 2c 20 6a 20 2c  eive ( i ,\, j ,
5810: 5c 2c 20 6d 20 29 7d 25 0a 5c 40 70 76 73 70 61  \, m )}%.\@pvspa
5820: 63 65 7b 38 2e 30 70 74 7d 25 0a 5c 40 78 7b 7d  ce{8.0pt}%.\@x{}
5830: 25 0a 5c 40 79 7b 5c 40 73 7b 30 7d 25 0a 20 45  %.\@y{\@s{0}%. E
5840: 6e 64 20 6f 66 20 6d 65 73 73 61 67 65 20 68 61  nd of message ha
5850: 6e 64 6c 65 72 73 0a 7d 25 0a 5c 40 78 78 7b 7d  ndlers.}%.\@xx{}
5860: 25 0a 5c 40 78 7b 7d 5c 6d 69 64 62 61 72 5c 40  %.\@x{}\midbar\@
5870: 78 78 7b 7d 25 0a 5c 40 78 7b 7d 25 0a 5c 40 79  xx{}%.\@x{}%.\@y
5880: 7b 5c 40 73 7b 30 7d 25 0a 20 44 65 66 69 6e 65  {\@s{0}%. Define
5890: 73 20 68 6f 77 20 74 68 65 20 76 61 72 69 61 62  s how the variab
58a0: 6c 65 73 20 6d 61 79 20 74 72 61 6e 73 69 74 69  les may transiti
58b0: 6f 6e 0a 7d 25 0a 5c 40 78 78 7b 7d 25 0a 5c 40  on.}%.\@xx{}%.\@
58c0: 70 76 73 70 61 63 65 7b 38 2e 30 70 74 7d 25 0a  pvspace{8.0pt}%.
58d0: 5c 40 78 7b 20 54 65 72 6d 69 6e 61 74 69 6f 6e  \@x{ Termination
58e0: 20 5c 2e 7b 5c 64 65 66 65 71 7d 7d 25 0a 20 5c   \.{\defeq}}%. \
58f0: 40 78 7b 5c 40 73 7b 31 36 2e 34 7d 20 5c 2e 7b  @x{\@s{16.4} \.{
5900: 5c 6c 61 6e 64 7d 20 5c 41 5c 2c 20 6c 20 5c 2e  \land} \A\, l \.
5910: 7b 5c 69 6e 7d 20 4c 65 64 67 65 72 20 5c 2e 7b  {\in} Ledger \.{
5920: 3a 7d 20 49 73 46 69 6e 61 6c 4c 65 64 67 65 72  :} IsFinalLedger
5930: 53 74 61 74 65 20 28 0a 20 6c 65 64 67 65 72 53  State (. ledgerS
5940: 74 61 74 65 20 5b 20 6c 20 5d 20 29 7d 25 0a 5c  tate [ l ] )}%.\
5950: 40 78 7b 5c 40 73 7b 31 36 2e 34 7d 20 5c 2e 7b  @x{\@s{16.4} \.{
5960: 5c 6c 61 6e 64 7d 20 73 65 6e 64 65 72 53 74 61  \land} senderSta
5970: 74 65 20 5c 2e 7b 3d 7d 20 53 5c 5f 44 6f 6e 65  te \.{=} S\_Done
5980: 7d 25 0a 5c 40 78 7b 5c 40 73 7b 31 36 2e 34 7d  }%.\@x{\@s{16.4}
5990: 20 5c 2e 7b 5c 6c 61 6e 64 7d 20 7b 5c 55 4e 43   \.{\land} {\UNC
59a0: 48 41 4e 47 45 44 7d 20 76 61 72 73 7d 25 0a 5c  HANGED} vars}%.\
59b0: 40 70 76 73 70 61 63 65 7b 38 2e 30 70 74 7d 25  @pvspace{8.0pt}%
59c0: 0a 20 5c 40 78 7b 20 4e 65 78 74 20 5c 2e 7b 5c  . \@x{ Next \.{\
59d0: 64 65 66 65 71 7d 20 5c 2e 7b 5c 6c 6f 72 7d 20  defeq} \.{\lor}
59e0: 5c 2e 7b 5c 6c 61 6e 64 7d 20 5c 2e 7b 5c 6c 6f  \.{\land} \.{\lo
59f0: 72 7d 20 53 74 61 72 74 50 72 6f 70 6f 73 61 6c  r} StartProposal
5a00: 50 68 61 73 65 20 28 20 53 65 6e 64 65 72 0a 20  Phase ( Sender.
5a10: 29 7d 25 0a 5c 40 78 7b 5c 40 73 7b 36 32 2e 30  )}%.\@x{\@s{62.0
5a20: 35 7d 20 5c 2e 7b 5c 6c 6f 72 7d 20 53 74 61 72  5} \.{\lor} Star
5a30: 74 50 72 65 70 61 72 61 74 69 6f 6e 50 68 61 73  tPreparationPhas
5a40: 65 20 28 20 53 65 6e 64 65 72 20 29 7d 25 0a 20  e ( Sender )}%.
5a50: 5c 40 78 7b 5c 40 73 7b 36 32 2e 30 35 7d 20 5c  \@x{\@s{62.05} \
5a60: 2e 7b 5c 6c 6f 72 7d 20 5c 45 5c 2c 20 6c 5c 40  .{\lor} \E\, l\@
5a70: 73 7b 35 2e 33 35 7d 20 5c 2e 7b 5c 69 6e 7d 20  s{5.35} \.{\in}
5a80: 4c 65 64 67 65 72 20 5c 2e 7b 3a 7d 20 4c 65 64  Ledger \.{:} Led
5a90: 67 65 72 41 62 6f 72 74 20 28 20 6c 0a 20 29 7d  gerAbort ( l. )}
5aa0: 25 0a 20 5c 40 78 7b 5c 40 73 7b 36 32 2e 30 35  %. \@x{\@s{62.05
5ab0: 7d 20 5c 2e 7b 5c 6c 6f 72 7d 20 5c 45 5c 2c 20  } \.{\lor} \E\,
5ac0: 6c 5c 40 73 7b 35 2e 33 35 7d 20 5c 2e 7b 5c 69  l\@s{5.35} \.{\i
5ad0: 6e 7d 20 4c 65 64 67 65 72 20 5c 2e 7b 3a 7d 20  n} Ledger \.{:}
5ae0: 4c 65 64 67 65 72 54 69 6d 65 6f 75 74 20 28 0a  LedgerTimeout (.
5af0: 20 6c 20 29 7d 25 0a 20 5c 40 78 7b 5c 40 73 7b   l )}%. \@x{\@s{
5b00: 36 32 2e 30 35 7d 20 5c 2e 7b 5c 6c 6f 72 7d 20  62.05} \.{\lor}
5b10: 5c 45 5c 2c 20 6d 20 5c 2e 7b 5c 69 6e 7d 20 7b  \E\, m \.{\in} {
5b20: 5c 44 4f 4d 41 49 4e 7d 20 6d 65 73 73 61 67 65  \DOMAIN} message
5b30: 73 20 5c 2e 7b 3a 7d 20 52 65 63 65 69 76 65 20  s \.{:} Receive
5b40: 28 20 6d 0a 20 29 7d 25 0a 5c 40 78 7b 5c 40 73  ( m. )}%.\@x{\@s
5b50: 7b 36 32 2e 30 35 7d 20 5c 2e 7b 5c 6c 6f 72 7d  {62.05} \.{\lor}
5b60: 20 4e 6f 74 68 69 6e 67 48 61 70 70 65 6e 73 7d   NothingHappens}
5b70: 25 0a 5c 40 78 7b 5c 40 73 7b 35 30 2e 39 34 7d  %.\@x{\@s{50.94}
5b80: 20 5c 2e 7b 5c 6c 61 6e 64 7d 20 63 6c 6f 63 6b   \.{\land} clock
5b90: 20 5c 2e 7b 27 7d 20 5c 2e 7b 3d 7d 20 63 6c 6f   \.{'} \.{=} clo
5ba0: 63 6b 20 5c 2e 7b 2b 7d 20 31 7d 25 0a 5c 40 78  ck \.{+} 1}%.\@x
5bb0: 7b 5c 40 73 7b 33 39 2e 38 33 7d 20 5c 2e 7b 5c  {\@s{39.83} \.{\
5bc0: 6c 6f 72 7d 20 54 65 72 6d 69 6e 61 74 69 6f 6e  lor} Termination
5bd0: 7d 25 0a 5c 40 70 76 73 70 61 63 65 7b 38 2e 30  }%.\@pvspace{8.0
5be0: 70 74 7d 25 0a 5c 40 78 7b 7d 25 0a 5c 40 79 7b  pt}%.\@x{}%.\@y{
5bf0: 5c 40 73 7b 30 7d 25 0a 20 54 68 65 20 73 70 65  \@s{0}%. The spe
5c00: 63 69 66 69 63 61 74 69 6f 6e 20 6d 75 73 74 20  cification must
5c10: 73 74 61 72 74 20 77 69 74 68 20 74 68 65 20 69  start with the i
5c20: 6e 69 74 69 61 6c 20 73 74 61 74 65 20 61 6e 64  nitial state and
5c30: 20 74 72 61 6e 73 69 74 69 6f 6e 20 61 63 63 6f   transition acco
5c40: 72 64 69 6e 67 0a 7d 25 0a 5c 40 78 78 7b 7d 25  rding.}%.\@xx{}%
5c50: 0a 5c 40 78 7b 7d 25 0a 5c 40 79 7b 5c 40 73 7b  .\@x{}%.\@y{\@s{
5c60: 30 7d 25 0a 20 74 6f 20 5c 65 6e 73 75 72 65 6d  0}%. to \ensurem
5c70: 61 74 68 7b 4e 65 78 74 7d 2e 0a 7d 25 0a 5c 40  ath{Next}..}%.\@
5c80: 78 78 7b 7d 25 0a 5c 40 78 7b 20 53 70 65 63 20  xx{}%.\@x{ Spec
5c90: 5c 2e 7b 5c 64 65 66 65 71 7d 20 49 6e 69 74 20  \.{\defeq} Init
5ca0: 5c 2e 7b 5c 6c 61 6e 64 7d 20 7b 5c 42 6f 78 7d  \.{\land} {\Box}
5cb0: 20 5b 20 4e 65 78 74 20 5d 5f 7b 20 76 61 72 73   [ Next ]_{ vars
5cc0: 7d 7d 25 0a 5c 40 70 76 73 70 61 63 65 7b 38 2e  }}%.\@pvspace{8.
5cd0: 30 70 74 7d 25 0a 5c 40 78 7b 7d 5c 62 6f 74 74  0pt}%.\@x{}\bott
5ce0: 6f 6d 62 61 72 5c 40 78 78 7b 7d 25 0a 5c 65 6e  ombar\@xx{}%.\en
5cf0: 64 7b 64 6f 63 75 6d 65 6e 74 7d                 d{document}