<!-- canonical: https://efficientnewlanguage.org/eml-p/projects/P119-two-phase-commit/ | updated: 2026-10-16 -->

# P119 Two-phase commit

A coordinator and its participants as state machines, the coordinator crashing after any step: wait, ask peers, presume abort and presume commit at every crash point, with the time each participant's data stays locked in doubt.

EML-P project `projects/two-phase-commit` in the EML language repo: 2 module(s), entry `main.eml`, terminal UI. There, `eml project run projects/two-phase-commit` runs it and `eml project verify projects/two-phase-commit` replays every session under CPython (two hash seeds) and in the interpreter; the site build replays every session in the interpreter again and publishes a session only if its screen matches.

Built on verified corpus cases: two-phase-commit-window (https://efficientnewlanguage.org/cases/259-two-phase-commit-window/).

## Sessions

### bad-input - interpreter: byte-equal to the golden

Input:

```text
0
x
2

2
fast
2
wait

2
wait
8
2
wait
x
2
wait
-1
4

4
yes
4
yes yes yes yes yes
4
yes maybe
4
YES yes
5

5
0
5
10
5
x
5
5

5
5
0
5
5
31
5
5
sometime
6
```

Screen:

```text
== Two-phase commit ==
A coordinator asks every participant to prepare, logs commit only if all vote yes, then tells each one. A participant that voted yes waits in doubt, its data locked, until it hears.

1) the transaction  2) one run  3) every crash point  4) votes  5) timing  6) quit
choice> 0
Pick a number from 1 to 6.

1) the transaction  2) one run  3) every crash point  4) votes  5) timing  6) quit
choice> x
Pick a number from 1 to 6.

1) the transaction  2) one run  3) every crash point  4) votes  5) timing  6) quit
choice> 2
strategy (wait, ask peers, presume abort or presume commit)> 
Cancelled.

1) the transaction  2) one run  3) every crash point  4) votes  5) timing  6) quit
choice> 2
strategy (wait, ask peers, presume abort or presume commit)> fast
Type wait, ask peers, presume abort or presume commit.

1) the transaction  2) one run  3) every crash point  4) votes  5) timing  6) quit
choice> 2
strategy (wait, ask peers, presume abort or presume commit)> wait
crash after step (0 to 7, or none)> 
Cancelled.

1) the transaction  2) one run  3) every crash point  4) votes  5) timing  6) quit
choice> 2
strategy (wait, ask peers, presume abort or presume commit)> wait
crash after step (0 to 7, or none)> 8
Type a step from 0 to 7, or none.

1) the transaction  2) one run  3) every crash point  4) votes  5) timing  6) quit
choice> 2
strategy (wait, ask peers, presume abort or presume commit)> wait
crash after step (0 to 7, or none)> x
Type a step from 0 to 7, or none.

1) the transaction  2) one run  3) every crash point  4) votes  5) timing  6) quit
choice> 2
strategy (wait, ask peers, presume abort or presume commit)> wait
crash after step (0 to 7, or none)> -1
Type a step from 0 to 7, or none.

1) the transaction  2) one run  3) every crash point  4) votes  5) timing  6) quit
choice> 4
votes (2 to 4 of yes or no, such as yes yes no)> 
Cancelled.

1) the transaction  2) one run  3) every crash point  4) votes  5) timing  6) quit
choice> 4
votes (2 to 4 of yes or no, such as yes yes no)> yes
Type 2 to 4 votes, each yes or no.

1) the transaction  2) one run  3) every crash point  4) votes  5) timing  6) quit
choice> 4
votes (2 to 4 of yes or no, such as yes yes no)> yes yes yes yes yes
Type 2 to 4 votes, each yes or no.

1) the transaction  2) one run  3) every crash point  4) votes  5) timing  6) quit
choice> 4
votes (2 to 4 of yes or no, such as yes yes no)> yes maybe
Type 2 to 4 votes, each yes or no.

1) the transaction  2) one run  3) every crash point  4) votes  5) timing  6) quit
choice> 4
votes (2 to 4 of yes or no, such as yes yes no)> YES yes
Type 2 to 4 votes, each yes or no.

1) the transaction  2) one run  3) every crash point  4) votes  5) timing  6) quit
choice> 5
in doubt for how long before acting (1 to 9 ticks)> 
Cancelled.

1) the transaction  2) one run  3) every crash point  4) votes  5) timing  6) quit
choice> 5
in doubt for how long before acting (1 to 9 ticks)> 0
Type a whole number from 1 to 9.

1) the transaction  2) one run  3) every crash point  4) votes  5) timing  6) quit
choice> 5
in doubt for how long before acting (1 to 9 ticks)> 10
Type a whole number from 1 to 9.

1) the transaction  2) one run  3) every crash point  4) votes  5) timing  6) quit
choice> 5
in doubt for how long before acting (1 to 9 ticks)> x
Type a whole number from 1 to 9.

1) the transaction  2) one run  3) every crash point  4) votes  5) timing  6) quit
choice> 5
in doubt for how long before acting (1 to 9 ticks)> 5
coordinator back after (1 to 30 ticks, or never)> 
Cancelled.

1) the transaction  2) one run  3) every crash point  4) votes  5) timing  6) quit
choice> 5
in doubt for how long before acting (1 to 9 ticks)> 5
coordinator back after (1 to 30 ticks, or never)> 0
Type a whole number from 1 to 30, or never.

1) the transaction  2) one run  3) every crash point  4) votes  5) timing  6) quit
choice> 5
in doubt for how long before acting (1 to 9 ticks)> 5
coordinator back after (1 to 30 ticks, or never)> 31
Type a whole number from 1 to 30, or never.

1) the transaction  2) one run  3) every crash point  4) votes  5) timing  6) quit
choice> 5
in doubt for how long before acting (1 to 9 ticks)> 5
coordinator back after (1 to 30 ticks, or never)> sometime
Type a whole number from 1 to 30, or never.

1) the transaction  2) one run  3) every crash point  4) votes  5) timing  6) quit
choice> 6
Bye.
```

### basic - interpreter: byte-equal to the golden

Input:

```text
1
3
2
wait
3
2
presume abort
4
2
ask peers
2
2
ask peers
4
5
5
never
3
2
ask peers
3
4
yes no yes yes
2
presume commit
1
3
4
yes yes yes
5
3
10
3
2
presume abort
none
6
```

Screen:

```text
== Two-phase commit ==
A coordinator asks every participant to prepare, logs commit only if all vote yes, then tells each one. A participant that voted yes waits in doubt, its data locked, until it hears.

1) the transaction  2) one run  3) every crash point  4) votes  5) timing  6) quit
choice> 1
Participants P1, P2 and P3 vote yes, yes and yes.
With no crash, the coordinator takes 7 steps, one a tick: 1 prepare P1, 2 prepare P2, 3 prepare P3, 4 log commit, 5 tell P1, 6 tell P2, 7 tell P3.
A participant in doubt for 5 ticks acts on its strategy; a crashed coordinator is back after 10 ticks.

1) the transaction  2) one run  3) every crash point  4) votes  5) timing  6) quit
choice> 3
Every crash point, votes yes, yes and yes; a participant in doubt acts after 5 ticks; the coordinator is back after 10 ticks:
  crash after                 wait       ask peers  presume abort  presume commit
  none                        c c c      c c c      c c c          c c c
  0 before any step           - - -      - - -      - - -          - - -
  1 prepare P1                a - -      a a -      a - -          c - - !
  2 prepare P2                a a -      a a a      a a -          c c - !
  3 prepare P3                a a a      a a a      a a a          c c c !
  4 log commit                c c c      c c c      a a a !        c c c
  5 tell P1                   c c c      c c c      c a a !        c c c
  6 tell P2                   c c c      c c c      c c a !        c c c
  7 tell P3                   c c c      c c c      c c c          c c c
  c committed, a aborted, ? still in doubt at tick 40, - never asked; ! wrong: split, against the coordinator, or committed without every yes.
  wait:           wrong at 0 of 9 crash points, still in doubt at 0, data locked at most 17 ticks.
  ask peers:      wrong at 0 of 9 crash points, still in doubt at 0, data locked at most 14 ticks.
  presume abort:  wrong at 3 of 9 crash points, still in doubt at 0, data locked at most 5 ticks.
  presume commit: wrong at 3 of 9 crash points, still in doubt at 0, data locked at most 5 ticks.
Every pattern of 3 votes, each with every crash point and none:
  strategy          runs  wrong  in doubt at the end  most ticks locked
  wait                45      0                    0                 17
  ask peers           45      0                    0                 14
  presume abort       45      3                    0                  5
  presume commit      45     14                    0                  5

1) the transaction  2) one run  3) every crash point  4) votes  5) timing  6) quit
choice> 2
strategy (wait, ask peers, presume abort or presume commit)> wait
crash after step (0 to 7, or none)> 3
wait, the coordinator crashing after step 3 (it is back after 10 ticks):
  tick  1  prepare P1: it votes yes and locks its data
  tick  2  prepare P2: it votes yes and locks its data
  tick  3  prepare P3: it votes yes and locks its data
  tick  3  the coordinator crashes
  tick  6  P1 in doubt: waits, its data locked
  tick  7  P2 in doubt: waits, its data locked
  tick  8  P3 in doubt: waits, its data locked
  tick 14  the coordinator is back; with no decision logged, it decides abort
  tick 15  tell P1 abort: it aborts and unlocks
  tick 16  tell P2 abort: it aborts and unlocks
  tick 17  tell P3 abort: it aborts and unlocks
  P1 aborted at tick 15, its data locked for 14 ticks.
  P2 aborted at tick 16, its data locked for 14 ticks.
  P3 aborted at tick 17, its data locked for 14 ticks.
Atomic: everyone who finished aborted, as the coordinator logged.

1) the transaction  2) one run  3) every crash point  4) votes  5) timing  6) quit
choice> 2
strategy (wait, ask peers, presume abort or presume commit)> presume abort
crash after step (0 to 7, or none)> 4
presume abort, the coordinator crashing after step 4 (it is back after 10 ticks):
  tick  1  prepare P1: it votes yes and locks its data
  tick  2  prepare P2: it votes yes and locks its data
  tick  3  prepare P3: it votes yes and locks its data
  tick  4  the coordinator logs commit
  tick  4  the coordinator crashes
  tick  6  P1 in doubt: presumes abort and unlocks
  tick  7  P2 in doubt: presumes abort and unlocks
  tick  8  P3 in doubt: presumes abort and unlocks
  tick 15  the coordinator is back with commit logged, and tells everyone again
  tick 16  tell P1 commit: but it had already aborted
  tick 17  tell P2 commit: but it had already aborted
  tick 18  tell P3 commit: but it had already aborted
  P1 aborted at tick 6, its data locked for 5 ticks.
  P2 aborted at tick 7, its data locked for 5 ticks.
  P3 aborted at tick 8, its data locked for 5 ticks.
Against the coordinator, which logged commit: P1, P2 and P3 aborted.

1) the transaction  2) one run  3) every crash point  4) votes  5) timing  6) quit
choice> 2
strategy (wait, ask peers, presume abort or presume commit)> ask peers
crash after step (0 to 7, or none)> 2
ask peers, the coordinator crashing after step 2 (it is back after 10 ticks):
  tick  1  prepare P1: it votes yes and locks its data
  tick  2  prepare P2: it votes yes and locks its data
  tick  2  the coordinator crashes
  tick  6  P3, never asked, aborts on its own
  tick  6  P1 in doubt: asks P3, and aborts too
  tick  7  P2 in doubt: asks P1, which has aborted, and aborts too
  tick 13  the coordinator is back; with no decision logged, it decides abort
  tick 14  tell P1 abort: it had already aborted
  tick 15  tell P2 abort: it had already aborted
  P1 aborted at tick 6, its data locked for 5 ticks.
  P2 aborted at tick 7, its data locked for 5 ticks.
  P3 aborted at tick 6, never locked.
Atomic: everyone who finished aborted, as the coordinator logged.

1) the transaction  2) one run  3) every crash point  4) votes  5) timing  6) quit
choice> 2
strategy (wait, ask peers, presume abort or presume commit)> ask peers
crash after step (0 to 7, or none)> 4
ask peers, the coordinator crashing after step 4 (it is back after 10 ticks):
  tick  1  prepare P1: it votes yes and locks its data
  tick  2  prepare P2: it votes yes and locks its data
  tick  3  prepare P3: it votes yes and locks its data
  tick  4  the coordinator logs commit
  tick  4  the coordinator crashes
  tick  6  P1 in doubt: asks the others, all in doubt too, so it waits, its data locked
  tick  7  P2 in doubt: asks the others, all in doubt too, so it waits, its data locked
  tick  8  P3 in doubt: asks the others, all in doubt too, so it waits, its data locked
  tick 15  the coordinator is back with commit logged, and tells everyone again
  tick 15  P1 in doubt: asks the coordinator: commit
  tick 15  P2 in doubt: asks the coordinator: commit
  tick 15  P3 in doubt: asks the coordinator: commit
  tick 16  tell P1 commit: it had already committed
  tick 17  tell P2 commit: it had already committed
  tick 18  tell P3 commit: it had already committed
  P1 committed at tick 15, its data locked for 14 ticks.
  P2 committed at tick 15, its data locked for 13 ticks.
  P3 committed at tick 15, its data locked for 12 ticks.
Atomic: everyone who finished committed, as the coordinator logged.

1) the transaction  2) one run  3) every crash point  4) votes  5) timing  6) quit
choice> 5
in doubt for how long before acting (1 to 9 ticks)> 5
coordinator back after (1 to 30 ticks, or never)> never
Participants P1, P2 and P3 vote yes, yes and yes.
With no crash, the coordinator takes 7 steps, one a tick: 1 prepare P1, 2 prepare P2, 3 prepare P3, 4 log commit, 5 tell P1, 6 tell P2, 7 tell P3.
A participant in doubt for 5 ticks acts on its strategy; a crashed coordinator never comes back.

1) the transaction  2) one run  3) every crash point  4) votes  5) timing  6) quit
choice> 3
Every crash point, votes yes, yes and yes; a participant in doubt acts after 5 ticks; the coordinator never comes back:
  crash after                 wait       ask peers  presume abort  presume commit
  none                        c c c      c c c      c c c          c c c
  0 before any step           - - -      - - -      - - -          - - -
  1 prepare P1                ? - -      a a -      a - -          c - - !
  2 prepare P2                ? ? -      a a a      a a -          c c - !
  3 prepare P3                ? ? ?      ? ? ?      a a a          c c c
  4 log commit                ? ? ?      ? ? ?      a a a !        c c c
  5 tell P1                   c ? ?      c c c      c a a !        c c c
  6 tell P2                   c c ?      c c c      c c a !        c c c
  7 tell P3                   c c c      c c c      c c c          c c c
  c committed, a aborted, ? still in doubt at tick 40, - never asked; ! wrong: split, against the coordinator, or committed without every yes.
  wait:           wrong at 0 of 9 crash points, still in doubt at 6, data locked at most 39 ticks.
  ask peers:      wrong at 0 of 9 crash points, still in doubt at 2, data locked at most 39 ticks.
  presume abort:  wrong at 3 of 9 crash points, still in doubt at 0, data locked at most 5 ticks.
  presume commit: wrong at 2 of 9 crash points, still in doubt at 0, data locked at most 5 ticks.
Ask peers is still in doubt only at crash points 3 and 4: every participant had voted yes, and none had heard the decision.
Every pattern of 3 votes, each with every crash point and none:
  strategy          runs  wrong  in doubt at the end  most ticks locked
  wait                45      0                   17                 39
  ask peers           45      0                    2                 39
  presume abort       45      3                    0                  5
  presume commit      45     13                    0                  5

1) the transaction  2) one run  3) every crash point  4) votes  5) timing  6) quit
choice> 2
strategy (wait, ask peers, presume abort or presume commit)> ask peers
crash after step (0 to 7, or none)> 3
ask peers, the coordinator crashing after step 3 (it never comes back):
  tick  1  prepare P1: it votes yes and locks its data
  tick  2  prepare P2: it votes yes and locks its data
  tick  3  prepare P3: it votes yes and locks its data
  tick  3  the coordinator crashes
  tick  6  P1 in doubt: asks the others, all in doubt too, so it waits, its data locked
  tick  7  P2 in doubt: asks the others, all in doubt too, so it waits, its data locked
  tick  8  P3 in doubt: asks the others, all in doubt too, so it waits, its data locked
  P1 still in doubt at tick 40, its data locked for 39 ticks.
  P2 still in doubt at tick 40, its data locked for 38 ticks.
  P3 still in doubt at tick 40, its data locked for 37 ticks.
Still in doubt at tick 40, data locked: P1, P2 and P3.

1) the transaction  2) one run  3) every crash point  4) votes  5) timing  6) quit
choice> 4
votes (2 to 4 of yes or no, such as yes yes no)> yes no yes yes
Participants P1, P2, P3 and P4 vote yes, no, yes and yes.
With no crash, the coordinator takes 4 steps, one a tick: 1 prepare P1, 2 prepare P2, 3 log abort, 4 tell P1.
A participant in doubt for 5 ticks acts on its strategy; a crashed coordinator never comes back.

1) the transaction  2) one run  3) every crash point  4) votes  5) timing  6) quit
choice> 2
strategy (wait, ask peers, presume abort or presume commit)> presume commit
crash after step (0 to 4, or none)> 1
presume commit, the coordinator crashing after step 1 (it never comes back):
  tick  1  prepare P1: it votes yes and locks its data
  tick  1  the coordinator crashes
  tick  6  P1 in doubt: presumes commit and unlocks
  P1 committed at tick 6, its data locked for 5 ticks.
  P2 was never asked.
  P3 was never asked.
  P4 was never asked.
Committed without every yes: P1 committed, though P2, P3 and P4 never voted yes.

1) the transaction  2) one run  3) every crash point  4) votes  5) timing  6) quit
choice> 3
Every crash point, votes yes, no, yes and yes; a participant in doubt acts after 5 ticks; the coordinator never comes back:
  crash after                 wait       ask peers  presume abort  presume commit
  none                        a a - -    a a - -    a a - -        a a - -
  0 before any step           - - - -    - - - -    - - - -        - - - -
  1 prepare P1                ? - - -    a a - -    a - - -        c - - - !
  2 prepare P2                ? a - -    a a - -    a a - -        c a - - !
  3 log abort                 ? a - -    a a - -    a a - -        c a - - !
  4 tell P1                   a a - -    a a - -    a a - -        a a - -
  c committed, a aborted, ? still in doubt at tick 40, - never asked; ! wrong: split, against the coordinator, or committed without every yes.
  wait:           wrong at 0 of 6 crash points, still in doubt at 3, data locked at most 39 ticks.
  ask peers:      wrong at 0 of 6 crash points, still in doubt at 0, data locked at most 5 ticks.
  presume abort:  wrong at 0 of 6 crash points, still in doubt at 0, data locked at most 5 ticks.
  presume commit: wrong at 3 of 6 crash points, still in doubt at 0, data locked at most 5 ticks.
Every pattern of 4 votes, each with every crash point and none:
  strategy          runs  wrong  in doubt at the end  most ticks locked
  wait                93      0                   37                 39
  ask peers           93      0                    2                 39
  presume abort       93      4                    0                  5
  presume commit      93     32                    0                  5

1) the transaction  2) one run  3) every crash point  4) votes  5) timing  6) quit
choice> 4
votes (2 to 4 of yes or no, such as yes yes no)> yes yes yes
Participants P1, P2 and P3 vote yes, yes and yes.
With no crash, the coordinator takes 7 steps, one a tick: 1 prepare P1, 2 prepare P2, 3 prepare P3, 4 log commit, 5 tell P1, 6 tell P2, 7 tell P3.
A participant in doubt for 5 ticks acts on its strategy; a crashed coordinator never comes back.

1) the transaction  2) one run  3) every crash point  4) votes  5) timing  6) quit
choice> 5
in doubt for how long before acting (1 to 9 ticks)> 3
coordinator back after (1 to 30 ticks, or never)> 10
Participants P1, P2 and P3 vote yes, yes and yes.
With no crash, the coordinator takes 7 steps, one a tick: 1 prepare P1, 2 prepare P2, 3 prepare P3, 4 log commit, 5 tell P1, 6 tell P2, 7 tell P3.
A participant in doubt for 3 ticks acts on its strategy; a crashed coordinator is back after 10 ticks.

1) the transaction  2) one run  3) every crash point  4) votes  5) timing  6) quit
choice> 3
Every crash point, votes yes, yes and yes; a participant in doubt acts after 3 ticks; the coordinator is back after 10 ticks:
  crash after                 wait       ask peers  presume abort  presume commit
  none                        c c c      c c c      a a a !        c c c
  0 before any step           - - -      - - -      - - -          - - -
  1 prepare P1                a - -      a a -      a - -          c - - !
  2 prepare P2                a a -      a a a      a a -          c c - !
  3 prepare P3                a a a      a a a      a a a          c c c !
  4 log commit                c c c      c c c      a a a !        c c c
  5 tell P1                   c c c      c c c      a a a !        c c c
  6 tell P2                   c c c      c c c      a a a !        c c c
  7 tell P3                   c c c      c c c      a a a !        c c c
  c committed, a aborted, ? still in doubt at tick 40, - never asked; ! wrong: split, against the coordinator, or committed without every yes.
  wait:           wrong at 0 of 9 crash points, still in doubt at 0, data locked at most 17 ticks.
  ask peers:      wrong at 0 of 9 crash points, still in doubt at 0, data locked at most 14 ticks.
  presume abort:  wrong at 5 of 9 crash points, still in doubt at 0, data locked at most 3 ticks.
  presume commit: wrong at 3 of 9 crash points, still in doubt at 0, data locked at most 3 ticks.
Every pattern of 3 votes, each with every crash point and none:
  strategy          runs  wrong  in doubt at the end  most ticks locked
  wait                45      0                    0                 17
  ask peers           45      0                    0                 14
  presume abort       45      5                    0                  3
  presume commit      45     16                    0                  3

1) the transaction  2) one run  3) every crash point  4) votes  5) timing  6) quit
choice> 2
strategy (wait, ask peers, presume abort or presume commit)> presume abort
crash after step (0 to 7, or none)> none
presume abort, no crash:
  tick  1  prepare P1: it votes yes and locks its data
  tick  2  prepare P2: it votes yes and locks its data
  tick  3  prepare P3: it votes yes and locks its data
  tick  4  the coordinator logs commit
  tick  4  P1 in doubt: presumes abort and unlocks
  tick  5  tell P1 commit: but it had already aborted
  tick  5  P2 in doubt: presumes abort and unlocks
  tick  6  tell P2 commit: but it had already aborted
  tick  6  P3 in doubt: presumes abort and unlocks
  tick  7  tell P3 commit: but it had already aborted
  P1 aborted at tick 4, its data locked for 3 ticks.
  P2 aborted at tick 5, its data locked for 3 ticks.
  P3 aborted at tick 6, its data locked for 3 ticks.
Against the coordinator, which logged commit: P1, P2 and P3 aborted.

1) the transaction  2) one run  3) every crash point  4) votes  5) timing  6) quit
choice> 6
Bye.
```

## Modules

### main.eml

```eml
# P119 two-phase commit: one run tick by tick with the coordinator crashing
# after a chosen step, every crash point under four strategies for a
# participant in doubt, and every pattern of votes counted.
import twopc

def plain(s):
    0 => i
    len(s) => j
    while i < j and s[i] == " ":
        i + 1 => i
    while j > i and s[j - 1] == " ":
        j - 1 => j
    return s[i:j]

def pad(s, n):
    s => out
    while len(out) < n:
        out + " " => out
    return out

def lpad(s, n):
    s => out
    while len(out) < n:
        " " + out => out
    return out

def is_digits(s):
    if len(s) == 0:
        return False
    for c in s:
        if c < "0" or c > "9":
            return False
    return True

def ticks_text(n):
    if n == 1:
        return "1 tick"
    return str(n) + " ticks"

def names_text(ns):
    "" => out
    for i in [0:len(ns) - 1]:
        if i > 0 and i == len(ns) - 1:
            out + " and " => out
        elif i > 0:
            out + ", " => out
        out + ns[i] => out
    return out

def votes_text(votes):
    [] => out
    for v in votes:
        if v:
            out + ["yes"] => out
        else:
            out + ["no"] => out
    return out

def back_text(back):
    if back == 0:
        return "never comes back"
    return "is back after " + ticks_text(back)

def show(votes, timeout, back):
    [] => ps
    for i in [0:len(votes) - 1]:
        ps + [twopc.name(i)] => ps
    ("Participants " + names_text(ps) + " vote " + names_text(votes_text(votes)) + ".") ^0
    twopc.run(votes, "wait", timeout, back, 0 - 1, 40) => r
    "" => line
    for k in [0:len(r[7]) - 1]:
        if line != "":
            line + ", " => line
        line + str(k + 1) + " " + r[7][k] => line
    ("With no crash, the coordinator takes " + str(r[5]) + " steps, one a tick: " + line + ".") ^0
    ("A participant in doubt for " + ticks_text(timeout) + " acts on its strategy; a crashed coordinator " + back_text(back) + ".") ^0

def ask_strategy():
    plain(input("strategy (wait, ask peers, presume abort or presume commit)> ")) => s
    if s == "":
        "Cancelled." ^0
        return ""
    for x in twopc.strategies():
        if x == s:
            return s
    "Type wait, ask peers, presume abort or presume commit." ^0
    return ""

def verdict(r):
    twopc.outcome(r) => o
    [] => c
    [] => a
    [] => d
    for i in [0:len(r[1]) - 1]:
        if r[1][i] == "committed":
            c + [twopc.name(i)] => c
        elif r[1][i] == "aborted":
            a + [twopc.name(i)] => a
        elif r[1][i] == "prepared":
            d + [twopc.name(i)] => d
    if o[0]:
        ("Split: " + names_text(c) + " committed, and " + names_text(a) + " aborted.") ^0
    if o[1]:
        [] => wrong
        for i in [0:len(r[1]) - 1]:
            if (r[1][i] == "committed" or r[1][i] == "aborted") and r[1][i] != twopc.past(r[4]):
                wrong + [twopc.name(i)] => wrong
        ("Against the coordinator, which logged " + r[4] + ": " + names_text(wrong) + " " + opposite(r[4]) + ".") ^0
    if o[3]:
        [] => never
        for i in [0:len(r[1]) - 1]:
            if r[8][i] < 0:
                never + [twopc.name(i)] => never
        ("Committed without every yes: " + names_text(c) + " committed, though " + names_text(never) + " never voted yes.") ^0
    if o[2]:
        ("Still in doubt at tick 40, data locked: " + names_text(d) + ".") ^0
    if len(c) == 0 and len(a) == 0 and len(d) == 0:
        if r[4] == "":
            "No participant was asked, and the coordinator never logged a decision." ^0
        else:
            ("No participant was asked; the coordinator logged " + r[4] + ".") ^0
    elif not twopc.wrong(o) and not o[2]:
        "aborted" => common
        if len(c) > 0:
            "committed" => common
        if r[4] == "":
            ("Atomic: everyone who finished " + common + ", and the coordinator never logged a decision.") ^0
        else:
            ("Atomic: everyone who finished " + common + ", as the coordinator logged.") ^0

def opposite(d):
    if d == "commit":
        return "aborted"
    return "committed"

def one_run(votes, timeout, back):
    ask_strategy() => s
    if s == "":
        return
    twopc.crash_points(votes, timeout, back, 40) => n
    plain(input("crash after step (0 to " + str(n) + ", or none)> ")) => t
    if t == "":
        "Cancelled." ^0
        return
    0 - 1 => crash
    if t != "none":
        if not is_digits(t) or len(t) > 2 or int(t) > n:
            ("Type a step from 0 to " + str(n) + ", or none.") ^0
            return
        int(t) => crash
    twopc.run(votes, s, timeout, back, crash, 40) => r
    if crash < 0:
        (s + ", no crash:") ^0
    else:
        (s + ", the coordinator crashing after step " + str(crash) + " (it " + back_text(back) + "):") ^0
    for e in r[0]:
        ("  tick " + lpad(str(e[0]), 2) + "  " + e[1]) ^0
    for i in [0:len(votes) - 1]:
        twopc.name(i) => p
        r[1][i] => st
        if st == "prepared":
            ("  " + p + " still in doubt at tick 40, its data locked for " + ticks_text(r[2][i]) + ".") ^0
        elif st == "idle":
            ("  " + p + " was never asked.") ^0
        elif r[2][i] == 0:
            ("  " + p + " " + st + " at tick " + str(r[6][i]) + ", never locked.") ^0
        else:
            ("  " + p + " " + st + " at tick " + str(r[6][i]) + ", its data locked for " + ticks_text(r[2][i]) + ".") ^0
    verdict(r)

def every(votes, timeout, back):
    twopc.crash_points(votes, timeout, back, 40) => n
    twopc.run(votes, "wait", timeout, back, 0 - 1, 40)[7] => labels
    ("Every crash point, votes " + names_text(votes_text(votes)) + "; a participant in doubt acts after " + ticks_text(timeout) + "; the coordinator " + back_text(back) + ":") ^0
    [9, 9, 13, 14] => widths
    "  " + pad("crash after", 26) => head
    for k in [0:3]:
        head + "  " + pad(twopc.strategies()[k], widths[k]) => head
    rstrip(head) ^0
    [0, 0, 0, 0] => wrong
    [0, 0, 0, 0] => doubt
    [0, 0, 0, 0] => most
    [] => stuck
    for c in [0 - 1:n]:
        "none" => label
        if c == 0:
            "0 before any step" => label
        elif c > 0:
            str(c) + " " + labels[c - 1] => label
        "  " + pad(label, 26) => line
        for k in [0:3]:
            twopc.run(votes, twopc.strategies()[k], timeout, back, c, 40) => r
            twopc.outcome(r) => o
            twopc.letters(r) => cell
            if twopc.wrong(o):
                cell + " !" => cell
                wrong[k] + 1 => wrong[k]
            if o[2]:
                doubt[k] + 1 => doubt[k]
                if k == 1:
                    stuck + [str(c)] => stuck
            for x in r[2]:
                if x > most[k]:
                    x => most[k]
            line + "  " + pad(cell, widths[k]) => line
        rstrip(line) ^0
    "  c committed, a aborted, ? still in doubt at tick 40, - never asked; ! wrong: split, against the coordinator, or committed without every yes." ^0
    for k in [0:3]:
        ("  " + pad(twopc.strategies()[k] + ":", 16) + "wrong at " + str(wrong[k]) + " of " + str(n + 2) + " crash points, still in doubt at " + str(doubt[k]) + ", data locked at most " + ticks_text(most[k]) + ".") ^0
    if len(stuck) == 1:
        ("Ask peers is still in doubt only at crash point " + stuck[0] + ": every participant had voted yes, and none had heard the decision.") ^0
    elif len(stuck) > 1:
        ("Ask peers is still in doubt only at crash points " + names_text(stuck) + ": every participant had voted yes, and none had heard the decision.") ^0
    ("Every pattern of " + str(len(votes)) + " votes, each with every crash point and none:") ^0
    "  strategy          runs  wrong  in doubt at the end  most ticks locked" ^0
    for s in twopc.strategies():
        twopc.census(len(votes), s, timeout, back, 40) => x
        ("  " + pad(s, 14) + lpad(str(x[0]), 8) + lpad(str(x[1]), 7) + lpad(str(x[2]), 21) + lpad(str(x[3]), 19)) ^0

def rstrip(s):
    len(s) => j
    while j > 0 and s[j - 1] == " ":
        j - 1 => j
    return s[0:j]

def ask_votes():
    plain(input("votes (2 to 4 of yes or no, such as yes yes no)> ")) => t
    if t == "":
        "Cancelled." ^0
        return []
    [] => out
    "" => w
    for c in t + " ":
        if c == " ":
            if w == "yes":
                out + [True] => out
            elif w == "no":
                out + [False] => out
            elif w != "":
                "Type 2 to 4 votes, each yes or no." ^0
                return []
            "" => w
        else:
            w + c => w
    if len(out) < 2 or len(out) > 4:
        "Type 2 to 4 votes, each yes or no." ^0
        return []
    return out

def ask_timing(timeout, back):
    plain(input("in doubt for how long before acting (1 to 9 ticks)> ")) => t
    if t == "":
        "Cancelled." ^0
        return []
    if len(t) != 1 or t < "1" or t > "9":
        "Type a whole number from 1 to 9." ^0
        return []
    plain(input("coordinator back after (1 to 30 ticks, or never)> ")) => b
    if b == "":
        "Cancelled." ^0
        return []
    0 => nb
    if b != "never":
        if not is_digits(b) or len(b) > 2 or int(b) < 1 or int(b) > 30:
            "Type a whole number from 1 to 30, or never." ^0
            return []
        int(b) => nb
    return [int(t), nb]

[True, True, True] => votes
5 => timeout
10 => back

"== Two-phase commit ==" ^0
"A coordinator asks every participant to prepare, logs commit only if all vote yes, then tells each one. A participant that voted yes waits in doubt, its data locked, until it hears." ^0
True => running
while running:
    "" ^0
    "1) the transaction  2) one run  3) every crash point  4) votes  5) timing  6) quit" ^0
    plain(input("choice> ")) => choice
    if choice == "1":
        show(votes, timeout, back)
    elif choice == "2":
        one_run(votes, timeout, back)
    elif choice == "3":
        every(votes, timeout, back)
    elif choice == "4":
        ask_votes() => v
        if len(v) > 0:
            v => votes
            show(votes, timeout, back)
    elif choice == "5":
        ask_timing(timeout, back) => x
        if len(x) > 0:
            x[0] => timeout
            x[1] => back
            show(votes, timeout, back)
    elif choice == "6":
        False => running
    else:
        "Pick a number from 1 to 6." ^0
"Bye." ^0
```

Python projection of main.eml:

```python
import twopc

def plain(s):
    i = 0
    j = len(s)
    while i < j and s[i] == " ":
        i = i + 1
    while j > i and s[j - 1] == " ":
        j = j - 1
    return s[i:j]

def pad(s, n):
    out = s
    while len(out) < n:
        out = out + " "
    return out

def lpad(s, n):
    out = s
    while len(out) < n:
        out = " " + out
    return out

def is_digits(s):
    if len(s) == 0:
        return False
    for c in s:
        if c < "0" or c > "9":
            return False
    return True

def ticks_text(n):
    if n == 1:
        return "1 tick"
    return str(n) + " ticks"

def names_text(ns):
    out = ""
    for i in range(0, len(ns)):
        if i > 0 and i == len(ns) - 1:
            out = out + " and "
        elif i > 0:
            out = out + ", "
        out = out + ns[i]
    return out

def votes_text(votes):
    out = []
    for v in votes:
        if v:
            out = out + ["yes"]
        else:
            out = out + ["no"]
    return out

def back_text(back):
    if back == 0:
        return "never comes back"
    return "is back after " + ticks_text(back)

def show(votes, timeout, back):
    ps = []
    for i in range(0, len(votes)):
        ps = ps + [twopc.name(i)]
    print("Participants " + names_text(ps) + " vote " + names_text(votes_text(votes)) + ".")
    r = twopc.run(votes, "wait", timeout, back, 0 - 1, 40)
    line = ""
    for k in range(0, len(r[7])):
        if line != "":
            line = line + ", "
        line = line + str(k + 1) + " " + r[7][k]
    print("With no crash, the coordinator takes " + str(r[5]) + " steps, one a tick: " + line + ".")
    print("A participant in doubt for " + ticks_text(timeout) + " acts on its strategy; a crashed coordinator " + back_text(back) + ".")

def ask_strategy():
    s = plain(input("strategy (wait, ask peers, presume abort or presume commit)> "))
    if s == "":
        print("Cancelled.")
        return ""
    for x in twopc.strategies():
        if x == s:
            return s
    print("Type wait, ask peers, presume abort or presume commit.")
    return ""

def verdict(r):
    o = twopc.outcome(r)
    c = []
    a = []
    d = []
    for i in range(0, len(r[1])):
        if r[1][i] == "committed":
            c = c + [twopc.name(i)]
        elif r[1][i] == "aborted":
            a = a + [twopc.name(i)]
        elif r[1][i] == "prepared":
            d = d + [twopc.name(i)]
    if o[0]:
        print("Split: " + names_text(c) + " committed, and " + names_text(a) + " aborted.")
    if o[1]:
        wrong = []
        for i in range(0, len(r[1])):
            if (r[1][i] == "committed" or r[1][i] == "aborted") and r[1][i] != twopc.past(r[4]):
                wrong = wrong + [twopc.name(i)]
        print("Against the coordinator, which logged " + r[4] + ": " + names_text(wrong) + " " + opposite(r[4]) + ".")
    if o[3]:
        never = []
        for i in range(0, len(r[1])):
            if r[8][i] < 0:
                never = never + [twopc.name(i)]
        print("Committed without every yes: " + names_text(c) + " committed, though " + names_text(never) + " never voted yes.")
    if o[2]:
        print("Still in doubt at tick 40, data locked: " + names_text(d) + ".")
    if len(c) == 0 and len(a) == 0 and len(d) == 0:
        if r[4] == "":
            print("No participant was asked, and the coordinator never logged a decision.")
        else:
            print("No participant was asked; the coordinator logged " + r[4] + ".")
    elif not twopc.wrong(o) and not o[2]:
        common = "aborted"
        if len(c) > 0:
            common = "committed"
        if r[4] == "":
            print("Atomic: everyone who finished " + common + ", and the coordinator never logged a decision.")
        else:
            print("Atomic: everyone who finished " + common + ", as the coordinator logged.")

def opposite(d):
    if d == "commit":
        return "aborted"
    return "committed"

def one_run(votes, timeout, back):
    s = ask_strategy()
    if s == "":
        return
    n = twopc.crash_points(votes, timeout, back, 40)
    t = plain(input("crash after step (0 to " + str(n) + ", or none)> "))
    if t == "":
        print("Cancelled.")
        return
    crash = 0 - 1
    if t != "none":
        if not is_digits(t) or len(t) > 2 or int(t) > n:
            print("Type a step from 0 to " + str(n) + ", or none.")
            return
        crash = int(t)
    r = twopc.run(votes, s, timeout, back, crash, 40)
    if crash < 0:
        print(s + ", no crash:")
    else:
        print(s + ", the coordinator crashing after step " + str(crash) + " (it " + back_text(back) + "):")
    for e in r[0]:
        print("  tick " + lpad(str(e[0]), 2) + "  " + e[1])
    for i in range(0, len(votes)):
        p = twopc.name(i)
        st = r[1][i]
        if st == "prepared":
            print("  " + p + " still in doubt at tick 40, its data locked for " + ticks_text(r[2][i]) + ".")
        elif st == "idle":
            print("  " + p + " was never asked.")
        elif r[2][i] == 0:
            print("  " + p + " " + st + " at tick " + str(r[6][i]) + ", never locked.")
        else:
            print("  " + p + " " + st + " at tick " + str(r[6][i]) + ", its data locked for " + ticks_text(r[2][i]) + ".")
    verdict(r)

def every(votes, timeout, back):
    n = twopc.crash_points(votes, timeout, back, 40)
    labels = twopc.run(votes, "wait", timeout, back, 0 - 1, 40)[7]
    print("Every crash point, votes " + names_text(votes_text(votes)) + "; a participant in doubt acts after " + ticks_text(timeout) + "; the coordinator " + back_text(back) + ":")
    widths = [9, 9, 13, 14]
    head = "  " + pad("crash after", 26)
    for k in range(0, 4):
        head = head + "  " + pad(twopc.strategies()[k], widths[k])
    print(rstrip(head))
    wrong = [0, 0, 0, 0]
    doubt = [0, 0, 0, 0]
    most = [0, 0, 0, 0]
    stuck = []
    for c in range(0 - 1, n+1):
        label = "none"
        if c == 0:
            label = "0 before any step"
        elif c > 0:
            label = str(c) + " " + labels[c - 1]
        line = "  " + pad(label, 26)
        for k in range(0, 4):
            r = twopc.run(votes, twopc.strategies()[k], timeout, back, c, 40)
            o = twopc.outcome(r)
            cell = twopc.letters(r)
            if twopc.wrong(o):
                cell = cell + " !"
                wrong[k] = wrong[k] + 1
            if o[2]:
                doubt[k] = doubt[k] + 1
                if k == 1:
                    stuck = stuck + [str(c)]
            for x in r[2]:
                if x > most[k]:
                    most[k] = x
            line = line + "  " + pad(cell, widths[k])
        print(rstrip(line))
    print("  c committed, a aborted, ? still in doubt at tick 40, - never asked; ! wrong: split, against the coordinator, or committed without every yes.")
    for k in range(0, 4):
        print("  " + pad(twopc.strategies()[k] + ":", 16) + "wrong at " + str(wrong[k]) + " of " + str(n + 2) + " crash points, still in doubt at " + str(doubt[k]) + ", data locked at most " + ticks_text(most[k]) + ".")
    if len(stuck) == 1:
        print("Ask peers is still in doubt only at crash point " + stuck[0] + ": every participant had voted yes, and none had heard the decision.")
    elif len(stuck) > 1:
        print("Ask peers is still in doubt only at crash points " + names_text(stuck) + ": every participant had voted yes, and none had heard the decision.")
    print("Every pattern of " + str(len(votes)) + " votes, each with every crash point and none:")
    print("  strategy          runs  wrong  in doubt at the end  most ticks locked")
    for s in twopc.strategies():
        x = twopc.census(len(votes), s, timeout, back, 40)
        print("  " + pad(s, 14) + lpad(str(x[0]), 8) + lpad(str(x[1]), 7) + lpad(str(x[2]), 21) + lpad(str(x[3]), 19))

def rstrip(s):
    j = len(s)
    while j > 0 and s[j - 1] == " ":
        j = j - 1
    return s[0:j]

def ask_votes():
    t = plain(input("votes (2 to 4 of yes or no, such as yes yes no)> "))
    if t == "":
        print("Cancelled.")
        return []
    out = []
    w = ""
    for c in t + " ":
        if c == " ":
            if w == "yes":
                out = out + [True]
            elif w == "no":
                out = out + [False]
            elif w != "":
                print("Type 2 to 4 votes, each yes or no.")
                return []
            w = ""
        else:
            w = w + c
    if len(out) < 2 or len(out) > 4:
        print("Type 2 to 4 votes, each yes or no.")
        return []
    return out

def ask_timing(timeout, back):
    t = plain(input("in doubt for how long before acting (1 to 9 ticks)> "))
    if t == "":
        print("Cancelled.")
        return []
    if len(t) != 1 or t < "1" or t > "9":
        print("Type a whole number from 1 to 9.")
        return []
    b = plain(input("coordinator back after (1 to 30 ticks, or never)> "))
    if b == "":
        print("Cancelled.")
        return []
    nb = 0
    if b != "never":
        if not is_digits(b) or len(b) > 2 or int(b) < 1 or int(b) > 30:
            print("Type a whole number from 1 to 30, or never.")
            return []
        nb = int(b)
    return [int(t), nb]

votes = [True, True, True]
timeout = 5
back = 10
print("== Two-phase commit ==")
print("A coordinator asks every participant to prepare, logs commit only if all vote yes, then tells each one. A participant that voted yes waits in doubt, its data locked, until it hears.")
running = True
while running:
    print("")
    print("1) the transaction  2) one run  3) every crash point  4) votes  5) timing  6) quit")
    choice = plain(input("choice> "))
    if choice == "1":
        show(votes, timeout, back)
    elif choice == "2":
        one_run(votes, timeout, back)
    elif choice == "3":
        every(votes, timeout, back)
    elif choice == "4":
        v = ask_votes()
        if len(v) > 0:
            votes = v
            show(votes, timeout, back)
    elif choice == "5":
        x = ask_timing(timeout, back)
        if len(x) > 0:
            timeout = x[0]
            back = x[1]
            show(votes, timeout, back)
    elif choice == "6":
        running = False
    else:
        print("Pick a number from 1 to 6.")
print("Bye.")
```

### twopc.eml

```eml
# P119 two-phase commit - a coordinator and its participants as state
# machines, one coordinator step a tick: prepare each participant (it votes,
# and a yes locks its data), log the decision, tell each participant that
# voted yes. A crash of the coordinator after any step leaves participants
# that voted yes in doubt, their data locked. As in the corpus case
# two-phase-commit-window, what a participant does then decides between
# blocking and a split outcome:
#   wait            keeps waiting for the coordinator;
#   ask peers       asks the coordinator if it is up, else the other
#                   participants: one that knows the outcome, or one never
#                   asked (which then aborts on its own), settles it;
#   presume abort   aborts once the timeout has passed;
#   presume commit  commits once the timeout has passed.
# A coordinator that comes back with no decision logged decides abort.

def strategies():
    return ["wait", "ask peers", "presume abort", "presume commit"]

def name(i):
    return "P" + str(i + 1)

def run(votes, strategy, timeout, back, crash, horizon):
    # votes: a yes or no per participant; back: ticks the coordinator stays
    # down after a crash (0: it never comes back); crash: the number of
    # steps after which it crashes (-1: none).
    # [events as [tick, text], final states, ticks locked, still locked,
    #  the coordinator's logged decision ("" if none), steps taken, the
    #  tick each participant finished (-1 if not), a label per step, the
    #  tick each voted yes (-1 if it never did)]
    len(votes) => n
    [] => state
    [] => since
    [] => until
    [] => noted
    for v in votes:
        state + ["idle"] => state
        since + [0 - 1] => since
        until + [0 - 1] => until
        noted + [""] => noted
    [] => events
    [] => labels
    "prepare" => phase
    0 => nxt
    "" => decision
    False => logged
    [] => told
    0 => tell_at
    False => done
    0 => steps
    False => down
    False => crashed_once
    0 - 1 => up_at
    if crash == 0:
        True => down
        True => crashed_once
        events + [[0, "the coordinator crashes before its first step"]] => events
        if back > 0:
            back + 1 => up_at
    for t in [1:horizon]:
        if down and up_at == t:
            False => down
            "tell" => phase
            0 => tell_at
            if not logged:
                events + [[t, "the coordinator is back; with no decision logged, it decides abort"]] => events
                "abort" => decision
                True => logged
                steps + 1 => steps
                labels + ["decide abort on its return"] => labels
            else:
                events + [[t, "the coordinator is back with " + decision + " logged, and tells everyone again"]] => events
        elif not down and not done:
            steps + 1 => steps
            if phase == "prepare":
                nxt => i
                nxt + 1 => nxt
                labels + ["prepare " + name(i)] => labels
                if state[i] == "idle" and votes[i]:
                    "prepared" => state[i]
                    t => since[i]
                    told + [i] => told
                    events + [[t, "prepare " + name(i) + ": it votes yes and locks its data"]] => events
                    if nxt == n:
                        "decide" => phase
                else:
                    if state[i] == "idle":
                        "aborted" => state[i]
                        t => until[i]
                    events + [[t, "prepare " + name(i) + ": it votes no"]] => events
                    "decide" => phase
                    "abort" => decision
            elif phase == "decide":
                if decision == "":
                    "commit" => decision
                True => logged
                labels + ["log " + decision] => labels
                events + [[t, "the coordinator logs " + decision]] => events
                "tell" => phase
                0 => tell_at
            else:
                told[tell_at] => i
                tell_at + 1 => tell_at
                labels + ["tell " + name(i)] => labels
                if state[i] == "prepared":
                    past(decision) => state[i]
                    t => until[i]
                    events + [[t, "tell " + name(i) + " " + decision + ": it " + verb(decision) + " and unlocks"]] => events
                elif state[i] == past(decision):
                    events + [[t, "tell " + name(i) + " " + decision + ": it had already " + past(decision)]] => events
                else:
                    events + [[t, "tell " + name(i) + " " + decision + ": but it had already " + state[i]]] => events
            if crash > 0 and steps == crash and not crashed_once:
                True => down
                True => crashed_once
                events + [[t, "the coordinator crashes"]] => events
                if back > 0:
                    t + back + 1 => up_at
        if not down and phase == "tell" and tell_at >= len(told):
            True => done
        "" => known
        if logged:
            decision => known
        for i in [0:n - 1]:
            if state[i] == "prepared" and t - since[i] >= timeout:
                learn(state, votes, i, strategy, down, known, n) => r
                if r[0] != "":
                    r[0] => state[i]
                    t => until[i]
                    if r[1] >= 0:
                        "aborted" => state[r[1]]
                        t => until[r[1]]
                        events + [[t, name(r[1]) + ", never asked, aborts on its own"]] => events
                    events + [[t, name(i) + " in doubt: " + r[2]]] => events
                elif noted[i] != r[2]:
                    r[2] => noted[i]
                    events + [[t, name(i) + " in doubt: " + r[2]]] => events
    [] => locked
    [] => still
    for i in [0:n - 1]:
        if since[i] < 0:
            locked + [0] => locked
            still + [False] => still
        elif until[i] < 0:
            locked + [horizon - since[i]] => locked
            still + [True] => still
        else:
            locked + [until[i] - since[i]] => locked
            still + [False] => still
    "" => final
    if logged:
        decision => final
    return [events, state, locked, still, final, steps, until, labels, since]

def verb(d):
    if d == "commit":
        return "commits"
    return "aborts"

def past(d):
    if d == "commit":
        return "committed"
    return "aborted"

def learn(state, votes, i, strategy, down, decision, n):
    # what participant i in doubt does now: [new state or "", a participant
    # never asked that aborts on its own or -1, what it says]
    if strategy == "presume abort":
        return ["aborted", 0 - 1, "presumes abort and unlocks"]
    if strategy == "presume commit":
        return ["committed", 0 - 1, "presumes commit and unlocks"]
    if strategy == "wait":
        return ["", 0 - 1, "waits, its data locked"]
    if not down:
        if decision != "":
            return [past(decision), 0 - 1, "asks the coordinator: " + decision]
        return ["", 0 - 1, "asks the coordinator: no decision yet, so it waits"]
    for j in [0:n - 1]:
        if j != i and (state[j] == "committed" or state[j] == "aborted"):
            return [state[j], 0 - 1, "asks " + name(j) + ", which has " + state[j] + ", and " + verb(present(state[j])) + " too"]
    for j in [0:n - 1]:
        if j != i and state[j] == "idle":
            return ["aborted", j, "asks " + name(j) + ", and aborts too"]
    return ["", 0 - 1, "asks the others, all in doubt too, so it waits, its data locked"]

def present(s):
    if s == "committed":
        return "commit"
    return "abort"

def outcome(r):
    # [split, against the coordinator, in doubt at the end, committed though
    #  someone never voted yes]
    False => c
    False => a
    False => doubt
    False => against
    False => no_yes
    for i in [0:len(r[1]) - 1]:
        if r[8][i] < 0:
            True => no_yes
        r[1][i] => s
        if s == "committed":
            True => c
        if s == "aborted":
            True => a
        if s == "prepared":
            True => doubt
        if r[4] != "" and (s == "committed" or s == "aborted") and s != past(r[4]):
            True => against
    return [c and a, against, doubt, c and no_yes]

def wrong(o):
    return o[0] or o[1] or o[3]

def letters(r):
    "" => out
    for s in r[1]:
        if out != "":
            out + " " => out
        if s == "committed":
            out + "c" => out
        elif s == "aborted":
            out + "a" => out
        elif s == "prepared":
            out + "?" => out
        else:
            out + "-" => out
    return out

def crash_points(votes, timeout, back, horizon):
    # the number of steps the coordinator takes with no crash
    return run(votes, "wait", timeout, back, 0 - 1, horizon)[5]

def patterns(n):
    [[]] => out
    for k in [1:n]:
        [] => more
        for p in out:
            more + [p + [True]] => more
            more + [p + [False]] => more
        more => out
    return out

def census(n, strategy, timeout, back, horizon):
    # over every vote pattern and every crash point (and none): [runs,
    # wrong (split or against the coordinator), in doubt at the end, most
    # ticks locked]
    0 => runs
    0 => bad
    0 => doubt
    0 => most
    for votes in patterns(n):
        for c in [0 - 1:crash_points(votes, timeout, back, horizon)]:
            run(votes, strategy, timeout, back, c, horizon) => r
            outcome(r) => o
            runs + 1 => runs
            if wrong(o):
                bad + 1 => bad
            if o[2]:
                doubt + 1 => doubt
            for x in r[2]:
                if x > most:
                    x => most
    return [runs, bad, doubt, most]
```

Python projection of twopc.eml:

```python
def strategies():
    return ["wait", "ask peers", "presume abort", "presume commit"]

def name(i):
    return "P" + str(i + 1)

def run(votes, strategy, timeout, back, crash, horizon):
    n = len(votes)
    state = []
    since = []
    until = []
    noted = []
    for v in votes:
        state = state + ["idle"]
        since = since + [0 - 1]
        until = until + [0 - 1]
        noted = noted + [""]
    events = []
    labels = []
    phase = "prepare"
    nxt = 0
    decision = ""
    logged = False
    told = []
    tell_at = 0
    done = False
    steps = 0
    down = False
    crashed_once = False
    up_at = 0 - 1
    if crash == 0:
        down = True
        crashed_once = True
        events = events + [[0, "the coordinator crashes before its first step"]]
        if back > 0:
            up_at = back + 1
    for t in range(1, horizon+1):
        if down and up_at == t:
            down = False
            phase = "tell"
            tell_at = 0
            if not logged:
                events = events + [[t, "the coordinator is back; with no decision logged, it decides abort"]]
                decision = "abort"
                logged = True
                steps = steps + 1
                labels = labels + ["decide abort on its return"]
            else:
                events = events + [[t, "the coordinator is back with " + decision + " logged, and tells everyone again"]]
        elif not down and not done:
            steps = steps + 1
            if phase == "prepare":
                i = nxt
                nxt = nxt + 1
                labels = labels + ["prepare " + name(i)]
                if state[i] == "idle" and votes[i]:
                    state[i] = "prepared"
                    since[i] = t
                    told = told + [i]
                    events = events + [[t, "prepare " + name(i) + ": it votes yes and locks its data"]]
                    if nxt == n:
                        phase = "decide"
                else:
                    if state[i] == "idle":
                        state[i] = "aborted"
                        until[i] = t
                    events = events + [[t, "prepare " + name(i) + ": it votes no"]]
                    phase = "decide"
                    decision = "abort"
            elif phase == "decide":
                if decision == "":
                    decision = "commit"
                logged = True
                labels = labels + ["log " + decision]
                events = events + [[t, "the coordinator logs " + decision]]
                phase = "tell"
                tell_at = 0
            else:
                i = told[tell_at]
                tell_at = tell_at + 1
                labels = labels + ["tell " + name(i)]
                if state[i] == "prepared":
                    state[i] = past(decision)
                    until[i] = t
                    events = events + [[t, "tell " + name(i) + " " + decision + ": it " + verb(decision) + " and unlocks"]]
                elif state[i] == past(decision):
                    events = events + [[t, "tell " + name(i) + " " + decision + ": it had already " + past(decision)]]
                else:
                    events = events + [[t, "tell " + name(i) + " " + decision + ": but it had already " + state[i]]]
            if crash > 0 and steps == crash and not crashed_once:
                down = True
                crashed_once = True
                events = events + [[t, "the coordinator crashes"]]
                if back > 0:
                    up_at = t + back + 1
        if not down and phase == "tell" and tell_at >= len(told):
            done = True
        known = ""
        if logged:
            known = decision
        for i in range(0, n):
            if state[i] == "prepared" and t - since[i] >= timeout:
                r = learn(state, votes, i, strategy, down, known, n)
                if r[0] != "":
                    state[i] = r[0]
                    until[i] = t
                    if r[1] >= 0:
                        state[r[1]] = "aborted"
                        until[r[1]] = t
                        events = events + [[t, name(r[1]) + ", never asked, aborts on its own"]]
                    events = events + [[t, name(i) + " in doubt: " + r[2]]]
                elif noted[i] != r[2]:
                    noted[i] = r[2]
                    events = events + [[t, name(i) + " in doubt: " + r[2]]]
    locked = []
    still = []
    for i in range(0, n):
        if since[i] < 0:
            locked = locked + [0]
            still = still + [False]
        elif until[i] < 0:
            locked = locked + [horizon - since[i]]
            still = still + [True]
        else:
            locked = locked + [until[i] - since[i]]
            still = still + [False]
    final = ""
    if logged:
        final = decision
    return [events, state, locked, still, final, steps, until, labels, since]

def verb(d):
    if d == "commit":
        return "commits"
    return "aborts"

def past(d):
    if d == "commit":
        return "committed"
    return "aborted"

def learn(state, votes, i, strategy, down, decision, n):
    if strategy == "presume abort":
        return ["aborted", 0 - 1, "presumes abort and unlocks"]
    if strategy == "presume commit":
        return ["committed", 0 - 1, "presumes commit and unlocks"]
    if strategy == "wait":
        return ["", 0 - 1, "waits, its data locked"]
    if not down:
        if decision != "":
            return [past(decision), 0 - 1, "asks the coordinator: " + decision]
        return ["", 0 - 1, "asks the coordinator: no decision yet, so it waits"]
    for j in range(0, n):
        if j != i and (state[j] == "committed" or state[j] == "aborted"):
            return [state[j], 0 - 1, "asks " + name(j) + ", which has " + state[j] + ", and " + verb(present(state[j])) + " too"]
    for j in range(0, n):
        if j != i and state[j] == "idle":
            return ["aborted", j, "asks " + name(j) + ", and aborts too"]
    return ["", 0 - 1, "asks the others, all in doubt too, so it waits, its data locked"]

def present(s):
    if s == "committed":
        return "commit"
    return "abort"

def outcome(r):
    c = False
    a = False
    doubt = False
    against = False
    no_yes = False
    for i in range(0, len(r[1])):
        if r[8][i] < 0:
            no_yes = True
        s = r[1][i]
        if s == "committed":
            c = True
        if s == "aborted":
            a = True
        if s == "prepared":
            doubt = True
        if r[4] != "" and (s == "committed" or s == "aborted") and s != past(r[4]):
            against = True
    return [c and a, against, doubt, c and no_yes]

def wrong(o):
    return o[0] or o[1] or o[3]

def letters(r):
    out = ""
    for s in r[1]:
        if out != "":
            out = out + " "
        if s == "committed":
            out = out + "c"
        elif s == "aborted":
            out = out + "a"
        elif s == "prepared":
            out = out + "?"
        else:
            out = out + "-"
    return out

def crash_points(votes, timeout, back, horizon):
    return run(votes, "wait", timeout, back, 0 - 1, horizon)[5]

def patterns(n):
    out = [[]]
    for k in range(1, n+1):
        more = []
        for p in out:
            more = more + [p + [True]]
            more = more + [p + [False]]
        out = more
    return out

def census(n, strategy, timeout, back, horizon):
    runs = 0
    bad = 0
    doubt = 0
    most = 0
    for votes in patterns(n):
        for c in range(0 - 1, crash_points(votes, timeout, back, horizon)+1):
            r = run(votes, strategy, timeout, back, c, horizon)
            o = outcome(r)
            runs = runs + 1
            if wrong(o):
                bad = bad + 1
            if o[2]:
                doubt = doubt + 1
            for x in r[2]:
                if x > most:
                    most = x
    return [runs, bad, doubt, most]
```

## README

# P119 - Two-phase commit

A coordinator asks every participant to prepare, logs commit only if all
vote yes, then tells each one. A participant that voted yes is in doubt,
its data locked, until it hears. The coordinator can crash after any
step.

- `main.eml` - the menu, the transaction, one run tick by tick, every
  crash point under four strategies, and the votes and timing
- `twopc.eml` - the coordinator and the participants, one coordinator
  step a tick, the four strategies, the outcome of a run, and the count
  over every pattern of votes

How each part works:

- The coordinator's steps: prepare each participant in turn (a yes locks
  its data, a no aborts at once and ends the asking), log the decision,
  tell each participant that voted yes. A coordinator that comes back with
  no decision logged decides abort; with one logged, it tells everyone
  again.
