Hex Artifact Content
Not logged in

## Artifact d9ba2bc3327ec6457a70116ac81d38635c691691:

0000: 2d 2d 2d 2d 2d 2d 2d 2d 2d 2d 2d 2d 2d 2d 2d 2d  ----------------
0010: 2d 2d 2d 2d 2d 2d 2d 2d 2d 2d 2d 2d 2d 2d 2d 20  ---------------
0020: 4d 4f 44 55 4c 45 20 55 6e 69 76 65 72 73 61 6c  MODULE Universal
0030: 20 2d 2d 2d 2d 2d 2d 2d 2d 2d 2d 2d 2d 2d 2d 2d   ---------------
0040: 2d 2d 2d 2d 2d 2d 2d 2d 2d 2d 2d 2d 2d 2d 2d 2d  ----------------
0050: 0a 28 2a 2a 2a 2a 2a 2a 2a 2a 2a 2a 2a 2a 2a 2a  .(**************
0060: 2a 2a 2a 2a 2a 2a 2a 2a 2a 2a 2a 2a 2a 2a 2a 2a  ****************
0070: 2a 2a 2a 2a 2a 2a 2a 2a 2a 2a 2a 2a 2a 2a 2a 2a  ****************
0080: 2a 2a 2a 2a 2a 2a 2a 2a 2a 2a 2a 2a 2a 2a 2a 2a  ****************
0090: 2a 2a 2a 2a 2a 2a 2a 2a 2a 2a 2a 2a 2a 29 0a 28  *************).(
00a0: 2a 20 46 6f 72 6d 61 6c 20 53 70 65 63 69 66 69  * Formal Specifi
00b0: 63 61 74 69 6f 6e 20 69 6e 20 54 4c 41 5e 2b 20  cation in TLA^+
00c0: 6f 66 20 74 68 65 20 20 20 20 20 20 20 20 20 20  of the
00d0: 20 20 20 20 20 20 20 20 20 20 20 20 20 20 20 20
00e0: 20 20 20 20 20 20 20 20 20 20 2a 29 0a 28 2a 20            *).(*
00f0: 49 6e 74 65 72 6c 65 64 67 65 72 20 50 72 6f 74  Interledger Prot
0100: 6f 63 6f 6c 20 55 6e 69 76 65 72 73 61 6c 20 28  ocol Universal (
0110: 49 4c 50 2f 55 29 20 20 20 20 20 20 20 20 20 20  ILP/U)
0120: 20 20 20 20 20 20 20 20 20 20 20 20 20 20 20 20
0130: 20 20 20 20 20 20 20 20 2a 29 0a 28 2a 20 20 20          *).(*
0140: 20 20 20 20 20 20 20 20 20 20 20 20 20 20 20 20
0150: 20 20 20 20 20 20 20 20 20 20 20 20 20 20 20 20
0160: 20 20 20 20 20 20 20 20 20 20 20 20 20 20 20 20
0170: 20 20 20 20 20 20 20 20 20 20 20 20 20 20 20 20
0180: 20 20 20 20 20 20 2a 29 0a 28 2a 60 2e 20 20 20        *).(*.
0190: 20 20 20 20 20 20 20 20 20 20 20 20 20 20 20 20
01a0: 20 20 20 20 20 20 20 20 20 20 20 20 20 20 20 20
01b0: 20 20 20 20 20 20 20 20 20 20 20 20 20 20 20 20
01c0: 20 20 20 20 20 20 20 20 20 20 20 20 20 20 20 20
01d0: 20 20 20 20 2a 29 0a 28 2a 20 4d 6f 64 65 6c 65      *).(* Modele
01e0: 64 20 61 66 74 65 72 20 74 68 65 20 65 78 63 65  d after the exce
01f0: 6c 6c 65 6e 74 20 52 61 66 74 20 73 70 65 63 69  llent Raft speci
0200: 66 69 63 61 74 69 6f 6e 20 62 79 20 44 69 65 67  fication by Dieg
0210: 6f 20 4f 6e 67 61 72 6f 2e 20 20 20 20 20 20 20  o Ongaro.
0220: 20 20 2a 29 0a 28 2a 20 20 20 41 76 61 69 6c 61    *).(*   Availa
0230: 62 6c 65 20 61 74 20 68 74 74 70 73 3a 2f 2f 67  ble at https://g
0240: 69 74 68 75 62 2e 63 6f 6d 2f 6f 6e 67 61 72 64  ithub.com/ongard
0250: 69 65 2f 72 61 66 74 2e 74 6c 61 20 20 20 20 20  ie/raft.tla
0260: 20 20 20 20 20 20 20 20 20 20 20 20 20 20 20 20
0270: 2a 29 0a 28 2a 20 20 20 20 20 20 20 20 20 20 20  *).(*
0280: 20 20 20 20 20 20 20 20 20 20 20 20 20 20 20 20
0290: 20 20 20 20 20 20 20 20 20 20 20 20 20 20 20 20
02a0: 20 20 20 20 20 20 20 20 20 20 20 20 20 20 20 20
02b0: 20 20 20 20 20 20 20 20 20 20 20 20 20 20 2a 29                *)
02c0: 0a 28 2a 20 20 20 43 6f 70 79 72 69 67 68 74 20  .(*   Copyright
02d0: 32 30 31 34 20 44 69 65 67 6f 20 4f 6e 67 61 72  2014 Diego Ongar
02e0: 6f 2e 20 20 20 20 20 20 20 20 20 20 20 20 20 20  o.
02f0: 20 20 20 20 20 20 20 20 20 20 20 20 20 20 20 20
0300: 20 20 20 20 20 20 20 20 20 20 20 20 2a 29 0a 28              *).(
0310: 2a 20 20 20 54 68 69 73 20 77 6f 72 6b 20 69 73  *   This work is
0320: 20 6c 69 63 65 6e 73 65 64 20 75 6e 64 65 72 20   licensed under
0330: 74 68 65 20 43 72 65 61 74 69 76 65 20 43 6f 6d  the Creative Com
0340: 6d 6f 6e 73 20 41 74 74 72 69 62 75 74 69 6f 6e  mons Attribution
0350: 2d 34 2e 30 20 20 20 20 20 20 2a 29 0a 28 2a 20  -4.0      *).(*
0360: 20 20 49 6e 74 65 72 6e 61 74 69 6f 6e 61 6c 20    International
0370: 4c 69 63 65 6e 73 65 20 68 74 74 70 73 3a 2f 2f  License https://
0380: 63 72 65 61 74 69 76 65 63 6f 6d 6d 6f 6e 73 2e  creativecommons.
0390: 6f 72 67 2f 6c 69 63 65 6e 73 65 73 2f 62 79 2f  org/licenses/by/
03a0: 34 2e 30 2f 20 20 2e 27 2a 29 0a 28 2a 2a 2a 2a  4.0/  .'*).(****
03b0: 2a 2a 2a 2a 2a 2a 2a 2a 2a 2a 2a 2a 2a 2a 2a 2a  ****************
03c0: 2a 2a 2a 2a 2a 2a 2a 2a 2a 2a 2a 2a 2a 2a 2a 2a  ****************
03d0: 2a 2a 2a 2a 2a 2a 2a 2a 2a 2a 2a 2a 2a 2a 2a 2a  ****************
03e0: 2a 2a 2a 2a 2a 2a 2a 2a 2a 2a 2a 2a 2a 2a 2a 2a  ****************
03f0: 2a 2a 2a 2a 2a 2a 2a 29 0a 0a 45 58 54 45 4e 44  *******)..EXTEND
0400: 53 20 4e 61 74 75 72 61 6c 73 2c 20 53 65 71 75  S Naturals, Sequ
0410: 65 6e 63 65 73 2c 20 46 69 6e 69 74 65 53 65 74  ences, FiniteSet
0420: 73 2c 20 42 61 67 73 2c 20 54 4c 43 0a 0a 5c 2a  s, Bags, TLC..\*
0430: 20 54 68 65 20 73 65 74 20 6f 66 20 6c 65 64 67   The set of ledg
0440: 65 72 20 49 44 73 0a 43 4f 4e 53 54 41 4e 54 53  er IDs.CONSTANTS
0450: 20 4c 65 64 67 65 72 0a 0a 5c 2a 20 54 68 65 20   Ledger..\* The
0460: 73 65 74 20 6f 66 20 70 61 72 74 69 63 69 70 61  set of participa
0470: 6e 74 20 49 44 73 0a 43 4f 4e 53 54 41 4e 54 53  nt IDs.CONSTANTS
0480: 20 50 61 72 74 69 63 69 70 61 6e 74 0a 0a 5c 2a   Participant..\*
0490: 20 53 65 6e 64 65 72 20 73 74 61 74 65 73 0a 43   Sender states.C
04a0: 4f 4e 53 54 41 4e 54 53 20 53 5f 52 65 61 64 79  ONSTANTS S_Ready
04b0: 2c 20 53 5f 50 72 6f 70 6f 73 61 6c 57 61 69 74  , S_ProposalWait
04c0: 69 6e 67 2c 20 53 5f 57 61 69 74 69 6e 67 2c 20  ing, S_Waiting,
04d0: 53 5f 44 6f 6e 65 0a 0a 5c 2a 20 43 6f 6e 6e 65  S_Done..\* Conne
04e0: 63 74 6f 72 20 73 74 61 74 65 73 0a 43 4f 4e 53  ctor states.CONS
04f0: 54 41 4e 54 53 20 43 5f 52 65 61 64 79 2c 20 43  TANTS C_Ready, C
0500: 5f 50 72 6f 70 6f 73 65 64 0a 0a 5c 2a 20 4c 65  _Proposed..\* Le
0510: 64 67 65 72 20 73 74 61 74 65 73 0a 43 4f 4e 53  dger states.CONS
0520: 54 41 4e 54 53 20 4c 5f 50 72 6f 70 6f 73 65 64  TANTS L_Proposed
0530: 2c 20 4c 5f 50 72 65 70 61 72 65 64 2c 20 4c 5f  , L_Prepared, L_
0540: 45 78 65 63 75 74 65 64 2c 20 4c 5f 41 62 6f 72  Executed, L_Abor
0550: 74 65 64 0a 0a 5c 2a 20 4d 65 73 73 61 67 65 20  ted..\* Message
0560: 74 79 70 65 73 0a 43 4f 4e 53 54 41 4e 54 53 20  types.CONSTANTS
0570: 50 72 65 70 61 72 65 52 65 71 75 65 73 74 2c 20  PrepareRequest,
0580: 45 78 65 63 75 74 65 52 65 71 75 65 73 74 2c 20  ExecuteRequest,
0590: 41 62 6f 72 74 52 65 71 75 65 73 74 2c 0a 20 20  AbortRequest,.
05a0: 20 20 20 20 20 20 20 20 50 72 65 70 61 72 65 4e          PrepareN
05b0: 6f 74 69 66 79 2c 20 45 78 65 63 75 74 65 4e 6f  otify, ExecuteNo
05c0: 74 69 66 79 2c 20 41 62 6f 72 74 4e 6f 74 69 66  tify, AbortNotif
05d0: 79 2c 0a 20 20 20 20 20 20 20 20 20 20 53 75 62  y,.          Sub
05e0: 70 61 79 6d 65 6e 74 50 72 6f 70 6f 73 61 6c 52  paymentProposalR
05f0: 65 71 75 65 73 74 2c 20 53 75 62 70 61 79 6d 65  equest, Subpayme
0600: 6e 74 50 72 6f 70 6f 73 61 6c 52 65 73 70 6f 6e  ntProposalRespon
0610: 73 65 0a 0a 5c 2a 20 52 65 63 65 69 70 74 20 73  se..\* Receipt s
0620: 69 67 6e 61 74 75 72 65 0a 43 4f 4e 53 54 41 4e  ignature.CONSTAN
0630: 54 53 20 52 5f 52 65 63 65 69 70 74 53 69 67 6e  TS R_ReceiptSign
0640: 61 74 75 72 65 0a 0a 2d 2d 2d 2d 0a 5c 2a 20 47  ature..----.\* G
0650: 6c 6f 62 61 6c 20 76 61 72 69 61 62 6c 65 73 0a  lobal variables.
0660: 0a 5c 2a 20 55 6e 64 65 72 20 73 79 6e 63 68 72  .\* Under synchr
0670: 6f 6e 79 20 77 65 20 61 72 65 20 61 6c 6c 6f 77  ony we are allow
0680: 65 64 20 74 6f 20 68 61 76 65 20 61 20 67 6c 6f  ed to have a glo
0690: 62 61 6c 20 63 6c 6f 63 6b 0a 56 41 52 49 41 42  bal clock.VARIAB
06a0: 4c 45 20 63 6c 6f 63 6b 0a 0a 5c 2a 20 41 20 62  LE clock..\* A b
06b0: 61 67 20 6f 66 20 72 65 63 6f 72 64 73 20 72 65  ag of records re
06c0: 70 72 65 73 65 6e 74 69 6e 67 20 72 65 71 75 65  presenting reque
06d0: 73 74 73 20 61 6e 64 20 72 65 73 70 6f 6e 73 65  sts and response
06e0: 73 20 73 65 6e 74 20 66 72 6f 6d 20 6f 6e 65 20  s sent from one
06f0: 70 72 6f 63 65 73 73 0a 5c 2a 20 74 6f 20 61 6e  process.\* to an
0700: 6f 74 68 65 72 0a 56 41 52 49 41 42 4c 45 20 6d  other.VARIABLE m
0710: 65 73 73 61 67 65 73 0a 0a 2d 2d 2d 2d 0a 5c 2a  essages..----.\*
0720: 20 53 65 6e 64 65 72 20 76 61 72 69 61 62 6c 65   Sender variable
0730: 73 0a 0a 5c 2a 20 53 74 61 74 65 20 6f 66 20 74  s..\* State of t
0740: 68 65 20 73 65 6e 64 65 72 20 28 53 5f 52 65 61  he sender (S_Rea
0750: 64 79 2c 20 53 5f 57 61 69 74 69 6e 67 2c 20 53  dy, S_Waiting, S
0760: 5f 44 6f 6e 65 29 0a 56 41 52 49 41 42 4c 45 20  _Done).VARIABLE
0770: 73 65 6e 64 65 72 53 74 61 74 65 0a 0a 5c 2a 20  senderState..\*
0780: 57 68 65 74 68 65 72 20 74 68 65 20 73 65 6e 64  Whether the send
0790: 65 72 20 68 61 73 20 72 65 63 65 69 76 65 64 20  er has received
07a0: 61 20 72 65 73 70 6f 6e 73 65 20 66 72 6f 6d 20  a response from
07b0: 61 20 67 69 76 65 6e 20 63 6f 6e 6e 65 63 74 6f  a given connecto
07c0: 72 0a 56 41 52 49 41 42 4c 45 20 73 65 6e 64 65  r.VARIABLE sende
07d0: 72 50 72 6f 70 6f 73 61 6c 52 65 73 70 6f 6e 73  rProposalRespons
07e0: 65 73 0a 0a 5c 2a 20 41 6c 6c 20 73 65 6e 64 65  es..\* All sende
07f0: 72 20 76 61 72 69 61 62 6c 65 73 0a 73 65 6e 64  r variables.send
0800: 65 72 56 61 72 73 20 3d 3d 20 3c 3c 73 65 6e 64  erVars == <<send
0810: 65 72 53 74 61 74 65 2c 20 73 65 6e 64 65 72 50  erState, senderP
0820: 72 6f 70 6f 73 61 6c 52 65 73 70 6f 6e 73 65 73  roposalResponses
0830: 3e 3e 0a 2d 2d 2d 2d 0a 5c 2a 20 43 6f 6e 6e 65  >>.----.\* Conne
0840: 63 74 6f 72 20 76 61 72 69 61 62 6c 65 73 0a 0a  ctor variables..
0850: 5c 2a 20 53 74 61 74 65 20 6f 66 20 74 68 65 20  \* State of the
0860: 63 6f 6e 6e 65 63 74 6f 72 20 28 43 5f 52 65 61  connector (C_Rea
0870: 64 79 2c 20 43 5f 50 72 6f 70 6f 73 65 64 29 0a  dy, C_Proposed).
0880: 56 41 52 49 41 42 4c 45 20 63 6f 6e 6e 65 63 74  VARIABLE connect
0890: 6f 72 53 74 61 74 65 0a 0a 5c 2a 20 41 6c 6c 20  orState..\* All
08a0: 73 65 6e 64 65 72 20 76 61 72 69 61 62 6c 65 73  sender variables
08b0: 0a 63 6f 6e 6e 65 63 74 6f 72 56 61 72 73 20 3d  .connectorVars =
08c0: 3d 20 3c 3c 63 6f 6e 6e 65 63 74 6f 72 53 74 61  = <<connectorSta
08d0: 74 65 3e 3e 0a 2d 2d 2d 2d 0a 5c 2a 20 54 68 65  te>>.----.\* The
08e0: 20 66 6f 6c 6c 6f 77 69 6e 67 20 76 61 72 69 61   following varia
08f0: 62 6c 65 73 20 61 72 65 20 61 6c 6c 20 70 65 72  bles are all per
0900: 20 6c 65 64 67 65 72 20 28 66 75 6e 63 74 69 6f   ledger (functio
0910: 6e 73 20 77 69 74 68 20 64 6f 6d 61 69 6e 20 4c  ns with domain L
0920: 65 64 67 65 72 29 0a 0a 5c 2a 20 54 68 65 20 6c  edger)..\* The l
0930: 65 64 67 65 72 20 73 74 61 74 65 20 28 4c 5f 50  edger state (L_P
0940: 72 6f 70 6f 73 65 64 2c 20 4c 5f 50 72 65 70 61  roposed, L_Prepa
0950: 72 65 64 2c 20 4c 5f 45 78 65 63 75 74 65 64 20  red, L_Executed
0960: 6f 72 20 4c 5f 41 62 6f 72 74 65 64 29 0a 56 41  or L_Aborted).VA
0970: 52 49 41 42 4c 45 20 6c 65 64 67 65 72 53 74 61  RIABLE ledgerSta
0980: 74 65 0a 0a 5c 2a 20 54 68 65 20 74 69 6d 65 6f  te..\* The timeo
0990: 75 74 73 20 66 6f 72 20 65 61 63 68 20 6f 66 20  uts for each of
09a0: 74 68 65 20 74 68 65 20 74 72 61 6e 73 66 65 72  the the transfer
09b0: 73 0a 56 41 52 49 41 42 4c 45 20 6c 65 64 67 65  s.VARIABLE ledge
09c0: 72 45 78 70 69 72 61 74 69 6f 6e 0a 0a 5c 2a 20  rExpiration..\*
09d0: 41 6c 6c 20 6c 65 64 67 65 72 20 76 61 72 69 61  All ledger varia
09e0: 62 6c 65 73 0a 6c 65 64 67 65 72 56 61 72 73 20  bles.ledgerVars
09f0: 3d 3d 20 3c 3c 6c 65 64 67 65 72 53 74 61 74 65  == <<ledgerState
0a00: 2c 20 6c 65 64 67 65 72 45 78 70 69 72 61 74 69  , ledgerExpirati
0a10: 6f 6e 3e 3e 0a 2d 2d 2d 2d 0a 0a 5c 2a 20 41 6c  on>>.----..\* Al
0a20: 6c 20 76 61 72 69 61 62 6c 65 73 3b 20 75 73 65  l variables; use
0a30: 64 20 66 6f 72 20 73 74 75 74 74 65 72 69 6e 67  d for stuttering
0a40: 20 28 61 73 73 65 72 74 69 6e 67 20 73 74 61 74   (asserting stat
0a50: 65 20 68 61 73 6e 27 74 20 63 68 61 6e 67 65 64  e hasn't changed
0a60: 29 0a 76 61 72 73 20 3d 3d 20 3c 3c 63 6c 6f 63  ).vars == <<cloc
0a70: 6b 2c 20 6d 65 73 73 61 67 65 73 2c 20 73 65 6e  k, messages, sen
0a80: 64 65 72 56 61 72 73 2c 20 63 6f 6e 6e 65 63 74  derVars, connect
0a90: 6f 72 56 61 72 73 2c 20 6c 65 64 67 65 72 56 61  orVars, ledgerVa
0aa0: 72 73 3e 3e 0a 0a 2d 2d 2d 2d 0a 5c 2a 20 48 65  rs>>..----.\* He
0ab0: 6c 70 65 72 73 0a 0a 5c 2a 20 41 64 64 20 61 20  lpers..\* Add a
0ac0: 73 65 74 20 6f 66 20 6e 65 77 20 6d 65 73 73 61  set of new messa
0ad0: 67 65 73 20 69 6e 20 74 72 61 6e 73 69 74 0a 42  ges in transit.B
0ae0: 72 6f 61 64 63 61 73 74 28 6d 29 20 3d 3d 20 6d  roadcast(m) == m
0af0: 65 73 73 61 67 65 73 27 20 3d 20 6d 65 73 73 61  essages' = messa
0b00: 67 65 73 20 28 2b 29 20 53 65 74 54 6f 42 61 67  ges (+) SetToBag
0b10: 28 6d 29 0a 0a 5c 2a 20 41 64 64 20 61 20 6d 65  (m)..\* Add a me
0b20: 73 73 61 67 65 20 74 6f 20 74 68 65 20 62 61 67  ssage to the bag
0b30: 20 6f 66 20 6d 65 73 73 61 67 65 73 0a 53 65 6e   of messages.Sen
0b40: 64 28 6d 29 20 3d 3d 20 42 72 6f 61 64 63 61 73  d(m) == Broadcas
0b50: 74 28 7b 6d 7d 29 0a 0a 5c 2a 20 52 65 6d 6f 76  t({m})..\* Remov
0b60: 65 20 61 20 6d 65 73 73 61 67 65 20 66 72 6f 6d  e a message from
0b70: 20 74 68 65 20 62 61 67 20 6f 66 20 6d 65 73 73   the bag of mess
0b80: 61 67 65 73 2e 20 55 73 65 64 20 77 68 65 6e 20  ages. Used when
0b90: 61 20 70 72 6f 63 65 73 73 20 69 73 20 64 6f 6e  a process is don
0ba0: 65 0a 5c 2a 20 70 72 6f 63 65 73 73 69 6e 67 20  e.\* processing
0bb0: 61 20 6d 65 73 73 61 67 65 2e 0a 44 69 73 63 61  a message..Disca
0bc0: 72 64 28 6d 29 20 3d 3d 20 6d 65 73 73 61 67 65  rd(m) == message
0bd0: 73 27 20 3d 20 6d 65 73 73 61 67 65 73 20 28 2d  s' = messages (-
0be0: 29 20 53 65 74 54 6f 42 61 67 28 7b 6d 7d 29 0a  ) SetToBag({m}).
0bf0: 0a 5c 2a 20 52 65 73 70 6f 6e 64 20 74 6f 20 61  .\* Respond to a
0c00: 20 6d 65 73 73 61 67 65 20 62 79 20 73 65 6e 64   message by send
0c10: 69 6e 67 20 6d 75 6c 74 69 70 6c 65 20 6d 65 73  ing multiple mes
0c20: 73 61 67 65 73 0a 52 65 70 6c 79 42 72 6f 61 64  sages.ReplyBroad
0c30: 63 61 73 74 28 72 65 73 70 6f 6e 73 65 73 2c 20  cast(responses,
0c40: 72 65 71 75 65 73 74 29 20 3d 3d 0a 20 20 20 20  request) ==.
0c50: 6d 65 73 73 61 67 65 73 27 20 3d 20 6d 65 73 73  messages' = mess
0c60: 61 67 65 73 20 28 2d 29 20 53 65 74 54 6f 42 61  ages (-) SetToBa
0c70: 67 28 7b 72 65 71 75 65 73 74 7d 29 20 28 2b 29  g({request}) (+)
0c80: 20 53 65 74 54 6f 42 61 67 28 72 65 73 70 6f 6e   SetToBag(respon
0c90: 73 65 73 29 0a 0a 5c 2a 20 43 6f 6d 62 69 6e 61  ses)..\* Combina
0ca0: 74 69 6f 6e 20 6f 66 20 53 65 6e 64 20 61 6e 64  tion of Send and
0cb0: 20 44 69 73 63 61 72 64 0a 52 65 70 6c 79 28 72   Discard.Reply(r
0cc0: 65 73 70 6f 6e 73 65 2c 20 72 65 71 75 65 73 74  esponse, request
0cd0: 29 20 3d 3d 0a 20 20 20 20 52 65 70 6c 79 42 72  ) ==.    ReplyBr
0ce0: 6f 61 64 63 61 73 74 28 7b 72 65 73 70 6f 6e 73  oadcast({respons
0cf0: 65 7d 2c 20 72 65 71 75 65 73 74 29 0a 0a 0a 5c  e}, request)...\
0d00: 2a 20 52 65 74 75 72 6e 20 74 68 65 20 6d 69 6e  * Return the min
0d10: 69 6d 75 6d 20 76 61 6c 75 65 20 66 72 6f 6d 20  imum value from
0d20: 61 20 73 65 74 2c 20 6f 72 20 75 6e 64 65 66 69  a set, or undefi
0d30: 6e 65 64 20 69 66 20 74 68 65 20 73 65 74 20 69  ned if the set i
0d40: 73 20 65 6d 70 74 79 2e 0a 4d 69 6e 28 73 29 20  s empty..Min(s)
0d50: 3d 3d 20 43 48 4f 4f 53 45 20 78 20 5c 69 6e 20  == CHOOSE x \in
0d60: 73 20 3a 20 5c 41 20 79 20 5c 69 6e 20 73 20 3a  s : \A y \in s :
0d70: 20 78 20 3c 3d 20 79 0a 5c 2a 20 52 65 74 75 72   x <= y.\* Retur
0d80: 6e 20 74 68 65 20 6d 61 78 69 6d 75 6d 20 76 61  n the maximum va
0d90: 6c 75 65 20 66 72 6f 6d 20 61 20 73 65 74 2c 20  lue from a set,
0da0: 6f 72 20 75 6e 64 65 66 69 6e 65 64 20 69 66 20  or undefined if
0db0: 74 68 65 20 73 65 74 20 69 73 20 65 6d 70 74 79  the set is empty
0dc0: 2e 0a 4d 61 78 28 73 29 20 3d 3d 20 43 48 4f 4f  ..Max(s) == CHOO
0dd0: 53 45 20 78 20 5c 69 6e 20 73 20 3a 20 5c 41 20  SE x \in s : \A
0de0: 79 20 5c 69 6e 20 73 20 3a 20 78 20 3e 3d 20 79  y \in s : x >= y
0df0: 0a 0a 5c 2a 20 49 73 20 61 20 66 69 6e 61 6c 20  ..\* Is a final
0e00: 6c 65 64 67 65 72 20 73 74 61 74 65 0a 49 73 46  ledger state.IsF
0e10: 69 6e 61 6c 4c 65 64 67 65 72 53 74 61 74 65 28  inalLedgerState(
0e20: 69 29 20 3d 3d 20 69 20 5c 69 6e 20 7b 4c 5f 45  i) == i \in {L_E
0e30: 78 65 63 75 74 65 64 2c 20 4c 5f 41 62 6f 72 74  xecuted, L_Abort
0e40: 65 64 7d 0a 0a 5c 2a 20 53 65 6e 64 65 72 0a 53  ed}..\* Sender.S
0e50: 65 6e 64 65 72 20 3d 3d 20 4d 69 6e 28 50 61 72  ender == Min(Par
0e60: 74 69 63 69 70 61 6e 74 29 0a 0a 5c 2a 20 52 65  ticipant)..\* Re
0e70: 63 69 70 69 65 6e 74 0a 52 65 63 69 70 69 65 6e  cipient.Recipien
0e80: 74 20 3d 3d 20 4d 61 78 28 50 61 72 74 69 63 69  t == Max(Partici
0e90: 70 61 6e 74 29 0a 0a 5c 2a 20 53 65 74 20 6f 66  pant)..\* Set of
0ea0: 20 63 6f 6e 6e 65 63 74 6f 72 73 0a 43 6f 6e 6e   connectors.Conn
0eb0: 65 63 74 6f 72 20 3d 3d 20 50 61 72 74 69 63 69  ector == Partici
0ec0: 70 61 6e 74 20 5c 20 7b 53 65 6e 64 65 72 2c 20  pant \ {Sender,
0ed0: 52 65 63 69 70 69 65 6e 74 7d 0a 0a 5c 2a 20 54  Recipient}..\* T
0ee0: 68 65 20 63 6c 6f 63 6b 20 76 61 6c 75 65 20 77  he clock value w
0ef0: 65 20 65 78 70 65 63 74 20 74 6f 20 62 65 20 61  e expect to be a
0f00: 74 20 61 66 74 65 72 20 74 68 65 20 70 72 6f 70  t after the prop
0f10: 6f 73 61 6c 20 70 68 61 73 65 0a 43 6c 6f 63 6b  osal phase.Clock
0f20: 41 66 74 65 72 50 72 6f 70 6f 73 61 6c 20 3d 3d  AfterProposal ==
0f30: 20 32 20 2a 20 43 61 72 64 69 6e 61 6c 69 74 79   2 * Cardinality
0f40: 28 43 6f 6e 6e 65 63 74 6f 72 29 20 2b 20 32 0a  (Connector) + 2.
0f50: 0a 5c 2a 20 54 68 65 20 63 6c 6f 63 6b 20 76 61  .\* The clock va
0f60: 6c 75 65 20 77 65 20 65 78 70 65 63 74 20 61 66  lue we expect af
0f70: 74 65 72 20 74 68 65 20 70 72 65 70 61 72 61 74  ter the preparat
0f80: 69 6f 6e 20 70 68 61 73 65 0a 43 6c 6f 63 6b 41  ion phase.ClockA
0f90: 66 74 65 72 50 72 65 70 61 72 65 20 3d 3d 20 43  fterPrepare == C
0fa0: 6c 6f 63 6b 41 66 74 65 72 50 72 6f 70 6f 73 61  lockAfterProposa
0fb0: 6c 20 2b 20 32 20 2a 20 43 61 72 64 69 6e 61 6c  l + 2 * Cardinal
0fc0: 69 74 79 28 4c 65 64 67 65 72 29 20 2b 20 31 0a  ity(Ledger) + 1.
0fd0: 0a 5c 2a 20 54 68 65 20 63 6c 6f 63 6b 20 76 61  .\* The clock va
0fe0: 6c 75 65 20 77 65 20 65 78 70 65 63 74 20 74 6f  lue we expect to
0ff0: 20 62 65 20 61 74 20 61 66 74 65 72 20 74 68 65   be at after the
1000: 20 65 78 65 63 75 74 69 6f 6e 20 70 68 61 73 65   execution phase
1010: 0a 43 6c 6f 63 6b 41 66 74 65 72 45 78 65 63 75  .ClockAfterExecu
1020: 74 69 6f 6e 20 3d 3d 20 43 6c 6f 63 6b 41 66 74  tion == ClockAft
1030: 65 72 50 72 65 70 61 72 65 20 2b 20 32 20 2a 20  erPrepare + 2 *
1040: 43 61 72 64 69 6e 61 6c 69 74 79 28 4c 65 64 67  Cardinality(Ledg
1050: 65 72 29 20 2b 20 31 0a 2d 2d 2d 2d 0a 5c 2a 20  er) + 1.----.\*
1060: 44 65 66 69 6e 65 20 74 79 70 65 20 73 70 65 63  Define type spec
1070: 69 66 69 63 61 74 69 6f 6e 20 66 6f 72 20 61 6c  ification for al
1080: 6c 20 76 61 72 69 61 62 6c 65 73 0a 0a 54 79 70  l variables..Typ
1090: 65 4f 4b 20 3d 3d 20 2f 5c 20 63 6c 6f 63 6b 20  eOK == /\ clock
10a0: 5c 69 6e 20 4e 61 74 0a 20 20 20 20 20 20 20 20  \in Nat.
10b0: 20 20 2f 5c 20 49 73 41 42 61 67 28 6d 65 73 73    /\ IsABag(mess
10c0: 61 67 65 73 29 0a 20 20 20 20 20 20 20 20 20 20  ages).
10d0: 2f 5c 20 73 65 6e 64 65 72 53 74 61 74 65 20 5c  /\ senderState \
10e0: 69 6e 20 7b 53 5f 52 65 61 64 79 2c 20 53 5f 50  in {S_Ready, S_P
10f0: 72 6f 70 6f 73 61 6c 57 61 69 74 69 6e 67 2c 20  roposalWaiting,
1100: 53 5f 57 61 69 74 69 6e 67 2c 20 53 5f 44 6f 6e  S_Waiting, S_Don
1110: 65 7d 0a 20 20 20 20 20 20 20 20 20 20 2f 5c 20  e}.          /\
1120: 73 65 6e 64 65 72 50 72 6f 70 6f 73 61 6c 52 65  senderProposalRe
1130: 73 70 6f 6e 73 65 73 20 5c 69 6e 20 5b 43 6f 6e  sponses \in [Con
1140: 6e 65 63 74 6f 72 20 2d 3e 20 42 4f 4f 4c 45 41  nector -> BOOLEA
1150: 4e 5d 0a 20 20 20 20 20 20 20 20 20 20 2f 5c 20  N].          /\
1160: 63 6f 6e 6e 65 63 74 6f 72 53 74 61 74 65 20 5c  connectorState \
1170: 69 6e 20 5b 43 6f 6e 6e 65 63 74 6f 72 20 2d 3e  in [Connector ->
1180: 20 7b 43 5f 52 65 61 64 79 2c 20 43 5f 50 72 6f   {C_Ready, C_Pro
1190: 70 6f 73 65 64 7d 5d 20 0a 20 20 20 20 20 20 20  posed}] .
11a0: 20 20 20 2f 5c 20 6c 65 64 67 65 72 53 74 61 74     /\ ledgerStat
11b0: 65 20 5c 69 6e 20 5b 4c 65 64 67 65 72 20 2d 3e  e \in [Ledger ->
11c0: 20 7b 4c 5f 50 72 6f 70 6f 73 65 64 2c 20 4c 5f   {L_Proposed, L_
11d0: 50 72 65 70 61 72 65 64 2c 20 4c 5f 45 78 65 63  Prepared, L_Exec
11e0: 75 74 65 64 2c 20 4c 5f 41 62 6f 72 74 65 64 7d  uted, L_Aborted}
11f0: 5d 0a 20 20 20 20 20 20 20 20 20 20 2f 5c 20 6c  ].          /\ l
1200: 65 64 67 65 72 45 78 70 69 72 61 74 69 6f 6e 20  edgerExpiration
1210: 5c 69 6e 20 5b 4c 65 64 67 65 72 20 2d 3e 20 4e  \in [Ledger -> N
1220: 61 74 5d 0a 0a 43 6f 6e 73 69 73 74 65 6e 63 79  at]..Consistency
1230: 20 3d 3d 0a 20 20 20 20 5c 41 20 6c 31 2c 20 6c   ==.    \A l1, l
1240: 32 20 5c 69 6e 20 4c 65 64 67 65 72 20 3a 20 5c  2 \in Ledger : \
1250: 6c 6e 6f 74 20 2f 5c 20 6c 65 64 67 65 72 53 74  lnot /\ ledgerSt
1260: 61 74 65 5b 6c 31 5d 20 3d 20 4c 5f 41 62 6f 72  ate[l1] = L_Abor
1270: 74 65 64 0a 20 20 20 20 20 20 20 20 20 20 20 20  ted.
1280: 20 20 20 20 20 20 20 20 20 20 20 20 20 20 20 20
1290: 20 20 20 20 20 2f 5c 20 6c 65 64 67 65 72 53 74       /\ ledgerSt
12a0: 61 74 65 5b 6c 32 5d 20 3d 20 4c 5f 45 78 65 63  ate[l2] = L_Exec
12b0: 75 74 65 64 0a 0a 49 6e 76 20 3d 3d 20 2f 5c 20  uted..Inv == /\
12c0: 54 79 70 65 4f 4b 0a 20 20 20 20 20 20 20 2f 5c  TypeOK.       /\
12d0: 20 43 6f 6e 73 69 73 74 65 6e 63 79 0a 0a 2d 2d   Consistency..--
12e0: 2d 2d 0a 5c 2a 20 44 65 66 69 6e 65 20 69 6e 69  --.\* Define ini
12f0: 74 69 61 6c 20 76 61 6c 75 65 73 20 66 6f 72 20  tial values for
1300: 61 6c 6c 20 76 61 72 69 61 62 6c 65 73 0a 0a 49  all variables..I
1310: 6e 69 74 53 65 6e 64 65 72 56 61 72 73 20 3d 3d  nitSenderVars ==
1320: 20 2f 5c 20 73 65 6e 64 65 72 53 74 61 74 65 20   /\ senderState
1330: 3d 20 53 5f 52 65 61 64 79 0a 20 20 20 20 20 20  = S_Ready.
1340: 20 20 20 20 20 20 20 20 20 20 20 20 2f 5c 20 73              /\ s
1350: 65 6e 64 65 72 50 72 6f 70 6f 73 61 6c 52 65 73  enderProposalRes
1360: 70 6f 6e 73 65 73 20 3d 20 5b 69 20 5c 69 6e 20  ponses = [i \in
1370: 43 6f 6e 6e 65 63 74 6f 72 20 7c 2d 3e 20 46 41  Connector |-> FA
1380: 4c 53 45 5d 0a 0a 49 6e 69 74 43 6f 6e 6e 65 63  LSE]..InitConnec
1390: 74 6f 72 56 61 72 73 20 3d 3d 20 63 6f 6e 6e 65  torVars == conne
13a0: 63 74 6f 72 53 74 61 74 65 20 3d 20 5b 69 20 5c  ctorState = [i \
13b0: 69 6e 20 43 6f 6e 6e 65 63 74 6f 72 20 7c 2d 3e  in Connector |->
13c0: 20 43 5f 52 65 61 64 79 5d 0a 0a 49 6e 69 74 4c   C_Ready]..InitL
13d0: 65 64 67 65 72 56 61 72 73 20 3d 3d 20 2f 5c 20  edgerVars == /\
13e0: 6c 65 64 67 65 72 53 74 61 74 65 20 3d 20 5b 69  ledgerState = [i
13f0: 20 5c 69 6e 20 4c 65 64 67 65 72 20 7c 2d 3e 20   \in Ledger |->
1400: 4c 5f 50 72 6f 70 6f 73 65 64 5d 0a 20 20 20 20  L_Proposed].
1410: 20 20 20 20 20 20 20 20 20 20 20 20 20 20 2f 5c                /\
1420: 20 6c 65 64 67 65 72 45 78 70 69 72 61 74 69 6f   ledgerExpiratio
1430: 6e 20 3d 20 5b 69 20 5c 69 6e 20 4c 65 64 67 65  n = [i \in Ledge
1440: 72 20 7c 2d 3e 20 43 6c 6f 63 6b 41 66 74 65 72  r |-> ClockAfter
1450: 45 78 65 63 75 74 69 6f 6e 20 2d 20 69 5d 0a 0a  Execution - i]..
1460: 49 6e 69 74 20 3d 3d 20 2f 5c 20 63 6c 6f 63 6b  Init == /\ clock
1470: 20 3d 20 30 0a 20 20 20 20 20 20 20 20 2f 5c 20   = 0.        /\
1480: 6d 65 73 73 61 67 65 73 20 3d 20 45 6d 70 74 79  messages = Empty
1490: 42 61 67 0a 20 20 20 20 20 20 20 20 2f 5c 20 49  Bag.        /\ I
14a0: 6e 69 74 53 65 6e 64 65 72 56 61 72 73 0a 20 20  nitSenderVars.
14b0: 20 20 20 20 20 20 2f 5c 20 49 6e 69 74 43 6f 6e        /\ InitCon
14c0: 6e 65 63 74 6f 72 56 61 72 73 0a 20 20 20 20 20  nectorVars.
14d0: 20 20 20 2f 5c 20 49 6e 69 74 4c 65 64 67 65 72     /\ InitLedger
14e0: 56 61 72 73 0a 0a 2d 2d 2d 2d 0a 5c 2a 20 44 65  Vars..----.\* De
14f0: 66 69 6e 65 20 73 74 61 74 65 20 74 72 61 6e 73  fine state trans
1500: 69 74 69 6f 6e 73 0a 0a 5c 2a 20 50 61 72 74 69  itions..\* Parti
1510: 63 69 70 61 6e 74 20 69 20 70 72 6f 70 6f 73 65  cipant i propose
1520: 73 20 61 6c 6c 20 74 68 65 20 73 75 62 70 61 79  s all the subpay
1530: 6d 65 6e 74 73 0a 53 74 61 72 74 50 72 6f 70 6f  ments.StartPropo
1540: 73 61 6c 50 68 61 73 65 28 69 29 20 3d 3d 0a 20  salPhase(i) ==.
1550: 20 20 20 2f 5c 20 73 65 6e 64 65 72 53 74 61 74     /\ senderStat
1560: 65 20 3d 20 53 5f 52 65 61 64 79 0a 20 20 20 20  e = S_Ready.
1570: 2f 5c 20 73 65 6e 64 65 72 53 74 61 74 65 27 20  /\ senderState'
1580: 3d 20 53 5f 50 72 6f 70 6f 73 61 6c 57 61 69 74  = S_ProposalWait
1590: 69 6e 67 0a 20 20 20 20 2f 5c 20 42 72 6f 61 64  ing.    /\ Broad
15a0: 63 61 73 74 28 7b 5b 0a 20 20 20 20 20 20 20 20  cast({[.
15b0: 20 6d 74 79 70 65 20 20 20 20 7c 2d 3e 20 53 75   mtype    |-> Su
15c0: 62 70 61 79 6d 65 6e 74 50 72 6f 70 6f 73 61 6c  bpaymentProposal
15d0: 52 65 71 75 65 73 74 2c 0a 20 20 20 20 20 20 20  Request,.
15e0: 20 20 6d 73 6f 75 72 63 65 20 20 7c 2d 3e 20 69    msource  |-> i
15f0: 2c 0a 20 20 20 20 20 20 20 20 20 6d 64 65 73 74  ,.         mdest
1600: 20 20 20 20 7c 2d 3e 20 6b 0a 20 20 20 20 20 20      |-> k.
1610: 20 5d 20 3a 20 6b 20 5c 69 6e 20 43 6f 6e 6e 65   ] : k \in Conne
1620: 63 74 6f 72 7d 29 0a 20 20 20 20 2f 5c 20 55 4e  ctor}).    /\ UN
1630: 43 48 41 4e 47 45 44 20 3c 3c 6c 65 64 67 65 72  CHANGED <<ledger
1640: 56 61 72 73 2c 20 63 6f 6e 6e 65 63 74 6f 72 56  Vars, connectorV
1650: 61 72 73 2c 20 73 65 6e 64 65 72 50 72 6f 70 6f  ars, senderPropo
1660: 73 61 6c 52 65 73 70 6f 6e 73 65 73 3e 3e 0a 0a  salResponses>>..
1670: 5c 2a 20 50 61 72 74 69 63 69 70 61 6e 74 20 69  \* Participant i
1680: 20 73 74 61 72 74 73 20 6f 66 66 20 74 68 65 20   starts off the
1690: 70 72 65 70 61 72 61 74 69 6f 6e 20 63 68 61 69  preparation chai
16a0: 6e 0a 53 74 61 72 74 50 72 65 70 61 72 61 74 69  n.StartPreparati
16b0: 6f 6e 50 68 61 73 65 28 69 29 20 3d 3d 0a 20 20  onPhase(i) ==.
16c0: 20 20 2f 5c 20 73 65 6e 64 65 72 53 74 61 74 65    /\ senderState
16d0: 20 3d 20 53 5f 50 72 6f 70 6f 73 61 6c 57 61 69   = S_ProposalWai
16e0: 74 69 6e 67 0a 20 20 20 20 2f 5c 20 5c 45 20 70  ting.    /\ \E p
16f0: 20 5c 69 6e 20 44 4f 4d 41 49 4e 20 73 65 6e 64   \in DOMAIN send
1700: 65 72 50 72 6f 70 6f 73 61 6c 52 65 73 70 6f 6e  erProposalRespon
1710: 73 65 73 20 3a 20 73 65 6e 64 65 72 50 72 6f 70  ses : senderProp
1720: 6f 73 61 6c 52 65 73 70 6f 6e 73 65 73 5b 70 5d  osalResponses[p]
1730: 0a 20 20 20 20 2f 5c 20 73 65 6e 64 65 72 53 74  .    /\ senderSt
1740: 61 74 65 27 20 3d 20 53 5f 57 61 69 74 69 6e 67  ate' = S_Waiting
1750: 0a 20 20 20 20 2f 5c 20 53 65 6e 64 28 5b 6d 74  .    /\ Send([mt
1760: 79 70 65 20 20 20 7c 2d 3e 20 50 72 65 70 61 72  ype   |-> Prepar
1770: 65 52 65 71 75 65 73 74 2c 0a 20 20 20 20 20 20  eRequest,.
1780: 20 20 20 20 20 20 20 6d 73 6f 75 72 63 65 20 7c         msource |
1790: 2d 3e 20 69 2c 0a 20 20 20 20 20 20 20 20 20 20  -> i,.
17a0: 20 20 20 6d 64 65 73 74 20 20 20 7c 2d 3e 20 69     mdest   |-> i
17b0: 2b 31 5d 29 0a 20 20 20 20 2f 5c 20 55 4e 43 48  +1]).    /\ UNCH
17c0: 41 4e 47 45 44 20 3c 3c 6c 65 64 67 65 72 56 61  ANGED <<ledgerVa
17d0: 72 73 2c 20 63 6f 6e 6e 65 63 74 6f 72 56 61 72  rs, connectorVar
17e0: 73 2c 20 73 65 6e 64 65 72 50 72 6f 70 6f 73 61  s, senderProposa
17f0: 6c 52 65 73 70 6f 6e 73 65 73 3e 3e 0a 0a 5c 2a  lResponses>>..\*
1800: 20 4c 65 64 67 65 72 20 73 70 6f 6e 74 61 6e 65   Ledger spontane
1810: 6f 75 73 6c 79 20 61 62 6f 72 74 73 0a 4c 65 64  ously aborts.Led
1820: 67 65 72 41 62 6f 72 74 28 6c 29 20 3d 3d 0a 20  gerAbort(l) ==.
1830: 20 20 20 2f 5c 20 6c 65 64 67 65 72 53 74 61 74     /\ ledgerStat
1840: 65 5b 6c 5d 20 3d 20 4c 5f 50 72 6f 70 6f 73 65  e[l] = L_Propose
1850: 64 0a 20 20 20 20 2f 5c 20 6c 65 64 67 65 72 53  d.    /\ ledgerS
1860: 74 61 74 65 27 20 3d 20 5b 6c 65 64 67 65 72 53  tate' = [ledgerS
1870: 74 61 74 65 20 45 58 43 45 50 54 20 21 5b 6c 5d  tate EXCEPT ![l]
1880: 20 3d 20 4c 5f 41 62 6f 72 74 65 64 5d 0a 20 20   = L_Aborted].
1890: 20 20 2f 5c 20 53 65 6e 64 28 5b 6d 74 79 70 65    /\ Send([mtype
18a0: 20 20 20 7c 2d 3e 20 41 62 6f 72 74 4e 6f 74 69     |-> AbortNoti
18b0: 66 79 2c 0a 20 20 20 20 20 20 20 20 20 20 20 20  fy,.
18c0: 20 6d 73 6f 75 72 63 65 20 7c 2d 3e 20 6c 2c 0a   msource |-> l,.
18d0: 20 20 20 20 20 20 20 20 20 20 20 20 20 6d 64 65               mde
18e0: 73 74 20 20 20 7c 2d 3e 20 6c 2d 31 5d 29 0a 20  st   |-> l-1]).
18f0: 20 20 20 2f 5c 20 55 4e 43 48 41 4e 47 45 44 20     /\ UNCHANGED
1900: 3c 3c 73 65 6e 64 65 72 56 61 72 73 2c 20 63 6f  <<senderVars, co
1910: 6e 6e 65 63 74 6f 72 56 61 72 73 2c 20 6c 65 64  nnectorVars, led
1920: 67 65 72 45 78 70 69 72 61 74 69 6f 6e 3e 3e 0a  gerExpiration>>.
1930: 0a 5c 2a 20 54 72 61 6e 73 66 65 72 20 74 69 6d  .\* Transfer tim
1940: 65 73 20 6f 75 74 0a 4c 65 64 67 65 72 54 69 6d  es out.LedgerTim
1950: 65 6f 75 74 28 6c 29 20 3d 3d 0a 20 20 20 20 2f  eout(l) ==.    /
1960: 5c 20 5c 6c 6e 6f 74 20 49 73 46 69 6e 61 6c 4c  \ \lnot IsFinalL
1970: 65 64 67 65 72 53 74 61 74 65 28 6c 65 64 67 65  edgerState(ledge
1980: 72 53 74 61 74 65 5b 6c 5d 29 0a 20 20 20 20 2f  rState[l]).    /
1990: 5c 20 6c 65 64 67 65 72 45 78 70 69 72 61 74 69  \ ledgerExpirati
19a0: 6f 6e 5b 6c 5d 20 3d 3c 20 63 6c 6f 63 6b 0a 20  on[l] =< clock.
19b0: 20 20 20 2f 5c 20 6c 65 64 67 65 72 53 74 61 74     /\ ledgerStat
19c0: 65 27 20 3d 20 5b 6c 65 64 67 65 72 53 74 61 74  e' = [ledgerStat
19d0: 65 20 45 58 43 45 50 54 20 21 5b 6c 5d 20 3d 20  e EXCEPT ![l] =
19e0: 4c 5f 41 62 6f 72 74 65 64 5d 0a 20 20 20 20 2f  L_Aborted].    /
19f0: 5c 20 53 65 6e 64 28 5b 6d 74 79 70 65 20 20 20  \ Send([mtype
1a00: 7c 2d 3e 20 41 62 6f 72 74 4e 6f 74 69 66 79 2c  |-> AbortNotify,
1a10: 0a 20 20 20 20 20 20 20 20 20 20 20 20 20 6d 73  .             ms
1a20: 6f 75 72 63 65 20 7c 2d 3e 20 6c 2c 0a 20 20 20  ource |-> l,.
1a30: 20 20 20 20 20 20 20 20 20 20 6d 64 65 73 74 20            mdest
1a40: 20 20 7c 2d 3e 20 6c 2d 31 5d 29 0a 20 20 20 20    |-> l-1]).
1a50: 2f 5c 20 55 4e 43 48 41 4e 47 45 44 20 3c 3c 73  /\ UNCHANGED <<s
1a60: 65 6e 64 65 72 56 61 72 73 2c 20 63 6f 6e 6e 65  enderVars, conne
1a70: 63 74 6f 72 56 61 72 73 2c 20 6c 65 64 67 65 72  ctorVars, ledger
1a80: 45 78 70 69 72 61 74 69 6f 6e 3e 3e 0a 0a 5c 2a  Expiration>>..\*
1a90: 20 49 66 20 6e 6f 20 6d 65 73 73 61 67 65 73 20   If no messages
1aa0: 61 72 65 20 69 6e 20 66 6c 69 67 68 74 20 61 6e  are in flight an
1ab0: 64 20 74 68 65 20 73 65 6e 64 65 72 20 69 73 6e  d the sender isn
1ac0: 27 74 20 64 6f 69 6e 67 20 61 6e 79 74 68 69 6e  't doing anythin
1ad0: 67 2c 20 61 64 76 61 6e 63 65 20 74 68 65 0a 5c  g, advance the.\
1ae0: 2a 20 63 6c 6f 63 6b 0a 4e 6f 74 68 69 6e 67 48  * clock.NothingH
1af0: 61 70 70 65 6e 73 20 3d 3d 0a 20 20 20 20 2f 5c  appens ==.    /\
1b00: 20 63 6c 6f 63 6b 20 5c 6c 65 71 20 4d 61 78 28   clock \leq Max(
1b10: 7b 6c 65 64 67 65 72 45 78 70 69 72 61 74 69 6f  {ledgerExpiratio
1b20: 6e 5b 78 5d 20 3a 20 78 20 5c 69 6e 20 4c 65 64  n[x] : x \in Led
1b30: 67 65 72 7d 29 0a 20 20 20 20 2f 5c 20 42 61 67  ger}).    /\ Bag
1b40: 43 61 72 64 69 6e 61 6c 69 74 79 28 6d 65 73 73  Cardinality(mess
1b50: 61 67 65 73 29 20 3d 20 30 0a 20 20 20 20 2f 5c  ages) = 0.    /\
1b60: 20 73 65 6e 64 65 72 53 74 61 74 65 20 23 20 53   senderState # S
1b70: 5f 52 65 61 64 79 0a 20 20 20 20 2f 5c 20 5c 2f  _Ready.    /\ \/
1b80: 20 73 65 6e 64 65 72 53 74 61 74 65 20 23 20 53   senderState # S
1b90: 5f 50 72 6f 70 6f 73 61 6c 57 61 69 74 69 6e 67  _ProposalWaiting
1ba0: 0a 20 20 20 20 20 20 20 5c 2f 20 5c 41 20 70 20  .       \/ \A p
1bb0: 5c 69 6e 20 44 4f 4d 41 49 4e 20 73 65 6e 64 65  \in DOMAIN sende
1bc0: 72 50 72 6f 70 6f 73 61 6c 52 65 73 70 6f 6e 73  rProposalRespons
1bd0: 65 73 20 3a 20 5c 6c 6e 6f 74 20 73 65 6e 64 65  es : \lnot sende
1be0: 72 50 72 6f 70 6f 73 61 6c 52 65 73 70 6f 6e 73  rProposalRespons
1bf0: 65 73 5b 70 5d 0a 20 20 20 20 2f 5c 20 55 4e 43  es[p].    /\ UNC
1c00: 48 41 4e 47 45 44 20 3c 3c 6d 65 73 73 61 67 65  HANGED <<message
1c10: 73 2c 20 73 65 6e 64 65 72 56 61 72 73 2c 20 63  s, senderVars, c
1c20: 6f 6e 6e 65 63 74 6f 72 56 61 72 73 2c 20 6c 65  onnectorVars, le
1c30: 64 67 65 72 56 61 72 73 3e 3e 0a 0a 2d 2d 2d 2d  dgerVars>>..----
1c40: 0a 5c 2a 20 4d 65 73 73 61 67 65 20 68 61 6e 64  .\* Message hand
1c50: 6c 65 72 73 0a 5c 2a 20 69 20 3d 20 72 65 63 69  lers.\* i = reci
1c60: 70 69 65 6e 74 2c 20 6a 20 3d 20 73 65 6e 64 65  pient, j = sende
1c70: 72 2c 20 6d 20 3d 20 6d 65 73 73 61 67 65 0a 0a  r, m = message..
1c80: 5c 2a 20 4c 65 64 67 65 72 20 69 20 72 65 63 65  \* Ledger i rece
1c90: 69 76 65 73 20 61 20 50 72 65 70 61 72 65 20 72  ives a Prepare r
1ca0: 65 71 75 65 73 74 20 66 72 6f 6d 20 70 61 72 74  equest from part
1cb0: 69 63 69 70 61 6e 74 20 6a 0a 4c 65 64 67 65 72  icipant j.Ledger
1cc0: 48 61 6e 64 6c 65 50 72 65 70 61 72 65 52 65 71  HandlePrepareReq
1cd0: 75 65 73 74 28 69 2c 20 6a 2c 20 6d 29 20 3d 3d  uest(i, j, m) ==
1ce0: 0a 20 20 20 20 4c 45 54 20 76 61 6c 69 64 20 3d  .    LET valid =
1cf0: 3d 20 2f 5c 20 6c 65 64 67 65 72 53 74 61 74 65  = /\ ledgerState
1d00: 5b 69 5d 20 3d 20 4c 5f 50 72 6f 70 6f 73 65 64  [i] = L_Proposed
1d10: 0a 20 20 20 20 20 20 20 20 20 20 20 20 20 20 20  .
1d20: 20 20 2f 5c 20 6a 20 3d 20 69 20 2d 20 31 0a 20    /\ j = i - 1.
1d30: 20 20 20 49 4e 20 5c 2f 20 2f 5c 20 76 61 6c 69     IN \/ /\ vali
1d40: 64 0a 20 20 20 20 20 20 20 20 20 20 2f 5c 20 69  d.          /\ i
1d50: 20 5c 69 6e 20 4c 65 64 67 65 72 0a 20 20 20 20   \in Ledger.
1d60: 20 20 20 20 20 20 2f 5c 20 6c 65 64 67 65 72 53        /\ ledgerS
1d70: 74 61 74 65 27 20 3d 20 5b 6c 65 64 67 65 72 53  tate' = [ledgerS
1d80: 74 61 74 65 20 45 58 43 45 50 54 20 21 5b 69 5d  tate EXCEPT ![i]
1d90: 20 3d 20 4c 5f 50 72 65 70 61 72 65 64 5d 0a 20   = L_Prepared].
1da0: 20 20 20 20 20 20 20 20 20 2f 5c 20 52 65 70 6c           /\ Repl
1db0: 79 28 5b 6d 74 79 70 65 20 20 20 7c 2d 3e 20 50  y([mtype   |-> P
1dc0: 72 65 70 61 72 65 4e 6f 74 69 66 79 2c 0a 20 20  repareNotify,.
1dd0: 20 20 20 20 20 20 20 20 20 20 20 20 20 20 20 20
1de0: 20 20 6d 73 6f 75 72 63 65 20 7c 2d 3e 20 69 2c    msource |-> i,
1df0: 0a 20 20 20 20 20 20 20 20 20 20 20 20 20 20 20  .
1e00: 20 20 20 20 20 6d 64 65 73 74 20 20 20 7c 2d 3e       mdest   |->
1e10: 20 69 2b 31 5d 2c 20 6d 29 0a 20 20 20 20 20 20   i+1], m).
1e20: 20 20 20 20 2f 5c 20 55 4e 43 48 41 4e 47 45 44      /\ UNCHANGED
1e30: 20 3c 3c 73 65 6e 64 65 72 56 61 72 73 2c 20 63   <<senderVars, c
1e40: 6f 6e 6e 65 63 74 6f 72 56 61 72 73 2c 20 6c 65  onnectorVars, le
1e50: 64 67 65 72 45 78 70 69 72 61 74 69 6f 6e 3e 3e  dgerExpiration>>
1e60: 0a 20 20 20 20 20 20 20 5c 2f 20 2f 5c 20 5c 6c  .       \/ /\ \l
1e70: 6e 6f 74 20 76 61 6c 69 64 0a 20 20 20 20 20 20  not valid.
1e80: 20 20 20 20 2f 5c 20 69 20 5c 69 6e 20 4c 65 64      /\ i \in Led
1e90: 67 65 72 0a 20 20 20 20 20 20 20 20 20 20 2f 5c  ger.          /\
1ea0: 20 44 69 73 63 61 72 64 28 6d 29 0a 20 20 20 20   Discard(m).
1eb0: 20 20 20 20 20 20 2f 5c 20 55 4e 43 48 41 4e 47        /\ UNCHANG
1ec0: 45 44 20 3c 3c 73 65 6e 64 65 72 56 61 72 73 2c  ED <<senderVars,
1ed0: 20 63 6f 6e 6e 65 63 74 6f 72 56 61 72 73 2c 20   connectorVars,
1ee0: 6c 65 64 67 65 72 56 61 72 73 3e 3e 0a 0a 5c 2a  ledgerVars>>..\*
1ef0: 20 4c 65 64 67 65 72 20 69 20 72 65 63 65 69 76   Ledger i receiv
1f00: 65 73 20 61 6e 20 45 78 65 63 75 74 65 20 72 65  es an Execute re
1f10: 71 75 65 73 74 20 66 72 6f 6d 20 70 72 6f 63 65  quest from proce
1f20: 73 73 20 6a 0a 4c 65 64 67 65 72 48 61 6e 64 6c  ss j.LedgerHandl
1f30: 65 45 78 65 63 75 74 65 52 65 71 75 65 73 74 28  eExecuteRequest(
1f40: 69 2c 20 6a 2c 20 6d 29 20 3d 3d 0a 20 20 20 20  i, j, m) ==.
1f50: 4c 45 54 20 76 61 6c 69 64 20 3d 3d 20 2f 5c 20  LET valid == /\
1f60: 6c 65 64 67 65 72 53 74 61 74 65 5b 69 5d 20 3d  ledgerState[i] =
1f70: 20 4c 5f 50 72 65 70 61 72 65 64 0a 20 20 20 20   L_Prepared.
1f80: 20 20 20 20 20 20 20 20 20 20 20 20 20 2f 5c 20               /\
1f90: 6c 65 64 67 65 72 45 78 70 69 72 61 74 69 6f 6e  ledgerExpiration
1fa0: 5b 69 5d 20 3e 20 63 6c 6f 63 6b 0a 20 20 20 20  [i] > clock.
1fb0: 20 20 20 20 20 20 20 20 20 20 20 20 20 2f 5c 20               /\
1fc0: 6d 2e 6d 72 65 63 65 69 70 74 20 3d 20 52 5f 52  m.mreceipt = R_R
1fd0: 65 63 65 69 70 74 53 69 67 6e 61 74 75 72 65 0a  eceiptSignature.
1fe0: 20 20 20 20 49 4e 20 5c 2f 20 2f 5c 20 76 61 6c      IN \/ /\ val
1ff0: 69 64 0a 20 20 20 20 20 20 20 20 20 20 2f 5c 20  id.          /\
2000: 6c 65 64 67 65 72 53 74 61 74 65 27 20 3d 20 5b  ledgerState' = [
2010: 6c 65 64 67 65 72 53 74 61 74 65 20 45 58 43 45  ledgerState EXCE
2020: 50 54 20 21 5b 69 5d 20 3d 20 4c 5f 45 78 65 63  PT ![i] = L_Exec
2030: 75 74 65 64 5d 0a 20 20 20 20 20 20 20 20 20 20  uted].
2040: 2f 5c 20 52 65 70 6c 79 28 5b 6d 74 79 70 65 20  /\ Reply([mtype
2050: 20 20 20 7c 2d 3e 20 45 78 65 63 75 74 65 4e 6f     |-> ExecuteNo
2060: 74 69 66 79 2c 0a 20 20 20 20 20 20 20 20 20 20  tify,.
2070: 20 20 20 20 20 20 20 20 20 20 6d 73 6f 75 72 63            msourc
2080: 65 20 20 7c 2d 3e 20 69 2c 0a 20 20 20 20 20 20  e  |-> i,.
2090: 20 20 20 20 20 20 20 20 20 20 20 20 20 20 6d 64                md
20a0: 65 73 74 20 20 20 20 7c 2d 3e 20 69 2d 31 2c 0a  est    |-> i-1,.
20b0: 20 20 20 20 20 20 20 20 20 20 20 20 20 20 20 20
20c0: 20 20 20 20 6d 72 65 63 65 69 70 74 20 7c 2d 3e      mreceipt |->
20d0: 20 6d 2e 6d 72 65 63 65 69 70 74 5d 2c 20 6d 29   m.mreceipt], m)
20e0: 0a 20 20 20 20 20 20 20 20 20 20 2f 5c 20 55 4e  .          /\ UN
20f0: 43 48 41 4e 47 45 44 20 3c 3c 73 65 6e 64 65 72  CHANGED <<sender
2100: 56 61 72 73 2c 20 63 6f 6e 6e 65 63 74 6f 72 56  Vars, connectorV
2110: 61 72 73 2c 20 6c 65 64 67 65 72 45 78 70 69 72  ars, ledgerExpir
2120: 61 74 69 6f 6e 3e 3e 0a 20 20 20 20 20 20 20 5c  ation>>.       \
2130: 2f 20 2f 5c 20 5c 6c 6e 6f 74 20 76 61 6c 69 64  / /\ \lnot valid
2140: 0a 20 20 20 20 20 20 20 20 20 20 2f 5c 20 44 69  .          /\ Di
2150: 73 63 61 72 64 28 6d 29 0a 20 20 20 20 20 20 20  scard(m).
2160: 20 20 20 2f 5c 20 55 4e 43 48 41 4e 47 45 44 20     /\ UNCHANGED
2170: 3c 3c 73 65 6e 64 65 72 56 61 72 73 2c 20 63 6f  <<senderVars, co
2180: 6e 6e 65 63 74 6f 72 56 61 72 73 2c 20 6c 65 64  nnectorVars, led
2190: 67 65 72 56 61 72 73 3e 3e 0a 0a 5c 2a 20 4c 65  gerVars>>..\* Le
21a0: 64 67 65 72 20 69 20 72 65 63 65 69 76 65 73 20  dger i receives
21b0: 61 20 6d 65 73 73 61 67 65 0a 4c 65 64 67 65 72  a message.Ledger
21c0: 52 65 63 65 69 76 65 28 69 2c 20 6a 2c 20 6d 29  Receive(i, j, m)
21d0: 20 3d 3d 0a 20 20 20 20 5c 2f 20 2f 5c 20 6d 2e   ==.    \/ /\ m.
21e0: 6d 74 79 70 65 20 3d 20 50 72 65 70 61 72 65 52  mtype = PrepareR
21f0: 65 71 75 65 73 74 0a 20 20 20 20 20 20 20 2f 5c  equest.       /\
2200: 20 4c 65 64 67 65 72 48 61 6e 64 6c 65 50 72 65   LedgerHandlePre
2210: 70 61 72 65 52 65 71 75 65 73 74 28 69 2c 20 6a  pareRequest(i, j
2220: 2c 20 6d 29 0a 20 20 20 20 5c 2f 20 2f 5c 20 6d  , m).    \/ /\ m
2230: 2e 6d 74 79 70 65 20 3d 20 45 78 65 63 75 74 65  .mtype = Execute
2240: 52 65 71 75 65 73 74 0a 20 20 20 20 20 20 20 2f  Request.       /
2250: 5c 20 4c 65 64 67 65 72 48 61 6e 64 6c 65 45 78  \ LedgerHandleEx
2260: 65 63 75 74 65 52 65 71 75 65 73 74 28 69 2c 20  ecuteRequest(i,
2270: 6a 2c 20 6d 29 0a 0a 5c 2a 20 53 65 6e 64 65 72  j, m)..\* Sender
2280: 20 72 65 63 65 69 76 65 73 20 61 20 53 75 62 70   receives a Subp
2290: 61 79 6d 65 6e 74 50 72 6f 70 6f 73 61 6c 20 72  aymentProposal r
22a0: 65 71 75 65 73 74 0a 53 65 6e 64 65 72 48 61 6e  equest.SenderHan
22b0: 64 6c 65 53 75 62 70 61 79 6d 65 6e 74 50 72 6f  dleSubpaymentPro
22c0: 70 6f 73 61 6c 52 65 73 70 6f 6e 73 65 28 69 2c  posalResponse(i,
22d0: 20 6a 2c 20 6d 29 20 3d 3d 0a 20 20 20 20 2f 5c   j, m) ==.    /\
22e0: 20 69 20 3d 20 53 65 6e 64 65 72 0a 20 20 20 20   i = Sender.
22f0: 2f 5c 20 73 65 6e 64 65 72 50 72 6f 70 6f 73 61  /\ senderProposa
2300: 6c 52 65 73 70 6f 6e 73 65 73 27 20 3d 20 5b 73  lResponses' = [s
2310: 65 6e 64 65 72 50 72 6f 70 6f 73 61 6c 52 65 73  enderProposalRes
2320: 70 6f 6e 73 65 73 20 45 58 43 45 50 54 20 21 5b  ponses EXCEPT ![
2330: 6a 5d 20 3d 20 54 52 55 45 5d 0a 20 20 20 20 2f  j] = TRUE].    /
2340: 5c 20 44 69 73 63 61 72 64 28 6d 29 0a 20 20 20  \ Discard(m).
2350: 20 2f 5c 20 55 4e 43 48 41 4e 47 45 44 20 3c 3c   /\ UNCHANGED <<
2360: 63 6f 6e 6e 65 63 74 6f 72 56 61 72 73 2c 20 6c  connectorVars, l
2370: 65 64 67 65 72 56 61 72 73 2c 20 73 65 6e 64 65  edgerVars, sende
2380: 72 53 74 61 74 65 3e 3e 0a 0a 5c 2a 20 4c 65 64  rState>>..\* Led
2390: 67 65 72 20 6a 20 6e 6f 74 69 66 69 65 73 20 73  ger j notifies s
23a0: 65 6e 64 65 72 20 74 68 61 74 20 74 68 65 20 74  ender that the t
23b0: 72 61 6e 73 66 65 72 20 69 73 20 65 78 65 63 75  ransfer is execu
23c0: 74 65 64 0a 53 65 6e 64 65 72 48 61 6e 64 6c 65  ted.SenderHandle
23d0: 45 78 65 63 75 74 65 4e 6f 74 69 66 79 28 69 2c  ExecuteNotify(i,
23e0: 20 6a 2c 20 6d 29 20 3d 3d 0a 20 20 20 20 5c 2f   j, m) ==.    \/
23f0: 20 2f 5c 20 73 65 6e 64 65 72 53 74 61 74 65 20   /\ senderState
2400: 3d 20 53 5f 57 61 69 74 69 6e 67 0a 20 20 20 20  = S_Waiting.
2410: 20 20 20 2f 5c 20 73 65 6e 64 65 72 53 74 61 74     /\ senderStat
2420: 65 27 20 3d 20 53 5f 44 6f 6e 65 0a 20 20 20 20  e' = S_Done.
2430: 20 20 20 2f 5c 20 44 69 73 63 61 72 64 28 6d 29     /\ Discard(m)
2440: 0a 20 20 20 20 20 20 20 2f 5c 20 55 4e 43 48 41  .       /\ UNCHA
2450: 4e 47 45 44 20 3c 3c 6c 65 64 67 65 72 56 61 72  NGED <<ledgerVar
2460: 73 2c 20 63 6f 6e 6e 65 63 74 6f 72 56 61 72 73  s, connectorVars
2470: 2c 20 73 65 6e 64 65 72 50 72 6f 70 6f 73 61 6c  , senderProposal
2480: 52 65 73 70 6f 6e 73 65 73 3e 3e 0a 20 20 20 20  Responses>>.
2490: 5c 2f 20 2f 5c 20 73 65 6e 64 65 72 53 74 61 74  \/ /\ senderStat
24a0: 65 20 23 20 53 5f 57 61 69 74 69 6e 67 0a 20 20  e # S_Waiting.
24b0: 20 20 20 20 20 2f 5c 20 44 69 73 63 61 72 64 28       /\ Discard(
24c0: 6d 29 0a 20 20 20 20 20 20 20 2f 5c 20 55 4e 43  m).       /\ UNC
24d0: 48 41 4e 47 45 44 20 3c 3c 73 65 6e 64 65 72 56  HANGED <<senderV
24e0: 61 72 73 2c 20 63 6f 6e 6e 65 63 74 6f 72 56 61  ars, connectorVa
24f0: 72 73 2c 20 6c 65 64 67 65 72 56 61 72 73 3e 3e  rs, ledgerVars>>
2500: 0a 0a 5c 2a 20 4c 65 64 67 65 72 20 6a 20 6e 6f  ..\* Ledger j no
2510: 74 69 66 69 65 73 20 73 65 6e 64 65 72 20 74 68  tifies sender th
2520: 61 74 20 74 68 65 20 74 72 61 6e 73 66 65 72 20  at the transfer
2530: 69 73 20 61 62 6f 72 74 65 64 0a 53 65 6e 64 65  is aborted.Sende
2540: 72 48 61 6e 64 6c 65 41 62 6f 72 74 4e 6f 74 69  rHandleAbortNoti
2550: 66 79 28 69 2c 20 6a 2c 20 6d 29 20 3d 3d 0a 20  fy(i, j, m) ==.
2560: 20 20 20 4c 45 54 20 69 73 53 65 6e 64 65 72 57     LET isSenderW
2570: 61 69 74 69 6e 67 20 3d 3d 20 73 65 6e 64 65 72  aiting == sender
2580: 53 74 61 74 65 20 5c 69 6e 20 7b 20 53 5f 50 72  State \in { S_Pr
2590: 6f 70 6f 73 61 6c 57 61 69 74 69 6e 67 2c 20 53  oposalWaiting, S
25a0: 5f 57 61 69 74 69 6e 67 2c 20 53 5f 52 65 61 64  _Waiting, S_Read
25b0: 79 20 7d 0a 20 20 20 20 49 4e 20 5c 2f 20 2f 5c  y }.    IN \/ /\
25c0: 20 69 73 53 65 6e 64 65 72 57 61 69 74 69 6e 67   isSenderWaiting
25d0: 0a 20 20 20 20 20 20 20 20 20 20 2f 5c 20 73 65  .          /\ se
25e0: 6e 64 65 72 53 74 61 74 65 27 20 3d 20 53 5f 44  nderState' = S_D
25f0: 6f 6e 65 0a 20 20 20 20 20 20 20 20 20 20 2f 5c  one.          /\
2600: 20 44 69 73 63 61 72 64 28 6d 29 0a 20 20 20 20   Discard(m).
2610: 20 20 20 20 20 20 2f 5c 20 55 4e 43 48 41 4e 47        /\ UNCHANG
2620: 45 44 20 3c 3c 6c 65 64 67 65 72 56 61 72 73 2c  ED <<ledgerVars,
2630: 20 63 6f 6e 6e 65 63 74 6f 72 56 61 72 73 2c 20   connectorVars,
2640: 73 65 6e 64 65 72 50 72 6f 70 6f 73 61 6c 52 65  senderProposalRe
2650: 73 70 6f 6e 73 65 73 3e 3e 0a 20 20 20 20 20 20  sponses>>.
2660: 20 5c 2f 20 2f 5c 20 5c 6c 6e 6f 74 20 69 73 53   \/ /\ \lnot isS
2670: 65 6e 64 65 72 57 61 69 74 69 6e 67 0a 20 20 20  enderWaiting.
2680: 20 20 20 20 20 20 20 2f 5c 20 44 69 73 63 61 72         /\ Discar
2690: 64 28 6d 29 0a 20 20 20 20 20 20 20 20 20 20 2f  d(m).          /
26a0: 5c 20 55 4e 43 48 41 4e 47 45 44 20 3c 3c 73 65  \ UNCHANGED <<se
26b0: 6e 64 65 72 56 61 72 73 2c 20 63 6f 6e 6e 65 63  nderVars, connec
26c0: 74 6f 72 56 61 72 73 2c 20 6c 65 64 67 65 72 56  torVars, ledgerV
26d0: 61 72 73 3e 3e 0a 0a 5c 2a 20 53 65 6e 64 65 72  ars>>..\* Sender
26e0: 20 72 65 63 65 69 76 65 73 20 61 20 6d 65 73 73   receives a mess
26f0: 61 67 65 0a 53 65 6e 64 65 72 52 65 63 65 69 76  age.SenderReceiv
2700: 65 28 69 2c 20 6a 2c 20 6d 29 20 3d 3d 0a 20 20  e(i, j, m) ==.
2710: 20 20 5c 2f 20 2f 5c 20 6d 2e 6d 74 79 70 65 20    \/ /\ m.mtype
2720: 3d 20 53 75 62 70 61 79 6d 65 6e 74 50 72 6f 70  = SubpaymentProp
2730: 6f 73 61 6c 52 65 73 70 6f 6e 73 65 0a 20 20 20  osalResponse.
2740: 20 20 20 20 2f 5c 20 53 65 6e 64 65 72 48 61 6e      /\ SenderHan
2750: 64 6c 65 53 75 62 70 61 79 6d 65 6e 74 50 72 6f  dleSubpaymentPro
2760: 70 6f 73 61 6c 52 65 73 70 6f 6e 73 65 28 69 2c  posalResponse(i,
2770: 20 6a 2c 20 6d 29 0a 20 20 20 20 5c 2f 20 2f 5c   j, m).    \/ /\
2780: 20 6d 2e 6d 74 79 70 65 20 3d 20 45 78 65 63 75   m.mtype = Execu
2790: 74 65 4e 6f 74 69 66 79 0a 20 20 20 20 20 20 20  teNotify.
27a0: 2f 5c 20 53 65 6e 64 65 72 48 61 6e 64 6c 65 45  /\ SenderHandleE
27b0: 78 65 63 75 74 65 4e 6f 74 69 66 79 28 69 2c 20  xecuteNotify(i,
27c0: 6a 2c 20 6d 29 0a 20 20 20 20 5c 2f 20 2f 5c 20  j, m).    \/ /\
27d0: 6d 2e 6d 74 79 70 65 20 3d 20 41 62 6f 72 74 4e  m.mtype = AbortN
27e0: 6f 74 69 66 79 0a 20 20 20 20 20 20 20 2f 5c 20  otify.       /\
27f0: 53 65 6e 64 65 72 48 61 6e 64 6c 65 41 62 6f 72  SenderHandleAbor
2800: 74 4e 6f 74 69 66 79 28 69 2c 20 6a 2c 20 6d 29  tNotify(i, j, m)
2810: 0a 0a 5c 2a 20 4c 65 64 67 65 72 20 6a 20 6e 6f  ..\* Ledger j no
2820: 74 69 66 69 65 73 20 72 65 63 69 70 69 65 6e 74  tifies recipient
2830: 20 74 68 61 74 20 74 68 65 20 74 72 61 6e 73 66   that the transf
2840: 65 72 20 69 73 20 70 72 65 70 61 72 65 64 0a 52  er is prepared.R
2850: 65 63 69 70 69 65 6e 74 48 61 6e 64 6c 65 50 72  ecipientHandlePr
2860: 65 70 61 72 65 4e 6f 74 69 66 79 28 69 2c 20 6a  epareNotify(i, j
2870: 2c 20 6d 29 20 3d 3d 0a 20 20 20 20 5c 2f 20 2f  , m) ==.    \/ /
2880: 5c 20 52 65 70 6c 79 28 5b 6d 74 79 70 65 20 20  \ Reply([mtype
2890: 20 20 7c 2d 3e 20 45 78 65 63 75 74 65 52 65 71    |-> ExecuteReq
28a0: 75 65 73 74 2c 0a 20 20 20 20 20 20 20 20 20 20  uest,.
28b0: 20 20 20 20 20 20 20 6d 73 6f 75 72 63 65 20 20         msource
28c0: 7c 2d 3e 20 69 2c 0a 20 20 20 20 20 20 20 20 20  |-> i,.
28d0: 20 20 20 20 20 20 20 20 6d 64 65 73 74 20 20 20          mdest
28e0: 20 7c 2d 3e 20 69 2d 31 2c 0a 20 20 20 20 20 20   |-> i-1,.
28f0: 20 20 20 20 20 20 20 20 20 20 20 6d 72 65 63 65             mrece
2900: 69 70 74 20 7c 2d 3e 20 52 5f 52 65 63 65 69 70  ipt |-> R_Receip
2910: 74 53 69 67 6e 61 74 75 72 65 5d 2c 20 6d 29 0a  tSignature], m).
2920: 20 20 20 20 20 20 20 2f 5c 20 55 4e 43 48 41 4e         /\ UNCHAN
2930: 47 45 44 20 3c 3c 73 65 6e 64 65 72 56 61 72 73  GED <<senderVars
2940: 2c 20 63 6f 6e 6e 65 63 74 6f 72 56 61 72 73 2c  , connectorVars,
2950: 20 6c 65 64 67 65 72 56 61 72 73 3e 3e 0a 0a 5c   ledgerVars>>..\
2960: 2a 20 52 65 63 69 70 69 65 6e 74 20 72 65 63 65  * Recipient rece
2970: 69 76 65 73 20 61 20 6d 65 73 73 61 67 65 0a 52  ives a message.R
2980: 65 63 69 70 69 65 6e 74 52 65 63 65 69 76 65 28  ecipientReceive(
2990: 69 2c 20 6a 2c 20 6d 29 20 3d 3d 0a 20 20 20 20  i, j, m) ==.
29a0: 5c 2f 20 2f 5c 20 6d 2e 6d 74 79 70 65 20 3d 20  \/ /\ m.mtype =
29b0: 50 72 65 70 61 72 65 4e 6f 74 69 66 79 0a 20 20  PrepareNotify.
29c0: 20 20 20 20 20 2f 5c 20 52 65 63 69 70 69 65 6e       /\ Recipien
29d0: 74 48 61 6e 64 6c 65 50 72 65 70 61 72 65 4e 6f  tHandlePrepareNo
29e0: 74 69 66 79 28 69 2c 20 6a 2c 20 6d 29 0a 0a 5c  tify(i, j, m)..\
29f0: 2a 20 43 6f 6e 6e 65 63 74 6f 72 20 69 20 72 65  * Connector i re
2a00: 63 65 69 76 65 73 20 61 20 53 75 62 70 61 79 6d  ceives a Subpaym
2a10: 65 6e 74 50 72 6f 70 6f 73 61 6c 20 72 65 71 75  entProposal requ
2a20: 65 73 74 0a 43 6f 6e 6e 65 63 74 6f 72 48 61 6e  est.ConnectorHan
2a30: 64 6c 65 53 75 62 70 61 79 6d 65 6e 74 50 72 6f  dleSubpaymentPro
2a40: 70 6f 73 61 6c 52 65 71 75 65 73 74 28 69 2c 20  posalRequest(i,
2a50: 6a 2c 20 6d 29 20 3d 3d 0a 20 20 20 20 2f 5c 20  j, m) ==.    /\
2a60: 63 6f 6e 6e 65 63 74 6f 72 53 74 61 74 65 27 20  connectorState'
2a70: 3d 20 5b 63 6f 6e 6e 65 63 74 6f 72 53 74 61 74  = [connectorStat
2a80: 65 20 45 58 43 45 50 54 20 21 5b 69 5d 20 3d 20  e EXCEPT ![i] =
2a90: 43 5f 50 72 6f 70 6f 73 65 64 5d 0a 20 20 20 20  C_Proposed].
2aa0: 2f 5c 20 52 65 70 6c 79 28 5b 6d 74 79 70 65 20  /\ Reply([mtype
2ab0: 20 20 20 7c 2d 3e 20 53 75 62 70 61 79 6d 65 6e     |-> Subpaymen
2ac0: 74 50 72 6f 70 6f 73 61 6c 52 65 73 70 6f 6e 73  tProposalRespons
2ad0: 65 2c 0a 20 20 20 20 20 20 20 20 20 20 20 20 20  e,.
2ae0: 20 6d 73 6f 75 72 63 65 20 20 7c 2d 3e 20 69 2c   msource  |-> i,
2af0: 0a 20 20 20 20 20 20 20 20 20 20 20 20 20 20 6d  .              m
2b00: 64 65 73 74 20 20 20 20 7c 2d 3e 20 6a 5d 2c 20  dest    |-> j],
2b10: 6d 29 0a 20 20 20 20 2f 5c 20 55 4e 43 48 41 4e  m).    /\ UNCHAN
2b20: 47 45 44 20 3c 3c 73 65 6e 64 65 72 56 61 72 73  GED <<senderVars
2b30: 2c 20 6c 65 64 67 65 72 56 61 72 73 3e 3e 0a 0a  , ledgerVars>>..
2b40: 5c 2a 20 4c 65 64 67 65 72 20 6a 20 6e 6f 74 69  \* Ledger j noti
2b50: 66 69 65 73 20 63 6f 6e 6e 65 63 74 6f 72 20 69  fies connector i
2b60: 20 74 68 61 74 20 74 68 65 20 74 72 61 6e 73 66   that the transf
2b70: 65 72 20 69 73 20 70 72 65 70 61 72 65 64 0a 43  er is prepared.C
2b80: 6f 6e 6e 65 63 74 6f 72 48 61 6e 64 6c 65 50 72  onnectorHandlePr
2b90: 65 70 61 72 65 4e 6f 74 69 66 79 28 69 2c 20 6a  epareNotify(i, j
2ba0: 2c 20 6d 29 20 3d 3d 0a 20 20 20 20 5c 2f 20 2f  , m) ==.    \/ /
2bb0: 5c 20 52 65 70 6c 79 28 5b 6d 74 79 70 65 20 20  \ Reply([mtype
2bc0: 20 7c 2d 3e 20 50 72 65 70 61 72 65 52 65 71 75   |-> PrepareRequ
2bd0: 65 73 74 2c 0a 20 20 20 20 20 20 20 20 20 20 20  est,.
2be0: 20 20 20 20 20 20 6d 73 6f 75 72 63 65 20 7c 2d        msource |-
2bf0: 3e 20 69 2c 0a 20 20 20 20 20 20 20 20 20 20 20  > i,.
2c00: 20 20 20 20 20 20 6d 64 65 73 74 20 20 20 7c 2d        mdest   |-
2c10: 3e 20 69 2b 31 5d 2c 20 6d 29 0a 20 20 20 20 20  > i+1], m).
2c20: 20 20 2f 5c 20 55 4e 43 48 41 4e 47 45 44 20 3c    /\ UNCHANGED <
2c30: 3c 73 65 6e 64 65 72 56 61 72 73 2c 20 63 6f 6e  <senderVars, con
2c40: 6e 65 63 74 6f 72 56 61 72 73 2c 20 6c 65 64 67  nectorVars, ledg
2c50: 65 72 56 61 72 73 3e 3e 0a 0a 5c 2a 20 4c 65 64  erVars>>..\* Led
2c60: 67 65 72 20 6a 20 6e 6f 74 69 66 69 65 73 20 63  ger j notifies c
2c70: 6f 6e 6e 65 63 74 6f 72 20 69 20 74 68 61 74 20  onnector i that
2c80: 74 68 65 20 74 72 61 6e 73 66 65 72 20 69 73 20  the transfer is
2c90: 65 78 65 63 75 74 65 64 0a 43 6f 6e 6e 65 63 74  executed.Connect
2ca0: 6f 72 48 61 6e 64 6c 65 45 78 65 63 75 74 65 4e  orHandleExecuteN
2cb0: 6f 74 69 66 79 28 69 2c 20 6a 2c 20 6d 29 20 3d  otify(i, j, m) =
2cc0: 3d 0a 20 20 20 20 2f 5c 20 52 65 70 6c 79 28 5b  =.    /\ Reply([
2cd0: 6d 74 79 70 65 20 20 20 20 7c 2d 3e 20 45 78 65  mtype    |-> Exe
2ce0: 63 75 74 65 52 65 71 75 65 73 74 2c 0a 20 20 20  cuteRequest,.
2cf0: 20 20 20 20 20 20 20 20 20 20 20 6d 73 6f 75 72             msour
2d00: 63 65 20 20 7c 2d 3e 20 69 2c 0a 20 20 20 20 20  ce  |-> i,.
2d10: 20 20 20 20 20 20 20 20 20 6d 64 65 73 74 20 20           mdest
2d20: 20 20 7c 2d 3e 20 69 2d 31 2c 0a 20 20 20 20 20    |-> i-1,.
2d30: 20 20 20 20 20 20 20 20 20 6d 72 65 63 65 69 70           mreceip
2d40: 74 20 7c 2d 3e 20 6d 2e 6d 72 65 63 65 69 70 74  t |-> m.mreceipt
2d50: 5d 2c 20 6d 29 0a 20 20 20 20 2f 5c 20 55 4e 43  ], m).    /\ UNC
2d60: 48 41 4e 47 45 44 20 3c 3c 73 65 6e 64 65 72 56  HANGED <<senderV
2d70: 61 72 73 2c 20 63 6f 6e 6e 65 63 74 6f 72 56 61  ars, connectorVa
2d80: 72 73 2c 20 6c 65 64 67 65 72 56 61 72 73 3e 3e  rs, ledgerVars>>
2d90: 0a 0a 5c 2a 20 4c 65 64 67 65 72 20 6a 20 6e 6f  ..\* Ledger j no
2da0: 74 69 66 69 65 73 20 63 6f 6e 6e 65 63 74 6f 72  tifies connector
2db0: 20 69 20 74 68 61 74 20 74 68 65 20 74 72 61 6e   i that the tran
2dc0: 73 66 65 72 20 69 73 20 61 62 6f 72 74 65 64 0a  sfer is aborted.
2dd0: 43 6f 6e 6e 65 63 74 6f 72 48 61 6e 64 6c 65 41  ConnectorHandleA
2de0: 62 6f 72 74 4e 6f 74 69 66 79 28 69 2c 20 6a 2c  bortNotify(i, j,
2df0: 20 6d 29 20 3d 3d 0a 20 20 20 20 2f 5c 20 44 69   m) ==.    /\ Di
2e00: 73 63 61 72 64 28 6d 29 0a 20 20 20 20 2f 5c 20  scard(m).    /\
2e10: 55 4e 43 48 41 4e 47 45 44 20 3c 3c 73 65 6e 64  UNCHANGED <<send
2e20: 65 72 56 61 72 73 2c 20 63 6f 6e 6e 65 63 74 6f  erVars, connecto
2e30: 72 56 61 72 73 2c 20 6c 65 64 67 65 72 56 61 72  rVars, ledgerVar
2e40: 73 3e 3e 0a 0a 5c 2a 20 43 6f 6e 6e 65 63 74 6f  s>>..\* Connecto
2e50: 72 20 72 65 63 65 69 76 65 73 20 61 20 6d 65 73  r receives a mes
2e60: 73 61 67 65 0a 43 6f 6e 6e 65 63 74 6f 72 52 65  sage.ConnectorRe
2e70: 63 65 69 76 65 28 69 2c 20 6a 2c 20 6d 29 20 3d  ceive(i, j, m) =
2e80: 3d 0a 20 20 20 20 5c 2f 20 2f 5c 20 6d 2e 6d 74  =.    \/ /\ m.mt
2e90: 79 70 65 20 3d 20 53 75 62 70 61 79 6d 65 6e 74  ype = Subpayment
2ea0: 50 72 6f 70 6f 73 61 6c 52 65 71 75 65 73 74 0a  ProposalRequest.
2eb0: 20 20 20 20 20 20 20 2f 5c 20 43 6f 6e 6e 65 63         /\ Connec
2ec0: 74 6f 72 48 61 6e 64 6c 65 53 75 62 70 61 79 6d  torHandleSubpaym
2ed0: 65 6e 74 50 72 6f 70 6f 73 61 6c 52 65 71 75 65  entProposalReque
2ee0: 73 74 28 69 2c 20 6a 2c 20 6d 29 0a 20 20 20 20  st(i, j, m).
2ef0: 5c 2f 20 2f 5c 20 6d 2e 6d 74 79 70 65 20 3d 20  \/ /\ m.mtype =
2f00: 50 72 65 70 61 72 65 4e 6f 74 69 66 79 0a 20 20  PrepareNotify.
2f10: 20 20 20 20 20 2f 5c 20 43 6f 6e 6e 65 63 74 6f       /\ Connecto
2f20: 72 48 61 6e 64 6c 65 50 72 65 70 61 72 65 4e 6f  rHandlePrepareNo
2f30: 74 69 66 79 28 69 2c 20 6a 2c 20 6d 29 0a 20 20  tify(i, j, m).
2f40: 20 20 5c 2f 20 2f 5c 20 6d 2e 6d 74 79 70 65 20    \/ /\ m.mtype
2f50: 3d 20 45 78 65 63 75 74 65 4e 6f 74 69 66 79 0a  = ExecuteNotify.
2f60: 20 20 20 20 20 20 20 2f 5c 20 43 6f 6e 6e 65 63         /\ Connec
2f70: 74 6f 72 48 61 6e 64 6c 65 45 78 65 63 75 74 65  torHandleExecute
2f80: 4e 6f 74 69 66 79 28 69 2c 20 6a 2c 20 6d 29 0a  Notify(i, j, m).
2f90: 20 20 20 20 5c 2f 20 2f 5c 20 6d 2e 6d 74 79 70      \/ /\ m.mtyp
2fa0: 65 20 3d 20 41 62 6f 72 74 4e 6f 74 69 66 79 0a  e = AbortNotify.
2fb0: 20 20 20 20 20 20 20 2f 5c 20 43 6f 6e 6e 65 63         /\ Connec
2fc0: 74 6f 72 48 61 6e 64 6c 65 41 62 6f 72 74 4e 6f  torHandleAbortNo
2fd0: 74 69 66 79 28 69 2c 20 6a 2c 20 6d 29 0a 0a 5c  tify(i, j, m)..\
2fe0: 2a 20 52 65 63 65 69 76 65 20 61 20 6d 65 73 73  * Receive a mess
2ff0: 61 67 65 0a 52 65 63 65 69 76 65 28 6d 29 20 3d  age.Receive(m) =
3000: 3d 0a 20 20 20 20 4c 45 54 20 69 20 3d 3d 20 6d  =.    LET i == m
3010: 2e 6d 64 65 73 74 0a 20 20 20 20 20 20 20 20 6a  .mdest.        j
3020: 20 3d 3d 20 6d 2e 6d 73 6f 75 72 63 65 0a 20 20   == m.msource.
3030: 20 20 49 4e 20 5c 2f 20 2f 5c 20 69 20 5c 69 6e    IN \/ /\ i \in
3040: 20 4c 65 64 67 65 72 0a 20 20 20 20 20 20 20 20   Ledger.
3050: 20 20 2f 5c 20 4c 65 64 67 65 72 52 65 63 65 69    /\ LedgerRecei
3060: 76 65 28 69 2c 20 6a 2c 20 6d 29 0a 20 20 20 20  ve(i, j, m).
3070: 20 20 20 5c 2f 20 2f 5c 20 69 20 3d 20 53 65 6e     \/ /\ i = Sen
3080: 64 65 72 0a 20 20 20 20 20 20 20 20 20 20 2f 5c  der.          /\
3090: 20 53 65 6e 64 65 72 52 65 63 65 69 76 65 28 69   SenderReceive(i
30a0: 2c 20 6a 2c 20 6d 29 0a 20 20 20 20 20 20 20 5c  , j, m).       \
30b0: 2f 20 2f 5c 20 69 20 3d 20 52 65 63 69 70 69 65  / /\ i = Recipie
30c0: 6e 74 0a 20 20 20 20 20 20 20 20 20 20 2f 5c 20  nt.          /\
30d0: 52 65 63 69 70 69 65 6e 74 52 65 63 65 69 76 65  RecipientReceive
30e0: 28 69 2c 20 6a 2c 20 6d 29 0a 20 20 20 20 20 20  (i, j, m).
30f0: 20 5c 2f 20 2f 5c 20 69 20 5c 69 6e 20 43 6f 6e   \/ /\ i \in Con
3100: 6e 65 63 74 6f 72 0a 20 20 20 20 20 20 20 20 20  nector.
3110: 20 2f 5c 20 43 6f 6e 6e 65 63 74 6f 72 52 65 63   /\ ConnectorRec
3120: 65 69 76 65 28 69 2c 20 6a 2c 20 6d 29 0a 0a 5c  eive(i, j, m)..\
3130: 2a 20 45 6e 64 20 6f 66 20 6d 65 73 73 61 67 65  * End of message
3140: 20 68 61 6e 64 6c 65 72 73 0a 2d 2d 2d 2d 0a 5c   handlers.----.\
3150: 2a 20 44 65 66 69 6e 65 73 20 68 6f 77 20 74 68  * Defines how th
3160: 65 20 76 61 72 69 61 62 6c 65 73 20 6d 61 79 20  e variables may
3170: 74 72 61 6e 73 69 74 69 6f 6e 0a 0a 54 65 72 6d  transition..Term
3180: 69 6e 61 74 69 6f 6e 20 3d 3d 0a 20 20 20 20 2f  ination ==.    /
3190: 5c 20 5c 41 20 6c 20 5c 69 6e 20 4c 65 64 67 65  \ \A l \in Ledge
31a0: 72 20 3a 20 49 73 46 69 6e 61 6c 4c 65 64 67 65  r : IsFinalLedge
31b0: 72 53 74 61 74 65 28 6c 65 64 67 65 72 53 74 61  rState(ledgerSta
31c0: 74 65 5b 6c 5d 29 0a 20 20 20 20 2f 5c 20 73 65  te[l]).    /\ se
31d0: 6e 64 65 72 53 74 61 74 65 20 3d 20 53 5f 44 6f  nderState = S_Do
31e0: 6e 65 0a 20 20 20 20 2f 5c 20 55 4e 43 48 41 4e  ne.    /\ UNCHAN
31f0: 47 45 44 20 76 61 72 73 0a 0a 4e 65 78 74 20 3d  GED vars..Next =
3200: 3d 20 5c 2f 20 2f 5c 20 5c 2f 20 53 74 61 72 74  = \/ /\ \/ Start
3210: 50 72 6f 70 6f 73 61 6c 50 68 61 73 65 28 53 65  ProposalPhase(Se
3220: 6e 64 65 72 29 0a 20 20 20 20 20 20 20 20 20 20  nder).
3230: 20 20 20 20 5c 2f 20 53 74 61 72 74 50 72 65 70      \/ StartPrep
3240: 61 72 61 74 69 6f 6e 50 68 61 73 65 28 53 65 6e  arationPhase(Sen
3250: 64 65 72 29 0a 20 20 20 20 20 20 20 20 20 20 20  der).
3260: 20 20 20 5c 2f 20 5c 45 20 6c 20 5c 69 6e 20 4c     \/ \E l \in L
3270: 65 64 67 65 72 20 3a 20 4c 65 64 67 65 72 41 62  edger : LedgerAb
3280: 6f 72 74 28 6c 29 0a 20 20 20 20 20 20 20 20 20  ort(l).
3290: 20 20 20 20 20 5c 2f 20 5c 45 20 6c 20 5c 69 6e       \/ \E l \in
32a0: 20 4c 65 64 67 65 72 20 3a 20 4c 65 64 67 65 72   Ledger : Ledger
32b0: 54 69 6d 65 6f 75 74 28 6c 29 0a 20 20 20 20 20  Timeout(l).
32c0: 20 20 20 20 20 20 20 20 20 5c 2f 20 5c 45 20 6d           \/ \E m
32d0: 20 5c 69 6e 20 44 4f 4d 41 49 4e 20 6d 65 73 73   \in DOMAIN mess
32e0: 61 67 65 73 20 3a 20 52 65 63 65 69 76 65 28 6d  ages : Receive(m
32f0: 29 0a 20 20 20 20 20 20 20 20 20 20 20 20 20 20  ).
3300: 5c 2f 20 4e 6f 74 68 69 6e 67 48 61 70 70 65 6e  \/ NothingHappen
3310: 73 0a 20 20 20 20 20 20 20 20 20 20 20 2f 5c 20  s.           /\
3320: 63 6c 6f 63 6b 27 20 3d 20 63 6c 6f 63 6b 20 2b  clock' = clock +
3330: 20 31 0a 20 20 20 20 20 20 20 20 5c 2f 20 54 65   1.        \/ Te
3340: 72 6d 69 6e 61 74 69 6f 6e 0a 0a 5c 2a 20 54 68  rmination..\* Th
3350: 65 20 73 70 65 63 69 66 69 63 61 74 69 6f 6e 20  e specification
3360: 6d 75 73 74 20 73 74 61 72 74 20 77 69 74 68 20  must start with
3370: 74 68 65 20 69 6e 69 74 69 61 6c 20 73 74 61 74  the initial stat
3380: 65 20 61 6e 64 20 74 72 61 6e 73 69 74 69 6f 6e  e and transition
3390: 20 61 63 63 6f 72 64 69 6e 67 0a 5c 2a 20 74 6f   according.\* to
33a0: 20 4e 65 78 74 2e 0a 53 70 65 63 20 3d 3d 20 49   Next..Spec == I
33b0: 6e 69 74 20 2f 5c 20 5b 5d 5b 4e 65 78 74 5d 5f  nit /\ [][Next]_
33c0: 76 61 72 73 0a 0a 3d 3d 3d 3d 3d 3d 3d 3d 3d 3d  vars..==========
33d0: 3d 3d 3d 3d 3d 3d 3d 3d 3d 3d 3d 3d 3d 3d 3d 3d  ================
33e0: 3d 3d 3d 3d 3d 3d 3d 3d 3d 3d 3d 3d 3d 3d 3d 3d  ================
33f0: 3d 3d 3d 3d 3d 3d 3d 3d 3d 3d 3d 3d 3d 3d 3d 3d  ================
3400: 3d 3d 3d 3d 3d 3d 3d 3d 3d 3d 3d 3d 3d 3d 3d 3d  ================
3410: 3d 3d 3d 0a                                      ===.
`