<!-- canonical: https://efficientnewlanguage.org/eml-p/projects/P130-lost-update/ | updated: 2026-10-17 -->

# P130 Lost update

Users reading, adding to and writing back one shared value by a schedule, with and without a version check: every order of their turns counted, and only the serial ones keep every update without the check.

EML-P project `projects/lost-update` in the EML language repo: 2 module(s), entry `main.eml`, terminal UI. There, `eml project run projects/lost-update` runs it and `eml project verify projects/lost-update` 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: lost-update-schedule (https://efficientnewlanguage.org/cases/223-lost-update-schedule/).

## Sessions

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

Input:

```text
0
x
2

2
1 3
2
1 x
2
1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1
4

4
10 5
4
10 0 5
4
10 x 5
4
100 5 5
4
5 -5 3
5

5
4
5
3
2
1 2 1 2 1 2 3 3 3
6
```

Screen:

```text
== Lost update ==
Users each read a shared value, add their own amount and write it back, one step a turn, in the order a schedule gives.

1) the users  2) one schedule  3) every order  4) amounts  5) two or three users  6) quit
choice> 0
Pick a number from 1 to 6.

1) the users  2) one schedule  3) every order  4) amounts  5) two or three users  6) quit
choice> x
Pick a number from 1 to 6.

1) the users  2) one schedule  3) every order  4) amounts  5) two or three users  6) quit
choice> 2
A schedule: whose turn it is, users 1 to 2, such as 1 2 1 2 1 2 (up to 30 turns).
schedule> 
Cancelled.

1) the users  2) one schedule  3) every order  4) amounts  5) two or three users  6) quit
choice> 2
A schedule: whose turn it is, users 1 to 2, such as 1 2 1 2 1 2 (up to 30 turns).
schedule> 1 3
Type user numbers from 1 to 2, separated by spaces.

1) the users  2) one schedule  3) every order  4) amounts  5) two or three users  6) quit
choice> 2
A schedule: whose turn it is, users 1 to 2, such as 1 2 1 2 1 2 (up to 30 turns).
schedule> 1 x
Type user numbers from 1 to 2, separated by spaces.

1) the users  2) one schedule  3) every order  4) amounts  5) two or three users  6) quit
choice> 2
A schedule: whose turn it is, users 1 to 2, such as 1 2 1 2 1 2 (up to 30 turns).
schedule> 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1
Up to 30 turns.

1) the users  2) one schedule  3) every order  4) amounts  5) two or three users  6) quit
choice> 4
Amounts for users 1, 2 and 3, such as 10 5 -3 (each from -99 to 99, not 0).
amounts> 
Cancelled.

1) the users  2) one schedule  3) every order  4) amounts  5) two or three users  6) quit
choice> 4
Amounts for users 1, 2 and 3, such as 10 5 -3 (each from -99 to 99, not 0).
amounts> 10 5
Type three amounts.

1) the users  2) one schedule  3) every order  4) amounts  5) two or three users  6) quit
choice> 4
Amounts for users 1, 2 and 3, such as 10 5 -3 (each from -99 to 99, not 0).
amounts> 10 0 5
Each amount is a whole number from -99 to 99, not 0.

1) the users  2) one schedule  3) every order  4) amounts  5) two or three users  6) quit
choice> 4
Amounts for users 1, 2 and 3, such as 10 5 -3 (each from -99 to 99, not 0).
amounts> 10 x 5
Each amount is a whole number from -99 to 99, not 0.

1) the users  2) one schedule  3) every order  4) amounts  5) two or three users  6) quit
choice> 4
Amounts for users 1, 2 and 3, such as 10 5 -3 (each from -99 to 99, not 0).
amounts> 100 5 5
Each amount is a whole number from -99 to 99, not 0.

1) the users  2) one schedule  3) every order  4) amounts  5) two or three users  6) quit
choice> 4
Amounts for users 1, 2 and 3, such as 10 5 -3 (each from -99 to 99, not 0).
amounts> 5 -5 3
Users now add +5, -5 and +3.

1) the users  2) one schedule  3) every order  4) amounts  5) two or three users  6) quit
choice> 5
users (2 or 3)> 
Cancelled.

1) the users  2) one schedule  3) every order  4) amounts  5) two or three users  6) quit
choice> 5
users (2 or 3)> 4
Type 2 or 3.

1) the users  2) one schedule  3) every order  4) amounts  5) two or three users  6) quit
choice> 5
users (2 or 3)> 3
Now 3 users.

1) the users  2) one schedule  3) every order  4) amounts  5) two or three users  6) quit
choice> 2
A schedule: whose turn it is, users 1 to 3, such as 1 2 1 2 1 2 (up to 30 turns).
schedule> 1 2 1 2 1 2 3 3 3
Without a check:
   1  user 1 reads 100
   2  user 2 reads 100
   3  user 1 adds +5, making 105
   4  user 2 adds -5, making 95
   5  user 1 writes 105 over 100
   6  user 2 writes 95 over 105
   7  user 3 reads 95
   8  user 3 adds +3, making 98
   9  user 3 writes 98 over 95
  ends at 98, where every update kept would make 103: user 1's update was lost, written over by a value read before it
With a version check:
   1  user 1 reads 100
   2  user 2 reads 100
   3  user 1 adds +5, making 105
   4  user 2 adds -5, making 95
   5  user 1 writes 105 over 100
   6  user 2 finds the version moved from 0 to 1: its write is refused, and it starts over
   7  user 3 reads 105
   8  user 3 adds +3, making 108
   9  user 3 writes 108 over 105
  10  then user 2 reads 108
  11  then user 2 adds -5, making 103
  12  then user 2 writes 103 over 108
  ends at 103: every update kept
  1 write refused and done again; 12 turns in all

1) the users  2) one schedule  3) every order  4) amounts  5) two or three users  6) quit
choice> 6
Bye.
```

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

Input:

```text
1
2
1 1 1 2 2 2
2
1 2 1 2 1 2
3
5
3
2
1 2 3 1 2 3 1 2 3
6
```

Screen:

```text
== Lost update ==
Users each read a shared value, add their own amount and write it back, one step a turn, in the order a schedule gives.

1) the users  2) one schedule  3) every order  4) amounts  5) two or three users  6) quit
choice> 1
The value starts at 100; user 1 adds +10, user 2 adds +5. Each user reads, adds, then writes: three turns.
Every update kept, it ends at 115.

1) the users  2) one schedule  3) every order  4) amounts  5) two or three users  6) quit
choice> 2
A schedule: whose turn it is, users 1 to 2, such as 1 2 1 2 1 2 (up to 30 turns).
schedule> 1 1 1 2 2 2
Without a check:
   1  user 1 reads 100
   2  user 1 adds +10, making 110
   3  user 1 writes 110 over 100
   4  user 2 reads 110
   5  user 2 adds +5, making 115
   6  user 2 writes 115 over 110
  ends at 115: every update kept
With a version check:
   1  user 1 reads 100
   2  user 1 adds +10, making 110
   3  user 1 writes 110 over 100
   4  user 2 reads 110
   5  user 2 adds +5, making 115
   6  user 2 writes 115 over 110
  ends at 115: every update kept

1) the users  2) one schedule  3) every order  4) amounts  5) two or three users  6) quit
choice> 2
A schedule: whose turn it is, users 1 to 2, such as 1 2 1 2 1 2 (up to 30 turns).
schedule> 1 2 1 2 1 2
Without a check:
   1  user 1 reads 100
   2  user 2 reads 100
   3  user 1 adds +10, making 110
   4  user 2 adds +5, making 105
   5  user 1 writes 110 over 100
   6  user 2 writes 105 over 110
  ends at 105, where every update kept would make 115: user 1's update was lost, written over by a value read before it
With a version check:
   1  user 1 reads 100
   2  user 2 reads 100
   3  user 1 adds +10, making 110
   4  user 2 adds +5, making 105
   5  user 1 writes 110 over 100
   6  user 2 finds the version moved from 0 to 1: its write is refused, and it starts over
   7  then user 2 reads 110
   8  then user 2 adds +5, making 115
   9  then user 2 writes 115 over 110
  ends at 115: every update kept
  1 write refused and done again; 9 turns in all

1) the users  2) one schedule  3) every order  4) amounts  5) two or three users  6) quit
choice> 3
2 users, 20 orders of their turns:
  without a check:      18 lose an update
  with a version check: 0 lose one; 18 writes refused and done again in all, at most 9 turns in one order
3 users, 1680 orders of their turns:
  without a check:      1674 lose an update
  with a version check: 0 lose one; 2970 writes refused and done again in all, at most 15 turns in one order
An order loses an update when one user's read and write enclose another user's write; run one after another, the users never lose one.

1) the users  2) one schedule  3) every order  4) amounts  5) two or three users  6) quit
choice> 5
users (2 or 3)> 3
Now 3 users.

1) the users  2) one schedule  3) every order  4) amounts  5) two or three users  6) quit
choice> 2
A schedule: whose turn it is, users 1 to 3, such as 1 2 1 2 1 2 (up to 30 turns).
schedule> 1 2 3 1 2 3 1 2 3
Without a check:
   1  user 1 reads 100
   2  user 2 reads 100
   3  user 3 reads 100
   4  user 1 adds +10, making 110
   5  user 2 adds +5, making 105
   6  user 3 adds -3, making 97
   7  user 1 writes 110 over 100
   8  user 2 writes 105 over 110
   9  user 3 writes 97 over 105
  ends at 97, where every update kept would make 112: user 1's and user 2's updates were lost, written over by values read before them
With a version check:
   1  user 1 reads 100
   2  user 2 reads 100
   3  user 3 reads 100
   4  user 1 adds +10, making 110
   5  user 2 adds +5, making 105
   6  user 3 adds -3, making 97
   7  user 1 writes 110 over 100
   8  user 2 finds the version moved from 0 to 1: its write is refused, and it starts over
   9  user 3 finds the version moved from 0 to 1: its write is refused, and it starts over
  10  then user 2 reads 110
  11  then user 2 adds +5, making 115
  12  then user 2 writes 115 over 110
  13  then user 3 reads 115
  14  then user 3 adds -3, making 112
  15  then user 3 writes 112 over 115
  ends at 112: every update kept
  2 writes refused and done again; 15 turns in all

1) the users  2) one schedule  3) every order  4) amounts  5) two or three users  6) quit
choice> 6
Bye.
```

## Modules

### main.eml

```eml
# P130 lost update: two or three users reading, adding and writing back
# one shared value by a schedule, with and without a version check, and
# every interleaving counted.
import update

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 lpad(s, n):
    s => out
    while len(out) < n:
        " " + out => out
    return out

def right_value(start, deltas):
    start => r
    for d in deltas:
        r + d => r
    return r

def show(start, deltas):
    "" => line
    for u in [0:len(deltas) - 1]:
        if line != "":
            line + ", " => line
        line + "user " + str(u + 1) + " adds " + update.signed(deltas[u]) => line
    ("The value starts at " + str(start) + "; " + line + ". Each user reads, adds, then writes: three turns.") ^0
    ("Every update kept, it ends at " + str(right_value(start, deltas)) + ".") ^0

def one(start, deltas):
    len(deltas) => n
    ("A schedule: whose turn it is, users 1 to " + str(n) + ", such as 1 2 1 2 1 2 (up to 30 turns).") ^0
    plain(input("schedule> ")) => t
    if t == "":
        "Cancelled." ^0
        return
    [] => sched
    "" => w
    for c in t + " ":
        if c == " ":
            if w != "":
                if len(w) != 1 or w[0] < "1" or w[0] > str(n):
                    ("Type user numbers from 1 to " + str(n) + ", separated by spaces.") ^0
                    return
                sched + [int(w) - 1] => sched
            "" => w
        else:
            w + c => w
    if len(sched) > 30:
        "Up to 30 turns." ^0
        return
    right_value(start, deltas) => right
    for checked in [False, True]:
        update.run(start, deltas, sched, checked) => r
        if checked:
            "With a version check:" ^0
        else:
            "Without a check:" ^0
        for k in [0:len(r[0]) - 1]:
            r[0][k] => e
            "  " => mark
            if k >= len(sched):
                "  then " => mark
            ("  " + lpad(str(k + 1), 2) + mark + "user " + str(e[0] + 1) + " " + e[1]) ^0
        if len(r[4]) == 0:
            ("  ends at " + str(r[1]) + ": every update kept") ^0
        else:
            "" => who
            for u in r[4]:
                if who != "":
                    who + " and " => who
                who + "user " + str(u + 1) + "'s" => who
            if len(r[4]) == 1:
                ("  ends at " + str(r[1]) + ", where every update kept would make " + str(right) + ": " + who + " update was lost, written over by a value read before it") ^0
            else:
                ("  ends at " + str(r[1]) + ", where every update kept would make " + str(right) + ": " + who + " updates were lost, written over by values read before them") ^0
        if r[2] == 1:
            ("  1 write refused and done again; " + str(r[3]) + " turns in all") ^0
        elif r[2] > 1:
            ("  " + str(r[2]) + " writes refused and done again; " + str(r[3]) + " turns in all") ^0

def every(start, deltas):
    for n in [2:3]:
        [] => ds
        for u in [0:n - 1]:
            ds + [deltas[u]] => ds
        update.census(start, ds, False) => a
        update.census(start, ds, True) => b
        (str(n) + " users, " + str(a[0]) + " orders of their turns:") ^0
        ("  without a check:      " + str(a[1]) + " lose an update") ^0
        ("  with a version check: " + str(b[1]) + " lose one; " + str(b[2]) + " writes refused and done again in all, at most " + str(b[3]) + " turns in one order") ^0
    "An order loses an update when one user's read and write enclose another user's write; run one after another, the users never lose one." ^0

def set_amounts(deltas):
    ("Amounts for users 1, 2 and 3, such as 10 5 -3 (each from -99 to 99, not 0).") ^0
    plain(input("amounts> ")) => t
    if t == "":
        "Cancelled." ^0
        return deltas
    [] => out
    "" => w
    for c in t + " ":
        if c == " ":
            if w != "":
                1 => sign
                w => d
                if d[0] == "-":
                    0 - 1 => sign
                    d[1:len(d)] => d
                True => digits
                if len(d) == 0 or len(d) > 2:
                    False => digits
                for ch in d:
                    if ch < "0" or ch > "9":
                        False => digits
                if not digits:
                    "Each amount is a whole number from -99 to 99, not 0." ^0
                    return deltas
                if int(d) == 0:
                    "Each amount is a whole number from -99 to 99, not 0." ^0
                    return deltas
                out + [sign * int(d)] => out
            "" => w
        else:
            w + c => w
    if len(out) != 3:
        "Type three amounts." ^0
        return deltas
    ("Users now add " + update.signed(out[0]) + ", " + update.signed(out[1]) + " and " + update.signed(out[2]) + ".") ^0
    return out

100 => start
[10, 5, 0 - 3] => deltas
2 => users

"== Lost update ==" ^0
"Users each read a shared value, add their own amount and write it back, one step a turn, in the order a schedule gives." ^0
True => running
while running:
    "" ^0
    "1) the users  2) one schedule  3) every order  4) amounts  5) two or three users  6) quit" ^0
    plain(input("choice> ")) => choice
    [] => ds
    for u in [0:users - 1]:
        ds + [deltas[u]] => ds
    if choice == "1":
        show(start, ds)
    elif choice == "2":
        one(start, ds)
    elif choice == "3":
        every(start, deltas)
    elif choice == "4":
        set_amounts(deltas) => deltas
    elif choice == "5":
        plain(input("users (2 or 3)> ")) => t
        if t == "2" or t == "3":
            int(t) => users
            ("Now " + t + " users.") ^0
        elif t == "":
            "Cancelled." ^0
        else:
            "Type 2 or 3." ^0
    elif choice == "6":
        False => running
    else:
        "Pick a number from 1 to 6." ^0
"Bye." ^0
```

Python projection of main.eml:

```python
import update

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 lpad(s, n):
    out = s
    while len(out) < n:
        out = " " + out
    return out

def right_value(start, deltas):
    r = start
    for d in deltas:
        r = r + d
    return r

def show(start, deltas):
    line = ""
    for u in range(0, len(deltas)):
        if line != "":
            line = line + ", "
        line = line + "user " + str(u + 1) + " adds " + update.signed(deltas[u])
    print("The value starts at " + str(start) + "; " + line + ". Each user reads, adds, then writes: three turns.")
    print("Every update kept, it ends at " + str(right_value(start, deltas)) + ".")

def one(start, deltas):
    n = len(deltas)
    print("A schedule: whose turn it is, users 1 to " + str(n) + ", such as 1 2 1 2 1 2 (up to 30 turns).")
    t = plain(input("schedule> "))
    if t == "":
        print("Cancelled.")
        return
    sched = []
    w = ""
    for c in t + " ":
        if c == " ":
            if w != "":
                if len(w) != 1 or w[0] < "1" or w[0] > str(n):
                    print("Type user numbers from 1 to " + str(n) + ", separated by spaces.")
                    return
                sched = sched + [int(w) - 1]
            w = ""
        else:
            w = w + c
    if len(sched) > 30:
        print("Up to 30 turns.")
        return
    right = right_value(start, deltas)
    for checked in [False, True]:
        r = update.run(start, deltas, sched, checked)
        if checked:
            print("With a version check:")
        else:
            print("Without a check:")
        for k in range(0, len(r[0])):
            e = r[0][k]
            mark = "  "
            if k >= len(sched):
                mark = "  then "
            print("  " + lpad(str(k + 1), 2) + mark + "user " + str(e[0] + 1) + " " + e[1])
        if len(r[4]) == 0:
            print("  ends at " + str(r[1]) + ": every update kept")
        else:
            who = ""
            for u in r[4]:
                if who != "":
                    who = who + " and "
                who = who + "user " + str(u + 1) + "'s"
            if len(r[4]) == 1:
                print("  ends at " + str(r[1]) + ", where every update kept would make " + str(right) + ": " + who + " update was lost, written over by a value read before it")
            else:
                print("  ends at " + str(r[1]) + ", where every update kept would make " + str(right) + ": " + who + " updates were lost, written over by values read before them")
        if r[2] == 1:
            print("  1 write refused and done again; " + str(r[3]) + " turns in all")
        elif r[2] > 1:
            print("  " + str(r[2]) + " writes refused and done again; " + str(r[3]) + " turns in all")

def every(start, deltas):
    for n in range(2, 4):
        ds = []
        for u in range(0, n):
            ds = ds + [deltas[u]]
        a = update.census(start, ds, False)
        b = update.census(start, ds, True)
        print(str(n) + " users, " + str(a[0]) + " orders of their turns:")
        print("  without a check:      " + str(a[1]) + " lose an update")
        print("  with a version check: " + str(b[1]) + " lose one; " + str(b[2]) + " writes refused and done again in all, at most " + str(b[3]) + " turns in one order")
    print("An order loses an update when one user's read and write enclose another user's write; run one after another, the users never lose one.")

def set_amounts(deltas):
    print("Amounts for users 1, 2 and 3, such as 10 5 -3 (each from -99 to 99, not 0).")
    t = plain(input("amounts> "))
    if t == "":
        print("Cancelled.")
        return deltas
    out = []
    w = ""
    for c in t + " ":
        if c == " ":
            if w != "":
                sign = 1
                d = w
                if d[0] == "-":
                    sign = 0 - 1
                    d = d[1:len(d)]
                digits = True
                if len(d) == 0 or len(d) > 2:
                    digits = False
                for ch in d:
                    if ch < "0" or ch > "9":
                        digits = False
                if not digits:
                    print("Each amount is a whole number from -99 to 99, not 0.")
                    return deltas
                if int(d) == 0:
                    print("Each amount is a whole number from -99 to 99, not 0.")
                    return deltas
                out = out + [sign * int(d)]
            w = ""
        else:
            w = w + c
    if len(out) != 3:
        print("Type three amounts.")
        return deltas
    print("Users now add " + update.signed(out[0]) + ", " + update.signed(out[1]) + " and " + update.signed(out[2]) + ".")
    return out

start = 100
deltas = [10, 5, 0 - 3]
users = 2
print("== Lost update ==")
print("Users each read a shared value, add their own amount and write it back, one step a turn, in the order a schedule gives.")
running = True
while running:
    print("")
    print("1) the users  2) one schedule  3) every order  4) amounts  5) two or three users  6) quit")
    choice = plain(input("choice> "))
    ds = []
    for u in range(0, users):
        ds = ds + [deltas[u]]
    if choice == "1":
        show(start, ds)
    elif choice == "2":
        one(start, ds)
    elif choice == "3":
        every(start, deltas)
    elif choice == "4":
        deltas = set_amounts(deltas)
    elif choice == "5":
        t = plain(input("users (2 or 3)> "))
        if t == "2" or t == "3":
            users = int(t)
            print("Now " + t + " users.")
        elif t == "":
            print("Cancelled.")
        else:
            print("Type 2 or 3.")
    elif choice == "6":
        running = False
    else:
        print("Pick a number from 1 to 6.")
print("Bye.")
```

### update.eml

```eml
# P130 lost update - users each read a shared value, add their own amount,
# and write it back, one step a turn as a schedule says. As in the corpus
# case lost-update-schedule, a write made from a value read before someone
# else's write throws that write away. With a version check, a write goes
# through only if nobody has written since its read; otherwise the user
# reads again and starts over.
#
# A user's state is [step, value read, version read, whose updates the value
# read holds]; step 0 reads, 1 adds, 2 writes, 3 is done. The shared value
# is [value, version, whose updates it holds].

def new_state(n):
    [] => out
    for i in [1:n]:
        out + [[0, 0, 0, []]] => out
    return out

def turn(users, shared, u, deltas, checked):
    # one turn for user u: [what happened]; users and shared change in place
    users[u] => s
    if s[0] == 0:
        shared[0] => s[1]
        shared[1] => s[2]
        shared[2] => s[3]
        1 => s[0]
        return "reads " + str(s[1])
    if s[0] == 1:
        s[1] + deltas[u] => s[1]
        2 => s[0]
        return "adds " + signed(deltas[u]) + ", making " + str(s[1])
    if s[0] == 2:
        if checked and shared[1] != s[2]:
            0 => s[0]
            return "finds the version moved from " + str(s[2]) + " to " + str(shared[1]) + ": its write is refused, and it starts over"
        shared[0] => old
        s[1] => shared[0]
        shared[1] + 1 => shared[1]
        s[3] + [u] => shared[2]
        3 => s[0]
        return "writes " + str(s[1]) + " over " + str(old)
    return "is done"

def signed(n):
    if n < 0:
        return str(n)
    return "+" + str(n)

def run(start, deltas, schedule, checked):
    # [trace of [user, what], final value, refused writes, turns used, whose
    # updates are lost]: the schedule, then every user still going, lowest
    # first, until all done
    len(deltas) => n
    new_state(n) => users
    [start, 0, []] => shared
    [] => trace
    0 => refused
    for u in schedule:
        turn(users, shared, u, deltas, checked) => w
        trace + [[u, w]] => trace
        if len(w) > 5 and w[0:5] == "finds":
            refused + 1 => refused
    True => going
    0 => extra
    while going and extra < 200:
        False => going
        for u in [0:n - 1]:
            if not going and users[u][0] < 3:
                turn(users, shared, u, deltas, checked) => w
                trace + [[u, w]] => trace
                if len(w) > 5 and w[0:5] == "finds":
                    refused + 1 => refused
                True => going
                extra + 1 => extra
    [] => lost
    for u in [0:n - 1]:
        False => kept
        for v in shared[2]:
            if v == u:
                True => kept
        if not kept:
            lost + [u] => lost
    return [trace, shared[0], refused, len(trace), lost]

def interleavings(n):
    # every order of n users' three turns
    [] => counts
    for i in [1:n]:
        counts + [3] => counts
    [[[], counts]] => todo
    [] => out
    while len(todo) > 0:
        todo[len(todo) - 1] => item
        todo[0:len(todo) - 1] => todo
        0 => left
        for c in item[1]:
            left + c => left
        if left == 0:
            out + [item[0]] => out
        else:
            for u in [0:n - 1]:
                if item[1][u] > 0:
                    [] => nc
                    for v in [0:n - 1]:
                        if v == u:
                            nc + [item[1][v] - 1] => nc
                        else:
                            nc + [item[1][v]] => nc
                    todo + [[item[0] + [u], nc]] => todo
    return out

def census(start, deltas, checked):
    # over every interleaving: [orders, orders losing an update, refused
    # writes in all, the most turns any order needs]
    0 => lost
    0 => refused
    0 => most
    interleavings(len(deltas)) => orders
    for o in orders:
        run(start, deltas, o, checked) => r
        if len(r[4]) > 0:
            lost + 1 => lost
        refused + r[2] => refused
        if r[3] > most:
            r[3] => most
    return [len(orders), lost, refused, most]
```

Python projection of update.eml:

```python
def new_state(n):
    out = []
    for i in range(1, n+1):
        out = out + [[0, 0, 0, []]]
    return out

def turn(users, shared, u, deltas, checked):
    s = users[u]
    if s[0] == 0:
        s[1] = shared[0]
        s[2] = shared[1]
        s[3] = shared[2]
        s[0] = 1
        return "reads " + str(s[1])
    if s[0] == 1:
        s[1] = s[1] + deltas[u]
        s[0] = 2
        return "adds " + signed(deltas[u]) + ", making " + str(s[1])
    if s[0] == 2:
        if checked and shared[1] != s[2]:
            s[0] = 0
            return "finds the version moved from " + str(s[2]) + " to " + str(shared[1]) + ": its write is refused, and it starts over"
        old = shared[0]
        shared[0] = s[1]
        shared[1] = shared[1] + 1
        shared[2] = s[3] + [u]
        s[0] = 3
        return "writes " + str(s[1]) + " over " + str(old)
    return "is done"

def signed(n):
    if n < 0:
        return str(n)
    return "+" + str(n)

def run(start, deltas, schedule, checked):
    n = len(deltas)
    users = new_state(n)
    shared = [start, 0, []]
    trace = []
    refused = 0
    for u in schedule:
        w = turn(users, shared, u, deltas, checked)
        trace = trace + [[u, w]]
        if len(w) > 5 and w[0:5] == "finds":
            refused = refused + 1
    going = True
    extra = 0
    while going and extra < 200:
        going = False
        for u in range(0, n):
            if not going and users[u][0] < 3:
                w = turn(users, shared, u, deltas, checked)
                trace = trace + [[u, w]]
                if len(w) > 5 and w[0:5] == "finds":
                    refused = refused + 1
                going = True
                extra = extra + 1
    lost = []
    for u in range(0, n):
        kept = False
        for v in shared[2]:
            if v == u:
                kept = True
        if not kept:
            lost = lost + [u]
    return [trace, shared[0], refused, len(trace), lost]

def interleavings(n):
    counts = []
    for i in range(1, n+1):
        counts = counts + [3]
    todo = [[[], counts]]
    out = []
    while len(todo) > 0:
        item = todo[len(todo) - 1]
        todo = todo[0:len(todo) - 1]
        left = 0
        for c in item[1]:
            left = left + c
        if left == 0:
            out = out + [item[0]]
        else:
            for u in range(0, n):
                if item[1][u] > 0:
                    nc = []
                    for v in range(0, n):
                        if v == u:
                            nc = nc + [item[1][v] - 1]
                        else:
                            nc = nc + [item[1][v]]
                    todo = todo + [[item[0] + [u], nc]]
    return out

def census(start, deltas, checked):
    lost = 0
    refused = 0
    most = 0
    orders = interleavings(len(deltas))
    for o in orders:
        r = run(start, deltas, o, checked)
        if len(r[4]) > 0:
            lost = lost + 1
        refused = refused + r[2]
        if r[3] > most:
            most = r[3]
    return [len(orders), lost, refused, most]
```

## README

# P130 - Lost update

Users each read a shared value, add their own amount and write it back,
one step a turn, in the order a schedule gives. A write made from a value
read before someone else's write throws that write away.

- `main.eml` - the menu, the users, one schedule with and without a
  version check, every order counted, the amounts, and two or three users
- `update.eml` - a user's turn, a run of a schedule, every order of the
  users' turns, and the counts

How each part works:

- As in the corpus case `lost-update-schedule`, each user takes three
  turns: read, add, write. The value starts at 100; users add +10, +5
  and -3. The value carries whose updates it holds, so a lost update is
  named even when the amounts would cancel out.
- Without a check, an order loses an update exactly when one user's read
  and write enclose another user's write. Only the orders that run the
  users one after another keep every update: 18 of the 20 orders of two
  users lose one, and 1674 of the 1680 orders of three.
- With a version check, a write goes through only if nobody has written
  since its read; otherwise it is refused, and the user reads again and
  starts over. No order loses an update; two users need 18 writes done
  again over the 20 orders, three need 2970.
- Turns left when the schedule ends are taken by the users still going,
  lowest number first.

What is checked: menu choices 1 to 6; a schedule of user numbers, up to
30 turns; three amounts from -99 to 99, not 0; 2 or 3 users. An empty
answer cancels.

Sessions: `sessions/basic.in` gives:
- the users, then 1 1 1 2 2 2 (one after another) and 1 2 1 2 1 2, where
  user 1's update is lost without a check;
- every order, for two and three users;
- three users with 1 2 3 three times: two updates lost, two writes done
  again with the check.

`sessions/bad-input.in` gives:
- menu choices 0 and x;
- schedules: a cancel, 1 3, 1 x and 31 turns;
- amounts: a cancel, two amounts, 0, x and 100, then 5 -5 3;
- users: a cancel and 4, then 3, and a schedule that loses user 1's +5.

Built on the verified corpus case `lost-update-schedule` (a read, modify
and write that loses another user's write when the steps interleave).