- A participant in doubt for the timeout acts on its strategy:
  - wait keeps waiting for the coordinator;
  - ask peers asks the coordinator if it is up, else the others: one that
    has committed or aborted settles it, and one never asked aborts on
    its own, and so does the one that asked;
  - presume abort and presume commit decide on their own.
- A run is wrong when it splits, goes against the coordinator's log, or
  commits though someone never voted yes. As in the corpus case
  `two-phase-commit-window`, with three yes votes, a timeout of 5 ticks and
  the coordinator back after 10:
  - wait and ask peers are never wrong, and hold the data for up to 17
    and 14 ticks;
  - presume abort is wrong at 3 of the 9 crash points, and presume commit
    at 3.
- If the coordinator never comes back, wait is left in doubt at 6 crash
  points, and ask peers only at 2: after every participant voted yes and
  before any heard the decision. That window is where two-phase commit
  blocks.
- A timeout of 3 ticks makes presume abort wrong with no crash at all:
  each participant is in doubt for 4 ticks before it hears.

What is checked: menu choices 1 to 6; one of the four strategies; a crash
point from 0 to the last step, or none; 2 to 4 votes of yes or no; a
timeout from 1 to 9 ticks; the coordinator back after 1 to 30 ticks, or
never. An empty answer cancels.

Sessions: `sessions/basic.in` gives:
- the transaction and every crash point;
- runs: wait after step 3, presume abort after step 4 (it aborts what the
  coordinator committed), ask peers after steps 2 and 4;
- the coordinator never back: every crash point, and ask peers after step
  3, left in doubt;
- the votes yes, no, yes and yes, presume commit after step 1, and every
  crash point;
- three yes votes again with a timeout of 3, every crash point, and
  presume abort with no crash.

`sessions/bad-input.in` gives:
- menu choices 0 and x;
- runs: a cancel, the strategy fast, then crash points of a cancel, 8, x
  and -1;
- votes: a cancel, one vote, five votes, yes maybe, and YES yes;
- timing: a cancel, 0, 10 and x, then 5 with a cancel, 0, 31 and
  sometime.

Built on the verified corpus case `two-phase-commit-window` (a coordinator
crash leaves participants in doubt, and presuming an outcome trades the
blocking for a split).