Project P097
Traffic lights
A junction of two roads with a walk button, run second by second; and an audit that checks every second of a log against six rules and reports every violation - on the run itself, the run with a fault put in, or a log typed in.
2 modules · 2 recorded sessionstext-menu UI in the terminalupdated 2026-10-15
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
A junction of two roads, north-south (NS) and east-west (EW), with a walk button, run second by second. Then an audit that checks every second of a log against six rules and reports every violation, not just the first. It audits the run itself, the run with a fault put in, or a log typed in. The program starts with 120 seconds and the button pressed at seconds 5 and 70.
main.eml- the menu, the run table, the audit report, presses and timingslights.eml- the controller, the audit, the faults, and reading a typed log
How each part works:
- The controller, as in the corpus case
traffic-light-simulator: each phase is held for its time, and an index moves on by hand: NS green, NS yellow, all red, EW green, EW yellow, all red. A press of the button is kept until the next all red ends. Then come walk, flashing, and the next green. A press during a walk is already answered. - A log is one entry a second: NS, EW and the walk signal.
- The audit, as in the corpus case
state-machine-trace-audit: every second is checked against every rule, and every violation is listed. The rules: 1. a light goes green, yellow, red, green, with no other change; 2. never both roads not red; 3. walk or flashing only while both roads are red; 4. the walk signal goes don't walk, walk, flashing, don't walk; 5. a yellow lasts at least the yellow time; 6. a road turns green only after the other has been red for the all red time.
A yellow already showing at second 0, or still showing at the end, is not timed. The report ends with clean seconds plus seconds with a violation, which add up to the seconds checked, and the count for each rule. - The faults: - stuck: NS stays green for the first 2 seconds of EW green; - no-yellow: NS's first yellow shows green instead; - short-yellow: NS's first yellow lasts 1 second; - early-walk: the first walk starts a second before the all red.
Each is put in only where it will show before the log ends.
What is checked: menu choices 1 to 5; a log name; 2 to 60 typed entries of three letters (G, Y or R twice, then D, W or F); up to 10 presses, each within the run, or none; green 5 to 60, yellow 3 to 6, all red 1 to 5, walk 4 to 20 and flashing 3 to 20 seconds, and a run of 30 to 300 seconds. An empty answer cancels.
Sessions: sessions/basic.in gives: - the run, with waits of 20 and 17 seconds; its audit, which is clean; - each fault and the violations it causes: 3, 1, 1 and 1; - a typed log with 8 violations in 5 of its 8 seconds; - presses at 30, 52 and 115: a wait, a press that is already walking, and one with no walk before the run ends; - shorter timings and a 60-second run, which drops the press at 115; its run and clean audit.
sessions/bad-input.in gives: - menu choices 0 and x; the log lizard; a cancel; - typed logs with one entry, a bad letter, and four letters; - presses abc, 120, eleven of them; a cancel; none, then a run with no presses and an early-walk with no walk; - timings out of range for green, yellow, all red and walk; then cancels.
Built on the verified corpus cases traffic-light-simulator (phases held for set times, the index moved on by hand) and state-machine-trace-audit (every event judged, not just the first bad one, and the totals that tie the verdicts together).
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== Traffic lights ==
A junction with a walk button, second by second - and an audit that checks every second of a log against every rule.
1) run 2) audit 3) walk button 4) timings 5) quit
choice> 0
Pick a number from 1 to 5.
1) run 2) audit 3) walk button 4) timings 5) quit
choice> x
Pick a number from 1 to 5.
1) run 2) audit 3) walk button 4) timings 5) quit
choice> 2
Audit the run as it is (run), the run with a fault (stuck, no-yellow, short-yellow, early-walk), or a log you type (own).
log (run, stuck, no-yellow, short-yellow, early-walk or own)> lizard
Type run, stuck, no-yellow, short-yellow, early-walk or own.
1) run 2) audit 3) walk button 4) timings 5) quit
choice> 2
Audit the run as it is (run), the run with a fault (stuck, no-yellow, short-yellow, early-walk), or a log you type (own).
log (run, stuck, no-yellow, short-yellow, early-walk or own)>
Cancelled.
1) run 2) audit 3) walk button 4) timings 5) quit
choice> 2
Audit the run as it is (run), the run with a fault (stuck, no-yellow, short-yellow, early-walk), or a log you type (own).
log (run, stuck, no-yellow, short-yellow, early-walk or own)> own
One entry a second, three letters each: NS and EW (G, Y or R), then the walk signal (D don't walk, W walk, F flashing). For example: GRD YRD RRD RGD.
log (2 to 60 entries)> GRD
Type 2 to 60 entries like GRD, separated by spaces.
1) run 2) audit 3) walk button 4) timings 5) quit
choice> 2
Audit the run as it is (run), the run with a fault (stuck, no-yellow, short-yellow, early-walk), or a log you type (own).
log (run, stuck, no-yellow, short-yellow, early-walk or own)> own
One entry a second, three letters each: NS and EW (G, Y or R), then the walk signal (D don't walk, W walk, F flashing). For example: GRD YRD RRD RGD.
log (2 to 60 entries)> GRD GXD
Type 2 to 60 entries like GRD, separated by spaces.
1) run 2) audit 3) walk button 4) timings 5) quit
choice> 2
Audit the run as it is (run), the run with a fault (stuck, no-yellow, short-yellow, early-walk), or a log you type (own).
log (run, stuck, no-yellow, short-yellow, early-walk or own)> own
One entry a second, three letters each: NS and EW (G, Y or R), then the walk signal (D don't walk, W walk, F flashing). For example: GRD YRD RRD RGD.
log (2 to 60 entries)> GRDD RRD
Type 2 to 60 entries like GRD, separated by spaces.
1) run 2) audit 3) walk button 4) timings 5) quit
choice> 3
Seconds the walk button is pressed, 0 to 119, up to 10 of them; or none.
presses> abc
Type up to 10 seconds from 0 to 119, separated by spaces, or none.
1) run 2) audit 3) walk button 4) timings 5) quit
choice> 3
Seconds the walk button is pressed, 0 to 119, up to 10 of them; or none.
presses> 120
Type up to 10 seconds from 0 to 119, separated by spaces, or none.
1) run 2) audit 3) walk button 4) timings 5) quit
choice> 3
Seconds the walk button is pressed, 0 to 119, up to 10 of them; or none.
presses> 1 2 3 4 5 6 7 8 9 10 11
Type up to 10 seconds from 0 to 119, separated by spaces, or none.
1) run 2) audit 3) walk button 4) timings 5) quit
choice> 3
Seconds the walk button is pressed, 0 to 119, up to 10 of them; or none.
presses>
Cancelled.
1) run 2) audit 3) walk button 4) timings 5) quit
choice> 3
Seconds the walk button is pressed, 0 to 119, up to 10 of them; or none.
presses> none
No presses.
1) run 2) audit 3) walk button 4) timings 5) quit
choice> 1
North-south (NS) and east-west (EW), 120 seconds: green 20, yellow 3, all red 2, walk 7, flashing 5.
seconds NS EW walk
0-19 green red don't walk
20-22 yellow red don't walk
23-24 red red don't walk
25-44 red green don't walk
45-47 red yellow don't walk
48-49 red red don't walk
50-69 green red don't walk
70-72 yellow red don't walk
73-74 red red don't walk
75-94 red green don't walk
95-97 red yellow don't walk
98-99 red red don't walk
100-119 green red don't walk
Nobody pressed the walk button.
The button is answered when the next all red ends: both roads have stopped, then walk, flashing, and the next green.
1) run 2) audit 3) walk button 4) timings 5) quit
choice> 2
Audit the run as it is (run), the run with a fault (stuck, no-yellow, short-yellow, early-walk), or a log you type (own).
log (run, stuck, no-yellow, short-yellow, early-walk or own)> early-walk
Nobody walks in this run; press the button first.
1) run 2) audit 3) walk button 4) timings 5) quit
choice> 4
green (5 to 60)> 4
Type a whole number from 5 to 60.
green (5 to 60)> 61
Type a whole number from 5 to 60.
green (5 to 60)> 20
yellow (3 to 6)> 2
Type a whole number from 3 to 6.
yellow (3 to 6)> 7
Type a whole number from 3 to 6.
yellow (3 to 6)> 3
all red (1 to 5)> 0
Type a whole number from 1 to 5.
all red (1 to 5)> 6
Type a whole number from 1 to 5.
all red (1 to 5)> 4
walk (4 to 20)> 21
Type a whole number from 4 to 20.
walk (4 to 20)>
Cancelled.
1) run 2) audit 3) walk button 4) timings 5) quit
choice> 5
Bye.
What was typed (41 lines)
0
x
2
lizard
2
2
own
GRD
2
own
GRD GXD
2
own
GRDD RRD
3
abc
3
120
3
1 2 3 4 5 6 7 8 9 10 11
3
3
none
1
2
early-walk
4
4
61
20
2
7
3
0
6
4
21
5
basic
interpreter: byte-equal== Traffic lights ==
A junction with a walk button, second by second - and an audit that checks every second of a log against every rule.
1) run 2) audit 3) walk button 4) timings 5) quit
choice> 1
North-south (NS) and east-west (EW), 120 seconds: green 20, yellow 3, all red 2, walk 7, flashing 5.
seconds NS EW walk
0-19 green red don't walk
20-22 yellow red don't walk
23-24 red red don't walk
25-31 red red walk
32-36 red red flashing
37-56 red green don't walk
57-59 red yellow don't walk
60-61 red red don't walk
62-81 green red don't walk
82-84 yellow red don't walk
85-86 red red don't walk
87-93 red red walk
94-98 red red flashing
99-118 red green don't walk
119 red yellow don't walk
Button at second 5: walk at second 25, after 20 seconds.
Button at second 70: walk at second 87, after 17 seconds.
The button is answered when the next all red ends: both roads have stopped, then walk, flashing, and the next green.
1) run 2) audit 3) walk button 4) timings 5) quit
choice> 2
Audit the run as it is (run), the run with a fault (stuck, no-yellow, short-yellow, early-walk), or a log you type (own).
log (run, stuck, no-yellow, short-yellow, early-walk or own)> run
Every second against every rule:
1 a light goes green, yellow, red, green - no other change
2 never both roads not red
3 walk or flashing only while both roads are red
4 the walk signal goes don't walk, walk, flashing, don't walk
5 a yellow lasts at least 3 seconds
6 a road turns green only after the other has been red for 2 seconds
No violations.
120 seconds checked: 120 clean + 0 with a violation.
1) run 2) audit 3) walk button 4) timings 5) quit
choice> 2
Audit the run as it is (run), the run with a fault (stuck, no-yellow, short-yellow, early-walk), or a log you type (own).
log (run, stuck, no-yellow, short-yellow, early-walk or own)> stuck
Fault: NS stays green for the first 2 seconds of EW green, like a stuck relay.
Every second against every rule:
1 a light goes green, yellow, red, green - no other change
2 never both roads not red
3 walk or flashing only while both roads are red
4 the walk signal goes don't walk, walk, flashing, don't walk
5 a yellow lasts at least 3 seconds
6 a road turns green only after the other has been red for 2 seconds
Every violation, not just the first:
second 37, rule 2: NS green and EW green at once
second 38, rule 2: NS green and EW green at once
second 39, rule 1: NS went green to red
120 seconds checked: 117 clean + 3 with a violation.
3 in all - rule 1: 1, rule 2: 2.
1) run 2) audit 3) walk button 4) timings 5) quit
choice> 2
Audit the run as it is (run), the run with a fault (stuck, no-yellow, short-yellow, early-walk), or a log you type (own).
log (run, stuck, no-yellow, short-yellow, early-walk or own)> no-yellow
Fault: NS's first yellow shows green instead.
Every second against every rule:
1 a light goes green, yellow, red, green - no other change
2 never both roads not red
3 walk or flashing only while both roads are red
4 the walk signal goes don't walk, walk, flashing, don't walk
5 a yellow lasts at least 3 seconds
6 a road turns green only after the other has been red for 2 seconds
Every violation, not just the first:
second 23, rule 1: NS went green to red
120 seconds checked: 119 clean + 1 with a violation.
1 in all - rule 1: 1.
1) run 2) audit 3) walk button 4) timings 5) quit
choice> 2
Audit the run as it is (run), the run with a fault (stuck, no-yellow, short-yellow, early-walk), or a log you type (own).
log (run, stuck, no-yellow, short-yellow, early-walk or own)> short-yellow
Fault: NS's first yellow lasts 1 second, with red after.
Every second against every rule:
1 a light goes green, yellow, red, green - no other change
2 never both roads not red
3 walk or flashing only while both roads are red
4 the walk signal goes don't walk, walk, flashing, don't walk
5 a yellow lasts at least 3 seconds
6 a road turns green only after the other has been red for 2 seconds
Every violation, not just the first:
second 21, rule 5: NS yellow lasted only 1 s
120 seconds checked: 119 clean + 1 with a violation.
1 in all - rule 5: 1.
1) run 2) audit 3) walk button 4) timings 5) quit
choice> 2
Audit the run as it is (run), the run with a fault (stuck, no-yellow, short-yellow, early-walk), or a log you type (own).
log (run, stuck, no-yellow, short-yellow, early-walk or own)> early-walk
Fault: the first walk starts a second before the all red, while a road is still yellow.
Every second against every rule:
1 a light goes green, yellow, red, green - no other change
2 never both roads not red
3 walk or flashing only while both roads are red
4 the walk signal goes don't walk, walk, flashing, don't walk
5 a yellow lasts at least 3 seconds
6 a road turns green only after the other has been red for 2 seconds
Every violation, not just the first:
second 22, rule 3: walk showing while NS is yellow
120 seconds checked: 119 clean + 1 with a violation.
1 in all - rule 3: 1.
1) run 2) audit 3) walk button 4) timings 5) quit
choice> 2
Audit the run as it is (run), the run with a fault (stuck, no-yellow, short-yellow, early-walk), or a log you type (own).
log (run, stuck, no-yellow, short-yellow, early-walk or own)> own
One entry a second, three letters each: NS and EW (G, Y or R), then the walk signal (D don't walk, W walk, F flashing). For example: GRD YRD RRD RGD.
log (2 to 60 entries)> GRD GRD YRD RRD RGD RGW GYD RRD
Every second against every rule:
1 a light goes green, yellow, red, green - no other change
2 never both roads not red
3 walk or flashing only while both roads are red
4 the walk signal goes don't walk, walk, flashing, don't walk
5 a yellow lasts at least 3 seconds
6 a road turns green only after the other has been red for 2 seconds
Every violation, not just the first:
second 3, rule 5: NS yellow lasted only 1 s
second 4, rule 6: EW turned green after only 1 s of NS red
second 5, rule 3: walk showing while EW is green
second 6, rule 2: NS green and EW yellow at once
second 6, rule 4: walk signal went walk to don't walk
second 6, rule 6: NS turned green after only 0 s of EW red
second 7, rule 1: NS went green to red
second 7, rule 5: EW yellow lasted only 1 s
8 seconds checked: 3 clean + 5 with a violation.
8 in all - rule 1: 1, rule 2: 1, rule 3: 1, rule 4: 1, rule 5: 2, rule 6: 2.
1) run 2) audit 3) walk button 4) timings 5) quit
choice> 3
Seconds the walk button is pressed, 0 to 119, up to 10 of them; or none.
presses> 30 52 115
Presses at 30, 52, 115.
1) run 2) audit 3) walk button 4) timings 5) quit
choice> 1
North-south (NS) and east-west (EW), 120 seconds: green 20, yellow 3, all red 2, walk 7, flashing 5.
seconds NS EW walk
0-19 green red don't walk
20-22 yellow red don't walk
23-24 red red don't walk
25-44 red green don't walk
45-47 red yellow don't walk
48-49 red red don't walk
50-56 red red walk
57-61 red red flashing
62-81 green red don't walk
82-84 yellow red don't walk
85-86 red red don't walk
87-106 red green don't walk
107-109 red yellow don't walk
110-111 red red don't walk
112-119 green red don't walk
Button at second 30: walk at second 50, after 20 seconds.
Button at second 52: already walking.
Button at second 115: no walk before the run ends.
The button is answered when the next all red ends: both roads have stopped, then walk, flashing, and the next green.
1) run 2) audit 3) walk button 4) timings 5) quit
choice> 4
green (5 to 60)> 10
yellow (3 to 6)> 3
all red (1 to 5)> 1
walk (4 to 20)> 5
flashing (3 to 20)> 3
seconds to run (30 to 300)> 60
Green 10, yellow 3, all red 1, walk 5, flashing 3; 60 seconds.
The run now ends at second 59; dropped: 115.
1) run 2) audit 3) walk button 4) timings 5) quit
choice> 1
North-south (NS) and east-west (EW), 60 seconds: green 10, yellow 3, all red 1, walk 5, flashing 3.
seconds NS EW walk
0-9 green red don't walk
10-12 yellow red don't walk
13 red red don't walk
14-23 red green don't walk
24-26 red yellow don't walk
27 red red don't walk
28-37 green red don't walk
38-40 yellow red don't walk
41 red red don't walk
42-46 red red walk
47-49 red red flashing
50-59 red green don't walk
Button at second 30: walk at second 42, after 12 seconds.
Button at second 52: no walk before the run ends.
The button is answered when the next all red ends: both roads have stopped, then walk, flashing, and the next green.
1) run 2) audit 3) walk button 4) timings 5) quit
choice> 2
Audit the run as it is (run), the run with a fault (stuck, no-yellow, short-yellow, early-walk), or a log you type (own).
log (run, stuck, no-yellow, short-yellow, early-walk or own)> run
Every second against every rule:
1 a light goes green, yellow, red, green - no other change
2 never both roads not red
3 walk or flashing only while both roads are red
4 the walk signal goes don't walk, walk, flashing, don't walk
5 a yellow lasts at least 3 seconds
6 a road turns green only after the other has been red for 1 second
No violations.
60 seconds checked: 60 clean + 0 with a violation.
1) run 2) audit 3) walk button 4) timings 5) quit
choice> 5
Bye.
What was typed (28 lines)
1
2
run
2
stuck
2
no-yellow
2
short-yellow
2
early-walk
2
own
GRD GRD YRD RRD RGD RGW GYD RRD
3
30 52 115
1
4
10
3
1
5
3
60
1
2
run
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# P097 traffic lights: a junction with a walk button, run second by second,
# and an audit that checks every second of a log against every rule -
# the run itself, the run with a fault put in, or a log typed in.
import lights
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 number(s, most):
if len(s) == 0 or len(s) > most:
return -1
0 => n
for c in s:
if not (c >= "0" and c <= "9"):
return -1
n * 10 + int(c) => n
return n
def pad(s, n):
while len(s) < n:
s + " " => s
return s
def lpad(s, n):
while len(s) < n:
" " + s => s
return s
def seconds(n):
if n == 1:
return "1 second"
return str(n) + " seconds"
def ask(prompt, low, high):
while True:
plain(input(prompt + " (" + str(low) + " to " + str(high) + ")> ")) => a
if a == "":
return -1
number(a, 6) => n
if n >= low and n <= high:
return n
("Type a whole number from " + str(low) + " to " + str(high) + ".") ^0
def show_run(cfg, presses):
lights.run(cfg, presses) => log
("North-south (NS) and east-west (EW), " + seconds(cfg[5]) + ": green " + str(cfg[0]) + ", yellow " + str(cfg[1]) + ", all red " + str(cfg[2]) + ", walk " + str(cfg[3]) + ", flashing " + str(cfg[4]) + ".") ^0
" seconds NS EW walk" ^0
for g in lights.runs(log):
" " => span
if g[1] > g[0]:
"-" + pad(str(g[1]), 4) => span
(" " + lpad(str(g[0]), 3) + span + pad(lights.name(g[2][0]), 8) + pad(lights.name(g[2][1]), 8) + lights.name(g[2][2])) ^0
if len(presses) == 0:
"Nobody pressed the walk button." ^0
for w in lights.waits(log, presses):
if w[1] == -1:
("Button at second " + str(w[0]) + ": no walk before the run ends.") ^0
elif w[1] == w[0]:
("Button at second " + str(w[0]) + ": already walking.") ^0
else:
("Button at second " + str(w[0]) + ": walk at second " + str(w[1]) + ", after " + seconds(w[1] - w[0]) + ".") ^0
"The button is answered when the next all red ends: both roads have stopped, then walk, flashing, and the next green." ^0
def report(log, cfg):
lights.audit(log, cfg[1], cfg[2]) => found
"Every second against every rule:" ^0
" 1 a light goes green, yellow, red, green - no other change" ^0
" 2 never both roads not red" ^0
" 3 walk or flashing only while both roads are red" ^0
" 4 the walk signal goes don't walk, walk, flashing, don't walk" ^0
(" 5 a yellow lasts at least " + seconds(cfg[1])) ^0
(" 6 a road turns green only after the other has been red for " + seconds(cfg[2])) ^0
if len(found) == 0:
"No violations." ^0
else:
"Every violation, not just the first:" ^0
{} => bad
[0, 0, 0, 0, 0, 0, 0] => by_rule
for f in found:
(" second " + lpad(str(f[0]), 3) + ", rule " + str(f[1]) + ": " + f[2]) ^0
True => bad[f[0]]
by_rule[f[1]] + 1 => by_rule[f[1]]
len(bad) => n
(str(len(log)) + " seconds checked: " + str(len(log) - n) + " clean + " + str(n) + " with a violation.") ^0
if len(found) > 0:
"" => line
for r in [1:6]:
if by_rule[r] > 0:
if line != "":
line + ", " => line
line + "rule " + str(r) + ": " + str(by_rule[r]) => line
(str(len(found)) + " in all - " + line + ".") ^0
def audit_menu(cfg, presses):
lights.run(cfg, presses) => log
"Audit the run as it is (run), the run with a fault (stuck, no-yellow, short-yellow, early-walk), or a log you type (own)." ^0
plain(input("log (run, stuck, no-yellow, short-yellow, early-walk or own)> ")) => s
if s == "":
"Cancelled." ^0
return
if s == "own":
"One entry a second, three letters each: NS and EW (G, Y or R), then the walk signal (D don't walk, W walk, F flashing). For example: GRD YRD RRD RGD." ^0
lights.parse(plain(input("log (2 to 60 entries)> "))) => log
if len(log) == 0:
"Type 2 to 60 entries like GRD, separated by spaces." ^0
return
elif s == "stuck" or s == "no-yellow" or s == "short-yellow" or s == "early-walk":
lights.inject(log, s, cfg) => faulty
if len(faulty) == 0:
if s == "stuck":
"EW never turns green with 2 seconds to spare in this run." ^0
elif s == "early-walk":
"Nobody walks in this run; press the button first." ^0
else:
"NS never finishes a yellow in this run." ^0
return
faulty => log
if s == "stuck":
"Fault: NS stays green for the first 2 seconds of EW green, like a stuck relay." ^0
elif s == "no-yellow":
"Fault: NS's first yellow shows green instead." ^0
elif s == "short-yellow":
"Fault: NS's first yellow lasts 1 second, with red after." ^0
else:
"Fault: the first walk starts a second before the all red, while a road is still yellow." ^0
elif s != "run":
"Type run, stuck, no-yellow, short-yellow, early-walk or own." ^0
return
report(log, cfg)
def set_presses(cfg, presses):
("Seconds the walk button is pressed, 0 to " + str(cfg[5] - 1) + ", up to 10 of them; or none.") ^0
plain(input("presses> ")) => t
if t == "":
"Cancelled." ^0
return presses
if t == "none":
"No presses." ^0
return []
{} => seen
[] => out
"" => w
True => ok
for c in t + " ":
if c == " ":
if w != "":
number(w, 3) => v
if v < 0 or v >= cfg[5]:
False => ok
elif not (v in seen):
True => seen[v]
out + [v] => out
"" => w
else:
w + c => w
if not ok or len(out) > 10:
("Type up to 10 seconds from 0 to " + str(cfg[5] - 1) + ", separated by spaces, or none.") ^0
return presses
# in order
for i in [1:len(out) - 1]:
i => j
while j > 0 and out[j - 1] > out[j]:
out[j] => x
out[j - 1] => out[j]
x => out[j - 1]
j - 1 => j
"" => line
for v in out:
if line != "":
line + ", " => line
line + str(v) => line
("Presses at " + line + ".") ^0
return out
def timings(cfg):
ask("green", 5, 60) => g
if g == -1:
"Cancelled." ^0
return cfg
ask("yellow", 3, 6) => y
if y == -1:
"Cancelled." ^0
return cfg
ask("all red", 1, 5) => a
if a == -1:
"Cancelled." ^0
return cfg
ask("walk", 4, 20) => w
if w == -1:
"Cancelled." ^0
return cfg
ask("flashing", 3, 20) => f
if f == -1:
"Cancelled." ^0
return cfg
ask("seconds to run", 30, 300) => n
if n == -1:
"Cancelled." ^0
return cfg
("Green " + str(g) + ", yellow " + str(y) + ", all red " + str(a) + ", walk " + str(w) + ", flashing " + str(f) + "; " + seconds(n) + ".") ^0
return [g, y, a, w, f, n]
[20, 3, 2, 7, 5, 120] => cfg
[5, 70] => presses
"== Traffic lights ==" ^0
"A junction with a walk button, second by second - and an audit that checks every second of a log against every rule." ^0
True => running
while running:
"" ^0
"1) run 2) audit 3) walk button 4) timings 5) quit" ^0
plain(input("choice> ")) => choice
if choice == "1":
show_run(cfg, presses)
elif choice == "2":
audit_menu(cfg, presses)
elif choice == "3":
set_presses(cfg, presses) => presses
elif choice == "4":
timings(cfg) => new
if new[5] != cfg[5]:
[] => kept
for v in presses:
if v < new[5]:
kept + [v] => kept
if len(kept) < len(presses):
"" => line
for v in presses:
if v >= new[5]:
if line != "":
line + ", " => line
line + str(v) => line
("The run now ends at second " + str(new[5] - 1) + "; dropped: " + line + ".") ^0
kept => presses
new => cfg
elif choice == "5":
False => running
else:
"Pick a number from 1 to 5." ^0
"Bye." ^0
Python projection (main.py)
import lights
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 number(s, most):
if len(s) == 0 or len(s) > most:
return -1
n = 0
for c in s:
if not (c >= "0" and c <= "9"):
return -1
n = n * 10 + int(c)
return n
def pad(s, n):
while len(s) < n:
s = s + " "
return s
def lpad(s, n):
while len(s) < n:
s = " " + s
return s
def seconds(n):
if n == 1:
return "1 second"
return str(n) + " seconds"
def ask(prompt, low, high):
while True:
a = plain(input(prompt + " (" + str(low) + " to " + str(high) + ")> "))
if a == "":
return -1
n = number(a, 6)
if n >= low and n <= high:
return n
print("Type a whole number from " + str(low) + " to " + str(high) + ".")
def show_run(cfg, presses):
log = lights.run(cfg, presses)
print("North-south (NS) and east-west (EW), " + seconds(cfg[5]) + ": green " + str(cfg[0]) + ", yellow " + str(cfg[1]) + ", all red " + str(cfg[2]) + ", walk " + str(cfg[3]) + ", flashing " + str(cfg[4]) + ".")
print(" seconds NS EW walk")
for g in lights.runs(log):
span = " "
if g[1] > g[0]:
span = "-" + pad(str(g[1]), 4)
print(" " + lpad(str(g[0]), 3) + span + pad(lights.name(g[2][0]), 8) + pad(lights.name(g[2][1]), 8) + lights.name(g[2][2]))
if len(presses) == 0:
print("Nobody pressed the walk button.")
for w in lights.waits(log, presses):
if w[1] == -1:
print("Button at second " + str(w[0]) + ": no walk before the run ends.")
elif w[1] == w[0]:
print("Button at second " + str(w[0]) + ": already walking.")
else:
print("Button at second " + str(w[0]) + ": walk at second " + str(w[1]) + ", after " + seconds(w[1] - w[0]) + ".")
print("The button is answered when the next all red ends: both roads have stopped, then walk, flashing, and the next green.")
def report(log, cfg):
found = lights.audit(log, cfg[1], cfg[2])
print("Every second against every rule:")
print(" 1 a light goes green, yellow, red, green - no other change")
print(" 2 never both roads not red")
print(" 3 walk or flashing only while both roads are red")
print(" 4 the walk signal goes don't walk, walk, flashing, don't walk")
print(" 5 a yellow lasts at least " + seconds(cfg[1]))
print(" 6 a road turns green only after the other has been red for " + seconds(cfg[2]))
if len(found) == 0:
print("No violations.")
else:
print("Every violation, not just the first:")
bad = {}
by_rule = [0, 0, 0, 0, 0, 0, 0]
for f in found:
print(" second " + lpad(str(f[0]), 3) + ", rule " + str(f[1]) + ": " + f[2])
bad[f[0]] = True
by_rule[f[1]] = by_rule[f[1]] + 1
n = len(bad)
print(str(len(log)) + " seconds checked: " + str(len(log) - n) + " clean + " + str(n) + " with a violation.")
if len(found) > 0:
line = ""
for r in range(1, 7):
if by_rule[r] > 0:
if line != "":
line = line + ", "
line = line + "rule " + str(r) + ": " + str(by_rule[r])
print(str(len(found)) + " in all - " + line + ".")
def audit_menu(cfg, presses):
log = lights.run(cfg, presses)
print("Audit the run as it is (run), the run with a fault (stuck, no-yellow, short-yellow, early-walk), or a log you type (own).")
s = plain(input("log (run, stuck, no-yellow, short-yellow, early-walk or own)> "))
if s == "":
print("Cancelled.")
return
if s == "own":
print("One entry a second, three letters each: NS and EW (G, Y or R), then the walk signal (D don't walk, W walk, F flashing). For example: GRD YRD RRD RGD.")
log = lights.parse(plain(input("log (2 to 60 entries)> ")))
if len(log) == 0:
print("Type 2 to 60 entries like GRD, separated by spaces.")
return
elif s == "stuck" or s == "no-yellow" or s == "short-yellow" or s == "early-walk":
faulty = lights.inject(log, s, cfg)
if len(faulty) == 0:
if s == "stuck":
print("EW never turns green with 2 seconds to spare in this run.")
elif s == "early-walk":
print("Nobody walks in this run; press the button first.")
else:
print("NS never finishes a yellow in this run.")
return
log = faulty
if s == "stuck":
print("Fault: NS stays green for the first 2 seconds of EW green, like a stuck relay.")
elif s == "no-yellow":
print("Fault: NS's first yellow shows green instead.")
elif s == "short-yellow":
print("Fault: NS's first yellow lasts 1 second, with red after.")
else:
print("Fault: the first walk starts a second before the all red, while a road is still yellow.")
elif s != "run":
print("Type run, stuck, no-yellow, short-yellow, early-walk or own.")
return
report(log, cfg)
def set_presses(cfg, presses):
print("Seconds the walk button is pressed, 0 to " + str(cfg[5] - 1) + ", up to 10 of them; or none.")
t = plain(input("presses> "))
if t == "":
print("Cancelled.")
return presses
if t == "none":
print("No presses.")
return []
seen = {}
out = []
w = ""
ok = True
for c in t + " ":
if c == " ":
if w != "":
v = number(w, 3)
if v < 0 or v >= cfg[5]:
ok = False
elif not v in seen:
seen[v] = True
out = out + [v]
w = ""
else:
w = w + c
if not ok or len(out) > 10:
print("Type up to 10 seconds from 0 to " + str(cfg[5] - 1) + ", separated by spaces, or none.")
return presses
for i in range(1, len(out)):
j = i
while j > 0 and out[j - 1] > out[j]:
x = out[j]
out[j] = out[j - 1]
out[j - 1] = x
j = j - 1
line = ""
for v in out:
if line != "":
line = line + ", "
line = line + str(v)
print("Presses at " + line + ".")
return out
def timings(cfg):
g = ask("green", 5, 60)
if g == -1:
print("Cancelled.")
return cfg
y = ask("yellow", 3, 6)
if y == -1:
print("Cancelled.")
return cfg
a = ask("all red", 1, 5)
if a == -1:
print("Cancelled.")
return cfg
w = ask("walk", 4, 20)
if w == -1:
print("Cancelled.")
return cfg
f = ask("flashing", 3, 20)
if f == -1:
print("Cancelled.")
return cfg
n = ask("seconds to run", 30, 300)
if n == -1:
print("Cancelled.")
return cfg
print("Green " + str(g) + ", yellow " + str(y) + ", all red " + str(a) + ", walk " + str(w) + ", flashing " + str(f) + "; " + seconds(n) + ".")
return [g, y, a, w, f, n]
cfg = [20, 3, 2, 7, 5, 120]
presses = [5, 70]
print("== Traffic lights ==")
print("A junction with a walk button, second by second - and an audit that checks every second of a log against every rule.")
running = True
while running:
print("")
print("1) run 2) audit 3) walk button 4) timings 5) quit")
choice = plain(input("choice> "))
if choice == "1":
show_run(cfg, presses)
elif choice == "2":
audit_menu(cfg, presses)
elif choice == "3":
presses = set_presses(cfg, presses)
elif choice == "4":
new = timings(cfg)
if new[5] != cfg[5]:
kept = []
for v in presses:
if v < new[5]:
kept = kept + [v]
if len(kept) < len(presses):
line = ""
for v in presses:
if v >= new[5]:
if line != "":
line = line + ", "
line = line + str(v)
print("The run now ends at second " + str(new[5] - 1) + "; dropped: " + line + ".")
presses = kept
cfg = new
elif choice == "5":
running = False
else:
print("Pick a number from 1 to 5.")
print("Bye.")
lights.eml
eml# P097 traffic lights - a junction of two roads, north-south (NS) and
# east-west (EW), with a walk button, run second by second as in the corpus
# case traffic-light-simulator (phases held for set times, an index moved
# on by hand). Then an audit of the log, as in the corpus case
# state-machine-trace-audit: every second against every rule, reporting
# every violation, not just the first.
#
# A log is one entry per second: [NS, EW, walk], the lights "G", "Y" or "R",
# the walk signal "D" (don't walk), "W" (walk) or "F" (flashing).
def name(c):
{"G": "green", "Y": "yellow", "R": "red", "D": "don't walk", "W": "walk", "F": "flashing"} => names
return names[c]
def run(cfg, presses):
# cfg: [green, yellow, all red, walk, flashing, seconds to run]. The
# cars go NS green, NS yellow, all red, EW green, EW yellow, all red. A
# press of the button (not during a walk) is kept until the next all
# red ends; then walk, flashing, and on to the next green.
[["G", "R", cfg[0]], ["Y", "R", cfg[1]], ["R", "R", cfg[2]], ["R", "G", cfg[0]], ["R", "Y", cfg[1]], ["R", "R", cfg[2]]] => phases
{} => pressed
for t in presses:
True => pressed[t]
[] => log
0 => p
"D" => walk
0 => elapsed
False => pending
for t in [0:cfg[5] - 1]:
if t in pressed and walk != "W":
True => pending
if walk == "D":
log + [[phases[p][0], phases[p][1], "D"]] => log
else:
log + [["R", "R", walk]] => log
elapsed + 1 => elapsed
if walk == "W":
if elapsed == cfg[3]:
"F" => walk
0 => elapsed
elif walk == "F":
if elapsed == cfg[4]:
"D" => walk
0 => elapsed
(p + 1) % 6 => p
elif elapsed == phases[p][2]:
0 => elapsed
if (p == 2 or p == 5) and pending:
"W" => walk
False => pending
else:
(p + 1) % 6 => p
return log
def same(a, b):
return a[0] == b[0] and a[1] == b[1] and a[2] == b[2]
def runs(log):
# Seconds in a row with the same lights: [first, last, entry].
[] => out
0 => first
for t in [1:len(log)]:
if t == len(log) or not same(log[t], log[first]):
out + [[first, t - 1, log[first]]] => out
t => first
return out
def waits(log, presses):
# For each press, the second the walk shows (the press itself if it is
# already walking), or -1 if no walk comes before the log ends.
[] => out
for t in presses:
-1 => at
t => s
while at == -1 and s < len(log):
if log[s][2] == "W":
s => at
s + 1 => s
out + [[t, at]] => out
return out
def copy(log):
[] => out
for e in log:
out + [[e[0], e[1], e[2]]] => out
return out
def inject(log, fault, cfg):
# A copy of the log with one fault put in, or [] if the log has no place
# where the fault would show before it ends.
copy(log) => out
if fault == "stuck":
# NS stays green for the first 2 seconds of EW green
for t in [1:len(log) - 3]:
if log[t][1] == "G" and log[t - 1][1] == "R":
"G" => out[t][0]
"G" => out[t + 1][0]
return out
return []
if fault == "no-yellow" or fault == "short-yellow":
# NS's first yellow: shown green, or cut to 1 second with red after
-1 => first
for t in [0:len(log) - 1]:
if first == -1 and log[t][0] == "Y":
t => first
if first == -1:
return []
first => t
while t < len(log) and log[t][0] == "Y":
t + 1 => t
if t == len(log):
return []
first => t
while t < len(log) and log[t][0] == "Y":
if fault == "no-yellow":
"G" => out[t][0]
elif t > first:
"R" => out[t][0]
t + 1 => t
return out
if fault == "early-walk":
# the first walk starts a second before the all red
for t in [1:len(log) - 1]:
if log[t][2] == "W" and log[t - 1][2] == "D":
if t - cfg[2] - 1 < 0:
return []
for k in [t - cfg[2] - 1:t - 1]:
"W" => out[k][2]
return out
return []
return []
def audit(log, yellow, allred):
# Every second against every rule; returns [second, rule, what] for each
# violation, in order. 1 a light goes green, yellow, red, green only;
# 2 never both roads not red; 3 walk or flashing only while both roads
# are red; 4 the walk signal goes don't walk, walk, flashing, don't
# walk; 5 a yellow lasts at least `yellow` seconds; 6 a road turns
# green only after the other has been red for `allred` seconds. A
# yellow already showing at second 0, or one still showing at the end,
# is not timed; nor is a green before second `allred`.
{"G": "Y", "Y": "R", "R": "G"} => after
{"D": "W", "W": "F", "F": "D"} => walk_after
["NS", "EW"] => road
[] => found
[-1, -1] => ystart
for t in [0:len(log) - 1]:
log[t] => s
if t > 0:
log[t - 1] => q
for r in [0:1]:
if s[r] != q[r] and s[r] != after[q[r]]:
found + [[t, 1, road[r] + " went " + name(q[r]) + " to " + name(s[r])]] => found
if s[0] != "R" and s[1] != "R":
found + [[t, 2, "NS " + name(s[0]) + " and EW " + name(s[1]) + " at once"]] => found
if s[2] != "D":
for r in [0:1]:
if s[r] != "R" and (r == 0 or s[0] == "R"):
found + [[t, 3, name(s[2]) + " showing while " + road[r] + " is " + name(s[r])]] => found
if t > 0:
if s[2] != q[2] and s[2] != walk_after[q[2]]:
found + [[t, 4, "walk signal went " + name(q[2]) + " to " + name(s[2])]] => found
for r in [0:1]:
if q[r] == "Y" and s[r] != "Y" and ystart[r] > 0 and t - ystart[r] < yellow:
found + [[t, 5, road[r] + " yellow lasted only " + str(t - ystart[r]) + " s"]] => found
for r in [0:1]:
if q[r] == "R" and s[r] == "G" and t - allred >= 0:
1 - r => o
t - 1 => k
while k >= t - allred and log[k][o] == "R":
k - 1 => k
if k >= t - allred:
found + [[t, 6, road[r] + " turned green after only " + str(t - 1 - k) + " s of " + road[o] + " red"]] => found
for r in [0:1]:
if s[r] == "Y" and (t == 0 or log[t - 1][r] != "Y"):
t => ystart[r]
return found
def parse(text):
# "GRD YRD RRD": one entry a second, NS and EW (G, Y, R), then the walk
# signal (D, W, F); 2 to 60 of them, or [] if anything is wrong.
[] => out
"" => w
for c in text + " ":
if c == " ":
if w != "":
if len(w) != 3 or not (w[0] in {"G": 1, "Y": 1, "R": 1}) or not (w[1] in {"G": 1, "Y": 1, "R": 1}) or not (w[2] in {"D": 1, "W": 1, "F": 1}):
return []
out + [[w[0], w[1], w[2]]] => out
"" => w
else:
w + c => w
if len(out) < 2 or len(out) > 60:
return []
return out
Python projection (lights.py)
def name(c):
names = {"G": "green", "Y": "yellow", "R": "red", "D": "don't walk", "W": "walk", "F": "flashing"}
return names[c]
def run(cfg, presses):
phases = [["G", "R", cfg[0]], ["Y", "R", cfg[1]], ["R", "R", cfg[2]], ["R", "G", cfg[0]], ["R", "Y", cfg[1]], ["R", "R", cfg[2]]]
pressed = {}
for t in presses:
pressed[t] = True
log = []
p = 0
walk = "D"
elapsed = 0
pending = False
for t in range(0, cfg[5]):
if t in pressed and walk != "W":
pending = True
if walk == "D":
log = log + [[phases[p][0], phases[p][1], "D"]]
else:
log = log + [["R", "R", walk]]
elapsed = elapsed + 1
if walk == "W":
if elapsed == cfg[3]:
walk = "F"
elapsed = 0
elif walk == "F":
if elapsed == cfg[4]:
walk = "D"
elapsed = 0
p = (p + 1) % 6
elif elapsed == phases[p][2]:
elapsed = 0
if (p == 2 or p == 5) and pending:
walk = "W"
pending = False
else:
p = (p + 1) % 6
return log
def same(a, b):
return a[0] == b[0] and a[1] == b[1] and a[2] == b[2]
def runs(log):
out = []
first = 0
for t in range(1, len(log)+1):
if t == len(log) or not same(log[t], log[first]):
out = out + [[first, t - 1, log[first]]]
first = t
return out
def waits(log, presses):
out = []
for t in presses:
at = -1
s = t
while at == -1 and s < len(log):
if log[s][2] == "W":
at = s
s = s + 1
out = out + [[t, at]]
return out
def copy(log):
out = []
for e in log:
out = out + [[e[0], e[1], e[2]]]
return out
def inject(log, fault, cfg):
out = copy(log)
if fault == "stuck":
for t in range(1, len(log) - 3+1):
if log[t][1] == "G" and log[t - 1][1] == "R":
out[t][0] = "G"
out[t + 1][0] = "G"
return out
return []
if fault == "no-yellow" or fault == "short-yellow":
first = -1
for t in range(0, len(log)):
if first == -1 and log[t][0] == "Y":
first = t
if first == -1:
return []
t = first
while t < len(log) and log[t][0] == "Y":
t = t + 1
if t == len(log):
return []
t = first
while t < len(log) and log[t][0] == "Y":
if fault == "no-yellow":
out[t][0] = "G"
elif t > first:
out[t][0] = "R"
t = t + 1
return out
if fault == "early-walk":
for t in range(1, len(log)):
if log[t][2] == "W" and log[t - 1][2] == "D":
if t - cfg[2] - 1 < 0:
return []
for k in range(t - cfg[2] - 1, t):
out[k][2] = "W"
return out
return []
return []
def audit(log, yellow, allred):
after = {"G": "Y", "Y": "R", "R": "G"}
walk_after = {"D": "W", "W": "F", "F": "D"}
road = ["NS", "EW"]
found = []
ystart = [-1, -1]
for t in range(0, len(log)):
s = log[t]
if t > 0:
q = log[t - 1]
for r in range(0, 2):
if s[r] != q[r] and s[r] != after[q[r]]:
found = found + [[t, 1, road[r] + " went " + name(q[r]) + " to " + name(s[r])]]
if s[0] != "R" and s[1] != "R":
found = found + [[t, 2, "NS " + name(s[0]) + " and EW " + name(s[1]) + " at once"]]
if s[2] != "D":
for r in range(0, 2):
if s[r] != "R" and (r == 0 or s[0] == "R"):
found = found + [[t, 3, name(s[2]) + " showing while " + road[r] + " is " + name(s[r])]]
if t > 0:
if s[2] != q[2] and s[2] != walk_after[q[2]]:
found = found + [[t, 4, "walk signal went " + name(q[2]) + " to " + name(s[2])]]
for r in range(0, 2):
if q[r] == "Y" and s[r] != "Y" and ystart[r] > 0 and t - ystart[r] < yellow:
found = found + [[t, 5, road[r] + " yellow lasted only " + str(t - ystart[r]) + " s"]]
for r in range(0, 2):
if q[r] == "R" and s[r] == "G" and t - allred >= 0:
o = 1 - r
k = t - 1
while k >= t - allred and log[k][o] == "R":
k = k - 1
if k >= t - allred:
found = found + [[t, 6, road[r] + " turned green after only " + str(t - 1 - k) + " s of " + road[o] + " red"]]
for r in range(0, 2):
if s[r] == "Y" and (t == 0 or log[t - 1][r] != "Y"):
ystart[r] = t
return found
def parse(text):
out = []
w = ""
for c in text + " ":
if c == " ":
if w != "":
if len(w) != 3 or not w[0] in {"G": 1, "Y": 1, "R": 1} or not w[1] in {"G": 1, "Y": 1, "R": 1} or not w[2] in {"D": 1, "W": 1, "F": 1}:
return []
out = out + [[w[0], w[1], w[2]]]
w = ""
else:
w = w + c
if len(out) < 2 or len(out) > 60:
return []
return out