Project P141
Event tickets
One concert's bookings kept by two designs side by side - cancel as an undo and cancel as a state - so a cancel sent twice gives back seats and money twice in one of them, and the extra seats get sold.
2 modules · 2 recorded sessionstext-menu UI in the terminalupdated 2026-10-18
Every screen below was recorded under CPython. When this page was built, the EML interpreter replayed each session from the same input and printed the same bytes.
About
One concert's bookings, kept by two designs side by side: a cancel that undoes what the booking did, and a cancel that sets the booking to cancelled.
main.eml- the menu, the bookings in each design, booking seats, cancelling with the request sent one to three times, and the checkstickets.eml- the hall, the opening bookings, booking, the two cancels, the seats held, what the cancelled bookings paid, and the three checks
How each part works:
- The hall has 10 seats at 25.00. Ana, Ben and Cleo have booked 2, 1 and 4.
- As in the corpus case
cancel-is-not-idempotent, the undo design's cancel is a delta: it gives the seats back and refunds what was paid, every time it is sent. The state design's cancel makes the booking cancelled, and a booking that already is stays as it is. - One cancel of a booking still held does the same in both designs. A cancel sent three times - a slow reply, a click again, a retry - gives back the seats and the money three times in the undo design: Ben's one seat becomes three free seats and 75.00 refunded.
- The extra seats can be sold. Once the undo design has more seats free than the hall has, it takes bookings the state design refuses, and holds 12 seats in a hall of 10; later the state design can take one the undo design has no room for.
- The checks: free seats plus seats held equal the hall, and the refunds equal what the cancelled bookings paid. The state design always passes; the undo design is off by exactly the seats and payments of every cancel after the first. Asking whether each booking says cancelled passes in both and cannot tell them apart.
What is checked: menu choices 1 to 5; a name of 1 to 12 letters and 1 to 4 seats; a booking number that exists in at least one design and a cancel sent 1 to 3 times. An empty answer cancels.
Sessions: sessions/basic.in gives: - the bookings; Ana's booking cancelled once, and Ben's with the cancel sent three times; the checks; - Dan, Eve and Fay booking 4, 4 and 2 seats: in both designs, in the undo design only, and in the state design only; the bookings and the checks.
sessions/bad-input.in gives: - menu choices 0 and x; - booking: a cancel, the name Ann3, then Gus with a cancel, 0, 5 and x seats; - cancelling: a cancel, x, booking 9, then booking 1 with a cancel, 0, 4 and x sends; - Ana's booking cancelled once and then once more; the checks and the bookings.
Built on the verified corpus case cancel-is-not-idempotent (cancel as a delta and cancel as a state, applied one, two and three times).
Recorded sessions
What the screen shows while someone uses the program. Each typed line appears after its prompt, the way a terminal shows it.
bad-input
interpreter: byte-equal== Event tickets ==
One concert's bookings, kept twice: cancel as an undo, and cancel as a state.
1) bookings 2) book seats 3) cancel a booking 4) checks 5) quit
choice> 0
Pick a number from 1 to 5.
1) bookings 2) book seats 3) cancel a booking 4) checks 5) quit
choice> x
Pick a number from 1 to 5.
1) bookings 2) book seats 3) cancel a booking 4) checks 5) quit
choice> 2
name>
Cancelled.
1) bookings 2) book seats 3) cancel a booking 4) checks 5) quit
choice> 2
name> Ann3
Type a name of 1 to 12 letters.
1) bookings 2) book seats 3) cancel a booking 4) checks 5) quit
choice> 2
name> Gus
seats (1 to 4)>
Cancelled.
1) bookings 2) book seats 3) cancel a booking 4) checks 5) quit
choice> 2
name> Gus
seats (1 to 4)> 0
Type a number of seats from 1 to 4.
1) bookings 2) book seats 3) cancel a booking 4) checks 5) quit
choice> 2
name> Gus
seats (1 to 4)> 5
Type a number of seats from 1 to 4.
1) bookings 2) book seats 3) cancel a booking 4) checks 5) quit
choice> 2
name> Gus
seats (1 to 4)> x
Type a number of seats from 1 to 4.
1) bookings 2) book seats 3) cancel a booking 4) checks 5) quit
choice> 3
booking number>
Cancelled.
1) bookings 2) book seats 3) cancel a booking 4) checks 5) quit
choice> 3
booking number> x
Type a booking number.
1) bookings 2) book seats 3) cancel a booking 4) checks 5) quit
choice> 3
booking number> 9
There is no booking 9.
1) bookings 2) book seats 3) cancel a booking 4) checks 5) quit
choice> 3
booking number> 1
times the cancel is sent (1 to 3)>
Cancelled.
1) bookings 2) book seats 3) cancel a booking 4) checks 5) quit
choice> 3
booking number> 1
times the cancel is sent (1 to 3)> 0
Type a number from 1 to 3.
1) bookings 2) book seats 3) cancel a booking 4) checks 5) quit
choice> 3
booking number> 1
times the cancel is sent (1 to 3)> 4
Type a number from 1 to 3.
1) bookings 2) book seats 3) cancel a booking 4) checks 5) quit
choice> 3
booking number> 1
times the cancel is sent (1 to 3)> x
Type a number from 1 to 3.
1) bookings 2) book seats 3) cancel a booking 4) checks 5) quit
choice> 3
booking number> 1
times the cancel is sent (1 to 3)> 1
Booking 1 (Ana, 2 seats, 50.00 paid), the cancel sent 1 time:
undo: seats free 3 -> 5, refunded 0.00 -> 50.00
state: seats free 3 -> 5, refunded 0.00 -> 50.00
One cancel of a booking still held, and the two designs agree.
1) bookings 2) book seats 3) cancel a booking 4) checks 5) quit
choice> 3
booking number> 1
times the cancel is sent (1 to 3)> 1
Booking 1 (Ana, 2 seats, 50.00 paid), the cancel sent 1 time:
undo: seats free 5 -> 7, refunded 50.00 -> 100.00
state: seats free 5 -> 5, refunded 50.00 -> 50.00
Booking 1 was already cancelled. The state design changes nothing; the undo design gave back 2 seats and 50.00 again.
1) bookings 2) book seats 3) cancel a booking 4) checks 5) quit
choice> 4
Checks on each design: undo state
seats free + seats held = 10 no yes
refunded = what cancelled bookings paid no yes
every booking sent a cancel says cancelled yes yes
The undo design: 7 free + 5 held = 12 seats in a hall of 10.
The undo design: 100.00 refunded against 50.00 paid by the cancelled bookings.
Asking whether each booking is cancelled cannot tell the designs apart; only the counts can.
1) bookings 2) book seats 3) cancel a booking 4) checks 5) quit
choice> 1
The hall has 10 seats at 25.00 each.
Undo design: 7 seats free, 100.00 refunded.
1 Ana 2 seats 50.00 cancelled, 100.00 back
2 Ben 1 seat 25.00 confirmed
3 Cleo 4 seats 100.00 confirmed
State design: 5 seats free, 50.00 refunded.
1 Ana 2 seats 50.00 cancelled, 50.00 back
2 Ben 1 seat 25.00 confirmed
3 Cleo 4 seats 100.00 confirmed
1) bookings 2) book seats 3) cancel a booking 4) checks 5) quit
choice> 5
Bye.
What was typed (45 lines)
0
x
2
2
Ann3
2
Gus
2
Gus
0
2
Gus
5
2
Gus
x
3
3
x
3
9
3
1
3
1
0
3
1
4
3
1
x
3
1
1
3
1
1
4
1
5
basic
interpreter: byte-equal== Event tickets ==
One concert's bookings, kept twice: cancel as an undo, and cancel as a state.
1) bookings 2) book seats 3) cancel a booking 4) checks 5) quit
choice> 1
The hall has 10 seats at 25.00 each.
Undo design: 3 seats free, 0.00 refunded.
1 Ana 2 seats 50.00 confirmed
2 Ben 1 seat 25.00 confirmed
3 Cleo 4 seats 100.00 confirmed
State design: 3 seats free, 0.00 refunded.
1 Ana 2 seats 50.00 confirmed
2 Ben 1 seat 25.00 confirmed
3 Cleo 4 seats 100.00 confirmed
1) bookings 2) book seats 3) cancel a booking 4) checks 5) quit
choice> 3
booking number> 1
times the cancel is sent (1 to 3)> 1
Booking 1 (Ana, 2 seats, 50.00 paid), the cancel sent 1 time:
undo: seats free 3 -> 5, refunded 0.00 -> 50.00
state: seats free 3 -> 5, refunded 0.00 -> 50.00
One cancel of a booking still held, and the two designs agree.
1) bookings 2) book seats 3) cancel a booking 4) checks 5) quit
choice> 3
booking number> 2
times the cancel is sent (1 to 3)> 3
Booking 2 (Ben, 1 seat, 25.00 paid), the cancel sent 3 times:
undo: seats free 5 -> 8, refunded 50.00 -> 125.00
state: seats free 5 -> 6, refunded 50.00 -> 75.00
Both say booking 2 is cancelled. The undo design gave back 2 seats and 50.00 more than the state design: each send undid the booking again.
1) bookings 2) book seats 3) cancel a booking 4) checks 5) quit
choice> 4
Checks on each design: undo state
seats free + seats held = 10 no yes
refunded = what cancelled bookings paid no yes
every booking sent a cancel says cancelled yes yes
The undo design: 8 free + 4 held = 12 seats in a hall of 10.
The undo design: 125.00 refunded against 75.00 paid by the cancelled bookings.
Asking whether each booking is cancelled cannot tell the designs apart; only the counts can.
1) bookings 2) book seats 3) cancel a booking 4) checks 5) quit
choice> 2
name> Dan
seats (1 to 4)> 4
Booking 4: Dan, 4 seats, 100.00, in both designs.
1) bookings 2) book seats 3) cancel a booking 4) checks 5) quit
choice> 2
name> Eve
seats (1 to 4)> 4
Booking 5: Eve, 4 seats, 100.00 - taken by the undo design only; the state design has 2 free.
The undo design now holds 12 seats in a hall of 10.
1) bookings 2) book seats 3) cancel a booking 4) checks 5) quit
choice> 2
name> Fay
seats (1 to 4)> 2
Booking 6: Fay, 2 seats, 50.00 - taken by the state design only; the undo design has 0 free.
1) bookings 2) book seats 3) cancel a booking 4) checks 5) quit
choice> 1
The hall has 10 seats at 25.00 each.
Undo design: 0 seats free, 125.00 refunded.
1 Ana 2 seats 50.00 cancelled, 50.00 back
2 Ben 1 seat 25.00 cancelled, 75.00 back
3 Cleo 4 seats 100.00 confirmed
4 Dan 4 seats 100.00 confirmed
5 Eve 4 seats 100.00 confirmed
State design: 0 seats free, 75.00 refunded.
1 Ana 2 seats 50.00 cancelled, 50.00 back
2 Ben 1 seat 25.00 cancelled, 25.00 back
3 Cleo 4 seats 100.00 confirmed
4 Dan 4 seats 100.00 confirmed
6 Fay 2 seats 50.00 confirmed
1) bookings 2) book seats 3) cancel a booking 4) checks 5) quit
choice> 4
Checks on each design: undo state
seats free + seats held = 10 no yes
refunded = what cancelled bookings paid no yes
every booking sent a cancel says cancelled yes yes
The undo design: 0 free + 12 held = 12 seats in a hall of 10.
The undo design: 125.00 refunded against 75.00 paid by the cancelled bookings.
Asking whether each booking is cancelled cannot tell the designs apart; only the counts can.
1) bookings 2) book seats 3) cancel a booking 4) checks 5) quit
choice> 5
Bye.
What was typed (20 lines)
1
3
1
1
3
2
3
4
2
Dan
4
2
Eve
4
2
Fay
2
1
4
5
Modules
The program as written, entry module first. Each module transpiles to its own Python file, which is what eml project run executes.
main.eml(entry)
eml# P141 event tickets: one concert's bookings kept by two designs side by
# side - cancel as an undo and cancel as a state - booking seats, cancelling
# with the request sent one to three times, and the checks on each.
import tickets
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 money(c):
c % 100 => p
if p < 10:
return str(int((c - p) / 100)) + ".0" + str(p)
return str(int((c - p) / 100)) + "." + str(p)
def seats_word(n):
if n == 1:
return "1 seat"
return str(n) + " seats"
def times_word(n):
if n == 1:
return "1 time"
return str(n) + " times"
def digits(t, most):
if len(t) == 0 or len(t) > most:
return False
for c in t:
if c < "0" or c > "9":
return False
return True
def letters(t):
if len(t) == 0 or len(t) > 12:
return False
for c in t:
if not ((c >= "a" and c <= "z") or (c >= "A" and c <= "Z")):
return False
return True
def show_design(label, led):
(label + ": " + seats_word(led[0]) + " free, " + money(led[1]) + " refunded.") ^0
for b in led[2]:
(" " + lpad(str(b[0]), 2) + " " + pad(b[1], 13) + pad(seats_word(b[2]), 9) + lpad(money(b[3]), 6) + " " + b[4]) => line
if b[5] > 0:
line + ", " + money(b[5]) + " back" => line
line ^0
def show(u, s):
tickets.venue() => v
("The hall has " + str(v[0]) + " seats at " + money(v[1]) + " each.") ^0
show_design("Undo design", u)
show_design("State design", s)
def book(u, s, n):
plain(input("name> ")) => name
if name == "":
"Cancelled." ^0
return [u, s, n]
if not letters(name):
"Type a name of 1 to 12 letters." ^0
return [u, s, n]
plain(input("seats (1 to 4)> ")) => t
if t == "":
"Cancelled." ^0
return [u, s, n]
if not digits(t, 1) or int(t) < 1 or int(t) > 4:
"Type a number of seats from 1 to 4." ^0
return [u, s, n]
int(t) => k
tickets.book(u, n, name, k) => u2
tickets.book(s, n, name, k) => s2
len(u2[2]) > len(u[2]) => in_u
len(s2[2]) > len(s[2]) => in_s
("Booking " + str(n) + ": " + name + ", " + seats_word(k) + ", " + money(k * tickets.venue()[1])) => head
if in_u and in_s:
(head + ", in both designs.") ^0
elif in_u:
(head + " - taken by the undo design only; the state design has " + str(s[0]) + " free.") ^0
tickets.held(u2) => h
if h > tickets.venue()[0]:
("The undo design now holds " + str(h) + " seats in a hall of " + str(tickets.venue()[0]) + ".") ^0
elif in_s:
(head + " - taken by the state design only; the undo design has " + str(u[0]) + " free.") ^0
else:
if u[0] == s[0]:
("Not enough seats: " + str(s[0]) + " free in both designs.") ^0
else:
("Not enough seats: the undo design has " + str(u[0]) + " free, the state design " + str(s[0]) + ".") ^0
return [u, s, n]
return [u2, s2, n + 1]
def effect(label, before, after):
(" " + label + "seats free " + str(before[0]) + " -> " + str(after[0]) + ", refunded " + money(before[1]) + " -> " + money(after[1])) ^0
def cancel(u, s):
plain(input("booking number> ")) => t
if t == "":
"Cancelled." ^0
return [u, s]
if not digits(t, 3):
"Type a booking number." ^0
return [u, s]
int(t) => n
tickets.find(u, n) => ku
tickets.find(s, n) => ks
if ku < 0 and ks < 0:
("There is no booking " + str(n) + ".") ^0
return [u, s]
plain(input("times the cancel is sent (1 to 3)> ")) => r
if r == "":
"Cancelled." ^0
return [u, s]
if not digits(r, 1) or int(r) < 1 or int(r) > 3:
"Type a number from 1 to 3." ^0
return [u, s]
int(r) => times
if ku >= 0:
u[2][ku] => b
else:
s[2][ks] => b
("Booking " + str(n) + " (" + b[1] + ", " + seats_word(b[2]) + ", " + money(b[3]) + " paid), the cancel sent " + times_word(times) + ":") ^0
u => u2
s => s2
0 => i
while i < times:
if ku >= 0:
tickets.cancel_undo(u2, n) => u2
if ks >= 0:
tickets.cancel_state(s2, n) => s2
i + 1 => i
if ku >= 0:
effect("undo: ", u, u2)
else:
(" undo: no booking " + str(n) + " here; this design refused it.") ^0
if ks >= 0:
effect("state: ", s, s2)
else:
(" state: no booking " + str(n) + " here; this design refused it.") ^0
if ku >= 0 and ks >= 0:
u2[0] - u[0] => du
s2[0] - s[0] => ds
u2[1] - u[1] => mu
s2[1] - s[1] => ms
if s[2][ks][4] == "cancelled":
("Booking " + str(n) + " was already cancelled. The state design changes nothing; the undo design gave back " + seats_word(du) + " and " + money(mu) + " again.") ^0
elif du == ds and mu == ms:
"One cancel of a booking still held, and the two designs agree." ^0
else:
("Both say booking " + str(n) + " is cancelled. The undo design gave back " + seats_word(du - ds) + " and " + money(mu - ms) + " more than the state design: each send undid the booking again.") ^0
return [u2, s2]
def yes(ok):
if ok:
return "yes"
return "no"
def checks(u, s):
tickets.venue()[0] => cap
"Checks on each design: undo state" ^0
(" " + pad("seats free + seats held = " + str(cap), 46) + pad(yes(tickets.seats_ok(u)), 7) + yes(tickets.seats_ok(s))) ^0
(" " + pad("refunded = what cancelled bookings paid", 46) + pad(yes(tickets.refunds_ok(u)), 7) + yes(tickets.refunds_ok(s))) ^0
(" " + pad("every booking sent a cancel says cancelled", 46) + pad(yes(tickets.statuses_ok(u)), 7) + yes(tickets.statuses_ok(s))) ^0
tickets.seats_ok(u) and tickets.refunds_ok(u) => u_ok
tickets.seats_ok(s) and tickets.refunds_ok(s) => s_ok
if u_ok and s_ok:
"Both designs pass every check." ^0
else:
if not tickets.seats_ok(u):
("The undo design: " + str(u[0]) + " free + " + str(tickets.held(u)) + " held = " + str(u[0] + tickets.held(u)) + " seats in a hall of " + str(cap) + ".") ^0
if not tickets.refunds_ok(u):
("The undo design: " + money(u[1]) + " refunded against " + money(tickets.owed_back(u)) + " paid by the cancelled bookings.") ^0
if tickets.statuses_ok(u) and tickets.statuses_ok(s):
"Asking whether each booking is cancelled cannot tell the designs apart; only the counts can." ^0
tickets.opening_ledger() => u
tickets.opening_ledger() => s
len(tickets.opening()) + 1 => next_number
"== Event tickets ==" ^0
"One concert's bookings, kept twice: cancel as an undo, and cancel as a state." ^0
True => running
while running:
"" ^0
"1) bookings 2) book seats 3) cancel a booking 4) checks 5) quit" ^0
plain(input("choice> ")) => choice
if choice == "1":
show(u, s)
elif choice == "2":
book(u, s, next_number) => r
r[0] => u
r[1] => s
r[2] => next_number
elif choice == "3":
cancel(u, s) => r
r[0] => u
r[1] => s
elif choice == "4":
checks(u, s)
elif choice == "5":
False => running
else:
"Pick a number from 1 to 5." ^0
"Bye." ^0
Python projection (main.py)
import tickets
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 money(c):
p = c % 100
if p < 10:
return str(int((c - p) / 100)) + ".0" + str(p)
return str(int((c - p) / 100)) + "." + str(p)
def seats_word(n):
if n == 1:
return "1 seat"
return str(n) + " seats"
def times_word(n):
if n == 1:
return "1 time"
return str(n) + " times"
def digits(t, most):
if len(t) == 0 or len(t) > most:
return False
for c in t:
if c < "0" or c > "9":
return False
return True
def letters(t):
if len(t) == 0 or len(t) > 12:
return False
for c in t:
if not (c >= "a" and c <= "z" or c >= "A" and c <= "Z"):
return False
return True
def show_design(label, led):
print(label + ": " + seats_word(led[0]) + " free, " + money(led[1]) + " refunded.")
for b in led[2]:
line = " " + lpad(str(b[0]), 2) + " " + pad(b[1], 13) + pad(seats_word(b[2]), 9) + lpad(money(b[3]), 6) + " " + b[4]
if b[5] > 0:
line = line + ", " + money(b[5]) + " back"
print(line)
def show(u, s):
v = tickets.venue()
print("The hall has " + str(v[0]) + " seats at " + money(v[1]) + " each.")
show_design("Undo design", u)
show_design("State design", s)
def book(u, s, n):
name = plain(input("name> "))
if name == "":
print("Cancelled.")
return [u, s, n]
if not letters(name):
print("Type a name of 1 to 12 letters.")
return [u, s, n]
t = plain(input("seats (1 to 4)> "))
if t == "":
print("Cancelled.")
return [u, s, n]
if not digits(t, 1) or int(t) < 1 or int(t) > 4:
print("Type a number of seats from 1 to 4.")
return [u, s, n]
k = int(t)
u2 = tickets.book(u, n, name, k)
s2 = tickets.book(s, n, name, k)
in_u = len(u2[2]) > len(u[2])
in_s = len(s2[2]) > len(s[2])
head = "Booking " + str(n) + ": " + name + ", " + seats_word(k) + ", " + money(k * tickets.venue()[1])
if in_u and in_s:
print(head + ", in both designs.")
elif in_u:
print(head + " - taken by the undo design only; the state design has " + str(s[0]) + " free.")
h = tickets.held(u2)
if h > tickets.venue()[0]:
print("The undo design now holds " + str(h) + " seats in a hall of " + str(tickets.venue()[0]) + ".")
elif in_s:
print(head + " - taken by the state design only; the undo design has " + str(u[0]) + " free.")
else:
if u[0] == s[0]:
print("Not enough seats: " + str(s[0]) + " free in both designs.")
else:
print("Not enough seats: the undo design has " + str(u[0]) + " free, the state design " + str(s[0]) + ".")
return [u, s, n]
return [u2, s2, n + 1]
def effect(label, before, after):
print(" " + label + "seats free " + str(before[0]) + " -> " + str(after[0]) + ", refunded " + money(before[1]) + " -> " + money(after[1]))
def cancel(u, s):
t = plain(input("booking number> "))
if t == "":
print("Cancelled.")
return [u, s]
if not digits(t, 3):
print("Type a booking number.")
return [u, s]
n = int(t)
ku = tickets.find(u, n)
ks = tickets.find(s, n)
if ku < 0 and ks < 0:
print("There is no booking " + str(n) + ".")
return [u, s]
r = plain(input("times the cancel is sent (1 to 3)> "))
if r == "":
print("Cancelled.")
return [u, s]
if not digits(r, 1) or int(r) < 1 or int(r) > 3:
print("Type a number from 1 to 3.")
return [u, s]
times = int(r)
if ku >= 0:
b = u[2][ku]
else:
b = s[2][ks]
print("Booking " + str(n) + " (" + b[1] + ", " + seats_word(b[2]) + ", " + money(b[3]) + " paid), the cancel sent " + times_word(times) + ":")
u2 = u
s2 = s
i = 0
while i < times:
if ku >= 0:
u2 = tickets.cancel_undo(u2, n)
if ks >= 0:
s2 = tickets.cancel_state(s2, n)
i = i + 1
if ku >= 0:
effect("undo: ", u, u2)
else:
print(" undo: no booking " + str(n) + " here; this design refused it.")
if ks >= 0:
effect("state: ", s, s2)
else:
print(" state: no booking " + str(n) + " here; this design refused it.")
if ku >= 0 and ks >= 0:
du = u2[0] - u[0]
ds = s2[0] - s[0]
mu = u2[1] - u[1]
ms = s2[1] - s[1]
if s[2][ks][4] == "cancelled":
print("Booking " + str(n) + " was already cancelled. The state design changes nothing; the undo design gave back " + seats_word(du) + " and " + money(mu) + " again.")
elif du == ds and mu == ms:
print("One cancel of a booking still held, and the two designs agree.")
else:
print("Both say booking " + str(n) + " is cancelled. The undo design gave back " + seats_word(du - ds) + " and " + money(mu - ms) + " more than the state design: each send undid the booking again.")
return [u2, s2]
def yes(ok):
if ok:
return "yes"
return "no"
def checks(u, s):
cap = tickets.venue()[0]
print("Checks on each design: undo state")
print(" " + pad("seats free + seats held = " + str(cap), 46) + pad(yes(tickets.seats_ok(u)), 7) + yes(tickets.seats_ok(s)))
print(" " + pad("refunded = what cancelled bookings paid", 46) + pad(yes(tickets.refunds_ok(u)), 7) + yes(tickets.refunds_ok(s)))
print(" " + pad("every booking sent a cancel says cancelled", 46) + pad(yes(tickets.statuses_ok(u)), 7) + yes(tickets.statuses_ok(s)))
u_ok = tickets.seats_ok(u) and tickets.refunds_ok(u)
s_ok = tickets.seats_ok(s) and tickets.refunds_ok(s)
if u_ok and s_ok:
print("Both designs pass every check.")
else:
if not tickets.seats_ok(u):
print("The undo design: " + str(u[0]) + " free + " + str(tickets.held(u)) + " held = " + str(u[0] + tickets.held(u)) + " seats in a hall of " + str(cap) + ".")
if not tickets.refunds_ok(u):
print("The undo design: " + money(u[1]) + " refunded against " + money(tickets.owed_back(u)) + " paid by the cancelled bookings.")
if tickets.statuses_ok(u) and tickets.statuses_ok(s):
print("Asking whether each booking is cancelled cannot tell the designs apart; only the counts can.")
u = tickets.opening_ledger()
s = tickets.opening_ledger()
next_number = len(tickets.opening()) + 1
print("== Event tickets ==")
print("One concert's bookings, kept twice: cancel as an undo, and cancel as a state.")
running = True
while running:
print("")
print("1) bookings 2) book seats 3) cancel a booking 4) checks 5) quit")
choice = plain(input("choice> "))
if choice == "1":
show(u, s)
elif choice == "2":
r = book(u, s, next_number)
u = r[0]
s = r[1]
next_number = r[2]
elif choice == "3":
r = cancel(u, s)
u = r[0]
s = r[1]
elif choice == "4":
checks(u, s)
elif choice == "5":
running = False
else:
print("Pick a number from 1 to 5.")
print("Bye.")
tickets.eml
eml# P141 event tickets - seats booked for one concert and cancelled two ways.
# As in the corpus case cancel-is-not-idempotent, a cancel written as "undo
# what the booking did" (give the seats back, refund what was paid) is a
# delta: sent twice, it undoes twice. A cancel written as "this booking is
# cancelled" is a state: reaching it again changes nothing. A ledger is
# [seats free, cents refunded, bookings]; a booking is [number, name, seats,
# cents paid, status, cents refunded, cancels received].
def venue():
# [seats in the hall, price of a seat in cents]
return [10, 2500]
def opening():
# the bookings already made: [name, seats]
return [["Ana", 2], ["Ben", 1], ["Cleo", 4]]
def find(led, number):
0 => i
for b in led[2]:
if b[0] == number:
return i
i + 1 => i
return 0 - 1
def book(led, number, name, seats):
# the ledger with the booking added, or the same ledger when there are
# not enough seats free
if seats > led[0]:
return led
seats * venue()[1] => paid
return [led[0] - seats, led[1], led[2] + [[number, name, seats, paid, "confirmed", 0, 0]]]
def cancel_undo(led, number):
# undo the booking: its seats back, what it paid refunded, every time
find(led, number) => k
led[0] => free
led[1] => refunded
[] => out
0 => i
for b in led[2]:
if i == k:
free + b[2] => free
refunded + b[3] => refunded
out + [[b[0], b[1], b[2], b[3], "cancelled", b[5] + b[3], b[6] + 1]] => out
else:
out + [b] => out
i + 1 => i
return [free, refunded, out]
def cancel_state(led, number):
# make the booking cancelled; one that already is stays as it is
find(led, number) => k
led[0] => free
led[1] => refunded
[] => out
0 => i
for b in led[2]:
if i == k:
if b[4] == "cancelled":
out + [[b[0], b[1], b[2], b[3], b[4], b[5], b[6] + 1]] => out
else:
free + b[2] => free
refunded + b[3] => refunded
out + [[b[0], b[1], b[2], b[3], "cancelled", b[3], b[6] + 1]] => out
else:
out + [b] => out
i + 1 => i
return [free, refunded, out]
def opening_ledger():
[venue()[0], 0, []] => led
1 => n
for b in opening():
book(led, n, b[0], b[1]) => led
n + 1 => n
return led
def held(led):
# seats held by bookings that are not cancelled
0 => h
for b in led[2]:
if b[4] == "confirmed":
h + b[2] => h
return h
def owed_back(led):
# what the cancelled bookings paid: all that should ever be refunded
0 => t
for b in led[2]:
if b[4] == "cancelled":
t + b[3] => t
return t
def seats_ok(led):
return led[0] + held(led) == venue()[0]
def refunds_ok(led):
return led[1] == owed_back(led)
def statuses_ok(led):
# every booking that was sent a cancel says cancelled
for b in led[2]:
if b[6] > 0 and b[4] != "cancelled":
return False
return True
Python projection (tickets.py)
def venue():
return [10, 2500]
def opening():
return [["Ana", 2], ["Ben", 1], ["Cleo", 4]]
def find(led, number):
i = 0
for b in led[2]:
if b[0] == number:
return i
i = i + 1
return 0 - 1
def book(led, number, name, seats):
if seats > led[0]:
return led
paid = seats * venue()[1]
return [led[0] - seats, led[1], led[2] + [[number, name, seats, paid, "confirmed", 0, 0]]]
def cancel_undo(led, number):
k = find(led, number)
free = led[0]
refunded = led[1]
out = []
i = 0
for b in led[2]:
if i == k:
free = free + b[2]
refunded = refunded + b[3]
out = out + [[b[0], b[1], b[2], b[3], "cancelled", b[5] + b[3], b[6] + 1]]
else:
out = out + [b]
i = i + 1
return [free, refunded, out]
def cancel_state(led, number):
k = find(led, number)
free = led[0]
refunded = led[1]
out = []
i = 0
for b in led[2]:
if i == k:
if b[4] == "cancelled":
out = out + [[b[0], b[1], b[2], b[3], b[4], b[5], b[6] + 1]]
else:
free = free + b[2]
refunded = refunded + b[3]
out = out + [[b[0], b[1], b[2], b[3], "cancelled", b[3], b[6] + 1]]
else:
out = out + [b]
i = i + 1
return [free, refunded, out]
def opening_ledger():
led = [venue()[0], 0, []]
n = 1
for b in opening():
led = book(led, n, b[0], b[1])
n = n + 1
return led
def held(led):
h = 0
for b in led[2]:
if b[4] == "confirmed":
h = h + b[2]
return h
def owed_back(led):
t = 0
for b in led[2]:
if b[4] == "cancelled":
t = t + b[3]
return t
def seats_ok(led):
return led[0] + held(led) == venue()[0]
def refunds_ok(led):
return led[1] == owed_back(led)
def statuses_ok(led):
for b in led[2]:
if b[6] > 0 and b[4] != "cancelled":
return False
return True